author  lcp 
Thu, 03 Nov 1994 12:43:42 +0100  
changeset 692  0ca24b09f4a6 
parent 534  cd8bec47e175 
child 760  f0200e91b272 
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 

534  6 
Datatype Definitions involving function space and/or infinitebranching 
488  7 
*) 
8 

534  9 
(*** FINITE BRANCHING ***) 
10 

11 
(** Closure under finite powerset **) 

516  12 

13 
val Fin_Univ_thy = merge_theories (Univ.thy,Finite.thy); 

14 

15 
goal Fin_Univ_thy 

16 
"!!i. [ b: Fin(Vfrom(A,i)); Limit(i) ] ==> EX j. b <= Vfrom(A,j) & j<i"; 

17 
by (eresolve_tac [Fin_induct] 1); 

18 
by (fast_tac (ZF_cs addSDs [Limit_has_0]) 1); 

19 
by (safe_tac ZF_cs); 

20 
by (eresolve_tac [Limit_VfromE] 1); 

21 
by (assume_tac 1); 

22 
by (res_inst_tac [("x", "xa Un j")] exI 1); 

23 
by (best_tac (ZF_cs addIs [subset_refl RS Vfrom_mono RS subsetD, 

24 
Un_least_lt]) 1); 

25 
val Fin_Vfrom_lemma = result(); 

26 

27 
goal Fin_Univ_thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)"; 

28 
by (rtac subsetI 1); 

29 
by (dresolve_tac [Fin_Vfrom_lemma] 1); 

30 
by (safe_tac ZF_cs); 

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

32 
by (fast_tac (ZF_cs addSDs [ltD]) 1); 

33 
val Fin_VLimit = result(); 

34 

35 
val Fin_subset_VLimit = 

36 
[Fin_mono, Fin_VLimit] MRS subset_trans > standard; 

37 

534  38 
goalw Fin_Univ_thy [univ_def] "Fin(univ(A)) <= univ(A)"; 
39 
by (rtac (Limit_nat RS Fin_VLimit) 1); 

40 
val Fin_univ = result(); 

41 

42 
(** Closure under finite powers (functions from a fixed natural number) **) 

43 

516  44 
goal Fin_Univ_thy 
45 
"!!i. [ n: nat; Limit(i) ] ==> n > Vfrom(A,i) <= Vfrom(A,i)"; 

46 
by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1); 

47 
by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, 

48 
nat_subset_VLimit, subset_refl] 1)); 

49 
val nat_fun_VLimit = result(); 

50 

51 
val nat_fun_subset_VLimit = 

52 
[Pi_mono, nat_fun_VLimit] MRS subset_trans > standard; 

53 

54 
goalw Fin_Univ_thy [univ_def] "!!i. n: nat ==> n > univ(A) <= univ(A)"; 

55 
by (etac (Limit_nat RSN (2,nat_fun_VLimit)) 1); 

56 
val nat_fun_univ = result(); 

57 

58 

534  59 
(** Closure under finite function space **) 
60 

61 
(*General but seldomused version; normally the domain is fixed*) 

62 
goal Fin_Univ_thy 

63 
"!!i. Limit(i) ==> Vfrom(A,i) > Vfrom(A,i) <= Vfrom(A,i)"; 

64 
by (resolve_tac [FiniteFun.dom_subset RS subset_trans] 1); 

65 
by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, subset_refl] 1)); 

66 
val FiniteFun_VLimit1 = result(); 

67 

68 
goalw Fin_Univ_thy [univ_def] "univ(A) > univ(A) <= univ(A)"; 

69 
by (rtac (Limit_nat RS FiniteFun_VLimit1) 1); 

70 
val FiniteFun_univ1 = result(); 

71 

72 
(*Version for a fixed domain*) 

73 
goal Fin_Univ_thy 

74 
"!!i. [ W <= Vfrom(A,i); Limit(i) ] ==> W > Vfrom(A,i) <= Vfrom(A,i)"; 

75 
by (eresolve_tac [subset_refl RSN (2, FiniteFun_mono) RS subset_trans] 1); 

76 
by (eresolve_tac [FiniteFun_VLimit1] 1); 

77 
val FiniteFun_VLimit = result(); 

78 

79 
goalw Fin_Univ_thy [univ_def] 

80 
"!!W. W <= univ(A) ==> W > univ(A) <= univ(A)"; 

81 
by (etac (Limit_nat RSN (2, FiniteFun_VLimit)) 1); 

82 
val FiniteFun_univ = result(); 

83 

84 
goal Fin_Univ_thy 

85 
"!!W. [ f: W > univ(A); W <= univ(A) ] ==> f : univ(A)"; 

86 
by (eresolve_tac [FiniteFun_univ RS subsetD] 1); 

87 
by (assume_tac 1); 

88 
val FiniteFun_in_univ = result(); 

89 

90 
(*Remove <= from the rule above*) 

91 
val FiniteFun_in_univ' = subsetI RSN (2, FiniteFun_in_univ); 

92 

93 

94 
(*** INFINITE BRANCHING ***) 

516  95 

488  96 
val fun_Limit_VfromE = 
97 
[apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE 

98 
> standard; 

99 

100 
goal InfDatatype.thy 

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

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

516  104 
by (resolve_tac [conjI] 1); 
517  105 
by (resolve_tac [le_UN_Ord_lt_csucc] 2); 
106 
by (rtac ballI 4 THEN 

107 
eresolve_tac [fun_Limit_VfromE] 4 THEN REPEAT_SOME assume_tac); 

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

517  110 
by (rename_tac "w" 2); 
516  111 
by (eresolve_tac [fun_Limit_VfromE] 2 THEN REPEAT_SOME assume_tac); 
517  112 
by (subgoal_tac "f`w : Vfrom(A, LEAST i. f`w : Vfrom(A,i))" 1); 
516  113 
by (fast_tac (ZF_cs addEs [LeastI, ltE]) 2); 
114 
by (eresolve_tac [[subset_refl, UN_upper] MRS Vfrom_mono RS subsetD] 1); 

115 
by (assume_tac 1); 

116 
val fun_Vcsucc_lemma = result(); 

117 

118 
goal InfDatatype.thy 

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

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

122 
val subset_Vcsucc = result(); 

488  123 

517  124 
(*Version for arbitrary index sets*) 
488  125 
goal InfDatatype.thy 
534  126 
"!!K. [ W le K; InfCard(K); W <= Vfrom(A,csucc(K)) ] ==> \ 
517  127 
\ W > Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"; 
128 
by (safe_tac (ZF_cs addSDs [fun_Vcsucc_lemma, subset_Vcsucc])); 

488  129 
by (resolve_tac [Vfrom RS ssubst] 1); 
692  130 
by (dresolve_tac [fun_is_rel] 1); 
488  131 
(*This level includes the function, and is below csucc(K)*) 
517  132 
by (res_inst_tac [("a1", "succ(succ(j Un ja))")] (UN_I RS UnI2) 1); 
488  133 
by (eresolve_tac [subset_trans RS PowI] 2); 
517  134 
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom, Vfrom_UnI1, Vfrom_UnI2]) 2); 
488  135 
by (REPEAT (ares_tac [ltD, InfCard_csucc, InfCard_is_Limit, 
136 
Limit_has_succ, Un_least_lt] 1)); 

516  137 
val fun_Vcsucc = result(); 
488  138 

139 
goal InfDatatype.thy 

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

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

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

144 
val fun_in_Vcsucc = result(); 

145 

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

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

147 
val fun_in_Vcsucc' = subsetI RSN (4, fun_in_Vcsucc); 
517  148 

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

149 
(** Version where K itself is the index set **) 
517  150 

151 
goal InfDatatype.thy 

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

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

154 
by (REPEAT (ares_tac [fun_Vcsucc, Ord_cardinal_le, 

155 
i_subset_Vfrom, 

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

157 
val Card_fun_Vcsucc = result(); 

158 

159 
goal InfDatatype.thy 

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

517  162 
by (REPEAT (ares_tac [Card_fun_Vcsucc RS subsetD] 1)); 
163 
val Card_fun_in_Vcsucc = result(); 

488  164 

516  165 
val Pair_in_Vcsucc = Limit_csucc RSN (3, Pair_in_VLimit) > standard; 
166 
val Inl_in_Vcsucc = Limit_csucc RSN (2, Inl_in_VLimit) > standard; 

167 
val Inr_in_Vcsucc = Limit_csucc RSN (2, Inr_in_VLimit) > standard; 

168 
val zero_in_Vcsucc = Limit_csucc RS zero_in_VLimit > standard; 

169 
val nat_into_Vcsucc = Limit_csucc RSN (2, nat_into_VLimit) > standard; 

488  170 

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

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

172 

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

173 
val InfCard_nat_Un_cardinal = [InfCard_nat, Card_cardinal] MRS InfCard_Un 
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset

174 
> standard; 
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset

175 

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

176 
val le_nat_Un_cardinal = 
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset

177 
[Ord_nat, Card_cardinal RS Card_is_Ord] MRS Un_upper2_le > standard; 
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset

178 

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

179 
val UN_upper_cardinal = UN_upper RS subset_imp_lepoll RS lepoll_imp_le 
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset

180 
> standard; 
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset

181 

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

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

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

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

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

187 
Card_fun_in_Vcsucc, fun_in_Vcsucc', UN_I] @ datatype_intrs; 