src/HOL/Divides.ML
 author paulson Thu Sep 23 13:06:31 1999 +0200 (1999-09-23) changeset 7584 5be4bb8e4e3f parent 7499 23e090051cb8 child 8393 c7772d3787c3 permissions -rw-r--r--
```     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 val 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";
```
```    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";
```
```    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
```
```    52 Goal "~ m < (n::nat) ==> m mod n = (m-n) mod n";
```
```    53 by (div_undefined_case_tac "n=0" 1);
```
```    54 by (rtac (mod_eq RS wf_less_trans) 1);
```
```    55 by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
```
```    56 qed "mod_geq";
```
```    57
```
```    58 (*Avoids the ugly ~m<n above*)
```
```    59 Goal "(n::nat) <= m ==> m mod n = (m-n) mod n";
```
```    60 by (asm_simp_tac (simpset() addsimps [mod_geq, not_less_iff_le]) 1);
```
```    61 qed "le_mod_geq";
```
```    62
```
```    63 Goal "m mod (n::nat) = (if m<n then m else (m-n) mod n)";
```
```    64 by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1);
```
```    65 qed "mod_if";
```
```    66
```
```    67 Goal "m mod 1 = 0";
```
```    68 by (induct_tac "m" 1);
```
```    69 by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_less, mod_geq])));
```
```    70 qed "mod_1";
```
```    71 Addsimps [mod_1];
```
```    72
```
```    73 Goal "n mod n = 0";
```
```    74 by (div_undefined_case_tac "n=0" 1);
```
```    75 by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1);
```
```    76 qed "mod_self";
```
```    77
```
```    78 Goal "(m+n) mod n = m mod (n::nat)";
```
```    79 by (subgoal_tac "(n + m) mod n = (n+m-n) mod n" 1);
```
```    80 by (stac (mod_geq RS sym) 2);
```
```    81 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
```
```    82 qed "mod_add_self2";
```
```    83
```
```    84 Goal "(n+m) mod n = m mod (n::nat)";
```
```    85 by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_self2]) 1);
```
```    86 qed "mod_add_self1";
```
```    87
```
```    88 Goal "(m + k*n) mod n = m mod (n::nat)";
```
```    89 by (induct_tac "k" 1);
```
```    90 by (ALLGOALS
```
```    91     (asm_simp_tac
```
```    92      (simpset() addsimps [read_instantiate [("y","n")] add_left_commute,
```
```    93 			  mod_add_self1])));
```
```    94 qed "mod_mult_self1";
```
```    95
```
```    96 Goal "(m + n*k) mod n = m mod (n::nat)";
```
```    97 by (asm_simp_tac (simpset() addsimps [mult_commute, mod_mult_self1]) 1);
```
```    98 qed "mod_mult_self2";
```
```    99
```
```   100 Addsimps [mod_mult_self1, mod_mult_self2];
```
```   101
```
```   102 Goal "(m mod n) * (k::nat) = (m*k) mod (n*k)";
```
```   103 by (div_undefined_case_tac "n=0" 1);
```
```   104 by (div_undefined_case_tac "k=0" 1);
```
```   105 by (res_inst_tac [("n","m")] less_induct 1);
```
```   106 by (stac mod_if 1);
```
```   107 by (Asm_simp_tac 1);
```
```   108 by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq,
```
```   109 				      diff_less, diff_mult_distrib]) 1);
```
```   110 qed "mod_mult_distrib";
```
```   111
```
```   112 Goal "(k::nat) * (m mod n) = (k*m) mod (k*n)";
```
```   113 by (asm_simp_tac
```
```   114     (simpset() addsimps [read_instantiate [("m","k")] mult_commute,
```
```   115 			 mod_mult_distrib]) 1);
```
```   116 qed "mod_mult_distrib2";
```
```   117
```
```   118 Goal "(m*n) mod n = 0";
```
```   119 by (div_undefined_case_tac "n=0" 1);
```
```   120 by (induct_tac "m" 1);
```
```   121 by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
```
```   122 by (rename_tac "k" 1);
```
```   123 by (cut_inst_tac [("m","k*n"),("n","n")] mod_add_self2 1);
```
```   124 by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
```
```   125 qed "mod_mult_self_is_0";
```
```   126
```
```   127 Goal "(n*m) mod n = 0";
```
```   128 by (simp_tac (simpset() addsimps [mult_commute, mod_mult_self_is_0]) 1);
```
```   129 qed "mod_mult_self1_is_0";
```
```   130 Addsimps [mod_mult_self_is_0, mod_mult_self1_is_0];
```
```   131
```
```   132
```
```   133 (*** Quotient ***)
```
```   134
```
```   135 Goal "m<n ==> m div n = 0";
```
```   136 by (rtac (div_eq RS wf_less_trans) 1);
```
```   137 by (Asm_simp_tac 1);
```
```   138 qed "div_less";
```
```   139
```
```   140 Goal "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)";
```
```   141 by (rtac (div_eq RS wf_less_trans) 1);
```
```   142 by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
```
```   143 qed "div_geq";
```
```   144
```
```   145 (*Avoids the ugly ~m<n above*)
```
```   146 Goal "[| 0<n;  n<=m |] ==> m div n = Suc((m-n) div n)";
```
```   147 by (asm_simp_tac (simpset() addsimps [div_geq, not_less_iff_le]) 1);
```
```   148 qed "le_div_geq";
```
```   149
```
```   150 Goal "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))";
```
```   151 by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1);
```
```   152 qed "div_if";
```
```   153
```
```   154
```
```   155 (*Main Result about quotient and remainder.*)
```
```   156 Goal "(m div n)*n + m mod n = (m::nat)";
```
```   157 by (div_undefined_case_tac "n=0" 1);
```
```   158 by (res_inst_tac [("n","m")] less_induct 1);
```
```   159 by (stac mod_if 1);
```
```   160 by (ALLGOALS (asm_simp_tac
```
```   161 	      (simpset() addsimps [add_assoc, div_less, div_geq,
```
```   162 				   add_diff_inverse, diff_less])));
```
```   163 qed "mod_div_equality";
```
```   164
```
```   165 (* a simple rearrangement of mod_div_equality: *)
```
```   166 Goal "(n::nat) * (m div n) = m - (m mod n)";
```
```   167 by (cut_inst_tac [("m","m"),("n","n")] mod_div_equality 1);
```
```   168 by (EVERY1[etac subst, simp_tac (simpset() addsimps mult_ac),
```
```   169            K(IF_UNSOLVED no_tac)]);
```
```   170 qed "mult_div_cancel";
```
```   171
```
```   172 Goal "m div 1 = m";
```
```   173 by (induct_tac "m" 1);
```
```   174 by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_less, div_geq])));
```
```   175 qed "div_1";
```
```   176 Addsimps [div_1];
```
```   177
```
```   178 Goal "0<n ==> n div n = 1";
```
```   179 by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1);
```
```   180 qed "div_self";
```
```   181
```
```   182
```
```   183 Goal "0<n ==> (m+n) div n = Suc (m div n)";
```
```   184 by (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n)" 1);
```
```   185 by (stac (div_geq RS sym) 2);
```
```   186 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
```
```   187 qed "div_add_self2";
```
```   188
```
```   189 Goal "0<n ==> (n+m) div n = Suc (m div n)";
```
```   190 by (asm_simp_tac (simpset() addsimps [add_commute, div_add_self2]) 1);
```
```   191 qed "div_add_self1";
```
```   192
```
```   193 Goal "!!n. 0<n ==> (m + k*n) div n = k + m div n";
```
```   194 by (induct_tac "k" 1);
```
```   195 by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [div_add_self1])));
```
```   196 qed "div_mult_self1";
```
```   197
```
```   198 Goal "0<n ==> (m + n*k) div n = k + m div n";
```
```   199 by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self1]) 1);
```
```   200 qed "div_mult_self2";
```
```   201
```
```   202 Addsimps [div_mult_self1, div_mult_self2];
```
```   203
```
```   204 (** A dividend of zero **)
```
```   205
```
```   206 Goal "0 div m = 0";
```
```   207 by (div_undefined_case_tac "m=0" 1);
```
```   208 by (asm_simp_tac (simpset() addsimps [div_less]) 1);
```
```   209 qed "div_0";
```
```   210
```
```   211 Goal "0 mod m = 0";
```
```   212 by (div_undefined_case_tac "m=0" 1);
```
```   213 by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
```
```   214 qed "mod_0";
```
```   215 Addsimps [div_0, mod_0];
```
```   216
```
```   217 (* Monotonicity of div in first argument *)
```
```   218 Goal "ALL m::nat. m <= n --> (m div k) <= (n div k)";
```
```   219 by (div_undefined_case_tac "k=0" 1);
```
```   220 by (res_inst_tac [("n","n")] less_induct 1);
```
```   221 by (Clarify_tac 1);
```
```   222 by (case_tac "n<k" 1);
```
```   223 (* 1  case n<k *)
```
```   224 by (asm_simp_tac (simpset() addsimps [div_less]) 1);
```
```   225 (* 2  case n >= k *)
```
```   226 by (case_tac "m<k" 1);
```
```   227 (* 2.1  case m<k *)
```
```   228 by (asm_simp_tac (simpset() addsimps [div_less]) 1);
```
```   229 (* 2.2  case m>=k *)
```
```   230 by (asm_simp_tac (simpset() addsimps [div_geq, diff_less, diff_le_mono]) 1);
```
```   231 qed_spec_mp "div_le_mono";
```
```   232
```
```   233 (* Antimonotonicity of div in second argument *)
```
```   234 Goal "[| 0<m; m<=n |] ==> (k div n) <= (k div m)";
```
```   235 by (subgoal_tac "0<n" 1);
```
```   236  by (Asm_simp_tac 2);
```
```   237 by (res_inst_tac [("n","k")] less_induct 1);
```
```   238 by (rename_tac "k" 1);
```
```   239 by (case_tac "k<n" 1);
```
```   240  by (asm_simp_tac (simpset() addsimps [div_less]) 1);
```
```   241 by (subgoal_tac "~(k<m)" 1);
```
```   242  by (Asm_simp_tac 2);
```
```   243 by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
```
```   244 by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
```
```   245  by (REPEAT (ares_tac [div_le_mono,diff_le_mono2] 2));
```
```   246 by (rtac le_trans 1);
```
```   247 by (Asm_simp_tac 1);
```
```   248 by (asm_simp_tac (simpset() addsimps [diff_less]) 1);
```
```   249 qed "div_le_mono2";
```
```   250
```
```   251 Goal "m div n <= (m::nat)";
```
```   252 by (div_undefined_case_tac "n=0" 1);
```
```   253 by (subgoal_tac "m div n <= m div 1" 1);
```
```   254 by (Asm_full_simp_tac 1);
```
```   255 by (rtac div_le_mono2 1);
```
```   256 by (ALLGOALS Asm_simp_tac);
```
```   257 qed "div_le_dividend";
```
```   258 Addsimps [div_le_dividend];
```
```   259
```
```   260 (* Similar for "less than" *)
```
```   261 Goal "1<n ==> (0 < m) --> (m div n < m)";
```
```   262 by (res_inst_tac [("n","m")] less_induct 1);
```
```   263 by (rename_tac "m" 1);
```
```   264 by (case_tac "m<n" 1);
```
```   265  by (asm_full_simp_tac (simpset() addsimps [div_less]) 1);
```
```   266 by (subgoal_tac "0<n" 1);
```
```   267  by (Asm_simp_tac 2);
```
```   268 by (asm_full_simp_tac (simpset() addsimps [div_geq]) 1);
```
```   269 by (case_tac "n<m" 1);
```
```   270  by (subgoal_tac "(m-n) div n < (m-n)" 1);
```
```   271   by (REPEAT (ares_tac [impI,less_trans_Suc] 1));
```
```   272   by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
```
```   273  by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
```
```   274 (* case n=m *)
```
```   275 by (subgoal_tac "m=n" 1);
```
```   276  by (Asm_simp_tac 2);
```
```   277 by (asm_simp_tac (simpset() addsimps [div_less]) 1);
```
```   278 qed_spec_mp "div_less_dividend";
```
```   279 Addsimps [div_less_dividend];
```
```   280
```
```   281 (*** Further facts about mod (mainly for the mutilated chess board ***)
```
```   282
```
```   283 Goal "0<n ==> Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
```
```   284 by (res_inst_tac [("n","m")] less_induct 1);
```
```   285 by (excluded_middle_tac "Suc(na)<n" 1);
```
```   286 (* case Suc(na) < n *)
```
```   287 by (forward_tac [lessI RS less_trans] 2);
```
```   288 by (asm_simp_tac (simpset() addsimps [mod_less, less_not_refl3]) 2);
```
```   289 (* case n <= Suc(na) *)
```
```   290 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, le_Suc_eq,
```
```   291 					   mod_geq]) 1);
```
```   292 by (etac disjE 1);
```
```   293  by (asm_simp_tac (simpset() addsimps [mod_less]) 2);
```
```   294 by (asm_simp_tac (simpset() addsimps [Suc_diff_le, diff_less,
```
```   295 				      le_mod_geq]) 1);
```
```   296 qed "mod_Suc";
```
```   297
```
```   298 Goal "0<n ==> m mod n < n";
```
```   299 by (res_inst_tac [("n","m")] less_induct 1);
```
```   300 by (case_tac "na<n" 1);
```
```   301 (*case n le na*)
```
```   302 by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 2);
```
```   303 (*case na<n*)
```
```   304 by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
```
```   305 qed "mod_less_divisor";
```
```   306
```
```   307
```
```   308 (** Evens and Odds **)
```
```   309
```
```   310 (*With less_zeroE, causes case analysis on b<2*)
```
```   311 AddSEs [less_SucE];
```
```   312
```
```   313 Goal "b<2 ==> (k mod 2 = b) | (k mod 2 = (if b=1 then 0 else 1))";
```
```   314 by (subgoal_tac "k mod 2 < 2" 1);
```
```   315 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
```
```   316 by (Asm_simp_tac 1);
```
```   317 by Safe_tac;
```
```   318 qed "mod2_cases";
```
```   319
```
```   320 Goal "Suc(Suc(m)) mod 2 = m mod 2";
```
```   321 by (subgoal_tac "m mod 2 < 2" 1);
```
```   322 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
```
```   323 by Safe_tac;
```
```   324 by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc])));
```
```   325 qed "mod2_Suc_Suc";
```
```   326 Addsimps [mod2_Suc_Suc];
```
```   327
```
```   328 Goal "(0 < m mod 2) = (m mod 2 = 1)";
```
```   329 by (subgoal_tac "m mod 2 < 2" 1);
```
```   330 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
```
```   331 by Auto_tac;
```
```   332 qed "mod2_gr_0";
```
```   333 Addsimps [mod2_gr_0];
```
```   334
```
```   335 Goal "(m+m) mod 2 = 0";
```
```   336 by (induct_tac "m" 1);
```
```   337 by (simp_tac (simpset() addsimps [mod_less]) 1);
```
```   338 by (Asm_simp_tac 1);
```
```   339 qed "mod2_add_self_eq_0";
```
```   340 Addsimps [mod2_add_self_eq_0];
```
```   341
```
```   342 Goal "((m+m)+n) mod 2 = n mod 2";
```
```   343 by (induct_tac "m" 1);
```
```   344 by (simp_tac (simpset() addsimps [mod_less]) 1);
```
```   345 by (Asm_simp_tac 1);
```
```   346 qed "mod2_add_self";
```
```   347 Addsimps [mod2_add_self];
```
```   348
```
```   349 (*Restore the default*)
```
```   350 Delrules [less_SucE];
```
```   351
```
```   352 (*** More division laws ***)
```
```   353
```
```   354 Goal "0<n ==> (m*n) div n = m";
```
```   355 by (cut_inst_tac [("m", "m*n"),("n","n")] mod_div_equality 1);
```
```   356 by (asm_full_simp_tac (simpset() addsimps [mod_mult_self_is_0]) 1);
```
```   357 qed "div_mult_self_is_m";
```
```   358
```
```   359 Goal "0<n ==> (n*m) div n = m";
```
```   360 by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self_is_m]) 1);
```
```   361 qed "div_mult_self1_is_m";
```
```   362 Addsimps [div_mult_self_is_m, div_mult_self1_is_m];
```
```   363
```
```   364 (*Cancellation law for division*)
```
```   365 Goal "0<k ==> (k*m) div (k*n) = m div n";
```
```   366 by (div_undefined_case_tac "n=0" 1);
```
```   367 by (res_inst_tac [("n","m")] less_induct 1);
```
```   368 by (case_tac "na<n" 1);
```
```   369 by (asm_simp_tac (simpset() addsimps [div_less, zero_less_mult_iff,
```
```   370 				      mult_less_mono2]) 1);
```
```   371 by (subgoal_tac "~ k*na < k*n" 1);
```
```   372 by (asm_simp_tac
```
```   373      (simpset() addsimps [zero_less_mult_iff, div_geq,
```
```   374 			  diff_mult_distrib2 RS sym, diff_less]) 1);
```
```   375 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le,
```
```   376                                           le_refl RS mult_le_mono]) 1);
```
```   377 qed "div_cancel";
```
```   378 Addsimps [div_cancel];
```
```   379
```
```   380 (*mod_mult_distrib2 above is the counterpart for remainder*)
```
```   381
```
```   382
```
```   383 (************************************************)
```
```   384 (** Divides Relation                           **)
```
```   385 (************************************************)
```
```   386
```
```   387 Goalw [dvd_def] "m dvd 0";
```
```   388 by (blast_tac (claset() addIs [mult_0_right RS sym]) 1);
```
```   389 qed "dvd_0_right";
```
```   390 AddIffs [dvd_0_right];
```
```   391
```
```   392 Goalw [dvd_def] "0 dvd m ==> m = 0";
```
```   393 by Auto_tac;
```
```   394 qed "dvd_0_left";
```
```   395
```
```   396 Goalw [dvd_def] "1 dvd k";
```
```   397 by (Simp_tac 1);
```
```   398 qed "dvd_1_left";
```
```   399 AddIffs [dvd_1_left];
```
```   400
```
```   401 Goalw [dvd_def] "m dvd (m::nat)";
```
```   402 by (blast_tac (claset() addIs [mult_1_right RS sym]) 1);
```
```   403 qed "dvd_refl";
```
```   404 Addsimps [dvd_refl];
```
```   405
```
```   406 Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd (p::nat)";
```
```   407 by (blast_tac (claset() addIs [mult_assoc] ) 1);
```
```   408 qed "dvd_trans";
```
```   409
```
```   410 Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m = (n::nat)";
```
```   411 by (force_tac (claset() addDs [mult_eq_self_implies_10],
```
```   412 	       simpset() addsimps [mult_assoc, mult_eq_1_iff]) 1);
```
```   413 qed "dvd_anti_sym";
```
```   414
```
```   415 Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)";
```
```   416 by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1);
```
```   417 qed "dvd_add";
```
```   418
```
```   419 Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)";
```
```   420 by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1);
```
```   421 qed "dvd_diff";
```
```   422
```
```   423 Goal "[| k dvd (m-n); k dvd n; n<=m |] ==> k dvd (m::nat)";
```
```   424 by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
```
```   425 by (blast_tac (claset() addIs [dvd_add]) 1);
```
```   426 qed "dvd_diffD";
```
```   427
```
```   428 Goalw [dvd_def] "k dvd n ==> k dvd (m*n :: nat)";
```
```   429 by (blast_tac (claset() addIs [mult_left_commute]) 1);
```
```   430 qed "dvd_mult";
```
```   431
```
```   432 Goal "k dvd m ==> k dvd (m*n :: nat)";
```
```   433 by (stac mult_commute 1);
```
```   434 by (etac dvd_mult 1);
```
```   435 qed "dvd_mult2";
```
```   436
```
```   437 (* k dvd (m*k) *)
```
```   438 AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
```
```   439
```
```   440 Goal "k dvd (n + k) = k dvd (n::nat)";
```
```   441 by (rtac iffI 1);
```
```   442 by (etac dvd_add 2);
```
```   443 by (rtac dvd_refl 2);
```
```   444 by (subgoal_tac "n = (n+k)-k" 1);
```
```   445 by  (Simp_tac 2);
```
```   446 by (etac ssubst 1);
```
```   447 by (etac dvd_diff 1);
```
```   448 by (rtac dvd_refl 1);
```
```   449 qed "dvd_reduce";
```
```   450
```
```   451 Goalw [dvd_def] "[| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
```
```   452 by (Clarify_tac 1);
```
```   453 by (Full_simp_tac 1);
```
```   454 by (res_inst_tac
```
```   455     [("x", "(((k div ka)*ka + k mod ka) - ((f*k) div (f*ka)) * ka)")]
```
```   456     exI 1);
```
```   457 by (asm_simp_tac
```
```   458     (simpset() addsimps [diff_mult_distrib2, mod_mult_distrib2 RS sym,
```
```   459 			 add_mult_distrib2]) 1);
```
```   460 qed "dvd_mod";
```
```   461
```
```   462 Goal "[| (k::nat) dvd (m mod n);  k dvd n |] ==> k dvd m";
```
```   463 by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1);
```
```   464 by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2);
```
```   465 by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
```
```   466 qed "dvd_mod_imp_dvd";
```
```   467
```
```   468 Goalw [dvd_def]  "!!k::nat. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
```
```   469 by (etac exE 1);
```
```   470 by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
```
```   471 by (Blast_tac 1);
```
```   472 qed "dvd_mult_cancel";
```
```   473
```
```   474 Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> (i*j) dvd (m*n :: nat)";
```
```   475 by (Clarify_tac 1);
```
```   476 by (res_inst_tac [("x","k*ka")] exI 1);
```
```   477 by (asm_simp_tac (simpset() addsimps mult_ac) 1);
```
```   478 qed "mult_dvd_mono";
```
```   479
```
```   480 Goalw [dvd_def] "(i*j :: nat) dvd k ==> i dvd k";
```
```   481 by (full_simp_tac (simpset() addsimps [mult_assoc]) 1);
```
```   482 by (Blast_tac 1);
```
```   483 qed "dvd_mult_left";
```
```   484
```
```   485 Goalw [dvd_def] "[| k dvd n; 0 < n |] ==> k <= n";
```
```   486 by (Clarify_tac 1);
```
```   487 by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff])));
```
```   488 by (etac conjE 1);
```
```   489 by (rtac le_trans 1);
```
```   490 by (rtac (le_refl RS mult_le_mono) 2);
```
```   491 by (etac Suc_leI 2);
```
```   492 by (Simp_tac 1);
```
```   493 qed "dvd_imp_le";
```
```   494
```
```   495 Goalw [dvd_def] "(k dvd n) = (n mod k = 0)";
```
```   496 by (div_undefined_case_tac "k=0" 1);
```
```   497 by Safe_tac;
```
```   498 by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
```
```   499 by (res_inst_tac [("t","n"),("n1","k")] (mod_div_equality RS subst) 1);
```
```   500 by (stac mult_commute 1);
```
```   501 by (Asm_simp_tac 1);
```
```   502 qed "dvd_eq_mod_eq_0";
```