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.15  
    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.24 -    by (simp add: dvd_add_right_iff)
    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")