1473

1 
(* Title: FOL/ex/list

0

2 
ID: $Id$

1473

3 
Author: Tobias Nipkow

0

4 
Copyright 1991 University of Cambridge


5 
*)


6 

17245

7 
header {* Examples of simplification and induction on lists *}

0

8 

17245

9 
theory List


10 
imports Nat2


11 
begin


12 


13 
typedecl 'a list


14 
arities list :: ("term") "term"

0

15 


16 
consts

17245

17 
hd :: "'a list => 'a"


18 
tl :: "'a list => 'a list"


19 
forall :: "['a list, 'a => o] => o"


20 
len :: "'a list => nat"


21 
at :: "['a list, nat] => 'a"


22 
Nil :: "'a list" ("[]")


23 
Cons :: "['a, 'a list] => 'a list" (infixr "." 80)


24 
app :: "['a list, 'a list] => 'a list" (infixr "++" 70)

0

25 

17245

26 
axioms


27 
list_ind: "[ P([]); ALL x l. P(l)>P(x . l) ] ==> All(P)"

0

28 

17245

29 
forall_cong:

0

30 
"[ l = l'; !!x. P(x)<>P'(x) ] ==> forall(l,P) <> forall(l',P')"


31 

17245

32 
list_distinct1: "~[] = x . l"


33 
list_distinct2: "~x . l = []"


34 


35 
list_free: "x . l = x' . l' <> x=x' & l=l'"

0

36 

17245

37 
app_nil: "[]++l = l"


38 
app_cons: "(x . l)++l' = x .(l++l')"


39 
tl_eq: "tl(m . q) = q"


40 
hd_eq: "hd(m . q) = m"

0

41 

17245

42 
forall_nil: "forall([],P)"


43 
forall_cons: "forall(x . l,P) <> P(x) & forall(l,P)"

0

44 

17245

45 
len_nil: "len([]) = 0"


46 
len_cons: "len(m . q) = succ(len(q))"

0

47 

17245

48 
at_0: "at(m . q,0) = m"


49 
at_succ: "at(m . q,succ(n)) = at(q,n)"

0

50 

17245

51 
ML {* use_legacy_bindings (the_context ()) *}

0

52 


53 
end
