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