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
|