author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 2033  639de962ded4 
permissions  rwrr 
1461  1 
(* Title: ZF/epsilon.ML 
0  2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  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); 

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

15 
by (rtac (nat_0I RS UN_upper) 1); 
760  16 
qed "arg_subset_eclose"; 
0  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); 

760  28 
qed "Transset_eclose"; 
0  29 

30 
(* x : eclose(A) ==> x <= eclose(A) *) 

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

31 
bind_thm ("eclose_subset", 
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset

32 
rewrite_rule [Transset_def] Transset_eclose RS bspec); 
0  33 

34 
(* [ A : eclose(B); c : A ] ==> c : eclose(B) *) 

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

35 
bind_thm ("ecloseD", eclose_subset RS subsetD); 
0  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 
*) 

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

44 
bind_thm ("eclose_induct", Transset_eclose RSN (2, Transset_induct)); 
0  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); 

760  51 
qed "eps_induct"; 
0  52 

53 
(*Perform epsiloninduction on i. *) 

54 
fun eps_ind_tac a = 

55 
EVERY' [res_inst_tac [("a",a)] eps_induct, 

1461  56 
rename_last_tac a ["1"]]; 
0  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); 
760  70 
qed "eclose_least_lemma"; 
0  71 

72 
goalw Epsilon.thy [eclose_def] 

73 
"!!X A. [ Transset(X); A<=X ] ==> eclose(A) <= X"; 

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

74 
by (rtac (eclose_least_lemma RS UN_least) 1); 
0  75 
by (REPEAT (assume_tac 1)); 
760  76 
qed "eclose_least"; 
0  77 

78 
(*COMPLETELY DIFFERENT induction principle from eclose_induct!!*) 

79 
val [major,base,step] = goal Epsilon.thy 

1461  80 
"[ a: eclose(b); \ 
81 
\ !!y. [ y: b ] ==> P(y); \ 

82 
\ !!y z. [ y: eclose(b); P(y); z: y ] ==> P(z) \ 

0  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); 

760  90 
qed "eclose_induct_down"; 
0  91 

92 
goal Epsilon.thy "!!X. Transset(X) ==> eclose(X) = X"; 

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

93 
by (etac ([eclose_least, arg_subset_eclose] MRS equalityI) 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

94 
by (rtac subset_refl 1); 
760  95 
qed "Transset_eclose_eq_arg"; 
0  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)); 

760  104 
qed "mem_eclose_trans"; 
0  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)); 

760  111 
qed "mem_eclose_sing_trans"; 
0  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); 

760  116 
qed "under_Memrel"; 
0  117 

118 
(* j : eclose(A) ==> Memrel(eclose(A)) `` j = j *) 

119 
val under_Memrel_eclose = Transset_eclose RS under_Memrel; 

120 

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

121 
bind_thm ("wfrec_ssubst", wf_Memrel RS wfrec RS ssubst); 
0  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, 
1461  130 
jmemi RSN (2,mem_eclose_sing_trans)]) 1); 
760  131 
qed "wfrec_eclose_eq"; 
0  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); 

760  137 
qed "wfrec_eclose_eq2"; 
0  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, 
1461  143 
under_Memrel_eclose]) 1); 
760  144 
qed "transrec"; 
0  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)); 

760  151 
qed "def_transrec"; 
0  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)); 

760  159 
qed "transrec_type"; 
0  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); 

760  164 
qed "eclose_sing_Ord"; 
0  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)); 

760  174 
qed "Ord_transrec_type"; 
0  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); 
760  182 
qed "rank"; 
0  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); 

760  190 
qed "Ord_rank"; 
0  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); 
760  196 
qed "rank_of_Ord"; 
0  197 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

198 
goal Epsilon.thy "!!a b. a:b ==> rank(a) < rank(b)"; 
0  199 
by (res_inst_tac [("a1","b")] (rank RS ssubst) 1); 
129  200 
by (etac (UN_I RS ltI) 1); 
0  201 
by (rtac succI1 1); 
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

202 
by (REPEAT (ares_tac [Ord_UN, Ord_succ, Ord_rank] 1)); 
760  203 
qed "rank_lt"; 
0  204 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

205 
val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) < rank(b)"; 
0  206 
by (rtac (major RS eclose_induct_down) 1); 
207 
by (etac rank_lt 1); 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

208 
by (etac (rank_lt RS lt_trans) 1); 
0  209 
by (assume_tac 1); 
760  210 
qed "eclose_rank_lt"; 
0  211 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

212 
goal Epsilon.thy "!!a b. a<=b ==> rank(a) le rank(b)"; 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

213 
by (rtac subset_imp_le 1); 
0  214 
by (rtac (rank RS ssubst) 1); 
215 
by (rtac (rank RS ssubst) 1); 

216 
by (etac UN_mono 1); 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

217 
by (REPEAT (resolve_tac [subset_refl, Ord_rank] 1)); 
760  218 
qed "rank_mono"; 
0  219 

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

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

437  222 
by (rtac le_anti_sym 1); 
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

223 
by (DO_GOAL [rtac (Ord_rank RS Ord_succ RS UN_least_le), 
1461  224 
etac (PowD RS rank_mono RS succ_leI)] 1); 
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

225 
by (DO_GOAL [rtac ([Pow_top, le_refl] MRS UN_upper_le), 
1461  226 
REPEAT o rtac (Ord_rank RS Ord_succ)] 1); 
760  227 
qed "rank_Pow"; 
0  228 

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

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

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

760  232 
qed "rank_0"; 
0  233 

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

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

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

236 
by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

237 
by (etac succE 1); 
0  238 
by (fast_tac ZF_cs 1); 
129  239 
by (etac (rank_lt RS leI RS succ_leI RS le_imp_subset) 1); 
760  240 
qed "rank_succ"; 
0  241 

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

243 
by (rtac equalityI 1); 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

244 
by (rtac (rank_mono RS le_imp_subset RS UN_least) 2); 
0  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); 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

251 
by (etac (rank_lt RS succ_leI RS le_imp_subset) 1); 
760  252 
qed "rank_Union"; 
0  253 

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

437  255 
by (rtac le_anti_sym 1); 
0  256 
by (rtac (arg_subset_eclose RS rank_mono) 2); 
257 
by (res_inst_tac [("a1","eclose(a)")] (rank RS ssubst) 1); 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

258 
by (rtac (Ord_rank RS UN_least_le) 1); 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

259 
by (etac (eclose_rank_lt RS succ_leI) 1); 
760  260 
qed "rank_eclose"; 
0  261 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

262 
goalw Epsilon.thy [Pair_def] "rank(a) < rank(<a,b>)"; 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

263 
by (rtac (consI1 RS rank_lt RS lt_trans) 1); 
0  264 
by (rtac (consI1 RS consI2 RS rank_lt) 1); 
760  265 
qed "rank_pair1"; 
0  266 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

267 
goalw Epsilon.thy [Pair_def] "rank(b) < rank(<a,b>)"; 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

268 
by (rtac (consI1 RS consI2 RS rank_lt RS lt_trans) 1); 
0  269 
by (rtac (consI1 RS consI2 RS rank_lt) 1); 
760  270 
qed "rank_pair2"; 
0  271 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

272 
goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inl_def] "rank(a) < rank(Inl(a))"; 
0  273 
by (rtac rank_pair2 1); 
274 
val rank_Inl = result(); 

275 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

276 
goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inr_def] "rank(a) < rank(Inr(a))"; 
0  277 
by (rtac rank_pair2 1); 
278 
val rank_Inr = result(); 

279 

280 
(*** Corollaries of leastness ***) 

281 

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

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

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

760  285 
qed "mem_eclose_subset"; 
0  286 

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

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

289 
by (etac subset_trans 1); 

290 
by (rtac arg_subset_eclose 1); 

760  291 
qed "eclose_mono"; 
0  292 

293 
(** Idempotence of eclose **) 

294 

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

296 
by (rtac equalityI 1); 

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

298 
by (rtac arg_subset_eclose 1); 

760  299 
qed "eclose_idem"; 