author | paulson |
Thu, 26 Sep 1996 12:47:47 +0200 | |
changeset 2031 | 03a843f0f447 |
parent 1875 | 54c0462f8fb2 |
child 3040 | 7d48671753da |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/Hoare/Arith2.ML |
1335 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Norbert Galm |
1335 | 4 |
Copyright 1995 TUM |
5 |
||
6 |
More arithmetic lemmas. |
|
7 |
*) |
|
8 |
||
9 |
open Arith2; |
|
10 |
||
11 |
||
12 |
(*** HOL lemmas ***) |
|
13 |
||
14 |
||
15 |
val [prem1,prem2]=goal HOL.thy "[|~P ==> ~Q; Q|] ==> P"; |
|
16 |
by (cut_facts_tac [prem1 COMP impI,prem2] 1); |
|
1875 | 17 |
by (Fast_tac 1); |
1335 | 18 |
val not_imp_swap=result(); |
19 |
||
20 |
||
21 |
(*** analogue of diff_induct, for simultaneous induction over 3 vars ***) |
|
22 |
||
23 |
val prems = goal Nat.thy |
|
24 |
"[| !!x. P x 0 0; \ |
|
25 |
\ !!y. P 0 (Suc y) 0; \ |
|
26 |
\ !!z. P 0 0 (Suc z); \ |
|
27 |
\ !!x y. [| P x y 0 |] ==> P (Suc x) (Suc y) 0; \ |
|
28 |
\ !!x z. [| P x 0 z |] ==> P (Suc x) 0 (Suc z); \ |
|
29 |
\ !!y z. [| P 0 y z |] ==> P 0 (Suc y) (Suc z); \ |
|
30 |
\ !!x y z. [| P x y z |] ==> P (Suc x) (Suc y) (Suc z) \ |
|
31 |
\ |] ==> P m n k"; |
|
32 |
by (res_inst_tac [("x","m")] spec 1); |
|
2031 | 33 |
by (rtac diff_induct 1); |
34 |
by (rtac allI 1); |
|
35 |
by (rtac allI 2); |
|
1335 | 36 |
by (res_inst_tac [("m","xa"),("n","x")] diff_induct 1); |
37 |
by (res_inst_tac [("m","x"),("n","Suc y")] diff_induct 4); |
|
2031 | 38 |
by (rtac allI 7); |
1335 | 39 |
by (nat_ind_tac "xa" 7); |
40 |
by (ALLGOALS (resolve_tac prems)); |
|
2031 | 41 |
by (assume_tac 1); |
42 |
by (assume_tac 1); |
|
1875 | 43 |
by (Fast_tac 1); |
44 |
by (Fast_tac 1); |
|
1335 | 45 |
qed "diff_induct3"; |
46 |
||
47 |
(*** interaction of + and - ***) |
|
48 |
||
49 |
val prems=goal Arith.thy "~m<n+k ==> (m - n) - k = m - ((n + k)::nat)"; |
|
50 |
by (cut_facts_tac prems 1); |
|
2031 | 51 |
by (rtac mp 1); |
52 |
by (assume_tac 2); |
|
1335 | 53 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
54 |
by (ALLGOALS Asm_simp_tac); |
|
55 |
qed "diff_not_assoc"; |
|
56 |
||
57 |
val prems=goal Arith.thy "[|~m<n; ~n<k|] ==> (m - n) + k = m - ((n - k)::nat)"; |
|
58 |
by (cut_facts_tac prems 1); |
|
2031 | 59 |
by (dtac conjI 1); |
60 |
by (assume_tac 1); |
|
1335 | 61 |
by (res_inst_tac [("P","~m<n & ~n<k")] mp 1); |
2031 | 62 |
by (assume_tac 2); |
1335 | 63 |
by (res_inst_tac [("m","m"),("n","n"),("k","k")] diff_induct3 1); |
64 |
by (ALLGOALS Asm_simp_tac); |
|
2031 | 65 |
by (rtac impI 1); |
1335 | 66 |
by (dres_inst_tac [("P","~x<y")] conjE 1); |
2031 | 67 |
by (assume_tac 2); |
68 |
by (rtac (Suc_diff_n RS sym) 1); |
|
69 |
by (rtac le_less_trans 1); |
|
70 |
by (etac (not_less_eq RS subst) 2); |
|
71 |
by (rtac (hd ([diff_less_Suc RS lessD] RL [Suc_le_mono RS subst])) 1); |
|
1335 | 72 |
qed "diff_add_not_assoc"; |
73 |
||
74 |
val prems=goal Arith.thy "~n<k ==> (m + n) - k = m + ((n - k)::nat)"; |
|
75 |
by (cut_facts_tac prems 1); |
|
2031 | 76 |
by (rtac mp 1); |
77 |
by (assume_tac 2); |
|
1335 | 78 |
by (res_inst_tac [("m","n"),("n","k")] diff_induct 1); |
79 |
by (ALLGOALS Asm_simp_tac); |
|
80 |
qed "add_diff_assoc"; |
|
81 |
||
82 |
(*** more ***) |
|
83 |
||
84 |
val prems = goal Arith.thy "m~=(n::nat) = (m<n | n<m)"; |
|
2031 | 85 |
by (rtac iffI 1); |
1335 | 86 |
by (cut_inst_tac [("m","m"),("n","n")] less_linear 1); |
87 |
by (Asm_full_simp_tac 1); |
|
2031 | 88 |
by (etac disjE 1); |
89 |
by (etac (less_not_refl2 RS not_sym) 1); |
|
90 |
by (etac less_not_refl2 1); |
|
1335 | 91 |
qed "not_eq_eq_less_or_gr"; |
92 |
||
93 |
val [prem] = goal Arith.thy "m<n ==> n-m~=0"; |
|
94 |
by (rtac (prem RS rev_mp) 1); |
|
95 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
|
96 |
by (ALLGOALS Asm_simp_tac); |
|
97 |
qed "less_imp_diff_not_0"; |
|
98 |
||
99 |
(*******************************************************************) |
|
100 |
||
1714
1a5e0101399d
Deleted diff_mult_distrib_r as diff_mult_distrib is not proved in Arith.
paulson
parents:
1476
diff
changeset
|
101 |
(** Some of these are now proved, with different names, in HOL/Arith.ML **) |
1a5e0101399d
Deleted diff_mult_distrib_r as diff_mult_distrib is not proved in Arith.
paulson
parents:
1476
diff
changeset
|
102 |
|
1335 | 103 |
val prems = goal Arith.thy "(i::nat)<j ==> k+i<k+j"; |
104 |
by (cut_facts_tac prems 1); |
|
105 |
by (nat_ind_tac "k" 1); |
|
106 |
by (ALLGOALS Asm_simp_tac); |
|
107 |
qed "add_less_mono_l"; |
|
108 |
||
109 |
val prems = goal Arith.thy "~(i::nat)<j ==> ~k+i<k+j"; |
|
110 |
by (cut_facts_tac prems 1); |
|
111 |
by (nat_ind_tac "k" 1); |
|
112 |
by (ALLGOALS Asm_simp_tac); |
|
113 |
qed "add_not_less_mono_l"; |
|
114 |
||
115 |
val prems = goal Arith.thy "[|0<k; m<(n::nat)|] ==> m*k<n*k"; |
|
116 |
by (cut_facts_tac prems 1); |
|
117 |
by (res_inst_tac [("n","k")] natE 1); |
|
118 |
by (ALLGOALS Asm_full_simp_tac); |
|
119 |
by (nat_ind_tac "x" 1); |
|
2031 | 120 |
by (etac add_less_mono 2); |
1335 | 121 |
by (ALLGOALS Asm_full_simp_tac); |
122 |
qed "mult_less_mono_r"; |
|
123 |
||
124 |
val prems = goal Arith.thy "~m<(n::nat) ==> ~m*k<n*k"; |
|
125 |
by (cut_facts_tac prems 1); |
|
126 |
by (nat_ind_tac "k" 1); |
|
127 |
by (ALLGOALS Simp_tac); |
|
128 |
by (fold_goals_tac [le_def]); |
|
2031 | 129 |
by (etac add_le_mono 1); |
130 |
by (assume_tac 1); |
|
1335 | 131 |
qed "mult_not_less_mono_r"; |
132 |
||
133 |
val prems = goal Arith.thy "m=(n::nat) ==> m*k=n*k"; |
|
134 |
by (cut_facts_tac prems 1); |
|
135 |
by (nat_ind_tac "k" 1); |
|
136 |
by (ALLGOALS Asm_simp_tac); |
|
137 |
qed "mult_eq_mono_r"; |
|
138 |
||
139 |
val prems = goal Arith.thy "[|0<k; m~=(n::nat)|] ==> m*k~=n*k"; |
|
140 |
by (cut_facts_tac prems 1); |
|
141 |
by (res_inst_tac [("P","m<n"),("Q","n<m")] disjE 1); |
|
2031 | 142 |
by (rtac (less_not_refl2 RS not_sym) 2); |
143 |
by (etac mult_less_mono_r 2); |
|
144 |
by (rtac less_not_refl2 3); |
|
145 |
by (etac mult_less_mono_r 3); |
|
1335 | 146 |
by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [not_eq_eq_less_or_gr]))); |
147 |
qed "mult_not_eq_mono_r"; |
|
148 |
||
149 |
(******************************************************************) |
|
150 |
||
151 |
(*** mod ***) |
|
152 |
||
1476 | 153 |
goal Arith.thy "(%m. m mod n) = wfrec (trancl pred_nat) \ |
154 |
\ (%f j. if j<n then j else f (j-n))"; |
|
155 |
by (simp_tac (HOL_ss addsimps [mod_def]) 1); |
|
156 |
val mod_def = result() RS eq_reflection; |
|
157 |
||
1335 | 158 |
(* Alternativ-Beweis zu mod_nn_is_0: Spezialfall zu mod_prod_nn_is_0 *) |
159 |
(* |
|
160 |
val prems = goal thy "0<n ==> n mod n = 0"; |
|
161 |
by (cut_inst_tac [("m","Suc(0)")] (mod_prod_nn_is_0 COMP impI) 1); |
|
162 |
by (cut_facts_tac prems 1); |
|
163 |
by (Asm_full_simp_tac 1); |
|
1875 | 164 |
by (Fast_tac 1); |
1335 | 165 |
*) |
166 |
||
167 |
val prems=goal thy "0<n ==> n mod n = 0"; |
|
168 |
by (cut_facts_tac prems 1); |
|
2031 | 169 |
by (rtac (mod_def RS wf_less_trans) 1); |
1335 | 170 |
by (asm_full_simp_tac ((simpset_of "Arith") addsimps [diff_self_eq_0,cut_def,less_eq]) 1); |
2031 | 171 |
by (etac mod_less 1); |
1335 | 172 |
qed "mod_nn_is_0"; |
173 |
||
174 |
val prems=goal thy "0<n ==> m mod n = (m+n) mod n"; |
|
175 |
by (cut_facts_tac prems 1); |
|
176 |
by (res_inst_tac [("s","n+m"),("t","m+n")] subst 1); |
|
2031 | 177 |
by (rtac add_commute 1); |
1335 | 178 |
by (res_inst_tac [("s","n+m-n"),("P","%x.x mod n = (n + m) mod n")] subst 1); |
2031 | 179 |
by (rtac diff_add_inverse 1); |
180 |
by (rtac sym 1); |
|
181 |
by (etac mod_geq 1); |
|
1335 | 182 |
by (res_inst_tac [("s","n<=n+m"),("t","~n+m<n")] subst 1); |
183 |
by (simp_tac ((simpset_of "Arith") addsimps [le_def]) 1); |
|
2031 | 184 |
by (rtac le_add1 1); |
1335 | 185 |
qed "mod_eq_add"; |
186 |
||
187 |
val prems=goal thy "0<n ==> m*n mod n = 0"; |
|
188 |
by (cut_facts_tac prems 1); |
|
189 |
by (nat_ind_tac "m" 1); |
|
190 |
by (Simp_tac 1); |
|
2031 | 191 |
by (etac mod_less 1); |
1335 | 192 |
by (dres_inst_tac [("n","n"),("m","m1*n")] mod_eq_add 1); |
193 |
by (asm_full_simp_tac ((simpset_of "Arith") addsimps [add_commute]) 1); |
|
194 |
qed "mod_prod_nn_is_0"; |
|
195 |
||
196 |
val prems=goal thy "[|0<x; m mod x = 0; n mod x = 0|] ==> (m+n) mod x = 0"; |
|
197 |
by (cut_facts_tac prems 1); |
|
198 |
by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1); |
|
2031 | 199 |
by (etac mod_div_equality 1); |
1335 | 200 |
by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1); |
2031 | 201 |
by (etac mod_div_equality 1); |
1335 | 202 |
by (Asm_simp_tac 1); |
203 |
by (res_inst_tac [("s","(m div x + n div x) * x"),("t","m div x * x + n div x * x")] subst 1); |
|
2031 | 204 |
by (rtac add_mult_distrib 1); |
205 |
by (etac mod_prod_nn_is_0 1); |
|
1335 | 206 |
qed "mod0_sum"; |
207 |
||
208 |
val prems=goal thy "[|0<x; m mod x = 0; n mod x = 0; n<=m|] ==> (m-n) mod x = 0"; |
|
209 |
by (cut_facts_tac prems 1); |
|
210 |
by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1); |
|
2031 | 211 |
by (etac mod_div_equality 1); |
1335 | 212 |
by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1); |
2031 | 213 |
by (etac mod_div_equality 1); |
1335 | 214 |
by (Asm_simp_tac 1); |
215 |
by (res_inst_tac [("s","(m div x - n div x) * x"),("t","m div x * x - n div x * x")] subst 1); |
|
2031 | 216 |
by (rtac diff_mult_distrib 1); |
217 |
by (etac mod_prod_nn_is_0 1); |
|
1335 | 218 |
qed "mod0_diff"; |
219 |
||
220 |
||
221 |
(*** div ***) |
|
222 |
||
1476 | 223 |
|
1335 | 224 |
val prems = goal thy "0<n ==> m*n div n = m"; |
225 |
by (cut_facts_tac prems 1); |
|
2031 | 226 |
by (rtac (mult_not_eq_mono_r RS not_imp_swap) 1); |
227 |
by (assume_tac 1); |
|
228 |
by (assume_tac 1); |
|
1335 | 229 |
by (res_inst_tac [("P","%x.m*n div n * n = x")] (mod_div_equality RS subst) 1); |
2031 | 230 |
by (assume_tac 1); |
1335 | 231 |
by (dres_inst_tac [("m","m")] mod_prod_nn_is_0 1); |
232 |
by (Asm_simp_tac 1); |
|
233 |
qed "div_prod_nn_is_m"; |
|
234 |
||
235 |
||
236 |
(*** divides ***) |
|
237 |
||
238 |
val prems=goalw thy [divides_def] "0<n ==> n divides n"; |
|
239 |
by (cut_facts_tac prems 1); |
|
240 |
by (forward_tac [mod_nn_is_0] 1); |
|
241 |
by (Asm_simp_tac 1); |
|
242 |
qed "divides_nn"; |
|
243 |
||
244 |
val prems=goalw thy [divides_def] "x divides n ==> x<=n"; |
|
245 |
by (cut_facts_tac prems 1); |
|
2031 | 246 |
by (rtac ((mod_less COMP rev_contrapos) RS (le_def RS meta_eq_to_obj_eq RS iffD2)) 1); |
1335 | 247 |
by (Asm_simp_tac 1); |
2031 | 248 |
by (rtac (less_not_refl2 RS not_sym) 1); |
1335 | 249 |
by (Asm_simp_tac 1); |
250 |
qed "divides_le"; |
|
251 |
||
252 |
val prems=goalw thy [divides_def] "[|x divides m; x divides n|] ==> x divides (m+n)"; |
|
253 |
by (cut_facts_tac prems 1); |
|
254 |
by (REPEAT ((dtac conjE 1) THEN (atac 2))); |
|
2031 | 255 |
by (rtac conjI 1); |
1335 | 256 |
by (dres_inst_tac [("m","0"),("n","m")] less_imp_add_less 1); |
2031 | 257 |
by (assume_tac 1); |
258 |
by (etac conjI 1); |
|
259 |
by (rtac mod0_sum 1); |
|
1335 | 260 |
by (ALLGOALS atac); |
261 |
qed "divides_sum"; |
|
262 |
||
263 |
val prems=goalw thy [divides_def] "[|x divides m; x divides n; n<m|] ==> x divides (m-n)"; |
|
264 |
by (cut_facts_tac prems 1); |
|
265 |
by (REPEAT ((dtac conjE 1) THEN (atac 2))); |
|
2031 | 266 |
by (rtac conjI 1); |
267 |
by (etac less_imp_diff_positive 1); |
|
268 |
by (etac conjI 1); |
|
269 |
by (rtac mod0_diff 1); |
|
1335 | 270 |
by (ALLGOALS (asm_simp_tac ((simpset_of "Arith") addsimps [le_def]))); |
2031 | 271 |
by (etac less_not_sym 1); |
1335 | 272 |
qed "divides_diff"; |
273 |
||
274 |
||
275 |
(*** cd ***) |
|
276 |
||
277 |
||
278 |
val prems=goalw thy [cd_def] "0<n ==> cd n n n"; |
|
279 |
by (cut_facts_tac prems 1); |
|
2031 | 280 |
by (dtac divides_nn 1); |
1335 | 281 |
by (Asm_simp_tac 1); |
282 |
qed "cd_nnn"; |
|
283 |
||
284 |
val prems=goalw thy [cd_def] "cd x m n ==> x<=m & x<=n"; |
|
285 |
by (cut_facts_tac prems 1); |
|
2031 | 286 |
by (dtac conjE 1); |
287 |
by (assume_tac 2); |
|
288 |
by (dtac divides_le 1); |
|
289 |
by (dtac divides_le 1); |
|
1335 | 290 |
by (Asm_simp_tac 1); |
291 |
qed "cd_le"; |
|
292 |
||
293 |
val prems=goalw thy [cd_def] "cd x m n = cd x n m"; |
|
1875 | 294 |
by (Fast_tac 1); |
1335 | 295 |
qed "cd_swap"; |
296 |
||
297 |
val prems=goalw thy [cd_def] "n<m ==> cd x m n = cd x (m-n) n"; |
|
298 |
by (cut_facts_tac prems 1); |
|
2031 | 299 |
by (rtac iffI 1); |
300 |
by (dtac conjE 1); |
|
301 |
by (assume_tac 2); |
|
302 |
by (rtac conjI 1); |
|
303 |
by (rtac divides_diff 1); |
|
304 |
by (dtac conjE 5); |
|
305 |
by (assume_tac 6); |
|
306 |
by (rtac conjI 5); |
|
307 |
by (dtac less_not_sym 5); |
|
308 |
by (dtac add_diff_inverse 5); |
|
1335 | 309 |
by (dres_inst_tac [("m","n"),("n","m-n")] divides_sum 5); |
310 |
by (ALLGOALS Asm_full_simp_tac); |
|
311 |
qed "cd_diff_l"; |
|
312 |
||
313 |
val prems=goalw thy [cd_def] "m<n ==> cd x m n = cd x m (n-m)"; |
|
314 |
by (cut_facts_tac prems 1); |
|
2031 | 315 |
by (rtac iffI 1); |
316 |
by (dtac conjE 1); |
|
317 |
by (assume_tac 2); |
|
318 |
by (rtac conjI 1); |
|
319 |
by (rtac divides_diff 2); |
|
320 |
by (dtac conjE 5); |
|
321 |
by (assume_tac 6); |
|
322 |
by (rtac conjI 5); |
|
323 |
by (dtac less_not_sym 6); |
|
324 |
by (dtac add_diff_inverse 6); |
|
1335 | 325 |
by (dres_inst_tac [("n","n-m")] divides_sum 6); |
326 |
by (ALLGOALS Asm_full_simp_tac); |
|
327 |
qed "cd_diff_r"; |
|
328 |
||
329 |
||
330 |
(*** gcd ***) |
|
331 |
||
332 |
val prems = goalw thy [gcd_def] "0<n ==> n = gcd n n"; |
|
333 |
by (cut_facts_tac prems 1); |
|
2031 | 334 |
by (dtac cd_nnn 1); |
335 |
by (rtac (select_equality RS sym) 1); |
|
336 |
by (etac conjI 1); |
|
337 |
by (rtac allI 1); |
|
338 |
by (rtac impI 1); |
|
339 |
by (dtac cd_le 1); |
|
340 |
by (dtac conjE 2); |
|
341 |
by (assume_tac 3); |
|
342 |
by (rtac le_anti_sym 2); |
|
1335 | 343 |
by (dres_inst_tac [("x","x")] cd_le 2); |
344 |
by (dres_inst_tac [("x","n")] spec 3); |
|
345 |
by (ALLGOALS Asm_full_simp_tac); |
|
346 |
qed "gcd_nnn"; |
|
347 |
||
348 |
val prems = goalw thy [gcd_def] "gcd m n = gcd n m"; |
|
349 |
by (simp_tac ((simpset_of "Arith") addsimps [cd_swap]) 1); |
|
350 |
qed "gcd_swap"; |
|
351 |
||
352 |
val prems=goalw thy [gcd_def] "n<m ==> gcd m n = gcd (m-n) n"; |
|
353 |
by (cut_facts_tac prems 1); |
|
354 |
by (subgoal_tac "n<m ==> !x.cd x m n = cd x (m-n) n" 1); |
|
355 |
by (Asm_simp_tac 1); |
|
2031 | 356 |
by (rtac allI 1); |
357 |
by (etac cd_diff_l 1); |
|
1335 | 358 |
qed "gcd_diff_l"; |
359 |
||
360 |
val prems=goalw thy [gcd_def] "m<n ==> gcd m n = gcd m (n-m)"; |
|
361 |
by (cut_facts_tac prems 1); |
|
362 |
by (subgoal_tac "m<n ==> !x.cd x m n = cd x m (n-m)" 1); |
|
363 |
by (Asm_simp_tac 1); |
|
2031 | 364 |
by (rtac allI 1); |
365 |
by (etac cd_diff_r 1); |
|
1335 | 366 |
qed "gcd_diff_r"; |
367 |
||
368 |
||
369 |
(*** pow ***) |
|
370 |
||
371 |
val [pow_0,pow_Suc] = nat_recs pow_def; |
|
372 |
store_thm("pow_0",pow_0); |
|
373 |
store_thm("pow_Suc",pow_Suc); |
|
374 |
||
375 |
goalw thy [pow_def] "m pow (n+k) = m pow n * m pow k"; |
|
376 |
by (nat_ind_tac "k" 1); |
|
377 |
by (ALLGOALS (asm_simp_tac ((simpset_of "Arith") addsimps [mult_left_commute]))); |
|
378 |
qed "pow_add_reduce"; |
|
379 |
||
380 |
goalw thy [pow_def] "m pow n pow k = m pow (n*k)"; |
|
381 |
by (nat_ind_tac "k" 1); |
|
382 |
by (ALLGOALS Asm_simp_tac); |
|
383 |
by (fold_goals_tac [pow_def]); |
|
2031 | 384 |
by (rtac (pow_add_reduce RS sym) 1); |
1335 | 385 |
qed "pow_pow_reduce"; |
386 |
||
387 |
(*** fac ***) |
|
388 |
||
389 |
Addsimps(nat_recs fac_def); |