standardized algebraic conventions: prefer a, b, c over x, y, z
authorhaftmann
Fri Jun 12 08:53:23 2015 +0200 (2015-06-12)
changeset 60430ce559c850a27
parent 60429 d3d1e185cd63
child 60431 db9c67b760f1
standardized algebraic conventions: prefer a, b, c over x, y, z
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 12 08:53:23 2015 +0200
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 12 08:53:23 2015 +0200
     1.3 @@ -11,26 +11,26 @@
     1.4  
     1.5  abbreviation is_unit :: "'a \<Rightarrow> bool"
     1.6  where
     1.7 -  "is_unit x \<equiv> x dvd 1"
     1.8 +  "is_unit a \<equiv> a dvd 1"
     1.9  
    1.10  definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
    1.11  where
    1.12 -  "associated x y \<longleftrightarrow> x dvd y \<and> y dvd x"
    1.13 +  "associated a b \<longleftrightarrow> a dvd b \<and> b dvd a"
    1.14  
    1.15  definition ring_inv :: "'a \<Rightarrow> 'a"
    1.16  where
    1.17 -  "ring_inv x = 1 div x"
    1.18 +  "ring_inv a = 1 div a"
    1.19  
    1.20  lemma unit_prod [intro]:
    1.21 -  "is_unit x \<Longrightarrow> is_unit y \<Longrightarrow> is_unit (x * y)"
    1.22 +  "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
    1.23    by (subst mult_1_left [of 1, symmetric], rule mult_dvd_mono) 
    1.24  
    1.25  lemma unit_ring_inv:
    1.26 -  "is_unit y \<Longrightarrow> x div y = x * ring_inv y"
    1.27 +  "is_unit b \<Longrightarrow> a div b = a * ring_inv b"
    1.28    by (simp add: div_mult_swap ring_inv_def)
    1.29  
    1.30  lemma unit_ring_inv_ring_inv [simp]:
    1.31 -  "is_unit x \<Longrightarrow> ring_inv (ring_inv x) = x"
    1.32 +  "is_unit a \<Longrightarrow> ring_inv (ring_inv a) = a"
    1.33    unfolding ring_inv_def
    1.34    by (metis div_mult_mult1_if div_mult_self1_is_id dvd_mult_div_cancel mult_1_right)
    1.35  
    1.36 @@ -47,67 +47,67 @@
    1.37    by (simp add: ac_simps)
    1.38  
    1.39  lemma unit_ring_inv_unit [simp, intro]:
    1.40 -  assumes "is_unit x"
    1.41 -  shows "is_unit (ring_inv x)"
    1.42 +  assumes "is_unit a"
    1.43 +  shows "is_unit (ring_inv a)"
    1.44  proof -
    1.45 -  from assms have "1 = ring_inv x * x" by simp
    1.46 -  then show "is_unit (ring_inv x)" by (rule dvdI)
    1.47 +  from assms have "1 = ring_inv a * a" by simp
    1.48 +  then show "is_unit (ring_inv a)" by (rule dvdI)
    1.49  qed
    1.50  
    1.51  lemma mult_unit_dvd_iff:
    1.52 -  "is_unit y \<Longrightarrow> x * y dvd z \<longleftrightarrow> x dvd z"
    1.53 +  "is_unit b \<Longrightarrow> a * b dvd c \<longleftrightarrow> a dvd c"
    1.54  proof
    1.55 -  assume "is_unit y" "x * y dvd z"
    1.56 -  then show "x dvd z" by (simp add: dvd_mult_left)
    1.57 +  assume "is_unit b" "a * b dvd c"
    1.58 +  then show "a dvd c" by (simp add: dvd_mult_left)
    1.59  next
    1.60 -  assume "is_unit y" "x dvd z"
    1.61 -  then obtain k where "z = x * k" unfolding dvd_def by blast
    1.62 -  with `is_unit y` have "z = (x * y) * (ring_inv y * k)" 
    1.63 +  assume "is_unit b" "a dvd c"
    1.64 +  then obtain k where "c = a * k" unfolding dvd_def by blast
    1.65 +  with `is_unit b` have "c = (a * b) * (ring_inv b * k)" 
    1.66        by (simp add: mult_ac)
    1.67 -  then show "x * y dvd z" by (rule dvdI)
    1.68 +  then show "a * b dvd c" by (rule dvdI)
    1.69  qed
    1.70  
    1.71  lemma div_unit_dvd_iff:
    1.72 -  "is_unit y \<Longrightarrow> x div y dvd z \<longleftrightarrow> x dvd z"
    1.73 +  "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"
    1.74    by (subst unit_ring_inv) (assumption, simp add: mult_unit_dvd_iff)
    1.75  
    1.76  lemma dvd_mult_unit_iff:
    1.77 -  "is_unit y \<Longrightarrow> x dvd z * y \<longleftrightarrow> x dvd z"
    1.78 +  "is_unit b \<Longrightarrow> a dvd c * b \<longleftrightarrow> a dvd c"
    1.79  proof
    1.80 -  assume "is_unit y" and "x dvd z * y"
    1.81 -  have "z * y dvd z * (y * ring_inv y)" by (subst mult_assoc [symmetric]) simp
    1.82 -  also from `is_unit y` have "y * ring_inv y = 1" by simp
    1.83 -  finally have "z * y dvd z" by simp
    1.84 -  with `x dvd z * y` show "x dvd z" by (rule dvd_trans)
    1.85 +  assume "is_unit b" and "a dvd c * b"
    1.86 +  have "c * b dvd c * (b * ring_inv b)" by (subst mult_assoc [symmetric]) simp
    1.87 +  also from `is_unit b` have "b * ring_inv b = 1" by simp
    1.88 +  finally have "c * b dvd c" by simp
    1.89 +  with `a dvd c * b` show "a dvd c" by (rule dvd_trans)
    1.90  next
    1.91 -  assume "x dvd z"
    1.92 -  then show "x dvd z * y" by simp
    1.93 +  assume "a dvd c"
    1.94 +  then show "a dvd c * b" by simp
    1.95  qed
    1.96  
    1.97  lemma dvd_div_unit_iff:
    1.98 -  "is_unit y \<Longrightarrow> x dvd z div y \<longleftrightarrow> x dvd z"
    1.99 +  "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c"
   1.100    by (subst unit_ring_inv) (assumption, simp add: dvd_mult_unit_iff)
   1.101  
   1.102  lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff dvd_div_unit_iff
   1.103  
   1.104  lemma unit_div [intro]:
   1.105 -  "is_unit x \<Longrightarrow> is_unit y \<Longrightarrow> is_unit (x div y)"
   1.106 +  "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
   1.107    by (subst unit_ring_inv) (assumption, rule unit_prod, simp_all)
   1.108  
   1.109  lemma unit_div_mult_swap:
   1.110 -  "is_unit z \<Longrightarrow> x * (y div z) = x * y div z"
   1.111 -  by (simp only: unit_ring_inv [of _ y] unit_ring_inv [of _ "x*y"] ac_simps)
   1.112 +  "is_unit c \<Longrightarrow> a * (b div c) = a * b div c"
   1.113 +  by (simp only: unit_ring_inv [of _ b] unit_ring_inv [of _ "a*b"] ac_simps)
   1.114  
   1.115  lemma unit_div_commute:
   1.116 -  "is_unit y \<Longrightarrow> x div y * z = x * z div y"
   1.117 -  by (simp only: unit_ring_inv [of _ x] unit_ring_inv [of _ "x*z"] ac_simps)
   1.118 +  "is_unit b \<Longrightarrow> a div b * c = a * c div b"
   1.119 +  by (simp only: unit_ring_inv [of _ a] unit_ring_inv [of _ "a*c"] ac_simps)
   1.120  
   1.121  lemma unit_imp_dvd [dest]:
   1.122 -  "is_unit y \<Longrightarrow> y dvd x"
   1.123 +  "is_unit b \<Longrightarrow> b dvd a"
   1.124    by (rule dvd_trans [of _ 1]) simp_all
   1.125  
   1.126  lemma dvd_unit_imp_unit:
   1.127 -  "is_unit y \<Longrightarrow> x dvd y \<Longrightarrow> is_unit x"
   1.128 +  "is_unit b \<Longrightarrow> a dvd b \<Longrightarrow> is_unit a"
   1.129    by (rule dvd_trans)
   1.130  
   1.131  lemma ring_inv_0 [simp]:
   1.132 @@ -115,20 +115,20 @@
   1.133    unfolding ring_inv_def by simp
   1.134  
   1.135  lemma unit_ring_inv'1:
   1.136 -  assumes "is_unit y"
   1.137 -  shows "x div (y * z) = x * ring_inv y div z" 
   1.138 +  assumes "is_unit b"
   1.139 +  shows "a div (b * c) = a * ring_inv b div c" 
   1.140  proof -
   1.141 -  from assms have "x div (y * z) = x * (ring_inv y * y) div (y * z)"
   1.142 +  from assms have "a div (b * c) = a * (ring_inv b * b) div (b * c)"
   1.143      by simp
   1.144 -  also have "... = y * (x * ring_inv y) div (y * z)"
   1.145 +  also have "... = b * (a * ring_inv b) div (b * c)"
   1.146      by (simp only: mult_ac)
   1.147 -  also have "... = x * ring_inv y div z"
   1.148 -    by (cases "y = 0", simp, rule div_mult_mult1)
   1.149 +  also have "... = a * ring_inv b div c"
   1.150 +    by (cases "b = 0", simp, rule div_mult_mult1)
   1.151    finally show ?thesis .
   1.152  qed
   1.153  
   1.154  lemma associated_comm:
   1.155 -  "associated x y \<Longrightarrow> associated y x"
   1.156 +  "associated a b \<Longrightarrow> associated b a"
   1.157    by (simp add: associated_def)
   1.158  
   1.159  lemma associated_0 [simp]:
   1.160 @@ -137,7 +137,7 @@
   1.161    unfolding associated_def by simp_all
   1.162  
   1.163  lemma associated_unit:
   1.164 -  "is_unit x \<Longrightarrow> associated x y \<Longrightarrow> is_unit y"
   1.165 +  "is_unit a \<Longrightarrow> associated a b \<Longrightarrow> is_unit b"
   1.166    unfolding associated_def using dvd_unit_imp_unit by auto
   1.167  
   1.168  lemma is_unit_1 [simp]:
   1.169 @@ -149,61 +149,61 @@
   1.170    by auto
   1.171  
   1.172  lemma unit_mult_left_cancel:
   1.173 -  assumes "is_unit x"
   1.174 -  shows "(x * y) = (x * z) \<longleftrightarrow> y = z"
   1.175 +  assumes "is_unit a"
   1.176 +  shows "(a * b) = (a * c) \<longleftrightarrow> b = c"
   1.177  proof -
   1.178 -  from assms have "x \<noteq> 0" by auto
   1.179 +  from assms have "a \<noteq> 0" by auto
   1.180    then show ?thesis by (metis div_mult_self1_is_id)
   1.181  qed
   1.182  
   1.183  lemma unit_mult_right_cancel:
   1.184 -  "is_unit x \<Longrightarrow> (y * x) = (z * x) \<longleftrightarrow> y = z"
   1.185 +  "is_unit a \<Longrightarrow> (b * a) = (c * a) \<longleftrightarrow> b = c"
   1.186    by (simp add: ac_simps unit_mult_left_cancel)
   1.187  
   1.188  lemma unit_div_cancel:
   1.189 -  "is_unit x \<Longrightarrow> (y div x) = (z div x) \<longleftrightarrow> y = z"
   1.190 -  apply (subst unit_ring_inv[of _ y], assumption)
   1.191 -  apply (subst unit_ring_inv[of _ z], assumption)
   1.192 +  "is_unit a \<Longrightarrow> (b div a) = (c div a) \<longleftrightarrow> b = c"
   1.193 +  apply (subst unit_ring_inv[of _ b], assumption)
   1.194 +  apply (subst unit_ring_inv[of _ c], assumption)
   1.195    apply (rule unit_mult_right_cancel, erule unit_ring_inv_unit)
   1.196    done
   1.197  
   1.198  lemma unit_eq_div1:
   1.199 -  "is_unit y \<Longrightarrow> x div y = z \<longleftrightarrow> x = z * y"
   1.200 +  "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b"
   1.201    apply (subst unit_ring_inv, assumption)
   1.202    apply (subst unit_mult_right_cancel[symmetric], assumption)
   1.203    apply (subst mult_assoc, subst ring_inv_is_inv2, assumption, simp)
   1.204    done
   1.205  
   1.206  lemma unit_eq_div2:
   1.207 -  "is_unit y \<Longrightarrow> x = z div y \<longleftrightarrow> x * y = z"
   1.208 +  "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = c"
   1.209    by (subst (1 2) eq_commute, simp add: unit_eq_div1, subst eq_commute, rule refl)
   1.210  
   1.211  lemma associated_iff_div_unit:
   1.212 -  "associated x y \<longleftrightarrow> (\<exists>z. is_unit z \<and> x = z * y)"
   1.213 +  "associated a b \<longleftrightarrow> (\<exists>c. is_unit c \<and> a = c * b)"
   1.214  proof
   1.215 -  assume "associated x y"
   1.216 -  show "\<exists>z. is_unit z \<and> x = z * y"
   1.217 -  proof (cases "x = 0")
   1.218 -    assume "x = 0"
   1.219 -    then show "\<exists>z. is_unit z \<and> x = z * y" using `associated x y`
   1.220 +  assume "associated a b"
   1.221 +  show "\<exists>c. is_unit c \<and> a = c * b"
   1.222 +  proof (cases "a = 0")
   1.223 +    assume "a = 0"
   1.224 +    then show "\<exists>c. is_unit c \<and> a = c * b" using `associated a b`
   1.225          by (intro exI[of _ 1], simp add: associated_def)
   1.226    next
   1.227 -    assume [simp]: "x \<noteq> 0"
   1.228 -    hence [simp]: "x dvd y" "y dvd x" using `associated x y`
   1.229 +    assume [simp]: "a \<noteq> 0"
   1.230 +    hence [simp]: "a dvd b" "b dvd a" using `associated a b`
   1.231          unfolding associated_def by simp_all
   1.232 -    hence "1 = x div y * (y div x)"
   1.233 +    hence "1 = a div b * (b div a)"
   1.234        by (simp add: div_mult_swap)
   1.235 -    hence "is_unit (x div y)" ..
   1.236 -    moreover have "x = (x div y) * y" by simp
   1.237 +    hence "is_unit (a div b)" ..
   1.238 +    moreover have "a = (a div b) * b" by simp
   1.239      ultimately show ?thesis by blast
   1.240    qed
   1.241  next
   1.242 -  assume "\<exists>z. is_unit z \<and> x = z * y"
   1.243 -  then obtain z where "is_unit z" and "x = z * y" by blast
   1.244 -  hence "y = x * ring_inv z" by (simp add: algebra_simps)
   1.245 -  hence "x dvd y" by simp
   1.246 -  moreover from `x = z * y` have "y dvd x" by simp
   1.247 -  ultimately show "associated x y" unfolding associated_def by simp
   1.248 +  assume "\<exists>c. is_unit c \<and> a = c * b"
   1.249 +  then obtain c where "is_unit c" and "a = c * b" by blast
   1.250 +  hence "b = a * ring_inv c" by (simp add: algebra_simps)
   1.251 +  hence "a dvd b" by simp
   1.252 +  moreover from `a = c * b` have "b dvd a" by simp
   1.253 +  ultimately show "associated a b" unfolding associated_def by simp
   1.254  qed
   1.255  
   1.256  lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff 
   1.257 @@ -217,7 +217,7 @@
   1.258  begin
   1.259  
   1.260  lemma is_unit_neg [simp]:
   1.261 -  "is_unit (- x) \<Longrightarrow> is_unit x"
   1.262 +  "is_unit (- a) \<Longrightarrow> is_unit a"
   1.263    by simp
   1.264  
   1.265  lemma is_unit_neg_1 [simp]:
   1.266 @@ -227,11 +227,11 @@
   1.267  end
   1.268  
   1.269  lemma is_unit_nat [simp]:
   1.270 -  "is_unit (x::nat) \<longleftrightarrow> x = 1"
   1.271 +  "is_unit (a::nat) \<longleftrightarrow> a = 1"
   1.272    by simp
   1.273  
   1.274  lemma is_unit_int:
   1.275 -  "is_unit (x::int) \<longleftrightarrow> x = 1 \<or> x = -1"
   1.276 +  "is_unit (a::int) \<longleftrightarrow> a = 1 \<or> a = -1"
   1.277    by auto
   1.278  
   1.279  text {*
   1.280 @@ -258,7 +258,7 @@
   1.281      "a \<noteq> 0 \<Longrightarrow> is_unit (normalisation_factor a)"
   1.282    assumes normalisation_factor_mult: "normalisation_factor (a * b) = 
   1.283      normalisation_factor a * normalisation_factor b"
   1.284 -  assumes normalisation_factor_unit: "is_unit x \<Longrightarrow> normalisation_factor x = x"
   1.285 +  assumes normalisation_factor_unit: "is_unit a \<Longrightarrow> normalisation_factor a = a"
   1.286    assumes normalisation_factor_0 [simp]: "normalisation_factor 0 = 0"
   1.287  begin
   1.288  
   1.289 @@ -271,41 +271,41 @@
   1.290    by (simp add: normalisation_factor_unit)
   1.291  
   1.292  lemma normalisation_factor_0_iff [simp]:
   1.293 -  "normalisation_factor x = 0 \<longleftrightarrow> x = 0"
   1.294 +  "normalisation_factor a = 0 \<longleftrightarrow> a = 0"
   1.295  proof
   1.296 -  assume "normalisation_factor x = 0"
   1.297 -  hence "\<not> is_unit (normalisation_factor x)"
   1.298 +  assume "normalisation_factor a = 0"
   1.299 +  hence "\<not> is_unit (normalisation_factor a)"
   1.300      by (metis not_is_unit_0)
   1.301 -  then show "x = 0" by force
   1.302 +  then show "a = 0" by force
   1.303  next
   1.304 -  assume "x = 0"
   1.305 -  then show "normalisation_factor x = 0" by simp
   1.306 +  assume "a = 0"
   1.307 +  then show "normalisation_factor a = 0" by simp
   1.308  qed
   1.309  
   1.310  lemma normalisation_factor_pow:
   1.311 -  "normalisation_factor (x ^ n) = normalisation_factor x ^ n"
   1.312 +  "normalisation_factor (a ^ n) = normalisation_factor a ^ n"
   1.313    by (induct n) (simp_all add: normalisation_factor_mult power_Suc2)
   1.314  
   1.315  lemma normalisation_correct [simp]:
   1.316 -  "normalisation_factor (x div normalisation_factor x) = (if x = 0 then 0 else 1)"
   1.317 -proof (cases "x = 0", simp)
   1.318 -  assume "x \<noteq> 0"
   1.319 +  "normalisation_factor (a div normalisation_factor a) = (if a = 0 then 0 else 1)"
   1.320 +proof (cases "a = 0", simp)
   1.321 +  assume "a \<noteq> 0"
   1.322    let ?nf = "normalisation_factor"
   1.323 -  from normalisation_factor_is_unit[OF `x \<noteq> 0`] have "?nf x \<noteq> 0"
   1.324 +  from normalisation_factor_is_unit[OF `a \<noteq> 0`] have "?nf a \<noteq> 0"
   1.325      by (metis not_is_unit_0) 
   1.326 -  have "?nf (x div ?nf x) * ?nf (?nf x) = ?nf (x div ?nf x * ?nf x)" 
   1.327 +  have "?nf (a div ?nf a) * ?nf (?nf a) = ?nf (a div ?nf a * ?nf a)" 
   1.328      by (simp add: normalisation_factor_mult)
   1.329 -  also have "x div ?nf x * ?nf x = x" using `x \<noteq> 0`
   1.330 +  also have "a div ?nf a * ?nf a = a" using `a \<noteq> 0`
   1.331      by simp
   1.332 -  also have "?nf (?nf x) = ?nf x" using `x \<noteq> 0` 
   1.333 +  also have "?nf (?nf a) = ?nf a" using `a \<noteq> 0` 
   1.334      normalisation_factor_is_unit normalisation_factor_unit by simp
   1.335 -  finally show ?thesis using `x \<noteq> 0` and `?nf x \<noteq> 0` 
   1.336 +  finally show ?thesis using `a \<noteq> 0` and `?nf a \<noteq> 0` 
   1.337      by (metis div_mult_self2_is_id div_self)
   1.338  qed
   1.339  
   1.340  lemma normalisation_0_iff [simp]:
   1.341 -  "x div normalisation_factor x = 0 \<longleftrightarrow> x = 0"
   1.342 -  by (cases "x = 0", simp, subst unit_eq_div1, blast, simp)
   1.343 +  "a div normalisation_factor a = 0 \<longleftrightarrow> a = 0"
   1.344 +  by (cases "a = 0", simp, subst unit_eq_div1, blast, simp)
   1.345  
   1.346  lemma associated_iff_normed_eq:
   1.347    "associated a b \<longleftrightarrow> a div normalisation_factor a = b div normalisation_factor b"
   1.348 @@ -316,15 +316,15 @@
   1.349      apply (subst (asm) unit_eq_div1, blast, subst (asm) unit_div_commute, blast)
   1.350      apply (subst div_mult_swap, simp, simp)
   1.351      done
   1.352 -  with `a \<noteq> 0` `b \<noteq> 0` have "\<exists>z. is_unit z \<and> a = z * b"
   1.353 +  with `a \<noteq> 0` `b \<noteq> 0` have "\<exists>c. is_unit c \<and> a = c * b"
   1.354      by (intro exI[of _ "?nf a div ?nf b"], force simp: mult_ac)
   1.355    with associated_iff_div_unit show "associated a b" by simp
   1.356  next
   1.357    let ?nf = normalisation_factor
   1.358    assume "a \<noteq> 0" "b \<noteq> 0" "associated a b"
   1.359 -  with associated_iff_div_unit obtain z where "is_unit z" and "a = z * b" by blast
   1.360 +  with associated_iff_div_unit obtain c where "is_unit c" and "a = c * b" by blast
   1.361    then show "a div ?nf a = b div ?nf b"
   1.362 -    apply (simp only: `a = z * b` normalisation_factor_mult normalisation_factor_unit)
   1.363 +    apply (simp only: `a = c * b` normalisation_factor_mult normalisation_factor_unit)
   1.364      apply (rule div_mult_mult1, force)
   1.365      done
   1.366    qed
   1.367 @@ -385,9 +385,9 @@
   1.368  
   1.369  definition Lcm_eucl :: "'a set \<Rightarrow> 'a"
   1.370  where
   1.371 -  "Lcm_eucl A = (if \<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l) then
   1.372 -     let l = SOME l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l) \<and> euclidean_size l =
   1.373 -       (LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l) \<and> euclidean_size l = n)
   1.374 +  "Lcm_eucl A = (if \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) then
   1.375 +     let l = SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l =
   1.376 +       (LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)
   1.377         in l div normalisation_factor l
   1.378        else 0)"
   1.379  
   1.380 @@ -403,37 +403,37 @@
   1.381  begin
   1.382  
   1.383  lemma gcd_red:
   1.384 -  "gcd x y = gcd y (x mod y)"
   1.385 +  "gcd a b = gcd b (a mod b)"
   1.386    by (metis gcd_eucl.simps mod_0 mod_by_0 gcd_gcd_eucl)
   1.387  
   1.388  lemma gcd_non_0:
   1.389 -  "y \<noteq> 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
   1.390 +  "b \<noteq> 0 \<Longrightarrow> gcd a b = gcd b (a mod b)"
   1.391    by (rule gcd_red)
   1.392  
   1.393  lemma gcd_0_left:
   1.394 -  "gcd 0 x = x div normalisation_factor x"
   1.395 +  "gcd 0 a = a div normalisation_factor a"
   1.396     by (simp only: gcd_gcd_eucl, subst gcd_eucl.simps, subst gcd_eucl.simps, simp add: Let_def)
   1.397  
   1.398  lemma gcd_0:
   1.399 -  "gcd x 0 = x div normalisation_factor x"
   1.400 +  "gcd a 0 = a div normalisation_factor a"
   1.401    by (simp only: gcd_gcd_eucl, subst gcd_eucl.simps, simp add: Let_def)
   1.402  
   1.403 -lemma gcd_dvd1 [iff]: "gcd x y dvd x"
   1.404 -  and gcd_dvd2 [iff]: "gcd x y dvd y"
   1.405 -proof (induct x y rule: gcd_eucl.induct)
   1.406 -  fix x y :: 'a
   1.407 -  assume IH1: "y \<noteq> 0 \<Longrightarrow> gcd y (x mod y) dvd y"
   1.408 -  assume IH2: "y \<noteq> 0 \<Longrightarrow> gcd y (x mod y) dvd (x mod y)"
   1.409 +lemma gcd_dvd1 [iff]: "gcd a b dvd a"
   1.410 +  and gcd_dvd2 [iff]: "gcd a b dvd b"
   1.411 +proof (induct a b rule: gcd_eucl.induct)
   1.412 +  fix a b :: 'a
   1.413 +  assume IH1: "b \<noteq> 0 \<Longrightarrow> gcd b (a mod b) dvd b"
   1.414 +  assume IH2: "b \<noteq> 0 \<Longrightarrow> gcd b (a mod b) dvd (a mod b)"
   1.415    
   1.416 -  have "gcd x y dvd x \<and> gcd x y dvd y"
   1.417 -  proof (cases "y = 0")
   1.418 +  have "gcd a b dvd a \<and> gcd a b dvd b"
   1.419 +  proof (cases "b = 0")
   1.420      case True
   1.421 -      then show ?thesis by (cases "x = 0", simp_all add: gcd_0)
   1.422 +      then show ?thesis by (cases "a = 0", simp_all add: gcd_0)
   1.423    next
   1.424      case False
   1.425        with IH1 and IH2 show ?thesis by (simp add: gcd_non_0 dvd_mod_iff)
   1.426    qed
   1.427 -  then show "gcd x y dvd x" "gcd x y dvd y" by simp_all
   1.428 +  then show "gcd a b dvd a" "gcd a b dvd b" by simp_all
   1.429  qed
   1.430  
   1.431  lemma dvd_gcd_D1: "k dvd gcd m n \<Longrightarrow> k dvd m"
   1.432 @@ -443,66 +443,66 @@
   1.433    by (rule dvd_trans, assumption, rule gcd_dvd2)
   1.434  
   1.435  lemma gcd_greatest:
   1.436 -  fixes k x y :: 'a
   1.437 -  shows "k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd gcd x y"
   1.438 -proof (induct x y rule: gcd_eucl.induct)
   1.439 -  case (1 x y)
   1.440 +  fixes k a b :: 'a
   1.441 +  shows "k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd gcd a b"
   1.442 +proof (induct a b rule: gcd_eucl.induct)
   1.443 +  case (1 a b)
   1.444    show ?case
   1.445 -    proof (cases "y = 0")
   1.446 -      assume "y = 0"
   1.447 -      with 1 show ?thesis by (cases "x = 0", simp_all add: gcd_0)
   1.448 +    proof (cases "b = 0")
   1.449 +      assume "b = 0"
   1.450 +      with 1 show ?thesis by (cases "a = 0", simp_all add: gcd_0)
   1.451      next
   1.452 -      assume "y \<noteq> 0"
   1.453 +      assume "b \<noteq> 0"
   1.454        with 1 show ?thesis by (simp add: gcd_non_0 dvd_mod_iff) 
   1.455      qed
   1.456  qed
   1.457  
   1.458  lemma dvd_gcd_iff:
   1.459 -  "k dvd gcd x y \<longleftrightarrow> k dvd x \<and> k dvd y"
   1.460 +  "k dvd gcd a b \<longleftrightarrow> k dvd a \<and> k dvd b"
   1.461    by (blast intro!: gcd_greatest intro: dvd_trans)
   1.462  
   1.463  lemmas gcd_greatest_iff = dvd_gcd_iff
   1.464  
   1.465  lemma gcd_zero [simp]:
   1.466 -  "gcd x y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   1.467 +  "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
   1.468    by (metis dvd_0_left dvd_refl gcd_dvd1 gcd_dvd2 gcd_greatest)+
   1.469  
   1.470  lemma normalisation_factor_gcd [simp]:
   1.471 -  "normalisation_factor (gcd x y) = (if x = 0 \<and> y = 0 then 0 else 1)" (is "?f x y = ?g x y")
   1.472 -proof (induct x y rule: gcd_eucl.induct)
   1.473 -  fix x y :: 'a
   1.474 -  assume IH: "y \<noteq> 0 \<Longrightarrow> ?f y (x mod y) = ?g y (x mod y)"
   1.475 -  then show "?f x y = ?g x y" by (cases "y = 0", auto simp: gcd_non_0 gcd_0)
   1.476 +  "normalisation_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)" (is "?f a b = ?g a b")
   1.477 +proof (induct a b rule: gcd_eucl.induct)
   1.478 +  fix a b :: 'a
   1.479 +  assume IH: "b \<noteq> 0 \<Longrightarrow> ?f b (a mod b) = ?g b (a mod b)"
   1.480 +  then show "?f a b = ?g a b" by (cases "b = 0", auto simp: gcd_non_0 gcd_0)
   1.481  qed
   1.482  
   1.483  lemma gcdI:
   1.484 -  "k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> (\<And>l. l dvd x \<Longrightarrow> l dvd y \<Longrightarrow> l dvd k)
   1.485 -    \<Longrightarrow> normalisation_factor k = (if k = 0 then 0 else 1) \<Longrightarrow> k = gcd x y"
   1.486 +  "k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> (\<And>l. l dvd a \<Longrightarrow> l dvd b \<Longrightarrow> l dvd k)
   1.487 +    \<Longrightarrow> normalisation_factor k = (if k = 0 then 0 else 1) \<Longrightarrow> k = gcd a b"
   1.488    by (intro normed_associated_imp_eq) (auto simp: associated_def intro: gcd_greatest)
   1.489  
   1.490  sublocale gcd!: abel_semigroup gcd
   1.491  proof
   1.492 -  fix x y z 
   1.493 -  show "gcd (gcd x y) z = gcd x (gcd y z)"
   1.494 +  fix a b c 
   1.495 +  show "gcd (gcd a b) c = gcd a (gcd b c)"
   1.496    proof (rule gcdI)
   1.497 -    have "gcd (gcd x y) z dvd gcd x y" "gcd x y dvd x" by simp_all
   1.498 -    then show "gcd (gcd x y) z dvd x" by (rule dvd_trans)
   1.499 -    have "gcd (gcd x y) z dvd gcd x y" "gcd x y dvd y" by simp_all
   1.500 -    hence "gcd (gcd x y) z dvd y" by (rule dvd_trans)
   1.501 -    moreover have "gcd (gcd x y) z dvd z" by simp
   1.502 -    ultimately show "gcd (gcd x y) z dvd gcd y z"
   1.503 +    have "gcd (gcd a b) c dvd gcd a b" "gcd a b dvd a" by simp_all
   1.504 +    then show "gcd (gcd a b) c dvd a" by (rule dvd_trans)
   1.505 +    have "gcd (gcd a b) c dvd gcd a b" "gcd a b dvd b" by simp_all
   1.506 +    hence "gcd (gcd a b) c dvd b" by (rule dvd_trans)
   1.507 +    moreover have "gcd (gcd a b) c dvd c" by simp
   1.508 +    ultimately show "gcd (gcd a b) c dvd gcd b c"
   1.509        by (rule gcd_greatest)
   1.510 -    show "normalisation_factor (gcd (gcd x y) z) =  (if gcd (gcd x y) z = 0 then 0 else 1)"
   1.511 +    show "normalisation_factor (gcd (gcd a b) c) =  (if gcd (gcd a b) c = 0 then 0 else 1)"
   1.512        by auto
   1.513 -    fix l assume "l dvd x" and "l dvd gcd y z"
   1.514 +    fix l assume "l dvd a" and "l dvd gcd b c"
   1.515      with dvd_trans[OF _ gcd_dvd1] and dvd_trans[OF _ gcd_dvd2]
   1.516 -      have "l dvd y" and "l dvd z" by blast+
   1.517 -    with `l dvd x` show "l dvd gcd (gcd x y) z"
   1.518 +      have "l dvd b" and "l dvd c" by blast+
   1.519 +    with `l dvd a` show "l dvd gcd (gcd a b) c"
   1.520        by (intro gcd_greatest)
   1.521    qed
   1.522  next
   1.523 -  fix x y
   1.524 -  show "gcd x y = gcd y x"
   1.525 +  fix a b
   1.526 +  show "gcd a b = gcd b a"
   1.527      by (rule gcdI) (simp_all add: gcd_greatest)
   1.528  qed
   1.529  
   1.530 @@ -514,18 +514,18 @@
   1.531  lemma gcd_dvd_prod: "gcd a b dvd k * b"
   1.532    using mult_dvd_mono [of 1] by auto
   1.533  
   1.534 -lemma gcd_1_left [simp]: "gcd 1 x = 1"
   1.535 +lemma gcd_1_left [simp]: "gcd 1 a = 1"
   1.536    by (rule sym, rule gcdI, simp_all)
   1.537  
   1.538 -lemma gcd_1 [simp]: "gcd x 1 = 1"
   1.539 +lemma gcd_1 [simp]: "gcd a 1 = 1"
   1.540    by (rule sym, rule gcdI, simp_all)
   1.541  
   1.542  lemma gcd_proj2_if_dvd: 
   1.543 -  "y dvd x \<Longrightarrow> gcd x y = y div normalisation_factor y"
   1.544 -  by (cases "y = 0", simp_all add: dvd_eq_mod_eq_0 gcd_non_0 gcd_0)
   1.545 +  "b dvd a \<Longrightarrow> gcd a b = b div normalisation_factor b"
   1.546 +  by (cases "b = 0", simp_all add: dvd_eq_mod_eq_0 gcd_non_0 gcd_0)
   1.547  
   1.548  lemma gcd_proj1_if_dvd: 
   1.549 -  "x dvd y \<Longrightarrow> gcd x y = x div normalisation_factor x"
   1.550 +  "a dvd b \<Longrightarrow> gcd a b = a div normalisation_factor a"
   1.551    by (subst gcd.commute, simp add: gcd_proj2_if_dvd)
   1.552  
   1.553  lemma gcd_proj1_iff: "gcd m n = m div normalisation_factor m \<longleftrightarrow> m dvd n"
   1.554 @@ -547,42 +547,42 @@
   1.555    by (subst gcd.commute, simp add: gcd_proj1_iff)
   1.556  
   1.557  lemma gcd_mod1 [simp]:
   1.558 -  "gcd (x mod y) y = gcd x y"
   1.559 +  "gcd (a mod b) b = gcd a b"
   1.560    by (rule gcdI, metis dvd_mod_iff gcd_dvd1 gcd_dvd2, simp_all add: gcd_greatest dvd_mod_iff)
   1.561  
   1.562  lemma gcd_mod2 [simp]:
   1.563 -  "gcd x (y mod x) = gcd x y"
   1.564 +  "gcd a (b mod a) = gcd a b"
   1.565    by (rule gcdI, simp, metis dvd_mod_iff gcd_dvd1 gcd_dvd2, simp_all add: gcd_greatest dvd_mod_iff)
   1.566           
   1.567  lemma normalisation_factor_dvd' [simp]:
   1.568 -  "normalisation_factor x dvd x"
   1.569 -  by (cases "x = 0", simp_all)
   1.570 +  "normalisation_factor a dvd a"
   1.571 +  by (cases "a = 0", simp_all)
   1.572  
   1.573  lemma gcd_mult_distrib': 
   1.574 -  "k div normalisation_factor k * gcd x y = gcd (k*x) (k*y)"
   1.575 -proof (induct x y rule: gcd_eucl.induct)
   1.576 -  case (1 x y)
   1.577 +  "k div normalisation_factor k * gcd a b = gcd (k*a) (k*b)"
   1.578 +proof (induct a b rule: gcd_eucl.induct)
   1.579 +  case (1 a b)
   1.580    show ?case
   1.581 -  proof (cases "y = 0")
   1.582 +  proof (cases "b = 0")
   1.583      case True
   1.584      then show ?thesis by (simp add: normalisation_factor_mult gcd_0 algebra_simps div_mult_div_if_dvd)
   1.585    next
   1.586      case False
   1.587 -    hence "k div normalisation_factor k * gcd x y =  gcd (k * y) (k * (x mod y))" 
   1.588 +    hence "k div normalisation_factor k * gcd a b =  gcd (k * b) (k * (a mod b))" 
   1.589        using 1 by (subst gcd_red, simp)
   1.590 -    also have "... = gcd (k * x) (k * y)"
   1.591 +    also have "... = gcd (k * a) (k * b)"
   1.592        by (simp add: mult_mod_right gcd.commute)
   1.593      finally show ?thesis .
   1.594    qed
   1.595  qed
   1.596  
   1.597  lemma gcd_mult_distrib:
   1.598 -  "k * gcd x y = gcd (k*x) (k*y) * normalisation_factor k"
   1.599 +  "k * gcd a b = gcd (k*a) (k*b) * normalisation_factor k"
   1.600  proof-
   1.601    let ?nf = "normalisation_factor"
   1.602    from gcd_mult_distrib' 
   1.603 -    have "gcd (k*x) (k*y) = k div ?nf k * gcd x y" ..
   1.604 -  also have "... = k * gcd x y div ?nf k"
   1.605 +    have "gcd (k*a) (k*b) = k div ?nf k * gcd a b" ..
   1.606 +  also have "... = k * gcd a b div ?nf k"
   1.607      by (metis dvd_div_mult dvd_eq_mod_eq_0 mod_0 normalisation_factor_dvd)
   1.608    finally show ?thesis
   1.609      by simp
   1.610 @@ -618,7 +618,7 @@
   1.611    shows "euclidean_size (gcd a b) < euclidean_size b"
   1.612    using assms by (subst gcd.commute, rule euclidean_size_gcd_less1)
   1.613  
   1.614 -lemma gcd_mult_unit1: "is_unit a \<Longrightarrow> gcd (x*a) y = gcd x y"
   1.615 +lemma gcd_mult_unit1: "is_unit a \<Longrightarrow> gcd (b * a) c = gcd b c"
   1.616    apply (rule gcdI)
   1.617    apply (rule dvd_trans, rule gcd_dvd1, simp add: unit_simps)
   1.618    apply (rule gcd_dvd2)
   1.619 @@ -626,19 +626,19 @@
   1.620    apply (subst normalisation_factor_gcd, simp add: gcd_0)
   1.621    done
   1.622  
   1.623 -lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd x (y*a) = gcd x y"
   1.624 +lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c"
   1.625    by (subst gcd.commute, subst gcd_mult_unit1, assumption, rule gcd.commute)
   1.626  
   1.627 -lemma gcd_div_unit1: "is_unit a \<Longrightarrow> gcd (x div a) y = gcd x y"
   1.628 +lemma gcd_div_unit1: "is_unit a \<Longrightarrow> gcd (b div a) c = gcd b c"
   1.629    by (simp add: unit_ring_inv gcd_mult_unit1)
   1.630  
   1.631 -lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd x (y div a) = gcd x y"
   1.632 +lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c"
   1.633    by (simp add: unit_ring_inv gcd_mult_unit2)
   1.634  
   1.635 -lemma gcd_idem: "gcd x x = x div normalisation_factor x"
   1.636 -  by (cases "x = 0") (simp add: gcd_0_left, rule sym, rule gcdI, simp_all)
   1.637 +lemma gcd_idem: "gcd a a = a div normalisation_factor a"
   1.638 +  by (cases "a = 0") (simp add: gcd_0_left, rule sym, rule gcdI, simp_all)
   1.639  
   1.640 -lemma gcd_right_idem: "gcd (gcd p q) q = gcd p q"
   1.641 +lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b"
   1.642    apply (rule gcdI)
   1.643    apply (simp add: ac_simps)
   1.644    apply (rule gcd_dvd2)
   1.645 @@ -646,7 +646,7 @@
   1.646    apply simp
   1.647    done
   1.648  
   1.649 -lemma gcd_left_idem: "gcd p (gcd p q) = gcd p q"
   1.650 +lemma gcd_left_idem: "gcd a (gcd a b) = gcd a b"
   1.651    apply (rule gcdI)
   1.652    apply simp
   1.653    apply (rule dvd_trans, rule gcd_dvd2, rule gcd_dvd2)
   1.654 @@ -664,17 +664,17 @@
   1.655  qed
   1.656  
   1.657  lemma coprime_dvd_mult:
   1.658 -  assumes "gcd k n = 1" and "k dvd m * n"
   1.659 -  shows "k dvd m"
   1.660 +  assumes "gcd c b = 1" and "c dvd a * b"
   1.661 +  shows "c dvd a"
   1.662  proof -
   1.663    let ?nf = "normalisation_factor"
   1.664 -  from assms gcd_mult_distrib [of m k n] 
   1.665 -    have A: "m = gcd (m * k) (m * n) * ?nf m" by simp
   1.666 -  from `k dvd m * n` show ?thesis by (subst A, simp_all add: gcd_greatest)
   1.667 +  from assms gcd_mult_distrib [of a c b] 
   1.668 +    have A: "a = gcd (a * c) (a * b) * ?nf a" by simp
   1.669 +  from `c dvd a * b` show ?thesis by (subst A, simp_all add: gcd_greatest)
   1.670  qed
   1.671  
   1.672  lemma coprime_dvd_mult_iff:
   1.673 -  "gcd k n = 1 \<Longrightarrow> (k dvd m * n) = (k dvd m)"
   1.674 +  "gcd c b = 1 \<Longrightarrow> (c dvd a * b) = (c dvd a)"
   1.675    by (rule, rule coprime_dvd_mult, simp_all)
   1.676  
   1.677  lemma gcd_dvd_antisym:
   1.678 @@ -737,7 +737,7 @@
   1.679  lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
   1.680    by (subst gcd.commute, subst gcd_red, simp)
   1.681  
   1.682 -lemma coprimeI: "(\<And>l. \<lbrakk>l dvd x; l dvd y\<rbrakk> \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd x y = 1"
   1.683 +lemma coprimeI: "(\<And>l. \<lbrakk>l dvd a; l dvd b\<rbrakk> \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd a b = 1"
   1.684    by (rule sym, rule gcdI, simp_all)
   1.685  
   1.686  lemma coprime: "gcd a b = 1 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)"
   1.687 @@ -796,10 +796,10 @@
   1.688    using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b] by blast
   1.689  
   1.690  lemma gcd_coprime:
   1.691 -  assumes z: "gcd a b \<noteq> 0" and a: "a = a' * gcd a b" and b: "b = b' * gcd a b"
   1.692 +  assumes c: "gcd a b \<noteq> 0" and a: "a = a' * gcd a b" and b: "b = b' * gcd a b"
   1.693    shows "gcd a' b' = 1"
   1.694  proof -
   1.695 -  from z have "a \<noteq> 0 \<or> b \<noteq> 0" by simp
   1.696 +  from c have "a \<noteq> 0 \<or> b \<noteq> 0" by simp
   1.697    with div_gcd_coprime have "gcd (a div gcd a b) (b div gcd a b) = 1" .
   1.698    also from assms have "a div gcd a b = a'" by (metis div_mult_self2_is_id)+
   1.699    also from assms have "b div gcd a b = b'" by (metis div_mult_self2_is_id)+
   1.700 @@ -856,8 +856,8 @@
   1.701  qed
   1.702  
   1.703  lemma coprime_common_divisor: 
   1.704 -  "gcd a b = 1 \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> is_unit x"
   1.705 -  apply (subgoal_tac "x dvd gcd a b")
   1.706 +  "gcd a b = 1 \<Longrightarrow> a dvd a \<Longrightarrow> a dvd b \<Longrightarrow> is_unit a"
   1.707 +  apply (subgoal_tac "a dvd gcd a b")
   1.708    apply simp
   1.709    apply (erule (1) gcd_greatest)
   1.710    done
   1.711 @@ -935,7 +935,7 @@
   1.712    by (subst add_commute, simp)
   1.713  
   1.714  lemma setprod_coprime [rule_format]:
   1.715 -  "(\<forall>i\<in>A. gcd (f i) x = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) x = 1"
   1.716 +  "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
   1.717    apply (cases "finite A")
   1.718    apply (induct set: finite)
   1.719    apply (auto simp add: gcd_mult_cancel)
   1.720 @@ -955,14 +955,14 @@
   1.721  qed
   1.722  
   1.723  lemma invertible_coprime:
   1.724 -  assumes "x * y mod m = 1"
   1.725 -  shows "coprime x m"
   1.726 +  assumes "a * b mod m = 1"
   1.727 +  shows "coprime a m"
   1.728  proof -
   1.729 -  from assms have "coprime m (x * y mod m)"
   1.730 +  from assms have "coprime m (a * b mod m)"
   1.731      by simp
   1.732 -  then have "coprime m (x * y)"
   1.733 +  then have "coprime m (a * b)"
   1.734      by simp
   1.735 -  then have "coprime m x"
   1.736 +  then have "coprime m a"
   1.737      by (rule coprime_lmult)
   1.738    then show ?thesis
   1.739      by (simp add: ac_simps)
   1.740 @@ -986,18 +986,18 @@
   1.741  qed (auto simp add: lcm_gcd)
   1.742  
   1.743  lemma lcm_dvd1 [iff]:
   1.744 -  "x dvd lcm x y"
   1.745 -proof (cases "x*y = 0")
   1.746 -  assume "x * y \<noteq> 0"
   1.747 -  hence "gcd x y \<noteq> 0" by simp
   1.748 -  let ?c = "ring_inv (normalisation_factor (x*y))"
   1.749 -  from `x * y \<noteq> 0` have [simp]: "is_unit (normalisation_factor (x*y))" by simp
   1.750 -  from lcm_gcd_prod[of x y] have "lcm x y * gcd x y = x * ?c * y"
   1.751 +  "a dvd lcm a b"
   1.752 +proof (cases "a*b = 0")
   1.753 +  assume "a * b \<noteq> 0"
   1.754 +  hence "gcd a b \<noteq> 0" by simp
   1.755 +  let ?c = "ring_inv (normalisation_factor (a*b))"
   1.756 +  from `a * b \<noteq> 0` have [simp]: "is_unit (normalisation_factor (a*b))" by simp
   1.757 +  from lcm_gcd_prod[of a b] have "lcm a b * gcd a b = a * ?c * b"
   1.758      by (simp add: mult_ac unit_ring_inv)
   1.759 -  hence "lcm x y * gcd x y div gcd x y = x * ?c * y div gcd x y" by simp
   1.760 -  with `gcd x y \<noteq> 0` have "lcm x y = x * ?c * y div gcd x y"
   1.761 +  hence "lcm a b * gcd a b div gcd a b = a * ?c * b div gcd a b" by simp
   1.762 +  with `gcd a b \<noteq> 0` have "lcm a b = a * ?c * b div gcd a b"
   1.763      by (subst (asm) div_mult_self2_is_id, simp_all)
   1.764 -  also have "... = x * (?c * y div gcd x y)"
   1.765 +  also have "... = a * (?c * b div gcd a b)"
   1.766      by (metis div_mult_swap gcd_dvd2 mult_assoc)
   1.767    finally show ?thesis by (rule dvdI)
   1.768  qed (auto simp add: lcm_gcd)
   1.769 @@ -1093,38 +1093,38 @@
   1.770    finally show ?thesis using False by simp
   1.771  qed
   1.772  
   1.773 -lemma lcm_dvd2 [iff]: "y dvd lcm x y"
   1.774 -  using lcm_dvd1 [of y x] by (simp add: lcm_gcd ac_simps)
   1.775 +lemma lcm_dvd2 [iff]: "b dvd lcm a b"
   1.776 +  using lcm_dvd1 [of b a] by (simp add: lcm_gcd ac_simps)
   1.777  
   1.778  lemma lcmI:
   1.779 -  "\<lbrakk>x dvd k; y dvd k; \<And>l. x dvd l \<Longrightarrow> y dvd l \<Longrightarrow> k dvd l;
   1.780 -    normalisation_factor k = (if k = 0 then 0 else 1)\<rbrakk> \<Longrightarrow> k = lcm x y"
   1.781 +  "\<lbrakk>a dvd k; b dvd k; \<And>l. a dvd l \<Longrightarrow> b dvd l \<Longrightarrow> k dvd l;
   1.782 +    normalisation_factor k = (if k = 0 then 0 else 1)\<rbrakk> \<Longrightarrow> k = lcm a b"
   1.783    by (intro normed_associated_imp_eq) (auto simp: associated_def intro: lcm_least)
   1.784  
   1.785  sublocale lcm!: abel_semigroup lcm
   1.786  proof
   1.787 -  fix x y z
   1.788 -  show "lcm (lcm x y) z = lcm x (lcm y z)"
   1.789 +  fix a b c
   1.790 +  show "lcm (lcm a b) c = lcm a (lcm b c)"
   1.791    proof (rule lcmI)
   1.792 -    have "x dvd lcm x y" and "lcm x y dvd lcm (lcm x y) z" by simp_all
   1.793 -    then show "x dvd lcm (lcm x y) z" by (rule dvd_trans)
   1.794 +    have "a dvd lcm a b" and "lcm a b dvd lcm (lcm a b) c" by simp_all
   1.795 +    then show "a dvd lcm (lcm a b) c" by (rule dvd_trans)
   1.796      
   1.797 -    have "y dvd lcm x y" and "lcm x y dvd lcm (lcm x y) z" by simp_all
   1.798 -    hence "y dvd lcm (lcm x y) z" by (rule dvd_trans)
   1.799 -    moreover have "z dvd lcm (lcm x y) z" by simp
   1.800 -    ultimately show "lcm y z dvd lcm (lcm x y) z" by (rule lcm_least)
   1.801 +    have "b dvd lcm a b" and "lcm a b dvd lcm (lcm a b) c" by simp_all
   1.802 +    hence "b dvd lcm (lcm a b) c" by (rule dvd_trans)
   1.803 +    moreover have "c dvd lcm (lcm a b) c" by simp
   1.804 +    ultimately show "lcm b c dvd lcm (lcm a b) c" by (rule lcm_least)
   1.805  
   1.806 -    fix l assume "x dvd l" and "lcm y z dvd l"
   1.807 -    have "y dvd lcm y z" by simp
   1.808 -    from this and `lcm y z dvd l` have "y dvd l" by (rule dvd_trans)
   1.809 -    have "z dvd lcm y z" by simp
   1.810 -    from this and `lcm y z dvd l` have "z dvd l" by (rule dvd_trans)
   1.811 -    from `x dvd l` and `y dvd l` have "lcm x y dvd l" by (rule lcm_least)
   1.812 -    from this and `z dvd l` show "lcm (lcm x y) z dvd l" by (rule lcm_least)
   1.813 +    fix l assume "a dvd l" and "lcm b c dvd l"
   1.814 +    have "b dvd lcm b c" by simp
   1.815 +    from this and `lcm b c dvd l` have "b dvd l" by (rule dvd_trans)
   1.816 +    have "c dvd lcm b c" by simp
   1.817 +    from this and `lcm b c dvd l` have "c dvd l" by (rule dvd_trans)
   1.818 +    from `a dvd l` and `b dvd l` have "lcm a b dvd l" by (rule lcm_least)
   1.819 +    from this and `c dvd l` show "lcm (lcm a b) c dvd l" by (rule lcm_least)
   1.820    qed (simp add: lcm_zero)
   1.821  next
   1.822 -  fix x y
   1.823 -  show "lcm x y = lcm y x"
   1.824 +  fix a b
   1.825 +  show "lcm a b = lcm b a"
   1.826      by (simp add: lcm_gcd ac_simps)
   1.827  qed
   1.828  
   1.829 @@ -1157,11 +1157,11 @@
   1.830  qed
   1.831  
   1.832  lemma lcm_0_left [simp]:
   1.833 -  "lcm 0 x = 0"
   1.834 +  "lcm 0 a = 0"
   1.835    by (rule sym, rule lcmI, simp_all)
   1.836  
   1.837  lemma lcm_0 [simp]:
   1.838 -  "lcm x 0 = 0"
   1.839 +  "lcm a 0 = 0"
   1.840    by (rule sym, rule lcmI, simp_all)
   1.841  
   1.842  lemma lcm_unique:
   1.843 @@ -1179,24 +1179,24 @@
   1.844    by (metis lcm_dvd2 dvd_trans)
   1.845  
   1.846  lemma lcm_1_left [simp]:
   1.847 -  "lcm 1 x = x div normalisation_factor x"
   1.848 -  by (cases "x = 0") (simp, rule sym, rule lcmI, simp_all)
   1.849 +  "lcm 1 a = a div normalisation_factor a"
   1.850 +  by (cases "a = 0") (simp, rule sym, rule lcmI, simp_all)
   1.851  
   1.852  lemma lcm_1_right [simp]:
   1.853 -  "lcm x 1 = x div normalisation_factor x"
   1.854 -  by (simp add: ac_simps)
   1.855 +  "lcm a 1 = a div normalisation_factor a"
   1.856 +  using lcm_1_left [of a] by (simp add: ac_simps)
   1.857  
   1.858  lemma lcm_coprime:
   1.859    "gcd a b = 1 \<Longrightarrow> lcm a b = a * b div normalisation_factor (a*b)"
   1.860    by (subst lcm_gcd) simp
   1.861  
   1.862  lemma lcm_proj1_if_dvd: 
   1.863 -  "y dvd x \<Longrightarrow> lcm x y = x div normalisation_factor x"
   1.864 -  by (cases "x = 0") (simp, rule sym, rule lcmI, simp_all)
   1.865 +  "b dvd a \<Longrightarrow> lcm a b = a div normalisation_factor a"
   1.866 +  by (cases "a = 0") (simp, rule sym, rule lcmI, simp_all)
   1.867  
   1.868  lemma lcm_proj2_if_dvd: 
   1.869 -  "x dvd y \<Longrightarrow> lcm x y = y div normalisation_factor y"
   1.870 -  using lcm_proj1_if_dvd [of x y] by (simp add: ac_simps)
   1.871 +  "a dvd b \<Longrightarrow> lcm a b = b div normalisation_factor b"
   1.872 +  using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps)
   1.873  
   1.874  lemma lcm_proj1_iff:
   1.875    "lcm m n = m div normalisation_factor m \<longleftrightarrow> n dvd m"
   1.876 @@ -1252,28 +1252,28 @@
   1.877    using assms euclidean_size_lcm_less1 [of a b] by (simp add: ac_simps)
   1.878  
   1.879  lemma lcm_mult_unit1:
   1.880 -  "is_unit a \<Longrightarrow> lcm (x*a) y = lcm x y"
   1.881 +  "is_unit a \<Longrightarrow> lcm (b * a) c = lcm b c"
   1.882    apply (rule lcmI)
   1.883 -  apply (rule dvd_trans[of _ "x*a"], simp, rule lcm_dvd1)
   1.884 +  apply (rule dvd_trans[of _ "b * a"], simp, rule lcm_dvd1)
   1.885    apply (rule lcm_dvd2)
   1.886    apply (rule lcm_least, simp add: unit_simps, assumption)
   1.887    apply (subst normalisation_factor_lcm, simp add: lcm_zero)
   1.888    done
   1.889  
   1.890  lemma lcm_mult_unit2:
   1.891 -  "is_unit a \<Longrightarrow> lcm x (y*a) = lcm x y"
   1.892 -  using lcm_mult_unit1 [of a y x] by (simp add: ac_simps)
   1.893 +  "is_unit a \<Longrightarrow> lcm b (c * a) = lcm b c"
   1.894 +  using lcm_mult_unit1 [of a c b] by (simp add: ac_simps)
   1.895  
   1.896  lemma lcm_div_unit1:
   1.897 -  "is_unit a \<Longrightarrow> lcm (x div a) y = lcm x y"
   1.898 +  "is_unit a \<Longrightarrow> lcm (b div a) c = lcm b c"
   1.899    by (simp add: unit_ring_inv lcm_mult_unit1)
   1.900  
   1.901  lemma lcm_div_unit2:
   1.902 -  "is_unit a \<Longrightarrow> lcm x (y div a) = lcm x y"
   1.903 +  "is_unit a \<Longrightarrow> lcm b (c div a) = lcm b c"
   1.904    by (simp add: unit_ring_inv lcm_mult_unit2)
   1.905  
   1.906  lemma lcm_left_idem:
   1.907 -  "lcm p (lcm p q) = lcm p q"
   1.908 +  "lcm a (lcm a b) = lcm a b"
   1.909    apply (rule lcmI)
   1.910    apply simp
   1.911    apply (subst lcm.assoc [symmetric], rule lcm_dvd2)
   1.912 @@ -1283,7 +1283,7 @@
   1.913    done
   1.914  
   1.915  lemma lcm_right_idem:
   1.916 -  "lcm (lcm p q) q = lcm p q"
   1.917 +  "lcm (lcm a b) b = lcm a b"
   1.918    apply (rule lcmI)
   1.919    apply (subst lcm.assoc, rule lcm_dvd1)
   1.920    apply (rule lcm_dvd2)
   1.921 @@ -1300,35 +1300,35 @@
   1.922      by (intro ext, simp add: lcm_left_idem)
   1.923  qed
   1.924  
   1.925 -lemma dvd_Lcm [simp]: "x \<in> A \<Longrightarrow> x dvd Lcm A"
   1.926 -  and Lcm_dvd [simp]: "(\<forall>x\<in>A. x dvd l') \<Longrightarrow> Lcm A dvd l'"
   1.927 +lemma dvd_Lcm [simp]: "a \<in> A \<Longrightarrow> a dvd Lcm A"
   1.928 +  and Lcm_dvd [simp]: "(\<forall>a\<in>A. a dvd l') \<Longrightarrow> Lcm A dvd l'"
   1.929    and normalisation_factor_Lcm [simp]: 
   1.930            "normalisation_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
   1.931  proof -
   1.932 -  have "(\<forall>x\<in>A. x dvd Lcm A) \<and> (\<forall>l'. (\<forall>x\<in>A. x dvd l') \<longrightarrow> Lcm A dvd l') \<and>
   1.933 +  have "(\<forall>a\<in>A. a dvd Lcm A) \<and> (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> Lcm A dvd l') \<and>
   1.934      normalisation_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" (is ?thesis)
   1.935 -  proof (cases "\<exists>l. l \<noteq>  0 \<and> (\<forall>x\<in>A. x dvd l)")
   1.936 +  proof (cases "\<exists>l. l \<noteq>  0 \<and> (\<forall>a\<in>A. a dvd l)")
   1.937      case False
   1.938      hence "Lcm A = 0" by (auto simp: Lcm_Lcm_eucl Lcm_eucl_def)
   1.939      with False show ?thesis by auto
   1.940    next
   1.941      case True
   1.942 -    then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l\<^sub>0)" by blast
   1.943 -    def n \<equiv> "LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l) \<and> euclidean_size l = n"
   1.944 -    def l \<equiv> "SOME l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l) \<and> euclidean_size l = n"
   1.945 -    have "\<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l) \<and> euclidean_size l = n"
   1.946 +    then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l\<^sub>0)" by blast
   1.947 +    def n \<equiv> "LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
   1.948 +    def l \<equiv> "SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
   1.949 +    have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
   1.950        apply (subst n_def)
   1.951        apply (rule LeastI[of _ "euclidean_size l\<^sub>0"])
   1.952        apply (rule exI[of _ l\<^sub>0])
   1.953        apply (simp add: l\<^sub>0_props)
   1.954        done
   1.955 -    from someI_ex[OF this] have "l \<noteq> 0" and "\<forall>x\<in>A. x dvd l" and "euclidean_size l = n" 
   1.956 +    from someI_ex[OF this] have "l \<noteq> 0" and "\<forall>a\<in>A. a dvd l" and "euclidean_size l = n" 
   1.957        unfolding l_def by simp_all
   1.958      {
   1.959 -      fix l' assume "\<forall>x\<in>A. x dvd l'"
   1.960 -      with `\<forall>x\<in>A. x dvd l` have "\<forall>x\<in>A. x dvd gcd l l'" by (auto intro: gcd_greatest)
   1.961 +      fix l' assume "\<forall>a\<in>A. a dvd l'"
   1.962 +      with `\<forall>a\<in>A. a dvd l` have "\<forall>a\<in>A. a dvd gcd l l'" by (auto intro: gcd_greatest)
   1.963        moreover from `l \<noteq> 0` have "gcd l l' \<noteq> 0" by simp
   1.964 -      ultimately have "\<exists>b. b \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd b) \<and> euclidean_size b = euclidean_size (gcd l l')"
   1.965 +      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.966          by (intro exI[of _ "gcd l l'"], auto)
   1.967        hence "euclidean_size (gcd l l') \<ge> n" by (subst n_def) (rule Least_le)
   1.968        moreover have "euclidean_size (gcd l l') \<le> n"
   1.969 @@ -1348,9 +1348,9 @@
   1.970        hence "l dvd l'" by (blast dest: dvd_gcd_D2)
   1.971      }
   1.972  
   1.973 -    with `(\<forall>x\<in>A. x dvd l)` and normalisation_factor_is_unit[OF `l \<noteq> 0`] and `l \<noteq> 0`
   1.974 -      have "(\<forall>x\<in>A. x dvd l div normalisation_factor l) \<and> 
   1.975 -        (\<forall>l'. (\<forall>x\<in>A. x dvd l') \<longrightarrow> l div normalisation_factor l dvd l') \<and>
   1.976 +    with `(\<forall>a\<in>A. a dvd l)` and normalisation_factor_is_unit[OF `l \<noteq> 0`] and `l \<noteq> 0`
   1.977 +      have "(\<forall>a\<in>A. a dvd l div normalisation_factor l) \<and> 
   1.978 +        (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> l div normalisation_factor l dvd l') \<and>
   1.979          normalisation_factor (l div normalisation_factor l) = 
   1.980          (if l div normalisation_factor l = 0 then 0 else 1)"
   1.981        by (auto simp: unit_simps)
   1.982 @@ -1360,13 +1360,13 @@
   1.983    qed
   1.984    note A = this
   1.985  
   1.986 -  {fix x assume "x \<in> A" then show "x dvd Lcm A" using A by blast}
   1.987 -  {fix l' assume "\<forall>x\<in>A. x dvd l'" then show "Lcm A dvd l'" using A by blast}
   1.988 +  {fix a assume "a \<in> A" then show "a dvd Lcm A" using A by blast}
   1.989 +  {fix l' assume "\<forall>a\<in>A. a dvd l'" then show "Lcm A dvd l'" using A by blast}
   1.990    from A show "normalisation_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" by blast
   1.991  qed
   1.992      
   1.993  lemma LcmI:
   1.994 -  "(\<And>x. x\<in>A \<Longrightarrow> x dvd l) \<Longrightarrow> (\<And>l'. (\<forall>x\<in>A. x dvd l') \<Longrightarrow> l dvd l') \<Longrightarrow>
   1.995 +  "(\<And>a. a\<in>A \<Longrightarrow> a dvd l) \<Longrightarrow> (\<And>l'. (\<forall>a\<in>A. a dvd l') \<Longrightarrow> l dvd l') \<Longrightarrow>
   1.996        normalisation_factor l = (if l = 0 then 0 else 1) \<Longrightarrow> l = Lcm A"
   1.997    by (intro normed_associated_imp_eq)
   1.998      (auto intro: Lcm_dvd dvd_Lcm simp: associated_def)
   1.999 @@ -1387,19 +1387,19 @@
  1.1000    done
  1.1001  
  1.1002  lemma Lcm_1_iff:
  1.1003 -  "Lcm A = 1 \<longleftrightarrow> (\<forall>x\<in>A. is_unit x)"
  1.1004 +  "Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)"
  1.1005  proof
  1.1006    assume "Lcm A = 1"
  1.1007 -  then show "\<forall>x\<in>A. is_unit x" by auto
  1.1008 +  then show "\<forall>a\<in>A. is_unit a" by auto
  1.1009  qed (rule LcmI [symmetric], auto)
  1.1010  
  1.1011  lemma Lcm_no_units:
  1.1012 -  "Lcm A = Lcm (A - {x. is_unit x})"
  1.1013 +  "Lcm A = Lcm (A - {a. is_unit a})"
  1.1014  proof -
  1.1015 -  have "(A - {x. is_unit x}) \<union> {x\<in>A. is_unit x} = A" by blast
  1.1016 -  hence "Lcm A = lcm (Lcm (A - {x. is_unit x})) (Lcm {x\<in>A. is_unit x})"
  1.1017 +  have "(A - {a. is_unit a}) \<union> {a\<in>A. is_unit a} = A" by blast
  1.1018 +  hence "Lcm A = lcm (Lcm (A - {a. is_unit a})) (Lcm {a\<in>A. is_unit a})"
  1.1019      by (simp add: Lcm_Un[symmetric])
  1.1020 -  also have "Lcm {x\<in>A. is_unit x} = 1" by (simp add: Lcm_1_iff)
  1.1021 +  also have "Lcm {a\<in>A. is_unit a} = 1" by (simp add: Lcm_1_iff)
  1.1022    finally show ?thesis by simp
  1.1023  qed
  1.1024  
  1.1025 @@ -1412,16 +1412,16 @@
  1.1026    by (drule dvd_Lcm) simp
  1.1027  
  1.1028  lemma Lcm0_iff':
  1.1029 -  "Lcm A = 0 \<longleftrightarrow> \<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l))"
  1.1030 +  "Lcm A = 0 \<longleftrightarrow> \<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
  1.1031  proof
  1.1032    assume "Lcm A = 0"
  1.1033 -  show "\<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l))"
  1.1034 +  show "\<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
  1.1035    proof
  1.1036 -    assume ex: "\<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l)"
  1.1037 -    then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l\<^sub>0)" by blast
  1.1038 -    def n \<equiv> "LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l) \<and> euclidean_size l = n"
  1.1039 -    def l \<equiv> "SOME l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l) \<and> euclidean_size l = n"
  1.1040 -    have "\<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l) \<and> euclidean_size l = n"
  1.1041 +    assume ex: "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l)"
  1.1042 +    then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l\<^sub>0)" by blast
  1.1043 +    def n \<equiv> "LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
  1.1044 +    def l \<equiv> "SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
  1.1045 +    have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
  1.1046        apply (subst n_def)
  1.1047        apply (rule LeastI[of _ "euclidean_size l\<^sub>0"])
  1.1048        apply (rule exI[of _ l\<^sub>0])
  1.1049 @@ -1449,18 +1449,18 @@
  1.1050        apply (rule no_zero_divisors)
  1.1051        apply blast+
  1.1052        done
  1.1053 -    moreover from `finite A` have "\<forall>x\<in>A. x dvd \<Prod>A" by blast
  1.1054 -    ultimately have "\<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l)" by blast
  1.1055 +    moreover from `finite A` have "\<forall>a\<in>A. a dvd \<Prod>A" by blast
  1.1056 +    ultimately have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l)" by blast
  1.1057      with Lcm0_iff' have "Lcm A \<noteq> 0" by simp
  1.1058    }
  1.1059    ultimately show "Lcm A = 0 \<longleftrightarrow> 0 \<in> A" by blast
  1.1060  qed
  1.1061  
  1.1062  lemma Lcm_no_multiple:
  1.1063 -  "(\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>x\<in>A. \<not>x dvd m)) \<Longrightarrow> Lcm A = 0"
  1.1064 +  "(\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not>a dvd m)) \<Longrightarrow> Lcm A = 0"
  1.1065  proof -
  1.1066 -  assume "\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>x\<in>A. \<not>x dvd m)"
  1.1067 -  hence "\<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l))" by blast
  1.1068 +  assume "\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not>a dvd m)"
  1.1069 +  hence "\<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))" by blast
  1.1070    then show "Lcm A = 0" by (simp only: Lcm_Lcm_eucl Lcm_eucl_def if_False)
  1.1071  qed
  1.1072  
  1.1073 @@ -1468,7 +1468,7 @@
  1.1074    "Lcm (insert a A) = lcm a (Lcm A)"
  1.1075  proof (rule lcmI)
  1.1076    fix l assume "a dvd l" and "Lcm A dvd l"
  1.1077 -  hence "\<forall>x\<in>A. x dvd l" by (blast intro: dvd_trans dvd_Lcm)
  1.1078 +  hence "\<forall>a\<in>A. a dvd l" by (blast intro: dvd_trans dvd_Lcm)
  1.1079    with `a dvd l` show "Lcm (insert a A) dvd l" by (force intro: Lcm_dvd)
  1.1080  qed (auto intro: Lcm_dvd dvd_Lcm)
  1.1081   
  1.1082 @@ -1512,20 +1512,20 @@
  1.1083    by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
  1.1084  
  1.1085  lemma Gcd_Lcm:
  1.1086 -  "Gcd A = Lcm {d. \<forall>x\<in>A. d dvd x}"
  1.1087 +  "Gcd A = Lcm {d. \<forall>a\<in>A. d dvd a}"
  1.1088    by (simp add: Gcd_Gcd_eucl Lcm_Lcm_eucl Gcd_eucl_def)
  1.1089  
  1.1090 -lemma Gcd_dvd [simp]: "x \<in> A \<Longrightarrow> Gcd A dvd x"
  1.1091 -  and dvd_Gcd [simp]: "(\<forall>x\<in>A. g' dvd x) \<Longrightarrow> g' dvd Gcd A"
  1.1092 +lemma Gcd_dvd [simp]: "a \<in> A \<Longrightarrow> Gcd A dvd a"
  1.1093 +  and dvd_Gcd [simp]: "(\<forall>a\<in>A. g' dvd a) \<Longrightarrow> g' dvd Gcd A"
  1.1094    and normalisation_factor_Gcd [simp]: 
  1.1095      "normalisation_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
  1.1096  proof -
  1.1097 -  fix x assume "x \<in> A"
  1.1098 -  hence "Lcm {d. \<forall>x\<in>A. d dvd x} dvd x" by (intro Lcm_dvd) blast
  1.1099 -  then show "Gcd A dvd x" by (simp add: Gcd_Lcm)
  1.1100 +  fix a assume "a \<in> A"
  1.1101 +  hence "Lcm {d. \<forall>a\<in>A. d dvd a} dvd a" by (intro Lcm_dvd) blast
  1.1102 +  then show "Gcd A dvd a" by (simp add: Gcd_Lcm)
  1.1103  next
  1.1104 -  fix g' assume "\<forall>x\<in>A. g' dvd x"
  1.1105 -  hence "g' dvd Lcm {d. \<forall>x\<in>A. d dvd x}" by (intro dvd_Lcm) blast
  1.1106 +  fix g' assume "\<forall>a\<in>A. g' dvd a"
  1.1107 +  hence "g' dvd Lcm {d. \<forall>a\<in>A. d dvd a}" by (intro dvd_Lcm) blast
  1.1108    then show "g' dvd Gcd A" by (simp add: Gcd_Lcm)
  1.1109  next
  1.1110    show "normalisation_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
  1.1111 @@ -1533,13 +1533,13 @@
  1.1112  qed
  1.1113  
  1.1114  lemma GcdI:
  1.1115 -  "(\<And>x. x\<in>A \<Longrightarrow> l dvd x) \<Longrightarrow> (\<And>l'. (\<forall>x\<in>A. l' dvd x) \<Longrightarrow> l' dvd l) \<Longrightarrow>
  1.1116 +  "(\<And>a. a\<in>A \<Longrightarrow> l dvd a) \<Longrightarrow> (\<And>l'. (\<forall>a\<in>A. l' dvd a) \<Longrightarrow> l' dvd l) \<Longrightarrow>
  1.1117      normalisation_factor l = (if l = 0 then 0 else 1) \<Longrightarrow> l = Gcd A"
  1.1118    by (intro normed_associated_imp_eq)
  1.1119      (auto intro: Gcd_dvd dvd_Gcd simp: associated_def)
  1.1120  
  1.1121  lemma Lcm_Gcd:
  1.1122 -  "Lcm A = Gcd {m. \<forall>x\<in>A. x dvd m}"
  1.1123 +  "Lcm A = Gcd {m. \<forall>a\<in>A. a dvd m}"
  1.1124    by (rule LcmI[symmetric]) (auto intro: dvd_Gcd Gcd_dvd)
  1.1125  
  1.1126  lemma Gcd_0_iff:
  1.1127 @@ -1561,7 +1561,7 @@
  1.1128    "Gcd (insert a A) = gcd a (Gcd A)"
  1.1129  proof (rule gcdI)
  1.1130    fix l assume "l dvd a" and "l dvd Gcd A"
  1.1131 -  hence "\<forall>x\<in>A. l dvd x" by (blast intro: dvd_trans Gcd_dvd)
  1.1132 +  hence "\<forall>a\<in>A. l dvd a" by (blast intro: dvd_trans Gcd_dvd)
  1.1133    with `l dvd a` show "l dvd Gcd (insert a A)" by (force intro: Gcd_dvd)
  1.1134  qed auto
  1.1135  
  1.1136 @@ -1596,19 +1596,19 @@
  1.1137  subclass euclidean_ring ..
  1.1138  
  1.1139  lemma gcd_neg1 [simp]:
  1.1140 -  "gcd (-x) y = gcd x y"
  1.1141 +  "gcd (-a) b = gcd a b"
  1.1142    by (rule sym, rule gcdI, simp_all add: gcd_greatest)
  1.1143  
  1.1144  lemma gcd_neg2 [simp]:
  1.1145 -  "gcd x (-y) = gcd x y"
  1.1146 +  "gcd a (-b) = gcd a b"
  1.1147    by (rule sym, rule gcdI, simp_all add: gcd_greatest)
  1.1148  
  1.1149  lemma gcd_neg_numeral_1 [simp]:
  1.1150 -  "gcd (- numeral n) x = gcd (numeral n) x"
  1.1151 +  "gcd (- numeral n) a = gcd (numeral n) a"
  1.1152    by (fact gcd_neg1)
  1.1153  
  1.1154  lemma gcd_neg_numeral_2 [simp]:
  1.1155 -  "gcd x (- numeral n) = gcd x (numeral n)"
  1.1156 +  "gcd a (- numeral n) = gcd a (numeral n)"
  1.1157    by (fact gcd_neg2)
  1.1158  
  1.1159  lemma gcd_diff1: "gcd (m - n) n = gcd m n"
  1.1160 @@ -1625,22 +1625,22 @@
  1.1161    finally show ?thesis .
  1.1162  qed
  1.1163  
  1.1164 -lemma lcm_neg1 [simp]: "lcm (-x) y = lcm x y"
  1.1165 +lemma lcm_neg1 [simp]: "lcm (-a) b = lcm a b"
  1.1166    by (rule sym, rule lcmI, simp_all add: lcm_least lcm_zero)
  1.1167  
  1.1168 -lemma lcm_neg2 [simp]: "lcm x (-y) = lcm x y"
  1.1169 +lemma lcm_neg2 [simp]: "lcm a (-b) = lcm a b"
  1.1170    by (rule sym, rule lcmI, simp_all add: lcm_least lcm_zero)
  1.1171  
  1.1172 -lemma lcm_neg_numeral_1 [simp]: "lcm (- numeral n) x = lcm (numeral n) x"
  1.1173 +lemma lcm_neg_numeral_1 [simp]: "lcm (- numeral n) a = lcm (numeral n) a"
  1.1174    by (fact lcm_neg1)
  1.1175  
  1.1176 -lemma lcm_neg_numeral_2 [simp]: "lcm x (- numeral n) = lcm x (numeral n)"
  1.1177 +lemma lcm_neg_numeral_2 [simp]: "lcm a (- numeral n) = lcm a (numeral n)"
  1.1178    by (fact lcm_neg2)
  1.1179  
  1.1180  function euclid_ext :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a \<times> 'a" where
  1.1181    "euclid_ext a b = 
  1.1182       (if b = 0 then 
  1.1183 -        let x = ring_inv (normalisation_factor a) in (x, 0, a * x)
  1.1184 +        let c = ring_inv (normalisation_factor a) in (c, 0, a * c)
  1.1185        else 
  1.1186          case euclid_ext b (a mod b) of
  1.1187              (s,t,c) \<Rightarrow> (t, s - t * (a div b), c))"
  1.1188 @@ -1682,21 +1682,21 @@
  1.1189    by (insert euclid_ext_gcd[of a b], drule (1) subst, simp)
  1.1190  
  1.1191  lemma euclid_ext_correct:
  1.1192 -  "case euclid_ext x y of (s,t,c) \<Rightarrow> s*x + t*y = c"
  1.1193 -proof (induct x y rule: euclid_ext.induct)
  1.1194 -  case (1 x y)
  1.1195 +  "case euclid_ext a b of (s,t,c) \<Rightarrow> s*a + t*b = c"
  1.1196 +proof (induct a b rule: euclid_ext.induct)
  1.1197 +  case (1 a b)
  1.1198    show ?case
  1.1199 -  proof (cases "y = 0")
  1.1200 +  proof (cases "b = 0")
  1.1201      case True
  1.1202      then show ?thesis by (simp add: euclid_ext_0 mult_ac)
  1.1203    next
  1.1204      case False
  1.1205 -    obtain s t c where stc: "euclid_ext y (x mod y) = (s,t,c)"
  1.1206 -      by (cases "euclid_ext y (x mod y)", blast)
  1.1207 -    from 1 have "c = s * y + t * (x mod y)" by (simp add: stc False)
  1.1208 -    also have "... = t*((x div y)*y + x mod y) + (s - t * (x div y))*y"
  1.1209 +    obtain s t c where stc: "euclid_ext b (a mod b) = (s,t,c)"
  1.1210 +      by (cases "euclid_ext b (a mod b)", blast)
  1.1211 +    from 1 have "c = s * b + t * (a mod b)" by (simp add: stc False)
  1.1212 +    also have "... = t*((a div b)*b + a mod b) + (s - t * (a div b))*b"
  1.1213        by (simp add: algebra_simps) 
  1.1214 -    also have "(x div y)*y + x mod y = x" using mod_div_equality .
  1.1215 +    also have "(a div b)*b + a mod b = a" using mod_div_equality .
  1.1216      finally show ?thesis
  1.1217        by (subst euclid_ext.simps, simp add: False stc)
  1.1218      qed
  1.1219 @@ -1711,15 +1711,15 @@
  1.1220      show ?thesis unfolding euclid_ext'_def by simp
  1.1221  qed
  1.1222  
  1.1223 -lemma bezout: "\<exists>s t. s * x + t * y = gcd x y"
  1.1224 +lemma bezout: "\<exists>s t. s * a + t * b = gcd a b"
  1.1225    using euclid_ext'_correct by blast
  1.1226  
  1.1227 -lemma euclid_ext'_0 [simp]: "euclid_ext' x 0 = (ring_inv (normalisation_factor x), 0)" 
  1.1228 +lemma euclid_ext'_0 [simp]: "euclid_ext' a 0 = (ring_inv (normalisation_factor a), 0)" 
  1.1229    by (simp add: bezw_def euclid_ext'_def euclid_ext_0)
  1.1230  
  1.1231 -lemma euclid_ext'_non_0: "y \<noteq> 0 \<Longrightarrow> euclid_ext' x y = (snd (euclid_ext' y (x mod y)),
  1.1232 -  fst (euclid_ext' y (x mod y)) - snd (euclid_ext' y (x mod y)) * (x div y))"
  1.1233 -  by (cases "euclid_ext y (x mod y)") 
  1.1234 +lemma euclid_ext'_non_0: "b \<noteq> 0 \<Longrightarrow> euclid_ext' a b = (snd (euclid_ext' b (a mod b)),
  1.1235 +  fst (euclid_ext' b (a mod b)) - snd (euclid_ext' b (a mod b)) * (a div b))"
  1.1236 +  by (cases "euclid_ext b (a mod b)") 
  1.1237      (simp add: euclid_ext'_def euclid_ext_non_0)
  1.1238    
  1.1239  end
  1.1240 @@ -1760,4 +1760,3 @@
  1.1241  end
  1.1242  
  1.1243  end
  1.1244 -