some progress towards "satisfies"
authorpaulson
Wed Jul 31 18:30:25 2002 +0200 (2002-07-31)
changeset 13440cdde97e1db1c
parent 13439 2f98365f57a8
child 13441 d6d620639243
some progress towards "satisfies"
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Rec_Separation.thy
src/ZF/Constructible/Separation.thy
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 31 17:42:38 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 31 18:30:25 2002 +0200
     1.3 @@ -596,6 +596,14 @@
     1.4         transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
     1.5  done
     1.6  
     1.7 +text{*Helps to prove instances of @{term transrec_replacement}*}
     1.8 +lemma (in M_eclose) transrec_replacementI: 
     1.9 +   "[|M(a);
    1.10 +    strong_replacement (M, 
    1.11 +                  \<lambda>x z. \<exists>y[M]. pair(M, x, y, z) \<and> is_wfrec(M,MH,Memrel(eclose({a})),x,y))|]
    1.12 +    ==> transrec_replacement(M,MH,a)"
    1.13 +by (simp add: transrec_replacement_def wfrec_replacement_def) 
    1.14 +
    1.15  
    1.16  subsection{*Absoluteness for the List Operator @{term length}*}
    1.17  constdefs
     2.1 --- a/src/ZF/Constructible/L_axioms.thy	Wed Jul 31 17:42:38 2002 +0200
     2.2 +++ b/src/ZF/Constructible/L_axioms.thy	Wed Jul 31 18:30:25 2002 +0200
     2.3 @@ -284,10 +284,27 @@
     2.4  apply (intro Imp_reflection All_reflection, assumption)
     2.5  done
     2.6  
     2.7 +text{*This version handles an alternative form of the bounded quantifier
     2.8 +      in the second argument of @{text REFLECTS}.*}
     2.9 +theorem Rex_reflection':
    2.10 +     "REFLECTS[ \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
    2.11 +      ==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z[**Lset(a)]. Q(a,x,z)]"
    2.12 +apply (unfold setclass_def rex_def)
    2.13 +apply (erule Rex_reflection [unfolded rex_def Bex_def]) 
    2.14 +done
    2.15 +
    2.16 +text{*As above.*}
    2.17 +theorem Rall_reflection':
    2.18 +     "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
    2.19 +      ==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z[**Lset(a)]. Q(a,x,z)]"
    2.20 +apply (unfold setclass_def rall_def)
    2.21 +apply (erule Rall_reflection [unfolded rall_def Ball_def]) 
    2.22 +done
    2.23 +
    2.24  lemmas FOL_reflections =
    2.25          Triv_reflection Not_reflection And_reflection Or_reflection
    2.26          Imp_reflection Iff_reflection Ex_reflection All_reflection
    2.27 -        Rex_reflection Rall_reflection
    2.28 +        Rex_reflection Rall_reflection Rex_reflection' Rall_reflection'
    2.29  
    2.30  lemma ReflectsD:
    2.31       "[|REFLECTS[P,Q]; Ord(i)|]
     3.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Wed Jul 31 17:42:38 2002 +0200
     3.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Wed Jul 31 18:30:25 2002 +0200
     3.3 @@ -1235,10 +1235,12 @@
     3.4  done
     3.5  
     3.6  theorem bool_of_o_reflection:
     3.7 -     "REFLECTS[\<lambda>x. is_bool_of_o(L, P(x), f(x)),  
     3.8 -               \<lambda>i x. is_bool_of_o(**Lset(i), P(x), f(x))]"
     3.9 -apply (simp only: is_bool_of_o_def setclass_simps)
    3.10 +     "REFLECTS [P(L), \<lambda>i. P(**Lset(i))] ==>
    3.11 +      REFLECTS[\<lambda>x. is_bool_of_o(L, P(L,x), f(x)),  
    3.12 +               \<lambda>i x. is_bool_of_o(**Lset(i), P(**Lset(i),x), f(x))]"
    3.13 +apply (simp (no_asm) only: is_bool_of_o_def setclass_simps)
    3.14  apply (intro FOL_reflections function_reflections) 
    3.15 +apply assumption+
    3.16  done
    3.17  
    3.18  
    3.19 @@ -1407,5 +1409,6 @@
    3.20  
    3.21  lemmas eclose_closed [intro, simp] = M_eclose.eclose_closed [OF M_eclose_L]
    3.22    and eclose_abs [intro, simp] = M_eclose.eclose_abs [OF M_eclose_L]
    3.23 +  and transrec_replacementI = M_eclose.transrec_replacementI [OF M_eclose_L]
    3.24  
    3.25  end
     4.1 --- a/src/ZF/Constructible/Separation.thy	Wed Jul 31 17:42:38 2002 +0200
     4.2 +++ b/src/ZF/Constructible/Separation.thy	Wed Jul 31 18:30:25 2002 +0200
     4.3 @@ -623,5 +623,7 @@
     4.4  declare Int_closed [intro, simp]
     4.5  declare is_funspace_abs [simp]
     4.6  declare finite_funspace_closed [intro, simp]
     4.7 +declare membership_abs [simp] 
     4.8 +declare Memrel_closed  [intro,simp]
     4.9  
    4.10  end