# HG changeset patch
# User haftmann
# Date 1434092003 -7200
# Node ID 720f210c5b1ddad77bf9d4f2a2118d3feffd5075
# Parent  68d75cff880905735e9b3db53194b3ddb3db7650
tuned lemmas and proofs

diff -r 68d75cff8809 -r 720f210c5b1d src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 12 08:53:23 2015 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -9,61 +9,92 @@
 context semiring_div
 begin 
 
+text \<open>Units: invertible elements in a ring\<close>
+
 abbreviation is_unit :: "'a \<Rightarrow> bool"
 where
   "is_unit a \<equiv> a dvd 1"
 
-definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
-where
-  "associated a b \<longleftrightarrow> a dvd b \<and> b dvd a"
+lemma not_is_unit_0 [simp]:
+  "\<not> is_unit 0"
+  by simp
+
+lemma unit_imp_dvd [dest]: 
+  "is_unit b \<Longrightarrow> b dvd a"
+  by (rule dvd_trans [of _ 1]) simp_all
+
+lemma unit_dvdE:
+  assumes "is_unit a"
+  obtains c where "a \<noteq> 0" and "b = a * c"
+proof -
+  from assms have "a dvd b" by auto
+  then obtain c where "b = a * c" ..
+  moreover from assms have "a \<noteq> 0" by auto
+  ultimately show thesis using that by blast
+qed
+
+lemma dvd_unit_imp_unit:
+  "a dvd b \<Longrightarrow> is_unit b \<Longrightarrow> is_unit a"
+  by (rule dvd_trans)
+
+lemma unit_div_1_unit [simp, intro]:
+  assumes "is_unit a"
+  shows "is_unit (1 div a)"
+proof -
+  from assms have "1 = 1 div a * a" by simp
+  then show "is_unit (1 div a)" by (rule dvdI)
+qed
+
+lemma is_unitE [elim?]:
+  assumes "is_unit a"
+  obtains b where "a \<noteq> 0" and "b \<noteq> 0"
+    and "is_unit b" and "1 div a = b" and "1 div b = a"
+    and "a * b = 1" and "c div a = c * b"
+proof (rule that)
+  def b \<equiv> "1 div a"
+  then show "1 div a = b" by simp
+  from b_def `is_unit a` show "is_unit b" by simp
+  from `is_unit a` and `is_unit b` show "a \<noteq> 0" and "b \<noteq> 0" by auto
+  from b_def `is_unit a` show "a * b = 1" by simp
+  then have "1 = a * b" ..
+  with b_def `b \<noteq> 0` show "1 div b = a" by simp
+  from `is_unit a` have "a dvd c" ..
+  then obtain d where "c = a * d" ..
+  with `a \<noteq> 0` `a * b = 1` show "c div a = c * b"
+    by (simp add: mult.assoc mult.left_commute [of a])
+qed
 
 lemma unit_prod [intro]:
   "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
-  by (subst mult_1_left [of 1, symmetric], rule mult_dvd_mono) 
-
-lemma unit_divide_1:
-  "is_unit b \<Longrightarrow> a div b = a * divide 1 b"
-  by (simp add: div_mult_swap)
-
-lemma unit_divide_1_divide_1 [simp]:
-  "is_unit a \<Longrightarrow> divide 1 (divide 1 a) = a"
-  by (metis div_mult_mult1_if div_mult_self1_is_id dvd_mult_div_cancel mult_1_right)
-
-lemma inv_imp_eq_divide_1:
-  "a * b = 1 \<Longrightarrow> divide 1 a = b"
-  by (metis dvd_mult_div_cancel dvd_mult_right mult_1_right mult.left_commute one_dvd)
-
-lemma unit_divide_1_unit [simp, intro]:
-  assumes "is_unit a"
-  shows "is_unit (divide 1 a)"
-proof -
-  from assms have "1 = divide 1 a * a" by simp
-  then show "is_unit (divide 1 a)" by (rule dvdI)
-qed
+  by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono) 
+  
+lemma unit_div [intro]:
+  "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
+  by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)
 
 lemma mult_unit_dvd_iff:
-  "is_unit b \<Longrightarrow> a * b dvd c \<longleftrightarrow> a dvd c"
+  assumes "is_unit b"
+  shows "a * b dvd c \<longleftrightarrow> a dvd c"
 proof
-  assume "is_unit b" "a * b dvd c"
-  then show "a dvd c" by (simp add: dvd_mult_left)
+  assume "a * b dvd c"
+  with assms show "a dvd c"
+    by (simp add: dvd_mult_left)
 next
-  assume "is_unit b" "a dvd c"
-  then obtain k where "c = a * k" unfolding dvd_def by blast
-  with `is_unit b` have "c = (a * b) * (divide 1 b * k)" 
-      by (simp add: mult_ac)
+  assume "a dvd c"
+  then obtain k where "c = a * k" ..
+  with assms have "c = (a * b) * (1 div b * k)"
+    by (simp add: mult_ac)
   then show "a * b dvd c" by (rule dvdI)
 qed
 
-lemma div_unit_dvd_iff:
-  "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"
-  by (subst unit_divide_1) (assumption, simp add: mult_unit_dvd_iff)
-
 lemma dvd_mult_unit_iff:
-  "is_unit b \<Longrightarrow> a dvd c * b \<longleftrightarrow> a dvd c"
+  assumes "is_unit b"
+  shows "a dvd c * b \<longleftrightarrow> a dvd c"
 proof
-  assume "is_unit b" and "a dvd c * b"
-  have "c * b dvd c * (b * divide 1 b)" by (subst mult_assoc [symmetric]) simp
-  also from `is_unit b` have "b * divide 1 b = 1" by simp
+  assume "a dvd c * b"
+  with assms have "c * b dvd c * (b * (1 div b))"
+    by (subst mult_assoc [symmetric]) simp
+  also from `is_unit b` have "b * (1 div b) = 1" by (rule is_unitE) simp
   finally have "c * b dvd c" by simp
   with `a dvd c * b` show "a dvd c" by (rule dvd_trans)
 next
@@ -71,95 +102,120 @@
   then show "a dvd c * b" by simp
 qed
 
+lemma div_unit_dvd_iff:
+  "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"
+  by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff)
+
 lemma dvd_div_unit_iff:
   "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c"
-  by (subst unit_divide_1) (assumption, simp add: dvd_mult_unit_iff)
+  by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff)
 
-lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff dvd_div_unit_iff
+lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff
+  dvd_mult_unit_iff dvd_div_unit_iff -- \<open>FIXME consider fact collection\<close>
 
-lemma unit_div [intro]:
-  "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
-  by (subst unit_divide_1) (assumption, rule unit_prod, simp_all)
+lemma unit_mult_div_div [simp]:
+  "is_unit a \<Longrightarrow> b * (1 div a) = b div a"
+  by (erule is_unitE [of _ b]) simp
+
+lemma unit_div_mult_self [simp]:
+  "is_unit a \<Longrightarrow> b div a * a = b"
+  by (rule dvd_div_mult_self) auto
+
+lemma unit_div_1_div_1 [simp]:
+  "is_unit a \<Longrightarrow> 1 div (1 div a) = a"
+  by (erule is_unitE) simp
 
 lemma unit_div_mult_swap:
-  "is_unit c \<Longrightarrow> a * (b div c) = a * b div c"
-  by (simp only: unit_divide_1 [of _ b] unit_divide_1 [of _ "a*b"] ac_simps)
+  "is_unit c \<Longrightarrow> a * (b div c) = (a * b) div c"
+  by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c])
 
 lemma unit_div_commute:
-  "is_unit b \<Longrightarrow> a div b * c = a * c div b"
-  by (simp only: unit_divide_1 [of _ a] unit_divide_1 [of _ "a*c"] ac_simps)
+  "is_unit b \<Longrightarrow> (a div b) * c = (a * c) div b"
+  using unit_div_mult_swap [of b c a] by (simp add: ac_simps)
 
-lemma unit_imp_dvd [dest]:
-  "is_unit b \<Longrightarrow> b dvd a"
-  by (rule dvd_trans [of _ 1]) simp_all
-
-lemma dvd_unit_imp_unit:
-  "is_unit b \<Longrightarrow> a dvd b \<Longrightarrow> is_unit a"
-  by (rule dvd_trans)
+lemma unit_eq_div1:
+  "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b"
+  by (auto elim: is_unitE)
 
-lemma unit_divide_1'1:
-  assumes "is_unit b"
-  shows "a div (b * c) = a * divide 1 b div c" 
-proof -
-  from assms have "a div (b * c) = a * (divide 1 b * b) div (b * c)"
-    by simp
-  also have "... = b * (a * divide 1 b) div (b * c)"
-    by (simp only: mult_ac)
-  also have "... = a * divide 1 b div c"
-    by (cases "b = 0", simp, rule div_mult_mult1)
-  finally show ?thesis .
+lemma unit_eq_div2:
+  "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = c"
+  using unit_eq_div1 [of b c a] by auto
+
+lemma unit_mult_left_cancel:
+  assumes "is_unit a"
+  shows "a * b = a * c \<longleftrightarrow> b = c" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?Q then show ?P by simp
+next
+  assume ?P then have "a * b div a = a * c div a" by simp
+  moreover from assms have "a \<noteq> 0" by auto
+  ultimately show ?Q by simp
 qed
 
-lemma associated_comm:
-  "associated a b \<Longrightarrow> associated b a"
+lemma unit_mult_right_cancel:
+  "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c"
+  using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps)
+
+lemma unit_div_cancel:
+  assumes "is_unit a"
+  shows "b div a = c div a \<longleftrightarrow> b = c"
+proof -
+  from assms have "is_unit (1 div a)" by simp
+  then have "b * (1 div a) = c * (1 div a) \<longleftrightarrow> b = c"
+    by (rule unit_mult_right_cancel)
+  with assms show ?thesis by simp
+qed
+  
+
+text \<open>Associated elements in a ring – an equivalence relation induced by the quasi-order divisibility \<close>
+
+definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
+where
+  "associated a b \<longleftrightarrow> a dvd b \<and> b dvd a"
+
+lemma associatedI:
+  "a dvd b \<Longrightarrow> b dvd a \<Longrightarrow> associated a b"
+  by (simp add: associated_def)
+
+lemma associatedD1:
+  "associated a b \<Longrightarrow> a dvd b"
   by (simp add: associated_def)
 
+lemma associatedD2:
+  "associated a b \<Longrightarrow> b dvd a"
+  by (simp add: associated_def)
+
+lemma associated_refl [simp]:
+  "associated a a"
+  by (auto intro: associatedI)
+
+lemma associated_sym:
+  "associated b a \<longleftrightarrow> associated a b"
+  by (auto intro: associatedI dest: associatedD1 associatedD2)
+
+lemma associated_trans:
+  "associated a b \<Longrightarrow> associated b c \<Longrightarrow> associated a c"
+  by (auto intro: associatedI dvd_trans dest: associatedD1 associatedD2)
+
+lemma equivp_associated:
+  "equivp associated"
+proof (rule equivpI)
+  show "reflp associated"
+    by (rule reflpI) simp
+  show "symp associated"
+    by (rule sympI) (simp add: associated_sym)
+  show "transp associated"
+    by (rule transpI) (fact associated_trans)
+qed
+
 lemma associated_0 [simp]:
   "associated 0 b \<longleftrightarrow> b = 0"
   "associated a 0 \<longleftrightarrow> a = 0"
-  unfolding associated_def by simp_all
+  by (auto dest: associatedD1 associatedD2)
 
 lemma associated_unit:
-  "is_unit a \<Longrightarrow> associated a b \<Longrightarrow> is_unit b"
-  unfolding associated_def using dvd_unit_imp_unit by auto
-
-lemma is_unit_1 [simp]:
-  "is_unit 1"
-  by simp
-
-lemma not_is_unit_0 [simp]:
-  "\<not> is_unit 0"
-  by auto
-
-lemma unit_mult_left_cancel:
-  assumes "is_unit a"
-  shows "(a * b) = (a * c) \<longleftrightarrow> b = c"
-proof -
-  from assms have "a \<noteq> 0" by auto
-  then show ?thesis by (metis div_mult_self1_is_id)
-qed
-
-lemma unit_mult_right_cancel:
-  "is_unit a \<Longrightarrow> (b * a) = (c * a) \<longleftrightarrow> b = c"
-  by (simp add: ac_simps unit_mult_left_cancel)
-
-lemma unit_div_cancel:
-  "is_unit a \<Longrightarrow> (b div a) = (c div a) \<longleftrightarrow> b = c"
-  apply (subst unit_divide_1[of _ b], assumption)
-  apply (subst unit_divide_1[of _ c], assumption)
-  apply (rule unit_mult_right_cancel, erule unit_divide_1_unit)
-  done
-
-lemma unit_eq_div1:
-  "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b"
-  apply (subst unit_divide_1, assumption)
-  apply (subst unit_mult_right_cancel[symmetric], assumption)
-  apply (subst mult_assoc, subst dvd_div_mult_self, assumption, simp)
-  done
-
-lemma unit_eq_div2:
-  "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = c"
-  by (subst (1 2) eq_commute, simp add: unit_eq_div1, subst eq_commute, rule refl)
+  "associated a b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
+  using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
 
 lemma associated_iff_div_unit:
   "associated a b \<longleftrightarrow> (\<exists>c. is_unit c \<and> a = c * b)"
@@ -183,7 +239,7 @@
 next
   assume "\<exists>c. is_unit c \<and> a = c * b"
   then obtain c where "is_unit c" and "a = c * b" by blast
-  hence "b = a * divide 1 c" by (simp add: algebra_simps)
+  hence "b = a * (1 div c)" by (simp add: algebra_simps)
   hence "a dvd b" by simp
   moreover from `a = c * b` have "b dvd a" by simp
   ultimately show "associated a b" unfolding associated_def by simp
@@ -196,27 +252,11 @@
 
 end
 
-context ring_div
-begin
-
-lemma is_unit_neg [simp]:
-  "is_unit (- a) \<Longrightarrow> is_unit a"
-  by simp
-
-lemma is_unit_neg_1 [simp]:
-  "is_unit (-1)"
-  by simp
-
-end
-
-lemma is_unit_nat [simp]:
-  "is_unit (a::nat) \<longleftrightarrow> a = 1"
-  by simp
-
 lemma is_unit_int:
-  "is_unit (a::int) \<longleftrightarrow> a = 1 \<or> a = -1"
+  "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
   by auto
 
+  
 text {*
   A Euclidean semiring is a semiring upon which the Euclidean algorithm can be
   implemented. It must provide:
@@ -225,7 +265,7 @@
   \item a size function such that @{term "size (a mod b) < size b"} 
         for any @{term "b \<noteq> 0"}
   \item a normalisation factor such that two associated numbers are equal iff 
-        they are the same when divided by their normalisation factors.
+        they are the same when divd by their normalisation factors.
   \end{itemize}
   The existence of these functions makes it possible to derive gcd and lcm functions 
   for any Euclidean semiring.
@@ -258,12 +298,9 @@
 proof
   assume "normalisation_factor a = 0"
   hence "\<not> is_unit (normalisation_factor a)"
-    by (metis not_is_unit_0)
-  then show "a = 0" by force
-next
-  assume "a = 0"
-  then show "normalisation_factor a = 0" by simp
-qed
+    by simp
+  then show "a = 0" by auto
+qed simp
 
 lemma normalisation_factor_pow:
   "normalisation_factor (a ^ n) = normalisation_factor a ^ n"
@@ -275,21 +312,26 @@
   assume "a \<noteq> 0"
   let ?nf = "normalisation_factor"
   from normalisation_factor_is_unit[OF `a \<noteq> 0`] have "?nf a \<noteq> 0"
-    by (metis not_is_unit_0) 
+    by auto
   have "?nf (a div ?nf a) * ?nf (?nf a) = ?nf (a div ?nf a * ?nf a)" 
     by (simp add: normalisation_factor_mult)
   also have "a div ?nf a * ?nf a = a" using `a \<noteq> 0`
     by simp
   also have "?nf (?nf a) = ?nf a" using `a \<noteq> 0` 
     normalisation_factor_is_unit normalisation_factor_unit by simp
-  finally show ?thesis using `a \<noteq> 0` and `?nf a \<noteq> 0` 
-    by (metis div_mult_self2_is_id div_self)
+  finally have "normalisation_factor (a div normalisation_factor a) = 1"  
+    using `?nf a \<noteq> 0` by (metis div_mult_self2_is_id div_self)
+  with `a \<noteq> 0` show ?thesis by simp
 qed
 
 lemma normalisation_0_iff [simp]:
   "a div normalisation_factor a = 0 \<longleftrightarrow> a = 0"
   by (cases "a = 0", simp, subst unit_eq_div1, blast, simp)
 
+lemma mult_div_normalisation [simp]:
+  "b * (1 div normalisation_factor a) = b div normalisation_factor a"
+  by (cases "a = 0") simp_all
+
 lemma associated_iff_normed_eq:
   "associated a b \<longleftrightarrow> a div normalisation_factor a = b div normalisation_factor b"
 proof (cases "b = 0", simp, cases "a = 0", metis associated_0(1) normalisation_0_iff, rule iffI)
@@ -613,10 +655,10 @@
   by (subst gcd.commute, subst gcd_mult_unit1, assumption, rule gcd.commute)
 
 lemma gcd_div_unit1: "is_unit a \<Longrightarrow> gcd (b div a) c = gcd b c"
-  by (subst unit_divide_1) (simp_all add: gcd_mult_unit1)
+  by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1)
 
 lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c"
-  by (subst unit_divide_1) (simp_all add: gcd_mult_unit2)
+  by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2)
 
 lemma gcd_idem: "gcd a a = a div normalisation_factor a"
   by (cases "a = 0") (simp add: gcd_0_left, rule sym, rule gcdI, simp_all)
@@ -870,7 +912,7 @@
   then show ?thesis by blast
 qed
 
-lemma pow_divides_pow:
+lemma pow_divs_pow:
   assumes ab: "a ^ n dvd b ^ n" and n: "n \<noteq> 0"
   shows "a dvd b"
 proof (cases "gcd a b = 0")
@@ -897,11 +939,11 @@
   with ab'(1,2) show ?thesis by simp
 qed
 
-lemma pow_divides_eq [simp]:
+lemma pow_divs_eq [simp]:
   "n \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
-  by (auto intro: pow_divides_pow dvd_power_same)
+  by (auto intro: pow_divs_pow dvd_power_same)
 
-lemma divides_mult:
+lemma divs_mult:
   assumes mr: "m dvd r" and nr: "n dvd r" and mn: "gcd m n = 1"
   shows "m * n dvd r"
 proof -
@@ -973,8 +1015,8 @@
 proof (cases "a*b = 0")
   assume "a * b \<noteq> 0"
   hence "gcd a b \<noteq> 0" by simp
-  let ?c = "divide 1 (normalisation_factor (a*b))"
-  from `a * b \<noteq> 0` have [simp]: "is_unit (normalisation_factor (a*b))" by simp
+  let ?c = "1 div normalisation_factor (a * b)"
+  from `a * b \<noteq> 0` have [simp]: "is_unit (normalisation_factor (a * b))" by simp
   from lcm_gcd_prod[of a b] have "lcm a b * gcd a b = a * ?c * b"
     by (simp add: div_mult_swap unit_div_commute)
   hence "lcm a b * gcd a b div gcd a b = a * ?c * b div gcd a b" by simp
@@ -1050,14 +1092,14 @@
   shows "gcd a b = a * b div (lcm a b * normalisation_factor (a * b))"
 proof-
   from assms have "gcd a b \<noteq> 0" by (simp add: lcm_zero)
-  let ?c = "normalisation_factor (a*b)"
+  let ?c = "normalisation_factor (a * b)"
   from `lcm a b \<noteq> 0` have "?c \<noteq> 0" by (intro notI, simp add: lcm_zero no_zero_divisors)
   hence "is_unit ?c" by simp
   from lcm_gcd_prod [of a b] have "gcd a b = a * b div ?c div lcm a b"
     by (subst (2) div_mult_self2_is_id[OF `lcm a b \<noteq> 0`, symmetric], simp add: mult_ac)
-  also from `is_unit ?c` have "... = a * b div (?c * lcm a b)"
-    by (metis local.unit_divide_1 local.unit_divide_1'1)
-  finally show ?thesis by (simp only: ac_simps)
+  also from `is_unit ?c` have "... = a * b div (lcm a b * ?c)"
+    by (metis `?c \<noteq> 0` div_mult_mult1 dvd_mult_div_cancel mult_commute normalisation_factor_dvd')
+  finally show ?thesis .
 qed
 
 lemma normalisation_factor_lcm [simp]:
@@ -1249,11 +1291,11 @@
 
 lemma lcm_div_unit1:
   "is_unit a \<Longrightarrow> lcm (b div a) c = lcm b c"
-  by (metis lcm_mult_unit1 local.unit_divide_1 local.unit_divide_1_unit)
+  by (erule is_unitE [of _ b]) (simp add: lcm_mult_unit1) 
 
 lemma lcm_div_unit2:
   "is_unit a \<Longrightarrow> lcm b (c div a) = lcm b c"
-  by (metis lcm_mult_unit2 local.unit_divide_1 local.unit_divide_1_unit)
+  by (erule is_unitE [of _ c]) (simp add: lcm_mult_unit2)
 
 lemma lcm_left_idem:
   "lcm a (lcm a b) = lcm a b"
@@ -1623,7 +1665,7 @@
 function euclid_ext :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a \<times> 'a" where
   "euclid_ext a b = 
      (if b = 0 then 
-        let c = divide 1 (normalisation_factor a) in (c, 0, a * c)
+        let c = 1 div normalisation_factor a in (c, 0, a * c)
       else 
         case euclid_ext b (a mod b) of
             (s,t,c) \<Rightarrow> (t, s - t * (a div b), c))"
@@ -1633,13 +1675,13 @@
 declare euclid_ext.simps [simp del]
 
 lemma euclid_ext_0: 
-  "euclid_ext a 0 = (divide 1 (normalisation_factor a), 0, a * divide 1 (normalisation_factor a))"
-  by (subst euclid_ext.simps, simp add: Let_def)
+  "euclid_ext a 0 = (1 div normalisation_factor a, 0, a div normalisation_factor a)"
+  by (subst euclid_ext.simps) (simp add: Let_def)
 
 lemma euclid_ext_non_0:
   "b \<noteq> 0 \<Longrightarrow> euclid_ext a b = (case euclid_ext b (a mod b) of 
     (s,t,c) \<Rightarrow> (t, s - t * (a div b), c))"
-  by (subst euclid_ext.simps, simp)
+  by (subst euclid_ext.simps) simp
 
 definition euclid_ext' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a"
 where
@@ -1652,8 +1694,8 @@
   then show ?case
   proof (cases "b = 0")
     case True
-      then show ?thesis by (cases "a = 0") 
-        (simp_all add: euclid_ext_0 unit_div mult_ac unit_simps gcd_0)
+      then show ?thesis by  
+        (simp add: euclid_ext_0 unit_div mult_ac unit_simps gcd_0)
     next
     case False with 1 show ?thesis
       by (simp add: euclid_ext_non_0 ac_simps split: prod.split prod.split_asm)
@@ -1697,7 +1739,7 @@
 lemma bezout: "\<exists>s t. s * a + t * b = gcd a b"
   using euclid_ext'_correct by blast
 
-lemma euclid_ext'_0 [simp]: "euclid_ext' a 0 = (divide 1 (normalisation_factor a), 0)" 
+lemma euclid_ext'_0 [simp]: "euclid_ext' a 0 = (1 div normalisation_factor a, 0)" 
   by (simp add: bezw_def euclid_ext'_def euclid_ext_0)
 
 lemma euclid_ext'_non_0: "b \<noteq> 0 \<Longrightarrow> euclid_ext' a b = (snd (euclid_ext' b (a mod b)),