
diff -r 342451d763f9 -r 8ed6989228bb src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Tue Dec 02 11:48:15 2003 +0100
+++ b/src/HOL/Integ/IntDiv.thy	Wed Dec 03 10:49:34 2003 +0100
@@ -89,7 +89,7 @@
 
 
 
-(*** Uniqueness and monotonicity of quotients and remainders ***)
+subsection{*Uniqueness and Monotonicity of Quotients and Remainders*}
 
 lemma unique_quotient_lemma:
      "[| b*q' + r'  <= b*q + r;  0 <= r';  0 < b;  r < b |]  
@@ -129,7 +129,9 @@
 done
 
 
-(*** Correctness of posDivAlg, the division algorithm for a>=0 and b>0 ***)
+subsection{*Correctness of posDivAlg, the Algorithm for Non-Negative Dividends*}
+
+text{*And positive divisors*}
 
 lemma adjust_eq [simp]:
      "adjust b (q,r) = 
@@ -160,7 +162,9 @@
 done
 
 
-(*** Correctness of negDivAlg, the division algorithm for a<0 and b>0 ***)
+subsection{*Correctness of negDivAlg, the Algorithm for Negative Dividends*}
+
+text{*And positive divisors*}
 
 declare negDivAlg.simps [simp del]
 
@@ -186,7 +190,7 @@
 done
 
 
-(*** Existence shown by proving the division algorithm to be correct ***)
+subsection{*Existence Shown by Proving the Division Algorithm to be Correct*}
 
 (*the case a=0*)
 lemma quorem_0: "b ~= 0 ==> quorem ((0,b), (0,0))"
@@ -211,8 +215,8 @@
 (** Arbitrary definitions for division by zero.  Useful to simplify 
     certain equations **)
 
-lemma DIVISION_BY_ZERO: "a div (0::int) = 0 & a mod (0::int) = a"
-by (simp add: div_def mod_def divAlg_def posDivAlg.simps)  (*NOT for adding to default simpset*)
+lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a"
+by (simp add: div_def mod_def divAlg_def posDivAlg.simps)  
 
 (** Basic laws about division and remainder **)
 
@@ -311,7 +315,7 @@
        auto)
 done
 
-(*** div, mod and unary minus ***)
+subsection{*div, mod and unary minus*}
 
 lemma zminus1_lemma:
      "quorem((a,b),(q,r))  
@@ -349,7 +353,7 @@
 by (simp add: zmod_zminus1_eq_if zmod_zminus2)
 
 
-(*** division of a number by itself ***)
+subsection{*Division of a Number by Itself*}
 
 lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 <= q"
 apply (subgoal_tac "0 < a*q")
@@ -385,7 +389,7 @@
 done
 
 
-(*** Computation of division and remainder ***)
+subsection{*Computation of Division and Remainder*}
 
 lemma zdiv_zero [simp]: "(0::int) div b = 0"
 by (simp add: div_def divAlg_def)
@@ -486,7 +490,7 @@
 declare negDivAlg_eqn [of concl: 1 "number_of w", standard, simp]
 
 
-(*** Monotonicity in the first argument (divisor) ***)
+subsection{*Monotonicity in the First Argument (Dividend)*}
 
 lemma zdiv_mono1: "[| a <= a';  0 < (b::int) |] ==> a div b <= a' div b"
 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
@@ -507,7 +511,7 @@
 done
 
 
-(*** Monotonicity in the second argument (dividend) ***)
+subsection{*Monotonicity in the Second Argument (Divisor)*}
 
 lemma q_pos_lemma:
      "[| 0 <= b'*q' + r'; r' < b';  0 < b' |] ==> 0 <= (q'::int)"
@@ -574,7 +578,7 @@
 done
 
 
-(*** More algebraic laws for div and mod ***)
+subsection{*More Algebraic Laws for div and mod*}
 
 (** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
 
@@ -686,7 +690,7 @@
 done
 
 
-(*** proving  a div (b*c) = (a div b) div c ***)
+subsection{*Proving  @{term "a div (b*c) = (a div b) div c"} *}
 
 (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
   7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
@@ -700,7 +704,7 @@
 apply (rule order_le_less_trans)
 apply (erule_tac [2] zmult_zless_mono1)
 apply (rule zmult_zle_mono2_neg)
-apply (auto simp add: zcompare_rls zadd_commute [of 1]
+apply (auto simp add: compare_rls zadd_commute [of 1]
                       add1_zle_eq pos_mod_bound)
 done
 
@@ -722,13 +726,13 @@
 apply (rule order_less_le_trans)
 apply (erule zmult_zless_mono1)
 apply (rule_tac [2] zmult_zle_mono2)
-apply (auto simp add: zcompare_rls zadd_commute [of 1]
+apply (auto simp add: compare_rls zadd_commute [of 1]
                       add1_zle_eq pos_mod_bound)
 done
 
 lemma zmult2_lemma: "[| quorem ((a,b), (q,r));  b ~= 0;  0 < c |]  
       ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
-by (auto simp add: zmult_ac quorem_def linorder_neq_iff
+by (auto simp add: mult_ac quorem_def linorder_neq_iff
                    int_0_less_mult_iff zadd_zmult_distrib2 [symmetric] 
                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)
 
@@ -744,7 +748,7 @@
 done
 
 
-(*** Cancellation of common factors in div ***)
+subsection{*Cancellation of Common Factors in div*}
 
 lemma zdiv_zmult_zmult1_aux1: "[| (0::int) < b;  c ~= 0 |] ==> (c*a) div (c*b) = a div b"
 by (subst zdiv_zmult2_eq, auto)
@@ -766,7 +770,7 @@
 
 
 
-(*** Distribution of factors over mod ***)
+subsection{*Distribution of Factors over mod*}
 
 lemma zmod_zmult_zmult1_aux1: "[| (0::int) < b;  c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
 by (subst zmod_zmult2_eq, auto)
@@ -788,7 +792,7 @@
 done
 
 
-subsection {*splitting rules for div and mod*}
+subsection {*Splitting Rules for div and mod*}
 
 text{*The proofs of the two lemmas below are essentially identical*}
 
@@ -853,7 +857,7 @@
 declare split_zmod [of _ _ "number_of k", simplified, standard, arith_split]
 
 
-subsection{*Speeding up the division algorithm with shifting*}
+subsection{*Speeding up the Division Algorithm with Shifting*}
 
 (** computing div by shifting **)
 
@@ -986,7 +990,7 @@
 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
 
 
-subsection {* Divides relation *}
+subsection {* The Divides Relation *}
 
 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
 by(simp add:dvd_def zmod_eq_0_iff)
@@ -1046,7 +1050,7 @@
 
 lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n"
   apply (unfold dvd_def)
-  apply (blast intro: zmult_left_commute)
+  apply (blast intro: mult_left_commute)
   done
 
 lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n"
@@ -1077,7 +1081,7 @@
 lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
   apply (unfold dvd_def, clarify)
   apply (rule_tac x = "k * ka" in exI)
-  apply (simp add: zmult_ac)
+  apply (simp add: mult_ac)
   done
 
 lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"




