src/HOL/Number_Theory/Euclidean_Algorithm.thy
 changeset 64592 7759f1766189 parent 64243 aee949f6642d child 64784 5cb5e7ecb284
1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sat Dec 17 15:22:13 2016 +0100
1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sat Dec 17 15:22:14 2016 +0100
1.3 @@ -17,7 +17,7 @@
1.4    The existence of these functions makes it possible to derive gcd and lcm functions
1.5    for any Euclidean semiring.
1.6  \<close>
1.7 -class euclidean_semiring = semiring_modulo + normalization_semidom +
1.8 +class euclidean_semiring = semidom_modulo + normalization_semidom +
1.9    fixes euclidean_size :: "'a \<Rightarrow> nat"
1.10    assumes size_0 [simp]: "euclidean_size 0 = 0"
1.11    assumes mod_size_less:
1.12 @@ -26,30 +26,6 @@
1.13      "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
1.14  begin
1.16 -lemma mod_0 [simp]: "0 mod a = 0"
1.17 -  using div_mult_mod_eq [of 0 a] by simp
1.18 -
1.19 -lemma dvd_mod_iff:
1.20 -  assumes "k dvd n"
1.21 -  shows   "(k dvd m mod n) = (k dvd m)"
1.22 -proof -
1.23 -  from assms have "(k dvd m mod n) \<longleftrightarrow> (k dvd ((m div n) * n + m mod n))"
1.25 -  also have "(m div n) * n + m mod n = m"
1.26 -    using div_mult_mod_eq [of m n] by simp
1.27 -  finally show ?thesis .
1.28 -qed
1.29 -
1.30 -lemma mod_0_imp_dvd:
1.31 -  assumes "a mod b = 0"
1.32 -  shows   "b dvd a"
1.33 -proof -
1.34 -  have "b dvd ((a div b) * b)" by simp
1.35 -  also have "(a div b) * b = a"
1.36 -    using div_mult_mod_eq [of a b] by (simp add: assms)
1.37 -  finally show ?thesis .
1.38 -qed
1.39 -
1.40  lemma euclidean_size_normalize [simp]:
1.41    "euclidean_size (normalize a) = euclidean_size a"
1.42  proof (cases "a = 0")