13306
|
1 |
header{*Proving instances of Separation using Reflection!*}
|
|
2 |
|
|
3 |
theory Separation = L_axioms:
|
|
4 |
|
|
5 |
text{*Helps us solve for de Bruijn indices!*}
|
|
6 |
lemma nth_ConsI: "[|nth(n,l) = x; n \<in> nat|] ==> nth(succ(n), Cons(a,l)) = x"
|
|
7 |
by simp
|
|
8 |
|
13316
|
9 |
lemmas nth_rules = nth_0 nth_ConsI nat_0I nat_succI
|
|
10 |
lemmas sep_rules = nth_0 nth_ConsI FOL_iff_sats fun_plus_iff_sats
|
13306
|
11 |
|
|
12 |
lemma Collect_conj_in_DPow:
|
|
13 |
"[| {x\<in>A. P(x)} \<in> DPow(A); {x\<in>A. Q(x)} \<in> DPow(A) |]
|
|
14 |
==> {x\<in>A. P(x) & Q(x)} \<in> DPow(A)"
|
|
15 |
by (simp add: Int_in_DPow Collect_Int_Collect_eq [symmetric])
|
|
16 |
|
|
17 |
lemma Collect_conj_in_DPow_Lset:
|
|
18 |
"[|z \<in> Lset(j); {x \<in> Lset(j). P(x)} \<in> DPow(Lset(j))|]
|
|
19 |
==> {x \<in> Lset(j). x \<in> z & P(x)} \<in> DPow(Lset(j))"
|
|
20 |
apply (frule mem_Lset_imp_subset_Lset)
|
|
21 |
apply (simp add: Collect_conj_in_DPow Collect_mem_eq
|
|
22 |
subset_Int_iff2 elem_subset_in_DPow)
|
|
23 |
done
|
|
24 |
|
|
25 |
lemma separation_CollectI:
|
|
26 |
"(\<And>z. L(z) ==> L({x \<in> z . P(x)})) ==> separation(L, \<lambda>x. P(x))"
|
|
27 |
apply (unfold separation_def, clarify)
|
|
28 |
apply (rule_tac x="{x\<in>z. P(x)}" in rexI)
|
|
29 |
apply simp_all
|
|
30 |
done
|
|
31 |
|
|
32 |
text{*Reduces the original comprehension to the reflected one*}
|
|
33 |
lemma reflection_imp_L_separation:
|
|
34 |
"[| \<forall>x\<in>Lset(j). P(x) <-> Q(x);
|
|
35 |
{x \<in> Lset(j) . Q(x)} \<in> DPow(Lset(j));
|
|
36 |
Ord(j); z \<in> Lset(j)|] ==> L({x \<in> z . P(x)})"
|
|
37 |
apply (rule_tac i = "succ(j)" in L_I)
|
|
38 |
prefer 2 apply simp
|
|
39 |
apply (subgoal_tac "{x \<in> z. P(x)} = {x \<in> Lset(j). x \<in> z & (Q(x))}")
|
|
40 |
prefer 2
|
|
41 |
apply (blast dest: mem_Lset_imp_subset_Lset)
|
|
42 |
apply (simp add: Lset_succ Collect_conj_in_DPow_Lset)
|
|
43 |
done
|
|
44 |
|
|
45 |
|
13316
|
46 |
subsection{*Separation for Intersection*}
|
13306
|
47 |
|
|
48 |
lemma Inter_Reflects:
|
13314
|
49 |
"REFLECTS[\<lambda>x. \<forall>y[L]. y\<in>A --> x \<in> y,
|
|
50 |
\<lambda>i x. \<forall>y\<in>Lset(i). y\<in>A --> x \<in> y]"
|
|
51 |
by (intro FOL_reflection)
|
13306
|
52 |
|
|
53 |
lemma Inter_separation:
|
|
54 |
"L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A --> x\<in>y)"
|
|
55 |
apply (rule separation_CollectI)
|
|
56 |
apply (rule_tac A="{A,z}" in subset_LsetE, blast )
|
|
57 |
apply (rule ReflectsE [OF Inter_Reflects], assumption)
|
|
58 |
apply (drule subset_Lset_ltD, assumption)
|
|
59 |
apply (erule reflection_imp_L_separation)
|
|
60 |
apply (simp_all add: lt_Ord2, clarify)
|
|
61 |
apply (rule DPowI2)
|
|
62 |
apply (rule ball_iff_sats)
|
|
63 |
apply (rule imp_iff_sats)
|
|
64 |
apply (rule_tac [2] i=1 and j=0 and env="[y,x,A]" in mem_iff_sats)
|
|
65 |
apply (rule_tac i=0 and j=2 in mem_iff_sats)
|
|
66 |
apply (simp_all add: succ_Un_distrib [symmetric])
|
|
67 |
done
|
|
68 |
|
13316
|
69 |
subsection{*Separation for Cartesian Product*}
|
13306
|
70 |
|
|
71 |
lemma cartprod_Reflects [simplified]:
|
13314
|
72 |
"REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)),
|
13306
|
73 |
\<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). y\<in>B &
|
13314
|
74 |
pair(**Lset(i),x,y,z))]"
|
|
75 |
by (intro FOL_reflection function_reflection)
|
13306
|
76 |
|
|
77 |
lemma cartprod_separation:
|
|
78 |
"[| L(A); L(B) |]
|
|
79 |
==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)))"
|
|
80 |
apply (rule separation_CollectI)
|
|
81 |
apply (rule_tac A="{A,B,z}" in subset_LsetE, blast )
|
|
82 |
apply (rule ReflectsE [OF cartprod_Reflects], assumption)
|
|
83 |
apply (drule subset_Lset_ltD, assumption)
|
|
84 |
apply (erule reflection_imp_L_separation)
|
|
85 |
apply (simp_all add: lt_Ord2, clarify)
|
|
86 |
apply (rule DPowI2)
|
|
87 |
apply (rename_tac u)
|
|
88 |
apply (rule bex_iff_sats)
|
|
89 |
apply (rule conj_iff_sats)
|
|
90 |
apply (rule_tac i=0 and j=2 and env="[x,u,A,B]" in mem_iff_sats, simp_all)
|
13316
|
91 |
apply (rule sep_rules | simp)+
|
13306
|
92 |
apply (simp_all add: succ_Un_distrib [symmetric])
|
|
93 |
done
|
|
94 |
|
13316
|
95 |
subsection{*Separation for Image*}
|
13306
|
96 |
|
|
97 |
text{*No @{text simplified} here: it simplifies the occurrence of
|
|
98 |
the predicate @{term pair}!*}
|
|
99 |
lemma image_Reflects:
|
13314
|
100 |
"REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)),
|
|
101 |
\<lambda>i y. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). x\<in>A & pair(**Lset(i),x,y,p))]"
|
|
102 |
by (intro FOL_reflection function_reflection)
|
13306
|
103 |
|
|
104 |
|
|
105 |
lemma image_separation:
|
|
106 |
"[| L(A); L(r) |]
|
|
107 |
==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)))"
|
|
108 |
apply (rule separation_CollectI)
|
|
109 |
apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
|
|
110 |
apply (rule ReflectsE [OF image_Reflects], assumption)
|
|
111 |
apply (drule subset_Lset_ltD, assumption)
|
|
112 |
apply (erule reflection_imp_L_separation)
|
|
113 |
apply (simp_all add: lt_Ord2, clarify)
|
|
114 |
apply (rule DPowI2)
|
|
115 |
apply (rule bex_iff_sats)
|
|
116 |
apply (rule conj_iff_sats)
|
|
117 |
apply (rule_tac env="[p,y,A,r]" in mem_iff_sats)
|
13316
|
118 |
apply (rule sep_rules | simp)+
|
13306
|
119 |
apply (simp_all add: succ_Un_distrib [symmetric])
|
|
120 |
done
|
|
121 |
|
|
122 |
|
13316
|
123 |
subsection{*Separation for Converse*}
|
13306
|
124 |
|
|
125 |
lemma converse_Reflects:
|
13314
|
126 |
"REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)),
|
13306
|
127 |
\<lambda>i z. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i).
|
13314
|
128 |
pair(**Lset(i),x,y,p) & pair(**Lset(i),y,x,z))]"
|
|
129 |
by (intro FOL_reflection function_reflection)
|
13306
|
130 |
|
|
131 |
lemma converse_separation:
|
|
132 |
"L(r) ==> separation(L,
|
|
133 |
\<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)))"
|
|
134 |
apply (rule separation_CollectI)
|
|
135 |
apply (rule_tac A="{r,z}" in subset_LsetE, blast )
|
|
136 |
apply (rule ReflectsE [OF converse_Reflects], assumption)
|
|
137 |
apply (drule subset_Lset_ltD, assumption)
|
|
138 |
apply (erule reflection_imp_L_separation)
|
|
139 |
apply (simp_all add: lt_Ord2, clarify)
|
|
140 |
apply (rule DPowI2)
|
|
141 |
apply (rename_tac u)
|
|
142 |
apply (rule bex_iff_sats)
|
|
143 |
apply (rule conj_iff_sats)
|
|
144 |
apply (rule_tac i=0 and j="2" and env="[p,u,r]" in mem_iff_sats, simp_all)
|
13316
|
145 |
apply (rule sep_rules | simp)+
|
13306
|
146 |
apply (simp_all add: succ_Un_distrib [symmetric])
|
|
147 |
done
|
|
148 |
|
|
149 |
|
13316
|
150 |
subsection{*Separation for Restriction*}
|
13306
|
151 |
|
|
152 |
lemma restrict_Reflects:
|
13314
|
153 |
"REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)),
|
|
154 |
\<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). pair(**Lset(i),x,y,z))]"
|
|
155 |
by (intro FOL_reflection function_reflection)
|
13306
|
156 |
|
|
157 |
lemma restrict_separation:
|
|
158 |
"L(A) ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)))"
|
|
159 |
apply (rule separation_CollectI)
|
|
160 |
apply (rule_tac A="{A,z}" in subset_LsetE, blast )
|
|
161 |
apply (rule ReflectsE [OF restrict_Reflects], assumption)
|
|
162 |
apply (drule subset_Lset_ltD, assumption)
|
|
163 |
apply (erule reflection_imp_L_separation)
|
|
164 |
apply (simp_all add: lt_Ord2, clarify)
|
|
165 |
apply (rule DPowI2)
|
|
166 |
apply (rename_tac u)
|
|
167 |
apply (rule bex_iff_sats)
|
|
168 |
apply (rule conj_iff_sats)
|
|
169 |
apply (rule_tac i=0 and j="2" and env="[x,u,A]" in mem_iff_sats, simp_all)
|
13316
|
170 |
apply (rule sep_rules | simp)+
|
13306
|
171 |
apply (simp_all add: succ_Un_distrib [symmetric])
|
|
172 |
done
|
|
173 |
|
|
174 |
|
13316
|
175 |
subsection{*Separation for Composition*}
|
13306
|
176 |
|
|
177 |
lemma comp_Reflects:
|
13314
|
178 |
"REFLECTS[\<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L].
|
13306
|
179 |
pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
|
|
180 |
xy\<in>s & yz\<in>r,
|
|
181 |
\<lambda>i xz. \<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). \<exists>z\<in>Lset(i). \<exists>xy\<in>Lset(i). \<exists>yz\<in>Lset(i).
|
|
182 |
pair(**Lset(i),x,z,xz) & pair(**Lset(i),x,y,xy) &
|
13314
|
183 |
pair(**Lset(i),y,z,yz) & xy\<in>s & yz\<in>r]"
|
|
184 |
by (intro FOL_reflection function_reflection)
|
13306
|
185 |
|
|
186 |
lemma comp_separation:
|
|
187 |
"[| L(r); L(s) |]
|
|
188 |
==> separation(L, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L].
|
|
189 |
pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
|
|
190 |
xy\<in>s & yz\<in>r)"
|
|
191 |
apply (rule separation_CollectI)
|
|
192 |
apply (rule_tac A="{r,s,z}" in subset_LsetE, blast )
|
|
193 |
apply (rule ReflectsE [OF comp_Reflects], assumption)
|
|
194 |
apply (drule subset_Lset_ltD, assumption)
|
|
195 |
apply (erule reflection_imp_L_separation)
|
|
196 |
apply (simp_all add: lt_Ord2, clarify)
|
|
197 |
apply (rule DPowI2)
|
|
198 |
apply (rename_tac u)
|
|
199 |
apply (rule bex_iff_sats)+
|
|
200 |
apply (rename_tac x y z)
|
|
201 |
apply (rule conj_iff_sats)
|
|
202 |
apply (rule_tac env="[z,y,x,u,r,s]" in pair_iff_sats)
|
13316
|
203 |
apply (rule sep_rules | simp)+
|
13306
|
204 |
apply (simp_all add: succ_Un_distrib [symmetric])
|
|
205 |
done
|
|
206 |
|
13316
|
207 |
subsection{*Separation for Predecessors in an Order*}
|
13306
|
208 |
|
|
209 |
lemma pred_Reflects:
|
13314
|
210 |
"REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p),
|
|
211 |
\<lambda>i y. \<exists>p \<in> Lset(i). p\<in>r & pair(**Lset(i),y,x,p)]"
|
|
212 |
by (intro FOL_reflection function_reflection)
|
13306
|
213 |
|
|
214 |
lemma pred_separation:
|
|
215 |
"[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p))"
|
|
216 |
apply (rule separation_CollectI)
|
|
217 |
apply (rule_tac A="{r,x,z}" in subset_LsetE, blast )
|
|
218 |
apply (rule ReflectsE [OF pred_Reflects], assumption)
|
|
219 |
apply (drule subset_Lset_ltD, assumption)
|
|
220 |
apply (erule reflection_imp_L_separation)
|
|
221 |
apply (simp_all add: lt_Ord2, clarify)
|
|
222 |
apply (rule DPowI2)
|
|
223 |
apply (rename_tac u)
|
|
224 |
apply (rule bex_iff_sats)
|
|
225 |
apply (rule conj_iff_sats)
|
|
226 |
apply (rule_tac env = "[p,u,r,x]" in mem_iff_sats)
|
13316
|
227 |
apply (rule sep_rules | simp)+
|
13306
|
228 |
apply (simp_all add: succ_Un_distrib [symmetric])
|
|
229 |
done
|
|
230 |
|
|
231 |
|
13316
|
232 |
subsection{*Separation for the Membership Relation*}
|
13306
|
233 |
|
|
234 |
lemma Memrel_Reflects:
|
13314
|
235 |
"REFLECTS[\<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y,
|
|
236 |
\<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(**Lset(i),x,y,z) & x \<in> y]"
|
|
237 |
by (intro FOL_reflection function_reflection)
|
13306
|
238 |
|
|
239 |
lemma Memrel_separation:
|
|
240 |
"separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)"
|
|
241 |
apply (rule separation_CollectI)
|
|
242 |
apply (rule_tac A="{z}" in subset_LsetE, blast )
|
|
243 |
apply (rule ReflectsE [OF Memrel_Reflects], assumption)
|
|
244 |
apply (drule subset_Lset_ltD, assumption)
|
|
245 |
apply (erule reflection_imp_L_separation)
|
|
246 |
apply (simp_all add: lt_Ord2)
|
|
247 |
apply (rule DPowI2)
|
|
248 |
apply (rename_tac u)
|
13316
|
249 |
apply (rule bex_iff_sats conj_iff_sats)+
|
13306
|
250 |
apply (rule_tac env = "[y,x,u]" in pair_iff_sats)
|
13316
|
251 |
apply (rule sep_rules | simp)+
|
13306
|
252 |
apply (simp_all add: succ_Un_distrib [symmetric])
|
|
253 |
done
|
|
254 |
|
|
255 |
|
13316
|
256 |
subsection{*Replacement for FunSpace*}
|
13306
|
257 |
|
|
258 |
lemma funspace_succ_Reflects:
|
13314
|
259 |
"REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>A & (\<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L].
|
13306
|
260 |
pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) &
|
|
261 |
upair(L,cnbf,cnbf,z)),
|
|
262 |
\<lambda>i z. \<exists>p \<in> Lset(i). p\<in>A & (\<exists>f \<in> Lset(i). \<exists>b \<in> Lset(i).
|
|
263 |
\<exists>nb \<in> Lset(i). \<exists>cnbf \<in> Lset(i).
|
|
264 |
pair(**Lset(i),f,b,p) & pair(**Lset(i),n,b,nb) &
|
13314
|
265 |
is_cons(**Lset(i),nb,f,cnbf) & upair(**Lset(i),cnbf,cnbf,z))]"
|
|
266 |
by (intro FOL_reflection function_reflection)
|
13306
|
267 |
|
|
268 |
lemma funspace_succ_replacement:
|
|
269 |
"L(n) ==>
|
|
270 |
strong_replacement(L, \<lambda>p z. \<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L].
|
|
271 |
pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) &
|
|
272 |
upair(L,cnbf,cnbf,z))"
|
|
273 |
apply (rule strong_replacementI)
|
|
274 |
apply (rule rallI)
|
|
275 |
apply (rule separation_CollectI)
|
|
276 |
apply (rule_tac A="{n,A,z}" in subset_LsetE, blast )
|
|
277 |
apply (rule ReflectsE [OF funspace_succ_Reflects], assumption)
|
|
278 |
apply (drule subset_Lset_ltD, assumption)
|
|
279 |
apply (erule reflection_imp_L_separation)
|
|
280 |
apply (simp_all add: lt_Ord2)
|
|
281 |
apply (rule DPowI2)
|
|
282 |
apply (rename_tac u)
|
|
283 |
apply (rule bex_iff_sats)
|
|
284 |
apply (rule conj_iff_sats)
|
|
285 |
apply (rule_tac env = "[x,u,n,A]" in mem_iff_sats)
|
13316
|
286 |
apply (rule sep_rules | simp)+
|
13306
|
287 |
apply (simp_all add: succ_Un_distrib [symmetric])
|
|
288 |
done
|
|
289 |
|
|
290 |
|
13316
|
291 |
subsection{*Separation for Order-Isomorphisms*}
|
13306
|
292 |
|
|
293 |
lemma well_ord_iso_Reflects:
|
13314
|
294 |
"REFLECTS[\<lambda>x. x\<in>A -->
|
|
295 |
(\<exists>y[L]. \<exists>p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r),
|
|
296 |
\<lambda>i x. x\<in>A --> (\<exists>y \<in> Lset(i). \<exists>p \<in> Lset(i).
|
|
297 |
fun_apply(**Lset(i),f,x,y) & pair(**Lset(i),y,x,p) & p \<in> r)]"
|
|
298 |
by (intro FOL_reflection function_reflection)
|
13306
|
299 |
|
|
300 |
lemma well_ord_iso_separation:
|
|
301 |
"[| L(A); L(f); L(r) |]
|
|
302 |
==> separation (L, \<lambda>x. x\<in>A --> (\<exists>y[L]. (\<exists>p[L].
|
|
303 |
fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r)))"
|
|
304 |
apply (rule separation_CollectI)
|
|
305 |
apply (rule_tac A="{A,f,r,z}" in subset_LsetE, blast )
|
|
306 |
apply (rule ReflectsE [OF well_ord_iso_Reflects], assumption)
|
|
307 |
apply (drule subset_Lset_ltD, assumption)
|
|
308 |
apply (erule reflection_imp_L_separation)
|
|
309 |
apply (simp_all add: lt_Ord2)
|
|
310 |
apply (rule DPowI2)
|
|
311 |
apply (rename_tac u)
|
|
312 |
apply (rule imp_iff_sats)
|
|
313 |
apply (rule_tac env = "[u,A,f,r]" in mem_iff_sats)
|
13316
|
314 |
apply (rule sep_rules | simp)+
|
|
315 |
apply (simp_all add: succ_Un_distrib [symmetric])
|
|
316 |
done
|
|
317 |
|
|
318 |
|
|
319 |
subsection{*Separation for @{term "obase"}*}
|
|
320 |
|
|
321 |
lemma obase_reflects:
|
|
322 |
"REFLECTS[\<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
|
|
323 |
ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
|
|
324 |
order_isomorphism(L,par,r,x,mx,g),
|
|
325 |
\<lambda>i a. \<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). \<exists>par \<in> Lset(i).
|
|
326 |
ordinal(**Lset(i),x) & membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) &
|
|
327 |
order_isomorphism(**Lset(i),par,r,x,mx,g)]"
|
|
328 |
by (intro FOL_reflection function_reflection fun_plus_reflection)
|
|
329 |
|
|
330 |
lemma obase_separation:
|
|
331 |
--{*part of the order type formalization*}
|
|
332 |
"[| L(A); L(r) |]
|
|
333 |
==> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
|
|
334 |
ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
|
|
335 |
order_isomorphism(L,par,r,x,mx,g))"
|
|
336 |
apply (rule separation_CollectI)
|
|
337 |
apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
|
|
338 |
apply (rule ReflectsE [OF obase_reflects], assumption)
|
|
339 |
apply (drule subset_Lset_ltD, assumption)
|
|
340 |
apply (erule reflection_imp_L_separation)
|
|
341 |
apply (simp_all add: lt_Ord2)
|
|
342 |
apply (rule DPowI2)
|
|
343 |
apply (rename_tac u)
|
13306
|
344 |
apply (rule bex_iff_sats)
|
|
345 |
apply (rule conj_iff_sats)
|
13316
|
346 |
apply (rule_tac env = "[x,u,A,r]" in ordinal_iff_sats)
|
|
347 |
apply (rule sep_rules | simp)+
|
|
348 |
apply (simp_all add: succ_Un_distrib [symmetric])
|
|
349 |
done
|
|
350 |
|
|
351 |
|
13319
|
352 |
subsection{*Separation for a Theorem about @{term "obase"}*}
|
13316
|
353 |
|
|
354 |
lemma obase_equals_reflects:
|
|
355 |
"REFLECTS[\<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L].
|
|
356 |
ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L].
|
|
357 |
membership(L,y,my) & pred_set(L,A,x,r,pxr) &
|
|
358 |
order_isomorphism(L,pxr,r,y,my,g))),
|
|
359 |
\<lambda>i x. x\<in>A --> ~(\<exists>y \<in> Lset(i). \<exists>g \<in> Lset(i).
|
|
360 |
ordinal(**Lset(i),y) & (\<exists>my \<in> Lset(i). \<exists>pxr \<in> Lset(i).
|
|
361 |
membership(**Lset(i),y,my) & pred_set(**Lset(i),A,x,r,pxr) &
|
|
362 |
order_isomorphism(**Lset(i),pxr,r,y,my,g)))]"
|
|
363 |
by (intro FOL_reflection function_reflection fun_plus_reflection)
|
|
364 |
|
|
365 |
|
|
366 |
lemma obase_equals_separation:
|
|
367 |
"[| L(A); L(r) |]
|
|
368 |
==> separation (L, \<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L].
|
|
369 |
ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L].
|
|
370 |
membership(L,y,my) & pred_set(L,A,x,r,pxr) &
|
|
371 |
order_isomorphism(L,pxr,r,y,my,g))))"
|
|
372 |
apply (rule separation_CollectI)
|
|
373 |
apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
|
|
374 |
apply (rule ReflectsE [OF obase_equals_reflects], assumption)
|
|
375 |
apply (drule subset_Lset_ltD, assumption)
|
|
376 |
apply (erule reflection_imp_L_separation)
|
|
377 |
apply (simp_all add: lt_Ord2)
|
|
378 |
apply (rule DPowI2)
|
|
379 |
apply (rename_tac u)
|
|
380 |
apply (rule imp_iff_sats ball_iff_sats disj_iff_sats not_iff_sats)+
|
|
381 |
apply (rule_tac env = "[u,A,r]" in mem_iff_sats)
|
|
382 |
apply (rule sep_rules | simp)+
|
|
383 |
apply (simp_all add: succ_Un_distrib [symmetric])
|
|
384 |
done
|
|
385 |
|
|
386 |
|
|
387 |
subsection{*Replacement for @{term "omap"}*}
|
|
388 |
|
|
389 |
lemma omap_reflects:
|
|
390 |
"REFLECTS[\<lambda>z. \<exists>a[L]. a\<in>B & (\<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
|
|
391 |
ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) &
|
|
392 |
pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g)),
|
|
393 |
\<lambda>i z. \<exists>a \<in> Lset(i). a\<in>B & (\<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i).
|
|
394 |
\<exists>par \<in> Lset(i).
|
|
395 |
ordinal(**Lset(i),x) & pair(**Lset(i),a,x,z) &
|
|
396 |
membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) &
|
|
397 |
order_isomorphism(**Lset(i),par,r,x,mx,g))]"
|
|
398 |
by (intro FOL_reflection function_reflection fun_plus_reflection)
|
|
399 |
|
|
400 |
lemma omap_replacement:
|
|
401 |
"[| L(A); L(r) |]
|
|
402 |
==> strong_replacement(L,
|
|
403 |
\<lambda>a z. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
|
|
404 |
ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) &
|
|
405 |
pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))"
|
|
406 |
apply (rule strong_replacementI)
|
|
407 |
apply (rule rallI)
|
|
408 |
apply (rename_tac B)
|
|
409 |
apply (rule separation_CollectI)
|
|
410 |
apply (rule_tac A="{A,B,r,z}" in subset_LsetE, blast )
|
|
411 |
apply (rule ReflectsE [OF omap_reflects], assumption)
|
|
412 |
apply (drule subset_Lset_ltD, assumption)
|
|
413 |
apply (erule reflection_imp_L_separation)
|
|
414 |
apply (simp_all add: lt_Ord2)
|
|
415 |
apply (rule DPowI2)
|
|
416 |
apply (rename_tac u)
|
|
417 |
apply (rule bex_iff_sats conj_iff_sats)+
|
|
418 |
apply (rule_tac env = "[x,u,A,B,r]" in mem_iff_sats)
|
|
419 |
apply (rule sep_rules | simp)+
|
13306
|
420 |
apply (simp_all add: succ_Un_distrib [symmetric])
|
|
421 |
done
|
|
422 |
|
|
423 |
end
|