--- a/src/ZF/Constructible/Reflection.thy Tue Sep 27 17:03:23 2022 +0100
+++ b/src/ZF/Constructible/Reflection.thy Tue Sep 27 17:46:52 2022 +0100
@@ -24,7 +24,7 @@
closed under ordered pairing provided \<open>l\<close> is limit. Possibly this
could be avoided: the induction hypothesis \<^term>\<open>Cl_reflects\<close>
(in locale \<open>ex_reflection\<close>) could be weakened to
-\<^term>\<open>\<forall>y\<in>Mset(a). \<forall>z\<in>Mset(a). P(<y,z>) \<longleftrightarrow> Q(a,<y,z>)\<close>, removing most
+\<^term>\<open>\<forall>y\<in>Mset(a). \<forall>z\<in>Mset(a). P(\<langle>y,z\<rangle>) \<longleftrightarrow> Q(a,\<langle>y,z\<rangle>)\<close>, removing most
uses of \<^term>\<open>Pair_in_Mset\<close>. But there isn't much point in doing so, since
ultimately the \<open>ex_reflection\<close> proof is packaged up using the
predicate \<open>Reflects\<close>.
@@ -34,15 +34,15 @@
assumes Mset_mono_le : "mono_le_subset(Mset)"
and Mset_cont : "cont_Ord(Mset)"
and Pair_in_Mset : "\<lbrakk>x \<in> Mset(a); y \<in> Mset(a); Limit(a)\<rbrakk>
- \<Longrightarrow> <x,y> \<in> Mset(a)"
+ \<Longrightarrow> \<langle>x,y\<rangle> \<in> Mset(a)"
defines "M(x) \<equiv> \<exists>a. Ord(a) \<and> x \<in> Mset(a)"
and "Reflects(Cl,P,Q) \<equiv> Closed_Unbounded(Cl) \<and>
(\<forall>a. Cl(a) \<longrightarrow> (\<forall>x\<in>Mset(a). P(x) \<longleftrightarrow> Q(a,x)))"
fixes F0 \<comment> \<open>ordinal for a specific value \<^term>\<open>y\<close>\<close>
fixes FF \<comment> \<open>sup over the whole level, \<^term>\<open>y\<in>Mset(a)\<close>\<close>
fixes ClEx \<comment> \<open>Reflecting ordinals for the formula \<^term>\<open>\<exists>z. P\<close>\<close>
- defines "F0(P,y) \<equiv> \<mu> b. (\<exists>z. M(z) \<and> P(<y,z>)) \<longrightarrow>
- (\<exists>z\<in>Mset(b). P(<y,z>))"
+ defines "F0(P,y) \<equiv> \<mu> b. (\<exists>z. M(z) \<and> P(\<langle>y,z\<rangle>)) \<longrightarrow>
+ (\<exists>z\<in>Mset(b). P(\<langle>y,z\<rangle>))"
and "FF(P) \<equiv> \<lambda>a. \<Union>y\<in>Mset(a). F0(P,y)"
and "ClEx(P,a) \<equiv> Limit(a) \<and> normalize(FF(P),a) = a"
@@ -97,7 +97,7 @@
subsection\<open>Reflection for Existential Quantifiers\<close>
lemma F0_works:
- "\<lbrakk>y\<in>Mset(a); Ord(a); M(z); P(<y,z>)\<rbrakk> \<Longrightarrow> \<exists>z\<in>Mset(F0(P,y)). P(<y,z>)"
+ "\<lbrakk>y\<in>Mset(a); Ord(a); M(z); P(\<langle>y,z\<rangle>)\<rbrakk> \<Longrightarrow> \<exists>z\<in>Mset(F0(P,y)). P(\<langle>y,z\<rangle>)"
unfolding F0_def M_def
apply clarify
apply (rule LeastI2)
@@ -117,7 +117,7 @@
text\<open>Recall that \<^term>\<open>F0\<close> depends upon \<^term>\<open>y\<in>Mset(a)\<close>,
while \<^term>\<open>FF\<close> depends only upon \<^term>\<open>a\<close>.\<close>
lemma FF_works:
- "\<lbrakk>M(z); y\<in>Mset(a); P(<y,z>); Ord(a)\<rbrakk> \<Longrightarrow> \<exists>z\<in>Mset(FF(P,a)). P(<y,z>)"
+ "\<lbrakk>M(z); y\<in>Mset(a); P(\<langle>y,z\<rangle>); Ord(a)\<rbrakk> \<Longrightarrow> \<exists>z\<in>Mset(FF(P,a)). P(\<langle>y,z\<rangle>)"
apply (simp add: FF_def)
apply (simp_all add: cont_Ord_Union [of concl: Mset]
Mset_cont Mset_mono_le not_emptyI)
@@ -125,8 +125,8 @@
done
lemma FFN_works:
- "\<lbrakk>M(z); y\<in>Mset(a); P(<y,z>); Ord(a)\<rbrakk>
- \<Longrightarrow> \<exists>z\<in>Mset(normalize(FF(P),a)). P(<y,z>)"
+ "\<lbrakk>M(z); y\<in>Mset(a); P(\<langle>y,z\<rangle>); Ord(a)\<rbrakk>
+ \<Longrightarrow> \<exists>z\<in>Mset(normalize(FF(P),a)). P(\<langle>y,z\<rangle>)"
apply (drule FF_works [of concl: P], assumption+)
apply (blast intro: cont_Ord_FF le_normalize [THEN Mset_mono, THEN subsetD])
done
@@ -144,8 +144,8 @@
begin
lemma ClEx_downward:
- "\<lbrakk>M(z); y\<in>Mset(a); P(<y,z>); Cl(a); ClEx(P,a)\<rbrakk>
- \<Longrightarrow> \<exists>z\<in>Mset(a). Q(a,<y,z>)"
+ "\<lbrakk>M(z); y\<in>Mset(a); P(\<langle>y,z\<rangle>); Cl(a); ClEx(P,a)\<rbrakk>
+ \<Longrightarrow> \<exists>z\<in>Mset(a). Q(a,\<langle>y,z\<rangle>)"
apply (simp add: ClEx_def, clarify)
apply (frule Limit_is_Ord)
apply (frule FFN_works [of concl: P], assumption+)
@@ -154,8 +154,8 @@
done
lemma ClEx_upward:
- "\<lbrakk>z\<in>Mset(a); y\<in>Mset(a); Q(a,<y,z>); Cl(a); ClEx(P,a)\<rbrakk>
- \<Longrightarrow> \<exists>z. M(z) \<and> P(<y,z>)"
+ "\<lbrakk>z\<in>Mset(a); y\<in>Mset(a); Q(a,\<langle>y,z\<rangle>); Cl(a); ClEx(P,a)\<rbrakk>
+ \<Longrightarrow> \<exists>z. M(z) \<and> P(\<langle>y,z\<rangle>)"
apply (simp add: ClEx_def M_def)
apply (blast dest: Cl_reflects
intro: Limit_is_Ord Pair_in_Mset)
@@ -164,7 +164,7 @@
text\<open>Class \<open>ClEx\<close> indeed consists of reflecting ordinals...\<close>
lemma ZF_ClEx_iff:
"\<lbrakk>y\<in>Mset(a); Cl(a); ClEx(P,a)\<rbrakk>
- \<Longrightarrow> (\<exists>z. M(z) \<and> P(<y,z>)) \<longleftrightarrow> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
+ \<Longrightarrow> (\<exists>z. M(z) \<and> P(\<langle>y,z\<rangle>)) \<longleftrightarrow> (\<exists>z\<in>Mset(a). Q(a,\<langle>y,z\<rangle>))"
by (blast intro: dest: ClEx_downward ClEx_upward)
text\<open>...and it is closed and unbounded\<close>
@@ -186,7 +186,7 @@
lemma ClEx_iff:
"\<lbrakk>y\<in>Mset(a); Cl(a); ClEx(P,a);
\<And>a. \<lbrakk>Cl(a); Ord(a)\<rbrakk> \<Longrightarrow> \<forall>x\<in>Mset(a). P(x) \<longleftrightarrow> Q(a,x)\<rbrakk>
- \<Longrightarrow> (\<exists>z. M(z) \<and> P(<y,z>)) \<longleftrightarrow> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
+ \<Longrightarrow> (\<exists>z. M(z) \<and> P(\<langle>y,z\<rangle>)) \<longleftrightarrow> (\<exists>z\<in>Mset(a). Q(a,\<langle>y,z\<rangle>))"
apply (unfold ClEx_def FF_def F0_def M_def)
apply (rule ex_reflection.ZF_ClEx_iff
[OF ex_reflection.intro, OF reflection.intro ex_reflection_axioms.intro,
@@ -215,8 +215,8 @@
lemma Ex_reflection_0:
"Reflects(Cl,P0,Q0)
\<Longrightarrow> Reflects(\<lambda>a. Cl(a) \<and> ClEx(P0,a),
- \<lambda>x. \<exists>z. M(z) \<and> P0(<x,z>),
- \<lambda>a x. \<exists>z\<in>Mset(a). Q0(a,<x,z>))"
+ \<lambda>x. \<exists>z. M(z) \<and> P0(\<langle>x,z\<rangle>),
+ \<lambda>a x. \<exists>z\<in>Mset(a). Q0(a,\<langle>x,z\<rangle>))"
apply (simp add: Reflects_def)
apply (intro conjI Closed_Unbounded_Int)
apply blast
@@ -227,8 +227,8 @@
lemma All_reflection_0:
"Reflects(Cl,P0,Q0)
\<Longrightarrow> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x.\<not>P0(x), a),
- \<lambda>x. \<forall>z. M(z) \<longrightarrow> P0(<x,z>),
- \<lambda>a x. \<forall>z\<in>Mset(a). Q0(a,<x,z>))"
+ \<lambda>x. \<forall>z. M(z) \<longrightarrow> P0(\<langle>x,z\<rangle>),
+ \<lambda>a x. \<forall>z\<in>Mset(a). Q0(a,\<langle>x,z\<rangle>))"
apply (simp only: all_iff_not_ex_not ball_iff_not_bex_not)
apply (rule Not_reflection, drule Not_reflection, simp)
apply (erule Ex_reflection_0)