src/ZF/epsilon.ML
author lcp
Fri Sep 17 16:16:38 1993 +0200 (1993-09-17)
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 14 1c0926788772
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/epsilon.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 For epsilon.thy.  Epsilon induction and recursion
     7 *)
     8 
     9 open Epsilon;
    10 
    11 (*** Basic closure properties ***)
    12 
    13 goalw Epsilon.thy [eclose_def] "A <= eclose(A)";
    14 by (rtac (nat_rec_0 RS equalityD2 RS subset_trans) 1);
    15 br (nat_0I RS UN_upper) 1;
    16 val arg_subset_eclose = result();
    17 
    18 val arg_into_eclose = arg_subset_eclose RS subsetD;
    19 
    20 goalw Epsilon.thy [eclose_def,Transset_def] "Transset(eclose(A))";
    21 by (rtac (subsetI RS ballI) 1);
    22 by (etac UN_E 1);
    23 by (rtac (nat_succI RS UN_I) 1);
    24 by (assume_tac 1);
    25 by (etac (nat_rec_succ RS ssubst) 1);
    26 by (etac UnionI 1);
    27 by (assume_tac 1);
    28 val Transset_eclose = result();
    29 
    30 (* x : eclose(A) ==> x <= eclose(A) *)
    31 val eclose_subset = 
    32     standard (rewrite_rule [Transset_def] Transset_eclose RS bspec);
    33 
    34 (* [| A : eclose(B); c : A |] ==> c : eclose(B) *)
    35 val ecloseD = standard (eclose_subset RS subsetD);
    36 
    37 val arg_in_eclose_sing = arg_subset_eclose RS singleton_subsetD;
    38 val arg_into_eclose_sing = arg_in_eclose_sing RS ecloseD;
    39 
    40 (* This is epsilon-induction for eclose(A); see also eclose_induct_down...
    41    [| a: eclose(A);  !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) 
    42    |] ==> P(a) 
    43 *)
    44 val eclose_induct = standard (Transset_eclose RSN (2, Transset_induct));
    45 
    46 (*Epsilon induction*)
    47 val prems = goal Epsilon.thy
    48     "[| !!x. ALL y:x. P(y) ==> P(x) |]  ==>  P(a)";
    49 by (rtac (arg_in_eclose_sing RS eclose_induct) 1);
    50 by (eresolve_tac prems 1);
    51 val eps_induct = result();
    52 
    53 (*Perform epsilon-induction on i. *)
    54 fun eps_ind_tac a = 
    55     EVERY' [res_inst_tac [("a",a)] eps_induct,
    56 	    rename_last_tac a ["1"]];
    57 
    58 
    59 (*** Leastness of eclose ***)
    60 
    61 (** eclose(A) is the least transitive set including A as a subset. **)
    62 
    63 goalw Epsilon.thy [Transset_def]
    64     "!!X A n. [| Transset(X);  A<=X;  n: nat |] ==> \
    65 \             nat_rec(n, A, %m r. Union(r)) <= X";
    66 by (etac nat_induct 1);
    67 by (asm_simp_tac (ZF_ss addsimps [nat_rec_0]) 1);
    68 by (asm_simp_tac (ZF_ss addsimps [nat_rec_succ]) 1);
    69 by (fast_tac ZF_cs 1);
    70 val eclose_least_lemma = result();
    71 
    72 goalw Epsilon.thy [eclose_def]
    73      "!!X A. [| Transset(X);  A<=X |] ==> eclose(A) <= X";
    74 br (eclose_least_lemma RS UN_least) 1;
    75 by (REPEAT (assume_tac 1));
    76 val eclose_least = result();
    77 
    78 (*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
    79 val [major,base,step] = goal Epsilon.thy
    80     "[| a: eclose(b);						\
    81 \       !!y.   [| y: b |] ==> P(y);				\
    82 \       !!y z. [| y: eclose(b);  P(y);  z: y |] ==> P(z)	\
    83 \    |] ==> P(a)";
    84 by (rtac (major RSN (3, eclose_least RS subsetD RS CollectD2)) 1);
    85 by (rtac (CollectI RS subsetI) 2);
    86 by (etac (arg_subset_eclose RS subsetD) 2);
    87 by (etac base 2);
    88 by (rewtac Transset_def);
    89 by (fast_tac (ZF_cs addEs [step,ecloseD]) 1);
    90 val eclose_induct_down = result();
    91 
    92 goal Epsilon.thy "!!X. Transset(X) ==> eclose(X) = X";
    93 be ([eclose_least, arg_subset_eclose] MRS equalityI) 1;
    94 br subset_refl 1;
    95 val Transset_eclose_eq_arg = result();
    96 
    97 
    98 (*** Epsilon recursion ***)
    99 
   100 (*Unused...*)
   101 goal Epsilon.thy "!!A B C. [| A: eclose(B);  B: eclose(C) |] ==> A: eclose(C)";
   102 by (rtac ([Transset_eclose, eclose_subset] MRS eclose_least RS subsetD) 1);
   103 by (REPEAT (assume_tac 1));
   104 val mem_eclose_trans = result();
   105 
   106 (*Variant of the previous lemma in a useable form for the sequel*)
   107 goal Epsilon.thy
   108     "!!A B C. [| A: eclose({B});  B: eclose({C}) |] ==> A: eclose({C})";
   109 by (rtac ([Transset_eclose, singleton_subsetI] MRS eclose_least RS subsetD) 1);
   110 by (REPEAT (assume_tac 1));
   111 val mem_eclose_sing_trans = result();
   112 
   113 goalw Epsilon.thy [Transset_def]
   114     "!!i j. [| Transset(i);  j:i |] ==> Memrel(i)-``{j} = j";
   115 by (fast_tac (eq_cs addSIs [MemrelI] addSEs [MemrelE]) 1);
   116 val under_Memrel = result();
   117 
   118 (* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
   119 val under_Memrel_eclose = Transset_eclose RS under_Memrel;
   120 
   121 val wfrec_ssubst = standard (wf_Memrel RS wfrec RS ssubst);
   122 
   123 val [kmemj,jmemi] = goal Epsilon.thy
   124     "[| k:eclose({j});  j:eclose({i}) |] ==> \
   125 \    wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)";
   126 by (rtac (kmemj RS eclose_induct) 1);
   127 by (rtac wfrec_ssubst 1);
   128 by (rtac wfrec_ssubst 1);
   129 by (asm_simp_tac (ZF_ss addsimps [under_Memrel_eclose,
   130 				  jmemi RSN (2,mem_eclose_sing_trans)]) 1);
   131 val wfrec_eclose_eq = result();
   132 
   133 val [prem] = goal Epsilon.thy
   134     "k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)";
   135 by (rtac (arg_in_eclose_sing RS wfrec_eclose_eq) 1);
   136 by (rtac (prem RS arg_into_eclose_sing) 1);
   137 val wfrec_eclose_eq2 = result();
   138 
   139 goalw Epsilon.thy [transrec_def]
   140     "transrec(a,H) = H(a, lam x:a. transrec(x,H))";
   141 by (rtac wfrec_ssubst 1);
   142 by (simp_tac (ZF_ss addsimps [wfrec_eclose_eq2, arg_in_eclose_sing,
   143 			      under_Memrel_eclose]) 1);
   144 val transrec = result();
   145 
   146 (*Avoids explosions in proofs; resolve it with a meta-level definition.*)
   147 val rew::prems = goal Epsilon.thy
   148     "[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, lam x:a. f(x))";
   149 by (rewtac rew);
   150 by (REPEAT (resolve_tac (prems@[transrec]) 1));
   151 val def_transrec = result();
   152 
   153 val prems = goal Epsilon.thy
   154     "[| !!x u. [| x:eclose({a});  u: Pi(x,B) |] ==> H(x,u) : B(x)   \
   155 \    |]  ==> transrec(a,H) : B(a)";
   156 by (res_inst_tac [("i", "a")] (arg_in_eclose_sing RS eclose_induct) 1);
   157 by (rtac (transrec RS ssubst) 1);
   158 by (REPEAT (ares_tac (prems @ [lam_type]) 1 ORELSE etac bspec 1));
   159 val transrec_type = result();
   160 
   161 goal Epsilon.thy "!!i. Ord(i) ==> eclose({i}) <= succ(i)";
   162 by (etac (Ord_is_Transset RS Transset_succ RS eclose_least) 1);
   163 by (rtac (succI1 RS singleton_subsetI) 1);
   164 val eclose_sing_Ord = result();
   165 
   166 val prems = goal Epsilon.thy
   167     "[| j: i;  Ord(i);  \
   168 \       !!x u. [| x: i;  u: Pi(x,B) |] ==> H(x,u) : B(x)   \
   169 \    |]  ==> transrec(j,H) : B(j)";
   170 by (rtac transrec_type 1);
   171 by (resolve_tac prems 1);
   172 by (rtac (Ord_in_Ord RS eclose_sing_Ord RS subsetD RS succE) 1);
   173 by (DEPTH_SOLVE (ares_tac prems 1 ORELSE eresolve_tac [ssubst,Ord_trans] 1));
   174 val Ord_transrec_type = result();
   175 
   176 (*** Rank ***)
   177 
   178 (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
   179 goal Epsilon.thy "rank(a) = (UN y:a. succ(rank(y)))";
   180 by (rtac (rank_def RS def_transrec RS ssubst) 1);
   181 by (simp_tac ZF_ss 1);
   182 val rank = result();
   183 
   184 goal Epsilon.thy "Ord(rank(a))";
   185 by (eps_ind_tac "a" 1);
   186 by (rtac (rank RS ssubst) 1);
   187 by (rtac (Ord_succ RS Ord_UN) 1);
   188 by (etac bspec 1);
   189 by (assume_tac 1);
   190 val Ord_rank = result();
   191 
   192 val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i";
   193 by (rtac (major RS trans_induct) 1);
   194 by (rtac (rank RS ssubst) 1);
   195 by (asm_simp_tac (ZF_ss addsimps [Ord_equality]) 1);
   196 val rank_of_Ord = result();
   197 
   198 val [prem] = goal Epsilon.thy "a:b ==> rank(a) : rank(b)";
   199 by (res_inst_tac [("a1","b")] (rank RS ssubst) 1);
   200 by (rtac (prem RS UN_I) 1);
   201 by (rtac succI1 1);
   202 val rank_lt = result();
   203 
   204 val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) : rank(b)";
   205 by (rtac (major RS eclose_induct_down) 1);
   206 by (etac rank_lt 1);
   207 by (etac (rank_lt RS Ord_trans) 1);
   208 by (assume_tac 1);
   209 by (rtac Ord_rank 1);
   210 val eclose_rank_lt = result();
   211 
   212 goal Epsilon.thy "!!a b. a<=b ==> rank(a) <= rank(b)";
   213 by (rtac (rank RS ssubst) 1);
   214 by (rtac (rank RS ssubst) 1);
   215 by (etac UN_mono 1);
   216 by (rtac subset_refl 1);
   217 val rank_mono = result();
   218 
   219 goal Epsilon.thy "rank(Pow(a)) = succ(rank(a))";
   220 by (rtac (rank RS trans) 1);
   221 by (rtac equalityI 1);
   222 by (fast_tac ZF_cs 2);
   223 by (rtac UN_least 1);
   224 by (etac (PowD RS rank_mono RS Ord_succ_mono) 1);
   225 by (rtac Ord_rank 1);
   226 by (rtac Ord_rank 1);
   227 val rank_Pow = result();
   228 
   229 goal Epsilon.thy "rank(0) = 0";
   230 by (rtac (rank RS trans) 1);
   231 by (fast_tac (ZF_cs addSIs [equalityI]) 1);
   232 val rank_0 = result();
   233 
   234 goal Epsilon.thy "rank(succ(x)) = succ(rank(x))";
   235 by (rtac (rank RS trans) 1);
   236 br ([UN_least, succI1 RS UN_upper] MRS equalityI) 1;
   237 be succE 1;
   238 by (fast_tac ZF_cs 1);
   239 by (REPEAT (ares_tac [Ord_succ_mono,Ord_rank,OrdmemD,rank_lt] 1));
   240 val rank_succ = result();
   241 
   242 goal Epsilon.thy "rank(Union(A)) = (UN x:A. rank(x))";
   243 by (rtac equalityI 1);
   244 by (rtac (rank_mono RS UN_least) 2);
   245 by (etac Union_upper 2);
   246 by (rtac (rank RS ssubst) 1);
   247 by (rtac UN_least 1);
   248 by (etac UnionE 1);
   249 by (rtac subset_trans 1);
   250 by (etac (RepFunI RS Union_upper) 2);
   251 by (etac (rank_lt RS Ord_succ_subsetI) 1);
   252 by (rtac Ord_rank 1);
   253 val rank_Union = result();
   254 
   255 goal Epsilon.thy "rank(eclose(a)) = rank(a)";
   256 by (rtac equalityI 1);
   257 by (rtac (arg_subset_eclose RS rank_mono) 2);
   258 by (res_inst_tac [("a1","eclose(a)")] (rank RS ssubst) 1);
   259 by (rtac UN_least 1);
   260 by (etac ([eclose_rank_lt, Ord_rank] MRS Ord_succ_subsetI) 1);
   261 val rank_eclose = result();
   262 
   263 (*  [| i: j; j: rank(a) |] ==> i: rank(a)  *)
   264 val rank_trans = Ord_rank RSN (3, Ord_trans);
   265 
   266 goalw Epsilon.thy [Pair_def] "rank(a) : rank(<a,b>)";
   267 by (rtac (consI1 RS rank_lt RS Ord_trans) 1);
   268 by (rtac (consI1 RS consI2 RS rank_lt) 1);
   269 by (rtac Ord_rank 1);
   270 val rank_pair1 = result();
   271 
   272 goalw Epsilon.thy [Pair_def] "rank(b) : rank(<a,b>)";
   273 by (rtac (consI1 RS consI2 RS rank_lt RS Ord_trans) 1);
   274 by (rtac (consI1 RS consI2 RS rank_lt) 1);
   275 by (rtac Ord_rank 1);
   276 val rank_pair2 = result();
   277 
   278 goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inl_def] "rank(a) : rank(Inl(a))";
   279 by (rtac rank_pair2 1);
   280 val rank_Inl = result();
   281 
   282 goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inr_def] "rank(a) : rank(Inr(a))";
   283 by (rtac rank_pair2 1);
   284 val rank_Inr = result();
   285 
   286 val [major] = goal Epsilon.thy "i: rank(a) ==> (EX x:a. i<=rank(x))";
   287 by (resolve_tac ([major] RL [rank RS subst] RL [UN_E]) 1);
   288 by (rtac bexI 1);
   289 by (etac member_succD 1);
   290 by (rtac Ord_rank 1);
   291 by (assume_tac 1);
   292 val rank_implies_mem = result();
   293 
   294 
   295 (*** Corollaries of leastness ***)
   296 
   297 goal Epsilon.thy "!!A B. A:B ==> eclose(A)<=eclose(B)";
   298 by (rtac (Transset_eclose RS eclose_least) 1);
   299 by (etac (arg_into_eclose RS eclose_subset) 1);
   300 val mem_eclose_subset = result();
   301 
   302 goal Epsilon.thy "!!A B. A<=B ==> eclose(A) <= eclose(B)";
   303 by (rtac (Transset_eclose RS eclose_least) 1);
   304 by (etac subset_trans 1);
   305 by (rtac arg_subset_eclose 1);
   306 val eclose_mono = result();
   307 
   308 (** Idempotence of eclose **)
   309 
   310 goal Epsilon.thy "eclose(eclose(A)) = eclose(A)";
   311 by (rtac equalityI 1);
   312 by (rtac ([Transset_eclose, subset_refl] MRS eclose_least) 1);
   313 by (rtac arg_subset_eclose 1);
   314 val eclose_idem = result();