equal
deleted
inserted
replaced
232 end |
232 end |
233 |
233 |
234 class euclidean_ring = euclidean_semiring + idom |
234 class euclidean_ring = euclidean_semiring + idom |
235 begin |
235 begin |
236 |
236 |
|
237 subclass ring_div .. |
|
238 |
237 function euclid_ext_aux :: "'a \<Rightarrow> _" where |
239 function euclid_ext_aux :: "'a \<Rightarrow> _" where |
238 "euclid_ext_aux r' r s' s t' t = ( |
240 "euclid_ext_aux r' r s' s t' t = ( |
239 if r = 0 then let c = 1 div unit_factor r' in (s' * c, t' * c, normalize r') |
241 if r = 0 then let c = 1 div unit_factor r' in (s' * c, t' * c, normalize r') |
240 else let q = r' div r |
242 else let q = r' div r |
241 in euclid_ext_aux r (r' mod r) s (s' - q * s) t (t' - q * t))" |
243 in euclid_ext_aux r (r' mod r) s (s' - q * s) t (t' - q * t))" |
303 |
305 |
304 lemma euclid_ext_correct': |
306 lemma euclid_ext_correct': |
305 "case euclid_ext x y of (a,b,c) \<Rightarrow> a * x + b * y = c \<and> c = gcd_eucl x y" |
307 "case euclid_ext x y of (a,b,c) \<Rightarrow> a * x + b * y = c \<and> c = gcd_eucl x y" |
306 unfolding euclid_ext_def by (rule euclid_ext_aux_correct) simp_all |
308 unfolding euclid_ext_def by (rule euclid_ext_aux_correct) simp_all |
307 |
309 |
|
310 lemma euclid_ext_gcd_eucl: |
|
311 "(case euclid_ext x y of (a,b,c) \<Rightarrow> c) = gcd_eucl x y" |
|
312 using euclid_ext_correct'[of x y] by (simp add: case_prod_unfold) |
|
313 |
308 definition euclid_ext' where |
314 definition euclid_ext' where |
309 "euclid_ext' x y = (case euclid_ext x y of (a, b, _) \<Rightarrow> (a, b))" |
315 "euclid_ext' x y = (case euclid_ext x y of (a, b, _) \<Rightarrow> (a, b))" |
310 |
316 |
311 lemma euclid_ext'_correct': |
317 lemma euclid_ext'_correct': |
312 "case euclid_ext' x y of (a,b) \<Rightarrow> a * x + b * y = gcd_eucl x y" |
318 "case euclid_ext' x y of (a,b) \<Rightarrow> a * x + b * y = gcd_eucl x y" |