# Theory Divides

Up to index of Isabelle/HOL

theory Divides
imports Datatype
begin

    (*  Title:      HOL/Divides.thy
        ID:         $Id: Divides.thy,v 1.30 2005/09/23 20:21:49 wenzelm Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1999  University of Cambridge

    The division operators div, mod and the divides relation "dvd"
    *)

    theory Divides
    imports Datatype
    begin

    (*We use the same class for div and mod;
      moreover, dvd is defined whenever multiplication is*)
    axclass
      div < type

    instance  nat :: div ..

    consts
      div  :: "'a::div => 'a => 'a"          (infixl 70)
      mod  :: "'a::div => 'a => 'a"          (infixl 70)
      dvd  :: "'a::times => 'a => bool"      (infixl 50)

    defs

      mod_def:   "m mod n == wfrec (trancl pred_nat)
                              (%f j. if j<n | n=0 then j else f (j-n)) m"

      div_def:   "m div n == wfrec (trancl pred_nat)
                              (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"

    (*The definition of dvd is polymorphic!*)
      dvd_def:   "m dvd n == ∃k. n = m*k"

    (*This definition helps prove the harder properties of div and mod.
      It is copied from IntDiv.thy; should it be overloaded?*)
    constdefs
      quorem :: "(nat*nat) * (nat*nat) => bool"
        "quorem == %((a,b), (q,r)).
                          a = b*q + r &
                          (if 0<b then 0≤r & r<b else b<r & r ≤0)"

    subsection{*Initial Lemmas*}

    lemmas wf_less_trans =
           def_wfrec [THEN trans, OF eq_reflection wf_pred_nat [THEN wf_trancl],
                      standard]

    lemma mod_eq: "(%m. m mod n) =
                  wfrec (trancl pred_nat) (%f j. if j<n | n=0 then j else f (j-n))"
    by (simp add: mod_def)

    lemma div_eq: "(%m. m div n) = wfrec (trancl pred_nat)
                   (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))"
    by (simp add: div_def)

    (** Aribtrary definitions for division by zero.  Useful to simplify
        certain equations **)

    lemma DIVISION_BY_ZERO_DIV [simp]: "a div 0 = (0::nat)"
    by (rule div_eq [THEN wf_less_trans], simp)

    lemma DIVISION_BY_ZERO_MOD [simp]: "a mod 0 = (a::nat)"
    by (rule mod_eq [THEN wf_less_trans], simp)

    subsection{*Remainder*}

    lemma mod_less [simp]: "m<n ==> m mod n = (m::nat)"
    by (rule mod_eq [THEN wf_less_trans], simp)

    lemma mod_geq: "~ m < (n::nat) ==> m mod n = (m-n) mod n"
    apply (case_tac "n=0", simp)
    apply (rule mod_eq [THEN wf_less_trans])
    apply (simp add: cut_apply less_eq)
    done

    (*Avoids the ugly ~m<n above*)
    lemma le_mod_geq: "(n::nat) ≤ m ==> m mod n = (m-n) mod n"
    by (simp add: mod_geq linorder_not_less)

    lemma mod_if: "m mod (n::nat) = (if m<n then m else (m-n) mod n)"
    by (simp add: mod_geq)

    lemma mod_1 [simp]: "m mod Suc 0 = 0"
    apply (induct "m")
    apply (simp_all (no_asm_simp) add: mod_geq)
    done

    lemma mod_self [simp]: "n mod n = (0::nat)"
    apply (case_tac "n=0")
    apply (simp_all add: mod_geq)
    done

    lemma mod_add_self2 [simp]: "(m+n) mod n = m mod (n::nat)"
    apply (subgoal_tac "(n + m) mod n = (n+m-n) mod n")
    apply (simp add: add_commute)
    apply (subst mod_geq [symmetric], simp_all)
    done

    lemma mod_add_self1 [simp]: "(n+m) mod n = m mod (n::nat)"
    by (simp add: add_commute mod_add_self2)

    lemma mod_mult_self1 [simp]: "(m + k*n) mod n = m mod (n::nat)"
    apply (induct "k")
    apply (simp_all add: add_left_commute [of _ n])
    done

    lemma mod_mult_self2 [simp]: "(m + n*k) mod n = m mod (n::nat)"
    by (simp add: mult_commute mod_mult_self1)

    lemma mod_mult_distrib: "(m mod n) * (k::nat) = (m*k) mod (n*k)"
    apply (case_tac "n=0", simp)
    apply (case_tac "k=0", simp)
    apply (induct "m" rule: nat_less_induct)
    apply (subst mod_if, simp)
    apply (simp add: mod_geq diff_mult_distrib)
    done

    lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"
    by (simp add: mult_commute [of k] mod_mult_distrib)

    lemma mod_mult_self_is_0 [simp]: "(m*n) mod n = (0::nat)"
    apply (case_tac "n=0", simp)
    apply (induct "m", simp)
    apply (rename_tac "k")
    apply (cut_tac m = "k*n" and n = n in mod_add_self2)
    apply (simp add: add_commute)
    done

    lemma mod_mult_self1_is_0 [simp]: "(n*m) mod n = (0::nat)"
    by (simp add: mult_commute mod_mult_self_is_0)

    subsection{*Quotient*}

    lemma div_less [simp]: "m<n ==> m div n = (0::nat)"
    by (rule div_eq [THEN wf_less_trans], simp)

    lemma div_geq: "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)"
    apply (rule div_eq [THEN wf_less_trans])
    apply (simp add: cut_apply less_eq)
    done

    (*Avoids the ugly ~m<n above*)
    lemma le_div_geq: "[| 0<n;  n≤m |] ==> m div n = Suc((m-n) div n)"
    by (simp add: div_geq linorder_not_less)

    lemma div_if: "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"
    by (simp add: div_geq)

    (*Main Result about quotient and remainder.*)
    lemma mod_div_equality: "(m div n)*n + m mod n = (m::nat)"
    apply (case_tac "n=0", simp)
    apply (induct "m" rule: nat_less_induct)
    apply (subst mod_if)
    apply (simp_all (no_asm_simp) add: add_assoc div_geq add_diff_inverse)
    done

    lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
    apply(cut_tac m = m and n = n in mod_div_equality)
    apply(simp add: mult_commute)
    done

    subsection{*Simproc for Cancelling Div and Mod*}

    lemma div_mod_equality: "((m div n)*n + m mod n) + k = (m::nat) + k"
    apply(simp add: mod_div_equality)
    done

    lemma div_mod_equality2: "(n*(m div n) + m mod n) + k = (m::nat) + k"
    apply(simp add: mod_div_equality2)
    done

    ML
    {*
    val div_mod_equality = thm "div_mod_equality";
    val div_mod_equality2 = thm "div_mod_equality2";

    structure CancelDivModData =
    struct

    val div_name = "Divides.op div";
    val mod_name = "Divides.op mod";
    val mk_binop = HOLogic.mk_binop;
    val mk_sum = NatArithUtils.mk_sum;
    val dest_sum = NatArithUtils.dest_sum;

    (*logic*)

    val div_mod_eqs = map mk_meta_eq [div_mod_equality,div_mod_equality2]

    val trans = trans

    val prove_eq_sums =
      let val simps = add_0 :: add_0_right :: add_ac
      in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;

    end;

    structure CancelDivMod = CancelDivModFun(CancelDivModData);

    val cancel_div_mod_proc = NatArithUtils.prep_simproc
          ("cancel_div_mod", ["(m::nat) + n"], CancelDivMod.proc);

    Addsimprocs[cancel_div_mod_proc];
    *}

    (* a simple rearrangement of mod_div_equality: *)
    lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
    by (cut_tac m = m and n = n in mod_div_equality2, arith)

    lemma mod_less_divisor [simp]: "0<n ==> m mod n < (n::nat)"
    apply (induct "m" rule: nat_less_induct)
    apply (case_tac "na<n", simp)
    txt{*case @{term "n ≤ na"}*}
    apply (simp add: mod_geq)
    done

    lemma mod_le_divisor[simp]: "0 < n ==> m mod n ≤ (n::nat)"
    apply(drule mod_less_divisor[where m = m])
    apply simp
    done

    lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
    by (cut_tac m = "m*n" and n = n in mod_div_equality, auto)

    lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
    by (simp add: mult_commute div_mult_self_is_m)

    (*mod_mult_distrib2 above is the counterpart for remainder*)

    subsection{*Proving facts about Quotient and Remainder*}

    lemma unique_quotient_lemma:
         "[| b*q' + r'  ≤ b*q + r;  x < b;  r < b |]
          ==> q' ≤ (q::nat)"
    apply (rule leI)
    apply (subst less_iff_Suc_add)
    apply (auto simp add: add_mult_distrib2)
    done

    lemma unique_quotient:
         "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]
          ==> q = q'"
    apply (simp add: split_ifs quorem_def)
    apply (blast intro: order_antisym
                 dest: order_eq_refl [THEN unique_quotient_lemma] sym)
    done

    lemma unique_remainder:
         "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]
          ==> r = r'"
    apply (subgoal_tac "q = q'")
    prefer 2 apply (blast intro: unique_quotient)
    apply (simp add: quorem_def)
    done

    lemma quorem_div_mod: "0 < b ==> quorem ((a, b), (a div b, a mod b))"
    by (auto simp add: quorem_def)

    lemma quorem_div: "[| quorem((a,b),(q,r));  0 < b |] ==> a div b = q"
    by (simp add: quorem_div_mod [THEN unique_quotient])

    lemma quorem_mod: "[| quorem((a,b),(q,r));  0 < b |] ==> a mod b = r"
    by (simp add: quorem_div_mod [THEN unique_remainder])

    (** A dividend of zero **)

    lemma div_0 [simp]: "0 div m = (0::nat)"
    by (case_tac "m=0", simp_all)

    lemma mod_0 [simp]: "0 mod m = (0::nat)"
    by (case_tac "m=0", simp_all)

    (** proving (a*b) div c = a * (b div c) + a * (b mod c) **)

    lemma quorem_mult1_eq:
         "[| quorem((b,c),(q,r));  0 < c |]
          ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
    apply (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
    done

    lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
    apply (case_tac "c = 0", simp)
    apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
    done

    lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
    apply (case_tac "c = 0", simp)
    apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_mod])
    done

    lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"
    apply (rule trans)
    apply (rule_tac s = "b*a mod c" in trans)
    apply (rule_tac [2] mod_mult1_eq)
    apply (simp_all (no_asm) add: mult_commute)
    done

    lemma mod_mult_distrib_mod: "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
    apply (rule mod_mult1_eq' [THEN trans])
    apply (rule mod_mult1_eq)
    done

    (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)

    lemma quorem_add1_eq:
         "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  0 < c |]
          ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
    by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)

    (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
    lemma div_add1_eq:
         "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
    apply (case_tac "c = 0", simp)
    apply (blast intro: quorem_add1_eq [THEN quorem_div] quorem_div_mod quorem_div_mod)
    done

    lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
    apply (case_tac "c = 0", simp)
    apply (blast intro: quorem_div_mod quorem_div_mod
                        quorem_add1_eq [THEN quorem_mod])
    done

    subsection{*Proving @{term "a div (b*c) = (a div b) div c"}*}

    (** first, a lemma to bound the remainder **)

    lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
    apply (cut_tac m = q and n = c in mod_less_divisor)
    apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
    apply (erule_tac P = "%x. ?lhs < ?rhs x" in ssubst)
    apply (simp add: add_mult_distrib2)
    done

    lemma quorem_mult2_eq: "[| quorem ((a,b), (q,r));  0 < b;  0 < c |]
          ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
    apply (auto simp add: mult_ac quorem_def add_mult_distrib2 [symmetric] mod_lemma)
    done

    lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"
    apply (case_tac "b=0", simp)
    apply (case_tac "c=0", simp)
    apply (force simp add: quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_div])
    done

    lemma mod_mult2_eq: "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)"
    apply (case_tac "b=0", simp)
    apply (case_tac "c=0", simp)
    apply (auto simp add: mult_commute quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_mod])
    done

    subsection{*Cancellation of Common Factors in Division*}

    lemma div_mult_mult_lemma:
         "[| (0::nat) < b;  0 < c |] ==> (c*a) div (c*b) = a div b"
    by (auto simp add: div_mult2_eq)

    lemma div_mult_mult1 [simp]: "(0::nat) < c ==> (c*a) div (c*b) = a div b"
    apply (case_tac "b = 0")
    apply (auto simp add: linorder_neq_iff [of b] div_mult_mult_lemma)
    done

    lemma div_mult_mult2 [simp]: "(0::nat) < c ==> (a*c) div (b*c) = a div b"
    apply (drule div_mult_mult1)
    apply (auto simp add: mult_commute)
    done

    (*Distribution of Factors over Remainders:

    Could prove these as in Integ/IntDiv.ML, but we already have
    mod_mult_distrib and mod_mult_distrib2 above!

    Goal "(c*a) mod (c*b) = (c::nat) * (a mod b)"
    qed "mod_mult_mult1";

    Goal "(a*c) mod (b*c) = (a mod b) * (c::nat)";
    qed "mod_mult_mult2";
     ***)

    subsection{*Further Facts about Quotient and Remainder*}

    lemma div_1 [simp]: "m div Suc 0 = m"
    apply (induct "m")
    apply (simp_all (no_asm_simp) add: div_geq)
    done

    lemma div_self [simp]: "0<n ==> n div n = (1::nat)"
    by (simp add: div_geq)

    lemma div_add_self2: "0<n ==> (m+n) div n = Suc (m div n)"
    apply (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n) ")
    apply (simp add: add_commute)
    apply (subst div_geq [symmetric], simp_all)
    done

    lemma div_add_self1: "0<n ==> (n+m) div n = Suc (m div n)"
    by (simp add: add_commute div_add_self2)

    lemma div_mult_self1 [simp]: "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n"
    apply (subst div_add1_eq)
    apply (subst div_mult1_eq, simp)
    done

    lemma div_mult_self2 [simp]: "0<n ==> (m + n*k) div n = k + m div (n::nat)"
    by (simp add: mult_commute div_mult_self1)

    (* Monotonicity of div in first argument *)
    lemma div_le_mono [rule_format (no_asm)]:
         "∀m::nat. m ≤ n --> (m div k) ≤ (n div k)"
    apply (case_tac "k=0", simp)
    apply (induct "n" rule: nat_less_induct, clarify)
    apply (case_tac "n<k")
    (* 1  case n<k *)
    apply simp
    (* 2  case n >= k *)
    apply (case_tac "m<k")
    (* 2.1  case m<k *)
    apply simp
    (* 2.2  case m>=k *)
    apply (simp add: div_geq diff_le_mono)
    done

    (* Antimonotonicity of div in second argument *)
    lemma div_le_mono2: "!!m::nat. [| 0<m; m≤n |] ==> (k div n) ≤ (k div m)"
    apply (subgoal_tac "0<n")
     prefer 2 apply simp
    apply (induct_tac k rule: nat_less_induct)
    apply (rename_tac "k")
    apply (case_tac "k<n", simp)
    apply (subgoal_tac "~ (k<m) ")
     prefer 2 apply simp
    apply (simp add: div_geq)
    apply (subgoal_tac "(k-n) div n ≤ (k-m) div n")
     prefer 2
     apply (blast intro: div_le_mono diff_le_mono2)
    apply (rule le_trans, simp)
    apply (simp)
    done

    lemma div_le_dividend [simp]: "m div n ≤ (m::nat)"
    apply (case_tac "n=0", simp)
    apply (subgoal_tac "m div n ≤ m div 1", simp)
    apply (rule div_le_mono2)
    apply (simp_all (no_asm_simp))
    done

    (* Similar for "less than" *)
    lemma div_less_dividend [rule_format]:
         "!!n::nat. 1<n ==> 0 < m --> m div n < m"
    apply (induct_tac m rule: nat_less_induct)
    apply (rename_tac "m")
    apply (case_tac "m<n", simp)
    apply (subgoal_tac "0<n")
     prefer 2 apply simp
    apply (simp add: div_geq)
    apply (case_tac "n<m")
     apply (subgoal_tac "(m-n) div n < (m-n) ")
      apply (rule impI less_trans_Suc)+
    apply assumption
      apply (simp_all)
    done

    declare div_less_dividend [simp]

    text{*A fact for the mutilated chess board*}
    lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
    apply (case_tac "n=0", simp)
    apply (induct "m" rule: nat_less_induct)
    apply (case_tac "Suc (na) <n")
    (* case Suc(na) < n *)
    apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
    (* case n ≤ Suc(na) *)
    apply (simp add: linorder_not_less le_Suc_eq mod_geq)
    apply (auto simp add: Suc_diff_le le_mod_geq)
    done

    lemma nat_mod_div_trivial [simp]: "m mod n div n = (0 :: nat)"
    by (case_tac "n=0", auto)

    lemma nat_mod_mod_trivial [simp]: "m mod n mod n = (m mod n :: nat)"
    by (case_tac "n=0", auto)

    subsection{*The Divides Relation*}

    lemma dvdI [intro?]: "n = m * k ==> m dvd n"
    by (unfold dvd_def, blast)

    lemma dvdE [elim?]: "!!P. [|m dvd n;  !!k. n = m*k ==> P|] ==> P"
    by (unfold dvd_def, blast)

    lemma dvd_0_right [iff]: "m dvd (0::nat)"
    apply (unfold dvd_def)
    apply (blast intro: mult_0_right [symmetric])
    done

    lemma dvd_0_left: "0 dvd m ==> m = (0::nat)"
    by (force simp add: dvd_def)

    lemma dvd_0_left_iff [iff]: "(0 dvd (m::nat)) = (m = 0)"
    by (blast intro: dvd_0_left)

    lemma dvd_1_left [iff]: "Suc 0 dvd k"
    by (unfold dvd_def, simp)

    lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
    by (simp add: dvd_def)

    lemma dvd_refl [simp]: "m dvd (m::nat)"
    apply (unfold dvd_def)
    apply (blast intro: mult_1_right [symmetric])
    done

    lemma dvd_trans [trans]: "[| m dvd n; n dvd p |] ==> m dvd (p::nat)"
    apply (unfold dvd_def)
    apply (blast intro: mult_assoc)
    done

    lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
    apply (unfold dvd_def)
    apply (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
    done

    lemma dvd_add: "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)"
    apply (unfold dvd_def)
    apply (blast intro: add_mult_distrib2 [symmetric])
    done

    lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
    apply (unfold dvd_def)
    apply (blast intro: diff_mult_distrib2 [symmetric])
    done

    lemma dvd_diffD: "[| k dvd m-n; k dvd n; n≤m |] ==> k dvd (m::nat)"
    apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
    apply (blast intro: dvd_add)
    done

    lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n≤m |] ==> k dvd (n::nat)"
    by (drule_tac m = m in dvd_diff, auto)

    lemma dvd_mult: "k dvd n ==> k dvd (m*n :: nat)"
    apply (unfold dvd_def)
    apply (blast intro: mult_left_commute)
    done

    lemma dvd_mult2: "k dvd m ==> k dvd (m*n :: nat)"
    apply (subst mult_commute)
    apply (erule dvd_mult)
    done

    lemma dvd_triv_right [iff]: "k dvd (m*k :: nat)"
    by (rule dvd_refl [THEN dvd_mult])

    lemma dvd_triv_left [iff]: "k dvd (k*m :: nat)"
    by (rule dvd_refl [THEN dvd_mult2])

    lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
    apply (rule iffI)
    apply (erule_tac [2] dvd_add)
    apply (rule_tac [2] dvd_refl)
    apply (subgoal_tac "n = (n+k) -k")
     prefer 2 apply simp
    apply (erule ssubst)
    apply (erule dvd_diff)
    apply (rule dvd_refl)
    done

    lemma dvd_mod: "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n"
    apply (unfold dvd_def)
    apply (case_tac "n=0", auto)
    apply (blast intro: mod_mult_distrib2 [symmetric])
    done

    lemma dvd_mod_imp_dvd: "[| (k::nat) dvd m mod n;  k dvd n |] ==> k dvd m"
    apply (subgoal_tac "k dvd (m div n) *n + m mod n")
     apply (simp add: mod_div_equality)
    apply (simp only: dvd_add dvd_mult)
    done

    lemma dvd_mod_iff: "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)"
    by (blast intro: dvd_mod_imp_dvd dvd_mod)

    lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
    apply (unfold dvd_def)
    apply (erule exE)
    apply (simp add: mult_ac)
    done

    lemma dvd_mult_cancel1: "0<m ==> (m*n dvd m) = (n = (1::nat))"
    apply auto
    apply (subgoal_tac "m*n dvd m*1")
    apply (drule dvd_mult_cancel, auto)
    done

    lemma dvd_mult_cancel2: "0<m ==> (n*m dvd m) = (n = (1::nat))"
    apply (subst mult_commute)
    apply (erule dvd_mult_cancel1)
    done

    lemma mult_dvd_mono: "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)"
    apply (unfold dvd_def, clarify)
    apply (rule_tac x = "k*ka" in exI)
    apply (simp add: mult_ac)
    done

    lemma dvd_mult_left: "(i*j :: nat) dvd k ==> i dvd k"
    by (simp add: dvd_def mult_assoc, blast)

    lemma dvd_mult_right: "(i*j :: nat) dvd k ==> j dvd k"
    apply (unfold dvd_def, clarify)
    apply (rule_tac x = "i*k" in exI)
    apply (simp add: mult_ac)
    done

    lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k ≤ (n::nat)"
    apply (unfold dvd_def, clarify)
    apply (simp_all (no_asm_use) add: zero_less_mult_iff)
    apply (erule conjE)
    apply (rule le_trans)
    apply (rule_tac [2] le_refl [THEN mult_le_mono])
    apply (erule_tac [2] Suc_leI, simp)
    done

    lemma dvd_eq_mod_eq_0: "!!k::nat. (k dvd n) = (n mod k = 0)"
    apply (unfold dvd_def)
    apply (case_tac "k=0", simp, safe)
    apply (simp add: mult_commute)
    apply (rule_tac t = n and n1 = k in mod_div_equality [THEN subst])
    apply (subst mult_commute, simp)
    done

    lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
    apply (subgoal_tac "m mod n = 0")
     apply (simp add: mult_div_cancel)
    apply (simp only: dvd_eq_mod_eq_0)
    done

    lemma mod_eq_0_iff: "(m mod d = 0) = (∃q::nat. m = d*q)"
    by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)

    lemmas mod_eq_0D = mod_eq_0_iff [THEN iffD1]
    declare mod_eq_0D [dest!]

    (*Loses information, namely we also have r<d provided d is nonzero*)
    lemma mod_eqD: "(m mod d = r) ==> ∃q::nat. m = r + q*d"
    apply (cut_tac m = m in mod_div_equality)
    apply (simp only: add_ac)
    apply (blast intro: sym)
    done

    lemma split_div:
     "P(n div k :: nat) =
     ((k = 0 --> P 0) ∧ (k ≠ 0 --> (!i. !j<k. n = k*i + j --> P i)))"
     (is "?P = ?Q" is "_ = (_ ∧ (_ --> ?R))")
    proof
      assume P: ?P
      show ?Q
      proof (cases)
        assume "k = 0"
        with P show ?Q by(simp add:DIVISION_BY_ZERO_DIV)
      next
        assume not0: "k ≠ 0"
        thus ?Q
        proof (simp, intro allI impI)
          fix i j
          assume n: "n = k*i + j" and j: "j < k"
          show "P i"
          proof (cases)
            assume "i = 0"
            with n j P show "P i" by simp
          next
            assume "i ≠ 0"
            with not0 n j P show "P i" by(simp add:add_ac)
          qed
        qed
      qed
    next
      assume Q: ?Q
      show ?P
      proof (cases)
        assume "k = 0"
        with Q show ?P by(simp add:DIVISION_BY_ZERO_DIV)
      next
        assume not0: "k ≠ 0"
        with Q have R: ?R by simp
        from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
        show ?P by simp
      qed
    qed

    lemma split_div_lemma:
      "0 < n ==> (n * q ≤ m ∧ m < n * (Suc q)) = (q = ((m::nat) div n))"
      apply (rule iffI)
      apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
    prefer 3; apply assumption
      apply (simp_all add: quorem_def)
      apply arith
      apply (rule conjI)
      apply (rule_tac P="%x. n * (m div n) ≤ x" in
        subst [OF mod_div_equality [of _ n]])
      apply (simp only: add: mult_ac)
      apply (rule_tac P="%x. x < n + n * (m div n)" in
        subst [OF mod_div_equality [of _ n]])
      apply (simp only: add: mult_ac add_ac)
      apply (rule add_less_mono1, simp)
      done

    theorem split_div':
      "P ((m::nat) div n) = ((n = 0 ∧ P 0) ∨
       (∃q. (n * q ≤ m ∧ m < n * (Suc q)) ∧ P q))"
      apply (case_tac "0 < n")
      apply (simp only: add: split_div_lemma)
      apply (simp_all add: DIVISION_BY_ZERO_DIV)
      done

    lemma split_mod:
     "P(n mod k :: nat) =
     ((k = 0 --> P n) ∧ (k ≠ 0 --> (!i. !j<k. n = k*i + j --> P j)))"
     (is "?P = ?Q" is "_ = (_ ∧ (_ --> ?R))")
    proof
      assume P: ?P
      show ?Q
      proof (cases)
        assume "k = 0"
        with P show ?Q by(simp add:DIVISION_BY_ZERO_MOD)
      next
        assume not0: "k ≠ 0"
        thus ?Q
        proof (simp, intro allI impI)
          fix i j
          assume "n = k*i + j" "j < k"
          thus "P j" using not0 P by(simp add:add_ac mult_ac)
        qed
      qed
    next
      assume Q: ?Q
      show ?P
      proof (cases)
        assume "k = 0"
        with Q show ?P by(simp add:DIVISION_BY_ZERO_MOD)
      next
        assume not0: "k ≠ 0"
        with Q have R: ?R by simp
        from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
        show ?P by simp
      qed
    qed

    theorem mod_div_equality': "(m::nat) mod n = m - (m div n) * n"
      apply (rule_tac P="%x. m mod n = x - (m div n) * n" in
        subst [OF mod_div_equality [of _ n]])
      apply arith
      done

    subsection {*An ``induction'' law for modulus arithmetic.*}

    lemma mod_induct_0:
      assumes step: "∀i<p. P i --> P ((Suc i) mod p)"
      and base: "P i" and i: "i<p"
      shows "P 0"
    proof (rule ccontr)
      assume contra: "¬(P 0)"
      from i have p: "0<p" by simp
      have "∀k. 0<k --> ¬ P (p-k)" (is "∀k. ?A k")
      proof
        fix k
        show "?A k"
        proof (induct k)
          show "?A 0" by simp  -- "by contradiction"
        next
          fix n
          assume ih: "?A n"
          show "?A (Suc n)"
          proof (clarsimp)
            assume y: "P (p - Suc n)"
            have n: "Suc n < p"
            proof (rule ccontr)
              assume "¬(Suc n < p)"
              hence "p - Suc n = 0"
                by simp
              with y contra show "False"
                by simp
            qed
            hence n2: "Suc (p - Suc n) = p-n" by arith
            from p have "p - Suc n < p" by arith
            with y step have z: "P ((Suc (p - Suc n)) mod p)"
              by blast
            show "False"
            proof (cases "n=0")
              case True
              with z n2 contra show ?thesis by simp
            next
              case False
              with p have "p-n < p" by arith
              with z n2 False ih show ?thesis by simp
            qed
          qed
        qed
      qed
      moreover
      from i obtain k where "0<k ∧ i+k=p"
        by (blast dest: less_imp_add_positive)
      hence "0<k ∧ i=p-k" by auto
      moreover
      note base
      ultimately
      show "False" by blast
    qed

    lemma mod_induct:
      assumes step: "∀i<p. P i --> P ((Suc i) mod p)"
      and base: "P i" and i: "i<p" and j: "j<p"
      shows "P j"
    proof -
      have "∀j<p. P j"
      proof
        fix j
        show "j<p --> P j" (is "?A j")
        proof (induct j)
          from step base i show "?A 0"
            by (auto elim: mod_induct_0)
        next
          fix k
          assume ih: "?A k"
          show "?A (Suc k)"
          proof
            assume suc: "Suc k < p"
            hence k: "k<p" by simp
            with ih have "P k" ..
            with step k have "P (Suc k mod p)"
              by blast
            moreover
            from suc have "Suc k mod p = Suc k"
              by simp
            ultimately
            show "P (Suc k)" by simp
          qed
        qed
      qed
      with j show ?thesis by blast
    qed

    ML
    {*
    val div_def = thm "div_def"
    val mod_def = thm "mod_def"
    val dvd_def = thm "dvd_def"
    val quorem_def = thm "quorem_def"

    val wf_less_trans = thm "wf_less_trans";
    val mod_eq = thm "mod_eq";
    val div_eq = thm "div_eq";
    val DIVISION_BY_ZERO_DIV = thm "DIVISION_BY_ZERO_DIV";
    val DIVISION_BY_ZERO_MOD = thm "DIVISION_BY_ZERO_MOD";
    val mod_less = thm "mod_less";
    val mod_geq = thm "mod_geq";
    val le_mod_geq = thm "le_mod_geq";
    val mod_if = thm "mod_if";
    val mod_1 = thm "mod_1";
    val mod_self = thm "mod_self";
    val mod_add_self2 = thm "mod_add_self2";
    val mod_add_self1 = thm "mod_add_self1";
    val mod_mult_self1 = thm "mod_mult_self1";
    val mod_mult_self2 = thm "mod_mult_self2";
    val mod_mult_distrib = thm "mod_mult_distrib";
    val mod_mult_distrib2 = thm "mod_mult_distrib2";
    val mod_mult_self_is_0 = thm "mod_mult_self_is_0";
    val mod_mult_self1_is_0 = thm "mod_mult_self1_is_0";
    val div_less = thm "div_less";
    val div_geq = thm "div_geq";
    val le_div_geq = thm "le_div_geq";
    val div_if = thm "div_if";
    val mod_div_equality = thm "mod_div_equality";
    val mod_div_equality2 = thm "mod_div_equality2";
    val div_mod_equality = thm "div_mod_equality";
    val div_mod_equality2 = thm "div_mod_equality2";
    val mult_div_cancel = thm "mult_div_cancel";
    val mod_less_divisor = thm "mod_less_divisor";
    val div_mult_self_is_m = thm "div_mult_self_is_m";
    val div_mult_self1_is_m = thm "div_mult_self1_is_m";
    val unique_quotient_lemma = thm "unique_quotient_lemma";
    val unique_quotient = thm "unique_quotient";
    val unique_remainder = thm "unique_remainder";
    val div_0 = thm "div_0";
    val mod_0 = thm "mod_0";
    val div_mult1_eq = thm "div_mult1_eq";
    val mod_mult1_eq = thm "mod_mult1_eq";
    val mod_mult1_eq' = thm "mod_mult1_eq'";
    val mod_mult_distrib_mod = thm "mod_mult_distrib_mod";
    val div_add1_eq = thm "div_add1_eq";
    val mod_add1_eq = thm "mod_add1_eq";
    val mod_lemma = thm "mod_lemma";
    val div_mult2_eq = thm "div_mult2_eq";
    val mod_mult2_eq = thm "mod_mult2_eq";
    val div_mult_mult_lemma = thm "div_mult_mult_lemma";
    val div_mult_mult1 = thm "div_mult_mult1";
    val div_mult_mult2 = thm "div_mult_mult2";
    val div_1 = thm "div_1";
    val div_self = thm "div_self";
    val div_add_self2 = thm "div_add_self2";
    val div_add_self1 = thm "div_add_self1";
    val div_mult_self1 = thm "div_mult_self1";
    val div_mult_self2 = thm "div_mult_self2";
    val div_le_mono = thm "div_le_mono";
    val div_le_mono2 = thm "div_le_mono2";
    val div_le_dividend = thm "div_le_dividend";
    val div_less_dividend = thm "div_less_dividend";
    val mod_Suc = thm "mod_Suc";
    val dvdI = thm "dvdI";
    val dvdE = thm "dvdE";
    val dvd_0_right = thm "dvd_0_right";
    val dvd_0_left = thm "dvd_0_left";
    val dvd_0_left_iff = thm "dvd_0_left_iff";
    val dvd_1_left = thm "dvd_1_left";
    val dvd_1_iff_1 = thm "dvd_1_iff_1";
    val dvd_refl = thm "dvd_refl";
    val dvd_trans = thm "dvd_trans";
    val dvd_anti_sym = thm "dvd_anti_sym";
    val dvd_add = thm "dvd_add";
    val dvd_diff = thm "dvd_diff";
    val dvd_diffD = thm "dvd_diffD";
    val dvd_diffD1 = thm "dvd_diffD1";
    val dvd_mult = thm "dvd_mult";
    val dvd_mult2 = thm "dvd_mult2";
    val dvd_reduce = thm "dvd_reduce";
    val dvd_mod = thm "dvd_mod";
    val dvd_mod_imp_dvd = thm "dvd_mod_imp_dvd";
    val dvd_mod_iff = thm "dvd_mod_iff";
    val dvd_mult_cancel = thm "dvd_mult_cancel";
    val dvd_mult_cancel1 = thm "dvd_mult_cancel1";
    val dvd_mult_cancel2 = thm "dvd_mult_cancel2";
    val mult_dvd_mono = thm "mult_dvd_mono";
    val dvd_mult_left = thm "dvd_mult_left";
    val dvd_mult_right = thm "dvd_mult_right";
    val dvd_imp_le = thm "dvd_imp_le";
    val dvd_eq_mod_eq_0 = thm "dvd_eq_mod_eq_0";
    val dvd_mult_div_cancel = thm "dvd_mult_div_cancel";
    val mod_eq_0_iff = thm "mod_eq_0_iff";
    val mod_eqD = thm "mod_eqD";
    *}

    (*
    lemma split_div:
    assumes m: "m ≠ 0"
    shows "P(n div m :: nat) = (!i. !j<m. n = m*i + j --> P i)"
           (is "?P = ?Q")
    proof
      assume P: ?P
      show ?Q
      proof (intro allI impI)
        fix i j
        assume n: "n = m*i + j" and j: "j < m"
        show "P i"
        proof (cases)
          assume "i = 0"
          with n j P show "P i" by simp
        next
          assume "i ≠ 0"
          with n j P show "P i" by (simp add:add_ac div_mult_self1)
        qed
      qed
    next
      assume Q: ?Q
      from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
      show ?P by simp
    qed

    lemma split_mod:
    assumes m: "m ≠ 0"
    shows "P(n mod m :: nat) = (!i. !j<m. n = m*i + j --> P j)"
           (is "?P = ?Q")
    proof
      assume P: ?P
      show ?Q
      proof (intro allI impI)
        fix i j
        assume "n = m*i + j" "j < m"
        thus "P j" using m P by(simp add:add_ac mult_ac)
      qed
    next
      assume Q: ?Q
      from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
      show ?P by simp
    qed
    *)
    end

### Initial Lemmas

lemmas wf_less_trans:

      [| f = wfrec (pred_nat+) H; H (cut f (pred_nat+) a) a = t |] ==> f a = t

lemmas wf_less_trans:

      [| f = wfrec (pred_nat+) H; H (cut f (pred_nat+) a) a = t |] ==> f a = t

lemma mod_eq:

      (%m. m mod n) = wfrec (pred_nat+) (%f j. if j < n ∨ n = 0 then j else f (j - n))

lemma div_eq:

      (%m. m div n) =
      wfrec (pred_nat+) (%f j. if j < n ∨ n = 0 then 0 else Suc (f (j - n)))

lemma DIVISION_BY_ZERO_DIV:

      a div 0 = 0

lemma DIVISION_BY_ZERO_MOD:

      a mod 0 = a

### Remainder

lemma mod_less:

      m < n ==> m mod n = m

lemma mod_geq:

      ¬ m < n ==> m mod n = (m - n) mod n

lemma le_mod_geq:

      n ≤ m ==> m mod n = (m - n) mod n

lemma mod_if:

      m mod n = (if m < n then m else (m - n) mod n)

lemma mod_1:

      m mod Suc 0 = 0

lemma mod_self:

      n mod n = 0

lemma mod_add_self2:

      (m + n) mod n = m mod n

lemma mod_add_self1:

      (n + m) mod n = m mod n

lemma mod_mult_self1:

      (m + k * n) mod n = m mod n

lemma mod_mult_self2:

      (m + n * k) mod n = m mod n

lemma mod_mult_distrib:

      m mod n * k = m * k mod (n * k)

lemma mod_mult_distrib2:

      k * (m mod n) = k * m mod (k * n)

lemma mod_mult_self_is_0:

      m * n mod n = 0

lemma mod_mult_self1_is_0:

      n * m mod n = 0

### Quotient

lemma div_less:

      m < n ==> m div n = 0

lemma div_geq:

      [| 0 < n; ¬ m < n |] ==> m div n = Suc ((m - n) div n)

lemma le_div_geq:

      [| 0 < n; n ≤ m |] ==> m div n = Suc ((m - n) div n)

lemma div_if:

      0 < n ==> m div n = (if m < n then 0 else Suc ((m - n) div n))

lemma mod_div_equality:

      m div n * n + m mod n = m

lemma mod_div_equality2:

      n * (m div n) + m mod n = m

### Simproc for Cancelling Div and Mod

lemma div_mod_equality:

      m div n * n + m mod n + k = m + k

lemma div_mod_equality2:

      n * (m div n) + m mod n + k = m + k

lemma mult_div_cancel:

      n * (m div n) = m - m mod n

lemma mod_less_divisor:

      0 < n ==> m mod n < n

lemma mod_le_divisor:

      0 < n ==> m mod n ≤ n

lemma div_mult_self_is_m:

      0 < n ==> m * n div n = m

lemma div_mult_self1_is_m:

      0 < n ==> n * m div n = m

### Proving facts about Quotient and Remainder

lemma unique_quotient_lemma:

      [| b * q' + r' ≤ b * q + r; x < b; r < b |] ==> q' ≤ q

lemma unique_quotient:

      [| quorem ((a, b), q, r); quorem ((a, b), q', r'); 0 < b |] ==> q = q'

lemma unique_remainder:

      [| quorem ((a, b), q, r); quorem ((a, b), q', r'); 0 < b |] ==> r = r'

lemma quorem_div_mod:

      0 < b ==> quorem ((a, b), a div b, a mod b)

lemma quorem_div:

      [| quorem ((a, b), q, r); 0 < b |] ==> a div b = q

lemma quorem_mod:

      [| quorem ((a, b), q, r); 0 < b |] ==> a mod b = r

lemma div_0:

      0 div m = 0

lemma mod_0:

      0 mod m = 0

lemma quorem_mult1_eq:

      [| quorem ((b, c), q, r); 0 < c |]
      ==> quorem ((a * b, c), a * q + a * r div c, a * r mod c)

lemma div_mult1_eq:

      a * b div c = a * (b div c) + a * (b mod c) div c

lemma mod_mult1_eq:

      a * b mod c = a * (b mod c) mod c

lemma mod_mult1_eq':

      a * b mod c = a mod c * b mod c

lemma mod_mult_distrib_mod:

      a * b mod c = a mod c * (b mod c) mod c

lemma quorem_add1_eq:

      [| quorem ((a, c), aq, ar); quorem ((b, c), bq, br); 0 < c |]
      ==> quorem ((a + b, c), aq + bq + (ar + br) div c, (ar + br) mod c)

lemma div_add1_eq:

      (a + b) div c = a div c + b div c + (a mod c + b mod c) div c

lemma mod_add1_eq:

      (a + b) mod c = (a mod c + b mod c) mod c

### Proving @{term "a div (b*c) = (a div b) div c"}

lemma mod_lemma:

      [| 0 < c; r < b |] ==> b * (q mod c) + r < b * c

lemma quorem_mult2_eq:

      [| quorem ((a, b), q, r); 0 < b; 0 < c |]
      ==> quorem ((a, b * c), q div c, b * (q mod c) + r)

lemma div_mult2_eq:

      a div (b * c) = a div b div c

lemma mod_mult2_eq:

      a mod (b * c) = b * (a div b mod c) + a mod b

### Cancellation of Common Factors in Division

lemma div_mult_mult_lemma:

      [| 0 < b; 0 < c |] ==> c * a div (c * b) = a div b

lemma div_mult_mult1:

      0 < c ==> c * a div (c * b) = a div b

lemma div_mult_mult2:

      0 < c ==> a * c div (b * c) = a div b

### Further Facts about Quotient and Remainder

lemma div_1:

      m div Suc 0 = m

lemma div_self:

      0 < n ==> n div n = 1

lemma div_add_self2:

      0 < n ==> (m + n) div n = Suc (m div n)

lemma div_add_self1:

      0 < n ==> (n + m) div n = Suc (m div n)

lemma div_mult_self1:

      0 < n ==> (m + k * n) div n = k + m div n

lemma div_mult_self2:

      0 < n ==> (m + n * k) div n = k + m div n

lemma div_le_mono:

      m ≤ n ==> m div k ≤ n div k

lemma div_le_mono2:

      [| 0 < m; m ≤ n |] ==> k div n ≤ k div m

lemma div_le_dividend:

      m div n ≤ m

lemma div_less_dividend:

      [| 1 < n; 0 < m |] ==> m div n < m

lemma mod_Suc:

      Suc m mod n = (if Suc (m mod n) = n then 0 else Suc (m mod n))

lemma nat_mod_div_trivial:

      m mod n div n = 0

lemma nat_mod_mod_trivial:

      m mod n mod n = m mod n

### The Divides Relation

lemma dvdI:

      n = m * k ==> m dvd n

lemma dvdE:

      [| m dvd n; !!k. n = m * k ==> P |] ==> P

lemma dvd_0_right:

      m dvd 0

lemma dvd_0_left:

      0 dvd m ==> m = 0

lemma dvd_0_left_iff:

      (0 dvd m) = (m = 0)

lemma dvd_1_left:

      Suc 0 dvd k

lemma dvd_1_iff_1:

      (m dvd Suc 0) = (m = Suc 0)

lemma dvd_refl:

      m dvd m

lemma dvd_trans:

      [| m dvd n; n dvd p |] ==> m dvd p

lemma dvd_anti_sym:

      [| m dvd n; n dvd m |] ==> m = n

lemma dvd_add:

      [| k dvd m; k dvd n |] ==> k dvd m + n

lemma dvd_diff:

      [| k dvd m; k dvd n |] ==> k dvd m - n

lemma dvd_diffD:

      [| k dvd m - n; k dvd n; n ≤ m |] ==> k dvd m

lemma dvd_diffD1:

      [| k dvd m - n; k dvd m; n ≤ m |] ==> k dvd n

lemma dvd_mult:

      k dvd n ==> k dvd m * n

lemma dvd_mult2:

      k dvd m ==> k dvd m * n

lemma dvd_triv_right:

      k dvd m * k

lemma dvd_triv_left:

      k dvd k * m

lemma dvd_reduce:

      (k dvd n + k) = (k dvd n)

lemma dvd_mod:

      [| f dvd m; f dvd n |] ==> f dvd m mod n

lemma dvd_mod_imp_dvd:

      [| k dvd m mod n; k dvd n |] ==> k dvd m

lemma dvd_mod_iff:

      k dvd n ==> (k dvd m mod n) = (k dvd m)

lemma dvd_mult_cancel:

      [| k * m dvd k * n; 0 < k |] ==> m dvd n

lemma dvd_mult_cancel1:

      0 < m ==> (m * n dvd m) = (n = 1)

lemma dvd_mult_cancel2:

      0 < m ==> (n * m dvd m) = (n = 1)

lemma mult_dvd_mono:

      [| i dvd m; j dvd n |] ==> i * j dvd m * n

lemma dvd_mult_left:

      i * j dvd k ==> i dvd k

lemma dvd_mult_right:

      i * j dvd k ==> j dvd k

lemma dvd_imp_le:

      [| k dvd n; 0 < n |] ==> k ≤ n

lemma dvd_eq_mod_eq_0:

      (k dvd n) = (n mod k = 0)

lemma dvd_mult_div_cancel:

      n dvd m ==> n * (m div n) = m

lemma mod_eq_0_iff:

      (m mod d = 0) = (∃q. m = d * q)

lemmas mod_eq_0D:

      m1 mod d1 = 0 ==> ∃q. m1 = d1 * q

lemmas mod_eq_0D:

      m1 mod d1 = 0 ==> ∃q. m1 = d1 * q

lemma mod_eqD:

      m mod d = r ==> ∃q. m = r + q * d

lemma split_div:

      P (n div k) =
      ((k = 0 --> P 0) ∧ (k ≠ 0 --> (∀i j. j < k --> n = k * i + j --> P i)))

lemma split_div_lemma:

      0 < n ==> (n * q ≤ m ∧ m < n * Suc q) = (q = m div n)

theorem split_div':

      P (m div n) = (n = 0 ∧ P 0 ∨ (∃q. (n * q ≤ m ∧ m < n * Suc q) ∧ P q))

lemma split_mod:

      P (n mod k) =
      ((k = 0 --> P n) ∧ (k ≠ 0 --> (∀i j. j < k --> n = k * i + j --> P j)))

theorem mod_div_equality':

      m mod n = m - m div n * n

### An ``induction'' law for modulus arithmetic.

lemma mod_induct_0:

      [| ∀i<p. P i --> P (Suc i mod p); P i; i < p |] ==> P 0

lemma mod_induct:

      [| ∀i<p. P i --> P (Suc i mod p); P i; i < p; j < p |] ==> P j