--- a/src/ZF/Constructible/Reflection.thy Tue Sep 27 16:51:35 2022 +0100
+++ b/src/ZF/Constructible/Reflection.thy Tue Sep 27 17:03:23 2022 +0100
@@ -35,16 +35,16 @@
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)"
- defines "M(x) \<equiv> \<exists>a. Ord(a) & x \<in> Mset(a)"
- and "Reflects(Cl,P,Q) \<equiv> Closed_Unbounded(Cl) &
+ 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) & P(<y,z>)) \<longrightarrow>
+ defines "F0(P,y) \<equiv> \<mu> b. (\<exists>z. M(z) \<and> P(<y,z>)) \<longrightarrow>
(\<exists>z\<in>Mset(b). P(<y,z>))"
and "FF(P) \<equiv> \<lambda>a. \<Union>y\<in>Mset(a). F0(P,y)"
- and "ClEx(P,a) \<equiv> Limit(a) & normalize(FF(P),a) = a"
+ and "ClEx(P,a) \<equiv> Limit(a) \<and> normalize(FF(P),a) = a"
begin
@@ -54,7 +54,7 @@
text\<open>Awkward: we need a version of \<open>ClEx_def\<close> as an equality
at the level of classes, which do not really exist\<close>
lemma ClEx_eq:
- "ClEx(P) \<equiv> \<lambda>a. Limit(a) & normalize(FF(P),a) = a"
+ "ClEx(P) \<equiv> \<lambda>a. Limit(a) \<and> normalize(FF(P),a) = a"
by (simp add: ClEx_def [symmetric])
@@ -70,26 +70,26 @@
theorem And_reflection [intro]:
"\<lbrakk>Reflects(Cl,P,Q); Reflects(C',P',Q')\<rbrakk>
- \<Longrightarrow> Reflects(\<lambda>a. Cl(a) & C'(a), \<lambda>x. P(x) & P'(x),
- \<lambda>a x. Q(a,x) & Q'(a,x))"
+ \<Longrightarrow> 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: Reflects_def Closed_Unbounded_Int, blast)
theorem Or_reflection [intro]:
"\<lbrakk>Reflects(Cl,P,Q); Reflects(C',P',Q')\<rbrakk>
- \<Longrightarrow> Reflects(\<lambda>a. Cl(a) & C'(a), \<lambda>x. P(x) | P'(x),
- \<lambda>a x. Q(a,x) | Q'(a,x))"
+ \<Longrightarrow> 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: Reflects_def Closed_Unbounded_Int, blast)
theorem Imp_reflection [intro]:
"\<lbrakk>Reflects(Cl,P,Q); Reflects(C',P',Q')\<rbrakk>
- \<Longrightarrow> Reflects(\<lambda>a. Cl(a) & C'(a),
+ \<Longrightarrow> Reflects(\<lambda>a. Cl(a) \<and> C'(a),
\<lambda>x. P(x) \<longrightarrow> P'(x),
\<lambda>a x. Q(a,x) \<longrightarrow> Q'(a,x))"
by (simp add: Reflects_def Closed_Unbounded_Int, blast)
theorem Iff_reflection [intro]:
"\<lbrakk>Reflects(Cl,P,Q); Reflects(C',P',Q')\<rbrakk>
- \<Longrightarrow> Reflects(\<lambda>a. Cl(a) & C'(a),
+ \<Longrightarrow> Reflects(\<lambda>a. Cl(a) \<and> C'(a),
\<lambda>x. P(x) \<longleftrightarrow> P'(x),
\<lambda>a x. Q(a,x) \<longleftrightarrow> Q'(a,x))"
by (simp add: Reflects_def Closed_Unbounded_Int, blast)
@@ -97,33 +97,32 @@
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>)"
-apply (unfold F0_def M_def, clarify)
-apply (rule LeastI2)
- apply (blast intro: Mset_mono [THEN subsetD])
- apply (blast intro: lt_Ord2, blast)
-done
+ "\<lbrakk>y\<in>Mset(a); Ord(a); M(z); P(<y,z>)\<rbrakk> \<Longrightarrow> \<exists>z\<in>Mset(F0(P,y)). P(<y,z>)"
+ unfolding F0_def M_def
+ apply clarify
+ apply (rule LeastI2)
+ apply (blast intro: Mset_mono [THEN subsetD])
+ apply (blast intro: lt_Ord2, blast)
+ done
lemma Ord_F0 [intro,simp]: "Ord(F0(P,y))"
-by (simp add: F0_def)
+ by (simp add: F0_def)
lemma Ord_FF [intro,simp]: "Ord(FF(P,y))"
-by (simp add: FF_def)
+ by (simp add: FF_def)
lemma cont_Ord_FF: "cont_Ord(FF(P))"
-apply (insert Mset_cont)
-apply (simp add: cont_Ord_def FF_def, blast)
-done
+ using Mset_cont by (simp add: cont_Ord_def FF_def, blast)
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>)"
-apply (simp add: FF_def)
-apply (simp_all add: cont_Ord_Union [of concl: Mset]
- Mset_cont Mset_mono_le not_emptyI)
-apply (blast intro: F0_works)
-done
+ "\<lbrakk>M(z); y\<in>Mset(a); P(<y,z>); Ord(a)\<rbrakk> \<Longrightarrow> \<exists>z\<in>Mset(FF(P,a)). P(<y,z>)"
+ apply (simp add: FF_def)
+ apply (simp_all add: cont_Ord_Union [of concl: Mset]
+ Mset_cont Mset_mono_le not_emptyI)
+ apply (blast intro: F0_works)
+ done
lemma FFN_works:
"\<lbrakk>M(z); y\<in>Mset(a); P(<y,z>); Ord(a)\<rbrakk>
@@ -156,7 +155,7 @@
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) & P(<y,z>)"
+ \<Longrightarrow> \<exists>z. M(z) \<and> P(<y,z>)"
apply (simp add: ClEx_def M_def)
apply (blast dest: Cl_reflects
intro: Limit_is_Ord Pair_in_Mset)
@@ -165,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) & P(<y,z>)) \<longleftrightarrow> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
+ \<Longrightarrow> (\<exists>z. M(z) \<and> P(<y,z>)) \<longleftrightarrow> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
by (blast intro: dest: ClEx_downward ClEx_upward)
text\<open>...and it is closed and unbounded\<close>
@@ -187,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) & P(<y,z>)) \<longleftrightarrow> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
+ \<Longrightarrow> (\<exists>z. M(z) \<and> P(<y,z>)) \<longleftrightarrow> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
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 +214,8 @@
lemma Ex_reflection_0:
"Reflects(Cl,P0,Q0)
- \<Longrightarrow> Reflects(\<lambda>a. Cl(a) & ClEx(P0,a),
- \<lambda>x. \<exists>z. M(z) & P0(<x,z>),
+ \<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>))"
apply (simp add: Reflects_def)
apply (intro conjI Closed_Unbounded_Int)
@@ -227,7 +226,7 @@
lemma All_reflection_0:
"Reflects(Cl,P0,Q0)
- \<Longrightarrow> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x.\<not>P0(x), a),
+ \<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>))"
apply (simp only: all_iff_not_ex_not ball_iff_not_bex_not)
@@ -237,15 +236,15 @@
theorem Ex_reflection [intro]:
"Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
- \<Longrightarrow> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x. P(fst(x),snd(x)), a),
- \<lambda>x. \<exists>z. M(z) & P(x,z),
+ \<Longrightarrow> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x. P(fst(x),snd(x)), a),
+ \<lambda>x. \<exists>z. M(z) \<and> P(x,z),
\<lambda>a x. \<exists>z\<in>Mset(a). Q(a,x,z))"
by (rule Ex_reflection_0 [of _ " \<lambda>x. P(fst(x),snd(x))"
"\<lambda>a x. Q(a,fst(x),snd(x))", simplified])
theorem All_reflection [intro]:
"Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
- \<Longrightarrow> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x. \<not>P(fst(x),snd(x)), a),
+ \<Longrightarrow> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x. \<not>P(fst(x),snd(x)), a),
\<lambda>x. \<forall>z. M(z) \<longrightarrow> P(x,z),
\<lambda>a x. \<forall>z\<in>Mset(a). Q(a,x,z))"
by (rule All_reflection_0 [of _ "\<lambda>x. P(fst(x),snd(x))"
@@ -255,14 +254,14 @@
theorem Rex_reflection [intro]:
"Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
- \<Longrightarrow> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x. P(fst(x),snd(x)), a),
+ \<Longrightarrow> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x. P(fst(x),snd(x)), a),
\<lambda>x. \<exists>z[M]. P(x,z),
\<lambda>a x. \<exists>z\<in>Mset(a). Q(a,x,z))"
by (unfold rex_def, blast)
theorem Rall_reflection [intro]:
"Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
- \<Longrightarrow> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x. \<not>P(fst(x),snd(x)), a),
+ \<Longrightarrow> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x. \<not>P(fst(x),snd(x)), a),
\<lambda>x. \<forall>z[M]. P(x,z),
\<lambda>a x. \<forall>z\<in>Mset(a). Q(a,x,z))"
by (unfold rall_def, blast)
@@ -278,7 +277,7 @@
proof state.\<close>
schematic_goal
"Reflects(?Cl,
- \<lambda>x. \<exists>y. M(y) & x \<in> y,
+ \<lambda>x. \<exists>y. M(y) \<and> x \<in> y,
\<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)"
by fast
@@ -286,8 +285,8 @@
in the class of reflecting ordinals. The \<^term>\<open>Ord(a)\<close> is redundant,
though harmless.\<close>
lemma
- "Reflects(\<lambda>a. Ord(a) & ClEx(\<lambda>x. fst(x) \<in> snd(x), a),
- \<lambda>x. \<exists>y. M(y) & x \<in> y,
+ "Reflects(\<lambda>a. Ord(a) \<and> ClEx(\<lambda>x. fst(x) \<in> snd(x), a),
+ \<lambda>x. \<exists>y. M(y) \<and> x \<in> y,
\<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)"
by fast
@@ -295,31 +294,31 @@
text\<open>Example 2\<close>
schematic_goal
"Reflects(?Cl,
- \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<subseteq> x \<longrightarrow> z \<in> y),
+ \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) \<longrightarrow> z \<subseteq> x \<longrightarrow> z \<in> y),
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x \<longrightarrow> z \<in> y)"
by fast
text\<open>Example 2'. We give the reflecting class explicitly.\<close>
lemma
"Reflects
- (\<lambda>a. (Ord(a) &
- ClEx(\<lambda>x. \<not> (snd(x) \<subseteq> fst(fst(x)) \<longrightarrow> snd(x) \<in> snd(fst(x))), a)) &
+ (\<lambda>a. (Ord(a) \<and>
+ ClEx(\<lambda>x. \<not> (snd(x) \<subseteq> fst(fst(x)) \<longrightarrow> snd(x) \<in> snd(fst(x))), a)) \<and>
ClEx(\<lambda>x. \<forall>z. M(z) \<longrightarrow> z \<subseteq> fst(x) \<longrightarrow> z \<in> snd(x), a),
- \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<subseteq> x \<longrightarrow> z \<in> y),
+ \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) \<longrightarrow> z \<subseteq> x \<longrightarrow> z \<in> y),
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x \<longrightarrow> z \<in> y)"
by fast
text\<open>Example 2''. We expand the subset relation.\<close>
schematic_goal
"Reflects(?Cl,
- \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> (\<forall>w. M(w) \<longrightarrow> w\<in>z \<longrightarrow> w\<in>x) \<longrightarrow> z\<in>y),
+ \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) \<longrightarrow> (\<forall>w. M(w) \<longrightarrow> w\<in>z \<longrightarrow> w\<in>x) \<longrightarrow> z\<in>y),
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). (\<forall>w\<in>Mset(a). w\<in>z \<longrightarrow> w\<in>x) \<longrightarrow> z\<in>y)"
by fast
text\<open>Example 2'''. Single-step version, to reveal the reflecting class.\<close>
schematic_goal
"Reflects(?Cl,
- \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<subseteq> x \<longrightarrow> z \<in> y),
+ \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) \<longrightarrow> z \<subseteq> x \<longrightarrow> z \<in> y),
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x \<longrightarrow> z \<in> y)"
apply (rule Ex_reflection)
txt\<open>
@@ -339,21 +338,21 @@
if \<^term>\<open>P\<close> is quantifier-free, since it is not being relativized.\<close>
schematic_goal
"Reflects(?Cl,
- \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<in> y \<longleftrightarrow> z \<in> x & P(z)),
- \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<in> y \<longleftrightarrow> z \<in> x & P(z))"
+ \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) \<longrightarrow> z \<in> y \<longleftrightarrow> z \<in> x \<and> P(z)),
+ \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<in> y \<longleftrightarrow> z \<in> x \<and> P(z))"
by fast
text\<open>Example 3'\<close>
schematic_goal
"Reflects(?Cl,
- \<lambda>x. \<exists>y. M(y) & y = Collect(x,P),
+ \<lambda>x. \<exists>y. M(y) \<and> y = Collect(x,P),
\<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))"
by fast
text\<open>Example 3''\<close>
schematic_goal
"Reflects(?Cl,
- \<lambda>x. \<exists>y. M(y) & y = Replace(x,P),
+ \<lambda>x. \<exists>y. M(y) \<and> y = Replace(x,P),
\<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))"
by fast
@@ -361,7 +360,7 @@
to be relativized.\<close>
schematic_goal
"Reflects(?Cl,
- \<lambda>A. 0\<notin>A \<longrightarrow> (\<exists>f. M(f) & f \<in> (\<Prod>X \<in> A. X)),
+ \<lambda>A. 0\<notin>A \<longrightarrow> (\<exists>f. M(f) \<and> f \<in> (\<Prod>X \<in> A. X)),
\<lambda>a A. 0\<notin>A \<longrightarrow> (\<exists>f\<in>Mset(a). f \<in> (\<Prod>X \<in> A. X)))"
by fast