src/HOL/Number_Theory/Euclidean_Algorithm.thy
 changeset 62442 26e4be6a680f parent 62429 25271ff79171 child 62457 a3c7bd201da7
1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sat Feb 27 21:09:43 2016 +0100
1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Feb 28 12:05:52 2016 +0100
1.3 @@ -234,67 +234,89 @@
1.4  class euclidean_ring = euclidean_semiring + idom
1.5  begin
1.7 -function euclid_ext :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a \<times> 'a" where
1.8 -  "euclid_ext a b =
1.9 -     (if b = 0 then
1.10 -        (1 div unit_factor a, 0, normalize a)
1.11 -      else
1.12 -        case euclid_ext b (a mod b) of
1.13 -            (s, t, c) \<Rightarrow> (t, s - t * (a div b), c))"
1.14 -  by pat_completeness simp
1.15 -termination
1.16 -  by (relation "measure (euclidean_size \<circ> snd)") (simp_all add: mod_size_less)
1.17 +function euclid_ext_aux :: "'a \<Rightarrow> _" where
1.18 +  "euclid_ext_aux r' r s' s t' t = (
1.19 +     if r = 0 then let c = 1 div unit_factor r' in (s' * c, t' * c, normalize r')
1.20 +     else let q = r' div r
1.21 +          in  euclid_ext_aux r (r' mod r) s (s' - q * s) t (t' - q * t))"
1.22 +by auto
1.23 +termination by (relation "measure (\<lambda>(_,b,_,_,_,_). euclidean_size b)") (simp_all add: mod_size_less)
1.24 +
1.25 +declare euclid_ext_aux.simps [simp del]
1.27 -declare euclid_ext.simps [simp del]
1.28 +lemma euclid_ext_aux_correct:
1.29 +  assumes "gcd_eucl r' r = gcd_eucl x y"
1.30 +  assumes "s' * x + t' * y = r'"
1.31 +  assumes "s * x + t * y = r"
1.32 +  shows   "case euclid_ext_aux r' r s' s t' t of (a,b,c) \<Rightarrow>
1.33 +             a * x + b * y = c \<and> c = gcd_eucl x y" (is "?P (euclid_ext_aux r' r s' s t' t)")
1.34 +using assms
1.35 +proof (induction r' r s' s t' t rule: euclid_ext_aux.induct)
1.36 +  case (1 r' r s' s t' t)
1.37 +  show ?case
1.38 +  proof (cases "r = 0")
1.39 +    case True
1.40 +    hence "euclid_ext_aux r' r s' s t' t =
1.41 +             (s' div unit_factor r', t' div unit_factor r', normalize r')"
1.42 +      by (subst euclid_ext_aux.simps) (simp add: Let_def)
1.43 +    also have "?P \<dots>"
1.44 +    proof safe
1.45 +      have "s' div unit_factor r' * x + t' div unit_factor r' * y =
1.46 +                (s' * x + t' * y) div unit_factor r'"
1.47 +        by (cases "r' = 0") (simp_all add: unit_div_commute)
1.48 +      also have "s' * x + t' * y = r'" by fact
1.49 +      also have "\<dots> div unit_factor r' = normalize r'" by simp
1.50 +      finally show "s' div unit_factor r' * x + t' div unit_factor r' * y = normalize r'" .
1.51 +    next
1.52 +      from "1.prems" True show "normalize r' = gcd_eucl x y" by (simp add: gcd_eucl_0)
1.53 +    qed
1.54 +    finally show ?thesis .
1.55 +  next
1.56 +    case False
1.57 +    hence "euclid_ext_aux r' r s' s t' t =
1.58 +             euclid_ext_aux r (r' mod r) s (s' - r' div r * s) t (t' - r' div r * t)"
1.59 +      by (subst euclid_ext_aux.simps) (simp add: Let_def)
1.60 +    also from "1.prems" False have "?P \<dots>"
1.61 +    proof (intro "1.IH")
1.62 +      have "(s' - r' div r * s) * x + (t' - r' div r * t) * y =
1.63 +              (s' * x + t' * y) - r' div r * (s * x + t * y)" by (simp add: algebra_simps)
1.64 +      also have "s' * x + t' * y = r'" by fact
1.65 +      also have "s * x + t * y = r" by fact
1.66 +      also have "r' - r' div r * r = r' mod r" using mod_div_equality[of r' r]
1.67 +        by (simp add: algebra_simps)
1.68 +      finally show "(s' - r' div r * s) * x + (t' - r' div r * t) * y = r' mod r" .
1.69 +    qed (auto simp: gcd_eucl_non_0 algebra_simps div_mod_equality')
1.70 +    finally show ?thesis .
1.71 +  qed
1.72 +qed
1.73 +
1.74 +definition euclid_ext where
1.75 +  "euclid_ext a b = euclid_ext_aux a b 1 0 0 1"
1.77  lemma euclid_ext_0:
1.78    "euclid_ext a 0 = (1 div unit_factor a, 0, normalize a)"
1.79 -  by (simp add: euclid_ext.simps [of a 0])
1.80 +  by (simp add: euclid_ext_def euclid_ext_aux.simps)
1.82  lemma euclid_ext_left_0:
1.83    "euclid_ext 0 a = (0, 1 div unit_factor a, normalize a)"
1.84 -  by (simp add: euclid_ext_0 euclid_ext.simps [of 0 a])
1.85 +  by (simp add: euclid_ext_def euclid_ext_aux.simps)
1.87 -lemma euclid_ext_non_0:
1.88 -  "b \<noteq> 0 \<Longrightarrow> euclid_ext a b = (case euclid_ext b (a mod b) of
1.89 -    (s, t, c) \<Rightarrow> (t, s - t * (a div b), c))"
1.90 -  by (simp add: euclid_ext.simps [of a b] euclid_ext.simps [of b 0])
1.91 -
1.92 -lemma euclid_ext_code [code]:
1.93 -  "euclid_ext a b = (if b = 0 then (1 div unit_factor a, 0, normalize a)
1.94 -    else let (s, t, c) = euclid_ext b (a mod b) in  (t, s - t * (a div b), c))"
1.95 -  by (simp add: euclid_ext.simps [of a b] euclid_ext.simps [of b 0])
1.96 +lemma euclid_ext_correct':
1.97 +  "case euclid_ext x y of (a,b,c) \<Rightarrow> a * x + b * y = c \<and> c = gcd_eucl x y"
1.98 +  unfolding euclid_ext_def by (rule euclid_ext_aux_correct) simp_all
1.100 -lemma euclid_ext_correct:
1.101 -  "case euclid_ext a b of (s, t, c) \<Rightarrow> s * a + t * b = c"
1.102 -proof (induct a b rule: gcd_eucl_induct)
1.103 -  case (zero a) then show ?case
1.104 -    by (simp add: euclid_ext_0 ac_simps)
1.105 -next
1.106 -  case (mod a b)
1.107 -  obtain s t c where stc: "euclid_ext b (a mod b) = (s,t,c)"
1.108 -    by (cases "euclid_ext b (a mod b)") blast
1.109 -  with mod have "c = s * b + t * (a mod b)" by simp
1.110 -  also have "... = t * ((a div b) * b + a mod b) + (s - t * (a div b)) * b"
1.111 -    by (simp add: algebra_simps)
1.112 -  also have "(a div b) * b + a mod b = a" using mod_div_equality .
1.113 -  finally show ?case
1.114 -    by (subst euclid_ext.simps) (simp add: stc mod ac_simps)
1.115 -qed
1.116 +definition euclid_ext' where
1.117 +  "euclid_ext' x y = (case euclid_ext x y of (a, b, _) \<Rightarrow> (a, b))"
1.119 -definition euclid_ext' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a"
1.120 -where
1.121 -  "euclid_ext' a b = (case euclid_ext a b of (s, t, _) \<Rightarrow> (s, t))"
1.122 +lemma euclid_ext'_correct':
1.123 +  "case euclid_ext' x y of (a,b) \<Rightarrow> a * x + b * y = gcd_eucl x y"
1.124 +  using euclid_ext_correct'[of x y] by (simp add: case_prod_unfold euclid_ext'_def)
1.126  lemma euclid_ext'_0: "euclid_ext' a 0 = (1 div unit_factor a, 0)"
1.127    by (simp add: euclid_ext'_def euclid_ext_0)
1.129  lemma euclid_ext'_left_0: "euclid_ext' 0 a = (0, 1 div unit_factor a)"
1.130    by (simp add: euclid_ext'_def euclid_ext_left_0)
1.132 -lemma euclid_ext'_non_0: "b \<noteq> 0 \<Longrightarrow> euclid_ext' a b = (snd (euclid_ext' b (a mod b)),
1.133 -  fst (euclid_ext' b (a mod b)) - snd (euclid_ext' b (a mod b)) * (a div b))"
1.134 -  by (simp add: euclid_ext'_def euclid_ext_non_0 split_def)
1.136  end
1.138 @@ -412,21 +434,21 @@
1.140  lemma euclid_ext_gcd [simp]:
1.141    "(case euclid_ext a b of (_, _ , t) \<Rightarrow> t) = gcd a b"
1.142 -  by (induct a b rule: gcd_eucl_induct)
1.143 -    (simp_all add: euclid_ext_0 euclid_ext_non_0 ac_simps split: prod.split prod.split_asm)
1.144 +  using euclid_ext_correct'[of a b] by (simp add: case_prod_unfold Let_def gcd_gcd_eucl)
1.146  lemma euclid_ext_gcd' [simp]:
1.147    "euclid_ext a b = (r, s, t) \<Longrightarrow> t = gcd a b"
1.148    by (insert euclid_ext_gcd[of a b], drule (1) subst, simp)
1.150 +lemma euclid_ext_correct:
1.151 +  "case euclid_ext x y of (a,b,c) \<Rightarrow> a * x + b * y = c \<and> c = gcd x y"
1.152 +  using euclid_ext_correct'[of x y]
1.153 +  by (simp add: gcd_gcd_eucl case_prod_unfold)
1.155  lemma euclid_ext'_correct:
1.156    "fst (euclid_ext' a b) * a + snd (euclid_ext' a b) * b = gcd a b"
1.157 -proof-
1.158 -  obtain s t c where "euclid_ext a b = (s,t,c)"
1.159 -    by (cases "euclid_ext a b", blast)
1.160 -  with euclid_ext_correct[of a b] euclid_ext_gcd[of a b]
1.161 -    show ?thesis unfolding euclid_ext'_def by simp
1.162 -qed
1.163 +  using euclid_ext_correct'[of a b]
1.164 +  by (simp add: gcd_gcd_eucl case_prod_unfold euclid_ext'_def)
1.166  lemma bezout: "\<exists>s t. s * a + t * b = gcd a b"
1.167    using euclid_ext'_correct by blast