# HG changeset patch
# User paulson
# Date 976094684 -3600
# Node ID 322475c2cb758432a4243261171549a8fbadfc2d
# Parent  2df753cf86e96c85195ef0ed43451ea6c6b65f5b
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
simplifying their proofs

diff -r 2df753cf86e9 -r 322475c2cb75 src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Wed Dec 06 10:23:06 2000 +0100
+++ b/src/HOL/Divides.ML	Wed Dec 06 10:24:44 2000 +0100
@@ -210,7 +210,7 @@
 Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |] \
 \     ==> q = q'";
 by (asm_full_simp_tac 
-    (simpset() addsimps split_ifs @ [quorem_def]) 1);
+    (simpset() addsimps split_ifs @ [Divides.quorem_def]) 1);
 by Auto_tac;  
 by (REPEAT 
     (blast_tac (claset() addIs [order_antisym]
@@ -222,14 +222,14 @@
 \     ==> r = r'";
 by (subgoal_tac "q = q'" 1);
 by (blast_tac (claset() addIs [unique_quotient]) 2);
-by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Divides.quorem_def]) 1);
 qed "unique_remainder";
 
 Goal "0 < b ==> quorem ((a, b), (a div b, a mod b))";
 by (cut_inst_tac [("m","a"),("n","b")] mod_div_equality 1);
 by (auto_tac
     (claset() addEs [sym],
-     simpset() addsimps mult_ac@[quorem_def]));
+     simpset() addsimps mult_ac@[Divides.quorem_def]));
 qed "quorem_div_mod";
 
 Goal "[| quorem((a,b),(q,r));  0 < b |] ==> a div b = q";
@@ -240,6 +240,19 @@
 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_remainder]) 1);
 qed "quorem_mod";
 
+(** A dividend of zero **)
+
+Goal "0 div m = (0::nat)";
+by (div_undefined_case_tac "m=0" 1);
+by (Asm_simp_tac 1);
+qed "div_0"; 
+
+Goal "0 mod m = (0::nat)";
+by (div_undefined_case_tac "m=0" 1);
+by (Asm_simp_tac 1);
+qed "mod_0"; 
+Addsimps [div_0, mod_0];
+
 (** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
 
 Goal "[| quorem((b,c),(q,r));  0 < c |] \
@@ -248,7 +261,7 @@
 by (auto_tac
     (claset(),
      simpset() addsimps split_ifs@mult_ac@
-                        [quorem_def, add_mult_distrib2]));
+                        [Divides.quorem_def, add_mult_distrib2]));
 val lemma = result();
 
 Goal "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)";
@@ -281,7 +294,7 @@
 by (auto_tac
     (claset(),
      simpset() addsimps split_ifs@mult_ac@
-                        [quorem_def, add_mult_distrib2]));
+                        [Divides.quorem_def, add_mult_distrib2]));
 val lemma = result();
 
 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
@@ -300,12 +313,7 @@
 
 (*** proving  a div (b*c) = (a div b) div c ***)
 
-(** first, two lemmas to bound the remainder for the cases b<0 and b>0 **)
-
-Goal "[| (0::nat) < c;  r < b |] ==> 0 <= b * (q mod c) + r";
-by (subgoal_tac "0 <= b * (q mod c)" 1);
-by Auto_tac;  
-val lemma3 = result();
+(** first, a lemma to bound the remainder **)
 
 Goal "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c";
 by (cut_inst_tac [("m","q"),("n","c")] mod_less_divisor 1);
@@ -313,7 +321,7 @@
 by Auto_tac;  
 by (eres_inst_tac [("P","%x. ?lhs < ?rhs x")] ssubst 1); 
 by (asm_simp_tac (simpset() addsimps [add_mult_distrib2]) 1);
-val lemma4 = result();
+val mod_lemma = result();
 
 Goal "[| quorem ((a,b), (q,r));  0 < b;  0 < c |] \
 \     ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))";
@@ -321,20 +329,24 @@
 by (auto_tac  
     (claset(),
      simpset() addsimps mult_ac@
-                        [quorem_def, add_mult_distrib2 RS sym,
-			 lemma3, lemma4]));
+                        [Divides.quorem_def, add_mult_distrib2 RS sym,
+			 mod_lemma]));
 val lemma = result();
 
-Goal "(0::nat) < c ==> a div (b*c) = (a div b) div c";
-by (div_undefined_case_tac "b = 0" 1);
+Goal "a div (b*c) = (a div b) div (c::nat)";
+by (div_undefined_case_tac "b=0" 1);
+by (div_undefined_case_tac "c=0" 1);
 by (force_tac (claset(),
 	       simpset() addsimps [quorem_div_mod RS lemma RS quorem_div]) 1);
 qed "div_mult2_eq";
 
-Goal "(0::nat) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b";
-by (div_undefined_case_tac "b = 0" 1);
-by (force_tac (claset(),
-	       simpset() addsimps [quorem_div_mod RS lemma RS quorem_mod]) 1);
+Goal "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)";
+by (div_undefined_case_tac "b=0" 1);
+by (div_undefined_case_tac "c=0" 1);
+by (cut_inst_tac [("m", "a"), ("n","b")] mod_div_equality 1);
+by (auto_tac (claset(),
+	       simpset() addsimps [mult_commute, 
+				   quorem_div_mod RS lemma RS quorem_mod]));
 qed "mod_mult2_eq";
 
 
@@ -408,19 +420,6 @@
 
 Addsimps [div_mult_self1, div_mult_self2];
 
-(** A dividend of zero **)
-
-Goal "0 div m = (0::nat)";
-by (div_undefined_case_tac "m=0" 1);
-by (Asm_simp_tac 1);
-qed "div_0"; 
-
-Goal "0 mod m = (0::nat)";
-by (div_undefined_case_tac "m=0" 1);
-by (Asm_simp_tac 1);
-qed "mod_0"; 
-Addsimps [div_0, mod_0];
-
 (* Monotonicity of div in first argument *)
 Goal "ALL m::nat. m <= n --> (m div k) <= (n div k)";
 by (div_undefined_case_tac "k=0" 1);