# HG changeset patch # User wenzelm # Date 1456693086 -3600 # Node ID 075ef5ec115c6229b3ed01f7c8290bab4eadceb3 # Parent 9590972c2caf2fe8a91385b7891779136b8e9012# Parent 4b2018eb92e83648142eb82cb0bac12d1eb34fe9 merged diff -r 4b2018eb92e8 -r 075ef5ec115c lib/scripts/run-polyml diff -r 4b2018eb92e8 -r 075ef5ec115c src/HOL/Number_Theory/Euclidean_Algorithm.thy --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sun Feb 28 21:25:55 2016 +0100 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sun Feb 28 21:58:06 2016 +0100 @@ -234,6 +234,8 @@ class euclidean_ring = euclidean_semiring + idom begin +subclass ring_div .. + function euclid_ext_aux :: "'a \ _" where "euclid_ext_aux r' r s' s t' t = ( if r = 0 then let c = 1 div unit_factor r' in (s' * c, t' * c, normalize r') @@ -305,6 +307,10 @@ "case euclid_ext x y of (a,b,c) \ a * x + b * y = c \ c = gcd_eucl x y" unfolding euclid_ext_def by (rule euclid_ext_aux_correct) simp_all +lemma euclid_ext_gcd_eucl: + "(case euclid_ext x y of (a,b,c) \ c) = gcd_eucl x y" + using euclid_ext_correct'[of x y] by (simp add: case_prod_unfold) + definition euclid_ext' where "euclid_ext' x y = (case euclid_ext x y of (a, b, _) \ (a, b))"