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