# HG changeset patch
# User haftmann
# Date 1415523797 -3600
# Node ID 2e19b392d9e3ca0fbe83141637c74031f754ec05
# Parent  5d82cdef6c1b95039a37f0402db1e1566e8e8db8
self-contained simp rules for dvd on numerals

diff -r 5d82cdef6c1b -r 2e19b392d9e3 src/HOL/Divides.thy
--- 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 *}
diff -r 5d82cdef6c1b -r 2e19b392d9e3 src/HOL/Matrix_LP/ComputeNumeral.thy
--- 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
 
diff -r 5d82cdef6c1b -r 2e19b392d9e3 src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- 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"