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.6  
     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.26  
    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.76  
    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.81  
    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.86  
    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.99  
   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.118  
   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.125  
   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.128  
   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.131 -  
   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.135  
   1.136  end
   1.137  
   1.138 @@ -412,21 +434,21 @@
   1.139  
   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.145  
   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.149 +
   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.154    
   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.165  
   1.166  lemma bezout: "\<exists>s t. s * a + t * b = gcd a b"
   1.167    using euclid_ext'_correct by blast