# HG changeset patch
# User paulson
# Date 881832484 -3600
# Node ID f6d019eefa1ed61186ab43dae102304cad949b3f
# Parent  429cba89b4c86343d3e54cfeecf8212ba9a86300
Got rid of mod2_neq_0

diff -r 429cba89b4c8 -r f6d019eefa1e src/HOL/Divides.ML
--- 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];
 
diff -r 429cba89b4c8 -r f6d019eefa1e src/HOL/ex/Fib.ML
--- 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 @