Theory HaskellLib

(*  Title:      Haskell Library
    Author:     Ricardo Peña, Javier de Dios
    Copyright:  May 2008, Universidad Complutense de Madrid
*)
header {* Useful functions and theorems from the Haskell Library or Prelude *}


theory  HaskellLib
imports Main
begin


text{* Function {\sl mapAccumL} is a powerful combination of {\sl map} and
{\sl foldl}. Functions {\sl unzip3} and {\sl unzip} are respectively the
inverse of {\sl zip3} and {\sl zip}. *}



consts 
  mapAccumL :: "('a => 'b => 'a × 'c) => 'a => 'b list => 'a  × 'c list"
  zipWith   :: "('a => 'b => 'c) => 'a list => 'b list => 'c list "
  unzip3    :: "('a × 'b× 'c) list => 'a list × 'b list × 'c list"
  unzip     :: "('a × 'b) list => 'a list × 'b list"

primrec 
  "mapAccumL f s []     = (s,[])"
  "mapAccumL f s (x#xs) = (let (s',y)   = f s x;
                               (s'',ys) = mapAccumL f s' xs
                           in (s'',y#ys))"

text {* Some lemmas about mapAccumL *}

lemma mapAccumL_non_empty: 
  "[| (s'',ys) = mapAccumL f s xs;
   xs = x#xx
   |] ==> (∃ s' y ys'.
             (s',y) = f s x
             ∧ ys = y # ys')"
apply clarify
apply (unfold mapAccumL.simps)
apply (rule_tac x="fst (f s x)" in exI)
apply (rule_tac x="snd (f s x)" in exI)
apply (rule_tac x="snd (mapAccumL f (fst (f s x)) xx)" in exI)
apply (rule conjI)
apply simp
apply (case_tac "f s x",simp)
by (case_tac "mapAccumL f a xx",simp)

lemma mapAccumL_non_empty2: 
  "[| (s'',ys) = mapAccumL f s xs;
   xs = x#xx
   |] ==> (∃ s' y ys'.
             (s',y) = f s x
             ∧ (s'',ys') = mapAccumL f s' xx
             ∧ ys = y # ys')"
apply clarify
apply (unfold mapAccumL.simps)
apply (rule_tac x="fst (f s x)" in exI)
apply (rule_tac x="snd (f s x)" in exI)
apply (rule_tac x="snd (mapAccumL f (fst (f s x)) xx)" in exI)
apply (rule conjI)
apply simp
apply (rule conjI)
apply (case_tac "f s x") apply (simp)
apply (case_tac "mapAccumL f a xx")
apply (simp)
apply (case_tac "f s x") apply (simp)
apply (case_tac "mapAccumL f a xx")
apply simp
done

axioms mapAccumL_non_empty3: 
  "[| (s'',ys) = mapAccumL f s xs;
   0<length xs
   |] ==> (∃ s' y ys'.
             (s',y) = f s (xs!0)
             ∧ (s'',ys') = mapAccumL f s' (tl xs))"

axioms mapAccumL_two_elements: 
  "[| (s3,ys) = mapAccumL f s xs;
   xs = x1#x2#xx
   |] ==> (∃ s1 s2 y1 y2 ys3.
             (s1,y1) = f s x1
             ∧ (s2,y2) = f s1 x2
             ∧ (s3,ys3) = mapAccumL f s2 xx
             ∧ ys = y1#y2#ys3)"

axioms mapAccumL_split: 
  "[| (s2,ys) = mapAccumL f s xs;
     xs1 @ xs2=xs
   |] ==> (∃ s1 ys1 ys2 .
         (s1,ys1) =  mapAccumL f s xs1
         ∧ (s2,ys2) =  mapAccumL f s1 xs2
         ∧ ys = ys1 @ ys2)"

axioms mapAccumL_one_more: 
  "[| (s1,ys) = mapAccumL f s xs;
     (s2,y) = f s1 x
   |] ==> (s2,ys@[y]) =  mapAccumL f s (xs@[x])"

text {* Some integer arithmetic lemmas  *}

lemma sum_nat:
  "[| (x1::nat)=x2;(y1::nat)=y2|] ==> x1+y1=x2+y2"
apply arith
done

axioms sum_substract:
  "(x::nat)-y+(z-x)=z-y"

axioms additions1:
   "[| i< m; Suc m + n ≤ l|]  ==> 
     m - i < nat (int l - 1) - n + 1 - (nat (int l - 1) - Suc m - n + 1)"
axioms additions2:
   "[| i< m; Suc m + n ≤ l|]  ==> 
     nat (int l - 1) - m + (m - Suc i) = nat (int l - 1) - Suc m + (m - i)"
axioms additions3:
   "[| i< m; Suc m + n ≤ l|]  ==> 
     nat (int l - 1)- Suc (m + n)+(m - i)=nat (int l - 1)-(m + n)+(m - Suc i)"
axioms additions4:
   "[| Suc m + n ≤ l|]  ==> 
     nat (int l - 1) - m = Suc (nat (int l - 1) - Suc m)"
axioms additions5:
   "[| Suc m + n ≤ l|]  ==> 
    Suc (nat (int l - 1) - Suc (m + n)) = nat (int l - 1 - int n - int m)"
axioms additions6:
   "[| Suc m + n ≤ l|]  ==> 
    n + (nat (int l - 1) - Suc (m + n)) < nat (int l - 1)"


text {* Some lemmas about lists *}

lemma list_non_empty:
  "0<length xs ==> (∃ y ys . xs = y # ys)"
apply auto
apply (insert neq_Nil_conv [of xs])
by simp


axioms drop_nth:
  "n < length xs ==> (∃ y ys . drop n xs = y#ys ∧ xs!n = y)"

axioms drop_nth3:
  "n < length xs ==> drop n xs = (xs!n) # drop (Suc n) xs"

axioms drop_take_Suc:
  "xs=(take n xs)@(z#zs) ==> drop (Suc n) xs=zs"

axioms drop_nth2:
  "[| n<length xs; drop n xs = ys|]
   ==> ys = xs!n # tl ys "

axioms drop_append2:
  "[| drop n xs = zs1 @ ys1 @ ys2 @ zs2 @ rest;
    drop (m-n) (zs1 @ ys1 @ ys2 @ zs2)= ys1 @ rest'
   |] ==>  
    drop (m+length ys1-n) (zs1 @ ys1 @ ys2 @ zs2) = ys2 @ zs2"

axioms drop_append3:
  "[| drop n xs = xs1 @ rest;
    drop (m-n) xs1 = ys1 @ ys2
   |] ==>  
    drop m xs = ys1 @ ys2 @ rest"

lemma nth_via_drop_append: "drop n xs  = (y#ys)@zs ==> xs!n = y"
apply (induct xs arbitrary: n, simp)
by(simp add:drop_Cons nth_Cons split:nat.splits)

lemma drop_Suc_append:
  "drop n xs = (y#ys)@zs ==> drop (Suc n) xs = ys@zs"
apply (induct xs arbitrary: n,simp)
apply (simp add:drop_Cons)
by (simp split:nat.splits)

lemma nth_via_drop_append_2: "drop n xs  = ((y # ys) @ ws @ zs) @ ms ==> xs!n = y"
apply (induct xs arbitrary: n, simp)
by(simp add:drop_Cons nth_Cons split:nat.splits)

lemma drop_Suc_append_2:
  "drop n xs = ((y # ys) @ ws @ zs) @ ms ==> drop (Suc n) xs = ys @ ws @ zs @ ms"
apply (induct xs arbitrary: n,simp)
apply (simp add:drop_Cons)
by (simp split:nat.splits)

axioms drop_append_length:
  "drop n xs = [] @ ys @ zs @ ms ==> drop (n + length ys) xs = zs @ ms"

axioms take_length:
  "n ≤ length xs ==> n = length (take n xs)"

axioms take_append2:
  "n<length xs ==> x # take n xs = take n (x # xs) @ [(x # xs)!n]"

axioms take_append3:
  "Suc n ≤ length xs ==> take (Suc n) xs = take n xs @ [xs!n]"

axioms concat1:
  "xs @ y # ys = (xs @ [y]) @ ys"

axioms concat2:
  "xs1 = xs2 ==> xs1 @ ys = xs2 @ ys "

axioms upt_length:
  "n ≤ m ==> length [n..<m]=m-n"


text {* Some lemmas about finite maps *}

axioms map_of_distinct:
  "[| distinct (map fst xys);
   l < length xys;
   (x,y) = xys ! l
   |] ==> map_of xys x = Some y"

axioms map_of_distinct2:
  "map_of xys x = Some y 
   ==> (∃ l . l < length xys ∧ (x,y) = xys ! l)"

axioms map_upds_nth:
  "i < m-n ==> (A([n..<m] [\<mapsto>] xs)) (n+i) = Some (xs ! i)"

-- "The unzip3 function of Haskell library"

primrec
  "unzip3 []         = ([],[],[])"
  "unzip3 (tup#tups) = (let (xs,ys,zs) = unzip3 tups;
                            (x,y,z)    = tup
                        in  (x#xs,y#ys,z#zs))"

axioms unzip3_length:
  "unzip3 xs = (ys1,ys2,ys3) ==> length ys1 = length ys2"

primrec
  "unzip []         = ([],[])"
  "unzip (tup#tups) = (let (xs,ys) = unzip tups;
                           (x,y)    = tup
                       in  (x#xs,y#ys))"

primrec
  "zipWith f (x#xs) yy = (case yy of
                           []   => []
                         | y#ys => f x y # zipWith f xs ys)"
  "zipWith f []     yy = []"


axioms zipWith_length:
  "length (zipWith f xs ys) = min (length xs) (length ys)"

-- "The Haskell sum type Either"

datatype ('a,'b) Either = Left 'a | Right 'b

-- "insertion sort for list of strings"


constdefs
  leString :: "string => string  => bool"
  "leString s1 s2 == True"

(*
primrec 
  "leList []     ts = True"
  "leList (s#ss) ts = (case ts of []   => False
                                | t#tt => (s <  t ∨ s=t ∧ leList ss tt))" 
*)

consts 
  ins :: "string => string list => string list"
primrec
  "ins s []      = [s]"
  "ins s (s'#ss) = (if leString s s' then s#s'#ss
                   else s'# ins s ss)"

fun sort :: "string list => string list"
where
  "sort ss = foldr ins ss []"


fun subList :: "'a list => 'a list => bool" 
where
  "subList xs ys = (∃ hs ts. ys = hs @ xs @ ts)"

end