author haftmann Fri Jun 12 08:53:23 2015 +0200 (2015-06-12) changeset 60433 720f210c5b1d parent 60432 68d75cff8809 child 60434 b050b557dbbe
tuned lemmas and proofs
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 12 08:53:23 2015 +0200
1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 12 08:53:23 2015 +0200
1.3 @@ -9,61 +9,92 @@
1.4  context semiring_div
1.5  begin
1.6
1.7 +text \<open>Units: invertible elements in a ring\<close>
1.8 +
1.9  abbreviation is_unit :: "'a \<Rightarrow> bool"
1.10  where
1.11    "is_unit a \<equiv> a dvd 1"
1.12
1.13 -definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
1.14 -where
1.15 -  "associated a b \<longleftrightarrow> a dvd b \<and> b dvd a"
1.16 +lemma not_is_unit_0 [simp]:
1.17 +  "\<not> is_unit 0"
1.18 +  by simp
1.19 +
1.20 +lemma unit_imp_dvd [dest]:
1.21 +  "is_unit b \<Longrightarrow> b dvd a"
1.22 +  by (rule dvd_trans [of _ 1]) simp_all
1.23 +
1.24 +lemma unit_dvdE:
1.25 +  assumes "is_unit a"
1.26 +  obtains c where "a \<noteq> 0" and "b = a * c"
1.27 +proof -
1.28 +  from assms have "a dvd b" by auto
1.29 +  then obtain c where "b = a * c" ..
1.30 +  moreover from assms have "a \<noteq> 0" by auto
1.31 +  ultimately show thesis using that by blast
1.32 +qed
1.33 +
1.34 +lemma dvd_unit_imp_unit:
1.35 +  "a dvd b \<Longrightarrow> is_unit b \<Longrightarrow> is_unit a"
1.36 +  by (rule dvd_trans)
1.37 +
1.38 +lemma unit_div_1_unit [simp, intro]:
1.39 +  assumes "is_unit a"
1.40 +  shows "is_unit (1 div a)"
1.41 +proof -
1.42 +  from assms have "1 = 1 div a * a" by simp
1.43 +  then show "is_unit (1 div a)" by (rule dvdI)
1.44 +qed
1.45 +
1.46 +lemma is_unitE [elim?]:
1.47 +  assumes "is_unit a"
1.48 +  obtains b where "a \<noteq> 0" and "b \<noteq> 0"
1.49 +    and "is_unit b" and "1 div a = b" and "1 div b = a"
1.50 +    and "a * b = 1" and "c div a = c * b"
1.51 +proof (rule that)
1.52 +  def b \<equiv> "1 div a"
1.53 +  then show "1 div a = b" by simp
1.54 +  from b_def is_unit a show "is_unit b" by simp
1.55 +  from is_unit a and is_unit b show "a \<noteq> 0" and "b \<noteq> 0" by auto
1.56 +  from b_def is_unit a show "a * b = 1" by simp
1.57 +  then have "1 = a * b" ..
1.58 +  with b_def b \<noteq> 0 show "1 div b = a" by simp
1.59 +  from is_unit a have "a dvd c" ..
1.60 +  then obtain d where "c = a * d" ..
1.61 +  with a \<noteq> 0 a * b = 1 show "c div a = c * b"
1.62 +    by (simp add: mult.assoc mult.left_commute [of a])
1.63 +qed
1.64
1.65  lemma unit_prod [intro]:
1.66    "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
1.67 -  by (subst mult_1_left [of 1, symmetric], rule mult_dvd_mono)
1.68 -
1.69 -lemma unit_divide_1:
1.70 -  "is_unit b \<Longrightarrow> a div b = a * divide 1 b"
1.71 -  by (simp add: div_mult_swap)
1.72 -
1.73 -lemma unit_divide_1_divide_1 [simp]:
1.74 -  "is_unit a \<Longrightarrow> divide 1 (divide 1 a) = a"
1.75 -  by (metis div_mult_mult1_if div_mult_self1_is_id dvd_mult_div_cancel mult_1_right)
1.76 -
1.77 -lemma inv_imp_eq_divide_1:
1.78 -  "a * b = 1 \<Longrightarrow> divide 1 a = b"
1.79 -  by (metis dvd_mult_div_cancel dvd_mult_right mult_1_right mult.left_commute one_dvd)
1.80 -
1.81 -lemma unit_divide_1_unit [simp, intro]:
1.82 -  assumes "is_unit a"
1.83 -  shows "is_unit (divide 1 a)"
1.84 -proof -
1.85 -  from assms have "1 = divide 1 a * a" by simp
1.86 -  then show "is_unit (divide 1 a)" by (rule dvdI)
1.87 -qed
1.88 +  by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)
1.89 +
1.90 +lemma unit_div [intro]:
1.91 +  "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
1.92 +  by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)
1.93
1.94  lemma mult_unit_dvd_iff:
1.95 -  "is_unit b \<Longrightarrow> a * b dvd c \<longleftrightarrow> a dvd c"
1.96 +  assumes "is_unit b"
1.97 +  shows "a * b dvd c \<longleftrightarrow> a dvd c"
1.98  proof
1.99 -  assume "is_unit b" "a * b dvd c"
1.100 -  then show "a dvd c" by (simp add: dvd_mult_left)
1.101 +  assume "a * b dvd c"
1.102 +  with assms show "a dvd c"
1.103 +    by (simp add: dvd_mult_left)
1.104  next
1.105 -  assume "is_unit b" "a dvd c"
1.106 -  then obtain k where "c = a * k" unfolding dvd_def by blast
1.107 -  with is_unit b have "c = (a * b) * (divide 1 b * k)"
1.108 -      by (simp add: mult_ac)
1.109 +  assume "a dvd c"
1.110 +  then obtain k where "c = a * k" ..
1.111 +  with assms have "c = (a * b) * (1 div b * k)"
1.112 +    by (simp add: mult_ac)
1.113    then show "a * b dvd c" by (rule dvdI)
1.114  qed
1.115
1.116 -lemma div_unit_dvd_iff:
1.117 -  "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"
1.118 -  by (subst unit_divide_1) (assumption, simp add: mult_unit_dvd_iff)
1.119 -
1.120  lemma dvd_mult_unit_iff:
1.121 -  "is_unit b \<Longrightarrow> a dvd c * b \<longleftrightarrow> a dvd c"
1.122 +  assumes "is_unit b"
1.123 +  shows "a dvd c * b \<longleftrightarrow> a dvd c"
1.124  proof
1.125 -  assume "is_unit b" and "a dvd c * b"
1.126 -  have "c * b dvd c * (b * divide 1 b)" by (subst mult_assoc [symmetric]) simp
1.127 -  also from is_unit b have "b * divide 1 b = 1" by simp
1.128 +  assume "a dvd c * b"
1.129 +  with assms have "c * b dvd c * (b * (1 div b))"
1.130 +    by (subst mult_assoc [symmetric]) simp
1.131 +  also from is_unit b have "b * (1 div b) = 1" by (rule is_unitE) simp
1.132    finally have "c * b dvd c" by simp
1.133    with a dvd c * b show "a dvd c" by (rule dvd_trans)
1.134  next
1.135 @@ -71,95 +102,120 @@
1.136    then show "a dvd c * b" by simp
1.137  qed
1.138
1.139 +lemma div_unit_dvd_iff:
1.140 +  "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"
1.141 +  by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff)
1.142 +
1.143  lemma dvd_div_unit_iff:
1.144    "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c"
1.145 -  by (subst unit_divide_1) (assumption, simp add: dvd_mult_unit_iff)
1.146 +  by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff)
1.147
1.148 -lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff dvd_div_unit_iff
1.149 +lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff
1.150 +  dvd_mult_unit_iff dvd_div_unit_iff -- \<open>FIXME consider fact collection\<close>
1.151
1.152 -lemma unit_div [intro]:
1.153 -  "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
1.154 -  by (subst unit_divide_1) (assumption, rule unit_prod, simp_all)
1.155 +lemma unit_mult_div_div [simp]:
1.156 +  "is_unit a \<Longrightarrow> b * (1 div a) = b div a"
1.157 +  by (erule is_unitE [of _ b]) simp
1.158 +
1.159 +lemma unit_div_mult_self [simp]:
1.160 +  "is_unit a \<Longrightarrow> b div a * a = b"
1.161 +  by (rule dvd_div_mult_self) auto
1.162 +
1.163 +lemma unit_div_1_div_1 [simp]:
1.164 +  "is_unit a \<Longrightarrow> 1 div (1 div a) = a"
1.165 +  by (erule is_unitE) simp
1.166
1.167  lemma unit_div_mult_swap:
1.168 -  "is_unit c \<Longrightarrow> a * (b div c) = a * b div c"
1.169 -  by (simp only: unit_divide_1 [of _ b] unit_divide_1 [of _ "a*b"] ac_simps)
1.170 +  "is_unit c \<Longrightarrow> a * (b div c) = (a * b) div c"
1.171 +  by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c])
1.172
1.173  lemma unit_div_commute:
1.174 -  "is_unit b \<Longrightarrow> a div b * c = a * c div b"
1.175 -  by (simp only: unit_divide_1 [of _ a] unit_divide_1 [of _ "a*c"] ac_simps)
1.176 +  "is_unit b \<Longrightarrow> (a div b) * c = (a * c) div b"
1.177 +  using unit_div_mult_swap [of b c a] by (simp add: ac_simps)
1.178
1.179 -lemma unit_imp_dvd [dest]:
1.180 -  "is_unit b \<Longrightarrow> b dvd a"
1.181 -  by (rule dvd_trans [of _ 1]) simp_all
1.182 -
1.183 -lemma dvd_unit_imp_unit:
1.184 -  "is_unit b \<Longrightarrow> a dvd b \<Longrightarrow> is_unit a"
1.185 -  by (rule dvd_trans)
1.186 +lemma unit_eq_div1:
1.187 +  "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b"
1.188 +  by (auto elim: is_unitE)
1.189
1.190 -lemma unit_divide_1'1:
1.191 -  assumes "is_unit b"
1.192 -  shows "a div (b * c) = a * divide 1 b div c"
1.193 -proof -
1.194 -  from assms have "a div (b * c) = a * (divide 1 b * b) div (b * c)"
1.195 -    by simp
1.196 -  also have "... = b * (a * divide 1 b) div (b * c)"
1.197 -    by (simp only: mult_ac)
1.198 -  also have "... = a * divide 1 b div c"
1.199 -    by (cases "b = 0", simp, rule div_mult_mult1)
1.200 -  finally show ?thesis .
1.201 +lemma unit_eq_div2:
1.202 +  "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = c"
1.203 +  using unit_eq_div1 [of b c a] by auto
1.204 +
1.205 +lemma unit_mult_left_cancel:
1.206 +  assumes "is_unit a"
1.207 +  shows "a * b = a * c \<longleftrightarrow> b = c" (is "?P \<longleftrightarrow> ?Q")
1.208 +proof
1.209 +  assume ?Q then show ?P by simp
1.210 +next
1.211 +  assume ?P then have "a * b div a = a * c div a" by simp
1.212 +  moreover from assms have "a \<noteq> 0" by auto
1.213 +  ultimately show ?Q by simp
1.214  qed
1.215
1.216 -lemma associated_comm:
1.217 -  "associated a b \<Longrightarrow> associated b a"
1.218 +lemma unit_mult_right_cancel:
1.219 +  "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c"
1.220 +  using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps)
1.221 +
1.222 +lemma unit_div_cancel:
1.223 +  assumes "is_unit a"
1.224 +  shows "b div a = c div a \<longleftrightarrow> b = c"
1.225 +proof -
1.226 +  from assms have "is_unit (1 div a)" by simp
1.227 +  then have "b * (1 div a) = c * (1 div a) \<longleftrightarrow> b = c"
1.228 +    by (rule unit_mult_right_cancel)
1.229 +  with assms show ?thesis by simp
1.230 +qed
1.231 +
1.232 +
1.233 +text \<open>Associated elements in a ring – an equivalence relation induced by the quasi-order divisibility \<close>
1.234 +
1.235 +definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
1.236 +where
1.237 +  "associated a b \<longleftrightarrow> a dvd b \<and> b dvd a"
1.238 +
1.239 +lemma associatedI:
1.240 +  "a dvd b \<Longrightarrow> b dvd a \<Longrightarrow> associated a b"
1.241 +  by (simp add: associated_def)
1.242 +
1.243 +lemma associatedD1:
1.244 +  "associated a b \<Longrightarrow> a dvd b"
1.246
1.247 +lemma associatedD2:
1.248 +  "associated a b \<Longrightarrow> b dvd a"
1.249 +  by (simp add: associated_def)
1.250 +
1.251 +lemma associated_refl [simp]:
1.252 +  "associated a a"
1.253 +  by (auto intro: associatedI)
1.254 +
1.255 +lemma associated_sym:
1.256 +  "associated b a \<longleftrightarrow> associated a b"
1.257 +  by (auto intro: associatedI dest: associatedD1 associatedD2)
1.258 +
1.259 +lemma associated_trans:
1.260 +  "associated a b \<Longrightarrow> associated b c \<Longrightarrow> associated a c"
1.261 +  by (auto intro: associatedI dvd_trans dest: associatedD1 associatedD2)
1.262 +
1.263 +lemma equivp_associated:
1.264 +  "equivp associated"
1.265 +proof (rule equivpI)
1.266 +  show "reflp associated"
1.267 +    by (rule reflpI) simp
1.268 +  show "symp associated"
1.269 +    by (rule sympI) (simp add: associated_sym)
1.270 +  show "transp associated"
1.271 +    by (rule transpI) (fact associated_trans)
1.272 +qed
1.273 +
1.274  lemma associated_0 [simp]:
1.275    "associated 0 b \<longleftrightarrow> b = 0"
1.276    "associated a 0 \<longleftrightarrow> a = 0"
1.277 -  unfolding associated_def by simp_all
1.278 +  by (auto dest: associatedD1 associatedD2)
1.279
1.280  lemma associated_unit:
1.281 -  "is_unit a \<Longrightarrow> associated a b \<Longrightarrow> is_unit b"
1.282 -  unfolding associated_def using dvd_unit_imp_unit by auto
1.283 -
1.284 -lemma is_unit_1 [simp]:
1.285 -  "is_unit 1"
1.286 -  by simp
1.287 -
1.288 -lemma not_is_unit_0 [simp]:
1.289 -  "\<not> is_unit 0"
1.290 -  by auto
1.291 -
1.292 -lemma unit_mult_left_cancel:
1.293 -  assumes "is_unit a"
1.294 -  shows "(a * b) = (a * c) \<longleftrightarrow> b = c"
1.295 -proof -
1.296 -  from assms have "a \<noteq> 0" by auto
1.297 -  then show ?thesis by (metis div_mult_self1_is_id)
1.298 -qed
1.299 -
1.300 -lemma unit_mult_right_cancel:
1.301 -  "is_unit a \<Longrightarrow> (b * a) = (c * a) \<longleftrightarrow> b = c"
1.302 -  by (simp add: ac_simps unit_mult_left_cancel)
1.303 -
1.304 -lemma unit_div_cancel:
1.305 -  "is_unit a \<Longrightarrow> (b div a) = (c div a) \<longleftrightarrow> b = c"
1.306 -  apply (subst unit_divide_1[of _ b], assumption)
1.307 -  apply (subst unit_divide_1[of _ c], assumption)
1.308 -  apply (rule unit_mult_right_cancel, erule unit_divide_1_unit)
1.309 -  done
1.310 -
1.311 -lemma unit_eq_div1:
1.312 -  "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b"
1.313 -  apply (subst unit_divide_1, assumption)
1.314 -  apply (subst unit_mult_right_cancel[symmetric], assumption)
1.315 -  apply (subst mult_assoc, subst dvd_div_mult_self, assumption, simp)
1.316 -  done
1.317 -
1.318 -lemma unit_eq_div2:
1.319 -  "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = c"
1.320 -  by (subst (1 2) eq_commute, simp add: unit_eq_div1, subst eq_commute, rule refl)
1.321 +  "associated a b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
1.322 +  using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
1.323
1.324  lemma associated_iff_div_unit:
1.325    "associated a b \<longleftrightarrow> (\<exists>c. is_unit c \<and> a = c * b)"
1.326 @@ -183,7 +239,7 @@
1.327  next
1.328    assume "\<exists>c. is_unit c \<and> a = c * b"
1.329    then obtain c where "is_unit c" and "a = c * b" by blast
1.330 -  hence "b = a * divide 1 c" by (simp add: algebra_simps)
1.331 +  hence "b = a * (1 div c)" by (simp add: algebra_simps)
1.332    hence "a dvd b" by simp
1.333    moreover from a = c * b have "b dvd a" by simp
1.334    ultimately show "associated a b" unfolding associated_def by simp
1.335 @@ -196,27 +252,11 @@
1.336
1.337  end
1.338
1.339 -context ring_div
1.340 -begin
1.341 -
1.342 -lemma is_unit_neg [simp]:
1.343 -  "is_unit (- a) \<Longrightarrow> is_unit a"
1.344 -  by simp
1.345 -
1.346 -lemma is_unit_neg_1 [simp]:
1.347 -  "is_unit (-1)"
1.348 -  by simp
1.349 -
1.350 -end
1.351 -
1.352 -lemma is_unit_nat [simp]:
1.353 -  "is_unit (a::nat) \<longleftrightarrow> a = 1"
1.354 -  by simp
1.355 -
1.356  lemma is_unit_int:
1.357 -  "is_unit (a::int) \<longleftrightarrow> a = 1 \<or> a = -1"
1.358 +  "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
1.359    by auto
1.360
1.361 +
1.362  text {*
1.363    A Euclidean semiring is a semiring upon which the Euclidean algorithm can be
1.364    implemented. It must provide:
1.365 @@ -225,7 +265,7 @@
1.366    \item a size function such that @{term "size (a mod b) < size b"}
1.367          for any @{term "b \<noteq> 0"}
1.368    \item a normalisation factor such that two associated numbers are equal iff
1.369 -        they are the same when divided by their normalisation factors.
1.370 +        they are the same when divd by their normalisation factors.
1.371    \end{itemize}
1.372    The existence of these functions makes it possible to derive gcd and lcm functions
1.373    for any Euclidean semiring.
1.374 @@ -258,12 +298,9 @@
1.375  proof
1.376    assume "normalisation_factor a = 0"
1.377    hence "\<not> is_unit (normalisation_factor a)"
1.378 -    by (metis not_is_unit_0)
1.379 -  then show "a = 0" by force
1.380 -next
1.381 -  assume "a = 0"
1.382 -  then show "normalisation_factor a = 0" by simp
1.383 -qed
1.384 +    by simp
1.385 +  then show "a = 0" by auto
1.386 +qed simp
1.387
1.388  lemma normalisation_factor_pow:
1.389    "normalisation_factor (a ^ n) = normalisation_factor a ^ n"
1.390 @@ -275,21 +312,26 @@
1.391    assume "a \<noteq> 0"
1.392    let ?nf = "normalisation_factor"
1.393    from normalisation_factor_is_unit[OF a \<noteq> 0] have "?nf a \<noteq> 0"
1.394 -    by (metis not_is_unit_0)
1.395 +    by auto
1.396    have "?nf (a div ?nf a) * ?nf (?nf a) = ?nf (a div ?nf a * ?nf a)"
1.398    also have "a div ?nf a * ?nf a = a" using a \<noteq> 0
1.399      by simp
1.400    also have "?nf (?nf a) = ?nf a" using a \<noteq> 0
1.401      normalisation_factor_is_unit normalisation_factor_unit by simp
1.402 -  finally show ?thesis using a \<noteq> 0 and ?nf a \<noteq> 0
1.403 -    by (metis div_mult_self2_is_id div_self)
1.404 +  finally have "normalisation_factor (a div normalisation_factor a) = 1"
1.405 +    using ?nf a \<noteq> 0 by (metis div_mult_self2_is_id div_self)
1.406 +  with a \<noteq> 0 show ?thesis by simp
1.407  qed
1.408
1.409  lemma normalisation_0_iff [simp]:
1.410    "a div normalisation_factor a = 0 \<longleftrightarrow> a = 0"
1.411    by (cases "a = 0", simp, subst unit_eq_div1, blast, simp)
1.412
1.413 +lemma mult_div_normalisation [simp]:
1.414 +  "b * (1 div normalisation_factor a) = b div normalisation_factor a"
1.415 +  by (cases "a = 0") simp_all
1.416 +
1.417  lemma associated_iff_normed_eq:
1.418    "associated a b \<longleftrightarrow> a div normalisation_factor a = b div normalisation_factor b"
1.419  proof (cases "b = 0", simp, cases "a = 0", metis associated_0(1) normalisation_0_iff, rule iffI)
1.420 @@ -613,10 +655,10 @@
1.421    by (subst gcd.commute, subst gcd_mult_unit1, assumption, rule gcd.commute)
1.422
1.423  lemma gcd_div_unit1: "is_unit a \<Longrightarrow> gcd (b div a) c = gcd b c"
1.424 -  by (subst unit_divide_1) (simp_all add: gcd_mult_unit1)
1.425 +  by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1)
1.426
1.427  lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c"
1.428 -  by (subst unit_divide_1) (simp_all add: gcd_mult_unit2)
1.429 +  by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2)
1.430
1.431  lemma gcd_idem: "gcd a a = a div normalisation_factor a"
1.432    by (cases "a = 0") (simp add: gcd_0_left, rule sym, rule gcdI, simp_all)
1.433 @@ -870,7 +912,7 @@
1.434    then show ?thesis by blast
1.435  qed
1.436
1.437 -lemma pow_divides_pow:
1.438 +lemma pow_divs_pow:
1.439    assumes ab: "a ^ n dvd b ^ n" and n: "n \<noteq> 0"
1.440    shows "a dvd b"
1.441  proof (cases "gcd a b = 0")
1.442 @@ -897,11 +939,11 @@
1.443    with ab'(1,2) show ?thesis by simp
1.444  qed
1.445
1.446 -lemma pow_divides_eq [simp]:
1.447 +lemma pow_divs_eq [simp]:
1.448    "n \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
1.449 -  by (auto intro: pow_divides_pow dvd_power_same)
1.450 +  by (auto intro: pow_divs_pow dvd_power_same)
1.451
1.452 -lemma divides_mult:
1.453 +lemma divs_mult:
1.454    assumes mr: "m dvd r" and nr: "n dvd r" and mn: "gcd m n = 1"
1.455    shows "m * n dvd r"
1.456  proof -
1.457 @@ -973,8 +1015,8 @@
1.458  proof (cases "a*b = 0")
1.459    assume "a * b \<noteq> 0"
1.460    hence "gcd a b \<noteq> 0" by simp
1.461 -  let ?c = "divide 1 (normalisation_factor (a*b))"
1.462 -  from a * b \<noteq> 0 have [simp]: "is_unit (normalisation_factor (a*b))" by simp
1.463 +  let ?c = "1 div normalisation_factor (a * b)"
1.464 +  from a * b \<noteq> 0 have [simp]: "is_unit (normalisation_factor (a * b))" by simp
1.465    from lcm_gcd_prod[of a b] have "lcm a b * gcd a b = a * ?c * b"
1.466      by (simp add: div_mult_swap unit_div_commute)
1.467    hence "lcm a b * gcd a b div gcd a b = a * ?c * b div gcd a b" by simp
1.468 @@ -1050,14 +1092,14 @@
1.469    shows "gcd a b = a * b div (lcm a b * normalisation_factor (a * b))"
1.470  proof-
1.471    from assms have "gcd a b \<noteq> 0" by (simp add: lcm_zero)
1.472 -  let ?c = "normalisation_factor (a*b)"
1.473 +  let ?c = "normalisation_factor (a * b)"
1.474    from lcm a b \<noteq> 0 have "?c \<noteq> 0" by (intro notI, simp add: lcm_zero no_zero_divisors)
1.475    hence "is_unit ?c" by simp
1.476    from lcm_gcd_prod [of a b] have "gcd a b = a * b div ?c div lcm a b"
1.477      by (subst (2) div_mult_self2_is_id[OF lcm a b \<noteq> 0, symmetric], simp add: mult_ac)
1.478 -  also from is_unit ?c have "... = a * b div (?c * lcm a b)"
1.479 -    by (metis local.unit_divide_1 local.unit_divide_1'1)
1.480 -  finally show ?thesis by (simp only: ac_simps)
1.481 +  also from is_unit ?c have "... = a * b div (lcm a b * ?c)"
1.482 +    by (metis ?c \<noteq> 0 div_mult_mult1 dvd_mult_div_cancel mult_commute normalisation_factor_dvd')
1.483 +  finally show ?thesis .
1.484  qed
1.485
1.486  lemma normalisation_factor_lcm [simp]:
1.487 @@ -1249,11 +1291,11 @@
1.488
1.489  lemma lcm_div_unit1:
1.490    "is_unit a \<Longrightarrow> lcm (b div a) c = lcm b c"
1.491 -  by (metis lcm_mult_unit1 local.unit_divide_1 local.unit_divide_1_unit)
1.492 +  by (erule is_unitE [of _ b]) (simp add: lcm_mult_unit1)
1.493
1.494  lemma lcm_div_unit2:
1.495    "is_unit a \<Longrightarrow> lcm b (c div a) = lcm b c"
1.496 -  by (metis lcm_mult_unit2 local.unit_divide_1 local.unit_divide_1_unit)
1.497 +  by (erule is_unitE [of _ c]) (simp add: lcm_mult_unit2)
1.498
1.499  lemma lcm_left_idem:
1.500    "lcm a (lcm a b) = lcm a b"
1.501 @@ -1623,7 +1665,7 @@
1.502  function euclid_ext :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a \<times> 'a" where
1.503    "euclid_ext a b =
1.504       (if b = 0 then
1.505 -        let c = divide 1 (normalisation_factor a) in (c, 0, a * c)
1.506 +        let c = 1 div normalisation_factor a in (c, 0, a * c)
1.507        else
1.508          case euclid_ext b (a mod b) of
1.509              (s,t,c) \<Rightarrow> (t, s - t * (a div b), c))"
1.510 @@ -1633,13 +1675,13 @@
1.511  declare euclid_ext.simps [simp del]
1.512
1.513  lemma euclid_ext_0:
1.514 -  "euclid_ext a 0 = (divide 1 (normalisation_factor a), 0, a * divide 1 (normalisation_factor a))"
1.515 -  by (subst euclid_ext.simps, simp add: Let_def)
1.516 +  "euclid_ext a 0 = (1 div normalisation_factor a, 0, a div normalisation_factor a)"
1.517 +  by (subst euclid_ext.simps) (simp add: Let_def)
1.518
1.519  lemma euclid_ext_non_0:
1.520    "b \<noteq> 0 \<Longrightarrow> euclid_ext a b = (case euclid_ext b (a mod b) of
1.521      (s,t,c) \<Rightarrow> (t, s - t * (a div b), c))"
1.522 -  by (subst euclid_ext.simps, simp)
1.523 +  by (subst euclid_ext.simps) simp
1.524
1.525  definition euclid_ext' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a"
1.526  where
1.527 @@ -1652,8 +1694,8 @@
1.528    then show ?case
1.529    proof (cases "b = 0")
1.530      case True
1.531 -      then show ?thesis by (cases "a = 0")
1.532 -        (simp_all add: euclid_ext_0 unit_div mult_ac unit_simps gcd_0)
1.533 +      then show ?thesis by
1.534 +        (simp add: euclid_ext_0 unit_div mult_ac unit_simps gcd_0)
1.535      next
1.536      case False with 1 show ?thesis
1.537        by (simp add: euclid_ext_non_0 ac_simps split: prod.split prod.split_asm)
1.538 @@ -1697,7 +1739,7 @@
1.539  lemma bezout: "\<exists>s t. s * a + t * b = gcd a b"
1.540    using euclid_ext'_correct by blast
1.541
1.542 -lemma euclid_ext'_0 [simp]: "euclid_ext' a 0 = (divide 1 (normalisation_factor a), 0)"
1.543 +lemma euclid_ext'_0 [simp]: "euclid_ext' a 0 = (1 div normalisation_factor a, 0)"
1.544    by (simp add: bezw_def euclid_ext'_def euclid_ext_0)
1.545
1.546  lemma euclid_ext'_non_0: "b \<noteq> 0 \<Longrightarrow> euclid_ext' a b = (snd (euclid_ext' b (a mod b)),