|
1 (* Title: FOL/ex/list |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 For ex/list.thy. Examples of simplification and induction on lists |
|
7 *) |
|
8 |
|
9 open List; |
|
10 |
|
11 val prems = goal List.thy "[| P([]); !!x l. P(x.l) |] ==> All(P)"; |
|
12 by (rtac list_ind 1); |
|
13 by (REPEAT (resolve_tac (prems@[allI,impI]) 1)); |
|
14 val list_exh = result(); |
|
15 |
|
16 val list_rew_thms = [list_distinct1,list_distinct2,app_nil,app_cons, |
|
17 hd_eq,tl_eq,forall_nil,forall_cons,list_free, |
|
18 len_nil,len_cons,at_0,at_succ]; |
|
19 |
|
20 val list_ss = nat_ss addsimps list_rew_thms; |
|
21 |
|
22 goal List.thy "~l=[] --> hd(l).tl(l) = l"; |
|
23 by(IND_TAC list_exh (simp_tac list_ss) "l" 1); |
|
24 result(); |
|
25 |
|
26 goal List.thy "(l1++l2)++l3 = l1++(l2++l3)"; |
|
27 by(IND_TAC list_ind (simp_tac list_ss) "l1" 1); |
|
28 val append_assoc = result(); |
|
29 |
|
30 goal List.thy "l++[] = l"; |
|
31 by(IND_TAC list_ind (simp_tac list_ss) "l" 1); |
|
32 val app_nil_right = result(); |
|
33 |
|
34 goal List.thy "l1++l2=[] <-> l1=[] & l2=[]"; |
|
35 by(IND_TAC list_exh (simp_tac list_ss) "l1" 1); |
|
36 val app_eq_nil_iff = result(); |
|
37 |
|
38 goal List.thy "forall(l++l',P) <-> forall(l,P) & forall(l',P)"; |
|
39 by(IND_TAC list_ind (simp_tac list_ss) "l" 1); |
|
40 val forall_app = result(); |
|
41 |
|
42 goal List.thy "forall(l,%x.P(x)&Q(x)) <-> forall(l,P) & forall(l,Q)"; |
|
43 by(IND_TAC list_ind (simp_tac list_ss) "l" 1); |
|
44 by(fast_tac FOL_cs 1); |
|
45 val forall_conj = result(); |
|
46 |
|
47 goal List.thy "~l=[] --> forall(l,P) <-> P(hd(l)) & forall(tl(l),P)"; |
|
48 by(IND_TAC list_ind (simp_tac list_ss) "l" 1); |
|
49 val forall_ne = result(); |
|
50 |
|
51 (*** Lists with natural numbers ***) |
|
52 |
|
53 goal List.thy "len(l1++l2) = len(l1)+len(l2)"; |
|
54 by (IND_TAC list_ind (simp_tac list_ss) "l1" 1); |
|
55 val len_app = result(); |
|
56 |
|
57 goal List.thy "i<len(l1) --> at(l1++l2,i) = at(l1,i)"; |
|
58 by (IND_TAC list_ind (simp_tac list_ss) "l1" 1); |
|
59 by (REPEAT (rtac allI 1)); |
|
60 by (rtac impI 1); |
|
61 by (ALL_IND_TAC nat_exh (asm_simp_tac list_ss) 1); |
|
62 val at_app1 = result(); |
|
63 |
|
64 goal List.thy "at(l1++(x.l2), len(l1)) = x"; |
|
65 by (IND_TAC list_ind (simp_tac list_ss) "l1" 1); |
|
66 val at_app_hd2 = result(); |
|
67 |