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