src/HOL/Divides.thy
 author haftmann Thu Apr 26 13:33:04 2007 +0200 (2007-04-26) changeset 22800 eaf5e7ef35d9 parent 22744 5cbe966d67a2 child 22845 5f9138bcb3d7 permissions -rw-r--r--
```     1 (*  Title:      HOL/Divides.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1999  University of Cambridge
```
```     5 *)
```
```     6
```
```     7 header {* The division operators div, mod and the divides relation "dvd" *}
```
```     8
```
```     9 theory Divides
```
```    10 imports Datatype Power
```
```    11 begin
```
```    12
```
```    13 (*We use the same class for div and mod;
```
```    14   moreover, dvd is defined whenever multiplication is*)
```
```    15 class div = type +
```
```    16   fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
```
```    17   fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
```
```    18 begin
```
```    19
```
```    20 notation
```
```    21   div (infixl "\<^loc>div" 70)
```
```    22
```
```    23 notation
```
```    24   mod (infixl "\<^loc>mod" 70)
```
```    25
```
```    26 end
```
```    27
```
```    28 notation
```
```    29   div (infixl "div" 70)
```
```    30
```
```    31 notation
```
```    32   mod (infixl "mod" 70)
```
```    33
```
```    34 instance nat :: "Divides.div"
```
```    35   mod_def: "m mod n == wfrec (pred_nat^+)
```
```    36                           (%f j. if j<n | n=0 then j else f (j-n)) m"
```
```    37   div_def:   "m div n == wfrec (pred_nat^+)
```
```    38                           (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m" ..
```
```    39
```
```    40 definition
```
```    41   (*The definition of dvd is polymorphic!*)
```
```    42   dvd  :: "'a::times \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where
```
```    43   dvd_def: "m dvd n \<longleftrightarrow> (\<exists>k. n = m*k)"
```
```    44
```
```    45 definition
```
```    46   quorem :: "(nat*nat) * (nat*nat) => bool" where
```
```    47   (*This definition helps prove the harder properties of div and mod.
```
```    48     It is copied from IntDiv.thy; should it be overloaded?*)
```
```    49   "quorem = (%((a,b), (q,r)).
```
```    50                     a = b*q + r &
```
```    51                     (if 0<b then 0\<le>r & r<b else b<r & r \<le>0))"
```
```    52
```
```    53
```
```    54
```
```    55 subsection{*Initial Lemmas*}
```
```    56
```
```    57 lemmas wf_less_trans =
```
```    58        def_wfrec [THEN trans, OF eq_reflection wf_pred_nat [THEN wf_trancl],
```
```    59                   standard]
```
```    60
```
```    61 lemma mod_eq: "(%m. m mod n) =
```
```    62               wfrec (pred_nat^+) (%f j. if j<n | n=0 then j else f (j-n))"
```
```    63 by (simp add: mod_def)
```
```    64
```
```    65 lemma div_eq: "(%m. m div n) = wfrec (pred_nat^+)
```
```    66                (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))"
```
```    67 by (simp add: div_def)
```
```    68
```
```    69
```
```    70 (** Aribtrary definitions for division by zero.  Useful to simplify
```
```    71     certain equations **)
```
```    72
```
```    73 lemma DIVISION_BY_ZERO_DIV [simp]: "a div 0 = (0::nat)"
```
```    74   by (rule div_eq [THEN wf_less_trans], simp)
```
```    75
```
```    76 lemma DIVISION_BY_ZERO_MOD [simp]: "a mod 0 = (a::nat)"
```
```    77   by (rule mod_eq [THEN wf_less_trans], simp)
```
```    78
```
```    79
```
```    80 subsection{*Remainder*}
```
```    81
```
```    82 lemma mod_less [simp]: "m<n ==> m mod n = (m::nat)"
```
```    83   by (rule mod_eq [THEN wf_less_trans]) simp
```
```    84
```
```    85 lemma mod_geq: "~ m < (n::nat) ==> m mod n = (m-n) mod n"
```
```    86   apply (cases "n=0")
```
```    87    apply simp
```
```    88   apply (rule mod_eq [THEN wf_less_trans])
```
```    89   apply (simp add: cut_apply less_eq)
```
```    90   done
```
```    91
```
```    92 (*Avoids the ugly ~m<n above*)
```
```    93 lemma le_mod_geq: "(n::nat) \<le> m ==> m mod n = (m-n) mod n"
```
```    94   by (simp add: mod_geq linorder_not_less)
```
```    95
```
```    96 lemma mod_if: "m mod (n::nat) = (if m<n then m else (m-n) mod n)"
```
```    97   by (simp add: mod_geq)
```
```    98
```
```    99 lemma mod_1 [simp]: "m mod Suc 0 = 0"
```
```   100   by (induct m) (simp_all add: mod_geq)
```
```   101
```
```   102 lemma mod_self [simp]: "n mod n = (0::nat)"
```
```   103   by (cases "n = 0") (simp_all add: mod_geq)
```
```   104
```
```   105 lemma mod_add_self2 [simp]: "(m+n) mod n = m mod (n::nat)"
```
```   106   apply (subgoal_tac "(n + m) mod n = (n+m-n) mod n")
```
```   107    apply (simp add: add_commute)
```
```   108   apply (subst mod_geq [symmetric], simp_all)
```
```   109   done
```
```   110
```
```   111 lemma mod_add_self1 [simp]: "(n+m) mod n = m mod (n::nat)"
```
```   112   by (simp add: add_commute mod_add_self2)
```
```   113
```
```   114 lemma mod_mult_self1 [simp]: "(m + k*n) mod n = m mod (n::nat)"
```
```   115   by (induct k) (simp_all add: add_left_commute [of _ n])
```
```   116
```
```   117 lemma mod_mult_self2 [simp]: "(m + n*k) mod n = m mod (n::nat)"
```
```   118   by (simp add: mult_commute mod_mult_self1)
```
```   119
```
```   120 lemma mod_mult_distrib: "(m mod n) * (k::nat) = (m*k) mod (n*k)"
```
```   121   apply (cases "n = 0", simp)
```
```   122   apply (cases "k = 0", simp)
```
```   123   apply (induct m rule: nat_less_induct)
```
```   124   apply (subst mod_if, simp)
```
```   125   apply (simp add: mod_geq diff_mult_distrib)
```
```   126   done
```
```   127
```
```   128 lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"
```
```   129   by (simp add: mult_commute [of k] mod_mult_distrib)
```
```   130
```
```   131 lemma mod_mult_self_is_0 [simp]: "(m*n) mod n = (0::nat)"
```
```   132   apply (cases "n = 0", simp)
```
```   133   apply (induct m, simp)
```
```   134   apply (rename_tac k)
```
```   135   apply (cut_tac m = "k * n" and n = n in mod_add_self2)
```
```   136   apply (simp add: add_commute)
```
```   137   done
```
```   138
```
```   139 lemma mod_mult_self1_is_0 [simp]: "(n*m) mod n = (0::nat)"
```
```   140   by (simp add: mult_commute mod_mult_self_is_0)
```
```   141
```
```   142
```
```   143 subsection{*Quotient*}
```
```   144
```
```   145 lemma div_less [simp]: "m<n ==> m div n = (0::nat)"
```
```   146   by (rule div_eq [THEN wf_less_trans], simp)
```
```   147
```
```   148 lemma div_geq: "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)"
```
```   149   apply (rule div_eq [THEN wf_less_trans])
```
```   150   apply (simp add: cut_apply less_eq)
```
```   151   done
```
```   152
```
```   153 (*Avoids the ugly ~m<n above*)
```
```   154 lemma le_div_geq: "[| 0<n;  n\<le>m |] ==> m div n = Suc((m-n) div n)"
```
```   155   by (simp add: div_geq linorder_not_less)
```
```   156
```
```   157 lemma div_if: "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"
```
```   158   by (simp add: div_geq)
```
```   159
```
```   160
```
```   161 (*Main Result about quotient and remainder.*)
```
```   162 lemma mod_div_equality: "(m div n)*n + m mod n = (m::nat)"
```
```   163   apply (cases "n = 0", simp)
```
```   164   apply (induct m rule: nat_less_induct)
```
```   165   apply (subst mod_if)
```
```   166   apply (simp_all add: add_assoc div_geq add_diff_inverse)
```
```   167   done
```
```   168
```
```   169 lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
```
```   170   apply (cut_tac m = m and n = n in mod_div_equality)
```
```   171   apply (simp add: mult_commute)
```
```   172   done
```
```   173
```
```   174 subsection{*Simproc for Cancelling Div and Mod*}
```
```   175
```
```   176 lemma div_mod_equality: "((m div n)*n + m mod n) + k = (m::nat) + k"
```
```   177   by (simp add: mod_div_equality)
```
```   178
```
```   179 lemma div_mod_equality2: "(n*(m div n) + m mod n) + k = (m::nat) + k"
```
```   180   by (simp add: mod_div_equality2)
```
```   181
```
```   182 ML
```
```   183 {*
```
```   184 structure CancelDivModData =
```
```   185 struct
```
```   186
```
```   187 val div_name = @{const_name Divides.div};
```
```   188 val mod_name = @{const_name Divides.mod};
```
```   189 val mk_binop = HOLogic.mk_binop;
```
```   190 val mk_sum = NatArithUtils.mk_sum;
```
```   191 val dest_sum = NatArithUtils.dest_sum;
```
```   192
```
```   193 (*logic*)
```
```   194
```
```   195 val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}]
```
```   196
```
```   197 val trans = trans
```
```   198
```
```   199 val prove_eq_sums =
```
```   200   let val simps = @{thm add_0} :: @{thm add_0_right} :: @{thms add_ac}
```
```   201   in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
```
```   202
```
```   203 end;
```
```   204
```
```   205 structure CancelDivMod = CancelDivModFun(CancelDivModData);
```
```   206
```
```   207 val cancel_div_mod_proc = NatArithUtils.prep_simproc
```
```   208       ("cancel_div_mod", ["(m::nat) + n"], K CancelDivMod.proc);
```
```   209
```
```   210 Addsimprocs[cancel_div_mod_proc];
```
```   211 *}
```
```   212
```
```   213
```
```   214 (* a simple rearrangement of mod_div_equality: *)
```
```   215 lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
```
```   216   by (cut_tac m = m and n = n in mod_div_equality2, arith)
```
```   217
```
```   218 lemma mod_less_divisor [simp]: "0<n ==> m mod n < (n::nat)"
```
```   219   apply (induct m rule: nat_less_induct)
```
```   220   apply (rename_tac m)
```
```   221   apply (case_tac "m<n", simp)
```
```   222   txt{*case @{term "n \<le> m"}*}
```
```   223   apply (simp add: mod_geq)
```
```   224   done
```
```   225
```
```   226 lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
```
```   227   apply (drule mod_less_divisor [where m = m])
```
```   228   apply simp
```
```   229   done
```
```   230
```
```   231 lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
```
```   232   by (cut_tac m = "m*n" and n = n in mod_div_equality, auto)
```
```   233
```
```   234 lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
```
```   235   by (simp add: mult_commute div_mult_self_is_m)
```
```   236
```
```   237 (*mod_mult_distrib2 above is the counterpart for remainder*)
```
```   238
```
```   239
```
```   240 subsection{*Proving facts about Quotient and Remainder*}
```
```   241
```
```   242 lemma unique_quotient_lemma:
```
```   243      "[| b*q' + r'  \<le> b*q + r;  x < b;  r < b |]
```
```   244       ==> q' \<le> (q::nat)"
```
```   245   apply (rule leI)
```
```   246   apply (subst less_iff_Suc_add)
```
```   247   apply (auto simp add: add_mult_distrib2)
```
```   248   done
```
```   249
```
```   250 lemma unique_quotient:
```
```   251      "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]
```
```   252       ==> q = q'"
```
```   253   apply (simp add: split_ifs quorem_def)
```
```   254   apply (blast intro: order_antisym
```
```   255     dest: order_eq_refl [THEN unique_quotient_lemma] sym)
```
```   256   done
```
```   257
```
```   258 lemma unique_remainder:
```
```   259      "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]
```
```   260       ==> r = r'"
```
```   261   apply (subgoal_tac "q = q'")
```
```   262    prefer 2 apply (blast intro: unique_quotient)
```
```   263   apply (simp add: quorem_def)
```
```   264   done
```
```   265
```
```   266 lemma quorem_div_mod: "0 < b ==> quorem ((a, b), (a div b, a mod b))"
```
```   267   unfolding quorem_def by simp
```
```   268
```
```   269 lemma quorem_div: "[| quorem((a,b),(q,r));  0 < b |] ==> a div b = q"
```
```   270   by (simp add: quorem_div_mod [THEN unique_quotient])
```
```   271
```
```   272 lemma quorem_mod: "[| quorem((a,b),(q,r));  0 < b |] ==> a mod b = r"
```
```   273   by (simp add: quorem_div_mod [THEN unique_remainder])
```
```   274
```
```   275 (** A dividend of zero **)
```
```   276
```
```   277 lemma div_0 [simp]: "0 div m = (0::nat)"
```
```   278   by (cases "m = 0") simp_all
```
```   279
```
```   280 lemma mod_0 [simp]: "0 mod m = (0::nat)"
```
```   281   by (cases "m = 0") simp_all
```
```   282
```
```   283 (** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
```
```   284
```
```   285 lemma quorem_mult1_eq:
```
```   286      "[| quorem((b,c),(q,r));  0 < c |]
```
```   287       ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
```
```   288   by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
```
```   289
```
```   290 lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
```
```   291   apply (cases "c = 0", simp)
```
```   292   apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
```
```   293   done
```
```   294
```
```   295 lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
```
```   296   apply (cases "c = 0", simp)
```
```   297   apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_mod])
```
```   298   done
```
```   299
```
```   300 lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"
```
```   301   apply (rule trans)
```
```   302    apply (rule_tac s = "b*a mod c" in trans)
```
```   303     apply (rule_tac [2] mod_mult1_eq)
```
```   304    apply (simp_all add: mult_commute)
```
```   305   done
```
```   306
```
```   307 lemma mod_mult_distrib_mod: "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
```
```   308   apply (rule mod_mult1_eq' [THEN trans])
```
```   309   apply (rule mod_mult1_eq)
```
```   310   done
```
```   311
```
```   312 (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
```
```   313
```
```   314 lemma quorem_add1_eq:
```
```   315      "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  0 < c |]
```
```   316       ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
```
```   317   by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
```
```   318
```
```   319 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
```
```   320 lemma div_add1_eq:
```
```   321      "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
```
```   322   apply (cases "c = 0", simp)
```
```   323   apply (blast intro: quorem_add1_eq [THEN quorem_div] quorem_div_mod quorem_div_mod)
```
```   324   done
```
```   325
```
```   326 lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
```
```   327   apply (cases "c = 0", simp)
```
```   328   apply (blast intro: quorem_div_mod quorem_div_mod quorem_add1_eq [THEN quorem_mod])
```
```   329   done
```
```   330
```
```   331
```
```   332 subsection{*Proving @{term "a div (b*c) = (a div b) div c"}*}
```
```   333
```
```   334 (** first, a lemma to bound the remainder **)
```
```   335
```
```   336 lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
```
```   337   apply (cut_tac m = q and n = c in mod_less_divisor)
```
```   338   apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
```
```   339   apply (erule_tac P = "%x. ?lhs < ?rhs x" in ssubst)
```
```   340   apply (simp add: add_mult_distrib2)
```
```   341   done
```
```   342
```
```   343 lemma quorem_mult2_eq: "[| quorem ((a,b), (q,r));  0 < b;  0 < c |]
```
```   344       ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
```
```   345   by (auto simp add: mult_ac quorem_def add_mult_distrib2 [symmetric] mod_lemma)
```
```   346
```
```   347 lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"
```
```   348   apply (cases "b = 0", simp)
```
```   349   apply (cases "c = 0", simp)
```
```   350   apply (force simp add: quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_div])
```
```   351   done
```
```   352
```
```   353 lemma mod_mult2_eq: "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)"
```
```   354   apply (cases "b = 0", simp)
```
```   355   apply (cases "c = 0", simp)
```
```   356   apply (auto simp add: mult_commute quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_mod])
```
```   357   done
```
```   358
```
```   359
```
```   360 subsection{*Cancellation of Common Factors in Division*}
```
```   361
```
```   362 lemma div_mult_mult_lemma:
```
```   363     "[| (0::nat) < b;  0 < c |] ==> (c*a) div (c*b) = a div b"
```
```   364   by (auto simp add: div_mult2_eq)
```
```   365
```
```   366 lemma div_mult_mult1 [simp]: "(0::nat) < c ==> (c*a) div (c*b) = a div b"
```
```   367   apply (cases "b = 0")
```
```   368   apply (auto simp add: linorder_neq_iff [of b] div_mult_mult_lemma)
```
```   369   done
```
```   370
```
```   371 lemma div_mult_mult2 [simp]: "(0::nat) < c ==> (a*c) div (b*c) = a div b"
```
```   372   apply (drule div_mult_mult1)
```
```   373   apply (auto simp add: mult_commute)
```
```   374   done
```
```   375
```
```   376
```
```   377 (*Distribution of Factors over Remainders:
```
```   378
```
```   379 Could prove these as in Integ/IntDiv.ML, but we already have
```
```   380 mod_mult_distrib and mod_mult_distrib2 above!
```
```   381
```
```   382 Goal "(c*a) mod (c*b) = (c::nat) * (a mod b)"
```
```   383 qed "mod_mult_mult1";
```
```   384
```
```   385 Goal "(a*c) mod (b*c) = (a mod b) * (c::nat)";
```
```   386 qed "mod_mult_mult2";
```
```   387  ***)
```
```   388
```
```   389 subsection{*Further Facts about Quotient and Remainder*}
```
```   390
```
```   391 lemma div_1 [simp]: "m div Suc 0 = m"
```
```   392   by (induct m) (simp_all add: div_geq)
```
```   393
```
```   394 lemma div_self [simp]: "0<n ==> n div n = (1::nat)"
```
```   395   by (simp add: div_geq)
```
```   396
```
```   397 lemma div_add_self2: "0<n ==> (m+n) div n = Suc (m div n)"
```
```   398   apply (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n) ")
```
```   399    apply (simp add: add_commute)
```
```   400   apply (subst div_geq [symmetric], simp_all)
```
```   401   done
```
```   402
```
```   403 lemma div_add_self1: "0<n ==> (n+m) div n = Suc (m div n)"
```
```   404   by (simp add: add_commute div_add_self2)
```
```   405
```
```   406 lemma div_mult_self1 [simp]: "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n"
```
```   407   apply (subst div_add1_eq)
```
```   408   apply (subst div_mult1_eq, simp)
```
```   409   done
```
```   410
```
```   411 lemma div_mult_self2 [simp]: "0<n ==> (m + n*k) div n = k + m div (n::nat)"
```
```   412   by (simp add: mult_commute div_mult_self1)
```
```   413
```
```   414
```
```   415 (* Monotonicity of div in first argument *)
```
```   416 lemma div_le_mono [rule_format (no_asm)]:
```
```   417     "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
```
```   418 apply (case_tac "k=0", simp)
```
```   419 apply (induct "n" rule: nat_less_induct, clarify)
```
```   420 apply (case_tac "n<k")
```
```   421 (* 1  case n<k *)
```
```   422 apply simp
```
```   423 (* 2  case n >= k *)
```
```   424 apply (case_tac "m<k")
```
```   425 (* 2.1  case m<k *)
```
```   426 apply simp
```
```   427 (* 2.2  case m>=k *)
```
```   428 apply (simp add: div_geq diff_le_mono)
```
```   429 done
```
```   430
```
```   431 (* Antimonotonicity of div in second argument *)
```
```   432 lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
```
```   433 apply (subgoal_tac "0<n")
```
```   434  prefer 2 apply simp
```
```   435 apply (induct_tac k rule: nat_less_induct)
```
```   436 apply (rename_tac "k")
```
```   437 apply (case_tac "k<n", simp)
```
```   438 apply (subgoal_tac "~ (k<m) ")
```
```   439  prefer 2 apply simp
```
```   440 apply (simp add: div_geq)
```
```   441 apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")
```
```   442  prefer 2
```
```   443  apply (blast intro: div_le_mono diff_le_mono2)
```
```   444 apply (rule le_trans, simp)
```
```   445 apply (simp)
```
```   446 done
```
```   447
```
```   448 lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
```
```   449 apply (case_tac "n=0", simp)
```
```   450 apply (subgoal_tac "m div n \<le> m div 1", simp)
```
```   451 apply (rule div_le_mono2)
```
```   452 apply (simp_all (no_asm_simp))
```
```   453 done
```
```   454
```
```   455 (* Similar for "less than" *)
```
```   456 lemma div_less_dividend [rule_format]:
```
```   457      "!!n::nat. 1<n ==> 0 < m --> m div n < m"
```
```   458 apply (induct_tac m rule: nat_less_induct)
```
```   459 apply (rename_tac "m")
```
```   460 apply (case_tac "m<n", simp)
```
```   461 apply (subgoal_tac "0<n")
```
```   462  prefer 2 apply simp
```
```   463 apply (simp add: div_geq)
```
```   464 apply (case_tac "n<m")
```
```   465  apply (subgoal_tac "(m-n) div n < (m-n) ")
```
```   466   apply (rule impI less_trans_Suc)+
```
```   467 apply assumption
```
```   468   apply (simp_all)
```
```   469 done
```
```   470
```
```   471 declare div_less_dividend [simp]
```
```   472
```
```   473 text{*A fact for the mutilated chess board*}
```
```   474 lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
```
```   475 apply (case_tac "n=0", simp)
```
```   476 apply (induct "m" rule: nat_less_induct)
```
```   477 apply (case_tac "Suc (na) <n")
```
```   478 (* case Suc(na) < n *)
```
```   479 apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
```
```   480 (* case n \<le> Suc(na) *)
```
```   481 apply (simp add: linorder_not_less le_Suc_eq mod_geq)
```
```   482 apply (auto simp add: Suc_diff_le le_mod_geq)
```
```   483 done
```
```   484
```
```   485 lemma nat_mod_div_trivial [simp]: "m mod n div n = (0 :: nat)"
```
```   486   by (cases "n = 0") auto
```
```   487
```
```   488 lemma nat_mod_mod_trivial [simp]: "m mod n mod n = (m mod n :: nat)"
```
```   489   by (cases "n = 0") auto
```
```   490
```
```   491
```
```   492 subsection{*The Divides Relation*}
```
```   493
```
```   494 lemma dvdI [intro?]: "n = m * k ==> m dvd n"
```
```   495   unfolding dvd_def by blast
```
```   496
```
```   497 lemma dvdE [elim?]: "!!P. [|m dvd n;  !!k. n = m*k ==> P|] ==> P"
```
```   498   unfolding dvd_def by blast
```
```   499
```
```   500 lemma dvd_0_right [iff]: "m dvd (0::nat)"
```
```   501   unfolding dvd_def by (blast intro: mult_0_right [symmetric])
```
```   502
```
```   503 lemma dvd_0_left: "0 dvd m ==> m = (0::nat)"
```
```   504   by (force simp add: dvd_def)
```
```   505
```
```   506 lemma dvd_0_left_iff [iff]: "(0 dvd (m::nat)) = (m = 0)"
```
```   507   by (blast intro: dvd_0_left)
```
```   508
```
```   509 lemma dvd_1_left [iff]: "Suc 0 dvd k"
```
```   510   unfolding dvd_def by simp
```
```   511
```
```   512 lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
```
```   513   by (simp add: dvd_def)
```
```   514
```
```   515 lemma dvd_refl [simp]: "m dvd (m::nat)"
```
```   516   unfolding dvd_def by (blast intro: mult_1_right [symmetric])
```
```   517
```
```   518 lemma dvd_trans [trans]: "[| m dvd n; n dvd p |] ==> m dvd (p::nat)"
```
```   519   unfolding dvd_def by (blast intro: mult_assoc)
```
```   520
```
```   521 lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
```
```   522   unfolding dvd_def
```
```   523   by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
```
```   524
```
```   525 lemma dvd_add: "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)"
```
```   526   unfolding dvd_def
```
```   527   by (blast intro: add_mult_distrib2 [symmetric])
```
```   528
```
```   529 lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
```
```   530   unfolding dvd_def
```
```   531   by (blast intro: diff_mult_distrib2 [symmetric])
```
```   532
```
```   533 lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)"
```
```   534   apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
```
```   535   apply (blast intro: dvd_add)
```
```   536   done
```
```   537
```
```   538 lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)"
```
```   539   by (drule_tac m = m in dvd_diff, auto)
```
```   540
```
```   541 lemma dvd_mult: "k dvd n ==> k dvd (m*n :: nat)"
```
```   542   unfolding dvd_def by (blast intro: mult_left_commute)
```
```   543
```
```   544 lemma dvd_mult2: "k dvd m ==> k dvd (m*n :: nat)"
```
```   545   apply (subst mult_commute)
```
```   546   apply (erule dvd_mult)
```
```   547   done
```
```   548
```
```   549 lemma dvd_triv_right [iff]: "k dvd (m*k :: nat)"
```
```   550   by (rule dvd_refl [THEN dvd_mult])
```
```   551
```
```   552 lemma dvd_triv_left [iff]: "k dvd (k*m :: nat)"
```
```   553   by (rule dvd_refl [THEN dvd_mult2])
```
```   554
```
```   555 lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
```
```   556   apply (rule iffI)
```
```   557    apply (erule_tac [2] dvd_add)
```
```   558    apply (rule_tac [2] dvd_refl)
```
```   559   apply (subgoal_tac "n = (n+k) -k")
```
```   560    prefer 2 apply simp
```
```   561   apply (erule ssubst)
```
```   562   apply (erule dvd_diff)
```
```   563   apply (rule dvd_refl)
```
```   564   done
```
```   565
```
```   566 lemma dvd_mod: "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n"
```
```   567   unfolding dvd_def
```
```   568   apply (case_tac "n = 0", auto)
```
```   569   apply (blast intro: mod_mult_distrib2 [symmetric])
```
```   570   done
```
```   571
```
```   572 lemma dvd_mod_imp_dvd: "[| (k::nat) dvd m mod n;  k dvd n |] ==> k dvd m"
```
```   573   apply (subgoal_tac "k dvd (m div n) *n + m mod n")
```
```   574    apply (simp add: mod_div_equality)
```
```   575   apply (simp only: dvd_add dvd_mult)
```
```   576   done
```
```   577
```
```   578 lemma dvd_mod_iff: "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)"
```
```   579   by (blast intro: dvd_mod_imp_dvd dvd_mod)
```
```   580
```
```   581 lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
```
```   582   unfolding dvd_def
```
```   583   apply (erule exE)
```
```   584   apply (simp add: mult_ac)
```
```   585   done
```
```   586
```
```   587 lemma dvd_mult_cancel1: "0<m ==> (m*n dvd m) = (n = (1::nat))"
```
```   588   apply auto
```
```   589    apply (subgoal_tac "m*n dvd m*1")
```
```   590    apply (drule dvd_mult_cancel, auto)
```
```   591   done
```
```   592
```
```   593 lemma dvd_mult_cancel2: "0<m ==> (n*m dvd m) = (n = (1::nat))"
```
```   594   apply (subst mult_commute)
```
```   595   apply (erule dvd_mult_cancel1)
```
```   596   done
```
```   597
```
```   598 lemma mult_dvd_mono: "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)"
```
```   599   apply (unfold dvd_def, clarify)
```
```   600   apply (rule_tac x = "k*ka" in exI)
```
```   601   apply (simp add: mult_ac)
```
```   602   done
```
```   603
```
```   604 lemma dvd_mult_left: "(i*j :: nat) dvd k ==> i dvd k"
```
```   605   by (simp add: dvd_def mult_assoc, blast)
```
```   606
```
```   607 lemma dvd_mult_right: "(i*j :: nat) dvd k ==> j dvd k"
```
```   608   apply (unfold dvd_def, clarify)
```
```   609   apply (rule_tac x = "i*k" in exI)
```
```   610   apply (simp add: mult_ac)
```
```   611   done
```
```   612
```
```   613 lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
```
```   614   apply (unfold dvd_def, clarify)
```
```   615   apply (simp_all (no_asm_use) add: zero_less_mult_iff)
```
```   616   apply (erule conjE)
```
```   617   apply (rule le_trans)
```
```   618    apply (rule_tac [2] le_refl [THEN mult_le_mono])
```
```   619    apply (erule_tac [2] Suc_leI, simp)
```
```   620   done
```
```   621
```
```   622 lemma dvd_eq_mod_eq_0: "!!k::nat. (k dvd n) = (n mod k = 0)"
```
```   623   apply (unfold dvd_def)
```
```   624   apply (case_tac "k=0", simp, safe)
```
```   625    apply (simp add: mult_commute)
```
```   626   apply (rule_tac t = n and n1 = k in mod_div_equality [THEN subst])
```
```   627   apply (subst mult_commute, simp)
```
```   628   done
```
```   629
```
```   630 lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
```
```   631   apply (subgoal_tac "m mod n = 0")
```
```   632    apply (simp add: mult_div_cancel)
```
```   633   apply (simp only: dvd_eq_mod_eq_0)
```
```   634   done
```
```   635
```
```   636 lemma le_imp_power_dvd: "!!i::nat. m \<le> n ==> i^m dvd i^n"
```
```   637   apply (unfold dvd_def)
```
```   638   apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
```
```   639   apply (simp add: power_add)
```
```   640   done
```
```   641
```
```   642 lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
```
```   643   by (induct n) auto
```
```   644
```
```   645 lemma power_le_dvd [rule_format]: "k^j dvd n --> i\<le>j --> k^i dvd (n::nat)"
```
```   646   apply (induct j)
```
```   647    apply (simp_all add: le_Suc_eq)
```
```   648   apply (blast dest!: dvd_mult_right)
```
```   649   done
```
```   650
```
```   651 lemma power_dvd_imp_le: "[|i^m dvd i^n;  (1::nat) < i|] ==> m \<le> n"
```
```   652   apply (rule power_le_imp_le_exp, assumption)
```
```   653   apply (erule dvd_imp_le, simp)
```
```   654   done
```
```   655
```
```   656 lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
```
```   657   by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
```
```   658
```
```   659 lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
```
```   660
```
```   661 (*Loses information, namely we also have r<d provided d is nonzero*)
```
```   662 lemma mod_eqD: "(m mod d = r) ==> \<exists>q::nat. m = r + q*d"
```
```   663   apply (cut_tac m = m in mod_div_equality)
```
```   664   apply (simp only: add_ac)
```
```   665   apply (blast intro: sym)
```
```   666   done
```
```   667
```
```   668
```
```   669 lemma split_div:
```
```   670  "P(n div k :: nat) =
```
```   671  ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
```
```   672  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
```
```   673 proof
```
```   674   assume P: ?P
```
```   675   show ?Q
```
```   676   proof (cases)
```
```   677     assume "k = 0"
```
```   678     with P show ?Q by(simp add:DIVISION_BY_ZERO_DIV)
```
```   679   next
```
```   680     assume not0: "k \<noteq> 0"
```
```   681     thus ?Q
```
```   682     proof (simp, intro allI impI)
```
```   683       fix i j
```
```   684       assume n: "n = k*i + j" and j: "j < k"
```
```   685       show "P i"
```
```   686       proof (cases)
```
```   687         assume "i = 0"
```
```   688         with n j P show "P i" by simp
```
```   689       next
```
```   690         assume "i \<noteq> 0"
```
```   691         with not0 n j P show "P i" by(simp add:add_ac)
```
```   692       qed
```
```   693     qed
```
```   694   qed
```
```   695 next
```
```   696   assume Q: ?Q
```
```   697   show ?P
```
```   698   proof (cases)
```
```   699     assume "k = 0"
```
```   700     with Q show ?P by(simp add:DIVISION_BY_ZERO_DIV)
```
```   701   next
```
```   702     assume not0: "k \<noteq> 0"
```
```   703     with Q have R: ?R by simp
```
```   704     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
```
```   705     show ?P by simp
```
```   706   qed
```
```   707 qed
```
```   708
```
```   709 lemma split_div_lemma:
```
```   710   "0 < n \<Longrightarrow> (n * q \<le> m \<and> m < n * (Suc q)) = (q = ((m::nat) div n))"
```
```   711   apply (rule iffI)
```
```   712   apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
```
```   713 prefer 3; apply assumption
```
```   714   apply (simp_all add: quorem_def) apply arith
```
```   715   apply (rule conjI)
```
```   716   apply (rule_tac P="%x. n * (m div n) \<le> x" in
```
```   717     subst [OF mod_div_equality [of _ n]])
```
```   718   apply (simp only: add: mult_ac)
```
```   719   apply (rule_tac P="%x. x < n + n * (m div n)" in
```
```   720     subst [OF mod_div_equality [of _ n]])
```
```   721   apply (simp only: add: mult_ac add_ac)
```
```   722   apply (rule add_less_mono1, simp)
```
```   723   done
```
```   724
```
```   725 theorem split_div':
```
```   726   "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
```
```   727    (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
```
```   728   apply (case_tac "0 < n")
```
```   729   apply (simp only: add: split_div_lemma)
```
```   730   apply (simp_all add: DIVISION_BY_ZERO_DIV)
```
```   731   done
```
```   732
```
```   733 lemma split_mod:
```
```   734  "P(n mod k :: nat) =
```
```   735  ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
```
```   736  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
```
```   737 proof
```
```   738   assume P: ?P
```
```   739   show ?Q
```
```   740   proof (cases)
```
```   741     assume "k = 0"
```
```   742     with P show ?Q by(simp add:DIVISION_BY_ZERO_MOD)
```
```   743   next
```
```   744     assume not0: "k \<noteq> 0"
```
```   745     thus ?Q
```
```   746     proof (simp, intro allI impI)
```
```   747       fix i j
```
```   748       assume "n = k*i + j" "j < k"
```
```   749       thus "P j" using not0 P by(simp add:add_ac mult_ac)
```
```   750     qed
```
```   751   qed
```
```   752 next
```
```   753   assume Q: ?Q
```
```   754   show ?P
```
```   755   proof (cases)
```
```   756     assume "k = 0"
```
```   757     with Q show ?P by(simp add:DIVISION_BY_ZERO_MOD)
```
```   758   next
```
```   759     assume not0: "k \<noteq> 0"
```
```   760     with Q have R: ?R by simp
```
```   761     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
```
```   762     show ?P by simp
```
```   763   qed
```
```   764 qed
```
```   765
```
```   766 theorem mod_div_equality': "(m::nat) mod n = m - (m div n) * n"
```
```   767   apply (rule_tac P="%x. m mod n = x - (m div n) * n" in
```
```   768     subst [OF mod_div_equality [of _ n]])
```
```   769   apply arith
```
```   770   done
```
```   771
```
```   772 lemma div_mod_equality':
```
```   773   fixes m n :: nat
```
```   774   shows "m div n * n = m - m mod n"
```
```   775 proof -
```
```   776   have "m mod n \<le> m mod n" ..
```
```   777   from div_mod_equality have
```
```   778     "m div n * n + m mod n - m mod n = m - m mod n" by simp
```
```   779   with diff_add_assoc [OF `m mod n \<le> m mod n`, of "m div n * n"] have
```
```   780     "m div n * n + (m mod n - m mod n) = m - m mod n"
```
```   781     by simp
```
```   782   then show ?thesis by simp
```
```   783 qed
```
```   784
```
```   785
```
```   786 subsection {*An ``induction'' law for modulus arithmetic.*}
```
```   787
```
```   788 lemma mod_induct_0:
```
```   789   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
```
```   790   and base: "P i" and i: "i<p"
```
```   791   shows "P 0"
```
```   792 proof (rule ccontr)
```
```   793   assume contra: "\<not>(P 0)"
```
```   794   from i have p: "0<p" by simp
```
```   795   have "\<forall>k. 0<k \<longrightarrow> \<not> P (p-k)" (is "\<forall>k. ?A k")
```
```   796   proof
```
```   797     fix k
```
```   798     show "?A k"
```
```   799     proof (induct k)
```
```   800       show "?A 0" by simp  -- "by contradiction"
```
```   801     next
```
```   802       fix n
```
```   803       assume ih: "?A n"
```
```   804       show "?A (Suc n)"
```
```   805       proof (clarsimp)
```
```   806         assume y: "P (p - Suc n)"
```
```   807         have n: "Suc n < p"
```
```   808         proof (rule ccontr)
```
```   809           assume "\<not>(Suc n < p)"
```
```   810           hence "p - Suc n = 0"
```
```   811             by simp
```
```   812           with y contra show "False"
```
```   813             by simp
```
```   814         qed
```
```   815         hence n2: "Suc (p - Suc n) = p-n" by arith
```
```   816         from p have "p - Suc n < p" by arith
```
```   817         with y step have z: "P ((Suc (p - Suc n)) mod p)"
```
```   818           by blast
```
```   819         show "False"
```
```   820         proof (cases "n=0")
```
```   821           case True
```
```   822           with z n2 contra show ?thesis by simp
```
```   823         next
```
```   824           case False
```
```   825           with p have "p-n < p" by arith
```
```   826           with z n2 False ih show ?thesis by simp
```
```   827         qed
```
```   828       qed
```
```   829     qed
```
```   830   qed
```
```   831   moreover
```
```   832   from i obtain k where "0<k \<and> i+k=p"
```
```   833     by (blast dest: less_imp_add_positive)
```
```   834   hence "0<k \<and> i=p-k" by auto
```
```   835   moreover
```
```   836   note base
```
```   837   ultimately
```
```   838   show "False" by blast
```
```   839 qed
```
```   840
```
```   841 lemma mod_induct:
```
```   842   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
```
```   843   and base: "P i" and i: "i<p" and j: "j<p"
```
```   844   shows "P j"
```
```   845 proof -
```
```   846   have "\<forall>j<p. P j"
```
```   847   proof
```
```   848     fix j
```
```   849     show "j<p \<longrightarrow> P j" (is "?A j")
```
```   850     proof (induct j)
```
```   851       from step base i show "?A 0"
```
```   852         by (auto elim: mod_induct_0)
```
```   853     next
```
```   854       fix k
```
```   855       assume ih: "?A k"
```
```   856       show "?A (Suc k)"
```
```   857       proof
```
```   858         assume suc: "Suc k < p"
```
```   859         hence k: "k<p" by simp
```
```   860         with ih have "P k" ..
```
```   861         with step k have "P (Suc k mod p)"
```
```   862           by blast
```
```   863         moreover
```
```   864         from suc have "Suc k mod p = Suc k"
```
```   865           by simp
```
```   866         ultimately
```
```   867         show "P (Suc k)" by simp
```
```   868       qed
```
```   869     qed
```
```   870   qed
```
```   871   with j show ?thesis by blast
```
```   872 qed
```
```   873
```
```   874
```
```   875 lemma mod_add_left_eq: "((a::nat) + b) mod c = (a mod c + b) mod c"
```
```   876   apply (rule trans [symmetric])
```
```   877    apply (rule mod_add1_eq, simp)
```
```   878   apply (rule mod_add1_eq [symmetric])
```
```   879   done
```
```   880
```
```   881 lemma mod_add_right_eq: "(a+b) mod (c::nat) = (a + (b mod c)) mod c"
```
```   882   apply (rule trans [symmetric])
```
```   883    apply (rule mod_add1_eq, simp)
```
```   884   apply (rule mod_add1_eq [symmetric])
```
```   885   done
```
```   886
```
```   887 lemma mod_div_decomp:
```
```   888   fixes n k :: nat
```
```   889   obtains m q where "m = n div k" and "q = n mod k"
```
```   890     and "n = m * k + q"
```
```   891 proof -
```
```   892   from mod_div_equality have "n = n div k * k + n mod k" by auto
```
```   893   moreover have "n div k = n div k" ..
```
```   894   moreover have "n mod k = n mod k" ..
```
```   895   note that ultimately show thesis by blast
```
```   896 qed
```
```   897
```
```   898
```
```   899 subsection {* Code generation for div, mod and dvd on nat *}
```
```   900
```
```   901 definition [code nofunc]:
```
```   902   "divmod (m\<Colon>nat) n = (m div n, m mod n)"
```
```   903
```
```   904 lemma divmod_zero [code]: "divmod m 0 = (0, m)"
```
```   905   unfolding divmod_def by simp
```
```   906
```
```   907 lemma divmod_succ [code]:
```
```   908   "divmod m (Suc k) = (if m < Suc k then (0, m) else
```
```   909     let
```
```   910       (p, q) = divmod (m - Suc k) (Suc k)
```
```   911     in (Suc p, q))"
```
```   912   unfolding divmod_def Let_def split_def
```
```   913   by (auto intro: div_geq mod_geq)
```
```   914
```
```   915 lemma div_divmod [code]: "m div n = fst (divmod m n)"
```
```   916   unfolding divmod_def by simp
```
```   917
```
```   918 lemma mod_divmod [code]: "m mod n = snd (divmod m n)"
```
```   919   unfolding divmod_def by simp
```
```   920
```
```   921 definition
```
```   922   dvd_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
```
```   923 where
```
```   924   "dvd_nat m n \<longleftrightarrow> n mod m = (0 \<Colon> nat)"
```
```   925
```
```   926 lemma [code inline]:
```
```   927   "op dvd = dvd_nat"
```
```   928   by (auto simp add: dvd_nat_def dvd_eq_mod_eq_0 expand_fun_eq)
```
```   929
```
```   930 code_modulename SML
```
```   931   Divides Integer
```
```   932
```
```   933 code_modulename OCaml
```
```   934   Divides Integer
```
```   935
```
```   936 hide (open) const divmod dvd_nat
```
```   937
```
```   938 subsection {* Legacy bindings *}
```
```   939
```
```   940 ML
```
```   941 {*
```
```   942 val div_def = thm "div_def"
```
```   943 val mod_def = thm "mod_def"
```
```   944 val dvd_def = thm "dvd_def"
```
```   945 val quorem_def = thm "quorem_def"
```
```   946
```
```   947 val wf_less_trans = thm "wf_less_trans";
```
```   948 val mod_eq = thm "mod_eq";
```
```   949 val div_eq = thm "div_eq";
```
```   950 val DIVISION_BY_ZERO_DIV = thm "DIVISION_BY_ZERO_DIV";
```
```   951 val DIVISION_BY_ZERO_MOD = thm "DIVISION_BY_ZERO_MOD";
```
```   952 val mod_less = thm "mod_less";
```
```   953 val mod_geq = thm "mod_geq";
```
```   954 val le_mod_geq = thm "le_mod_geq";
```
```   955 val mod_if = thm "mod_if";
```
```   956 val mod_1 = thm "mod_1";
```
```   957 val mod_self = thm "mod_self";
```
```   958 val mod_add_self2 = thm "mod_add_self2";
```
```   959 val mod_add_self1 = thm "mod_add_self1";
```
```   960 val mod_mult_self1 = thm "mod_mult_self1";
```
```   961 val mod_mult_self2 = thm "mod_mult_self2";
```
```   962 val mod_mult_distrib = thm "mod_mult_distrib";
```
```   963 val mod_mult_distrib2 = thm "mod_mult_distrib2";
```
```   964 val mod_mult_self_is_0 = thm "mod_mult_self_is_0";
```
```   965 val mod_mult_self1_is_0 = thm "mod_mult_self1_is_0";
```
```   966 val div_less = thm "div_less";
```
```   967 val div_geq = thm "div_geq";
```
```   968 val le_div_geq = thm "le_div_geq";
```
```   969 val div_if = thm "div_if";
```
```   970 val mod_div_equality = thm "mod_div_equality";
```
```   971 val mod_div_equality2 = thm "mod_div_equality2";
```
```   972 val div_mod_equality = thm "div_mod_equality";
```
```   973 val div_mod_equality2 = thm "div_mod_equality2";
```
```   974 val mult_div_cancel = thm "mult_div_cancel";
```
```   975 val mod_less_divisor = thm "mod_less_divisor";
```
```   976 val div_mult_self_is_m = thm "div_mult_self_is_m";
```
```   977 val div_mult_self1_is_m = thm "div_mult_self1_is_m";
```
```   978 val unique_quotient_lemma = thm "unique_quotient_lemma";
```
```   979 val unique_quotient = thm "unique_quotient";
```
```   980 val unique_remainder = thm "unique_remainder";
```
```   981 val div_0 = thm "div_0";
```
```   982 val mod_0 = thm "mod_0";
```
```   983 val div_mult1_eq = thm "div_mult1_eq";
```
```   984 val mod_mult1_eq = thm "mod_mult1_eq";
```
```   985 val mod_mult1_eq' = thm "mod_mult1_eq'";
```
```   986 val mod_mult_distrib_mod = thm "mod_mult_distrib_mod";
```
```   987 val div_add1_eq = thm "div_add1_eq";
```
```   988 val mod_add1_eq = thm "mod_add1_eq";
```
```   989 val mod_add_left_eq = thm "mod_add_left_eq";
```
```   990  val mod_add_right_eq = thm "mod_add_right_eq";
```
```   991 val mod_lemma = thm "mod_lemma";
```
```   992 val div_mult2_eq = thm "div_mult2_eq";
```
```   993 val mod_mult2_eq = thm "mod_mult2_eq";
```
```   994 val div_mult_mult_lemma = thm "div_mult_mult_lemma";
```
```   995 val div_mult_mult1 = thm "div_mult_mult1";
```
```   996 val div_mult_mult2 = thm "div_mult_mult2";
```
```   997 val div_1 = thm "div_1";
```
```   998 val div_self = thm "div_self";
```
```   999 val div_add_self2 = thm "div_add_self2";
```
```  1000 val div_add_self1 = thm "div_add_self1";
```
```  1001 val div_mult_self1 = thm "div_mult_self1";
```
```  1002 val div_mult_self2 = thm "div_mult_self2";
```
```  1003 val div_le_mono = thm "div_le_mono";
```
```  1004 val div_le_mono2 = thm "div_le_mono2";
```
```  1005 val div_le_dividend = thm "div_le_dividend";
```
```  1006 val div_less_dividend = thm "div_less_dividend";
```
```  1007 val mod_Suc = thm "mod_Suc";
```
```  1008 val dvdI = thm "dvdI";
```
```  1009 val dvdE = thm "dvdE";
```
```  1010 val dvd_0_right = thm "dvd_0_right";
```
```  1011 val dvd_0_left = thm "dvd_0_left";
```
```  1012 val dvd_0_left_iff = thm "dvd_0_left_iff";
```
```  1013 val dvd_1_left = thm "dvd_1_left";
```
```  1014 val dvd_1_iff_1 = thm "dvd_1_iff_1";
```
```  1015 val dvd_refl = thm "dvd_refl";
```
```  1016 val dvd_trans = thm "dvd_trans";
```
```  1017 val dvd_anti_sym = thm "dvd_anti_sym";
```
```  1018 val dvd_add = thm "dvd_add";
```
```  1019 val dvd_diff = thm "dvd_diff";
```
```  1020 val dvd_diffD = thm "dvd_diffD";
```
```  1021 val dvd_diffD1 = thm "dvd_diffD1";
```
```  1022 val dvd_mult = thm "dvd_mult";
```
```  1023 val dvd_mult2 = thm "dvd_mult2";
```
```  1024 val dvd_reduce = thm "dvd_reduce";
```
```  1025 val dvd_mod = thm "dvd_mod";
```
```  1026 val dvd_mod_imp_dvd = thm "dvd_mod_imp_dvd";
```
```  1027 val dvd_mod_iff = thm "dvd_mod_iff";
```
```  1028 val dvd_mult_cancel = thm "dvd_mult_cancel";
```
```  1029 val dvd_mult_cancel1 = thm "dvd_mult_cancel1";
```
```  1030 val dvd_mult_cancel2 = thm "dvd_mult_cancel2";
```
```  1031 val mult_dvd_mono = thm "mult_dvd_mono";
```
```  1032 val dvd_mult_left = thm "dvd_mult_left";
```
```  1033 val dvd_mult_right = thm "dvd_mult_right";
```
```  1034 val dvd_imp_le = thm "dvd_imp_le";
```
```  1035 val dvd_eq_mod_eq_0 = thm "dvd_eq_mod_eq_0";
```
```  1036 val dvd_mult_div_cancel = thm "dvd_mult_div_cancel";
```
```  1037 val mod_eq_0_iff = thm "mod_eq_0_iff";
```
```  1038 val mod_eqD = thm "mod_eqD";
```
```  1039 *}
```
```  1040
```
```  1041 (*
```
```  1042 lemma split_div:
```
```  1043 assumes m: "m \<noteq> 0"
```
```  1044 shows "P(n div m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P i)"
```
```  1045        (is "?P = ?Q")
```
```  1046 proof
```
```  1047   assume P: ?P
```
```  1048   show ?Q
```
```  1049   proof (intro allI impI)
```
```  1050     fix i j
```
```  1051     assume n: "n = m*i + j" and j: "j < m"
```
```  1052     show "P i"
```
```  1053     proof (cases)
```
```  1054       assume "i = 0"
```
```  1055       with n j P show "P i" by simp
```
```  1056     next
```
```  1057       assume "i \<noteq> 0"
```
```  1058       with n j P show "P i" by (simp add:add_ac div_mult_self1)
```
```  1059     qed
```
```  1060   qed
```
```  1061 next
```
```  1062   assume Q: ?Q
```
```  1063   from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
```
```  1064   show ?P by simp
```
```  1065 qed
```
```  1066
```
```  1067 lemma split_mod:
```
```  1068 assumes m: "m \<noteq> 0"
```
```  1069 shows "P(n mod m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P j)"
```
```  1070        (is "?P = ?Q")
```
```  1071 proof
```
```  1072   assume P: ?P
```
```  1073   show ?Q
```
```  1074   proof (intro allI impI)
```
```  1075     fix i j
```
```  1076     assume "n = m*i + j" "j < m"
```
```  1077     thus "P j" using m P by(simp add:add_ac mult_ac)
```
```  1078   qed
```
```  1079 next
```
```  1080   assume Q: ?Q
```
```  1081   from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
```
```  1082   show ?P by simp
```
```  1083 qed
```
```  1084 *)
```
```  1085 end
```