--- a/src/HOL/Divides.thy Sat Nov 08 16:53:26 2014 +0100
+++ b/src/HOL/Divides.thy Sun Nov 09 10:03:17 2014 +0100
@@ -26,6 +26,8 @@
and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
begin
+subclass semiring_no_zero_divisors ..
+
text {* @{const div} and @{const mod} *}
lemma mod_div_equality2: "b * (a div b) + a mod b = a"
@@ -539,8 +541,8 @@
case False
from mod_div_equality have "1 div 2 * 2 + 1 mod 2 = 1" .
with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
- then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq)
- then have "1 div 2 = 0 \<or> 2 = 0" by (rule divisors_zero)
+ then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
+ then have "1 div 2 = 0 \<or> 2 = 0" by simp
with False show ?thesis by auto
qed
@@ -641,6 +643,20 @@
"a - 0 = a"
by (rule diff_invert_add1 [symmetric]) simp
+lemma dvd_times_left_cancel_iff [simp]: -- \<open>FIXME generalize\<close>
+ assumes "c \<noteq> 0"
+ shows "c * a dvd c * b \<longleftrightarrow> a dvd b"
+proof -
+ have "(c * b) mod (c * a) = 0 \<longleftrightarrow> b mod a = 0" (is "?P \<longleftrightarrow> ?Q")
+ using assms by (simp add: mod_mult_mult1)
+ then show ?thesis by (simp add: mod_eq_0_iff_dvd)
+qed
+
+lemma dvd_times_right_cancel_iff [simp]: -- \<open>FIXME generalize\<close>
+ assumes "c \<noteq> 0"
+ shows "a * c dvd b * c \<longleftrightarrow> a dvd b"
+ using assms dvd_times_left_cancel_iff [of c a b] by (simp add: ac_simps)
+
subclass semiring_div_parity
proof
fix a
@@ -799,7 +815,12 @@
with False show ?thesis by simp
qed
-lemma divmod_cancel [code]:
+lemma divmod_eq [simp]:
+ "m < n \<Longrightarrow> divmod m n = (0, numeral m)"
+ "n \<le> m \<Longrightarrow> divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
+ by (auto simp add: divmod_divmod_step [of m n])
+
+lemma divmod_cancel [simp, code]:
"divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
"divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q)
proof -
@@ -810,7 +831,21 @@
then show ?P and ?Q
by (simp_all add: prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2] add.commute del: numeral_times_numeral)
- qed
+qed
+
+text {* Special case: divisibility *}
+
+definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
+where
+ "divides_aux qr \<longleftrightarrow> snd qr = 0"
+
+lemma divides_aux_eq [simp]:
+ "divides_aux (q, r) \<longleftrightarrow> r = 0"
+ by (simp add: divides_aux_def)
+
+lemma dvd_numeral_simp [simp]:
+ "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"
+ by (simp add: divmod_def mod_eq_0_iff_dvd)
end
@@ -2556,8 +2591,9 @@
subsubsection {* The Divides Relation *}
-lemmas dvd_eq_mod_eq_0_numeral [simp] =
- dvd_eq_mod_eq_0 [of "numeral x" "numeral y"] for x y
+lemma dvd_eq_mod_eq_0_numeral:
+ "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semiring_div)"
+ by (fact dvd_eq_mod_eq_0)
subsubsection {* Further properties *}
--- a/src/HOL/Matrix_LP/ComputeNumeral.thy Sat Nov 08 16:53:26 2014 +0100
+++ b/src/HOL/Matrix_LP/ComputeNumeral.thy Sun Nov 09 10:03:17 2014 +0100
@@ -71,10 +71,10 @@
by simp
lemma even_Bit0_int: "even (numeral (Num.Bit0 x) :: int) = True"
- by simp
+ by (simp only: even_numeral)
lemma even_Bit1_int: "even (numeral (Num.Bit1 x) :: int) = False"
- by simp
+ by (simp only: odd_numeral)
lemmas compute_even = even_0_int even_One_int even_Bit0_int even_Bit1_int
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sat Nov 08 16:53:26 2014 +0100
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sun Nov 09 10:03:17 2014 +0100
@@ -108,7 +108,7 @@
lemma ring_inv_is_inv1 [simp]:
"is_unit a \<Longrightarrow> a * ring_inv a = 1"
- unfolding is_unit_def ring_inv_def by (simp add: dvd_mult_div_cancel)
+ unfolding is_unit_def ring_inv_def by simp
lemma ring_inv_is_inv2 [simp]:
"is_unit a \<Longrightarrow> ring_inv a * a = 1"
@@ -1034,19 +1034,19 @@
proof (cases "a * b = 0")
let ?nf = normalisation_factor
assume "a * b \<noteq> 0"
- hence "gcd a b \<noteq> 0" by (auto simp add: gcd_zero)
+ hence "gcd a b \<noteq> 0" by simp
from lcm_gcd have "lcm a b * gcd a b = gcd a b * (a * b div (?nf (a*b) * gcd a b))"
by (simp add: mult_ac)
also from `a * b \<noteq> 0` have "... = a * b div ?nf (a*b)"
- by (simp_all add: unit_ring_inv'1 dvd_mult_div_cancel unit_ring_inv)
+ by (simp_all add: unit_ring_inv'1 unit_ring_inv)
finally show ?thesis .
-qed (simp add: lcm_gcd)
+qed (auto simp add: lcm_gcd)
lemma lcm_dvd1 [iff]:
"x dvd lcm x y"
proof (cases "x*y = 0")
assume "x * y \<noteq> 0"
- hence "gcd x y \<noteq> 0" by (auto simp: gcd_zero)
+ hence "gcd x y \<noteq> 0" by simp
let ?c = "ring_inv (normalisation_factor (x*y))"
from `x * y \<noteq> 0` have [simp]: "is_unit (normalisation_factor (x*y))" by simp
from lcm_gcd_prod[of x y] have "lcm x y * gcd x y = x * ?c * y"
@@ -1057,7 +1057,7 @@
also have "... = x * (?c * y div gcd x y)"
by (metis div_mult_swap gcd_dvd2 mult_assoc)
finally show ?thesis by (rule dvdI)
-qed (simp add: lcm_gcd)
+qed (auto simp add: lcm_gcd)
lemma lcm_least:
"\<lbrakk>a dvd k; b dvd k\<rbrakk> \<Longrightarrow> lcm a b dvd k"
@@ -1067,17 +1067,17 @@
hence "is_unit (?nf k)" by simp
hence "?nf k \<noteq> 0" by (metis not_is_unit_0)
assume A: "a dvd k" "b dvd k"
- hence "gcd a b \<noteq> 0" using `k \<noteq> 0` by (auto simp add: gcd_zero)
+ hence "gcd a b \<noteq> 0" using `k \<noteq> 0` by auto
from A obtain r s where ar: "k = a * r" and bs: "k = b * s"
unfolding dvd_def by blast
- with `k \<noteq> 0` have "r * s \<noteq> 0"
- by (intro notI) (drule divisors_zero, elim disjE, simp_all)
+ with `k \<noteq> 0` have "r * s \<noteq> 0"
+ by auto (drule sym [of 0], simp)
hence "is_unit (?nf (r * s))" by simp
let ?c = "?nf k div ?nf (r*s)"
from `is_unit (?nf k)` and `is_unit (?nf (r * s))` have "is_unit ?c" by (rule unit_div)
hence "?c \<noteq> 0" using not_is_unit_0 by fast
from ar bs have "k * k * gcd s r = ?nf k * k * gcd (k * s) (k * r)"
- by (subst mult_assoc, subst gcd_mult_distrib[of k s r], simp only: ac_simps mult_assoc)
+ by (subst mult_assoc, subst gcd_mult_distrib[of k s r], simp only: ac_simps)
also have "... = ?nf k * k * gcd ((r*s) * a) ((r*s) * b)"
by (subst (3) `k = a * r`, subst (3) `k = b * s`, simp add: algebra_simps)
also have "... = ?c * r*s * k * gcd a b" using `r * s \<noteq> 0`
@@ -1138,7 +1138,7 @@
"normalisation_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
proof (cases "a = 0 \<or> b = 0")
case True then show ?thesis
- by (simp add: lcm_gcd) (metis div_0 ac_simps mult_zero_left normalisation_factor_0)
+ by (auto simp add: lcm_gcd)
next
case False
let ?nf = normalisation_factor
@@ -1146,8 +1146,8 @@
have "?nf (lcm a b) * ?nf (gcd a b) = ?nf (a*b) div ?nf (a*b)"
by (metis div_by_0 div_self normalisation_correct normalisation_factor_0 normalisation_factor_mult)
also have "... = (if a*b = 0 then 0 else 1)"
- by (cases "a*b = 0", simp, subst div_self, metis dvd_0_left normalisation_factor_dvd, simp)
- finally show ?thesis using False by (simp add: no_zero_divisors)
+ by simp
+ finally show ?thesis using False by simp
qed
lemma lcm_dvd2 [iff]: "y dvd lcm x y"