src/HOL/Arith.ML
author clasohm
Wed Mar 13 11:55:25 1996 +0100 (1996-03-13 ago)
changeset 1574 5a63ab90ee8a
parent 1552 6f71b5d46700
child 1618 372880456b5b
permissions -rw-r--r--
modified primrec so it can be used in MiniML/Type.thy
     1 (*  Title:      HOL/Arith.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Proofs about elementary arithmetic: addition, multiplication, etc.
     7 Tests definitions and simplifier.
     8 *)
     9 
    10 open Arith;
    11 
    12 (*** Basic rewrite rules for the arithmetic operators ***)
    13 
    14 val [pred_0, pred_Suc] = nat_recs pred_def;
    15 val [add_0,add_Suc] = nat_recs add_def; 
    16 val [mult_0,mult_Suc] = nat_recs mult_def; 
    17 Addsimps [pred_0,pred_Suc,add_0,add_Suc,mult_0,mult_Suc];
    18 
    19 (** pred **)
    20 
    21 val prems = goal Arith.thy "n ~= 0 ==> Suc(pred n) = n";
    22 by (res_inst_tac [("n","n")] natE 1);
    23 by (cut_facts_tac prems 1);
    24 by (ALLGOALS Asm_full_simp_tac);
    25 qed "Suc_pred";
    26 Addsimps [Suc_pred];
    27 
    28 (** Difference **)
    29 
    30 val diff_0 = diff_def RS def_nat_rec_0;
    31 
    32 qed_goalw "diff_0_eq_0" Arith.thy [diff_def, pred_def]
    33     "0 - n = 0"
    34  (fn _ => [nat_ind_tac "n" 1,  ALLGOALS Asm_simp_tac]);
    35 
    36 (*Must simplify BEFORE the induction!!  (Else we get a critical pair)
    37   Suc(m) - Suc(n)   rewrites to   pred(Suc(m) - n)  *)
    38 qed_goalw "diff_Suc_Suc" Arith.thy [diff_def, pred_def]
    39     "Suc(m) - Suc(n) = m - n"
    40  (fn _ =>
    41   [Simp_tac 1, nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]);
    42 
    43 Addsimps [diff_0, diff_0_eq_0, diff_Suc_Suc];
    44 
    45 
    46 (**** Inductive properties of the operators ****)
    47 
    48 (*** Addition ***)
    49 
    50 qed_goal "add_0_right" Arith.thy "m + 0 = m"
    51  (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
    52 
    53 qed_goal "add_Suc_right" Arith.thy "m + Suc(n) = Suc(m+n)"
    54  (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
    55 
    56 Addsimps [add_0_right,add_Suc_right];
    57 
    58 (*Associative law for addition*)
    59 qed_goal "add_assoc" Arith.thy "(m + n) + k = m + ((n + k)::nat)"
    60  (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
    61 
    62 (*Commutative law for addition*)  
    63 qed_goal "add_commute" Arith.thy "m + n = n + (m::nat)"
    64  (fn _ =>  [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
    65 
    66 qed_goal "add_left_commute" Arith.thy "x+(y+z)=y+((x+z)::nat)"
    67  (fn _ => [rtac (add_commute RS trans) 1, rtac (add_assoc RS trans) 1,
    68            rtac (add_commute RS arg_cong) 1]);
    69 
    70 (*Addition is an AC-operator*)
    71 val add_ac = [add_assoc, add_commute, add_left_commute];
    72 
    73 goal Arith.thy "!!k::nat. (k + m = k + n) = (m=n)";
    74 by (nat_ind_tac "k" 1);
    75 by (Simp_tac 1);
    76 by (Asm_simp_tac 1);
    77 qed "add_left_cancel";
    78 
    79 goal Arith.thy "!!k::nat. (m + k = n + k) = (m=n)";
    80 by (nat_ind_tac "k" 1);
    81 by (Simp_tac 1);
    82 by (Asm_simp_tac 1);
    83 qed "add_right_cancel";
    84 
    85 goal Arith.thy "!!k::nat. (k + m <= k + n) = (m<=n)";
    86 by (nat_ind_tac "k" 1);
    87 by (Simp_tac 1);
    88 by (Asm_simp_tac 1);
    89 qed "add_left_cancel_le";
    90 
    91 goal Arith.thy "!!k::nat. (k + m < k + n) = (m<n)";
    92 by (nat_ind_tac "k" 1);
    93 by (Simp_tac 1);
    94 by (Asm_simp_tac 1);
    95 qed "add_left_cancel_less";
    96 
    97 Addsimps [add_left_cancel, add_right_cancel,
    98           add_left_cancel_le, add_left_cancel_less];
    99 
   100 goal Arith.thy "(m+n = 0) = (m=0 & n=0)";
   101 by (nat_ind_tac "m" 1);
   102 by (ALLGOALS Asm_simp_tac);
   103 qed "add_is_0";
   104 Addsimps [add_is_0];
   105 
   106 goal Arith.thy "!!n. n ~= 0 ==> m + pred n = pred(m+n)";
   107 by (nat_ind_tac "m" 1);
   108 by (ALLGOALS Asm_simp_tac);
   109 qed "add_pred";
   110 Addsimps [add_pred];
   111 
   112 (*** Multiplication ***)
   113 
   114 (*right annihilation in product*)
   115 qed_goal "mult_0_right" Arith.thy "m * 0 = 0"
   116  (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
   117 
   118 (*right Sucessor law for multiplication*)
   119 qed_goal "mult_Suc_right" Arith.thy  "m * Suc(n) = m + (m * n)"
   120  (fn _ => [nat_ind_tac "m" 1,
   121            ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
   122 
   123 Addsimps [mult_0_right,mult_Suc_right];
   124 
   125 (*Commutative law for multiplication*)
   126 qed_goal "mult_commute" Arith.thy "m * n = n * (m::nat)"
   127  (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
   128 
   129 (*addition distributes over multiplication*)
   130 qed_goal "add_mult_distrib" Arith.thy "(m + n)*k = (m*k) + ((n*k)::nat)"
   131  (fn _ => [nat_ind_tac "m" 1,
   132            ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
   133 
   134 qed_goal "add_mult_distrib2" Arith.thy "k*(m + n) = (k*m) + ((k*n)::nat)"
   135  (fn _ => [nat_ind_tac "m" 1,
   136            ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
   137 
   138 Addsimps [add_mult_distrib,add_mult_distrib2];
   139 
   140 (*Associative law for multiplication*)
   141 qed_goal "mult_assoc" Arith.thy "(m * n) * k = m * ((n * k)::nat)"
   142   (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
   143 
   144 qed_goal "mult_left_commute" Arith.thy "x*(y*z) = y*((x*z)::nat)"
   145  (fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1,
   146            rtac mult_assoc 1, rtac (mult_commute RS arg_cong) 1]);
   147 
   148 val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
   149 
   150 (*** Difference ***)
   151 
   152 qed_goal "diff_self_eq_0" Arith.thy "m - m = 0"
   153  (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
   154 Addsimps [diff_self_eq_0];
   155 
   156 (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
   157 val [prem] = goal Arith.thy "[| ~ m<n |] ==> n+(m-n) = (m::nat)";
   158 by (rtac (prem RS rev_mp) 1);
   159 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   160 by (ALLGOALS Asm_simp_tac);
   161 qed "add_diff_inverse";
   162 
   163 
   164 (*** Remainder ***)
   165 
   166 goal Arith.thy "m - n < Suc(m)";
   167 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   168 by (etac less_SucE 3);
   169 by (ALLGOALS Asm_simp_tac);
   170 qed "diff_less_Suc";
   171 
   172 goal Arith.thy "!!m::nat. m - n <= m";
   173 by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
   174 by (ALLGOALS Asm_simp_tac);
   175 qed "diff_le_self";
   176 
   177 goal Arith.thy "!!n::nat. (n+m) - n = m";
   178 by (nat_ind_tac "n" 1);
   179 by (ALLGOALS Asm_simp_tac);
   180 qed "diff_add_inverse";
   181 
   182 goal Arith.thy "!!n::nat. n - (n+m) = 0";
   183 by (nat_ind_tac "n" 1);
   184 by (ALLGOALS Asm_simp_tac);
   185 qed "diff_add_0";
   186 
   187 (*In ordinary notation: if 0<n and n<=m then m-n < m *)
   188 goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m";
   189 by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
   190 by (fast_tac HOL_cs 1);
   191 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   192 by (ALLGOALS(asm_simp_tac(!simpset addsimps [diff_less_Suc])));
   193 qed "diff_less";
   194 
   195 val wf_less_trans = wf_pred_nat RS wf_trancl RSN (2, def_wfrec RS trans);
   196 
   197 goalw Nat.thy [less_def] "(m,n) : pred_nat^+ = (m<n)";
   198 by (rtac refl 1);
   199 qed "less_eq";
   200 
   201 goal Arith.thy "(%m. m mod n) = wfrec (trancl pred_nat) \
   202              \                      (%f j. if j<n then j else f (j-n))";
   203 by (simp_tac (HOL_ss addsimps [mod_def]) 1);
   204 val mod_def1 = result() RS eq_reflection;
   205 
   206 goal Arith.thy "!!m. m<n ==> m mod n = m";
   207 by (rtac (mod_def1 RS wf_less_trans) 1);
   208 by (Asm_simp_tac 1);
   209 qed "mod_less";
   210 
   211 goal Arith.thy "!!m. [| 0<n;  ~m<n |] ==> m mod n = (m-n) mod n";
   212 by (rtac (mod_def1 RS wf_less_trans) 1);
   213 by (asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1);
   214 qed "mod_geq";
   215 
   216 
   217 (*** Quotient ***)
   218 
   219 goal Arith.thy "(%m. m div n) = wfrec (trancl pred_nat) \
   220                         \            (%f j. if j<n then 0 else Suc (f (j-n)))";
   221 by (simp_tac (HOL_ss addsimps [div_def]) 1);
   222 val div_def1 = result() RS eq_reflection;
   223 
   224 goal Arith.thy "!!m. m<n ==> m div n = 0";
   225 by (rtac (div_def1 RS wf_less_trans) 1);
   226 by (Asm_simp_tac 1);
   227 qed "div_less";
   228 
   229 goal Arith.thy "!!M. [| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)";
   230 by (rtac (div_def1 RS wf_less_trans) 1);
   231 by (asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1);
   232 qed "div_geq";
   233 
   234 (*Main Result about quotient and remainder.*)
   235 goal Arith.thy "!!m. 0<n ==> (m div n)*n + m mod n = m";
   236 by (res_inst_tac [("n","m")] less_induct 1);
   237 by (rename_tac "k" 1);    (*Variable name used in line below*)
   238 by (case_tac "k<n" 1);
   239 by (ALLGOALS (asm_simp_tac(!simpset addsimps (add_ac @
   240                        [mod_less, mod_geq, div_less, div_geq,
   241                         add_diff_inverse, diff_less]))));
   242 qed "mod_div_equality";
   243 
   244 
   245 (*** More results about difference ***)
   246 
   247 val [prem] = goal Arith.thy "m < Suc(n) ==> m-n = 0";
   248 by (rtac (prem RS rev_mp) 1);
   249 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   250 by (ALLGOALS Asm_simp_tac);
   251 qed "less_imp_diff_is_0";
   252 
   253 val prems = goal Arith.thy "m-n = 0  -->  n-m = 0  -->  m=n";
   254 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   255 by (REPEAT(Simp_tac 1 THEN TRY(atac 1)));
   256 qed_spec_mp "diffs0_imp_equal";
   257 
   258 val [prem] = goal Arith.thy "m<n ==> 0<n-m";
   259 by (rtac (prem RS rev_mp) 1);
   260 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   261 by (ALLGOALS Asm_simp_tac);
   262 qed "less_imp_diff_positive";
   263 
   264 val [prem] = goal Arith.thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
   265 by (rtac (prem RS rev_mp) 1);
   266 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   267 by (ALLGOALS Asm_simp_tac);
   268 qed "Suc_diff_n";
   269 
   270 goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
   271 by (simp_tac (!simpset addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
   272                     setloop (split_tac [expand_if])) 1);
   273 qed "if_Suc_diff_n";
   274 
   275 goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
   276 by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
   277 by (ALLGOALS (strip_tac THEN' Simp_tac THEN' TRY o fast_tac HOL_cs));
   278 qed "zero_induct_lemma";
   279 
   280 val prems = goal Arith.thy "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
   281 by (rtac (diff_self_eq_0 RS subst) 1);
   282 by (rtac (zero_induct_lemma RS mp RS mp) 1);
   283 by (REPEAT (ares_tac ([impI,allI]@prems) 1));
   284 qed "zero_induct";
   285 
   286 (*13 July 1992: loaded in 105.7s*)
   287 
   288 (**** Additional theorems about "less than" ****)
   289 
   290 goal Arith.thy "!!m. m<n --> (? k. n=Suc(m+k))";
   291 by (nat_ind_tac "n" 1);
   292 by (ALLGOALS(Simp_tac));
   293 by (REPEAT_FIRST (ares_tac [conjI, impI]));
   294 by (res_inst_tac [("x","0")] exI 2);
   295 by (Simp_tac 2);
   296 by (safe_tac HOL_cs);
   297 by (res_inst_tac [("x","Suc(k)")] exI 1);
   298 by (Simp_tac 1);
   299 qed_spec_mp "less_eq_Suc_add";
   300 
   301 goal Arith.thy "n <= ((m + n)::nat)";
   302 by (nat_ind_tac "m" 1);
   303 by (ALLGOALS Simp_tac);
   304 by (etac le_trans 1);
   305 by (rtac (lessI RS less_imp_le) 1);
   306 qed "le_add2";
   307 
   308 goal Arith.thy "n <= ((n + m)::nat)";
   309 by (simp_tac (!simpset addsimps add_ac) 1);
   310 by (rtac le_add2 1);
   311 qed "le_add1";
   312 
   313 bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans)));
   314 bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans)));
   315 
   316 (*"i <= j ==> i <= j+m"*)
   317 bind_thm ("trans_le_add1", le_add1 RSN (2,le_trans));
   318 
   319 (*"i <= j ==> i <= m+j"*)
   320 bind_thm ("trans_le_add2", le_add2 RSN (2,le_trans));
   321 
   322 (*"i < j ==> i < j+m"*)
   323 bind_thm ("trans_less_add1", le_add1 RSN (2,less_le_trans));
   324 
   325 (*"i < j ==> i < m+j"*)
   326 bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
   327 
   328 goal Arith.thy "!!i. i+j < (k::nat) ==> i<k";
   329 by (etac rev_mp 1);
   330 by (nat_ind_tac "j" 1);
   331 by (ALLGOALS Asm_simp_tac);
   332 by (fast_tac (HOL_cs addDs [Suc_lessD]) 1);
   333 qed "add_lessD1";
   334 
   335 goal Arith.thy "!!k::nat. m <= n ==> m <= n+k";
   336 by (etac le_trans 1);
   337 by (rtac le_add1 1);
   338 qed "le_imp_add_le";
   339 
   340 goal Arith.thy "!!k::nat. m < n ==> m < n+k";
   341 by (etac less_le_trans 1);
   342 by (rtac le_add1 1);
   343 qed "less_imp_add_less";
   344 
   345 goal Arith.thy "m+k<=n --> m<=(n::nat)";
   346 by (nat_ind_tac "k" 1);
   347 by (ALLGOALS Asm_simp_tac);
   348 by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
   349 qed_spec_mp "add_leD1";
   350 
   351 goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n";
   352 by (safe_tac (HOL_cs addSDs [less_eq_Suc_add]));
   353 by (asm_full_simp_tac
   354     (!simpset delsimps [add_Suc_right]
   355                 addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1);
   356 by (etac subst 1);
   357 by (simp_tac (!simpset addsimps [less_add_Suc1]) 1);
   358 qed "less_add_eq_less";
   359 
   360 
   361 (** Monotonicity of addition (from ZF/Arith) **)
   362 
   363 (** Monotonicity results **)
   364 
   365 (*strict, in 1st argument*)
   366 goal Arith.thy "!!i j k::nat. i < j ==> i + k < j + k";
   367 by (nat_ind_tac "k" 1);
   368 by (ALLGOALS Asm_simp_tac);
   369 qed "add_less_mono1";
   370 
   371 (*strict, in both arguments*)
   372 goal Arith.thy "!!i j k::nat. [|i < j; k < l|] ==> i + k < j + l";
   373 by (rtac (add_less_mono1 RS less_trans) 1);
   374 by (REPEAT (assume_tac 1));
   375 by (nat_ind_tac "j" 1);
   376 by (ALLGOALS Asm_simp_tac);
   377 qed "add_less_mono";
   378 
   379 (*A [clumsy] way of lifting < monotonicity to <= monotonicity *)
   380 val [lt_mono,le] = goal Arith.thy
   381      "[| !!i j::nat. i<j ==> f(i) < f(j);       \
   382 \        i <= j                                 \
   383 \     |] ==> f(i) <= (f(j)::nat)";
   384 by (cut_facts_tac [le] 1);
   385 by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
   386 by (fast_tac (HOL_cs addSIs [lt_mono]) 1);
   387 qed "less_mono_imp_le_mono";
   388 
   389 (*non-strict, in 1st argument*)
   390 goal Arith.thy "!!i j k::nat. i<=j ==> i + k <= j + k";
   391 by (res_inst_tac [("f", "%j.j+k")] less_mono_imp_le_mono 1);
   392 by (etac add_less_mono1 1);
   393 by (assume_tac 1);
   394 qed "add_le_mono1";
   395 
   396 (*non-strict, in both arguments*)
   397 goal Arith.thy "!!k l::nat. [|i<=j;  k<=l |] ==> i + k <= j + l";
   398 by (etac (add_le_mono1 RS le_trans) 1);
   399 by (simp_tac (!simpset addsimps [add_commute]) 1);
   400 (*j moves to the end because it is free while k, l are bound*)
   401 by (etac add_le_mono1 1);
   402 qed "add_le_mono";