# HG changeset patch
# User haftmann
# Date 1436379552 -7200
# Node ID a9e45c9588c3679fad39383356c6a7d3a872c41b
# Parent  8a2d7c04d8c0328c759489cc4be3fdccc90e3148
tuned facts

diff -r 8a2d7c04d8c0 -r a9e45c9588c3 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Jul 08 14:01:41 2015 +0200
+++ b/src/HOL/Divides.thy	Wed Jul 08 20:19:12 2015 +0200
@@ -118,8 +118,8 @@
 lemma mod_mult_self2_is_0 [simp]: "a * b mod b = 0"
   using mod_mult_self1 [of 0 a b] by simp
 
-lemma div_by_1 [simp]: "a div 1 = a"
-  using div_mult_self2_is_id [of 1 a] zero_neq_one by simp
+lemma div_by_1: "a div 1 = a"
+  by (fact divide_1)
 
 lemma mod_by_1 [simp]: "a mod 1 = 0"
 proof -
@@ -378,20 +378,6 @@
 lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
   by (fact mod_mult_mult1 [symmetric])
 
-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)
-
 lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
   unfolding dvd_def by (auto simp add: mod_mult_mult1)
 
diff -r 8a2d7c04d8c0 -r a9e45c9588c3 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Wed Jul 08 14:01:41 2015 +0200
+++ b/src/HOL/Fields.thy	Wed Jul 08 20:19:12 2015 +0200
@@ -145,9 +145,6 @@
 lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
 by (simp add: divide_inverse algebra_simps)
 
-lemma divide_1 [simp]: "a / 1 = a"
-  by (simp add: divide_inverse)
-
 lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c"
   by (simp add: divide_inverse mult.assoc)
 
diff -r 8a2d7c04d8c0 -r a9e45c9588c3 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Wed Jul 08 14:01:41 2015 +0200
+++ b/src/HOL/GCD.thy	Wed Jul 08 20:19:12 2015 +0200
@@ -31,51 +31,6 @@
 imports Main
 begin
 
-context semidom_divide
-begin
-
-lemma divide_1 [simp]:
-  "a div 1 = a"
-  using nonzero_mult_divide_cancel_left [of 1 a] by simp
-
-lemma dvd_mult_cancel_left [simp]:
-  assumes "a \<noteq> 0"
-  shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
-proof
-  assume ?P then obtain d where "a * c = a * b * d" ..
-  with assms have "c = b * d" by (simp add: ac_simps)
-  then show ?Q ..
-next
-  assume ?Q then obtain d where "c = b * d" .. 
-  then have "a * c = a * b * d" by (simp add: ac_simps)
-  then show ?P ..
-qed
-  
-lemma dvd_mult_cancel_right [simp]:
-  assumes "a \<noteq> 0"
-  shows "b * a dvd c * a \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
-using dvd_mult_cancel_left [of a b c] assms by (simp add: ac_simps)
-  
-lemma div_dvd_iff_mult:
-  assumes "b \<noteq> 0" and "b dvd a"
-  shows "a div b dvd c \<longleftrightarrow> a dvd c * b"
-proof -
-  from \<open>b dvd a\<close> obtain d where "a = b * d" ..
-  with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps)
-qed
-
-lemma dvd_div_iff_mult:
-  assumes "c \<noteq> 0" and "c dvd b"
-  shows "a dvd b div c \<longleftrightarrow> a * c dvd b"
-proof -
-  from \<open>c dvd b\<close> obtain d where "b = c * d" ..
-  with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
-qed
-
-end
-
-declare One_nat_def [simp del]
-
 subsection {* GCD and LCM definitions *}
 
 class gcd = zero + one + dvd +
@@ -145,6 +100,10 @@
   with False show ?thesis by simp
 qed
 
+lemma is_unit_gcd [simp]:
+  "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
+  by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor)
+
 sublocale gcd!: abel_semigroup gcd
 proof
   fix a b c
@@ -772,7 +731,7 @@
   by simp
 
 lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
-  by (simp add: One_nat_def)
+  by simp
 
 lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1"
   by (simp add: gcd_int_def)
@@ -928,23 +887,29 @@
   apply auto
 done
 
-lemma coprime_dvd_mult_nat: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
-  apply (insert gcd_mult_distrib_nat [of m k n])
-  apply simp
-  apply (erule_tac t = m in ssubst)
-  apply simp
-  done
+context semiring_gcd
+begin
 
-lemma coprime_dvd_mult_int:
-  "coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
-apply (subst abs_dvd_iff [symmetric])
-apply (subst dvd_abs_iff [symmetric])
-apply (subst (asm) gcd_abs_int)
-apply (rule coprime_dvd_mult_nat [transferred])
-    prefer 4 apply assumption
-   apply auto
-apply (subst abs_mult [symmetric], auto)
-done
+lemma coprime_dvd_mult:
+  assumes "coprime a b" and "a dvd c * b"
+  shows "a dvd c"
+proof (cases "c = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  then have unit: "is_unit (unit_factor c)" by simp
+  from \<open>coprime a b\<close> mult_gcd_left [of c a b]
+  have "gcd (c * a) (c * b) * unit_factor c = c"
+    by (simp add: ac_simps)
+  moreover from \<open>a dvd c * b\<close> have "a dvd gcd (c * a) (c * b) * unit_factor c"
+    by (simp add: dvd_mult_unit_iff unit)
+  ultimately show ?thesis by simp
+qed
+
+end
+
+lemmas coprime_dvd_mult_nat = coprime_dvd_mult [where ?'a = nat]
+lemmas coprime_dvd_mult_int = coprime_dvd_mult [where ?'a = int]
 
 lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
     (k dvd m * n) = (k dvd m)"
@@ -954,21 +919,22 @@
     (k dvd m * n) = (k dvd m)"
   by (auto intro: coprime_dvd_mult_int)
 
-lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
-  apply (rule dvd_antisym)
+context semiring_gcd
+begin
+
+lemma gcd_mult_cancel:
+  "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b"
+  apply (rule associated_eqI)
   apply (rule gcd_greatest)
-  apply (rule_tac n = k in coprime_dvd_mult_nat)
-  apply (simp add: gcd_assoc_nat)
-  apply (simp add: gcd_commute_nat)
-  apply (simp_all add: mult.commute)
-done
+  apply (rule_tac b = c in coprime_dvd_mult)
+  apply (simp add: gcd.assoc)
+  apply (simp_all add: ac_simps)
+  done
 
-lemma gcd_mult_cancel_int:
-  "coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n"
-apply (subst (1 2) gcd_abs_int)
-apply (subst abs_mult)
-apply (rule gcd_mult_cancel_nat [transferred], auto)
-done
+end  
+
+lemmas gcd_mult_cancel_nat = gcd_mult_cancel [where ?'a = nat] 
+lemmas gcd_mult_cancel_int = gcd_mult_cancel [where ?'a = int] 
 
 lemma coprime_crossproduct_nat:
   fixes a b c d :: nat
@@ -1121,8 +1087,11 @@
 
 subsection {* Coprimality *}
 
-lemma div_gcd_coprime_nat:
-  assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
+context semiring_gcd
+begin
+
+lemma div_gcd_coprime:
+  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
   shows "coprime (a div gcd a b) (b div gcd a b)"
 proof -
   let ?g = "gcd a b"
@@ -1140,29 +1109,22 @@
     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   have "?g \<noteq> 0" using nz by simp
-  then have gp: "?g > 0" by arith
-  from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
-  with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
+  moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
+  thm dvd_mult_cancel_left
+  ultimately show ?thesis using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
 qed
 
-lemma div_gcd_coprime_int:
-  assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
-  shows "coprime (a div gcd a b) (b div gcd a b)"
-apply (subst (1 2 3) gcd_abs_int)
-apply (subst (1 2) abs_div)
-  apply simp
- apply simp
-apply(subst (1 2) abs_gcd_int)
-apply (rule div_gcd_coprime_nat [transferred])
-using nz apply (auto simp add: gcd_abs_int [symmetric])
-done
+end
+
+lemmas div_gcd_coprime_nat = div_gcd_coprime [where ?'a = nat]
+lemmas div_gcd_coprime_int = div_gcd_coprime [where ?'a = int]
 
 lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   using gcd_unique_nat[of 1 a b, simplified] by auto
 
 lemma coprime_Suc_0_nat:
     "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
-  using coprime_nat by (simp add: One_nat_def)
+  using coprime_nat by simp
 
 lemma coprime_int: "coprime (a::int) b \<longleftrightarrow>
     (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
@@ -1211,22 +1173,23 @@
   using z apply force
   done
 
-lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b"
-    shows "coprime d (a * b)"
-  apply (subst gcd_commute_nat)
-  using da apply (subst gcd_mult_cancel_nat)
-  apply (subst gcd_commute_nat, assumption)
-  apply (subst gcd_commute_nat, rule db)
-done
+context semiring_gcd
+begin
 
-lemma coprime_mult_int: assumes da: "coprime (d::int) a" and db: "coprime d b"
-    shows "coprime d (a * b)"
-  apply (subst gcd_commute_int)
-  using da apply (subst gcd_mult_cancel_int)
-  apply (subst gcd_commute_int, assumption)
-  apply (subst gcd_commute_int, rule db)
-done
+lemma coprime_mult:
+  assumes da: "coprime d a" and db: "coprime d b"
+  shows "coprime d (a * b)"
+  apply (subst gcd.commute)
+  using da apply (subst gcd_mult_cancel)
+  apply (subst gcd.commute, assumption)
+  apply (subst gcd.commute, rule db)
+  done
 
+end
+
+lemmas coprime_mult_nat = coprime_mult [where ?'a = nat]
+lemmas coprime_mult_int = coprime_mult [where ?'a = int]
+  
 lemma coprime_lmult_nat:
   assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
 proof -
@@ -1305,20 +1268,41 @@
 lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
   by (induct n) (simp_all add: coprime_mult_int)
 
+context semiring_gcd
+begin
+
+lemma coprime_exp_left:
+  assumes "coprime a b"
+  shows "coprime (a ^ n) b"
+  using assms by (induct n) (simp_all add: gcd_mult_cancel)
+
+lemma coprime_exp2:
+  assumes "coprime a b"
+  shows "coprime (a ^ n) (b ^ m)"
+proof (rule coprime_exp_left)
+  from assms show "coprime a (b ^ m)"
+    by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a])
+qed
+
+end
+
 lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
-  by (simp add: coprime_exp_nat ac_simps)
+  by (fact coprime_exp2)
 
 lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
-  by (simp add: coprime_exp_int ac_simps)
+  by (fact coprime_exp2)
 
-lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
-proof (cases)
-  assume "a = 0 & b = 0"
-  thus ?thesis by simp
-  next assume "~(a = 0 & b = 0)"
-  hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
-    by (auto simp:div_gcd_coprime_nat)
-  hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
+lemma gcd_exp_nat:
+  "gcd ((a :: nat) ^ n) (b ^ n) = gcd a b ^ n"
+proof (cases "a = 0 \<and> b = 0")
+  case True then show ?thesis by (cases "n > 0") (simp_all add: zero_power)
+next
+  case False
+  then have "coprime (a div gcd a b) (b div gcd a b)"
+    by (auto simp: div_gcd_coprime)
+  then have "coprime ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
+    by (simp add: coprime_exp2)
+  then have "gcd ((a div gcd a b)^n * (gcd a b)^n)
       ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
     by (metis gcd_mult_distrib_nat mult.commute mult.right_neutral)
   also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
@@ -1373,7 +1357,7 @@
     with dc have th0: "a' dvd b*c"
       using dvd_trans[of a' a "b*c"] by simp
     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
-    hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc)
+    hence "?g*a' dvd ?g * (b' * c)" by (simp add: ac_simps)
     with z have th_1: "a' dvd b' * c" by auto
     from coprime_dvd_mult_int[OF ab'(3)] th_1
     have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
@@ -1471,10 +1455,10 @@
 qed
 
 lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
-  by (simp add: gcd.commute)
+  by (simp add: gcd.commute del: One_nat_def)
 
 lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
-  using coprime_plus_one_nat by (simp add: One_nat_def)
+  using coprime_plus_one_nat by simp
 
 lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
   by (simp add: gcd.commute)
@@ -1850,7 +1834,7 @@
 
 interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
   + lcm_nat: semilattice_neutr "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat" 1
-  by standard simp_all
+  by standard (simp_all del: One_nat_def)
 
 interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int" ..
 
@@ -1950,11 +1934,11 @@
 
 lemma Lcm_nat_empty:
   "Lcm {} = (1::nat)"
-  by (simp add: Lcm_nat_def)
+  by (simp add: Lcm_nat_def del: One_nat_def)
 
 lemma Lcm_nat_insert:
   "Lcm (insert n M) = lcm (n::nat) (Lcm M)"
-  by (cases "finite M") (simp_all add: Lcm_nat_def Lcm_nat_infinite)
+  by (cases "finite M") (simp_all add: Lcm_nat_def Lcm_nat_infinite del: One_nat_def)
 
 definition
   "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
@@ -2107,7 +2091,7 @@
 lemma mult_inj_if_coprime_nat:
   "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
    \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
-apply(auto simp add:inj_on_def)
+apply (auto simp add: inj_on_def simp del: One_nat_def)
 apply (metis coprime_dvd_mult_iff_nat dvd.neq_le_trans dvd_triv_left)
 apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
              dvd.neq_le_trans dvd_triv_right mult.commute)
diff -r 8a2d7c04d8c0 -r a9e45c9588c3 src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 08 14:01:41 2015 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 08 20:19:12 2015 +0200
@@ -794,15 +794,15 @@
 
 lemma dvd_lcm_D1:
   "lcm m n dvd k \<Longrightarrow> m dvd k"
-  by (rule dvd_trans, rule lcm_dvd1, assumption)
+  by (rule dvd_trans, rule dvd_lcm1, assumption)
 
 lemma dvd_lcm_D2:
   "lcm m n dvd k \<Longrightarrow> n dvd k"
-  by (rule dvd_trans, rule lcm_dvd2, assumption)
+  by (rule dvd_trans, rule dvd_lcm2, assumption)
 
 lemma gcd_dvd_lcm [simp]:
   "gcd a b dvd lcm a b"
-  by (metis dvd_trans gcd_dvd2 lcm_dvd2)
+  using gcd_dvd2 by (rule dvd_lcmI2)
 
 lemma lcm_1_iff:
   "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
@@ -830,14 +830,6 @@
   (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
   by rule (auto intro: lcmI simp: lcm_least lcm_zero)
 
-lemma dvd_lcm_I1 [simp]:
-  "k dvd m \<Longrightarrow> k dvd lcm m n"
-  by (metis lcm_dvd1 dvd_trans)
-
-lemma dvd_lcm_I2 [simp]:
-  "k dvd n \<Longrightarrow> k dvd lcm m n"
-  by (metis lcm_dvd2 dvd_trans)
-
 lemma lcm_coprime:
   "gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)"
   by (subst lcm_gcd) simp
@@ -874,8 +866,8 @@
   assumes "a \<noteq> 0" and "b \<noteq> 0"
   shows "euclidean_size a \<le> euclidean_size (lcm a b)"
 proof -
-  have "a dvd lcm a b" by (rule lcm_dvd1)
-  then obtain c where A: "lcm a b = a * c" unfolding dvd_def by blast
+  have "a dvd lcm a b" by (rule dvd_lcm1)
+  then obtain c where A: "lcm a b = a * c" ..
   with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "c \<noteq> 0" by (auto simp: lcm_zero)
   then show ?thesis by (subst A, intro size_mult_mono)
 qed
@@ -905,12 +897,7 @@
 
 lemma lcm_mult_unit1:
   "is_unit a \<Longrightarrow> lcm (b * a) c = lcm b c"
-  apply (rule lcmI)
-  apply (rule dvd_trans[of _ "b * a"], simp, rule lcm_dvd1)
-  apply (rule lcm_dvd2)
-  apply (rule lcm_least, simp add: unit_simps, assumption)
-  apply simp
-  done
+  by (rule associated_eqI) (simp_all add: mult_unit_dvd_iff dvd_lcmI1)
 
 lemma lcm_mult_unit2:
   "is_unit a \<Longrightarrow> lcm b (c * a) = lcm b c"
@@ -944,22 +931,11 @@
 
 lemma lcm_left_idem:
   "lcm a (lcm a b) = lcm a b"
-  apply (rule lcmI)
-  apply simp
-  apply (subst lcm.assoc [symmetric], rule lcm_dvd2)
-  apply (rule lcm_least, assumption)
-  apply (erule (1) lcm_least)
-  apply (auto simp: lcm_zero)
-  done
+  by (rule associated_eqI) simp_all
 
 lemma lcm_right_idem:
   "lcm (lcm a b) b = lcm a b"
-  apply (rule lcmI)
-  apply (subst lcm.assoc, rule lcm_dvd1)
-  apply (rule lcm_dvd2)
-  apply (rule lcm_least, erule (1) lcm_least, assumption)
-  apply (auto simp: lcm_zero)
-  done
+  by (rule associated_eqI) simp_all
 
 lemma comp_fun_idem_lcm: "comp_fun_idem lcm"
 proof
@@ -1012,10 +988,10 @@
         also note \<open>euclidean_size l = n\<close>
         finally show "euclidean_size (gcd l l') \<le> n" .
       qed
-      ultimately have "euclidean_size l = euclidean_size (gcd l l')" 
+      ultimately have *: "euclidean_size l = euclidean_size (gcd l l')" 
         by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>)
-      with \<open>l \<noteq> 0\<close> have "l dvd gcd l l'"
-        using dvd_euclidean_size_eq_imp_dvd by auto
+      from \<open>l \<noteq> 0\<close> have "l dvd gcd l l'"
+        by (rule dvd_euclidean_size_eq_imp_dvd) (auto simp add: *)
       hence "l dvd l'" by (blast dest: dvd_gcd_D2)
     }
 
diff -r 8a2d7c04d8c0 -r a9e45c9588c3 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Wed Jul 08 14:01:41 2015 +0200
+++ b/src/HOL/Rings.thy	Wed Jul 08 20:19:12 2015 +0200
@@ -629,6 +629,44 @@
   then show ?thesis by simp
 qed 
 
+lemma divide_1 [simp]:
+  "a div 1 = a"
+  using nonzero_mult_divide_cancel_left [of 1 a] by simp
+
+lemma dvd_times_left_cancel_iff [simp]:
+  assumes "a \<noteq> 0"
+  shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?P then obtain d where "a * c = a * b * d" ..
+  with assms have "c = b * d" by (simp add: ac_simps)
+  then show ?Q ..
+next
+  assume ?Q then obtain d where "c = b * d" .. 
+  then have "a * c = a * b * d" by (simp add: ac_simps)
+  then show ?P ..
+qed
+  
+lemma dvd_times_right_cancel_iff [simp]:
+  assumes "a \<noteq> 0"
+  shows "b * a dvd c * a \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
+using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps)
+  
+lemma div_dvd_iff_mult:
+  assumes "b \<noteq> 0" and "b dvd a"
+  shows "a div b dvd c \<longleftrightarrow> a dvd c * b"
+proof -
+  from \<open>b dvd a\<close> obtain d where "a = b * d" ..
+  with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps)
+qed
+
+lemma dvd_div_iff_mult:
+  assumes "c \<noteq> 0" and "c dvd b"
+  shows "a dvd b div c \<longleftrightarrow> a * c dvd b"
+proof -
+  from \<open>c dvd b\<close> obtain d where "b = c * d" ..
+  with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
+qed
+
 end
 
 class idom_divide = idom + semidom_divide
diff -r 8a2d7c04d8c0 -r a9e45c9588c3 src/HOL/ex/Sqrt.thy
--- a/src/HOL/ex/Sqrt.thy	Wed Jul 08 14:01:41 2015 +0200
+++ b/src/HOL/ex/Sqrt.thy	Wed Jul 08 20:19:12 2015 +0200
@@ -18,7 +18,7 @@
   assume "sqrt p \<in> \<rat>"
   then obtain m n :: nat where
       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
-    and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
+    and "coprime m n" by (rule Rats_abs_nat_div_natE)
   have eq: "m\<^sup>2 = p * n\<^sup>2"
   proof -
     from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp
@@ -38,9 +38,8 @@
     then have "p dvd n\<^sup>2" ..
     with \<open>prime p\<close> show "p dvd n" by (rule prime_dvd_power_nat)
   qed
-  then have "p dvd gcd m n" ..
-  with gcd have "p dvd 1" by simp
-  then have "p \<le> 1" by (simp add: dvd_imp_le)
+  then have "p dvd gcd m n" by simp
+  with \<open>coprime m n\<close> have "p = 1" by simp
   with p show False by simp
 qed
 
@@ -64,7 +63,7 @@
   assume "sqrt p \<in> \<rat>"
   then obtain m n :: nat where
       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
-    and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
+    and "coprime m n" by (rule Rats_abs_nat_div_natE)
   from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp
   then have "m\<^sup>2 = (sqrt p)\<^sup>2 * n\<^sup>2"
     by (auto simp add: power2_eq_square)
@@ -79,8 +78,7 @@
   then have "p dvd n\<^sup>2" ..
   with \<open>prime p\<close> have "p dvd n" by (rule prime_dvd_power_nat)
   with dvd_m have "p dvd gcd m n" by (rule gcd_greatest_nat)
-  with gcd have "p dvd 1" by simp
-  then have "p \<le> 1" by (simp add: dvd_imp_le)
+  with \<open>coprime m n\<close> have "p = 1" by simp
   with p show False by simp
 qed