0

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 epsiloninduction 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 epsiloninduction 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 metalevel 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();
