--- a/src/ZF/Constructible/Rank_Separation.thy Tue Sep 27 16:51:35 2022 +0100
+++ b/src/ZF/Constructible/Rank_Separation.thy Tue Sep 27 17:03:23 2022 +0100
@@ -18,15 +18,15 @@
lemma well_ord_iso_Reflects:
"REFLECTS[\<lambda>x. x\<in>A \<longrightarrow>
- (\<exists>y[L]. \<exists>p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r),
+ (\<exists>y[L]. \<exists>p[L]. fun_apply(L,f,x,y) \<and> pair(L,y,x,p) \<and> p \<in> r),
\<lambda>i x. x\<in>A \<longrightarrow> (\<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)]"
+ fun_apply(##Lset(i),f,x,y) \<and> pair(##Lset(i),y,x,p) \<and> p \<in> r)]"
by (intro FOL_reflections function_reflections)
lemma well_ord_iso_separation:
"\<lbrakk>L(A); L(f); L(r)\<rbrakk>
\<Longrightarrow> separation (L, \<lambda>x. x\<in>A \<longrightarrow> (\<exists>y[L]. (\<exists>p[L].
- fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r)))"
+ fun_apply(L,f,x,y) \<and> pair(L,y,x,p) \<and> p \<in> r)))"
apply (rule gen_separation_multi [OF well_ord_iso_Reflects, of "{A,f,r}"],
auto)
apply (rule_tac env="[A,f,r]" in DPow_LsetI)
@@ -38,10 +38,10 @@
lemma obase_reflects:
"REFLECTS[\<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
- ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
+ ordinal(L,x) \<and> membership(L,x,mx) \<and> pred_set(L,A,a,r,par) \<and>
order_isomorphism(L,par,r,x,mx,g),
\<lambda>i a. \<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). \<exists>par \<in> Lset(i).
- ordinal(##Lset(i),x) & membership(##Lset(i),x,mx) & pred_set(##Lset(i),A,a,r,par) &
+ ordinal(##Lset(i),x) \<and> membership(##Lset(i),x,mx) \<and> pred_set(##Lset(i),A,a,r,par) \<and>
order_isomorphism(##Lset(i),par,r,x,mx,g)]"
by (intro FOL_reflections function_reflections fun_plus_reflections)
@@ -49,7 +49,7 @@
\<comment> \<open>part of the order type formalization\<close>
"\<lbrakk>L(A); L(r)\<rbrakk>
\<Longrightarrow> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
- ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
+ ordinal(L,x) \<and> membership(L,x,mx) \<and> pred_set(L,A,a,r,par) \<and>
order_isomorphism(L,par,r,x,mx,g))"
apply (rule gen_separation_multi [OF obase_reflects, of "{A,r}"], auto)
apply (rule_tac env="[A,r]" in DPow_LsetI)
@@ -61,20 +61,20 @@
lemma obase_equals_reflects:
"REFLECTS[\<lambda>x. x\<in>A \<longrightarrow> \<not>(\<exists>y[L]. \<exists>g[L].
- ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L].
- membership(L,y,my) & pred_set(L,A,x,r,pxr) &
+ ordinal(L,y) \<and> (\<exists>my[L]. \<exists>pxr[L].
+ membership(L,y,my) \<and> pred_set(L,A,x,r,pxr) \<and>
order_isomorphism(L,pxr,r,y,my,g))),
\<lambda>i x. x\<in>A \<longrightarrow> \<not>(\<exists>y \<in> Lset(i). \<exists>g \<in> Lset(i).
- ordinal(##Lset(i),y) & (\<exists>my \<in> Lset(i). \<exists>pxr \<in> Lset(i).
- membership(##Lset(i),y,my) & pred_set(##Lset(i),A,x,r,pxr) &
+ ordinal(##Lset(i),y) \<and> (\<exists>my \<in> Lset(i). \<exists>pxr \<in> Lset(i).
+ membership(##Lset(i),y,my) \<and> pred_set(##Lset(i),A,x,r,pxr) \<and>
order_isomorphism(##Lset(i),pxr,r,y,my,g)))]"
by (intro FOL_reflections function_reflections fun_plus_reflections)
lemma obase_equals_separation:
"\<lbrakk>L(A); L(r)\<rbrakk>
\<Longrightarrow> separation (L, \<lambda>x. x\<in>A \<longrightarrow> \<not>(\<exists>y[L]. \<exists>g[L].
- ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L].
- membership(L,y,my) & pred_set(L,A,x,r,pxr) &
+ ordinal(L,y) \<and> (\<exists>my[L]. \<exists>pxr[L].
+ membership(L,y,my) \<and> pred_set(L,A,x,r,pxr) \<and>
order_isomorphism(L,pxr,r,y,my,g))))"
apply (rule gen_separation_multi [OF obase_equals_reflects, of "{A,r}"], auto)
apply (rule_tac env="[A,r]" in DPow_LsetI)
@@ -85,13 +85,13 @@
subsubsection\<open>Replacement for \<^term>\<open>omap\<close>\<close>
lemma omap_reflects:
- "REFLECTS[\<lambda>z. \<exists>a[L]. a\<in>B & (\<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
- ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) &
- pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g)),
- \<lambda>i z. \<exists>a \<in> Lset(i). a\<in>B & (\<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i).
+ "REFLECTS[\<lambda>z. \<exists>a[L]. a\<in>B \<and> (\<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
+ ordinal(L,x) \<and> pair(L,a,x,z) \<and> membership(L,x,mx) \<and>
+ pred_set(L,A,a,r,par) \<and> order_isomorphism(L,par,r,x,mx,g)),
+ \<lambda>i z. \<exists>a \<in> Lset(i). a\<in>B \<and> (\<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i).
\<exists>par \<in> Lset(i).
- ordinal(##Lset(i),x) & pair(##Lset(i),a,x,z) &
- membership(##Lset(i),x,mx) & pred_set(##Lset(i),A,a,r,par) &
+ ordinal(##Lset(i),x) \<and> pair(##Lset(i),a,x,z) \<and>
+ membership(##Lset(i),x,mx) \<and> pred_set(##Lset(i),A,a,r,par) \<and>
order_isomorphism(##Lset(i),par,r,x,mx,g))]"
by (intro FOL_reflections function_reflections fun_plus_reflections)
@@ -99,8 +99,8 @@
"\<lbrakk>L(A); L(r)\<rbrakk>
\<Longrightarrow> strong_replacement(L,
\<lambda>a z. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
- ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) &
- pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))"
+ ordinal(L,x) \<and> pair(L,a,x,z) \<and> membership(L,x,mx) \<and>
+ pred_set(L,A,a,r,par) \<and> order_isomorphism(L,par,r,x,mx,g))"
apply (rule strong_replacementI)
apply (rule_tac u="{A,r,B}" in gen_separation_multi [OF omap_reflects], auto)
apply (rule_tac env="[A,B,r]" in DPow_LsetI)
@@ -153,15 +153,15 @@
subsubsection\<open>Replacement for \<^term>\<open>wfrank\<close>\<close>
lemma wfrank_replacement_Reflects:
- "REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A &
+ "REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A \<and>
(\<forall>rplus[L]. tran_closure(L,r,rplus) \<longrightarrow>
- (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z) &
- M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
+ (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z) \<and>
+ M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) \<and>
is_range(L,f,y))),
- \<lambda>i z. \<exists>x \<in> Lset(i). x \<in> A &
+ \<lambda>i z. \<exists>x \<in> Lset(i). x \<in> A \<and>
(\<forall>rplus \<in> Lset(i). tran_closure(##Lset(i),r,rplus) \<longrightarrow>
- (\<exists>y \<in> Lset(i). \<exists>f \<in> Lset(i). pair(##Lset(i),x,y,z) &
- M_is_recfun(##Lset(i), %x f y. is_range(##Lset(i),f,y), rplus, x, f) &
+ (\<exists>y \<in> Lset(i). \<exists>f \<in> Lset(i). pair(##Lset(i),x,y,z) \<and>
+ M_is_recfun(##Lset(i), %x f y. is_range(##Lset(i),f,y), rplus, x, f) \<and>
is_range(##Lset(i),f,y)))]"
by (intro FOL_reflections function_reflections fun_plus_reflections
is_recfun_reflection tran_closure_reflection)
@@ -170,8 +170,8 @@
"L(r) \<Longrightarrow>
strong_replacement(L, \<lambda>x z.
\<forall>rplus[L]. tran_closure(L,r,rplus) \<longrightarrow>
- (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z) &
- M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
+ (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z) \<and>
+ M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) \<and>
is_range(L,f,y)))"
apply (rule strong_replacementI)
apply (rule_tac u="{r,B}"