src/HOL/Divides.ML
 author oheimb Wed Jan 31 10:15:55 2001 +0100 (2001-01-31) changeset 11008 f7333f055ef6 parent 10964 afc1dfc5a92d child 11313 04c8da2e0917 permissions -rw-r--r--
improved theory reference in comment
```     1 (*  Title:      HOL/Divides.ML
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1993  University of Cambridge
```
```     5
```
```     6 The division operators div, mod and the divides relation "dvd"
```
```     7 *)
```
```     8
```
```     9
```
```    10 (** Less-then properties **)
```
```    11
```
```    12 bind_thm ("wf_less_trans", [eq_reflection, wf_pred_nat RS wf_trancl] MRS
```
```    13                     def_wfrec RS trans);
```
```    14
```
```    15 Goal "(%m. m mod n) = wfrec (trancl pred_nat) \
```
```    16 \                           (%f j. if j<n | n=0 then j else f (j-n))";
```
```    17 by (simp_tac (simpset() addsimps [mod_def]) 1);
```
```    18 qed "mod_eq";
```
```    19
```
```    20 Goal "(%m. m div n) = wfrec (trancl pred_nat) \
```
```    21 \            (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))";
```
```    22 by (simp_tac (simpset() addsimps [div_def]) 1);
```
```    23 qed "div_eq";
```
```    24
```
```    25
```
```    26 (** Aribtrary definitions for division by zero.  Useful to simplify
```
```    27     certain equations **)
```
```    28
```
```    29 Goal "a div 0 = (0::nat)";
```
```    30 by (rtac (div_eq RS wf_less_trans) 1);
```
```    31 by (Asm_simp_tac 1);
```
```    32 qed "DIVISION_BY_ZERO_DIV";  (*NOT for adding to default simpset*)
```
```    33
```
```    34 Goal "a mod 0 = (a::nat)";
```
```    35 by (rtac (mod_eq RS wf_less_trans) 1);
```
```    36 by (Asm_simp_tac 1);
```
```    37 qed "DIVISION_BY_ZERO_MOD";  (*NOT for adding to default simpset*)
```
```    38
```
```    39 fun div_undefined_case_tac s i =
```
```    40   case_tac s i THEN
```
```    41   Full_simp_tac (i+1) THEN
```
```    42   asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_DIV,
```
```    43 				    DIVISION_BY_ZERO_MOD]) i;
```
```    44
```
```    45 (*** Remainder ***)
```
```    46
```
```    47 Goal "m<n ==> m mod n = (m::nat)";
```
```    48 by (rtac (mod_eq RS wf_less_trans) 1);
```
```    49 by (Asm_simp_tac 1);
```
```    50 qed "mod_less";
```
```    51 Addsimps [mod_less];
```
```    52
```
```    53 Goal "~ m < (n::nat) ==> m mod n = (m-n) mod n";
```
```    54 by (div_undefined_case_tac "n=0" 1);
```
```    55 by (rtac (mod_eq RS wf_less_trans) 1);
```
```    56 by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
```
```    57 qed "mod_geq";
```
```    58
```
```    59 (*Avoids the ugly ~m<n above*)
```
```    60 Goal "(n::nat) <= m ==> m mod n = (m-n) mod n";
```
```    61 by (asm_simp_tac (simpset() addsimps [mod_geq, not_less_iff_le]) 1);
```
```    62 qed "le_mod_geq";
```
```    63
```
```    64 Goal "m mod (n::nat) = (if m<n then m else (m-n) mod n)";
```
```    65 by (asm_simp_tac (simpset() addsimps [mod_geq]) 1);
```
```    66 qed "mod_if";
```
```    67
```
```    68 Goal "m mod 1 = (0::nat)";
```
```    69 by (induct_tac "m" 1);
```
```    70 by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_geq])));
```
```    71 qed "mod_1";
```
```    72 Addsimps [mod_1];
```
```    73
```
```    74 Goal "n mod n = (0::nat)";
```
```    75 by (div_undefined_case_tac "n=0" 1);
```
```    76 by (asm_simp_tac (simpset() addsimps [mod_geq]) 1);
```
```    77 qed "mod_self";
```
```    78 Addsimps [mod_self];
```
```    79
```
```    80 Goal "(m+n) mod n = m mod (n::nat)";
```
```    81 by (subgoal_tac "(n + m) mod n = (n+m-n) mod n" 1);
```
```    82 by (stac (mod_geq RS sym) 2);
```
```    83 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
```
```    84 qed "mod_add_self2";
```
```    85
```
```    86 Goal "(n+m) mod n = m mod (n::nat)";
```
```    87 by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_self2]) 1);
```
```    88 qed "mod_add_self1";
```
```    89
```
```    90 Addsimps [mod_add_self1, mod_add_self2];
```
```    91
```
```    92 Goal "(m + k*n) mod n = m mod (n::nat)";
```
```    93 by (induct_tac "k" 1);
```
```    94 by (ALLGOALS
```
```    95     (asm_simp_tac
```
```    96      (simpset() addsimps [read_instantiate [("y","n")] add_left_commute])));
```
```    97 qed "mod_mult_self1";
```
```    98
```
```    99 Goal "(m + n*k) mod n = m mod (n::nat)";
```
```   100 by (asm_simp_tac (simpset() addsimps [mult_commute, mod_mult_self1]) 1);
```
```   101 qed "mod_mult_self2";
```
```   102
```
```   103 Addsimps [mod_mult_self1, mod_mult_self2];
```
```   104
```
```   105 Goal "(m mod n) * (k::nat) = (m*k) mod (n*k)";
```
```   106 by (div_undefined_case_tac "n=0" 1);
```
```   107 by (div_undefined_case_tac "k=0" 1);
```
```   108 by (induct_thm_tac nat_less_induct "m" 1);
```
```   109 by (stac mod_if 1);
```
```   110 by (Asm_simp_tac 1);
```
```   111 by (asm_simp_tac (simpset() addsimps [mod_geq,
```
```   112 				      diff_less, diff_mult_distrib]) 1);
```
```   113 qed "mod_mult_distrib";
```
```   114
```
```   115 Goal "(k::nat) * (m mod n) = (k*m) mod (k*n)";
```
```   116 by (asm_simp_tac
```
```   117     (simpset() addsimps [read_instantiate [("m","k")] mult_commute,
```
```   118 			 mod_mult_distrib]) 1);
```
```   119 qed "mod_mult_distrib2";
```
```   120
```
```   121 Goal "(m*n) mod n = (0::nat)";
```
```   122 by (div_undefined_case_tac "n=0" 1);
```
```   123 by (induct_tac "m" 1);
```
```   124 by (Asm_simp_tac 1);
```
```   125 by (rename_tac "k" 1);
```
```   126 by (cut_inst_tac [("m","k*n"),("n","n")] mod_add_self2 1);
```
```   127 by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
```
```   128 qed "mod_mult_self_is_0";
```
```   129
```
```   130 Goal "(n*m) mod n = (0::nat)";
```
```   131 by (simp_tac (simpset() addsimps [mult_commute, mod_mult_self_is_0]) 1);
```
```   132 qed "mod_mult_self1_is_0";
```
```   133 Addsimps [mod_mult_self_is_0, mod_mult_self1_is_0];
```
```   134
```
```   135
```
```   136 (*** Quotient ***)
```
```   137
```
```   138 Goal "m<n ==> m div n = (0::nat)";
```
```   139 by (rtac (div_eq RS wf_less_trans) 1);
```
```   140 by (Asm_simp_tac 1);
```
```   141 qed "div_less";
```
```   142 Addsimps [div_less];
```
```   143
```
```   144 Goal "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)";
```
```   145 by (rtac (div_eq RS wf_less_trans) 1);
```
```   146 by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
```
```   147 qed "div_geq";
```
```   148
```
```   149 (*Avoids the ugly ~m<n above*)
```
```   150 Goal "[| 0<n;  n<=m |] ==> m div n = Suc((m-n) div n)";
```
```   151 by (asm_simp_tac (simpset() addsimps [div_geq, not_less_iff_le]) 1);
```
```   152 qed "le_div_geq";
```
```   153
```
```   154 Goal "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))";
```
```   155 by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
```
```   156 qed "div_if";
```
```   157
```
```   158
```
```   159 (*Main Result about quotient and remainder.*)
```
```   160 Goal "(m div n)*n + m mod n = (m::nat)";
```
```   161 by (div_undefined_case_tac "n=0" 1);
```
```   162 by (induct_thm_tac nat_less_induct "m" 1);
```
```   163 by (stac mod_if 1);
```
```   164 by (ALLGOALS (asm_simp_tac
```
```   165 	      (simpset() addsimps [add_assoc, div_geq,
```
```   166 				   add_diff_inverse, diff_less])));
```
```   167 qed "mod_div_equality";
```
```   168
```
```   169 (* a simple rearrangement of mod_div_equality: *)
```
```   170 Goal "(n::nat) * (m div n) = m - (m mod n)";
```
```   171 by (cut_inst_tac [("m","m"),("n","n")] mod_div_equality 1);
```
```   172 by (full_simp_tac (simpset() addsimps mult_ac) 1);
```
```   173 by (arith_tac 1);
```
```   174 qed "mult_div_cancel";
```
```   175
```
```   176 Goal "0<n ==> m mod n < (n::nat)";
```
```   177 by (induct_thm_tac nat_less_induct "m" 1);
```
```   178 by (case_tac "na<n" 1);
```
```   179 (*case n le na*)
```
```   180 by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 2);
```
```   181 (*case na<n*)
```
```   182 by (Asm_simp_tac 1);
```
```   183 qed "mod_less_divisor";
```
```   184 Addsimps [mod_less_divisor];
```
```   185
```
```   186 (*** More division laws ***)
```
```   187
```
```   188 Goal "0<n ==> (m*n) div n = (m::nat)";
```
```   189 by (cut_inst_tac [("m", "m*n"),("n","n")] mod_div_equality 1);
```
```   190 by Auto_tac;
```
```   191 qed "div_mult_self_is_m";
```
```   192
```
```   193 Goal "0<n ==> (n*m) div n = (m::nat)";
```
```   194 by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self_is_m]) 1);
```
```   195 qed "div_mult_self1_is_m";
```
```   196 Addsimps [div_mult_self_is_m, div_mult_self1_is_m];
```
```   197
```
```   198 (*mod_mult_distrib2 above is the counterpart for remainder*)
```
```   199
```
```   200
```
```   201 (*** Proving facts about div and mod using quorem ***)
```
```   202
```
```   203 Goal "[| b*q' + r'  <= b*q + r;  0 < b;  r < b |] \
```
```   204 \     ==> q' <= (q::nat)";
```
```   205 by (rtac leI 1);
```
```   206 by (stac less_iff_Suc_add 1);
```
```   207 by (auto_tac (claset(), simpset() addsimps [add_mult_distrib2]));
```
```   208 qed "unique_quotient_lemma";
```
```   209
```
```   210 Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |] \
```
```   211 \     ==> q = q'";
```
```   212 by (asm_full_simp_tac
```
```   213     (simpset() addsimps split_ifs @ [Divides.quorem_def]) 1);
```
```   214 by Auto_tac;
```
```   215 by (REPEAT
```
```   216     (blast_tac (claset() addIs [order_antisym]
```
```   217 			 addDs [order_eq_refl RS unique_quotient_lemma,
```
```   218 				sym]) 1));
```
```   219 qed "unique_quotient";
```
```   220
```
```   221 Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |] \
```
```   222 \     ==> r = r'";
```
```   223 by (subgoal_tac "q = q'" 1);
```
```   224 by (blast_tac (claset() addIs [unique_quotient]) 2);
```
```   225 by (asm_full_simp_tac (simpset() addsimps [Divides.quorem_def]) 1);
```
```   226 qed "unique_remainder";
```
```   227
```
```   228 Goal "0 < b ==> quorem ((a, b), (a div b, a mod b))";
```
```   229 by (cut_inst_tac [("m","a"),("n","b")] mod_div_equality 1);
```
```   230 by (auto_tac
```
```   231     (claset() addEs [sym],
```
```   232      simpset() addsimps mult_ac@[Divides.quorem_def]));
```
```   233 qed "quorem_div_mod";
```
```   234
```
```   235 Goal "[| quorem((a,b),(q,r));  0 < b |] ==> a div b = q";
```
```   236 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_quotient]) 1);
```
```   237 qed "quorem_div";
```
```   238
```
```   239 Goal "[| quorem((a,b),(q,r));  0 < b |] ==> a mod b = r";
```
```   240 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_remainder]) 1);
```
```   241 qed "quorem_mod";
```
```   242
```
```   243 (** A dividend of zero **)
```
```   244
```
```   245 Goal "0 div m = (0::nat)";
```
```   246 by (div_undefined_case_tac "m=0" 1);
```
```   247 by (Asm_simp_tac 1);
```
```   248 qed "div_0";
```
```   249
```
```   250 Goal "0 mod m = (0::nat)";
```
```   251 by (div_undefined_case_tac "m=0" 1);
```
```   252 by (Asm_simp_tac 1);
```
```   253 qed "mod_0";
```
```   254 Addsimps [div_0, mod_0];
```
```   255
```
```   256 (** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
```
```   257
```
```   258 Goal "[| quorem((b,c),(q,r));  0 < c |] \
```
```   259 \     ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))";
```
```   260 by (cut_inst_tac [("m", "a*r"), ("n","c")] mod_div_equality 1);
```
```   261 by (auto_tac
```
```   262     (claset(),
```
```   263      simpset() addsimps split_ifs@mult_ac@
```
```   264                         [Divides.quorem_def, add_mult_distrib2]));
```
```   265 val lemma = result();
```
```   266
```
```   267 Goal "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)";
```
```   268 by (div_undefined_case_tac "c = 0" 1);
```
```   269 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1);
```
```   270 qed "div_mult1_eq";
```
```   271
```
```   272 Goal "(a*b) mod c = a*(b mod c) mod (c::nat)";
```
```   273 by (div_undefined_case_tac "c = 0" 1);
```
```   274 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1);
```
```   275 qed "mod_mult1_eq";
```
```   276
```
```   277 Goal "(a*b) mod (c::nat) = ((a mod c) * b) mod c";
```
```   278 by (rtac trans 1);
```
```   279 by (res_inst_tac [("s","b*a mod c")] trans 1);
```
```   280 by (rtac mod_mult1_eq 2);
```
```   281 by (ALLGOALS (simp_tac (simpset() addsimps [mult_commute])));
```
```   282 qed "mod_mult1_eq'";
```
```   283
```
```   284 Goal "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c";
```
```   285 by (rtac (mod_mult1_eq' RS trans) 1);
```
```   286 by (rtac mod_mult1_eq 1);
```
```   287 qed "mod_mult_distrib_mod";
```
```   288
```
```   289 (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
```
```   290
```
```   291 Goal "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  0 < c |] \
```
```   292 \     ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))";
```
```   293 by (cut_inst_tac [("m", "ar+br"), ("n","c")] mod_div_equality 1);
```
```   294 by (auto_tac
```
```   295     (claset(),
```
```   296      simpset() addsimps split_ifs@mult_ac@
```
```   297                         [Divides.quorem_def, add_mult_distrib2]));
```
```   298 val lemma = result();
```
```   299
```
```   300 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
```
```   301 Goal "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)";
```
```   302 by (div_undefined_case_tac "c = 0" 1);
```
```   303 by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod]
```
```   304 			       MRS lemma RS quorem_div]) 1);
```
```   305 qed "div_add1_eq";
```
```   306
```
```   307 Goal "(a+b) mod (c::nat) = (a mod c + b mod c) mod c";
```
```   308 by (div_undefined_case_tac "c = 0" 1);
```
```   309 by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod]
```
```   310 			       MRS lemma RS quorem_mod]) 1);
```
```   311 qed "mod_add1_eq";
```
```   312
```
```   313
```
```   314 (*** proving  a div (b*c) = (a div b) div c ***)
```
```   315
```
```   316 (** first, a lemma to bound the remainder **)
```
```   317
```
```   318 Goal "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c";
```
```   319 by (cut_inst_tac [("m","q"),("n","c")] mod_less_divisor 1);
```
```   320 by (dres_inst_tac [("m","q mod c")] less_imp_Suc_add 2);
```
```   321 by Auto_tac;
```
```   322 by (eres_inst_tac [("P","%x. ?lhs < ?rhs x")] ssubst 1);
```
```   323 by (asm_simp_tac (simpset() addsimps [add_mult_distrib2]) 1);
```
```   324 val mod_lemma = result();
```
```   325
```
```   326 Goal "[| quorem ((a,b), (q,r));  0 < b;  0 < c |] \
```
```   327 \     ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))";
```
```   328 by (cut_inst_tac [("m", "q"), ("n","c")] mod_div_equality 1);
```
```   329 by (auto_tac
```
```   330     (claset(),
```
```   331      simpset() addsimps mult_ac@
```
```   332                         [Divides.quorem_def, add_mult_distrib2 RS sym,
```
```   333 			 mod_lemma]));
```
```   334 val lemma = result();
```
```   335
```
```   336 Goal "a div (b*c) = (a div b) div (c::nat)";
```
```   337 by (div_undefined_case_tac "b=0" 1);
```
```   338 by (div_undefined_case_tac "c=0" 1);
```
```   339 by (force_tac (claset(),
```
```   340 	       simpset() addsimps [quorem_div_mod RS lemma RS quorem_div]) 1);
```
```   341 qed "div_mult2_eq";
```
```   342
```
```   343 Goal "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)";
```
```   344 by (div_undefined_case_tac "b=0" 1);
```
```   345 by (div_undefined_case_tac "c=0" 1);
```
```   346 by (cut_inst_tac [("m", "a"), ("n","b")] mod_div_equality 1);
```
```   347 by (auto_tac (claset(),
```
```   348 	       simpset() addsimps [mult_commute,
```
```   349 				   quorem_div_mod RS lemma RS quorem_mod]));
```
```   350 qed "mod_mult2_eq";
```
```   351
```
```   352
```
```   353 (*** Cancellation of common factors in "div" ***)
```
```   354
```
```   355 Goal "[| (0::nat) < b;  0 < c |] ==> (c*a) div (c*b) = a div b";
```
```   356 by (stac div_mult2_eq 1);
```
```   357 by Auto_tac;
```
```   358 val lemma1 = result();
```
```   359
```
```   360 Goal "(0::nat) < c ==> (c*a) div (c*b) = a div b";
```
```   361 by (div_undefined_case_tac "b = 0" 1);
```
```   362 by (auto_tac
```
```   363     (claset(),
```
```   364      simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff,
```
```   365 			 lemma1, lemma2]));
```
```   366 qed "div_mult_mult1";
```
```   367
```
```   368 Goal "(0::nat) < c ==> (a*c) div (b*c) = a div b";
```
```   369 by (dtac div_mult_mult1 1);
```
```   370 by (auto_tac (claset(), simpset() addsimps [mult_commute]));
```
```   371 qed "div_mult_mult2";
```
```   372
```
```   373 Addsimps [div_mult_mult1, div_mult_mult2];
```
```   374
```
```   375
```
```   376 (*** Distribution of factors over "mod"
```
```   377
```
```   378 Could prove these as in Integ/IntDiv.ML, but we already have
```
```   379 mod_mult_distrib and mod_mult_distrib2 above!
```
```   380
```
```   381 Goal "(c*a) mod (c*b) = (c::nat) * (a mod b)";
```
```   382 qed "mod_mult_mult1";
```
```   383
```
```   384 Goal "(a*c) mod (b*c) = (a mod b) * (c::nat)";
```
```   385 qed "mod_mult_mult2";
```
```   386  ***)
```
```   387
```
```   388 (*** Further facts about div and mod ***)
```
```   389
```
```   390 Goal "m div 1 = m";
```
```   391 by (induct_tac "m" 1);
```
```   392 by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_geq])));
```
```   393 qed "div_1";
```
```   394 Addsimps [div_1];
```
```   395
```
```   396 Goal "0<n ==> n div n = (1::nat)";
```
```   397 by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
```
```   398 qed "div_self";
```
```   399 Addsimps [div_self];
```
```   400
```
```   401 Goal "0<n ==> (m+n) div n = Suc (m div n)";
```
```   402 by (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n)" 1);
```
```   403 by (stac (div_geq RS sym) 2);
```
```   404 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
```
```   405 qed "div_add_self2";
```
```   406
```
```   407 Goal "0<n ==> (n+m) div n = Suc (m div n)";
```
```   408 by (asm_simp_tac (simpset() addsimps [add_commute, div_add_self2]) 1);
```
```   409 qed "div_add_self1";
```
```   410
```
```   411 Goal "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n";
```
```   412 by (stac div_add1_eq 1);
```
```   413 by (stac div_mult1_eq 1);
```
```   414 by (Asm_simp_tac 1);
```
```   415 qed "div_mult_self1";
```
```   416
```
```   417 Goal "0<n ==> (m + n*k) div n = k + m div (n::nat)";
```
```   418 by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self1]) 1);
```
```   419 qed "div_mult_self2";
```
```   420
```
```   421 Addsimps [div_mult_self1, div_mult_self2];
```
```   422
```
```   423 (* Monotonicity of div in first argument *)
```
```   424 Goal "ALL m::nat. m <= n --> (m div k) <= (n div k)";
```
```   425 by (div_undefined_case_tac "k=0" 1);
```
```   426 by (induct_thm_tac nat_less_induct "n" 1);
```
```   427 by (Clarify_tac 1);
```
```   428 by (case_tac "n<k" 1);
```
```   429 (* 1  case n<k *)
```
```   430 by (Asm_simp_tac 1);
```
```   431 (* 2  case n >= k *)
```
```   432 by (case_tac "m<k" 1);
```
```   433 (* 2.1  case m<k *)
```
```   434 by (Asm_simp_tac 1);
```
```   435 (* 2.2  case m>=k *)
```
```   436 by (asm_simp_tac (simpset() addsimps [div_geq, diff_less, diff_le_mono]) 1);
```
```   437 qed_spec_mp "div_le_mono";
```
```   438
```
```   439 (* Antimonotonicity of div in second argument *)
```
```   440 Goal "!!m::nat. [| 0<m; m<=n |] ==> (k div n) <= (k div m)";
```
```   441 by (subgoal_tac "0<n" 1);
```
```   442  by (Asm_simp_tac 2);
```
```   443 by (induct_thm_tac nat_less_induct "k" 1);
```
```   444 by (rename_tac "k" 1);
```
```   445 by (case_tac "k<n" 1);
```
```   446  by (Asm_simp_tac 1);
```
```   447 by (subgoal_tac "~(k<m)" 1);
```
```   448  by (Asm_simp_tac 2);
```
```   449 by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
```
```   450 by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
```
```   451  by (REPEAT (ares_tac [div_le_mono,diff_le_mono2] 2));
```
```   452 by (rtac le_trans 1);
```
```   453 by (Asm_simp_tac 1);
```
```   454 by (asm_simp_tac (simpset() addsimps [diff_less]) 1);
```
```   455 qed "div_le_mono2";
```
```   456
```
```   457 Goal "m div n <= (m::nat)";
```
```   458 by (div_undefined_case_tac "n=0" 1);
```
```   459 by (subgoal_tac "m div n <= m div 1" 1);
```
```   460 by (Asm_full_simp_tac 1);
```
```   461 by (rtac div_le_mono2 1);
```
```   462 by (ALLGOALS Asm_simp_tac);
```
```   463 qed "div_le_dividend";
```
```   464 Addsimps [div_le_dividend];
```
```   465
```
```   466 (* Similar for "less than" *)
```
```   467 Goal "!!n::nat. 1<n ==> (0 < m) --> (m div n < m)";
```
```   468 by (induct_thm_tac nat_less_induct "m" 1);
```
```   469 by (rename_tac "m" 1);
```
```   470 by (case_tac "m<n" 1);
```
```   471  by (Asm_full_simp_tac 1);
```
```   472 by (subgoal_tac "0<n" 1);
```
```   473  by (Asm_simp_tac 2);
```
```   474 by (asm_full_simp_tac (simpset() addsimps [div_geq]) 1);
```
```   475 by (case_tac "n<m" 1);
```
```   476  by (subgoal_tac "(m-n) div n < (m-n)" 1);
```
```   477   by (REPEAT (ares_tac [impI,less_trans_Suc] 1));
```
```   478   by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
```
```   479  by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
```
```   480 (* case n=m *)
```
```   481 by (subgoal_tac "m=n" 1);
```
```   482  by (Asm_simp_tac 2);
```
```   483 by (Asm_simp_tac 1);
```
```   484 qed_spec_mp "div_less_dividend";
```
```   485 Addsimps [div_less_dividend];
```
```   486
```
```   487 (*** Further facts about mod (mainly for the mutilated chess board ***)
```
```   488
```
```   489 Goal "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
```
```   490 by (div_undefined_case_tac "n=0" 1);
```
```   491 by (induct_thm_tac nat_less_induct "m" 1);
```
```   492 by (case_tac "Suc(na)<n" 1);
```
```   493 (* case Suc(na) < n *)
```
```   494 by (forward_tac [lessI RS less_trans] 1
```
```   495     THEN asm_simp_tac (simpset() addsimps [less_not_refl3]) 1);
```
```   496 (* case n <= Suc(na) *)
```
```   497 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, le_Suc_eq,
```
```   498 					   mod_geq]) 1);
```
```   499 by (auto_tac (claset(),
```
```   500 	      simpset() addsimps [Suc_diff_le, diff_less, le_mod_geq]));
```
```   501 qed "mod_Suc";
```
```   502
```
```   503
```
```   504 (************************************************)
```
```   505 (** Divides Relation                           **)
```
```   506 (************************************************)
```
```   507
```
```   508 Goalw [dvd_def] "m dvd (0::nat)";
```
```   509 by (blast_tac (claset() addIs [mult_0_right RS sym]) 1);
```
```   510 qed "dvd_0_right";
```
```   511 AddIffs [dvd_0_right];
```
```   512
```
```   513 Goalw [dvd_def] "0 dvd m ==> m = (0::nat)";
```
```   514 by Auto_tac;
```
```   515 qed "dvd_0_left";
```
```   516
```
```   517 Goalw [dvd_def] "1 dvd (k::nat)";
```
```   518 by (Simp_tac 1);
```
```   519 qed "dvd_1_left";
```
```   520 AddIffs [dvd_1_left];
```
```   521
```
```   522 Goalw [dvd_def] "m dvd (m::nat)";
```
```   523 by (blast_tac (claset() addIs [mult_1_right RS sym]) 1);
```
```   524 qed "dvd_refl";
```
```   525 Addsimps [dvd_refl];
```
```   526
```
```   527 Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd (p::nat)";
```
```   528 by (blast_tac (claset() addIs [mult_assoc] ) 1);
```
```   529 qed "dvd_trans";
```
```   530
```
```   531 Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m = (n::nat)";
```
```   532 by (force_tac (claset() addDs [mult_eq_self_implies_10],
```
```   533 	       simpset() addsimps [mult_assoc, mult_eq_1_iff]) 1);
```
```   534 qed "dvd_anti_sym";
```
```   535
```
```   536 Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)";
```
```   537 by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1);
```
```   538 qed "dvd_add";
```
```   539
```
```   540 Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)";
```
```   541 by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1);
```
```   542 qed "dvd_diff";
```
```   543
```
```   544 Goal "[| k dvd m-n; k dvd n; n<=m |] ==> k dvd (m::nat)";
```
```   545 by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
```
```   546 by (blast_tac (claset() addIs [dvd_add]) 1);
```
```   547 qed "dvd_diffD";
```
```   548
```
```   549 Goalw [dvd_def] "k dvd n ==> k dvd (m*n :: nat)";
```
```   550 by (blast_tac (claset() addIs [mult_left_commute]) 1);
```
```   551 qed "dvd_mult";
```
```   552
```
```   553 Goal "k dvd m ==> k dvd (m*n :: nat)";
```
```   554 by (stac mult_commute 1);
```
```   555 by (etac dvd_mult 1);
```
```   556 qed "dvd_mult2";
```
```   557
```
```   558 (* k dvd (m*k) *)
```
```   559 AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
```
```   560
```
```   561 Goal "(k dvd n + k) = (k dvd (n::nat))";
```
```   562 by (rtac iffI 1);
```
```   563 by (etac dvd_add 2);
```
```   564 by (rtac dvd_refl 2);
```
```   565 by (subgoal_tac "n = (n+k)-k" 1);
```
```   566 by  (Simp_tac 2);
```
```   567 by (etac ssubst 1);
```
```   568 by (etac dvd_diff 1);
```
```   569 by (rtac dvd_refl 1);
```
```   570 qed "dvd_reduce";
```
```   571
```
```   572 Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n; 0<n |] ==> f dvd m mod n";
```
```   573 by (Clarify_tac 1);
```
```   574 by (Full_simp_tac 1);
```
```   575 by (res_inst_tac
```
```   576     [("x", "(((k div ka)*ka + k mod ka) - ((f*k) div (f*ka)) * ka)")]
```
```   577     exI 1);
```
```   578 by (asm_simp_tac
```
```   579     (simpset() addsimps [diff_mult_distrib2, mod_mult_distrib2 RS sym,
```
```   580 			 add_mult_distrib2]) 1);
```
```   581 qed "dvd_mod";
```
```   582
```
```   583 Goal "[| (k::nat) dvd m mod n;  k dvd n |] ==> k dvd m";
```
```   584 by (subgoal_tac "k dvd (m div n)*n + m mod n" 1);
```
```   585 by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2);
```
```   586 by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
```
```   587 qed "dvd_mod_imp_dvd";
```
```   588
```
```   589 Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n";
```
```   590 by (div_undefined_case_tac "n=0" 1);
```
```   591 by (Clarify_tac 1);
```
```   592 by (Full_simp_tac 1);
```
```   593 by (rename_tac "j" 1);
```
```   594 by (res_inst_tac
```
```   595     [("x", "(((k div j)*j + k mod j) - ((f*k) div (f*j)) * j)")]
```
```   596     exI 1);
```
```   597 by (asm_simp_tac
```
```   598     (simpset() addsimps [diff_mult_distrib2, mod_mult_distrib2 RS sym,
```
```   599 			 add_mult_distrib2]) 1);
```
```   600 qed "dvd_mod";
```
```   601
```
```   602 Goal "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)";
```
```   603 by (blast_tac (claset() addIs [dvd_mod_imp_dvd, dvd_mod]) 1);
```
```   604 qed "dvd_mod_iff";
```
```   605
```
```   606 Goalw [dvd_def]  "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n";
```
```   607 by (etac exE 1);
```
```   608 by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
```
```   609 qed "dvd_mult_cancel";
```
```   610
```
```   611 Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)";
```
```   612 by (Clarify_tac 1);
```
```   613 by (res_inst_tac [("x","k*ka")] exI 1);
```
```   614 by (asm_simp_tac (simpset() addsimps mult_ac) 1);
```
```   615 qed "mult_dvd_mono";
```
```   616
```
```   617 Goalw [dvd_def] "(i*j :: nat) dvd k ==> i dvd k";
```
```   618 by (full_simp_tac (simpset() addsimps [mult_assoc]) 1);
```
```   619 by (Blast_tac 1);
```
```   620 qed "dvd_mult_left";
```
```   621
```
```   622 Goalw [dvd_def] "[| k dvd n; 0 < n |] ==> k <= (n::nat)";
```
```   623 by (Clarify_tac 1);
```
```   624 by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff])));
```
```   625 by (etac conjE 1);
```
```   626 by (rtac le_trans 1);
```
```   627 by (rtac (le_refl RS mult_le_mono) 2);
```
```   628 by (etac Suc_leI 2);
```
```   629 by (Simp_tac 1);
```
```   630 qed "dvd_imp_le";
```
```   631
```
```   632 Goalw [dvd_def] "!!k::nat. (k dvd n) = (n mod k = 0)";
```
```   633 by (div_undefined_case_tac "k=0" 1);
```
```   634 by Safe_tac;
```
```   635 by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
```
```   636 by (res_inst_tac [("t","n"),("n1","k")] (mod_div_equality RS subst) 1);
```
```   637 by (stac mult_commute 1);
```
```   638 by (Asm_simp_tac 1);
```
```   639 qed "dvd_eq_mod_eq_0";
```
```   640
```
```   641 Goal "(m mod d = 0) = (EX q::nat. m = d*q)";
```
```   642 by (auto_tac (claset(),
```
```   643      simpset() addsimps [dvd_eq_mod_eq_0 RS sym, dvd_def]));
```
```   644 qed "mod_eq_0_iff";
```
```   645 AddSDs [mod_eq_0_iff RS iffD1];
```
```   646
```
```   647 (*Loses information, namely we also have r<d provided d is nonzero*)
```
```   648 Goal "(m mod d = r) ==> EX q::nat. m = r + q*d";
```
```   649 by (cut_inst_tac [("m","m")] mod_div_equality 1);
```
```   650 by (full_simp_tac (simpset() addsimps add_ac) 1);
```
```   651 by (blast_tac (claset() addIs [sym]) 1);
```
```   652 qed "mod_eqD";
```
```   653
```