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