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.5  
     1.6 -section {* Abstract euclidean algorithm *}
     1.7 +section \<open>Abstract euclidean algorithm\<close>
     1.8  
     1.9  theory Euclidean_Algorithm
    1.10  imports Complex_Main
    1.11  begin
    1.12    
    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.48  
    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.98  
    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.112  
   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.121  
   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.159  
   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.167  
   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.176  
   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.268    {
   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.292  
   1.293 @@ -891,11 +891,11 @@
   1.294  
   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.326  
   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.340  
   1.341  lemma euclidean_size_lcm_less2:
   1.342 @@ -1101,8 +1101,8 @@
   1.343        unfolding l_def by simp_all
   1.344      {
   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.373      }
   1.374  
   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.388  
   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.404    }
   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.412   
   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.419  
   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.428  
   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.435  
   1.436  lemma Gcd_set [code_unfold]:
   1.437 @@ -1361,10 +1361,10 @@
   1.438    
   1.439  end
   1.440  
   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.447  
   1.448  class euclidean_ring = euclidean_semiring + idom
   1.449