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
```