Minor adjustments to euclidean rings
authorManuel Eberl <eberlm@in.tum.de>
Sun Feb 28 21:19:58 2016 +0100 (2016-02-28)
changeset 62457a3c7bd201da7
parent 62442 26e4be6a680f
child 62458 9590972c2caf
Minor adjustments to euclidean rings
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Feb 28 12:05:52 2016 +0100
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Feb 28 21:19:58 2016 +0100
     1.3 @@ -234,6 +234,8 @@
     1.4  class euclidean_ring = euclidean_semiring + idom
     1.5  begin
     1.6  
     1.7 +subclass ring_div ..
     1.8 +
     1.9  function euclid_ext_aux :: "'a \<Rightarrow> _" where
    1.10    "euclid_ext_aux r' r s' s t' t = (
    1.11       if r = 0 then let c = 1 div unit_factor r' in (s' * c, t' * c, normalize r')
    1.12 @@ -305,6 +307,10 @@
    1.13    "case euclid_ext x y of (a,b,c) \<Rightarrow> a * x + b * y = c \<and> c = gcd_eucl x y"
    1.14    unfolding euclid_ext_def by (rule euclid_ext_aux_correct) simp_all
    1.15  
    1.16 +lemma euclid_ext_gcd_eucl:
    1.17 +  "(case euclid_ext x y of (a,b,c) \<Rightarrow> c) = gcd_eucl x y"
    1.18 +  using euclid_ext_correct'[of x y] by (simp add: case_prod_unfold)
    1.19 +
    1.20  definition euclid_ext' where
    1.21    "euclid_ext' x y = (case euclid_ext x y of (a, b, _) \<Rightarrow> (a, b))"
    1.22