src/HOL/Divides.thy
changeset 66808 1907167b6038
parent 66806 a4e82b58d833
child 66810 cc2b490f9dc4
     1.1 --- a/src/HOL/Divides.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -9,95 +9,6 @@
     1.4  imports Parity
     1.5  begin
     1.6  
     1.7 -subsection \<open>Parity\<close>
     1.8 -
     1.9 -class unique_euclidean_semiring_parity = unique_euclidean_semiring +
    1.10 -  assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
    1.11 -  assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
    1.12 -  assumes zero_not_eq_two: "0 \<noteq> 2"
    1.13 -begin
    1.14 -
    1.15 -lemma parity_cases [case_names even odd]:
    1.16 -  assumes "a mod 2 = 0 \<Longrightarrow> P"
    1.17 -  assumes "a mod 2 = 1 \<Longrightarrow> P"
    1.18 -  shows P
    1.19 -  using assms parity by blast
    1.20 -
    1.21 -lemma one_div_two_eq_zero [simp]:
    1.22 -  "1 div 2 = 0"
    1.23 -proof (cases "2 = 0")
    1.24 -  case True then show ?thesis by simp
    1.25 -next
    1.26 -  case False
    1.27 -  from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
    1.28 -  with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
    1.29 -  then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
    1.30 -  then have "1 div 2 = 0 \<or> 2 = 0" by simp
    1.31 -  with False show ?thesis by auto
    1.32 -qed
    1.33 -
    1.34 -lemma not_mod_2_eq_0_eq_1 [simp]:
    1.35 -  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
    1.36 -  by (cases a rule: parity_cases) simp_all
    1.37 -
    1.38 -lemma not_mod_2_eq_1_eq_0 [simp]:
    1.39 -  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
    1.40 -  by (cases a rule: parity_cases) simp_all
    1.41 -
    1.42 -subclass semiring_parity
    1.43 -proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
    1.44 -  show "1 mod 2 = 1"
    1.45 -    by (fact one_mod_two_eq_one)
    1.46 -next
    1.47 -  fix a b
    1.48 -  assume "a mod 2 = 1"
    1.49 -  moreover assume "b mod 2 = 1"
    1.50 -  ultimately show "(a + b) mod 2 = 0"
    1.51 -    using mod_add_eq [of a 2 b] by simp
    1.52 -next
    1.53 -  fix a b
    1.54 -  assume "(a * b) mod 2 = 0"
    1.55 -  then have "(a mod 2) * (b mod 2) mod 2 = 0"
    1.56 -    by (simp add: mod_mult_eq)
    1.57 -  then have "(a mod 2) * (b mod 2) = 0"
    1.58 -    by (cases "a mod 2 = 0") simp_all
    1.59 -  then show "a mod 2 = 0 \<or> b mod 2 = 0"
    1.60 -    by (rule divisors_zero)
    1.61 -next
    1.62 -  fix a
    1.63 -  assume "a mod 2 = 1"
    1.64 -  then have "a = a div 2 * 2 + 1"
    1.65 -    using div_mult_mod_eq [of a 2] by simp
    1.66 -  then show "\<exists>b. a = b + 1" ..
    1.67 -qed
    1.68 -
    1.69 -lemma even_iff_mod_2_eq_zero:
    1.70 -  "even a \<longleftrightarrow> a mod 2 = 0"
    1.71 -  by (fact dvd_eq_mod_eq_0)
    1.72 -
    1.73 -lemma odd_iff_mod_2_eq_one:
    1.74 -  "odd a \<longleftrightarrow> a mod 2 = 1"
    1.75 -  by (simp add: even_iff_mod_2_eq_zero)
    1.76 -
    1.77 -lemma even_succ_div_two [simp]:
    1.78 -  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
    1.79 -  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
    1.80 -
    1.81 -lemma odd_succ_div_two [simp]:
    1.82 -  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
    1.83 -  by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
    1.84 -
    1.85 -lemma even_two_times_div_two:
    1.86 -  "even a \<Longrightarrow> 2 * (a div 2) = a"
    1.87 -  by (fact dvd_mult_div_cancel)
    1.88 -
    1.89 -lemma odd_two_times_div_two_succ [simp]:
    1.90 -  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
    1.91 -  using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
    1.92 - 
    1.93 -end
    1.94 -
    1.95 -
    1.96  subsection \<open>Numeral division with a pragmatic type class\<close>
    1.97  
    1.98  text \<open>
    1.99 @@ -382,445 +293,11 @@
   1.100  
   1.101  end
   1.102  
   1.103 +hide_fact (open) div_less mod_less mod_less_eq_dividend mod_mult2_eq div_mult2_eq
   1.104 +
   1.105  
   1.106  subsection \<open>Division on @{typ nat}\<close>
   1.107  
   1.108 -context
   1.109 -begin
   1.110 -
   1.111 -text \<open>
   1.112 -  We define @{const divide} and @{const modulo} on @{typ nat} by means
   1.113 -  of a characteristic relation with two input arguments
   1.114 -  @{term "m::nat"}, @{term "n::nat"} and two output arguments
   1.115 -  @{term "q::nat"}(uotient) and @{term "r::nat"}(emainder).
   1.116 -\<close>
   1.117 -
   1.118 -inductive eucl_rel_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool"
   1.119 -  where eucl_rel_nat_by0: "eucl_rel_nat m 0 (0, m)"
   1.120 -  | eucl_rel_natI: "r < n \<Longrightarrow> m = q * n + r \<Longrightarrow> eucl_rel_nat m n (q, r)"
   1.121 -
   1.122 -text \<open>@{const eucl_rel_nat} is total:\<close>
   1.123 -
   1.124 -qualified lemma eucl_rel_nat_ex:
   1.125 -  obtains q r where "eucl_rel_nat m n (q, r)"
   1.126 -proof (cases "n = 0")
   1.127 -  case True
   1.128 -  with that eucl_rel_nat_by0 show thesis
   1.129 -    by blast
   1.130 -next
   1.131 -  case False
   1.132 -  have "\<exists>q r. m = q * n + r \<and> r < n"
   1.133 -  proof (induct m)
   1.134 -    case 0 with \<open>n \<noteq> 0\<close>
   1.135 -    have "(0::nat) = 0 * n + 0 \<and> 0 < n" by simp
   1.136 -    then show ?case by blast
   1.137 -  next
   1.138 -    case (Suc m) then obtain q' r'
   1.139 -      where m: "m = q' * n + r'" and n: "r' < n" by auto
   1.140 -    then show ?case proof (cases "Suc r' < n")
   1.141 -      case True
   1.142 -      from m n have "Suc m = q' * n + Suc r'" by simp
   1.143 -      with True show ?thesis by blast
   1.144 -    next
   1.145 -      case False then have "n \<le> Suc r'"
   1.146 -        by (simp add: not_less)
   1.147 -      moreover from n have "Suc r' \<le> n"
   1.148 -        by (simp add: Suc_le_eq)
   1.149 -      ultimately have "n = Suc r'" by auto
   1.150 -      with m have "Suc m = Suc q' * n + 0" by simp
   1.151 -      with \<open>n \<noteq> 0\<close> show ?thesis by blast
   1.152 -    qed
   1.153 -  qed
   1.154 -  with that \<open>n \<noteq> 0\<close> eucl_rel_natI show thesis
   1.155 -    by blast
   1.156 -qed
   1.157 -
   1.158 -text \<open>@{const eucl_rel_nat} is injective:\<close>
   1.159 -
   1.160 -qualified lemma eucl_rel_nat_unique_div:
   1.161 -  assumes "eucl_rel_nat m n (q, r)"
   1.162 -    and "eucl_rel_nat m n (q', r')"
   1.163 -  shows "q = q'"
   1.164 -proof (cases "n = 0")
   1.165 -  case True with assms show ?thesis
   1.166 -    by (auto elim: eucl_rel_nat.cases)
   1.167 -next
   1.168 -  case False
   1.169 -  have *: "q' \<le> q" if "q' * n + r' = q * n + r" "r < n" for q r q' r' :: nat
   1.170 -  proof (rule ccontr)
   1.171 -    assume "\<not> q' \<le> q"
   1.172 -    then have "q < q'"
   1.173 -      by (simp add: not_le)
   1.174 -    with that show False
   1.175 -      by (auto simp add: less_iff_Suc_add algebra_simps)
   1.176 -  qed
   1.177 -  from \<open>n \<noteq> 0\<close> assms show ?thesis
   1.178 -    by (auto intro: order_antisym elim: eucl_rel_nat.cases dest: * sym split: if_splits)
   1.179 -qed
   1.180 -
   1.181 -qualified lemma eucl_rel_nat_unique_mod:
   1.182 -  assumes "eucl_rel_nat m n (q, r)"
   1.183 -    and "eucl_rel_nat m n (q', r')"
   1.184 -  shows "r = r'"
   1.185 -proof -
   1.186 -  from assms have "q' = q"
   1.187 -    by (auto intro: eucl_rel_nat_unique_div)
   1.188 -  with assms show ?thesis
   1.189 -    by (auto elim!: eucl_rel_nat.cases)
   1.190 -qed
   1.191 -
   1.192 -text \<open>
   1.193 -  We instantiate divisibility on the natural numbers by
   1.194 -  means of @{const eucl_rel_nat}:
   1.195 -\<close>
   1.196 -
   1.197 -qualified definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
   1.198 -  "divmod_nat m n = (THE qr. eucl_rel_nat m n qr)"
   1.199 -
   1.200 -qualified lemma eucl_rel_nat_divmod_nat:
   1.201 -  "eucl_rel_nat m n (divmod_nat m n)"
   1.202 -proof -
   1.203 -  from eucl_rel_nat_ex
   1.204 -    obtain q r where rel: "eucl_rel_nat m n (q, r)" .
   1.205 -  then show ?thesis
   1.206 -    by (auto simp add: divmod_nat_def intro: theI
   1.207 -      elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
   1.208 -qed
   1.209 -
   1.210 -qualified lemma divmod_nat_unique:
   1.211 -  "divmod_nat m n = (q, r)" if "eucl_rel_nat m n (q, r)"
   1.212 -  using that
   1.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)
   1.214 -
   1.215 -qualified lemma divmod_nat_zero:
   1.216 -  "divmod_nat m 0 = (0, m)"
   1.217 -  by (rule divmod_nat_unique) (fact eucl_rel_nat_by0)
   1.218 -
   1.219 -qualified lemma divmod_nat_zero_left:
   1.220 -  "divmod_nat 0 n = (0, 0)"
   1.221 -  by (rule divmod_nat_unique) 
   1.222 -    (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
   1.223 -
   1.224 -qualified lemma divmod_nat_base:
   1.225 -  "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
   1.226 -  by (rule divmod_nat_unique) 
   1.227 -    (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
   1.228 -
   1.229 -qualified lemma divmod_nat_step:
   1.230 -  assumes "0 < n" and "n \<le> m"
   1.231 -  shows "divmod_nat m n =
   1.232 -    (Suc (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
   1.233 -proof (rule divmod_nat_unique)
   1.234 -  have "eucl_rel_nat (m - n) n (divmod_nat (m - n) n)"
   1.235 -    by (fact eucl_rel_nat_divmod_nat)
   1.236 -  then show "eucl_rel_nat m n (Suc
   1.237 -    (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
   1.238 -    using assms
   1.239 -      by (auto split: if_splits intro: eucl_rel_natI elim!: eucl_rel_nat.cases simp add: algebra_simps)
   1.240 -qed
   1.241 -
   1.242 -end
   1.243 -
   1.244 -instantiation nat :: "{semidom_modulo, normalization_semidom}"
   1.245 -begin
   1.246 -
   1.247 -definition normalize_nat :: "nat \<Rightarrow> nat"
   1.248 -  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
   1.249 -
   1.250 -definition unit_factor_nat :: "nat \<Rightarrow> nat"
   1.251 -  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
   1.252 -
   1.253 -lemma unit_factor_simps [simp]:
   1.254 -  "unit_factor 0 = (0::nat)"
   1.255 -  "unit_factor (Suc n) = 1"
   1.256 -  by (simp_all add: unit_factor_nat_def)
   1.257 -
   1.258 -definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   1.259 -  where div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
   1.260 -
   1.261 -definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   1.262 -  where mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)"
   1.263 -
   1.264 -lemma fst_divmod_nat [simp]:
   1.265 -  "fst (Divides.divmod_nat m n) = m div n"
   1.266 -  by (simp add: div_nat_def)
   1.267 -
   1.268 -lemma snd_divmod_nat [simp]:
   1.269 -  "snd (Divides.divmod_nat m n) = m mod n"
   1.270 -  by (simp add: mod_nat_def)
   1.271 -
   1.272 -lemma divmod_nat_div_mod:
   1.273 -  "Divides.divmod_nat m n = (m div n, m mod n)"
   1.274 -  by (simp add: prod_eq_iff)
   1.275 -
   1.276 -lemma div_nat_unique:
   1.277 -  assumes "eucl_rel_nat m n (q, r)"
   1.278 -  shows "m div n = q"
   1.279 -  using assms
   1.280 -  by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
   1.281 -
   1.282 -lemma mod_nat_unique:
   1.283 -  assumes "eucl_rel_nat m n (q, r)"
   1.284 -  shows "m mod n = r"
   1.285 -  using assms
   1.286 -  by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
   1.287 -
   1.288 -lemma eucl_rel_nat: "eucl_rel_nat m n (m div n, m mod n)"
   1.289 -  using Divides.eucl_rel_nat_divmod_nat
   1.290 -  by (simp add: divmod_nat_div_mod)
   1.291 -
   1.292 -text \<open>The ''recursion'' equations for @{const divide} and @{const modulo}\<close>
   1.293 -
   1.294 -lemma div_less [simp]:
   1.295 -  fixes m n :: nat
   1.296 -  assumes "m < n"
   1.297 -  shows "m div n = 0"
   1.298 -  using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
   1.299 -
   1.300 -lemma le_div_geq:
   1.301 -  fixes m n :: nat
   1.302 -  assumes "0 < n" and "n \<le> m"
   1.303 -  shows "m div n = Suc ((m - n) div n)"
   1.304 -  using assms Divides.divmod_nat_step by (simp add: prod_eq_iff)
   1.305 -
   1.306 -lemma mod_less [simp]:
   1.307 -  fixes m n :: nat
   1.308 -  assumes "m < n"
   1.309 -  shows "m mod n = m"
   1.310 -  using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
   1.311 -
   1.312 -lemma le_mod_geq:
   1.313 -  fixes m n :: nat
   1.314 -  assumes "n \<le> m"
   1.315 -  shows "m mod n = (m - n) mod n"
   1.316 -  using assms Divides.divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
   1.317 -
   1.318 -lemma mod_less_divisor [simp]:
   1.319 -  fixes m n :: nat
   1.320 -  assumes "n > 0"
   1.321 -  shows "m mod n < n"
   1.322 -  using assms eucl_rel_nat [of m n]
   1.323 -    by (auto elim: eucl_rel_nat.cases)
   1.324 -
   1.325 -lemma mod_le_divisor [simp]:
   1.326 -  fixes m n :: nat
   1.327 -  assumes "n > 0"
   1.328 -  shows "m mod n \<le> n"
   1.329 -  using assms eucl_rel_nat [of m n]
   1.330 -    by (auto elim: eucl_rel_nat.cases)
   1.331 -
   1.332 -instance proof
   1.333 -  fix m n :: nat
   1.334 -  show "m div n * n + m mod n = m"
   1.335 -    using eucl_rel_nat [of m n]
   1.336 -    by (auto elim: eucl_rel_nat.cases)
   1.337 -next
   1.338 -  fix n :: nat show "n div 0 = 0"
   1.339 -    by (simp add: div_nat_def Divides.divmod_nat_zero)
   1.340 -next
   1.341 -  fix m n :: nat
   1.342 -  assume "n \<noteq> 0"
   1.343 -  then show "m * n div n = m"
   1.344 -    by (auto intro!: eucl_rel_natI div_nat_unique [of _ _ _ 0])
   1.345 -qed (simp_all add: unit_factor_nat_def)
   1.346 -
   1.347 -end
   1.348 -
   1.349 -text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close>
   1.350 -
   1.351 -lemma (in semiring_modulo) cancel_div_mod_rules:
   1.352 -  "((a div b) * b + a mod b) + c = a + c"
   1.353 -  "(b * (a div b) + a mod b) + c = a + c"
   1.354 -  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
   1.355 -
   1.356 -ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
   1.357 -
   1.358 -ML \<open>
   1.359 -structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
   1.360 -(
   1.361 -  val div_name = @{const_name divide};
   1.362 -  val mod_name = @{const_name modulo};
   1.363 -  val mk_binop = HOLogic.mk_binop;
   1.364 -  val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
   1.365 -  val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
   1.366 -  fun mk_sum [] = HOLogic.zero
   1.367 -    | mk_sum [t] = t
   1.368 -    | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   1.369 -  fun dest_sum tm =
   1.370 -    if HOLogic.is_zero tm then []
   1.371 -    else
   1.372 -      (case try HOLogic.dest_Suc tm of
   1.373 -        SOME t => HOLogic.Suc_zero :: dest_sum t
   1.374 -      | NONE =>
   1.375 -          (case try dest_plus tm of
   1.376 -            SOME (t, u) => dest_sum t @ dest_sum u
   1.377 -          | NONE => [tm]));
   1.378 -
   1.379 -  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
   1.380 -
   1.381 -  val prove_eq_sums = Arith_Data.prove_conv2 all_tac
   1.382 -    (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps})
   1.383 -)
   1.384 -\<close>
   1.385 -
   1.386 -simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
   1.387 -  \<open>K Cancel_Div_Mod_Nat.proc\<close>
   1.388 -
   1.389 -lemma div_by_Suc_0 [simp]:
   1.390 -  "m div Suc 0 = m"
   1.391 -  using div_by_1 [of m] by simp
   1.392 -
   1.393 -lemma mod_by_Suc_0 [simp]:
   1.394 -  "m mod Suc 0 = 0"
   1.395 -  using mod_by_1 [of m] by simp
   1.396 -
   1.397 -lemma mod_greater_zero_iff_not_dvd:
   1.398 -  fixes m n :: nat
   1.399 -  shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
   1.400 -  by (simp add: dvd_eq_mod_eq_0)
   1.401 -
   1.402 -instantiation nat :: unique_euclidean_semiring
   1.403 -begin
   1.404 -
   1.405 -definition [simp]:
   1.406 -  "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
   1.407 -
   1.408 -definition [simp]:
   1.409 -  "uniqueness_constraint_nat = (top :: nat \<Rightarrow> nat \<Rightarrow> bool)"
   1.410 -
   1.411 -instance proof
   1.412 -  fix n q r :: nat
   1.413 -  assume "euclidean_size r < euclidean_size n"
   1.414 -  then have "n > r"
   1.415 -    by simp_all
   1.416 -  then have "eucl_rel_nat (q * n + r) n (q, r)"
   1.417 -    by (rule eucl_rel_natI) rule
   1.418 -  then show "(q * n + r) div n = q"
   1.419 -    by (rule div_nat_unique)
   1.420 -qed (use mult_le_mono2 [of 1] in \<open>simp_all\<close>)
   1.421 -
   1.422 -end
   1.423 -  
   1.424 -lemma divmod_nat_if [code]:
   1.425 -  "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
   1.426 -    let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
   1.427 -  by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
   1.428 -
   1.429 -lemma mod_Suc_eq [mod_simps]:
   1.430 -  "Suc (m mod n) mod n = Suc m mod n"
   1.431 -proof -
   1.432 -  have "(m mod n + 1) mod n = (m + 1) mod n"
   1.433 -    by (simp only: mod_simps)
   1.434 -  then show ?thesis
   1.435 -    by simp
   1.436 -qed
   1.437 -
   1.438 -lemma mod_Suc_Suc_eq [mod_simps]:
   1.439 -  "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
   1.440 -proof -
   1.441 -  have "(m mod n + 2) mod n = (m + 2) mod n"
   1.442 -    by (simp only: mod_simps)
   1.443 -  then show ?thesis
   1.444 -    by simp
   1.445 -qed
   1.446 -
   1.447 -
   1.448 -subsubsection \<open>Quotient\<close>
   1.449 -
   1.450 -lemma div_geq: "0 < n \<Longrightarrow>  \<not> m < n \<Longrightarrow> m div n = Suc ((m - n) div n)"
   1.451 -by (simp add: le_div_geq linorder_not_less)
   1.452 -
   1.453 -lemma div_if: "0 < n \<Longrightarrow> m div n = (if m < n then 0 else Suc ((m - n) div n))"
   1.454 -by (simp add: div_geq)
   1.455 -
   1.456 -lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
   1.457 -by simp
   1.458 -
   1.459 -lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
   1.460 -by simp
   1.461 -
   1.462 -lemma div_positive:
   1.463 -  fixes m n :: nat
   1.464 -  assumes "n > 0"
   1.465 -  assumes "m \<ge> n"
   1.466 -  shows "m div n > 0"
   1.467 -proof -
   1.468 -  from \<open>m \<ge> n\<close> obtain q where "m = n + q"
   1.469 -    by (auto simp add: le_iff_add)
   1.470 -  with \<open>n > 0\<close> show ?thesis by (simp add: div_add_self1)
   1.471 -qed
   1.472 -
   1.473 -lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"
   1.474 -  by auto (metis div_positive less_numeral_extra(3) not_less)
   1.475 -
   1.476 -
   1.477 -subsubsection \<open>Remainder\<close>
   1.478 -
   1.479 -lemma mod_Suc_le_divisor [simp]:
   1.480 -  "m mod Suc n \<le> n"
   1.481 -  using mod_less_divisor [of "Suc n" m] by arith
   1.482 -
   1.483 -lemma mod_less_eq_dividend [simp]:
   1.484 -  fixes m n :: nat
   1.485 -  shows "m mod n \<le> m"
   1.486 -proof (rule add_leD2)
   1.487 -  from div_mult_mod_eq have "m div n * n + m mod n = m" .
   1.488 -  then show "m div n * n + m mod n \<le> m" by auto
   1.489 -qed
   1.490 -
   1.491 -lemma mod_geq: "\<not> m < (n::nat) \<Longrightarrow> m mod n = (m - n) mod n"
   1.492 -by (simp add: le_mod_geq linorder_not_less)
   1.493 -
   1.494 -lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)"
   1.495 -by (simp add: le_mod_geq)
   1.496 -
   1.497 -
   1.498 -subsubsection \<open>Quotient and Remainder\<close>
   1.499 -
   1.500 -lemma div_mult1_eq:
   1.501 -  "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
   1.502 -  by (cases "c = 0")
   1.503 -     (auto simp add: algebra_simps distrib_left [symmetric]
   1.504 -     intro!: div_nat_unique [of _ _ _ "(a * (b mod c)) mod c"] eucl_rel_natI)
   1.505 -
   1.506 -lemma eucl_rel_nat_add1_eq:
   1.507 -  "eucl_rel_nat a c (aq, ar) \<Longrightarrow> eucl_rel_nat b c (bq, br)
   1.508 -   \<Longrightarrow> eucl_rel_nat (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
   1.509 -  by (auto simp add: split_ifs algebra_simps elim!: eucl_rel_nat.cases intro: eucl_rel_nat_by0 eucl_rel_natI)
   1.510 -
   1.511 -(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   1.512 -lemma div_add1_eq:
   1.513 -  "(a + b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
   1.514 -by (blast intro: eucl_rel_nat_add1_eq [THEN div_nat_unique] eucl_rel_nat)
   1.515 -
   1.516 -lemma eucl_rel_nat_mult2_eq:
   1.517 -  assumes "eucl_rel_nat a b (q, r)"
   1.518 -  shows "eucl_rel_nat a (b * c) (q div c, b *(q mod c) + r)"
   1.519 -proof (cases "c = 0")
   1.520 -  case True
   1.521 -  with assms show ?thesis
   1.522 -    by (auto intro: eucl_rel_nat_by0 elim!: eucl_rel_nat.cases simp add: ac_simps)
   1.523 -next
   1.524 -  case False
   1.525 -  { assume "r < b"
   1.526 -    with False have "b * (q mod c) + r < b * c"
   1.527 -      apply (cut_tac m = q and n = c in mod_less_divisor)
   1.528 -      apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
   1.529 -      apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
   1.530 -      apply (simp add: add_mult_distrib2)
   1.531 -      done
   1.532 -    then have "r + b * (q mod c) < b * c"
   1.533 -      by (simp add: ac_simps)
   1.534 -  } with assms False show ?thesis
   1.535 -    by (auto simp add: algebra_simps add_mult_distrib2 [symmetric] elim!: eucl_rel_nat.cases intro: eucl_rel_nat.intros)
   1.536 -qed
   1.537 -
   1.538 -lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
   1.539 -by (force simp add: eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN div_nat_unique])
   1.540 -
   1.541 -lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
   1.542 -by (auto simp add: mult.commute eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN mod_nat_unique])
   1.543 -
   1.544  instantiation nat :: unique_euclidean_semiring_numeral
   1.545  begin
   1.546  
   1.547 @@ -834,370 +311,15 @@
   1.548      in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
   1.549      else (2 * q, r))"
   1.550  
   1.551 -instance
   1.552 -  by standard (auto intro: div_positive simp add: divmod'_nat_def divmod_step_nat_def mod_mult2_eq div_mult2_eq)
   1.553 +instance by standard
   1.554 +  (auto simp add: divmod'_nat_def divmod_step_nat_def div_greater_zero_iff div_mult2_eq mod_mult2_eq)
   1.555  
   1.556  end
   1.557  
   1.558  declare divmod_algorithm_code [where ?'a = nat, code]
   1.559 -  
   1.560  
   1.561 -subsubsection \<open>Further Facts about Quotient and Remainder\<close>
   1.562 -
   1.563 -lemma div_le_mono:
   1.564 -  fixes m n k :: nat
   1.565 -  assumes "m \<le> n"
   1.566 -  shows "m div k \<le> n div k"
   1.567 -proof -
   1.568 -  from assms obtain q where "n = m + q"
   1.569 -    by (auto simp add: le_iff_add)
   1.570 -  then show ?thesis
   1.571 -    by (simp add: div_add1_eq [of m q k])
   1.572 -qed
   1.573 -
   1.574 -(* Antimonotonicity of div in second argument *)
   1.575 -lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
   1.576 -apply (subgoal_tac "0<n")
   1.577 - prefer 2 apply simp
   1.578 -apply (induct_tac k rule: nat_less_induct)
   1.579 -apply (rename_tac "k")
   1.580 -apply (case_tac "k<n", simp)
   1.581 -apply (subgoal_tac "~ (k<m) ")
   1.582 - prefer 2 apply simp
   1.583 -apply (simp add: div_geq)
   1.584 -apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")
   1.585 - prefer 2
   1.586 - apply (blast intro: div_le_mono diff_le_mono2)
   1.587 -apply (rule le_trans, simp)
   1.588 -apply (simp)
   1.589 -done
   1.590 -
   1.591 -lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
   1.592 -apply (case_tac "n=0", simp)
   1.593 -apply (subgoal_tac "m div n \<le> m div 1", simp)
   1.594 -apply (rule div_le_mono2)
   1.595 -apply (simp_all (no_asm_simp))
   1.596 -done
   1.597 -
   1.598 -(* Similar for "less than" *)
   1.599 -lemma div_less_dividend [simp]:
   1.600 -  "\<lbrakk>(1::nat) < n; 0 < m\<rbrakk> \<Longrightarrow> m div n < m"
   1.601 -apply (induct m rule: nat_less_induct)
   1.602 -apply (rename_tac "m")
   1.603 -apply (case_tac "m<n", simp)
   1.604 -apply (subgoal_tac "0<n")
   1.605 - prefer 2 apply simp
   1.606 -apply (simp add: div_geq)
   1.607 -apply (case_tac "n<m")
   1.608 - apply (subgoal_tac "(m-n) div n < (m-n) ")
   1.609 -  apply (rule impI less_trans_Suc)+
   1.610 -apply assumption
   1.611 -  apply (simp_all)
   1.612 -done
   1.613 -
   1.614 -text\<open>A fact for the mutilated chess board\<close>
   1.615 -lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
   1.616 -apply (case_tac "n=0", simp)
   1.617 -apply (induct "m" rule: nat_less_induct)
   1.618 -apply (case_tac "Suc (na) <n")
   1.619 -(* case Suc(na) < n *)
   1.620 -apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
   1.621 -(* case n \<le> Suc(na) *)
   1.622 -apply (simp add: linorder_not_less le_Suc_eq mod_geq)
   1.623 -apply (auto simp add: Suc_diff_le le_mod_geq)
   1.624 -done
   1.625 -
   1.626 -lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
   1.627 -by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
   1.628 -
   1.629 -lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
   1.630 -
   1.631 -(*Loses information, namely we also have r<d provided d is nonzero*)
   1.632 -lemma mod_eqD:
   1.633 -  fixes m d r q :: nat
   1.634 -  assumes "m mod d = r"
   1.635 -  shows "\<exists>q. m = r + q * d"
   1.636 -proof -
   1.637 -  from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
   1.638 -  with assms have "m = r + q * d" by simp
   1.639 -  then show ?thesis ..
   1.640 -qed
   1.641 -
   1.642 -lemma split_div:
   1.643 - "P(n div k :: nat) =
   1.644 - ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
   1.645 - (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
   1.646 -proof
   1.647 -  assume P: ?P
   1.648 -  show ?Q
   1.649 -  proof (cases)
   1.650 -    assume "k = 0"
   1.651 -    with P show ?Q by simp
   1.652 -  next
   1.653 -    assume not0: "k \<noteq> 0"
   1.654 -    thus ?Q
   1.655 -    proof (simp, intro allI impI)
   1.656 -      fix i j
   1.657 -      assume n: "n = k*i + j" and j: "j < k"
   1.658 -      show "P i"
   1.659 -      proof (cases)
   1.660 -        assume "i = 0"
   1.661 -        with n j P show "P i" by simp
   1.662 -      next
   1.663 -        assume "i \<noteq> 0"
   1.664 -        with not0 n j P show "P i" by(simp add:ac_simps)
   1.665 -      qed
   1.666 -    qed
   1.667 -  qed
   1.668 -next
   1.669 -  assume Q: ?Q
   1.670 -  show ?P
   1.671 -  proof (cases)
   1.672 -    assume "k = 0"
   1.673 -    with Q show ?P by simp
   1.674 -  next
   1.675 -    assume not0: "k \<noteq> 0"
   1.676 -    with Q have R: ?R by simp
   1.677 -    from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
   1.678 -    show ?P by simp
   1.679 -  qed
   1.680 -qed
   1.681 -
   1.682 -lemma split_div_lemma:
   1.683 -  assumes "0 < n"
   1.684 -  shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m::nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")
   1.685 -proof
   1.686 -  assume ?rhs
   1.687 -  with minus_mod_eq_mult_div [symmetric] have nq: "n * q = m - (m mod n)" by simp
   1.688 -  then have A: "n * q \<le> m" by simp
   1.689 -  have "n - (m mod n) > 0" using mod_less_divisor assms by auto
   1.690 -  then have "m < m + (n - (m mod n))" by simp
   1.691 -  then have "m < n + (m - (m mod n))" by simp
   1.692 -  with nq have "m < n + n * q" by simp
   1.693 -  then have B: "m < n * Suc q" by simp
   1.694 -  from A B show ?lhs ..
   1.695 -next
   1.696 -  assume P: ?lhs
   1.697 -  then have "eucl_rel_nat m n (q, m - n * q)"
   1.698 -    by (auto intro: eucl_rel_natI simp add: ac_simps)
   1.699 -  then have "m div n = q"
   1.700 -    by (rule div_nat_unique)
   1.701 -  then show ?rhs by simp
   1.702 -qed
   1.703 -
   1.704 -theorem split_div':
   1.705 -  "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
   1.706 -   (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
   1.707 -  apply (cases "0 < n")
   1.708 -  apply (simp only: add: split_div_lemma)
   1.709 -  apply simp_all
   1.710 -  done
   1.711 -
   1.712 -lemma split_mod:
   1.713 - "P(n mod k :: nat) =
   1.714 - ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
   1.715 - (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
   1.716 -proof
   1.717 -  assume P: ?P
   1.718 -  show ?Q
   1.719 -  proof (cases)
   1.720 -    assume "k = 0"
   1.721 -    with P show ?Q by simp
   1.722 -  next
   1.723 -    assume not0: "k \<noteq> 0"
   1.724 -    thus ?Q
   1.725 -    proof (simp, intro allI impI)
   1.726 -      fix i j
   1.727 -      assume "n = k*i + j" "j < k"
   1.728 -      thus "P j" using not0 P by (simp add: ac_simps)
   1.729 -    qed
   1.730 -  qed
   1.731 -next
   1.732 -  assume Q: ?Q
   1.733 -  show ?P
   1.734 -  proof (cases)
   1.735 -    assume "k = 0"
   1.736 -    with Q show ?P by simp
   1.737 -  next
   1.738 -    assume not0: "k \<noteq> 0"
   1.739 -    with Q have R: ?R by simp
   1.740 -    from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
   1.741 -    show ?P by simp
   1.742 -  qed
   1.743 -qed
   1.744 -
   1.745 -lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
   1.746 -  apply rule
   1.747 -  apply (cases "b = 0")
   1.748 -  apply simp_all
   1.749 -  apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)
   1.750 -  done
   1.751 -
   1.752 -lemma (in field_char_0) of_nat_div:
   1.753 -  "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
   1.754 -proof -
   1.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)"
   1.756 -    unfolding of_nat_add by (cases "n = 0") simp_all
   1.757 -  then show ?thesis
   1.758 -    by simp
   1.759 -qed
   1.760 -
   1.761 -
   1.762 -subsubsection \<open>An ``induction'' law for modulus arithmetic.\<close>
   1.763 -
   1.764 -lemma mod_induct_0:
   1.765 -  assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
   1.766 -  and base: "P i" and i: "i<p"
   1.767 -  shows "P 0"
   1.768 -proof (rule ccontr)
   1.769 -  assume contra: "\<not>(P 0)"
   1.770 -  from i have p: "0<p" by simp
   1.771 -  have "\<forall>k. 0<k \<longrightarrow> \<not> P (p-k)" (is "\<forall>k. ?A k")
   1.772 -  proof
   1.773 -    fix k
   1.774 -    show "?A k"
   1.775 -    proof (induct k)
   1.776 -      show "?A 0" by simp  \<comment> "by contradiction"
   1.777 -    next
   1.778 -      fix n
   1.779 -      assume ih: "?A n"
   1.780 -      show "?A (Suc n)"
   1.781 -      proof (clarsimp)
   1.782 -        assume y: "P (p - Suc n)"
   1.783 -        have n: "Suc n < p"
   1.784 -        proof (rule ccontr)
   1.785 -          assume "\<not>(Suc n < p)"
   1.786 -          hence "p - Suc n = 0"
   1.787 -            by simp
   1.788 -          with y contra show "False"
   1.789 -            by simp
   1.790 -        qed
   1.791 -        hence n2: "Suc (p - Suc n) = p-n" by arith
   1.792 -        from p have "p - Suc n < p" by arith
   1.793 -        with y step have z: "P ((Suc (p - Suc n)) mod p)"
   1.794 -          by blast
   1.795 -        show "False"
   1.796 -        proof (cases "n=0")
   1.797 -          case True
   1.798 -          with z n2 contra show ?thesis by simp
   1.799 -        next
   1.800 -          case False
   1.801 -          with p have "p-n < p" by arith
   1.802 -          with z n2 False ih show ?thesis by simp
   1.803 -        qed
   1.804 -      qed
   1.805 -    qed
   1.806 -  qed
   1.807 -  moreover
   1.808 -  from i obtain k where "0<k \<and> i+k=p"
   1.809 -    by (blast dest: less_imp_add_positive)
   1.810 -  hence "0<k \<and> i=p-k" by auto
   1.811 -  moreover
   1.812 -  note base
   1.813 -  ultimately
   1.814 -  show "False" by blast
   1.815 -qed
   1.816 -
   1.817 -lemma mod_induct:
   1.818 -  assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
   1.819 -  and base: "P i" and i: "i<p" and j: "j<p"
   1.820 -  shows "P j"
   1.821 -proof -
   1.822 -  have "\<forall>j<p. P j"
   1.823 -  proof
   1.824 -    fix j
   1.825 -    show "j<p \<longrightarrow> P j" (is "?A j")
   1.826 -    proof (induct j)
   1.827 -      from step base i show "?A 0"
   1.828 -        by (auto elim: mod_induct_0)
   1.829 -    next
   1.830 -      fix k
   1.831 -      assume ih: "?A k"
   1.832 -      show "?A (Suc k)"
   1.833 -      proof
   1.834 -        assume suc: "Suc k < p"
   1.835 -        hence k: "k<p" by simp
   1.836 -        with ih have "P k" ..
   1.837 -        with step k have "P (Suc k mod p)"
   1.838 -          by blast
   1.839 -        moreover
   1.840 -        from suc have "Suc k mod p = Suc k"
   1.841 -          by simp
   1.842 -        ultimately
   1.843 -        show "P (Suc k)" by simp
   1.844 -      qed
   1.845 -    qed
   1.846 -  qed
   1.847 -  with j show ?thesis by blast
   1.848 -qed
   1.849 -
   1.850 -lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)"
   1.851 -  by (simp add: numeral_2_eq_2 le_div_geq)
   1.852 -
   1.853 -lemma mod2_Suc_Suc [simp]: "Suc (Suc m) mod 2 = m mod 2"
   1.854 -  by (simp add: numeral_2_eq_2 le_mod_geq)
   1.855 -
   1.856 -lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
   1.857 -by (simp add: mult_2 [symmetric])
   1.858 -
   1.859 -lemma mod2_gr_0 [simp]: "0 < (m::nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
   1.860 -proof -
   1.861 -  { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all }
   1.862 -  moreover have "m mod 2 < 2" by simp
   1.863 -  ultimately have "m mod 2 = 0 \<or> m mod 2 = 1" .
   1.864 -  then show ?thesis by auto
   1.865 -qed
   1.866 -
   1.867 -text\<open>These lemmas collapse some needless occurrences of Suc:
   1.868 -    at least three Sucs, since two and fewer are rewritten back to Suc again!
   1.869 -    We already have some rules to simplify operands smaller than 3.\<close>
   1.870 -
   1.871 -lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
   1.872 -by (simp add: Suc3_eq_add_3)
   1.873 -
   1.874 -lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
   1.875 -by (simp add: Suc3_eq_add_3)
   1.876 -
   1.877 -lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
   1.878 -by (simp add: Suc3_eq_add_3)
   1.879 -
   1.880 -lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
   1.881 -by (simp add: Suc3_eq_add_3)
   1.882 -
   1.883 -lemmas Suc_div_eq_add3_div_numeral [simp] = Suc_div_eq_add3_div [of _ "numeral v"] for v
   1.884 -lemmas Suc_mod_eq_add3_mod_numeral [simp] = Suc_mod_eq_add3_mod [of _ "numeral v"] for v
   1.885 -
   1.886 -lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1"
   1.887 -apply (induct "m")
   1.888 -apply (simp_all add: mod_Suc)
   1.889 -done
   1.890 -
   1.891 -declare Suc_times_mod_eq [of "numeral w", simp] for w
   1.892 -
   1.893 -lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"
   1.894 -by (simp add: div_le_mono)
   1.895 -
   1.896 -lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
   1.897 -by (cases n) simp_all
   1.898 -
   1.899 -lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2"
   1.900 -proof -
   1.901 -  from A have B: "0 < n - 1" and C: "n - 1 + 1 = n" by simp_all
   1.902 -  from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp
   1.903 -qed
   1.904 -
   1.905 -lemma mod_mult_self3' [simp]: "Suc (k * n + m) mod n = Suc m mod n"
   1.906 -  using mod_mult_self3 [of k n "Suc m"] by simp
   1.907 -
   1.908 -lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
   1.909 -apply (subst mod_Suc [of m])
   1.910 -apply (subst mod_Suc [of "m mod n"], simp)
   1.911 -done
   1.912 -
   1.913 -lemma mod_2_not_eq_zero_eq_one_nat:
   1.914 -  fixes n :: nat
   1.915 -  shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
   1.916 -  by (fact not_mod_2_eq_0_eq_1)
   1.917 +lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
   1.918 +  by (auto elim: oddE)
   1.919  
   1.920  lemma even_Suc_div_two [simp]:
   1.921    "even n \<Longrightarrow> Suc n div 2 = n div 2"
   1.922 @@ -1245,6 +367,11 @@
   1.923    qed
   1.924  qed
   1.925  
   1.926 +lemma mod_2_not_eq_zero_eq_one_nat:
   1.927 +  fixes n :: nat
   1.928 +  shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
   1.929 +  by (fact not_mod_2_eq_0_eq_1)
   1.930 +
   1.931  lemma Suc_0_div_numeral [simp]:
   1.932    fixes k l :: num
   1.933    shows "Suc 0 div numeral k = fst (divmod Num.One k)"
   1.934 @@ -1255,6 +382,27 @@
   1.935    shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
   1.936    by (simp_all add: snd_divmod)
   1.937  
   1.938 +definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
   1.939 +  where "divmod_nat m n = (m div n, m mod n)"
   1.940 +
   1.941 +lemma fst_divmod_nat [simp]:
   1.942 +  "fst (divmod_nat m n) = m div n"
   1.943 +  by (simp add: divmod_nat_def)
   1.944 +
   1.945 +lemma snd_divmod_nat [simp]:
   1.946 +  "snd (divmod_nat m n) = m mod n"
   1.947 +  by (simp add: divmod_nat_def)
   1.948 +
   1.949 +lemma divmod_nat_if [code]:
   1.950 +  "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
   1.951 +    let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
   1.952 +  by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
   1.953 +
   1.954 +lemma [code]:
   1.955 +  "m div n = fst (divmod_nat m n)"
   1.956 +  "m mod n = snd (divmod_nat m n)"
   1.957 +  by simp_all
   1.958 +
   1.959  
   1.960  subsection \<open>Division on @{typ int}\<close>
   1.961  
   1.962 @@ -2225,7 +1373,7 @@
   1.963  lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
   1.964  apply (subgoal_tac "nat x div nat k < nat x")
   1.965   apply (simp add: nat_div_distrib [symmetric])
   1.966 -apply (rule Divides.div_less_dividend, simp_all)
   1.967 +apply (rule div_less_dividend, simp_all)
   1.968  done
   1.969  
   1.970  lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
   1.971 @@ -2258,11 +1406,12 @@
   1.972    thus  ?lhs by simp
   1.973  qed
   1.974  
   1.975 +
   1.976  subsubsection \<open>Dedicated simproc for calculation\<close>
   1.977  
   1.978  text \<open>
   1.979    There is space for improvement here: the calculation itself
   1.980 -  could be carried outside the logic, and a generic simproc
   1.981 +  could be carried out outside the logic, and a generic simproc
   1.982    (simplifier setup) for generic calculation would be helpful. 
   1.983  \<close>
   1.984  
   1.985 @@ -2348,4 +1497,39 @@
   1.986  
   1.987  declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
   1.988  
   1.989 +
   1.990 +subsubsection \<open>Lemmas of doubtful value\<close>
   1.991 +
   1.992 +lemma mod_mult_self3':
   1.993 +  "Suc (k * n + m) mod n = Suc m mod n"
   1.994 +  by (fact Suc_mod_mult_self3)
   1.995 +
   1.996 +lemma mod_Suc_eq_Suc_mod:
   1.997 +  "Suc m mod n = Suc (m mod n) mod n"
   1.998 +  by (simp add: mod_simps)
   1.999 +
  1.1000 +lemma div_geq:
  1.1001 +  "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
  1.1002 +  by (rule le_div_geq) (use that in \<open>simp_all add: not_less\<close>)
  1.1003 +
  1.1004 +lemma mod_geq:
  1.1005 +  "m mod n = (m - n) mod n" if "\<not> m < n" for m n :: nat
  1.1006 +  by (rule le_mod_geq) (use that in \<open>simp add: not_less\<close>)
  1.1007 +
  1.1008 +lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
  1.1009 +  by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
  1.1010 +
  1.1011 +lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
  1.1012 +
  1.1013 +(*Loses information, namely we also have r<d provided d is nonzero*)
  1.1014 +lemma mod_eqD:
  1.1015 +  fixes m d r q :: nat
  1.1016 +  assumes "m mod d = r"
  1.1017 +  shows "\<exists>q. m = r + q * d"
  1.1018 +proof -
  1.1019 +  from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
  1.1020 +  with assms have "m = r + q * d" by simp
  1.1021 +  then show ?thesis ..
  1.1022 +qed
  1.1023 +
  1.1024  end