equal
deleted
inserted
replaced
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); |
44 qed "pred_less"; |
44 qed "pred_less"; |
45 Addsimps [pred_less]; |
45 Addsimps [pred_less]; |
46 |
46 |
47 (** Difference **) |
47 (** Difference **) |
48 |
48 |
325 by (induct_tac "n" 2); |
325 by (induct_tac "n" 2); |
326 by (ALLGOALS Asm_simp_tac); |
326 by (ALLGOALS Asm_simp_tac); |
327 qed "mult_is_0"; |
327 qed "mult_is_0"; |
328 Addsimps [mult_is_0]; |
328 Addsimps [mult_is_0]; |
329 |
329 |
|
330 goal Arith.thy "!!m::nat. m <= m*m"; |
|
331 by (induct_tac "m" 1); |
|
332 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym]))); |
|
333 by (etac (le_add2 RSN (2,le_trans)) 1); |
|
334 qed "le_square"; |
|
335 |
330 |
336 |
331 (*** Difference ***) |
337 (*** Difference ***) |
332 |
338 |
333 qed_goal "pred_Suc_diff" Arith.thy "pred(Suc m - n) = m - n" |
339 qed_goal "pred_Suc_diff" Arith.thy "pred(Suc m - n) = m - n" |
334 (fn _ => [induct_tac "n" 1, ALLGOALS Asm_simp_tac]); |
340 (fn _ => [induct_tac "n" 1, ALLGOALS Asm_simp_tac]); |