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