src/HOL/Euclidean_Division.thy
changeset 64785 ae0bbc8e45ad
child 66798 39bb2462e681
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Euclidean_Division.thy	Wed Jan 04 21:28:29 2017 +0100
     1.3 @@ -0,0 +1,287 @@
     1.4 +(*  Title:      HOL/Euclidean_Division.thy
     1.5 +    Author:     Manuel Eberl, TU Muenchen
     1.6 +    Author:     Florian Haftmann, TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +section \<open>Uniquely determined division in euclidean (semi)rings\<close>
    1.10 +
    1.11 +theory Euclidean_Division
    1.12 +  imports Nat_Transfer
    1.13 +begin
    1.14 +
    1.15 +subsection \<open>Quotient and remainder in integral domains\<close>
    1.16 +
    1.17 +class semidom_modulo = algebraic_semidom + semiring_modulo
    1.18 +begin
    1.19 +
    1.20 +lemma mod_0 [simp]: "0 mod a = 0"
    1.21 +  using div_mult_mod_eq [of 0 a] by simp
    1.22 +
    1.23 +lemma mod_by_0 [simp]: "a mod 0 = a"
    1.24 +  using div_mult_mod_eq [of a 0] by simp
    1.25 +
    1.26 +lemma mod_by_1 [simp]:
    1.27 +  "a mod 1 = 0"
    1.28 +proof -
    1.29 +  from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
    1.30 +  then have "a + a mod 1 = a + 0" by simp
    1.31 +  then show ?thesis by (rule add_left_imp_eq)
    1.32 +qed
    1.33 +
    1.34 +lemma mod_self [simp]:
    1.35 +  "a mod a = 0"
    1.36 +  using div_mult_mod_eq [of a a] by simp
    1.37 +
    1.38 +lemma dvd_imp_mod_0 [simp]:
    1.39 +  assumes "a dvd b"
    1.40 +  shows "b mod a = 0"
    1.41 +  using assms minus_div_mult_eq_mod [of b a] by simp
    1.42 +
    1.43 +lemma mod_0_imp_dvd: 
    1.44 +  assumes "a mod b = 0"
    1.45 +  shows   "b dvd a"
    1.46 +proof -
    1.47 +  have "b dvd ((a div b) * b)" by simp
    1.48 +  also have "(a div b) * b = a"
    1.49 +    using div_mult_mod_eq [of a b] by (simp add: assms)
    1.50 +  finally show ?thesis .
    1.51 +qed
    1.52 +
    1.53 +lemma mod_eq_0_iff_dvd:
    1.54 +  "a mod b = 0 \<longleftrightarrow> b dvd a"
    1.55 +  by (auto intro: mod_0_imp_dvd)
    1.56 +
    1.57 +lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
    1.58 +  "a dvd b \<longleftrightarrow> b mod a = 0"
    1.59 +  by (simp add: mod_eq_0_iff_dvd)
    1.60 +
    1.61 +lemma dvd_mod_iff: 
    1.62 +  assumes "c dvd b"
    1.63 +  shows "c dvd a mod b \<longleftrightarrow> c dvd a"
    1.64 +proof -
    1.65 +  from assms have "(c dvd a mod b) \<longleftrightarrow> (c dvd ((a div b) * b + a mod b))" 
    1.66 +    by (simp add: dvd_add_right_iff)
    1.67 +  also have "(a div b) * b + a mod b = a"
    1.68 +    using div_mult_mod_eq [of a b] by simp
    1.69 +  finally show ?thesis .
    1.70 +qed
    1.71 +
    1.72 +lemma dvd_mod_imp_dvd:
    1.73 +  assumes "c dvd a mod b" and "c dvd b"
    1.74 +  shows "c dvd a"
    1.75 +  using assms dvd_mod_iff [of c b a] by simp
    1.76 +
    1.77 +end
    1.78 +
    1.79 +class idom_modulo = idom + semidom_modulo
    1.80 +begin
    1.81 +
    1.82 +subclass idom_divide ..
    1.83 +
    1.84 +lemma div_diff [simp]:
    1.85 +  "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
    1.86 +  using div_add [of _  _ "- b"] by (simp add: dvd_neg_div)
    1.87 +
    1.88 +end
    1.89 +
    1.90 +  
    1.91 +subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
    1.92 +  
    1.93 +class euclidean_semiring = semidom_modulo + normalization_semidom + 
    1.94 +  fixes euclidean_size :: "'a \<Rightarrow> nat"
    1.95 +  assumes size_0 [simp]: "euclidean_size 0 = 0"
    1.96 +  assumes mod_size_less: 
    1.97 +    "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
    1.98 +  assumes size_mult_mono:
    1.99 +    "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
   1.100 +begin
   1.101 +
   1.102 +lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
   1.103 +  by (subst mult.commute) (rule size_mult_mono)
   1.104 +
   1.105 +lemma euclidean_size_normalize [simp]:
   1.106 +  "euclidean_size (normalize a) = euclidean_size a"
   1.107 +proof (cases "a = 0")
   1.108 +  case True
   1.109 +  then show ?thesis
   1.110 +    by simp
   1.111 +next
   1.112 +  case [simp]: False
   1.113 +  have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
   1.114 +    by (rule size_mult_mono) simp
   1.115 +  moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
   1.116 +    by (rule size_mult_mono) simp
   1.117 +  ultimately show ?thesis
   1.118 +    by simp
   1.119 +qed
   1.120 +
   1.121 +lemma dvd_euclidean_size_eq_imp_dvd:
   1.122 +  assumes "a \<noteq> 0" and "euclidean_size a = euclidean_size b"
   1.123 +    and "b dvd a" 
   1.124 +  shows "a dvd b"
   1.125 +proof (rule ccontr)
   1.126 +  assume "\<not> a dvd b"
   1.127 +  hence "b mod a \<noteq> 0" using mod_0_imp_dvd [of b a] by blast
   1.128 +  then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd)
   1.129 +  from \<open>b dvd a\<close> have "b dvd b mod a" by (simp add: dvd_mod_iff)
   1.130 +  then obtain c where "b mod a = b * c" unfolding dvd_def by blast
   1.131 +    with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
   1.132 +  with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
   1.133 +    using size_mult_mono by force
   1.134 +  moreover from \<open>\<not> a dvd b\<close> and \<open>a \<noteq> 0\<close>
   1.135 +  have "euclidean_size (b mod a) < euclidean_size a"
   1.136 +    using mod_size_less by blast
   1.137 +  ultimately show False using \<open>euclidean_size a = euclidean_size b\<close>
   1.138 +    by simp
   1.139 +qed
   1.140 +
   1.141 +lemma euclidean_size_times_unit:
   1.142 +  assumes "is_unit a"
   1.143 +  shows   "euclidean_size (a * b) = euclidean_size b"
   1.144 +proof (rule antisym)
   1.145 +  from assms have [simp]: "a \<noteq> 0" by auto
   1.146 +  thus "euclidean_size (a * b) \<ge> euclidean_size b" by (rule size_mult_mono')
   1.147 +  from assms have "is_unit (1 div a)" by simp
   1.148 +  hence "1 div a \<noteq> 0" by (intro notI) simp_all
   1.149 +  hence "euclidean_size (a * b) \<le> euclidean_size ((1 div a) * (a * b))"
   1.150 +    by (rule size_mult_mono')
   1.151 +  also from assms have "(1 div a) * (a * b) = b"
   1.152 +    by (simp add: algebra_simps unit_div_mult_swap)
   1.153 +  finally show "euclidean_size (a * b) \<le> euclidean_size b" .
   1.154 +qed
   1.155 +
   1.156 +lemma euclidean_size_unit:
   1.157 +  "is_unit a \<Longrightarrow> euclidean_size a = euclidean_size 1"
   1.158 +  using euclidean_size_times_unit [of a 1] by simp
   1.159 +
   1.160 +lemma unit_iff_euclidean_size: 
   1.161 +  "is_unit a \<longleftrightarrow> euclidean_size a = euclidean_size 1 \<and> a \<noteq> 0"
   1.162 +proof safe
   1.163 +  assume A: "a \<noteq> 0" and B: "euclidean_size a = euclidean_size 1"
   1.164 +  show "is_unit a"
   1.165 +    by (rule dvd_euclidean_size_eq_imp_dvd [OF A B]) simp_all
   1.166 +qed (auto intro: euclidean_size_unit)
   1.167 +
   1.168 +lemma euclidean_size_times_nonunit:
   1.169 +  assumes "a \<noteq> 0" "b \<noteq> 0" "\<not> is_unit a"
   1.170 +  shows   "euclidean_size b < euclidean_size (a * b)"
   1.171 +proof (rule ccontr)
   1.172 +  assume "\<not>euclidean_size b < euclidean_size (a * b)"
   1.173 +  with size_mult_mono'[OF assms(1), of b] 
   1.174 +    have eq: "euclidean_size (a * b) = euclidean_size b" by simp
   1.175 +  have "a * b dvd b"
   1.176 +    by (rule dvd_euclidean_size_eq_imp_dvd [OF _ eq]) (insert assms, simp_all)
   1.177 +  hence "a * b dvd 1 * b" by simp
   1.178 +  with \<open>b \<noteq> 0\<close> have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff)
   1.179 +  with assms(3) show False by contradiction
   1.180 +qed
   1.181 +
   1.182 +lemma dvd_imp_size_le:
   1.183 +  assumes "a dvd b" "b \<noteq> 0" 
   1.184 +  shows   "euclidean_size a \<le> euclidean_size b"
   1.185 +  using assms by (auto elim!: dvdE simp: size_mult_mono)
   1.186 +
   1.187 +lemma dvd_proper_imp_size_less:
   1.188 +  assumes "a dvd b" "\<not> b dvd a" "b \<noteq> 0" 
   1.189 +  shows   "euclidean_size a < euclidean_size b"
   1.190 +proof -
   1.191 +  from assms(1) obtain c where "b = a * c" by (erule dvdE)
   1.192 +  hence z: "b = c * a" by (simp add: mult.commute)
   1.193 +  from z assms have "\<not>is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff)
   1.194 +  with z assms show ?thesis
   1.195 +    by (auto intro!: euclidean_size_times_nonunit)
   1.196 +qed
   1.197 +
   1.198 +end
   1.199 +
   1.200 +class euclidean_ring = idom_modulo + euclidean_semiring
   1.201 +
   1.202 +  
   1.203 +subsection \<open>Uniquely determined division\<close>
   1.204 +  
   1.205 +class unique_euclidean_semiring = euclidean_semiring + 
   1.206 +  fixes uniqueness_constraint :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   1.207 +  assumes size_mono_mult:
   1.208 +    "b \<noteq> 0 \<Longrightarrow> euclidean_size a < euclidean_size c
   1.209 +      \<Longrightarrow> euclidean_size (a * b) < euclidean_size (c * b)"
   1.210 +    -- \<open>FIXME justify\<close>
   1.211 +  assumes uniqueness_constraint_mono_mult:
   1.212 +    "uniqueness_constraint a b \<Longrightarrow> uniqueness_constraint (a * c) (b * c)"
   1.213 +  assumes uniqueness_constraint_mod:
   1.214 +    "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> uniqueness_constraint (a mod b) b"
   1.215 +  assumes div_bounded:
   1.216 +    "b \<noteq> 0 \<Longrightarrow> uniqueness_constraint r b
   1.217 +    \<Longrightarrow> euclidean_size r < euclidean_size b
   1.218 +    \<Longrightarrow> (q * b + r) div b = q"
   1.219 +begin
   1.220 +
   1.221 +lemma divmod_cases [case_names divides remainder by0]:
   1.222 +  obtains 
   1.223 +    (divides) q where "b \<noteq> 0"
   1.224 +      and "a div b = q"
   1.225 +      and "a mod b = 0"
   1.226 +      and "a = q * b"
   1.227 +  | (remainder) q r where "b \<noteq> 0" and "r \<noteq> 0"
   1.228 +      and "uniqueness_constraint r b"
   1.229 +      and "euclidean_size r < euclidean_size b"
   1.230 +      and "a div b = q"
   1.231 +      and "a mod b = r"
   1.232 +      and "a = q * b + r"
   1.233 +  | (by0) "b = 0"
   1.234 +proof (cases "b = 0")
   1.235 +  case True
   1.236 +  then show thesis
   1.237 +  by (rule by0)
   1.238 +next
   1.239 +  case False
   1.240 +  show thesis
   1.241 +  proof (cases "b dvd a")
   1.242 +    case True
   1.243 +    then obtain q where "a = b * q" ..
   1.244 +    with \<open>b \<noteq> 0\<close> divides
   1.245 +    show thesis
   1.246 +      by (simp add: ac_simps)
   1.247 +  next
   1.248 +    case False
   1.249 +    then have "a mod b \<noteq> 0"
   1.250 +      by (simp add: mod_eq_0_iff_dvd)
   1.251 +    moreover from \<open>b \<noteq> 0\<close> \<open>\<not> b dvd a\<close> have "uniqueness_constraint (a mod b) b"
   1.252 +      by (rule uniqueness_constraint_mod)
   1.253 +    moreover have "euclidean_size (a mod b) < euclidean_size b"
   1.254 +      using \<open>b \<noteq> 0\<close> by (rule mod_size_less)
   1.255 +    moreover have "a = a div b * b + a mod b"
   1.256 +      by (simp add: div_mult_mod_eq)
   1.257 +    ultimately show thesis
   1.258 +      using \<open>b \<noteq> 0\<close> by (blast intro: remainder)
   1.259 +  qed
   1.260 +qed
   1.261 +
   1.262 +lemma div_eqI:
   1.263 +  "a div b = q" if "b \<noteq> 0" "uniqueness_constraint r b"
   1.264 +    "euclidean_size r < euclidean_size b" "q * b + r = a"
   1.265 +proof -
   1.266 +  from that have "(q * b + r) div b = q"
   1.267 +    by (auto intro: div_bounded)
   1.268 +  with that show ?thesis
   1.269 +    by simp
   1.270 +qed
   1.271 +
   1.272 +lemma mod_eqI:
   1.273 +  "a mod b = r" if "b \<noteq> 0" "uniqueness_constraint r b"
   1.274 +    "euclidean_size r < euclidean_size b" "q * b + r = a" 
   1.275 +proof -
   1.276 +  from that have "a div b = q"
   1.277 +    by (rule div_eqI)
   1.278 +  moreover have "a div b * b + a mod b = a"
   1.279 +    by (fact div_mult_mod_eq)
   1.280 +  ultimately have "a div b * b + a mod b = a div b * b + r"
   1.281 +    using \<open>q * b + r = a\<close> by simp
   1.282 +  then show ?thesis
   1.283 +    by simp
   1.284 +qed
   1.285 +
   1.286 +end
   1.287 +
   1.288 +class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
   1.289 +
   1.290 +end