src/ZF/epsilon.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 6 8ce8c4d13d4d
permissions -rw-r--r--
Initial revision
     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 addrews [nat_rec_0]) 1);
    68 by (ASM_SIMP_TAC (ZF_ss addrews [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 (wf_ss addrews [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 (wf_ss addrews [wfrec_eclose_eq2,
   143 			     arg_in_eclose_sing, 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 (*Congruence*)
   177 val prems = goalw Epsilon.thy [transrec_def,Memrel_def]
   178     "[| a=a';  !!x u. H(x,u)=H'(x,u) |]  ==> transrec(a,H)=transrec(a',H')";
   179 val transrec_ss = 
   180     ZF_ss addcongs ([wfrec_cong] @ mk_congs Epsilon.thy ["eclose"])
   181 	  addrews (prems RL [sym]);
   182 by (SIMP_TAC transrec_ss 1);
   183 val transrec_cong = result();
   184 
   185 (*** Rank ***)
   186 
   187 val ord_ss = ZF_ss addcongs (mk_congs Ord.thy ["Ord"]);
   188 
   189 (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
   190 goal Epsilon.thy "rank(a) = (UN y:a. succ(rank(y)))";
   191 by (rtac (rank_def RS def_transrec RS ssubst) 1);
   192 by (SIMP_TAC ZF_ss 1);
   193 val rank = result();
   194 
   195 goal Epsilon.thy "Ord(rank(a))";
   196 by (eps_ind_tac "a" 1);
   197 by (rtac (rank RS ssubst) 1);
   198 by (rtac (Ord_succ RS Ord_UN) 1);
   199 by (etac bspec 1);
   200 by (assume_tac 1);
   201 val Ord_rank = result();
   202 
   203 val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i";
   204 by (rtac (major RS trans_induct) 1);
   205 by (rtac (rank RS ssubst) 1);
   206 by (ASM_SIMP_TAC (ord_ss addrews [Ord_equality]) 1);
   207 val rank_of_Ord = result();
   208 
   209 val [prem] = goal Epsilon.thy "a:b ==> rank(a) : rank(b)";
   210 by (res_inst_tac [("a1","b")] (rank RS ssubst) 1);
   211 by (rtac (prem RS UN_I) 1);
   212 by (rtac succI1 1);
   213 val rank_lt = result();
   214 
   215 val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) : rank(b)";
   216 by (rtac (major RS eclose_induct_down) 1);
   217 by (etac rank_lt 1);
   218 by (etac (rank_lt RS Ord_trans) 1);
   219 by (assume_tac 1);
   220 by (rtac Ord_rank 1);
   221 val eclose_rank_lt = result();
   222 
   223 goal Epsilon.thy "!!a b. a<=b ==> rank(a) <= rank(b)";
   224 by (rtac (rank RS ssubst) 1);
   225 by (rtac (rank RS ssubst) 1);
   226 by (etac UN_mono 1);
   227 by (rtac subset_refl 1);
   228 val rank_mono = result();
   229 
   230 goal Epsilon.thy "rank(Pow(a)) = succ(rank(a))";
   231 by (rtac (rank RS trans) 1);
   232 by (rtac equalityI 1);
   233 by (fast_tac ZF_cs 2);
   234 by (rtac UN_least 1);
   235 by (etac (PowD RS rank_mono RS Ord_succ_mono) 1);
   236 by (rtac Ord_rank 1);
   237 by (rtac Ord_rank 1);
   238 val rank_Pow = result();
   239 
   240 goal Epsilon.thy "rank(0) = 0";
   241 by (rtac (rank RS trans) 1);
   242 by (fast_tac (ZF_cs addSIs [equalityI]) 1);
   243 val rank_0 = result();
   244 
   245 goal Epsilon.thy "rank(succ(x)) = succ(rank(x))";
   246 by (rtac (rank RS trans) 1);
   247 br ([UN_least, succI1 RS UN_upper] MRS equalityI) 1;
   248 be succE 1;
   249 by (fast_tac ZF_cs 1);
   250 by (REPEAT (ares_tac [Ord_succ_mono,Ord_rank,OrdmemD,rank_lt] 1));
   251 val rank_succ = result();
   252 
   253 goal Epsilon.thy "rank(Union(A)) = (UN x:A. rank(x))";
   254 by (rtac equalityI 1);
   255 by (rtac (rank_mono RS UN_least) 2);
   256 by (etac Union_upper 2);
   257 by (rtac (rank RS ssubst) 1);
   258 by (rtac UN_least 1);
   259 by (etac UnionE 1);
   260 by (rtac subset_trans 1);
   261 by (etac (RepFunI RS Union_upper) 2);
   262 by (etac (rank_lt RS Ord_succ_subsetI) 1);
   263 by (rtac Ord_rank 1);
   264 val rank_Union = result();
   265 
   266 goal Epsilon.thy "rank(eclose(a)) = rank(a)";
   267 by (rtac equalityI 1);
   268 by (rtac (arg_subset_eclose RS rank_mono) 2);
   269 by (res_inst_tac [("a1","eclose(a)")] (rank RS ssubst) 1);
   270 by (rtac UN_least 1);
   271 by (etac ([eclose_rank_lt, Ord_rank] MRS Ord_succ_subsetI) 1);
   272 val rank_eclose = result();
   273 
   274 (*  [| i: j; j: rank(a) |] ==> i: rank(a)  *)
   275 val rank_trans = Ord_rank RSN (3, Ord_trans);
   276 
   277 goalw Epsilon.thy [Pair_def] "rank(a) : rank(<a,b>)";
   278 by (rtac (consI1 RS rank_lt RS Ord_trans) 1);
   279 by (rtac (consI1 RS consI2 RS rank_lt) 1);
   280 by (rtac Ord_rank 1);
   281 val rank_pair1 = result();
   282 
   283 goalw Epsilon.thy [Pair_def] "rank(b) : rank(<a,b>)";
   284 by (rtac (consI1 RS consI2 RS rank_lt RS Ord_trans) 1);
   285 by (rtac (consI1 RS consI2 RS rank_lt) 1);
   286 by (rtac Ord_rank 1);
   287 val rank_pair2 = result();
   288 
   289 goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inl_def] "rank(a) : rank(Inl(a))";
   290 by (rtac rank_pair2 1);
   291 val rank_Inl = result();
   292 
   293 goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inr_def] "rank(a) : rank(Inr(a))";
   294 by (rtac rank_pair2 1);
   295 val rank_Inr = result();
   296 
   297 val [major] = goal Epsilon.thy "i: rank(a) ==> (EX x:a. i<=rank(x))";
   298 by (resolve_tac ([major] RL [rank RS subst] RL [UN_E]) 1);
   299 by (rtac bexI 1);
   300 by (etac member_succD 1);
   301 by (rtac Ord_rank 1);
   302 by (assume_tac 1);
   303 val rank_implies_mem = result();
   304 
   305 
   306 (*** Corollaries of leastness ***)
   307 
   308 goal Epsilon.thy "!!A B. A:B ==> eclose(A)<=eclose(B)";
   309 by (rtac (Transset_eclose RS eclose_least) 1);
   310 by (etac (arg_into_eclose RS eclose_subset) 1);
   311 val mem_eclose_subset = result();
   312 
   313 goal Epsilon.thy "!!A B. A<=B ==> eclose(A) <= eclose(B)";
   314 by (rtac (Transset_eclose RS eclose_least) 1);
   315 by (etac subset_trans 1);
   316 by (rtac arg_subset_eclose 1);
   317 val eclose_mono = result();
   318 
   319 (** Idempotence of eclose **)
   320 
   321 goal Epsilon.thy "eclose(eclose(A)) = eclose(A)";
   322 by (rtac equalityI 1);
   323 by (rtac ([Transset_eclose, subset_refl] MRS eclose_least) 1);
   324 by (rtac arg_subset_eclose 1);
   325 val eclose_idem = result();