equal
deleted
inserted
replaced
6 For ex/list.thy. Examples of simplification and induction on lists |
6 For ex/list.thy. Examples of simplification and induction on lists |
7 *) |
7 *) |
8 |
8 |
9 open List; |
9 open List; |
10 |
10 |
11 val prems = goal List.thy "[| P([]); !!x l. P(x.l) |] ==> All(P)"; |
11 val prems = goal List.thy "[| P([]); !!x l. P(x. l) |] ==> All(P)"; |
12 by (rtac list_ind 1); |
12 by (rtac list_ind 1); |
13 by (REPEAT (resolve_tac (prems@[allI,impI]) 1)); |
13 by (REPEAT (resolve_tac (prems@[allI,impI]) 1)); |
14 qed "list_exh"; |
14 qed "list_exh"; |
15 |
15 |
16 Addsimps [list_distinct1, list_distinct2, app_nil, app_cons, |
16 Addsimps [list_distinct1, list_distinct2, app_nil, app_cons, |
35 |
35 |
36 goal List.thy "forall(l++l',P) <-> forall(l,P) & forall(l',P)"; |
36 goal List.thy "forall(l++l',P) <-> forall(l,P) & forall(l',P)"; |
37 by (IND_TAC list_ind Simp_tac "l" 1); |
37 by (IND_TAC list_ind Simp_tac "l" 1); |
38 qed "forall_app"; |
38 qed "forall_app"; |
39 |
39 |
40 goal List.thy "forall(l,%x.P(x)&Q(x)) <-> forall(l,P) & forall(l,Q)"; |
40 goal List.thy "forall(l,%x. P(x)&Q(x)) <-> forall(l,P) & forall(l,Q)"; |
41 by (IND_TAC list_ind Simp_tac "l" 1); |
41 by (IND_TAC list_ind Simp_tac "l" 1); |
42 by (Fast_tac 1); |
42 by (Fast_tac 1); |
43 qed "forall_conj"; |
43 qed "forall_conj"; |
44 |
44 |
45 goal List.thy "~l=[] --> forall(l,P) <-> P(hd(l)) & forall(tl(l),P)"; |
45 goal List.thy "~l=[] --> forall(l,P) <-> P(hd(l)) & forall(tl(l),P)"; |
57 by (REPEAT (rtac allI 1)); |
57 by (REPEAT (rtac allI 1)); |
58 by (rtac impI 1); |
58 by (rtac impI 1); |
59 by (ALL_IND_TAC nat_exh Asm_simp_tac 1); |
59 by (ALL_IND_TAC nat_exh Asm_simp_tac 1); |
60 qed "at_app1"; |
60 qed "at_app1"; |
61 |
61 |
62 goal List.thy "at(l1++(x.l2), len(l1)) = x"; |
62 goal List.thy "at(l1++(x. l2), len(l1)) = x"; |
63 by (IND_TAC list_ind Simp_tac "l1" 1); |
63 by (IND_TAC list_ind Simp_tac "l1" 1); |
64 qed "at_app_hd2"; |
64 qed "at_app_hd2"; |
65 |
65 |