# HG changeset patch
# User paulson
# Date 864306465 -7200
# Node ID c05f73cf32275ff8864de411dbcda960adf5f154
# Parent  8b143c196d42fa62f6ecea6973c76599391ac384
New lemmas used for ex/Fib

diff -r 8b143c196d42 -r c05f73cf3227 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Thu May 22 13:05:52 1997 +0200
+++ b/src/HOL/Arith.ML	Thu May 22 15:07:45 1997 +0200
@@ -118,6 +118,12 @@
 qed "add_is_0";
 Addsimps [add_is_0];
 
+goal Arith.thy "(pred (m+n) = 0) = (m=0 & pred n = 0 | pred m = 0 & n=0)";
+by (nat_ind_tac "m" 1);
+by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+qed "pred_add_is_0";
+Addsimps [pred_add_is_0];
+
 goal Arith.thy "!!n. n ~= 0 ==> m + pred n = pred(m+n)";
 by (nat_ind_tac "m" 1);
 by (ALLGOALS Asm_simp_tac);
@@ -267,12 +273,12 @@
 qed_goal "mult_0_right" Arith.thy "m * 0 = 0"
  (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
 
-(*right Sucessor law for multiplication*)
+(*right successor law for multiplication*)
 qed_goal "mult_Suc_right" Arith.thy  "m * Suc(n) = m + (m * n)"
  (fn _ => [nat_ind_tac "m" 1,
            ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
 
-Addsimps [mult_0_right,mult_Suc_right];
+Addsimps [mult_0_right, mult_Suc_right];
 
 goal Arith.thy "1 * n = n";
 by (Asm_simp_tac 1);
@@ -306,6 +312,13 @@
 
 val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
 
+goal Arith.thy "(m*n = 0) = (m=0 | n=0)";
+by (nat_ind_tac "m" 1);
+by (nat_ind_tac "n" 2);
+by (ALLGOALS Asm_simp_tac);
+qed "mult_is_0";
+Addsimps [mult_is_0];
+
 
 (*** Difference ***)
 
@@ -522,7 +535,7 @@
 qed "mod_div_equality";
 
 
-(*** Further facts about mod (mainly for mutilated checkerboard ***)
+(*** Further facts about mod (mainly for the mutilated chess board ***)
 
 goal Arith.thy
     "!!m n. 0<n ==> \
@@ -571,6 +584,13 @@
 qed "mod2_Suc_Suc";
 Addsimps [mod2_Suc_Suc];
 
+goal Arith.thy "!!m. m mod 2 ~= 0 ==> m mod 2 = 1";
+by (subgoal_tac "m mod 2 < 2" 1);
+by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
+by (safe_tac (!claset addSEs [lessE]));
+by (ALLGOALS (blast_tac (!claset addIs [sym])));
+qed "mod2_neq_0";
+
 goal thy "(m+m) mod 2 = 0";
 by (nat_ind_tac "m" 1);
 by (simp_tac (!simpset addsimps [mod_less]) 1);