60 |
60 |
61 lemma rtran_closure_mem_iff_sats: |
61 lemma rtran_closure_mem_iff_sats: |
62 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
62 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
63 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
63 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
64 ==> rtran_closure_mem(##A, x, y, z) \<longleftrightarrow> sats(A, rtran_closure_mem_fm(i,j,k), env)" |
64 ==> rtran_closure_mem(##A, x, y, z) \<longleftrightarrow> sats(A, rtran_closure_mem_fm(i,j,k), env)" |
65 by (simp add: sats_rtran_closure_mem_fm) |
65 by (simp) |
66 |
66 |
67 lemma rtran_closure_mem_reflection: |
67 lemma rtran_closure_mem_reflection: |
68 "REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)), |
68 "REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)), |
69 \<lambda>i x. rtran_closure_mem(##Lset(i),f(x),g(x),h(x))]" |
69 \<lambda>i x. rtran_closure_mem(##Lset(i),f(x),g(x),h(x))]" |
70 apply (simp only: rtran_closure_mem_def) |
70 apply (simp only: rtran_closure_mem_def) |
176 |
176 |
177 subsubsection\<open>Instantiating the locale \<open>M_trancl\<close>\<close> |
177 subsubsection\<open>Instantiating the locale \<open>M_trancl\<close>\<close> |
178 |
178 |
179 lemma M_trancl_axioms_L: "M_trancl_axioms(L)" |
179 lemma M_trancl_axioms_L: "M_trancl_axioms(L)" |
180 apply (rule M_trancl_axioms.intro) |
180 apply (rule M_trancl_axioms.intro) |
181 apply (assumption | rule rtrancl_separation wellfounded_trancl_separation)+ |
181 apply (assumption | rule rtrancl_separation wellfounded_trancl_separation L_nat)+ |
182 done |
182 done |
183 |
183 |
184 theorem M_trancl_L: "PROP M_trancl(L)" |
184 theorem M_trancl_L: "M_trancl(L)" |
185 by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L]) |
185 by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L]) |
186 |
186 |
187 interpretation L?: M_trancl L by (rule M_trancl_L) |
187 interpretation L?: M_trancl L by (rule M_trancl_L) |
188 |
188 |
189 |
189 |
207 "L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)" |
207 "L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)" |
208 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
208 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
209 apply (rule strong_replacementI) |
209 apply (rule strong_replacementI) |
210 apply (rule_tac u="{B,A,n,0,Memrel(succ(n))}" |
210 apply (rule_tac u="{B,A,n,0,Memrel(succ(n))}" |
211 in gen_separation_multi [OF list_replacement1_Reflects], |
211 in gen_separation_multi [OF list_replacement1_Reflects], |
212 auto simp add: nonempty) |
212 auto) |
213 apply (rule_tac env="[B,A,n,0,Memrel(succ(n))]" in DPow_LsetI) |
213 apply (rule_tac env="[B,A,n,0,Memrel(succ(n))]" in DPow_LsetI) |
214 apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats |
214 apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats |
215 is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
215 is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
216 done |
216 done |
217 |
217 |
229 "L(A) ==> strong_replacement(L, |
229 "L(A) ==> strong_replacement(L, |
230 \<lambda>n y. n\<in>nat & is_iterates(L, is_list_functor(L,A), 0, n, y))" |
230 \<lambda>n y. n\<in>nat & is_iterates(L, is_list_functor(L,A), 0, n, y))" |
231 apply (rule strong_replacementI) |
231 apply (rule strong_replacementI) |
232 apply (rule_tac u="{A,B,0,nat}" |
232 apply (rule_tac u="{A,B,0,nat}" |
233 in gen_separation_multi [OF list_replacement2_Reflects], |
233 in gen_separation_multi [OF list_replacement2_Reflects], |
234 auto simp add: L_nat nonempty) |
234 auto) |
235 apply (rule_tac env="[A,B,0,nat]" in DPow_LsetI) |
235 apply (rule_tac env="[A,B,0,nat]" in DPow_LsetI) |
236 apply (rule sep_rules list_functor_iff_sats is_iterates_iff_sats | simp)+ |
236 apply (rule sep_rules list_functor_iff_sats is_iterates_iff_sats | simp)+ |
237 done |
237 done |
238 |
238 |
239 |
239 |
258 "iterates_replacement(L, is_formula_functor(L), 0)" |
258 "iterates_replacement(L, is_formula_functor(L), 0)" |
259 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
259 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
260 apply (rule strong_replacementI) |
260 apply (rule strong_replacementI) |
261 apply (rule_tac u="{B,n,0,Memrel(succ(n))}" |
261 apply (rule_tac u="{B,n,0,Memrel(succ(n))}" |
262 in gen_separation_multi [OF formula_replacement1_Reflects], |
262 in gen_separation_multi [OF formula_replacement1_Reflects], |
263 auto simp add: nonempty) |
263 auto) |
264 apply (rule_tac env="[n,B,0,Memrel(succ(n))]" in DPow_LsetI) |
264 apply (rule_tac env="[n,B,0,Memrel(succ(n))]" in DPow_LsetI) |
265 apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats |
265 apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats |
266 is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
266 is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ |
267 done |
267 done |
268 |
268 |
279 "strong_replacement(L, |
279 "strong_replacement(L, |
280 \<lambda>n y. n\<in>nat & is_iterates(L, is_formula_functor(L), 0, n, y))" |
280 \<lambda>n y. n\<in>nat & is_iterates(L, is_formula_functor(L), 0, n, y))" |
281 apply (rule strong_replacementI) |
281 apply (rule strong_replacementI) |
282 apply (rule_tac u="{B,0,nat}" |
282 apply (rule_tac u="{B,0,nat}" |
283 in gen_separation_multi [OF formula_replacement2_Reflects], |
283 in gen_separation_multi [OF formula_replacement2_Reflects], |
284 auto simp add: nonempty L_nat) |
284 auto) |
285 apply (rule_tac env="[B,0,nat]" in DPow_LsetI) |
285 apply (rule_tac env="[B,0,nat]" in DPow_LsetI) |
286 apply (rule sep_rules formula_functor_iff_sats is_iterates_iff_sats | simp)+ |
286 apply (rule sep_rules formula_functor_iff_sats is_iterates_iff_sats | simp)+ |
287 done |
287 done |
288 |
288 |
289 text\<open>NB The proofs for type \<^term>\<open>formula\<close> are virtually identical to those |
289 text\<open>NB The proofs for type \<^term>\<open>formula\<close> are virtually identical to those |
314 |
314 |
315 lemma nth_iff_sats: |
315 lemma nth_iff_sats: |
316 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
316 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
317 i < length(env); j \<in> nat; k \<in> nat; env \<in> list(A)|] |
317 i < length(env); j \<in> nat; k \<in> nat; env \<in> list(A)|] |
318 ==> is_nth(##A, x, y, z) \<longleftrightarrow> sats(A, nth_fm(i,j,k), env)" |
318 ==> is_nth(##A, x, y, z) \<longleftrightarrow> sats(A, nth_fm(i,j,k), env)" |
319 by (simp add: sats_nth_fm) |
319 by (simp) |
320 |
320 |
321 theorem nth_reflection: |
321 theorem nth_reflection: |
322 "REFLECTS[\<lambda>x. is_nth(L, f(x), g(x), h(x)), |
322 "REFLECTS[\<lambda>x. is_nth(L, f(x), g(x), h(x)), |
323 \<lambda>i x. is_nth(##Lset(i), f(x), g(x), h(x))]" |
323 \<lambda>i x. is_nth(##Lset(i), f(x), g(x), h(x))]" |
324 apply (simp only: is_nth_def) |
324 apply (simp only: is_nth_def) |
363 list_replacement1 list_replacement2 |
363 list_replacement1 list_replacement2 |
364 formula_replacement1 formula_replacement2 |
364 formula_replacement1 formula_replacement2 |
365 nth_replacement)+ |
365 nth_replacement)+ |
366 done |
366 done |
367 |
367 |
368 theorem M_datatypes_L: "PROP M_datatypes(L)" |
368 theorem M_datatypes_L: "M_datatypes(L)" |
369 apply (rule M_datatypes.intro) |
369 apply (rule M_datatypes.intro) |
370 apply (rule M_trancl_L) |
370 apply (rule M_trancl_L) |
371 apply (rule M_datatypes_axioms_L) |
371 apply (rule M_datatypes_axioms_L) |
372 done |
372 done |
373 |
373 |
413 "L(A) ==> strong_replacement(L, |
413 "L(A) ==> strong_replacement(L, |
414 \<lambda>n y. n\<in>nat & is_iterates(L, big_union(L), A, n, y))" |
414 \<lambda>n y. n\<in>nat & is_iterates(L, big_union(L), A, n, y))" |
415 apply (rule strong_replacementI) |
415 apply (rule strong_replacementI) |
416 apply (rule_tac u="{A,B,nat}" |
416 apply (rule_tac u="{A,B,nat}" |
417 in gen_separation_multi [OF eclose_replacement2_Reflects], |
417 in gen_separation_multi [OF eclose_replacement2_Reflects], |
418 auto simp add: L_nat) |
418 auto) |
419 apply (rule_tac env="[A,B,nat]" in DPow_LsetI) |
419 apply (rule_tac env="[A,B,nat]" in DPow_LsetI) |
420 apply (rule sep_rules is_iterates_iff_sats big_union_iff_sats | simp)+ |
420 apply (rule sep_rules is_iterates_iff_sats big_union_iff_sats | simp)+ |
421 done |
421 done |
422 |
422 |
423 |
423 |
426 lemma M_eclose_axioms_L: "M_eclose_axioms(L)" |
426 lemma M_eclose_axioms_L: "M_eclose_axioms(L)" |
427 apply (rule M_eclose_axioms.intro) |
427 apply (rule M_eclose_axioms.intro) |
428 apply (assumption | rule eclose_replacement1 eclose_replacement2)+ |
428 apply (assumption | rule eclose_replacement1 eclose_replacement2)+ |
429 done |
429 done |
430 |
430 |
431 theorem M_eclose_L: "PROP M_eclose(L)" |
431 theorem M_eclose_L: "M_eclose(L)" |
432 apply (rule M_eclose.intro) |
432 apply (rule M_eclose.intro) |
433 apply (rule M_datatypes_L) |
433 apply (rule M_datatypes_L) |
434 apply (rule M_eclose_axioms_L) |
434 apply (rule M_eclose_axioms_L) |
435 done |
435 done |
436 |
436 |