33 by (ALLGOALS Asm_simp_tac); |
33 by (ALLGOALS Asm_simp_tac); |
34 qed "pred_le"; |
34 qed "pred_le"; |
35 AddIffs [pred_le]; |
35 AddIffs [pred_le]; |
36 |
36 |
37 goalw Arith.thy [pred_def] "m<=n --> pred(m) <= pred(n)"; |
37 goalw Arith.thy [pred_def] "m<=n --> pred(m) <= pred(n)"; |
38 by(simp_tac (!simpset addsplits [expand_nat_case]) 1); |
38 by(simp_tac (simpset() addsplits [expand_nat_case]) 1); |
39 qed_spec_mp "pred_le_mono"; |
39 qed_spec_mp "pred_le_mono"; |
40 |
40 |
41 goal Arith.thy "!!n. n ~= 0 ==> pred n < n"; |
41 goal Arith.thy "!!n. n ~= 0 ==> pred n < n"; |
42 by(exhaust_tac "n" 1); |
42 by(exhaust_tac "n" 1); |
43 by(ALLGOALS Asm_full_simp_tac); |
43 by(ALLGOALS Asm_full_simp_tac); |
138 (**** Additional theorems about "less than" ****) |
138 (**** Additional theorems about "less than" ****) |
139 |
139 |
140 goal Arith.thy "i<j --> (EX k. j = Suc(i+k))"; |
140 goal Arith.thy "i<j --> (EX k. j = Suc(i+k))"; |
141 by (induct_tac "j" 1); |
141 by (induct_tac "j" 1); |
142 by (Simp_tac 1); |
142 by (Simp_tac 1); |
143 by (blast_tac (!claset addSEs [less_SucE] |
143 by (blast_tac (claset() addSEs [less_SucE] |
144 addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1); |
144 addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1); |
145 val lemma = result(); |
145 val lemma = result(); |
146 |
146 |
147 (* [| i<j; !!x. j = Suc(i+x) ==> Q |] ==> Q *) |
147 (* [| i<j; !!x. j = Suc(i+x) ==> Q |] ==> Q *) |
148 bind_thm ("less_natE", lemma RS mp RS exE); |
148 bind_thm ("less_natE", lemma RS mp RS exE); |
149 |
149 |
150 goal Arith.thy "!!m. m<n --> (? k. n=Suc(m+k))"; |
150 goal Arith.thy "!!m. m<n --> (? k. n=Suc(m+k))"; |
151 by (induct_tac "n" 1); |
151 by (induct_tac "n" 1); |
152 by (ALLGOALS (simp_tac (!simpset addsimps [less_Suc_eq]))); |
152 by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq]))); |
153 by (blast_tac (!claset addSEs [less_SucE] |
153 by (blast_tac (claset() addSEs [less_SucE] |
154 addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1); |
154 addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1); |
155 qed_spec_mp "less_eq_Suc_add"; |
155 qed_spec_mp "less_eq_Suc_add"; |
156 |
156 |
157 goal Arith.thy "n <= ((m + n)::nat)"; |
157 goal Arith.thy "n <= ((m + n)::nat)"; |
158 by (induct_tac "m" 1); |
158 by (induct_tac "m" 1); |
160 by (etac le_trans 1); |
160 by (etac le_trans 1); |
161 by (rtac (lessI RS less_imp_le) 1); |
161 by (rtac (lessI RS less_imp_le) 1); |
162 qed "le_add2"; |
162 qed "le_add2"; |
163 |
163 |
164 goal Arith.thy "n <= ((n + m)::nat)"; |
164 goal Arith.thy "n <= ((n + m)::nat)"; |
165 by (simp_tac (!simpset addsimps add_ac) 1); |
165 by (simp_tac (simpset() addsimps add_ac) 1); |
166 by (rtac le_add2 1); |
166 by (rtac le_add2 1); |
167 qed "le_add1"; |
167 qed "le_add1"; |
168 |
168 |
169 bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans))); |
169 bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans))); |
170 bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans))); |
170 bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans))); |
183 |
183 |
184 goal Arith.thy "!!i. i+j < (k::nat) ==> i<k"; |
184 goal Arith.thy "!!i. i+j < (k::nat) ==> i<k"; |
185 by (etac rev_mp 1); |
185 by (etac rev_mp 1); |
186 by (induct_tac "j" 1); |
186 by (induct_tac "j" 1); |
187 by (ALLGOALS Asm_simp_tac); |
187 by (ALLGOALS Asm_simp_tac); |
188 by (blast_tac (!claset addDs [Suc_lessD]) 1); |
188 by (blast_tac (claset() addDs [Suc_lessD]) 1); |
189 qed "add_lessD1"; |
189 qed "add_lessD1"; |
190 |
190 |
191 goal Arith.thy "!!i::nat. ~ (i+j < i)"; |
191 goal Arith.thy "!!i::nat. ~ (i+j < i)"; |
192 by (rtac notI 1); |
192 by (rtac notI 1); |
193 by (etac (add_lessD1 RS less_irrefl) 1); |
193 by (etac (add_lessD1 RS less_irrefl) 1); |
194 qed "not_add_less1"; |
194 qed "not_add_less1"; |
195 |
195 |
196 goal Arith.thy "!!i::nat. ~ (j+i < i)"; |
196 goal Arith.thy "!!i::nat. ~ (j+i < i)"; |
197 by (simp_tac (!simpset addsimps [add_commute, not_add_less1]) 1); |
197 by (simp_tac (simpset() addsimps [add_commute, not_add_less1]) 1); |
198 qed "not_add_less2"; |
198 qed "not_add_less2"; |
199 AddIffs [not_add_less1, not_add_less2]; |
199 AddIffs [not_add_less1, not_add_less2]; |
200 |
200 |
201 goal Arith.thy "!!k::nat. m <= n ==> m <= n+k"; |
201 goal Arith.thy "!!k::nat. m <= n ==> m <= n+k"; |
202 by (etac le_trans 1); |
202 by (etac le_trans 1); |
209 qed "less_imp_add_less"; |
209 qed "less_imp_add_less"; |
210 |
210 |
211 goal Arith.thy "m+k<=n --> m<=(n::nat)"; |
211 goal Arith.thy "m+k<=n --> m<=(n::nat)"; |
212 by (induct_tac "k" 1); |
212 by (induct_tac "k" 1); |
213 by (ALLGOALS Asm_simp_tac); |
213 by (ALLGOALS Asm_simp_tac); |
214 by (blast_tac (!claset addDs [Suc_leD]) 1); |
214 by (blast_tac (claset() addDs [Suc_leD]) 1); |
215 qed_spec_mp "add_leD1"; |
215 qed_spec_mp "add_leD1"; |
216 |
216 |
217 goal Arith.thy "!!n::nat. m+k<=n ==> k<=n"; |
217 goal Arith.thy "!!n::nat. m+k<=n ==> k<=n"; |
218 by (full_simp_tac (!simpset addsimps [add_commute]) 1); |
218 by (full_simp_tac (simpset() addsimps [add_commute]) 1); |
219 by (etac add_leD1 1); |
219 by (etac add_leD1 1); |
220 qed_spec_mp "add_leD2"; |
220 qed_spec_mp "add_leD2"; |
221 |
221 |
222 goal Arith.thy "!!n::nat. m+k<=n ==> m<=n & k<=n"; |
222 goal Arith.thy "!!n::nat. m+k<=n ==> m<=n & k<=n"; |
223 by (blast_tac (!claset addDs [add_leD1, add_leD2]) 1); |
223 by (blast_tac (claset() addDs [add_leD1, add_leD2]) 1); |
224 bind_thm ("add_leE", result() RS conjE); |
224 bind_thm ("add_leE", result() RS conjE); |
225 |
225 |
226 goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n"; |
226 goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n"; |
227 by (safe_tac (!claset addSDs [less_eq_Suc_add])); |
227 by (safe_tac (claset() addSDs [less_eq_Suc_add])); |
228 by (asm_full_simp_tac |
228 by (asm_full_simp_tac |
229 (!simpset delsimps [add_Suc_right] |
229 (simpset() delsimps [add_Suc_right] |
230 addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1); |
230 addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1); |
231 by (etac subst 1); |
231 by (etac subst 1); |
232 by (simp_tac (!simpset addsimps [less_add_Suc1]) 1); |
232 by (simp_tac (simpset() addsimps [less_add_Suc1]) 1); |
233 qed "less_add_eq_less"; |
233 qed "less_add_eq_less"; |
234 |
234 |
235 |
235 |
236 (*** Monotonicity of Addition ***) |
236 (*** Monotonicity of Addition ***) |
237 |
237 |
253 val [lt_mono,le] = goal Arith.thy |
253 val [lt_mono,le] = goal Arith.thy |
254 "[| !!i j::nat. i<j ==> f(i) < f(j); \ |
254 "[| !!i j::nat. i<j ==> f(i) < f(j); \ |
255 \ i <= j \ |
255 \ i <= j \ |
256 \ |] ==> f(i) <= (f(j)::nat)"; |
256 \ |] ==> f(i) <= (f(j)::nat)"; |
257 by (cut_facts_tac [le] 1); |
257 by (cut_facts_tac [le] 1); |
258 by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); |
258 by (asm_full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1); |
259 by (blast_tac (!claset addSIs [lt_mono]) 1); |
259 by (blast_tac (claset() addSIs [lt_mono]) 1); |
260 qed "less_mono_imp_le_mono"; |
260 qed "less_mono_imp_le_mono"; |
261 |
261 |
262 (*non-strict, in 1st argument*) |
262 (*non-strict, in 1st argument*) |
263 goal Arith.thy "!!i j k::nat. i<=j ==> i + k <= j + k"; |
263 goal Arith.thy "!!i j k::nat. i<=j ==> i + k <= j + k"; |
264 by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1); |
264 by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1); |
267 qed "add_le_mono1"; |
267 qed "add_le_mono1"; |
268 |
268 |
269 (*non-strict, in both arguments*) |
269 (*non-strict, in both arguments*) |
270 goal Arith.thy "!!k l::nat. [|i<=j; k<=l |] ==> i + k <= j + l"; |
270 goal Arith.thy "!!k l::nat. [|i<=j; k<=l |] ==> i + k <= j + l"; |
271 by (etac (add_le_mono1 RS le_trans) 1); |
271 by (etac (add_le_mono1 RS le_trans) 1); |
272 by (simp_tac (!simpset addsimps [add_commute]) 1); |
272 by (simp_tac (simpset() addsimps [add_commute]) 1); |
273 (*j moves to the end because it is free while k, l are bound*) |
273 (*j moves to the end because it is free while k, l are bound*) |
274 by (etac add_le_mono1 1); |
274 by (etac add_le_mono1 1); |
275 qed "add_le_mono"; |
275 qed "add_le_mono"; |
276 |
276 |
277 |
277 |
282 (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]); |
282 (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]); |
283 |
283 |
284 (*right successor law for multiplication*) |
284 (*right successor law for multiplication*) |
285 qed_goal "mult_Suc_right" Arith.thy "m * Suc(n) = m + (m * n)" |
285 qed_goal "mult_Suc_right" Arith.thy "m * Suc(n) = m + (m * n)" |
286 (fn _ => [induct_tac "m" 1, |
286 (fn _ => [induct_tac "m" 1, |
287 ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]); |
287 ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]); |
288 |
288 |
289 Addsimps [mult_0_right, mult_Suc_right]; |
289 Addsimps [mult_0_right, mult_Suc_right]; |
290 |
290 |
291 goal Arith.thy "1 * n = n"; |
291 goal Arith.thy "1 * n = n"; |
292 by (Asm_simp_tac 1); |
292 by (Asm_simp_tac 1); |
301 (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]); |
301 (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]); |
302 |
302 |
303 (*addition distributes over multiplication*) |
303 (*addition distributes over multiplication*) |
304 qed_goal "add_mult_distrib" Arith.thy "(m + n)*k = (m*k) + ((n*k)::nat)" |
304 qed_goal "add_mult_distrib" Arith.thy "(m + n)*k = (m*k) + ((n*k)::nat)" |
305 (fn _ => [induct_tac "m" 1, |
305 (fn _ => [induct_tac "m" 1, |
306 ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]); |
306 ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]); |
307 |
307 |
308 qed_goal "add_mult_distrib2" Arith.thy "k*(m + n) = (k*m) + ((k*n)::nat)" |
308 qed_goal "add_mult_distrib2" Arith.thy "k*(m + n) = (k*m) + ((k*n)::nat)" |
309 (fn _ => [induct_tac "m" 1, |
309 (fn _ => [induct_tac "m" 1, |
310 ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]); |
310 ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]); |
311 |
311 |
312 (*Associative law for multiplication*) |
312 (*Associative law for multiplication*) |
313 qed_goal "mult_assoc" Arith.thy "(m * n) * k = m * ((n * k)::nat)" |
313 qed_goal "mult_assoc" Arith.thy "(m * n) * k = m * ((n * k)::nat)" |
314 (fn _ => [induct_tac "m" 1, |
314 (fn _ => [induct_tac "m" 1, |
315 ALLGOALS (asm_simp_tac (!simpset addsimps [add_mult_distrib]))]); |
315 ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib]))]); |
316 |
316 |
317 qed_goal "mult_left_commute" Arith.thy "x*(y*z) = y*((x*z)::nat)" |
317 qed_goal "mult_left_commute" Arith.thy "x*(y*z) = y*((x*z)::nat)" |
318 (fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1, |
318 (fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1, |
319 rtac mult_assoc 1, rtac (mult_commute RS arg_cong) 1]); |
319 rtac mult_assoc 1, rtac (mult_commute RS arg_cong) 1]); |
320 |
320 |
343 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
343 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
344 by (ALLGOALS Asm_simp_tac); |
344 by (ALLGOALS Asm_simp_tac); |
345 qed_spec_mp "add_diff_inverse"; |
345 qed_spec_mp "add_diff_inverse"; |
346 |
346 |
347 goal Arith.thy "!!m. n<=m ==> n+(m-n) = (m::nat)"; |
347 goal Arith.thy "!!m. n<=m ==> n+(m-n) = (m::nat)"; |
348 by (asm_simp_tac (!simpset addsimps [add_diff_inverse, not_less_iff_le]) 1); |
348 by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1); |
349 qed "le_add_diff_inverse"; |
349 qed "le_add_diff_inverse"; |
350 |
350 |
351 goal Arith.thy "!!m. n<=m ==> (m-n)+n = (m::nat)"; |
351 goal Arith.thy "!!m. n<=m ==> (m-n)+n = (m::nat)"; |
352 by (asm_simp_tac (!simpset addsimps [le_add_diff_inverse, add_commute]) 1); |
352 by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1); |
353 qed "le_add_diff_inverse2"; |
353 qed "le_add_diff_inverse2"; |
354 |
354 |
355 Addsimps [le_add_diff_inverse, le_add_diff_inverse2]; |
355 Addsimps [le_add_diff_inverse, le_add_diff_inverse2]; |
356 Delsimps [diff_Suc]; |
356 Delsimps [diff_Suc]; |
357 |
357 |
365 qed "Suc_diff_n"; |
365 qed "Suc_diff_n"; |
366 |
366 |
367 goal Arith.thy "m - n < Suc(m)"; |
367 goal Arith.thy "m - n < Suc(m)"; |
368 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
368 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
369 by (etac less_SucE 3); |
369 by (etac less_SucE 3); |
370 by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq]))); |
370 by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq]))); |
371 qed "diff_less_Suc"; |
371 qed "diff_less_Suc"; |
372 |
372 |
373 goal Arith.thy "!!m::nat. m - n <= m"; |
373 goal Arith.thy "!!m::nat. m - n <= m"; |
374 by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1); |
374 by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1); |
375 by (ALLGOALS Asm_simp_tac); |
375 by (ALLGOALS Asm_simp_tac); |
381 by (ALLGOALS Asm_simp_tac); |
381 by (ALLGOALS Asm_simp_tac); |
382 qed "diff_diff_left"; |
382 qed "diff_diff_left"; |
383 |
383 |
384 (*This and the next few suggested by Florian Kammueller*) |
384 (*This and the next few suggested by Florian Kammueller*) |
385 goal Arith.thy "!!i::nat. i-j-k = i-k-j"; |
385 goal Arith.thy "!!i::nat. i-j-k = i-k-j"; |
386 by (simp_tac (!simpset addsimps [diff_diff_left, add_commute]) 1); |
386 by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1); |
387 qed "diff_commute"; |
387 qed "diff_commute"; |
388 |
388 |
389 goal Arith.thy "!!i j k:: nat. k<=j --> j<=i --> i - (j - k) = i - j + k"; |
389 goal Arith.thy "!!i j k:: nat. k<=j --> j<=i --> i - (j - k) = i - j + k"; |
390 by (res_inst_tac [("m","i"),("n","j")] diff_induct 1); |
390 by (res_inst_tac [("m","i"),("n","j")] diff_induct 1); |
391 by (ALLGOALS Asm_simp_tac); |
391 by (ALLGOALS Asm_simp_tac); |
392 by (asm_simp_tac |
392 by (asm_simp_tac |
393 (!simpset addsimps [Suc_diff_n, le_imp_less_Suc, le_Suc_eq]) 1); |
393 (simpset() addsimps [Suc_diff_n, le_imp_less_Suc, le_Suc_eq]) 1); |
394 qed_spec_mp "diff_diff_right"; |
394 qed_spec_mp "diff_diff_right"; |
395 |
395 |
396 goal Arith.thy "!!i j k:: nat. k<=j --> (i + j) - k = i + (j - k)"; |
396 goal Arith.thy "!!i j k:: nat. k<=j --> (i + j) - k = i + (j - k)"; |
397 by (res_inst_tac [("m","j"),("n","k")] diff_induct 1); |
397 by (res_inst_tac [("m","j"),("n","k")] diff_induct 1); |
398 by (ALLGOALS Asm_simp_tac); |
398 by (ALLGOALS Asm_simp_tac); |
403 by (ALLGOALS Asm_simp_tac); |
403 by (ALLGOALS Asm_simp_tac); |
404 qed "diff_add_inverse"; |
404 qed "diff_add_inverse"; |
405 Addsimps [diff_add_inverse]; |
405 Addsimps [diff_add_inverse]; |
406 |
406 |
407 goal Arith.thy "!!n::nat.(m+n) - n = m"; |
407 goal Arith.thy "!!n::nat.(m+n) - n = m"; |
408 by (simp_tac (!simpset addsimps [diff_add_assoc]) 1); |
408 by (simp_tac (simpset() addsimps [diff_add_assoc]) 1); |
409 qed "diff_add_inverse2"; |
409 qed "diff_add_inverse2"; |
410 Addsimps [diff_add_inverse2]; |
410 Addsimps [diff_add_inverse2]; |
411 |
411 |
412 goal Arith.thy "!!i j k::nat. i<=j ==> (j-i=k) = (j=k+i)"; |
412 goal Arith.thy "!!i j k::nat. i<=j ==> (j-i=k) = (j=k+i)"; |
413 by Safe_tac; |
413 by Safe_tac; |
415 qed "le_imp_diff_is_add"; |
415 qed "le_imp_diff_is_add"; |
416 |
416 |
417 val [prem] = goal Arith.thy "m < Suc(n) ==> m-n = 0"; |
417 val [prem] = goal Arith.thy "m < Suc(n) ==> m-n = 0"; |
418 by (rtac (prem RS rev_mp) 1); |
418 by (rtac (prem RS rev_mp) 1); |
419 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
419 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
420 by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1); |
420 by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1); |
421 by (ALLGOALS Asm_simp_tac); |
421 by (ALLGOALS Asm_simp_tac); |
422 qed "less_imp_diff_is_0"; |
422 qed "less_imp_diff_is_0"; |
423 |
423 |
424 val prems = goal Arith.thy "m-n = 0 --> n-m = 0 --> m=n"; |
424 val prems = goal Arith.thy "m-n = 0 --> n-m = 0 --> m=n"; |
425 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
425 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
431 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
431 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
432 by (ALLGOALS Asm_simp_tac); |
432 by (ALLGOALS Asm_simp_tac); |
433 qed "less_imp_diff_positive"; |
433 qed "less_imp_diff_positive"; |
434 |
434 |
435 goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))"; |
435 goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))"; |
436 by (simp_tac (!simpset addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n] |
436 by (simp_tac (simpset() addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n] |
437 addsplits [expand_if]) 1); |
437 addsplits [expand_if]) 1); |
438 qed "if_Suc_diff_n"; |
438 qed "if_Suc_diff_n"; |
439 |
439 |
440 goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)"; |
440 goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)"; |
441 by (res_inst_tac [("m","k"),("n","i")] diff_induct 1); |
441 by (res_inst_tac [("m","k"),("n","i")] diff_induct 1); |
454 qed "diff_cancel"; |
454 qed "diff_cancel"; |
455 Addsimps [diff_cancel]; |
455 Addsimps [diff_cancel]; |
456 |
456 |
457 goal Arith.thy "!!m::nat. (m+k) - (n+k) = m - n"; |
457 goal Arith.thy "!!m::nat. (m+k) - (n+k) = m - n"; |
458 val add_commute_k = read_instantiate [("n","k")] add_commute; |
458 val add_commute_k = read_instantiate [("n","k")] add_commute; |
459 by (asm_simp_tac (!simpset addsimps ([add_commute_k])) 1); |
459 by (asm_simp_tac (simpset() addsimps ([add_commute_k])) 1); |
460 qed "diff_cancel2"; |
460 qed "diff_cancel2"; |
461 Addsimps [diff_cancel2]; |
461 Addsimps [diff_cancel2]; |
462 |
462 |
463 (*From Clemens Ballarin*) |
463 (*From Clemens Ballarin*) |
464 goal Arith.thy "!!n::nat. [| k<=n; n<=m |] ==> (m-k) - (n-k) = m-n"; |
464 goal Arith.thy "!!n::nat. [| k<=n; n<=m |] ==> (m-k) - (n-k) = m-n"; |
468 by (Simp_tac 1); |
468 by (Simp_tac 1); |
469 (* Induction step *) |
469 (* Induction step *) |
470 by (subgoal_tac "Suc na <= m --> n <= m --> Suc na <= n --> \ |
470 by (subgoal_tac "Suc na <= m --> n <= m --> Suc na <= n --> \ |
471 \ Suc (m - Suc na) - Suc (n - Suc na) = m-n" 1); |
471 \ Suc (m - Suc na) - Suc (n - Suc na) = m-n" 1); |
472 by (Asm_full_simp_tac 1); |
472 by (Asm_full_simp_tac 1); |
473 by (blast_tac (!claset addIs [le_trans]) 1); |
473 by (blast_tac (claset() addIs [le_trans]) 1); |
474 by (auto_tac (!claset addIs [Suc_leD], !simpset delsimps [diff_Suc_Suc])); |
474 by (auto_tac (claset() addIs [Suc_leD], simpset() delsimps [diff_Suc_Suc])); |
475 by (asm_full_simp_tac (!simpset delsimps [Suc_less_eq] |
475 by (asm_full_simp_tac (simpset() delsimps [Suc_less_eq] |
476 addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1); |
476 addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1); |
477 qed "diff_right_cancel"; |
477 qed "diff_right_cancel"; |
478 |
478 |
479 goal Arith.thy "!!n::nat. n - (n+m) = 0"; |
479 goal Arith.thy "!!n::nat. n - (n+m) = 0"; |
480 by (induct_tac "n" 1); |
480 by (induct_tac "n" 1); |
489 by (ALLGOALS Asm_simp_tac); |
489 by (ALLGOALS Asm_simp_tac); |
490 qed "diff_mult_distrib" ; |
490 qed "diff_mult_distrib" ; |
491 |
491 |
492 goal Arith.thy "!!m::nat. k * (m - n) = (k * m) - (k * n)"; |
492 goal Arith.thy "!!m::nat. k * (m - n) = (k * m) - (k * n)"; |
493 val mult_commute_k = read_instantiate [("m","k")] mult_commute; |
493 val mult_commute_k = read_instantiate [("m","k")] mult_commute; |
494 by (simp_tac (!simpset addsimps [diff_mult_distrib, mult_commute_k]) 1); |
494 by (simp_tac (simpset() addsimps [diff_mult_distrib, mult_commute_k]) 1); |
495 qed "diff_mult_distrib2" ; |
495 qed "diff_mult_distrib2" ; |
496 (*NOT added as rewrites, since sometimes they are used from right-to-left*) |
496 (*NOT added as rewrites, since sometimes they are used from right-to-left*) |
497 |
497 |
498 |
498 |
499 (*** Monotonicity of Multiplication ***) |
499 (*** Monotonicity of Multiplication ***) |
500 |
500 |
501 goal Arith.thy "!!i::nat. i<=j ==> i*k<=j*k"; |
501 goal Arith.thy "!!i::nat. i<=j ==> i*k<=j*k"; |
502 by (induct_tac "k" 1); |
502 by (induct_tac "k" 1); |
503 by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_le_mono]))); |
503 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono]))); |
504 qed "mult_le_mono1"; |
504 qed "mult_le_mono1"; |
505 |
505 |
506 (*<=monotonicity, BOTH arguments*) |
506 (*<=monotonicity, BOTH arguments*) |
507 goal Arith.thy "!!i::nat. [| i<=j; k<=l |] ==> i*k<=j*l"; |
507 goal Arith.thy "!!i::nat. [| i<=j; k<=l |] ==> i*k<=j*l"; |
508 by (etac (mult_le_mono1 RS le_trans) 1); |
508 by (etac (mult_le_mono1 RS le_trans) 1); |
509 by (rtac le_trans 1); |
509 by (rtac le_trans 1); |
510 by (stac mult_commute 2); |
510 by (stac mult_commute 2); |
511 by (etac mult_le_mono1 2); |
511 by (etac mult_le_mono1 2); |
512 by (simp_tac (!simpset addsimps [mult_commute]) 1); |
512 by (simp_tac (simpset() addsimps [mult_commute]) 1); |
513 qed "mult_le_mono"; |
513 qed "mult_le_mono"; |
514 |
514 |
515 (*strict, in 1st argument; proof is by induction on k>0*) |
515 (*strict, in 1st argument; proof is by induction on k>0*) |
516 goal Arith.thy "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j"; |
516 goal Arith.thy "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j"; |
517 by (eres_inst_tac [("i","0")] less_natE 1); |
517 by (eres_inst_tac [("i","0")] less_natE 1); |
518 by (Asm_simp_tac 1); |
518 by (Asm_simp_tac 1); |
519 by (induct_tac "x" 1); |
519 by (induct_tac "x" 1); |
520 by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_less_mono]))); |
520 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono]))); |
521 qed "mult_less_mono2"; |
521 qed "mult_less_mono2"; |
522 |
522 |
523 goal Arith.thy "!!i::nat. [| i<j; 0<k |] ==> i*k < j*k"; |
523 goal Arith.thy "!!i::nat. [| i<j; 0<k |] ==> i*k < j*k"; |
524 by (dtac mult_less_mono2 1); |
524 by (dtac mult_less_mono2 1); |
525 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [mult_commute]))); |
525 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute]))); |
526 qed "mult_less_mono1"; |
526 qed "mult_less_mono1"; |
527 |
527 |
528 goal Arith.thy "(0 < m*n) = (0<m & 0<n)"; |
528 goal Arith.thy "(0 < m*n) = (0<m & 0<n)"; |
529 by (induct_tac "m" 1); |
529 by (induct_tac "m" 1); |
530 by (induct_tac "n" 2); |
530 by (induct_tac "n" 2); |
534 goal Arith.thy "(m*n = 1) = (m=1 & n=1)"; |
534 goal Arith.thy "(m*n = 1) = (m=1 & n=1)"; |
535 by (induct_tac "m" 1); |
535 by (induct_tac "m" 1); |
536 by (Simp_tac 1); |
536 by (Simp_tac 1); |
537 by (induct_tac "n" 1); |
537 by (induct_tac "n" 1); |
538 by (Simp_tac 1); |
538 by (Simp_tac 1); |
539 by (fast_tac (!claset addss !simpset) 1); |
539 by (fast_tac (claset() addss simpset()) 1); |
540 qed "mult_eq_1_iff"; |
540 qed "mult_eq_1_iff"; |
541 |
541 |
542 goal Arith.thy "!!k. 0<k ==> (m*k < n*k) = (m<n)"; |
542 goal Arith.thy "!!k. 0<k ==> (m*k < n*k) = (m<n)"; |
543 by (safe_tac (!claset addSIs [mult_less_mono1])); |
543 by (safe_tac (claset() addSIs [mult_less_mono1])); |
544 by (cut_facts_tac [less_linear] 1); |
544 by (cut_facts_tac [less_linear] 1); |
545 by (blast_tac (!claset addDs [mult_less_mono1] addEs [less_asym]) 1); |
545 by (blast_tac (claset() addDs [mult_less_mono1] addEs [less_asym]) 1); |
546 qed "mult_less_cancel2"; |
546 qed "mult_less_cancel2"; |
547 |
547 |
548 goal Arith.thy "!!k. 0<k ==> (k*m < k*n) = (m<n)"; |
548 goal Arith.thy "!!k. 0<k ==> (k*m < k*n) = (m<n)"; |
549 by (dtac mult_less_cancel2 1); |
549 by (dtac mult_less_cancel2 1); |
550 by (asm_full_simp_tac (!simpset addsimps [mult_commute]) 1); |
550 by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1); |
551 qed "mult_less_cancel1"; |
551 qed "mult_less_cancel1"; |
552 Addsimps [mult_less_cancel1, mult_less_cancel2]; |
552 Addsimps [mult_less_cancel1, mult_less_cancel2]; |
553 |
553 |
554 goal Arith.thy "!!k. 0<k ==> (m*k = n*k) = (m=n)"; |
554 goal Arith.thy "!!k. 0<k ==> (m*k = n*k) = (m=n)"; |
555 by (cut_facts_tac [less_linear] 1); |
555 by (cut_facts_tac [less_linear] 1); |
559 by (ALLGOALS Asm_full_simp_tac); |
559 by (ALLGOALS Asm_full_simp_tac); |
560 qed "mult_cancel2"; |
560 qed "mult_cancel2"; |
561 |
561 |
562 goal Arith.thy "!!k. 0<k ==> (k*m = k*n) = (m=n)"; |
562 goal Arith.thy "!!k. 0<k ==> (k*m = k*n) = (m=n)"; |
563 by (dtac mult_cancel2 1); |
563 by (dtac mult_cancel2 1); |
564 by (asm_full_simp_tac (!simpset addsimps [mult_commute]) 1); |
564 by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1); |
565 qed "mult_cancel1"; |
565 qed "mult_cancel1"; |
566 Addsimps [mult_cancel1, mult_cancel2]; |
566 Addsimps [mult_cancel1, mult_cancel2]; |
567 |
567 |
568 |
568 |
569 (** Lemma for gcd **) |
569 (** Lemma for gcd **) |
570 |
570 |
571 goal Arith.thy "!!m n. m = m*n ==> n=1 | m=0"; |
571 goal Arith.thy "!!m n. m = m*n ==> n=1 | m=0"; |
572 by (dtac sym 1); |
572 by (dtac sym 1); |
573 by (rtac disjCI 1); |
573 by (rtac disjCI 1); |
574 by (rtac nat_less_cases 1 THEN assume_tac 2); |
574 by (rtac nat_less_cases 1 THEN assume_tac 2); |
575 by (fast_tac (!claset addSEs [less_SucE] addss !simpset) 1); |
575 by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1); |
576 by (best_tac (!claset addDs [mult_less_mono2] |
576 by (best_tac (claset() addDs [mult_less_mono2] |
577 addss (!simpset addsimps [zero_less_eq RS sym])) 1); |
577 addss (simpset() addsimps [zero_less_eq RS sym])) 1); |
578 qed "mult_eq_self_implies_10"; |
578 qed "mult_eq_self_implies_10"; |
579 |
579 |
580 |
580 |
581 (*** Subtraction laws -- from Clemens Ballarin ***) |
581 (*** Subtraction laws -- from Clemens Ballarin ***) |
582 |
582 |
583 goal Arith.thy "!! a b c::nat. [| a < b; c <= a |] ==> a-c < b-c"; |
583 goal Arith.thy "!! a b c::nat. [| a < b; c <= a |] ==> a-c < b-c"; |
584 by (subgoal_tac "c+(a-c) < c+(b-c)" 1); |
584 by (subgoal_tac "c+(a-c) < c+(b-c)" 1); |
585 by (Full_simp_tac 1); |
585 by (Full_simp_tac 1); |
586 by (subgoal_tac "c <= b" 1); |
586 by (subgoal_tac "c <= b" 1); |
587 by (blast_tac (!claset addIs [less_imp_le, le_trans]) 2); |
587 by (blast_tac (claset() addIs [less_imp_le, le_trans]) 2); |
588 by (Asm_simp_tac 1); |
588 by (Asm_simp_tac 1); |
589 qed "diff_less_mono"; |
589 qed "diff_less_mono"; |
590 |
590 |
591 goal Arith.thy "!! a b c::nat. a+b < c ==> a < c-b"; |
591 goal Arith.thy "!! a b c::nat. a+b < c ==> a < c-b"; |
592 by (dtac diff_less_mono 1); |
592 by (dtac diff_less_mono 1); |
594 by (Asm_full_simp_tac 1); |
594 by (Asm_full_simp_tac 1); |
595 qed "add_less_imp_less_diff"; |
595 qed "add_less_imp_less_diff"; |
596 |
596 |
597 goal Arith.thy "!! n. n <= m ==> Suc m - n = Suc (m - n)"; |
597 goal Arith.thy "!! n. n <= m ==> Suc m - n = Suc (m - n)"; |
598 by (rtac Suc_diff_n 1); |
598 by (rtac Suc_diff_n 1); |
599 by (asm_full_simp_tac (!simpset addsimps [le_eq_less_Suc]) 1); |
599 by (asm_full_simp_tac (simpset() addsimps [le_eq_less_Suc]) 1); |
600 qed "Suc_diff_le"; |
600 qed "Suc_diff_le"; |
601 |
601 |
602 goal Arith.thy "!! n. Suc i <= n ==> Suc (n - Suc i) = n - i"; |
602 goal Arith.thy "!! n. Suc i <= n ==> Suc (n - Suc i) = n - i"; |
603 by (asm_full_simp_tac |
603 by (asm_full_simp_tac |
604 (!simpset addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1); |
604 (simpset() addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1); |
605 qed "Suc_diff_Suc"; |
605 qed "Suc_diff_Suc"; |
606 |
606 |
607 goal Arith.thy "!! i::nat. i <= n ==> n - (n - i) = i"; |
607 goal Arith.thy "!! i::nat. i <= n ==> n - (n - i) = i"; |
608 by (etac rev_mp 1); |
608 by (etac rev_mp 1); |
609 by (res_inst_tac [("m","n"),("n","i")] diff_induct 1); |
609 by (res_inst_tac [("m","n"),("n","i")] diff_induct 1); |
610 by (ALLGOALS (asm_simp_tac (!simpset addsimps [Suc_diff_le]))); |
610 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Suc_diff_le]))); |
611 qed "diff_diff_cancel"; |
611 qed "diff_diff_cancel"; |
612 Addsimps [diff_diff_cancel]; |
612 Addsimps [diff_diff_cancel]; |
613 |
613 |
614 goal Arith.thy "!!k::nat. k <= n ==> m <= n + m - k"; |
614 goal Arith.thy "!!k::nat. k <= n ==> m <= n + m - k"; |
615 by (etac rev_mp 1); |
615 by (etac rev_mp 1); |
616 by (res_inst_tac [("m", "k"), ("n", "n")] diff_induct 1); |
616 by (res_inst_tac [("m", "k"), ("n", "n")] diff_induct 1); |
617 by (Simp_tac 1); |
617 by (Simp_tac 1); |
618 by (simp_tac (!simpset addsimps [less_add_Suc2, less_imp_le]) 1); |
618 by (simp_tac (simpset() addsimps [less_add_Suc2, less_imp_le]) 1); |
619 by (Simp_tac 1); |
619 by (Simp_tac 1); |
620 qed "le_add_diff"; |
620 qed "le_add_diff"; |
621 |
621 |
622 |
622 |
623 (** (Anti)Monotonicity of subtraction -- by Stefan Merz **) |
623 (** (Anti)Monotonicity of subtraction -- by Stefan Merz **) |
624 |
624 |
625 (* Monotonicity of subtraction in first argument *) |
625 (* Monotonicity of subtraction in first argument *) |
626 goal Arith.thy "!!n::nat. m<=n --> (m-l) <= (n-l)"; |
626 goal Arith.thy "!!n::nat. m<=n --> (m-l) <= (n-l)"; |
627 by (induct_tac "n" 1); |
627 by (induct_tac "n" 1); |
628 by (Simp_tac 1); |
628 by (Simp_tac 1); |
629 by (simp_tac (!simpset addsimps [le_Suc_eq]) 1); |
629 by (simp_tac (simpset() addsimps [le_Suc_eq]) 1); |
630 by (rtac impI 1); |
630 by (rtac impI 1); |
631 by (etac impE 1); |
631 by (etac impE 1); |
632 by (atac 1); |
632 by (atac 1); |
633 by (etac le_trans 1); |
633 by (etac le_trans 1); |
634 by (res_inst_tac [("m1","n")] (pred_Suc_diff RS subst) 1); |
634 by (res_inst_tac [("m1","n")] (pred_Suc_diff RS subst) 1); |
638 goal Arith.thy "!!n::nat. m<=n ==> (l-n) <= (l-m)"; |
638 goal Arith.thy "!!n::nat. m<=n ==> (l-n) <= (l-m)"; |
639 by (induct_tac "l" 1); |
639 by (induct_tac "l" 1); |
640 by (Simp_tac 1); |
640 by (Simp_tac 1); |
641 by (case_tac "n <= l" 1); |
641 by (case_tac "n <= l" 1); |
642 by (subgoal_tac "m <= l" 1); |
642 by (subgoal_tac "m <= l" 1); |
643 by (asm_simp_tac (!simpset addsimps [Suc_diff_le]) 1); |
643 by (asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1); |
644 by (fast_tac (!claset addEs [le_trans]) 1); |
644 by (fast_tac (claset() addEs [le_trans]) 1); |
645 by (dtac not_leE 1); |
645 by (dtac not_leE 1); |
646 by (asm_simp_tac (!simpset addsimps [if_Suc_diff_n]) 1); |
646 by (asm_simp_tac (simpset() addsimps [if_Suc_diff_n]) 1); |
647 qed_spec_mp "diff_le_mono2"; |
647 qed_spec_mp "diff_le_mono2"; |