author paulson Mon, 08 Jul 2002 15:56:39 +0200 changeset 13314 84b9de3cbc91 parent 13313 e4dc78f4e51e child 13315 685499c73215
Defining a meta-existential quantifier. Using it to streamline reflection proofs.
 src/ZF/Constructible/L_axioms.thy file | annotate | diff | comparison | revisions src/ZF/Constructible/MetaExists.thy file | annotate | diff | comparison | revisions src/ZF/Constructible/Separation.thy file | annotate | diff | comparison | revisions
```--- a/src/ZF/Constructible/L_axioms.thy	Mon Jul 08 15:03:04 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy	Mon Jul 08 15:56:39 2002 +0200
@@ -1,6 +1,6 @@
header {*The Class L Satisfies the ZF Axioms*}

-theory L_axioms = Formula + Relative + Reflection:
+theory L_axioms = Formula + Relative + Reflection + MetaExists:

text {* The class L satisfies the premises of locale @{text M_axioms} *}
@@ -189,10 +189,6 @@

text{*instances of locale constants*}
constdefs
-  L_Reflects :: "[i=>o,i=>o,[i,i]=>o] => o"
-    "L_Reflects(Cl,P,Q) == Closed_Unbounded(Cl) &
-                           (\<forall>a. Cl(a) --> (\<forall>x \<in> Lset(a). P(x) <-> Q(a,x)))"
-
L_F0 :: "[i=>o,i] => i"
"L_F0(P,y) == \<mu>b. (\<exists>z. L(z) \<and> P(<y,z>)) --> (\<exists>z\<in>Lset(b). P(<y,z>))"

@@ -202,87 +198,120 @@
L_ClEx :: "[i=>o,i] => o"
"L_ClEx(P) == \<lambda>a. Limit(a) \<and> normalize(L_FF(P),a) = a"

-theorem Triv_reflection [intro]:
-     "L_Reflects(Ord, P, \<lambda>a x. P(x))"

-theorem Not_reflection [intro]:
-     "L_Reflects(Cl,P,Q) ==> L_Reflects(Cl, \<lambda>x. ~P(x), \<lambda>a x. ~Q(a,x))"
-
-theorem And_reflection [intro]:
-     "[| L_Reflects(Cl,P,Q); L_Reflects(C',P',Q') |]
-      ==> L_Reflects(\<lambda>a. Cl(a) \<and> C'(a), \<lambda>x. P(x) \<and> P'(x),
-                                      \<lambda>a x. Q(a,x) \<and> Q'(a,x))"
-by (simp add: L_Reflects_def Closed_Unbounded_Int, blast)
-
-theorem Or_reflection [intro]:
-     "[| L_Reflects(Cl,P,Q); L_Reflects(C',P',Q') |]
-      ==> L_Reflects(\<lambda>a. Cl(a) \<and> C'(a), \<lambda>x. P(x) \<or> P'(x),
-                                      \<lambda>a x. Q(a,x) \<or> Q'(a,x))"
-by (simp add: L_Reflects_def Closed_Unbounded_Int, blast)
-
-theorem Imp_reflection [intro]:
-     "[| L_Reflects(Cl,P,Q); L_Reflects(C',P',Q') |]
-      ==> L_Reflects(\<lambda>a. Cl(a) \<and> C'(a),
-                   \<lambda>x. P(x) --> P'(x),
-                   \<lambda>a x. Q(a,x) --> Q'(a,x))"
-by (simp add: L_Reflects_def Closed_Unbounded_Int, blast)
-
-theorem Iff_reflection [intro]:
-     "[| L_Reflects(Cl,P,Q); L_Reflects(C',P',Q') |]
-      ==> L_Reflects(\<lambda>a. Cl(a) \<and> C'(a),
-                   \<lambda>x. P(x) <-> P'(x),
-                   \<lambda>a x. Q(a,x) <-> Q'(a,x))"
-by (simp add: L_Reflects_def Closed_Unbounded_Int, blast)
+text{*We must use the meta-existential quantifier; otherwise the reflection
+      terms become enormous!*}
+constdefs
+  L_Reflects :: "[i=>o,[i,i]=>o] => prop"      ("(3REFLECTS/ [_,/ _])")
+    "REFLECTS[P,Q] == (??Cl. Closed_Unbounded(Cl) &
+                           (\<forall>a. Cl(a) --> (\<forall>x \<in> Lset(a). P(x) <-> Q(a,x))))"

-theorem Ex_reflection [intro]:
-     "L_Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
-      ==> L_Reflects(\<lambda>a. Cl(a) \<and> L_ClEx(\<lambda>x. P(fst(x),snd(x)), a),
-                   \<lambda>x. \<exists>z. L(z) \<and> P(x,z),
-                   \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z))"
+theorem Triv_reflection:
+     "REFLECTS[P, \<lambda>a x. P(x)]"
+apply (rule meta_exI)
+apply (rule Closed_Unbounded_Ord)
+done
+
+theorem Not_reflection:
+     "REFLECTS[P,Q] ==> REFLECTS[\<lambda>x. ~P(x), \<lambda>a x. ~Q(a,x)]"
+apply (unfold L_Reflects_def)
+apply (erule meta_exE)
+apply (rule_tac x=Cl in meta_exI, simp)
+done
+
+theorem And_reflection:
+     "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
+      ==> REFLECTS[\<lambda>x. P(x) \<and> P'(x), \<lambda>a x. Q(a,x) \<and> Q'(a,x)]"
+apply (unfold L_Reflects_def)
+apply (elim meta_exE)
+apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
+done
+
+theorem Or_reflection:
+     "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
+      ==> REFLECTS[\<lambda>x. P(x) \<or> P'(x), \<lambda>a x. Q(a,x) \<or> Q'(a,x)]"
+apply (unfold L_Reflects_def)
+apply (elim meta_exE)
+apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
+done
+
+theorem Imp_reflection:
+     "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
+      ==> REFLECTS[\<lambda>x. P(x) --> P'(x), \<lambda>a x. Q(a,x) --> Q'(a,x)]"
+apply (unfold L_Reflects_def)
+apply (elim meta_exE)
+apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
+done
+
+theorem Iff_reflection:
+     "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
+      ==> REFLECTS[\<lambda>x. P(x) <-> P'(x), \<lambda>a x. Q(a,x) <-> Q'(a,x)]"
+apply (unfold L_Reflects_def)
+apply (elim meta_exE)
+apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
+done
+
+
+theorem Ex_reflection:
+     "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
+      ==> REFLECTS[\<lambda>x. \<exists>z. L(z) \<and> P(x,z), \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z)]"
apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def)
+apply (elim meta_exE)
+apply (rule meta_exI)
apply (rule reflection.Ex_reflection [OF Lset_mono_le Lset_cont Pair_in_Lset],
assumption+)
done

-theorem All_reflection [intro]:
-     "L_Reflects(Cl,  \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
-      ==> L_Reflects(\<lambda>a. Cl(a) \<and> L_ClEx(\<lambda>x. ~P(fst(x),snd(x)), a),
-                   \<lambda>x. \<forall>z. L(z) --> P(x,z),
-                   \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z))"
+theorem All_reflection:
+     "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
+      ==> REFLECTS[\<lambda>x. \<forall>z. L(z) --> P(x,z), \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z)]"
apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def)
+apply (elim meta_exE)
+apply (rule meta_exI)
apply (rule reflection.All_reflection [OF Lset_mono_le Lset_cont Pair_in_Lset],
assumption+)
done

-theorem Rex_reflection [intro]:
-     "L_Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
-      ==> L_Reflects(\<lambda>a. Cl(a) \<and> L_ClEx(\<lambda>x. P(fst(x),snd(x)), a),
-                   \<lambda>x. \<exists>z[L]. P(x,z),
-                   \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z))"
-by (unfold rex_def, blast)
+theorem Rex_reflection:
+     "REFLECTS[ \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
+      ==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z)]"
+apply (unfold rex_def)
+apply (intro And_reflection Ex_reflection, assumption)
+done

-theorem Rall_reflection [intro]:
-     "L_Reflects(Cl,  \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
-      ==> L_Reflects(\<lambda>a. Cl(a) \<and> L_ClEx(\<lambda>x. ~P(fst(x),snd(x)), a),
-                   \<lambda>x. \<forall>z[L]. P(x,z),
-                   \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z))"
-by (unfold rall_def, blast)
+theorem Rall_reflection:
+     "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
+      ==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z)]"
+apply (unfold rall_def)
+apply (intro Imp_reflection All_reflection, assumption)
+done
+
+lemmas FOL_reflection =
+        Triv_reflection Not_reflection And_reflection Or_reflection
+        Imp_reflection Iff_reflection Ex_reflection All_reflection
+        Rex_reflection Rall_reflection

lemma ReflectsD:
-     "[|L_Reflects(Cl,P,Q); Ord(i)|]
+     "[|REFLECTS[P,Q]; Ord(i)|]
==> \<exists>j. i<j & (\<forall>x \<in> Lset(j). P(x) <-> Q(j,x))"
-apply (simp add: L_Reflects_def Closed_Unbounded_def, clarify)
+apply (unfold L_Reflects_def Closed_Unbounded_def)
+apply (elim meta_exE, clarify)
apply (blast dest!: UnboundedD)
done

lemma ReflectsE:
-     "[| L_Reflects(Cl,P,Q); Ord(i);
+     "[| REFLECTS[P,Q]; Ord(i);
!!j. [|i<j;  \<forall>x \<in> Lset(j). P(x) <-> Q(j,x)|] ==> R |]
==> R"
-by (blast dest!: ReflectsD)
+apply (drule ReflectsD, assumption)
+apply blast
+done

lemma Collect_mem_eq: "{x\<in>A. x\<in>B} = A \<inter> B";
by blast
@@ -352,11 +381,12 @@
apply (blast intro: nth_type)
done

-text{*The @{text simplified} attribute tidies up the reflecting class.*}
-theorem upair_reflection [simplified,intro]:
-     "L_Reflects(?Cl, \<lambda>x. upair(L,f(x),g(x),h(x)),
-                    \<lambda>i x. upair(**Lset(i),f(x),g(x),h(x)))"
+theorem upair_reflection:
+     "REFLECTS[\<lambda>x. upair(L,f(x),g(x),h(x)),
+               \<lambda>i x. upair(**Lset(i),f(x),g(x),h(x))]"
+apply (intro FOL_reflection)
+done

subsubsection{*Ordered pairs*}

@@ -387,10 +417,12 @@
==> pair(**A, x, y, z) <-> sats(A, pair_fm(i,j,k), env)"

-theorem pair_reflection [simplified,intro]:
-     "L_Reflects(?Cl, \<lambda>x. pair(L,f(x),g(x),h(x)),
-                    \<lambda>i x. pair(**Lset(i),f(x),g(x),h(x)))"
-by (simp only: pair_def setclass_simps, fast)
+theorem pair_reflection:
+     "REFLECTS[\<lambda>x. pair(L,f(x),g(x),h(x)),
+               \<lambda>i x. pair(**Lset(i),f(x),g(x),h(x))]"
+apply (simp only: pair_def setclass_simps)
+apply (intro FOL_reflection upair_reflection)
+done

subsubsection{*Binary Unions*}
@@ -421,10 +453,12 @@
==> union(**A, x, y, z) <-> sats(A, union_fm(i,j,k), env)"

-theorem union_reflection [simplified,intro]:
-     "L_Reflects(?Cl, \<lambda>x. union(L,f(x),g(x),h(x)),
-                    \<lambda>i x. union(**Lset(i),f(x),g(x),h(x)))"
+theorem union_reflection:
+     "REFLECTS[\<lambda>x. union(L,f(x),g(x),h(x)),
+               \<lambda>i x. union(**Lset(i),f(x),g(x),h(x))]"
+apply (simp only: union_def setclass_simps)
+apply (intro FOL_reflection)
+done

subsubsection{*`Cons' for sets*}
@@ -456,10 +490,12 @@
==> is_cons(**A, x, y, z) <-> sats(A, cons_fm(i,j,k), env)"
by simp

-theorem cons_reflection [simplified,intro]:
-     "L_Reflects(?Cl, \<lambda>x. is_cons(L,f(x),g(x),h(x)),
-                    \<lambda>i x. is_cons(**Lset(i),f(x),g(x),h(x)))"
-by (simp only: is_cons_def setclass_simps, fast)
+theorem cons_reflection:
+     "REFLECTS[\<lambda>x. is_cons(L,f(x),g(x),h(x)),
+               \<lambda>i x. is_cons(**Lset(i),f(x),g(x),h(x))]"
+apply (simp only: is_cons_def setclass_simps)
+apply (intro FOL_reflection upair_reflection union_reflection)
+done

subsubsection{*Function Applications*}
@@ -491,10 +527,12 @@
==> fun_apply(**A, x, y, z) <-> sats(A, fun_apply_fm(i,j,k), env)"
by simp

-theorem fun_apply_reflection [simplified,intro]:
-     "L_Reflects(?Cl, \<lambda>x. fun_apply(L,f(x),g(x),h(x)),
-                    \<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x)))"
-by (simp only: fun_apply_def setclass_simps, fast)
+theorem fun_apply_reflection:
+     "REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)),
+               \<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x))]"
+apply (simp only: fun_apply_def setclass_simps)
+apply (intro FOL_reflection pair_reflection)
+done

subsubsection{*Variants of Satisfaction Definitions for Ordinals, etc.*}
@@ -507,20 +545,24 @@
==> sats(A, subset_fm(x,y), env) <-> subset(**A, nth(x,env), nth(y,env))"

-theorem subset_reflection [simplified,intro]:
-     "L_Reflects(?Cl, \<lambda>x. subset(L,f(x),g(x)),
-                    \<lambda>i x. subset(**Lset(i),f(x),g(x)))"
+theorem subset_reflection:
+     "REFLECTS[\<lambda>x. subset(L,f(x),g(x)),
+               \<lambda>i x. subset(**Lset(i),f(x),g(x))]"
+apply (simp only: subset_def setclass_simps)
+apply (intro FOL_reflection)
+done

lemma sats_transset_fm':
"[|x \<in> nat; env \<in> list(A)|]
==> sats(A, transset_fm(x), env) <-> transitive_set(**A, nth(x,env))"
by (simp add: sats_subset_fm' transset_fm_def transitive_set_def)

-theorem transitive_set_reflection [simplified,intro]:
-     "L_Reflects(?Cl, \<lambda>x. transitive_set(L,f(x)),
-                    \<lambda>i x. transitive_set(**Lset(i),f(x)))"
-by (simp only: transitive_set_def setclass_simps, fast)
+theorem transitive_set_reflection:
+     "REFLECTS[\<lambda>x. transitive_set(L,f(x)),
+               \<lambda>i x. transitive_set(**Lset(i),f(x))]"
+apply (simp only: transitive_set_def setclass_simps)
+apply (intro FOL_reflection subset_reflection)
+done

lemma sats_ordinal_fm':
"[|x \<in> nat; env \<in> list(A)|]
@@ -532,10 +574,11 @@
==> ordinal(**A, x) <-> sats(A, ordinal_fm(i), env)"

-theorem ordinal_reflection [simplified,intro]:
-     "L_Reflects(?Cl, \<lambda>x. ordinal(L,f(x)),
-                    \<lambda>i x. ordinal(**Lset(i),f(x)))"
-by (simp only: ordinal_def setclass_simps, fast)
+theorem ordinal_reflection:
+     "REFLECTS[\<lambda>x. ordinal(L,f(x)), \<lambda>i x. ordinal(**Lset(i),f(x))]"
+apply (simp only: ordinal_def setclass_simps)
+apply (intro FOL_reflection transitive_set_reflection)
+done

subsubsection{*Membership Relation*}
@@ -569,11 +612,12 @@
==> membership(**A, x, y) <-> sats(A, Memrel_fm(i,j), env)"
by simp

-theorem membership_reflection [simplified,intro]:
-     "L_Reflects(?Cl, \<lambda>x. membership(L,f(x),g(x)),
-                    \<lambda>i x. membership(**Lset(i),f(x),g(x)))"
-by (simp only: membership_def setclass_simps, fast)
-
+theorem membership_reflection:
+     "REFLECTS[\<lambda>x. membership(L,f(x),g(x)),
+               \<lambda>i x. membership(**Lset(i),f(x),g(x))]"
+apply (simp only: membership_def setclass_simps)
+apply (intro FOL_reflection pair_reflection)
+done

subsubsection{*Predecessor Set*}

@@ -607,10 +651,12 @@
==> pred_set(**A,U,x,r,B) <-> sats(A, pred_set_fm(i,j,k,l), env)"

-theorem pred_set_reflection [simplified,intro]:
-     "L_Reflects(?Cl, \<lambda>x. pred_set(L,f(x),g(x),h(x),b(x)),
-                    \<lambda>i x. pred_set(**Lset(i),f(x),g(x),h(x),b(x)))"
-by (simp only: pred_set_def setclass_simps, fast)
+theorem pred_set_reflection:
+     "REFLECTS[\<lambda>x. pred_set(L,f(x),g(x),h(x),b(x)),
+               \<lambda>i x. pred_set(**Lset(i),f(x),g(x),h(x),b(x))]"
+apply (simp only: pred_set_def setclass_simps)
+apply (intro FOL_reflection pair_reflection)
+done

@@ -645,10 +691,12 @@
==> is_domain(**A, x, y) <-> sats(A, domain_fm(i,j), env)"
by simp

-theorem domain_reflection [simplified,intro]:
-     "L_Reflects(?Cl, \<lambda>x. is_domain(L,f(x),g(x)),
-                    \<lambda>i x. is_domain(**Lset(i),f(x),g(x)))"
-by (simp only: is_domain_def setclass_simps, fast)
+theorem domain_reflection:
+     "REFLECTS[\<lambda>x. is_domain(L,f(x),g(x)),
+               \<lambda>i x. is_domain(**Lset(i),f(x),g(x))]"
+apply (simp only: is_domain_def setclass_simps)
+apply (intro FOL_reflection pair_reflection)
+done

subsubsection{*Range*}
@@ -682,15 +730,14 @@
==> is_range(**A, x, y) <-> sats(A, range_fm(i,j), env)"
by simp

-theorem range_reflection [simplified,intro]:
-     "L_Reflects(?Cl, \<lambda>x. is_range(L,f(x),g(x)),
-                    \<lambda>i x. is_range(**Lset(i),f(x),g(x)))"
-by (simp only: is_range_def setclass_simps, fast)
-
-
+theorem range_reflection:
+     "REFLECTS[\<lambda>x. is_range(L,f(x),g(x)),
+               \<lambda>i x. is_range(**Lset(i),f(x),g(x))]"
+apply (simp only: is_range_def setclass_simps)
+apply (intro FOL_reflection pair_reflection)
+done

-
subsubsection{*Image*}

(* "image(M,r,A,z) ==
@@ -723,10 +770,12 @@
==> image(**A, x, y, z) <-> sats(A, image_fm(i,j,k), env)"

-theorem image_reflection [simplified,intro]:
-     "L_Reflects(?Cl, \<lambda>x. image(L,f(x),g(x),h(x)),
-                    \<lambda>i x. image(**Lset(i),f(x),g(x),h(x)))"
-by (simp only: image_def setclass_simps, fast)
+theorem image_reflection:
+     "REFLECTS[\<lambda>x. image(L,f(x),g(x),h(x)),
+               \<lambda>i x. image(**Lset(i),f(x),g(x),h(x))]"
+apply (simp only: image_def setclass_simps)
+apply (intro FOL_reflection pair_reflection)
+done

subsubsection{*The Concept of Relation*}
@@ -756,10 +805,12 @@
==> is_relation(**A, x) <-> sats(A, relation_fm(i), env)"
by simp

-theorem is_relation_reflection [simplified,intro]:
-     "L_Reflects(?Cl, \<lambda>x. is_relation(L,f(x)),
-                    \<lambda>i x. is_relation(**Lset(i),f(x)))"
-by (simp only: is_relation_def setclass_simps, fast)
+theorem is_relation_reflection:
+     "REFLECTS[\<lambda>x. is_relation(L,f(x)),
+               \<lambda>i x. is_relation(**Lset(i),f(x))]"
+apply (simp only: is_relation_def setclass_simps)
+apply (intro FOL_reflection pair_reflection)
+done

subsubsection{*The Concept of Function*}
@@ -794,10 +845,12 @@
==> is_function(**A, x) <-> sats(A, function_fm(i), env)"
by simp

-theorem is_function_reflection [simplified,intro]:
-     "L_Reflects(?Cl, \<lambda>x. is_function(L,f(x)),
-                    \<lambda>i x. is_function(**Lset(i),f(x)))"
-by (simp only: is_function_def setclass_simps, fast)
+theorem is_function_reflection:
+     "REFLECTS[\<lambda>x. is_function(L,f(x)),
+               \<lambda>i x. is_function(**Lset(i),f(x))]"
+apply (simp only: is_function_def setclass_simps)
+apply (intro FOL_reflection pair_reflection)
+done

subsubsection{*Typed Functions*}
@@ -835,12 +888,21 @@
==> typed_function(**A, x, y, z) <-> sats(A, typed_function_fm(i,j,k), env)"
by simp

-theorem typed_function_reflection [simplified,intro]:
-     "L_Reflects(?Cl, \<lambda>x. typed_function(L,f(x),g(x),h(x)),
-                    \<lambda>i x. typed_function(**Lset(i),f(x),g(x),h(x)))"
-by (simp only: typed_function_def setclass_simps, fast)
+lemmas function_reflection =
+        upair_reflection pair_reflection union_reflection
+	cons_reflection fun_apply_reflection subset_reflection
+	transitive_set_reflection ordinal_reflection membership_reflection
+	pred_set_reflection domain_reflection range_reflection image_reflection
+	is_relation_reflection is_function_reflection

+theorem typed_function_reflection:
+     "REFLECTS[\<lambda>x. typed_function(L,f(x),g(x),h(x)),
+               \<lambda>i x. typed_function(**Lset(i),f(x),g(x),h(x))]"
+apply (simp only: typed_function_def setclass_simps)
+apply (intro FOL_reflection function_reflection)
+done
+

subsubsection{*Injections*}

@@ -879,10 +941,12 @@
==> injection(**A, x, y, z) <-> sats(A, injection_fm(i,j,k), env)"
by simp

-theorem injection_reflection [simplified,intro]:
-     "L_Reflects(?Cl, \<lambda>x. injection(L,f(x),g(x),h(x)),
-                    \<lambda>i x. injection(**Lset(i),f(x),g(x),h(x)))"
-by (simp only: injection_def setclass_simps, fast)
+theorem injection_reflection:
+     "REFLECTS[\<lambda>x. injection(L,f(x),g(x),h(x)),
+               \<lambda>i x. injection(**Lset(i),f(x),g(x),h(x))]"
+apply (simp only: injection_def setclass_simps)
+apply (intro FOL_reflection function_reflection typed_function_reflection)
+done

subsubsection{*Surjections*}
@@ -919,10 +983,12 @@
==> surjection(**A, x, y, z) <-> sats(A, surjection_fm(i,j,k), env)"
by simp

-theorem surjection_reflection [simplified,intro]:
-     "L_Reflects(?Cl, \<lambda>x. surjection(L,f(x),g(x),h(x)),
-                    \<lambda>i x. surjection(**Lset(i),f(x),g(x),h(x)))"
-by (simp only: surjection_def setclass_simps, fast)
+theorem surjection_reflection:
+     "REFLECTS[\<lambda>x. surjection(L,f(x),g(x),h(x)),
+               \<lambda>i x. surjection(**Lset(i),f(x),g(x),h(x))]"
+apply (simp only: surjection_def setclass_simps)
+apply (intro FOL_reflection function_reflection typed_function_reflection)
+done

@@ -954,11 +1020,12 @@
==> bijection(**A, x, y, z) <-> sats(A, bijection_fm(i,j,k), env)"
by simp

-theorem bijection_reflection [simplified,intro]:
-     "L_Reflects(?Cl, \<lambda>x. bijection(L,f(x),g(x),h(x)),
-                    \<lambda>i x. bijection(**Lset(i),f(x),g(x),h(x)))"
-by (simp only: bijection_def setclass_simps, fast)
-
+theorem bijection_reflection:
+     "REFLECTS[\<lambda>x. bijection(L,f(x),g(x),h(x)),
+               \<lambda>i x. bijection(**Lset(i),f(x),g(x),h(x))]"
+apply (simp only: bijection_def setclass_simps)
+apply (intro And_reflection injection_reflection surjection_reflection)
+done

subsubsection{*Order-Isomorphisms*}
@@ -1010,10 +1077,11 @@
sats(A, order_isomorphism_fm(i,j,k,j',k'), env)"
by simp

-theorem order_isomorphism_reflection [simplified,intro]:
-     "L_Reflects(?Cl, \<lambda>x. order_isomorphism(L,f(x),g(x),h(x),g'(x),h'(x)),
-               \<lambda>i x. order_isomorphism(**Lset(i),f(x),g(x),h(x),g'(x),h'(x)))"
-by (simp only: order_isomorphism_def setclass_simps, fast)
-
+theorem order_isomorphism_reflection:
+     "REFLECTS[\<lambda>x. order_isomorphism(L,f(x),g(x),h(x),g'(x),h'(x)),
+               \<lambda>i x. order_isomorphism(**Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
+apply (simp only: order_isomorphism_def setclass_simps)
+apply (intro FOL_reflection function_reflection bijection_reflection)
+done

end```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/MetaExists.thy	Mon Jul 08 15:56:39 2002 +0200
@@ -0,0 +1,35 @@
+
+theory MetaExists = Main:
+
+text{*Allows quantification over any term having sort @{text logic}.  Used to
+quantify over classes.  Yields a proposition rather than a FOL formula.*}
+
+constdefs
+  ex :: "(('a::logic) => prop) => prop"            (binder "?? " 0)
+  "ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)"
+
+syntax (xsymbols)
+  "?? "        :: "[idts, o] => o"             ("(3\<Or>_./ _)" [0, 0] 0)
+
+lemma meta_exI: "PROP P(x) ==> (?? x. PROP P(x))"
+proof -
+  assume P: "PROP P(x)"
+  show "?? x. PROP P(x)"
+  apply (unfold ex_def)
+  proof -
+    fix Q
+    assume PQ: "\<And>x. PROP P(x) \<Longrightarrow> PROP Q"
+    from P show "PROP Q" by (rule PQ)
+  qed
+qed
+
+lemma meta_exE: "[| ?? x. PROP P(x);  !!x. PROP P(x) ==> PROP R |] ==> PROP R"
+apply (unfold ex_def)
+proof -
+  assume QPQ: "\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q"
+  assume PR: "\<And>x. PROP P(x) \<Longrightarrow> PROP R"
+  from PR show "PROP R" by (rule QPQ)
+qed
+
+end```
```--- a/src/ZF/Constructible/Separation.thy	Mon Jul 08 15:03:04 2002 +0200
+++ b/src/ZF/Constructible/Separation.thy	Mon Jul 08 15:56:39 2002 +0200
@@ -44,9 +44,9 @@
subsubsection{*Separation for Intersection*}

lemma Inter_Reflects:
-     "L_Reflects(?Cl, \<lambda>x. \<forall>y[L]. y\<in>A --> x \<in> y,
-               \<lambda>i x. \<forall>y\<in>Lset(i). y\<in>A --> x \<in> y)"
-by fast
+     "REFLECTS[\<lambda>x. \<forall>y[L]. y\<in>A --> x \<in> y,
+               \<lambda>i x. \<forall>y\<in>Lset(i). y\<in>A --> x \<in> y]"
+by (intro FOL_reflection)

lemma Inter_separation:
"L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A --> x\<in>y)"
@@ -67,10 +67,10 @@
subsubsection{*Separation for Cartesian Product*}

lemma cartprod_Reflects [simplified]:
-     "L_Reflects(?Cl, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)),
+     "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)),
\<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). y\<in>B &
-                               pair(**Lset(i),x,y,z)))"
-by fast
+                                   pair(**Lset(i),x,y,z))]"
+by (intro FOL_reflection function_reflection)

lemma cartprod_separation:
"[| L(A); L(B) |]
@@ -100,9 +100,9 @@
text{*No @{text simplified} here: it simplifies the occurrence of
the predicate @{term pair}!*}
lemma image_Reflects:
-     "L_Reflects(?Cl, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)),
-           \<lambda>i y. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). x\<in>A & pair(**Lset(i),x,y,p)))"
-by fast
+     "REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)),
+           \<lambda>i y. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). x\<in>A & pair(**Lset(i),x,y,p))]"
+by (intro FOL_reflection function_reflection)

lemma image_separation:
@@ -136,11 +136,10 @@
subsubsection{*Separation for Converse*}

lemma converse_Reflects:
-     "L_Reflects(?Cl,
-        \<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)),
+  "REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)),
\<lambda>i z. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i).
-                     pair(**Lset(i),x,y,p) & pair(**Lset(i),y,x,z)))"
-by fast
+                     pair(**Lset(i),x,y,p) & pair(**Lset(i),y,x,z))]"
+by (intro FOL_reflection function_reflection)

lemma converse_separation:
"L(r) ==> separation(L,
@@ -171,9 +170,9 @@
subsubsection{*Separation for Restriction*}

lemma restrict_Reflects:
-     "L_Reflects(?Cl, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)),
-        \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). pair(**Lset(i),x,y,z)))"
-by fast
+     "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)),
+        \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). pair(**Lset(i),x,y,z))]"
+by (intro FOL_reflection function_reflection)

lemma restrict_separation:
"L(A) ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)))"
@@ -197,13 +196,13 @@
subsubsection{*Separation for Composition*}

lemma comp_Reflects:
-     "L_Reflects(?Cl, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L].
+     "REFLECTS[\<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L].
pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
xy\<in>s & yz\<in>r,
\<lambda>i xz. \<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). \<exists>z\<in>Lset(i). \<exists>xy\<in>Lset(i). \<exists>yz\<in>Lset(i).
pair(**Lset(i),x,z,xz) & pair(**Lset(i),x,y,xy) &
-                  pair(**Lset(i),y,z,yz) & xy\<in>s & yz\<in>r)"
-by fast
+                  pair(**Lset(i),y,z,yz) & xy\<in>s & yz\<in>r]"
+by (intro FOL_reflection function_reflection)

lemma comp_separation:
"[| L(r); L(s) |]
@@ -250,9 +249,9 @@
subsubsection{*Separation for Predecessors in an Order*}

lemma pred_Reflects:
-     "L_Reflects(?Cl, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p),
-                    \<lambda>i y. \<exists>p \<in> Lset(i). p\<in>r & pair(**Lset(i),y,x,p))"
-by fast
+     "REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p),
+                    \<lambda>i y. \<exists>p \<in> Lset(i). p\<in>r & pair(**Lset(i),y,x,p)]"
+by (intro FOL_reflection function_reflection)

lemma pred_separation:
"[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p))"
@@ -280,9 +279,9 @@
subsubsection{*Separation for the Membership Relation*}

lemma Memrel_Reflects:
-     "L_Reflects(?Cl, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y,
-            \<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(**Lset(i),x,y,z) & x \<in> y)"
-by fast
+     "REFLECTS[\<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y,
+            \<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(**Lset(i),x,y,z) & x \<in> y]"
+by (intro FOL_reflection function_reflection)

lemma Memrel_separation:
"separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)"
@@ -310,14 +309,14 @@
subsubsection{*Replacement for FunSpace*}

lemma funspace_succ_Reflects:
- "L_Reflects(?Cl, \<lambda>z. \<exists>p[L]. p\<in>A & (\<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L].
+ "REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>A & (\<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L].
pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) &
upair(L,cnbf,cnbf,z)),
\<lambda>i z. \<exists>p \<in> Lset(i). p\<in>A & (\<exists>f \<in> Lset(i). \<exists>b \<in> Lset(i).
\<exists>nb \<in> Lset(i). \<exists>cnbf \<in> Lset(i).
pair(**Lset(i),f,b,p) & pair(**Lset(i),n,b,nb) &
-		is_cons(**Lset(i),nb,f,cnbf) & upair(**Lset(i),cnbf,cnbf,z)))"
-by fast
+		is_cons(**Lset(i),nb,f,cnbf) & upair(**Lset(i),cnbf,cnbf,z))]"
+by (intro FOL_reflection function_reflection)

lemma funspace_succ_replacement:
"L(n) ==>
@@ -367,11 +366,11 @@
subsubsection{*Separation for Order-Isomorphisms*}

lemma well_ord_iso_Reflects:
-     "L_Reflects(?Cl, \<lambda>x. x\<in>A --> (\<exists>y[L]. \<exists>p[L].
-		     fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r),
-            \<lambda>i x. x\<in>A --> (\<exists>y \<in> Lset(i). \<exists>p \<in> Lset(i).
-		     fun_apply(**Lset(i),f,x,y) & pair(**Lset(i),y,x,p) & p \<in> r))"
-by fast
+  "REFLECTS[\<lambda>x. x\<in>A -->
+                (\<exists>y[L]. \<exists>p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r),
+        \<lambda>i x. x\<in>A --> (\<exists>y \<in> Lset(i). \<exists>p \<in> Lset(i).
+                fun_apply(**Lset(i),f,x,y) & pair(**Lset(i),y,x,p) & p \<in> r)]"
+by (intro FOL_reflection function_reflection)

lemma well_ord_iso_separation:
"[| L(A); L(f); L(r) |] ```