src/ZF/Nat.ML
author lcp
Fri Sep 17 16:16:38 1993 +0200 (1993-09-17)
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 15 6c6d2f6e3185
permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
     1 (*  Title: 	ZF/nat.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 For nat.thy.  Natural numbers in Zermelo-Fraenkel Set Theory 
     7 *)
     8 
     9 open Nat;
    10 
    11 goal Nat.thy "bnd_mono(Inf, %X. {0} Un {succ(i). i:X})";
    12 by (rtac bnd_monoI 1);
    13 by (REPEAT (ares_tac [subset_refl, RepFun_mono, Un_mono] 2)); 
    14 by (cut_facts_tac [infinity] 1);
    15 by (fast_tac ZF_cs 1);
    16 val nat_bnd_mono = result();
    17 
    18 (* nat = {0} Un {succ(x). x:nat} *)
    19 val nat_unfold = nat_bnd_mono RS (nat_def RS def_lfp_Tarski);
    20 
    21 (** Type checking of 0 and successor **)
    22 
    23 goal Nat.thy "0 : nat";
    24 by (rtac (nat_unfold RS ssubst) 1);
    25 by (rtac (singletonI RS UnI1) 1);
    26 val nat_0I = result();
    27 
    28 val prems = goal Nat.thy "n : nat ==> succ(n) : nat";
    29 by (rtac (nat_unfold RS ssubst) 1);
    30 by (rtac (RepFunI RS UnI2) 1);
    31 by (resolve_tac prems 1);
    32 val nat_succI = result();
    33 
    34 goalw Nat.thy [one_def] "1 : nat";
    35 by (rtac (nat_0I RS nat_succI) 1);
    36 val nat_1I = result();
    37 
    38 goal Nat.thy "bool <= nat";
    39 by (REPEAT (ares_tac [subsetI,nat_0I,nat_1I] 1 ORELSE etac boolE 1));
    40 val bool_subset_nat = result();
    41 
    42 val bool_into_nat = bool_subset_nat RS subsetD;
    43 
    44 
    45 (** Injectivity properties and induction **)
    46 
    47 (*Mathematical induction*)
    48 val major::prems = goal Nat.thy
    49     "[| n: nat;  P(0);  !!x. [| x: nat;  P(x) |] ==> P(succ(x)) |] ==> P(n)";
    50 by (rtac ([nat_def, nat_bnd_mono, major] MRS def_induct) 1);
    51 by (fast_tac (ZF_cs addIs prems) 1);
    52 val nat_induct = result();
    53 
    54 (*Perform induction on n, then prove the n:nat subgoal using prems. *)
    55 fun nat_ind_tac a prems i = 
    56     EVERY [res_inst_tac [("n",a)] nat_induct i,
    57 	   rename_last_tac a ["1"] (i+2),
    58 	   ares_tac prems i];
    59 
    60 val major::prems = goal Nat.thy
    61     "[| n: nat;  n=0 ==> P;  !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P";
    62 br (major RS (nat_unfold RS equalityD1 RS subsetD) RS UnE) 1;
    63 by (DEPTH_SOLVE (eresolve_tac [singletonE,RepFunE] 1
    64           ORELSE ares_tac prems 1));
    65 val natE = result();
    66 
    67 val prems = goal Nat.thy "n: nat ==> Ord(n)";
    68 by (nat_ind_tac "n" prems 1);
    69 by (REPEAT (ares_tac [Ord_0, Ord_succ] 1));
    70 val naturals_are_ordinals = result();
    71 
    72 goal Nat.thy "!!n. n: nat ==> n=0 | 0:n";
    73 by (etac nat_induct 1);
    74 by (fast_tac ZF_cs 1);
    75 by (fast_tac (ZF_cs addIs [naturals_are_ordinals RS Ord_0_mem_succ]) 1);
    76 val natE0 = result();
    77 
    78 goal Nat.thy "Ord(nat)";
    79 by (rtac OrdI 1);
    80 by (etac (naturals_are_ordinals RS Ord_is_Transset) 2);
    81 by (rewtac Transset_def);
    82 by (rtac ballI 1);
    83 by (etac nat_induct 1);
    84 by (REPEAT (ares_tac [empty_subsetI,succ_subsetI] 1));
    85 val Ord_nat = result();
    86 
    87 (** Variations on mathematical induction **)
    88 
    89 (*complete induction*)
    90 val complete_induct = Ord_nat RSN (2, Ord_induct);
    91 
    92 val prems = goal Nat.thy
    93     "[| m: nat;  n: nat;  \
    94 \       !!x. [| x: nat;  m<=x;  P(x) |] ==> P(succ(x)) \
    95 \    |] ==> m <= n --> P(m) --> P(n)";
    96 by (nat_ind_tac "n" prems 1);
    97 by (ALLGOALS
    98     (asm_simp_tac
    99      (ZF_ss addsimps (prems@distrib_rews@[subset_empty_iff, subset_succ_iff, 
   100 					 Ord_nat RS Ord_in_Ord]))));
   101 val nat_induct_from_lemma = result();
   102 
   103 (*Induction starting from m rather than 0*)
   104 val prems = goal Nat.thy
   105     "[| m <= n;  m: nat;  n: nat;  \
   106 \       P(m);  \
   107 \       !!x. [| x: nat;  m<=x;  P(x) |] ==> P(succ(x)) \
   108 \    |] ==> P(n)";
   109 by (rtac (nat_induct_from_lemma RS mp RS mp) 1);
   110 by (REPEAT (ares_tac prems 1));
   111 val nat_induct_from = result();
   112 
   113 (*Induction suitable for subtraction and less-than*)
   114 val prems = goal Nat.thy
   115     "[| m: nat;  n: nat;  \
   116 \       !!x. [| x: nat |] ==> P(x,0);  \
   117 \       !!y. [| y: nat |] ==> P(0,succ(y));  \
   118 \       !!x y. [| x: nat;  y: nat;  P(x,y) |] ==> P(succ(x),succ(y))  \
   119 \    |] ==> P(m,n)";
   120 by (res_inst_tac [("x","m")] bspec 1);
   121 by (resolve_tac prems 2);
   122 by (nat_ind_tac "n" prems 1);
   123 by (rtac ballI 2);
   124 by (nat_ind_tac "x" [] 2);
   125 by (REPEAT (ares_tac (prems@[ballI]) 1 ORELSE etac bspec 1));
   126 val diff_induct = result();
   127 
   128 (** nat_case **)
   129 
   130 goalw Nat.thy [nat_case_def] "nat_case(a,b,0) = a";
   131 by (fast_tac (ZF_cs addIs [the_equality]) 1);
   132 val nat_case_0 = result();
   133 
   134 goalw Nat.thy [nat_case_def] "nat_case(a,b,succ(m)) = b(m)";
   135 by (fast_tac (ZF_cs addIs [the_equality]) 1);
   136 val nat_case_succ = result();
   137 
   138 val major::prems = goal Nat.thy
   139     "[| n: nat;  a: C(0);  !!m. m: nat ==> b(m): C(succ(m))  \
   140 \    |] ==> nat_case(a,b,n) : C(n)";
   141 by (rtac (major RS nat_induct) 1);
   142 by (REPEAT (resolve_tac [nat_case_0 RS ssubst,
   143 			 nat_case_succ RS ssubst] 1 
   144        THEN resolve_tac prems 1));
   145 by (assume_tac 1);
   146 val nat_case_type = result();
   147 
   148 
   149 (** nat_rec -- used to define eclose and transrec, then obsolete **)
   150 
   151 val nat_rec_trans = wf_Memrel RS (nat_rec_def RS def_wfrec RS trans);
   152 
   153 goal Nat.thy "nat_rec(0,a,b) = a";
   154 by (rtac nat_rec_trans 1);
   155 by (rtac nat_case_0 1);
   156 val nat_rec_0 = result();
   157 
   158 val [prem] = goal Nat.thy 
   159     "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))";
   160 val nat_rec_ss = ZF_ss 
   161       addsimps [prem, nat_case_succ, nat_succI, Memrel_iff, 
   162 		vimage_singleton_iff];
   163 by (rtac nat_rec_trans 1);
   164 by (simp_tac nat_rec_ss 1);
   165 val nat_rec_succ = result();
   166 
   167 (** The union of two natural numbers is a natural number -- their maximum **)
   168 
   169 (*  [| ?i : nat; ?j : nat |] ==> ?i Un ?j : nat  *)
   170 val Un_nat_type = standard (Ord_nat RSN (3,Ord_member_UnI));
   171 
   172 (*  [| ?i : nat; ?j : nat |] ==> ?i Int ?j : nat  *)
   173 val Int_nat_type = standard (Ord_nat RSN (3,Ord_member_IntI));
   174