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.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.31 -end
1.32 \ No newline at end of file
1.33 +end