src/HOL/Number_Theory/Euclidean_Algorithm.thy
 changeset 60526 fad653acf58f parent 60517 f16e4fb20652 child 60569 f2f1f6860959 child 60580 7e741e22d7fc
1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 19 21:33:03 2015 +0200
1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 19 21:41:33 2015 +0200
1.3 @@ -1,12 +1,12 @@
1.4  (* Author: Manuel Eberl *)
1.6 -section {* Abstract euclidean algorithm *}
1.7 +section \<open>Abstract euclidean algorithm\<close>
1.9  theory Euclidean_Algorithm
1.10  imports Complex_Main
1.11  begin
1.13 -text {*
1.14 +text \<open>
1.15    A Euclidean semiring is a semiring upon which the Euclidean algorithm can be
1.16    implemented. It must provide:
1.17    \begin{itemize}
1.18 @@ -18,7 +18,7 @@
1.19    \end{itemize}
1.20    The existence of these functions makes it possible to derive gcd and lcm functions
1.21    for any Euclidean semiring.
1.22 -*}
1.23 +\<close>
1.24  class euclidean_semiring = semiring_div +
1.25    fixes euclidean_size :: "'a \<Rightarrow> nat"
1.26    fixes normalization_factor :: "'a \<Rightarrow> 'a"
1.27 @@ -60,17 +60,17 @@
1.28  proof (cases "a = 0", simp)
1.29    assume "a \<noteq> 0"
1.30    let ?nf = "normalization_factor"
1.31 -  from normalization_factor_is_unit[OF a \<noteq> 0] have "?nf a \<noteq> 0"
1.32 +  from normalization_factor_is_unit[OF \<open>a \<noteq> 0\<close>] have "?nf a \<noteq> 0"
1.33      by auto
1.34    have "?nf (a div ?nf a) * ?nf (?nf a) = ?nf (a div ?nf a * ?nf a)"
1.35      by (simp add: normalization_factor_mult)
1.36 -  also have "a div ?nf a * ?nf a = a" using a \<noteq> 0
1.37 +  also have "a div ?nf a * ?nf a = a" using \<open>a \<noteq> 0\<close>
1.38      by simp
1.39 -  also have "?nf (?nf a) = ?nf a" using a \<noteq> 0
1.40 +  also have "?nf (?nf a) = ?nf a" using \<open>a \<noteq> 0\<close>
1.41      normalization_factor_is_unit normalization_factor_unit by simp
1.42    finally have "normalization_factor (a div normalization_factor a) = 1"
1.43 -    using ?nf a \<noteq> 0 by (metis div_mult_self2_is_id div_self)
1.44 -  with a \<noteq> 0 show ?thesis by simp
1.45 +    using \<open>?nf a \<noteq> 0\<close> by (metis div_mult_self2_is_id div_self)
1.46 +  with \<open>a \<noteq> 0\<close> show ?thesis by simp
1.47  qed
1.49  lemma normalization_0_iff [simp]:
1.50 @@ -90,7 +90,7 @@
1.51      apply (subst (asm) unit_eq_div1, blast, subst (asm) unit_div_commute, blast)
1.52      apply (subst div_mult_swap, simp, simp)
1.53      done
1.54 -  with a \<noteq> 0 b \<noteq> 0 have "\<exists>c. is_unit c \<and> a = c * b"
1.55 +  with \<open>a \<noteq> 0\<close> \<open>b \<noteq> 0\<close> have "\<exists>c. is_unit c \<and> a = c * b"
1.56      by (intro exI[of _ "?nf a div ?nf b"], force simp: mult_ac)
1.57    then obtain c where "is_unit c" and "a = c * b" by blast
1.58    then show "associated a b" by (rule is_unit_associatedI)
1.59 @@ -99,7 +99,7 @@
1.60    assume "a \<noteq> 0" "b \<noteq> 0" "associated a b"
1.61    then obtain c where "is_unit c" and "a = c * b" by (blast elim: associated_is_unitE)
1.62    then show "a div ?nf a = b div ?nf b"
1.63 -    apply (simp only: a = c * b normalization_factor_mult normalization_factor_unit)
1.64 +    apply (simp only: \<open>a = c * b\<close> normalization_factor_mult normalization_factor_unit)
1.65      apply (rule div_mult_mult1, force)
1.66      done
1.67    qed
1.68 @@ -129,10 +129,10 @@
1.69    assume "b mod a \<noteq> 0"
1.70    from b_dvd_a have b_dvd_mod: "b dvd b mod a" by (simp add: dvd_mod_iff)
1.71    from b_dvd_mod obtain c where "b mod a = b * c" unfolding dvd_def by blast
1.72 -    with b mod a \<noteq> 0 have "c \<noteq> 0" by auto
1.73 -  with b mod a = b * c have "euclidean_size (b mod a) \<ge> euclidean_size b"
1.74 +    with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
1.75 +  with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
1.76        using size_mult_mono by force
1.77 -  moreover from a \<noteq> 0 have "euclidean_size (b mod a) < euclidean_size a"
1.78 +  moreover from \<open>a \<noteq> 0\<close> have "euclidean_size (b mod a) < euclidean_size a"
1.79        using mod_size_less by blast
1.80    ultimately show False using size_eq by simp
1.81  qed
1.82 @@ -272,7 +272,7 @@
1.83      fix l assume "l dvd a" and "l dvd gcd b c"
1.84      with dvd_trans[OF _ gcd_dvd1] and dvd_trans[OF _ gcd_dvd2]
1.85        have "l dvd b" and "l dvd c" by blast+
1.86 -    with l dvd a show "l dvd gcd (gcd a b) c"
1.87 +    with \<open>l dvd a\<close> show "l dvd gcd (gcd a b) c"
1.88        by (intro gcd_greatest)
1.89    qed
1.90  next
1.91 @@ -369,7 +369,7 @@
1.92  proof -
1.93     have "gcd a b dvd a" by (rule gcd_dvd1)
1.94     then obtain c where A: "a = gcd a b * c" unfolding dvd_def by blast
1.95 -   with a \<noteq> 0 show ?thesis by (subst (2) A, intro size_mult_mono) auto
1.96 +   with \<open>a \<noteq> 0\<close> show ?thesis by (subst (2) A, intro size_mult_mono) auto
1.97  qed
1.99  lemma euclidean_size_gcd_le2 [simp]:
1.100 @@ -381,11 +381,11 @@
1.101    shows "euclidean_size (gcd a b) < euclidean_size a"
1.102  proof (rule ccontr)
1.103    assume "\<not>euclidean_size (gcd a b) < euclidean_size a"
1.104 -  with a \<noteq> 0 have "euclidean_size (gcd a b) = euclidean_size a"
1.105 +  with \<open>a \<noteq> 0\<close> have "euclidean_size (gcd a b) = euclidean_size a"
1.106      by (intro le_antisym, simp_all)
1.107    with assms have "a dvd gcd a b" by (auto intro: dvd_euclidean_size_eq_imp_dvd)
1.108    hence "a dvd b" using dvd_gcd_D2 by blast
1.109 -  with \<not>a dvd b show False by contradiction
1.110 +  with \<open>\<not>a dvd b\<close> show False by contradiction
1.111  qed
1.113  lemma euclidean_size_gcd_less2:
1.114 @@ -445,7 +445,7 @@
1.115    let ?nf = "normalization_factor"
1.116    from assms gcd_mult_distrib [of a c b]
1.117      have A: "a = gcd (a * c) (a * b) * ?nf a" by simp
1.118 -  from c dvd a * b show ?thesis by (subst A, simp_all add: gcd_greatest)
1.119 +  from \<open>c dvd a * b\<close> show ?thesis by (subst A, simp_all add: gcd_greatest)
1.120  qed
1.122  lemma coprime_dvd_mult_iff:
1.123 @@ -472,7 +472,7 @@
1.124    shows "gcd (k * m) n = gcd m n"
1.125  proof (rule gcd_dvd_antisym)
1.126    have "gcd (gcd (k * m) n) k = gcd (gcd k n) (k * m)" by (simp add: ac_simps)
1.127 -  also note gcd k n = 1
1.128 +  also note \<open>gcd k n = 1\<close>
1.129    finally have "gcd (gcd (k * m) n) k = 1" by simp
1.130    hence "gcd (k * m) n dvd m" by (rule coprime_dvd_mult, simp add: ac_simps)
1.131    moreover have "gcd (k * m) n dvd n" by simp
1.132 @@ -488,14 +488,14 @@
1.133    assume ?rhs then show ?lhs unfolding associated_def by (fast intro: mult_dvd_mono)
1.134  next
1.135    assume ?lhs
1.136 -  from ?lhs have "a dvd b * d" unfolding associated_def by (metis dvd_mult_left)
1.137 +  from \<open>?lhs\<close> have "a dvd b * d" unfolding associated_def by (metis dvd_mult_left)
1.138    hence "a dvd b" by (simp add: coprime_dvd_mult_iff)
1.139 -  moreover from ?lhs have "b dvd a * c" unfolding associated_def by (metis dvd_mult_left)
1.140 +  moreover from \<open>?lhs\<close> have "b dvd a * c" unfolding associated_def by (metis dvd_mult_left)
1.141    hence "b dvd a" by (simp add: coprime_dvd_mult_iff)
1.142 -  moreover from ?lhs have "c dvd d * b"
1.143 +  moreover from \<open>?lhs\<close> have "c dvd d * b"
1.144      unfolding associated_def by (auto dest: dvd_mult_right simp add: ac_simps)
1.145    hence "c dvd d" by (simp add: coprime_dvd_mult_iff gcd.commute)
1.146 -  moreover from ?lhs have "d dvd c * a"
1.147 +  moreover from \<open>?lhs\<close> have "d dvd c * a"
1.148      unfolding associated_def by (auto dest: dvd_mult_right simp add: ac_simps)
1.149    hence "d dvd c" by (simp add: coprime_dvd_mult_iff gcd.commute)
1.150    ultimately show ?rhs unfolding associated_def by simp
1.151 @@ -536,7 +536,7 @@
1.152    moreover from nz have "d \<noteq> 0" by simp
1.153    with div_mult_self1_is_id have "d * (l * u) div d = l * u" .
1.154    ultimately have "1 = l * u"
1.155 -    using d \<noteq> 0 by simp
1.156 +    using \<open>d \<noteq> 0\<close> by simp
1.157    then show "l dvd 1" ..
1.158  qed
1.160 @@ -555,7 +555,7 @@
1.161  proof (rule coprimeI)
1.162    fix l assume "l dvd d" and "l dvd a"
1.163    hence "l dvd a * b" by simp
1.164 -  with l dvd d and dab show "l dvd 1" by (auto intro: gcd_greatest)
1.165 +  with \<open>l dvd d\<close> and dab show "l dvd 1" by (auto intro: gcd_greatest)
1.166  qed
1.168  lemma coprime_rmult:
1.169 @@ -564,7 +564,7 @@
1.170  proof (rule coprimeI)
1.171    fix l assume "l dvd d" and "l dvd b"
1.172    hence "l dvd a * b" by simp
1.173 -  with l dvd d and dab show "l dvd 1" by (auto intro: gcd_greatest)
1.174 +  with \<open>l dvd d\<close> and dab show "l dvd 1" by (auto intro: gcd_greatest)
1.175  qed
1.177  lemma coprime_mul_eq: "gcd d (a * b) = 1 \<longleftrightarrow> gcd d a = 1 \<and> gcd d b = 1"
1.178 @@ -655,7 +655,7 @@
1.179    with dc have "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
1.180    from dc ab'(1,2) have "a'*?d dvd (b'*?d) * c" by simp
1.181    hence "?d * a' dvd ?d * (b' * c)" by (simp add: mult_ac)
1.182 -  with ?d \<noteq> 0 have "a' dvd b' * c" by simp
1.183 +  with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c" by simp
1.184    with coprime_dvd_mult[OF ab'(3)]
1.185      have "a' dvd c" by (subst (asm) ac_simps, blast)
1.186    with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c" by (simp add: mult_ac)
1.187 @@ -672,8 +672,8 @@
1.188    let ?d = "gcd a b"
1.189    assume "?d \<noteq> 0"
1.190    from n obtain m where m: "n = Suc m" by (cases n, simp_all)
1.191 -  from ?d \<noteq> 0 have zn: "?d ^ n \<noteq> 0" by (rule power_not_zero)
1.192 -  from gcd_coprime_exists[OF ?d \<noteq> 0]
1.193 +  from \<open>?d \<noteq> 0\<close> have zn: "?d ^ n \<noteq> 0" by (rule power_not_zero)
1.194 +  from gcd_coprime_exists[OF \<open>?d \<noteq> 0\<close>]
1.195      obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
1.196      by blast
1.197    from ab have "(a' * ?d) ^ n dvd (b' * ?d) ^ n"
1.198 @@ -755,7 +755,7 @@
1.199    hence "gcd a b \<noteq> 0" by simp
1.200    from lcm_gcd have "lcm a b * gcd a b = gcd a b * (a * b div (?nf (a*b) * gcd a b))"
1.201      by (simp add: mult_ac)
1.202 -  also from a * b \<noteq> 0 have "... = a * b div ?nf (a*b)"
1.203 +  also from \<open>a * b \<noteq> 0\<close> have "... = a * b div ?nf (a*b)"
1.204      by (simp add: div_mult_swap mult.commute)
1.205    finally show ?thesis .
1.206  qed (auto simp add: lcm_gcd)
1.207 @@ -766,11 +766,11 @@
1.208    assume "a * b \<noteq> 0"
1.209    hence "gcd a b \<noteq> 0" by simp
1.210    let ?c = "1 div normalization_factor (a * b)"
1.211 -  from a * b \<noteq> 0 have [simp]: "is_unit (normalization_factor (a * b))" by simp
1.212 +  from \<open>a * b \<noteq> 0\<close> have [simp]: "is_unit (normalization_factor (a * b))" by simp
1.213    from lcm_gcd_prod[of a b] have "lcm a b * gcd a b = a * ?c * b"
1.214      by (simp add: div_mult_swap unit_div_commute)
1.215    hence "lcm a b * gcd a b div gcd a b = a * ?c * b div gcd a b" by simp
1.216 -  with gcd a b \<noteq> 0 have "lcm a b = a * ?c * b div gcd a b"
1.217 +  with \<open>gcd a b \<noteq> 0\<close> have "lcm a b = a * ?c * b div gcd a b"
1.218      by (subst (asm) div_mult_self2_is_id, simp_all)
1.219    also have "... = a * (?c * b div gcd a b)"
1.220      by (metis div_mult_swap gcd_dvd2 mult_assoc)
1.221 @@ -785,36 +785,36 @@
1.222    hence "is_unit (?nf k)" by simp
1.223    hence "?nf k \<noteq> 0" by (metis not_is_unit_0)
1.224    assume A: "a dvd k" "b dvd k"
1.225 -  hence "gcd a b \<noteq> 0" using k \<noteq> 0 by auto
1.226 +  hence "gcd a b \<noteq> 0" using \<open>k \<noteq> 0\<close> by auto
1.227    from A obtain r s where ar: "k = a * r" and bs: "k = b * s"
1.228      unfolding dvd_def by blast
1.229 -  with k \<noteq> 0 have "r * s \<noteq> 0"
1.230 +  with \<open>k \<noteq> 0\<close> have "r * s \<noteq> 0"
1.231      by auto (drule sym [of 0], simp)
1.232    hence "is_unit (?nf (r * s))" by simp
1.233    let ?c = "?nf k div ?nf (r*s)"
1.234 -  from is_unit (?nf k) and is_unit (?nf (r * s)) have "is_unit ?c" by (rule unit_div)
1.235 +  from \<open>is_unit (?nf k)\<close> and \<open>is_unit (?nf (r * s))\<close> have "is_unit ?c" by (rule unit_div)
1.236    hence "?c \<noteq> 0" using not_is_unit_0 by fast
1.237    from ar bs have "k * k * gcd s r = ?nf k * k * gcd (k * s) (k * r)"
1.238      by (subst mult_assoc, subst gcd_mult_distrib[of k s r], simp only: ac_simps)
1.239    also have "... = ?nf k * k * gcd ((r*s) * a) ((r*s) * b)"
1.240 -    by (subst (3) k = a * r, subst (3) k = b * s, simp add: algebra_simps)
1.241 -  also have "... = ?c * r*s * k * gcd a b" using r * s \<noteq> 0
1.242 +    by (subst (3) \<open>k = a * r\<close>, subst (3) \<open>k = b * s\<close>, simp add: algebra_simps)
1.243 +  also have "... = ?c * r*s * k * gcd a b" using \<open>r * s \<noteq> 0\<close>
1.244      by (subst gcd_mult_distrib'[symmetric], simp add: algebra_simps unit_simps)
1.245    finally have "(a*r) * (b*s) * gcd s r = ?c * k * r * s * gcd a b"
1.246      by (subst ar[symmetric], subst bs[symmetric], simp add: mult_ac)
1.247    hence "a * b * gcd s r * (r * s) = ?c * k * gcd a b * (r * s)"
1.248      by (simp add: algebra_simps)
1.249 -  hence "?c * k * gcd a b = a * b * gcd s r" using r * s \<noteq> 0
1.250 +  hence "?c * k * gcd a b = a * b * gcd s r" using \<open>r * s \<noteq> 0\<close>
1.251      by (metis div_mult_self2_is_id)
1.252    also have "... = lcm a b * gcd a b * gcd s r * ?nf (a*b)"
1.253      by (subst lcm_gcd_prod[of a b], metis gcd_mult_distrib gcd_mult_distrib')
1.254    also have "... = lcm a b * gcd s r * ?nf (a*b) * gcd a b"
1.255      by (simp add: algebra_simps)
1.256 -  finally have "k * ?c = lcm a b * gcd s r * ?nf (a*b)" using gcd a b \<noteq> 0
1.257 +  finally have "k * ?c = lcm a b * gcd s r * ?nf (a*b)" using \<open>gcd a b \<noteq> 0\<close>
1.258      by (metis mult.commute div_mult_self2_is_id)
1.259 -  hence "k = lcm a b * (gcd s r * ?nf (a*b)) div ?c" using ?c \<noteq> 0
1.260 +  hence "k = lcm a b * (gcd s r * ?nf (a*b)) div ?c" using \<open>?c \<noteq> 0\<close>
1.261      by (metis div_mult_self2_is_id mult_assoc)
1.262 -  also have "... = lcm a b * (gcd s r * ?nf (a*b) div ?c)" using is_unit ?c
1.263 +  also have "... = lcm a b * (gcd s r * ?nf (a*b) div ?c)" using \<open>is_unit ?c\<close>
1.264      by (simp add: unit_simps)
1.265    finally show ?thesis by (rule dvdI)
1.266  qed simp
1.267 @@ -826,7 +826,7 @@
1.269      assume "a \<noteq> 0" "b \<noteq> 0"
1.270      hence "a * b div ?nf (a * b) \<noteq> 0" by (simp add: no_zero_divisors)
1.271 -    moreover from a \<noteq> 0 and b \<noteq> 0 have "gcd a b \<noteq> 0" by simp
1.272 +    moreover from \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "gcd a b \<noteq> 0" by simp
1.273      ultimately have "lcm a b \<noteq> 0" using lcm_gcd_prod[of a b] by (intro notI, simp)
1.274    } moreover {
1.275      assume "a = 0 \<or> b = 0"
1.276 @@ -843,12 +843,12 @@
1.277  proof-
1.278    from assms have "gcd a b \<noteq> 0" by (simp add: lcm_zero)
1.279    let ?c = "normalization_factor (a * b)"
1.280 -  from lcm a b \<noteq> 0 have "?c \<noteq> 0" by (intro notI, simp add: lcm_zero no_zero_divisors)
1.281 +  from \<open>lcm a b \<noteq> 0\<close> have "?c \<noteq> 0" by (intro notI, simp add: lcm_zero no_zero_divisors)
1.282    hence "is_unit ?c" by simp
1.283    from lcm_gcd_prod [of a b] have "gcd a b = a * b div ?c div lcm a b"
1.284 -    by (subst (2) div_mult_self2_is_id[OF lcm a b \<noteq> 0, symmetric], simp add: mult_ac)
1.285 -  also from is_unit ?c have "... = a * b div (lcm a b * ?c)"
1.286 -    by (metis ?c \<noteq> 0 div_mult_mult1 dvd_mult_div_cancel mult_commute normalization_factor_dvd')
1.287 +    by (subst (2) div_mult_self2_is_id[OF \<open>lcm a b \<noteq> 0\<close>, symmetric], simp add: mult_ac)
1.288 +  also from \<open>is_unit ?c\<close> have "... = a * b div (lcm a b * ?c)"
1.289 +    by (metis \<open>?c \<noteq> 0\<close> div_mult_mult1 dvd_mult_div_cancel mult_commute normalization_factor_dvd')
1.290    finally show ?thesis .
1.291  qed
1.293 @@ -891,11 +891,11 @@
1.295      fix l assume "a dvd l" and "lcm b c dvd l"
1.296      have "b dvd lcm b c" by simp
1.297 -    from this and lcm b c dvd l have "b dvd l" by (rule dvd_trans)
1.298 +    from this and \<open>lcm b c dvd l\<close> have "b dvd l" by (rule dvd_trans)
1.299      have "c dvd lcm b c" by simp
1.300 -    from this and lcm b c dvd l have "c dvd l" by (rule dvd_trans)
1.301 -    from a dvd l and b dvd l have "lcm a b dvd l" by (rule lcm_least)
1.302 -    from this and c dvd l show "lcm (lcm a b) c dvd l" by (rule lcm_least)
1.303 +    from this and \<open>lcm b c dvd l\<close> have "c dvd l" by (rule dvd_trans)
1.304 +    from \<open>a dvd l\<close> and \<open>b dvd l\<close> have "lcm a b dvd l" by (rule lcm_least)
1.305 +    from this and \<open>c dvd l\<close> show "lcm (lcm a b) c dvd l" by (rule lcm_least)
1.306    qed (simp add: lcm_zero)
1.307  next
1.308    fix a b
1.309 @@ -926,7 +926,7 @@
1.310    hence "is_unit (lcm a b)" by (rule lcm_least)
1.311    hence "lcm a b = normalization_factor (lcm a b)"
1.312      by (subst normalization_factor_unit, simp_all)
1.313 -  also have "\<dots> = 1" using is_unit a \<and> is_unit b
1.314 +  also have "\<dots> = 1" using \<open>is_unit a \<and> is_unit b\<close>
1.315      by auto
1.316    finally show "lcm a b = 1" .
1.317  qed
1.318 @@ -999,7 +999,7 @@
1.319  proof -
1.320    have "a dvd lcm a b" by (rule lcm_dvd1)
1.321    then obtain c where A: "lcm a b = a * c" unfolding dvd_def by blast
1.322 -  with a \<noteq> 0 and b \<noteq> 0 have "c \<noteq> 0" by (auto simp: lcm_zero)
1.323 +  with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "c \<noteq> 0" by (auto simp: lcm_zero)
1.324    then show ?thesis by (subst A, intro size_mult_mono)
1.325  qed
1.327 @@ -1013,12 +1013,12 @@
1.328  proof (rule ccontr)
1.329    from assms have "a \<noteq> 0" by auto
1.330    assume "\<not>euclidean_size a < euclidean_size (lcm a b)"
1.331 -  with a \<noteq> 0 and b \<noteq> 0 have "euclidean_size (lcm a b) = euclidean_size a"
1.332 +  with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "euclidean_size (lcm a b) = euclidean_size a"
1.333      by (intro le_antisym, simp, intro euclidean_size_lcm_le1)
1.334    with assms have "lcm a b dvd a"
1.335      by (rule_tac dvd_euclidean_size_eq_imp_dvd) (auto simp: lcm_zero)
1.336    hence "b dvd a" by (rule dvd_lcm_D2)
1.337 -  with \<not>b dvd a show False by contradiction
1.338 +  with \<open>\<not>b dvd a\<close> show False by contradiction
1.339  qed
1.341  lemma euclidean_size_lcm_less2:
1.342 @@ -1101,8 +1101,8 @@
1.343        unfolding l_def by simp_all
1.345        fix l' assume "\<forall>a\<in>A. a dvd l'"
1.346 -      with \<forall>a\<in>A. a dvd l have "\<forall>a\<in>A. a dvd gcd l l'" by (auto intro: gcd_greatest)
1.347 -      moreover from l \<noteq> 0 have "gcd l l' \<noteq> 0" by simp
1.348 +      with \<open>\<forall>a\<in>A. a dvd l\<close> have "\<forall>a\<in>A. a dvd gcd l l'" by (auto intro: gcd_greatest)
1.349 +      moreover from \<open>l \<noteq> 0\<close> have "gcd l l' \<noteq> 0" by simp
1.350        ultimately have "\<exists>b. b \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd b) \<and> euclidean_size b = euclidean_size (gcd l l')"
1.351          by (intro exI[of _ "gcd l l'"], auto)
1.352        hence "euclidean_size (gcd l l') \<ge> n" by (subst n_def) (rule Least_le)
1.353 @@ -1110,20 +1110,20 @@
1.354        proof -
1.355          have "gcd l l' dvd l" by simp
1.356          then obtain a where "l = gcd l l' * a" unfolding dvd_def by blast
1.357 -        with l \<noteq> 0 have "a \<noteq> 0" by auto
1.358 +        with \<open>l \<noteq> 0\<close> have "a \<noteq> 0" by auto
1.359          hence "euclidean_size (gcd l l') \<le> euclidean_size (gcd l l' * a)"
1.360            by (rule size_mult_mono)
1.361 -        also have "gcd l l' * a = l" using l = gcd l l' * a ..
1.362 -        also note euclidean_size l = n
1.363 +        also have "gcd l l' * a = l" using \<open>l = gcd l l' * a\<close> ..
1.364 +        also note \<open>euclidean_size l = n\<close>
1.365          finally show "euclidean_size (gcd l l') \<le> n" .
1.366        qed
1.367        ultimately have "euclidean_size l = euclidean_size (gcd l l')"
1.368 -        by (intro le_antisym, simp_all add: euclidean_size l = n)
1.369 -      with l \<noteq> 0 have "l dvd gcd l l'" by (blast intro: dvd_euclidean_size_eq_imp_dvd)
1.370 +        by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>)
1.371 +      with \<open>l \<noteq> 0\<close> have "l dvd gcd l l'" by (blast intro: dvd_euclidean_size_eq_imp_dvd)
1.372        hence "l dvd l'" by (blast dest: dvd_gcd_D2)
1.375 -    with (\<forall>a\<in>A. a dvd l) and normalization_factor_is_unit[OF l \<noteq> 0] and l \<noteq> 0
1.376 +    with \<open>(\<forall>a\<in>A. a dvd l)\<close> and normalization_factor_is_unit[OF \<open>l \<noteq> 0\<close>] and \<open>l \<noteq> 0\<close>
1.377        have "(\<forall>a\<in>A. a dvd l div normalization_factor l) \<and>
1.378          (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> l div normalization_factor l dvd l') \<and>
1.379          normalization_factor (l div normalization_factor l) =
1.380 @@ -1206,7 +1206,7 @@
1.381      hence "l div normalization_factor l \<noteq> 0" by simp
1.382      also from ex have "l div normalization_factor l = Lcm A"
1.383         by (simp only: Lcm_Lcm_eucl Lcm_eucl_def n_def l_def if_True Let_def)
1.384 -    finally show False using Lcm A = 0 by contradiction
1.385 +    finally show False using \<open>Lcm A = 0\<close> by contradiction
1.386    qed
1.387  qed (simp only: Lcm_Lcm_eucl Lcm_eucl_def if_False)
1.389 @@ -1218,13 +1218,13 @@
1.390    moreover {
1.391      assume "0 \<notin> A"
1.392      hence "\<Prod>A \<noteq> 0"
1.393 -      apply (induct rule: finite_induct[OF finite A])
1.394 +      apply (induct rule: finite_induct[OF \<open>finite A\<close>])
1.395        apply simp
1.396        apply (subst setprod.insert, assumption, assumption)
1.397        apply (rule no_zero_divisors)
1.398        apply blast+
1.399        done
1.400 -    moreover from finite A have "\<forall>a\<in>A. a dvd \<Prod>A" by blast
1.401 +    moreover from \<open>finite A\<close> have "\<forall>a\<in>A. a dvd \<Prod>A" by blast
1.402      ultimately have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l)" by blast
1.403      with Lcm0_iff' have "Lcm A \<noteq> 0" by simp
1.405 @@ -1244,13 +1244,13 @@
1.406  proof (rule lcmI)
1.407    fix l assume "a dvd l" and "Lcm A dvd l"
1.408    hence "\<forall>a\<in>A. a dvd l" by (blast intro: dvd_trans dvd_Lcm)
1.409 -  with a dvd l show "Lcm (insert a A) dvd l" by (force intro: Lcm_dvd)
1.410 +  with \<open>a dvd l\<close> show "Lcm (insert a A) dvd l" by (force intro: Lcm_dvd)
1.411  qed (auto intro: Lcm_dvd dvd_Lcm)
1.413  lemma Lcm_finite:
1.414    assumes "finite A"
1.415    shows "Lcm A = Finite_Set.fold lcm 1 A"
1.416 -  by (induct rule: finite.induct[OF finite A])
1.417 +  by (induct rule: finite.induct[OF \<open>finite A\<close>])
1.418      (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm])
1.420  lemma Lcm_set [code_unfold]:
1.421 @@ -1337,13 +1337,13 @@
1.422  proof (rule gcdI)
1.423    fix l assume "l dvd a" and "l dvd Gcd A"
1.424    hence "\<forall>a\<in>A. l dvd a" by (blast intro: dvd_trans Gcd_dvd)
1.425 -  with l dvd a show "l dvd Gcd (insert a A)" by (force intro: Gcd_dvd)
1.426 +  with \<open>l dvd a\<close> show "l dvd Gcd (insert a A)" by (force intro: Gcd_dvd)
1.427  qed auto
1.429  lemma Gcd_finite:
1.430    assumes "finite A"
1.431    shows "Gcd A = Finite_Set.fold gcd 0 A"
1.432 -  by (induct rule: finite.induct[OF finite A])
1.433 +  by (induct rule: finite.induct[OF \<open>finite A\<close>])
1.434      (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd])
1.436  lemma Gcd_set [code_unfold]:
1.437 @@ -1361,10 +1361,10 @@
1.439  end
1.441 -text {*
1.442 +text \<open>
1.443    A Euclidean ring is a Euclidean semiring with additive inverses. It provides a
1.444    few more lemmas; in particular, Bezout's lemma holds for any Euclidean ring.
1.445 -*}
1.446 +\<close>
1.448  class euclidean_ring = euclidean_semiring + idom