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