src/HOL/Euclidean_Division.thy

 *)
 
 section \<open>Uniquely determined division in euclidean (semi)rings\<close>
 
 theory Euclidean_Division
-  imports Nat_Transfer
+  imports Nat_Transfer Lattices_Big
 begin
+
+subsection \<open>Prelude: simproc for cancelling @{const divide} and @{const modulo}\<close>
+
+lemma (in semiring_modulo) cancel_div_mod_rules:
+  "((a div b) * b + a mod b) + c = a + c"
+  "(b * (a div b) + a mod b) + c = a + c"
+  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
+
+ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
+
 
 subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
   
 class euclidean_semiring = semidom_modulo + normalization_semidom + 
   fixes euclidean_size :: "'a \<Rightarrow> nat"

   
 subclass euclidean_ring_cancel ..
 
 end
 
+
+subsection \<open>Euclidean division on @{typ nat}\<close>
+
+instantiation nat :: unique_euclidean_semiring
+begin
+
+definition normalize_nat :: "nat \<Rightarrow> nat"
+  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
+
+definition unit_factor_nat :: "nat \<Rightarrow> nat"
+  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
+
+lemma unit_factor_simps [simp]:
+  "unit_factor 0 = (0::nat)"
+  "unit_factor (Suc n) = 1"
+  by (simp_all add: unit_factor_nat_def)
+
+definition euclidean_size_nat :: "nat \<Rightarrow> nat"
+  where [simp]: "euclidean_size_nat = id"
+
+definition uniqueness_constraint_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
+  where [simp]: "uniqueness_constraint_nat = \<top>"
+
+definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  where "m div n = (if n = 0 then 0 else Max {k::nat. k * n \<le> m})"
+
+definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  where "m mod n = m - (m div n * (n::nat))"
+
+instance proof
+  fix m n :: nat
+  have ex: "\<exists>k. k * n \<le> l" for l :: nat
+    by (rule exI [of _ 0]) simp
+  have fin: "finite {k. k * n \<le> l}" if "n > 0" for l
+  proof -
+    from that have "{k. k * n \<le> l} \<subseteq> {k. k \<le> l}"
+      by (cases n) auto
+    then show ?thesis
+      by (rule finite_subset) simp
+  qed
+  have mult_div_unfold: "n * (m div n) = Max {l. l \<le> m \<and> n dvd l}"
+  proof (cases "n = 0")
+    case True
+    moreover have "{l. l = 0 \<and> l \<le> m} = {0::nat}"
+      by auto
+    ultimately show ?thesis
+      by simp
+  next
+    case False
+    with ex [of m] fin have "n * Max {k. k * n \<le> m} = Max (times n ` {k. k * n \<le> m})"
+      by (auto simp add: nat_mult_max_right intro: hom_Max_commute)
+    also have "times n ` {k. k * n \<le> m} = {l. l \<le> m \<and> n dvd l}"
+      by (auto simp add: ac_simps elim!: dvdE)
+    finally show ?thesis
+      using False by (simp add: divide_nat_def ac_simps)
+  qed
+  show "n div 0 = 0"
+    by (simp add: divide_nat_def)
+  have less_eq: "m div n * n \<le> m"
+    by (auto simp add: mult_div_unfold ac_simps intro: Max.boundedI)
+  then show "m div n * n + m mod n = m"
+    by (simp add: modulo_nat_def)
+  assume "n \<noteq> 0" 
+  show "m * n div n = m"
+    using \<open>n \<noteq> 0\<close> by (auto simp add: divide_nat_def ac_simps intro: Max_eqI)
+  show "euclidean_size (m mod n) < euclidean_size n"
+  proof -
+    have "m < Suc (m div n) * n"
+    proof (rule ccontr)
+      assume "\<not> m < Suc (m div n) * n"
+      then have "Suc (m div n) * n \<le> m"
+        by (simp add: not_less)
+      moreover from \<open>n \<noteq> 0\<close> have "Max {k. k * n \<le> m} < Suc (m div n)"
+        by (simp add: divide_nat_def)
+      with \<open>n \<noteq> 0\<close> ex fin have "\<And>k. k * n \<le> m \<Longrightarrow> k < Suc (m div n)"
+        by auto
+      ultimately have "Suc (m div n) < Suc (m div n)"
+        by blast
+      then show False
+        by simp
+    qed
+    with \<open>n \<noteq> 0\<close> show ?thesis
+      by (simp add: modulo_nat_def)
+  qed
+  show "euclidean_size m \<le> euclidean_size (m * n)"
+    using \<open>n \<noteq> 0\<close> by (cases n) simp_all
+  fix q r :: nat
+  show "(q * n + r) div n = q" if "euclidean_size r < euclidean_size n"
+  proof -
+    from that have "r < n"
+      by simp
+    have "k \<le> q" if "k * n \<le> q * n + r" for k
+    proof (rule ccontr)
+      assume "\<not> k \<le> q"
+      then have "q < k"
+        by simp
+      then obtain l where "k = Suc (q + l)"
+        by (auto simp add: less_iff_Suc_add)
+      with \<open>r < n\<close> that show False
+        by (simp add: algebra_simps)
+    qed
+    with \<open>n \<noteq> 0\<close> ex fin show ?thesis
+      by (auto simp add: divide_nat_def Max_eq_iff)
+  qed
+qed (simp_all add: unit_factor_nat_def)
+
 end
+
+text \<open>Tool support\<close>
+
+ML \<open>
+structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
+(
+  val div_name = @{const_name divide};
+  val mod_name = @{const_name modulo};
+  val mk_binop = HOLogic.mk_binop;
+  val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
+  val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
+  fun mk_sum [] = HOLogic.zero
+    | mk_sum [t] = t
+    | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+  fun dest_sum tm =
+    if HOLogic.is_zero tm then []
+    else
+      (case try HOLogic.dest_Suc tm of
+        SOME t => HOLogic.Suc_zero :: dest_sum t
+      | NONE =>
+          (case try dest_plus tm of
+            SOME (t, u) => dest_sum t @ dest_sum u
+          | NONE => [tm]));
+
+  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
+
+  val prove_eq_sums = Arith_Data.prove_conv2 all_tac
+    (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps})
+)
+\<close>
+
+simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
+  \<open>K Cancel_Div_Mod_Nat.proc\<close>
+
+lemma div_nat_eqI:
+  "m div n = q" if "n * q \<le> m" and "m < n * Suc q" for m n q :: nat
+  by (rule div_eqI [of _ "m - n * q"]) (use that in \<open>simp_all add: algebra_simps\<close>)
+
+lemma mod_nat_eqI:
+  "m mod n = r" if "r < n" and "r \<le> m" and "n dvd m - r" for m n r :: nat
+  by (rule mod_eqI [of _ _ "(m - r) div n"]) (use that in \<open>simp_all add: algebra_simps\<close>)
+
+lemma div_mult_self_is_m [simp]:
+  "m * n div n = m" if "n > 0" for m n :: nat
+  using that by simp
+
+lemma div_mult_self1_is_m [simp]:
+  "n * m div n = m" if "n > 0" for m n :: nat
+  using that by simp
+
+lemma mod_less_divisor [simp]:
+  "m mod n < n" if "n > 0" for m n :: nat
+  using mod_size_less [of n m] that by simp
+
+lemma mod_le_divisor [simp]:
+  "m mod n \<le> n" if "n > 0" for m n :: nat
+  using that by (auto simp add: le_less)
+
+lemma div_times_less_eq_dividend [simp]:
+  "m div n * n \<le> m" for m n :: nat
+  by (simp add: minus_mod_eq_div_mult [symmetric])
+
+lemma times_div_less_eq_dividend [simp]:
+  "n * (m div n) \<le> m" for m n :: nat
+  using div_times_less_eq_dividend [of m n]
+  by (simp add: ac_simps)
+
+lemma dividend_less_div_times:
+  "m < n + (m div n) * n" if "0 < n" for m n :: nat
+proof -
+  from that have "m mod n < n"
+    by simp
+  then show ?thesis
+    by (simp add: minus_mod_eq_div_mult [symmetric])
+qed
+
+lemma dividend_less_times_div:
+  "m < n + n * (m div n)" if "0 < n" for m n :: nat
+  using dividend_less_div_times [of n m] that
+  by (simp add: ac_simps)
+
+lemma mod_Suc_le_divisor [simp]:
+  "m mod Suc n \<le> n"
+  using mod_less_divisor [of "Suc n" m] by arith
+
+lemma mod_less_eq_dividend [simp]:
+  "m mod n \<le> m" for m n :: nat
+proof (rule add_leD2)
+  from div_mult_mod_eq have "m div n * n + m mod n = m" .
+  then show "m div n * n + m mod n \<le> m" by auto
+qed
+
+lemma
+  div_less [simp]: "m div n = 0"
+  and mod_less [simp]: "m mod n = m"
+  if "m < n" for m n :: nat
+  using that by (auto intro: div_eqI mod_eqI) 
+
+lemma le_div_geq:
+  "m div n = Suc ((m - n) div n)" if "0 < n" and "n \<le> m" for m n :: nat
+proof -
+  from \<open>n \<le> m\<close> obtain q where "m = n + q"
+    by (auto simp add: le_iff_add)
+  with \<open>0 < n\<close> show ?thesis
+    by (simp add: div_add_self1)
+qed
+
+lemma le_mod_geq:
+  "m mod n = (m - n) mod n" if "n \<le> m" for m n :: nat
+proof -
+  from \<open>n \<le> m\<close> obtain q where "m = n + q"
+    by (auto simp add: le_iff_add)
+  then show ?thesis
+    by simp
+qed
+
+lemma div_if:
+  "m div n = (if m < n \<or> n = 0 then 0 else Suc ((m - n) div n))"
+  by (simp add: le_div_geq)
+
+lemma mod_if:
+  "m mod n = (if m < n then m else (m - n) mod n)" for m n :: nat
+  by (simp add: le_mod_geq)
+
+lemma div_eq_0_iff:
+  "m div n = 0 \<longleftrightarrow> m < n \<or> n = 0" for m n :: nat
+  by (simp add: div_if)
+
+lemma div_greater_zero_iff:
+  "m div n > 0 \<longleftrightarrow> n \<le> m \<and> n > 0" for m n :: nat
+  using div_eq_0_iff [of m n] by auto
+
+lemma mod_greater_zero_iff_not_dvd:
+  "m mod n > 0 \<longleftrightarrow> \<not> n dvd m" for m n :: nat
+  by (simp add: dvd_eq_mod_eq_0)
+
+lemma div_by_Suc_0 [simp]:
+  "m div Suc 0 = m"
+  using div_by_1 [of m] by simp
+
+lemma mod_by_Suc_0 [simp]:
+  "m mod Suc 0 = 0"
+  using mod_by_1 [of m] by simp
+
+lemma div2_Suc_Suc [simp]:
+  "Suc (Suc m) div 2 = Suc (m div 2)"
+  by (simp add: numeral_2_eq_2 le_div_geq)
+
+lemma Suc_n_div_2_gt_zero [simp]:
+  "0 < Suc n div 2" if "n > 0" for n :: nat
+  using that by (cases n) simp_all
+
+lemma div_2_gt_zero [simp]:
+  "0 < n div 2" if "Suc 0 < n" for n :: nat
+  using that Suc_n_div_2_gt_zero [of "n - 1"] by simp
+
+lemma mod2_Suc_Suc [simp]:
+  "Suc (Suc m) mod 2 = m mod 2"
+  by (simp add: numeral_2_eq_2 le_mod_geq)
+
+lemma add_self_div_2 [simp]:
+  "(m + m) div 2 = m" for m :: nat
+  by (simp add: mult_2 [symmetric])
+
+lemma add_self_mod_2 [simp]:
+  "(m + m) mod 2 = 0" for m :: nat
+  by (simp add: mult_2 [symmetric])
+
+lemma mod2_gr_0 [simp]:
+  "0 < m mod 2 \<longleftrightarrow> m mod 2 = 1" for m :: nat
+proof -
+  have "m mod 2 < 2"
+    by (rule mod_less_divisor) simp
+  then have "m mod 2 = 0 \<or> m mod 2 = 1"
+    by arith
+  then show ?thesis
+    by auto     
+qed
+
+lemma mod_Suc_eq [mod_simps]:
+  "Suc (m mod n) mod n = Suc m mod n"
+proof -
+  have "(m mod n + 1) mod n = (m + 1) mod n"
+    by (simp only: mod_simps)
+  then show ?thesis
+    by simp
+qed
+
+lemma mod_Suc_Suc_eq [mod_simps]:
+  "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
+proof -
+  have "(m mod n + 2) mod n = (m + 2) mod n"
+    by (simp only: mod_simps)
+  then show ?thesis
+    by simp
+qed
+
+lemma
+  Suc_mod_mult_self1 [simp]: "Suc (m + k * n) mod n = Suc m mod n"
+  and Suc_mod_mult_self2 [simp]: "Suc (m + n * k) mod n = Suc m mod n"
+  and Suc_mod_mult_self3 [simp]: "Suc (k * n + m) mod n = Suc m mod n"
+  and Suc_mod_mult_self4 [simp]: "Suc (n * k + m) mod n = Suc m mod n"
+  by (subst mod_Suc_eq [symmetric], simp add: mod_simps)+
+
+lemma div_mult1_eq: -- \<open>TODO: Generalization candidate\<close>
+  "(a * b) div c = a * (b div c) + a * (b mod c) div c" for a b c :: nat
+  apply (cases "c = 0")
+   apply simp
+  apply (rule div_eqI [of _ "(a * (b mod c)) mod c"])
+     apply (auto simp add: algebra_simps distrib_left [symmetric])
+  done
+
+lemma div_add1_eq: -- \<open>NOT suitable for rewriting: the RHS has an instance of the LHS\<close>
+   -- \<open>TODO: Generalization candidate\<close>
+  "(a + b) div c = a div c + b div c + ((a mod c + b mod c) div c)" for a b c :: nat
+  apply (cases "c = 0")
+   apply simp
+  apply (rule div_eqI [of _ "(a mod c + b mod c) mod c"])
+  apply (auto simp add: algebra_simps)
+  done
+
+context
+  fixes m n q :: nat
+begin
+
+private lemma eucl_rel_mult2:
+  "m mod n + n * (m div n mod q) < n * q"
+  if "n > 0" and "q > 0"
+proof -
+  from \<open>n > 0\<close> have "m mod n < n"
+    by (rule mod_less_divisor)
+  from \<open>q > 0\<close> have "m div n mod q < q"
+    by (rule mod_less_divisor)
+  then obtain s where "q = Suc (m div n mod q + s)"
+    by (blast dest: less_imp_Suc_add)
+  moreover have "m mod n + n * (m div n mod q) < n * Suc (m div n mod q + s)"
+    using \<open>m mod n < n\<close> by (simp add: add_mult_distrib2)
+  ultimately show ?thesis
+    by simp
+qed
+
+lemma div_mult2_eq:
+  "m div (n * q) = (m div n) div q"
+proof (cases "n = 0 \<or> q = 0")
+  case True
+  then show ?thesis
+    by auto
+next
+  case False
+  with eucl_rel_mult2 show ?thesis
+    by (auto intro: div_eqI [of _ "n * (m div n mod q) + m mod n"]
+      simp add: algebra_simps add_mult_distrib2 [symmetric])
+qed
+
+lemma mod_mult2_eq:
+  "m mod (n * q) = n * (m div n mod q) + m mod n"
+proof (cases "n = 0 \<or> q = 0")
+  case True
+  then show ?thesis
+    by auto
+next
+  case False
+  with eucl_rel_mult2 show ?thesis
+    by (auto intro: mod_eqI [of _ _ "(m div n) div q"]
+      simp add: algebra_simps add_mult_distrib2 [symmetric])
+qed
+
+end
+
+lemma div_le_mono:
+  "m div k \<le> n div k" if "m \<le> n" for m n k :: nat
+proof -
+  from that obtain q where "n = m + q"
+    by (auto simp add: le_iff_add)
+  then show ?thesis
+    by (simp add: div_add1_eq [of m q k])
+qed
+
+text \<open>Antimonotonicity of @{const divide} in second argument\<close>
+
+lemma div_le_mono2:
+  "k div n \<le> k div m" if "0 < m" and "m \<le> n" for m n k :: nat
+using that proof (induct k arbitrary: m rule: less_induct)
+  case (less k)
+  show ?case
+  proof (cases "n \<le> k")
+    case False
+    then show ?thesis
+      by simp
+  next
+    case True
+    have "(k - n) div n \<le> (k - m) div n"
+      using less.prems
+      by (blast intro: div_le_mono diff_le_mono2)
+    also have "\<dots> \<le> (k - m) div m"
+      using \<open>n \<le> k\<close> less.prems less.hyps [of "k - m" m]
+      by simp
+    finally show ?thesis
+      using \<open>n \<le> k\<close> less.prems
+      by (simp add: le_div_geq)
+  qed
+qed
+
+lemma div_le_dividend [simp]:
+  "m div n \<le> m" for m n :: nat
+  using div_le_mono2 [of 1 n m] by (cases "n = 0") simp_all
+
+lemma div_less_dividend [simp]:
+  "m div n < m" if "1 < n" and "0 < m" for m n :: nat
+using that proof (induct m rule: less_induct)
+  case (less m)
+  show ?case
+  proof (cases "n < m")
+    case False
+    with less show ?thesis
+      by (cases "n = m") simp_all
+  next
+    case True
+    then show ?thesis
+      using less.hyps [of "m - n"] less.prems
+      by (simp add: le_div_geq)
+  qed
+qed
+
+lemma div_eq_dividend_iff:
+  "m div n = m \<longleftrightarrow> n = 1" if "m > 0" for m n :: nat
+proof
+  assume "n = 1"
+  then show "m div n = m"
+    by simp
+next
+  assume P: "m div n = m"
+  show "n = 1"
+  proof (rule ccontr)
+    have "n \<noteq> 0"
+      by (rule ccontr) (use that P in auto)
+    moreover assume "n \<noteq> 1"
+    ultimately have "n > 1"
+      by simp
+    with that have "m div n < m"
+      by simp
+    with P show False
+      by simp
+  qed
+qed
+
+lemma less_mult_imp_div_less:
+  "m div n < i" if "m < i * n" for m n i :: nat
+proof -
+  from that have "i * n > 0"
+    by (cases "i * n = 0") simp_all
+  then have "i > 0" and "n > 0"
+    by simp_all
+  have "m div n * n \<le> m"
+    by simp
+  then have "m div n * n < i * n"
+    using that by (rule le_less_trans)
+  with \<open>n > 0\<close> show ?thesis
+    by simp
+qed
+
+text \<open>A fact for the mutilated chess board\<close>
+
+lemma mod_Suc:
+  "Suc m mod n = (if Suc (m mod n) = n then 0 else Suc (m mod n))" (is "_ = ?rhs")
+proof (cases "n = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  have "Suc m mod n = Suc (m mod n) mod n"
+    by (simp add: mod_simps)
+  also have "\<dots> = ?rhs"
+    using False by (auto intro!: mod_nat_eqI intro: neq_le_trans simp add: Suc_le_eq)
+  finally show ?thesis .
+qed
+
+lemma Suc_times_mod_eq:
+  "Suc (m * n) mod m = 1" if "Suc 0 < m"
+  using that by (simp add: mod_Suc)
+
+lemma Suc_times_numeral_mod_eq [simp]:
+  "Suc (numeral k * n) mod numeral k = 1" if "numeral k \<noteq> (1::nat)"
+  by (rule Suc_times_mod_eq) (use that in simp)
+
+lemma Suc_div_le_mono [simp]:
+  "m div n \<le> Suc m div n"
+  by (simp add: div_le_mono)
+
+text \<open>These lemmas collapse some needless occurrences of Suc:
+  at least three Sucs, since two and fewer are rewritten back to Suc again!
+  We already have some rules to simplify operands smaller than 3.\<close>
+
+lemma div_Suc_eq_div_add3 [simp]:
+  "m div Suc (Suc (Suc n)) = m div (3 + n)"
+  by (simp add: Suc3_eq_add_3)
+
+lemma mod_Suc_eq_mod_add3 [simp]:
+  "m mod Suc (Suc (Suc n)) = m mod (3 + n)"
+  by (simp add: Suc3_eq_add_3)
+
+lemma Suc_div_eq_add3_div:
+  "Suc (Suc (Suc m)) div n = (3 + m) div n"
+  by (simp add: Suc3_eq_add_3)
+
+lemma Suc_mod_eq_add3_mod:
+  "Suc (Suc (Suc m)) mod n = (3 + m) mod n"
+  by (simp add: Suc3_eq_add_3)
+
+lemmas Suc_div_eq_add3_div_numeral [simp] =
+  Suc_div_eq_add3_div [of _ "numeral v"] for v
+
+lemmas Suc_mod_eq_add3_mod_numeral [simp] =
+  Suc_mod_eq_add3_mod [of _ "numeral v"] for v
+
+lemma (in field_char_0) of_nat_div:
+  "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
+proof -
+  have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
+    unfolding of_nat_add by (cases "n = 0") simp_all
+  then show ?thesis
+    by simp
+qed
+
+text \<open>An ``induction'' law for modulus arithmetic.\<close>
+
+lemma mod_induct [consumes 3, case_names step]:
+  "P m" if "P n" and "n < p" and "m < p"
+    and step: "\<And>n. n < p \<Longrightarrow> P n \<Longrightarrow> P (Suc n mod p)"
+using \<open>m < p\<close> proof (induct m)
+  case 0
+  show ?case
+  proof (rule ccontr)
+    assume "\<not> P 0"
+    from \<open>n < p\<close> have "0 < p"
+      by simp
+    from \<open>n < p\<close> obtain m where "0 < m" and "p = n + m"
+      by (blast dest: less_imp_add_positive)
+    with \<open>P n\<close> have "P (p - m)"
+      by simp
+    moreover have "\<not> P (p - m)"
+    using \<open>0 < m\<close> proof (induct m)
+      case 0
+      then show ?case
+        by simp
+    next
+      case (Suc m)
+      show ?case
+      proof
+        assume P: "P (p - Suc m)"
+        with \<open>\<not> P 0\<close> have "Suc m < p"
+          by (auto intro: ccontr) 
+        then have "Suc (p - Suc m) = p - m"
+          by arith
+        moreover from \<open>0 < p\<close> have "p - Suc m < p"
+          by arith
+        with P step have "P ((Suc (p - Suc m)) mod p)"
+          by blast
+        ultimately show False
+          using \<open>\<not> P 0\<close> Suc.hyps by (cases "m = 0") simp_all
+      qed
+    qed
+    ultimately show False
+      by blast
+  qed
+next
+  case (Suc m)
+  then have "m < p" and mod: "Suc m mod p = Suc m"
+    by simp_all
+  from \<open>m < p\<close> have "P m"
+    by (rule Suc.hyps)
+  with \<open>m < p\<close> have "P (Suc m mod p)"
+    by (rule step)
+  with mod show ?case
+    by simp
+qed
+
+lemma split_div:
+  "P (m div n) \<longleftrightarrow> (n = 0 \<longrightarrow> P 0) \<and> (n \<noteq> 0 \<longrightarrow>
+     (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P i))"
+     (is "?P = ?Q") for m n :: nat
+proof (cases "n = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  show ?thesis
+  proof
+    assume ?P
+    with False show ?Q
+      by auto
+  next
+    assume ?Q
+    with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P i"
+      by simp
+    with False show ?P
+      by (auto intro: * [of "m mod n"])
+  qed
+qed
+
+lemma split_div':
+  "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)"
+proof (cases "n = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  then have "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> m div n = q" for q
+    by (auto intro: div_nat_eqI dividend_less_times_div)
+  then show ?thesis
+    by auto
+qed
+
+lemma split_mod:
+  "P (m mod n) \<longleftrightarrow> (n = 0 \<longrightarrow> P m) \<and> (n \<noteq> 0 \<longrightarrow>
+     (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P j))"
+     (is "?P \<longleftrightarrow> ?Q") for m n :: nat
+proof (cases "n = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  show ?thesis
+  proof
+    assume ?P
+    with False show ?Q
+      by auto
+  next
+    assume ?Q
+    with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P j"
+      by simp
+    with False show ?P
+      by (auto intro: * [of _ "m div n"])
+  qed
+qed
+
+
+subsection \<open>Code generation\<close>
+
+code_identifier
+  code_module Euclidean_Division \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
+
+end