equal
deleted
inserted
replaced
263 qed "add_eq_self_zero"; |
263 qed "add_eq_self_zero"; |
264 |
264 |
265 |
265 |
266 (**** Additional theorems about "less than" ****) |
266 (**** Additional theorems about "less than" ****) |
267 |
267 |
268 (*Deleted less_natE; instead use less_eq_Suc_add RS exE*) |
268 (*Deleted less_natE; instead use less_imp_Suc_add RS exE*) |
269 Goal "m<n --> (EX k. n=Suc(m+k))"; |
269 Goal "m<n --> (EX k. n=Suc(m+k))"; |
270 by (induct_tac "n" 1); |
270 by (induct_tac "n" 1); |
271 by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less]))); |
271 by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less]))); |
272 by (blast_tac (claset() addSEs [less_SucE] |
272 by (blast_tac (claset() addSEs [less_SucE] |
273 addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1); |
273 addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1); |
274 qed_spec_mp "less_eq_Suc_add"; |
274 qed_spec_mp "less_imp_Suc_add"; |
275 |
275 |
276 Goal "n <= ((m + n)::nat)"; |
276 Goal "n <= ((m + n)::nat)"; |
277 by (induct_tac "m" 1); |
277 by (induct_tac "m" 1); |
278 by (ALLGOALS Simp_tac); |
278 by (ALLGOALS Simp_tac); |
279 by (etac le_SucI 1); |
279 by (etac le_SucI 1); |
286 |
286 |
287 bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans))); |
287 bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans))); |
288 bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans))); |
288 bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans))); |
289 |
289 |
290 Goal "(m<n) = (EX k. n=Suc(m+k))"; |
290 Goal "(m<n) = (EX k. n=Suc(m+k))"; |
291 by (blast_tac (claset() addSIs [less_add_Suc1, less_eq_Suc_add]) 1); |
291 by (blast_tac (claset() addSIs [less_add_Suc1, less_imp_Suc_add]) 1); |
292 qed "less_iff_Suc_add"; |
292 qed "less_iff_Suc_add"; |
293 |
293 |
294 |
294 |
295 (*"i <= j ==> i <= j+m"*) |
295 (*"i <= j ==> i <= j+m"*) |
296 bind_thm ("trans_le_add1", le_add1 RSN (2,le_trans)); |
296 bind_thm ("trans_le_add1", le_add1 RSN (2,le_trans)); |
632 by (etac mult_le_mono2 1); |
632 by (etac mult_le_mono2 1); |
633 qed "mult_le_mono"; |
633 qed "mult_le_mono"; |
634 |
634 |
635 (*strict, in 1st argument; proof is by induction on k>0*) |
635 (*strict, in 1st argument; proof is by induction on k>0*) |
636 Goal "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j"; |
636 Goal "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j"; |
637 by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1); |
637 by (eres_inst_tac [("m1","0")] (less_imp_Suc_add RS exE) 1); |
638 by (Asm_simp_tac 1); |
638 by (Asm_simp_tac 1); |
639 by (induct_tac "x" 1); |
639 by (induct_tac "x" 1); |
640 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono]))); |
640 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono]))); |
641 qed "mult_less_mono2"; |
641 qed "mult_less_mono2"; |
642 |
642 |