tuned structure
authorhaftmann
Sun Oct 08 22:28:21 2017 +0200 (19 months ago)
changeset 66807c3631f32dfeb
parent 66806 a4e82b58d833
child 66808 1907167b6038
tuned structure
src/HOL/Euclidean_Division.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -9,82 +9,6 @@
     1.4    imports Nat_Transfer
     1.5  begin
     1.6  
     1.7 -subsection \<open>Quotient and remainder in integral domains\<close>
     1.8 -
     1.9 -class semidom_modulo = algebraic_semidom + semiring_modulo
    1.10 -begin
    1.11 -
    1.12 -lemma mod_0 [simp]: "0 mod a = 0"
    1.13 -  using div_mult_mod_eq [of 0 a] by simp
    1.14 -
    1.15 -lemma mod_by_0 [simp]: "a mod 0 = a"
    1.16 -  using div_mult_mod_eq [of a 0] by simp
    1.17 -
    1.18 -lemma mod_by_1 [simp]:
    1.19 -  "a mod 1 = 0"
    1.20 -proof -
    1.21 -  from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
    1.22 -  then have "a + a mod 1 = a + 0" by simp
    1.23 -  then show ?thesis by (rule add_left_imp_eq)
    1.24 -qed
    1.25 -
    1.26 -lemma mod_self [simp]:
    1.27 -  "a mod a = 0"
    1.28 -  using div_mult_mod_eq [of a a] by simp
    1.29 -
    1.30 -lemma dvd_imp_mod_0 [simp]:
    1.31 -  assumes "a dvd b"
    1.32 -  shows "b mod a = 0"
    1.33 -  using assms minus_div_mult_eq_mod [of b a] by simp
    1.34 -
    1.35 -lemma mod_0_imp_dvd: 
    1.36 -  assumes "a mod b = 0"
    1.37 -  shows   "b dvd a"
    1.38 -proof -
    1.39 -  have "b dvd ((a div b) * b)" by simp
    1.40 -  also have "(a div b) * b = a"
    1.41 -    using div_mult_mod_eq [of a b] by (simp add: assms)
    1.42 -  finally show ?thesis .
    1.43 -qed
    1.44 -
    1.45 -lemma mod_eq_0_iff_dvd:
    1.46 -  "a mod b = 0 \<longleftrightarrow> b dvd a"
    1.47 -  by (auto intro: mod_0_imp_dvd)
    1.48 -
    1.49 -lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
    1.50 -  "a dvd b \<longleftrightarrow> b mod a = 0"
    1.51 -  by (simp add: mod_eq_0_iff_dvd)
    1.52 -
    1.53 -lemma dvd_mod_iff: 
    1.54 -  assumes "c dvd b"
    1.55 -  shows "c dvd a mod b \<longleftrightarrow> c dvd a"
    1.56 -proof -
    1.57 -  from assms have "(c dvd a mod b) \<longleftrightarrow> (c dvd ((a div b) * b + a mod b))" 
    1.58 -    by (simp add: dvd_add_right_iff)
    1.59 -  also have "(a div b) * b + a mod b = a"
    1.60 -    using div_mult_mod_eq [of a b] by simp
    1.61 -  finally show ?thesis .
    1.62 -qed
    1.63 -
    1.64 -lemma dvd_mod_imp_dvd:
    1.65 -  assumes "c dvd a mod b" and "c dvd b"
    1.66 -  shows "c dvd a"
    1.67 -  using assms dvd_mod_iff [of c b a] by simp
    1.68 -
    1.69 -end
    1.70 -
    1.71 -class idom_modulo = idom + semidom_modulo
    1.72 -begin
    1.73 -
    1.74 -subclass idom_divide ..
    1.75 -
    1.76 -lemma div_diff [simp]:
    1.77 -  "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
    1.78 -  using div_add [of _  _ "- b"] by (simp add: dvd_neg_div)
    1.79 -
    1.80 -end
    1.81 -
    1.82 -  
    1.83  subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
    1.84    
    1.85  class euclidean_semiring = semidom_modulo + normalization_semidom + 
     2.1 --- a/src/HOL/Rings.thy	Sun Oct 08 22:28:21 2017 +0200
     2.2 +++ b/src/HOL/Rings.thy	Sun Oct 08 22:28:21 2017 +0200
     2.3 @@ -1558,6 +1558,82 @@
     2.4  end
     2.5  
     2.6  
     2.7 +text \<open>Quotient and remainder in integral domains\<close>
     2.8 +
     2.9 +class semidom_modulo = algebraic_semidom + semiring_modulo
    2.10 +begin
    2.11 +
    2.12 +lemma mod_0 [simp]: "0 mod a = 0"
    2.13 +  using div_mult_mod_eq [of 0 a] by simp
    2.14 +
    2.15 +lemma mod_by_0 [simp]: "a mod 0 = a"
    2.16 +  using div_mult_mod_eq [of a 0] by simp
    2.17 +
    2.18 +lemma mod_by_1 [simp]:
    2.19 +  "a mod 1 = 0"
    2.20 +proof -
    2.21 +  from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
    2.22 +  then have "a + a mod 1 = a + 0" by simp
    2.23 +  then show ?thesis by (rule add_left_imp_eq)
    2.24 +qed
    2.25 +
    2.26 +lemma mod_self [simp]:
    2.27 +  "a mod a = 0"
    2.28 +  using div_mult_mod_eq [of a a] by simp
    2.29 +
    2.30 +lemma dvd_imp_mod_0 [simp]:
    2.31 +  assumes "a dvd b"
    2.32 +  shows "b mod a = 0"
    2.33 +  using assms minus_div_mult_eq_mod [of b a] by simp
    2.34 +
    2.35 +lemma mod_0_imp_dvd: 
    2.36 +  assumes "a mod b = 0"
    2.37 +  shows   "b dvd a"
    2.38 +proof -
    2.39 +  have "b dvd ((a div b) * b)" by simp
    2.40 +  also have "(a div b) * b = a"
    2.41 +    using div_mult_mod_eq [of a b] by (simp add: assms)
    2.42 +  finally show ?thesis .
    2.43 +qed
    2.44 +
    2.45 +lemma mod_eq_0_iff_dvd:
    2.46 +  "a mod b = 0 \<longleftrightarrow> b dvd a"
    2.47 +  by (auto intro: mod_0_imp_dvd)
    2.48 +
    2.49 +lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
    2.50 +  "a dvd b \<longleftrightarrow> b mod a = 0"
    2.51 +  by (simp add: mod_eq_0_iff_dvd)
    2.52 +
    2.53 +lemma dvd_mod_iff: 
    2.54 +  assumes "c dvd b"
    2.55 +  shows "c dvd a mod b \<longleftrightarrow> c dvd a"
    2.56 +proof -
    2.57 +  from assms have "(c dvd a mod b) \<longleftrightarrow> (c dvd ((a div b) * b + a mod b))" 
    2.58 +    by (simp add: dvd_add_right_iff)
    2.59 +  also have "(a div b) * b + a mod b = a"
    2.60 +    using div_mult_mod_eq [of a b] by simp
    2.61 +  finally show ?thesis .
    2.62 +qed
    2.63 +
    2.64 +lemma dvd_mod_imp_dvd:
    2.65 +  assumes "c dvd a mod b" and "c dvd b"
    2.66 +  shows "c dvd a"
    2.67 +  using assms dvd_mod_iff [of c b a] by simp
    2.68 +
    2.69 +end
    2.70 +
    2.71 +class idom_modulo = idom + semidom_modulo
    2.72 +begin
    2.73 +
    2.74 +subclass idom_divide ..
    2.75 +
    2.76 +lemma div_diff [simp]:
    2.77 +  "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
    2.78 +  using div_add [of _  _ "- b"] by (simp add: dvd_neg_div)
    2.79 +
    2.80 +end
    2.81 +
    2.82 +
    2.83  class ordered_semiring = semiring + ordered_comm_monoid_add +
    2.84    assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
    2.85    assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"