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))"