src/HOL/Number_Theory/Euclidean_Algorithm.thy
changeset 64177 006f303fb173
parent 64164 38c407446400
child 64240 eabf80376aab
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Oct 12 22:38:50 2016 +0200
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Oct 12 21:48:52 2016 +0200
     1.3 @@ -113,14 +113,14 @@
     1.4    finally show "euclidean_size (a * b) \<le> euclidean_size b" .
     1.5  qed
     1.6  
     1.7 -lemma euclidean_size_unit: "is_unit x \<Longrightarrow> euclidean_size x = euclidean_size 1"
     1.8 -  using euclidean_size_times_unit[of x 1] by simp
     1.9 +lemma euclidean_size_unit: "is_unit a \<Longrightarrow> euclidean_size a = euclidean_size 1"
    1.10 +  using euclidean_size_times_unit[of a 1] by simp
    1.11  
    1.12  lemma unit_iff_euclidean_size: 
    1.13 -  "is_unit x \<longleftrightarrow> euclidean_size x = euclidean_size 1 \<and> x \<noteq> 0"
    1.14 +  "is_unit a \<longleftrightarrow> euclidean_size a = euclidean_size 1 \<and> a \<noteq> 0"
    1.15  proof safe
    1.16 -  assume A: "x \<noteq> 0" and B: "euclidean_size x = euclidean_size 1"
    1.17 -  show "is_unit x" by (rule dvd_euclidean_size_eq_imp_dvd[OF A _ B]) simp_all
    1.18 +  assume A: "a \<noteq> 0" and B: "euclidean_size a = euclidean_size 1"
    1.19 +  show "is_unit a" by (rule dvd_euclidean_size_eq_imp_dvd[OF A _ B]) simp_all
    1.20  qed (auto intro: euclidean_size_unit)
    1.21  
    1.22  lemma euclidean_size_times_nonunit:
    1.23 @@ -138,17 +138,17 @@
    1.24  qed
    1.25  
    1.26  lemma dvd_imp_size_le:
    1.27 -  assumes "x dvd y" "y \<noteq> 0" 
    1.28 -  shows   "euclidean_size x \<le> euclidean_size y"
    1.29 +  assumes "a dvd b" "b \<noteq> 0" 
    1.30 +  shows   "euclidean_size a \<le> euclidean_size b"
    1.31    using assms by (auto elim!: dvdE simp: size_mult_mono)
    1.32  
    1.33  lemma dvd_proper_imp_size_less:
    1.34 -  assumes "x dvd y" "\<not>y dvd x" "y \<noteq> 0" 
    1.35 -  shows   "euclidean_size x < euclidean_size y"
    1.36 +  assumes "a dvd b" "\<not>b dvd a" "b \<noteq> 0" 
    1.37 +  shows   "euclidean_size a < euclidean_size b"
    1.38  proof -
    1.39 -  from assms(1) obtain z where "y = x * z" by (erule dvdE)
    1.40 -  hence z: "y = z * x" by (simp add: mult.commute)
    1.41 -  from z assms have "\<not>is_unit z" by (auto simp: mult.commute mult_unit_dvd_iff)
    1.42 +  from assms(1) obtain c where "b = a * c" by (erule dvdE)
    1.43 +  hence z: "b = c * a" by (simp add: mult.commute)
    1.44 +  from z assms have "\<not>is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff)
    1.45    with z assms show ?thesis
    1.46      by (auto intro!: euclidean_size_times_nonunit simp: )
    1.47  qed
    1.48 @@ -335,7 +335,7 @@
    1.49            "\<And>A. normalize (lcm A) = lcm A" shows "lcm = Lcm_eucl"
    1.50    by (intro ext, rule associated_eqI) (auto simp: assms intro: Lcm_eucl_least)  
    1.51  
    1.52 -lemma Gcd_eucl_dvd: "x \<in> A \<Longrightarrow> Gcd_eucl A dvd x"
    1.53 +lemma Gcd_eucl_dvd: "a \<in> A \<Longrightarrow> Gcd_eucl A dvd a"
    1.54    unfolding Gcd_eucl_def by (auto intro: Lcm_eucl_least)
    1.55  
    1.56  lemma Gcd_eucl_greatest: "(\<And>x. x \<in> A \<Longrightarrow> d dvd x) \<Longrightarrow> d dvd Gcd_eucl A"
    1.57 @@ -470,11 +470,11 @@
    1.58  declare euclid_ext_aux.simps [simp del]
    1.59  
    1.60  lemma euclid_ext_aux_correct:
    1.61 -  assumes "gcd_eucl r' r = gcd_eucl x y"
    1.62 -  assumes "s' * x + t' * y = r'"
    1.63 -  assumes "s * x + t * y = r"
    1.64 -  shows   "case euclid_ext_aux r' r s' s t' t of (a,b,c) \<Rightarrow>
    1.65 -             a * x + b * y = c \<and> c = gcd_eucl x y" (is "?P (euclid_ext_aux r' r s' s t' t)")
    1.66 +  assumes "gcd_eucl r' r = gcd_eucl a b"
    1.67 +  assumes "s' * a + t' * b = r'"
    1.68 +  assumes "s * a + t * b = r"
    1.69 +  shows   "case euclid_ext_aux r' r s' s t' t of (x,y,c) \<Rightarrow>
    1.70 +             x * a + y * b = c \<and> c = gcd_eucl a b" (is "?P (euclid_ext_aux r' r s' s t' t)")
    1.71  using assms
    1.72  proof (induction r' r s' s t' t rule: euclid_ext_aux.induct)
    1.73    case (1 r' r s' s t' t)
    1.74 @@ -486,14 +486,14 @@
    1.75        by (subst euclid_ext_aux.simps) (simp add: Let_def)
    1.76      also have "?P \<dots>"
    1.77      proof safe
    1.78 -      have "s' div unit_factor r' * x + t' div unit_factor r' * y = 
    1.79 -                (s' * x + t' * y) div unit_factor r'"
    1.80 +      have "s' div unit_factor r' * a + t' div unit_factor r' * b = 
    1.81 +                (s' * a + t' * b) div unit_factor r'"
    1.82          by (cases "r' = 0") (simp_all add: unit_div_commute)
    1.83 -      also have "s' * x + t' * y = r'" by fact
    1.84 +      also have "s' * a + t' * b = r'" by fact
    1.85        also have "\<dots> div unit_factor r' = normalize r'" by simp
    1.86 -      finally show "s' div unit_factor r' * x + t' div unit_factor r' * y = normalize r'" .
    1.87 +      finally show "s' div unit_factor r' * a + t' div unit_factor r' * b = normalize r'" .
    1.88      next
    1.89 -      from "1.prems" True show "normalize r' = gcd_eucl x y" by (simp add: gcd_eucl_0)
    1.90 +      from "1.prems" True show "normalize r' = gcd_eucl a b" by (simp add: gcd_eucl_0)
    1.91      qed
    1.92      finally show ?thesis .
    1.93    next
    1.94 @@ -503,13 +503,13 @@
    1.95        by (subst euclid_ext_aux.simps) (simp add: Let_def)
    1.96      also from "1.prems" False have "?P \<dots>"
    1.97      proof (intro "1.IH")
    1.98 -      have "(s' - r' div r * s) * x + (t' - r' div r * t) * y =
    1.99 -              (s' * x + t' * y) - r' div r * (s * x + t * y)" by (simp add: algebra_simps)
   1.100 -      also have "s' * x + t' * y = r'" by fact
   1.101 -      also have "s * x + t * y = r" by fact
   1.102 +      have "(s' - r' div r * s) * a + (t' - r' div r * t) * b =
   1.103 +              (s' * a + t' * b) - r' div r * (s * a + t * b)" by (simp add: algebra_simps)
   1.104 +      also have "s' * a + t' * b = r'" by fact
   1.105 +      also have "s * a + t * b = r" by fact
   1.106        also have "r' - r' div r * r = r' mod r" using mod_div_equality [of r' r]
   1.107          by (simp add: algebra_simps)
   1.108 -      finally show "(s' - r' div r * s) * x + (t' - r' div r * t) * y = r' mod r" .
   1.109 +      finally show "(s' - r' div r * s) * a + (t' - r' div r * t) * b = r' mod r" .
   1.110      qed (auto simp: gcd_eucl_non_0 algebra_simps div_mod_equality')
   1.111      finally show ?thesis .
   1.112    qed
   1.113 @@ -527,19 +527,19 @@
   1.114    by (simp add: euclid_ext_def euclid_ext_aux.simps)
   1.115  
   1.116  lemma euclid_ext_correct':
   1.117 -  "case euclid_ext x y of (a,b,c) \<Rightarrow> a * x + b * y = c \<and> c = gcd_eucl x y"
   1.118 +  "case euclid_ext a b of (x,y,c) \<Rightarrow> x * a + y * b = c \<and> c = gcd_eucl a b"
   1.119    unfolding euclid_ext_def by (rule euclid_ext_aux_correct) simp_all
   1.120  
   1.121  lemma euclid_ext_gcd_eucl:
   1.122 -  "(case euclid_ext x y of (a,b,c) \<Rightarrow> c) = gcd_eucl x y"
   1.123 -  using euclid_ext_correct'[of x y] by (simp add: case_prod_unfold)
   1.124 +  "(case euclid_ext a b of (x,y,c) \<Rightarrow> c) = gcd_eucl a b"
   1.125 +  using euclid_ext_correct'[of a b] by (simp add: case_prod_unfold)
   1.126  
   1.127  definition euclid_ext' where
   1.128 -  "euclid_ext' x y = (case euclid_ext x y of (a, b, _) \<Rightarrow> (a, b))"
   1.129 +  "euclid_ext' a b = (case euclid_ext a b of (x, y, _) \<Rightarrow> (x, y))"
   1.130  
   1.131  lemma euclid_ext'_correct':
   1.132 -  "case euclid_ext' x y of (a,b) \<Rightarrow> a * x + b * y = gcd_eucl x y"
   1.133 -  using euclid_ext_correct'[of x y] by (simp add: case_prod_unfold euclid_ext'_def)
   1.134 +  "case euclid_ext' a b of (x,y) \<Rightarrow> x * a + y * b = gcd_eucl a b"
   1.135 +  using euclid_ext_correct'[of a b] by (simp add: case_prod_unfold euclid_ext'_def)
   1.136  
   1.137  lemma euclid_ext'_0: "euclid_ext' a 0 = (1 div unit_factor a, 0)" 
   1.138    by (simp add: euclid_ext'_def euclid_ext_0)
   1.139 @@ -687,8 +687,8 @@
   1.140    by (insert euclid_ext_gcd[of a b], drule (1) subst, simp)
   1.141  
   1.142  lemma euclid_ext_correct:
   1.143 -  "case euclid_ext x y of (a,b,c) \<Rightarrow> a * x + b * y = c \<and> c = gcd x y"
   1.144 -  using euclid_ext_correct'[of x y]
   1.145 +  "case euclid_ext a b of (x,y,c) \<Rightarrow> x * a + y * b = c \<and> c = gcd a b"
   1.146 +  using euclid_ext_correct'[of a b]
   1.147    by (simp add: gcd_gcd_eucl case_prod_unfold)
   1.148    
   1.149  lemma euclid_ext'_correct: