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--
tidied; added lemma restrict_to_left
     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";