src/ZF/Arith.ML
author lcp
Thu Sep 30 10:10:21 1993 +0100 (1993-09-30)
changeset 14 1c0926788772
parent 6 8ce8c4d13d4d
child 25 3ac1c0c0016e
permissions -rw-r--r--
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext

domrange/image_subset,vimage_subset: deleted needless premise!
misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem

ind-syntax/rule_concl: recoded to avoid exceptions
intr-elim: now checks conclusions of introduction rules

func/fun_disjoint_Un: now uses ex_ex1I
list-fn/hd,tl,drop: new
simpdata/bquant_simps: new

list/list_case_type: restored!

bool.thy: changed 1 from a "def" to a translation
Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML

nat/succ_less_induct: new induction principle
arith/add_mono: new results about monotonicity

simpdata/mem_simps: removed the ones for succ and cons; added succI1,
consI2 to ZF_ss

upair/succ_iff: new, for use with simp_tac (cons_iff already existed)

ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ
nat/nat_0_in_succ: new

ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed
     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_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat];
    46 
    47 val nat_ss = ZF_ss addsimps ([rec_0,rec_succ] @ nat_typechecks);
    48 
    49 
    50 (** Addition **)
    51 
    52 val add_type = prove_goalw Arith.thy [add_def]
    53     "[| m:nat;  n:nat |] ==> m #+ n : nat"
    54  (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
    55 
    56 val add_0 = prove_goalw Arith.thy [add_def]
    57     "0 #+ n = n"
    58  (fn _ => [ (rtac rec_0 1) ]);
    59 
    60 val add_succ = prove_goalw Arith.thy [add_def]
    61     "succ(m) #+ n = succ(m #+ n)"
    62  (fn _=> [ (rtac rec_succ 1) ]); 
    63 
    64 (** Multiplication **)
    65 
    66 val mult_type = prove_goalw Arith.thy [mult_def]
    67     "[| m:nat;  n:nat |] ==> m #* n : nat"
    68  (fn prems=>
    69   [ (typechk_tac (prems@[add_type]@nat_typechecks@ZF_typechecks)) ]);
    70 
    71 val mult_0 = prove_goalw Arith.thy [mult_def]
    72     "0 #* n = 0"
    73  (fn _ => [ (rtac rec_0 1) ]);
    74 
    75 val mult_succ = prove_goalw Arith.thy [mult_def]
    76     "succ(m) #* n = n #+ (m #* n)"
    77  (fn _ => [ (rtac rec_succ 1) ]); 
    78 
    79 (** Difference **)
    80 
    81 val diff_type = prove_goalw Arith.thy [diff_def]
    82     "[| m:nat;  n:nat |] ==> m #- n : nat"
    83  (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
    84 
    85 val diff_0 = prove_goalw Arith.thy [diff_def]
    86     "m #- 0 = m"
    87  (fn _ => [ (rtac rec_0 1) ]);
    88 
    89 val diff_0_eq_0 = prove_goalw Arith.thy [diff_def]
    90     "n:nat ==> 0 #- n = 0"
    91  (fn [prem]=>
    92   [ (rtac (prem RS nat_induct) 1),
    93     (ALLGOALS (asm_simp_tac nat_ss)) ]);
    94 
    95 (*Must simplify BEFORE the induction!!  (Else we get a critical pair)
    96   succ(m) #- succ(n)   rewrites to   pred(succ(m) #- n)  *)
    97 val diff_succ_succ = prove_goalw Arith.thy [diff_def]
    98     "[| m:nat;  n:nat |] ==> succ(m) #- succ(n) = m #- n"
    99  (fn prems=>
   100   [ (asm_simp_tac (nat_ss addsimps prems) 1),
   101     (nat_ind_tac "n" prems 1),
   102     (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
   103 
   104 (*The conclusion is equivalent to m#-n <= m *)
   105 val prems = goal Arith.thy 
   106     "[| m:nat;  n:nat |] ==> m #- n : succ(m)";
   107 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   108 by (resolve_tac prems 1);
   109 by (resolve_tac prems 1);
   110 by (etac succE 3);
   111 by (ALLGOALS
   112     (asm_simp_tac
   113      (nat_ss addsimps (prems @ [succ_iff, diff_0, diff_0_eq_0, 
   114 				diff_succ_succ]))));
   115 val diff_less_succ = result();
   116 
   117 (*** Simplification over add, mult, diff ***)
   118 
   119 val arith_typechecks = [add_type, mult_type, diff_type];
   120 val arith_rews = [add_0, add_succ,
   121 		  mult_0, mult_succ,
   122 		  diff_0, diff_0_eq_0, diff_succ_succ];
   123 
   124 val arith_ss = nat_ss addsimps (arith_rews@arith_typechecks);
   125 
   126 (*** Addition ***)
   127 
   128 (*Associative law for addition*)
   129 val add_assoc = prove_goal Arith.thy 
   130     "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"
   131  (fn prems=>
   132   [ (nat_ind_tac "m" prems 1),
   133     (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
   134 
   135 (*The following two lemmas are used for add_commute and sometimes
   136   elsewhere, since they are safe for rewriting.*)
   137 val add_0_right = prove_goal Arith.thy
   138     "m:nat ==> m #+ 0 = m"
   139  (fn prems=>
   140   [ (nat_ind_tac "m" prems 1),
   141     (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
   142 
   143 val add_succ_right = prove_goal Arith.thy
   144     "m:nat ==> m #+ succ(n) = succ(m #+ n)"
   145  (fn prems=>
   146   [ (nat_ind_tac "m" prems 1),
   147     (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
   148 
   149 (*Commutative law for addition*)  
   150 val add_commute = prove_goal Arith.thy 
   151     "[| m:nat;  n:nat |] ==> m #+ n = n #+ m"
   152  (fn prems=>
   153   [ (nat_ind_tac "n" prems 1),
   154     (ALLGOALS
   155      (asm_simp_tac
   156       (arith_ss addsimps (prems@[add_0_right, add_succ_right])))) ]);
   157 
   158 (*Cancellation law on the left*)
   159 val [knat,eqn] = goal Arith.thy 
   160     "[| k:nat;  k #+ m = k #+ n |] ==> m=n";
   161 by (rtac (eqn RS rev_mp) 1);
   162 by (nat_ind_tac "k" [knat] 1);
   163 by (ALLGOALS (simp_tac arith_ss));
   164 by (fast_tac ZF_cs 1);
   165 val add_left_cancel = result();
   166 
   167 (*** Multiplication ***)
   168 
   169 (*right annihilation in product*)
   170 val mult_0_right = prove_goal Arith.thy 
   171     "m:nat ==> m #* 0 = 0"
   172  (fn prems=>
   173   [ (nat_ind_tac "m" prems 1),
   174     (ALLGOALS (asm_simp_tac (arith_ss addsimps prems)))  ]);
   175 
   176 (*right successor law for multiplication*)
   177 val mult_succ_right = prove_goal Arith.thy 
   178     "!!m n. [| m:nat;  n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
   179  (fn _=>
   180   [ (nat_ind_tac "m" [] 1),
   181     (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))),
   182        (*The final goal requires the commutative law for addition*)
   183     (rtac (add_commute RS subst_context) 1),
   184     (REPEAT (assume_tac 1))  ]);
   185 
   186 (*Commutative law for multiplication*)
   187 val mult_commute = prove_goal Arith.thy 
   188     "[| m:nat;  n:nat |] ==> m #* n = n #* m"
   189  (fn prems=>
   190   [ (nat_ind_tac "m" prems 1),
   191     (ALLGOALS (asm_simp_tac
   192 	     (arith_ss addsimps (prems@[mult_0_right, mult_succ_right])))) ]);
   193 
   194 (*addition distributes over multiplication*)
   195 val add_mult_distrib = prove_goal Arith.thy 
   196     "!!m n. [| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
   197  (fn _=>
   198   [ (etac nat_induct 1),
   199     (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))) ]);
   200 
   201 (*Distributive law on the left; requires an extra typing premise*)
   202 val add_mult_distrib_left = prove_goal Arith.thy 
   203     "[| m:nat;  n:nat;  k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
   204  (fn prems=>
   205       let val mult_commute' = read_instantiate [("m","k")] mult_commute
   206           val ss = arith_ss addsimps ([mult_commute',add_mult_distrib]@prems)
   207       in [ (simp_tac ss 1) ]
   208       end);
   209 
   210 (*Associative law for multiplication*)
   211 val mult_assoc = prove_goal Arith.thy 
   212     "!!m n k. [| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
   213  (fn _=>
   214   [ (etac nat_induct 1),
   215     (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_mult_distrib]))) ]);
   216 
   217 
   218 (*** Difference ***)
   219 
   220 val diff_self_eq_0 = prove_goal Arith.thy 
   221     "m:nat ==> m #- m = 0"
   222  (fn prems=>
   223   [ (nat_ind_tac "m" prems 1),
   224     (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
   225 
   226 (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
   227 val notless::prems = goal Arith.thy
   228     "[| ~m:n;  m:nat;  n:nat |] ==> n #+ (m#-n) = m";
   229 by (rtac (notless RS rev_mp) 1);
   230 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   231 by (resolve_tac prems 1);
   232 by (resolve_tac prems 1);
   233 by (ALLGOALS (asm_simp_tac
   234 	      (arith_ss addsimps (prems@[succ_mem_succ_iff, nat_0_in_succ,
   235 					 naturals_are_ordinals]))));
   236 val add_diff_inverse = result();
   237 
   238 
   239 (*Subtraction is the inverse of addition. *)
   240 val [mnat,nnat] = goal Arith.thy
   241     "[| m:nat;  n:nat |] ==> (n#+m) #-n = m";
   242 by (rtac (nnat RS nat_induct) 1);
   243 by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
   244 val diff_add_inverse = result();
   245 
   246 val [mnat,nnat] = goal Arith.thy
   247     "[| m:nat;  n:nat |] ==> n #- (n#+m) = 0";
   248 by (rtac (nnat RS nat_induct) 1);
   249 by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
   250 val diff_add_0 = result();
   251 
   252 
   253 (*** Remainder ***)
   254 
   255 (*In ordinary notation: if 0<n and n<=m then m-n < m *)
   256 goal Arith.thy "!!m n. [| 0:n; ~ m:n;  m:nat;  n:nat |] ==> m #- n : m";
   257 by (etac rev_mp 1);
   258 by (etac rev_mp 1);
   259 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   260 by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_less_succ,diff_succ_succ])));
   261 val div_termination = result();
   262 
   263 val div_rls =
   264     [Ord_transrec_type, apply_type, div_termination, if_type] @ 
   265     nat_typechecks;
   266 
   267 (*Type checking depends upon termination!*)
   268 val prems = goalw Arith.thy [mod_def]
   269     "[| 0:n;  m:nat;  n:nat |] ==> m mod n : nat";
   270 by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
   271 val mod_type = result();
   272 
   273 val div_ss = ZF_ss addsimps [naturals_are_ordinals,div_termination];
   274 
   275 val prems = goal Arith.thy "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m mod n = m";
   276 by (rtac (mod_def RS def_transrec RS trans) 1);
   277 by (simp_tac (div_ss addsimps prems) 1);
   278 val mod_less = result();
   279 
   280 val prems = goal Arith.thy
   281     "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m mod n = (m#-n) mod n";
   282 by (rtac (mod_def RS def_transrec RS trans) 1);
   283 by (simp_tac (div_ss addsimps prems) 1);
   284 val mod_geq = result();
   285 
   286 (*** Quotient ***)
   287 
   288 (*Type checking depends upon termination!*)
   289 val prems = goalw Arith.thy [div_def]
   290     "[| 0:n;  m:nat;  n:nat |] ==> m div n : nat";
   291 by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
   292 val div_type = result();
   293 
   294 val prems = goal Arith.thy
   295     "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m div n = 0";
   296 by (rtac (div_def RS def_transrec RS trans) 1);
   297 by (simp_tac (div_ss addsimps prems) 1);
   298 val div_less = result();
   299 
   300 val prems = goal Arith.thy
   301     "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m div n = succ((m#-n) div n)";
   302 by (rtac (div_def RS def_transrec RS trans) 1);
   303 by (simp_tac (div_ss addsimps prems) 1);
   304 val div_geq = result();
   305 
   306 (*Main Result.*)
   307 val prems = goal Arith.thy
   308     "[| 0:n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m";
   309 by (res_inst_tac [("i","m")] complete_induct 1);
   310 by (resolve_tac prems 1);
   311 by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1);
   312 by (ALLGOALS 
   313     (asm_simp_tac
   314      (arith_ss addsimps ([mod_type,div_type] @ prems @
   315         [mod_less,mod_geq, div_less, div_geq,
   316 	 add_assoc, add_diff_inverse, div_termination]))));
   317 val mod_div_equality = result();
   318 
   319 
   320 (**** Additional theorems about "less than" ****)
   321 
   322 val [mnat,nnat] = goal Arith.thy
   323     "[| m:nat;  n:nat |] ==> ~ (m #+ n) : n";
   324 by (rtac (mnat RS nat_induct) 1);
   325 by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mem_not_refl])));
   326 by (rtac notI 1);
   327 by (etac notE 1);
   328 by (etac (succI1 RS Ord_trans) 1);
   329 by (rtac (nnat RS naturals_are_ordinals) 1);
   330 val add_not_less_self = result();
   331 
   332 val [mnat,nnat] = goal Arith.thy
   333     "[| m:nat;  n:nat |] ==> m : succ(m #+ n)";
   334 by (rtac (mnat RS nat_induct) 1);
   335 (*May not simplify even with ZF_ss because it would expand m:succ(...) *)
   336 by (rtac (add_0 RS ssubst) 1);
   337 by (rtac (add_succ RS ssubst) 2);
   338 by (REPEAT (ares_tac [nnat, nat_0_in_succ, succ_mem_succI, 
   339 		      naturals_are_ordinals, nat_succI, add_type] 1));
   340 val add_less_succ_self = result();
   341 
   342 goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m <= m #+ n";
   343 by (rtac (add_less_succ_self RS member_succD) 1);
   344 by (REPEAT (ares_tac [naturals_are_ordinals, add_type] 1));
   345 val add_leq_self = result();
   346 
   347 goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m <= n #+ m";
   348 by (rtac (add_commute RS ssubst) 1);
   349 by (REPEAT (ares_tac [add_leq_self] 1));
   350 val add_leq_self2 = result();
   351 
   352 (** Monotonicity of addition **)
   353 
   354 (*strict, in 1st argument*)
   355 goal Arith.thy "!!i j k. [| i:j; j:nat |] ==> i#+k : j#+k";
   356 by (etac succ_less_induct 1);
   357 by (ALLGOALS (asm_simp_tac (arith_ss addsimps [succ_iff])));
   358 val add_less_mono1 = result();
   359 
   360 (*strict, in both arguments*)
   361 goal Arith.thy "!!i j k l. [| i:j; k:l; j:nat; l:nat |] ==> i#+k : j#+l";
   362 by (rtac (add_less_mono1 RS Ord_trans) 1);
   363 by (REPEAT_FIRST (ares_tac [add_type, naturals_are_ordinals]));
   364 by (EVERY [rtac (add_commute RS ssubst) 1,
   365 	   rtac (add_commute RS ssubst) 3,
   366 	   rtac add_less_mono1 5]);
   367 by (REPEAT (ares_tac [Ord_nat RSN (3,Ord_trans)] 1));
   368 val add_less_mono = result();
   369 
   370 (*A [clumsy] way of lifting < monotonictity to <= monotonicity *)
   371 val less_mono::ford::prems = goal Ord.thy
   372      "[| !!i j. [| i:j; j:k |] ==> f(i) : f(j);	\
   373 \        !!i. i:k ==> f(i):k;			\
   374 \        i<=j;  i:k;  j:k;  Ord(k)		\
   375 \     |] ==> f(i) <= f(j)";
   376 by (cut_facts_tac prems 1);
   377 by (rtac member_succD 1);
   378 by (dtac member_succI 1);
   379 by (fast_tac (ZF_cs addSIs [less_mono]) 3);
   380 by (REPEAT (ares_tac [ford,Ord_in_Ord] 1));
   381 val Ord_less_mono_imp_mono = result();
   382 
   383 (*<=, in 1st argument*)
   384 goal Arith.thy
   385     "!!i j k. [| i<=j; i:nat; j:nat; k:nat |] ==> i#+k <= j#+k";
   386 by (res_inst_tac [("f", "%j.j#+k")] Ord_less_mono_imp_mono 1);
   387 by (REPEAT (ares_tac [add_less_mono1, add_type, Ord_nat] 1));
   388 val add_mono1 = result();
   389 
   390 (*<=, in both arguments*)
   391 goal Arith.thy
   392     "!!i j k. [| i<=j; k<=l; i:nat; j:nat; k:nat; l:nat |] ==> i#+k <= j#+l";
   393 by (rtac (add_mono1 RS subset_trans) 1);
   394 by (REPEAT (assume_tac 1));
   395 by (EVERY [rtac (add_commute RS ssubst) 1,
   396 	   rtac (add_commute RS ssubst) 3,
   397 	   rtac add_mono1 5]);
   398 by (REPEAT (assume_tac 1));
   399 val add_mono = result();