tuned lemmas and proofs
authorhaftmann
Fri Jun 12 08:53:23 2015 +0200 (2015-06-12)
changeset 60433720f210c5b1d
parent 60432 68d75cff8809
child 60434 b050b557dbbe
tuned lemmas and proofs
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     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.245    by (simp add: associated_def)
   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.397      by (simp add: normalisation_factor_mult)
   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)),