author  lcp 
Fri, 17 Sep 1993 16:16:38 +0200  
changeset 6  8ce8c4d13d4d 
parent 0  a5a9c433f639 
child 14  1c0926788772 
permissions  rwrr 
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); 

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

67 
by (asm_simp_tac (ZF_ss addsimps [nat_rec_0]) 1); 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

68 
by (asm_simp_tac (ZF_ss addsimps [nat_rec_succ]) 1); 
0  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); 

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

129 
by (asm_simp_tac (ZF_ss addsimps [under_Memrel_eclose, 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

130 
jmemi RSN (2,mem_eclose_sing_trans)]) 1); 
0  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); 

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

142 
by (simp_tac (ZF_ss addsimps [wfrec_eclose_eq2, arg_in_eclose_sing, 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

143 
under_Memrel_eclose]) 1); 
0  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 
(*** Rank ***) 

177 

178 
(*NOT SUITABLE FOR REWRITING  RECURSIVE!*) 

179 
goal Epsilon.thy "rank(a) = (UN y:a. succ(rank(y)))"; 

180 
by (rtac (rank_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

181 
by (simp_tac ZF_ss 1); 
0  182 
val rank = result(); 
183 

184 
goal Epsilon.thy "Ord(rank(a))"; 

185 
by (eps_ind_tac "a" 1); 

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

187 
by (rtac (Ord_succ RS Ord_UN) 1); 

188 
by (etac bspec 1); 

189 
by (assume_tac 1); 

190 
val Ord_rank = result(); 

191 

192 
val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i"; 

193 
by (rtac (major RS trans_induct) 1); 

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

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

195 
by (asm_simp_tac (ZF_ss addsimps [Ord_equality]) 1); 
0  196 
val rank_of_Ord = result(); 
197 

198 
val [prem] = goal Epsilon.thy "a:b ==> rank(a) : rank(b)"; 

199 
by (res_inst_tac [("a1","b")] (rank RS ssubst) 1); 

200 
by (rtac (prem RS UN_I) 1); 

201 
by (rtac succI1 1); 

202 
val rank_lt = result(); 

203 

204 
val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) : rank(b)"; 

205 
by (rtac (major RS eclose_induct_down) 1); 

206 
by (etac rank_lt 1); 

207 
by (etac (rank_lt RS Ord_trans) 1); 

208 
by (assume_tac 1); 

209 
by (rtac Ord_rank 1); 

210 
val eclose_rank_lt = result(); 

211 

212 
goal Epsilon.thy "!!a b. a<=b ==> rank(a) <= rank(b)"; 

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

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

215 
by (etac UN_mono 1); 

216 
by (rtac subset_refl 1); 

217 
val rank_mono = result(); 

218 

219 
goal Epsilon.thy "rank(Pow(a)) = succ(rank(a))"; 

220 
by (rtac (rank RS trans) 1); 

221 
by (rtac equalityI 1); 

222 
by (fast_tac ZF_cs 2); 

223 
by (rtac UN_least 1); 

224 
by (etac (PowD RS rank_mono RS Ord_succ_mono) 1); 

225 
by (rtac Ord_rank 1); 

226 
by (rtac Ord_rank 1); 

227 
val rank_Pow = result(); 

228 

229 
goal Epsilon.thy "rank(0) = 0"; 

230 
by (rtac (rank RS trans) 1); 

231 
by (fast_tac (ZF_cs addSIs [equalityI]) 1); 

232 
val rank_0 = result(); 

233 

234 
goal Epsilon.thy "rank(succ(x)) = succ(rank(x))"; 

235 
by (rtac (rank RS trans) 1); 

236 
br ([UN_least, succI1 RS UN_upper] MRS equalityI) 1; 

237 
be succE 1; 

238 
by (fast_tac ZF_cs 1); 

239 
by (REPEAT (ares_tac [Ord_succ_mono,Ord_rank,OrdmemD,rank_lt] 1)); 

240 
val rank_succ = result(); 

241 

242 
goal Epsilon.thy "rank(Union(A)) = (UN x:A. rank(x))"; 

243 
by (rtac equalityI 1); 

244 
by (rtac (rank_mono RS UN_least) 2); 

245 
by (etac Union_upper 2); 

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

247 
by (rtac UN_least 1); 

248 
by (etac UnionE 1); 

249 
by (rtac subset_trans 1); 

250 
by (etac (RepFunI RS Union_upper) 2); 

251 
by (etac (rank_lt RS Ord_succ_subsetI) 1); 

252 
by (rtac Ord_rank 1); 

253 
val rank_Union = result(); 

254 

255 
goal Epsilon.thy "rank(eclose(a)) = rank(a)"; 

256 
by (rtac equalityI 1); 

257 
by (rtac (arg_subset_eclose RS rank_mono) 2); 

258 
by (res_inst_tac [("a1","eclose(a)")] (rank RS ssubst) 1); 

259 
by (rtac UN_least 1); 

260 
by (etac ([eclose_rank_lt, Ord_rank] MRS Ord_succ_subsetI) 1); 

261 
val rank_eclose = result(); 

262 

263 
(* [ i: j; j: rank(a) ] ==> i: rank(a) *) 

264 
val rank_trans = Ord_rank RSN (3, Ord_trans); 

265 

266 
goalw Epsilon.thy [Pair_def] "rank(a) : rank(<a,b>)"; 

267 
by (rtac (consI1 RS rank_lt RS Ord_trans) 1); 

268 
by (rtac (consI1 RS consI2 RS rank_lt) 1); 

269 
by (rtac Ord_rank 1); 

270 
val rank_pair1 = result(); 

271 

272 
goalw Epsilon.thy [Pair_def] "rank(b) : rank(<a,b>)"; 

273 
by (rtac (consI1 RS consI2 RS rank_lt RS Ord_trans) 1); 

274 
by (rtac (consI1 RS consI2 RS rank_lt) 1); 

275 
by (rtac Ord_rank 1); 

276 
val rank_pair2 = result(); 

277 

278 
goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inl_def] "rank(a) : rank(Inl(a))"; 

279 
by (rtac rank_pair2 1); 

280 
val rank_Inl = result(); 

281 

282 
goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inr_def] "rank(a) : rank(Inr(a))"; 

283 
by (rtac rank_pair2 1); 

284 
val rank_Inr = result(); 

285 

286 
val [major] = goal Epsilon.thy "i: rank(a) ==> (EX x:a. i<=rank(x))"; 

287 
by (resolve_tac ([major] RL [rank RS subst] RL [UN_E]) 1); 

288 
by (rtac bexI 1); 

289 
by (etac member_succD 1); 

290 
by (rtac Ord_rank 1); 

291 
by (assume_tac 1); 

292 
val rank_implies_mem = result(); 

293 

294 

295 
(*** Corollaries of leastness ***) 

296 

297 
goal Epsilon.thy "!!A B. A:B ==> eclose(A)<=eclose(B)"; 

298 
by (rtac (Transset_eclose RS eclose_least) 1); 

299 
by (etac (arg_into_eclose RS eclose_subset) 1); 

300 
val mem_eclose_subset = result(); 

301 

302 
goal Epsilon.thy "!!A B. A<=B ==> eclose(A) <= eclose(B)"; 

303 
by (rtac (Transset_eclose RS eclose_least) 1); 

304 
by (etac subset_trans 1); 

305 
by (rtac arg_subset_eclose 1); 

306 
val eclose_mono = result(); 

307 

308 
(** Idempotence of eclose **) 

309 

310 
goal Epsilon.thy "eclose(eclose(A)) = eclose(A)"; 

311 
by (rtac equalityI 1); 

312 
by (rtac ([Transset_eclose, subset_refl] MRS eclose_least) 1); 

313 
by (rtac arg_subset_eclose 1); 

314 
val eclose_idem = result(); 