src/HOL/Euclidean_Division.thy
changeset 66808 1907167b6038
parent 66807 c3631f32dfeb
child 66810 cc2b490f9dc4
     1.1 --- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -6,9 +6,19 @@
     1.4  section \<open>Uniquely determined division in euclidean (semi)rings\<close>
     1.5  
     1.6  theory Euclidean_Division
     1.7 -  imports Nat_Transfer
     1.8 +  imports Nat_Transfer Lattices_Big
     1.9  begin
    1.10  
    1.11 +subsection \<open>Prelude: simproc for cancelling @{const divide} and @{const modulo}\<close>
    1.12 +
    1.13 +lemma (in semiring_modulo) cancel_div_mod_rules:
    1.14 +  "((a div b) * b + a mod b) + c = a + c"
    1.15 +  "(b * (a div b) + a mod b) + c = a + c"
    1.16 +  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
    1.17 +
    1.18 +ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
    1.19 +
    1.20 +
    1.21  subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
    1.22    
    1.23  class euclidean_semiring = semidom_modulo + normalization_semidom + 
    1.24 @@ -639,4 +649,657 @@
    1.25  
    1.26  end
    1.27  
    1.28 +
    1.29 +subsection \<open>Euclidean division on @{typ nat}\<close>
    1.30 +
    1.31 +instantiation nat :: unique_euclidean_semiring
    1.32 +begin
    1.33 +
    1.34 +definition normalize_nat :: "nat \<Rightarrow> nat"
    1.35 +  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
    1.36 +
    1.37 +definition unit_factor_nat :: "nat \<Rightarrow> nat"
    1.38 +  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
    1.39 +
    1.40 +lemma unit_factor_simps [simp]:
    1.41 +  "unit_factor 0 = (0::nat)"
    1.42 +  "unit_factor (Suc n) = 1"
    1.43 +  by (simp_all add: unit_factor_nat_def)
    1.44 +
    1.45 +definition euclidean_size_nat :: "nat \<Rightarrow> nat"
    1.46 +  where [simp]: "euclidean_size_nat = id"
    1.47 +
    1.48 +definition uniqueness_constraint_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
    1.49 +  where [simp]: "uniqueness_constraint_nat = \<top>"
    1.50 +
    1.51 +definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    1.52 +  where "m div n = (if n = 0 then 0 else Max {k::nat. k * n \<le> m})"
    1.53 +
    1.54 +definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    1.55 +  where "m mod n = m - (m div n * (n::nat))"
    1.56 +
    1.57 +instance proof
    1.58 +  fix m n :: nat
    1.59 +  have ex: "\<exists>k. k * n \<le> l" for l :: nat
    1.60 +    by (rule exI [of _ 0]) simp
    1.61 +  have fin: "finite {k. k * n \<le> l}" if "n > 0" for l
    1.62 +  proof -
    1.63 +    from that have "{k. k * n \<le> l} \<subseteq> {k. k \<le> l}"
    1.64 +      by (cases n) auto
    1.65 +    then show ?thesis
    1.66 +      by (rule finite_subset) simp
    1.67 +  qed
    1.68 +  have mult_div_unfold: "n * (m div n) = Max {l. l \<le> m \<and> n dvd l}"
    1.69 +  proof (cases "n = 0")
    1.70 +    case True
    1.71 +    moreover have "{l. l = 0 \<and> l \<le> m} = {0::nat}"
    1.72 +      by auto
    1.73 +    ultimately show ?thesis
    1.74 +      by simp
    1.75 +  next
    1.76 +    case False
    1.77 +    with ex [of m] fin have "n * Max {k. k * n \<le> m} = Max (times n ` {k. k * n \<le> m})"
    1.78 +      by (auto simp add: nat_mult_max_right intro: hom_Max_commute)
    1.79 +    also have "times n ` {k. k * n \<le> m} = {l. l \<le> m \<and> n dvd l}"
    1.80 +      by (auto simp add: ac_simps elim!: dvdE)
    1.81 +    finally show ?thesis
    1.82 +      using False by (simp add: divide_nat_def ac_simps)
    1.83 +  qed
    1.84 +  show "n div 0 = 0"
    1.85 +    by (simp add: divide_nat_def)
    1.86 +  have less_eq: "m div n * n \<le> m"
    1.87 +    by (auto simp add: mult_div_unfold ac_simps intro: Max.boundedI)
    1.88 +  then show "m div n * n + m mod n = m"
    1.89 +    by (simp add: modulo_nat_def)
    1.90 +  assume "n \<noteq> 0" 
    1.91 +  show "m * n div n = m"
    1.92 +    using \<open>n \<noteq> 0\<close> by (auto simp add: divide_nat_def ac_simps intro: Max_eqI)
    1.93 +  show "euclidean_size (m mod n) < euclidean_size n"
    1.94 +  proof -
    1.95 +    have "m < Suc (m div n) * n"
    1.96 +    proof (rule ccontr)
    1.97 +      assume "\<not> m < Suc (m div n) * n"
    1.98 +      then have "Suc (m div n) * n \<le> m"
    1.99 +        by (simp add: not_less)
   1.100 +      moreover from \<open>n \<noteq> 0\<close> have "Max {k. k * n \<le> m} < Suc (m div n)"
   1.101 +        by (simp add: divide_nat_def)
   1.102 +      with \<open>n \<noteq> 0\<close> ex fin have "\<And>k. k * n \<le> m \<Longrightarrow> k < Suc (m div n)"
   1.103 +        by auto
   1.104 +      ultimately have "Suc (m div n) < Suc (m div n)"
   1.105 +        by blast
   1.106 +      then show False
   1.107 +        by simp
   1.108 +    qed
   1.109 +    with \<open>n \<noteq> 0\<close> show ?thesis
   1.110 +      by (simp add: modulo_nat_def)
   1.111 +  qed
   1.112 +  show "euclidean_size m \<le> euclidean_size (m * n)"
   1.113 +    using \<open>n \<noteq> 0\<close> by (cases n) simp_all
   1.114 +  fix q r :: nat
   1.115 +  show "(q * n + r) div n = q" if "euclidean_size r < euclidean_size n"
   1.116 +  proof -
   1.117 +    from that have "r < n"
   1.118 +      by simp
   1.119 +    have "k \<le> q" if "k * n \<le> q * n + r" for k
   1.120 +    proof (rule ccontr)
   1.121 +      assume "\<not> k \<le> q"
   1.122 +      then have "q < k"
   1.123 +        by simp
   1.124 +      then obtain l where "k = Suc (q + l)"
   1.125 +        by (auto simp add: less_iff_Suc_add)
   1.126 +      with \<open>r < n\<close> that show False
   1.127 +        by (simp add: algebra_simps)
   1.128 +    qed
   1.129 +    with \<open>n \<noteq> 0\<close> ex fin show ?thesis
   1.130 +      by (auto simp add: divide_nat_def Max_eq_iff)
   1.131 +  qed
   1.132 +qed (simp_all add: unit_factor_nat_def)
   1.133 +
   1.134  end
   1.135 +
   1.136 +text \<open>Tool support\<close>
   1.137 +
   1.138 +ML \<open>
   1.139 +structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
   1.140 +(
   1.141 +  val div_name = @{const_name divide};
   1.142 +  val mod_name = @{const_name modulo};
   1.143 +  val mk_binop = HOLogic.mk_binop;
   1.144 +  val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
   1.145 +  val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
   1.146 +  fun mk_sum [] = HOLogic.zero
   1.147 +    | mk_sum [t] = t
   1.148 +    | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   1.149 +  fun dest_sum tm =
   1.150 +    if HOLogic.is_zero tm then []
   1.151 +    else
   1.152 +      (case try HOLogic.dest_Suc tm of
   1.153 +        SOME t => HOLogic.Suc_zero :: dest_sum t
   1.154 +      | NONE =>
   1.155 +          (case try dest_plus tm of
   1.156 +            SOME (t, u) => dest_sum t @ dest_sum u
   1.157 +          | NONE => [tm]));
   1.158 +
   1.159 +  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
   1.160 +
   1.161 +  val prove_eq_sums = Arith_Data.prove_conv2 all_tac
   1.162 +    (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps})
   1.163 +)
   1.164 +\<close>
   1.165 +
   1.166 +simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
   1.167 +  \<open>K Cancel_Div_Mod_Nat.proc\<close>
   1.168 +
   1.169 +lemma div_nat_eqI:
   1.170 +  "m div n = q" if "n * q \<le> m" and "m < n * Suc q" for m n q :: nat
   1.171 +  by (rule div_eqI [of _ "m - n * q"]) (use that in \<open>simp_all add: algebra_simps\<close>)
   1.172 +
   1.173 +lemma mod_nat_eqI:
   1.174 +  "m mod n = r" if "r < n" and "r \<le> m" and "n dvd m - r" for m n r :: nat
   1.175 +  by (rule mod_eqI [of _ _ "(m - r) div n"]) (use that in \<open>simp_all add: algebra_simps\<close>)
   1.176 +
   1.177 +lemma div_mult_self_is_m [simp]:
   1.178 +  "m * n div n = m" if "n > 0" for m n :: nat
   1.179 +  using that by simp
   1.180 +
   1.181 +lemma div_mult_self1_is_m [simp]:
   1.182 +  "n * m div n = m" if "n > 0" for m n :: nat
   1.183 +  using that by simp
   1.184 +
   1.185 +lemma mod_less_divisor [simp]:
   1.186 +  "m mod n < n" if "n > 0" for m n :: nat
   1.187 +  using mod_size_less [of n m] that by simp
   1.188 +
   1.189 +lemma mod_le_divisor [simp]:
   1.190 +  "m mod n \<le> n" if "n > 0" for m n :: nat
   1.191 +  using that by (auto simp add: le_less)
   1.192 +
   1.193 +lemma div_times_less_eq_dividend [simp]:
   1.194 +  "m div n * n \<le> m" for m n :: nat
   1.195 +  by (simp add: minus_mod_eq_div_mult [symmetric])
   1.196 +
   1.197 +lemma times_div_less_eq_dividend [simp]:
   1.198 +  "n * (m div n) \<le> m" for m n :: nat
   1.199 +  using div_times_less_eq_dividend [of m n]
   1.200 +  by (simp add: ac_simps)
   1.201 +
   1.202 +lemma dividend_less_div_times:
   1.203 +  "m < n + (m div n) * n" if "0 < n" for m n :: nat
   1.204 +proof -
   1.205 +  from that have "m mod n < n"
   1.206 +    by simp
   1.207 +  then show ?thesis
   1.208 +    by (simp add: minus_mod_eq_div_mult [symmetric])
   1.209 +qed
   1.210 +
   1.211 +lemma dividend_less_times_div:
   1.212 +  "m < n + n * (m div n)" if "0 < n" for m n :: nat
   1.213 +  using dividend_less_div_times [of n m] that
   1.214 +  by (simp add: ac_simps)
   1.215 +
   1.216 +lemma mod_Suc_le_divisor [simp]:
   1.217 +  "m mod Suc n \<le> n"
   1.218 +  using mod_less_divisor [of "Suc n" m] by arith
   1.219 +
   1.220 +lemma mod_less_eq_dividend [simp]:
   1.221 +  "m mod n \<le> m" for m n :: nat
   1.222 +proof (rule add_leD2)
   1.223 +  from div_mult_mod_eq have "m div n * n + m mod n = m" .
   1.224 +  then show "m div n * n + m mod n \<le> m" by auto
   1.225 +qed
   1.226 +
   1.227 +lemma
   1.228 +  div_less [simp]: "m div n = 0"
   1.229 +  and mod_less [simp]: "m mod n = m"
   1.230 +  if "m < n" for m n :: nat
   1.231 +  using that by (auto intro: div_eqI mod_eqI) 
   1.232 +
   1.233 +lemma le_div_geq:
   1.234 +  "m div n = Suc ((m - n) div n)" if "0 < n" and "n \<le> m" for m n :: nat
   1.235 +proof -
   1.236 +  from \<open>n \<le> m\<close> obtain q where "m = n + q"
   1.237 +    by (auto simp add: le_iff_add)
   1.238 +  with \<open>0 < n\<close> show ?thesis
   1.239 +    by (simp add: div_add_self1)
   1.240 +qed
   1.241 +
   1.242 +lemma le_mod_geq:
   1.243 +  "m mod n = (m - n) mod n" if "n \<le> m" for m n :: nat
   1.244 +proof -
   1.245 +  from \<open>n \<le> m\<close> obtain q where "m = n + q"
   1.246 +    by (auto simp add: le_iff_add)
   1.247 +  then show ?thesis
   1.248 +    by simp
   1.249 +qed
   1.250 +
   1.251 +lemma div_if:
   1.252 +  "m div n = (if m < n \<or> n = 0 then 0 else Suc ((m - n) div n))"
   1.253 +  by (simp add: le_div_geq)
   1.254 +
   1.255 +lemma mod_if:
   1.256 +  "m mod n = (if m < n then m else (m - n) mod n)" for m n :: nat
   1.257 +  by (simp add: le_mod_geq)
   1.258 +
   1.259 +lemma div_eq_0_iff:
   1.260 +  "m div n = 0 \<longleftrightarrow> m < n \<or> n = 0" for m n :: nat
   1.261 +  by (simp add: div_if)
   1.262 +
   1.263 +lemma div_greater_zero_iff:
   1.264 +  "m div n > 0 \<longleftrightarrow> n \<le> m \<and> n > 0" for m n :: nat
   1.265 +  using div_eq_0_iff [of m n] by auto
   1.266 +
   1.267 +lemma mod_greater_zero_iff_not_dvd:
   1.268 +  "m mod n > 0 \<longleftrightarrow> \<not> n dvd m" for m n :: nat
   1.269 +  by (simp add: dvd_eq_mod_eq_0)
   1.270 +
   1.271 +lemma div_by_Suc_0 [simp]:
   1.272 +  "m div Suc 0 = m"
   1.273 +  using div_by_1 [of m] by simp
   1.274 +
   1.275 +lemma mod_by_Suc_0 [simp]:
   1.276 +  "m mod Suc 0 = 0"
   1.277 +  using mod_by_1 [of m] by simp
   1.278 +
   1.279 +lemma div2_Suc_Suc [simp]:
   1.280 +  "Suc (Suc m) div 2 = Suc (m div 2)"
   1.281 +  by (simp add: numeral_2_eq_2 le_div_geq)
   1.282 +
   1.283 +lemma Suc_n_div_2_gt_zero [simp]:
   1.284 +  "0 < Suc n div 2" if "n > 0" for n :: nat
   1.285 +  using that by (cases n) simp_all
   1.286 +
   1.287 +lemma div_2_gt_zero [simp]:
   1.288 +  "0 < n div 2" if "Suc 0 < n" for n :: nat
   1.289 +  using that Suc_n_div_2_gt_zero [of "n - 1"] by simp
   1.290 +
   1.291 +lemma mod2_Suc_Suc [simp]:
   1.292 +  "Suc (Suc m) mod 2 = m mod 2"
   1.293 +  by (simp add: numeral_2_eq_2 le_mod_geq)
   1.294 +
   1.295 +lemma add_self_div_2 [simp]:
   1.296 +  "(m + m) div 2 = m" for m :: nat
   1.297 +  by (simp add: mult_2 [symmetric])
   1.298 +
   1.299 +lemma add_self_mod_2 [simp]:
   1.300 +  "(m + m) mod 2 = 0" for m :: nat
   1.301 +  by (simp add: mult_2 [symmetric])
   1.302 +
   1.303 +lemma mod2_gr_0 [simp]:
   1.304 +  "0 < m mod 2 \<longleftrightarrow> m mod 2 = 1" for m :: nat
   1.305 +proof -
   1.306 +  have "m mod 2 < 2"
   1.307 +    by (rule mod_less_divisor) simp
   1.308 +  then have "m mod 2 = 0 \<or> m mod 2 = 1"
   1.309 +    by arith
   1.310 +  then show ?thesis
   1.311 +    by auto     
   1.312 +qed
   1.313 +
   1.314 +lemma mod_Suc_eq [mod_simps]:
   1.315 +  "Suc (m mod n) mod n = Suc m mod n"
   1.316 +proof -
   1.317 +  have "(m mod n + 1) mod n = (m + 1) mod n"
   1.318 +    by (simp only: mod_simps)
   1.319 +  then show ?thesis
   1.320 +    by simp
   1.321 +qed
   1.322 +
   1.323 +lemma mod_Suc_Suc_eq [mod_simps]:
   1.324 +  "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
   1.325 +proof -
   1.326 +  have "(m mod n + 2) mod n = (m + 2) mod n"
   1.327 +    by (simp only: mod_simps)
   1.328 +  then show ?thesis
   1.329 +    by simp
   1.330 +qed
   1.331 +
   1.332 +lemma
   1.333 +  Suc_mod_mult_self1 [simp]: "Suc (m + k * n) mod n = Suc m mod n"
   1.334 +  and Suc_mod_mult_self2 [simp]: "Suc (m + n * k) mod n = Suc m mod n"
   1.335 +  and Suc_mod_mult_self3 [simp]: "Suc (k * n + m) mod n = Suc m mod n"
   1.336 +  and Suc_mod_mult_self4 [simp]: "Suc (n * k + m) mod n = Suc m mod n"
   1.337 +  by (subst mod_Suc_eq [symmetric], simp add: mod_simps)+
   1.338 +
   1.339 +lemma div_mult1_eq: -- \<open>TODO: Generalization candidate\<close>
   1.340 +  "(a * b) div c = a * (b div c) + a * (b mod c) div c" for a b c :: nat
   1.341 +  apply (cases "c = 0")
   1.342 +   apply simp
   1.343 +  apply (rule div_eqI [of _ "(a * (b mod c)) mod c"])
   1.344 +     apply (auto simp add: algebra_simps distrib_left [symmetric])
   1.345 +  done
   1.346 +
   1.347 +lemma div_add1_eq: -- \<open>NOT suitable for rewriting: the RHS has an instance of the LHS\<close>
   1.348 +   -- \<open>TODO: Generalization candidate\<close>
   1.349 +  "(a + b) div c = a div c + b div c + ((a mod c + b mod c) div c)" for a b c :: nat
   1.350 +  apply (cases "c = 0")
   1.351 +   apply simp
   1.352 +  apply (rule div_eqI [of _ "(a mod c + b mod c) mod c"])
   1.353 +  apply (auto simp add: algebra_simps)
   1.354 +  done
   1.355 +
   1.356 +context
   1.357 +  fixes m n q :: nat
   1.358 +begin
   1.359 +
   1.360 +private lemma eucl_rel_mult2:
   1.361 +  "m mod n + n * (m div n mod q) < n * q"
   1.362 +  if "n > 0" and "q > 0"
   1.363 +proof -
   1.364 +  from \<open>n > 0\<close> have "m mod n < n"
   1.365 +    by (rule mod_less_divisor)
   1.366 +  from \<open>q > 0\<close> have "m div n mod q < q"
   1.367 +    by (rule mod_less_divisor)
   1.368 +  then obtain s where "q = Suc (m div n mod q + s)"
   1.369 +    by (blast dest: less_imp_Suc_add)
   1.370 +  moreover have "m mod n + n * (m div n mod q) < n * Suc (m div n mod q + s)"
   1.371 +    using \<open>m mod n < n\<close> by (simp add: add_mult_distrib2)
   1.372 +  ultimately show ?thesis
   1.373 +    by simp
   1.374 +qed
   1.375 +
   1.376 +lemma div_mult2_eq:
   1.377 +  "m div (n * q) = (m div n) div q"
   1.378 +proof (cases "n = 0 \<or> q = 0")
   1.379 +  case True
   1.380 +  then show ?thesis
   1.381 +    by auto
   1.382 +next
   1.383 +  case False
   1.384 +  with eucl_rel_mult2 show ?thesis
   1.385 +    by (auto intro: div_eqI [of _ "n * (m div n mod q) + m mod n"]
   1.386 +      simp add: algebra_simps add_mult_distrib2 [symmetric])
   1.387 +qed
   1.388 +
   1.389 +lemma mod_mult2_eq:
   1.390 +  "m mod (n * q) = n * (m div n mod q) + m mod n"
   1.391 +proof (cases "n = 0 \<or> q = 0")
   1.392 +  case True
   1.393 +  then show ?thesis
   1.394 +    by auto
   1.395 +next
   1.396 +  case False
   1.397 +  with eucl_rel_mult2 show ?thesis
   1.398 +    by (auto intro: mod_eqI [of _ _ "(m div n) div q"]
   1.399 +      simp add: algebra_simps add_mult_distrib2 [symmetric])
   1.400 +qed
   1.401 +
   1.402 +end
   1.403 +
   1.404 +lemma div_le_mono:
   1.405 +  "m div k \<le> n div k" if "m \<le> n" for m n k :: nat
   1.406 +proof -
   1.407 +  from that obtain q where "n = m + q"
   1.408 +    by (auto simp add: le_iff_add)
   1.409 +  then show ?thesis
   1.410 +    by (simp add: div_add1_eq [of m q k])
   1.411 +qed
   1.412 +
   1.413 +text \<open>Antimonotonicity of @{const divide} in second argument\<close>
   1.414 +
   1.415 +lemma div_le_mono2:
   1.416 +  "k div n \<le> k div m" if "0 < m" and "m \<le> n" for m n k :: nat
   1.417 +using that proof (induct k arbitrary: m rule: less_induct)
   1.418 +  case (less k)
   1.419 +  show ?case
   1.420 +  proof (cases "n \<le> k")
   1.421 +    case False
   1.422 +    then show ?thesis
   1.423 +      by simp
   1.424 +  next
   1.425 +    case True
   1.426 +    have "(k - n) div n \<le> (k - m) div n"
   1.427 +      using less.prems
   1.428 +      by (blast intro: div_le_mono diff_le_mono2)
   1.429 +    also have "\<dots> \<le> (k - m) div m"
   1.430 +      using \<open>n \<le> k\<close> less.prems less.hyps [of "k - m" m]
   1.431 +      by simp
   1.432 +    finally show ?thesis
   1.433 +      using \<open>n \<le> k\<close> less.prems
   1.434 +      by (simp add: le_div_geq)
   1.435 +  qed
   1.436 +qed
   1.437 +
   1.438 +lemma div_le_dividend [simp]:
   1.439 +  "m div n \<le> m" for m n :: nat
   1.440 +  using div_le_mono2 [of 1 n m] by (cases "n = 0") simp_all
   1.441 +
   1.442 +lemma div_less_dividend [simp]:
   1.443 +  "m div n < m" if "1 < n" and "0 < m" for m n :: nat
   1.444 +using that proof (induct m rule: less_induct)
   1.445 +  case (less m)
   1.446 +  show ?case
   1.447 +  proof (cases "n < m")
   1.448 +    case False
   1.449 +    with less show ?thesis
   1.450 +      by (cases "n = m") simp_all
   1.451 +  next
   1.452 +    case True
   1.453 +    then show ?thesis
   1.454 +      using less.hyps [of "m - n"] less.prems
   1.455 +      by (simp add: le_div_geq)
   1.456 +  qed
   1.457 +qed
   1.458 +
   1.459 +lemma div_eq_dividend_iff:
   1.460 +  "m div n = m \<longleftrightarrow> n = 1" if "m > 0" for m n :: nat
   1.461 +proof
   1.462 +  assume "n = 1"
   1.463 +  then show "m div n = m"
   1.464 +    by simp
   1.465 +next
   1.466 +  assume P: "m div n = m"
   1.467 +  show "n = 1"
   1.468 +  proof (rule ccontr)
   1.469 +    have "n \<noteq> 0"
   1.470 +      by (rule ccontr) (use that P in auto)
   1.471 +    moreover assume "n \<noteq> 1"
   1.472 +    ultimately have "n > 1"
   1.473 +      by simp
   1.474 +    with that have "m div n < m"
   1.475 +      by simp
   1.476 +    with P show False
   1.477 +      by simp
   1.478 +  qed
   1.479 +qed
   1.480 +
   1.481 +lemma less_mult_imp_div_less:
   1.482 +  "m div n < i" if "m < i * n" for m n i :: nat
   1.483 +proof -
   1.484 +  from that have "i * n > 0"
   1.485 +    by (cases "i * n = 0") simp_all
   1.486 +  then have "i > 0" and "n > 0"
   1.487 +    by simp_all
   1.488 +  have "m div n * n \<le> m"
   1.489 +    by simp
   1.490 +  then have "m div n * n < i * n"
   1.491 +    using that by (rule le_less_trans)
   1.492 +  with \<open>n > 0\<close> show ?thesis
   1.493 +    by simp
   1.494 +qed
   1.495 +
   1.496 +text \<open>A fact for the mutilated chess board\<close>
   1.497 +
   1.498 +lemma mod_Suc:
   1.499 +  "Suc m mod n = (if Suc (m mod n) = n then 0 else Suc (m mod n))" (is "_ = ?rhs")
   1.500 +proof (cases "n = 0")
   1.501 +  case True
   1.502 +  then show ?thesis
   1.503 +    by simp
   1.504 +next
   1.505 +  case False
   1.506 +  have "Suc m mod n = Suc (m mod n) mod n"
   1.507 +    by (simp add: mod_simps)
   1.508 +  also have "\<dots> = ?rhs"
   1.509 +    using False by (auto intro!: mod_nat_eqI intro: neq_le_trans simp add: Suc_le_eq)
   1.510 +  finally show ?thesis .
   1.511 +qed
   1.512 +
   1.513 +lemma Suc_times_mod_eq:
   1.514 +  "Suc (m * n) mod m = 1" if "Suc 0 < m"
   1.515 +  using that by (simp add: mod_Suc)
   1.516 +
   1.517 +lemma Suc_times_numeral_mod_eq [simp]:
   1.518 +  "Suc (numeral k * n) mod numeral k = 1" if "numeral k \<noteq> (1::nat)"
   1.519 +  by (rule Suc_times_mod_eq) (use that in simp)
   1.520 +
   1.521 +lemma Suc_div_le_mono [simp]:
   1.522 +  "m div n \<le> Suc m div n"
   1.523 +  by (simp add: div_le_mono)
   1.524 +
   1.525 +text \<open>These lemmas collapse some needless occurrences of Suc:
   1.526 +  at least three Sucs, since two and fewer are rewritten back to Suc again!
   1.527 +  We already have some rules to simplify operands smaller than 3.\<close>
   1.528 +
   1.529 +lemma div_Suc_eq_div_add3 [simp]:
   1.530 +  "m div Suc (Suc (Suc n)) = m div (3 + n)"
   1.531 +  by (simp add: Suc3_eq_add_3)
   1.532 +
   1.533 +lemma mod_Suc_eq_mod_add3 [simp]:
   1.534 +  "m mod Suc (Suc (Suc n)) = m mod (3 + n)"
   1.535 +  by (simp add: Suc3_eq_add_3)
   1.536 +
   1.537 +lemma Suc_div_eq_add3_div:
   1.538 +  "Suc (Suc (Suc m)) div n = (3 + m) div n"
   1.539 +  by (simp add: Suc3_eq_add_3)
   1.540 +
   1.541 +lemma Suc_mod_eq_add3_mod:
   1.542 +  "Suc (Suc (Suc m)) mod n = (3 + m) mod n"
   1.543 +  by (simp add: Suc3_eq_add_3)
   1.544 +
   1.545 +lemmas Suc_div_eq_add3_div_numeral [simp] =
   1.546 +  Suc_div_eq_add3_div [of _ "numeral v"] for v
   1.547 +
   1.548 +lemmas Suc_mod_eq_add3_mod_numeral [simp] =
   1.549 +  Suc_mod_eq_add3_mod [of _ "numeral v"] for v
   1.550 +
   1.551 +lemma (in field_char_0) of_nat_div:
   1.552 +  "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
   1.553 +proof -
   1.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)"
   1.555 +    unfolding of_nat_add by (cases "n = 0") simp_all
   1.556 +  then show ?thesis
   1.557 +    by simp
   1.558 +qed
   1.559 +
   1.560 +text \<open>An ``induction'' law for modulus arithmetic.\<close>
   1.561 +
   1.562 +lemma mod_induct [consumes 3, case_names step]:
   1.563 +  "P m" if "P n" and "n < p" and "m < p"
   1.564 +    and step: "\<And>n. n < p \<Longrightarrow> P n \<Longrightarrow> P (Suc n mod p)"
   1.565 +using \<open>m < p\<close> proof (induct m)
   1.566 +  case 0
   1.567 +  show ?case
   1.568 +  proof (rule ccontr)
   1.569 +    assume "\<not> P 0"
   1.570 +    from \<open>n < p\<close> have "0 < p"
   1.571 +      by simp
   1.572 +    from \<open>n < p\<close> obtain m where "0 < m" and "p = n + m"
   1.573 +      by (blast dest: less_imp_add_positive)
   1.574 +    with \<open>P n\<close> have "P (p - m)"
   1.575 +      by simp
   1.576 +    moreover have "\<not> P (p - m)"
   1.577 +    using \<open>0 < m\<close> proof (induct m)
   1.578 +      case 0
   1.579 +      then show ?case
   1.580 +        by simp
   1.581 +    next
   1.582 +      case (Suc m)
   1.583 +      show ?case
   1.584 +      proof
   1.585 +        assume P: "P (p - Suc m)"
   1.586 +        with \<open>\<not> P 0\<close> have "Suc m < p"
   1.587 +          by (auto intro: ccontr) 
   1.588 +        then have "Suc (p - Suc m) = p - m"
   1.589 +          by arith
   1.590 +        moreover from \<open>0 < p\<close> have "p - Suc m < p"
   1.591 +          by arith
   1.592 +        with P step have "P ((Suc (p - Suc m)) mod p)"
   1.593 +          by blast
   1.594 +        ultimately show False
   1.595 +          using \<open>\<not> P 0\<close> Suc.hyps by (cases "m = 0") simp_all
   1.596 +      qed
   1.597 +    qed
   1.598 +    ultimately show False
   1.599 +      by blast
   1.600 +  qed
   1.601 +next
   1.602 +  case (Suc m)
   1.603 +  then have "m < p" and mod: "Suc m mod p = Suc m"
   1.604 +    by simp_all
   1.605 +  from \<open>m < p\<close> have "P m"
   1.606 +    by (rule Suc.hyps)
   1.607 +  with \<open>m < p\<close> have "P (Suc m mod p)"
   1.608 +    by (rule step)
   1.609 +  with mod show ?case
   1.610 +    by simp
   1.611 +qed
   1.612 +
   1.613 +lemma split_div:
   1.614 +  "P (m div n) \<longleftrightarrow> (n = 0 \<longrightarrow> P 0) \<and> (n \<noteq> 0 \<longrightarrow>
   1.615 +     (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P i))"
   1.616 +     (is "?P = ?Q") for m n :: nat
   1.617 +proof (cases "n = 0")
   1.618 +  case True
   1.619 +  then show ?thesis
   1.620 +    by simp
   1.621 +next
   1.622 +  case False
   1.623 +  show ?thesis
   1.624 +  proof
   1.625 +    assume ?P
   1.626 +    with False show ?Q
   1.627 +      by auto
   1.628 +  next
   1.629 +    assume ?Q
   1.630 +    with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P i"
   1.631 +      by simp
   1.632 +    with False show ?P
   1.633 +      by (auto intro: * [of "m mod n"])
   1.634 +  qed
   1.635 +qed
   1.636 +
   1.637 +lemma split_div':
   1.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)"
   1.639 +proof (cases "n = 0")
   1.640 +  case True
   1.641 +  then show ?thesis
   1.642 +    by simp
   1.643 +next
   1.644 +  case False
   1.645 +  then have "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> m div n = q" for q
   1.646 +    by (auto intro: div_nat_eqI dividend_less_times_div)
   1.647 +  then show ?thesis
   1.648 +    by auto
   1.649 +qed
   1.650 +
   1.651 +lemma split_mod:
   1.652 +  "P (m mod n) \<longleftrightarrow> (n = 0 \<longrightarrow> P m) \<and> (n \<noteq> 0 \<longrightarrow>
   1.653 +     (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P j))"
   1.654 +     (is "?P \<longleftrightarrow> ?Q") for m n :: nat
   1.655 +proof (cases "n = 0")
   1.656 +  case True
   1.657 +  then show ?thesis
   1.658 +    by simp
   1.659 +next
   1.660 +  case False
   1.661 +  show ?thesis
   1.662 +  proof
   1.663 +    assume ?P
   1.664 +    with False show ?Q
   1.665 +      by auto
   1.666 +  next
   1.667 +    assume ?Q
   1.668 +    with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P j"
   1.669 +      by simp
   1.670 +    with False show ?P
   1.671 +      by (auto intro: * [of _ "m div n"])
   1.672 +  qed
   1.673 +qed
   1.674 +
   1.675 +
   1.676 +subsection \<open>Code generation\<close>
   1.677 +
   1.678 +code_identifier
   1.679 +  code_module Euclidean_Division \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   1.680 +
   1.681 +end