The Theory list
 Parents

 Children

 char
 Constants
 IsListRep (( 'a) ) BOOL Cons 'a 'a LIST 'a LIST [] 'a LIST Length 'a LIST Hd 'a LIST 'a Tl 'a LIST 'a LIST Append 'a LIST 'a LIST 'a LIST Rev 'a LIST 'a LIST Split ('a 'b) LIST 'a LIST 'b LIST Combine 'a LIST 'b LIST ('a 'b) LIST Map ('a 'b) 'a LIST 'b LIST Fold ('a 'b 'b) 'a LIST 'b 'b
 Aliases
 @ Append : 'a LIST 'a LIST 'a LIST
 Types
 '1 LIST
 Fixity

 Infix 300: @
 Definitions
 IsListRep is_list_rep_def mk_var("nil", (( 'a) )) mk_var("cons", ('a (( 'a) ) ( 'a) )) IsListRep mk_var("nil", (( 'a) )) ( x IsListRep x ( h mk_var("cons", ('a (( 'a) ) ( 'a) )) h x = mk_var("nil", ( 'a) ))) ( x y IsListRep x IsListRep y ( a b mk_var("cons", ('a (( 'a) ) ( 'a) )) a x = mk_var("cons", ('a (( 'a) ) ( 'a) )) b y a = b x = y)) ( x IsListRep x ( h IsListRep (mk_var("cons", ('a (( 'a) ) ( 'a) )) h x))) ( p p mk_var("nil", (( 'a) )) ( m p m ( h p (mk_var("cons", ('a (( 'a) ) ( 'a) )) h m))) ( n IsListRep n p n)) LIST list_def f TypeDefn IsListRep f Nil Cons nil_cons_def ( x mk_var("list", 'a LIST) Cons x mk_var("list", 'a LIST) = []) ( x1 x2 list1 list2 Cons x1 list1 = Cons x2 list2 x1 = x2 list1 = list2) ( p p [] ( mk_var("list", 'a LIST) p mk_var("list", 'a LIST) ( x p (Cons x mk_var("list", 'a LIST)))) ( mk_var("list", 'a LIST) p mk_var("list", 'a LIST))) Length length_def Length [] = 0 ( h mk_var("list", 'a LIST) Length (Cons h mk_var("list", 'a LIST)) = Length mk_var("list", 'a LIST) + 1) Hd hd_def h mk_var("list", 'a LIST) Hd (Cons h mk_var("list", 'a LIST)) = h Tl tl_def h mk_var("list", 'a LIST) Tl (Cons h mk_var("list", 'a LIST)) = mk_var("list", 'a LIST) Append append_def ( mk_var("list", 'a LIST) [] @ mk_var("list", 'a LIST) = mk_var("list", 'a LIST)) ( h mk_var("list", 'a LIST) list' Cons h mk_var("list", 'a LIST) @ list' = Cons h (mk_var("list", 'a LIST) @ list')) Rev rev_def Rev [] = [] ( h mk_var("list", 'a LIST) Rev (Cons h mk_var("list", 'a LIST)) = Rev mk_var("list", 'a LIST) @ [h]) Split split_def Split [] = ([], []) ( mk_var("list", ('a 'b) LIST) h1 h2 Split (Cons (h1, h2) mk_var("list", ('a 'b) LIST)) = (Cons h1 (Fst (Split mk_var("list", ('a 'b) LIST))), Cons h2 (Snd (Split mk_var("list", ('a 'b) LIST))))) Combine combine_def Combine [] [] = [] ( h1 h2 list1 list2 Combine (Cons h1 list1) (Cons h2 list2) = Cons (h1, h2) (Combine list1 list2)) Map map_def ( g Map g [] = []) ( h g mk_var("list", 'a LIST) Map g (Cons h mk_var("list", 'a LIST)) = Cons (g h) (Map g mk_var("list", 'a LIST))) Fold fold_def ( g x Fold g [] x = x) ( h g x mk_var("list", 'a LIST) Fold g (Cons h mk_var("list", 'a LIST)) x = g h (Fold g mk_var("list", 'a LIST) x))
 Theorems
 list_induction_thm p p [] ( mk_var("list", 'a LIST) p mk_var("list", 'a LIST) ( x p (Cons x mk_var("list", 'a LIST)))) ( mk_var("list", 'a LIST) p mk_var("list", 'a LIST)) list_prim_rec_thm n c 1 f f [] = n ( mk_var("list", 'a LIST) a f (Cons a mk_var("list", 'a LIST)) = c a (f mk_var("list", 'a LIST)) mk_var("list", 'a LIST)) list_clauses x1 x2 list1 list2 Cons x1 list1 = [] [] = Cons x1 list1 (Cons x1 list1 = Cons x2 list2 x1 = x2 list1 = list2) Hd (Cons x1 list1) = x1 Tl (Cons x1 list1) = list1 list_cases_thm list1 list1 = [] ( x list2 list1 = Cons x list2)