author | blanchet |
Wed, 27 Aug 2014 08:41:12 +0200 | |
changeset 58043 | a90847f03ec8 |
parent 47072 | 777549486d44 |
child 58871 | c399ae4b836f |
permissions | -rw-r--r-- |
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 |