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