author haftmann Sun Oct 08 22:28:21 2017 +0200 (19 months ago) changeset 66808 1907167b6038 parent 66807 c3631f32dfeb child 66809 f6a30d48aab0
elementary definition of division on natural numbers
 src/HOL/Computational_Algebra/Polynomial_Factorial.thy file | annotate | diff | revisions src/HOL/Divides.thy file | annotate | diff | revisions src/HOL/Euclidean_Division.thy file | annotate | diff | revisions src/HOL/Library/Code_Target_Nat.thy file | annotate | diff | revisions src/HOL/Library/RBT_Impl.thy file | annotate | diff | revisions src/HOL/Parity.thy file | annotate | diff | revisions src/HOL/Rings.thy file | annotate | diff | revisions src/HOL/Word/Word.thy file | annotate | diff | revisions src/HOL/Word/Word_Miscellaneous.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:21 2017 +0200
1.2 +++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:21 2017 +0200
1.3 @@ -15,7 +15,7 @@
1.4
1.5  definition to_fract :: "'a :: idom \<Rightarrow> 'a fract"
1.6    where "to_fract x = Fract x 1"
1.7 -  \<comment> \<open>FIXME: name \<open>of_idom\<close>, abbreviation\<close>
1.8 +  \<comment> \<open>FIXME: more idiomatic name, abbreviation\<close>
1.9
1.10  lemma to_fract_0 [simp]: "to_fract 0 = 0"
1.11    by (simp add: to_fract_def eq_fract Zero_fract_def)
1.12 @@ -438,8 +438,8 @@
1.14    show "comm_semiring_1.prime_elem times 1 0 = prime_elem"
1.16 -  show "class.unique_euclidean_ring divide plus minus (0 :: 'a poly) times 1 modulo
1.18 +  show "class.unique_euclidean_ring divide plus minus (0 :: 'a poly) times 1
1.19 +    (\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p) modulo
1.20      (\<lambda>p. if p = 0 then 0 else 2 ^ degree p) uminus top"
1.21    proof (standard, fold dvd_dict)
1.22      fix p :: "'a poly"
```
```     2.1 --- a/src/HOL/Divides.thy	Sun Oct 08 22:28:21 2017 +0200
2.2 +++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:21 2017 +0200
2.3 @@ -9,95 +9,6 @@
2.4  imports Parity
2.5  begin
2.6
2.7 -subsection \<open>Parity\<close>
2.8 -
2.9 -class unique_euclidean_semiring_parity = unique_euclidean_semiring +
2.10 -  assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
2.11 -  assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
2.12 -  assumes zero_not_eq_two: "0 \<noteq> 2"
2.13 -begin
2.14 -
2.15 -lemma parity_cases [case_names even odd]:
2.16 -  assumes "a mod 2 = 0 \<Longrightarrow> P"
2.17 -  assumes "a mod 2 = 1 \<Longrightarrow> P"
2.18 -  shows P
2.19 -  using assms parity by blast
2.20 -
2.21 -lemma one_div_two_eq_zero [simp]:
2.22 -  "1 div 2 = 0"
2.23 -proof (cases "2 = 0")
2.24 -  case True then show ?thesis by simp
2.25 -next
2.26 -  case False
2.27 -  from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
2.28 -  with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
2.29 -  then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
2.30 -  then have "1 div 2 = 0 \<or> 2 = 0" by simp
2.31 -  with False show ?thesis by auto
2.32 -qed
2.33 -
2.34 -lemma not_mod_2_eq_0_eq_1 [simp]:
2.35 -  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
2.36 -  by (cases a rule: parity_cases) simp_all
2.37 -
2.38 -lemma not_mod_2_eq_1_eq_0 [simp]:
2.39 -  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
2.40 -  by (cases a rule: parity_cases) simp_all
2.41 -
2.42 -subclass semiring_parity
2.43 -proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
2.44 -  show "1 mod 2 = 1"
2.45 -    by (fact one_mod_two_eq_one)
2.46 -next
2.47 -  fix a b
2.48 -  assume "a mod 2 = 1"
2.49 -  moreover assume "b mod 2 = 1"
2.50 -  ultimately show "(a + b) mod 2 = 0"
2.51 -    using mod_add_eq [of a 2 b] by simp
2.52 -next
2.53 -  fix a b
2.54 -  assume "(a * b) mod 2 = 0"
2.55 -  then have "(a mod 2) * (b mod 2) mod 2 = 0"
2.56 -    by (simp add: mod_mult_eq)
2.57 -  then have "(a mod 2) * (b mod 2) = 0"
2.58 -    by (cases "a mod 2 = 0") simp_all
2.59 -  then show "a mod 2 = 0 \<or> b mod 2 = 0"
2.60 -    by (rule divisors_zero)
2.61 -next
2.62 -  fix a
2.63 -  assume "a mod 2 = 1"
2.64 -  then have "a = a div 2 * 2 + 1"
2.65 -    using div_mult_mod_eq [of a 2] by simp
2.66 -  then show "\<exists>b. a = b + 1" ..
2.67 -qed
2.68 -
2.69 -lemma even_iff_mod_2_eq_zero:
2.70 -  "even a \<longleftrightarrow> a mod 2 = 0"
2.71 -  by (fact dvd_eq_mod_eq_0)
2.72 -
2.73 -lemma odd_iff_mod_2_eq_one:
2.74 -  "odd a \<longleftrightarrow> a mod 2 = 1"
2.75 -  by (simp add: even_iff_mod_2_eq_zero)
2.76 -
2.77 -lemma even_succ_div_two [simp]:
2.78 -  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
2.79 -  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
2.80 -
2.81 -lemma odd_succ_div_two [simp]:
2.82 -  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
2.84 -
2.85 -lemma even_two_times_div_two:
2.86 -  "even a \<Longrightarrow> 2 * (a div 2) = a"
2.87 -  by (fact dvd_mult_div_cancel)
2.88 -
2.89 -lemma odd_two_times_div_two_succ [simp]:
2.90 -  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
2.91 -  using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
2.92 -
2.93 -end
2.94 -
2.95 -
2.96  subsection \<open>Numeral division with a pragmatic type class\<close>
2.97
2.98  text \<open>
2.99 @@ -382,445 +293,11 @@
2.100
2.101  end
2.102
2.103 +hide_fact (open) div_less mod_less mod_less_eq_dividend mod_mult2_eq div_mult2_eq
2.104 +
2.105
2.106  subsection \<open>Division on @{typ nat}\<close>
2.107
2.108 -context
2.109 -begin
2.110 -
2.111 -text \<open>
2.112 -  We define @{const divide} and @{const modulo} on @{typ nat} by means
2.113 -  of a characteristic relation with two input arguments
2.114 -  @{term "m::nat"}, @{term "n::nat"} and two output arguments
2.115 -  @{term "q::nat"}(uotient) and @{term "r::nat"}(emainder).
2.116 -\<close>
2.117 -
2.118 -inductive eucl_rel_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool"
2.119 -  where eucl_rel_nat_by0: "eucl_rel_nat m 0 (0, m)"
2.120 -  | eucl_rel_natI: "r < n \<Longrightarrow> m = q * n + r \<Longrightarrow> eucl_rel_nat m n (q, r)"
2.121 -
2.122 -text \<open>@{const eucl_rel_nat} is total:\<close>
2.123 -
2.124 -qualified lemma eucl_rel_nat_ex:
2.125 -  obtains q r where "eucl_rel_nat m n (q, r)"
2.126 -proof (cases "n = 0")
2.127 -  case True
2.128 -  with that eucl_rel_nat_by0 show thesis
2.129 -    by blast
2.130 -next
2.131 -  case False
2.132 -  have "\<exists>q r. m = q * n + r \<and> r < n"
2.133 -  proof (induct m)
2.134 -    case 0 with \<open>n \<noteq> 0\<close>
2.135 -    have "(0::nat) = 0 * n + 0 \<and> 0 < n" by simp
2.136 -    then show ?case by blast
2.137 -  next
2.138 -    case (Suc m) then obtain q' r'
2.139 -      where m: "m = q' * n + r'" and n: "r' < n" by auto
2.140 -    then show ?case proof (cases "Suc r' < n")
2.141 -      case True
2.142 -      from m n have "Suc m = q' * n + Suc r'" by simp
2.143 -      with True show ?thesis by blast
2.144 -    next
2.145 -      case False then have "n \<le> Suc r'"
2.146 -        by (simp add: not_less)
2.147 -      moreover from n have "Suc r' \<le> n"
2.148 -        by (simp add: Suc_le_eq)
2.149 -      ultimately have "n = Suc r'" by auto
2.150 -      with m have "Suc m = Suc q' * n + 0" by simp
2.151 -      with \<open>n \<noteq> 0\<close> show ?thesis by blast
2.152 -    qed
2.153 -  qed
2.154 -  with that \<open>n \<noteq> 0\<close> eucl_rel_natI show thesis
2.155 -    by blast
2.156 -qed
2.157 -
2.158 -text \<open>@{const eucl_rel_nat} is injective:\<close>
2.159 -
2.160 -qualified lemma eucl_rel_nat_unique_div:
2.161 -  assumes "eucl_rel_nat m n (q, r)"
2.162 -    and "eucl_rel_nat m n (q', r')"
2.163 -  shows "q = q'"
2.164 -proof (cases "n = 0")
2.165 -  case True with assms show ?thesis
2.166 -    by (auto elim: eucl_rel_nat.cases)
2.167 -next
2.168 -  case False
2.169 -  have *: "q' \<le> q" if "q' * n + r' = q * n + r" "r < n" for q r q' r' :: nat
2.170 -  proof (rule ccontr)
2.171 -    assume "\<not> q' \<le> q"
2.172 -    then have "q < q'"
2.173 -      by (simp add: not_le)
2.174 -    with that show False
2.176 -  qed
2.177 -  from \<open>n \<noteq> 0\<close> assms show ?thesis
2.178 -    by (auto intro: order_antisym elim: eucl_rel_nat.cases dest: * sym split: if_splits)
2.179 -qed
2.180 -
2.181 -qualified lemma eucl_rel_nat_unique_mod:
2.182 -  assumes "eucl_rel_nat m n (q, r)"
2.183 -    and "eucl_rel_nat m n (q', r')"
2.184 -  shows "r = r'"
2.185 -proof -
2.186 -  from assms have "q' = q"
2.187 -    by (auto intro: eucl_rel_nat_unique_div)
2.188 -  with assms show ?thesis
2.189 -    by (auto elim!: eucl_rel_nat.cases)
2.190 -qed
2.191 -
2.192 -text \<open>
2.193 -  We instantiate divisibility on the natural numbers by
2.194 -  means of @{const eucl_rel_nat}:
2.195 -\<close>
2.196 -
2.197 -qualified definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
2.198 -  "divmod_nat m n = (THE qr. eucl_rel_nat m n qr)"
2.199 -
2.200 -qualified lemma eucl_rel_nat_divmod_nat:
2.201 -  "eucl_rel_nat m n (divmod_nat m n)"
2.202 -proof -
2.203 -  from eucl_rel_nat_ex
2.204 -    obtain q r where rel: "eucl_rel_nat m n (q, r)" .
2.205 -  then show ?thesis
2.206 -    by (auto simp add: divmod_nat_def intro: theI
2.207 -      elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
2.208 -qed
2.209 -
2.210 -qualified lemma divmod_nat_unique:
2.211 -  "divmod_nat m n = (q, r)" if "eucl_rel_nat m n (q, r)"
2.212 -  using that
2.213 -  by (auto simp add: divmod_nat_def intro: eucl_rel_nat_divmod_nat elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
2.214 -
2.215 -qualified lemma divmod_nat_zero:
2.216 -  "divmod_nat m 0 = (0, m)"
2.217 -  by (rule divmod_nat_unique) (fact eucl_rel_nat_by0)
2.218 -
2.219 -qualified lemma divmod_nat_zero_left:
2.220 -  "divmod_nat 0 n = (0, 0)"
2.221 -  by (rule divmod_nat_unique)
2.222 -    (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
2.223 -
2.224 -qualified lemma divmod_nat_base:
2.225 -  "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
2.226 -  by (rule divmod_nat_unique)
2.227 -    (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
2.228 -
2.229 -qualified lemma divmod_nat_step:
2.230 -  assumes "0 < n" and "n \<le> m"
2.231 -  shows "divmod_nat m n =
2.232 -    (Suc (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
2.233 -proof (rule divmod_nat_unique)
2.234 -  have "eucl_rel_nat (m - n) n (divmod_nat (m - n) n)"
2.235 -    by (fact eucl_rel_nat_divmod_nat)
2.236 -  then show "eucl_rel_nat m n (Suc
2.237 -    (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
2.238 -    using assms
2.239 -      by (auto split: if_splits intro: eucl_rel_natI elim!: eucl_rel_nat.cases simp add: algebra_simps)
2.240 -qed
2.241 -
2.242 -end
2.243 -
2.244 -instantiation nat :: "{semidom_modulo, normalization_semidom}"
2.245 -begin
2.246 -
2.247 -definition normalize_nat :: "nat \<Rightarrow> nat"
2.248 -  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
2.249 -
2.250 -definition unit_factor_nat :: "nat \<Rightarrow> nat"
2.251 -  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
2.252 -
2.253 -lemma unit_factor_simps [simp]:
2.254 -  "unit_factor 0 = (0::nat)"
2.255 -  "unit_factor (Suc n) = 1"
2.256 -  by (simp_all add: unit_factor_nat_def)
2.257 -
2.258 -definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
2.259 -  where div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
2.260 -
2.261 -definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
2.262 -  where mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)"
2.263 -
2.264 -lemma fst_divmod_nat [simp]:
2.265 -  "fst (Divides.divmod_nat m n) = m div n"
2.266 -  by (simp add: div_nat_def)
2.267 -
2.268 -lemma snd_divmod_nat [simp]:
2.269 -  "snd (Divides.divmod_nat m n) = m mod n"
2.270 -  by (simp add: mod_nat_def)
2.271 -
2.272 -lemma divmod_nat_div_mod:
2.273 -  "Divides.divmod_nat m n = (m div n, m mod n)"
2.274 -  by (simp add: prod_eq_iff)
2.275 -
2.276 -lemma div_nat_unique:
2.277 -  assumes "eucl_rel_nat m n (q, r)"
2.278 -  shows "m div n = q"
2.279 -  using assms
2.280 -  by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
2.281 -
2.282 -lemma mod_nat_unique:
2.283 -  assumes "eucl_rel_nat m n (q, r)"
2.284 -  shows "m mod n = r"
2.285 -  using assms
2.286 -  by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
2.287 -
2.288 -lemma eucl_rel_nat: "eucl_rel_nat m n (m div n, m mod n)"
2.289 -  using Divides.eucl_rel_nat_divmod_nat
2.290 -  by (simp add: divmod_nat_div_mod)
2.291 -
2.292 -text \<open>The ''recursion'' equations for @{const divide} and @{const modulo}\<close>
2.293 -
2.294 -lemma div_less [simp]:
2.295 -  fixes m n :: nat
2.296 -  assumes "m < n"
2.297 -  shows "m div n = 0"
2.298 -  using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
2.299 -
2.300 -lemma le_div_geq:
2.301 -  fixes m n :: nat
2.302 -  assumes "0 < n" and "n \<le> m"
2.303 -  shows "m div n = Suc ((m - n) div n)"
2.304 -  using assms Divides.divmod_nat_step by (simp add: prod_eq_iff)
2.305 -
2.306 -lemma mod_less [simp]:
2.307 -  fixes m n :: nat
2.308 -  assumes "m < n"
2.309 -  shows "m mod n = m"
2.310 -  using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
2.311 -
2.312 -lemma le_mod_geq:
2.313 -  fixes m n :: nat
2.314 -  assumes "n \<le> m"
2.315 -  shows "m mod n = (m - n) mod n"
2.316 -  using assms Divides.divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
2.317 -
2.318 -lemma mod_less_divisor [simp]:
2.319 -  fixes m n :: nat
2.320 -  assumes "n > 0"
2.321 -  shows "m mod n < n"
2.322 -  using assms eucl_rel_nat [of m n]
2.323 -    by (auto elim: eucl_rel_nat.cases)
2.324 -
2.325 -lemma mod_le_divisor [simp]:
2.326 -  fixes m n :: nat
2.327 -  assumes "n > 0"
2.328 -  shows "m mod n \<le> n"
2.329 -  using assms eucl_rel_nat [of m n]
2.330 -    by (auto elim: eucl_rel_nat.cases)
2.331 -
2.332 -instance proof
2.333 -  fix m n :: nat
2.334 -  show "m div n * n + m mod n = m"
2.335 -    using eucl_rel_nat [of m n]
2.336 -    by (auto elim: eucl_rel_nat.cases)
2.337 -next
2.338 -  fix n :: nat show "n div 0 = 0"
2.339 -    by (simp add: div_nat_def Divides.divmod_nat_zero)
2.340 -next
2.341 -  fix m n :: nat
2.342 -  assume "n \<noteq> 0"
2.343 -  then show "m * n div n = m"
2.344 -    by (auto intro!: eucl_rel_natI div_nat_unique [of _ _ _ 0])
2.346 -
2.347 -end
2.348 -
2.349 -text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close>
2.350 -
2.351 -lemma (in semiring_modulo) cancel_div_mod_rules:
2.352 -  "((a div b) * b + a mod b) + c = a + c"
2.353 -  "(b * (a div b) + a mod b) + c = a + c"
2.354 -  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
2.355 -
2.356 -ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
2.357 -
2.358 -ML \<open>
2.359 -structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
2.360 -(
2.361 -  val div_name = @{const_name divide};
2.362 -  val mod_name = @{const_name modulo};
2.363 -  val mk_binop = HOLogic.mk_binop;
2.364 -  val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
2.365 -  val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
2.366 -  fun mk_sum [] = HOLogic.zero
2.367 -    | mk_sum [t] = t
2.368 -    | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
2.369 -  fun dest_sum tm =
2.370 -    if HOLogic.is_zero tm then []
2.371 -    else
2.372 -      (case try HOLogic.dest_Suc tm of
2.373 -        SOME t => HOLogic.Suc_zero :: dest_sum t
2.374 -      | NONE =>
2.375 -          (case try dest_plus tm of
2.376 -            SOME (t, u) => dest_sum t @ dest_sum u
2.377 -          | NONE => [tm]));
2.378 -
2.379 -  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
2.380 -
2.381 -  val prove_eq_sums = Arith_Data.prove_conv2 all_tac
2.383 -)
2.384 -\<close>
2.385 -
2.386 -simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
2.387 -  \<open>K Cancel_Div_Mod_Nat.proc\<close>
2.388 -
2.389 -lemma div_by_Suc_0 [simp]:
2.390 -  "m div Suc 0 = m"
2.391 -  using div_by_1 [of m] by simp
2.392 -
2.393 -lemma mod_by_Suc_0 [simp]:
2.394 -  "m mod Suc 0 = 0"
2.395 -  using mod_by_1 [of m] by simp
2.396 -
2.397 -lemma mod_greater_zero_iff_not_dvd:
2.398 -  fixes m n :: nat
2.399 -  shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
2.400 -  by (simp add: dvd_eq_mod_eq_0)
2.401 -
2.402 -instantiation nat :: unique_euclidean_semiring
2.403 -begin
2.404 -
2.405 -definition [simp]:
2.406 -  "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
2.407 -
2.408 -definition [simp]:
2.409 -  "uniqueness_constraint_nat = (top :: nat \<Rightarrow> nat \<Rightarrow> bool)"
2.410 -
2.411 -instance proof
2.412 -  fix n q r :: nat
2.413 -  assume "euclidean_size r < euclidean_size n"
2.414 -  then have "n > r"
2.415 -    by simp_all
2.416 -  then have "eucl_rel_nat (q * n + r) n (q, r)"
2.417 -    by (rule eucl_rel_natI) rule
2.418 -  then show "(q * n + r) div n = q"
2.419 -    by (rule div_nat_unique)
2.420 -qed (use mult_le_mono2 [of 1] in \<open>simp_all\<close>)
2.421 -
2.422 -end
2.423 -
2.424 -lemma divmod_nat_if [code]:
2.425 -  "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
2.426 -    let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
2.427 -  by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
2.428 -
2.429 -lemma mod_Suc_eq [mod_simps]:
2.430 -  "Suc (m mod n) mod n = Suc m mod n"
2.431 -proof -
2.432 -  have "(m mod n + 1) mod n = (m + 1) mod n"
2.433 -    by (simp only: mod_simps)
2.434 -  then show ?thesis
2.435 -    by simp
2.436 -qed
2.437 -
2.438 -lemma mod_Suc_Suc_eq [mod_simps]:
2.439 -  "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
2.440 -proof -
2.441 -  have "(m mod n + 2) mod n = (m + 2) mod n"
2.442 -    by (simp only: mod_simps)
2.443 -  then show ?thesis
2.444 -    by simp
2.445 -qed
2.446 -
2.447 -
2.448 -subsubsection \<open>Quotient\<close>
2.449 -
2.450 -lemma div_geq: "0 < n \<Longrightarrow>  \<not> m < n \<Longrightarrow> m div n = Suc ((m - n) div n)"
2.451 -by (simp add: le_div_geq linorder_not_less)
2.452 -
2.453 -lemma div_if: "0 < n \<Longrightarrow> m div n = (if m < n then 0 else Suc ((m - n) div n))"
2.455 -
2.456 -lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
2.457 -by simp
2.458 -
2.459 -lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
2.460 -by simp
2.461 -
2.462 -lemma div_positive:
2.463 -  fixes m n :: nat
2.464 -  assumes "n > 0"
2.465 -  assumes "m \<ge> n"
2.466 -  shows "m div n > 0"
2.467 -proof -
2.468 -  from \<open>m \<ge> n\<close> obtain q where "m = n + q"
2.470 -  with \<open>n > 0\<close> show ?thesis by (simp add: div_add_self1)
2.471 -qed
2.472 -
2.473 -lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"
2.474 -  by auto (metis div_positive less_numeral_extra(3) not_less)
2.475 -
2.476 -
2.477 -subsubsection \<open>Remainder\<close>
2.478 -
2.479 -lemma mod_Suc_le_divisor [simp]:
2.480 -  "m mod Suc n \<le> n"
2.481 -  using mod_less_divisor [of "Suc n" m] by arith
2.482 -
2.483 -lemma mod_less_eq_dividend [simp]:
2.484 -  fixes m n :: nat
2.485 -  shows "m mod n \<le> m"
2.487 -  from div_mult_mod_eq have "m div n * n + m mod n = m" .
2.488 -  then show "m div n * n + m mod n \<le> m" by auto
2.489 -qed
2.490 -
2.491 -lemma mod_geq: "\<not> m < (n::nat) \<Longrightarrow> m mod n = (m - n) mod n"
2.492 -by (simp add: le_mod_geq linorder_not_less)
2.493 -
2.494 -lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)"
2.496 -
2.497 -
2.498 -subsubsection \<open>Quotient and Remainder\<close>
2.499 -
2.500 -lemma div_mult1_eq:
2.501 -  "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
2.502 -  by (cases "c = 0")
2.503 -     (auto simp add: algebra_simps distrib_left [symmetric]
2.504 -     intro!: div_nat_unique [of _ _ _ "(a * (b mod c)) mod c"] eucl_rel_natI)
2.505 -
2.507 -  "eucl_rel_nat a c (aq, ar) \<Longrightarrow> eucl_rel_nat b c (bq, br)
2.508 -   \<Longrightarrow> eucl_rel_nat (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
2.509 -  by (auto simp add: split_ifs algebra_simps elim!: eucl_rel_nat.cases intro: eucl_rel_nat_by0 eucl_rel_natI)
2.510 -
2.511 -(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
2.513 -  "(a + b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
2.514 -by (blast intro: eucl_rel_nat_add1_eq [THEN div_nat_unique] eucl_rel_nat)
2.515 -
2.516 -lemma eucl_rel_nat_mult2_eq:
2.517 -  assumes "eucl_rel_nat a b (q, r)"
2.518 -  shows "eucl_rel_nat a (b * c) (q div c, b *(q mod c) + r)"
2.519 -proof (cases "c = 0")
2.520 -  case True
2.521 -  with assms show ?thesis
2.522 -    by (auto intro: eucl_rel_nat_by0 elim!: eucl_rel_nat.cases simp add: ac_simps)
2.523 -next
2.524 -  case False
2.525 -  { assume "r < b"
2.526 -    with False have "b * (q mod c) + r < b * c"
2.527 -      apply (cut_tac m = q and n = c in mod_less_divisor)
2.528 -      apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
2.529 -      apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
2.531 -      done
2.532 -    then have "r + b * (q mod c) < b * c"
2.533 -      by (simp add: ac_simps)
2.534 -  } with assms False show ?thesis
2.535 -    by (auto simp add: algebra_simps add_mult_distrib2 [symmetric] elim!: eucl_rel_nat.cases intro: eucl_rel_nat.intros)
2.536 -qed
2.537 -
2.538 -lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
2.539 -by (force simp add: eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN div_nat_unique])
2.540 -
2.541 -lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
2.542 -by (auto simp add: mult.commute eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN mod_nat_unique])
2.543 -
2.544  instantiation nat :: unique_euclidean_semiring_numeral
2.545  begin
2.546
2.547 @@ -834,370 +311,15 @@
2.548      in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
2.549      else (2 * q, r))"
2.550
2.551 -instance
2.552 -  by standard (auto intro: div_positive simp add: divmod'_nat_def divmod_step_nat_def mod_mult2_eq div_mult2_eq)
2.553 +instance by standard
2.554 +  (auto simp add: divmod'_nat_def divmod_step_nat_def div_greater_zero_iff div_mult2_eq mod_mult2_eq)
2.555
2.556  end
2.557
2.558  declare divmod_algorithm_code [where ?'a = nat, code]
2.559 -
2.560
2.561 -subsubsection \<open>Further Facts about Quotient and Remainder\<close>
2.562 -
2.563 -lemma div_le_mono:
2.564 -  fixes m n k :: nat
2.565 -  assumes "m \<le> n"
2.566 -  shows "m div k \<le> n div k"
2.567 -proof -
2.568 -  from assms obtain q where "n = m + q"
2.570 -  then show ?thesis
2.572 -qed
2.573 -
2.574 -(* Antimonotonicity of div in second argument *)
2.575 -lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
2.576 -apply (subgoal_tac "0<n")
2.577 - prefer 2 apply simp
2.578 -apply (induct_tac k rule: nat_less_induct)
2.579 -apply (rename_tac "k")
2.580 -apply (case_tac "k<n", simp)
2.581 -apply (subgoal_tac "~ (k<m) ")
2.582 - prefer 2 apply simp
2.584 -apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")
2.585 - prefer 2
2.586 - apply (blast intro: div_le_mono diff_le_mono2)
2.587 -apply (rule le_trans, simp)
2.588 -apply (simp)
2.589 -done
2.590 -
2.591 -lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
2.592 -apply (case_tac "n=0", simp)
2.593 -apply (subgoal_tac "m div n \<le> m div 1", simp)
2.594 -apply (rule div_le_mono2)
2.595 -apply (simp_all (no_asm_simp))
2.596 -done
2.597 -
2.598 -(* Similar for "less than" *)
2.599 -lemma div_less_dividend [simp]:
2.600 -  "\<lbrakk>(1::nat) < n; 0 < m\<rbrakk> \<Longrightarrow> m div n < m"
2.601 -apply (induct m rule: nat_less_induct)
2.602 -apply (rename_tac "m")
2.603 -apply (case_tac "m<n", simp)
2.604 -apply (subgoal_tac "0<n")
2.605 - prefer 2 apply simp
2.607 -apply (case_tac "n<m")
2.608 - apply (subgoal_tac "(m-n) div n < (m-n) ")
2.609 -  apply (rule impI less_trans_Suc)+
2.610 -apply assumption
2.611 -  apply (simp_all)
2.612 -done
2.613 -
2.614 -text\<open>A fact for the mutilated chess board\<close>
2.615 -lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
2.616 -apply (case_tac "n=0", simp)
2.617 -apply (induct "m" rule: nat_less_induct)
2.618 -apply (case_tac "Suc (na) <n")
2.619 -(* case Suc(na) < n *)
2.620 -apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
2.621 -(* case n \<le> Suc(na) *)
2.622 -apply (simp add: linorder_not_less le_Suc_eq mod_geq)
2.623 -apply (auto simp add: Suc_diff_le le_mod_geq)
2.624 -done
2.625 -
2.626 -lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
2.627 -by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
2.628 -
2.629 -lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
2.630 -
2.631 -(*Loses information, namely we also have r<d provided d is nonzero*)
2.632 -lemma mod_eqD:
2.633 -  fixes m d r q :: nat
2.634 -  assumes "m mod d = r"
2.635 -  shows "\<exists>q. m = r + q * d"
2.636 -proof -
2.637 -  from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
2.638 -  with assms have "m = r + q * d" by simp
2.639 -  then show ?thesis ..
2.640 -qed
2.641 -
2.642 -lemma split_div:
2.643 - "P(n div k :: nat) =
2.644 - ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
2.645 - (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
2.646 -proof
2.647 -  assume P: ?P
2.648 -  show ?Q
2.649 -  proof (cases)
2.650 -    assume "k = 0"
2.651 -    with P show ?Q by simp
2.652 -  next
2.653 -    assume not0: "k \<noteq> 0"
2.654 -    thus ?Q
2.655 -    proof (simp, intro allI impI)
2.656 -      fix i j
2.657 -      assume n: "n = k*i + j" and j: "j < k"
2.658 -      show "P i"
2.659 -      proof (cases)
2.660 -        assume "i = 0"
2.661 -        with n j P show "P i" by simp
2.662 -      next
2.663 -        assume "i \<noteq> 0"
2.664 -        with not0 n j P show "P i" by(simp add:ac_simps)
2.665 -      qed
2.666 -    qed
2.667 -  qed
2.668 -next
2.669 -  assume Q: ?Q
2.670 -  show ?P
2.671 -  proof (cases)
2.672 -    assume "k = 0"
2.673 -    with Q show ?P by simp
2.674 -  next
2.675 -    assume not0: "k \<noteq> 0"
2.676 -    with Q have R: ?R by simp
2.677 -    from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
2.678 -    show ?P by simp
2.679 -  qed
2.680 -qed
2.681 -
2.682 -lemma split_div_lemma:
2.683 -  assumes "0 < n"
2.684 -  shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m::nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")
2.685 -proof
2.686 -  assume ?rhs
2.687 -  with minus_mod_eq_mult_div [symmetric] have nq: "n * q = m - (m mod n)" by simp
2.688 -  then have A: "n * q \<le> m" by simp
2.689 -  have "n - (m mod n) > 0" using mod_less_divisor assms by auto
2.690 -  then have "m < m + (n - (m mod n))" by simp
2.691 -  then have "m < n + (m - (m mod n))" by simp
2.692 -  with nq have "m < n + n * q" by simp
2.693 -  then have B: "m < n * Suc q" by simp
2.694 -  from A B show ?lhs ..
2.695 -next
2.696 -  assume P: ?lhs
2.697 -  then have "eucl_rel_nat m n (q, m - n * q)"
2.698 -    by (auto intro: eucl_rel_natI simp add: ac_simps)
2.699 -  then have "m div n = q"
2.700 -    by (rule div_nat_unique)
2.701 -  then show ?rhs by simp
2.702 -qed
2.703 -
2.704 -theorem split_div':
2.705 -  "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
2.706 -   (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
2.707 -  apply (cases "0 < n")
2.708 -  apply (simp only: add: split_div_lemma)
2.709 -  apply simp_all
2.710 -  done
2.711 -
2.712 -lemma split_mod:
2.713 - "P(n mod k :: nat) =
2.714 - ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
2.715 - (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
2.716 -proof
2.717 -  assume P: ?P
2.718 -  show ?Q
2.719 -  proof (cases)
2.720 -    assume "k = 0"
2.721 -    with P show ?Q by simp
2.722 -  next
2.723 -    assume not0: "k \<noteq> 0"
2.724 -    thus ?Q
2.725 -    proof (simp, intro allI impI)
2.726 -      fix i j
2.727 -      assume "n = k*i + j" "j < k"
2.728 -      thus "P j" using not0 P by (simp add: ac_simps)
2.729 -    qed
2.730 -  qed
2.731 -next
2.732 -  assume Q: ?Q
2.733 -  show ?P
2.734 -  proof (cases)
2.735 -    assume "k = 0"
2.736 -    with Q show ?P by simp
2.737 -  next
2.738 -    assume not0: "k \<noteq> 0"
2.739 -    with Q have R: ?R by simp
2.740 -    from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
2.741 -    show ?P by simp
2.742 -  qed
2.743 -qed
2.744 -
2.745 -lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
2.746 -  apply rule
2.747 -  apply (cases "b = 0")
2.748 -  apply simp_all
2.749 -  apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)
2.750 -  done
2.751 -
2.752 -lemma (in field_char_0) of_nat_div:
2.753 -  "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
2.754 -proof -
2.755 -  have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
2.756 -    unfolding of_nat_add by (cases "n = 0") simp_all
2.757 -  then show ?thesis
2.758 -    by simp
2.759 -qed
2.760 -
2.761 -
2.762 -subsubsection \<open>An ``induction'' law for modulus arithmetic.\<close>
2.763 -
2.764 -lemma mod_induct_0:
2.765 -  assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
2.766 -  and base: "P i" and i: "i<p"
2.767 -  shows "P 0"
2.768 -proof (rule ccontr)
2.769 -  assume contra: "\<not>(P 0)"
2.770 -  from i have p: "0<p" by simp
2.771 -  have "\<forall>k. 0<k \<longrightarrow> \<not> P (p-k)" (is "\<forall>k. ?A k")
2.772 -  proof
2.773 -    fix k
2.774 -    show "?A k"
2.775 -    proof (induct k)
2.776 -      show "?A 0" by simp  \<comment> "by contradiction"
2.777 -    next
2.778 -      fix n
2.779 -      assume ih: "?A n"
2.780 -      show "?A (Suc n)"
2.781 -      proof (clarsimp)
2.782 -        assume y: "P (p - Suc n)"
2.783 -        have n: "Suc n < p"
2.784 -        proof (rule ccontr)
2.785 -          assume "\<not>(Suc n < p)"
2.786 -          hence "p - Suc n = 0"
2.787 -            by simp
2.788 -          with y contra show "False"
2.789 -            by simp
2.790 -        qed
2.791 -        hence n2: "Suc (p - Suc n) = p-n" by arith
2.792 -        from p have "p - Suc n < p" by arith
2.793 -        with y step have z: "P ((Suc (p - Suc n)) mod p)"
2.794 -          by blast
2.795 -        show "False"
2.796 -        proof (cases "n=0")
2.797 -          case True
2.798 -          with z n2 contra show ?thesis by simp
2.799 -        next
2.800 -          case False
2.801 -          with p have "p-n < p" by arith
2.802 -          with z n2 False ih show ?thesis by simp
2.803 -        qed
2.804 -      qed
2.805 -    qed
2.806 -  qed
2.807 -  moreover
2.808 -  from i obtain k where "0<k \<and> i+k=p"
2.809 -    by (blast dest: less_imp_add_positive)
2.810 -  hence "0<k \<and> i=p-k" by auto
2.811 -  moreover
2.812 -  note base
2.813 -  ultimately
2.814 -  show "False" by blast
2.815 -qed
2.816 -
2.817 -lemma mod_induct:
2.818 -  assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
2.819 -  and base: "P i" and i: "i<p" and j: "j<p"
2.820 -  shows "P j"
2.821 -proof -
2.822 -  have "\<forall>j<p. P j"
2.823 -  proof
2.824 -    fix j
2.825 -    show "j<p \<longrightarrow> P j" (is "?A j")
2.826 -    proof (induct j)
2.827 -      from step base i show "?A 0"
2.828 -        by (auto elim: mod_induct_0)
2.829 -    next
2.830 -      fix k
2.831 -      assume ih: "?A k"
2.832 -      show "?A (Suc k)"
2.833 -      proof
2.834 -        assume suc: "Suc k < p"
2.835 -        hence k: "k<p" by simp
2.836 -        with ih have "P k" ..
2.837 -        with step k have "P (Suc k mod p)"
2.838 -          by blast
2.839 -        moreover
2.840 -        from suc have "Suc k mod p = Suc k"
2.841 -          by simp
2.842 -        ultimately
2.843 -        show "P (Suc k)" by simp
2.844 -      qed
2.845 -    qed
2.846 -  qed
2.847 -  with j show ?thesis by blast
2.848 -qed
2.849 -
2.850 -lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)"
2.851 -  by (simp add: numeral_2_eq_2 le_div_geq)
2.852 -
2.853 -lemma mod2_Suc_Suc [simp]: "Suc (Suc m) mod 2 = m mod 2"
2.854 -  by (simp add: numeral_2_eq_2 le_mod_geq)
2.855 -
2.856 -lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
2.857 -by (simp add: mult_2 [symmetric])
2.858 -
2.859 -lemma mod2_gr_0 [simp]: "0 < (m::nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
2.860 -proof -
2.861 -  { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all }
2.862 -  moreover have "m mod 2 < 2" by simp
2.863 -  ultimately have "m mod 2 = 0 \<or> m mod 2 = 1" .
2.864 -  then show ?thesis by auto
2.865 -qed
2.866 -
2.867 -text\<open>These lemmas collapse some needless occurrences of Suc:
2.868 -    at least three Sucs, since two and fewer are rewritten back to Suc again!
2.869 -    We already have some rules to simplify operands smaller than 3.\<close>
2.870 -
2.871 -lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
2.873 -
2.874 -lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
2.876 -
2.877 -lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
2.879 -
2.880 -lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
2.882 -
2.883 -lemmas Suc_div_eq_add3_div_numeral [simp] = Suc_div_eq_add3_div [of _ "numeral v"] for v
2.884 -lemmas Suc_mod_eq_add3_mod_numeral [simp] = Suc_mod_eq_add3_mod [of _ "numeral v"] for v
2.885 -
2.886 -lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1"
2.887 -apply (induct "m")
2.889 -done
2.890 -
2.891 -declare Suc_times_mod_eq [of "numeral w", simp] for w
2.892 -
2.893 -lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"
2.895 -
2.896 -lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
2.897 -by (cases n) simp_all
2.898 -
2.899 -lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2"
2.900 -proof -
2.901 -  from A have B: "0 < n - 1" and C: "n - 1 + 1 = n" by simp_all
2.902 -  from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp
2.903 -qed
2.904 -
2.905 -lemma mod_mult_self3' [simp]: "Suc (k * n + m) mod n = Suc m mod n"
2.906 -  using mod_mult_self3 [of k n "Suc m"] by simp
2.907 -
2.908 -lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
2.909 -apply (subst mod_Suc [of m])
2.910 -apply (subst mod_Suc [of "m mod n"], simp)
2.911 -done
2.912 -
2.913 -lemma mod_2_not_eq_zero_eq_one_nat:
2.914 -  fixes n :: nat
2.915 -  shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
2.916 -  by (fact not_mod_2_eq_0_eq_1)
2.917 +lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
2.918 +  by (auto elim: oddE)
2.919
2.920  lemma even_Suc_div_two [simp]:
2.921    "even n \<Longrightarrow> Suc n div 2 = n div 2"
2.922 @@ -1245,6 +367,11 @@
2.923    qed
2.924  qed
2.925
2.926 +lemma mod_2_not_eq_zero_eq_one_nat:
2.927 +  fixes n :: nat
2.928 +  shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
2.929 +  by (fact not_mod_2_eq_0_eq_1)
2.930 +
2.931  lemma Suc_0_div_numeral [simp]:
2.932    fixes k l :: num
2.933    shows "Suc 0 div numeral k = fst (divmod Num.One k)"
2.934 @@ -1255,6 +382,27 @@
2.935    shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
2.937
2.938 +definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
2.939 +  where "divmod_nat m n = (m div n, m mod n)"
2.940 +
2.941 +lemma fst_divmod_nat [simp]:
2.942 +  "fst (divmod_nat m n) = m div n"
2.943 +  by (simp add: divmod_nat_def)
2.944 +
2.945 +lemma snd_divmod_nat [simp]:
2.946 +  "snd (divmod_nat m n) = m mod n"
2.947 +  by (simp add: divmod_nat_def)
2.948 +
2.949 +lemma divmod_nat_if [code]:
2.950 +  "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
2.951 +    let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
2.952 +  by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
2.953 +
2.954 +lemma [code]:
2.955 +  "m div n = fst (divmod_nat m n)"
2.956 +  "m mod n = snd (divmod_nat m n)"
2.957 +  by simp_all
2.958 +
2.959
2.960  subsection \<open>Division on @{typ int}\<close>
2.961
2.962 @@ -2225,7 +1373,7 @@
2.963  lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
2.964  apply (subgoal_tac "nat x div nat k < nat x")
2.965   apply (simp add: nat_div_distrib [symmetric])
2.966 -apply (rule Divides.div_less_dividend, simp_all)
2.967 +apply (rule div_less_dividend, simp_all)
2.968  done
2.969
2.970  lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
2.971 @@ -2258,11 +1406,12 @@
2.972    thus  ?lhs by simp
2.973  qed
2.974
2.975 +
2.976  subsubsection \<open>Dedicated simproc for calculation\<close>
2.977
2.978  text \<open>
2.979    There is space for improvement here: the calculation itself
2.980 -  could be carried outside the logic, and a generic simproc
2.981 +  could be carried out outside the logic, and a generic simproc
2.982    (simplifier setup) for generic calculation would be helpful.
2.983  \<close>
2.984
2.985 @@ -2348,4 +1497,39 @@
2.986
2.987  declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
2.988
2.989 +
2.990 +subsubsection \<open>Lemmas of doubtful value\<close>
2.991 +
2.992 +lemma mod_mult_self3':
2.993 +  "Suc (k * n + m) mod n = Suc m mod n"
2.994 +  by (fact Suc_mod_mult_self3)
2.995 +
2.996 +lemma mod_Suc_eq_Suc_mod:
2.997 +  "Suc m mod n = Suc (m mod n) mod n"
2.998 +  by (simp add: mod_simps)
2.999 +
2.1000 +lemma div_geq:
2.1001 +  "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
2.1002 +  by (rule le_div_geq) (use that in \<open>simp_all add: not_less\<close>)
2.1003 +
2.1004 +lemma mod_geq:
2.1005 +  "m mod n = (m - n) mod n" if "\<not> m < n" for m n :: nat
2.1006 +  by (rule le_mod_geq) (use that in \<open>simp add: not_less\<close>)
2.1007 +
2.1008 +lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
2.1009 +  by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
2.1010 +
2.1011 +lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
2.1012 +
2.1013 +(*Loses information, namely we also have r<d provided d is nonzero*)
2.1014 +lemma mod_eqD:
2.1015 +  fixes m d r q :: nat
2.1016 +  assumes "m mod d = r"
2.1017 +  shows "\<exists>q. m = r + q * d"
2.1018 +proof -
2.1019 +  from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
2.1020 +  with assms have "m = r + q * d" by simp
2.1021 +  then show ?thesis ..
2.1022 +qed
2.1023 +
2.1024  end
```
```     3.1 --- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
3.2 +++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
3.3 @@ -6,9 +6,19 @@
3.4  section \<open>Uniquely determined division in euclidean (semi)rings\<close>
3.5
3.6  theory Euclidean_Division
3.7 -  imports Nat_Transfer
3.8 +  imports Nat_Transfer Lattices_Big
3.9  begin
3.10
3.11 +subsection \<open>Prelude: simproc for cancelling @{const divide} and @{const modulo}\<close>
3.12 +
3.13 +lemma (in semiring_modulo) cancel_div_mod_rules:
3.14 +  "((a div b) * b + a mod b) + c = a + c"
3.15 +  "(b * (a div b) + a mod b) + c = a + c"
3.16 +  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
3.17 +
3.18 +ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
3.19 +
3.20 +
3.21  subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
3.22
3.23  class euclidean_semiring = semidom_modulo + normalization_semidom +
3.24 @@ -639,4 +649,657 @@
3.25
3.26  end
3.27
3.28 +
3.29 +subsection \<open>Euclidean division on @{typ nat}\<close>
3.30 +
3.31 +instantiation nat :: unique_euclidean_semiring
3.32 +begin
3.33 +
3.34 +definition normalize_nat :: "nat \<Rightarrow> nat"
3.35 +  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
3.36 +
3.37 +definition unit_factor_nat :: "nat \<Rightarrow> nat"
3.38 +  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
3.39 +
3.40 +lemma unit_factor_simps [simp]:
3.41 +  "unit_factor 0 = (0::nat)"
3.42 +  "unit_factor (Suc n) = 1"
3.43 +  by (simp_all add: unit_factor_nat_def)
3.44 +
3.45 +definition euclidean_size_nat :: "nat \<Rightarrow> nat"
3.46 +  where [simp]: "euclidean_size_nat = id"
3.47 +
3.48 +definition uniqueness_constraint_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
3.49 +  where [simp]: "uniqueness_constraint_nat = \<top>"
3.50 +
3.51 +definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
3.52 +  where "m div n = (if n = 0 then 0 else Max {k::nat. k * n \<le> m})"
3.53 +
3.54 +definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
3.55 +  where "m mod n = m - (m div n * (n::nat))"
3.56 +
3.57 +instance proof
3.58 +  fix m n :: nat
3.59 +  have ex: "\<exists>k. k * n \<le> l" for l :: nat
3.60 +    by (rule exI [of _ 0]) simp
3.61 +  have fin: "finite {k. k * n \<le> l}" if "n > 0" for l
3.62 +  proof -
3.63 +    from that have "{k. k * n \<le> l} \<subseteq> {k. k \<le> l}"
3.64 +      by (cases n) auto
3.65 +    then show ?thesis
3.66 +      by (rule finite_subset) simp
3.67 +  qed
3.68 +  have mult_div_unfold: "n * (m div n) = Max {l. l \<le> m \<and> n dvd l}"
3.69 +  proof (cases "n = 0")
3.70 +    case True
3.71 +    moreover have "{l. l = 0 \<and> l \<le> m} = {0::nat}"
3.72 +      by auto
3.73 +    ultimately show ?thesis
3.74 +      by simp
3.75 +  next
3.76 +    case False
3.77 +    with ex [of m] fin have "n * Max {k. k * n \<le> m} = Max (times n ` {k. k * n \<le> m})"
3.78 +      by (auto simp add: nat_mult_max_right intro: hom_Max_commute)
3.79 +    also have "times n ` {k. k * n \<le> m} = {l. l \<le> m \<and> n dvd l}"
3.80 +      by (auto simp add: ac_simps elim!: dvdE)
3.81 +    finally show ?thesis
3.82 +      using False by (simp add: divide_nat_def ac_simps)
3.83 +  qed
3.84 +  show "n div 0 = 0"
3.85 +    by (simp add: divide_nat_def)
3.86 +  have less_eq: "m div n * n \<le> m"
3.87 +    by (auto simp add: mult_div_unfold ac_simps intro: Max.boundedI)
3.88 +  then show "m div n * n + m mod n = m"
3.89 +    by (simp add: modulo_nat_def)
3.90 +  assume "n \<noteq> 0"
3.91 +  show "m * n div n = m"
3.92 +    using \<open>n \<noteq> 0\<close> by (auto simp add: divide_nat_def ac_simps intro: Max_eqI)
3.93 +  show "euclidean_size (m mod n) < euclidean_size n"
3.94 +  proof -
3.95 +    have "m < Suc (m div n) * n"
3.96 +    proof (rule ccontr)
3.97 +      assume "\<not> m < Suc (m div n) * n"
3.98 +      then have "Suc (m div n) * n \<le> m"
3.99 +        by (simp add: not_less)
3.100 +      moreover from \<open>n \<noteq> 0\<close> have "Max {k. k * n \<le> m} < Suc (m div n)"
3.101 +        by (simp add: divide_nat_def)
3.102 +      with \<open>n \<noteq> 0\<close> ex fin have "\<And>k. k * n \<le> m \<Longrightarrow> k < Suc (m div n)"
3.103 +        by auto
3.104 +      ultimately have "Suc (m div n) < Suc (m div n)"
3.105 +        by blast
3.106 +      then show False
3.107 +        by simp
3.108 +    qed
3.109 +    with \<open>n \<noteq> 0\<close> show ?thesis
3.110 +      by (simp add: modulo_nat_def)
3.111 +  qed
3.112 +  show "euclidean_size m \<le> euclidean_size (m * n)"
3.113 +    using \<open>n \<noteq> 0\<close> by (cases n) simp_all
3.114 +  fix q r :: nat
3.115 +  show "(q * n + r) div n = q" if "euclidean_size r < euclidean_size n"
3.116 +  proof -
3.117 +    from that have "r < n"
3.118 +      by simp
3.119 +    have "k \<le> q" if "k * n \<le> q * n + r" for k
3.120 +    proof (rule ccontr)
3.121 +      assume "\<not> k \<le> q"
3.122 +      then have "q < k"
3.123 +        by simp
3.124 +      then obtain l where "k = Suc (q + l)"
3.126 +      with \<open>r < n\<close> that show False
3.127 +        by (simp add: algebra_simps)
3.128 +    qed
3.129 +    with \<open>n \<noteq> 0\<close> ex fin show ?thesis
3.130 +      by (auto simp add: divide_nat_def Max_eq_iff)
3.131 +  qed
3.133 +
3.134  end
3.135 +
3.136 +text \<open>Tool support\<close>
3.137 +
3.138 +ML \<open>
3.139 +structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
3.140 +(
3.141 +  val div_name = @{const_name divide};
3.142 +  val mod_name = @{const_name modulo};
3.143 +  val mk_binop = HOLogic.mk_binop;
3.144 +  val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
3.145 +  val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
3.146 +  fun mk_sum [] = HOLogic.zero
3.147 +    | mk_sum [t] = t
3.148 +    | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
3.149 +  fun dest_sum tm =
3.150 +    if HOLogic.is_zero tm then []
3.151 +    else
3.152 +      (case try HOLogic.dest_Suc tm of
3.153 +        SOME t => HOLogic.Suc_zero :: dest_sum t
3.154 +      | NONE =>
3.155 +          (case try dest_plus tm of
3.156 +            SOME (t, u) => dest_sum t @ dest_sum u
3.157 +          | NONE => [tm]));
3.158 +
3.159 +  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
3.160 +
3.161 +  val prove_eq_sums = Arith_Data.prove_conv2 all_tac
3.163 +)
3.164 +\<close>
3.165 +
3.166 +simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
3.167 +  \<open>K Cancel_Div_Mod_Nat.proc\<close>
3.168 +
3.169 +lemma div_nat_eqI:
3.170 +  "m div n = q" if "n * q \<le> m" and "m < n * Suc q" for m n q :: nat
3.171 +  by (rule div_eqI [of _ "m - n * q"]) (use that in \<open>simp_all add: algebra_simps\<close>)
3.172 +
3.173 +lemma mod_nat_eqI:
3.174 +  "m mod n = r" if "r < n" and "r \<le> m" and "n dvd m - r" for m n r :: nat
3.175 +  by (rule mod_eqI [of _ _ "(m - r) div n"]) (use that in \<open>simp_all add: algebra_simps\<close>)
3.176 +
3.177 +lemma div_mult_self_is_m [simp]:
3.178 +  "m * n div n = m" if "n > 0" for m n :: nat
3.179 +  using that by simp
3.180 +
3.181 +lemma div_mult_self1_is_m [simp]:
3.182 +  "n * m div n = m" if "n > 0" for m n :: nat
3.183 +  using that by simp
3.184 +
3.185 +lemma mod_less_divisor [simp]:
3.186 +  "m mod n < n" if "n > 0" for m n :: nat
3.187 +  using mod_size_less [of n m] that by simp
3.188 +
3.189 +lemma mod_le_divisor [simp]:
3.190 +  "m mod n \<le> n" if "n > 0" for m n :: nat
3.191 +  using that by (auto simp add: le_less)
3.192 +
3.193 +lemma div_times_less_eq_dividend [simp]:
3.194 +  "m div n * n \<le> m" for m n :: nat
3.195 +  by (simp add: minus_mod_eq_div_mult [symmetric])
3.196 +
3.197 +lemma times_div_less_eq_dividend [simp]:
3.198 +  "n * (m div n) \<le> m" for m n :: nat
3.199 +  using div_times_less_eq_dividend [of m n]
3.200 +  by (simp add: ac_simps)
3.201 +
3.202 +lemma dividend_less_div_times:
3.203 +  "m < n + (m div n) * n" if "0 < n" for m n :: nat
3.204 +proof -
3.205 +  from that have "m mod n < n"
3.206 +    by simp
3.207 +  then show ?thesis
3.208 +    by (simp add: minus_mod_eq_div_mult [symmetric])
3.209 +qed
3.210 +
3.211 +lemma dividend_less_times_div:
3.212 +  "m < n + n * (m div n)" if "0 < n" for m n :: nat
3.213 +  using dividend_less_div_times [of n m] that
3.214 +  by (simp add: ac_simps)
3.215 +
3.216 +lemma mod_Suc_le_divisor [simp]:
3.217 +  "m mod Suc n \<le> n"
3.218 +  using mod_less_divisor [of "Suc n" m] by arith
3.219 +
3.220 +lemma mod_less_eq_dividend [simp]:
3.221 +  "m mod n \<le> m" for m n :: nat
3.223 +  from div_mult_mod_eq have "m div n * n + m mod n = m" .
3.224 +  then show "m div n * n + m mod n \<le> m" by auto
3.225 +qed
3.226 +
3.227 +lemma
3.228 +  div_less [simp]: "m div n = 0"
3.229 +  and mod_less [simp]: "m mod n = m"
3.230 +  if "m < n" for m n :: nat
3.231 +  using that by (auto intro: div_eqI mod_eqI)
3.232 +
3.233 +lemma le_div_geq:
3.234 +  "m div n = Suc ((m - n) div n)" if "0 < n" and "n \<le> m" for m n :: nat
3.235 +proof -
3.236 +  from \<open>n \<le> m\<close> obtain q where "m = n + q"
3.238 +  with \<open>0 < n\<close> show ?thesis
3.240 +qed
3.241 +
3.242 +lemma le_mod_geq:
3.243 +  "m mod n = (m - n) mod n" if "n \<le> m" for m n :: nat
3.244 +proof -
3.245 +  from \<open>n \<le> m\<close> obtain q where "m = n + q"
3.247 +  then show ?thesis
3.248 +    by simp
3.249 +qed
3.250 +
3.251 +lemma div_if:
3.252 +  "m div n = (if m < n \<or> n = 0 then 0 else Suc ((m - n) div n))"
3.253 +  by (simp add: le_div_geq)
3.254 +
3.255 +lemma mod_if:
3.256 +  "m mod n = (if m < n then m else (m - n) mod n)" for m n :: nat
3.257 +  by (simp add: le_mod_geq)
3.258 +
3.259 +lemma div_eq_0_iff:
3.260 +  "m div n = 0 \<longleftrightarrow> m < n \<or> n = 0" for m n :: nat
3.261 +  by (simp add: div_if)
3.262 +
3.263 +lemma div_greater_zero_iff:
3.264 +  "m div n > 0 \<longleftrightarrow> n \<le> m \<and> n > 0" for m n :: nat
3.265 +  using div_eq_0_iff [of m n] by auto
3.266 +
3.267 +lemma mod_greater_zero_iff_not_dvd:
3.268 +  "m mod n > 0 \<longleftrightarrow> \<not> n dvd m" for m n :: nat
3.269 +  by (simp add: dvd_eq_mod_eq_0)
3.270 +
3.271 +lemma div_by_Suc_0 [simp]:
3.272 +  "m div Suc 0 = m"
3.273 +  using div_by_1 [of m] by simp
3.274 +
3.275 +lemma mod_by_Suc_0 [simp]:
3.276 +  "m mod Suc 0 = 0"
3.277 +  using mod_by_1 [of m] by simp
3.278 +
3.279 +lemma div2_Suc_Suc [simp]:
3.280 +  "Suc (Suc m) div 2 = Suc (m div 2)"
3.281 +  by (simp add: numeral_2_eq_2 le_div_geq)
3.282 +
3.283 +lemma Suc_n_div_2_gt_zero [simp]:
3.284 +  "0 < Suc n div 2" if "n > 0" for n :: nat
3.285 +  using that by (cases n) simp_all
3.286 +
3.287 +lemma div_2_gt_zero [simp]:
3.288 +  "0 < n div 2" if "Suc 0 < n" for n :: nat
3.289 +  using that Suc_n_div_2_gt_zero [of "n - 1"] by simp
3.290 +
3.291 +lemma mod2_Suc_Suc [simp]:
3.292 +  "Suc (Suc m) mod 2 = m mod 2"
3.293 +  by (simp add: numeral_2_eq_2 le_mod_geq)
3.294 +
3.296 +  "(m + m) div 2 = m" for m :: nat
3.297 +  by (simp add: mult_2 [symmetric])
3.298 +
3.300 +  "(m + m) mod 2 = 0" for m :: nat
3.301 +  by (simp add: mult_2 [symmetric])
3.302 +
3.303 +lemma mod2_gr_0 [simp]:
3.304 +  "0 < m mod 2 \<longleftrightarrow> m mod 2 = 1" for m :: nat
3.305 +proof -
3.306 +  have "m mod 2 < 2"
3.307 +    by (rule mod_less_divisor) simp
3.308 +  then have "m mod 2 = 0 \<or> m mod 2 = 1"
3.309 +    by arith
3.310 +  then show ?thesis
3.311 +    by auto
3.312 +qed
3.313 +
3.314 +lemma mod_Suc_eq [mod_simps]:
3.315 +  "Suc (m mod n) mod n = Suc m mod n"
3.316 +proof -
3.317 +  have "(m mod n + 1) mod n = (m + 1) mod n"
3.318 +    by (simp only: mod_simps)
3.319 +  then show ?thesis
3.320 +    by simp
3.321 +qed
3.322 +
3.323 +lemma mod_Suc_Suc_eq [mod_simps]:
3.324 +  "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
3.325 +proof -
3.326 +  have "(m mod n + 2) mod n = (m + 2) mod n"
3.327 +    by (simp only: mod_simps)
3.328 +  then show ?thesis
3.329 +    by simp
3.330 +qed
3.331 +
3.332 +lemma
3.333 +  Suc_mod_mult_self1 [simp]: "Suc (m + k * n) mod n = Suc m mod n"
3.334 +  and Suc_mod_mult_self2 [simp]: "Suc (m + n * k) mod n = Suc m mod n"
3.335 +  and Suc_mod_mult_self3 [simp]: "Suc (k * n + m) mod n = Suc m mod n"
3.336 +  and Suc_mod_mult_self4 [simp]: "Suc (n * k + m) mod n = Suc m mod n"
3.337 +  by (subst mod_Suc_eq [symmetric], simp add: mod_simps)+
3.338 +
3.339 +lemma div_mult1_eq: -- \<open>TODO: Generalization candidate\<close>
3.340 +  "(a * b) div c = a * (b div c) + a * (b mod c) div c" for a b c :: nat
3.341 +  apply (cases "c = 0")
3.342 +   apply simp
3.343 +  apply (rule div_eqI [of _ "(a * (b mod c)) mod c"])
3.344 +     apply (auto simp add: algebra_simps distrib_left [symmetric])
3.345 +  done
3.346 +
3.347 +lemma div_add1_eq: -- \<open>NOT suitable for rewriting: the RHS has an instance of the LHS\<close>
3.348 +   -- \<open>TODO: Generalization candidate\<close>
3.349 +  "(a + b) div c = a div c + b div c + ((a mod c + b mod c) div c)" for a b c :: nat
3.350 +  apply (cases "c = 0")
3.351 +   apply simp
3.352 +  apply (rule div_eqI [of _ "(a mod c + b mod c) mod c"])
3.353 +  apply (auto simp add: algebra_simps)
3.354 +  done
3.355 +
3.356 +context
3.357 +  fixes m n q :: nat
3.358 +begin
3.359 +
3.360 +private lemma eucl_rel_mult2:
3.361 +  "m mod n + n * (m div n mod q) < n * q"
3.362 +  if "n > 0" and "q > 0"
3.363 +proof -
3.364 +  from \<open>n > 0\<close> have "m mod n < n"
3.365 +    by (rule mod_less_divisor)
3.366 +  from \<open>q > 0\<close> have "m div n mod q < q"
3.367 +    by (rule mod_less_divisor)
3.368 +  then obtain s where "q = Suc (m div n mod q + s)"
3.369 +    by (blast dest: less_imp_Suc_add)
3.370 +  moreover have "m mod n + n * (m div n mod q) < n * Suc (m div n mod q + s)"
3.371 +    using \<open>m mod n < n\<close> by (simp add: add_mult_distrib2)
3.372 +  ultimately show ?thesis
3.373 +    by simp
3.374 +qed
3.375 +
3.376 +lemma div_mult2_eq:
3.377 +  "m div (n * q) = (m div n) div q"
3.378 +proof (cases "n = 0 \<or> q = 0")
3.379 +  case True
3.380 +  then show ?thesis
3.381 +    by auto
3.382 +next
3.383 +  case False
3.384 +  with eucl_rel_mult2 show ?thesis
3.385 +    by (auto intro: div_eqI [of _ "n * (m div n mod q) + m mod n"]
3.387 +qed
3.388 +
3.389 +lemma mod_mult2_eq:
3.390 +  "m mod (n * q) = n * (m div n mod q) + m mod n"
3.391 +proof (cases "n = 0 \<or> q = 0")
3.392 +  case True
3.393 +  then show ?thesis
3.394 +    by auto
3.395 +next
3.396 +  case False
3.397 +  with eucl_rel_mult2 show ?thesis
3.398 +    by (auto intro: mod_eqI [of _ _ "(m div n) div q"]
3.400 +qed
3.401 +
3.402 +end
3.403 +
3.404 +lemma div_le_mono:
3.405 +  "m div k \<le> n div k" if "m \<le> n" for m n k :: nat
3.406 +proof -
3.407 +  from that obtain q where "n = m + q"
3.409 +  then show ?thesis
3.411 +qed
3.412 +
3.413 +text \<open>Antimonotonicity of @{const divide} in second argument\<close>
3.414 +
3.415 +lemma div_le_mono2:
3.416 +  "k div n \<le> k div m" if "0 < m" and "m \<le> n" for m n k :: nat
3.417 +using that proof (induct k arbitrary: m rule: less_induct)
3.418 +  case (less k)
3.419 +  show ?case
3.420 +  proof (cases "n \<le> k")
3.421 +    case False
3.422 +    then show ?thesis
3.423 +      by simp
3.424 +  next
3.425 +    case True
3.426 +    have "(k - n) div n \<le> (k - m) div n"
3.427 +      using less.prems
3.428 +      by (blast intro: div_le_mono diff_le_mono2)
3.429 +    also have "\<dots> \<le> (k - m) div m"
3.430 +      using \<open>n \<le> k\<close> less.prems less.hyps [of "k - m" m]
3.431 +      by simp
3.432 +    finally show ?thesis
3.433 +      using \<open>n \<le> k\<close> less.prems
3.434 +      by (simp add: le_div_geq)
3.435 +  qed
3.436 +qed
3.437 +
3.438 +lemma div_le_dividend [simp]:
3.439 +  "m div n \<le> m" for m n :: nat
3.440 +  using div_le_mono2 [of 1 n m] by (cases "n = 0") simp_all
3.441 +
3.442 +lemma div_less_dividend [simp]:
3.443 +  "m div n < m" if "1 < n" and "0 < m" for m n :: nat
3.444 +using that proof (induct m rule: less_induct)
3.445 +  case (less m)
3.446 +  show ?case
3.447 +  proof (cases "n < m")
3.448 +    case False
3.449 +    with less show ?thesis
3.450 +      by (cases "n = m") simp_all
3.451 +  next
3.452 +    case True
3.453 +    then show ?thesis
3.454 +      using less.hyps [of "m - n"] less.prems
3.455 +      by (simp add: le_div_geq)
3.456 +  qed
3.457 +qed
3.458 +
3.459 +lemma div_eq_dividend_iff:
3.460 +  "m div n = m \<longleftrightarrow> n = 1" if "m > 0" for m n :: nat
3.461 +proof
3.462 +  assume "n = 1"
3.463 +  then show "m div n = m"
3.464 +    by simp
3.465 +next
3.466 +  assume P: "m div n = m"
3.467 +  show "n = 1"
3.468 +  proof (rule ccontr)
3.469 +    have "n \<noteq> 0"
3.470 +      by (rule ccontr) (use that P in auto)
3.471 +    moreover assume "n \<noteq> 1"
3.472 +    ultimately have "n > 1"
3.473 +      by simp
3.474 +    with that have "m div n < m"
3.475 +      by simp
3.476 +    with P show False
3.477 +      by simp
3.478 +  qed
3.479 +qed
3.480 +
3.481 +lemma less_mult_imp_div_less:
3.482 +  "m div n < i" if "m < i * n" for m n i :: nat
3.483 +proof -
3.484 +  from that have "i * n > 0"
3.485 +    by (cases "i * n = 0") simp_all
3.486 +  then have "i > 0" and "n > 0"
3.487 +    by simp_all
3.488 +  have "m div n * n \<le> m"
3.489 +    by simp
3.490 +  then have "m div n * n < i * n"
3.491 +    using that by (rule le_less_trans)
3.492 +  with \<open>n > 0\<close> show ?thesis
3.493 +    by simp
3.494 +qed
3.495 +
3.496 +text \<open>A fact for the mutilated chess board\<close>
3.497 +
3.498 +lemma mod_Suc:
3.499 +  "Suc m mod n = (if Suc (m mod n) = n then 0 else Suc (m mod n))" (is "_ = ?rhs")
3.500 +proof (cases "n = 0")
3.501 +  case True
3.502 +  then show ?thesis
3.503 +    by simp
3.504 +next
3.505 +  case False
3.506 +  have "Suc m mod n = Suc (m mod n) mod n"
3.507 +    by (simp add: mod_simps)
3.508 +  also have "\<dots> = ?rhs"
3.509 +    using False by (auto intro!: mod_nat_eqI intro: neq_le_trans simp add: Suc_le_eq)
3.510 +  finally show ?thesis .
3.511 +qed
3.512 +
3.513 +lemma Suc_times_mod_eq:
3.514 +  "Suc (m * n) mod m = 1" if "Suc 0 < m"
3.515 +  using that by (simp add: mod_Suc)
3.516 +
3.517 +lemma Suc_times_numeral_mod_eq [simp]:
3.518 +  "Suc (numeral k * n) mod numeral k = 1" if "numeral k \<noteq> (1::nat)"
3.519 +  by (rule Suc_times_mod_eq) (use that in simp)
3.520 +
3.521 +lemma Suc_div_le_mono [simp]:
3.522 +  "m div n \<le> Suc m div n"
3.523 +  by (simp add: div_le_mono)
3.524 +
3.525 +text \<open>These lemmas collapse some needless occurrences of Suc:
3.526 +  at least three Sucs, since two and fewer are rewritten back to Suc again!
3.527 +  We already have some rules to simplify operands smaller than 3.\<close>
3.528 +
3.530 +  "m div Suc (Suc (Suc n)) = m div (3 + n)"
3.532 +
3.534 +  "m mod Suc (Suc (Suc n)) = m mod (3 + n)"
3.536 +
3.538 +  "Suc (Suc (Suc m)) div n = (3 + m) div n"
3.540 +
3.542 +  "Suc (Suc (Suc m)) mod n = (3 + m) mod n"
3.544 +
3.546 +  Suc_div_eq_add3_div [of _ "numeral v"] for v
3.547 +
3.549 +  Suc_mod_eq_add3_mod [of _ "numeral v"] for v
3.550 +
3.551 +lemma (in field_char_0) of_nat_div:
3.552 +  "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
3.553 +proof -
3.554 +  have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
3.555 +    unfolding of_nat_add by (cases "n = 0") simp_all
3.556 +  then show ?thesis
3.557 +    by simp
3.558 +qed
3.559 +
3.560 +text \<open>An ``induction'' law for modulus arithmetic.\<close>
3.561 +
3.562 +lemma mod_induct [consumes 3, case_names step]:
3.563 +  "P m" if "P n" and "n < p" and "m < p"
3.564 +    and step: "\<And>n. n < p \<Longrightarrow> P n \<Longrightarrow> P (Suc n mod p)"
3.565 +using \<open>m < p\<close> proof (induct m)
3.566 +  case 0
3.567 +  show ?case
3.568 +  proof (rule ccontr)
3.569 +    assume "\<not> P 0"
3.570 +    from \<open>n < p\<close> have "0 < p"
3.571 +      by simp
3.572 +    from \<open>n < p\<close> obtain m where "0 < m" and "p = n + m"
3.573 +      by (blast dest: less_imp_add_positive)
3.574 +    with \<open>P n\<close> have "P (p - m)"
3.575 +      by simp
3.576 +    moreover have "\<not> P (p - m)"
3.577 +    using \<open>0 < m\<close> proof (induct m)
3.578 +      case 0
3.579 +      then show ?case
3.580 +        by simp
3.581 +    next
3.582 +      case (Suc m)
3.583 +      show ?case
3.584 +      proof
3.585 +        assume P: "P (p - Suc m)"
3.586 +        with \<open>\<not> P 0\<close> have "Suc m < p"
3.587 +          by (auto intro: ccontr)
3.588 +        then have "Suc (p - Suc m) = p - m"
3.589 +          by arith
3.590 +        moreover from \<open>0 < p\<close> have "p - Suc m < p"
3.591 +          by arith
3.592 +        with P step have "P ((Suc (p - Suc m)) mod p)"
3.593 +          by blast
3.594 +        ultimately show False
3.595 +          using \<open>\<not> P 0\<close> Suc.hyps by (cases "m = 0") simp_all
3.596 +      qed
3.597 +    qed
3.598 +    ultimately show False
3.599 +      by blast
3.600 +  qed
3.601 +next
3.602 +  case (Suc m)
3.603 +  then have "m < p" and mod: "Suc m mod p = Suc m"
3.604 +    by simp_all
3.605 +  from \<open>m < p\<close> have "P m"
3.606 +    by (rule Suc.hyps)
3.607 +  with \<open>m < p\<close> have "P (Suc m mod p)"
3.608 +    by (rule step)
3.609 +  with mod show ?case
3.610 +    by simp
3.611 +qed
3.612 +
3.613 +lemma split_div:
3.614 +  "P (m div n) \<longleftrightarrow> (n = 0 \<longrightarrow> P 0) \<and> (n \<noteq> 0 \<longrightarrow>
3.615 +     (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P i))"
3.616 +     (is "?P = ?Q") for m n :: nat
3.617 +proof (cases "n = 0")
3.618 +  case True
3.619 +  then show ?thesis
3.620 +    by simp
3.621 +next
3.622 +  case False
3.623 +  show ?thesis
3.624 +  proof
3.625 +    assume ?P
3.626 +    with False show ?Q
3.627 +      by auto
3.628 +  next
3.629 +    assume ?Q
3.630 +    with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P i"
3.631 +      by simp
3.632 +    with False show ?P
3.633 +      by (auto intro: * [of "m mod n"])
3.634 +  qed
3.635 +qed
3.636 +
3.637 +lemma split_div':
3.638 +  "P (m div n) \<longleftrightarrow> n = 0 \<and> P 0 \<or> (\<exists>q. (n * q \<le> m \<and> m < n * Suc q) \<and> P q)"
3.639 +proof (cases "n = 0")
3.640 +  case True
3.641 +  then show ?thesis
3.642 +    by simp
3.643 +next
3.644 +  case False
3.645 +  then have "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> m div n = q" for q
3.646 +    by (auto intro: div_nat_eqI dividend_less_times_div)
3.647 +  then show ?thesis
3.648 +    by auto
3.649 +qed
3.650 +
3.651 +lemma split_mod:
3.652 +  "P (m mod n) \<longleftrightarrow> (n = 0 \<longrightarrow> P m) \<and> (n \<noteq> 0 \<longrightarrow>
3.653 +     (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P j))"
3.654 +     (is "?P \<longleftrightarrow> ?Q") for m n :: nat
3.655 +proof (cases "n = 0")
3.656 +  case True
3.657 +  then show ?thesis
3.658 +    by simp
3.659 +next
3.660 +  case False
3.661 +  show ?thesis
3.662 +  proof
3.663 +    assume ?P
3.664 +    with False show ?Q
3.665 +      by auto
3.666 +  next
3.667 +    assume ?Q
3.668 +    with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P j"
3.669 +      by simp
3.670 +    with False show ?P
3.671 +      by (auto intro: * [of _ "m div n"])
3.672 +  qed
3.673 +qed
3.674 +
3.675 +
3.676 +subsection \<open>Code generation\<close>
3.677 +
3.678 +code_identifier
3.679 +  code_module Euclidean_Division \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
3.680 +
3.681 +end
```
```     4.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Sun Oct 08 22:28:21 2017 +0200
4.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Sun Oct 08 22:28:21 2017 +0200
4.3 @@ -95,7 +95,7 @@
4.4
4.5  lemma [code]:
4.6    "Divides.divmod_nat m n = (m div n, m mod n)"
4.7 -  by (fact divmod_nat_div_mod)
4.8 +  by (fact divmod_nat_def)
4.9
4.10  lemma [code]:
4.11    "divmod m n = map_prod nat_of_integer nat_of_integer (divmod m n)"
4.12 @@ -130,7 +130,7 @@
4.13  proof -
4.14    from div_mult_mod_eq have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
4.15    show ?thesis
4.19  qed
4.20
```
```     5.1 --- a/src/HOL/Library/RBT_Impl.thy	Sun Oct 08 22:28:21 2017 +0200
5.2 +++ b/src/HOL/Library/RBT_Impl.thy	Sun Oct 08 22:28:21 2017 +0200
5.3 @@ -1169,7 +1169,7 @@
5.4            apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
5.5        else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
5.6            apfst (Branch B t1 k v) (rbtreeify_f n' kvs'))"
5.7 -by (subst rbtreeify_f.simps) (simp only: Let_def divmod_nat_div_mod prod.case)
5.8 +by (subst rbtreeify_f.simps) (simp only: Let_def divmod_nat_def prod.case)
5.9
5.10  lemma rbtreeify_g_code [code]:
5.11    "rbtreeify_g n kvs =
5.12 @@ -1180,7 +1180,7 @@
5.13            apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
5.14        else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
5.15            apfst (Branch B t1 k v) (rbtreeify_g n' kvs'))"
5.16 -by(subst rbtreeify_g.simps)(simp only: Let_def divmod_nat_div_mod prod.case)
5.17 +by(subst rbtreeify_g.simps)(simp only: Let_def divmod_nat_def prod.case)
5.18
5.19  lemma Suc_double_half: "Suc (2 * n) div 2 = n"
5.20  by simp
```
```     6.1 --- a/src/HOL/Parity.thy	Sun Oct 08 22:28:21 2017 +0200
6.2 +++ b/src/HOL/Parity.thy	Sun Oct 08 22:28:21 2017 +0200
6.3 @@ -101,6 +101,92 @@
6.4
6.5  end
6.6
6.7 +class unique_euclidean_semiring_parity = unique_euclidean_semiring +
6.8 +  assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
6.9 +  assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
6.10 +  assumes zero_not_eq_two: "0 \<noteq> 2"
6.11 +begin
6.12 +
6.13 +lemma parity_cases [case_names even odd]:
6.14 +  assumes "a mod 2 = 0 \<Longrightarrow> P"
6.15 +  assumes "a mod 2 = 1 \<Longrightarrow> P"
6.16 +  shows P
6.17 +  using assms parity by blast
6.18 +
6.19 +lemma one_div_two_eq_zero [simp]:
6.20 +  "1 div 2 = 0"
6.21 +proof (cases "2 = 0")
6.22 +  case True then show ?thesis by simp
6.23 +next
6.24 +  case False
6.25 +  from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
6.26 +  with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
6.27 +  then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
6.28 +  then have "1 div 2 = 0 \<or> 2 = 0" by simp
6.29 +  with False show ?thesis by auto
6.30 +qed
6.31 +
6.32 +lemma not_mod_2_eq_0_eq_1 [simp]:
6.33 +  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
6.34 +  by (cases a rule: parity_cases) simp_all
6.35 +
6.36 +lemma not_mod_2_eq_1_eq_0 [simp]:
6.37 +  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
6.38 +  by (cases a rule: parity_cases) simp_all
6.39 +
6.40 +subclass semiring_parity
6.41 +proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
6.42 +  show "1 mod 2 = 1"
6.43 +    by (fact one_mod_two_eq_one)
6.44 +next
6.45 +  fix a b
6.46 +  assume "a mod 2 = 1"
6.47 +  moreover assume "b mod 2 = 1"
6.48 +  ultimately show "(a + b) mod 2 = 0"
6.49 +    using mod_add_eq [of a 2 b] by simp
6.50 +next
6.51 +  fix a b
6.52 +  assume "(a * b) mod 2 = 0"
6.53 +  then have "(a mod 2) * (b mod 2) mod 2 = 0"
6.54 +    by (simp add: mod_mult_eq)
6.55 +  then have "(a mod 2) * (b mod 2) = 0"
6.56 +    by (cases "a mod 2 = 0") simp_all
6.57 +  then show "a mod 2 = 0 \<or> b mod 2 = 0"
6.58 +    by (rule divisors_zero)
6.59 +next
6.60 +  fix a
6.61 +  assume "a mod 2 = 1"
6.62 +  then have "a = a div 2 * 2 + 1"
6.63 +    using div_mult_mod_eq [of a 2] by simp
6.64 +  then show "\<exists>b. a = b + 1" ..
6.65 +qed
6.66 +
6.67 +lemma even_iff_mod_2_eq_zero:
6.68 +  "even a \<longleftrightarrow> a mod 2 = 0"
6.69 +  by (fact dvd_eq_mod_eq_0)
6.70 +
6.71 +lemma odd_iff_mod_2_eq_one:
6.72 +  "odd a \<longleftrightarrow> a mod 2 = 1"
6.73 +  by (simp add: even_iff_mod_2_eq_zero)
6.74 +
6.75 +lemma even_succ_div_two [simp]:
6.76 +  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
6.77 +  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
6.78 +
6.79 +lemma odd_succ_div_two [simp]:
6.80 +  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
6.82 +
6.83 +lemma even_two_times_div_two:
6.84 +  "even a \<Longrightarrow> 2 * (a div 2) = a"
6.85 +  by (fact dvd_mult_div_cancel)
6.86 +
6.87 +lemma odd_two_times_div_two_succ [simp]:
6.88 +  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
6.89 +  using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
6.90 +
6.91 +end
6.92 +
6.93
6.94  subsection \<open>Instances for @{typ nat} and @{typ int}\<close>
6.95
6.96 @@ -190,9 +276,6 @@
6.97    for k l :: int
6.99
6.100 -lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
6.101 -  by (auto elim: oddE)
6.102 -
6.103  instance int :: ring_parity
6.104  proof
6.105    show "\<not> 2 dvd (1 :: int)"
```
```     7.1 --- a/src/HOL/Rings.thy	Sun Oct 08 22:28:21 2017 +0200
7.2 +++ b/src/HOL/Rings.thy	Sun Oct 08 22:28:21 2017 +0200
7.3 @@ -1620,6 +1620,10 @@
7.4    shows "c dvd a"
7.5    using assms dvd_mod_iff [of c b a] by simp
7.6
7.7 +lemma dvd_minus_mod [simp]:
7.8 +  "b dvd a - a mod b"
7.9 +  by (simp add: minus_mod_eq_div_mult)
7.10 +
7.11  end
7.12
7.13  class idom_modulo = idom + semidom_modulo
```
```     8.1 --- a/src/HOL/Word/Word.thy	Sun Oct 08 22:28:21 2017 +0200
8.2 +++ b/src/HOL/Word/Word.thy	Sun Oct 08 22:28:21 2017 +0200
8.3 @@ -2024,7 +2024,7 @@
8.4
8.5  lemmas le_unat_uoi = unat_le [THEN word_unat.Abs_inverse]
8.6
8.7 -lemmas thd = refl [THEN [2] split_div_lemma [THEN iffD2], THEN conjunct1]
8.8 +lemmas thd = times_div_less_eq_dividend
8.9
8.10  lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend dtle
8.11
8.12 @@ -3724,7 +3724,7 @@
8.13  lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
8.14
8.15  (* alternative proof of word_rcat_rsplit *)
8.16 -lemmas tdle = iffD2 [OF split_div_lemma refl, THEN conjunct1]
8.17 +lemmas tdle = times_div_less_eq_dividend
8.18  lemmas dtle = xtr4 [OF tdle mult.commute]
8.19
8.20  lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
8.21 @@ -3734,7 +3734,7 @@
8.23        refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
8.24     apply safe
8.25 -   apply (erule xtr7, rule len_gt_0 [THEN dtle])+
8.26 +   apply (erule xtr7, rule dtle)+
8.27    done
8.28
8.29  lemma size_word_rsplit_rcat_size:
```
```     9.1 --- a/src/HOL/Word/Word_Miscellaneous.thy	Sun Oct 08 22:28:21 2017 +0200
9.2 +++ b/src/HOL/Word/Word_Miscellaneous.thy	Sun Oct 08 22:28:21 2017 +0200
9.3 @@ -304,8 +304,8 @@
9.4  lemmas pl_pl_mm' = add.commute [THEN [2] trans, THEN pl_pl_mm]
9.5
9.6  lemmas dme = div_mult_mod_eq
9.7 -lemmas dtle = xtr3 [OF dme [symmetric] le_add1]
9.8 -lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] dtle]
9.9 +lemmas dtle = div_times_less_eq_dividend
9.10 +lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] div_times_less_eq_dividend]
9.11
9.12  lemma td_gal: "0 < c \<Longrightarrow> a \<ge> b * c \<longleftrightarrow> a div c \<ge> b"
9.13    for a b c :: nat
9.14 @@ -316,15 +316,13 @@
9.15
9.16  lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified]
9.17
9.18 -lemma div_mult_le: "a div b * b \<le> a"
9.19 -  for a b :: nat
9.20 -  by (fact dtle)
9.21 +lemmas div_mult_le = div_times_less_eq_dividend
9.22
9.23 -lemmas sdl = split_div_lemma [THEN iffD1, symmetric]
9.24 +lemmas sdl = div_nat_eqI
9.25
9.26  lemma given_quot: "f > 0 \<Longrightarrow> (f * l + (f - 1)) div f = l"
9.27    for f l :: nat
9.28 -  by (rule sdl, assumption) (simp (no_asm))
9.29 +  by (rule div_nat_eqI) (simp_all)
9.30
9.31  lemma given_quot_alt: "f > 0 \<Longrightarrow> (l * f + f - Suc 0) div f = l"
9.32    for f l :: nat
```