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)|]
```