--- a/src/ZF/Constructible/Rank_Separation.thy Tue Sep 27 13:34:54 2022 +0200
+++ b/src/ZF/Constructible/Rank_Separation.thy Tue Sep 27 16:51:35 2022 +0100
@@ -24,8 +24,8 @@
by (intro FOL_reflections function_reflections)
lemma well_ord_iso_separation:
- "[| L(A); L(f); L(r) |]
- ==> separation (L, \<lambda>x. x\<in>A \<longrightarrow> (\<exists>y[L]. (\<exists>p[L].
+ "\<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)))"
apply (rule gen_separation_multi [OF well_ord_iso_Reflects, of "{A,f,r}"],
auto)
@@ -47,8 +47,8 @@
lemma obase_separation:
\<comment> \<open>part of the order type formalization\<close>
- "[| L(A); L(r) |]
- ==> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
+ "\<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) &
order_isomorphism(L,par,r,x,mx,g))"
apply (rule gen_separation_multi [OF obase_reflects, of "{A,r}"], auto)
@@ -60,19 +60,19 @@
subsubsection\<open>Separation for a Theorem about \<^term>\<open>obase\<close>\<close>
lemma obase_equals_reflects:
- "REFLECTS[\<lambda>x. x\<in>A \<longrightarrow> ~(\<exists>y[L]. \<exists>g[L].
+ "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) &
order_isomorphism(L,pxr,r,y,my,g))),
- \<lambda>i x. x\<in>A \<longrightarrow> ~(\<exists>y \<in> Lset(i). \<exists>g \<in> Lset(i).
+ \<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) &
order_isomorphism(##Lset(i),pxr,r,y,my,g)))]"
by (intro FOL_reflections function_reflections fun_plus_reflections)
lemma obase_equals_separation:
- "[| L(A); L(r) |]
- ==> separation (L, \<lambda>x. x\<in>A \<longrightarrow> ~(\<exists>y[L]. \<exists>g[L].
+ "\<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) &
order_isomorphism(L,pxr,r,y,my,g))))"
@@ -96,8 +96,8 @@
by (intro FOL_reflections function_reflections fun_plus_reflections)
lemma omap_replacement:
- "[| L(A); L(r) |]
- ==> strong_replacement(L,
+ "\<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))"
@@ -133,17 +133,17 @@
lemma wfrank_Reflects:
"REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) \<longrightarrow>
- ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)),
+ \<not> (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)),
\<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(##Lset(i),r,rplus) \<longrightarrow>
- ~ (\<exists>f \<in> Lset(i).
+ \<not> (\<exists>f \<in> Lset(i).
M_is_recfun(##Lset(i), %x f y. is_range(##Lset(i),f,y),
rplus, x, f))]"
by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection)
lemma wfrank_separation:
- "L(r) ==>
+ "L(r) \<Longrightarrow>
separation (L, \<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) \<longrightarrow>
- ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))"
+ \<not> (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))"
apply (rule gen_separation [OF wfrank_Reflects], simp)
apply (rule_tac env="[r]" in DPow_LsetI)
apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+
@@ -167,7 +167,7 @@
is_recfun_reflection tran_closure_reflection)
lemma wfrank_strong_replacement:
- "L(r) ==>
+ "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) &
@@ -186,12 +186,12 @@
lemma Ord_wfrank_Reflects:
"REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) \<longrightarrow>
- ~ (\<forall>f[L]. \<forall>rangef[L].
+ \<not> (\<forall>f[L]. \<forall>rangef[L].
is_range(L,f,rangef) \<longrightarrow>
M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) \<longrightarrow>
ordinal(L,rangef)),
\<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(##Lset(i),r,rplus) \<longrightarrow>
- ~ (\<forall>f \<in> Lset(i). \<forall>rangef \<in> Lset(i).
+ \<not> (\<forall>f \<in> Lset(i). \<forall>rangef \<in> Lset(i).
is_range(##Lset(i),f,rangef) \<longrightarrow>
M_is_recfun(##Lset(i), \<lambda>x f y. is_range(##Lset(i),f,y),
rplus, x, f) \<longrightarrow>
@@ -200,10 +200,10 @@
tran_closure_reflection ordinal_reflection)
lemma Ord_wfrank_separation:
- "L(r) ==>
+ "L(r) \<Longrightarrow>
separation (L, \<lambda>x.
\<forall>rplus[L]. tran_closure(L,r,rplus) \<longrightarrow>
- ~ (\<forall>f[L]. \<forall>rangef[L].
+ \<not> (\<forall>f[L]. \<forall>rangef[L].
is_range(L,f,rangef) \<longrightarrow>
M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) \<longrightarrow>
ordinal(L,rangef)))"