# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1533074961 -3600
# Node ID 77858f347020d0fc0cba99c9fbca2f82e308e0c5
# Parent  5b269897df9dfad47fb84b4f8a6f92ea1fa8e8ec
de-applying

diff -r 5b269897df9d -r 77858f347020 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun Jul 29 23:04:22 2018 +0100
+++ b/src/HOL/GCD.thy	Tue Jul 31 23:09:21 2018 +0100
@@ -110,7 +110,7 @@
   assumes "a \<in> A"
   shows "a \<^bold>* F A = F A"
   using assms by (induct A rule: infinite_finite_induct)
-    (auto simp add: left_commute [of a])
+    (auto simp: left_commute [of a])
 
 lemma union:
   "F (A \<union> B) = F A \<^bold>* F B"
@@ -239,7 +239,7 @@
 
 lemma is_unit_gcd_iff [simp]:
   "is_unit (gcd a b) \<longleftrightarrow> gcd a b = 1"
-  by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor)
+  by (cases "a = 0 \<and> b = 0") (auto simp: unit_factor_gcd dest: is_unit_unit_factor)
 
 sublocale gcd: abel_semigroup gcd
 proof
@@ -569,20 +569,17 @@
 lemma normalize_lcm_right: "lcm a (normalize b) = lcm a b"
   by (fact lcm.normalize_right_idem)
 
-lemma gcd_mult_unit1: "is_unit a \<Longrightarrow> gcd (b * a) c = gcd b c"
-  apply (rule gcdI)
-     apply simp_all
-  apply (rule dvd_trans)
-   apply (rule gcd_dvd1)
-  apply (simp add: unit_simps)
-  done
+lemma gcd_mult_unit1: 
+  assumes "is_unit a" shows "gcd (b * a) c = gcd b c"
+proof -
+  have "gcd (b * a) c dvd b"
+    using assms local.dvd_mult_unit_iff by blast
+  then show ?thesis
+    by (rule gcdI) simp_all
+qed
 
 lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c"
-  apply (subst gcd.commute)
-  apply (subst gcd_mult_unit1)
-   apply assumption
-  apply (rule gcd.commute)
-  done
+  using gcd.commute gcd_mult_unit1 by auto
 
 lemma gcd_div_unit1: "is_unit a \<Longrightarrow> gcd (b div a) c = gcd b c"
   by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1)
@@ -652,13 +649,13 @@
   "a dvd d \<and> b dvd d \<and> normalize d = d \<and> (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
   by rule (auto intro: lcmI simp: lcm_least lcm_eq_0_iff)
 
-lemma lcm_proj1_if_dvd: "b dvd a \<Longrightarrow> lcm a b = normalize a"
-  apply (cases "a = 0")
-   apply simp
-  apply (rule sym)
-  apply (rule lcmI)
-     apply simp_all
-  done
+lemma lcm_proj1_if_dvd:
+  assumes "b dvd a" shows "lcm a b = normalize a"
+proof (cases "a = 0")
+  case False
+  then show ?thesis
+    using assms gcd_proj2_if_dvd lcm_mult_gcd local.lcm_gcd by auto
+qed auto
 
 lemma lcm_proj2_if_dvd: "a dvd b \<Longrightarrow> lcm a b = normalize b"
   using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps)
@@ -841,14 +838,12 @@
   by (blast intro: Lcm_least dvd_Lcm)
 
 lemma Lcm_Un: "Lcm (A \<union> B) = lcm (Lcm A) (Lcm B)"
-  apply (rule lcmI)
-     apply (blast intro: Lcm_subset)
-    apply (blast intro: Lcm_subset)
-   apply (intro Lcm_least ballI, elim UnE)
-    apply (rule dvd_trans, erule dvd_Lcm, assumption)
-   apply (rule dvd_trans, erule dvd_Lcm, assumption)
-  apply simp
-  done
+proof -
+  have "\<And>d. \<lbrakk>Lcm A dvd d; Lcm B dvd d\<rbrakk> \<Longrightarrow> Lcm (A \<union> B) dvd d"
+    by (meson UnE local.Lcm_least local.dvd_Lcm local.dvd_trans)
+  then show ?thesis
+    by (meson Lcm_subset local.lcm_unique local.normalize_Lcm sup.cobounded1 sup.cobounded2)
+qed
 
 lemma Gcd_0_iff [simp]: "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}"
   (is "?P \<longleftrightarrow> ?Q")
@@ -963,7 +958,7 @@
 next
   case False
   with assms show ?thesis
-    by (induct A rule: finite_ne_induct) (auto simp add: lcm_eq_0_iff)
+    by (induct A rule: finite_ne_induct) (auto simp: lcm_eq_0_iff)
 qed
 
 lemma Gcd_image_normalize [simp]: "Gcd (normalize ` A) = Gcd A"
@@ -996,25 +991,25 @@
 lemma dvd_Gcd_iff: "x dvd Gcd A \<longleftrightarrow> (\<forall>y\<in>A. x dvd y)"
   by (blast dest: dvd_GcdD intro: Gcd_greatest)
 
-lemma Gcd_mult: "Gcd (( * ) c ` A) = normalize c * Gcd A"
+lemma Gcd_mult: "Gcd (( *) c ` A) = normalize c * Gcd A"
 proof (cases "c = 0")
   case True
   then show ?thesis by auto
 next
   case [simp]: False
-  have "Gcd (( * ) c ` A) div c dvd Gcd A"
+  have "Gcd (( *) c ` A) div c dvd Gcd A"
     by (intro Gcd_greatest, subst div_dvd_iff_mult)
        (auto intro!: Gcd_greatest Gcd_dvd simp: mult.commute[of _ c])
-  then have "Gcd (( * ) c ` A) dvd c * Gcd A"
+  then have "Gcd (( *) c ` A) dvd c * Gcd A"
     by (subst (asm) div_dvd_iff_mult) (auto intro: Gcd_greatest simp: mult_ac)
   also have "c * Gcd A = (normalize c * Gcd A) * unit_factor c"
     by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
-  also have "Gcd (( * ) c ` A) dvd \<dots> \<longleftrightarrow> Gcd (( * ) c ` A) dvd normalize c * Gcd A"
+  also have "Gcd (( *) c ` A) dvd \<dots> \<longleftrightarrow> Gcd (( *) c ` A) dvd normalize c * Gcd A"
     by (simp add: dvd_mult_unit_iff)
-  finally have "Gcd (( * ) c ` A) dvd normalize c * Gcd A" .
-  moreover have "normalize c * Gcd A dvd Gcd (( * ) c ` A)"
+  finally have "Gcd (( *) c ` A) dvd normalize c * Gcd A" .
+  moreover have "normalize c * Gcd A dvd Gcd (( *) c ` A)"
     by (intro Gcd_greatest) (auto intro: mult_dvd_mono Gcd_dvd)
-  ultimately have "normalize (Gcd (( * ) c ` A)) = normalize (normalize c * Gcd A)"
+  ultimately have "normalize (Gcd (( *) c ` A)) = normalize (normalize c * Gcd A)"
     by (rule associatedI)
   then show ?thesis
     by (simp add: normalize_mult)
@@ -1035,10 +1030,10 @@
 
 lemma Lcm_mult:
   assumes "A \<noteq> {}"
-  shows "Lcm (( * ) c ` A) = normalize c * Lcm A"
+  shows "Lcm (( *) c ` A) = normalize c * Lcm A"
 proof (cases "c = 0")
   case True
-  with assms have "( * ) c ` A = {0}"
+  with assms have "( *) c ` A = {0}"
     by auto
   with True show ?thesis by auto
 next
@@ -1047,23 +1042,23 @@
     by blast
   have "c dvd c * x"
     by simp
-  also from x have "c * x dvd Lcm (( * ) c ` A)"
+  also from x have "c * x dvd Lcm (( *) c ` A)"
     by (intro dvd_Lcm) auto
-  finally have dvd: "c dvd Lcm (( * ) c ` A)" .
-
-  have "Lcm A dvd Lcm (( * ) c ` A) div c"
+  finally have dvd: "c dvd Lcm (( *) c ` A)" .
+
+  have "Lcm A dvd Lcm (( *) c ` A) div c"
     by (intro Lcm_least dvd_mult_imp_div)
       (auto intro!: Lcm_least dvd_Lcm simp: mult.commute[of _ c])
-  then have "c * Lcm A dvd Lcm (( * ) c ` A)"
+  then have "c * Lcm A dvd Lcm (( *) c ` A)"
     by (subst (asm) dvd_div_iff_mult) (auto intro!: Lcm_least simp: mult_ac dvd)
   also have "c * Lcm A = (normalize c * Lcm A) * unit_factor c"
     by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
-  also have "\<dots> dvd Lcm (( * ) c ` A) \<longleftrightarrow> normalize c * Lcm A dvd Lcm (( * ) c ` A)"
+  also have "\<dots> dvd Lcm (( *) c ` A) \<longleftrightarrow> normalize c * Lcm A dvd Lcm (( *) c ` A)"
     by (simp add: mult_unit_dvd_iff)
-  finally have "normalize c * Lcm A dvd Lcm (( * ) c ` A)" .
-  moreover have "Lcm (( * ) c ` A) dvd normalize c * Lcm A"
+  finally have "normalize c * Lcm A dvd Lcm (( *) c ` A)" .
+  moreover have "Lcm (( *) c ` A) dvd normalize c * Lcm A"
     by (intro Lcm_least) (auto intro: mult_dvd_mono dvd_Lcm)
-  ultimately have "normalize (normalize c * Lcm A) = normalize (Lcm (( * ) c ` A))"
+  ultimately have "normalize (normalize c * Lcm A) = normalize (Lcm (( *) c ` A))"
     by (rule associatedI)
   then show ?thesis
     by (simp add: normalize_mult)
@@ -1240,7 +1235,7 @@
 
 lemma Lcm_fin_0_iff:
   "Lcm\<^sub>f\<^sub>i\<^sub>n A = 0 \<longleftrightarrow> 0 \<in> A" if "finite A"
-  using that by (induct A) (auto simp add: lcm_eq_0_iff)
+  using that by (induct A) (auto simp: lcm_eq_0_iff)
 
 lemma Lcm_fin_1_iff:
   "Lcm\<^sub>f\<^sub>i\<^sub>n A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a) \<and> finite A"
@@ -1452,7 +1447,7 @@
   from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
     by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
-    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
+    by (auto simp: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   have "?g \<noteq> 0"
     using assms by simp
   moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
@@ -1480,11 +1475,12 @@
 lemma gcd_coprime_exists:
   assumes "gcd a b \<noteq> 0"
   shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
-  apply (rule_tac x = "a div gcd a b" in exI)
-  apply (rule_tac x = "b div gcd a b" in exI)
-  using assms
-  apply (auto intro: div_gcd_coprime)
-  done
+proof -
+  have "coprime (a div gcd a b) (b div gcd a b)"
+    using assms div_gcd_coprime by auto
+  then show ?thesis
+    by force
+qed
 
 lemma pow_divides_pow_iff [simp]:
   "a ^ n dvd b ^ n \<longleftrightarrow> a dvd b" if "n > 0"
@@ -1628,7 +1624,7 @@
     by simp
   also note gcd_mult_distrib
   also have "unit_factor (gcd a b ^ n) = 1"
-    using False by (auto simp add: unit_factor_power unit_factor_gcd)
+    using False by (auto simp: unit_factor_power unit_factor_gcd)
   also have "(gcd a b) ^ n * (a div gcd a b) ^ n = a ^ n"
     by (simp add: ac_simps div_power dvd_power_same)
   also have "(gcd a b) ^ n * (b div gcd a b) ^ n = b ^ n"
@@ -1809,16 +1805,16 @@
   for i j :: int
   by (simp only: lcm_int_def)
 
-lemma gcd_nat_induct:
+lemma gcd_nat_induct [case_names base step]:
   fixes m n :: nat
   assumes "\<And>m. P m 0"
     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
   shows "P m n"
-  apply (rule gcd_nat.induct)
-  apply (case_tac "y = 0")
-  using assms
-   apply simp_all
-  done
+proof (induction m n rule: gcd_nat.induct)
+  case (1 x y)
+  then show ?case
+    using assms neq0_conv by blast
+qed
 
 lemma gcd_neg1_int [simp]: "gcd (- x) y = gcd x y"
   for x y :: int
@@ -1856,7 +1852,7 @@
     and "x \<le> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (lcm (- x) y)"
     and "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (lcm (- x) (- y))"
   shows "P (lcm x y)"
-  using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith
+  using assms by (auto simp: lcm_neg1_int lcm_neg2_int) arith
 
 lemma lcm_ge_0_int [simp]: "lcm x y \<ge> 0"
   for x y :: int
@@ -1907,7 +1903,7 @@
 
 lemma gcd_idem_int: "gcd x x = \<bar>x\<bar>"
   for x :: int
-  by (auto simp add: gcd_int_def)
+  by (auto simp: gcd_int_def)
 
 declare gcd_nat.simps [simp del]
 
@@ -1921,13 +1917,10 @@
   fix m n :: nat
   show "gcd m n dvd m" and "gcd m n dvd n"
   proof (induct m n rule: gcd_nat_induct)
-    fix m n :: nat
-    assume "gcd n (m mod n) dvd m mod n"
-      and "gcd n (m mod n) dvd n"
+    case (step m n)
     then have "gcd n (m mod n) dvd m"
-      by (rule dvd_mod_imp_dvd)
-    moreover assume "0 < n"
-    ultimately show "gcd m n dvd m"
+      by (metis dvd_mod_imp_dvd)
+    with step show "gcd m n dvd m"
       by (simp add: gcd_non_0_nat)
   qed (simp_all add: gcd_0_nat gcd_non_0_nat)
 next
@@ -1979,25 +1972,16 @@
 
 lemma gcd_unique_nat: "d dvd a \<and> d dvd b \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   for d a :: nat
-  apply auto
-  apply (rule dvd_antisym)
-   apply (erule (1) gcd_greatest)
-  apply auto
-  done
+  using gcd_unique by fastforce
 
 lemma gcd_unique_int:
   "d \<ge> 0 \<and> d dvd a \<and> d dvd b \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   for d a :: int
-  apply (cases "d = 0")
-   apply simp
-  apply (rule iffI)
-   apply (rule zdvd_antisym_nonneg)
-      apply (auto intro: gcd_greatest)
-  done
+  using zdvd_antisym_nonneg by auto
 
 interpretation gcd_nat:
   semilattice_neutr_order gcd "0::nat" Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n"
-  by standard (auto simp add: gcd_unique_nat [symmetric] intro: dvd_antisym dvd_trans)
+  by standard (auto simp: gcd_unique_nat [symmetric] intro: dvd_antisym dvd_trans)
 
 lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd x y = \<bar>x\<bar>"
   for x y :: int
@@ -2013,11 +1997,11 @@
 lemma gcd_mult_distrib_nat: "k * gcd m n = gcd (k * m) (k * n)"
   for k m n :: nat
   \<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close>
-  apply (induct m n rule: gcd_nat_induct)
-   apply simp
-  apply (cases "k = 0")
-   apply (simp_all add: gcd_non_0_nat)
-  done
+proof (induct m n rule: gcd_nat_induct)
+  case (step m n)
+  then show ?case
+    by (metis gcd_mult_distrib' gcd_red_nat)
+qed auto
 
 lemma gcd_mult_distrib_int: "\<bar>k\<bar> * gcd m n = gcd (k * m) (k * n)"
   for k m n :: int
@@ -2033,34 +2017,49 @@
 
 lemma gcd_diff2_nat: "n \<ge> m \<Longrightarrow> gcd (n - m) n = gcd m n"
   for m n :: nat
-  apply (subst gcd.commute)
-  apply (subst gcd_diff1_nat [symmetric])
-   apply auto
-  apply (subst gcd.commute)
-  apply (subst gcd_diff1_nat)
-   apply assumption
-  apply (rule gcd.commute)
-  done
-
-lemma gcd_non_0_int: "y > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
-  for x y :: int
-  apply (frule_tac b = y and a = x in pos_mod_sign)
-  apply (simp del: Euclidean_Division.pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
-  apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
-  apply (frule_tac a = x in pos_mod_bound)
-  apply (subst (1 2) gcd.commute)
-  apply (simp del: Euclidean_Division.pos_mod_bound add: nat_diff_distrib gcd_diff2_nat nat_le_eq_zle)
-  done
+  by (metis gcd.commute gcd_add2 gcd_diff1_nat le_add_diff_inverse2)
+
+lemma gcd_non_0_int: 
+  fixes x y :: int
+  assumes "y > 0" shows "gcd x y = gcd y (x mod y)"
+proof (cases "x mod y = 0")
+  case False
+  then have neg: "x mod y = y - (- x) mod y"
+    by (simp add: zmod_zminus1_eq_if)
+  have xy: "0 \<le> x mod y" 
+    by (simp add: assms)
+  show ?thesis
+  proof (cases "x < 0")
+    case True
+    have "nat (- x mod y) \<le> nat y"
+      by (simp add: assms dual_order.order_iff_strict)
+    moreover have "gcd (nat (- x)) (nat y) = gcd (nat (- x mod y)) (nat y)"
+      using True assms gcd_non_0_nat nat_mod_distrib by auto
+    ultimately have "gcd (nat (- x)) (nat y) = gcd (nat y) (nat (x mod y))"
+      using assms 
+      by (simp add: neg nat_diff_distrib') (metis gcd.commute gcd_diff2_nat)
+    with assms \<open>0 \<le> x mod y\<close> show ?thesis
+      by (simp add: True dual_order.order_iff_strict gcd_int_def)
+  next
+    case False
+    with assms xy have "gcd (nat x) (nat y) = gcd (nat y) (nat x mod nat y)"
+      using gcd_red_nat by blast
+    with False assms show ?thesis
+      by (simp add: gcd_int_def nat_mod_distrib)
+  qed
+qed (use assms in auto)
 
 lemma gcd_red_int: "gcd x y = gcd y (x mod y)"
   for x y :: int
-  apply (cases "y = 0")
-   apply force
-  apply (cases "y > 0")
-   apply (subst gcd_non_0_int, auto)
-  apply (insert gcd_non_0_int [of "- y" "- x"])
-  apply auto
-  done
+proof (cases y "0::int" rule: linorder_cases)
+  case less
+  with gcd_non_0_int [of "- y" "- x"] show ?thesis
+    by auto
+next
+  case greater
+  with gcd_non_0_int [of y x] show ?thesis
+    by auto
+qed auto
 
 (* TODO: differences, and all variations of addition rules
     as simplification rules for nat and int *)
@@ -2092,34 +2091,34 @@
 qed
 
 lemma Max_divisors_self_nat [simp]: "n \<noteq> 0 \<Longrightarrow> Max {d::nat. d dvd n} = n"
-  apply (rule antisym)
-   apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
-  apply simp
-  done
-
-lemma Max_divisors_self_int [simp]: "n \<noteq> 0 \<Longrightarrow> Max {d::int. d dvd n} = \<bar>n\<bar>"
-  apply (rule antisym)
-   apply (rule Max_le_iff [THEN iffD2])
-     apply (auto intro: abs_le_D1 dvd_imp_le_int)
-  done
-
-lemma gcd_is_Max_divisors_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> gcd m n = Max {d. d dvd m \<and> d dvd n}"
-  for m n :: nat
-  apply (rule Max_eqI[THEN sym])
-    apply (metis finite_Collect_conjI finite_divisors_nat)
-   apply simp
-   apply (metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff gcd_pos_nat)
-  apply simp
-  done
-
-lemma gcd_is_Max_divisors_int: "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> gcd m n = Max {d. d dvd m \<and> d dvd n}"
-  for m n :: int
-  apply (rule Max_eqI[THEN sym])
-    apply (metis finite_Collect_conjI finite_divisors_int)
-   apply simp
-   apply (metis gcd_greatest_iff gcd_pos_int zdvd_imp_le)
-  apply simp
-  done
+  by (fastforce intro: antisym Max_le_iff[THEN iffD2] simp: dvd_imp_le)
+
+lemma Max_divisors_self_int [simp]: 
+  assumes "n \<noteq> 0" shows "Max {d::int. d dvd n} = \<bar>n\<bar>"
+proof (rule antisym)
+  show "Max {d. d dvd n} \<le> \<bar>n\<bar>"
+    using assms by (auto intro: abs_le_D1 dvd_imp_le_int intro!: Max_le_iff [THEN iffD2])
+qed (simp add: assms)
+
+lemma gcd_is_Max_divisors_nat:
+  fixes m n :: nat
+  assumes "n > 0" shows "gcd m n = Max {d. d dvd m \<and> d dvd n}"
+proof (rule Max_eqI[THEN sym], simp_all)
+  show "finite {d. d dvd m \<and> d dvd n}"
+    by (simp add: \<open>n > 0\<close>)
+  show "\<And>y. y dvd m \<and> y dvd n \<Longrightarrow> y \<le> gcd m n"
+    by (simp add: \<open>n > 0\<close> dvd_imp_le)
+qed
+
+lemma gcd_is_Max_divisors_int:
+  fixes m n :: int
+  assumes "n \<noteq> 0" shows "gcd m n = Max {d. d dvd m \<and> d dvd n}"
+proof (rule Max_eqI[THEN sym], simp_all)
+  show "finite {d. d dvd m \<and> d dvd n}"
+    by (simp add: \<open>n \<noteq> 0\<close>)
+  show "\<And>y. y dvd m \<and> y dvd n \<Longrightarrow> y \<le> gcd m n"
+    by (simp add: \<open>n \<noteq> 0\<close> zdvd_imp_le)
+qed
 
 lemma gcd_code_int [code]: "gcd k l = \<bar>if l = 0 then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
   for k l :: int
@@ -2178,25 +2177,22 @@
 
 declare bezw.simps [simp del]
 
-lemma bezw_aux: "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
+
+lemma bezw_aux: "int (gcd x y) = fst (bezw x y) * int x + snd (bezw x y) * int y"
 proof (induct x y rule: gcd_nat_induct)
-  fix m :: nat
-  show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
-    by auto
-next
-  fix m n :: nat
-  assume ngt0: "n > 0"
-    and ih: "fst (bezw n (m mod n)) * int n + snd (bezw n (m mod n)) * int (m mod n) =
-      int (gcd n (m mod n))"
-  then show "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
-    apply (simp add: bezw_non_0 gcd_non_0_nat)
-    apply (erule subst)
-    apply (simp add: field_simps)
-    apply (subst div_mult_mod_eq [of m n, symmetric])
-      (* applying simp here undoes the last substitution! what is procedure cancel_div_mod? *)
-    apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult)
-    done
-qed
+  case (step m n)
+  then have "fst (bezw m n) * int m + snd (bezw m n) * int n - int (gcd m n) 
+             = int m * snd (bezw n (m mod n)) -
+               (int (m mod n) * snd (bezw n (m mod n)) + int n * (int (m div n) * snd (bezw n (m mod n))))"
+    by (simp add: bezw_non_0 gcd_non_0_nat field_simps)
+  also have "\<dots> = int m * snd (bezw n (m mod n)) - (int (m mod n) + int (n * (m div n))) * snd (bezw n (m mod n))"
+    by (simp add: distrib_right)
+  also have "\<dots> = 0"
+    by (metis cancel_comm_monoid_add_class.diff_cancel mod_mult_div_eq of_nat_add)
+  finally show ?case
+    by simp
+qed auto
+
 
 lemma bezout_int: "\<exists>u v. u * x + v * y = gcd x y"
   for x y :: int
@@ -2204,13 +2200,9 @@
   have aux: "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> \<exists>u v. u * x + v * y = gcd x y" for x y :: int
     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
-    apply (unfold gcd_int_def)
-    apply simp
-    apply (subst bezw_aux [symmetric])
-    apply auto
-    done
+    by (simp add: bezw_aux gcd_int_def)
   consider "x \<ge> 0" "y \<ge> 0" | "x \<ge> 0" "y \<le> 0" | "x \<le> 0" "y \<ge> 0" | "x \<le> 0" "y \<le> 0"
-    by atomize_elim auto
+    using linear by blast
   then show ?thesis
   proof cases
     case 1
@@ -2218,48 +2210,29 @@
   next
     case 2
     then show ?thesis
-      apply -
-      apply (insert aux [of x "-y"])
-      apply auto
-      apply (rule_tac x = u in exI)
-      apply (rule_tac x = "-v" in exI)
-      apply (subst gcd_neg2_int [symmetric])
-      apply auto
-      done
+      using aux [of x "-y"]
+      by (metis gcd_neg2_int mult.commute mult_minus_right neg_0_le_iff_le)
   next
     case 3
     then show ?thesis
-      apply -
-      apply (insert aux [of "-x" y])
-      apply auto
-      apply (rule_tac x = "-u" in exI)
-      apply (rule_tac x = v in exI)
-      apply (subst gcd_neg1_int [symmetric])
-      apply auto
-      done
+      using aux [of "-x" y]
+      by (metis gcd.commute gcd_neg2_int mult.commute mult_minus_right neg_0_le_iff_le)
   next
     case 4
     then show ?thesis
-      apply -
-      apply (insert aux [of "-x" "-y"])
-      apply auto
-      apply (rule_tac x = "-u" in exI)
-      apply (rule_tac x = "-v" in exI)
-      apply (subst gcd_neg1_int [symmetric])
-      apply (subst gcd_neg2_int [symmetric])
-      apply auto
-      done
+      using aux [of "-x" "-y"]
+      by (metis diff_0 diff_ge_0_iff_ge gcd_neg1_int gcd_neg2_int mult.commute mult_minus_right)
   qed
 qed
 
 
 text \<open>Versions of Bezout for \<open>nat\<close>, by Amine Chaieb.\<close>
 
-lemma ind_euclid:
+lemma Euclid_induct [case_names swap zero add]:
   fixes P :: "nat \<Rightarrow> nat \<Rightarrow> bool"
-  assumes c: " \<forall>a b. P a b \<longleftrightarrow> P b a"
-    and z: "\<forall>a. P a 0"
-    and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
+  assumes c: "\<And>a b. P a b \<longleftrightarrow> P b a"
+    and z: "\<And>a. P a 0"
+    and add: "\<And>a b. P a b \<longrightarrow> P a (a + b)"
   shows "P a b"
 proof (induct "a + b" arbitrary: a b rule: less_induct)
   case less
@@ -2302,53 +2275,32 @@
 qed
 
 lemma bezout_lemma_nat:
-  assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
-    (a * x = b * y + d \<or> b * x = a * y + d)"
-  shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
-    (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
-  using ex
-  apply clarsimp
-  apply (rule_tac x="d" in exI)
-  apply simp
-  apply (case_tac "a * x = b * y + d")
-   apply simp_all
-   apply (rule_tac x="x + y" in exI)
-   apply (rule_tac x="y" in exI)
-   apply algebra
-  apply (rule_tac x="x" in exI)
-  apply (rule_tac x="x + y" in exI)
-  apply algebra
-  done
-
-lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
-    (a * x = b * y + d \<or> b * x = a * y + d)"
-  apply (induct a b rule: ind_euclid)
-    apply blast
-   apply clarify
-   apply (rule_tac x="a" in exI)
-   apply simp
-  apply clarsimp
-  apply (rule_tac x="d" in exI)
-  apply (case_tac "a * x = b * y + d")
-   apply simp_all
-   apply (rule_tac x="x+y" in exI)
-   apply (rule_tac x="y" in exI)
-   apply algebra
-  apply (rule_tac x="x" in exI)
-  apply (rule_tac x="x+y" in exI)
-  apply algebra
-  done
-
-lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
-    (a * x - b * y = d \<or> b * x - a * y = d)"
-  using bezout_add_nat[of a b]
-  apply clarsimp
-  apply (rule_tac x="d" in exI)
-  apply simp
-  apply (rule_tac x="x" in exI)
-  apply (rule_tac x="y" in exI)
+  fixes d::nat
+  shows "\<lbrakk>d dvd a; d dvd b; a * x = b * y + d \<or> b * x = a * y + d\<rbrakk>
+    \<Longrightarrow> \<exists>x y. d dvd a \<and> d dvd a + b \<and> (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
   apply auto
-  done
+  apply (metis add_mult_distrib2 left_add_mult_distrib)
+  apply (rule_tac x=x in exI)
+  by (metis add_mult_distrib2 mult.commute add.assoc)
+
+lemma bezout_add_nat: 
+  "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> (a * x = b * y + d \<or> b * x = a * y + d)"
+proof (induct a b rule: Euclid_induct)
+  case (swap a b)
+  then show ?case
+    by blast
+next
+  case (zero a)
+  then show ?case
+    by fastforce    
+next
+  case (add a b)
+  then show ?case
+    by (meson bezout_lemma_nat)
+qed
+
+lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> (a * x - b * y = d \<or> b * x - a * y = d)"
+  using bezout_add_nat[of a b]  by (metis add_diff_cancel_left')
 
 lemma bezout_add_strong_nat:
   fixes a b :: nat
@@ -2356,7 +2308,7 @@
   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
 proof -
   consider d x y where "d dvd a" "d dvd b" "a * x = b * y + d"
-    | d x y where "d dvd a" "d dvd b" "b * x = a * y + d"
+         | d x y where "d dvd a" "d dvd b" "b * x = a * y + d"
     using bezout_add_nat [of a b] by blast
   then show ?thesis
   proof cases
@@ -2377,13 +2329,7 @@
       proof cases
         case 1
         with a H show ?thesis
-          apply simp
-          apply (rule exI[where x = b])
-          apply simp
-          apply (rule exI[where x = b])
-          apply (rule exI[where x = "a - 1"])
-          apply (simp add: diff_mult_distrib2)
-          done
+          by (metis Suc_pred add.commute mult.commute mult_Suc_right neq0_conv)
       next
         case 2
         show ?thesis
@@ -2410,13 +2356,7 @@
           then have "a * ((b - 1) * y) = b * (x * (b - 1) - d) + d"
             by (simp only: diff_mult_distrib2 ac_simps)
           with H(1,2) show ?thesis
-            apply -
-            apply (rule exI [where x = d])
-            apply simp
-            apply (rule exI [where x = "(b - 1) * y"])
-            apply (rule exI [where x = "x * (b - 1) - d"])
-            apply simp
-            done
+            by blast
         qed
       qed
     qed
@@ -2451,17 +2391,11 @@
   
 lemma prod_gcd_lcm_nat: "m * n = gcd m n * lcm m n"
   for m n :: nat
-  unfolding lcm_nat_def
-  by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod])
+  by simp
 
 lemma prod_gcd_lcm_int: "\<bar>m\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
   for m n :: int
-  unfolding lcm_int_def gcd_int_def
-  apply (subst of_nat_mult [symmetric])
-  apply (subst prod_gcd_lcm_nat [symmetric])
-  apply (subst nat_abs_mult_distrib [symmetric])
-  apply (simp add: abs_mult)
-  done
+  by simp
 
 lemma lcm_pos_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> lcm m n > 0"
   for m n :: nat
@@ -2473,7 +2407,7 @@
 
 lemma dvd_pos_nat: "n > 0 \<Longrightarrow> m dvd n \<Longrightarrow> m > 0"  (* FIXME move *)
   for m n :: nat
-  by (cases m) auto
+  by auto
 
 lemma lcm_unique_nat:
   "a dvd d \<and> b dvd d \<and> (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
@@ -2487,17 +2421,11 @@
 
 lemma lcm_proj2_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> lcm x y = y"
   for x y :: nat
-  apply (rule sym)
-  apply (subst lcm_unique_nat [symmetric])
-  apply auto
-  done
+  by (simp add: lcm_proj2_if_dvd)
 
 lemma lcm_proj2_if_dvd_int [simp]: "x dvd y \<Longrightarrow> lcm x y = \<bar>y\<bar>"
   for x y :: int
-  apply (rule sym)
-  apply (subst lcm_unique_int [symmetric])
-  apply auto
-  done
+  by (simp add: lcm_proj2_if_dvd)
 
 lemma lcm_proj1_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> lcm y x = y"
   for x y :: nat
@@ -2551,7 +2479,7 @@
   by (simp add: Lcm_nat_def del: One_nat_def)
 
 lemma Lcm_nat_insert: "Lcm (insert n M) = lcm n (Lcm M)" for n :: nat
-  by (cases "finite M") (auto simp add: Lcm_nat_def simp del: One_nat_def)
+  by (cases "finite M") (auto simp: Lcm_nat_def simp del: One_nat_def)
 
 lemma Lcm_nat_infinite: "infinite M \<Longrightarrow> Lcm M = 0" for M :: "nat set"
   by (simp add: Lcm_nat_def)
@@ -2595,9 +2523,9 @@
   fix N :: "nat set"
   fix n :: nat
   show "Gcd N dvd n" if "n \<in> N"
-    using that by (induct N rule: infinite_finite_induct) (auto simp add: Gcd_nat_def)
+    using that by (induct N rule: infinite_finite_induct) (auto simp: Gcd_nat_def)
   show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m"
-    using that by (induct N rule: infinite_finite_induct) (auto simp add: Gcd_nat_def)
+    using that by (induct N rule: infinite_finite_induct) (auto simp: Gcd_nat_def)
   show "n dvd Lcm N" if "n \<in> N"
     using that by (induct N rule: infinite_finite_induct) auto
   show "Lcm N dvd n" if "\<And>m. m \<in> N \<Longrightarrow> m dvd n"
@@ -2629,52 +2557,51 @@
   from fin show "Gcd M \<le> Max (\<Inter>m\<in>M. {d. d dvd m})"
     by (auto intro: Max_ge Gcd_dvd)
   from fin show "Max (\<Inter>m\<in>M. {d. d dvd m}) \<le> Gcd M"
-    apply (rule Max.boundedI)
-     apply auto
-    apply (meson Gcd_dvd Gcd_greatest \<open>0 < m\<close> \<open>m \<in> M\<close> dvd_imp_le dvd_pos_nat)
-    done
+  proof (rule Max.boundedI, simp_all)
+    show "(\<Inter>m\<in>M. {d. d dvd m}) \<noteq> {}"
+      by auto
+    show "\<And>a. \<forall>x\<in>M. a dvd x \<Longrightarrow> a \<le> Gcd M"
+      by (meson Gcd_dvd Gcd_greatest \<open>0 < m\<close> \<open>m \<in> M\<close> dvd_imp_le dvd_pos_nat)
+  qed
 qed
 
 lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0})"
   for M :: "nat set"
-  apply (induct pred: finite)
-   apply simp
-  apply (case_tac "x = 0")
-   apply simp
-  apply (subgoal_tac "insert x F - {0} = insert x (F - {0})")
-   apply simp
-  apply blast
-  done
+proof (induct pred: finite)
+  case (insert x M)
+  then show ?case
+    by (simp add: insert_Diff_if)
+qed auto
 
 lemma Lcm_in_lcm_closed_set_nat:
-  "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> \<forall>m n. m \<in> M \<longrightarrow> n \<in> M \<longrightarrow> lcm m n \<in> M \<Longrightarrow> Lcm M \<in> M"
-  for M :: "nat set"
-  apply (induct rule: finite_linorder_min_induct)
-   apply simp
-  apply simp
-  apply (subgoal_tac "\<forall>m n. m \<in> A \<longrightarrow> n \<in> A \<longrightarrow> lcm m n \<in> A")
-   apply simp
-   apply(case_tac "A = {}")
-    apply simp
-   apply simp
-  apply (metis lcm_pos_nat lcm_unique_nat linorder_neq_iff nat_dvd_not_less not_less0)
-  done
+  fixes M :: "nat set" 
+  assumes "finite M" "M \<noteq> {}" "\<And>m n. \<lbrakk>m \<in> M; n \<in> M\<rbrakk> \<Longrightarrow> lcm m n \<in> M"
+  shows "Lcm M \<in> M"
+  using assms
+proof (induction M rule: finite_linorder_min_induct)
+  case (insert x M)
+  then have "\<And>m n. m \<in> M \<Longrightarrow> n \<in> M \<Longrightarrow> lcm m n \<in> M"
+    by (metis dvd_lcm1 gr0I insert_iff lcm_pos_nat nat_dvd_not_less)
+  with insert show ?case
+    by simp (metis Lcm_nat_empty One_nat_def dvd_1_left dvd_lcm2)
+qed auto
 
 lemma Lcm_eq_Max_nat:
-  "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> 0 \<notin> M \<Longrightarrow> \<forall>m n. m \<in> M \<longrightarrow> n \<in> M \<longrightarrow> lcm m n \<in> M \<Longrightarrow> Lcm M = Max M"
-  for M :: "nat set"
-  apply (rule antisym)
-   apply (rule Max_ge)
-    apply assumption
-   apply (erule (2) Lcm_in_lcm_closed_set_nat)
-  apply (auto simp add: not_le Lcm_0_iff dvd_imp_le leD le_neq_trans)
-  done
+  fixes M :: "nat set" 
+  assumes M: "finite M" "M \<noteq> {}" "0 \<notin> M" and lcm: "\<And>m n. \<lbrakk>m \<in> M; n \<in> M\<rbrakk> \<Longrightarrow> lcm m n \<in> M"
+  shows "Lcm M = Max M"
+proof (rule antisym)
+  show "Lcm M \<le> Max M"
+    by (simp add: Lcm_in_lcm_closed_set_nat \<open>finite M\<close> \<open>M \<noteq> {}\<close> lcm)
+  show "Max M \<le> Lcm M"
+    by (meson Lcm_0_iff Max_in M dvd_Lcm dvd_imp_le le_0_eq not_le)
+qed
 
 lemma mult_inj_if_coprime_nat:
-  "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> \<forall>a\<in>A. \<forall>b\<in>B. coprime (f a) (g b) \<Longrightarrow>
+  "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> (\<And>a b. \<lbrakk>a\<in>A; b\<in>B\<rbrakk> \<Longrightarrow> coprime (f a) (g b)) \<Longrightarrow>
     inj_on (\<lambda>(a, b). f a * g b) (A \<times> B)"
   for f :: "'a \<Rightarrow> nat" and g :: "'b \<Rightarrow> nat"
-  by (auto simp add: inj_on_def coprime_crossproduct_nat simp del: One_nat_def)
+  by (auto simp: inj_on_def coprime_crossproduct_nat simp del: One_nat_def)
 
 
 subsubsection \<open>Setwise GCD and LCM for integers\<close>