1.1 --- a/NEWS Wed Apr 15 15:52:37 2009 +0200
1.2 +++ b/NEWS Thu Apr 16 10:11:34 2009 +0200
1.3 @@ -1,6 +1,14 @@
1.4 Isabelle NEWS -- history user-relevant changes
1.5 ==============================================
1.6
1.7 +*** HOL ***
1.8 +
1.9 +* Class semiring_div now requires no_zero_divisors and proof of div_mult_mult1;
1.10 +theorems div_mult_mult1, div_mult_mult2, div_mult_mult1_if, div_mult_mult1 and
1.11 +div_mult_mult2 have been generalized to class semiring_div, subsuming former
1.12 +theorems zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and zdiv_zmult_zmult2.
1.13 +div_mult_mult1 is now [simp] by default. INCOMPATIBILITY.
1.14 +
1.15 New in Isabelle2009 (April 2009)
1.16 --------------------------------
1.17
2.1 --- a/src/HOL/Divides.thy Wed Apr 15 15:52:37 2009 +0200
2.2 +++ b/src/HOL/Divides.thy Thu Apr 16 10:11:34 2009 +0200
2.3 @@ -19,11 +19,12 @@
2.4
2.5 subsection {* Abstract division in commutative semirings. *}
2.6
2.7 -class semiring_div = comm_semiring_1_cancel + div +
2.8 +class semiring_div = comm_semiring_1_cancel + no_zero_divisors + div +
2.9 assumes mod_div_equality: "a div b * b + a mod b = a"
2.10 and div_by_0 [simp]: "a div 0 = 0"
2.11 and div_0 [simp]: "0 div a = 0"
2.12 and div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
2.13 + and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
2.14 begin
2.15
2.16 text {* @{const div} and @{const mod} *}
2.17 @@ -296,21 +297,41 @@
2.18 finally show ?thesis .
2.19 qed
2.20
2.21 -end
2.22 -
2.23 -lemma div_mult_div_if_dvd: "(y::'a::{semiring_div,no_zero_divisors}) dvd x \<Longrightarrow>
2.24 - z dvd w \<Longrightarrow> (x div y) * (w div z) = (x * w) div (y * z)"
2.25 -unfolding dvd_def
2.26 - apply clarify
2.27 - apply (case_tac "y = 0")
2.28 - apply simp
2.29 - apply (case_tac "z = 0")
2.30 - apply simp
2.31 - apply (simp add: algebra_simps)
2.32 +lemma div_mult_div_if_dvd:
2.33 + "y dvd x \<Longrightarrow> z dvd w \<Longrightarrow> (x div y) * (w div z) = (x * w) div (y * z)"
2.34 + apply (cases "y = 0", simp)
2.35 + apply (cases "z = 0", simp)
2.36 + apply (auto elim!: dvdE simp add: algebra_simps)
2.37 apply (subst mult_assoc [symmetric])
2.38 apply (simp add: no_zero_divisors)
2.39 -done
2.40 + done
2.41
2.42 +lemma div_mult_mult2 [simp]:
2.43 + "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
2.44 + by (drule div_mult_mult1) (simp add: mult_commute)
2.45 +
2.46 +lemma div_mult_mult1_if [simp]:
2.47 + "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
2.48 + by simp_all
2.49 +
2.50 +lemma mod_mult_mult1:
2.51 + "(c * a) mod (c * b) = c * (a mod b)"
2.52 +proof (cases "c = 0")
2.53 + case True then show ?thesis by simp
2.54 +next
2.55 + case False
2.56 + from mod_div_equality
2.57 + have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
2.58 + with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
2.59 + = c * a + c * (a mod b)" by (simp add: algebra_simps)
2.60 + with mod_div_equality show ?thesis by simp
2.61 +qed
2.62 +
2.63 +lemma mod_mult_mult2:
2.64 + "(a * c) mod (b * c) = (a mod b) * c"
2.65 + using mod_mult_mult1 [of c a b] by (simp add: mult_commute)
2.66 +
2.67 +end
2.68
2.69 lemma div_power: "(y::'a::{semiring_div,no_zero_divisors,recpower}) dvd x \<Longrightarrow>
2.70 (x div y)^n = x^n div y^n"
2.71 @@ -566,18 +587,40 @@
2.72 shows "m mod n = (m - n) mod n"
2.73 using assms divmod_step divmod_div_mod by (cases "n = 0") simp_all
2.74
2.75 -instance proof
2.76 - fix m n :: nat show "m div n * n + m mod n = m"
2.77 - using divmod_rel [of m n] by (simp add: divmod_rel_def)
2.78 -next
2.79 - fix n :: nat show "n div 0 = 0"
2.80 - using divmod_zero divmod_div_mod [of n 0] by simp
2.81 -next
2.82 - fix n :: nat show "0 div n = 0"
2.83 - using divmod_rel [of 0 n] by (cases n) (simp_all add: divmod_rel_def)
2.84 -next
2.85 - fix m n q :: nat assume "n \<noteq> 0" then show "(q + m * n) div n = m + q div n"
2.86 - by (induct m) (simp_all add: le_div_geq)
2.87 +instance proof -
2.88 + have [simp]: "\<And>n::nat. n div 0 = 0"
2.89 + by (simp add: div_nat_def divmod_zero)
2.90 + have [simp]: "\<And>n::nat. 0 div n = 0"
2.91 + proof -
2.92 + fix n :: nat
2.93 + show "0 div n = 0"
2.94 + by (cases "n = 0") simp_all
2.95 + qed
2.96 + show "OFCLASS(nat, semiring_div_class)" proof
2.97 + fix m n :: nat
2.98 + show "m div n * n + m mod n = m"
2.99 + using divmod_rel [of m n] by (simp add: divmod_rel_def)
2.100 + next
2.101 + fix m n q :: nat
2.102 + assume "n \<noteq> 0"
2.103 + then show "(q + m * n) div n = m + q div n"
2.104 + by (induct m) (simp_all add: le_div_geq)
2.105 + next
2.106 + fix m n q :: nat
2.107 + assume "m \<noteq> 0"
2.108 + then show "(m * n) div (m * q) = n div q"
2.109 + proof (cases "n \<noteq> 0 \<and> q \<noteq> 0")
2.110 + case False then show ?thesis by auto
2.111 + next
2.112 + case True with `m \<noteq> 0`
2.113 + have "m > 0" and "n > 0" and "q > 0" by auto
2.114 + then have "\<And>a b. divmod_rel n q (a, b) \<Longrightarrow> divmod_rel (m * n) (m * q) (a, m * b)"
2.115 + by (auto simp add: divmod_rel_def) (simp_all add: algebra_simps)
2.116 + moreover from divmod_rel have "divmod_rel n q (n div q, n mod q)" .
2.117 + ultimately have "divmod_rel (m * n) (m * q) (n div q, m * (n mod q))" .
2.118 + then show ?thesis by (simp add: div_eq)
2.119 + qed
2.120 + qed simp_all
2.121 qed
2.122
2.123 end
2.124 @@ -744,23 +787,6 @@
2.125 done
2.126
2.127
2.128 -subsubsection{*Cancellation of Common Factors in Division*}
2.129 -
2.130 -lemma div_mult_mult_lemma:
2.131 - "[| (0::nat) < b; 0 < c |] ==> (c*a) div (c*b) = a div b"
2.132 -by (auto simp add: div_mult2_eq)
2.133 -
2.134 -lemma div_mult_mult1 [simp]: "(0::nat) < c ==> (c*a) div (c*b) = a div b"
2.135 - apply (cases "b = 0")
2.136 - apply (auto simp add: linorder_neq_iff [of b] div_mult_mult_lemma)
2.137 - done
2.138 -
2.139 -lemma div_mult_mult2 [simp]: "(0::nat) < c ==> (a*c) div (b*c) = a div b"
2.140 - apply (drule div_mult_mult1)
2.141 - apply (auto simp add: mult_commute)
2.142 - done
2.143 -
2.144 -
2.145 subsubsection{*Further Facts about Quotient and Remainder*}
2.146
2.147 lemma div_1 [simp]: "m div Suc 0 = m"
3.1 --- a/src/HOL/IntDiv.thy Wed Apr 15 15:52:37 2009 +0200
3.2 +++ b/src/HOL/IntDiv.thy Thu Apr 16 10:11:34 2009 +0200
3.3 @@ -711,6 +711,26 @@
3.4 show "(a + c * b) div b = c + a div b"
3.5 unfolding zdiv_zadd1_eq [of a "c * b"] using not0
3.6 by (simp add: zmod_zmult1_eq zmod_zdiv_trivial zdiv_zmult1_eq)
3.7 +next
3.8 + fix a b c :: int
3.9 + assume "a \<noteq> 0"
3.10 + then show "(a * b) div (a * c) = b div c"
3.11 + proof (cases "b \<noteq> 0 \<and> c \<noteq> 0")
3.12 + case False then show ?thesis by auto
3.13 + next
3.14 + case True then have "b \<noteq> 0" and "c \<noteq> 0" by auto
3.15 + with `a \<noteq> 0`
3.16 + have "\<And>q r. divmod_rel b c (q, r) \<Longrightarrow> divmod_rel (a * b) (a * c) (q, a * r)"
3.17 + apply (auto simp add: divmod_rel_def)
3.18 + apply (auto simp add: algebra_simps)
3.19 + apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff)
3.20 + apply (simp_all add: mult_less_cancel_left_disj mult_commute [of _ a])
3.21 + done
3.22 + moreover with `c \<noteq> 0` divmod_rel_div_mod have "divmod_rel b c (b div c, b mod c)" by auto
3.23 + ultimately have "divmod_rel (a * b) (a * c) (b div c, a * (b mod c))" .
3.24 + moreover from `a \<noteq> 0` `c \<noteq> 0` have "a * c \<noteq> 0" by simp
3.25 + ultimately show ?thesis by (rule divmod_rel_div)
3.26 + qed
3.27 qed auto
3.28
3.29 lemma posDivAlg_div_mod:
3.30 @@ -808,52 +828,6 @@
3.31 done
3.32
3.33
3.34 -subsection{*Cancellation of Common Factors in div*}
3.35 -
3.36 -lemma zdiv_zmult_zmult1_aux1:
3.37 - "[| (0::int) < b; c \<noteq> 0 |] ==> (c*a) div (c*b) = a div b"
3.38 -by (subst zdiv_zmult2_eq, auto)
3.39 -
3.40 -lemma zdiv_zmult_zmult1_aux2:
3.41 - "[| b < (0::int); c \<noteq> 0 |] ==> (c*a) div (c*b) = a div b"
3.42 -apply (subgoal_tac " (c * (-a)) div (c * (-b)) = (-a) div (-b) ")
3.43 -apply (rule_tac [2] zdiv_zmult_zmult1_aux1, auto)
3.44 -done
3.45 -
3.46 -lemma zdiv_zmult_zmult1: "c \<noteq> (0::int) ==> (c*a) div (c*b) = a div b"
3.47 -apply (case_tac "b = 0", simp)
3.48 -apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
3.49 -done
3.50 -
3.51 -lemma zdiv_zmult_zmult1_if[simp]:
3.52 - "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)"
3.53 -by (simp add:zdiv_zmult_zmult1)
3.54 -
3.55 -
3.56 -subsection{*Distribution of Factors over mod*}
3.57 -
3.58 -lemma zmod_zmult_zmult1_aux1:
3.59 - "[| (0::int) < b; c \<noteq> 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
3.60 -by (subst zmod_zmult2_eq, auto)
3.61 -
3.62 -lemma zmod_zmult_zmult1_aux2:
3.63 - "[| b < (0::int); c \<noteq> 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
3.64 -apply (subgoal_tac " (c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))")
3.65 -apply (rule_tac [2] zmod_zmult_zmult1_aux1, auto)
3.66 -done
3.67 -
3.68 -lemma zmod_zmult_zmult1: "(c*a) mod (c*b) = (c::int) * (a mod b)"
3.69 -apply (case_tac "b = 0", simp)
3.70 -apply (case_tac "c = 0", simp)
3.71 -apply (auto simp add: linorder_neq_iff zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)
3.72 -done
3.73 -
3.74 -lemma zmod_zmult_zmult2: "(a*c) mod (b*c) = (a mod b) * (c::int)"
3.75 -apply (cut_tac c = c in zmod_zmult_zmult1)
3.76 -apply (auto simp add: mult_commute)
3.77 -done
3.78 -
3.79 -
3.80 subsection {*Splitting Rules for div and mod*}
3.81
3.82 text{*The proofs of the two lemmas below are essentially identical*}
3.83 @@ -937,7 +911,7 @@
3.84 right_distrib)
3.85 thus ?thesis
3.86 by (subst zdiv_zadd1_eq,
3.87 - simp add: zdiv_zmult_zmult1 zmod_zmult_zmult1 one_less_a2
3.88 + simp add: mod_mult_mult1 one_less_a2
3.89 div_pos_pos_trivial)
3.90 qed
3.91
3.92 @@ -961,7 +935,7 @@
3.93 then number_of v div (number_of w)
3.94 else (number_of v + (1::int)) div (number_of w))"
3.95 apply (simp only: number_of_eq numeral_simps UNIV_I split: split_if)
3.96 -apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac)
3.97 +apply (simp add: pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac)
3.98 done
3.99
3.100
3.101 @@ -977,7 +951,7 @@
3.102 apply (auto simp add: add_commute [of 1] mult_commute add1_zle_eq
3.103 pos_mod_bound)
3.104 apply (subst mod_add_eq)
3.105 -apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)
3.106 +apply (simp add: mod_mult_mult2 mod_pos_pos_trivial)
3.107 apply (rule mod_pos_pos_trivial)
3.108 apply (auto simp add: mod_pos_pos_trivial ring_distribs)
3.109 apply (subgoal_tac "0 \<le> b mod a", arith, simp)
3.110 @@ -998,7 +972,7 @@
3.111 "number_of (Int.Bit0 v) mod number_of (Int.Bit0 w) =
3.112 (2::int) * (number_of v mod number_of w)"
3.113 apply (simp only: number_of_eq numeral_simps)
3.114 -apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2
3.115 +apply (simp add: mod_mult_mult1 pos_zmod_mult_2
3.116 neg_zmod_mult_2 add_ac)
3.117 done
3.118
3.119 @@ -1008,7 +982,7 @@
3.120 then 2 * (number_of v mod number_of w) + 1
3.121 else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
3.122 apply (simp only: number_of_eq numeral_simps)
3.123 -apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2
3.124 +apply (simp add: mod_mult_mult1 pos_zmod_mult_2
3.125 neg_zmod_mult_2 add_ac)
3.126 done
3.127
3.128 @@ -1090,9 +1064,7 @@
3.129 done
3.130
3.131 lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
3.132 - apply (simp add: dvd_def)
3.133 - apply (auto simp add: zmod_zmult_zmult1)
3.134 - done
3.135 + by (auto elim!: dvdE simp add: mod_mult_mult1)
3.136
3.137 lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
3.138 apply (subgoal_tac "k dvd n * (m div n) + m mod n")
3.139 @@ -1247,9 +1219,9 @@
3.140 lemmas zmod_simps =
3.141 mod_add_left_eq [symmetric]
3.142 mod_add_right_eq [symmetric]
3.143 - IntDiv.zmod_zmult1_eq [symmetric]
3.144 - mod_mult_left_eq [symmetric]
3.145 - IntDiv.zpower_zmod
3.146 + zmod_zmult1_eq [symmetric]
3.147 + mod_mult_left_eq [symmetric]
3.148 + zpower_zmod
3.149 zminus_zmod zdiff_zmod_left zdiff_zmod_right
3.150
3.151 text {* Distributive laws for function @{text nat}. *}
4.1 --- a/src/HOL/Library/Polynomial.thy Wed Apr 15 15:52:37 2009 +0200
4.2 +++ b/src/HOL/Library/Polynomial.thy Thu Apr 16 10:11:34 2009 +0200
4.3 @@ -987,6 +987,30 @@
4.4 by (simp add: pdivmod_rel_def left_distrib)
4.5 thus "(x + z * y) div y = z + x div y"
4.6 by (rule div_poly_eq)
4.7 +next
4.8 + fix x y z :: "'a poly"
4.9 + assume "x \<noteq> 0"
4.10 + show "(x * y) div (x * z) = y div z"
4.11 + proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
4.12 + have "\<And>x::'a poly. pdivmod_rel x 0 0 x"
4.13 + by (rule pdivmod_rel_by_0)
4.14 + then have [simp]: "\<And>x::'a poly. x div 0 = 0"
4.15 + by (rule div_poly_eq)
4.16 + have "\<And>x::'a poly. pdivmod_rel 0 x 0 0"
4.17 + by (rule pdivmod_rel_0)
4.18 + then have [simp]: "\<And>x::'a poly. 0 div x = 0"
4.19 + by (rule div_poly_eq)
4.20 + case False then show ?thesis by auto
4.21 + next
4.22 + case True then have "y \<noteq> 0" and "z \<noteq> 0" by auto
4.23 + with `x \<noteq> 0`
4.24 + have "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> pdivmod_rel (x * y) (x * z) q (x * r)"
4.25 + by (auto simp add: pdivmod_rel_def algebra_simps)
4.26 + (rule classical, simp add: degree_mult_eq)
4.27 + moreover from pdivmod_rel have "pdivmod_rel y z (y div z) (y mod z)" .
4.28 + ultimately have "pdivmod_rel (x * y) (x * z) (y div z) (x * (y mod z))" .
4.29 + then show ?thesis by (simp add: div_poly_eq)
4.30 + qed
4.31 qed
4.32
4.33 end