de-applying
authorpaulson <lp15@cam.ac.uk>
Tue Jul 31 23:09:21 2018 +0100 (11 months ago)
changeset 6870877858f347020
parent 68707 5b269897df9d
child 68709 6d9eca4805ff
de-applying
src/HOL/GCD.thy
     1.1 --- a/src/HOL/GCD.thy	Sun Jul 29 23:04:22 2018 +0100
     1.2 +++ b/src/HOL/GCD.thy	Tue Jul 31 23:09:21 2018 +0100
     1.3 @@ -110,7 +110,7 @@
     1.4    assumes "a \<in> A"
     1.5    shows "a \<^bold>* F A = F A"
     1.6    using assms by (induct A rule: infinite_finite_induct)
     1.7 -    (auto simp add: left_commute [of a])
     1.8 +    (auto simp: left_commute [of a])
     1.9  
    1.10  lemma union:
    1.11    "F (A \<union> B) = F A \<^bold>* F B"
    1.12 @@ -239,7 +239,7 @@
    1.13  
    1.14  lemma is_unit_gcd_iff [simp]:
    1.15    "is_unit (gcd a b) \<longleftrightarrow> gcd a b = 1"
    1.16 -  by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor)
    1.17 +  by (cases "a = 0 \<and> b = 0") (auto simp: unit_factor_gcd dest: is_unit_unit_factor)
    1.18  
    1.19  sublocale gcd: abel_semigroup gcd
    1.20  proof
    1.21 @@ -569,20 +569,17 @@
    1.22  lemma normalize_lcm_right: "lcm a (normalize b) = lcm a b"
    1.23    by (fact lcm.normalize_right_idem)
    1.24  
    1.25 -lemma gcd_mult_unit1: "is_unit a \<Longrightarrow> gcd (b * a) c = gcd b c"
    1.26 -  apply (rule gcdI)
    1.27 -     apply simp_all
    1.28 -  apply (rule dvd_trans)
    1.29 -   apply (rule gcd_dvd1)
    1.30 -  apply (simp add: unit_simps)
    1.31 -  done
    1.32 +lemma gcd_mult_unit1: 
    1.33 +  assumes "is_unit a" shows "gcd (b * a) c = gcd b c"
    1.34 +proof -
    1.35 +  have "gcd (b * a) c dvd b"
    1.36 +    using assms local.dvd_mult_unit_iff by blast
    1.37 +  then show ?thesis
    1.38 +    by (rule gcdI) simp_all
    1.39 +qed
    1.40  
    1.41  lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c"
    1.42 -  apply (subst gcd.commute)
    1.43 -  apply (subst gcd_mult_unit1)
    1.44 -   apply assumption
    1.45 -  apply (rule gcd.commute)
    1.46 -  done
    1.47 +  using gcd.commute gcd_mult_unit1 by auto
    1.48  
    1.49  lemma gcd_div_unit1: "is_unit a \<Longrightarrow> gcd (b div a) c = gcd b c"
    1.50    by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1)
    1.51 @@ -652,13 +649,13 @@
    1.52    "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"
    1.53    by rule (auto intro: lcmI simp: lcm_least lcm_eq_0_iff)
    1.54  
    1.55 -lemma lcm_proj1_if_dvd: "b dvd a \<Longrightarrow> lcm a b = normalize a"
    1.56 -  apply (cases "a = 0")
    1.57 -   apply simp
    1.58 -  apply (rule sym)
    1.59 -  apply (rule lcmI)
    1.60 -     apply simp_all
    1.61 -  done
    1.62 +lemma lcm_proj1_if_dvd:
    1.63 +  assumes "b dvd a" shows "lcm a b = normalize a"
    1.64 +proof (cases "a = 0")
    1.65 +  case False
    1.66 +  then show ?thesis
    1.67 +    using assms gcd_proj2_if_dvd lcm_mult_gcd local.lcm_gcd by auto
    1.68 +qed auto
    1.69  
    1.70  lemma lcm_proj2_if_dvd: "a dvd b \<Longrightarrow> lcm a b = normalize b"
    1.71    using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps)
    1.72 @@ -841,14 +838,12 @@
    1.73    by (blast intro: Lcm_least dvd_Lcm)
    1.74  
    1.75  lemma Lcm_Un: "Lcm (A \<union> B) = lcm (Lcm A) (Lcm B)"
    1.76 -  apply (rule lcmI)
    1.77 -     apply (blast intro: Lcm_subset)
    1.78 -    apply (blast intro: Lcm_subset)
    1.79 -   apply (intro Lcm_least ballI, elim UnE)
    1.80 -    apply (rule dvd_trans, erule dvd_Lcm, assumption)
    1.81 -   apply (rule dvd_trans, erule dvd_Lcm, assumption)
    1.82 -  apply simp
    1.83 -  done
    1.84 +proof -
    1.85 +  have "\<And>d. \<lbrakk>Lcm A dvd d; Lcm B dvd d\<rbrakk> \<Longrightarrow> Lcm (A \<union> B) dvd d"
    1.86 +    by (meson UnE local.Lcm_least local.dvd_Lcm local.dvd_trans)
    1.87 +  then show ?thesis
    1.88 +    by (meson Lcm_subset local.lcm_unique local.normalize_Lcm sup.cobounded1 sup.cobounded2)
    1.89 +qed
    1.90  
    1.91  lemma Gcd_0_iff [simp]: "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}"
    1.92    (is "?P \<longleftrightarrow> ?Q")
    1.93 @@ -963,7 +958,7 @@
    1.94  next
    1.95    case False
    1.96    with assms show ?thesis
    1.97 -    by (induct A rule: finite_ne_induct) (auto simp add: lcm_eq_0_iff)
    1.98 +    by (induct A rule: finite_ne_induct) (auto simp: lcm_eq_0_iff)
    1.99  qed
   1.100  
   1.101  lemma Gcd_image_normalize [simp]: "Gcd (normalize ` A) = Gcd A"
   1.102 @@ -996,25 +991,25 @@
   1.103  lemma dvd_Gcd_iff: "x dvd Gcd A \<longleftrightarrow> (\<forall>y\<in>A. x dvd y)"
   1.104    by (blast dest: dvd_GcdD intro: Gcd_greatest)
   1.105  
   1.106 -lemma Gcd_mult: "Gcd (( * ) c ` A) = normalize c * Gcd A"
   1.107 +lemma Gcd_mult: "Gcd (( *) c ` A) = normalize c * Gcd A"
   1.108  proof (cases "c = 0")
   1.109    case True
   1.110    then show ?thesis by auto
   1.111  next
   1.112    case [simp]: False
   1.113 -  have "Gcd (( * ) c ` A) div c dvd Gcd A"
   1.114 +  have "Gcd (( *) c ` A) div c dvd Gcd A"
   1.115      by (intro Gcd_greatest, subst div_dvd_iff_mult)
   1.116         (auto intro!: Gcd_greatest Gcd_dvd simp: mult.commute[of _ c])
   1.117 -  then have "Gcd (( * ) c ` A) dvd c * Gcd A"
   1.118 +  then have "Gcd (( *) c ` A) dvd c * Gcd A"
   1.119      by (subst (asm) div_dvd_iff_mult) (auto intro: Gcd_greatest simp: mult_ac)
   1.120    also have "c * Gcd A = (normalize c * Gcd A) * unit_factor c"
   1.121      by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
   1.122 -  also have "Gcd (( * ) c ` A) dvd \<dots> \<longleftrightarrow> Gcd (( * ) c ` A) dvd normalize c * Gcd A"
   1.123 +  also have "Gcd (( *) c ` A) dvd \<dots> \<longleftrightarrow> Gcd (( *) c ` A) dvd normalize c * Gcd A"
   1.124      by (simp add: dvd_mult_unit_iff)
   1.125 -  finally have "Gcd (( * ) c ` A) dvd normalize c * Gcd A" .
   1.126 -  moreover have "normalize c * Gcd A dvd Gcd (( * ) c ` A)"
   1.127 +  finally have "Gcd (( *) c ` A) dvd normalize c * Gcd A" .
   1.128 +  moreover have "normalize c * Gcd A dvd Gcd (( *) c ` A)"
   1.129      by (intro Gcd_greatest) (auto intro: mult_dvd_mono Gcd_dvd)
   1.130 -  ultimately have "normalize (Gcd (( * ) c ` A)) = normalize (normalize c * Gcd A)"
   1.131 +  ultimately have "normalize (Gcd (( *) c ` A)) = normalize (normalize c * Gcd A)"
   1.132      by (rule associatedI)
   1.133    then show ?thesis
   1.134      by (simp add: normalize_mult)
   1.135 @@ -1035,10 +1030,10 @@
   1.136  
   1.137  lemma Lcm_mult:
   1.138    assumes "A \<noteq> {}"
   1.139 -  shows "Lcm (( * ) c ` A) = normalize c * Lcm A"
   1.140 +  shows "Lcm (( *) c ` A) = normalize c * Lcm A"
   1.141  proof (cases "c = 0")
   1.142    case True
   1.143 -  with assms have "( * ) c ` A = {0}"
   1.144 +  with assms have "( *) c ` A = {0}"
   1.145      by auto
   1.146    with True show ?thesis by auto
   1.147  next
   1.148 @@ -1047,23 +1042,23 @@
   1.149      by blast
   1.150    have "c dvd c * x"
   1.151      by simp
   1.152 -  also from x have "c * x dvd Lcm (( * ) c ` A)"
   1.153 +  also from x have "c * x dvd Lcm (( *) c ` A)"
   1.154      by (intro dvd_Lcm) auto
   1.155 -  finally have dvd: "c dvd Lcm (( * ) c ` A)" .
   1.156 -
   1.157 -  have "Lcm A dvd Lcm (( * ) c ` A) div c"
   1.158 +  finally have dvd: "c dvd Lcm (( *) c ` A)" .
   1.159 +
   1.160 +  have "Lcm A dvd Lcm (( *) c ` A) div c"
   1.161      by (intro Lcm_least dvd_mult_imp_div)
   1.162        (auto intro!: Lcm_least dvd_Lcm simp: mult.commute[of _ c])
   1.163 -  then have "c * Lcm A dvd Lcm (( * ) c ` A)"
   1.164 +  then have "c * Lcm A dvd Lcm (( *) c ` A)"
   1.165      by (subst (asm) dvd_div_iff_mult) (auto intro!: Lcm_least simp: mult_ac dvd)
   1.166    also have "c * Lcm A = (normalize c * Lcm A) * unit_factor c"
   1.167      by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
   1.168 -  also have "\<dots> dvd Lcm (( * ) c ` A) \<longleftrightarrow> normalize c * Lcm A dvd Lcm (( * ) c ` A)"
   1.169 +  also have "\<dots> dvd Lcm (( *) c ` A) \<longleftrightarrow> normalize c * Lcm A dvd Lcm (( *) c ` A)"
   1.170      by (simp add: mult_unit_dvd_iff)
   1.171 -  finally have "normalize c * Lcm A dvd Lcm (( * ) c ` A)" .
   1.172 -  moreover have "Lcm (( * ) c ` A) dvd normalize c * Lcm A"
   1.173 +  finally have "normalize c * Lcm A dvd Lcm (( *) c ` A)" .
   1.174 +  moreover have "Lcm (( *) c ` A) dvd normalize c * Lcm A"
   1.175      by (intro Lcm_least) (auto intro: mult_dvd_mono dvd_Lcm)
   1.176 -  ultimately have "normalize (normalize c * Lcm A) = normalize (Lcm (( * ) c ` A))"
   1.177 +  ultimately have "normalize (normalize c * Lcm A) = normalize (Lcm (( *) c ` A))"
   1.178      by (rule associatedI)
   1.179    then show ?thesis
   1.180      by (simp add: normalize_mult)
   1.181 @@ -1240,7 +1235,7 @@
   1.182  
   1.183  lemma Lcm_fin_0_iff:
   1.184    "Lcm\<^sub>f\<^sub>i\<^sub>n A = 0 \<longleftrightarrow> 0 \<in> A" if "finite A"
   1.185 -  using that by (induct A) (auto simp add: lcm_eq_0_iff)
   1.186 +  using that by (induct A) (auto simp: lcm_eq_0_iff)
   1.187  
   1.188  lemma Lcm_fin_1_iff:
   1.189    "Lcm\<^sub>f\<^sub>i\<^sub>n A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a) \<and> finite A"
   1.190 @@ -1452,7 +1447,7 @@
   1.191    from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
   1.192      by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
   1.193    then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   1.194 -    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   1.195 +    by (auto simp: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   1.196    have "?g \<noteq> 0"
   1.197      using assms by simp
   1.198    moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   1.199 @@ -1480,11 +1475,12 @@
   1.200  lemma gcd_coprime_exists:
   1.201    assumes "gcd a b \<noteq> 0"
   1.202    shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   1.203 -  apply (rule_tac x = "a div gcd a b" in exI)
   1.204 -  apply (rule_tac x = "b div gcd a b" in exI)
   1.205 -  using assms
   1.206 -  apply (auto intro: div_gcd_coprime)
   1.207 -  done
   1.208 +proof -
   1.209 +  have "coprime (a div gcd a b) (b div gcd a b)"
   1.210 +    using assms div_gcd_coprime by auto
   1.211 +  then show ?thesis
   1.212 +    by force
   1.213 +qed
   1.214  
   1.215  lemma pow_divides_pow_iff [simp]:
   1.216    "a ^ n dvd b ^ n \<longleftrightarrow> a dvd b" if "n > 0"
   1.217 @@ -1628,7 +1624,7 @@
   1.218      by simp
   1.219    also note gcd_mult_distrib
   1.220    also have "unit_factor (gcd a b ^ n) = 1"
   1.221 -    using False by (auto simp add: unit_factor_power unit_factor_gcd)
   1.222 +    using False by (auto simp: unit_factor_power unit_factor_gcd)
   1.223    also have "(gcd a b) ^ n * (a div gcd a b) ^ n = a ^ n"
   1.224      by (simp add: ac_simps div_power dvd_power_same)
   1.225    also have "(gcd a b) ^ n * (b div gcd a b) ^ n = b ^ n"
   1.226 @@ -1809,16 +1805,16 @@
   1.227    for i j :: int
   1.228    by (simp only: lcm_int_def)
   1.229  
   1.230 -lemma gcd_nat_induct:
   1.231 +lemma gcd_nat_induct [case_names base step]:
   1.232    fixes m n :: nat
   1.233    assumes "\<And>m. P m 0"
   1.234      and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
   1.235    shows "P m n"
   1.236 -  apply (rule gcd_nat.induct)
   1.237 -  apply (case_tac "y = 0")
   1.238 -  using assms
   1.239 -   apply simp_all
   1.240 -  done
   1.241 +proof (induction m n rule: gcd_nat.induct)
   1.242 +  case (1 x y)
   1.243 +  then show ?case
   1.244 +    using assms neq0_conv by blast
   1.245 +qed
   1.246  
   1.247  lemma gcd_neg1_int [simp]: "gcd (- x) y = gcd x y"
   1.248    for x y :: int
   1.249 @@ -1856,7 +1852,7 @@
   1.250      and "x \<le> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (lcm (- x) y)"
   1.251      and "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (lcm (- x) (- y))"
   1.252    shows "P (lcm x y)"
   1.253 -  using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith
   1.254 +  using assms by (auto simp: lcm_neg1_int lcm_neg2_int) arith
   1.255  
   1.256  lemma lcm_ge_0_int [simp]: "lcm x y \<ge> 0"
   1.257    for x y :: int
   1.258 @@ -1907,7 +1903,7 @@
   1.259  
   1.260  lemma gcd_idem_int: "gcd x x = \<bar>x\<bar>"
   1.261    for x :: int
   1.262 -  by (auto simp add: gcd_int_def)
   1.263 +  by (auto simp: gcd_int_def)
   1.264  
   1.265  declare gcd_nat.simps [simp del]
   1.266  
   1.267 @@ -1921,13 +1917,10 @@
   1.268    fix m n :: nat
   1.269    show "gcd m n dvd m" and "gcd m n dvd n"
   1.270    proof (induct m n rule: gcd_nat_induct)
   1.271 -    fix m n :: nat
   1.272 -    assume "gcd n (m mod n) dvd m mod n"
   1.273 -      and "gcd n (m mod n) dvd n"
   1.274 +    case (step m n)
   1.275      then have "gcd n (m mod n) dvd m"
   1.276 -      by (rule dvd_mod_imp_dvd)
   1.277 -    moreover assume "0 < n"
   1.278 -    ultimately show "gcd m n dvd m"
   1.279 +      by (metis dvd_mod_imp_dvd)
   1.280 +    with step show "gcd m n dvd m"
   1.281        by (simp add: gcd_non_0_nat)
   1.282    qed (simp_all add: gcd_0_nat gcd_non_0_nat)
   1.283  next
   1.284 @@ -1979,25 +1972,16 @@
   1.285  
   1.286  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"
   1.287    for d a :: nat
   1.288 -  apply auto
   1.289 -  apply (rule dvd_antisym)
   1.290 -   apply (erule (1) gcd_greatest)
   1.291 -  apply auto
   1.292 -  done
   1.293 +  using gcd_unique by fastforce
   1.294  
   1.295  lemma gcd_unique_int:
   1.296    "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"
   1.297    for d a :: int
   1.298 -  apply (cases "d = 0")
   1.299 -   apply simp
   1.300 -  apply (rule iffI)
   1.301 -   apply (rule zdvd_antisym_nonneg)
   1.302 -      apply (auto intro: gcd_greatest)
   1.303 -  done
   1.304 +  using zdvd_antisym_nonneg by auto
   1.305  
   1.306  interpretation gcd_nat:
   1.307    semilattice_neutr_order gcd "0::nat" Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n"
   1.308 -  by standard (auto simp add: gcd_unique_nat [symmetric] intro: dvd_antisym dvd_trans)
   1.309 +  by standard (auto simp: gcd_unique_nat [symmetric] intro: dvd_antisym dvd_trans)
   1.310  
   1.311  lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd x y = \<bar>x\<bar>"
   1.312    for x y :: int
   1.313 @@ -2013,11 +1997,11 @@
   1.314  lemma gcd_mult_distrib_nat: "k * gcd m n = gcd (k * m) (k * n)"
   1.315    for k m n :: nat
   1.316    \<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close>
   1.317 -  apply (induct m n rule: gcd_nat_induct)
   1.318 -   apply simp
   1.319 -  apply (cases "k = 0")
   1.320 -   apply (simp_all add: gcd_non_0_nat)
   1.321 -  done
   1.322 +proof (induct m n rule: gcd_nat_induct)
   1.323 +  case (step m n)
   1.324 +  then show ?case
   1.325 +    by (metis gcd_mult_distrib' gcd_red_nat)
   1.326 +qed auto
   1.327  
   1.328  lemma gcd_mult_distrib_int: "\<bar>k\<bar> * gcd m n = gcd (k * m) (k * n)"
   1.329    for k m n :: int
   1.330 @@ -2033,34 +2017,49 @@
   1.331  
   1.332  lemma gcd_diff2_nat: "n \<ge> m \<Longrightarrow> gcd (n - m) n = gcd m n"
   1.333    for m n :: nat
   1.334 -  apply (subst gcd.commute)
   1.335 -  apply (subst gcd_diff1_nat [symmetric])
   1.336 -   apply auto
   1.337 -  apply (subst gcd.commute)
   1.338 -  apply (subst gcd_diff1_nat)
   1.339 -   apply assumption
   1.340 -  apply (rule gcd.commute)
   1.341 -  done
   1.342 -
   1.343 -lemma gcd_non_0_int: "y > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
   1.344 -  for x y :: int
   1.345 -  apply (frule_tac b = y and a = x in pos_mod_sign)
   1.346 -  apply (simp del: Euclidean_Division.pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
   1.347 -  apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
   1.348 -  apply (frule_tac a = x in pos_mod_bound)
   1.349 -  apply (subst (1 2) gcd.commute)
   1.350 -  apply (simp del: Euclidean_Division.pos_mod_bound add: nat_diff_distrib gcd_diff2_nat nat_le_eq_zle)
   1.351 -  done
   1.352 +  by (metis gcd.commute gcd_add2 gcd_diff1_nat le_add_diff_inverse2)
   1.353 +
   1.354 +lemma gcd_non_0_int: 
   1.355 +  fixes x y :: int
   1.356 +  assumes "y > 0" shows "gcd x y = gcd y (x mod y)"
   1.357 +proof (cases "x mod y = 0")
   1.358 +  case False
   1.359 +  then have neg: "x mod y = y - (- x) mod y"
   1.360 +    by (simp add: zmod_zminus1_eq_if)
   1.361 +  have xy: "0 \<le> x mod y" 
   1.362 +    by (simp add: assms)
   1.363 +  show ?thesis
   1.364 +  proof (cases "x < 0")
   1.365 +    case True
   1.366 +    have "nat (- x mod y) \<le> nat y"
   1.367 +      by (simp add: assms dual_order.order_iff_strict)
   1.368 +    moreover have "gcd (nat (- x)) (nat y) = gcd (nat (- x mod y)) (nat y)"
   1.369 +      using True assms gcd_non_0_nat nat_mod_distrib by auto
   1.370 +    ultimately have "gcd (nat (- x)) (nat y) = gcd (nat y) (nat (x mod y))"
   1.371 +      using assms 
   1.372 +      by (simp add: neg nat_diff_distrib') (metis gcd.commute gcd_diff2_nat)
   1.373 +    with assms \<open>0 \<le> x mod y\<close> show ?thesis
   1.374 +      by (simp add: True dual_order.order_iff_strict gcd_int_def)
   1.375 +  next
   1.376 +    case False
   1.377 +    with assms xy have "gcd (nat x) (nat y) = gcd (nat y) (nat x mod nat y)"
   1.378 +      using gcd_red_nat by blast
   1.379 +    with False assms show ?thesis
   1.380 +      by (simp add: gcd_int_def nat_mod_distrib)
   1.381 +  qed
   1.382 +qed (use assms in auto)
   1.383  
   1.384  lemma gcd_red_int: "gcd x y = gcd y (x mod y)"
   1.385    for x y :: int
   1.386 -  apply (cases "y = 0")
   1.387 -   apply force
   1.388 -  apply (cases "y > 0")
   1.389 -   apply (subst gcd_non_0_int, auto)
   1.390 -  apply (insert gcd_non_0_int [of "- y" "- x"])
   1.391 -  apply auto
   1.392 -  done
   1.393 +proof (cases y "0::int" rule: linorder_cases)
   1.394 +  case less
   1.395 +  with gcd_non_0_int [of "- y" "- x"] show ?thesis
   1.396 +    by auto
   1.397 +next
   1.398 +  case greater
   1.399 +  with gcd_non_0_int [of y x] show ?thesis
   1.400 +    by auto
   1.401 +qed auto
   1.402  
   1.403  (* TODO: differences, and all variations of addition rules
   1.404      as simplification rules for nat and int *)
   1.405 @@ -2092,34 +2091,34 @@
   1.406  qed
   1.407  
   1.408  lemma Max_divisors_self_nat [simp]: "n \<noteq> 0 \<Longrightarrow> Max {d::nat. d dvd n} = n"
   1.409 -  apply (rule antisym)
   1.410 -   apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
   1.411 -  apply simp
   1.412 -  done
   1.413 -
   1.414 -lemma Max_divisors_self_int [simp]: "n \<noteq> 0 \<Longrightarrow> Max {d::int. d dvd n} = \<bar>n\<bar>"
   1.415 -  apply (rule antisym)
   1.416 -   apply (rule Max_le_iff [THEN iffD2])
   1.417 -     apply (auto intro: abs_le_D1 dvd_imp_le_int)
   1.418 -  done
   1.419 -
   1.420 -lemma gcd_is_Max_divisors_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> gcd m n = Max {d. d dvd m \<and> d dvd n}"
   1.421 -  for m n :: nat
   1.422 -  apply (rule Max_eqI[THEN sym])
   1.423 -    apply (metis finite_Collect_conjI finite_divisors_nat)
   1.424 -   apply simp
   1.425 -   apply (metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff gcd_pos_nat)
   1.426 -  apply simp
   1.427 -  done
   1.428 -
   1.429 -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}"
   1.430 -  for m n :: int
   1.431 -  apply (rule Max_eqI[THEN sym])
   1.432 -    apply (metis finite_Collect_conjI finite_divisors_int)
   1.433 -   apply simp
   1.434 -   apply (metis gcd_greatest_iff gcd_pos_int zdvd_imp_le)
   1.435 -  apply simp
   1.436 -  done
   1.437 +  by (fastforce intro: antisym Max_le_iff[THEN iffD2] simp: dvd_imp_le)
   1.438 +
   1.439 +lemma Max_divisors_self_int [simp]: 
   1.440 +  assumes "n \<noteq> 0" shows "Max {d::int. d dvd n} = \<bar>n\<bar>"
   1.441 +proof (rule antisym)
   1.442 +  show "Max {d. d dvd n} \<le> \<bar>n\<bar>"
   1.443 +    using assms by (auto intro: abs_le_D1 dvd_imp_le_int intro!: Max_le_iff [THEN iffD2])
   1.444 +qed (simp add: assms)
   1.445 +
   1.446 +lemma gcd_is_Max_divisors_nat:
   1.447 +  fixes m n :: nat
   1.448 +  assumes "n > 0" shows "gcd m n = Max {d. d dvd m \<and> d dvd n}"
   1.449 +proof (rule Max_eqI[THEN sym], simp_all)
   1.450 +  show "finite {d. d dvd m \<and> d dvd n}"
   1.451 +    by (simp add: \<open>n > 0\<close>)
   1.452 +  show "\<And>y. y dvd m \<and> y dvd n \<Longrightarrow> y \<le> gcd m n"
   1.453 +    by (simp add: \<open>n > 0\<close> dvd_imp_le)
   1.454 +qed
   1.455 +
   1.456 +lemma gcd_is_Max_divisors_int:
   1.457 +  fixes m n :: int
   1.458 +  assumes "n \<noteq> 0" shows "gcd m n = Max {d. d dvd m \<and> d dvd n}"
   1.459 +proof (rule Max_eqI[THEN sym], simp_all)
   1.460 +  show "finite {d. d dvd m \<and> d dvd n}"
   1.461 +    by (simp add: \<open>n \<noteq> 0\<close>)
   1.462 +  show "\<And>y. y dvd m \<and> y dvd n \<Longrightarrow> y \<le> gcd m n"
   1.463 +    by (simp add: \<open>n \<noteq> 0\<close> zdvd_imp_le)
   1.464 +qed
   1.465  
   1.466  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>"
   1.467    for k l :: int
   1.468 @@ -2178,25 +2177,22 @@
   1.469  
   1.470  declare bezw.simps [simp del]
   1.471  
   1.472 -lemma bezw_aux: "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
   1.473 +
   1.474 +lemma bezw_aux: "int (gcd x y) = fst (bezw x y) * int x + snd (bezw x y) * int y"
   1.475  proof (induct x y rule: gcd_nat_induct)
   1.476 -  fix m :: nat
   1.477 -  show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
   1.478 -    by auto
   1.479 -next
   1.480 -  fix m n :: nat
   1.481 -  assume ngt0: "n > 0"
   1.482 -    and ih: "fst (bezw n (m mod n)) * int n + snd (bezw n (m mod n)) * int (m mod n) =
   1.483 -      int (gcd n (m mod n))"
   1.484 -  then show "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
   1.485 -    apply (simp add: bezw_non_0 gcd_non_0_nat)
   1.486 -    apply (erule subst)
   1.487 -    apply (simp add: field_simps)
   1.488 -    apply (subst div_mult_mod_eq [of m n, symmetric])
   1.489 -      (* applying simp here undoes the last substitution! what is procedure cancel_div_mod? *)
   1.490 -    apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult)
   1.491 -    done
   1.492 -qed
   1.493 +  case (step m n)
   1.494 +  then have "fst (bezw m n) * int m + snd (bezw m n) * int n - int (gcd m n) 
   1.495 +             = int m * snd (bezw n (m mod n)) -
   1.496 +               (int (m mod n) * snd (bezw n (m mod n)) + int n * (int (m div n) * snd (bezw n (m mod n))))"
   1.497 +    by (simp add: bezw_non_0 gcd_non_0_nat field_simps)
   1.498 +  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))"
   1.499 +    by (simp add: distrib_right)
   1.500 +  also have "\<dots> = 0"
   1.501 +    by (metis cancel_comm_monoid_add_class.diff_cancel mod_mult_div_eq of_nat_add)
   1.502 +  finally show ?case
   1.503 +    by simp
   1.504 +qed auto
   1.505 +
   1.506  
   1.507  lemma bezout_int: "\<exists>u v. u * x + v * y = gcd x y"
   1.508    for x y :: int
   1.509 @@ -2204,13 +2200,9 @@
   1.510    have aux: "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> \<exists>u v. u * x + v * y = gcd x y" for x y :: int
   1.511      apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
   1.512      apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
   1.513 -    apply (unfold gcd_int_def)
   1.514 -    apply simp
   1.515 -    apply (subst bezw_aux [symmetric])
   1.516 -    apply auto
   1.517 -    done
   1.518 +    by (simp add: bezw_aux gcd_int_def)
   1.519    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"
   1.520 -    by atomize_elim auto
   1.521 +    using linear by blast
   1.522    then show ?thesis
   1.523    proof cases
   1.524      case 1
   1.525 @@ -2218,48 +2210,29 @@
   1.526    next
   1.527      case 2
   1.528      then show ?thesis
   1.529 -      apply -
   1.530 -      apply (insert aux [of x "-y"])
   1.531 -      apply auto
   1.532 -      apply (rule_tac x = u in exI)
   1.533 -      apply (rule_tac x = "-v" in exI)
   1.534 -      apply (subst gcd_neg2_int [symmetric])
   1.535 -      apply auto
   1.536 -      done
   1.537 +      using aux [of x "-y"]
   1.538 +      by (metis gcd_neg2_int mult.commute mult_minus_right neg_0_le_iff_le)
   1.539    next
   1.540      case 3
   1.541      then show ?thesis
   1.542 -      apply -
   1.543 -      apply (insert aux [of "-x" y])
   1.544 -      apply auto
   1.545 -      apply (rule_tac x = "-u" in exI)
   1.546 -      apply (rule_tac x = v in exI)
   1.547 -      apply (subst gcd_neg1_int [symmetric])
   1.548 -      apply auto
   1.549 -      done
   1.550 +      using aux [of "-x" y]
   1.551 +      by (metis gcd.commute gcd_neg2_int mult.commute mult_minus_right neg_0_le_iff_le)
   1.552    next
   1.553      case 4
   1.554      then show ?thesis
   1.555 -      apply -
   1.556 -      apply (insert aux [of "-x" "-y"])
   1.557 -      apply auto
   1.558 -      apply (rule_tac x = "-u" in exI)
   1.559 -      apply (rule_tac x = "-v" in exI)
   1.560 -      apply (subst gcd_neg1_int [symmetric])
   1.561 -      apply (subst gcd_neg2_int [symmetric])
   1.562 -      apply auto
   1.563 -      done
   1.564 +      using aux [of "-x" "-y"]
   1.565 +      by (metis diff_0 diff_ge_0_iff_ge gcd_neg1_int gcd_neg2_int mult.commute mult_minus_right)
   1.566    qed
   1.567  qed
   1.568  
   1.569  
   1.570  text \<open>Versions of Bezout for \<open>nat\<close>, by Amine Chaieb.\<close>
   1.571  
   1.572 -lemma ind_euclid:
   1.573 +lemma Euclid_induct [case_names swap zero add]:
   1.574    fixes P :: "nat \<Rightarrow> nat \<Rightarrow> bool"
   1.575 -  assumes c: " \<forall>a b. P a b \<longleftrightarrow> P b a"
   1.576 -    and z: "\<forall>a. P a 0"
   1.577 -    and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
   1.578 +  assumes c: "\<And>a b. P a b \<longleftrightarrow> P b a"
   1.579 +    and z: "\<And>a. P a 0"
   1.580 +    and add: "\<And>a b. P a b \<longrightarrow> P a (a + b)"
   1.581    shows "P a b"
   1.582  proof (induct "a + b" arbitrary: a b rule: less_induct)
   1.583    case less
   1.584 @@ -2302,53 +2275,32 @@
   1.585  qed
   1.586  
   1.587  lemma bezout_lemma_nat:
   1.588 -  assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
   1.589 -    (a * x = b * y + d \<or> b * x = a * y + d)"
   1.590 -  shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
   1.591 -    (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
   1.592 -  using ex
   1.593 -  apply clarsimp
   1.594 -  apply (rule_tac x="d" in exI)
   1.595 -  apply simp
   1.596 -  apply (case_tac "a * x = b * y + d")
   1.597 -   apply simp_all
   1.598 -   apply (rule_tac x="x + y" in exI)
   1.599 -   apply (rule_tac x="y" in exI)
   1.600 -   apply algebra
   1.601 -  apply (rule_tac x="x" in exI)
   1.602 -  apply (rule_tac x="x + y" in exI)
   1.603 -  apply algebra
   1.604 -  done
   1.605 -
   1.606 -lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
   1.607 -    (a * x = b * y + d \<or> b * x = a * y + d)"
   1.608 -  apply (induct a b rule: ind_euclid)
   1.609 -    apply blast
   1.610 -   apply clarify
   1.611 -   apply (rule_tac x="a" in exI)
   1.612 -   apply simp
   1.613 -  apply clarsimp
   1.614 -  apply (rule_tac x="d" in exI)
   1.615 -  apply (case_tac "a * x = b * y + d")
   1.616 -   apply simp_all
   1.617 -   apply (rule_tac x="x+y" in exI)
   1.618 -   apply (rule_tac x="y" in exI)
   1.619 -   apply algebra
   1.620 -  apply (rule_tac x="x" in exI)
   1.621 -  apply (rule_tac x="x+y" in exI)
   1.622 -  apply algebra
   1.623 -  done
   1.624 -
   1.625 -lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
   1.626 -    (a * x - b * y = d \<or> b * x - a * y = d)"
   1.627 -  using bezout_add_nat[of a b]
   1.628 -  apply clarsimp
   1.629 -  apply (rule_tac x="d" in exI)
   1.630 -  apply simp
   1.631 -  apply (rule_tac x="x" in exI)
   1.632 -  apply (rule_tac x="y" in exI)
   1.633 +  fixes d::nat
   1.634 +  shows "\<lbrakk>d dvd a; d dvd b; a * x = b * y + d \<or> b * x = a * y + d\<rbrakk>
   1.635 +    \<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)"
   1.636    apply auto
   1.637 -  done
   1.638 +  apply (metis add_mult_distrib2 left_add_mult_distrib)
   1.639 +  apply (rule_tac x=x in exI)
   1.640 +  by (metis add_mult_distrib2 mult.commute add.assoc)
   1.641 +
   1.642 +lemma bezout_add_nat: 
   1.643 +  "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> (a * x = b * y + d \<or> b * x = a * y + d)"
   1.644 +proof (induct a b rule: Euclid_induct)
   1.645 +  case (swap a b)
   1.646 +  then show ?case
   1.647 +    by blast
   1.648 +next
   1.649 +  case (zero a)
   1.650 +  then show ?case
   1.651 +    by fastforce    
   1.652 +next
   1.653 +  case (add a b)
   1.654 +  then show ?case
   1.655 +    by (meson bezout_lemma_nat)
   1.656 +qed
   1.657 +
   1.658 +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)"
   1.659 +  using bezout_add_nat[of a b]  by (metis add_diff_cancel_left')
   1.660  
   1.661  lemma bezout_add_strong_nat:
   1.662    fixes a b :: nat
   1.663 @@ -2356,7 +2308,7 @@
   1.664    shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
   1.665  proof -
   1.666    consider d x y where "d dvd a" "d dvd b" "a * x = b * y + d"
   1.667 -    | d x y where "d dvd a" "d dvd b" "b * x = a * y + d"
   1.668 +         | d x y where "d dvd a" "d dvd b" "b * x = a * y + d"
   1.669      using bezout_add_nat [of a b] by blast
   1.670    then show ?thesis
   1.671    proof cases
   1.672 @@ -2377,13 +2329,7 @@
   1.673        proof cases
   1.674          case 1
   1.675          with a H show ?thesis
   1.676 -          apply simp
   1.677 -          apply (rule exI[where x = b])
   1.678 -          apply simp
   1.679 -          apply (rule exI[where x = b])
   1.680 -          apply (rule exI[where x = "a - 1"])
   1.681 -          apply (simp add: diff_mult_distrib2)
   1.682 -          done
   1.683 +          by (metis Suc_pred add.commute mult.commute mult_Suc_right neq0_conv)
   1.684        next
   1.685          case 2
   1.686          show ?thesis
   1.687 @@ -2410,13 +2356,7 @@
   1.688            then have "a * ((b - 1) * y) = b * (x * (b - 1) - d) + d"
   1.689              by (simp only: diff_mult_distrib2 ac_simps)
   1.690            with H(1,2) show ?thesis
   1.691 -            apply -
   1.692 -            apply (rule exI [where x = d])
   1.693 -            apply simp
   1.694 -            apply (rule exI [where x = "(b - 1) * y"])
   1.695 -            apply (rule exI [where x = "x * (b - 1) - d"])
   1.696 -            apply simp
   1.697 -            done
   1.698 +            by blast
   1.699          qed
   1.700        qed
   1.701      qed
   1.702 @@ -2451,17 +2391,11 @@
   1.703    
   1.704  lemma prod_gcd_lcm_nat: "m * n = gcd m n * lcm m n"
   1.705    for m n :: nat
   1.706 -  unfolding lcm_nat_def
   1.707 -  by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod])
   1.708 +  by simp
   1.709  
   1.710  lemma prod_gcd_lcm_int: "\<bar>m\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
   1.711    for m n :: int
   1.712 -  unfolding lcm_int_def gcd_int_def
   1.713 -  apply (subst of_nat_mult [symmetric])
   1.714 -  apply (subst prod_gcd_lcm_nat [symmetric])
   1.715 -  apply (subst nat_abs_mult_distrib [symmetric])
   1.716 -  apply (simp add: abs_mult)
   1.717 -  done
   1.718 +  by simp
   1.719  
   1.720  lemma lcm_pos_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> lcm m n > 0"
   1.721    for m n :: nat
   1.722 @@ -2473,7 +2407,7 @@
   1.723  
   1.724  lemma dvd_pos_nat: "n > 0 \<Longrightarrow> m dvd n \<Longrightarrow> m > 0"  (* FIXME move *)
   1.725    for m n :: nat
   1.726 -  by (cases m) auto
   1.727 +  by auto
   1.728  
   1.729  lemma lcm_unique_nat:
   1.730    "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"
   1.731 @@ -2487,17 +2421,11 @@
   1.732  
   1.733  lemma lcm_proj2_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> lcm x y = y"
   1.734    for x y :: nat
   1.735 -  apply (rule sym)
   1.736 -  apply (subst lcm_unique_nat [symmetric])
   1.737 -  apply auto
   1.738 -  done
   1.739 +  by (simp add: lcm_proj2_if_dvd)
   1.740  
   1.741  lemma lcm_proj2_if_dvd_int [simp]: "x dvd y \<Longrightarrow> lcm x y = \<bar>y\<bar>"
   1.742    for x y :: int
   1.743 -  apply (rule sym)
   1.744 -  apply (subst lcm_unique_int [symmetric])
   1.745 -  apply auto
   1.746 -  done
   1.747 +  by (simp add: lcm_proj2_if_dvd)
   1.748  
   1.749  lemma lcm_proj1_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> lcm y x = y"
   1.750    for x y :: nat
   1.751 @@ -2551,7 +2479,7 @@
   1.752    by (simp add: Lcm_nat_def del: One_nat_def)
   1.753  
   1.754  lemma Lcm_nat_insert: "Lcm (insert n M) = lcm n (Lcm M)" for n :: nat
   1.755 -  by (cases "finite M") (auto simp add: Lcm_nat_def simp del: One_nat_def)
   1.756 +  by (cases "finite M") (auto simp: Lcm_nat_def simp del: One_nat_def)
   1.757  
   1.758  lemma Lcm_nat_infinite: "infinite M \<Longrightarrow> Lcm M = 0" for M :: "nat set"
   1.759    by (simp add: Lcm_nat_def)
   1.760 @@ -2595,9 +2523,9 @@
   1.761    fix N :: "nat set"
   1.762    fix n :: nat
   1.763    show "Gcd N dvd n" if "n \<in> N"
   1.764 -    using that by (induct N rule: infinite_finite_induct) (auto simp add: Gcd_nat_def)
   1.765 +    using that by (induct N rule: infinite_finite_induct) (auto simp: Gcd_nat_def)
   1.766    show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m"
   1.767 -    using that by (induct N rule: infinite_finite_induct) (auto simp add: Gcd_nat_def)
   1.768 +    using that by (induct N rule: infinite_finite_induct) (auto simp: Gcd_nat_def)
   1.769    show "n dvd Lcm N" if "n \<in> N"
   1.770      using that by (induct N rule: infinite_finite_induct) auto
   1.771    show "Lcm N dvd n" if "\<And>m. m \<in> N \<Longrightarrow> m dvd n"
   1.772 @@ -2629,52 +2557,51 @@
   1.773    from fin show "Gcd M \<le> Max (\<Inter>m\<in>M. {d. d dvd m})"
   1.774      by (auto intro: Max_ge Gcd_dvd)
   1.775    from fin show "Max (\<Inter>m\<in>M. {d. d dvd m}) \<le> Gcd M"
   1.776 -    apply (rule Max.boundedI)
   1.777 -     apply auto
   1.778 -    apply (meson Gcd_dvd Gcd_greatest \<open>0 < m\<close> \<open>m \<in> M\<close> dvd_imp_le dvd_pos_nat)
   1.779 -    done
   1.780 +  proof (rule Max.boundedI, simp_all)
   1.781 +    show "(\<Inter>m\<in>M. {d. d dvd m}) \<noteq> {}"
   1.782 +      by auto
   1.783 +    show "\<And>a. \<forall>x\<in>M. a dvd x \<Longrightarrow> a \<le> Gcd M"
   1.784 +      by (meson Gcd_dvd Gcd_greatest \<open>0 < m\<close> \<open>m \<in> M\<close> dvd_imp_le dvd_pos_nat)
   1.785 +  qed
   1.786  qed
   1.787  
   1.788  lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0})"
   1.789    for M :: "nat set"
   1.790 -  apply (induct pred: finite)
   1.791 -   apply simp
   1.792 -  apply (case_tac "x = 0")
   1.793 -   apply simp
   1.794 -  apply (subgoal_tac "insert x F - {0} = insert x (F - {0})")
   1.795 -   apply simp
   1.796 -  apply blast
   1.797 -  done
   1.798 +proof (induct pred: finite)
   1.799 +  case (insert x M)
   1.800 +  then show ?case
   1.801 +    by (simp add: insert_Diff_if)
   1.802 +qed auto
   1.803  
   1.804  lemma Lcm_in_lcm_closed_set_nat:
   1.805 -  "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"
   1.806 -  for M :: "nat set"
   1.807 -  apply (induct rule: finite_linorder_min_induct)
   1.808 -   apply simp
   1.809 -  apply simp
   1.810 -  apply (subgoal_tac "\<forall>m n. m \<in> A \<longrightarrow> n \<in> A \<longrightarrow> lcm m n \<in> A")
   1.811 -   apply simp
   1.812 -   apply(case_tac "A = {}")
   1.813 -    apply simp
   1.814 -   apply simp
   1.815 -  apply (metis lcm_pos_nat lcm_unique_nat linorder_neq_iff nat_dvd_not_less not_less0)
   1.816 -  done
   1.817 +  fixes M :: "nat set" 
   1.818 +  assumes "finite M" "M \<noteq> {}" "\<And>m n. \<lbrakk>m \<in> M; n \<in> M\<rbrakk> \<Longrightarrow> lcm m n \<in> M"
   1.819 +  shows "Lcm M \<in> M"
   1.820 +  using assms
   1.821 +proof (induction M rule: finite_linorder_min_induct)
   1.822 +  case (insert x M)
   1.823 +  then have "\<And>m n. m \<in> M \<Longrightarrow> n \<in> M \<Longrightarrow> lcm m n \<in> M"
   1.824 +    by (metis dvd_lcm1 gr0I insert_iff lcm_pos_nat nat_dvd_not_less)
   1.825 +  with insert show ?case
   1.826 +    by simp (metis Lcm_nat_empty One_nat_def dvd_1_left dvd_lcm2)
   1.827 +qed auto
   1.828  
   1.829  lemma Lcm_eq_Max_nat:
   1.830 -  "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"
   1.831 -  for M :: "nat set"
   1.832 -  apply (rule antisym)
   1.833 -   apply (rule Max_ge)
   1.834 -    apply assumption
   1.835 -   apply (erule (2) Lcm_in_lcm_closed_set_nat)
   1.836 -  apply (auto simp add: not_le Lcm_0_iff dvd_imp_le leD le_neq_trans)
   1.837 -  done
   1.838 +  fixes M :: "nat set" 
   1.839 +  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"
   1.840 +  shows "Lcm M = Max M"
   1.841 +proof (rule antisym)
   1.842 +  show "Lcm M \<le> Max M"
   1.843 +    by (simp add: Lcm_in_lcm_closed_set_nat \<open>finite M\<close> \<open>M \<noteq> {}\<close> lcm)
   1.844 +  show "Max M \<le> Lcm M"
   1.845 +    by (meson Lcm_0_iff Max_in M dvd_Lcm dvd_imp_le le_0_eq not_le)
   1.846 +qed
   1.847  
   1.848  lemma mult_inj_if_coprime_nat:
   1.849 -  "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> \<forall>a\<in>A. \<forall>b\<in>B. coprime (f a) (g b) \<Longrightarrow>
   1.850 +  "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>
   1.851      inj_on (\<lambda>(a, b). f a * g b) (A \<times> B)"
   1.852    for f :: "'a \<Rightarrow> nat" and g :: "'b \<Rightarrow> nat"
   1.853 -  by (auto simp add: inj_on_def coprime_crossproduct_nat simp del: One_nat_def)
   1.854 +  by (auto simp: inj_on_def coprime_crossproduct_nat simp del: One_nat_def)
   1.855  
   1.856  
   1.857  subsubsection \<open>Setwise GCD and LCM for integers\<close>