src/HOL/Divides.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5983 79e301a6a51b
child 6073 fba734ba6894
permissions -rw-r--r--
tidying
     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 (Simp_tac 2);
   193 by (res_inst_tac [("n","k")] less_induct 1);
   194 by (Simp_tac 1);
   195 by (rename_tac "k" 1);
   196 by (case_tac "k<n" 1);
   197  by (asm_simp_tac (simpset() addsimps [div_less]) 1);
   198 by (subgoal_tac "~(k<m)" 1);
   199  by (Simp_tac 2);
   200 by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
   201 by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
   202 by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 2));
   203 by (rtac le_trans 1);
   204 by (Asm_simp_tac 1);
   205 by (asm_simp_tac (simpset() addsimps [diff_less]) 1);
   206 qed "div_le_mono2";
   207 
   208 Goal "0<n ==> m div n <= m";
   209 by (subgoal_tac "m div n <= m div 1" 1);
   210 by (Asm_full_simp_tac 1);
   211 by (rtac div_le_mono2 1);
   212 by (ALLGOALS Simp_tac);
   213 qed "div_le_dividend";
   214 Addsimps [div_le_dividend];
   215 
   216 (* Similar for "less than" *)
   217 Goal "1<n ==> (0 < m) --> (m div n < m)";
   218 by (res_inst_tac [("n","m")] less_induct 1);
   219 by (Simp_tac 1);
   220 by (rename_tac "m" 1);
   221 by (case_tac "m<n" 1);
   222  by (asm_full_simp_tac (simpset() addsimps [div_less]) 1);
   223 by (subgoal_tac "0<n" 1);
   224  by (Simp_tac 2);
   225 by (asm_full_simp_tac (simpset() addsimps [div_geq]) 1);
   226 by (case_tac "n<m" 1);
   227  by (subgoal_tac "(m-n) div n < (m-n)" 1);
   228   by (REPEAT (ares_tac [impI,less_trans_Suc] 1));
   229   by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
   230  by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
   231 (* case n=m *)
   232 by (subgoal_tac "m=n" 1);
   233  by (Simp_tac 2);
   234 by (asm_simp_tac (simpset() addsimps [div_less]) 1);
   235 qed_spec_mp "div_less_dividend";
   236 Addsimps [div_less_dividend];
   237 
   238 (*** Further facts about mod (mainly for the mutilated chess board ***)
   239 
   240 Goal "0<n ==> Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
   241 by (res_inst_tac [("n","m")] less_induct 1);
   242 by (excluded_middle_tac "Suc(na)<n" 1);
   243 (* case Suc(na) < n *)
   244 by (forward_tac [lessI RS less_trans] 2);
   245 by (asm_simp_tac (simpset() addsimps [mod_less, less_not_refl3]) 2);
   246 (* case n <= Suc(na) *)
   247 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, le_Suc_eq, 
   248 					   mod_geq]) 1);
   249 by (etac disjE 1);
   250  by (asm_simp_tac (simpset() addsimps [mod_less]) 2);
   251 by (asm_simp_tac (simpset() addsimps [Suc_diff_le, le_diff_less, 
   252 				      le_mod_geq]) 1);
   253 qed "mod_Suc";
   254 
   255 Goal "0<n ==> m mod n < n";
   256 by (res_inst_tac [("n","m")] less_induct 1);
   257 by (case_tac "na<n" 1);
   258 (*case n le na*)
   259 by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 2);
   260 (*case na<n*)
   261 by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
   262 qed "mod_less_divisor";
   263 
   264 
   265 (** Evens and Odds **)
   266 
   267 (*With less_zeroE, causes case analysis on b<2*)
   268 AddSEs [less_SucE];
   269 
   270 Goal "b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
   271 by (subgoal_tac "k mod 2 < 2" 1);
   272 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
   273 by (Asm_simp_tac 1);
   274 by Safe_tac;
   275 qed "mod2_cases";
   276 
   277 Goal "Suc(Suc(m)) mod 2 = m mod 2";
   278 by (subgoal_tac "m mod 2 < 2" 1);
   279 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
   280 by Safe_tac;
   281 by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc])));
   282 qed "mod2_Suc_Suc";
   283 Addsimps [mod2_Suc_Suc];
   284 
   285 Goal "(0 < m mod 2) = (m mod 2 = 1)";
   286 by (subgoal_tac "m mod 2 < 2" 1);
   287 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
   288 by Auto_tac;
   289 qed "mod2_gr_0";
   290 Addsimps [mod2_gr_0];
   291 
   292 Goal "(m+m) mod 2 = 0";
   293 by (induct_tac "m" 1);
   294 by (simp_tac (simpset() addsimps [mod_less]) 1);
   295 by (Asm_simp_tac 1);
   296 qed "mod2_add_self_eq_0";
   297 Addsimps [mod2_add_self_eq_0];
   298 
   299 Goal "((m+m)+n) mod 2 = n mod 2";
   300 by (induct_tac "m" 1);
   301 by (simp_tac (simpset() addsimps [mod_less]) 1);
   302 by (Asm_simp_tac 1);
   303 qed "mod2_add_self";
   304 Addsimps [mod2_add_self];
   305 
   306 (*Restore the default*)
   307 Delrules [less_SucE];
   308 
   309 (*** More division laws ***)
   310 
   311 Goal "0<n ==> m*n div n = m";
   312 by (cut_inst_tac [("m", "m*n")] mod_div_equality 1);
   313 by (assume_tac 1);
   314 by (asm_full_simp_tac (simpset() addsimps [mod_mult_self_is_0]) 1);
   315 qed "div_mult_self_is_m";
   316 Addsimps [div_mult_self_is_m];
   317 
   318 (*Cancellation law for division*)
   319 Goal "[| 0<n; 0<k |] ==> (k*m) div (k*n) = m div n";
   320 by (res_inst_tac [("n","m")] less_induct 1);
   321 by (case_tac "na<n" 1);
   322 by (asm_simp_tac (simpset() addsimps [div_less, zero_less_mult_iff, 
   323                                      mult_less_mono2]) 1);
   324 by (subgoal_tac "~ k*na < k*n" 1);
   325 by (asm_simp_tac
   326      (simpset() addsimps [zero_less_mult_iff, div_geq,
   327 			  diff_mult_distrib2 RS sym, diff_less]) 1);
   328 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, 
   329                                           le_refl RS mult_le_mono]) 1);
   330 qed "div_cancel";
   331 Addsimps [div_cancel];
   332 
   333 Goal "[| 0<n; 0<k |] ==> (k*m) mod (k*n) = k * (m mod n)";
   334 by (res_inst_tac [("n","m")] less_induct 1);
   335 by (case_tac "na<n" 1);
   336 by (asm_simp_tac (simpset() addsimps [mod_less, zero_less_mult_iff, 
   337                                      mult_less_mono2]) 1);
   338 by (subgoal_tac "~ k*na < k*n" 1);
   339 by (asm_simp_tac
   340      (simpset() addsimps [zero_less_mult_iff, mod_geq,
   341                          diff_mult_distrib2 RS sym, diff_less]) 1);
   342 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, 
   343                                           le_refl RS mult_le_mono]) 1);
   344 qed "mult_mod_distrib";
   345 
   346 
   347 (************************************************)
   348 (** Divides Relation                           **)
   349 (************************************************)
   350 
   351 Goalw [dvd_def] "m dvd 0";
   352 by (blast_tac (claset() addIs [mult_0_right RS sym]) 1);
   353 qed "dvd_0_right";
   354 Addsimps [dvd_0_right];
   355 
   356 Goalw [dvd_def] "0 dvd m ==> m = 0";
   357 by (fast_tac (claset() addss simpset()) 1);
   358 qed "dvd_0_left";
   359 
   360 Goalw [dvd_def] "1 dvd k";
   361 by (Simp_tac 1);
   362 qed "dvd_1_left";
   363 AddIffs [dvd_1_left];
   364 
   365 Goalw [dvd_def] "m dvd m";
   366 by (blast_tac (claset() addIs [mult_1_right RS sym]) 1);
   367 qed "dvd_refl";
   368 Addsimps [dvd_refl];
   369 
   370 Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd p";
   371 by (blast_tac (claset() addIs [mult_assoc] ) 1);
   372 qed "dvd_trans";
   373 
   374 Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m=n";
   375 by (fast_tac (claset() addDs [mult_eq_self_implies_10]
   376                      addss (simpset() addsimps [mult_assoc, mult_eq_1_iff])) 1);
   377 qed "dvd_anti_sym";
   378 
   379 Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m + n)";
   380 by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1);
   381 qed "dvd_add";
   382 
   383 Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n)";
   384 by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1);
   385 qed "dvd_diff";
   386 
   387 Goal "[| k dvd (m-n); k dvd n; n<=m |] ==> k dvd m";
   388 by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
   389 by (blast_tac (claset() addIs [dvd_add]) 1);
   390 qed "dvd_diffD";
   391 
   392 Goalw [dvd_def] "k dvd n ==> k dvd (m*n)";
   393 by (blast_tac (claset() addIs [mult_left_commute]) 1);
   394 qed "dvd_mult";
   395 
   396 Goal "k dvd m ==> k dvd (m*n)";
   397 by (stac mult_commute 1);
   398 by (etac dvd_mult 1);
   399 qed "dvd_mult2";
   400 
   401 (* k dvd (m*k) *)
   402 AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
   403 
   404 Goalw [dvd_def] "[| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
   405 by (Clarify_tac 1);
   406 by (full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 1);
   407 by (res_inst_tac 
   408     [("x", "(((k div ka)*ka + k mod ka) - ((f*k) div (f*ka)) * ka)")] 
   409     exI 1);
   410 by (asm_simp_tac (simpset() addsimps [diff_mult_distrib2, 
   411                                      mult_mod_distrib, add_mult_distrib2]) 1);
   412 qed "dvd_mod";
   413 
   414 Goal "[| k dvd (m mod n); k dvd n; 0<n |] ==> k dvd m";
   415 by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1);
   416 by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2);
   417 by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
   418 qed "dvd_mod_imp_dvd";
   419 
   420 Goalw [dvd_def]  "!!k. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
   421 by (etac exE 1);
   422 by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
   423 by (Blast_tac 1);
   424 qed "dvd_mult_cancel";
   425 
   426 Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> (i*j) dvd (m*n)";
   427 by (Clarify_tac 1);
   428 by (res_inst_tac [("x","k*ka")] exI 1);
   429 by (asm_simp_tac (simpset() addsimps mult_ac) 1);
   430 qed "mult_dvd_mono";
   431 
   432 Goalw [dvd_def] "(i*j) dvd k ==> i dvd k";
   433 by (full_simp_tac (simpset() addsimps [mult_assoc]) 1);
   434 by (Blast_tac 1);
   435 qed "dvd_mult_left";
   436 
   437 Goalw [dvd_def] "[| k dvd n; 0 < n |] ==> k <= n";
   438 by (Clarify_tac 1);
   439 by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff])));
   440 by (etac conjE 1);
   441 by (rtac le_trans 1);
   442 by (rtac (le_refl RS mult_le_mono) 2);
   443 by (etac Suc_leI 2);
   444 by (Simp_tac 1);
   445 qed "dvd_imp_le";
   446 
   447 Goalw [dvd_def] "0<k ==> (k dvd n) = (n mod k = 0)";
   448 by Safe_tac;
   449 by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
   450 by (eres_inst_tac [("t","n")] (mod_div_equality RS subst) 1);
   451 by (stac mult_commute 1);
   452 by (Asm_simp_tac 1);
   453 by (Blast_tac 1);
   454 qed "dvd_eq_mod_eq_0";