src/HOL/Divides.ML
author paulson
Wed Dec 24 10:02:30 1997 +0100 (1997-12-24)
changeset 4477 b3e5857d8d99
parent 4423 a129b817b58a
child 4686 74a12e86b20b
permissions -rw-r--r--
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
     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 thy "(%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 thy "!!m. 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 thy "!!m. [| 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 goal thy "m mod 1 = 0";
    41 by (induct_tac "m" 1);
    42 by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_less, mod_geq])));
    43 qed "mod_1";
    44 Addsimps [mod_1];
    45 
    46 goal thy "!!n. 0<n ==> n mod n = 0";
    47 by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1);
    48 qed "mod_self";
    49 
    50 goal thy "!!n. 0<n ==> (m+n) mod n = m mod n";
    51 by (subgoal_tac "(n + m) mod n = (n+m-n) mod n" 1);
    52 by (stac (mod_geq RS sym) 2);
    53 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
    54 qed "mod_eq_add";
    55 
    56 goal thy "!!k. [| 0<k; 0<n |] ==> (m mod n)*k = (m*k) mod (n*k)";
    57 by (res_inst_tac [("n","m")] less_induct 1);
    58 by (case_tac "na<n" 1);
    59 (*case na<n*)
    60 by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
    61 (*case n<=na*)
    62 by (asm_simp_tac (simpset() addsimps [mod_geq, diff_less, zero_less_mult_iff, 
    63 				     diff_mult_distrib]) 1);
    64 qed "mod_mult_distrib";
    65 
    66 goal thy "!!k. [| 0<k; 0<n |] ==> k*(m mod n) = (k*m) mod (k*n)";
    67 by (res_inst_tac [("n","m")] less_induct 1);
    68 by (case_tac "na<n" 1);
    69 (*case na<n*)
    70 by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
    71 (*case n<=na*)
    72 by (asm_simp_tac (simpset() addsimps [mod_geq, diff_less, zero_less_mult_iff, 
    73 				     diff_mult_distrib2]) 1);
    74 qed "mod_mult_distrib2";
    75 
    76 goal thy "!!n. 0<n ==> m*n mod n = 0";
    77 by (induct_tac "m" 1);
    78 by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
    79 by (dres_inst_tac [("m","m*n")] mod_eq_add 1);
    80 by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
    81 qed "mod_mult_self_is_0";
    82 Addsimps [mod_mult_self_is_0];
    83 
    84 (*** Quotient ***)
    85 
    86 goal thy "(%m. m div n) = wfrec (trancl pred_nat) \
    87                         \            (%f j. if j<n then 0 else Suc (f (j-n)))";
    88 by (simp_tac (simpset() addsimps [div_def]) 1);
    89 qed "div_eq";
    90 
    91 goal thy "!!m. m<n ==> m div n = 0";
    92 by (rtac (div_eq RS wf_less_trans) 1);
    93 by (Asm_simp_tac 1);
    94 qed "div_less";
    95 
    96 goal thy "!!M. [| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)";
    97 by (rtac (div_eq RS wf_less_trans) 1);
    98 by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
    99 qed "div_geq";
   100 
   101 (*Main Result about quotient and remainder.*)
   102 goal thy "!!m. 0<n ==> (m div n)*n + m mod n = m";
   103 by (res_inst_tac [("n","m")] less_induct 1);
   104 by (rename_tac "k" 1);    (*Variable name used in line below*)
   105 by (case_tac "k<n" 1);
   106 by (ALLGOALS (asm_simp_tac(simpset() addsimps ([add_assoc] @
   107                        [mod_less, mod_geq, div_less, div_geq,
   108                         add_diff_inverse, diff_less]))));
   109 qed "mod_div_equality";
   110 
   111 (* a simple rearrangement of mod_div_equality: *)
   112 goal thy "!!k. 0<k ==> k*(m div k) = m - (m mod k)";
   113 by (dres_inst_tac [("m","m")] mod_div_equality 1);
   114 by (EVERY1[etac subst, simp_tac (simpset() addsimps mult_ac),
   115            K(IF_UNSOLVED no_tac)]);
   116 qed "mult_div_cancel";
   117 
   118 goal thy "m div 1 = m";
   119 by (induct_tac "m" 1);
   120 by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_less, div_geq])));
   121 qed "div_1";
   122 Addsimps [div_1];
   123 
   124 goal thy "!!n. 0<n ==> n div n = 1";
   125 by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1);
   126 qed "div_self";
   127 
   128 (* Monotonicity of div in first argument *)
   129 goal thy "!!n. 0<k ==> ALL m. m <= n --> (m div k) <= (n div k)";
   130 by (res_inst_tac [("n","n")] less_induct 1);
   131 by (Clarify_tac 1);
   132 by (case_tac "na<k" 1);
   133 (* 1  case n<k *)
   134 by (subgoal_tac "m<k" 1);
   135 by (asm_simp_tac (simpset() addsimps [div_less]) 1);
   136 by (trans_tac 1);
   137 (* 2  case n >= k *)
   138 by (case_tac "m<k" 1);
   139 (* 2.1  case m<k *)
   140 by (asm_simp_tac (simpset() addsimps [div_less]) 1);
   141 (* 2.2  case m>=k *)
   142 by (asm_simp_tac (simpset() addsimps [div_geq, diff_less, diff_le_mono]) 1);
   143 qed_spec_mp "div_le_mono";
   144 
   145 
   146 (* Antimonotonicity of div in second argument *)
   147 goal thy "!!k m n. [| 0<m; m<=n |] ==> (k div n) <= (k div m)";
   148 by (subgoal_tac "0<n" 1);
   149  by (trans_tac 2);
   150 by (res_inst_tac [("n","k")] less_induct 1);
   151 by (Simp_tac 1);
   152 by (rename_tac "k" 1);
   153 by (case_tac "k<n" 1);
   154  by (asm_simp_tac (simpset() addsimps [div_less]) 1);
   155 by (subgoal_tac "~(k<m)" 1);
   156  by (trans_tac 2);
   157 by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
   158 by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
   159  by (best_tac (claset() addIs [le_trans] 
   160                        addss (simpset() addsimps [diff_less])) 1);
   161 by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 1));
   162 qed "div_le_mono2";
   163 
   164 goal thy "!!m n. 0<n ==> m div n <= m";
   165 by (subgoal_tac "m div n <= m div 1" 1);
   166 by (Asm_full_simp_tac 1);
   167 by (rtac div_le_mono2 1);
   168 by (ALLGOALS trans_tac);
   169 qed "div_le_dividend";
   170 Addsimps [div_le_dividend];
   171 
   172 (* Similar for "less than" *)
   173 goal thy "!!m n. 1<n ==> (0 < m) --> (m div n < m)";
   174 by (res_inst_tac [("n","m")] less_induct 1);
   175 by (Simp_tac 1);
   176 by (rename_tac "m" 1);
   177 by (case_tac "m<n" 1);
   178  by (asm_full_simp_tac (simpset() addsimps [div_less]) 1);
   179 by (subgoal_tac "0<n" 1);
   180  by (trans_tac 2);
   181 by (asm_full_simp_tac (simpset() addsimps [div_geq]) 1);
   182 by (case_tac "n<m" 1);
   183  by (subgoal_tac "(m-n) div n < (m-n)" 1);
   184   by (REPEAT (ares_tac [impI,less_trans_Suc] 1));
   185   by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
   186  by (dres_inst_tac [("m","n")] less_imp_diff_positive 1);
   187  by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
   188 (* case n=m *)
   189 by (subgoal_tac "m=n" 1);
   190  by (trans_tac 2);
   191 by (asm_simp_tac (simpset() addsimps [div_less]) 1);
   192 qed_spec_mp "div_less_dividend";
   193 Addsimps [div_less_dividend];
   194 
   195 (*** Further facts about mod (mainly for the mutilated chess board ***)
   196 
   197 goal thy
   198     "!!m n. 0<n ==> \
   199 \           Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
   200 by (res_inst_tac [("n","m")] less_induct 1);
   201 by (excluded_middle_tac "Suc(na)<n" 1);
   202 (* case Suc(na) < n *)
   203 by (forward_tac [lessI RS less_trans] 2);
   204 by (asm_simp_tac (simpset() addsimps [mod_less, less_not_refl2 RS not_sym]) 2);
   205 (* case n <= Suc(na) *)
   206 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, mod_geq]) 1);
   207 by (etac (le_imp_less_or_eq RS disjE) 1);
   208 by (asm_simp_tac (simpset() addsimps [Suc_diff_n]) 1);
   209 by (asm_full_simp_tac (simpset() addsimps [not_less_eq RS sym, 
   210                                           diff_less, mod_geq]) 1);
   211 by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
   212 qed "mod_Suc";
   213 
   214 goal thy "!!m n. 0<n ==> m mod n < n";
   215 by (res_inst_tac [("n","m")] less_induct 1);
   216 by (excluded_middle_tac "na<n" 1);
   217 (*case na<n*)
   218 by (asm_simp_tac (simpset() addsimps [mod_less]) 2);
   219 (*case n le na*)
   220 by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 1);
   221 qed "mod_less_divisor";
   222 
   223 
   224 (** Evens and Odds **)
   225 
   226 (*With less_zeroE, causes case analysis on b<2*)
   227 AddSEs [less_SucE];
   228 
   229 goal thy "!!k b. b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
   230 by (subgoal_tac "k mod 2 < 2" 1);
   231 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
   232 by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
   233 by Safe_tac;
   234 qed "mod2_cases";
   235 
   236 goal thy "Suc(Suc(m)) mod 2 = m mod 2";
   237 by (subgoal_tac "m mod 2 < 2" 1);
   238 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
   239 by Safe_tac;
   240 by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc])));
   241 qed "mod2_Suc_Suc";
   242 Addsimps [mod2_Suc_Suc];
   243 
   244 goal Divides.thy "(0 < m mod 2) = (m mod 2 = 1)";
   245 by (subgoal_tac "m mod 2 < 2" 1);
   246 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
   247 by Auto_tac;
   248 qed "mod2_gr_0";
   249 Addsimps [mod2_gr_0];
   250 
   251 goal thy "(m+m) mod 2 = 0";
   252 by (induct_tac "m" 1);
   253 by (simp_tac (simpset() addsimps [mod_less]) 1);
   254 by (Asm_simp_tac 1);
   255 qed "mod2_add_self_eq_0";
   256 Addsimps [mod2_add_self_eq_0];
   257 
   258 goal thy "((m+m)+n) mod 2 = n mod 2";
   259 by (induct_tac "m" 1);
   260 by (simp_tac (simpset() addsimps [mod_less]) 1);
   261 by (Asm_simp_tac 1);
   262 qed "mod2_add_self";
   263 Addsimps [mod2_add_self];
   264 
   265 Delrules [less_SucE];
   266 
   267 
   268 (*** More division laws ***)
   269 
   270 goal thy "!!n. 0<n ==> m*n div n = m";
   271 by (cut_inst_tac [("m", "m*n")] mod_div_equality 1);
   272 by (assume_tac 1);
   273 by (asm_full_simp_tac (simpset() addsimps [mod_mult_self_is_0]) 1);
   274 qed "div_mult_self_is_m";
   275 Addsimps [div_mult_self_is_m];
   276 
   277 (*Cancellation law for division*)
   278 goal thy "!!k. [| 0<n; 0<k |] ==> (k*m) div (k*n) = m div n";
   279 by (res_inst_tac [("n","m")] less_induct 1);
   280 by (case_tac "na<n" 1);
   281 by (asm_simp_tac (simpset() addsimps [div_less, zero_less_mult_iff, 
   282                                      mult_less_mono2]) 1);
   283 by (subgoal_tac "~ k*na < k*n" 1);
   284 by (asm_simp_tac
   285      (simpset() addsimps [zero_less_mult_iff, div_geq,
   286                          diff_mult_distrib2 RS sym, diff_less]) 1);
   287 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, 
   288                                           le_refl RS mult_le_mono]) 1);
   289 qed "div_cancel";
   290 Addsimps [div_cancel];
   291 
   292 goal thy "!!k. [| 0<n; 0<k |] ==> (k*m) mod (k*n) = k * (m mod n)";
   293 by (res_inst_tac [("n","m")] less_induct 1);
   294 by (case_tac "na<n" 1);
   295 by (asm_simp_tac (simpset() addsimps [mod_less, zero_less_mult_iff, 
   296                                      mult_less_mono2]) 1);
   297 by (subgoal_tac "~ k*na < k*n" 1);
   298 by (asm_simp_tac
   299      (simpset() addsimps [zero_less_mult_iff, mod_geq,
   300                          diff_mult_distrib2 RS sym, diff_less]) 1);
   301 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, 
   302                                           le_refl RS mult_le_mono]) 1);
   303 qed "mult_mod_distrib";
   304 
   305 
   306 (************************************************)
   307 (** Divides Relation                           **)
   308 (************************************************)
   309 
   310 goalw thy [dvd_def] "m dvd 0";
   311 by (blast_tac (claset() addIs [mult_0_right RS sym]) 1);
   312 qed "dvd_0_right";
   313 Addsimps [dvd_0_right];
   314 
   315 goalw thy [dvd_def] "!!m. 0 dvd m ==> m = 0";
   316 by (fast_tac (claset() addss simpset()) 1);
   317 qed "dvd_0_left";
   318 
   319 goalw thy [dvd_def] "1 dvd k";
   320 by (Simp_tac 1);
   321 qed "dvd_1_left";
   322 AddIffs [dvd_1_left];
   323 
   324 goalw thy [dvd_def] "m dvd m";
   325 by (blast_tac (claset() addIs [mult_1_right RS sym]) 1);
   326 qed "dvd_refl";
   327 Addsimps [dvd_refl];
   328 
   329 goalw thy [dvd_def] "!!m n p. [| m dvd n; n dvd p |] ==> m dvd p";
   330 by (blast_tac (claset() addIs [mult_assoc] ) 1);
   331 qed "dvd_trans";
   332 
   333 goalw thy [dvd_def] "!!m n. [| m dvd n; n dvd m |] ==> m=n";
   334 by (fast_tac (claset() addDs [mult_eq_self_implies_10]
   335                      addss (simpset() addsimps [mult_assoc, mult_eq_1_iff])) 1);
   336 qed "dvd_anti_sym";
   337 
   338 goalw thy [dvd_def] "!!k. [| k dvd m; k dvd n |] ==> k dvd (m + n)";
   339 by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1);
   340 qed "dvd_add";
   341 
   342 goalw thy [dvd_def] "!!k. [| k dvd m; k dvd n |] ==> k dvd (m-n)";
   343 by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1);
   344 qed "dvd_diff";
   345 
   346 goal thy "!!k. [| k dvd (m-n); k dvd n; n<=m |] ==> k dvd m";
   347 by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
   348 by (blast_tac (claset() addIs [dvd_add]) 1);
   349 qed "dvd_diffD";
   350 
   351 goalw thy [dvd_def] "!!k. k dvd n ==> k dvd (m*n)";
   352 by (blast_tac (claset() addIs [mult_left_commute]) 1);
   353 qed "dvd_mult";
   354 
   355 goal thy "!!k. k dvd m ==> k dvd (m*n)";
   356 by (stac mult_commute 1);
   357 by (etac dvd_mult 1);
   358 qed "dvd_mult2";
   359 
   360 (* k dvd (m*k) *)
   361 AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
   362 
   363 goalw thy [dvd_def] "!!m. [| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
   364 by (Clarify_tac 1);
   365 by (full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 1);
   366 by (res_inst_tac 
   367     [("x", "(((k div ka)*ka + k mod ka) - ((f*k) div (f*ka)) * ka)")] 
   368     exI 1);
   369 by (asm_simp_tac (simpset() addsimps [diff_mult_distrib2, 
   370                                      mult_mod_distrib, add_mult_distrib2]) 1);
   371 qed "dvd_mod";
   372 
   373 goal thy "!!k. [| k dvd (m mod n); k dvd n; 0<n |] ==> k dvd m";
   374 by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1);
   375 by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2);
   376 by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
   377 qed "dvd_mod_imp_dvd";
   378 
   379 goalw thy [dvd_def]  "!!k m n. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
   380 by (etac exE 1);
   381 by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
   382 by (Blast_tac 1);
   383 qed "dvd_mult_cancel";
   384 
   385 goalw thy [dvd_def] "!!i j. [| i dvd m; j dvd n|] ==> (i*j) dvd (m*n)";
   386 by (Clarify_tac 1);
   387 by (res_inst_tac [("x","k*ka")] exI 1);
   388 by (asm_simp_tac (simpset() addsimps mult_ac) 1);
   389 qed "mult_dvd_mono";
   390 
   391 goalw thy [dvd_def] "!!c. (i*j) dvd k ==> i dvd k";
   392 by (full_simp_tac (simpset() addsimps [mult_assoc]) 1);
   393 by (Blast_tac 1);
   394 qed "dvd_mult_left";
   395 
   396 goalw thy [dvd_def] "!!n. [| k dvd n; 0 < n |] ==> k <= n";
   397 by (Clarify_tac 1);
   398 by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff])));
   399 by (etac conjE 1);
   400 by (rtac le_trans 1);
   401 by (rtac (le_refl RS mult_le_mono) 2);
   402 by (etac Suc_leI 2);
   403 by (Simp_tac 1);
   404 qed "dvd_imp_le";
   405 
   406 goalw thy [dvd_def] "!!k. 0<k ==> (k dvd n) = (n mod k = 0)";
   407 by Safe_tac;
   408 by (stac mult_commute 1);
   409 by (Asm_simp_tac 1);
   410 by (eres_inst_tac [("t","n")] (mod_div_equality RS subst) 1);
   411 by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
   412 by (Blast_tac 1);
   413 qed "dvd_eq_mod_eq_0";