|
clasohm@0
|
1 |
(* Title: FOL/ex/list
|
|
clasohm@0
|
2 |
ID: $Id$
|
|
clasohm@0
|
3 |
Author: Tobias Nipkow
|
|
clasohm@0
|
4 |
Copyright 1991 University of Cambridge
|
|
clasohm@0
|
5 |
|
|
clasohm@0
|
6 |
Examples of simplification and induction on lists
|
|
clasohm@0
|
7 |
*)
|
|
clasohm@0
|
8 |
|
|
clasohm@0
|
9 |
List = Nat2 +
|
|
clasohm@0
|
10 |
|
|
lcp@352
|
11 |
types 'a list
|
|
clasohm@0
|
12 |
arities list :: (term)term
|
|
clasohm@0
|
13 |
|
|
clasohm@0
|
14 |
consts
|
|
clasohm@0
|
15 |
hd :: "'a list => 'a"
|
|
clasohm@0
|
16 |
tl :: "'a list => 'a list"
|
|
clasohm@0
|
17 |
forall :: "['a list, 'a => o] => o"
|
|
clasohm@0
|
18 |
len :: "'a list => nat"
|
|
clasohm@0
|
19 |
at :: "['a list, nat] => 'a"
|
|
clasohm@0
|
20 |
"[]" :: "'a list" ("[]")
|
|
clasohm@0
|
21 |
"." :: "['a, 'a list] => 'a list" (infixr 80)
|
|
clasohm@0
|
22 |
"++" :: "['a list, 'a list] => 'a list" (infixr 70)
|
|
clasohm@0
|
23 |
|
|
clasohm@0
|
24 |
rules
|
|
clasohm@0
|
25 |
list_ind "[| P([]); ALL x l. P(l)-->P(x.l) |] ==> All(P)"
|
|
clasohm@0
|
26 |
|
|
clasohm@0
|
27 |
forall_cong
|
|
clasohm@0
|
28 |
"[| l = l'; !!x. P(x)<->P'(x) |] ==> forall(l,P) <-> forall(l',P')"
|
|
clasohm@0
|
29 |
|
|
clasohm@0
|
30 |
list_distinct1 "~[] = x.l"
|
|
clasohm@0
|
31 |
list_distinct2 "~x.l = []"
|
|
clasohm@0
|
32 |
|
|
clasohm@0
|
33 |
list_free "x.l = x'.l' <-> x=x' & l=l'"
|
|
clasohm@0
|
34 |
|
|
clasohm@0
|
35 |
app_nil "[]++l = l"
|
|
clasohm@0
|
36 |
app_cons "(x.l)++l' = x.(l++l')"
|
|
clasohm@0
|
37 |
tl_eq "tl(m.q) = q"
|
|
clasohm@0
|
38 |
hd_eq "hd(m.q) = m"
|
|
clasohm@0
|
39 |
|
|
clasohm@0
|
40 |
forall_nil "forall([],P)"
|
|
clasohm@0
|
41 |
forall_cons "forall(x.l,P) <-> P(x) & forall(l,P)"
|
|
clasohm@0
|
42 |
|
|
clasohm@0
|
43 |
len_nil "len([]) = 0"
|
|
clasohm@0
|
44 |
len_cons "len(m.q) = succ(len(q))"
|
|
clasohm@0
|
45 |
|
|
clasohm@0
|
46 |
at_0 "at(m.q,0) = m"
|
|
clasohm@0
|
47 |
at_succ "at(m.q,succ(n)) = at(q,n)"
|
|
clasohm@0
|
48 |
|
|
clasohm@0
|
49 |
end
|