author  lcp 
Fri, 23 Dec 1994 16:29:53 +0100  
changeset 828  03d7bfa70289 
parent 803  4c8333ab3eae 
child 853  a4b286dfdd6f 
permissions  rwrr 
435  1 
(* Title: ZF/Univ 
0  2 
ID: $Id$ 
3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

435  4 
Copyright 1994 University of Cambridge 
0  5 

6 
The cumulative hierarchy and a small universe for recursive types 

7 
*) 

8 

9 
open Univ; 

10 

11 
(*NOT SUITABLE FOR REWRITING  RECURSIVE!*) 

12 
goal Univ.thy "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))"; 

13 
by (rtac (Vfrom_def RS def_transrec RS ssubst) 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

14 
by (simp_tac ZF_ss 1); 
760  15 
qed "Vfrom"; 
0  16 

17 
(** Monotonicity **) 

18 

19 
goal Univ.thy "!!A B. A<=B ==> ALL j. i<=j > Vfrom(A,i) <= Vfrom(B,j)"; 

20 
by (eps_ind_tac "i" 1); 

21 
by (rtac (impI RS allI) 1); 

22 
by (rtac (Vfrom RS ssubst) 1); 

23 
by (rtac (Vfrom RS ssubst) 1); 

24 
by (etac Un_mono 1); 

25 
by (rtac UN_mono 1); 

26 
by (assume_tac 1); 

27 
by (rtac Pow_mono 1); 

28 
by (etac (bspec RS spec RS mp) 1); 

29 
by (assume_tac 1); 

30 
by (rtac subset_refl 1); 

760  31 
qed "Vfrom_mono_lemma"; 
0  32 

33 
(* [ A<=B; i<=x ] ==> Vfrom(A,i) <= Vfrom(B,x) *) 

782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset

34 
bind_thm ("Vfrom_mono", (Vfrom_mono_lemma RS spec RS mp)); 
0  35 

36 

37 
(** A fundamental equality: Vfrom does not require ordinals! **) 

38 

39 
goal Univ.thy "Vfrom(A,x) <= Vfrom(A,rank(x))"; 

40 
by (eps_ind_tac "x" 1); 

41 
by (rtac (Vfrom RS ssubst) 1); 

42 
by (rtac (Vfrom RS ssubst) 1); 

27  43 
by (fast_tac (ZF_cs addSIs [rank_lt RS ltD]) 1); 
760  44 
qed "Vfrom_rank_subset1"; 
0  45 

46 
goal Univ.thy "Vfrom(A,rank(x)) <= Vfrom(A,x)"; 

47 
by (eps_ind_tac "x" 1); 

48 
by (rtac (Vfrom RS ssubst) 1); 

49 
by (rtac (Vfrom RS ssubst) 1); 

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

50 
by (rtac (subset_refl RS Un_mono) 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

51 
by (rtac UN_least 1); 
27  52 
(*expand rank(x1) = (UN y:x1. succ(rank(y))) in assumptions*) 
53 
by (etac (rank RS equalityD1 RS subsetD RS UN_E) 1); 

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

54 
by (rtac subset_trans 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

55 
by (etac UN_upper 2); 
27  56 
by (rtac (subset_refl RS Vfrom_mono RS subset_trans RS Pow_mono) 1); 
57 
by (etac (ltI RS le_imp_subset) 1); 

58 
by (rtac (Ord_rank RS Ord_succ) 1); 

0  59 
by (etac bspec 1); 
60 
by (assume_tac 1); 

760  61 
qed "Vfrom_rank_subset2"; 
0  62 

63 
goal Univ.thy "Vfrom(A,rank(x)) = Vfrom(A,x)"; 

64 
by (rtac equalityI 1); 

65 
by (rtac Vfrom_rank_subset2 1); 

66 
by (rtac Vfrom_rank_subset1 1); 

760  67 
qed "Vfrom_rank_eq"; 
0  68 

69 

70 
(*** Basic closure properties ***) 

71 

72 
goal Univ.thy "!!x y. y:x ==> 0 : Vfrom(A,x)"; 

73 
by (rtac (Vfrom RS ssubst) 1); 

74 
by (fast_tac ZF_cs 1); 

760  75 
qed "zero_in_Vfrom"; 
0  76 

77 
goal Univ.thy "i <= Vfrom(A,i)"; 

78 
by (eps_ind_tac "i" 1); 

79 
by (rtac (Vfrom RS ssubst) 1); 

80 
by (fast_tac ZF_cs 1); 

760  81 
qed "i_subset_Vfrom"; 
0  82 

83 
goal Univ.thy "A <= Vfrom(A,i)"; 

84 
by (rtac (Vfrom RS ssubst) 1); 

85 
by (rtac Un_upper1 1); 

760  86 
qed "A_subset_Vfrom"; 
0  87 

803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

88 
bind_thm ("A_into_Vfrom", A_subset_Vfrom RS subsetD); 
488  89 

0  90 
goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))"; 
91 
by (rtac (Vfrom RS ssubst) 1); 

92 
by (fast_tac ZF_cs 1); 

760  93 
qed "subset_mem_Vfrom"; 
0  94 

95 
(** Finite sets and ordered pairs **) 

96 

97 
goal Univ.thy "!!a. a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))"; 

98 
by (rtac subset_mem_Vfrom 1); 

99 
by (safe_tac ZF_cs); 

760  100 
qed "singleton_in_Vfrom"; 
0  101 

102 
goal Univ.thy 

103 
"!!A. [ a: Vfrom(A,i); b: Vfrom(A,i) ] ==> {a,b} : Vfrom(A,succ(i))"; 

104 
by (rtac subset_mem_Vfrom 1); 

105 
by (safe_tac ZF_cs); 

760  106 
qed "doubleton_in_Vfrom"; 
0  107 

108 
goalw Univ.thy [Pair_def] 

109 
"!!A. [ a: Vfrom(A,i); b: Vfrom(A,i) ] ==> \ 

110 
\ <a,b> : Vfrom(A,succ(succ(i)))"; 

111 
by (REPEAT (ares_tac [doubleton_in_Vfrom] 1)); 

760  112 
qed "Pair_in_Vfrom"; 
0  113 

114 
val [prem] = goal Univ.thy 

115 
"a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))"; 

116 
by (REPEAT (resolve_tac [subset_mem_Vfrom, succ_subsetI] 1)); 

117 
by (rtac (Vfrom_mono RSN (2,subset_trans)) 2); 

118 
by (REPEAT (resolve_tac [prem, subset_refl, subset_succI] 1)); 

760  119 
qed "succ_in_Vfrom"; 
0  120 

121 
(*** 0, successor and limit equations fof Vfrom ***) 

122 

123 
goal Univ.thy "Vfrom(A,0) = A"; 

124 
by (rtac (Vfrom RS ssubst) 1); 

125 
by (fast_tac eq_cs 1); 

760  126 
qed "Vfrom_0"; 
0  127 

128 
goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"; 

129 
by (rtac (Vfrom RS trans) 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

130 
by (rtac (succI1 RS RepFunI RS Union_upper RSN 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

131 
(2, equalityI RS subst_context)) 1); 
0  132 
by (rtac UN_least 1); 
133 
by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1); 

27  134 
by (etac (ltI RS le_imp_subset) 1); 
135 
by (etac Ord_succ 1); 

760  136 
qed "Vfrom_succ_lemma"; 
0  137 

138 
goal Univ.thy "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"; 

139 
by (res_inst_tac [("x1", "succ(i)")] (Vfrom_rank_eq RS subst) 1); 

140 
by (res_inst_tac [("x1", "i")] (Vfrom_rank_eq RS subst) 1); 

141 
by (rtac (rank_succ RS ssubst) 1); 

142 
by (rtac (Ord_rank RS Vfrom_succ_lemma) 1); 

760  143 
qed "Vfrom_succ"; 
0  144 

145 
(*The premise distinguishes this from Vfrom(A,0); allowing X=0 forces 

146 
the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *) 

147 
val [prem] = goal Univ.thy "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))"; 

148 
by (rtac (Vfrom RS ssubst) 1); 

149 
by (rtac equalityI 1); 

150 
(*first inclusion*) 

151 
by (rtac Un_least 1); 

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

152 
by (rtac (A_subset_Vfrom RS subset_trans) 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

153 
by (rtac (prem RS UN_upper) 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

154 
by (rtac UN_least 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

155 
by (etac UnionE 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

156 
by (rtac subset_trans 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

157 
by (etac UN_upper 2); 
0  158 
by (rtac (Vfrom RS ssubst) 1); 
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

159 
by (etac ([UN_upper, Un_upper2] MRS subset_trans) 1); 
0  160 
(*opposite inclusion*) 
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

161 
by (rtac UN_least 1); 
0  162 
by (rtac (Vfrom RS ssubst) 1); 
163 
by (fast_tac ZF_cs 1); 

760  164 
qed "Vfrom_Union"; 
0  165 

166 
goal Univ.thy "!!i. Ord(i) ==> i=0  (EX j. i=succ(j))  Limit(i)"; 

27  167 
by (fast_tac (ZF_cs addSIs [non_succ_LimitI, Ord_0_lt]) 1); 
760  168 
qed "Ord_cases_lemma"; 
0  169 

170 
val major::prems = goal Univ.thy 

171 
"[ Ord(i); \ 

172 
\ i=0 ==> P; \ 

173 
\ !!j. i=succ(j) ==> P; \ 

174 
\ Limit(i) ==> P \ 

175 
\ ] ==> P"; 

176 
by (cut_facts_tac [major RS Ord_cases_lemma] 1); 

177 
by (REPEAT (eresolve_tac (prems@[disjE, exE]) 1)); 

760  178 
qed "Ord_cases"; 
0  179 

180 

181 
(*** Vfrom applied to Limit ordinals ***) 

182 

183 
(*NB. limit ordinals are nonempty; 

184 
Vfrom(A,0) = A = A Un (UN y:0. Vfrom(A,y)) *) 

185 
val [limiti] = goal Univ.thy 

186 
"Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))"; 

27  187 
by (rtac (limiti RS (Limit_has_0 RS ltD) RS Vfrom_Union RS subst) 1); 
0  188 
by (rtac (limiti RS Limit_Union_eq RS ssubst) 1); 
189 
by (rtac refl 1); 

760  190 
qed "Limit_Vfrom_eq"; 
0  191 

27  192 
goal Univ.thy "!!a. [ a: Vfrom(A,j); Limit(i); j<i ] ==> a : Vfrom(A,i)"; 
193 
by (rtac (Limit_Vfrom_eq RS equalityD2 RS subsetD) 1); 

194 
by (REPEAT (ares_tac [ltD RS UN_I] 1)); 

760  195 
qed "Limit_VfromI"; 
27  196 

197 
val prems = goal Univ.thy 

198 
"[ a: Vfrom(A,i); Limit(i); \ 

199 
\ !!x. [ x<i; a: Vfrom(A,x) ] ==> R \ 

200 
\ ] ==> R"; 

201 
by (rtac (Limit_Vfrom_eq RS equalityD1 RS subsetD RS UN_E) 1); 

202 
by (REPEAT (ares_tac (prems @ [ltI, Limit_is_Ord]) 1)); 

760  203 
qed "Limit_VfromE"; 
0  204 

516  205 
val zero_in_VLimit = Limit_has_0 RS ltD RS zero_in_Vfrom; 
484  206 

0  207 
val [major,limiti] = goal Univ.thy 
208 
"[ a: Vfrom(A,i); Limit(i) ] ==> {a} : Vfrom(A,i)"; 

27  209 
by (rtac ([major,limiti] MRS Limit_VfromE) 1); 
210 
by (etac ([singleton_in_Vfrom, limiti] MRS Limit_VfromI) 1); 

0  211 
by (etac (limiti RS Limit_has_succ) 1); 
760  212 
qed "singleton_in_VLimit"; 
0  213 

214 
val Vfrom_UnI1 = Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD) 

215 
and Vfrom_UnI2 = Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD); 

216 

217 
(*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*) 

218 
val [aprem,bprem,limiti] = goal Univ.thy 

219 
"[ a: Vfrom(A,i); b: Vfrom(A,i); Limit(i) ] ==> \ 

220 
\ {a,b} : Vfrom(A,i)"; 

27  221 
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1); 
222 
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1); 

223 
by (rtac ([doubleton_in_Vfrom, limiti] MRS Limit_VfromI) 1); 

224 
by (etac Vfrom_UnI1 1); 

225 
by (etac Vfrom_UnI2 1); 

226 
by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1)); 

760  227 
qed "doubleton_in_VLimit"; 
0  228 

229 
val [aprem,bprem,limiti] = goal Univ.thy 

230 
"[ a: Vfrom(A,i); b: Vfrom(A,i); Limit(i) ] ==> \ 

231 
\ <a,b> : Vfrom(A,i)"; 

232 
(*Infer that a, b occur at ordinals x,xa < i.*) 

27  233 
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1); 
234 
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1); 

235 
by (rtac ([Pair_in_Vfrom, limiti] MRS Limit_VfromI) 1); 

0  236 
(*Infer that succ(succ(x Un xa)) < i *) 
27  237 
by (etac Vfrom_UnI1 1); 
238 
by (etac Vfrom_UnI2 1); 

239 
by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1)); 

760  240 
qed "Pair_in_VLimit"; 
484  241 

242 
goal Univ.thy "!!i. Limit(i) ==> Vfrom(A,i)*Vfrom(A,i) <= Vfrom(A,i)"; 

516  243 
by (REPEAT (ares_tac [subsetI,Pair_in_VLimit] 1 
484  244 
ORELSE eresolve_tac [SigmaE, ssubst] 1)); 
760  245 
qed "product_VLimit"; 
484  246 

803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

247 
bind_thm ("Sigma_subset_VLimit", 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

248 
[Sigma_mono, product_VLimit] MRS subset_trans); 
484  249 

803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

250 
bind_thm ("nat_subset_VLimit", 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

251 
[nat_le_Limit RS le_imp_subset, i_subset_Vfrom] MRS subset_trans); 
484  252 

488  253 
goal Univ.thy "!!i. [ n: nat; Limit(i) ] ==> n : Vfrom(A,i)"; 
516  254 
by (REPEAT (ares_tac [nat_subset_VLimit RS subsetD] 1)); 
760  255 
qed "nat_into_VLimit"; 
484  256 

257 
(** Closure under disjoint union **) 

258 

803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

259 
bind_thm ("zero_in_VLimit", Limit_has_0 RS ltD RS zero_in_Vfrom); 
484  260 

261 
goal Univ.thy "!!i. Limit(i) ==> 1 : Vfrom(A,i)"; 

516  262 
by (REPEAT (ares_tac [nat_into_VLimit, nat_0I, nat_succI] 1)); 
760  263 
qed "one_in_VLimit"; 
484  264 

265 
goalw Univ.thy [Inl_def] 

266 
"!!A a. [ a: Vfrom(A,i); Limit(i) ] ==> Inl(a) : Vfrom(A,i)"; 

516  267 
by (REPEAT (ares_tac [zero_in_VLimit, Pair_in_VLimit] 1)); 
760  268 
qed "Inl_in_VLimit"; 
484  269 

270 
goalw Univ.thy [Inr_def] 

271 
"!!A b. [ b: Vfrom(A,i); Limit(i) ] ==> Inr(b) : Vfrom(A,i)"; 

516  272 
by (REPEAT (ares_tac [one_in_VLimit, Pair_in_VLimit] 1)); 
760  273 
qed "Inr_in_VLimit"; 
484  274 

275 
goal Univ.thy "!!i. Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)"; 

516  276 
by (fast_tac (sum_cs addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1); 
760  277 
qed "sum_VLimit"; 
484  278 

803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

279 
bind_thm ("sum_subset_VLimit", [sum_mono, sum_VLimit] MRS subset_trans); 
484  280 

0  281 

282 

283 
(*** Properties assuming Transset(A) ***) 

284 

285 
goal Univ.thy "!!i A. Transset(A) ==> Transset(Vfrom(A,i))"; 

286 
by (eps_ind_tac "i" 1); 

287 
by (rtac (Vfrom RS ssubst) 1); 

288 
by (fast_tac (ZF_cs addSIs [Transset_Union_family, Transset_Un, 

289 
Transset_Pow]) 1); 

760  290 
qed "Transset_Vfrom"; 
0  291 

292 
goal Univ.thy "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))"; 

293 
by (rtac (Vfrom_succ RS trans) 1); 

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

294 
by (rtac (Un_upper2 RSN (2,equalityI)) 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

295 
by (rtac (subset_refl RSN (2,Un_least)) 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

296 
by (rtac (A_subset_Vfrom RS subset_trans) 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

297 
by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1); 
760  298 
qed "Transset_Vfrom_succ"; 
0  299 

435  300 
goalw Ordinal.thy [Pair_def,Transset_def] 
0  301 
"!!C. [ <a,b> <= C; Transset(C) ] ==> a: C & b: C"; 
302 
by (fast_tac ZF_cs 1); 

760  303 
qed "Transset_Pair_subset"; 
0  304 

305 
goal Univ.thy 

306 
"!!a b.[ <a,b> <= Vfrom(A,i); Transset(A); Limit(i) ] ==> \ 

307 
\ <a,b> : Vfrom(A,i)"; 

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

308 
by (etac (Transset_Pair_subset RS conjE) 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

309 
by (etac Transset_Vfrom 1); 
516  310 
by (REPEAT (ares_tac [Pair_in_VLimit] 1)); 
760  311 
qed "Transset_Pair_subset_VLimit"; 
0  312 

313 

314 
(*** Closure under product/sum applied to elements  thus Vfrom(A,i) 

315 
is a model of simple type theory provided A is a transitive set 

316 
and i is a limit ordinal 

317 
***) 

318 

187  319 
(*General theorem for membership in Vfrom(A,i) when i is a limit ordinal*) 
320 
val [aprem,bprem,limiti,step] = goal Univ.thy 

321 
"[ a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); \ 

322 
\ !!x y j. [ j<i; 1:j; x: Vfrom(A,j); y: Vfrom(A,j) \ 

323 
\ ] ==> EX k. h(x,y): Vfrom(A,k) & k<i ] ==> \ 

324 
\ h(a,b) : Vfrom(A,i)"; 

325 
(*Infer that a, b occur at ordinals x,xa < i.*) 

326 
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1); 

327 
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1); 

828  328 
by (res_inst_tac [("j1", "x Un xa Un 2")] (step RS exE) 1); 
187  329 
by (DO_GOAL [etac conjE, etac Limit_VfromI, rtac limiti, atac] 5); 
330 
by (etac (Vfrom_UnI2 RS Vfrom_UnI1) 4); 

331 
by (etac (Vfrom_UnI1 RS Vfrom_UnI1) 3); 

332 
by (rtac (succI1 RS UnI2) 2); 

333 
by (REPEAT (ares_tac [limiti, Limit_has_0, Limit_has_succ, Un_least_lt] 1)); 

760  334 
qed "in_VLimit"; 
0  335 

336 
(** products **) 

337 

338 
goal Univ.thy 

187  339 
"!!A. [ a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) ] ==> \ 
340 
\ a*b : Vfrom(A, succ(succ(succ(j))))"; 

0  341 
by (dtac Transset_Vfrom 1); 
342 
by (rtac subset_mem_Vfrom 1); 

343 
by (rewtac Transset_def); 

344 
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1); 

760  345 
qed "prod_in_Vfrom"; 
0  346 

347 
val [aprem,bprem,limiti,transset] = goal Univ.thy 

348 
"[ a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) ] ==> \ 

349 
\ a*b : Vfrom(A,i)"; 

516  350 
by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1); 
187  351 
by (REPEAT (ares_tac [exI, conjI, prod_in_Vfrom, transset, 
352 
limiti RS Limit_has_succ] 1)); 

760  353 
qed "prod_in_VLimit"; 
0  354 

355 
(** Disjoint sums, aka Quine ordered pairs **) 

356 

357 
goalw Univ.thy [sum_def] 

187  358 
"!!A. [ a: Vfrom(A,j); b: Vfrom(A,j); Transset(A); 1:j ] ==> \ 
359 
\ a+b : Vfrom(A, succ(succ(succ(j))))"; 

0  360 
by (dtac Transset_Vfrom 1); 
361 
by (rtac subset_mem_Vfrom 1); 

362 
by (rewtac Transset_def); 

363 
by (fast_tac (ZF_cs addIs [zero_in_Vfrom, Pair_in_Vfrom, 

364 
i_subset_Vfrom RS subsetD]) 1); 

760  365 
qed "sum_in_Vfrom"; 
0  366 

367 
val [aprem,bprem,limiti,transset] = goal Univ.thy 

368 
"[ a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) ] ==> \ 

369 
\ a+b : Vfrom(A,i)"; 

516  370 
by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1); 
187  371 
by (REPEAT (ares_tac [exI, conjI, sum_in_Vfrom, transset, 
372 
limiti RS Limit_has_succ] 1)); 

760  373 
qed "sum_in_VLimit"; 
0  374 

375 
(** function space! **) 

376 

377 
goalw Univ.thy [Pi_def] 

187  378 
"!!A. [ a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) ] ==> \ 
379 
\ a>b : Vfrom(A, succ(succ(succ(succ(j)))))"; 

0  380 
by (dtac Transset_Vfrom 1); 
381 
by (rtac subset_mem_Vfrom 1); 

382 
by (rtac (Collect_subset RS subset_trans) 1); 

383 
by (rtac (Vfrom RS ssubst) 1); 

384 
by (rtac (subset_trans RS subset_trans) 1); 

385 
by (rtac Un_upper2 3); 

386 
by (rtac (succI1 RS UN_upper) 2); 

387 
by (rtac Pow_mono 1); 

388 
by (rewtac Transset_def); 

389 
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1); 

760  390 
qed "fun_in_Vfrom"; 
0  391 

392 
val [aprem,bprem,limiti,transset] = goal Univ.thy 

393 
"[ a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) ] ==> \ 

394 
\ a>b : Vfrom(A,i)"; 

516  395 
by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1); 
187  396 
by (REPEAT (ares_tac [exI, conjI, fun_in_Vfrom, transset, 
397 
limiti RS Limit_has_succ] 1)); 

760  398 
qed "fun_in_VLimit"; 
0  399 

400 

401 
(*** The set Vset(i) ***) 

402 

403 
goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))"; 

404 
by (rtac (Vfrom RS ssubst) 1); 

405 
by (fast_tac eq_cs 1); 

760  406 
qed "Vset"; 
0  407 

408 
val Vset_succ = Transset_0 RS Transset_Vfrom_succ; 

409 

410 
val Transset_Vset = Transset_0 RS Transset_Vfrom; 

411 

412 
(** Characterisation of the elements of Vset(i) **) 

413 

27  414 
val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. b : Vset(i) > rank(b) < i"; 
0  415 
by (rtac (ordi RS trans_induct) 1); 
416 
by (rtac (Vset RS ssubst) 1); 

417 
by (safe_tac ZF_cs); 

418 
by (rtac (rank RS ssubst) 1); 

27  419 
by (rtac UN_succ_least_lt 1); 
420 
by (fast_tac ZF_cs 2); 

421 
by (REPEAT (ares_tac [ltI] 1)); 

760  422 
qed "Vset_rank_imp1"; 
0  423 

27  424 
(* [ Ord(i); x : Vset(i) ] ==> rank(x) < i *) 
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset

425 
bind_thm ("VsetD", (Vset_rank_imp1 RS spec RS mp)); 
0  426 

427 
val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i > b : Vset(i)"; 

428 
by (rtac (ordi RS trans_induct) 1); 

429 
by (rtac allI 1); 

430 
by (rtac (Vset RS ssubst) 1); 

27  431 
by (fast_tac (ZF_cs addSIs [rank_lt RS ltD]) 1); 
760  432 
qed "Vset_rank_imp2"; 
0  433 

27  434 
goal Univ.thy "!!x i. rank(x)<i ==> x : Vset(i)"; 
435 
by (etac ltE 1); 

436 
by (etac (Vset_rank_imp2 RS spec RS mp) 1); 

437 
by (assume_tac 1); 

760  438 
qed "VsetI"; 
0  439 

27  440 
goal Univ.thy "!!i. Ord(i) ==> b : Vset(i) <> rank(b) < i"; 
0  441 
by (rtac iffI 1); 
27  442 
by (REPEAT (eresolve_tac [asm_rl, VsetD, VsetI] 1)); 
760  443 
qed "Vset_Ord_rank_iff"; 
0  444 

27  445 
goal Univ.thy "b : Vset(a) <> rank(b) < rank(a)"; 
0  446 
by (rtac (Vfrom_rank_eq RS subst) 1); 
447 
by (rtac (Ord_rank RS Vset_Ord_rank_iff) 1); 

760  448 
qed "Vset_rank_iff"; 
0  449 

450 
goal Univ.thy "!!i. Ord(i) ==> rank(Vset(i)) = i"; 

451 
by (rtac (rank RS ssubst) 1); 

452 
by (rtac equalityI 1); 

453 
by (safe_tac ZF_cs); 

828  454 
by (EVERY' [rtac UN_I, 
0  455 
etac (i_subset_Vfrom RS subsetD), 
456 
etac (Ord_in_Ord RS rank_of_Ord RS ssubst), 

457 
assume_tac, 

458 
rtac succI1] 3); 

27  459 
by (REPEAT (eresolve_tac [asm_rl, VsetD RS ltD, Ord_trans] 1)); 
760  460 
qed "rank_Vset"; 
0  461 

462 
(** Lemmas for reasoning about sets in terms of their elements' ranks **) 

463 

464 
goal Univ.thy "a <= Vset(rank(a))"; 

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

465 
by (rtac subsetI 1); 
27  466 
by (etac (rank_lt RS VsetI) 1); 
760  467 
qed "arg_subset_Vset_rank"; 
0  468 

469 
val [iprem] = goal Univ.thy 

470 
"[ !!i. Ord(i) ==> a Int Vset(i) <= b ] ==> a <= b"; 

27  471 
by (rtac ([subset_refl, arg_subset_Vset_rank] MRS 
472 
Int_greatest RS subset_trans) 1); 

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

473 
by (rtac (Ord_rank RS iprem) 1); 
760  474 
qed "Int_Vset_subset"; 
0  475 

476 
(** Set up an environment for simplification **) 

477 

478 
val rank_rls = [rank_Inl, rank_Inr, rank_pair1, rank_pair2]; 

27  479 
val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [lt_trans])); 
0  480 

481 
val rank_ss = ZF_ss 

27  482 
addsimps [case_Inl, case_Inr, VsetI] 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

483 
addsimps rank_trans_rls; 
0  484 

485 
(** Recursion over Vset levels! **) 

486 

487 
(*NOT SUITABLE FOR REWRITING: recursive!*) 

488 
goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))"; 

489 
by (rtac (transrec RS ssubst) 1); 

27  490 
by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, 
491 
VsetI RS beta, le_refl]) 1); 

760  492 
qed "Vrec"; 
0  493 

494 
(*This form avoids giant explosions in proofs. NOTE USE OF == *) 

495 
val rew::prems = goal Univ.thy 

496 
"[ !!x. h(x)==Vrec(x,H) ] ==> \ 

497 
\ h(a) = H(a, lam x: Vset(rank(a)). h(x))"; 

498 
by (rewtac rew); 

499 
by (rtac Vrec 1); 

760  500 
qed "def_Vrec"; 
0  501 

502 

503 
(*** univ(A) ***) 

504 

505 
goalw Univ.thy [univ_def] "!!A B. A<=B ==> univ(A) <= univ(B)"; 

506 
by (etac Vfrom_mono 1); 

507 
by (rtac subset_refl 1); 

760  508 
qed "univ_mono"; 
0  509 

510 
goalw Univ.thy [univ_def] "!!A. Transset(A) ==> Transset(univ(A))"; 

511 
by (etac Transset_Vfrom 1); 

760  512 
qed "Transset_univ"; 
0  513 

514 
(** univ(A) as a limit **) 

515 

516 
goalw Univ.thy [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))"; 

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

517 
by (rtac (Limit_nat RS Limit_Vfrom_eq) 1); 
760  518 
qed "univ_eq_UN"; 
0  519 

520 
goal Univ.thy "!!c. c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))"; 

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

521 
by (rtac (subset_UN_iff_eq RS iffD1) 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

522 
by (etac (univ_eq_UN RS subst) 1); 
760  523 
qed "subset_univ_eq_Int"; 
0  524 

525 
val [aprem, iprem] = goal Univ.thy 

526 
"[ a <= univ(X); \ 

527 
\ !!i. i:nat ==> a Int Vfrom(X,i) <= b \ 

528 
\ ] ==> a <= b"; 

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

529 
by (rtac (aprem RS subset_univ_eq_Int RS ssubst) 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

530 
by (rtac UN_least 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

531 
by (etac iprem 1); 
760  532 
qed "univ_Int_Vfrom_subset"; 
0  533 

534 
val prems = goal Univ.thy 

535 
"[ a <= univ(X); b <= univ(X); \ 

536 
\ !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \ 

537 
\ ] ==> a = b"; 

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

538 
by (rtac equalityI 1); 
0  539 
by (ALLGOALS 
540 
(resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN' 

541 
eresolve_tac (prems RL [equalityD1,equalityD2] RL [subset_trans]) THEN' 

542 
rtac Int_lower1)); 

760  543 
qed "univ_Int_Vfrom_eq"; 
0  544 

545 
(** Closure properties **) 

546 

547 
goalw Univ.thy [univ_def] "0 : univ(A)"; 

548 
by (rtac (nat_0I RS zero_in_Vfrom) 1); 

760  549 
qed "zero_in_univ"; 
0  550 

551 
goalw Univ.thy [univ_def] "A <= univ(A)"; 

552 
by (rtac A_subset_Vfrom 1); 

760  553 
qed "A_subset_univ"; 
0  554 

555 
val A_into_univ = A_subset_univ RS subsetD; 

556 

557 
(** Closure under unordered and ordered pairs **) 

558 

559 
goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> {a} : univ(A)"; 

516  560 
by (REPEAT (ares_tac [singleton_in_VLimit, Limit_nat] 1)); 
760  561 
qed "singleton_in_univ"; 
0  562 

563 
goalw Univ.thy [univ_def] 

564 
"!!A a. [ a: univ(A); b: univ(A) ] ==> {a,b} : univ(A)"; 

516  565 
by (REPEAT (ares_tac [doubleton_in_VLimit, Limit_nat] 1)); 
760  566 
qed "doubleton_in_univ"; 
0  567 

568 
goalw Univ.thy [univ_def] 

569 
"!!A a. [ a: univ(A); b: univ(A) ] ==> <a,b> : univ(A)"; 

516  570 
by (REPEAT (ares_tac [Pair_in_VLimit, Limit_nat] 1)); 
760  571 
qed "Pair_in_univ"; 
0  572 

484  573 
goalw Univ.thy [univ_def] "univ(A)*univ(A) <= univ(A)"; 
516  574 
by (rtac (Limit_nat RS product_VLimit) 1); 
760  575 
qed "product_univ"; 
0  576 

577 

578 
(** The natural numbers **) 

579 

580 
goalw Univ.thy [univ_def] "nat <= univ(A)"; 

581 
by (rtac i_subset_Vfrom 1); 

760  582 
qed "nat_subset_univ"; 
0  583 

584 
(* n:nat ==> n:univ(A) *) 

782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset

585 
bind_thm ("nat_into_univ", (nat_subset_univ RS subsetD)); 
0  586 

587 
(** instances for 1 and 2 **) 

588 

484  589 
goalw Univ.thy [univ_def] "1 : univ(A)"; 
516  590 
by (rtac (Limit_nat RS one_in_VLimit) 1); 
760  591 
qed "one_in_univ"; 
0  592 

593 
(*unused!*) 

828  594 
goal Univ.thy "2 : univ(A)"; 
0  595 
by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1)); 
760  596 
qed "two_in_univ"; 
0  597 

598 
goalw Univ.thy [bool_def] "bool <= univ(A)"; 

599 
by (fast_tac (ZF_cs addSIs [zero_in_univ,one_in_univ]) 1); 

760  600 
qed "bool_subset_univ"; 
0  601 

782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset

602 
bind_thm ("bool_into_univ", (bool_subset_univ RS subsetD)); 
0  603 

604 

605 
(** Closure under disjoint union **) 

606 

484  607 
goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)"; 
516  608 
by (etac (Limit_nat RSN (2,Inl_in_VLimit)) 1); 
760  609 
qed "Inl_in_univ"; 
0  610 

484  611 
goalw Univ.thy [univ_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)"; 
516  612 
by (etac (Limit_nat RSN (2,Inr_in_VLimit)) 1); 
760  613 
qed "Inr_in_univ"; 
0  614 

484  615 
goalw Univ.thy [univ_def] "univ(C)+univ(C) <= univ(C)"; 
516  616 
by (rtac (Limit_nat RS sum_VLimit) 1); 
760  617 
qed "sum_univ"; 
0  618 

803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

619 
bind_thm ("sum_subset_univ", [sum_mono, sum_univ] MRS subset_trans); 
484  620 

621 

0  622 
(** Closure under binary union  use Un_least **) 
623 
(** Closure under Collect  use (Collect_subset RS subset_trans) **) 

624 
(** Closure under RepFun  use RepFun_subset **) 

803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

625 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

626 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

627 
(*** Finite Branching Closure Properties ***) 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

628 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

629 
(** Closure under finite powerset **) 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

630 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

631 
goal Univ.thy 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

632 
"!!i. [ b: Fin(Vfrom(A,i)); Limit(i) ] ==> EX j. b <= Vfrom(A,j) & j<i"; 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

633 
by (eresolve_tac [Fin_induct] 1); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

634 
by (fast_tac (ZF_cs addSDs [Limit_has_0]) 1); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

635 
by (safe_tac ZF_cs); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

636 
by (eresolve_tac [Limit_VfromE] 1); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

637 
by (assume_tac 1); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

638 
by (res_inst_tac [("x", "xa Un j")] exI 1); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

639 
by (best_tac (ZF_cs addIs [subset_refl RS Vfrom_mono RS subsetD, 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

640 
Un_least_lt]) 1); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

641 
val Fin_Vfrom_lemma = result(); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

642 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

643 
goal Univ.thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)"; 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

644 
by (rtac subsetI 1); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

645 
by (dresolve_tac [Fin_Vfrom_lemma] 1); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

646 
by (safe_tac ZF_cs); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

647 
by (resolve_tac [Vfrom RS ssubst] 1); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

648 
by (fast_tac (ZF_cs addSDs [ltD]) 1); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

649 
val Fin_VLimit = result(); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

650 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

651 
bind_thm ("Fin_subset_VLimit", [Fin_mono, Fin_VLimit] MRS subset_trans); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

652 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

653 
goalw Univ.thy [univ_def] "Fin(univ(A)) <= univ(A)"; 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

654 
by (rtac (Limit_nat RS Fin_VLimit) 1); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

655 
val Fin_univ = result(); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

656 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

657 
(** Closure under finite powers (functions from a fixed natural number) **) 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

658 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

659 
goal Univ.thy 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

660 
"!!i. [ n: nat; Limit(i) ] ==> n > Vfrom(A,i) <= Vfrom(A,i)"; 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

661 
by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

662 
by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

663 
nat_subset_VLimit, subset_refl] 1)); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

664 
val nat_fun_VLimit = result(); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

665 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

666 
bind_thm ("nat_fun_subset_VLimit", [Pi_mono, nat_fun_VLimit] MRS subset_trans); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

667 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

668 
goalw Univ.thy [univ_def] "!!i. n: nat ==> n > univ(A) <= univ(A)"; 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

669 
by (etac (Limit_nat RSN (2,nat_fun_VLimit)) 1); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

670 
val nat_fun_univ = result(); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

671 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

672 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

673 
(** Closure under finite function space **) 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

674 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

675 
(*General but seldomused version; normally the domain is fixed*) 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

676 
goal Univ.thy 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

677 
"!!i. Limit(i) ==> Vfrom(A,i) > Vfrom(A,i) <= Vfrom(A,i)"; 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

678 
by (resolve_tac [FiniteFun.dom_subset RS subset_trans] 1); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

679 
by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, subset_refl] 1)); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

680 
val FiniteFun_VLimit1 = result(); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

681 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

682 
goalw Univ.thy [univ_def] "univ(A) > univ(A) <= univ(A)"; 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

683 
by (rtac (Limit_nat RS FiniteFun_VLimit1) 1); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

684 
val FiniteFun_univ1 = result(); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

685 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

686 
(*Version for a fixed domain*) 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

687 
goal Univ.thy 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

688 
"!!i. [ W <= Vfrom(A,i); Limit(i) ] ==> W > Vfrom(A,i) <= Vfrom(A,i)"; 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

689 
by (eresolve_tac [subset_refl RSN (2, FiniteFun_mono) RS subset_trans] 1); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

690 
by (eresolve_tac [FiniteFun_VLimit1] 1); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

691 
val FiniteFun_VLimit = result(); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

692 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

693 
goalw Univ.thy [univ_def] 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

694 
"!!W. W <= univ(A) ==> W > univ(A) <= univ(A)"; 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

695 
by (etac (Limit_nat RSN (2, FiniteFun_VLimit)) 1); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

696 
val FiniteFun_univ = result(); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

697 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

698 
goal Univ.thy 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

699 
"!!W. [ f: W > univ(A); W <= univ(A) ] ==> f : univ(A)"; 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

700 
by (eresolve_tac [FiniteFun_univ RS subsetD] 1); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

701 
by (assume_tac 1); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

702 
val FiniteFun_in_univ = result(); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

703 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

704 
(*Remove <= from the rule above*) 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

705 
val FiniteFun_in_univ' = subsetI RSN (2, FiniteFun_in_univ); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

706 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

707 