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

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();
```