--- a/src/HOL/Divides.ML Mon Dec 08 20:29:49 1997 +0100
+++ b/src/HOL/Divides.ML Thu Dec 11 10:28:04 1997 +0100
@@ -241,17 +241,10 @@
qed "mod2_Suc_Suc";
Addsimps [mod2_Suc_Suc];
-(* FIXME: this thm is subsumed by the next one. Get rid of it. *)
-goal thy "!!m. m mod 2 ~= 0 ==> m mod 2 = 1";
+goal Divides.thy "(0 < m mod 2) = (m mod 2 = 1)";
by (subgoal_tac "m mod 2 < 2" 1);
by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
-by (Asm_full_simp_tac 1);
-by (trans_tac 1);
-qed "mod2_neq_0";
-
-goal Divides.thy "(0 < m mod 2) = (m mod 2 = 1)";
-by (rtac iffI 1);
-by(ALLGOALS (asm_full_simp_tac (simpset() addsimps [mod2_neq_0])));
+by (Auto_tac());
qed "mod2_gr_0";
Addsimps [mod2_gr_0];
@@ -259,6 +252,13 @@
by (induct_tac "m" 1);
by (simp_tac (simpset() addsimps [mod_less]) 1);
by (Asm_simp_tac 1);
+qed "mod2_add_self_eq_0";
+Addsimps [mod2_add_self_eq_0];
+
+goal thy "((m+m)+n) mod 2 = n mod 2";
+by (induct_tac "m" 1);
+by (simp_tac (simpset() addsimps [mod_less]) 1);
+by (Asm_simp_tac 1);
qed "mod2_add_self";
Addsimps [mod2_add_self];
--- a/src/HOL/ex/Fib.ML Mon Dec 08 20:29:49 1997 +0100
+++ b/src/HOL/ex/Fib.ML Thu Dec 11 10:28:04 1997 +0100
@@ -25,7 +25,7 @@
by (res_inst_tac [("u","n")] fib.induct 1);
(*Simplify the LHS just enough to apply the induction hypotheses*)
by (asm_full_simp_tac
- (simpset() addsimps [read_instantiate[("x", "Suc(?m+?n)")] fib_Suc_Suc]) 3);
+ (simpset() addsimps [read_instantiate[("x","Suc(?m+?n)")] fib_Suc_Suc]) 3);
by (ALLGOALS
(asm_simp_tac (simpset() addsimps
(fib.rules @ add_ac @ mult_ac @
@@ -58,9 +58,8 @@
by (stac (read_instantiate [("x", "Suc ?n")] fib_Suc_Suc) 3);
by (ALLGOALS (*using fib.rules here results in a longer proof!*)
(asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2,
- mod_less, mod_Suc]
- addsplits [expand_if])));
-by (safe_tac (claset() addSDs [mod2_neq_0]));
+ mod_less, mod_Suc]
+ addsplits [expand_if])));
by (ALLGOALS
(asm_full_simp_tac
(simpset() addsimps (fib.rules @ add_ac @ mult_ac @