--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Tue Sep 20 14:51:58 2016 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sun Sep 18 17:57:55 2016 +0200
@@ -112,23 +112,6 @@
by (auto intro!: euclidean_size_times_nonunit simp: )
qed
-lemma irreducible_normalized_divisors:
- assumes "irreducible x" "y dvd x" "normalize y = y"
- shows "y = 1 \<or> y = normalize x"
-proof -
- from assms have "is_unit y \<or> x dvd y" by (auto simp: irreducible_altdef)
- thus ?thesis
- proof (elim disjE)
- assume "is_unit y"
- hence "normalize y = 1" by (simp add: is_unit_normalize)
- with assms show ?thesis by simp
- next
- assume "x dvd y"
- with \<open>y dvd x\<close> have "normalize y = normalize x" by (rule associatedI)
- with assms show ?thesis by simp
- qed
-qed
-
function gcd_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
where
"gcd_eucl a b = (if b = 0 then normalize a else gcd_eucl b (a mod b))"
@@ -720,4 +703,4 @@
semiring_Gcd_class.Gcd_Lcm Gcd_eucl_def abs_mult)+
qed
-end
\ No newline at end of file
+end