tuned proof;
authorwenzelm
Sat Mar 09 13:24:59 2019 +0100 (6 weeks ago ago)
changeset 70065dec7cc38a5dc
parent 70064 f8293bf510a0
child 70066 6dc5506ad449
tuned proof;
src/HOL/Computational_Algebra/Euclidean_Algorithm.thy
     1.1 --- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Sat Mar 09 13:19:13 2019 +0100
     1.2 +++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Sat Mar 09 13:24:59 2019 +0100
     1.3 @@ -235,10 +235,12 @@
     1.4          with less.prems have "y \<noteq> 0" "z \<noteq> 0" by auto
     1.5          have normalized_factors_product:
     1.6            "{p. p dvd a * b \<and> normalize p = p} = 
     1.7 -             (\<lambda>(x,y). x * y) ` ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})" for a b
     1.8 +             (\<lambda>(x,y). x * y) ` ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})"
     1.9 +          for a b
    1.10          proof safe
    1.11            fix p assume p: "p dvd a * b" "normalize p = p"
    1.12 -          from dvd_productE[OF p(1)] guess x y . note xy = this
    1.13 +          from p(1) obtain x y where xy: "p = x * y" "x dvd a" "y dvd b"
    1.14 +            by (rule dvd_productE)
    1.15            define x' y' where "x' = normalize x" and "y' = normalize y"
    1.16            have "p = x' * y'"
    1.17              by (subst p(2) [symmetric]) (simp add: xy x'_def y'_def normalize_mult)