src/HOL/Divides.thy
changeset 64785 ae0bbc8e45ad
parent 64715 33d5fa0ce6e5
child 64848 c50db2128048
     1.1 --- a/src/HOL/Divides.thy	Wed Jan 04 21:28:28 2017 +0100
     1.2 +++ b/src/HOL/Divides.thy	Wed Jan 04 21:28:29 2017 +0100
     1.3 @@ -3,88 +3,12 @@
     1.4      Copyright   1999  University of Cambridge
     1.5  *)
     1.6  
     1.7 -section \<open>Quotient and remainder\<close>
     1.8 +section \<open>More on quotient and remainder\<close>
     1.9  
    1.10  theory Divides
    1.11  imports Parity
    1.12  begin
    1.13  
    1.14 -subsection \<open>Quotient and remainder in integral domains\<close>
    1.15 -
    1.16 -class semidom_modulo = algebraic_semidom + semiring_modulo
    1.17 -begin
    1.18 -
    1.19 -lemma mod_0 [simp]: "0 mod a = 0"
    1.20 -  using div_mult_mod_eq [of 0 a] by simp
    1.21 -
    1.22 -lemma mod_by_0 [simp]: "a mod 0 = a"
    1.23 -  using div_mult_mod_eq [of a 0] by simp
    1.24 -
    1.25 -lemma mod_by_1 [simp]:
    1.26 -  "a mod 1 = 0"
    1.27 -proof -
    1.28 -  from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
    1.29 -  then have "a + a mod 1 = a + 0" by simp
    1.30 -  then show ?thesis by (rule add_left_imp_eq)
    1.31 -qed
    1.32 -
    1.33 -lemma mod_self [simp]:
    1.34 -  "a mod a = 0"
    1.35 -  using div_mult_mod_eq [of a a] by simp
    1.36 -
    1.37 -lemma dvd_imp_mod_0 [simp]:
    1.38 -  assumes "a dvd b"
    1.39 -  shows "b mod a = 0"
    1.40 -  using assms minus_div_mult_eq_mod [of b a] by simp
    1.41 -
    1.42 -lemma mod_0_imp_dvd: 
    1.43 -  assumes "a mod b = 0"
    1.44 -  shows   "b dvd a"
    1.45 -proof -
    1.46 -  have "b dvd ((a div b) * b)" by simp
    1.47 -  also have "(a div b) * b = a"
    1.48 -    using div_mult_mod_eq [of a b] by (simp add: assms)
    1.49 -  finally show ?thesis .
    1.50 -qed
    1.51 -
    1.52 -lemma mod_eq_0_iff_dvd:
    1.53 -  "a mod b = 0 \<longleftrightarrow> b dvd a"
    1.54 -  by (auto intro: mod_0_imp_dvd)
    1.55 -
    1.56 -lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
    1.57 -  "a dvd b \<longleftrightarrow> b mod a = 0"
    1.58 -  by (simp add: mod_eq_0_iff_dvd)
    1.59 -
    1.60 -lemma dvd_mod_iff: 
    1.61 -  assumes "c dvd b"
    1.62 -  shows "c dvd a mod b \<longleftrightarrow> c dvd a"
    1.63 -proof -
    1.64 -  from assms have "(c dvd a mod b) \<longleftrightarrow> (c dvd ((a div b) * b + a mod b))" 
    1.65 -    by (simp add: dvd_add_right_iff)
    1.66 -  also have "(a div b) * b + a mod b = a"
    1.67 -    using div_mult_mod_eq [of a b] by simp
    1.68 -  finally show ?thesis .
    1.69 -qed
    1.70 -
    1.71 -lemma dvd_mod_imp_dvd:
    1.72 -  assumes "c dvd a mod b" and "c dvd b"
    1.73 -  shows "c dvd a"
    1.74 -  using assms dvd_mod_iff [of c b a] by simp
    1.75 -
    1.76 -end
    1.77 -
    1.78 -class idom_modulo = idom + semidom_modulo
    1.79 -begin
    1.80 -
    1.81 -subclass idom_divide ..
    1.82 -
    1.83 -lemma div_diff [simp]:
    1.84 -  "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
    1.85 -  using div_add [of _  _ "- b"] by (simp add: dvd_neg_div)
    1.86 -
    1.87 -end
    1.88 -
    1.89 -
    1.90  subsection \<open>Quotient and remainder in integral domains with additional properties\<close>
    1.91  
    1.92  class semiring_div = semidom_modulo +
    1.93 @@ -440,6 +364,65 @@
    1.94  
    1.95  end
    1.96  
    1.97 +  
    1.98 +subsection \<open>Euclidean (semi)rings with cancel rules\<close>
    1.99 +
   1.100 +class euclidean_semiring_cancel = euclidean_semiring + semiring_div
   1.101 +
   1.102 +class euclidean_ring_cancel = euclidean_ring + ring_div
   1.103 +
   1.104 +context unique_euclidean_semiring
   1.105 +begin
   1.106 +
   1.107 +subclass euclidean_semiring_cancel
   1.108 +proof
   1.109 +  show "(a + c * b) div b = c + a div b" if "b \<noteq> 0" for a b c
   1.110 +  proof (cases a b rule: divmod_cases)
   1.111 +    case by0
   1.112 +    with \<open>b \<noteq> 0\<close> show ?thesis
   1.113 +      by simp
   1.114 +  next
   1.115 +    case (divides q)
   1.116 +    then show ?thesis
   1.117 +      by (simp add: ac_simps)
   1.118 +  next
   1.119 +    case (remainder q r)
   1.120 +    then show ?thesis
   1.121 +      by (auto intro: div_eqI simp add: algebra_simps)
   1.122 +  qed
   1.123 +next
   1.124 +  show"(c * a) div (c * b) = a div b" if "c \<noteq> 0" for a b c
   1.125 +  proof (cases a b rule: divmod_cases)
   1.126 +    case by0
   1.127 +    then show ?thesis
   1.128 +      by simp
   1.129 +  next
   1.130 +    case (divides q)
   1.131 +    with \<open>c \<noteq> 0\<close> show ?thesis
   1.132 +      by (simp add: mult.left_commute [of c])
   1.133 +  next
   1.134 +    case (remainder q r)
   1.135 +    from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
   1.136 +      by simp
   1.137 +    from remainder \<open>c \<noteq> 0\<close>
   1.138 +    have "uniqueness_constraint (r * c) (b * c)"
   1.139 +      and "euclidean_size (r * c) < euclidean_size (b * c)"
   1.140 +      by (simp_all add: uniqueness_constraint_mono_mult uniqueness_constraint_mod size_mono_mult)
   1.141 +    with remainder show ?thesis
   1.142 +      by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps)
   1.143 +        (use \<open>b * c \<noteq> 0\<close> in simp)
   1.144 +  qed
   1.145 +qed
   1.146 +
   1.147 +end
   1.148 +
   1.149 +context unique_euclidean_ring
   1.150 +begin
   1.151 +
   1.152 +subclass euclidean_ring_cancel ..
   1.153 +
   1.154 +end
   1.155 +
   1.156  
   1.157  subsection \<open>Parity\<close>
   1.158  
   1.159 @@ -1097,6 +1080,20 @@
   1.160    shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
   1.161    by (simp add: dvd_eq_mod_eq_0)
   1.162  
   1.163 +instantiation nat :: unique_euclidean_semiring
   1.164 +begin
   1.165 +
   1.166 +definition [simp]:
   1.167 +  "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
   1.168 +
   1.169 +definition [simp]:
   1.170 +  "uniqueness_constraint_nat = (top :: nat \<Rightarrow> nat \<Rightarrow> bool)"
   1.171 +
   1.172 +instance
   1.173 +  by standard (use mult_le_mono2 [of 1] in \<open>simp_all add: unit_factor_nat_def mod_greater_zero_iff_not_dvd\<close>)
   1.174 +
   1.175 +end
   1.176 +
   1.177  text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close>
   1.178  
   1.179  lemma (in semiring_modulo) cancel_div_mod_rules:
   1.180 @@ -2415,6 +2412,22 @@
   1.181      by simp
   1.182  qed
   1.183  
   1.184 +instantiation int :: unique_euclidean_ring
   1.185 +begin
   1.186 +
   1.187 +definition [simp]:
   1.188 +  "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
   1.189 +
   1.190 +definition [simp]:
   1.191 +  "uniqueness_constraint_int (k :: int) l \<longleftrightarrow> unit_factor k = unit_factor l"
   1.192 +  
   1.193 +instance
   1.194 +  by standard
   1.195 +    (use mult_le_mono2 [of 1] in \<open>auto simp add: abs_mult nat_mult_distrib sgn_mod zdiv_eq_0_iff sgn_1_pos sgn_mult split: abs_split\<close>)
   1.196 +
   1.197 +end
   1.198 +
   1.199 +  
   1.200  subsubsection \<open>Quotients of Signs\<close>
   1.201  
   1.202  lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"