Theory HaskellLib

(*  Title:      Haskell Library
    Author:     Ricardo Peña, Javier de Dios
    Copyright:  May 2008, Universidad Complutense de Madrid
*)
header {* Useful functions 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))"


thm mapAccumL.induct


primrec
  "unzip3 []         = ([],[],[])"
  "unzip3 (tup#tups) = (let (xs,ys,zs) = unzip3 tups;
                            (x,y,z)    = tup
                        in  (x#xs,y#ys,z#zs))"
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 = []"



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