src/ZF/Constructible/L_axioms.thy
changeset 13440 cdde97e1db1c
parent 13434 78b93a667c01
child 13493 5aa68c051725
     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Wed Jul 31 17:42:38 2002 +0200
     1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Wed Jul 31 18:30:25 2002 +0200
     1.3 @@ -284,10 +284,27 @@
     1.4  apply (intro Imp_reflection All_reflection, assumption)
     1.5  done
     1.6  
     1.7 +text{*This version handles an alternative form of the bounded quantifier
     1.8 +      in the second argument of @{text REFLECTS}.*}
     1.9 +theorem Rex_reflection':
    1.10 +     "REFLECTS[ \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
    1.11 +      ==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z[**Lset(a)]. Q(a,x,z)]"
    1.12 +apply (unfold setclass_def rex_def)
    1.13 +apply (erule Rex_reflection [unfolded rex_def Bex_def]) 
    1.14 +done
    1.15 +
    1.16 +text{*As above.*}
    1.17 +theorem Rall_reflection':
    1.18 +     "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
    1.19 +      ==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z[**Lset(a)]. Q(a,x,z)]"
    1.20 +apply (unfold setclass_def rall_def)
    1.21 +apply (erule Rall_reflection [unfolded rall_def Ball_def]) 
    1.22 +done
    1.23 +
    1.24  lemmas FOL_reflections =
    1.25          Triv_reflection Not_reflection And_reflection Or_reflection
    1.26          Imp_reflection Iff_reflection Ex_reflection All_reflection
    1.27 -        Rex_reflection Rall_reflection
    1.28 +        Rex_reflection Rall_reflection Rex_reflection' Rall_reflection'
    1.29  
    1.30  lemma ReflectsD:
    1.31       "[|REFLECTS[P,Q]; Ord(i)|]