488

1 
(* Title: ZF/InfDatatype.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1994 University of Cambridge


5 


6 
InfiniteBranching Datatype Definitions


7 
*)


8 


9 
val fun_Limit_VfromE =


10 
[apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE


11 
> standard;


12 


13 
goal InfDatatype.thy


14 
"!!K. [ f: K > Vfrom(A,csucc(K)); InfCard(K) \


15 
\ ] ==> EX j. f: K > Vfrom(A,j) & j < csucc(K)";


16 
by (res_inst_tac [("x", "UN k:K. LEAST i. f`k : Vfrom(A,i)")] exI 1);


17 
by (resolve_tac [conjI] 1);


18 
by (resolve_tac [ballI RSN (2,cardinal_UN_Ord_lt_csucc)] 2);


19 
by (eresolve_tac [fun_Limit_VfromE] 3 THEN REPEAT_SOME assume_tac);


20 
by (fast_tac (ZF_cs addEs [Least_le RS lt_trans1, ltE]) 2);


21 
by (resolve_tac [Pi_type] 1);


22 
by (rename_tac "k" 2);


23 
by (eresolve_tac [fun_Limit_VfromE] 2 THEN REPEAT_SOME assume_tac);


24 
by (subgoal_tac "f`k : Vfrom(A, LEAST i. f`k : Vfrom(A,i))" 1);


25 
by (fast_tac (ZF_cs addEs [LeastI, ltE]) 2);


26 
by (eresolve_tac [[subset_refl, UN_upper] MRS Vfrom_mono RS subsetD] 1);


27 
by (assume_tac 1);


28 
val fun_Vfrom_csucc_lemma = result();


29 


30 
goal InfDatatype.thy


31 
"!!K. InfCard(K) ==> K > Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";


32 
by (safe_tac (ZF_cs addSDs [fun_Vfrom_csucc_lemma]));


33 
by (resolve_tac [Vfrom RS ssubst] 1);


34 
by (eresolve_tac [PiE] 1);


35 
(*This level includes the function, and is below csucc(K)*)


36 
by (res_inst_tac [("a1", "succ(succ(K Un j))")] (UN_I RS UnI2) 1);


37 
by (eresolve_tac [subset_trans RS PowI] 2);


38 
by (safe_tac (ZF_cs addSIs [Pair_in_Vfrom]));


39 
by (fast_tac (ZF_cs addIs [i_subset_Vfrom RS subsetD]) 2);


40 
by (eresolve_tac [[subset_refl, Un_upper2] MRS Vfrom_mono RS subsetD] 2);


41 
by (REPEAT (ares_tac [ltD, InfCard_csucc, InfCard_is_Limit,


42 
Limit_has_succ, Un_least_lt] 1));


43 
by (eresolve_tac [InfCard_is_Card RS Card_is_Ord RS lt_csucc] 1);


44 
by (assume_tac 1);


45 
val fun_Vfrom_csucc = result();


46 


47 
goal InfDatatype.thy


48 
"!!K. [ f: K > Vfrom(A, csucc(K)); InfCard(K) \


49 
\ ] ==> f: Vfrom(A,csucc(K))";


50 
by (REPEAT (ares_tac [fun_Vfrom_csucc RS subsetD] 1));


51 
val fun_in_Vfrom_csucc = result();


52 


53 
val fun_subset_Vfrom_csucc =


54 
[Pi_mono, fun_Vfrom_csucc] MRS subset_trans > standard;


55 


56 
goal InfDatatype.thy


57 
"!!f. [ f: K > B; B <= Vfrom(A,csucc(K)); InfCard(K) \


58 
\ ] ==> f: Vfrom(A,csucc(K))";


59 
by (REPEAT (ares_tac [fun_subset_Vfrom_csucc RS subsetD] 1));


60 
val fun_into_Vfrom_csucc = result();


61 


62 
val Limit_csucc = InfCard_csucc RS InfCard_is_Limit > standard;


63 


64 
val Pair_in_Vfrom_csucc = Limit_csucc RSN (3, Pair_in_Vfrom_Limit) > standard;


65 
val Inl_in_Vfrom_csucc = Limit_csucc RSN (2, Inl_in_Vfrom_Limit) > standard;


66 
val Inr_in_Vfrom_csucc = Limit_csucc RSN (2, Inr_in_Vfrom_Limit) > standard;


67 
val zero_in_Vfrom_csucc = Limit_csucc RS zero_in_Vfrom_Limit > standard;


68 
val nat_into_Vfrom_csucc = Limit_csucc RSN (2, nat_into_Vfrom_Limit)


69 
> standard;


70 


71 
(*For most Kbranching datatypes with domain Vfrom(A, csucc(K)) *)


72 
val inf_datatype_intrs =


73 
[fun_in_Vfrom_csucc, InfCard_nat, Pair_in_Vfrom_csucc,


74 
Inl_in_Vfrom_csucc, Inr_in_Vfrom_csucc,


75 
zero_in_Vfrom_csucc, A_into_Vfrom, nat_into_Vfrom_csucc] @ datatype_intrs;


76 
