author haftmann Thu Jun 25 15:01:43 2015 +0200 (2015-06-25) changeset 60572 718b1ba06429 parent 60571 c9fdf2080447 child 60582 d694f217ee41
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
```     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.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.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.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"
```