tuned facts
authorhaftmann
Wed Jul 08 20:19:12 2015 +0200 (2015-07-08)
changeset 60690a9e45c9588c3
parent 60689 8a2d7c04d8c0
child 60700 7536369a5546
child 60701 61352c31b273
tuned facts
src/HOL/Divides.thy
src/HOL/Fields.thy
src/HOL/GCD.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
src/HOL/Rings.thy
src/HOL/ex/Sqrt.thy
     1.1 --- a/src/HOL/Divides.thy	Wed Jul 08 14:01:41 2015 +0200
     1.2 +++ b/src/HOL/Divides.thy	Wed Jul 08 20:19:12 2015 +0200
     1.3 @@ -118,8 +118,8 @@
     1.4  lemma mod_mult_self2_is_0 [simp]: "a * b mod b = 0"
     1.5    using mod_mult_self1 [of 0 a b] by simp
     1.6  
     1.7 -lemma div_by_1 [simp]: "a div 1 = a"
     1.8 -  using div_mult_self2_is_id [of 1 a] zero_neq_one by simp
     1.9 +lemma div_by_1: "a div 1 = a"
    1.10 +  by (fact divide_1)
    1.11  
    1.12  lemma mod_by_1 [simp]: "a mod 1 = 0"
    1.13  proof -
    1.14 @@ -378,20 +378,6 @@
    1.15  lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
    1.16    by (fact mod_mult_mult1 [symmetric])
    1.17  
    1.18 -lemma dvd_times_left_cancel_iff [simp]: -- \<open>FIXME generalize\<close>
    1.19 -  assumes "c \<noteq> 0"
    1.20 -  shows "c * a dvd c * b \<longleftrightarrow> a dvd b"
    1.21 -proof -
    1.22 -  have "(c * b) mod (c * a) = 0 \<longleftrightarrow> b mod a = 0" (is "?P \<longleftrightarrow> ?Q")
    1.23 -    using assms by (simp add: mod_mult_mult1)
    1.24 -  then show ?thesis by (simp add: mod_eq_0_iff_dvd)
    1.25 -qed
    1.26 -
    1.27 -lemma dvd_times_right_cancel_iff [simp]: -- \<open>FIXME generalize\<close>
    1.28 -  assumes "c \<noteq> 0"
    1.29 -  shows "a * c dvd b * c \<longleftrightarrow> a dvd b"
    1.30 -  using assms dvd_times_left_cancel_iff [of c a b] by (simp add: ac_simps)
    1.31 -
    1.32  lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
    1.33    unfolding dvd_def by (auto simp add: mod_mult_mult1)
    1.34  
     2.1 --- a/src/HOL/Fields.thy	Wed Jul 08 14:01:41 2015 +0200
     2.2 +++ b/src/HOL/Fields.thy	Wed Jul 08 20:19:12 2015 +0200
     2.3 @@ -145,9 +145,6 @@
     2.4  lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
     2.5  by (simp add: divide_inverse algebra_simps)
     2.6  
     2.7 -lemma divide_1 [simp]: "a / 1 = a"
     2.8 -  by (simp add: divide_inverse)
     2.9 -
    2.10  lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c"
    2.11    by (simp add: divide_inverse mult.assoc)
    2.12  
     3.1 --- a/src/HOL/GCD.thy	Wed Jul 08 14:01:41 2015 +0200
     3.2 +++ b/src/HOL/GCD.thy	Wed Jul 08 20:19:12 2015 +0200
     3.3 @@ -31,51 +31,6 @@
     3.4  imports Main
     3.5  begin
     3.6  
     3.7 -context semidom_divide
     3.8 -begin
     3.9 -
    3.10 -lemma divide_1 [simp]:
    3.11 -  "a div 1 = a"
    3.12 -  using nonzero_mult_divide_cancel_left [of 1 a] by simp
    3.13 -
    3.14 -lemma dvd_mult_cancel_left [simp]:
    3.15 -  assumes "a \<noteq> 0"
    3.16 -  shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
    3.17 -proof
    3.18 -  assume ?P then obtain d where "a * c = a * b * d" ..
    3.19 -  with assms have "c = b * d" by (simp add: ac_simps)
    3.20 -  then show ?Q ..
    3.21 -next
    3.22 -  assume ?Q then obtain d where "c = b * d" .. 
    3.23 -  then have "a * c = a * b * d" by (simp add: ac_simps)
    3.24 -  then show ?P ..
    3.25 -qed
    3.26 -  
    3.27 -lemma dvd_mult_cancel_right [simp]:
    3.28 -  assumes "a \<noteq> 0"
    3.29 -  shows "b * a dvd c * a \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
    3.30 -using dvd_mult_cancel_left [of a b c] assms by (simp add: ac_simps)
    3.31 -  
    3.32 -lemma div_dvd_iff_mult:
    3.33 -  assumes "b \<noteq> 0" and "b dvd a"
    3.34 -  shows "a div b dvd c \<longleftrightarrow> a dvd c * b"
    3.35 -proof -
    3.36 -  from \<open>b dvd a\<close> obtain d where "a = b * d" ..
    3.37 -  with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps)
    3.38 -qed
    3.39 -
    3.40 -lemma dvd_div_iff_mult:
    3.41 -  assumes "c \<noteq> 0" and "c dvd b"
    3.42 -  shows "a dvd b div c \<longleftrightarrow> a * c dvd b"
    3.43 -proof -
    3.44 -  from \<open>c dvd b\<close> obtain d where "b = c * d" ..
    3.45 -  with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
    3.46 -qed
    3.47 -
    3.48 -end
    3.49 -
    3.50 -declare One_nat_def [simp del]
    3.51 -
    3.52  subsection {* GCD and LCM definitions *}
    3.53  
    3.54  class gcd = zero + one + dvd +
    3.55 @@ -145,6 +100,10 @@
    3.56    with False show ?thesis by simp
    3.57  qed
    3.58  
    3.59 +lemma is_unit_gcd [simp]:
    3.60 +  "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
    3.61 +  by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor)
    3.62 +
    3.63  sublocale gcd!: abel_semigroup gcd
    3.64  proof
    3.65    fix a b c
    3.66 @@ -772,7 +731,7 @@
    3.67    by simp
    3.68  
    3.69  lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
    3.70 -  by (simp add: One_nat_def)
    3.71 +  by simp
    3.72  
    3.73  lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1"
    3.74    by (simp add: gcd_int_def)
    3.75 @@ -928,23 +887,29 @@
    3.76    apply auto
    3.77  done
    3.78  
    3.79 -lemma coprime_dvd_mult_nat: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
    3.80 -  apply (insert gcd_mult_distrib_nat [of m k n])
    3.81 -  apply simp
    3.82 -  apply (erule_tac t = m in ssubst)
    3.83 -  apply simp
    3.84 -  done
    3.85 +context semiring_gcd
    3.86 +begin
    3.87  
    3.88 -lemma coprime_dvd_mult_int:
    3.89 -  "coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
    3.90 -apply (subst abs_dvd_iff [symmetric])
    3.91 -apply (subst dvd_abs_iff [symmetric])
    3.92 -apply (subst (asm) gcd_abs_int)
    3.93 -apply (rule coprime_dvd_mult_nat [transferred])
    3.94 -    prefer 4 apply assumption
    3.95 -   apply auto
    3.96 -apply (subst abs_mult [symmetric], auto)
    3.97 -done
    3.98 +lemma coprime_dvd_mult:
    3.99 +  assumes "coprime a b" and "a dvd c * b"
   3.100 +  shows "a dvd c"
   3.101 +proof (cases "c = 0")
   3.102 +  case True then show ?thesis by simp
   3.103 +next
   3.104 +  case False
   3.105 +  then have unit: "is_unit (unit_factor c)" by simp
   3.106 +  from \<open>coprime a b\<close> mult_gcd_left [of c a b]
   3.107 +  have "gcd (c * a) (c * b) * unit_factor c = c"
   3.108 +    by (simp add: ac_simps)
   3.109 +  moreover from \<open>a dvd c * b\<close> have "a dvd gcd (c * a) (c * b) * unit_factor c"
   3.110 +    by (simp add: dvd_mult_unit_iff unit)
   3.111 +  ultimately show ?thesis by simp
   3.112 +qed
   3.113 +
   3.114 +end
   3.115 +
   3.116 +lemmas coprime_dvd_mult_nat = coprime_dvd_mult [where ?'a = nat]
   3.117 +lemmas coprime_dvd_mult_int = coprime_dvd_mult [where ?'a = int]
   3.118  
   3.119  lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
   3.120      (k dvd m * n) = (k dvd m)"
   3.121 @@ -954,21 +919,22 @@
   3.122      (k dvd m * n) = (k dvd m)"
   3.123    by (auto intro: coprime_dvd_mult_int)
   3.124  
   3.125 -lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
   3.126 -  apply (rule dvd_antisym)
   3.127 +context semiring_gcd
   3.128 +begin
   3.129 +
   3.130 +lemma gcd_mult_cancel:
   3.131 +  "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b"
   3.132 +  apply (rule associated_eqI)
   3.133    apply (rule gcd_greatest)
   3.134 -  apply (rule_tac n = k in coprime_dvd_mult_nat)
   3.135 -  apply (simp add: gcd_assoc_nat)
   3.136 -  apply (simp add: gcd_commute_nat)
   3.137 -  apply (simp_all add: mult.commute)
   3.138 -done
   3.139 +  apply (rule_tac b = c in coprime_dvd_mult)
   3.140 +  apply (simp add: gcd.assoc)
   3.141 +  apply (simp_all add: ac_simps)
   3.142 +  done
   3.143  
   3.144 -lemma gcd_mult_cancel_int:
   3.145 -  "coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n"
   3.146 -apply (subst (1 2) gcd_abs_int)
   3.147 -apply (subst abs_mult)
   3.148 -apply (rule gcd_mult_cancel_nat [transferred], auto)
   3.149 -done
   3.150 +end  
   3.151 +
   3.152 +lemmas gcd_mult_cancel_nat = gcd_mult_cancel [where ?'a = nat] 
   3.153 +lemmas gcd_mult_cancel_int = gcd_mult_cancel [where ?'a = int] 
   3.154  
   3.155  lemma coprime_crossproduct_nat:
   3.156    fixes a b c d :: nat
   3.157 @@ -1121,8 +1087,11 @@
   3.158  
   3.159  subsection {* Coprimality *}
   3.160  
   3.161 -lemma div_gcd_coprime_nat:
   3.162 -  assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
   3.163 +context semiring_gcd
   3.164 +begin
   3.165 +
   3.166 +lemma div_gcd_coprime:
   3.167 +  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
   3.168    shows "coprime (a div gcd a b) (b div gcd a b)"
   3.169  proof -
   3.170    let ?g = "gcd a b"
   3.171 @@ -1140,29 +1109,22 @@
   3.172      by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
   3.173        dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   3.174    have "?g \<noteq> 0" using nz by simp
   3.175 -  then have gp: "?g > 0" by arith
   3.176 -  from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   3.177 -  with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
   3.178 +  moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   3.179 +  thm dvd_mult_cancel_left
   3.180 +  ultimately show ?thesis using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
   3.181  qed
   3.182  
   3.183 -lemma div_gcd_coprime_int:
   3.184 -  assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
   3.185 -  shows "coprime (a div gcd a b) (b div gcd a b)"
   3.186 -apply (subst (1 2 3) gcd_abs_int)
   3.187 -apply (subst (1 2) abs_div)
   3.188 -  apply simp
   3.189 - apply simp
   3.190 -apply(subst (1 2) abs_gcd_int)
   3.191 -apply (rule div_gcd_coprime_nat [transferred])
   3.192 -using nz apply (auto simp add: gcd_abs_int [symmetric])
   3.193 -done
   3.194 +end
   3.195 +
   3.196 +lemmas div_gcd_coprime_nat = div_gcd_coprime [where ?'a = nat]
   3.197 +lemmas div_gcd_coprime_int = div_gcd_coprime [where ?'a = int]
   3.198  
   3.199  lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   3.200    using gcd_unique_nat[of 1 a b, simplified] by auto
   3.201  
   3.202  lemma coprime_Suc_0_nat:
   3.203      "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
   3.204 -  using coprime_nat by (simp add: One_nat_def)
   3.205 +  using coprime_nat by simp
   3.206  
   3.207  lemma coprime_int: "coprime (a::int) b \<longleftrightarrow>
   3.208      (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   3.209 @@ -1211,22 +1173,23 @@
   3.210    using z apply force
   3.211    done
   3.212  
   3.213 -lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b"
   3.214 -    shows "coprime d (a * b)"
   3.215 -  apply (subst gcd_commute_nat)
   3.216 -  using da apply (subst gcd_mult_cancel_nat)
   3.217 -  apply (subst gcd_commute_nat, assumption)
   3.218 -  apply (subst gcd_commute_nat, rule db)
   3.219 -done
   3.220 +context semiring_gcd
   3.221 +begin
   3.222  
   3.223 -lemma coprime_mult_int: assumes da: "coprime (d::int) a" and db: "coprime d b"
   3.224 -    shows "coprime d (a * b)"
   3.225 -  apply (subst gcd_commute_int)
   3.226 -  using da apply (subst gcd_mult_cancel_int)
   3.227 -  apply (subst gcd_commute_int, assumption)
   3.228 -  apply (subst gcd_commute_int, rule db)
   3.229 -done
   3.230 +lemma coprime_mult:
   3.231 +  assumes da: "coprime d a" and db: "coprime d b"
   3.232 +  shows "coprime d (a * b)"
   3.233 +  apply (subst gcd.commute)
   3.234 +  using da apply (subst gcd_mult_cancel)
   3.235 +  apply (subst gcd.commute, assumption)
   3.236 +  apply (subst gcd.commute, rule db)
   3.237 +  done
   3.238  
   3.239 +end
   3.240 +
   3.241 +lemmas coprime_mult_nat = coprime_mult [where ?'a = nat]
   3.242 +lemmas coprime_mult_int = coprime_mult [where ?'a = int]
   3.243 +  
   3.244  lemma coprime_lmult_nat:
   3.245    assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
   3.246  proof -
   3.247 @@ -1305,20 +1268,41 @@
   3.248  lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
   3.249    by (induct n) (simp_all add: coprime_mult_int)
   3.250  
   3.251 +context semiring_gcd
   3.252 +begin
   3.253 +
   3.254 +lemma coprime_exp_left:
   3.255 +  assumes "coprime a b"
   3.256 +  shows "coprime (a ^ n) b"
   3.257 +  using assms by (induct n) (simp_all add: gcd_mult_cancel)
   3.258 +
   3.259 +lemma coprime_exp2:
   3.260 +  assumes "coprime a b"
   3.261 +  shows "coprime (a ^ n) (b ^ m)"
   3.262 +proof (rule coprime_exp_left)
   3.263 +  from assms show "coprime a (b ^ m)"
   3.264 +    by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a])
   3.265 +qed
   3.266 +
   3.267 +end
   3.268 +
   3.269  lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
   3.270 -  by (simp add: coprime_exp_nat ac_simps)
   3.271 +  by (fact coprime_exp2)
   3.272  
   3.273  lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
   3.274 -  by (simp add: coprime_exp_int ac_simps)
   3.275 +  by (fact coprime_exp2)
   3.276  
   3.277 -lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
   3.278 -proof (cases)
   3.279 -  assume "a = 0 & b = 0"
   3.280 -  thus ?thesis by simp
   3.281 -  next assume "~(a = 0 & b = 0)"
   3.282 -  hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
   3.283 -    by (auto simp:div_gcd_coprime_nat)
   3.284 -  hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
   3.285 +lemma gcd_exp_nat:
   3.286 +  "gcd ((a :: nat) ^ n) (b ^ n) = gcd a b ^ n"
   3.287 +proof (cases "a = 0 \<and> b = 0")
   3.288 +  case True then show ?thesis by (cases "n > 0") (simp_all add: zero_power)
   3.289 +next
   3.290 +  case False
   3.291 +  then have "coprime (a div gcd a b) (b div gcd a b)"
   3.292 +    by (auto simp: div_gcd_coprime)
   3.293 +  then have "coprime ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
   3.294 +    by (simp add: coprime_exp2)
   3.295 +  then have "gcd ((a div gcd a b)^n * (gcd a b)^n)
   3.296        ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
   3.297      by (metis gcd_mult_distrib_nat mult.commute mult.right_neutral)
   3.298    also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
   3.299 @@ -1373,7 +1357,7 @@
   3.300      with dc have th0: "a' dvd b*c"
   3.301        using dvd_trans[of a' a "b*c"] by simp
   3.302      from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   3.303 -    hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc)
   3.304 +    hence "?g*a' dvd ?g * (b' * c)" by (simp add: ac_simps)
   3.305      with z have th_1: "a' dvd b' * c" by auto
   3.306      from coprime_dvd_mult_int[OF ab'(3)] th_1
   3.307      have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
   3.308 @@ -1471,10 +1455,10 @@
   3.309  qed
   3.310  
   3.311  lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
   3.312 -  by (simp add: gcd.commute)
   3.313 +  by (simp add: gcd.commute del: One_nat_def)
   3.314  
   3.315  lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
   3.316 -  using coprime_plus_one_nat by (simp add: One_nat_def)
   3.317 +  using coprime_plus_one_nat by simp
   3.318  
   3.319  lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
   3.320    by (simp add: gcd.commute)
   3.321 @@ -1850,7 +1834,7 @@
   3.322  
   3.323  interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
   3.324    + lcm_nat: semilattice_neutr "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat" 1
   3.325 -  by standard simp_all
   3.326 +  by standard (simp_all del: One_nat_def)
   3.327  
   3.328  interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int" ..
   3.329  
   3.330 @@ -1950,11 +1934,11 @@
   3.331  
   3.332  lemma Lcm_nat_empty:
   3.333    "Lcm {} = (1::nat)"
   3.334 -  by (simp add: Lcm_nat_def)
   3.335 +  by (simp add: Lcm_nat_def del: One_nat_def)
   3.336  
   3.337  lemma Lcm_nat_insert:
   3.338    "Lcm (insert n M) = lcm (n::nat) (Lcm M)"
   3.339 -  by (cases "finite M") (simp_all add: Lcm_nat_def Lcm_nat_infinite)
   3.340 +  by (cases "finite M") (simp_all add: Lcm_nat_def Lcm_nat_infinite del: One_nat_def)
   3.341  
   3.342  definition
   3.343    "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
   3.344 @@ -2107,7 +2091,7 @@
   3.345  lemma mult_inj_if_coprime_nat:
   3.346    "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
   3.347     \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
   3.348 -apply(auto simp add:inj_on_def)
   3.349 +apply (auto simp add: inj_on_def simp del: One_nat_def)
   3.350  apply (metis coprime_dvd_mult_iff_nat dvd.neq_le_trans dvd_triv_left)
   3.351  apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
   3.352               dvd.neq_le_trans dvd_triv_right mult.commute)
     4.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 08 14:01:41 2015 +0200
     4.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 08 20:19:12 2015 +0200
     4.3 @@ -794,15 +794,15 @@
     4.4  
     4.5  lemma dvd_lcm_D1:
     4.6    "lcm m n dvd k \<Longrightarrow> m dvd k"
     4.7 -  by (rule dvd_trans, rule lcm_dvd1, assumption)
     4.8 +  by (rule dvd_trans, rule dvd_lcm1, assumption)
     4.9  
    4.10  lemma dvd_lcm_D2:
    4.11    "lcm m n dvd k \<Longrightarrow> n dvd k"
    4.12 -  by (rule dvd_trans, rule lcm_dvd2, assumption)
    4.13 +  by (rule dvd_trans, rule dvd_lcm2, assumption)
    4.14  
    4.15  lemma gcd_dvd_lcm [simp]:
    4.16    "gcd a b dvd lcm a b"
    4.17 -  by (metis dvd_trans gcd_dvd2 lcm_dvd2)
    4.18 +  using gcd_dvd2 by (rule dvd_lcmI2)
    4.19  
    4.20  lemma lcm_1_iff:
    4.21    "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
    4.22 @@ -830,14 +830,6 @@
    4.23    (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
    4.24    by rule (auto intro: lcmI simp: lcm_least lcm_zero)
    4.25  
    4.26 -lemma dvd_lcm_I1 [simp]:
    4.27 -  "k dvd m \<Longrightarrow> k dvd lcm m n"
    4.28 -  by (metis lcm_dvd1 dvd_trans)
    4.29 -
    4.30 -lemma dvd_lcm_I2 [simp]:
    4.31 -  "k dvd n \<Longrightarrow> k dvd lcm m n"
    4.32 -  by (metis lcm_dvd2 dvd_trans)
    4.33 -
    4.34  lemma lcm_coprime:
    4.35    "gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)"
    4.36    by (subst lcm_gcd) simp
    4.37 @@ -874,8 +866,8 @@
    4.38    assumes "a \<noteq> 0" and "b \<noteq> 0"
    4.39    shows "euclidean_size a \<le> euclidean_size (lcm a b)"
    4.40  proof -
    4.41 -  have "a dvd lcm a b" by (rule lcm_dvd1)
    4.42 -  then obtain c where A: "lcm a b = a * c" unfolding dvd_def by blast
    4.43 +  have "a dvd lcm a b" by (rule dvd_lcm1)
    4.44 +  then obtain c where A: "lcm a b = a * c" ..
    4.45    with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "c \<noteq> 0" by (auto simp: lcm_zero)
    4.46    then show ?thesis by (subst A, intro size_mult_mono)
    4.47  qed
    4.48 @@ -905,12 +897,7 @@
    4.49  
    4.50  lemma lcm_mult_unit1:
    4.51    "is_unit a \<Longrightarrow> lcm (b * a) c = lcm b c"
    4.52 -  apply (rule lcmI)
    4.53 -  apply (rule dvd_trans[of _ "b * a"], simp, rule lcm_dvd1)
    4.54 -  apply (rule lcm_dvd2)
    4.55 -  apply (rule lcm_least, simp add: unit_simps, assumption)
    4.56 -  apply simp
    4.57 -  done
    4.58 +  by (rule associated_eqI) (simp_all add: mult_unit_dvd_iff dvd_lcmI1)
    4.59  
    4.60  lemma lcm_mult_unit2:
    4.61    "is_unit a \<Longrightarrow> lcm b (c * a) = lcm b c"
    4.62 @@ -944,22 +931,11 @@
    4.63  
    4.64  lemma lcm_left_idem:
    4.65    "lcm a (lcm a b) = lcm a b"
    4.66 -  apply (rule lcmI)
    4.67 -  apply simp
    4.68 -  apply (subst lcm.assoc [symmetric], rule lcm_dvd2)
    4.69 -  apply (rule lcm_least, assumption)
    4.70 -  apply (erule (1) lcm_least)
    4.71 -  apply (auto simp: lcm_zero)
    4.72 -  done
    4.73 +  by (rule associated_eqI) simp_all
    4.74  
    4.75  lemma lcm_right_idem:
    4.76    "lcm (lcm a b) b = lcm a b"
    4.77 -  apply (rule lcmI)
    4.78 -  apply (subst lcm.assoc, rule lcm_dvd1)
    4.79 -  apply (rule lcm_dvd2)
    4.80 -  apply (rule lcm_least, erule (1) lcm_least, assumption)
    4.81 -  apply (auto simp: lcm_zero)
    4.82 -  done
    4.83 +  by (rule associated_eqI) simp_all
    4.84  
    4.85  lemma comp_fun_idem_lcm: "comp_fun_idem lcm"
    4.86  proof
    4.87 @@ -1012,10 +988,10 @@
    4.88          also note \<open>euclidean_size l = n\<close>
    4.89          finally show "euclidean_size (gcd l l') \<le> n" .
    4.90        qed
    4.91 -      ultimately have "euclidean_size l = euclidean_size (gcd l l')" 
    4.92 +      ultimately have *: "euclidean_size l = euclidean_size (gcd l l')" 
    4.93          by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>)
    4.94 -      with \<open>l \<noteq> 0\<close> have "l dvd gcd l l'"
    4.95 -        using dvd_euclidean_size_eq_imp_dvd by auto
    4.96 +      from \<open>l \<noteq> 0\<close> have "l dvd gcd l l'"
    4.97 +        by (rule dvd_euclidean_size_eq_imp_dvd) (auto simp add: *)
    4.98        hence "l dvd l'" by (blast dest: dvd_gcd_D2)
    4.99      }
   4.100  
     5.1 --- a/src/HOL/Rings.thy	Wed Jul 08 14:01:41 2015 +0200
     5.2 +++ b/src/HOL/Rings.thy	Wed Jul 08 20:19:12 2015 +0200
     5.3 @@ -629,6 +629,44 @@
     5.4    then show ?thesis by simp
     5.5  qed 
     5.6  
     5.7 +lemma divide_1 [simp]:
     5.8 +  "a div 1 = a"
     5.9 +  using nonzero_mult_divide_cancel_left [of 1 a] by simp
    5.10 +
    5.11 +lemma dvd_times_left_cancel_iff [simp]:
    5.12 +  assumes "a \<noteq> 0"
    5.13 +  shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
    5.14 +proof
    5.15 +  assume ?P then obtain d where "a * c = a * b * d" ..
    5.16 +  with assms have "c = b * d" by (simp add: ac_simps)
    5.17 +  then show ?Q ..
    5.18 +next
    5.19 +  assume ?Q then obtain d where "c = b * d" .. 
    5.20 +  then have "a * c = a * b * d" by (simp add: ac_simps)
    5.21 +  then show ?P ..
    5.22 +qed
    5.23 +  
    5.24 +lemma dvd_times_right_cancel_iff [simp]:
    5.25 +  assumes "a \<noteq> 0"
    5.26 +  shows "b * a dvd c * a \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
    5.27 +using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps)
    5.28 +  
    5.29 +lemma div_dvd_iff_mult:
    5.30 +  assumes "b \<noteq> 0" and "b dvd a"
    5.31 +  shows "a div b dvd c \<longleftrightarrow> a dvd c * b"
    5.32 +proof -
    5.33 +  from \<open>b dvd a\<close> obtain d where "a = b * d" ..
    5.34 +  with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps)
    5.35 +qed
    5.36 +
    5.37 +lemma dvd_div_iff_mult:
    5.38 +  assumes "c \<noteq> 0" and "c dvd b"
    5.39 +  shows "a dvd b div c \<longleftrightarrow> a * c dvd b"
    5.40 +proof -
    5.41 +  from \<open>c dvd b\<close> obtain d where "b = c * d" ..
    5.42 +  with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
    5.43 +qed
    5.44 +
    5.45  end
    5.46  
    5.47  class idom_divide = idom + semidom_divide
     6.1 --- a/src/HOL/ex/Sqrt.thy	Wed Jul 08 14:01:41 2015 +0200
     6.2 +++ b/src/HOL/ex/Sqrt.thy	Wed Jul 08 20:19:12 2015 +0200
     6.3 @@ -18,7 +18,7 @@
     6.4    assume "sqrt p \<in> \<rat>"
     6.5    then obtain m n :: nat where
     6.6        n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
     6.7 -    and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
     6.8 +    and "coprime m n" by (rule Rats_abs_nat_div_natE)
     6.9    have eq: "m\<^sup>2 = p * n\<^sup>2"
    6.10    proof -
    6.11      from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp
    6.12 @@ -38,9 +38,8 @@
    6.13      then have "p dvd n\<^sup>2" ..
    6.14      with \<open>prime p\<close> show "p dvd n" by (rule prime_dvd_power_nat)
    6.15    qed
    6.16 -  then have "p dvd gcd m n" ..
    6.17 -  with gcd have "p dvd 1" by simp
    6.18 -  then have "p \<le> 1" by (simp add: dvd_imp_le)
    6.19 +  then have "p dvd gcd m n" by simp
    6.20 +  with \<open>coprime m n\<close> have "p = 1" by simp
    6.21    with p show False by simp
    6.22  qed
    6.23  
    6.24 @@ -64,7 +63,7 @@
    6.25    assume "sqrt p \<in> \<rat>"
    6.26    then obtain m n :: nat where
    6.27        n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
    6.28 -    and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
    6.29 +    and "coprime m n" by (rule Rats_abs_nat_div_natE)
    6.30    from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp
    6.31    then have "m\<^sup>2 = (sqrt p)\<^sup>2 * n\<^sup>2"
    6.32      by (auto simp add: power2_eq_square)
    6.33 @@ -79,8 +78,7 @@
    6.34    then have "p dvd n\<^sup>2" ..
    6.35    with \<open>prime p\<close> have "p dvd n" by (rule prime_dvd_power_nat)
    6.36    with dvd_m have "p dvd gcd m n" by (rule gcd_greatest_nat)
    6.37 -  with gcd have "p dvd 1" by simp
    6.38 -  then have "p \<le> 1" by (simp add: dvd_imp_le)
    6.39 +  with \<open>coprime m n\<close> have "p = 1" by simp
    6.40    with p show False by simp
    6.41  qed
    6.42