author | berghofe |
Tue, 30 Jul 1996 17:33:26 +0200 | |
changeset 1894 | c2c8279d40f0 |
parent 1673 | d22110ddd0af |
child 1985 | 84cf16192e03 |
permissions | -rw-r--r-- |
1051 | 1 |
(* Title: HOL/IOA/NTP/Lemmas.ML |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow & Konrad Slind |
|
4 |
Copyright 1994 TU Muenchen |
|
5 |
||
6 |
(Mostly) Arithmetic lemmas |
|
7 |
Should realy go in Arith.ML. |
|
8 |
Also: Get rid of all the --> in favour of ==> !!! |
|
9 |
*) |
|
10 |
||
11 |
(* Logic *) |
|
12 |
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R"; |
|
1894 | 13 |
by(fast_tac (!claset addDs prems) 1); |
1051 | 14 |
qed "imp_conj_lemma"; |
15 |
||
16 |
goal HOL.thy "(P --> (? x. Q(x))) = (? x. P --> Q(x))"; |
|
1894 | 17 |
by(Fast_tac 1); |
1051 | 18 |
qed "imp_ex_equiv"; |
19 |
||
20 |
goal HOL.thy "(A --> B & C) = ((A --> B) & (A --> C))"; |
|
1894 | 21 |
by (Fast_tac 1); |
1051 | 22 |
qed "fork_lemma"; |
23 |
||
24 |
goal HOL.thy "((A --> B) & (C --> B)) = ((A | C) --> B)"; |
|
1894 | 25 |
by (Fast_tac 1); |
1051 | 26 |
qed "imp_or_lem"; |
27 |
||
28 |
goal HOL.thy "(X = (~ Y)) = ((~X) = Y)"; |
|
1894 | 29 |
by (Fast_tac 1); |
1051 | 30 |
qed "neg_flip"; |
31 |
||
32 |
goal HOL.thy "P --> Q(M) --> Q(if P then M else N)"; |
|
33 |
by (rtac impI 1); |
|
34 |
by (rtac impI 1); |
|
35 |
by (rtac (expand_if RS iffD2) 1); |
|
1894 | 36 |
by (Fast_tac 1); |
1051 | 37 |
qed "imp_true_decompose"; |
38 |
||
39 |
goal HOL.thy "(~P) --> Q(N) --> Q(if P then M else N)"; |
|
40 |
by (rtac impI 1); |
|
41 |
by (rtac impI 1); |
|
42 |
by (rtac (expand_if RS iffD2) 1); |
|
1894 | 43 |
by (Fast_tac 1); |
1051 | 44 |
qed "imp_false_decompose"; |
45 |
||
46 |
||
47 |
(* Sets *) |
|
48 |
val set_lemmas = |
|
1894 | 49 |
map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1])) |
1051 | 50 |
["f(x) : (UN x. {f(x)})", |
51 |
"f x y : (UN x y. {f x y})", |
|
52 |
"!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})", |
|
53 |
"!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"]; |
|
54 |
||
55 |
||
56 |
(* Arithmetic *) |
|
57 |
goal Arith.thy "n ~= 0 --> Suc(m+pred(n)) = m+n"; |
|
58 |
by (nat_ind_tac "n" 1); |
|
1266 | 59 |
by (REPEAT(Simp_tac 1)); |
1051 | 60 |
val Suc_pred_lemma = store_thm("Suc_pred_lemma", result() RS mp); |
61 |
||
62 |
goal Arith.thy "((m::nat) + n = m + p) = (n = p)"; |
|
63 |
by (nat_ind_tac "m" 1); |
|
1266 | 64 |
by (Simp_tac 1); |
65 |
by (Asm_simp_tac 1); |
|
1051 | 66 |
qed "left_plus_cancel"; |
67 |
||
68 |
goal Arith.thy "((x::nat) + y = Suc(x + z)) = (y = Suc(z))"; |
|
69 |
by (nat_ind_tac "x" 1); |
|
1266 | 70 |
by (Simp_tac 1); |
71 |
by (Asm_simp_tac 1); |
|
1051 | 72 |
qed "left_plus_cancel_inside_succ"; |
73 |
||
74 |
goal Arith.thy "(x ~= 0) = (? y. x = Suc(y))"; |
|
75 |
by (nat_ind_tac "x" 1); |
|
1266 | 76 |
by (Simp_tac 1); |
77 |
by (Asm_simp_tac 1); |
|
1894 | 78 |
by (Fast_tac 1); |
1051 | 79 |
qed "nonzero_is_succ"; |
80 |
||
81 |
goal Arith.thy "(m::nat) < n --> m + p < n + p"; |
|
82 |
by (nat_ind_tac "p" 1); |
|
1266 | 83 |
by (Simp_tac 1); |
84 |
by (Asm_simp_tac 1); |
|
1051 | 85 |
qed "less_add_same_less"; |
86 |
||
87 |
goal Arith.thy "(x::nat)<= y --> x<=y+k"; |
|
88 |
by (nat_ind_tac "k" 1); |
|
1266 | 89 |
by (Simp_tac 1); |
1328 | 90 |
by (Asm_full_simp_tac 1); |
1051 | 91 |
qed "leq_add_leq"; |
92 |
||
93 |
goal Arith.thy "(x::nat) + y <= z --> x <= z"; |
|
94 |
by (nat_ind_tac "y" 1); |
|
1266 | 95 |
by (Simp_tac 1); |
96 |
by (Asm_simp_tac 1); |
|
1051 | 97 |
by (rtac impI 1); |
98 |
by (dtac Suc_leD 1); |
|
1894 | 99 |
by (Fast_tac 1); |
1051 | 100 |
qed "left_add_leq"; |
101 |
||
102 |
goal Arith.thy "(A::nat) < B --> C < D --> A + C < B + D"; |
|
103 |
by (rtac impI 1); |
|
104 |
by (rtac impI 1); |
|
105 |
by (rtac less_trans 1); |
|
106 |
by (rtac (less_add_same_less RS mp) 1); |
|
107 |
by (assume_tac 1); |
|
108 |
by (rtac (add_commute RS ssubst)1);; |
|
109 |
by (res_inst_tac [("m1","B")] (add_commute RS ssubst) 1); |
|
110 |
by (rtac (less_add_same_less RS mp) 1); |
|
111 |
by (assume_tac 1); |
|
112 |
qed "less_add_cong"; |
|
113 |
||
114 |
goal Arith.thy "(A::nat) <= B --> C <= D --> A + C <= B + D"; |
|
115 |
by (rtac impI 1); |
|
116 |
by (rtac impI 1); |
|
1266 | 117 |
by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); |
1894 | 118 |
by (safe_tac (!claset)); |
1051 | 119 |
by (rtac (less_add_cong RS mp RS mp) 1); |
120 |
by (assume_tac 1); |
|
121 |
by (assume_tac 1); |
|
122 |
by (rtac (less_add_same_less RS mp) 1); |
|
123 |
by (assume_tac 1); |
|
124 |
by (rtac (add_commute RS ssubst)1);; |
|
125 |
by (res_inst_tac [("m1","B")] (add_commute RS ssubst) 1); |
|
126 |
by (rtac (less_add_same_less RS mp) 1); |
|
127 |
by (assume_tac 1); |
|
128 |
qed "less_eq_add_cong"; |
|
129 |
||
130 |
goal Arith.thy "(w <= y) --> ((x::nat) + y <= z) --> (x + w <= z)"; |
|
131 |
by (rtac impI 1); |
|
132 |
by (dtac (less_eq_add_cong RS mp) 1); |
|
133 |
by (cut_facts_tac [le_refl] 1); |
|
134 |
by (dres_inst_tac [("P","x<=x")] mp 1);by (assume_tac 1); |
|
1266 | 135 |
by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1); |
1051 | 136 |
by (rtac impI 1); |
137 |
by (etac le_trans 1); |
|
138 |
by (assume_tac 1); |
|
139 |
qed "leq_add_left_cong"; |
|
140 |
||
141 |
goal Arith.thy "(? x. y = Suc(x)) = (~(y = 0))"; |
|
142 |
by (nat_ind_tac "y" 1); |
|
1266 | 143 |
by (Simp_tac 1); |
1051 | 144 |
by (rtac iffI 1); |
1266 | 145 |
by (Asm_full_simp_tac 1); |
1894 | 146 |
by (Fast_tac 1); |
1051 | 147 |
qed "suc_not_zero"; |
148 |
||
149 |
goal Arith.thy "Suc(x) <= y --> (? z. y = Suc(z))"; |
|
150 |
by (rtac impI 1); |
|
1266 | 151 |
by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); |
1894 | 152 |
by (safe_tac (!claset)); |
153 |
by (Fast_tac 2); |
|
1266 | 154 |
by (asm_simp_tac (!simpset addsimps [suc_not_zero]) 1); |
1051 | 155 |
qed "suc_leq_suc"; |
156 |
||
157 |
goal Arith.thy "~0<n --> n = 0"; |
|
158 |
by (nat_ind_tac "n" 1); |
|
1266 | 159 |
by (Asm_simp_tac 1); |
1894 | 160 |
by (safe_tac (!claset)); |
1266 | 161 |
by (Asm_full_simp_tac 1); |
162 |
by (Asm_full_simp_tac 1); |
|
1051 | 163 |
qed "zero_eq"; |
164 |
||
165 |
goal Arith.thy "x < Suc(y) --> x<=y"; |
|
166 |
by (nat_ind_tac "n" 1); |
|
1673
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
167 |
by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1); |
1894 | 168 |
by (safe_tac (!claset)); |
1051 | 169 |
by (etac less_imp_le 1); |
170 |
qed "less_suc_imp_leq"; |
|
171 |
||
172 |
goal Arith.thy "0<x --> Suc(pred(x)) = x"; |
|
173 |
by (nat_ind_tac "x" 1); |
|
1266 | 174 |
by (Simp_tac 1); |
175 |
by (Asm_simp_tac 1); |
|
1051 | 176 |
qed "suc_pred_id"; |
177 |
||
178 |
goal Arith.thy "0<x --> (pred(x) = y) = (x = Suc(y))"; |
|
179 |
by (nat_ind_tac "x" 1); |
|
1266 | 180 |
by (Simp_tac 1); |
181 |
by (Asm_simp_tac 1); |
|
1051 | 182 |
qed "pred_suc"; |
183 |
||
184 |
goal Arith.thy "(x ~= 0) = (0<x)"; |
|
185 |
by (nat_ind_tac "x" 1); |
|
1266 | 186 |
by (Simp_tac 1); |
187 |
by (Asm_simp_tac 1); |
|
1051 | 188 |
qed "unzero_less"; |
189 |
||
190 |
(* Odd proof. Why do induction? *) |
|
191 |
goal Arith.thy "((x::nat) = y + z) --> (y <= x)"; |
|
192 |
by (nat_ind_tac "y" 1); |
|
1266 | 193 |
by (Simp_tac 1); |
194 |
by (simp_tac (!simpset addsimps [le_refl RS (leq_add_leq RS mp)]) 1); |
|
1051 | 195 |
qed "plus_leq_lem"; |
196 |
||
197 |
(* Lists *) |
|
198 |
||
1266 | 199 |
val list_ss = simpset_of "List"; |
200 |
||
1051 | 201 |
goal List.thy "(xs @ (y#ys)) ~= []"; |
202 |
by (list.induct_tac "xs" 1); |
|
203 |
by (simp_tac list_ss 1); |
|
204 |
by (asm_simp_tac list_ss 1); |
|
205 |
qed "append_cons"; |
|
206 |
||
207 |
goal List.thy "(x ~= hd(xs@ys)) = (x ~= (if xs = [] then hd ys else hd xs))"; |
|
208 |
by (list.induct_tac "xs" 1); |
|
209 |
by (simp_tac list_ss 1); |
|
210 |
by (asm_full_simp_tac list_ss 1); |
|
211 |
qed "not_hd_append"; |
|
212 |
||
1328 | 213 |
|
1465 | 214 |
Addsimps ([append_cons,not_hd_append,Suc_pred_lemma] @ set_lemmas); |