streamlined definitions and primitive lemma of euclidean algorithm, including code generation
authorhaftmann
Thu Jun 25 15:01:43 2015 +0200 (2015-06-25)
changeset 60572718b1ba06429
parent 60571 c9fdf2080447
child 60582 d694f217ee41
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jun 25 15:01:42 2015 +0200
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jun 25 15:01:43 2015 +0200
     1.3 @@ -174,7 +174,7 @@
     1.4    "gcd_eucl a b = (if b = 0 then a div normalization_factor a
     1.5      else if b dvd a then b div normalization_factor b
     1.6      else gcd_eucl b (a mod b))"
     1.7 -  by (pat_completeness, simp)
     1.8 +  by pat_completeness simp
     1.9  termination
    1.10    by (relation "measure (euclidean_size \<circ> snd)") (simp_all add: mod_size_less)
    1.11  
    1.12 @@ -209,10 +209,9 @@
    1.13  where
    1.14    "lcm_eucl a b = a * b div (gcd_eucl a b * normalization_factor (a * b))"
    1.15  
    1.16 -  (* Somewhat complicated definition of Lcm that has the advantage of working
    1.17 -     for infinite sets as well *)
    1.18 -
    1.19 -definition Lcm_eucl :: "'a set \<Rightarrow> 'a"
    1.20 +definition Lcm_eucl :: "'a set \<Rightarrow> 'a" -- \<open>
    1.21 +  Somewhat complicated definition of Lcm that has the advantage of working
    1.22 +  for infinite sets as well\<close>
    1.23  where
    1.24    "Lcm_eucl A = (if \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) then
    1.25       let l = SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l =
    1.26 @@ -224,6 +223,23 @@
    1.27  where
    1.28    "Gcd_eucl A = Lcm_eucl {d. \<forall>a\<in>A. d dvd a}"
    1.29  
    1.30 +lemma gcd_eucl_0:
    1.31 +  "gcd_eucl a 0 = a div normalization_factor a"
    1.32 +  by (simp add: gcd_eucl.simps [of a 0])
    1.33 +
    1.34 +lemma gcd_eucl_0_left:
    1.35 +  "gcd_eucl 0 a = a div normalization_factor a"
    1.36 +  by (simp add: gcd_eucl.simps [of 0 a])
    1.37 +
    1.38 +lemma gcd_eucl_non_0:
    1.39 +  "b \<noteq> 0 \<Longrightarrow> gcd_eucl a b = gcd_eucl b (a mod b)"
    1.40 +  by (cases "b dvd a")
    1.41 +    (simp_all add: gcd_eucl.simps [of a b] gcd_eucl.simps [of b 0])
    1.42 +
    1.43 +lemma gcd_eucl_code [code]:
    1.44 +  "gcd_eucl a b = (if b = 0 then a div normalization_factor a else gcd_eucl b (a mod b))"
    1.45 +  by (auto simp add: gcd_eucl_non_0 gcd_eucl_0 gcd_eucl_0_left) 
    1.46 +
    1.47  end
    1.48  
    1.49  class euclidean_semiring_gcd = euclidean_semiring + gcd + Gcd +
    1.50 @@ -231,22 +247,17 @@
    1.51    assumes Gcd_Gcd_eucl: "Gcd = Gcd_eucl" and Lcm_Lcm_eucl: "Lcm = Lcm_eucl"
    1.52  begin
    1.53  
    1.54 -lemma gcd_red:
    1.55 -  "gcd a b = gcd b (a mod b)"
    1.56 -  by (cases "b dvd a")
    1.57 -    (auto simp add: gcd_gcd_eucl gcd_eucl.simps [of a b] gcd_eucl.simps [of 0 a] gcd_eucl.simps [of b 0])
    1.58 +lemma gcd_0_left:
    1.59 +  "gcd 0 a = a div normalization_factor a"
    1.60 +  unfolding gcd_gcd_eucl by (fact gcd_eucl_0_left)
    1.61 +
    1.62 +lemma gcd_0:
    1.63 +  "gcd a 0 = a div normalization_factor a"
    1.64 +  unfolding gcd_gcd_eucl by (fact gcd_eucl_0)
    1.65  
    1.66  lemma gcd_non_0:
    1.67    "b \<noteq> 0 \<Longrightarrow> gcd a b = gcd b (a mod b)"
    1.68 -  by (rule gcd_red)
    1.69 -
    1.70 -lemma gcd_0_left:
    1.71 -  "gcd 0 a = a div normalization_factor a"
    1.72 -   by (simp only: gcd_gcd_eucl, subst gcd_eucl.simps, subst gcd_eucl.simps, simp add: Let_def)
    1.73 -
    1.74 -lemma gcd_0:
    1.75 -  "gcd a 0 = a div normalization_factor a"
    1.76 -  by (simp only: gcd_gcd_eucl, subst gcd_eucl.simps, simp add: Let_def)
    1.77 +  unfolding gcd_gcd_eucl by (fact gcd_eucl_non_0)
    1.78  
    1.79  lemma gcd_dvd1 [iff]: "gcd a b dvd a"
    1.80    and gcd_dvd2 [iff]: "gcd a b dvd b"
    1.81 @@ -543,8 +554,13 @@
    1.82    "gcd m (m + n) = gcd m n"
    1.83    using gcd_add1 [of n m] by (simp add: ac_simps)
    1.84  
    1.85 -lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
    1.86 -  by (subst gcd.commute, subst gcd_red, simp)
    1.87 +lemma gcd_add_mult:
    1.88 +  "gcd m (k * m + n) = gcd m n"
    1.89 +proof -
    1.90 +  have "gcd m ((k * m + n) mod m) = gcd m (k * m + n)"
    1.91 +    by (fact gcd_mod2)
    1.92 +  then show ?thesis by simp 
    1.93 +qed
    1.94  
    1.95  lemma coprimeI: "(\<And>l. \<lbrakk>l dvd a; l dvd b\<rbrakk> \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd a b = 1"
    1.96    by (rule sym, rule gcdI, simp_all)
    1.97 @@ -1401,6 +1417,74 @@
    1.98  \<close>
    1.99  
   1.100  class euclidean_ring = euclidean_semiring + idom
   1.101 +begin
   1.102 +
   1.103 +function euclid_ext :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a \<times> 'a" where
   1.104 +  "euclid_ext a b = 
   1.105 +     (if b = 0 then 
   1.106 +        let c = 1 div normalization_factor a in (c, 0, a * c)
   1.107 +      else if b dvd a then
   1.108 +        let c = 1 div normalization_factor b in (0, c, b * c)
   1.109 +      else
   1.110 +        case euclid_ext b (a mod b) of
   1.111 +            (s, t, c) \<Rightarrow> (t, s - t * (a div b), c))"
   1.112 +  by pat_completeness simp
   1.113 +termination
   1.114 +  by (relation "measure (euclidean_size \<circ> snd)") (simp_all add: mod_size_less)
   1.115 +
   1.116 +declare euclid_ext.simps [simp del]
   1.117 +
   1.118 +lemma euclid_ext_0: 
   1.119 +  "euclid_ext a 0 = (1 div normalization_factor a, 0, a div normalization_factor a)"
   1.120 +  by (simp add: euclid_ext.simps [of a 0])
   1.121 +
   1.122 +lemma euclid_ext_left_0: 
   1.123 +  "euclid_ext 0 a = (0, 1 div normalization_factor a, a div normalization_factor a)"
   1.124 +  by (simp add: euclid_ext.simps [of 0 a])
   1.125 +
   1.126 +lemma euclid_ext_non_0: 
   1.127 +  "b \<noteq> 0 \<Longrightarrow> euclid_ext a b = (case euclid_ext b (a mod b) of
   1.128 +    (s, t, c) \<Rightarrow> (t, s - t * (a div b), c))"
   1.129 +  by (cases "b dvd a")
   1.130 +    (simp_all add: euclid_ext.simps [of a b] euclid_ext.simps [of b 0])
   1.131 +
   1.132 +lemma euclid_ext_code [code]:
   1.133 +  "euclid_ext a b = (if b = 0 then (1 div normalization_factor a, 0, a div normalization_factor a)
   1.134 +    else let (s, t, c) = euclid_ext b (a mod b) in  (t, s - t * (a div b), c))"
   1.135 +  by (simp add: euclid_ext.simps [of a b] euclid_ext.simps [of b 0])
   1.136 +
   1.137 +lemma euclid_ext_correct:
   1.138 +  "case euclid_ext a b of (s, t, c) \<Rightarrow> s * a + t * b = c"
   1.139 +proof (induct a b rule: gcd_eucl_induct)
   1.140 +  case (zero a) then show ?case
   1.141 +    by (simp add: euclid_ext_0 ac_simps)
   1.142 +next
   1.143 +  case (mod a b)
   1.144 +  obtain s t c where stc: "euclid_ext b (a mod b) = (s,t,c)"
   1.145 +    by (cases "euclid_ext b (a mod b)") blast
   1.146 +  with mod have "c = s * b + t * (a mod b)" by simp
   1.147 +  also have "... = t * ((a div b) * b + a mod b) + (s - t * (a div b)) * b"
   1.148 +    by (simp add: algebra_simps) 
   1.149 +  also have "(a div b) * b + a mod b = a" using mod_div_equality .
   1.150 +  finally show ?case
   1.151 +    by (subst euclid_ext.simps) (simp add: stc mod ac_simps)
   1.152 +qed
   1.153 +
   1.154 +definition euclid_ext' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a"
   1.155 +where
   1.156 +  "euclid_ext' a b = (case euclid_ext a b of (s, t, _) \<Rightarrow> (s, t))"
   1.157 +
   1.158 +lemma euclid_ext'_0: "euclid_ext' a 0 = (1 div normalization_factor a, 0)" 
   1.159 +  by (simp add: euclid_ext'_def euclid_ext_0)
   1.160 +
   1.161 +lemma euclid_ext'_left_0: "euclid_ext' 0 a = (0, 1 div normalization_factor a)" 
   1.162 +  by (simp add: euclid_ext'_def euclid_ext_left_0)
   1.163 +  
   1.164 +lemma euclid_ext'_non_0: "b \<noteq> 0 \<Longrightarrow> euclid_ext' a b = (snd (euclid_ext' b (a mod b)),
   1.165 +  fst (euclid_ext' b (a mod b)) - snd (euclid_ext' b (a mod b)) * (a div b))"
   1.166 +  by (simp add: euclid_ext'_def euclid_ext_non_0 split_def)
   1.167 +
   1.168 +end
   1.169  
   1.170  class euclidean_ring_gcd = euclidean_semiring_gcd + idom
   1.171  begin
   1.172 @@ -1409,6 +1493,27 @@
   1.173  
   1.174  subclass ring_gcd ..
   1.175  
   1.176 +lemma euclid_ext_gcd [simp]:
   1.177 +  "(case euclid_ext a b of (_, _ , t) \<Rightarrow> t) = gcd a b"
   1.178 +  by (induct a b rule: gcd_eucl_induct)
   1.179 +    (simp_all add: euclid_ext_0 gcd_0 euclid_ext_non_0 ac_simps split: prod.split prod.split_asm)
   1.180 +
   1.181 +lemma euclid_ext_gcd' [simp]:
   1.182 +  "euclid_ext a b = (r, s, t) \<Longrightarrow> t = gcd a b"
   1.183 +  by (insert euclid_ext_gcd[of a b], drule (1) subst, simp)
   1.184 +  
   1.185 +lemma euclid_ext'_correct:
   1.186 +  "fst (euclid_ext' a b) * a + snd (euclid_ext' a b) * b = gcd a b"
   1.187 +proof-
   1.188 +  obtain s t c where "euclid_ext a b = (s,t,c)"
   1.189 +    by (cases "euclid_ext a b", blast)
   1.190 +  with euclid_ext_correct[of a b] euclid_ext_gcd[of a b]
   1.191 +    show ?thesis unfolding euclid_ext'_def by simp
   1.192 +qed
   1.193 +
   1.194 +lemma bezout: "\<exists>s t. s * a + t * b = gcd a b"
   1.195 +  using euclid_ext'_correct by blast
   1.196 +
   1.197  lemma gcd_neg1 [simp]:
   1.198    "gcd (-a) b = gcd a b"
   1.199    by (rule sym, rule gcdI, simp_all add: gcd_greatest)
   1.200 @@ -1451,85 +1556,10 @@
   1.201  lemma lcm_neg_numeral_2 [simp]: "lcm a (- numeral n) = lcm a (numeral n)"
   1.202    by (fact lcm_neg2)
   1.203  
   1.204 -function euclid_ext :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a \<times> 'a" where
   1.205 -  "euclid_ext a b = 
   1.206 -     (if b = 0 then 
   1.207 -        let c = 1 div normalization_factor a in (c, 0, a * c)
   1.208 -      else if b dvd a then
   1.209 -        let c = 1 div normalization_factor b in (0, c, b * c)
   1.210 -      else
   1.211 -        case euclid_ext b (a mod b) of
   1.212 -            (s, t, c) \<Rightarrow> (t, s - t * (a div b), c))"
   1.213 -  by (pat_completeness, simp)
   1.214 -  termination by (relation "measure (euclidean_size \<circ> snd)")
   1.215 -    (simp_all add: mod_size_less)
   1.216 -
   1.217 -declare euclid_ext.simps [simp del]
   1.218 -
   1.219 -lemma euclid_ext_0: 
   1.220 -  "euclid_ext a 0 = (1 div normalization_factor a, 0, a div normalization_factor a)"
   1.221 -  by (subst euclid_ext.simps) (simp add: Let_def)
   1.222 -
   1.223 -lemma euclid_ext_non_0:
   1.224 -  "b \<noteq> 0 \<Longrightarrow> euclid_ext a b = (case euclid_ext b (a mod b) of 
   1.225 -    (s, t, c) \<Rightarrow> (t, s - t * (a div b), c))"
   1.226 -  apply (subst euclid_ext.simps)
   1.227 -  apply (auto simp add: split: if_splits)
   1.228 -  apply (subst euclid_ext.simps)
   1.229 -  apply (auto simp add: split: if_splits)
   1.230 -  done
   1.231 -
   1.232 -definition euclid_ext' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a"
   1.233 -where
   1.234 -  "euclid_ext' a b = (case euclid_ext a b of (s, t, _) \<Rightarrow> (s, t))"
   1.235 -
   1.236 -lemma euclid_ext_gcd [simp]:
   1.237 -  "(case euclid_ext a b of (_, _ , t) \<Rightarrow> t) = gcd a b"
   1.238 -  by (induct a b rule: gcd_eucl_induct)
   1.239 -    (simp_all add: euclid_ext_0 gcd_0 euclid_ext_non_0 ac_simps split: prod.split prod.split_asm)
   1.240 +end
   1.241  
   1.242 -lemma euclid_ext_gcd' [simp]:
   1.243 -  "euclid_ext a b = (r, s, t) \<Longrightarrow> t = gcd a b"
   1.244 -  by (insert euclid_ext_gcd[of a b], drule (1) subst, simp)
   1.245  
   1.246 -lemma euclid_ext_correct:
   1.247 -  "case euclid_ext a b of (s, t, c) \<Rightarrow> s * a + t * b = c"
   1.248 -proof (induct a b rule: gcd_eucl_induct)
   1.249 -  case (zero a) then show ?case
   1.250 -    by (simp add: euclid_ext_0 ac_simps)
   1.251 -next
   1.252 -  case (mod a b)
   1.253 -  obtain s t c where stc: "euclid_ext b (a mod b) = (s,t,c)"
   1.254 -    by (cases "euclid_ext b (a mod b)") blast
   1.255 -  with mod have "c = s * b + t * (a mod b)" by simp
   1.256 -  also have "... = t * ((a div b) * b + a mod b) + (s - t * (a div b)) * b"
   1.257 -    by (simp add: algebra_simps) 
   1.258 -  also have "(a div b) * b + a mod b = a" using mod_div_equality .
   1.259 -  finally show ?case
   1.260 -    by (subst euclid_ext.simps) (simp add: stc mod ac_simps)
   1.261 -qed
   1.262 -
   1.263 -lemma euclid_ext'_correct:
   1.264 -  "fst (euclid_ext' a b) * a + snd (euclid_ext' a b) * b = gcd a b"
   1.265 -proof-
   1.266 -  obtain s t c where "euclid_ext a b = (s,t,c)"
   1.267 -    by (cases "euclid_ext a b", blast)
   1.268 -  with euclid_ext_correct[of a b] euclid_ext_gcd[of a b]
   1.269 -    show ?thesis unfolding euclid_ext'_def by simp
   1.270 -qed
   1.271 -
   1.272 -lemma bezout: "\<exists>s t. s * a + t * b = gcd a b"
   1.273 -  using euclid_ext'_correct by blast
   1.274 -
   1.275 -lemma euclid_ext'_0 [simp]: "euclid_ext' a 0 = (1 div normalization_factor a, 0)" 
   1.276 -  by (simp add: bezw_def euclid_ext'_def euclid_ext_0)
   1.277 -
   1.278 -lemma euclid_ext'_non_0: "b \<noteq> 0 \<Longrightarrow> euclid_ext' a b = (snd (euclid_ext' b (a mod b)),
   1.279 -  fst (euclid_ext' b (a mod b)) - snd (euclid_ext' b (a mod b)) * (a div b))"
   1.280 -  by (cases "euclid_ext b (a mod b)") 
   1.281 -    (simp add: euclid_ext'_def euclid_ext_non_0)
   1.282 -  
   1.283 -end
   1.284 +subsection \<open>Typical instances\<close>
   1.285  
   1.286  instantiation nat :: euclidean_semiring
   1.287  begin
   1.288 @@ -1566,7 +1596,7 @@
   1.289  
   1.290  end
   1.291  
   1.292 -instantiation poly :: (field) euclidean_semiring
   1.293 +instantiation poly :: (field) euclidean_ring
   1.294  begin
   1.295  
   1.296  definition euclidean_size_poly :: "'a poly \<Rightarrow> nat"