author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 47072  777549486d44 
child 58871  c399ae4b836f 
permissions  rwrr 
13503  1 
(* Title: ZF/Constructible/DPow_absolute.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 
*) 

4 

5 
header {*Absoluteness for the Definable Powerset Function*} 

6 

7 

16417  8 
theory DPow_absolute imports Satisfies_absolute begin 
13503  9 

10 

11 
subsection{*Preliminary Internalizations*} 

12 

13 
subsubsection{*The Operator @{term is_formula_rec}*} 

14 

15 
text{*The three arguments of @{term p} are always 2, 1, 0. It is buried 

16 
within 11 quantifiers!!*} 

17 

18 
(* is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o" 

19 
"is_formula_rec(M,MH,p,z) == 

20 
\<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) & 

21 
2 1 0 

22 
successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)" 

23 
*) 

24 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

25 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

26 
formula_rec_fm :: "[i, i, i]=>i" where 
13503  27 
"formula_rec_fm(mh,p,z) == 
28 
Exists(Exists(Exists( 

29 
And(finite_ordinal_fm(2), 

30 
And(depth_fm(p#+3,2), 

31 
And(succ_fm(2,1), 

32 
And(fun_apply_fm(0,p#+3,z#+3), is_transrec_fm(mh,1,0))))))))" 

33 

34 
lemma is_formula_rec_type [TC]: 

35 
"[ p \<in> formula; x \<in> nat; z \<in> nat ] 

36 
==> formula_rec_fm(p,x,z) \<in> formula" 

37 
by (simp add: formula_rec_fm_def) 

38 

39 
lemma sats_formula_rec_fm: 

40 
assumes MH_iff_sats: 

41 
"!!a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10. 

42 
[a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>A; a8\<in>A; a9\<in>A; a10\<in>A] 

46823  43 
==> MH(a2, a1, a0) \<longleftrightarrow> 
13503  44 
sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3, 
45 
Cons(a4,Cons(a5,Cons(a6,Cons(a7, 

46 
Cons(a8,Cons(a9,Cons(a10,env))))))))))))" 

47 
shows 

48 
"[x \<in> nat; z \<in> nat; env \<in> list(A)] 

46823  49 
==> sats(A, formula_rec_fm(p,x,z), env) \<longleftrightarrow> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

50 
is_formula_rec(##A, MH, nth(x,env), nth(z,env))" 
13503  51 
by (simp add: formula_rec_fm_def sats_is_transrec_fm is_formula_rec_def 
52 
MH_iff_sats [THEN iff_sym]) 

53 

54 
lemma formula_rec_iff_sats: 

55 
assumes MH_iff_sats: 

56 
"!!a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10. 

57 
[a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>A; a8\<in>A; a9\<in>A; a10\<in>A] 

46823  58 
==> MH(a2, a1, a0) \<longleftrightarrow> 
13503  59 
sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3, 
60 
Cons(a4,Cons(a5,Cons(a6,Cons(a7, 

61 
Cons(a8,Cons(a9,Cons(a10,env))))))))))))" 

62 
shows 

63 
"[nth(i,env) = x; nth(k,env) = z; 

64 
i \<in> nat; k \<in> nat; env \<in> list(A)] 

46823  65 
==> is_formula_rec(##A, MH, x, z) \<longleftrightarrow> sats(A, formula_rec_fm(p,i,k), env)" 
13503  66 
by (simp add: sats_formula_rec_fm [OF MH_iff_sats]) 
67 

68 
theorem formula_rec_reflection: 

69 
assumes MH_reflection: 

70 
"!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)), 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

71 
\<lambda>i x. MH(##Lset(i), f'(x), f(x), g(x), h(x))]" 
13503  72 
shows "REFLECTS[\<lambda>x. is_formula_rec(L, MH(L,x), f(x), h(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

73 
\<lambda>i x. is_formula_rec(##Lset(i), MH(##Lset(i),x), f(x), h(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13634
diff
changeset

74 
apply (simp (no_asm_use) only: is_formula_rec_def) 
13503  75 
apply (intro FOL_reflections function_reflections fun_plus_reflections 
76 
depth_reflection is_transrec_reflection MH_reflection) 

77 
done 

78 

79 

80 
subsubsection{*The Operator @{term is_satisfies}*} 

81 

82 
(* is_satisfies(M,A,p,z) == is_formula_rec (M, satisfies_MH(M,A), p, z) *) 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

83 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

84 
satisfies_fm :: "[i,i,i]=>i" where 
13503  85 
"satisfies_fm(x) == formula_rec_fm (satisfies_MH_fm(x#+5#+6, 2, 1, 0))" 
86 

87 
lemma is_satisfies_type [TC]: 

88 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> satisfies_fm(x,y,z) \<in> formula" 

89 
by (simp add: satisfies_fm_def) 

90 

91 
lemma sats_satisfies_fm [simp]: 

92 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 

46823  93 
==> sats(A, satisfies_fm(x,y,z), env) \<longleftrightarrow> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

94 
is_satisfies(##A, nth(x,env), nth(y,env), nth(z,env))" 
13503  95 
by (simp add: satisfies_fm_def is_satisfies_def sats_satisfies_MH_fm 
96 
sats_formula_rec_fm) 

97 

98 
lemma satisfies_iff_sats: 

99 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 

100 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 

46823  101 
==> is_satisfies(##A, x, y, z) \<longleftrightarrow> sats(A, satisfies_fm(i,j,k), env)" 
13503  102 
by (simp add: sats_satisfies_fm) 
103 

104 
theorem satisfies_reflection: 

105 
"REFLECTS[\<lambda>x. is_satisfies(L,f(x),g(x),h(x)), 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

106 
\<lambda>i x. is_satisfies(##Lset(i),f(x),g(x),h(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13634
diff
changeset

107 
apply (simp only: is_satisfies_def) 
13503  108 
apply (intro formula_rec_reflection satisfies_MH_reflection) 
109 
done 

110 

111 

112 
subsection {*Relativization of the Operator @{term DPow'}*} 

113 

114 
lemma DPow'_eq: 

13692  115 
"DPow'(A) = {z . ep \<in> list(A) * formula, 
116 
\<exists>env \<in> list(A). \<exists>p \<in> formula. 

117 
ep = <env,p> & z = {x\<in>A. sats(A, p, Cons(x,env))}}" 

118 
by (simp add: DPow'_def, blast) 

13503  119 

120 

13692  121 
text{*Relativize the use of @{term sats} within @{term DPow'} 
122 
(the comprehension).*} 

21233  123 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

124 
is_DPow_sats :: "[i=>o,i,i,i,i] => o" where 
13692  125 
"is_DPow_sats(M,A,env,p,x) == 
13503  126 
\<forall>n1[M]. \<forall>e[M]. \<forall>sp[M]. 
46823  127 
is_satisfies(M,A,p,sp) \<longrightarrow> is_Cons(M,x,env,e) \<longrightarrow> 
128 
fun_apply(M, sp, e, n1) \<longrightarrow> number1(M, n1)" 

13503  129 

13692  130 
lemma (in M_satisfies) DPow_sats_abs: 
13503  131 
"[ M(A); env \<in> list(A); p \<in> formula; M(x) ] 
46823  132 
==> is_DPow_sats(M,A,env,p,x) \<longleftrightarrow> sats(A, p, Cons(x,env))" 
13503  133 
apply (subgoal_tac "M(env)") 
13692  134 
apply (simp add: is_DPow_sats_def satisfies_closed satisfies_abs) 
13503  135 
apply (blast dest: transM) 
136 
done 

137 

13692  138 
lemma (in M_satisfies) Collect_DPow_sats_abs: 
13503  139 
"[ M(A); env \<in> list(A); p \<in> formula ] 
13692  140 
==> Collect(A, is_DPow_sats(M,A,env,p)) = 
13503  141 
{x \<in> A. sats(A, p, Cons(x,env))}" 
13692  142 
by (simp add: DPow_sats_abs transM [of _ A]) 
13503  143 

144 

13692  145 
subsubsection{*The Operator @{term is_DPow_sats}, Internalized*} 
13503  146 

13692  147 
(* is_DPow_sats(M,A,env,p,x) == 
13503  148 
\<forall>n1[M]. \<forall>e[M]. \<forall>sp[M]. 
46823  149 
is_satisfies(M,A,p,sp) \<longrightarrow> is_Cons(M,x,env,e) \<longrightarrow> 
150 
fun_apply(M, sp, e, n1) \<longrightarrow> number1(M, n1) *) 

13503  151 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

152 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

153 
DPow_sats_fm :: "[i,i,i,i]=>i" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

154 
"DPow_sats_fm(A,env,p,x) == 
13503  155 
Forall(Forall(Forall( 
156 
Implies(satisfies_fm(A#+3,p#+3,0), 

157 
Implies(Cons_fm(x#+3,env#+3,1), 

158 
Implies(fun_apply_fm(0,1,2), number1_fm(2)))))))" 

159 

13692  160 
lemma is_DPow_sats_type [TC]: 
13503  161 
"[ A \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat ] 
13692  162 
==> DPow_sats_fm(A,x,y,z) \<in> formula" 
163 
by (simp add: DPow_sats_fm_def) 

13503  164 

13692  165 
lemma sats_DPow_sats_fm [simp]: 
13503  166 
"[ u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 
46823  167 
==> sats(A, DPow_sats_fm(u,x,y,z), env) \<longleftrightarrow> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

168 
is_DPow_sats(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))" 
13692  169 
by (simp add: DPow_sats_fm_def is_DPow_sats_def) 
13503  170 

13692  171 
lemma DPow_sats_iff_sats: 
13503  172 
"[ nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz; 
173 
u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 

46823  174 
==> is_DPow_sats(##A,nu,nx,ny,nz) \<longleftrightarrow> 
13692  175 
sats(A, DPow_sats_fm(u,x,y,z), env)" 
13503  176 
by simp 
177 

13692  178 
theorem DPow_sats_reflection: 
179 
"REFLECTS[\<lambda>x. is_DPow_sats(L,f(x),g(x),h(x),g'(x)), 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

180 
\<lambda>i x. is_DPow_sats(##Lset(i),f(x),g(x),h(x),g'(x))]" 
13692  181 
apply (unfold is_DPow_sats_def) 
13503  182 
apply (intro FOL_reflections function_reflections extra_reflections 
183 
satisfies_reflection) 

184 
done 

185 

186 

13687  187 
subsection{*A Locale for Relativizing the Operator @{term DPow'}*} 
13503  188 

189 
locale M_DPow = M_satisfies + 

190 
assumes sep: 

191 
"[ M(A); env \<in> list(A); p \<in> formula ] 

13692  192 
==> separation(M, \<lambda>x. is_DPow_sats(M,A,env,p,x))" 
13503  193 
and rep: 
194 
"M(A) 

195 
==> strong_replacement (M, 

196 
\<lambda>ep z. \<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) & 

197 
pair(M,env,p,ep) & 

13692  198 
is_Collect(M, A, \<lambda>x. is_DPow_sats(M,A,env,p,x), z))" 
13503  199 

200 
lemma (in M_DPow) sep': 

201 
"[ M(A); env \<in> list(A); p \<in> formula ] 

202 
==> separation(M, \<lambda>x. sats(A, p, Cons(x,env)))" 

13692  203 
by (insert sep [of A env p], simp add: DPow_sats_abs) 
13503  204 

205 
lemma (in M_DPow) rep': 

206 
"M(A) 

207 
==> strong_replacement (M, 

208 
\<lambda>ep z. \<exists>env\<in>list(A). \<exists>p\<in>formula. 

13504  209 
ep = <env,p> & z = {x \<in> A . sats(A, p, Cons(x, env))})" 
13692  210 
by (insert rep [of A], simp add: Collect_DPow_sats_abs) 
13503  211 

212 

213 
lemma univalent_pair_eq: 

214 
"univalent (M, A, \<lambda>xy z. \<exists>x\<in>B. \<exists>y\<in>C. xy = \<langle>x,y\<rangle> \<and> z = f(x,y))" 

215 
by (simp add: univalent_def, blast) 

216 

217 
lemma (in M_DPow) DPow'_closed: "M(A) ==> M(DPow'(A))" 

218 
apply (simp add: DPow'_eq) 

219 
apply (fast intro: rep' sep' univalent_pair_eq) 

220 
done 

221 

222 
text{*Relativization of the Operator @{term DPow'}*} 

21233  223 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

224 
is_DPow' :: "[i=>o,i,i] => o" where 
13503  225 
"is_DPow'(M,A,Z) == 
46823  226 
\<forall>X[M]. X \<in> Z \<longleftrightarrow> 
13503  227 
subset(M,X,A) & 
228 
(\<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) & 

13692  229 
is_Collect(M, A, is_DPow_sats(M,A,env,p), X))" 
13503  230 

231 
lemma (in M_DPow) DPow'_abs: 

46823  232 
"[M(A); M(Z)] ==> is_DPow'(M,A,Z) \<longleftrightarrow> Z = DPow'(A)" 
13503  233 
apply (rule iffI) 
13692  234 
prefer 2 apply (simp add: is_DPow'_def DPow'_def Collect_DPow_sats_abs) 
13503  235 
apply (rule M_equalityI) 
13692  236 
apply (simp add: is_DPow'_def DPow'_def Collect_DPow_sats_abs, assumption) 
13503  237 
apply (erule DPow'_closed) 
238 
done 

239 

240 

241 
subsection{*Instantiating the Locale @{text M_DPow}*} 

242 

243 
subsubsection{*The Instance of Separation*} 

244 

245 
lemma DPow_separation: 

246 
"[ L(A); env \<in> list(A); p \<in> formula ] 

13692  247 
==> separation(L, \<lambda>x. is_DPow_sats(L,A,env,p,x))" 
248 
apply (rule gen_separation_multi [OF DPow_sats_reflection, of "{A,env,p}"], 

13687  249 
auto intro: transL) 
250 
apply (rule_tac env="[A,env,p]" in DPow_LsetI) 

13692  251 
apply (rule DPow_sats_iff_sats sep_rules  simp)+ 
13503  252 
done 
253 

254 

255 

256 
subsubsection{*The Instance of Replacement*} 

257 

258 
lemma DPow_replacement_Reflects: 

259 
"REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B & 

260 
(\<exists>env[L]. \<exists>p[L]. 

261 
mem_formula(L,p) & mem_list(L,A,env) & pair(L,env,p,u) & 

13692  262 
is_Collect (L, A, is_DPow_sats(L,A,env,p), x)), 
13503  263 
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & 
264 
(\<exists>env \<in> Lset(i). \<exists>p \<in> Lset(i). 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

265 
mem_formula(##Lset(i),p) & mem_list(##Lset(i),A,env) & 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

266 
pair(##Lset(i),env,p,u) & 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

267 
is_Collect (##Lset(i), A, is_DPow_sats(##Lset(i),A,env,p), x))]" 
13503  268 
apply (unfold is_Collect_def) 
269 
apply (intro FOL_reflections function_reflections mem_formula_reflection 

13692  270 
mem_list_reflection DPow_sats_reflection) 
13503  271 
done 
272 

273 
lemma DPow_replacement: 

274 
"L(A) 

275 
==> strong_replacement (L, 

276 
\<lambda>ep z. \<exists>env[L]. \<exists>p[L]. mem_formula(L,p) & mem_list(L,A,env) & 

277 
pair(L,env,p,ep) & 

13692  278 
is_Collect(L, A, \<lambda>x. is_DPow_sats(L,A,env,p,x), z))" 
13503  279 
apply (rule strong_replacementI) 
13687  280 
apply (rule_tac u="{A,B}" 
281 
in gen_separation_multi [OF DPow_replacement_Reflects], 

282 
auto) 

13566  283 
apply (unfold is_Collect_def) 
13687  284 
apply (rule_tac env="[A,B]" in DPow_LsetI) 
13503  285 
apply (rule sep_rules mem_formula_iff_sats mem_list_iff_sats 
13692  286 
DPow_sats_iff_sats  simp)+ 
13503  287 
done 
288 

289 

290 
subsubsection{*Actually Instantiating the Locale*} 

291 

292 
lemma M_DPow_axioms_L: "M_DPow_axioms(L)" 

293 
apply (rule M_DPow_axioms.intro) 

294 
apply (assumption  rule DPow_separation DPow_replacement)+ 

295 
done 

296 

297 
theorem M_DPow_L: "PROP M_DPow(L)" 

298 
apply (rule M_DPow.intro) 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset

299 
apply (rule M_satisfies_L) 
13503  300 
apply (rule M_DPow_axioms_L) 
301 
done 

302 

303 
lemmas DPow'_closed [intro, simp] = M_DPow.DPow'_closed [OF M_DPow_L] 

304 
and DPow'_abs [intro, simp] = M_DPow.DPow'_abs [OF M_DPow_L] 

305 

13505  306 

307 
subsubsection{*The Operator @{term is_Collect}*} 

308 

309 
text{*The formula @{term is_P} has one free variable, 0, and it is 

310 
enclosed within a single quantifier.*} 

311 

312 
(* is_Collect :: "[i=>o,i,i=>o,i] => o" 

46823  313 
"is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> A & P(x)" *) 
13505  314 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

315 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

316 
Collect_fm :: "[i, i, i]=>i" where 
13505  317 
"Collect_fm(A,is_P,z) == 
318 
Forall(Iff(Member(0,succ(z)), 

319 
And(Member(0,succ(A)), is_P)))" 

320 

321 
lemma is_Collect_type [TC]: 

322 
"[ is_P \<in> formula; x \<in> nat; y \<in> nat ] 

323 
==> Collect_fm(x,is_P,y) \<in> formula" 

324 
by (simp add: Collect_fm_def) 

325 

326 
lemma sats_Collect_fm: 

327 
assumes is_P_iff_sats: 

46823  328 
"!!a. a \<in> A ==> is_P(a) \<longleftrightarrow> sats(A, p, Cons(a, env))" 
13505  329 
shows 
330 
"[x \<in> nat; y \<in> nat; env \<in> list(A)] 

46823  331 
==> sats(A, Collect_fm(x,p,y), env) \<longleftrightarrow> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

332 
is_Collect(##A, nth(x,env), is_P, nth(y,env))" 
13505  333 
by (simp add: Collect_fm_def is_Collect_def is_P_iff_sats [THEN iff_sym]) 
334 

335 
lemma Collect_iff_sats: 

336 
assumes is_P_iff_sats: 

46823  337 
"!!a. a \<in> A ==> is_P(a) \<longleftrightarrow> sats(A, p, Cons(a, env))" 
13505  338 
shows 
339 
"[ nth(i,env) = x; nth(j,env) = y; 

340 
i \<in> nat; j \<in> nat; env \<in> list(A)] 

46823  341 
==> is_Collect(##A, x, is_P, y) \<longleftrightarrow> sats(A, Collect_fm(i,p,j), env)" 
13505  342 
by (simp add: sats_Collect_fm [OF is_P_iff_sats]) 
343 

344 

345 
text{*The second argument of @{term is_P} gives it direct access to @{term x}, 

346 
which is essential for handling free variable references.*} 

347 
theorem Collect_reflection: 

348 
assumes is_P_reflection: 

349 
"!!h f g. REFLECTS[\<lambda>x. is_P(L, f(x), g(x)), 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

350 
\<lambda>i x. is_P(##Lset(i), f(x), g(x))]" 
13505  351 
shows "REFLECTS[\<lambda>x. is_Collect(L, f(x), is_P(L,x), g(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

352 
\<lambda>i x. is_Collect(##Lset(i), f(x), is_P(##Lset(i), x), g(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13634
diff
changeset

353 
apply (simp (no_asm_use) only: is_Collect_def) 
13505  354 
apply (intro FOL_reflections is_P_reflection) 
355 
done 

356 

357 

358 
subsubsection{*The Operator @{term is_Replace}*} 

359 

360 
text{*BEWARE! The formula @{term is_P} has free variables 0, 1 

361 
and not the usual 1, 0! It is enclosed within two quantifiers.*} 

362 

363 
(* is_Replace :: "[i=>o,i,[i,i]=>o,i] => o" 

46823  364 
"is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z \<longleftrightarrow> (\<exists>x[M]. x\<in>A & P(x,u))" *) 
13505  365 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

366 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

367 
Replace_fm :: "[i, i, i]=>i" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

368 
"Replace_fm(A,is_P,z) == 
13505  369 
Forall(Iff(Member(0,succ(z)), 
370 
Exists(And(Member(0,A#+2), is_P))))" 

371 

372 
lemma is_Replace_type [TC]: 

373 
"[ is_P \<in> formula; x \<in> nat; y \<in> nat ] 

374 
==> Replace_fm(x,is_P,y) \<in> formula" 

375 
by (simp add: Replace_fm_def) 

376 

377 
lemma sats_Replace_fm: 

378 
assumes is_P_iff_sats: 

379 
"!!a b. [a \<in> A; b \<in> A] 

46823  380 
==> is_P(a,b) \<longleftrightarrow> sats(A, p, Cons(a,Cons(b,env)))" 
13505  381 
shows 
382 
"[x \<in> nat; y \<in> nat; env \<in> list(A)] 

46823  383 
==> sats(A, Replace_fm(x,p,y), env) \<longleftrightarrow> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

384 
is_Replace(##A, nth(x,env), is_P, nth(y,env))" 
13505  385 
by (simp add: Replace_fm_def is_Replace_def is_P_iff_sats [THEN iff_sym]) 
386 

387 
lemma Replace_iff_sats: 

388 
assumes is_P_iff_sats: 

389 
"!!a b. [a \<in> A; b \<in> A] 

46823  390 
==> is_P(a,b) \<longleftrightarrow> sats(A, p, Cons(a,Cons(b,env)))" 
13505  391 
shows 
392 
"[ nth(i,env) = x; nth(j,env) = y; 

393 
i \<in> nat; j \<in> nat; env \<in> list(A)] 

46823  394 
==> is_Replace(##A, x, is_P, y) \<longleftrightarrow> sats(A, Replace_fm(i,p,j), env)" 
13505  395 
by (simp add: sats_Replace_fm [OF is_P_iff_sats]) 
396 

397 

398 
text{*The second argument of @{term is_P} gives it direct access to @{term x}, 

399 
which is essential for handling free variable references.*} 

400 
theorem Replace_reflection: 

401 
assumes is_P_reflection: 

402 
"!!h f g. REFLECTS[\<lambda>x. is_P(L, f(x), g(x), h(x)), 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

403 
\<lambda>i x. is_P(##Lset(i), f(x), g(x), h(x))]" 
13505  404 
shows "REFLECTS[\<lambda>x. is_Replace(L, f(x), is_P(L,x), g(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

405 
\<lambda>i x. is_Replace(##Lset(i), f(x), is_P(##Lset(i), x), g(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13634
diff
changeset

406 
apply (simp (no_asm_use) only: is_Replace_def) 
13505  407 
apply (intro FOL_reflections is_P_reflection) 
408 
done 

409 

410 

411 

412 
subsubsection{*The Operator @{term is_DPow'}, Internalized*} 

413 

414 
(* "is_DPow'(M,A,Z) == 

46823  415 
\<forall>X[M]. X \<in> Z \<longleftrightarrow> 
13505  416 
subset(M,X,A) & 
417 
(\<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) & 

13692  418 
is_Collect(M, A, is_DPow_sats(M,A,env,p), X))" *) 
13505  419 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

420 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

421 
DPow'_fm :: "[i,i]=>i" where 
13505  422 
"DPow'_fm(A,Z) == 
423 
Forall( 

424 
Iff(Member(0,succ(Z)), 

425 
And(subset_fm(0,succ(A)), 

426 
Exists(Exists( 

427 
And(mem_formula_fm(0), 

428 
And(mem_list_fm(A#+3,1), 

429 
Collect_fm(A#+3, 

13692  430 
DPow_sats_fm(A#+4, 2, 1, 0), 2))))))))" 
13505  431 

432 
lemma is_DPow'_type [TC]: 

433 
"[ x \<in> nat; y \<in> nat ] ==> DPow'_fm(x,y) \<in> formula" 

434 
by (simp add: DPow'_fm_def) 

435 

436 
lemma sats_DPow'_fm [simp]: 

437 
"[ x \<in> nat; y \<in> nat; env \<in> list(A)] 

46823  438 
==> sats(A, DPow'_fm(x,y), env) \<longleftrightarrow> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

439 
is_DPow'(##A, nth(x,env), nth(y,env))" 
13505  440 
by (simp add: DPow'_fm_def is_DPow'_def sats_subset_fm' sats_Collect_fm) 
441 

442 
lemma DPow'_iff_sats: 

443 
"[ nth(i,env) = x; nth(j,env) = y; 

444 
i \<in> nat; j \<in> nat; env \<in> list(A)] 

46823  445 
==> is_DPow'(##A, x, y) \<longleftrightarrow> sats(A, DPow'_fm(i,j), env)" 
13505  446 
by (simp add: sats_DPow'_fm) 
447 

448 
theorem DPow'_reflection: 

449 
"REFLECTS[\<lambda>x. is_DPow'(L,f(x),g(x)), 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

450 
\<lambda>i x. is_DPow'(##Lset(i),f(x),g(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13634
diff
changeset

451 
apply (simp only: is_DPow'_def) 
13505  452 
apply (intro FOL_reflections function_reflections mem_formula_reflection 
13692  453 
mem_list_reflection Collect_reflection DPow_sats_reflection) 
13505  454 
done 
455 

456 

13687  457 
subsection{*A Locale for Relativizing the Operator @{term Lset}*} 
13505  458 

21233  459 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

460 
transrec_body :: "[i=>o,i,i,i,i] => o" where 
13505  461 
"transrec_body(M,g,x) == 
462 
\<lambda>y z. \<exists>gy[M]. y \<in> x & fun_apply(M,g,y,gy) & is_DPow'(M,gy,z)" 

463 

464 
lemma (in M_DPow) transrec_body_abs: 

465 
"[M(x); M(g); M(z)] 

46823  466 
==> transrec_body(M,g,x,y,z) \<longleftrightarrow> y \<in> x & z = DPow'(g`y)" 
13505  467 
by (simp add: transrec_body_def DPow'_abs transM [of _ x]) 
468 

469 
locale M_Lset = M_DPow + 

470 
assumes strong_rep: 

471 
"[M(x); M(g)] ==> strong_replacement(M, \<lambda>y z. transrec_body(M,g,x,y,z))" 

472 
and transrec_rep: 

473 
"M(i) ==> transrec_replacement(M, \<lambda>x f u. 

474 
\<exists>r[M]. is_Replace(M, x, transrec_body(M,f,x), r) & 

475 
big_union(M, r, u), i)" 

476 

477 

478 
lemma (in M_Lset) strong_rep': 

479 
"[M(x); M(g)] 

480 
==> strong_replacement(M, \<lambda>y z. y \<in> x & z = DPow'(g`y))" 

481 
by (insert strong_rep [of x g], simp add: transrec_body_abs) 

482 

483 
lemma (in M_Lset) DPow_apply_closed: 

484 
"[M(f); M(x); y\<in>x] ==> M(DPow'(f`y))" 

485 
by (blast intro: DPow'_closed dest: transM) 

486 

487 
lemma (in M_Lset) RepFun_DPow_apply_closed: 

488 
"[M(f); M(x)] ==> M({DPow'(f`y). y\<in>x})" 

489 
by (blast intro: DPow_apply_closed RepFun_closed2 strong_rep') 

490 

491 
lemma (in M_Lset) RepFun_DPow_abs: 

492 
"[M(x); M(f); M(r) ] 

46823  493 
==> is_Replace(M, x, \<lambda>y z. transrec_body(M,f,x,y,z), r) \<longleftrightarrow> 
13505  494 
r = {DPow'(f`y). y\<in>x}" 
495 
apply (simp add: transrec_body_abs RepFun_def) 

496 
apply (rule iff_trans) 

497 
apply (rule Replace_abs) 

498 
apply (simp_all add: DPow_apply_closed strong_rep') 

499 
done 

500 

501 
lemma (in M_Lset) transrec_rep': 

502 
"M(i) ==> transrec_replacement(M, \<lambda>x f u. u = (\<Union>y\<in>x. DPow'(f ` y)), i)" 

503 
apply (insert transrec_rep [of i]) 

504 
apply (simp add: RepFun_DPow_apply_closed RepFun_DPow_abs 

505 
transrec_replacement_def) 

506 
done 

507 

508 

13687  509 
text{*Relativization of the Operator @{term Lset}*} 
13692  510 

21233  511 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

512 
is_Lset :: "[i=>o, i, i] => o" where 
13692  513 
{*We can use the term language below because @{term is_Lset} will 
514 
not have to be internalized: it isn't used in any instance of 

515 
separation.*} 

13505  516 
"is_Lset(M,a,z) == is_transrec(M, %x f u. u = (\<Union>y\<in>x. DPow'(f`y)), a, z)" 
517 

518 
lemma (in M_Lset) Lset_abs: 

519 
"[Ord(i); M(i); M(z)] 

46823  520 
==> is_Lset(M,i,z) \<longleftrightarrow> z = Lset(i)" 
13505  521 
apply (simp add: is_Lset_def Lset_eq_transrec_DPow') 
522 
apply (rule transrec_abs) 

13634  523 
apply (simp_all add: transrec_rep' relation2_def RepFun_DPow_apply_closed) 
13505  524 
done 
525 

526 
lemma (in M_Lset) Lset_closed: 

527 
"[Ord(i); M(i)] ==> M(Lset(i))" 

528 
apply (simp add: Lset_eq_transrec_DPow') 

529 
apply (rule transrec_closed [OF transrec_rep']) 

13634  530 
apply (simp_all add: relation2_def RepFun_DPow_apply_closed) 
13505  531 
done 
532 

533 

534 
subsection{*Instantiating the Locale @{text M_Lset}*} 

535 

536 
subsubsection{*The First Instance of Replacement*} 

537 

538 
lemma strong_rep_Reflects: 

539 
"REFLECTS [\<lambda>u. \<exists>v[L]. v \<in> B & (\<exists>gy[L]. 

540 
v \<in> x & fun_apply(L,g,v,gy) & is_DPow'(L,gy,u)), 

541 
\<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B & (\<exists>gy \<in> Lset(i). 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

542 
v \<in> x & fun_apply(##Lset(i),g,v,gy) & is_DPow'(##Lset(i),gy,u))]" 
13505  543 
by (intro FOL_reflections function_reflections DPow'_reflection) 
544 

545 
lemma strong_rep: 

546 
"[L(x); L(g)] ==> strong_replacement(L, \<lambda>y z. transrec_body(L,g,x,y,z))" 

547 
apply (unfold transrec_body_def) 

548 
apply (rule strong_replacementI) 

13687  549 
apply (rule_tac u="{x,g,B}" 
550 
in gen_separation_multi [OF strong_rep_Reflects], auto) 

551 
apply (rule_tac env="[x,g,B]" in DPow_LsetI) 

13505  552 
apply (rule sep_rules DPow'_iff_sats  simp)+ 
553 
done 

554 

555 

556 
subsubsection{*The Second Instance of Replacement*} 

557 

558 
lemma transrec_rep_Reflects: 

559 
"REFLECTS [\<lambda>x. \<exists>v[L]. v \<in> B & 

560 
(\<exists>y[L]. pair(L,v,y,x) & 

561 
is_wfrec (L, \<lambda>x f u. \<exists>r[L]. 

562 
is_Replace (L, x, \<lambda>y z. 

563 
\<exists>gy[L]. y \<in> x & fun_apply(L,f,y,gy) & 

564 
is_DPow'(L,gy,z), r) & big_union(L,r,u), mr, v, y)), 

565 
\<lambda>i x. \<exists>v \<in> Lset(i). v \<in> B & 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

566 
(\<exists>y \<in> Lset(i). pair(##Lset(i),v,y,x) & 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

567 
is_wfrec (##Lset(i), \<lambda>x f u. \<exists>r \<in> Lset(i). 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

568 
is_Replace (##Lset(i), x, \<lambda>y z. 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

569 
\<exists>gy \<in> Lset(i). y \<in> x & fun_apply(##Lset(i),f,y,gy) & 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

570 
is_DPow'(##Lset(i),gy,z), r) & 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

571 
big_union(##Lset(i),r,u), mr, v, y))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13634
diff
changeset

572 
apply (simp only: rex_setclass_is_bex [symmetric]) 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13692
diff
changeset

573 
{*Convert @{text "\<exists>y\<in>Lset(i)"} to @{text "\<exists>y[##Lset(i)]"} within the body 
13505  574 
of the @{term is_wfrec} application. *} 
575 
apply (intro FOL_reflections function_reflections 

576 
is_wfrec_reflection Replace_reflection DPow'_reflection) 

577 
done 

578 

579 

580 
lemma transrec_rep: 

581 
"[L(j)] 

582 
==> transrec_replacement(L, \<lambda>x f u. 

583 
\<exists>r[L]. is_Replace(L, x, transrec_body(L,f,x), r) & 

584 
big_union(L, r, u), j)" 

585 
apply (rule transrec_replacementI, assumption) 

13566  586 
apply (unfold transrec_body_def) 
13505  587 
apply (rule strong_replacementI) 
13566  588 
apply (rule_tac u="{j,B,Memrel(eclose({j}))}" 
13687  589 
in gen_separation_multi [OF transrec_rep_Reflects], auto) 
590 
apply (rule_tac env="[j,B,Memrel(eclose({j}))]" in DPow_LsetI) 

13505  591 
apply (rule sep_rules is_wfrec_iff_sats Replace_iff_sats DPow'_iff_sats  
592 
simp)+ 

593 
done 

594 

595 

596 
subsubsection{*Actually Instantiating @{text M_Lset}*} 

597 

598 
lemma M_Lset_axioms_L: "M_Lset_axioms(L)" 

599 
apply (rule M_Lset_axioms.intro) 

600 
apply (assumption  rule strong_rep transrec_rep)+ 

601 
done 

602 

603 
theorem M_Lset_L: "PROP M_Lset(L)" 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset

604 
apply (rule M_Lset.intro) 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset

605 
apply (rule M_DPow_L) 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset

606 
apply (rule M_Lset_axioms_L) 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset

607 
done 
13505  608 

609 
text{*Finally: the point of the whole theory!*} 

610 
lemmas Lset_closed = M_Lset.Lset_closed [OF M_Lset_L] 

611 
and Lset_abs = M_Lset.Lset_abs [OF M_Lset_L] 

612 

613 

614 
subsection{*The Notion of Constructible Set*} 

615 

21233  616 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

617 
constructible :: "[i=>o,i] => o" where 
13505  618 
"constructible(M,x) == 
619 
\<exists>i[M]. \<exists>Li[M]. ordinal(M,i) & is_Lset(M,i,Li) & x \<in> Li" 

620 

621 
theorem V_equals_L_in_L: 

47072  622 
"L(x) \<longleftrightarrow> constructible(L,x)" 
623 
apply (simp add: constructible_def Lset_abs Lset_closed) 

13505  624 
apply (simp add: L_def) 
625 
apply (blast intro: Ord_in_L) 

626 
done 

627 

13503  628 
end 