src/ZF/arith.ML
author lcp
Thu Nov 18 14:57:05 1993 +0100 (1993-11-18)
changeset 127 eec6bb9c58ea
parent 25 3ac1c0c0016e
permissions -rw-r--r--
Misc modifs such as expandshort
     1 (*  Title: 	ZF/arith.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 For arith.thy.  Arithmetic operators and their definitions
     7 
     8 Proofs about elementary arithmetic: addition, multiplication, etc.
     9 
    10 Could prove def_rec_0, def_rec_succ...
    11 *)
    12 
    13 open Arith;
    14 
    15 (*"Difference" is subtraction of natural numbers.
    16   There are no negative numbers; we have
    17      m #- n = 0  iff  m<=n   and     m #- n = succ(k) iff m>n.
    18   Also, rec(m, 0, %z w.z) is pred(m).   
    19 *)
    20 
    21 (** rec -- better than nat_rec; the succ case has no type requirement! **)
    22 
    23 val rec_trans = rec_def RS def_transrec RS trans;
    24 
    25 goal Arith.thy "rec(0,a,b) = a";
    26 by (rtac rec_trans 1);
    27 by (rtac nat_case_0 1);
    28 val rec_0 = result();
    29 
    30 goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))";
    31 by (rtac rec_trans 1);
    32 by (simp_tac (ZF_ss addsimps [nat_case_succ, nat_succI]) 1);
    33 val rec_succ = result();
    34 
    35 val major::prems = goal Arith.thy
    36     "[| n: nat;  \
    37 \       a: C(0);  \
    38 \       !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m))  \
    39 \    |] ==> rec(n,a,b) : C(n)";
    40 by (rtac (major RS nat_induct) 1);
    41 by (ALLGOALS
    42     (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
    43 val rec_type = result();
    44 
    45 val nat_le_refl = naturals_are_ordinals RS le_refl;
    46 
    47 val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat];
    48 
    49 val nat_simps = [rec_0, rec_succ, not_lt0, nat_0_le, le0_iff, succ_le_iff,
    50 		 nat_le_refl];
    51 
    52 val nat_ss = ZF_ss addsimps (nat_simps @ nat_typechecks);
    53 
    54 
    55 (** Addition **)
    56 
    57 val add_type = prove_goalw Arith.thy [add_def]
    58     "[| m:nat;  n:nat |] ==> m #+ n : nat"
    59  (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
    60 
    61 val add_0 = prove_goalw Arith.thy [add_def]
    62     "0 #+ n = n"
    63  (fn _ => [ (rtac rec_0 1) ]);
    64 
    65 val add_succ = prove_goalw Arith.thy [add_def]
    66     "succ(m) #+ n = succ(m #+ n)"
    67  (fn _=> [ (rtac rec_succ 1) ]); 
    68 
    69 (** Multiplication **)
    70 
    71 val mult_type = prove_goalw Arith.thy [mult_def]
    72     "[| m:nat;  n:nat |] ==> m #* n : nat"
    73  (fn prems=>
    74   [ (typechk_tac (prems@[add_type]@nat_typechecks@ZF_typechecks)) ]);
    75 
    76 val mult_0 = prove_goalw Arith.thy [mult_def]
    77     "0 #* n = 0"
    78  (fn _ => [ (rtac rec_0 1) ]);
    79 
    80 val mult_succ = prove_goalw Arith.thy [mult_def]
    81     "succ(m) #* n = n #+ (m #* n)"
    82  (fn _ => [ (rtac rec_succ 1) ]); 
    83 
    84 (** Difference **)
    85 
    86 val diff_type = prove_goalw Arith.thy [diff_def]
    87     "[| m:nat;  n:nat |] ==> m #- n : nat"
    88  (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
    89 
    90 val diff_0 = prove_goalw Arith.thy [diff_def]
    91     "m #- 0 = m"
    92  (fn _ => [ (rtac rec_0 1) ]);
    93 
    94 val diff_0_eq_0 = prove_goalw Arith.thy [diff_def]
    95     "n:nat ==> 0 #- n = 0"
    96  (fn [prem]=>
    97   [ (rtac (prem RS nat_induct) 1),
    98     (ALLGOALS (asm_simp_tac nat_ss)) ]);
    99 
   100 (*Must simplify BEFORE the induction!!  (Else we get a critical pair)
   101   succ(m) #- succ(n)   rewrites to   pred(succ(m) #- n)  *)
   102 val diff_succ_succ = prove_goalw Arith.thy [diff_def]
   103     "[| m:nat;  n:nat |] ==> succ(m) #- succ(n) = m #- n"
   104  (fn prems=>
   105   [ (asm_simp_tac (nat_ss addsimps prems) 1),
   106     (nat_ind_tac "n" prems 1),
   107     (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
   108 
   109 val prems = goal Arith.thy 
   110     "[| m:nat;  n:nat |] ==> m #- n le m";
   111 by (rtac (prems MRS diff_induct) 1);
   112 by (etac leE 3);
   113 by (ALLGOALS
   114     (asm_simp_tac
   115      (nat_ss addsimps (prems @ [le_iff, diff_0, diff_0_eq_0, 
   116 				diff_succ_succ, naturals_are_ordinals]))));
   117 val diff_le_self = result();
   118 
   119 (*** Simplification over add, mult, diff ***)
   120 
   121 val arith_typechecks = [add_type, mult_type, diff_type];
   122 val arith_simps = [add_0, add_succ,
   123 		   mult_0, mult_succ,
   124 		   diff_0, diff_0_eq_0, diff_succ_succ];
   125 
   126 val arith_ss = nat_ss addsimps (arith_simps@arith_typechecks);
   127 
   128 (*** Addition ***)
   129 
   130 (*Associative law for addition*)
   131 val add_assoc = prove_goal Arith.thy 
   132     "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"
   133  (fn prems=>
   134   [ (nat_ind_tac "m" prems 1),
   135     (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
   136 
   137 (*The following two lemmas are used for add_commute and sometimes
   138   elsewhere, since they are safe for rewriting.*)
   139 val add_0_right = prove_goal Arith.thy
   140     "m:nat ==> m #+ 0 = m"
   141  (fn prems=>
   142   [ (nat_ind_tac "m" prems 1),
   143     (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
   144 
   145 val add_succ_right = prove_goal Arith.thy
   146     "m:nat ==> m #+ succ(n) = succ(m #+ n)"
   147  (fn prems=>
   148   [ (nat_ind_tac "m" prems 1),
   149     (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
   150 
   151 (*Commutative law for addition*)  
   152 val add_commute = prove_goal Arith.thy 
   153     "[| m:nat;  n:nat |] ==> m #+ n = n #+ m"
   154  (fn prems=>
   155   [ (nat_ind_tac "n" prems 1),
   156     (ALLGOALS
   157      (asm_simp_tac
   158       (arith_ss addsimps (prems@[add_0_right, add_succ_right])))) ]);
   159 
   160 (*Cancellation law on the left*)
   161 val [knat,eqn] = goal Arith.thy 
   162     "[| k:nat;  k #+ m = k #+ n |] ==> m=n";
   163 by (rtac (eqn RS rev_mp) 1);
   164 by (nat_ind_tac "k" [knat] 1);
   165 by (ALLGOALS (simp_tac arith_ss));
   166 by (fast_tac ZF_cs 1);
   167 val add_left_cancel = result();
   168 
   169 (*** Multiplication ***)
   170 
   171 (*right annihilation in product*)
   172 val mult_0_right = prove_goal Arith.thy 
   173     "m:nat ==> m #* 0 = 0"
   174  (fn prems=>
   175   [ (nat_ind_tac "m" prems 1),
   176     (ALLGOALS (asm_simp_tac (arith_ss addsimps prems)))  ]);
   177 
   178 (*right successor law for multiplication*)
   179 val mult_succ_right = prove_goal Arith.thy 
   180     "!!m n. [| m:nat;  n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
   181  (fn _=>
   182   [ (nat_ind_tac "m" [] 1),
   183     (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))),
   184        (*The final goal requires the commutative law for addition*)
   185     (rtac (add_commute RS subst_context) 1),
   186     (REPEAT (assume_tac 1))  ]);
   187 
   188 (*Commutative law for multiplication*)
   189 val mult_commute = prove_goal Arith.thy 
   190     "[| m:nat;  n:nat |] ==> m #* n = n #* m"
   191  (fn prems=>
   192   [ (nat_ind_tac "m" prems 1),
   193     (ALLGOALS (asm_simp_tac
   194 	     (arith_ss addsimps (prems@[mult_0_right, mult_succ_right])))) ]);
   195 
   196 (*addition distributes over multiplication*)
   197 val add_mult_distrib = prove_goal Arith.thy 
   198     "!!m n. [| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
   199  (fn _=>
   200   [ (etac nat_induct 1),
   201     (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))) ]);
   202 
   203 (*Distributive law on the left; requires an extra typing premise*)
   204 val add_mult_distrib_left = prove_goal Arith.thy 
   205     "[| m:nat;  n:nat;  k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
   206  (fn prems=>
   207       let val mult_commute' = read_instantiate [("m","k")] mult_commute
   208           val ss = arith_ss addsimps ([mult_commute',add_mult_distrib]@prems)
   209       in [ (simp_tac ss 1) ]
   210       end);
   211 
   212 (*Associative law for multiplication*)
   213 val mult_assoc = prove_goal Arith.thy 
   214     "!!m n k. [| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
   215  (fn _=>
   216   [ (etac nat_induct 1),
   217     (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_mult_distrib]))) ]);
   218 
   219 
   220 (*** Difference ***)
   221 
   222 val diff_self_eq_0 = prove_goal Arith.thy 
   223     "m:nat ==> m #- m = 0"
   224  (fn prems=>
   225   [ (nat_ind_tac "m" prems 1),
   226     (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
   227 
   228 (*Addition is the inverse of subtraction*)
   229 goal Arith.thy "!!m n. [| n le m;  m:nat |] ==> n #+ (m#-n) = m";
   230 by (forward_tac [lt_nat_in_nat] 1);
   231 by (etac nat_succI 1);
   232 by (etac rev_mp 1);
   233 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   234 by (ALLGOALS (asm_simp_tac arith_ss));
   235 val add_diff_inverse = result();
   236 
   237 (*Subtraction is the inverse of addition. *)
   238 val [mnat,nnat] = goal Arith.thy
   239     "[| m:nat;  n:nat |] ==> (n#+m) #-n = m";
   240 by (rtac (nnat RS nat_induct) 1);
   241 by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
   242 val diff_add_inverse = result();
   243 
   244 val [mnat,nnat] = goal Arith.thy
   245     "[| m:nat;  n:nat |] ==> n #- (n#+m) = 0";
   246 by (rtac (nnat RS nat_induct) 1);
   247 by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
   248 val diff_add_0 = result();
   249 
   250 
   251 (*** Remainder ***)
   252 
   253 goal Arith.thy "!!m n. [| 0<n;  n le m;  m:nat |] ==> m #- n < m";
   254 by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
   255 by (etac rev_mp 1);
   256 by (etac rev_mp 1);
   257 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   258 by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_le_self,diff_succ_succ])));
   259 val div_termination = result();
   260 
   261 val div_rls =	(*for mod and div*)
   262     nat_typechecks @
   263     [Ord_transrec_type, apply_type, div_termination RS ltD, if_type,
   264      naturals_are_ordinals, not_lt_iff_le RS iffD1];
   265 
   266 val div_ss = ZF_ss addsimps [naturals_are_ordinals, div_termination RS ltD,
   267 			     not_lt_iff_le RS iffD2];
   268 
   269 (*Type checking depends upon termination!*)
   270 goalw Arith.thy [mod_def] "!!m n. [| 0<n;  m:nat;  n:nat |] ==> m mod n : nat";
   271 by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
   272 val mod_type = result();
   273 
   274 goal Arith.thy "!!m n. [| 0<n;  m<n |] ==> m mod n = m";
   275 by (rtac (mod_def RS def_transrec RS trans) 1);
   276 by (asm_simp_tac div_ss 1);
   277 val mod_less = result();
   278 
   279 goal Arith.thy "!!m n. [| 0<n;  n le m;  m:nat |] ==> m mod n = (m#-n) mod n";
   280 by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
   281 by (rtac (mod_def RS def_transrec RS trans) 1);
   282 by (asm_simp_tac div_ss 1);
   283 val mod_geq = result();
   284 
   285 (*** Quotient ***)
   286 
   287 (*Type checking depends upon termination!*)
   288 goalw Arith.thy [div_def]
   289     "!!m n. [| 0<n;  m:nat;  n:nat |] ==> m div n : nat";
   290 by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
   291 val div_type = result();
   292 
   293 goal Arith.thy "!!m n. [| 0<n;  m<n |] ==> m div n = 0";
   294 by (rtac (div_def RS def_transrec RS trans) 1);
   295 by (asm_simp_tac div_ss 1);
   296 val div_less = result();
   297 
   298 goal Arith.thy
   299  "!!m n. [| 0<n;  n le m;  m:nat |] ==> m div n = succ((m#-n) div n)";
   300 by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
   301 by (rtac (div_def RS def_transrec RS trans) 1);
   302 by (asm_simp_tac div_ss 1);
   303 val div_geq = result();
   304 
   305 (*Main Result.*)
   306 goal Arith.thy
   307     "!!m n. [| 0<n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m";
   308 by (etac complete_induct 1);
   309 by (res_inst_tac [("Q","x<n")] (excluded_middle RS disjE) 1);
   310 (*case x<n*)
   311 by (asm_simp_tac (arith_ss addsimps [mod_less, div_less]) 2);
   312 (*case n le x*)
   313 by (asm_full_simp_tac
   314      (arith_ss addsimps [not_lt_iff_le, naturals_are_ordinals,
   315 			 mod_geq, div_geq, add_assoc,
   316 			 div_termination RS ltD, add_diff_inverse]) 1);
   317 val mod_div_equality = result();
   318 
   319 
   320 (**** Additional theorems about "le" ****)
   321 
   322 goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m le m #+ n";
   323 by (etac nat_induct 1);
   324 by (ALLGOALS (asm_simp_tac arith_ss));
   325 val add_le_self = result();
   326 
   327 goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m le n #+ m";
   328 by (rtac (add_commute RS ssubst) 1);
   329 by (REPEAT (ares_tac [add_le_self] 1));
   330 val add_le_self2 = result();
   331 
   332 (** Monotonicity of addition **)
   333 
   334 (*strict, in 1st argument*)
   335 goal Arith.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
   336 by (forward_tac [lt_nat_in_nat] 1);
   337 by (assume_tac 1);
   338 by (etac succ_lt_induct 1);
   339 by (ALLGOALS (asm_simp_tac (arith_ss addsimps [leI])));
   340 val add_lt_mono1 = result();
   341 
   342 (*strict, in both arguments*)
   343 goal Arith.thy "!!i j k l. [| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
   344 by (rtac (add_lt_mono1 RS lt_trans) 1);
   345 by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
   346 by (EVERY [rtac (add_commute RS ssubst) 1,
   347 	   rtac (add_commute RS ssubst) 3,
   348 	   rtac add_lt_mono1 5]);
   349 by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
   350 val add_lt_mono = result();
   351 
   352 (*A [clumsy] way of lifting < monotonicity to le monotonicity *)
   353 val lt_mono::ford::prems = goal Ord.thy
   354      "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j);	\
   355 \        !!i. i:k ==> Ord(f(i));		\
   356 \        i le j;  j:k				\
   357 \     |] ==> f(i) le f(j)";
   358 by (cut_facts_tac prems 1);
   359 by (fast_tac (lt_cs addSIs [lt_mono,ford] addSEs [leE]) 1);
   360 val Ord_lt_mono_imp_le_mono = result();
   361 
   362 (*le monotonicity, 1st argument*)
   363 goal Arith.thy
   364     "!!i j k. [| i le j; j:nat; k:nat |] ==> i#+k le j#+k";
   365 by (res_inst_tac [("f", "%j.j#+k")] Ord_lt_mono_imp_le_mono 1);
   366 by (REPEAT (ares_tac [add_lt_mono1, add_type RS naturals_are_ordinals] 1));
   367 val add_le_mono1 = result();
   368 
   369 (* le monotonicity, BOTH arguments*)
   370 goal Arith.thy
   371     "!!i j k. [| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l";
   372 by (rtac (add_le_mono1 RS le_trans) 1);
   373 by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
   374 by (EVERY [rtac (add_commute RS ssubst) 1,
   375 	   rtac (add_commute RS ssubst) 3,
   376 	   rtac add_le_mono1 5]);
   377 by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
   378 val add_le_mono = result();