# HG changeset patch # User haftmann # Date 1239869494 -7200 # Node ID 11010e5f18f0bd254c3d53ffe85b4e19a2b77de2 # Parent d9343c0aac11b3577060d80d4dd24afd8d2ff7ad tightended specification of class semiring_div diff -r d9343c0aac11 -r 11010e5f18f0 NEWS --- a/NEWS Wed Apr 15 15:52:37 2009 +0200 +++ b/NEWS Thu Apr 16 10:11:34 2009 +0200 @@ -1,6 +1,14 @@ Isabelle NEWS -- history user-relevant changes ============================================== +*** HOL *** + +* Class semiring_div now requires no_zero_divisors and proof of div_mult_mult1; +theorems div_mult_mult1, div_mult_mult2, div_mult_mult1_if, div_mult_mult1 and +div_mult_mult2 have been generalized to class semiring_div, subsuming former +theorems zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and zdiv_zmult_zmult2. +div_mult_mult1 is now [simp] by default. INCOMPATIBILITY. + New in Isabelle2009 (April 2009) -------------------------------- diff -r d9343c0aac11 -r 11010e5f18f0 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Wed Apr 15 15:52:37 2009 +0200 +++ b/src/HOL/Divides.thy Thu Apr 16 10:11:34 2009 +0200 @@ -19,11 +19,12 @@ subsection {* Abstract division in commutative semirings. *} -class semiring_div = comm_semiring_1_cancel + div + +class semiring_div = comm_semiring_1_cancel + no_zero_divisors + div + assumes mod_div_equality: "a div b * b + a mod b = a" and div_by_0 [simp]: "a div 0 = 0" and div_0 [simp]: "0 div a = 0" and div_mult_self1 [simp]: "b \ 0 \ (a + c * b) div b = c + a div b" + and div_mult_mult1 [simp]: "c \ 0 \ (c * a) div (c * b) = a div b" begin text {* @{const div} and @{const mod} *} @@ -296,21 +297,41 @@ finally show ?thesis . qed -end - -lemma div_mult_div_if_dvd: "(y::'a::{semiring_div,no_zero_divisors}) dvd x \ - z dvd w \ (x div y) * (w div z) = (x * w) div (y * z)" -unfolding dvd_def - apply clarify - apply (case_tac "y = 0") - apply simp - apply (case_tac "z = 0") - apply simp - apply (simp add: algebra_simps) +lemma div_mult_div_if_dvd: + "y dvd x \ z dvd w \ (x div y) * (w div z) = (x * w) div (y * z)" + apply (cases "y = 0", simp) + apply (cases "z = 0", simp) + apply (auto elim!: dvdE simp add: algebra_simps) apply (subst mult_assoc [symmetric]) apply (simp add: no_zero_divisors) -done + done + +lemma div_mult_mult2 [simp]: + "c \ 0 \ (a * c) div (b * c) = a div b" + by (drule div_mult_mult1) (simp add: mult_commute) + +lemma div_mult_mult1_if [simp]: + "(c * a) div (c * b) = (if c = 0 then 0 else a div b)" + by simp_all +lemma mod_mult_mult1: + "(c * a) mod (c * b) = c * (a mod b)" +proof (cases "c = 0") + case True then show ?thesis by simp +next + case False + from mod_div_equality + have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" . + with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b) + = c * a + c * (a mod b)" by (simp add: algebra_simps) + with mod_div_equality show ?thesis by simp +qed + +lemma mod_mult_mult2: + "(a * c) mod (b * c) = (a mod b) * c" + using mod_mult_mult1 [of c a b] by (simp add: mult_commute) + +end lemma div_power: "(y::'a::{semiring_div,no_zero_divisors,recpower}) dvd x \ (x div y)^n = x^n div y^n" @@ -566,18 +587,40 @@ shows "m mod n = (m - n) mod n" using assms divmod_step divmod_div_mod by (cases "n = 0") simp_all -instance proof - fix m n :: nat show "m div n * n + m mod n = m" - using divmod_rel [of m n] by (simp add: divmod_rel_def) -next - fix n :: nat show "n div 0 = 0" - using divmod_zero divmod_div_mod [of n 0] by simp -next - fix n :: nat show "0 div n = 0" - using divmod_rel [of 0 n] by (cases n) (simp_all add: divmod_rel_def) -next - fix m n q :: nat assume "n \ 0" then show "(q + m * n) div n = m + q div n" - by (induct m) (simp_all add: le_div_geq) +instance proof - + have [simp]: "\n::nat. n div 0 = 0" + by (simp add: div_nat_def divmod_zero) + have [simp]: "\n::nat. 0 div n = 0" + proof - + fix n :: nat + show "0 div n = 0" + by (cases "n = 0") simp_all + qed + show "OFCLASS(nat, semiring_div_class)" proof + fix m n :: nat + show "m div n * n + m mod n = m" + using divmod_rel [of m n] by (simp add: divmod_rel_def) + next + fix m n q :: nat + assume "n \ 0" + then show "(q + m * n) div n = m + q div n" + by (induct m) (simp_all add: le_div_geq) + next + fix m n q :: nat + assume "m \ 0" + then show "(m * n) div (m * q) = n div q" + proof (cases "n \ 0 \ q \ 0") + case False then show ?thesis by auto + next + case True with `m \ 0` + have "m > 0" and "n > 0" and "q > 0" by auto + then have "\a b. divmod_rel n q (a, b) \ divmod_rel (m * n) (m * q) (a, m * b)" + by (auto simp add: divmod_rel_def) (simp_all add: algebra_simps) + moreover from divmod_rel have "divmod_rel n q (n div q, n mod q)" . + ultimately have "divmod_rel (m * n) (m * q) (n div q, m * (n mod q))" . + then show ?thesis by (simp add: div_eq) + qed + qed simp_all qed end @@ -744,23 +787,6 @@ done -subsubsection{*Cancellation of Common Factors in Division*} - -lemma div_mult_mult_lemma: - "[| (0::nat) < b; 0 < c |] ==> (c*a) div (c*b) = a div b" -by (auto simp add: div_mult2_eq) - -lemma div_mult_mult1 [simp]: "(0::nat) < c ==> (c*a) div (c*b) = a div b" - apply (cases "b = 0") - apply (auto simp add: linorder_neq_iff [of b] div_mult_mult_lemma) - done - -lemma div_mult_mult2 [simp]: "(0::nat) < c ==> (a*c) div (b*c) = a div b" - apply (drule div_mult_mult1) - apply (auto simp add: mult_commute) - done - - subsubsection{*Further Facts about Quotient and Remainder*} lemma div_1 [simp]: "m div Suc 0 = m" diff -r d9343c0aac11 -r 11010e5f18f0 src/HOL/IntDiv.thy --- a/src/HOL/IntDiv.thy Wed Apr 15 15:52:37 2009 +0200 +++ b/src/HOL/IntDiv.thy Thu Apr 16 10:11:34 2009 +0200 @@ -711,6 +711,26 @@ show "(a + c * b) div b = c + a div b" unfolding zdiv_zadd1_eq [of a "c * b"] using not0 by (simp add: zmod_zmult1_eq zmod_zdiv_trivial zdiv_zmult1_eq) +next + fix a b c :: int + assume "a \ 0" + then show "(a * b) div (a * c) = b div c" + proof (cases "b \ 0 \ c \ 0") + case False then show ?thesis by auto + next + case True then have "b \ 0" and "c \ 0" by auto + with `a \ 0` + have "\q r. divmod_rel b c (q, r) \ divmod_rel (a * b) (a * c) (q, a * r)" + apply (auto simp add: divmod_rel_def) + apply (auto simp add: algebra_simps) + apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff) + apply (simp_all add: mult_less_cancel_left_disj mult_commute [of _ a]) + done + moreover with `c \ 0` divmod_rel_div_mod have "divmod_rel b c (b div c, b mod c)" by auto + ultimately have "divmod_rel (a * b) (a * c) (b div c, a * (b mod c))" . + moreover from `a \ 0` `c \ 0` have "a * c \ 0" by simp + ultimately show ?thesis by (rule divmod_rel_div) + qed qed auto lemma posDivAlg_div_mod: @@ -808,52 +828,6 @@ done -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) - -lemma zdiv_zmult_zmult1_aux2: - "[| b < (0::int); c \ 0 |] ==> (c*a) div (c*b) = a div b" -apply (subgoal_tac " (c * (-a)) div (c * (-b)) = (-a) div (-b) ") -apply (rule_tac [2] zdiv_zmult_zmult1_aux1, auto) -done - -lemma zdiv_zmult_zmult1: "c \ (0::int) ==> (c*a) div (c*b) = a div b" -apply (case_tac "b = 0", simp) -apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2) -done - -lemma zdiv_zmult_zmult1_if[simp]: - "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)" -by (simp add:zdiv_zmult_zmult1) - - -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) - -lemma zmod_zmult_zmult1_aux2: - "[| b < (0::int); c \ 0 |] ==> (c*a) mod (c*b) = c * (a mod b)" -apply (subgoal_tac " (c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))") -apply (rule_tac [2] zmod_zmult_zmult1_aux1, auto) -done - -lemma zmod_zmult_zmult1: "(c*a) mod (c*b) = (c::int) * (a mod b)" -apply (case_tac "b = 0", simp) -apply (case_tac "c = 0", simp) -apply (auto simp add: linorder_neq_iff zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2) -done - -lemma zmod_zmult_zmult2: "(a*c) mod (b*c) = (a mod b) * (c::int)" -apply (cut_tac c = c in zmod_zmult_zmult1) -apply (auto simp add: mult_commute) -done - - subsection {*Splitting Rules for div and mod*} text{*The proofs of the two lemmas below are essentially identical*} @@ -937,7 +911,7 @@ right_distrib) thus ?thesis by (subst zdiv_zadd1_eq, - simp add: zdiv_zmult_zmult1 zmod_zmult_zmult1 one_less_a2 + simp add: mod_mult_mult1 one_less_a2 div_pos_pos_trivial) qed @@ -961,7 +935,7 @@ then number_of v div (number_of w) else (number_of v + (1::int)) div (number_of w))" apply (simp only: number_of_eq numeral_simps UNIV_I split: split_if) -apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac) +apply (simp add: pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac) done @@ -977,7 +951,7 @@ apply (auto simp add: add_commute [of 1] mult_commute add1_zle_eq pos_mod_bound) apply (subst mod_add_eq) -apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial) +apply (simp add: mod_mult_mult2 mod_pos_pos_trivial) apply (rule mod_pos_pos_trivial) apply (auto simp add: mod_pos_pos_trivial ring_distribs) apply (subgoal_tac "0 \ b mod a", arith, simp) @@ -998,7 +972,7 @@ "number_of (Int.Bit0 v) mod number_of (Int.Bit0 w) = (2::int) * (number_of v mod number_of w)" apply (simp only: number_of_eq numeral_simps) -apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 +apply (simp add: mod_mult_mult1 pos_zmod_mult_2 neg_zmod_mult_2 add_ac) done @@ -1008,7 +982,7 @@ then 2 * (number_of v mod number_of w) + 1 else 2 * ((number_of v + (1::int)) mod number_of w) - 1)" apply (simp only: number_of_eq numeral_simps) -apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 +apply (simp add: mod_mult_mult1 pos_zmod_mult_2 neg_zmod_mult_2 add_ac) done @@ -1090,9 +1064,7 @@ done lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n" - apply (simp add: dvd_def) - apply (auto simp add: zmod_zmult_zmult1) - done + by (auto elim!: dvdE simp add: mod_mult_mult1) lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)" apply (subgoal_tac "k dvd n * (m div n) + m mod n") @@ -1247,9 +1219,9 @@ lemmas zmod_simps = mod_add_left_eq [symmetric] mod_add_right_eq [symmetric] - IntDiv.zmod_zmult1_eq [symmetric] - mod_mult_left_eq [symmetric] - IntDiv.zpower_zmod + zmod_zmult1_eq [symmetric] + mod_mult_left_eq [symmetric] + zpower_zmod zminus_zmod zdiff_zmod_left zdiff_zmod_right text {* Distributive laws for function @{text nat}. *} diff -r d9343c0aac11 -r 11010e5f18f0 src/HOL/Library/Polynomial.thy --- a/src/HOL/Library/Polynomial.thy Wed Apr 15 15:52:37 2009 +0200 +++ b/src/HOL/Library/Polynomial.thy Thu Apr 16 10:11:34 2009 +0200 @@ -987,6 +987,30 @@ by (simp add: pdivmod_rel_def left_distrib) thus "(x + z * y) div y = z + x div y" by (rule div_poly_eq) +next + fix x y z :: "'a poly" + assume "x \ 0" + show "(x * y) div (x * z) = y div z" + proof (cases "y \ 0 \ z \ 0") + have "\x::'a poly. pdivmod_rel x 0 0 x" + by (rule pdivmod_rel_by_0) + then have [simp]: "\x::'a poly. x div 0 = 0" + by (rule div_poly_eq) + have "\x::'a poly. pdivmod_rel 0 x 0 0" + by (rule pdivmod_rel_0) + then have [simp]: "\x::'a poly. 0 div x = 0" + by (rule div_poly_eq) + case False then show ?thesis by auto + next + case True then have "y \ 0" and "z \ 0" by auto + with `x \ 0` + have "\q r. pdivmod_rel y z q r \ pdivmod_rel (x * y) (x * z) q (x * r)" + by (auto simp add: pdivmod_rel_def algebra_simps) + (rule classical, simp add: degree_mult_eq) + moreover from pdivmod_rel have "pdivmod_rel y z (y div z) (y mod z)" . + ultimately have "pdivmod_rel (x * y) (x * z) (y div z) (x * (y mod z))" . + then show ?thesis by (simp add: div_poly_eq) + qed qed end