author  lcp 
Fri, 16 Dec 1994 17:44:09 +0100  
changeset 801  316121afb5b5 
parent 768  59c0a821e468 
child 1461  6bcb44e4d6e5 
permissions  rwrr 
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 

801  6 
Infinitebranching datatype definitions 
488  7 
*) 
8 

801  9 
val fun_Limit_VfromE = 
10 
[apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE 

11 
> standard; 

488  12 

13 
goal InfDatatype.thy 

517  14 
"!!K. [ f: W > Vfrom(A,csucc(K)); W le K; InfCard(K) \ 
15 
\ ] ==> EX j. f: W > Vfrom(A,j) & j < csucc(K)"; 

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

516  17 
by (resolve_tac [conjI] 1); 
517  18 
by (resolve_tac [le_UN_Ord_lt_csucc] 2); 
19 
by (rtac ballI 4 THEN 

20 
eresolve_tac [fun_Limit_VfromE] 4 THEN REPEAT_SOME assume_tac); 

516  21 
by (fast_tac (ZF_cs addEs [Least_le RS lt_trans1, ltE]) 2); 
22 
by (resolve_tac [Pi_type] 1); 

517  23 
by (rename_tac "w" 2); 
516  24 
by (eresolve_tac [fun_Limit_VfromE] 2 THEN REPEAT_SOME assume_tac); 
517  25 
by (subgoal_tac "f`w : Vfrom(A, LEAST i. f`w : Vfrom(A,i))" 1); 
516  26 
by (fast_tac (ZF_cs addEs [LeastI, ltE]) 2); 
27 
by (eresolve_tac [[subset_refl, UN_upper] MRS Vfrom_mono RS subsetD] 1); 

28 
by (assume_tac 1); 

760  29 
qed "fun_Vcsucc_lemma"; 
516  30 

31 
goal InfDatatype.thy 

517  32 
"!!K. [ W <= Vfrom(A,csucc(K)); W le K; InfCard(K) \ 
33 
\ ] ==> EX j. W <= Vfrom(A,j) & j < csucc(K)"; 

34 
by (asm_full_simp_tac (ZF_ss addsimps [subset_iff_id, fun_Vcsucc_lemma]) 1); 

760  35 
qed "subset_Vcsucc"; 
488  36 

517  37 
(*Version for arbitrary index sets*) 
488  38 
goal InfDatatype.thy 
534  39 
"!!K. [ W le K; InfCard(K); W <= Vfrom(A,csucc(K)) ] ==> \ 
517  40 
\ W > Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"; 
41 
by (safe_tac (ZF_cs addSDs [fun_Vcsucc_lemma, subset_Vcsucc])); 

488  42 
by (resolve_tac [Vfrom RS ssubst] 1); 
692  43 
by (dresolve_tac [fun_is_rel] 1); 
488  44 
(*This level includes the function, and is below csucc(K)*) 
517  45 
by (res_inst_tac [("a1", "succ(succ(j Un ja))")] (UN_I RS UnI2) 1); 
488  46 
by (eresolve_tac [subset_trans RS PowI] 2); 
517  47 
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom, Vfrom_UnI1, Vfrom_UnI2]) 2); 
488  48 
by (REPEAT (ares_tac [ltD, InfCard_csucc, InfCard_is_Limit, 
49 
Limit_has_succ, Un_least_lt] 1)); 

760  50 
qed "fun_Vcsucc"; 
488  51 

52 
goal InfDatatype.thy 

517  53 
"!!K. [ f: W > Vfrom(A, csucc(K)); W le K; InfCard(K); \ 
54 
\ W <= Vfrom(A,csucc(K)) \ 

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

56 
by (REPEAT (ares_tac [fun_Vcsucc RS subsetD] 1)); 

760  57 
qed "fun_in_Vcsucc"; 
517  58 

524
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset

59 
(*Remove <= from the rule above*) 
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset

60 
val fun_in_Vcsucc' = subsetI RSN (4, fun_in_Vcsucc); 
517  61 

524
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset

62 
(** Version where K itself is the index set **) 
517  63 

64 
goal InfDatatype.thy 

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

66 
by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1); 

67 
by (REPEAT (ares_tac [fun_Vcsucc, Ord_cardinal_le, 

68 
i_subset_Vfrom, 

69 
lt_csucc RS leI RS le_imp_subset RS subset_trans] 1)); 

760  70 
qed "Card_fun_Vcsucc"; 
517  71 

72 
goal InfDatatype.thy 

488  73 
"!!K. [ f: K > Vfrom(A, csucc(K)); InfCard(K) \ 
74 
\ ] ==> f: Vfrom(A,csucc(K))"; 

517  75 
by (REPEAT (ares_tac [Card_fun_Vcsucc RS subsetD] 1)); 
760  76 
qed "Card_fun_in_Vcsucc"; 
488  77 

801  78 
(*Proved explicitly, in theory InfDatatype, to allow the bind_thm calls below*) 
79 
qed_goal "Limit_csucc" InfDatatype.thy 

80 
"!!K. InfCard(K) ==> Limit(csucc(K))" 

81 
(fn _ => [etac (InfCard_csucc RS InfCard_is_Limit) 1]); 

82 

83 
bind_thm ("Pair_in_Vcsucc", Limit_csucc RSN (3, Pair_in_VLimit)); 

84 
bind_thm ("Inl_in_Vcsucc", Limit_csucc RSN (2, Inl_in_VLimit)); 

85 
bind_thm ("Inr_in_Vcsucc", Limit_csucc RSN (2, Inr_in_VLimit)); 

86 
bind_thm ("zero_in_Vcsucc", Limit_csucc RS zero_in_VLimit); 

87 
bind_thm ("nat_into_Vcsucc", Limit_csucc RSN (2, nat_into_VLimit)); 

488  88 

524
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset

89 
(*For handling Cardinals of the form (nat Un X) *) 
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset

90 

801  91 
bind_thm ("InfCard_nat_Un_cardinal", 
92 
[InfCard_nat, Card_cardinal] MRS InfCard_Un); 

524
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset

93 

801  94 
bind_thm ("le_nat_Un_cardinal", 
95 
[Ord_nat, Card_cardinal RS Card_is_Ord] MRS Un_upper2_le); 

524
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset

96 

801  97 
bind_thm ("UN_upper_cardinal", 
98 
UN_upper RS subset_imp_lepoll RS lepoll_imp_Card_le); 

524
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset

99 

488  100 
(*For most Kbranching datatypes with domain Vfrom(A, csucc(K)) *) 
101 
val inf_datatype_intrs = 

524
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset

102 
[InfCard_nat, InfCard_nat_Un_cardinal, 
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset

103 
Pair_in_Vcsucc, Inl_in_Vcsucc, Inr_in_Vcsucc, 
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset

104 
zero_in_Vcsucc, A_into_Vfrom, nat_into_Vcsucc, 
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset

105 
Card_fun_in_Vcsucc, fun_in_Vcsucc', UN_I] @ datatype_intrs; 