src/ZF/Epsilon.ML
changeset 0 a5a9c433f639
child 6 8ce8c4d13d4d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/Epsilon.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,325 @@
     1.4 +(*  Title: 	ZF/epsilon.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +For epsilon.thy.  Epsilon induction and recursion
    1.10 +*)
    1.11 +
    1.12 +open Epsilon;
    1.13 +
    1.14 +(*** Basic closure properties ***)
    1.15 +
    1.16 +goalw Epsilon.thy [eclose_def] "A <= eclose(A)";
    1.17 +by (rtac (nat_rec_0 RS equalityD2 RS subset_trans) 1);
    1.18 +br (nat_0I RS UN_upper) 1;
    1.19 +val arg_subset_eclose = result();
    1.20 +
    1.21 +val arg_into_eclose = arg_subset_eclose RS subsetD;
    1.22 +
    1.23 +goalw Epsilon.thy [eclose_def,Transset_def] "Transset(eclose(A))";
    1.24 +by (rtac (subsetI RS ballI) 1);
    1.25 +by (etac UN_E 1);
    1.26 +by (rtac (nat_succI RS UN_I) 1);
    1.27 +by (assume_tac 1);
    1.28 +by (etac (nat_rec_succ RS ssubst) 1);
    1.29 +by (etac UnionI 1);
    1.30 +by (assume_tac 1);
    1.31 +val Transset_eclose = result();
    1.32 +
    1.33 +(* x : eclose(A) ==> x <= eclose(A) *)
    1.34 +val eclose_subset = 
    1.35 +    standard (rewrite_rule [Transset_def] Transset_eclose RS bspec);
    1.36 +
    1.37 +(* [| A : eclose(B); c : A |] ==> c : eclose(B) *)
    1.38 +val ecloseD = standard (eclose_subset RS subsetD);
    1.39 +
    1.40 +val arg_in_eclose_sing = arg_subset_eclose RS singleton_subsetD;
    1.41 +val arg_into_eclose_sing = arg_in_eclose_sing RS ecloseD;
    1.42 +
    1.43 +(* This is epsilon-induction for eclose(A); see also eclose_induct_down...
    1.44 +   [| a: eclose(A);  !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) 
    1.45 +   |] ==> P(a) 
    1.46 +*)
    1.47 +val eclose_induct = standard (Transset_eclose RSN (2, Transset_induct));
    1.48 +
    1.49 +(*Epsilon induction*)
    1.50 +val prems = goal Epsilon.thy
    1.51 +    "[| !!x. ALL y:x. P(y) ==> P(x) |]  ==>  P(a)";
    1.52 +by (rtac (arg_in_eclose_sing RS eclose_induct) 1);
    1.53 +by (eresolve_tac prems 1);
    1.54 +val eps_induct = result();
    1.55 +
    1.56 +(*Perform epsilon-induction on i. *)
    1.57 +fun eps_ind_tac a = 
    1.58 +    EVERY' [res_inst_tac [("a",a)] eps_induct,
    1.59 +	    rename_last_tac a ["1"]];
    1.60 +
    1.61 +
    1.62 +(*** Leastness of eclose ***)
    1.63 +
    1.64 +(** eclose(A) is the least transitive set including A as a subset. **)
    1.65 +
    1.66 +goalw Epsilon.thy [Transset_def]
    1.67 +    "!!X A n. [| Transset(X);  A<=X;  n: nat |] ==> \
    1.68 +\             nat_rec(n, A, %m r. Union(r)) <= X";
    1.69 +by (etac nat_induct 1);
    1.70 +by (ASM_SIMP_TAC (ZF_ss addrews [nat_rec_0]) 1);
    1.71 +by (ASM_SIMP_TAC (ZF_ss addrews [nat_rec_succ]) 1);
    1.72 +by (fast_tac ZF_cs 1);
    1.73 +val eclose_least_lemma = result();
    1.74 +
    1.75 +goalw Epsilon.thy [eclose_def]
    1.76 +     "!!X A. [| Transset(X);  A<=X |] ==> eclose(A) <= X";
    1.77 +br (eclose_least_lemma RS UN_least) 1;
    1.78 +by (REPEAT (assume_tac 1));
    1.79 +val eclose_least = result();
    1.80 +
    1.81 +(*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
    1.82 +val [major,base,step] = goal Epsilon.thy
    1.83 +    "[| a: eclose(b);						\
    1.84 +\       !!y.   [| y: b |] ==> P(y);				\
    1.85 +\       !!y z. [| y: eclose(b);  P(y);  z: y |] ==> P(z)	\
    1.86 +\    |] ==> P(a)";
    1.87 +by (rtac (major RSN (3, eclose_least RS subsetD RS CollectD2)) 1);
    1.88 +by (rtac (CollectI RS subsetI) 2);
    1.89 +by (etac (arg_subset_eclose RS subsetD) 2);
    1.90 +by (etac base 2);
    1.91 +by (rewtac Transset_def);
    1.92 +by (fast_tac (ZF_cs addEs [step,ecloseD]) 1);
    1.93 +val eclose_induct_down = result();
    1.94 +
    1.95 +goal Epsilon.thy "!!X. Transset(X) ==> eclose(X) = X";
    1.96 +be ([eclose_least, arg_subset_eclose] MRS equalityI) 1;
    1.97 +br subset_refl 1;
    1.98 +val Transset_eclose_eq_arg = result();
    1.99 +
   1.100 +
   1.101 +(*** Epsilon recursion ***)
   1.102 +
   1.103 +(*Unused...*)
   1.104 +goal Epsilon.thy "!!A B C. [| A: eclose(B);  B: eclose(C) |] ==> A: eclose(C)";
   1.105 +by (rtac ([Transset_eclose, eclose_subset] MRS eclose_least RS subsetD) 1);
   1.106 +by (REPEAT (assume_tac 1));
   1.107 +val mem_eclose_trans = result();
   1.108 +
   1.109 +(*Variant of the previous lemma in a useable form for the sequel*)
   1.110 +goal Epsilon.thy
   1.111 +    "!!A B C. [| A: eclose({B});  B: eclose({C}) |] ==> A: eclose({C})";
   1.112 +by (rtac ([Transset_eclose, singleton_subsetI] MRS eclose_least RS subsetD) 1);
   1.113 +by (REPEAT (assume_tac 1));
   1.114 +val mem_eclose_sing_trans = result();
   1.115 +
   1.116 +goalw Epsilon.thy [Transset_def]
   1.117 +    "!!i j. [| Transset(i);  j:i |] ==> Memrel(i)-``{j} = j";
   1.118 +by (fast_tac (eq_cs addSIs [MemrelI] addSEs [MemrelE]) 1);
   1.119 +val under_Memrel = result();
   1.120 +
   1.121 +(* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
   1.122 +val under_Memrel_eclose = Transset_eclose RS under_Memrel;
   1.123 +
   1.124 +val wfrec_ssubst = standard (wf_Memrel RS wfrec RS ssubst);
   1.125 +
   1.126 +val [kmemj,jmemi] = goal Epsilon.thy
   1.127 +    "[| k:eclose({j});  j:eclose({i}) |] ==> \
   1.128 +\    wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)";
   1.129 +by (rtac (kmemj RS eclose_induct) 1);
   1.130 +by (rtac wfrec_ssubst 1);
   1.131 +by (rtac wfrec_ssubst 1);
   1.132 +by (ASM_SIMP_TAC (wf_ss addrews [under_Memrel_eclose,
   1.133 +				 jmemi RSN (2,mem_eclose_sing_trans)]) 1);
   1.134 +val wfrec_eclose_eq = result();
   1.135 +
   1.136 +val [prem] = goal Epsilon.thy
   1.137 +    "k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)";
   1.138 +by (rtac (arg_in_eclose_sing RS wfrec_eclose_eq) 1);
   1.139 +by (rtac (prem RS arg_into_eclose_sing) 1);
   1.140 +val wfrec_eclose_eq2 = result();
   1.141 +
   1.142 +goalw Epsilon.thy [transrec_def]
   1.143 +    "transrec(a,H) = H(a, lam x:a. transrec(x,H))";
   1.144 +by (rtac wfrec_ssubst 1);
   1.145 +by (SIMP_TAC (wf_ss addrews [wfrec_eclose_eq2,
   1.146 +			     arg_in_eclose_sing, under_Memrel_eclose]) 1);
   1.147 +val transrec = result();
   1.148 +
   1.149 +(*Avoids explosions in proofs; resolve it with a meta-level definition.*)
   1.150 +val rew::prems = goal Epsilon.thy
   1.151 +    "[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, lam x:a. f(x))";
   1.152 +by (rewtac rew);
   1.153 +by (REPEAT (resolve_tac (prems@[transrec]) 1));
   1.154 +val def_transrec = result();
   1.155 +
   1.156 +val prems = goal Epsilon.thy
   1.157 +    "[| !!x u. [| x:eclose({a});  u: Pi(x,B) |] ==> H(x,u) : B(x)   \
   1.158 +\    |]  ==> transrec(a,H) : B(a)";
   1.159 +by (res_inst_tac [("i", "a")] (arg_in_eclose_sing RS eclose_induct) 1);
   1.160 +by (rtac (transrec RS ssubst) 1);
   1.161 +by (REPEAT (ares_tac (prems @ [lam_type]) 1 ORELSE etac bspec 1));
   1.162 +val transrec_type = result();
   1.163 +
   1.164 +goal Epsilon.thy "!!i. Ord(i) ==> eclose({i}) <= succ(i)";
   1.165 +by (etac (Ord_is_Transset RS Transset_succ RS eclose_least) 1);
   1.166 +by (rtac (succI1 RS singleton_subsetI) 1);
   1.167 +val eclose_sing_Ord = result();
   1.168 +
   1.169 +val prems = goal Epsilon.thy
   1.170 +    "[| j: i;  Ord(i);  \
   1.171 +\       !!x u. [| x: i;  u: Pi(x,B) |] ==> H(x,u) : B(x)   \
   1.172 +\    |]  ==> transrec(j,H) : B(j)";
   1.173 +by (rtac transrec_type 1);
   1.174 +by (resolve_tac prems 1);
   1.175 +by (rtac (Ord_in_Ord RS eclose_sing_Ord RS subsetD RS succE) 1);
   1.176 +by (DEPTH_SOLVE (ares_tac prems 1 ORELSE eresolve_tac [ssubst,Ord_trans] 1));
   1.177 +val Ord_transrec_type = result();
   1.178 +
   1.179 +(*Congruence*)
   1.180 +val prems = goalw Epsilon.thy [transrec_def,Memrel_def]
   1.181 +    "[| a=a';  !!x u. H(x,u)=H'(x,u) |]  ==> transrec(a,H)=transrec(a',H')";
   1.182 +val transrec_ss = 
   1.183 +    ZF_ss addcongs ([wfrec_cong] @ mk_congs Epsilon.thy ["eclose"])
   1.184 +	  addrews (prems RL [sym]);
   1.185 +by (SIMP_TAC transrec_ss 1);
   1.186 +val transrec_cong = result();
   1.187 +
   1.188 +(*** Rank ***)
   1.189 +
   1.190 +val ord_ss = ZF_ss addcongs (mk_congs Ord.thy ["Ord"]);
   1.191 +
   1.192 +(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
   1.193 +goal Epsilon.thy "rank(a) = (UN y:a. succ(rank(y)))";
   1.194 +by (rtac (rank_def RS def_transrec RS ssubst) 1);
   1.195 +by (SIMP_TAC ZF_ss 1);
   1.196 +val rank = result();
   1.197 +
   1.198 +goal Epsilon.thy "Ord(rank(a))";
   1.199 +by (eps_ind_tac "a" 1);
   1.200 +by (rtac (rank RS ssubst) 1);
   1.201 +by (rtac (Ord_succ RS Ord_UN) 1);
   1.202 +by (etac bspec 1);
   1.203 +by (assume_tac 1);
   1.204 +val Ord_rank = result();
   1.205 +
   1.206 +val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i";
   1.207 +by (rtac (major RS trans_induct) 1);
   1.208 +by (rtac (rank RS ssubst) 1);
   1.209 +by (ASM_SIMP_TAC (ord_ss addrews [Ord_equality]) 1);
   1.210 +val rank_of_Ord = result();
   1.211 +
   1.212 +val [prem] = goal Epsilon.thy "a:b ==> rank(a) : rank(b)";
   1.213 +by (res_inst_tac [("a1","b")] (rank RS ssubst) 1);
   1.214 +by (rtac (prem RS UN_I) 1);
   1.215 +by (rtac succI1 1);
   1.216 +val rank_lt = result();
   1.217 +
   1.218 +val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) : rank(b)";
   1.219 +by (rtac (major RS eclose_induct_down) 1);
   1.220 +by (etac rank_lt 1);
   1.221 +by (etac (rank_lt RS Ord_trans) 1);
   1.222 +by (assume_tac 1);
   1.223 +by (rtac Ord_rank 1);
   1.224 +val eclose_rank_lt = result();
   1.225 +
   1.226 +goal Epsilon.thy "!!a b. a<=b ==> rank(a) <= rank(b)";
   1.227 +by (rtac (rank RS ssubst) 1);
   1.228 +by (rtac (rank RS ssubst) 1);
   1.229 +by (etac UN_mono 1);
   1.230 +by (rtac subset_refl 1);
   1.231 +val rank_mono = result();
   1.232 +
   1.233 +goal Epsilon.thy "rank(Pow(a)) = succ(rank(a))";
   1.234 +by (rtac (rank RS trans) 1);
   1.235 +by (rtac equalityI 1);
   1.236 +by (fast_tac ZF_cs 2);
   1.237 +by (rtac UN_least 1);
   1.238 +by (etac (PowD RS rank_mono RS Ord_succ_mono) 1);
   1.239 +by (rtac Ord_rank 1);
   1.240 +by (rtac Ord_rank 1);
   1.241 +val rank_Pow = result();
   1.242 +
   1.243 +goal Epsilon.thy "rank(0) = 0";
   1.244 +by (rtac (rank RS trans) 1);
   1.245 +by (fast_tac (ZF_cs addSIs [equalityI]) 1);
   1.246 +val rank_0 = result();
   1.247 +
   1.248 +goal Epsilon.thy "rank(succ(x)) = succ(rank(x))";
   1.249 +by (rtac (rank RS trans) 1);
   1.250 +br ([UN_least, succI1 RS UN_upper] MRS equalityI) 1;
   1.251 +be succE 1;
   1.252 +by (fast_tac ZF_cs 1);
   1.253 +by (REPEAT (ares_tac [Ord_succ_mono,Ord_rank,OrdmemD,rank_lt] 1));
   1.254 +val rank_succ = result();
   1.255 +
   1.256 +goal Epsilon.thy "rank(Union(A)) = (UN x:A. rank(x))";
   1.257 +by (rtac equalityI 1);
   1.258 +by (rtac (rank_mono RS UN_least) 2);
   1.259 +by (etac Union_upper 2);
   1.260 +by (rtac (rank RS ssubst) 1);
   1.261 +by (rtac UN_least 1);
   1.262 +by (etac UnionE 1);
   1.263 +by (rtac subset_trans 1);
   1.264 +by (etac (RepFunI RS Union_upper) 2);
   1.265 +by (etac (rank_lt RS Ord_succ_subsetI) 1);
   1.266 +by (rtac Ord_rank 1);
   1.267 +val rank_Union = result();
   1.268 +
   1.269 +goal Epsilon.thy "rank(eclose(a)) = rank(a)";
   1.270 +by (rtac equalityI 1);
   1.271 +by (rtac (arg_subset_eclose RS rank_mono) 2);
   1.272 +by (res_inst_tac [("a1","eclose(a)")] (rank RS ssubst) 1);
   1.273 +by (rtac UN_least 1);
   1.274 +by (etac ([eclose_rank_lt, Ord_rank] MRS Ord_succ_subsetI) 1);
   1.275 +val rank_eclose = result();
   1.276 +
   1.277 +(*  [| i: j; j: rank(a) |] ==> i: rank(a)  *)
   1.278 +val rank_trans = Ord_rank RSN (3, Ord_trans);
   1.279 +
   1.280 +goalw Epsilon.thy [Pair_def] "rank(a) : rank(<a,b>)";
   1.281 +by (rtac (consI1 RS rank_lt RS Ord_trans) 1);
   1.282 +by (rtac (consI1 RS consI2 RS rank_lt) 1);
   1.283 +by (rtac Ord_rank 1);
   1.284 +val rank_pair1 = result();
   1.285 +
   1.286 +goalw Epsilon.thy [Pair_def] "rank(b) : rank(<a,b>)";
   1.287 +by (rtac (consI1 RS consI2 RS rank_lt RS Ord_trans) 1);
   1.288 +by (rtac (consI1 RS consI2 RS rank_lt) 1);
   1.289 +by (rtac Ord_rank 1);
   1.290 +val rank_pair2 = result();
   1.291 +
   1.292 +goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inl_def] "rank(a) : rank(Inl(a))";
   1.293 +by (rtac rank_pair2 1);
   1.294 +val rank_Inl = result();
   1.295 +
   1.296 +goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inr_def] "rank(a) : rank(Inr(a))";
   1.297 +by (rtac rank_pair2 1);
   1.298 +val rank_Inr = result();
   1.299 +
   1.300 +val [major] = goal Epsilon.thy "i: rank(a) ==> (EX x:a. i<=rank(x))";
   1.301 +by (resolve_tac ([major] RL [rank RS subst] RL [UN_E]) 1);
   1.302 +by (rtac bexI 1);
   1.303 +by (etac member_succD 1);
   1.304 +by (rtac Ord_rank 1);
   1.305 +by (assume_tac 1);
   1.306 +val rank_implies_mem = result();
   1.307 +
   1.308 +
   1.309 +(*** Corollaries of leastness ***)
   1.310 +
   1.311 +goal Epsilon.thy "!!A B. A:B ==> eclose(A)<=eclose(B)";
   1.312 +by (rtac (Transset_eclose RS eclose_least) 1);
   1.313 +by (etac (arg_into_eclose RS eclose_subset) 1);
   1.314 +val mem_eclose_subset = result();
   1.315 +
   1.316 +goal Epsilon.thy "!!A B. A<=B ==> eclose(A) <= eclose(B)";
   1.317 +by (rtac (Transset_eclose RS eclose_least) 1);
   1.318 +by (etac subset_trans 1);
   1.319 +by (rtac arg_subset_eclose 1);
   1.320 +val eclose_mono = result();
   1.321 +
   1.322 +(** Idempotence of eclose **)
   1.323 +
   1.324 +goal Epsilon.thy "eclose(eclose(A)) = eclose(A)";
   1.325 +by (rtac equalityI 1);
   1.326 +by (rtac ([Transset_eclose, subset_refl] MRS eclose_least) 1);
   1.327 +by (rtac arg_subset_eclose 1);
   1.328 +val eclose_idem = result();