|
1 (* Title: ZF/Constructible/Satisfies_absolute.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 2002 University of Cambridge |
|
5 *) |
|
6 |
|
7 theory Satisfies_absolute = Datatype_absolute + Rec_Separation: |
|
8 |
|
9 |
|
10 subsection{*More Internalizations*} |
|
11 |
|
12 lemma and_reflection: |
|
13 "REFLECTS[\<lambda>x. is_and(L,f(x),g(x),h(x)), |
|
14 \<lambda>i x. is_and(**Lset(i),f(x),g(x),h(x))]" |
|
15 apply (simp only: is_and_def setclass_simps) |
|
16 apply (intro FOL_reflections function_reflections) |
|
17 done |
|
18 |
|
19 lemma not_reflection: |
|
20 "REFLECTS[\<lambda>x. is_not(L,f(x),g(x)), |
|
21 \<lambda>i x. is_not(**Lset(i),f(x),g(x))]" |
|
22 apply (simp only: is_not_def setclass_simps) |
|
23 apply (intro FOL_reflections function_reflections) |
|
24 done |
|
25 |
|
26 subsubsection{*The Operator @{term is_lambda}*} |
|
27 |
|
28 text{*The two arguments of @{term p} are always 1, 0. Remember that |
|
29 @{term p} will be enclosed by three quantifiers.*} |
|
30 |
|
31 (* is_lambda :: "[i=>o, i, [i,i]=>o, i] => o" |
|
32 "is_lambda(M, A, is_b, z) == |
|
33 \<forall>p[M]. p \<in> z <-> |
|
34 (\<exists>u[M]. \<exists>v[M]. u\<in>A & pair(M,u,v,p) & is_b(u,v))" *) |
|
35 constdefs lambda_fm :: "[i, i, i]=>i" |
|
36 "lambda_fm(p,A,z) == |
|
37 Forall(Iff(Member(0,succ(z)), |
|
38 Exists(Exists(And(Member(1,A#+3), |
|
39 And(pair_fm(1,0,2), p))))))" |
|
40 |
|
41 text{*We call @{term p} with arguments x, y by equating them with |
|
42 the corresponding quantified variables with de Bruijn indices 1, 0.*} |
|
43 |
|
44 lemma is_lambda_type [TC]: |
|
45 "[| p \<in> formula; x \<in> nat; y \<in> nat |] |
|
46 ==> lambda_fm(p,x,y) \<in> formula" |
|
47 by (simp add: lambda_fm_def) |
|
48 |
|
49 lemma sats_lambda_fm: |
|
50 assumes is_b_iff_sats: |
|
51 "!!a0 a1 a2. |
|
52 [|a0\<in>A; a1\<in>A; a2\<in>A|] |
|
53 ==> is_b(a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,env))))" |
|
54 shows |
|
55 "[|x \<in> nat; y \<in> nat; env \<in> list(A)|] |
|
56 ==> sats(A, lambda_fm(p,x,y), env) <-> |
|
57 is_lambda(**A, nth(x,env), is_b, nth(y,env))" |
|
58 by (simp add: lambda_fm_def sats_is_recfun_fm is_lambda_def is_b_iff_sats [THEN iff_sym]) |
|
59 |
|
60 |
|
61 lemma is_lambda_iff_sats: |
|
62 assumes is_b_iff_sats: |
|
63 "!!a0 a1 a2. |
|
64 [|a0\<in>A; a1\<in>A; a2\<in>A|] |
|
65 ==> is_b(a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,env))))" |
|
66 shows |
|
67 "[|nth(i,env) = x; nth(j,env) = y; |
|
68 i \<in> nat; j \<in> nat; env \<in> list(A)|] |
|
69 ==> is_lambda(**A, x, is_b, y) <-> sats(A, lambda_fm(p,i,j), env)" |
|
70 by (simp add: sats_lambda_fm [OF is_b_iff_sats]) |
|
71 |
|
72 theorem is_lambda_reflection: |
|
73 assumes is_b_reflection: |
|
74 "!!f' f g h. REFLECTS[\<lambda>x. is_b(L, f'(x), f(x), g(x)), |
|
75 \<lambda>i x. is_b(**Lset(i), f'(x), f(x), g(x))]" |
|
76 shows "REFLECTS[\<lambda>x. is_lambda(L, A(x), is_b(L,x), f(x)), |
|
77 \<lambda>i x. is_lambda(**Lset(i), A(x), is_b(**Lset(i),x), f(x))]" |
|
78 apply (simp (no_asm_use) only: is_lambda_def setclass_simps) |
|
79 apply (intro FOL_reflections is_b_reflection pair_reflection) |
|
80 done |
|
81 |
|
82 |
|
83 subsubsection{*The Operator @{term is_Member}, Internalized*} |
|
84 |
|
85 (* "is_Member(M,x,y,Z) == |
|
86 \<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inl(M,u,Z)" *) |
|
87 constdefs Member_fm :: "[i,i,i]=>i" |
|
88 "Member_fm(x,y,Z) == |
|
89 Exists(Exists(And(pair_fm(x#+2,y#+2,1), |
|
90 And(Inl_fm(1,0), Inl_fm(0,Z#+2)))))" |
|
91 |
|
92 lemma is_Member_type [TC]: |
|
93 "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Member_fm(x,y,z) \<in> formula" |
|
94 by (simp add: Member_fm_def) |
|
95 |
|
96 lemma sats_Member_fm [simp]: |
|
97 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
|
98 ==> sats(A, Member_fm(x,y,z), env) <-> |
|
99 is_Member(**A, nth(x,env), nth(y,env), nth(z,env))" |
|
100 by (simp add: Member_fm_def is_Member_def) |
|
101 |
|
102 lemma Member_iff_sats: |
|
103 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
|
104 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
|
105 ==> is_Member(**A, x, y, z) <-> sats(A, Member_fm(i,j,k), env)" |
|
106 by (simp add: sats_Member_fm) |
|
107 |
|
108 theorem Member_reflection: |
|
109 "REFLECTS[\<lambda>x. is_Member(L,f(x),g(x),h(x)), |
|
110 \<lambda>i x. is_Member(**Lset(i),f(x),g(x),h(x))]" |
|
111 apply (simp only: is_Member_def setclass_simps) |
|
112 apply (intro FOL_reflections pair_reflection Inl_reflection) |
|
113 done |
|
114 |
|
115 subsubsection{*The Operator @{term is_Equal}, Internalized*} |
|
116 |
|
117 (* "is_Equal(M,x,y,Z) == |
|
118 \<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inr(M,p,u) & is_Inl(M,u,Z)" *) |
|
119 constdefs Equal_fm :: "[i,i,i]=>i" |
|
120 "Equal_fm(x,y,Z) == |
|
121 Exists(Exists(And(pair_fm(x#+2,y#+2,1), |
|
122 And(Inr_fm(1,0), Inl_fm(0,Z#+2)))))" |
|
123 |
|
124 lemma is_Equal_type [TC]: |
|
125 "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Equal_fm(x,y,z) \<in> formula" |
|
126 by (simp add: Equal_fm_def) |
|
127 |
|
128 lemma sats_Equal_fm [simp]: |
|
129 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
|
130 ==> sats(A, Equal_fm(x,y,z), env) <-> |
|
131 is_Equal(**A, nth(x,env), nth(y,env), nth(z,env))" |
|
132 by (simp add: Equal_fm_def is_Equal_def) |
|
133 |
|
134 lemma Equal_iff_sats: |
|
135 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
|
136 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
|
137 ==> is_Equal(**A, x, y, z) <-> sats(A, Equal_fm(i,j,k), env)" |
|
138 by (simp add: sats_Equal_fm) |
|
139 |
|
140 theorem Equal_reflection: |
|
141 "REFLECTS[\<lambda>x. is_Equal(L,f(x),g(x),h(x)), |
|
142 \<lambda>i x. is_Equal(**Lset(i),f(x),g(x),h(x))]" |
|
143 apply (simp only: is_Equal_def setclass_simps) |
|
144 apply (intro FOL_reflections pair_reflection Inl_reflection Inr_reflection) |
|
145 done |
|
146 |
|
147 subsubsection{*The Operator @{term is_Nand}, Internalized*} |
|
148 |
|
149 (* "is_Nand(M,x,y,Z) == |
|
150 \<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inr(M,u,Z)" *) |
|
151 constdefs Nand_fm :: "[i,i,i]=>i" |
|
152 "Nand_fm(x,y,Z) == |
|
153 Exists(Exists(And(pair_fm(x#+2,y#+2,1), |
|
154 And(Inl_fm(1,0), Inr_fm(0,Z#+2)))))" |
|
155 |
|
156 lemma is_Nand_type [TC]: |
|
157 "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Nand_fm(x,y,z) \<in> formula" |
|
158 by (simp add: Nand_fm_def) |
|
159 |
|
160 lemma sats_Nand_fm [simp]: |
|
161 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
|
162 ==> sats(A, Nand_fm(x,y,z), env) <-> |
|
163 is_Nand(**A, nth(x,env), nth(y,env), nth(z,env))" |
|
164 by (simp add: Nand_fm_def is_Nand_def) |
|
165 |
|
166 lemma Nand_iff_sats: |
|
167 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
|
168 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
|
169 ==> is_Nand(**A, x, y, z) <-> sats(A, Nand_fm(i,j,k), env)" |
|
170 by (simp add: sats_Nand_fm) |
|
171 |
|
172 theorem Nand_reflection: |
|
173 "REFLECTS[\<lambda>x. is_Nand(L,f(x),g(x),h(x)), |
|
174 \<lambda>i x. is_Nand(**Lset(i),f(x),g(x),h(x))]" |
|
175 apply (simp only: is_Nand_def setclass_simps) |
|
176 apply (intro FOL_reflections pair_reflection Inl_reflection Inr_reflection) |
|
177 done |
|
178 |
|
179 subsubsection{*The Operator @{term is_Forall}, Internalized*} |
|
180 |
|
181 (* "is_Forall(M,p,Z) == \<exists>u[M]. is_Inr(M,p,u) & is_Inr(M,u,Z)" *) |
|
182 constdefs Forall_fm :: "[i,i]=>i" |
|
183 "Forall_fm(x,Z) == |
|
184 Exists(And(Inr_fm(succ(x),0), Inr_fm(0,succ(Z))))" |
|
185 |
|
186 lemma is_Forall_type [TC]: |
|
187 "[| x \<in> nat; y \<in> nat |] ==> Forall_fm(x,y) \<in> formula" |
|
188 by (simp add: Forall_fm_def) |
|
189 |
|
190 lemma sats_Forall_fm [simp]: |
|
191 "[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
|
192 ==> sats(A, Forall_fm(x,y), env) <-> |
|
193 is_Forall(**A, nth(x,env), nth(y,env))" |
|
194 by (simp add: Forall_fm_def is_Forall_def) |
|
195 |
|
196 lemma Forall_iff_sats: |
|
197 "[| nth(i,env) = x; nth(j,env) = y; |
|
198 i \<in> nat; j \<in> nat; env \<in> list(A)|] |
|
199 ==> is_Forall(**A, x, y) <-> sats(A, Forall_fm(i,j), env)" |
|
200 by (simp add: sats_Forall_fm) |
|
201 |
|
202 theorem Forall_reflection: |
|
203 "REFLECTS[\<lambda>x. is_Forall(L,f(x),g(x)), |
|
204 \<lambda>i x. is_Forall(**Lset(i),f(x),g(x))]" |
|
205 apply (simp only: is_Forall_def setclass_simps) |
|
206 apply (intro FOL_reflections pair_reflection Inr_reflection) |
|
207 done |
|
208 |
|
209 |
|
210 subsubsection{*The Formula @{term is_formula_N}, Internalized*} |
|
211 |
|
212 (* "is_nth(M,n,l,Z) == |
|
213 \<exists>X[M]. \<exists>sn[M]. \<exists>msn[M]. |
|
214 2 1 0 |
|
215 successor(M,n,sn) & membership(M,sn,msn) & |
|
216 is_wfrec(M, iterates_MH(M, is_tl(M), l), msn, n, X) & |
|
217 is_hd(M,X,Z)" *) |
|
218 |
|
219 (* "is_formula_N(M,n,Z) == |
|
220 \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M]. |
|
221 2 1 0 |
|
222 empty(M,zero) & |
|
223 successor(M,n,sn) & membership(M,sn,msn) & |
|
224 is_wfrec(M, iterates_MH(M, is_formula_functor(M),zero), msn, n, Z)" *) |
|
225 constdefs formula_N_fm :: "[i,i]=>i" |
|
226 "formula_N_fm(n,Z) == |
|
227 Exists(Exists(Exists( |
|
228 And(empty_fm(2), |
|
229 And(succ_fm(n#+3,1), |
|
230 And(Memrel_fm(1,0), |
|
231 is_wfrec_fm(iterates_MH_fm(formula_functor_fm(1,0),7,2,1,0), |
|
232 0, n#+3, Z#+3)))))))" |
|
233 |
|
234 lemma formula_N_fm_type [TC]: |
|
235 "[| x \<in> nat; y \<in> nat |] ==> formula_N_fm(x,y) \<in> formula" |
|
236 by (simp add: formula_N_fm_def) |
|
237 |
|
238 lemma sats_formula_N_fm [simp]: |
|
239 "[| x < length(env); y < length(env); env \<in> list(A)|] |
|
240 ==> sats(A, formula_N_fm(x,y), env) <-> |
|
241 is_formula_N(**A, nth(x,env), nth(y,env))" |
|
242 apply (frule_tac x=y in lt_length_in_nat, assumption) |
|
243 apply (frule lt_length_in_nat, assumption) |
|
244 apply (simp add: formula_N_fm_def is_formula_N_def sats_is_wfrec_fm sats_iterates_MH_fm) |
|
245 done |
|
246 |
|
247 lemma formula_N_iff_sats: |
|
248 "[| nth(i,env) = x; nth(j,env) = y; |
|
249 i < length(env); j < length(env); env \<in> list(A)|] |
|
250 ==> is_formula_N(**A, x, y) <-> sats(A, formula_N_fm(i,j), env)" |
|
251 by (simp add: sats_formula_N_fm) |
|
252 |
|
253 theorem formula_N_reflection: |
|
254 "REFLECTS[\<lambda>x. is_formula_N(L, f(x), g(x)), |
|
255 \<lambda>i x. is_formula_N(**Lset(i), f(x), g(x))]" |
|
256 apply (simp only: is_formula_N_def setclass_simps) |
|
257 apply (intro FOL_reflections function_reflections is_wfrec_reflection |
|
258 iterates_MH_reflection formula_functor_reflection) |
|
259 done |
|
260 |
|
261 |
|
262 |
|
263 subsubsection{*The Predicate ``Is A Formula''*} |
|
264 |
|
265 (* mem_formula(M,p) == |
|
266 \<exists>n[M]. \<exists>formn[M]. |
|
267 finite_ordinal(M,n) & is_formula_N(M,n,formn) & p \<in> formn *) |
|
268 constdefs mem_formula_fm :: "i=>i" |
|
269 "mem_formula_fm(x) == |
|
270 Exists(Exists( |
|
271 And(finite_ordinal_fm(1), |
|
272 And(formula_N_fm(1,0), Member(x#+2,0)))))" |
|
273 |
|
274 lemma mem_formula_type [TC]: |
|
275 "x \<in> nat ==> mem_formula_fm(x) \<in> formula" |
|
276 by (simp add: mem_formula_fm_def) |
|
277 |
|
278 lemma sats_mem_formula_fm [simp]: |
|
279 "[| x \<in> nat; env \<in> list(A)|] |
|
280 ==> sats(A, mem_formula_fm(x), env) <-> mem_formula(**A, nth(x,env))" |
|
281 by (simp add: mem_formula_fm_def mem_formula_def) |
|
282 |
|
283 lemma mem_formula_iff_sats: |
|
284 "[| nth(i,env) = x; nth(j,env) = y; |
|
285 i \<in> nat; env \<in> list(A)|] |
|
286 ==> mem_formula(**A, x) <-> sats(A, mem_formula_fm(i), env)" |
|
287 by simp |
|
288 |
|
289 theorem mem_formula_reflection: |
|
290 "REFLECTS[\<lambda>x. mem_formula(L,f(x)), |
|
291 \<lambda>i x. mem_formula(**Lset(i),f(x))]" |
|
292 apply (simp only: mem_formula_def setclass_simps) |
|
293 apply (intro FOL_reflections finite_ordinal_reflection formula_N_reflection) |
|
294 done |
|
295 |
|
296 |
|
297 |
|
298 subsubsection{*The Formula @{term is_depth}, Internalized*} |
|
299 |
|
300 (* "is_depth(M,p,n) == |
|
301 \<exists>sn[M]. \<exists>formula_n[M]. \<exists>formula_sn[M]. |
|
302 2 1 0 |
|
303 is_formula_N(M,n,formula_n) & p \<notin> formula_n & |
|
304 successor(M,n,sn) & is_formula_N(M,sn,formula_sn) & p \<in> formula_sn" *) |
|
305 constdefs depth_fm :: "[i,i]=>i" |
|
306 "depth_fm(p,n) == |
|
307 Exists(Exists(Exists( |
|
308 And(formula_N_fm(n#+3,1), |
|
309 And(Neg(Member(p#+3,1)), |
|
310 And(succ_fm(n#+3,2), |
|
311 And(formula_N_fm(2,0), Member(p#+3,0))))))))" |
|
312 |
|
313 lemma depth_fm_type [TC]: |
|
314 "[| x \<in> nat; y \<in> nat |] ==> depth_fm(x,y) \<in> formula" |
|
315 by (simp add: depth_fm_def) |
|
316 |
|
317 lemma sats_depth_fm [simp]: |
|
318 "[| x \<in> nat; y < length(env); env \<in> list(A)|] |
|
319 ==> sats(A, depth_fm(x,y), env) <-> |
|
320 is_depth(**A, nth(x,env), nth(y,env))" |
|
321 apply (frule_tac x=y in lt_length_in_nat, assumption) |
|
322 apply (simp add: depth_fm_def is_depth_def) |
|
323 done |
|
324 |
|
325 lemma depth_iff_sats: |
|
326 "[| nth(i,env) = x; nth(j,env) = y; |
|
327 i \<in> nat; j < length(env); env \<in> list(A)|] |
|
328 ==> is_depth(**A, x, y) <-> sats(A, depth_fm(i,j), env)" |
|
329 by (simp add: sats_depth_fm) |
|
330 |
|
331 theorem depth_reflection: |
|
332 "REFLECTS[\<lambda>x. is_depth(L, f(x), g(x)), |
|
333 \<lambda>i x. is_depth(**Lset(i), f(x), g(x))]" |
|
334 apply (simp only: is_depth_def setclass_simps) |
|
335 apply (intro FOL_reflections function_reflections formula_N_reflection) |
|
336 done |
|
337 |
|
338 |
|
339 |
|
340 subsubsection{*The Operator @{term is_formula_case}*} |
|
341 |
|
342 text{*The arguments of @{term is_a} are always 2, 1, 0, and the formula |
|
343 will be enclosed by three quantifiers.*} |
|
344 |
|
345 (* is_formula_case :: |
|
346 "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o" |
|
347 "is_formula_case(M, is_a, is_b, is_c, is_d, v, z) == |
|
348 (\<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> is_Member(M,x,y,v) --> is_a(x,y,z)) & |
|
349 (\<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> is_Equal(M,x,y,v) --> is_b(x,y,z)) & |
|
350 (\<forall>x[M]. \<forall>y[M]. x\<in>formula --> y\<in>formula --> |
|
351 is_Nand(M,x,y,v) --> is_c(x,y,z)) & |
|
352 (\<forall>x[M]. x\<in>formula --> is_Forall(M,x,v) --> is_d(x,z))" *) |
|
353 |
|
354 constdefs formula_case_fm :: "[i, i, i, i, i, i]=>i" |
|
355 "formula_case_fm(is_a, is_b, is_c, is_d, v, z) == |
|
356 And(Forall(Forall(Implies(finite_ordinal_fm(1), |
|
357 Implies(finite_ordinal_fm(0), |
|
358 Implies(Member_fm(1,0,v#+2), |
|
359 Forall(Implies(Equal(0,z#+3), is_a))))))), |
|
360 And(Forall(Forall(Implies(finite_ordinal_fm(1), |
|
361 Implies(finite_ordinal_fm(0), |
|
362 Implies(Equal_fm(1,0,v#+2), |
|
363 Forall(Implies(Equal(0,z#+3), is_b))))))), |
|
364 And(Forall(Forall(Implies(mem_formula_fm(1), |
|
365 Implies(mem_formula_fm(0), |
|
366 Implies(Nand_fm(1,0,v#+2), |
|
367 Forall(Implies(Equal(0,z#+3), is_c))))))), |
|
368 Forall(Implies(mem_formula_fm(0), |
|
369 Implies(Forall_fm(0,succ(v)), |
|
370 Forall(Implies(Equal(0,z#+2), is_d))))))))" |
|
371 |
|
372 |
|
373 lemma is_formula_case_type [TC]: |
|
374 "[| is_a \<in> formula; is_b \<in> formula; is_c \<in> formula; is_d \<in> formula; |
|
375 x \<in> nat; y \<in> nat |] |
|
376 ==> formula_case_fm(is_a, is_b, is_c, is_d, x, y) \<in> formula" |
|
377 by (simp add: formula_case_fm_def) |
|
378 |
|
379 lemma sats_formula_case_fm: |
|
380 assumes is_a_iff_sats: |
|
381 "!!a0 a1 a2. |
|
382 [|a0\<in>A; a1\<in>A; a2\<in>A|] |
|
383 ==> ISA(a2, a1, a0) <-> sats(A, is_a, Cons(a0,Cons(a1,Cons(a2,env))))" |
|
384 and is_b_iff_sats: |
|
385 "!!a0 a1 a2. |
|
386 [|a0\<in>A; a1\<in>A; a2\<in>A|] |
|
387 ==> ISB(a2, a1, a0) <-> sats(A, is_b, Cons(a0,Cons(a1,Cons(a2,env))))" |
|
388 and is_c_iff_sats: |
|
389 "!!a0 a1 a2. |
|
390 [|a0\<in>A; a1\<in>A; a2\<in>A|] |
|
391 ==> ISC(a2, a1, a0) <-> sats(A, is_c, Cons(a0,Cons(a1,Cons(a2,env))))" |
|
392 and is_d_iff_sats: |
|
393 "!!a0 a1. |
|
394 [|a0\<in>A; a1\<in>A|] |
|
395 ==> ISD(a1, a0) <-> sats(A, is_d, Cons(a0,Cons(a1,env)))" |
|
396 shows |
|
397 "[|x \<in> nat; y < length(env); env \<in> list(A)|] |
|
398 ==> sats(A, formula_case_fm(is_a,is_b,is_c,is_d,x,y), env) <-> |
|
399 is_formula_case(**A, ISA, ISB, ISC, ISD, nth(x,env), nth(y,env))" |
|
400 apply (frule_tac x=y in lt_length_in_nat, assumption) |
|
401 apply (simp add: formula_case_fm_def is_formula_case_def |
|
402 is_a_iff_sats [THEN iff_sym] is_b_iff_sats [THEN iff_sym] |
|
403 is_c_iff_sats [THEN iff_sym] is_d_iff_sats [THEN iff_sym]) |
|
404 done |
|
405 |
|
406 lemma formula_case_iff_sats: |
|
407 assumes is_a_iff_sats: |
|
408 "!!a0 a1 a2. |
|
409 [|a0\<in>A; a1\<in>A; a2\<in>A|] |
|
410 ==> ISA(a2, a1, a0) <-> sats(A, is_a, Cons(a0,Cons(a1,Cons(a2,env))))" |
|
411 and is_b_iff_sats: |
|
412 "!!a0 a1 a2. |
|
413 [|a0\<in>A; a1\<in>A; a2\<in>A|] |
|
414 ==> ISB(a2, a1, a0) <-> sats(A, is_b, Cons(a0,Cons(a1,Cons(a2,env))))" |
|
415 and is_c_iff_sats: |
|
416 "!!a0 a1 a2. |
|
417 [|a0\<in>A; a1\<in>A; a2\<in>A|] |
|
418 ==> ISC(a2, a1, a0) <-> sats(A, is_c, Cons(a0,Cons(a1,Cons(a2,env))))" |
|
419 and is_d_iff_sats: |
|
420 "!!a0 a1. |
|
421 [|a0\<in>A; a1\<in>A|] |
|
422 ==> ISD(a1, a0) <-> sats(A, is_d, Cons(a0,Cons(a1,env)))" |
|
423 shows |
|
424 "[|nth(i,env) = x; nth(j,env) = y; |
|
425 i \<in> nat; j < length(env); env \<in> list(A)|] |
|
426 ==> is_formula_case(**A, ISA, ISB, ISC, ISD, x, y) <-> |
|
427 sats(A, formula_case_fm(is_a,is_b,is_c,is_d,i,j), env)" |
|
428 by (simp add: sats_formula_case_fm [OF is_a_iff_sats is_b_iff_sats |
|
429 is_c_iff_sats is_d_iff_sats]) |
|
430 |
|
431 |
|
432 text{*The second argument of @{term is_a} gives it direct access to @{term x}, |
|
433 which is essential for handling free variable references. Treatment is |
|
434 based on that of @{text is_nat_case_reflection}.*} |
|
435 theorem is_formula_case_reflection: |
|
436 assumes is_a_reflection: |
|
437 "!!h f g g'. REFLECTS[\<lambda>x. is_a(L, h(x), f(x), g(x), g'(x)), |
|
438 \<lambda>i x. is_a(**Lset(i), h(x), f(x), g(x), g'(x))]" |
|
439 and is_b_reflection: |
|
440 "!!h f g g'. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x), g'(x)), |
|
441 \<lambda>i x. is_b(**Lset(i), h(x), f(x), g(x), g'(x))]" |
|
442 and is_c_reflection: |
|
443 "!!h f g g'. REFLECTS[\<lambda>x. is_c(L, h(x), f(x), g(x), g'(x)), |
|
444 \<lambda>i x. is_c(**Lset(i), h(x), f(x), g(x), g'(x))]" |
|
445 and is_d_reflection: |
|
446 "!!h f g g'. REFLECTS[\<lambda>x. is_d(L, h(x), f(x), g(x)), |
|
447 \<lambda>i x. is_d(**Lset(i), h(x), f(x), g(x))]" |
|
448 shows "REFLECTS[\<lambda>x. is_formula_case(L, is_a(L,x), is_b(L,x), is_c(L,x), is_d(L,x), g(x), h(x)), |
|
449 \<lambda>i x. is_formula_case(**Lset(i), is_a(**Lset(i), x), is_b(**Lset(i), x), is_c(**Lset(i), x), is_d(**Lset(i), x), g(x), h(x))]" |
|
450 apply (simp (no_asm_use) only: is_formula_case_def setclass_simps) |
|
451 apply (intro FOL_reflections function_reflections finite_ordinal_reflection |
|
452 mem_formula_reflection |
|
453 Member_reflection Equal_reflection Nand_reflection Forall_reflection |
|
454 is_a_reflection is_b_reflection is_c_reflection is_d_reflection) |
|
455 done |
|
456 |
|
457 |
|
458 |
|
459 subsection {*Absoluteness for @{term formula_rec}*} |
|
460 |
|
461 constdefs |
|
462 |
|
463 formula_rec_case :: "[[i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, i, i] => i" |
|
464 --{* the instance of @{term formula_case} in @{term formula_rec}*} |
|
465 "formula_rec_case(a,b,c,d,h) == |
|
466 formula_case (a, b, |
|
467 \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u, |
|
468 h ` succ(depth(v)) ` v), |
|
469 \<lambda>u. d(u, h ` succ(depth(u)) ` u))" |
|
470 |
|
471 is_formula_rec :: "[i=>o, [i,i,i]=>o, |
|
472 [i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, |
|
473 i, i] => o" |
|
474 --{* predicate to relative the functional @{term formula_rec}*} |
|
475 "is_formula_rec(M,MH,a,b,c,d,p,z) == |
|
476 \<exists>i[M]. \<exists>f[M]. i = succ(depth(p)) & fun_apply(M,f,p,z) & |
|
477 is_transrec(M,MH,i,f)" |
|
478 |
|
479 text{*Unfold @{term formula_rec} to @{term formula_rec_case}*} |
|
480 lemma (in M_triv_axioms) formula_rec_eq2: |
|
481 "p \<in> formula ==> |
|
482 formula_rec(a,b,c,d,p) = |
|
483 transrec (succ(depth(p)), |
|
484 \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h))) ` p" |
|
485 by (simp add: formula_rec_eq formula_rec_case_def) |
|
486 |
|
487 |
|
488 text{*Sufficient conditions to relative the instance of @{term formula_case} |
|
489 in @{term formula_rec}*} |
|
490 lemma (in M_datatypes) Relativize1_formula_rec_case: |
|
491 "[|Relativize2(M, nat, nat, is_a, a); |
|
492 Relativize2(M, nat, nat, is_b, b); |
|
493 Relativize2 (M, formula, formula, |
|
494 is_c, \<lambda>u v. c(u, v, h`succ(depth(u))`u, h`succ(depth(v))`v)); |
|
495 Relativize1(M, formula, |
|
496 is_d, \<lambda>u. d(u, h ` succ(depth(u)) ` u)); |
|
497 M(h) |] |
|
498 ==> Relativize1(M, formula, |
|
499 is_formula_case (M, is_a, is_b, is_c, is_d), |
|
500 formula_rec_case(a, b, c, d, h))" |
|
501 apply (simp (no_asm) add: formula_rec_case_def Relativize1_def) |
|
502 apply (simp add: formula_case_abs) |
|
503 done |
|
504 |
|
505 |
|
506 text{*This locale packages the premises of the following theorems, |
|
507 which is the normal purpose of locales. It doesn't accumulate |
|
508 constraints on the class @{term M}, as in most of this deveopment.*} |
|
509 locale M_formula_rec = M_eclose + |
|
510 fixes a and is_a and b and is_b and c and is_c and d and is_d and MH |
|
511 defines |
|
512 "MH(u::i,f,z) == |
|
513 is_lambda |
|
514 (M, formula, is_formula_case (M, is_a, is_b, is_c(f), is_d(f)), z)" |
|
515 |
|
516 assumes a_closed: "[|x\<in>nat; y\<in>nat|] ==> M(a(x,y))" |
|
517 and a_rel: "Relativize2(M, nat, nat, is_a, a)" |
|
518 and b_closed: "[|x\<in>nat; y\<in>nat|] ==> M(b(x,y))" |
|
519 and b_rel: "Relativize2(M, nat, nat, is_b, b)" |
|
520 and c_closed: "[|x \<in> formula; y \<in> formula; M(gx); M(gy)|] |
|
521 ==> M(c(x, y, gx, gy))" |
|
522 and c_rel: |
|
523 "M(f) ==> |
|
524 Relativize2 (M, formula, formula, is_c(f), |
|
525 \<lambda>u v. c(u, v, f ` succ(depth(u)) ` u, f ` succ(depth(v)) ` v))" |
|
526 and d_closed: "[|x \<in> formula; M(gx)|] ==> M(d(x, gx))" |
|
527 and d_rel: |
|
528 "M(f) ==> |
|
529 Relativize1(M, formula, is_d(f), \<lambda>u. d(u, f ` succ(depth(u)) ` u))" |
|
530 and fr_replace: "n \<in> nat ==> transrec_replacement(M,MH,n)" |
|
531 and fr_lam_replace: |
|
532 "M(g) ==> |
|
533 strong_replacement |
|
534 (M, \<lambda>x y. x \<in> formula & |
|
535 y = \<langle>x, formula_rec_case(a,b,c,d,g,x)\<rangle>)"; |
|
536 |
|
537 lemma (in M_formula_rec) formula_rec_case_closed: |
|
538 "[|M(g); p \<in> formula|] ==> M(formula_rec_case(a, b, c, d, g, p))" |
|
539 by (simp add: formula_rec_case_def a_closed b_closed c_closed d_closed) |
|
540 |
|
541 lemma (in M_formula_rec) formula_rec_lam_closed: |
|
542 "M(g) ==> M(Lambda (formula, formula_rec_case(a,b,c,d,g)))" |
|
543 by (simp add: lam_closed2 fr_lam_replace formula_rec_case_closed) |
|
544 |
|
545 lemma (in M_formula_rec) MH_rel2: |
|
546 "relativize2 (M, MH, |
|
547 \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h)))" |
|
548 apply (simp add: relativize2_def MH_def, clarify) |
|
549 apply (rule lambda_abs2) |
|
550 apply (rule fr_lam_replace, assumption) |
|
551 apply (rule Relativize1_formula_rec_case) |
|
552 apply (simp_all add: a_rel b_rel c_rel d_rel formula_rec_case_closed) |
|
553 done |
|
554 |
|
555 lemma (in M_formula_rec) fr_transrec_closed: |
|
556 "n \<in> nat |
|
557 ==> M(transrec |
|
558 (n, \<lambda>x h. Lambda(formula, formula_rec_case(a, b, c, d, h))))" |
|
559 by (simp add: transrec_closed [OF fr_replace MH_rel2] |
|
560 nat_into_M formula_rec_lam_closed) |
|
561 |
|
562 text{*The main two results: @{term formula_rec} is absolute for @{term M}.*} |
|
563 theorem (in M_formula_rec) formula_rec_closed: |
|
564 "p \<in> formula ==> M(formula_rec(a,b,c,d,p))" |
|
565 by (simp add: formula_rec_eq2 fr_transrec_closed |
|
566 transM [OF _ formula_closed]) |
|
567 |
|
568 theorem (in M_formula_rec) formula_rec_abs: |
|
569 "[| p \<in> formula; M(z)|] |
|
570 ==> is_formula_rec(M,MH,a,b,c,d,p,z) <-> z = formula_rec(a,b,c,d,p)" |
|
571 by (simp add: is_formula_rec_def formula_rec_eq2 transM [OF _ formula_closed] |
|
572 transrec_abs [OF fr_replace MH_rel2] |
|
573 fr_transrec_closed formula_rec_lam_closed eq_commute) |
|
574 |
|
575 |
|
576 subsection {*Absoluteness for the Function @{term satisfies}*} |
|
577 |
|
578 constdefs |
|
579 is_depth_apply :: "[i=>o,i,i,i] => o" |
|
580 --{*Merely a useful abbreviation for the sequel.*} |
|
581 "is_depth_apply(M,h,p,z) == |
|
582 \<exists>dp[M]. \<exists>sdp[M]. \<exists>hsdp[M]. |
|
583 dp \<in> nat & is_depth(M,p,dp) & successor(M,dp,sdp) & |
|
584 fun_apply(M,h,sdp,hsdp) & fun_apply(M,hsdp,p,z)" |
|
585 |
|
586 lemma (in M_datatypes) is_depth_apply_abs [simp]: |
|
587 "[|M(h); p \<in> formula; M(z)|] |
|
588 ==> is_depth_apply(M,h,p,z) <-> z = h ` succ(depth(p)) ` p" |
|
589 by (simp add: is_depth_apply_def formula_into_M depth_type eq_commute) |
|
590 |
|
591 lemma depth_apply_reflection: |
|
592 "REFLECTS[\<lambda>x. is_depth_apply(L,f(x),g(x),h(x)), |
|
593 \<lambda>i x. is_depth_apply(**Lset(i),f(x),g(x),h(x))]" |
|
594 apply (simp only: is_depth_apply_def setclass_simps) |
|
595 apply (intro FOL_reflections function_reflections depth_reflection) |
|
596 done |
|
597 |
|
598 |
|
599 text{*There is at present some redundancy between the relativizations in |
|
600 e.g. @{text satisfies_is_a} and those in e.g. @{text Member_replacement}.*} |
|
601 |
|
602 text{*These constants let us instantiate the parameters @{term a}, @{term b}, |
|
603 @{term c}, @{term d}, etc., of the locale @{text M_formula_rec}.*} |
|
604 constdefs |
|
605 satisfies_a :: "[i,i,i]=>i" |
|
606 "satisfies_a(A) == |
|
607 \<lambda>x y. \<lambda>env \<in> list(A). bool_of_o (nth(x,env) \<in> nth(y,env))" |
|
608 |
|
609 satisfies_is_a :: "[i=>o,i,i,i,i]=>o" |
|
610 "satisfies_is_a(M,A) == |
|
611 \<lambda>x y. is_lambda(M, list(A), |
|
612 \<lambda>env z. is_bool_of_o(M, \<exists>nx[M]. \<exists>ny[M]. |
|
613 is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & nx \<in> ny, z))" |
|
614 |
|
615 satisfies_b :: "[i,i,i]=>i" |
|
616 "satisfies_b(A) == |
|
617 \<lambda>x y. \<lambda>env \<in> list(A). bool_of_o (nth(x,env) = nth(y,env))" |
|
618 |
|
619 satisfies_is_b :: "[i=>o,i,i,i,i]=>o" |
|
620 --{*We simplify the formula to have just @{term nx} rather than |
|
621 introducing @{term ny} with @{term "nx=ny"} *} |
|
622 "satisfies_is_b(M,A) == |
|
623 \<lambda>x y. is_lambda(M, list(A), |
|
624 \<lambda>env z. |
|
625 is_bool_of_o(M, \<exists>nx[M]. is_nth(M,x,env,nx) & is_nth(M,y,env,nx), z))" |
|
626 |
|
627 satisfies_c :: "[i,i,i,i,i]=>i" |
|
628 "satisfies_c(A,p,q,rp,rq) == \<lambda>env \<in> list(A). not(rp ` env and rq ` env)" |
|
629 |
|
630 satisfies_is_c :: "[i=>o,i,i,i,i,i]=>o" |
|
631 "satisfies_is_c(M,A,h) == |
|
632 \<lambda>p q. is_lambda(M, list(A), |
|
633 \<lambda>env z. \<exists>hp[M]. \<exists>hq[M]. |
|
634 (\<exists>rp[M]. is_depth_apply(M,h,p,rp) & fun_apply(M,rp,env,hp)) & |
|
635 (\<exists>rq[M]. is_depth_apply(M,h,q,rq) & fun_apply(M,rq,env,hq)) & |
|
636 (\<exists>pq[M]. is_and(M,hp,hq,pq) & is_not(M,pq,z)))" |
|
637 |
|
638 satisfies_d :: "[i,i,i]=>i" |
|
639 "satisfies_d(A) |
|
640 == \<lambda>p rp. \<lambda>env \<in> list(A). bool_of_o (\<forall>x\<in>A. rp ` (Cons(x,env)) = 1)" |
|
641 |
|
642 satisfies_is_d :: "[i=>o,i,i,i,i]=>o" |
|
643 "satisfies_is_d(M,A,h) == |
|
644 \<lambda>p. is_lambda(M, list(A), |
|
645 \<lambda>env z. \<exists>rp[M]. is_depth_apply(M,h,p,rp) & |
|
646 is_bool_of_o(M, |
|
647 \<forall>x[M]. \<forall>xenv[M]. \<forall>hp[M]. |
|
648 x\<in>A --> is_Cons(M,x,env,xenv) --> |
|
649 fun_apply(M,rp,xenv,hp) --> number1(M,hp), |
|
650 z))" |
|
651 |
|
652 satisfies_MH :: "[i=>o,i,i,i,i]=>o" |
|
653 "satisfies_MH == |
|
654 \<lambda>M A u f. is_lambda |
|
655 (M, formula, |
|
656 is_formula_case (M, satisfies_is_a(M,A), |
|
657 satisfies_is_b(M,A), |
|
658 satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)))" |
|
659 |
|
660 |
|
661 text{*Further constraints on the class @{term M} in order to prove |
|
662 absoluteness for the constants defined above. The ultimate goal |
|
663 is the absoluteness of the function @{term satisfies}. *} |
|
664 locale M_satisfies = M_datatypes + |
|
665 assumes |
|
666 Member_replacement: |
|
667 "[|M(A); x \<in> nat; y \<in> nat|] |
|
668 ==> strong_replacement |
|
669 (M, \<lambda>env z. \<exists>bo[M]. \<exists>nx[M]. \<exists>ny[M]. |
|
670 env \<in> list(A) & is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & |
|
671 is_bool_of_o(M, nx \<in> ny, bo) & |
|
672 pair(M, env, bo, z))" |
|
673 and |
|
674 Equal_replacement: |
|
675 "[|M(A); x \<in> nat; y \<in> nat|] |
|
676 ==> strong_replacement |
|
677 (M, \<lambda>env z. \<exists>bo[M]. \<exists>nx[M]. \<exists>ny[M]. |
|
678 env \<in> list(A) & is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & |
|
679 is_bool_of_o(M, nx = ny, bo) & |
|
680 pair(M, env, bo, z))" |
|
681 and |
|
682 Nand_replacement: |
|
683 "[|M(A); M(rp); M(rq)|] |
|
684 ==> strong_replacement |
|
685 (M, \<lambda>env z. \<exists>rpe[M]. \<exists>rqe[M]. \<exists>andpq[M]. \<exists>notpq[M]. |
|
686 fun_apply(M,rp,env,rpe) & fun_apply(M,rq,env,rqe) & |
|
687 is_and(M,rpe,rqe,andpq) & is_not(M,andpq,notpq) & |
|
688 env \<in> list(A) & pair(M, env, notpq, z))" |
|
689 and |
|
690 Forall_replacement: |
|
691 "[|M(A); M(rp)|] |
|
692 ==> strong_replacement |
|
693 (M, \<lambda>env z. \<exists>bo[M]. |
|
694 env \<in> list(A) & |
|
695 is_bool_of_o (M, |
|
696 \<forall>a[M]. \<forall>co[M]. \<forall>rpco[M]. |
|
697 a\<in>A --> is_Cons(M,a,env,co) --> |
|
698 fun_apply(M,rp,co,rpco) --> number1(M, rpco), |
|
699 bo) & |
|
700 pair(M,env,bo,z))" |
|
701 and |
|
702 formula_rec_replacement: |
|
703 --{*For the @{term transrec}*} |
|
704 "[|n \<in> nat; M(A)|] ==> transrec_replacement(M, satisfies_MH(M,A), n)" |
|
705 (*NEEDS RELATIVIZATION?*) |
|
706 and |
|
707 formula_rec_lambda_replacement: |
|
708 --{*For the @{text "\<lambda>-abstraction"} in the @{term transrec} body*} |
|
709 "M(g) ==> |
|
710 strong_replacement (M, \<lambda>x y. x \<in> formula & |
|
711 y = \<langle>x, |
|
712 formula_rec_case(satisfies_a(A), |
|
713 satisfies_b(A), |
|
714 satisfies_c(A), |
|
715 satisfies_d(A), g, x)\<rangle>)" |
|
716 |
|
717 |
|
718 lemma (in M_satisfies) Member_replacement': |
|
719 "[|M(A); x \<in> nat; y \<in> nat|] |
|
720 ==> strong_replacement |
|
721 (M, \<lambda>env z. env \<in> list(A) & |
|
722 z = \<langle>env, bool_of_o(nth(x, env) \<in> nth(y, env))\<rangle>)" |
|
723 by (insert Member_replacement, simp) |
|
724 |
|
725 lemma (in M_satisfies) Equal_replacement': |
|
726 "[|M(A); x \<in> nat; y \<in> nat|] |
|
727 ==> strong_replacement |
|
728 (M, \<lambda>env z. env \<in> list(A) & |
|
729 z = \<langle>env, bool_of_o(nth(x, env) = nth(y, env))\<rangle>)" |
|
730 by (insert Equal_replacement, simp) |
|
731 |
|
732 lemma (in M_satisfies) Nand_replacement': |
|
733 "[|M(A); M(rp); M(rq)|] |
|
734 ==> strong_replacement |
|
735 (M, \<lambda>env z. env \<in> list(A) & z = \<langle>env, not(rp`env and rq`env)\<rangle>)" |
|
736 by (insert Nand_replacement, simp) |
|
737 |
|
738 lemma (in M_satisfies) Forall_replacement': |
|
739 "[|M(A); M(rp)|] |
|
740 ==> strong_replacement |
|
741 (M, \<lambda>env z. |
|
742 env \<in> list(A) & |
|
743 z = \<langle>env, bool_of_o (\<forall>a\<in>A. rp ` Cons(a,env) = 1)\<rangle>)" |
|
744 by (insert Forall_replacement, simp) |
|
745 |
|
746 lemma (in M_satisfies) a_closed: |
|
747 "[|M(A); x\<in>nat; y\<in>nat|] ==> M(satisfies_a(A,x,y))" |
|
748 apply (simp add: satisfies_a_def) |
|
749 apply (blast intro: lam_closed2 Member_replacement') |
|
750 done |
|
751 |
|
752 lemma (in M_satisfies) a_rel: |
|
753 "M(A) ==> Relativize2(M, nat, nat, satisfies_is_a(M,A), satisfies_a(A))" |
|
754 apply (simp add: Relativize2_def satisfies_is_a_def satisfies_a_def) |
|
755 apply (simp add: lambda_abs2 [OF Member_replacement'] Relativize1_def) |
|
756 done |
|
757 |
|
758 lemma (in M_satisfies) b_closed: |
|
759 "[|M(A); x\<in>nat; y\<in>nat|] ==> M(satisfies_b(A,x,y))" |
|
760 apply (simp add: satisfies_b_def) |
|
761 apply (blast intro: lam_closed2 Equal_replacement') |
|
762 done |
|
763 |
|
764 lemma (in M_satisfies) b_rel: |
|
765 "M(A) ==> Relativize2(M, nat, nat, satisfies_is_b(M,A), satisfies_b(A))" |
|
766 apply (simp add: Relativize2_def satisfies_is_b_def satisfies_b_def) |
|
767 apply (simp add: lambda_abs2 [OF Equal_replacement'] Relativize1_def) |
|
768 done |
|
769 |
|
770 lemma (in M_satisfies) c_closed: |
|
771 "[|M(A); x \<in> formula; y \<in> formula; M(rx); M(ry)|] |
|
772 ==> M(satisfies_c(A,x,y,rx,ry))" |
|
773 apply (simp add: satisfies_c_def) |
|
774 apply (rule lam_closed2) |
|
775 apply (rule Nand_replacement') |
|
776 apply (simp_all add: formula_into_M list_into_M [of _ A]) |
|
777 done |
|
778 |
|
779 lemma (in M_satisfies) c_rel: |
|
780 "[|M(A); M(f)|] ==> |
|
781 Relativize2 (M, formula, formula, |
|
782 satisfies_is_c(M,A,f), |
|
783 \<lambda>u v. satisfies_c(A, u, v, f ` succ(depth(u)) ` u, |
|
784 f ` succ(depth(v)) ` v))" |
|
785 apply (simp add: Relativize2_def satisfies_is_c_def satisfies_c_def) |
|
786 apply (simp add: lambda_abs2 [OF Nand_replacement' triv_Relativize1] |
|
787 formula_into_M) |
|
788 done |
|
789 |
|
790 lemma (in M_satisfies) d_closed: |
|
791 "[|M(A); x \<in> formula; M(rx)|] ==> M(satisfies_d(A,x,rx))" |
|
792 apply (simp add: satisfies_d_def) |
|
793 apply (rule lam_closed2) |
|
794 apply (rule Forall_replacement') |
|
795 apply (simp_all add: formula_into_M list_into_M [of _ A]) |
|
796 done |
|
797 |
|
798 lemma (in M_satisfies) d_rel: |
|
799 "[|M(A); M(f)|] ==> |
|
800 Relativize1(M, formula, satisfies_is_d(M,A,f), |
|
801 \<lambda>u. satisfies_d(A, u, f ` succ(depth(u)) ` u))" |
|
802 apply (simp del: rall_abs |
|
803 add: Relativize1_def satisfies_is_d_def satisfies_d_def) |
|
804 apply (simp add: lambda_abs2 [OF Forall_replacement' triv_Relativize1] |
|
805 formula_into_M) |
|
806 done |
|
807 |
|
808 |
|
809 lemma (in M_satisfies) fr_replace: |
|
810 "[|n \<in> nat; M(A)|] ==> transrec_replacement(M,satisfies_MH(M,A),n)" |
|
811 by (blast intro: formula_rec_replacement) |
|
812 |
|
813 lemma (in M_satisfies) fr_lam_replace: |
|
814 "M(g) ==> |
|
815 strong_replacement (M, \<lambda>x y. x \<in> formula & |
|
816 y = \<langle>x, |
|
817 formula_rec_case(satisfies_a(A), |
|
818 satisfies_b(A), |
|
819 satisfies_c(A), |
|
820 satisfies_d(A), g, x)\<rangle>)" |
|
821 by (blast intro: formula_rec_lambda_replacement) |
|
822 |
|
823 |
|
824 |
|
825 subsection{*Instantiating the Locale @{text "M_satisfies"}*} |
|
826 |
|
827 |
|
828 subsubsection{*The @{term "Member"} Case*} |
|
829 |
|
830 lemma Member_Reflects: |
|
831 "REFLECTS[\<lambda>u. \<exists>v[L]. v \<in> B \<and> (\<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L]. |
|
832 v \<in> lstA \<and> is_nth(L,x,v,nx) \<and> is_nth(L,y,v,ny) \<and> |
|
833 is_bool_of_o(L, nx \<in> ny, bo) \<and> pair(L,v,bo,u)), |
|
834 \<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B \<and> (\<exists>bo \<in> Lset(i). \<exists>nx \<in> Lset(i). \<exists>ny \<in> Lset(i). |
|
835 v \<in> lstA \<and> is_nth(**Lset(i), x, v, nx) \<and> |
|
836 is_nth(**Lset(i), y, v, ny) \<and> |
|
837 is_bool_of_o(**Lset(i), nx \<in> ny, bo) \<and> pair(**Lset(i), v, bo, u))]" |
|
838 by (intro FOL_reflections function_reflections nth_reflection |
|
839 bool_of_o_reflection) |
|
840 |
|
841 |
|
842 lemma Member_replacement: |
|
843 "[|L(A); x \<in> nat; y \<in> nat|] |
|
844 ==> strong_replacement |
|
845 (L, \<lambda>env z. \<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L]. |
|
846 env \<in> list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) & |
|
847 is_bool_of_o(L, nx \<in> ny, bo) & |
|
848 pair(L, env, bo, z))" |
|
849 apply (frule list_closed) |
|
850 apply (rule strong_replacementI) |
|
851 apply (rule rallI) |
|
852 apply (rename_tac B) |
|
853 apply (rule separation_CollectI) |
|
854 apply (rule_tac A="{list(A),B,x,y,z}" in subset_LsetE, blast ) |
|
855 apply (rule ReflectsE [OF Member_Reflects], assumption) |
|
856 apply (drule subset_Lset_ltD, assumption) |
|
857 apply (erule reflection_imp_L_separation) |
|
858 apply (simp_all add: lt_Ord2) |
|
859 apply (simp add: is_nth_def is_wfrec_def is_bool_of_o_def) |
|
860 apply (rule DPow_LsetI) |
|
861 apply (rename_tac u) |
|
862 apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+ |
|
863 apply (rule_tac env = "[v,u,list(A),B,x,y,z]" in mem_iff_sats) |
|
864 apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats |
|
865 is_recfun_iff_sats hd_iff_sats tl_iff_sats quasinat_iff_sats |
|
866 | simp)+ |
|
867 done |
|
868 |
|
869 |
|
870 subsubsection{*The @{term "Equal"} Case*} |
|
871 |
|
872 lemma Equal_Reflects: |
|
873 "REFLECTS[\<lambda>u. \<exists>v[L]. v \<in> B \<and> (\<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L]. |
|
874 v \<in> lstA \<and> is_nth(L, x, v, nx) \<and> is_nth(L, y, v, ny) \<and> |
|
875 is_bool_of_o(L, nx = ny, bo) \<and> pair(L, v, bo, u)), |
|
876 \<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B \<and> (\<exists>bo \<in> Lset(i). \<exists>nx \<in> Lset(i). \<exists>ny \<in> Lset(i). |
|
877 v \<in> lstA \<and> is_nth(**Lset(i), x, v, nx) \<and> |
|
878 is_nth(**Lset(i), y, v, ny) \<and> |
|
879 is_bool_of_o(**Lset(i), nx = ny, bo) \<and> pair(**Lset(i), v, bo, u))]" |
|
880 by (intro FOL_reflections function_reflections nth_reflection |
|
881 bool_of_o_reflection) |
|
882 |
|
883 |
|
884 lemma Equal_replacement: |
|
885 "[|L(A); x \<in> nat; y \<in> nat|] |
|
886 ==> strong_replacement |
|
887 (L, \<lambda>env z. \<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L]. |
|
888 env \<in> list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) & |
|
889 is_bool_of_o(L, nx = ny, bo) & |
|
890 pair(L, env, bo, z))" |
|
891 apply (frule list_closed) |
|
892 apply (rule strong_replacementI) |
|
893 apply (rule rallI) |
|
894 apply (rename_tac B) |
|
895 apply (rule separation_CollectI) |
|
896 apply (rule_tac A="{list(A),B,x,y,z}" in subset_LsetE, blast ) |
|
897 apply (rule ReflectsE [OF Equal_Reflects], assumption) |
|
898 apply (drule subset_Lset_ltD, assumption) |
|
899 apply (erule reflection_imp_L_separation) |
|
900 apply (simp_all add: lt_Ord2) |
|
901 apply (simp add: is_nth_def is_wfrec_def is_bool_of_o_def) |
|
902 apply (rule DPow_LsetI) |
|
903 apply (rename_tac u) |
|
904 apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+ |
|
905 apply (rule_tac env = "[v,u,list(A),B,x,y,z]" in mem_iff_sats) |
|
906 apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats |
|
907 is_recfun_iff_sats hd_iff_sats tl_iff_sats quasinat_iff_sats |
|
908 | simp)+ |
|
909 done |
|
910 |
|
911 subsubsection{*The @{term "Nand"} Case*} |
|
912 |
|
913 lemma Nand_Reflects: |
|
914 "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and> |
|
915 (\<exists>rpe[L]. \<exists>rqe[L]. \<exists>andpq[L]. \<exists>notpq[L]. |
|
916 fun_apply(L, rp, u, rpe) \<and> fun_apply(L, rq, u, rqe) \<and> |
|
917 is_and(L, rpe, rqe, andpq) \<and> is_not(L, andpq, notpq) \<and> |
|
918 u \<in> list(A) \<and> pair(L, u, notpq, x)), |
|
919 \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> |
|
920 (\<exists>rpe \<in> Lset(i). \<exists>rqe \<in> Lset(i). \<exists>andpq \<in> Lset(i). \<exists>notpq \<in> Lset(i). |
|
921 fun_apply(**Lset(i), rp, u, rpe) \<and> fun_apply(**Lset(i), rq, u, rqe) \<and> |
|
922 is_and(**Lset(i), rpe, rqe, andpq) \<and> is_not(**Lset(i), andpq, notpq) \<and> |
|
923 u \<in> list(A) \<and> pair(**Lset(i), u, notpq, x))]" |
|
924 apply (unfold is_and_def is_not_def) |
|
925 apply (intro FOL_reflections function_reflections) |
|
926 done |
|
927 |
|
928 lemma Nand_replacement: |
|
929 "[|L(A); L(rp); L(rq)|] |
|
930 ==> strong_replacement |
|
931 (L, \<lambda>env z. \<exists>rpe[L]. \<exists>rqe[L]. \<exists>andpq[L]. \<exists>notpq[L]. |
|
932 fun_apply(L,rp,env,rpe) & fun_apply(L,rq,env,rqe) & |
|
933 is_and(L,rpe,rqe,andpq) & is_not(L,andpq,notpq) & |
|
934 env \<in> list(A) & pair(L, env, notpq, z))" |
|
935 apply (frule list_closed) |
|
936 apply (rule strong_replacementI) |
|
937 apply (rule rallI) |
|
938 apply (rename_tac B) |
|
939 apply (rule separation_CollectI) |
|
940 apply (rule_tac A="{list(A),B,rp,rq,z}" in subset_LsetE, blast ) |
|
941 apply (rule ReflectsE [OF Nand_Reflects], assumption) |
|
942 apply (drule subset_Lset_ltD, assumption) |
|
943 apply (erule reflection_imp_L_separation) |
|
944 apply (simp_all add: lt_Ord2) |
|
945 apply (simp add: is_and_def is_not_def) |
|
946 apply (rule DPow_LsetI) |
|
947 apply (rename_tac v) |
|
948 apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+ |
|
949 apply (rule_tac env = "[u,v,list(A),B,rp,rq,z]" in mem_iff_sats) |
|
950 apply (rule sep_rules | simp)+ |
|
951 done |
|
952 |
|
953 |
|
954 subsubsection{*The @{term "Forall"} Case*} |
|
955 |
|
956 lemma Forall_Reflects: |
|
957 "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>bo[L]. u \<in> list(A) \<and> |
|
958 is_bool_of_o (L, |
|
959 \<forall>a[L]. \<forall>co[L]. \<forall>rpco[L]. a \<in> A \<longrightarrow> |
|
960 is_Cons(L,a,u,co) \<longrightarrow> fun_apply(L,rp,co,rpco) \<longrightarrow> |
|
961 number1(L,rpco), |
|
962 bo) \<and> pair(L,u,bo,x)), |
|
963 \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>bo \<in> Lset(i). u \<in> list(A) \<and> |
|
964 is_bool_of_o (**Lset(i), |
|
965 \<forall>a \<in> Lset(i). \<forall>co \<in> Lset(i). \<forall>rpco \<in> Lset(i). a \<in> A \<longrightarrow> |
|
966 is_Cons(**Lset(i),a,u,co) \<longrightarrow> fun_apply(**Lset(i),rp,co,rpco) \<longrightarrow> |
|
967 number1(**Lset(i),rpco), |
|
968 bo) \<and> pair(**Lset(i),u,bo,x))]" |
|
969 apply (unfold is_bool_of_o_def) |
|
970 apply (intro FOL_reflections function_reflections Cons_reflection) |
|
971 done |
|
972 |
|
973 lemma Forall_replacement: |
|
974 "[|L(A); L(rp)|] |
|
975 ==> strong_replacement |
|
976 (L, \<lambda>env z. \<exists>bo[L]. |
|
977 env \<in> list(A) & |
|
978 is_bool_of_o (L, |
|
979 \<forall>a[L]. \<forall>co[L]. \<forall>rpco[L]. |
|
980 a\<in>A --> is_Cons(L,a,env,co) --> |
|
981 fun_apply(L,rp,co,rpco) --> number1(L, rpco), |
|
982 bo) & |
|
983 pair(L,env,bo,z))" |
|
984 apply (frule list_closed) |
|
985 apply (rule strong_replacementI) |
|
986 apply (rule rallI) |
|
987 apply (rename_tac B) |
|
988 apply (rule separation_CollectI) |
|
989 apply (rule_tac A="{A,list(A),B,rp,z}" in subset_LsetE, blast ) |
|
990 apply (rule ReflectsE [OF Forall_Reflects], assumption) |
|
991 apply (drule subset_Lset_ltD, assumption) |
|
992 apply (erule reflection_imp_L_separation) |
|
993 apply (simp_all add: lt_Ord2) |
|
994 apply (simp add: is_bool_of_o_def) |
|
995 apply (rule DPow_LsetI) |
|
996 apply (rename_tac v) |
|
997 apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+ |
|
998 apply (rule_tac env = "[u,v,A,list(A),B,rp,z]" in mem_iff_sats) |
|
999 apply (rule sep_rules Cons_iff_sats | simp)+ |
|
1000 done |
|
1001 |
|
1002 subsubsection{*The @{term "transrec_replacement"} Case*} |
|
1003 |
|
1004 |
|
1005 |
|
1006 theorem satisfies_is_a_reflection: |
|
1007 "REFLECTS[\<lambda>x. satisfies_is_a(L,f(x),g(x),h(x),g'(x)), |
|
1008 \<lambda>i x. satisfies_is_a(**Lset(i),f(x),g(x),h(x),g'(x))]" |
|
1009 apply (unfold satisfies_is_a_def) |
|
1010 apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection |
|
1011 nth_reflection) |
|
1012 done |
|
1013 |
|
1014 |
|
1015 theorem satisfies_is_b_reflection: |
|
1016 "REFLECTS[\<lambda>x. satisfies_is_b(L,f(x),g(x),h(x),g'(x)), |
|
1017 \<lambda>i x. satisfies_is_b(**Lset(i),f(x),g(x),h(x),g'(x))]" |
|
1018 apply (unfold satisfies_is_b_def) |
|
1019 apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection |
|
1020 nth_reflection) |
|
1021 done |
|
1022 |
|
1023 theorem satisfies_is_c_reflection: |
|
1024 "REFLECTS[\<lambda>x. satisfies_is_c(L,f(x),g(x),h(x),g'(x),h'(x)), |
|
1025 \<lambda>i x. satisfies_is_c(**Lset(i),f(x),g(x),h(x),g'(x),h'(x))]" |
|
1026 apply (unfold satisfies_is_c_def ) |
|
1027 apply (intro FOL_reflections function_reflections is_lambda_reflection |
|
1028 bool_of_o_reflection not_reflection and_reflection |
|
1029 nth_reflection depth_apply_reflection) |
|
1030 done |
|
1031 |
|
1032 theorem satisfies_is_d_reflection: |
|
1033 "REFLECTS[\<lambda>x. satisfies_is_d(L,f(x),g(x),h(x),g'(x)), |
|
1034 \<lambda>i x. satisfies_is_d(**Lset(i),f(x),g(x),h(x),g'(x))]" |
|
1035 apply (unfold satisfies_is_d_def ) |
|
1036 apply (intro FOL_reflections function_reflections is_lambda_reflection |
|
1037 bool_of_o_reflection not_reflection and_reflection |
|
1038 nth_reflection depth_apply_reflection Cons_reflection) |
|
1039 done |
|
1040 |
|
1041 |
|
1042 lemma formula_rec_replacement_Reflects: |
|
1043 "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L, u, y, x) \<and> |
|
1044 is_wfrec (L, satisfies_MH(L,A), mesa, u, y)), |
|
1045 \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and> |
|
1046 is_wfrec (**Lset(i), satisfies_MH(**Lset(i),A), mesa, u, y))]" |
|
1047 apply (unfold satisfies_MH_def) |
|
1048 apply (intro FOL_reflections function_reflections is_wfrec_reflection |
|
1049 is_lambda_reflection) |
|
1050 apply (simp only: is_formula_case_def) |
|
1051 apply (intro FOL_reflections finite_ordinal_reflection mem_formula_reflection |
|
1052 Member_reflection Equal_reflection Nand_reflection Forall_reflection |
|
1053 satisfies_is_a_reflection satisfies_is_b_reflection |
|
1054 satisfies_is_c_reflection satisfies_is_d_reflection) |
|
1055 done |
|
1056 |
|
1057 end |
|
1058 |
|
1059 |
|
1060 |