--- 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)
--------------------------------
--- 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 \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
+ and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (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 \<Longrightarrow>
- z dvd w \<Longrightarrow> (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 \<Longrightarrow> z dvd w \<Longrightarrow> (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 \<noteq> 0 \<Longrightarrow> (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 \<Longrightarrow>
(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 \<noteq> 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]: "\<And>n::nat. n div 0 = 0"
+ by (simp add: div_nat_def divmod_zero)
+ have [simp]: "\<And>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 \<noteq> 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 \<noteq> 0"
+ then show "(m * n) div (m * q) = n div q"
+ proof (cases "n \<noteq> 0 \<and> q \<noteq> 0")
+ case False then show ?thesis by auto
+ next
+ case True with `m \<noteq> 0`
+ have "m > 0" and "n > 0" and "q > 0" by auto
+ then have "\<And>a b. divmod_rel n q (a, b) \<Longrightarrow> 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"
--- 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 \<noteq> 0"
+ then show "(a * b) div (a * c) = b div c"
+ proof (cases "b \<noteq> 0 \<and> c \<noteq> 0")
+ case False then show ?thesis by auto
+ next
+ case True then have "b \<noteq> 0" and "c \<noteq> 0" by auto
+ with `a \<noteq> 0`
+ have "\<And>q r. divmod_rel b c (q, r) \<Longrightarrow> 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 \<noteq> 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 \<noteq> 0` `c \<noteq> 0` have "a * c \<noteq> 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 \<noteq> 0 |] ==> (c*a) div (c*b) = a div b"
-by (subst zdiv_zmult2_eq, auto)
-
-lemma zdiv_zmult_zmult1_aux2:
- "[| b < (0::int); c \<noteq> 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 \<noteq> (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 \<noteq> 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 \<noteq> 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 \<le> 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}. *}
--- 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 \<noteq> 0"
+ show "(x * y) div (x * z) = y div z"
+ proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
+ have "\<And>x::'a poly. pdivmod_rel x 0 0 x"
+ by (rule pdivmod_rel_by_0)
+ then have [simp]: "\<And>x::'a poly. x div 0 = 0"
+ by (rule div_poly_eq)
+ have "\<And>x::'a poly. pdivmod_rel 0 x 0 0"
+ by (rule pdivmod_rel_0)
+ then have [simp]: "\<And>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 \<noteq> 0" and "z \<noteq> 0" by auto
+ with `x \<noteq> 0`
+ have "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> 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