src/HOL/Number_Theory/Euclidean_Algorithm.thy
changeset 63924 f91766530e13
parent 63633 2accfb71e33b
child 63947 559f0882d6a6
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Tue Sep 20 14:51:58 2016 +0200
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Sep 18 17:57:55 2016 +0200
     1.3 @@ -112,23 +112,6 @@
     1.4      by (auto intro!: euclidean_size_times_nonunit simp: )
     1.5  qed
     1.6  
     1.7 -lemma irreducible_normalized_divisors:
     1.8 -  assumes "irreducible x" "y dvd x" "normalize y = y"
     1.9 -  shows   "y = 1 \<or> y = normalize x"
    1.10 -proof -
    1.11 -  from assms have "is_unit y \<or> x dvd y" by (auto simp: irreducible_altdef)
    1.12 -  thus ?thesis
    1.13 -  proof (elim disjE)
    1.14 -    assume "is_unit y"
    1.15 -    hence "normalize y = 1" by (simp add: is_unit_normalize)
    1.16 -    with assms show ?thesis by simp
    1.17 -  next
    1.18 -    assume "x dvd y"
    1.19 -    with \<open>y dvd x\<close> have "normalize y = normalize x" by (rule associatedI)
    1.20 -    with assms show ?thesis by simp
    1.21 -  qed
    1.22 -qed
    1.23 -
    1.24  function gcd_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.25  where
    1.26    "gcd_eucl a b = (if b = 0 then normalize a else gcd_eucl b (a mod b))"
    1.27 @@ -720,4 +703,4 @@
    1.28            semiring_Gcd_class.Gcd_Lcm Gcd_eucl_def abs_mult)+
    1.29  qed
    1.30  
    1.31 -end
    1.32 \ No newline at end of file
    1.33 +end