--- a/src/ZF/Constructible/DPow_absolute.thy Tue Sep 27 13:34:54 2022 +0200
+++ b/src/ZF/Constructible/DPow_absolute.thy Tue Sep 27 16:51:35 2022 +0100
@@ -13,10 +13,10 @@
subsubsection\<open>The Operator \<^term>\<open>is_formula_rec\<close>\<close>
text\<open>The three arguments of \<^term>\<open>p\<close> are always 2, 1, 0. It is buried
- within 11 quantifiers!!\<close>
+ within 11 quantifiers\<And>\<close>
(* is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o"
- "is_formula_rec(M,MH,p,z) ==
+ "is_formula_rec(M,MH,p,z) \<equiv>
\<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) &
2 1 0
successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"
@@ -24,7 +24,7 @@
definition
formula_rec_fm :: "[i, i, i]=>i" where
- "formula_rec_fm(mh,p,z) ==
+ "formula_rec_fm(mh,p,z) \<equiv>
Exists(Exists(Exists(
And(finite_ordinal_fm(2),
And(depth_fm(p#+3,2),
@@ -32,42 +32,42 @@
And(fun_apply_fm(0,p#+3,z#+3), is_transrec_fm(mh,1,0))))))))"
lemma is_formula_rec_type [TC]:
- "[| p \<in> formula; x \<in> nat; z \<in> nat |]
- ==> formula_rec_fm(p,x,z) \<in> formula"
+ "\<lbrakk>p \<in> formula; x \<in> nat; z \<in> nat\<rbrakk>
+ \<Longrightarrow> formula_rec_fm(p,x,z) \<in> formula"
by (simp add: formula_rec_fm_def)
lemma sats_formula_rec_fm:
assumes MH_iff_sats:
- "!!a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10.
- [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>A; a8\<in>A; a9\<in>A; a10\<in>A|]
- ==> MH(a2, a1, a0) \<longleftrightarrow>
+ "\<And>a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10.
+ \<lbrakk>a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>A; a8\<in>A; a9\<in>A; a10\<in>A\<rbrakk>
+ \<Longrightarrow> MH(a2, a1, a0) \<longleftrightarrow>
sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,
Cons(a4,Cons(a5,Cons(a6,Cons(a7,
Cons(a8,Cons(a9,Cons(a10,env))))))))))))"
shows
- "[|x \<in> nat; z \<in> nat; env \<in> list(A)|]
- ==> sats(A, formula_rec_fm(p,x,z), env) \<longleftrightarrow>
+ "\<lbrakk>x \<in> nat; z \<in> nat; env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> sats(A, formula_rec_fm(p,x,z), env) \<longleftrightarrow>
is_formula_rec(##A, MH, nth(x,env), nth(z,env))"
by (simp add: formula_rec_fm_def sats_is_transrec_fm is_formula_rec_def
MH_iff_sats [THEN iff_sym])
lemma formula_rec_iff_sats:
assumes MH_iff_sats:
- "!!a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10.
- [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>A; a8\<in>A; a9\<in>A; a10\<in>A|]
- ==> MH(a2, a1, a0) \<longleftrightarrow>
+ "\<And>a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10.
+ \<lbrakk>a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>A; a8\<in>A; a9\<in>A; a10\<in>A\<rbrakk>
+ \<Longrightarrow> MH(a2, a1, a0) \<longleftrightarrow>
sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,
Cons(a4,Cons(a5,Cons(a6,Cons(a7,
Cons(a8,Cons(a9,Cons(a10,env))))))))))))"
shows
- "[|nth(i,env) = x; nth(k,env) = z;
- i \<in> nat; k \<in> nat; env \<in> list(A)|]
- ==> is_formula_rec(##A, MH, x, z) \<longleftrightarrow> sats(A, formula_rec_fm(p,i,k), env)"
+ "\<lbrakk>nth(i,env) = x; nth(k,env) = z;
+ i \<in> nat; k \<in> nat; env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> is_formula_rec(##A, MH, x, z) \<longleftrightarrow> sats(A, formula_rec_fm(p,i,k), env)"
by (simp add: sats_formula_rec_fm [OF MH_iff_sats])
theorem formula_rec_reflection:
assumes MH_reflection:
- "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)),
+ "\<And>f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)),
\<lambda>i x. MH(##Lset(i), f'(x), f(x), g(x), h(x))]"
shows "REFLECTS[\<lambda>x. is_formula_rec(L, MH(L,x), f(x), h(x)),
\<lambda>i x. is_formula_rec(##Lset(i), MH(##Lset(i),x), f(x), h(x))]"
@@ -79,25 +79,25 @@
subsubsection\<open>The Operator \<^term>\<open>is_satisfies\<close>\<close>
-(* is_satisfies(M,A,p,z) == is_formula_rec (M, satisfies_MH(M,A), p, z) *)
+(* is_satisfies(M,A,p,z) \<equiv> is_formula_rec (M, satisfies_MH(M,A), p, z) *)
definition
satisfies_fm :: "[i,i,i]=>i" where
- "satisfies_fm(x) == formula_rec_fm (satisfies_MH_fm(x#+5#+6, 2, 1, 0))"
+ "satisfies_fm(x) \<equiv> formula_rec_fm (satisfies_MH_fm(x#+5#+6, 2, 1, 0))"
lemma is_satisfies_type [TC]:
- "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> satisfies_fm(x,y,z) \<in> formula"
+ "\<lbrakk>x \<in> nat; y \<in> nat; z \<in> nat\<rbrakk> \<Longrightarrow> satisfies_fm(x,y,z) \<in> formula"
by (simp add: satisfies_fm_def)
lemma sats_satisfies_fm [simp]:
- "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
- ==> sats(A, satisfies_fm(x,y,z), env) \<longleftrightarrow>
+ "\<lbrakk>x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> sats(A, satisfies_fm(x,y,z), env) \<longleftrightarrow>
is_satisfies(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: satisfies_fm_def is_satisfies_def sats_formula_rec_fm)
lemma satisfies_iff_sats:
- "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
- i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
- ==> is_satisfies(##A, x, y, z) \<longleftrightarrow> sats(A, satisfies_fm(i,j,k), env)"
+ "\<lbrakk>nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
+ i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> is_satisfies(##A, x, y, z) \<longleftrightarrow> sats(A, satisfies_fm(i,j,k), env)"
by (simp)
theorem satisfies_reflection:
@@ -121,56 +121,56 @@
(the comprehension).\<close>
definition
is_DPow_sats :: "[i=>o,i,i,i,i] => o" where
- "is_DPow_sats(M,A,env,p,x) ==
+ "is_DPow_sats(M,A,env,p,x) \<equiv>
\<forall>n1[M]. \<forall>e[M]. \<forall>sp[M].
is_satisfies(M,A,p,sp) \<longrightarrow> is_Cons(M,x,env,e) \<longrightarrow>
fun_apply(M, sp, e, n1) \<longrightarrow> number1(M, n1)"
lemma (in M_satisfies) DPow_sats_abs:
- "[| M(A); env \<in> list(A); p \<in> formula; M(x) |]
- ==> is_DPow_sats(M,A,env,p,x) \<longleftrightarrow> sats(A, p, Cons(x,env))"
+ "\<lbrakk>M(A); env \<in> list(A); p \<in> formula; M(x)\<rbrakk>
+ \<Longrightarrow> is_DPow_sats(M,A,env,p,x) \<longleftrightarrow> sats(A, p, Cons(x,env))"
apply (subgoal_tac "M(env)")
apply (simp add: is_DPow_sats_def satisfies_closed satisfies_abs)
apply (blast dest: transM)
done
lemma (in M_satisfies) Collect_DPow_sats_abs:
- "[| M(A); env \<in> list(A); p \<in> formula |]
- ==> Collect(A, is_DPow_sats(M,A,env,p)) =
+ "\<lbrakk>M(A); env \<in> list(A); p \<in> formula\<rbrakk>
+ \<Longrightarrow> Collect(A, is_DPow_sats(M,A,env,p)) =
{x \<in> A. sats(A, p, Cons(x,env))}"
by (simp add: DPow_sats_abs transM [of _ A])
subsubsection\<open>The Operator \<^term>\<open>is_DPow_sats\<close>, Internalized\<close>
-(* is_DPow_sats(M,A,env,p,x) ==
+(* is_DPow_sats(M,A,env,p,x) \<equiv>
\<forall>n1[M]. \<forall>e[M]. \<forall>sp[M].
is_satisfies(M,A,p,sp) \<longrightarrow> is_Cons(M,x,env,e) \<longrightarrow>
fun_apply(M, sp, e, n1) \<longrightarrow> number1(M, n1) *)
definition
DPow_sats_fm :: "[i,i,i,i]=>i" where
- "DPow_sats_fm(A,env,p,x) ==
+ "DPow_sats_fm(A,env,p,x) \<equiv>
Forall(Forall(Forall(
Implies(satisfies_fm(A#+3,p#+3,0),
Implies(Cons_fm(x#+3,env#+3,1),
Implies(fun_apply_fm(0,1,2), number1_fm(2)))))))"
lemma is_DPow_sats_type [TC]:
- "[| A \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
- ==> DPow_sats_fm(A,x,y,z) \<in> formula"
+ "\<lbrakk>A \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat\<rbrakk>
+ \<Longrightarrow> DPow_sats_fm(A,x,y,z) \<in> formula"
by (simp add: DPow_sats_fm_def)
lemma sats_DPow_sats_fm [simp]:
- "[| u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
- ==> sats(A, DPow_sats_fm(u,x,y,z), env) \<longleftrightarrow>
+ "\<lbrakk>u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> sats(A, DPow_sats_fm(u,x,y,z), env) \<longleftrightarrow>
is_DPow_sats(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
by (simp add: DPow_sats_fm_def is_DPow_sats_def)
lemma DPow_sats_iff_sats:
- "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
- u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
- ==> is_DPow_sats(##A,nu,nx,ny,nz) \<longleftrightarrow>
+ "\<lbrakk>nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
+ u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> is_DPow_sats(##A,nu,nx,ny,nz) \<longleftrightarrow>
sats(A, DPow_sats_fm(u,x,y,z), env)"
by simp
@@ -187,23 +187,23 @@
locale M_DPow = M_satisfies +
assumes sep:
- "[| M(A); env \<in> list(A); p \<in> formula |]
- ==> separation(M, \<lambda>x. is_DPow_sats(M,A,env,p,x))"
+ "\<lbrakk>M(A); env \<in> list(A); p \<in> formula\<rbrakk>
+ \<Longrightarrow> separation(M, \<lambda>x. is_DPow_sats(M,A,env,p,x))"
and rep:
"M(A)
- ==> strong_replacement (M,
+ \<Longrightarrow> strong_replacement (M,
\<lambda>ep z. \<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
pair(M,env,p,ep) &
is_Collect(M, A, \<lambda>x. is_DPow_sats(M,A,env,p,x), z))"
lemma (in M_DPow) sep':
- "[| M(A); env \<in> list(A); p \<in> formula |]
- ==> separation(M, \<lambda>x. sats(A, p, Cons(x,env)))"
+ "\<lbrakk>M(A); env \<in> list(A); p \<in> formula\<rbrakk>
+ \<Longrightarrow> separation(M, \<lambda>x. sats(A, p, Cons(x,env)))"
by (insert sep [of A env p], simp add: DPow_sats_abs)
lemma (in M_DPow) rep':
"M(A)
- ==> strong_replacement (M,
+ \<Longrightarrow> strong_replacement (M,
\<lambda>ep z. \<exists>env\<in>list(A). \<exists>p\<in>formula.
ep = <env,p> & z = {x \<in> A . sats(A, p, Cons(x, env))})"
by (insert rep [of A], simp add: Collect_DPow_sats_abs)
@@ -213,7 +213,7 @@
"univalent (M, A, \<lambda>xy z. \<exists>x\<in>B. \<exists>y\<in>C. xy = \<langle>x,y\<rangle> \<and> z = f(x,y))"
by (simp add: univalent_def, blast)
-lemma (in M_DPow) DPow'_closed: "M(A) ==> M(DPow'(A))"
+lemma (in M_DPow) DPow'_closed: "M(A) \<Longrightarrow> M(DPow'(A))"
apply (simp add: DPow'_eq)
apply (fast intro: rep' sep' univalent_pair_eq)
done
@@ -221,14 +221,14 @@
text\<open>Relativization of the Operator \<^term>\<open>DPow'\<close>\<close>
definition
is_DPow' :: "[i=>o,i,i] => o" where
- "is_DPow'(M,A,Z) ==
+ "is_DPow'(M,A,Z) \<equiv>
\<forall>X[M]. X \<in> Z \<longleftrightarrow>
subset(M,X,A) &
(\<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
is_Collect(M, A, is_DPow_sats(M,A,env,p), X))"
lemma (in M_DPow) DPow'_abs:
- "[|M(A); M(Z)|] ==> is_DPow'(M,A,Z) \<longleftrightarrow> Z = DPow'(A)"
+ "\<lbrakk>M(A); M(Z)\<rbrakk> \<Longrightarrow> is_DPow'(M,A,Z) \<longleftrightarrow> Z = DPow'(A)"
apply (rule iffI)
prefer 2 apply (simp add: is_DPow'_def DPow'_def Collect_DPow_sats_abs)
apply (rule M_equalityI)
@@ -242,8 +242,8 @@
subsubsection\<open>The Instance of Separation\<close>
lemma DPow_separation:
- "[| L(A); env \<in> list(A); p \<in> formula |]
- ==> separation(L, \<lambda>x. is_DPow_sats(L,A,env,p,x))"
+ "\<lbrakk>L(A); env \<in> list(A); p \<in> formula\<rbrakk>
+ \<Longrightarrow> separation(L, \<lambda>x. is_DPow_sats(L,A,env,p,x))"
apply (rule gen_separation_multi [OF DPow_sats_reflection, of "{A,env,p}"],
auto intro: transL)
apply (rule_tac env="[A,env,p]" in DPow_LsetI)
@@ -271,7 +271,7 @@
lemma DPow_replacement:
"L(A)
- ==> strong_replacement (L,
+ \<Longrightarrow> strong_replacement (L,
\<lambda>ep z. \<exists>env[L]. \<exists>p[L]. mem_formula(L,p) & mem_list(L,A,env) &
pair(L,env,p,ep) &
is_Collect(L, A, \<lambda>x. is_DPow_sats(L,A,env,p,x), z))"
@@ -309,35 +309,35 @@
enclosed within a single quantifier.\<close>
(* is_Collect :: "[i=>o,i,i=>o,i] => o"
- "is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> A & P(x)" *)
+ "is_Collect(M,A,P,z) \<equiv> \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> A & P(x)" *)
definition
Collect_fm :: "[i, i, i]=>i" where
- "Collect_fm(A,is_P,z) ==
+ "Collect_fm(A,is_P,z) \<equiv>
Forall(Iff(Member(0,succ(z)),
And(Member(0,succ(A)), is_P)))"
lemma is_Collect_type [TC]:
- "[| is_P \<in> formula; x \<in> nat; y \<in> nat |]
- ==> Collect_fm(x,is_P,y) \<in> formula"
+ "\<lbrakk>is_P \<in> formula; x \<in> nat; y \<in> nat\<rbrakk>
+ \<Longrightarrow> Collect_fm(x,is_P,y) \<in> formula"
by (simp add: Collect_fm_def)
lemma sats_Collect_fm:
assumes is_P_iff_sats:
- "!!a. a \<in> A ==> is_P(a) \<longleftrightarrow> sats(A, p, Cons(a, env))"
+ "\<And>a. a \<in> A \<Longrightarrow> is_P(a) \<longleftrightarrow> sats(A, p, Cons(a, env))"
shows
- "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
- ==> sats(A, Collect_fm(x,p,y), env) \<longleftrightarrow>
+ "\<lbrakk>x \<in> nat; y \<in> nat; env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> sats(A, Collect_fm(x,p,y), env) \<longleftrightarrow>
is_Collect(##A, nth(x,env), is_P, nth(y,env))"
by (simp add: Collect_fm_def is_Collect_def is_P_iff_sats [THEN iff_sym])
lemma Collect_iff_sats:
assumes is_P_iff_sats:
- "!!a. a \<in> A ==> is_P(a) \<longleftrightarrow> sats(A, p, Cons(a, env))"
+ "\<And>a. a \<in> A \<Longrightarrow> is_P(a) \<longleftrightarrow> sats(A, p, Cons(a, env))"
shows
- "[| nth(i,env) = x; nth(j,env) = y;
- i \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> is_Collect(##A, x, is_P, y) \<longleftrightarrow> sats(A, Collect_fm(i,p,j), env)"
+ "\<lbrakk>nth(i,env) = x; nth(j,env) = y;
+ i \<in> nat; j \<in> nat; env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> is_Collect(##A, x, is_P, y) \<longleftrightarrow> sats(A, Collect_fm(i,p,j), env)"
by (simp add: sats_Collect_fm [OF is_P_iff_sats])
@@ -345,7 +345,7 @@
which is essential for handling free variable references.\<close>
theorem Collect_reflection:
assumes is_P_reflection:
- "!!h f g. REFLECTS[\<lambda>x. is_P(L, f(x), g(x)),
+ "\<And>h f g. REFLECTS[\<lambda>x. is_P(L, f(x), g(x)),
\<lambda>i x. is_P(##Lset(i), f(x), g(x))]"
shows "REFLECTS[\<lambda>x. is_Collect(L, f(x), is_P(L,x), g(x)),
\<lambda>i x. is_Collect(##Lset(i), f(x), is_P(##Lset(i), x), g(x))]"
@@ -360,37 +360,37 @@
and not the usual 1, 0! It is enclosed within two quantifiers.\<close>
(* is_Replace :: "[i=>o,i,[i,i]=>o,i] => o"
- "is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z \<longleftrightarrow> (\<exists>x[M]. x\<in>A & P(x,u))" *)
+ "is_Replace(M,A,P,z) \<equiv> \<forall>u[M]. u \<in> z \<longleftrightarrow> (\<exists>x[M]. x\<in>A & P(x,u))" *)
definition
Replace_fm :: "[i, i, i]=>i" where
- "Replace_fm(A,is_P,z) ==
+ "Replace_fm(A,is_P,z) \<equiv>
Forall(Iff(Member(0,succ(z)),
Exists(And(Member(0,A#+2), is_P))))"
lemma is_Replace_type [TC]:
- "[| is_P \<in> formula; x \<in> nat; y \<in> nat |]
- ==> Replace_fm(x,is_P,y) \<in> formula"
+ "\<lbrakk>is_P \<in> formula; x \<in> nat; y \<in> nat\<rbrakk>
+ \<Longrightarrow> Replace_fm(x,is_P,y) \<in> formula"
by (simp add: Replace_fm_def)
lemma sats_Replace_fm:
assumes is_P_iff_sats:
- "!!a b. [|a \<in> A; b \<in> A|]
- ==> is_P(a,b) \<longleftrightarrow> sats(A, p, Cons(a,Cons(b,env)))"
+ "\<And>a b. \<lbrakk>a \<in> A; b \<in> A\<rbrakk>
+ \<Longrightarrow> is_P(a,b) \<longleftrightarrow> sats(A, p, Cons(a,Cons(b,env)))"
shows
- "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
- ==> sats(A, Replace_fm(x,p,y), env) \<longleftrightarrow>
+ "\<lbrakk>x \<in> nat; y \<in> nat; env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> sats(A, Replace_fm(x,p,y), env) \<longleftrightarrow>
is_Replace(##A, nth(x,env), is_P, nth(y,env))"
by (simp add: Replace_fm_def is_Replace_def is_P_iff_sats [THEN iff_sym])
lemma Replace_iff_sats:
assumes is_P_iff_sats:
- "!!a b. [|a \<in> A; b \<in> A|]
- ==> is_P(a,b) \<longleftrightarrow> sats(A, p, Cons(a,Cons(b,env)))"
+ "\<And>a b. \<lbrakk>a \<in> A; b \<in> A\<rbrakk>
+ \<Longrightarrow> is_P(a,b) \<longleftrightarrow> sats(A, p, Cons(a,Cons(b,env)))"
shows
- "[| nth(i,env) = x; nth(j,env) = y;
- i \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> is_Replace(##A, x, is_P, y) \<longleftrightarrow> sats(A, Replace_fm(i,p,j), env)"
+ "\<lbrakk>nth(i,env) = x; nth(j,env) = y;
+ i \<in> nat; j \<in> nat; env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> is_Replace(##A, x, is_P, y) \<longleftrightarrow> sats(A, Replace_fm(i,p,j), env)"
by (simp add: sats_Replace_fm [OF is_P_iff_sats])
@@ -398,7 +398,7 @@
which is essential for handling free variable references.\<close>
theorem Replace_reflection:
assumes is_P_reflection:
- "!!h f g. REFLECTS[\<lambda>x. is_P(L, f(x), g(x), h(x)),
+ "\<And>h f g. REFLECTS[\<lambda>x. is_P(L, f(x), g(x), h(x)),
\<lambda>i x. is_P(##Lset(i), f(x), g(x), h(x))]"
shows "REFLECTS[\<lambda>x. is_Replace(L, f(x), is_P(L,x), g(x)),
\<lambda>i x. is_Replace(##Lset(i), f(x), is_P(##Lset(i), x), g(x))]"
@@ -410,7 +410,7 @@
subsubsection\<open>The Operator \<^term>\<open>is_DPow'\<close>, Internalized\<close>
-(* "is_DPow'(M,A,Z) ==
+(* "is_DPow'(M,A,Z) \<equiv>
\<forall>X[M]. X \<in> Z \<longleftrightarrow>
subset(M,X,A) &
(\<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
@@ -418,7 +418,7 @@
definition
DPow'_fm :: "[i,i]=>i" where
- "DPow'_fm(A,Z) ==
+ "DPow'_fm(A,Z) \<equiv>
Forall(
Iff(Member(0,succ(Z)),
And(subset_fm(0,succ(A)),
@@ -429,19 +429,19 @@
DPow_sats_fm(A#+4, 2, 1, 0), 2))))))))"
lemma is_DPow'_type [TC]:
- "[| x \<in> nat; y \<in> nat |] ==> DPow'_fm(x,y) \<in> formula"
+ "\<lbrakk>x \<in> nat; y \<in> nat\<rbrakk> \<Longrightarrow> DPow'_fm(x,y) \<in> formula"
by (simp add: DPow'_fm_def)
lemma sats_DPow'_fm [simp]:
- "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
- ==> sats(A, DPow'_fm(x,y), env) \<longleftrightarrow>
+ "\<lbrakk>x \<in> nat; y \<in> nat; env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> sats(A, DPow'_fm(x,y), env) \<longleftrightarrow>
is_DPow'(##A, nth(x,env), nth(y,env))"
by (simp add: DPow'_fm_def is_DPow'_def sats_subset_fm' sats_Collect_fm)
lemma DPow'_iff_sats:
- "[| nth(i,env) = x; nth(j,env) = y;
- i \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> is_DPow'(##A, x, y) \<longleftrightarrow> sats(A, DPow'_fm(i,j), env)"
+ "\<lbrakk>nth(i,env) = x; nth(j,env) = y;
+ i \<in> nat; j \<in> nat; env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> is_DPow'(##A, x, y) \<longleftrightarrow> sats(A, DPow'_fm(i,j), env)"
by (simp)
theorem DPow'_reflection:
@@ -457,39 +457,39 @@
definition
transrec_body :: "[i=>o,i,i,i,i] => o" where
- "transrec_body(M,g,x) ==
+ "transrec_body(M,g,x) \<equiv>
\<lambda>y z. \<exists>gy[M]. y \<in> x & fun_apply(M,g,y,gy) & is_DPow'(M,gy,z)"
lemma (in M_DPow) transrec_body_abs:
- "[|M(x); M(g); M(z)|]
- ==> transrec_body(M,g,x,y,z) \<longleftrightarrow> y \<in> x & z = DPow'(g`y)"
+ "\<lbrakk>M(x); M(g); M(z)\<rbrakk>
+ \<Longrightarrow> transrec_body(M,g,x,y,z) \<longleftrightarrow> y \<in> x & z = DPow'(g`y)"
by (simp add: transrec_body_def DPow'_abs transM [of _ x])
locale M_Lset = M_DPow +
assumes strong_rep:
- "[|M(x); M(g)|] ==> strong_replacement(M, \<lambda>y z. transrec_body(M,g,x,y,z))"
+ "\<lbrakk>M(x); M(g)\<rbrakk> \<Longrightarrow> strong_replacement(M, \<lambda>y z. transrec_body(M,g,x,y,z))"
and transrec_rep:
- "M(i) ==> transrec_replacement(M, \<lambda>x f u.
+ "M(i) \<Longrightarrow> transrec_replacement(M, \<lambda>x f u.
\<exists>r[M]. is_Replace(M, x, transrec_body(M,f,x), r) &
big_union(M, r, u), i)"
lemma (in M_Lset) strong_rep':
- "[|M(x); M(g)|]
- ==> strong_replacement(M, \<lambda>y z. y \<in> x & z = DPow'(g`y))"
+ "\<lbrakk>M(x); M(g)\<rbrakk>
+ \<Longrightarrow> strong_replacement(M, \<lambda>y z. y \<in> x & z = DPow'(g`y))"
by (insert strong_rep [of x g], simp add: transrec_body_abs)
lemma (in M_Lset) DPow_apply_closed:
- "[|M(f); M(x); y\<in>x|] ==> M(DPow'(f`y))"
+ "\<lbrakk>M(f); M(x); y\<in>x\<rbrakk> \<Longrightarrow> M(DPow'(f`y))"
by (blast intro: DPow'_closed dest: transM)
lemma (in M_Lset) RepFun_DPow_apply_closed:
- "[|M(f); M(x)|] ==> M({DPow'(f`y). y\<in>x})"
+ "\<lbrakk>M(f); M(x)\<rbrakk> \<Longrightarrow> M({DPow'(f`y). y\<in>x})"
by (blast intro: DPow_apply_closed RepFun_closed2 strong_rep')
lemma (in M_Lset) RepFun_DPow_abs:
- "[|M(x); M(f); M(r) |]
- ==> is_Replace(M, x, \<lambda>y z. transrec_body(M,f,x,y,z), r) \<longleftrightarrow>
+ "\<lbrakk>M(x); M(f); M(r)\<rbrakk>
+ \<Longrightarrow> is_Replace(M, x, \<lambda>y z. transrec_body(M,f,x,y,z), r) \<longleftrightarrow>
r = {DPow'(f`y). y\<in>x}"
apply (simp add: transrec_body_abs RepFun_def)
apply (rule iff_trans)
@@ -498,7 +498,7 @@
done
lemma (in M_Lset) transrec_rep':
- "M(i) ==> transrec_replacement(M, \<lambda>x f u. u = (\<Union>y\<in>x. DPow'(f ` y)), i)"
+ "M(i) \<Longrightarrow> transrec_replacement(M, \<lambda>x f u. u = (\<Union>y\<in>x. DPow'(f ` y)), i)"
apply (insert transrec_rep [of i])
apply (simp add: RepFun_DPow_apply_closed RepFun_DPow_abs
transrec_replacement_def)
@@ -512,18 +512,18 @@
\<comment> \<open>We can use the term language below because \<^term>\<open>is_Lset\<close> will
not have to be internalized: it isn't used in any instance of
separation.\<close>
- "is_Lset(M,a,z) == is_transrec(M, %x f u. u = (\<Union>y\<in>x. DPow'(f`y)), a, z)"
+ "is_Lset(M,a,z) \<equiv> is_transrec(M, %x f u. u = (\<Union>y\<in>x. DPow'(f`y)), a, z)"
lemma (in M_Lset) Lset_abs:
- "[|Ord(i); M(i); M(z)|]
- ==> is_Lset(M,i,z) \<longleftrightarrow> z = Lset(i)"
+ "\<lbrakk>Ord(i); M(i); M(z)\<rbrakk>
+ \<Longrightarrow> is_Lset(M,i,z) \<longleftrightarrow> z = Lset(i)"
apply (simp add: is_Lset_def Lset_eq_transrec_DPow')
apply (rule transrec_abs)
apply (simp_all add: transrec_rep' relation2_def RepFun_DPow_apply_closed)
done
lemma (in M_Lset) Lset_closed:
- "[|Ord(i); M(i)|] ==> M(Lset(i))"
+ "\<lbrakk>Ord(i); M(i)\<rbrakk> \<Longrightarrow> M(Lset(i))"
apply (simp add: Lset_eq_transrec_DPow')
apply (rule transrec_closed [OF transrec_rep'])
apply (simp_all add: relation2_def RepFun_DPow_apply_closed)
@@ -542,7 +542,7 @@
by (intro FOL_reflections function_reflections DPow'_reflection)
lemma strong_rep:
- "[|L(x); L(g)|] ==> strong_replacement(L, \<lambda>y z. transrec_body(L,g,x,y,z))"
+ "\<lbrakk>L(x); L(g)\<rbrakk> \<Longrightarrow> strong_replacement(L, \<lambda>y z. transrec_body(L,g,x,y,z))"
apply (unfold transrec_body_def)
apply (rule strong_replacementI)
apply (rule_tac u="{x,g,B}"
@@ -577,8 +577,8 @@
lemma transrec_rep:
- "[|L(j)|]
- ==> transrec_replacement(L, \<lambda>x f u.
+ "\<lbrakk>L(j)\<rbrakk>
+ \<Longrightarrow> transrec_replacement(L, \<lambda>x f u.
\<exists>r[L]. is_Replace(L, x, transrec_body(L,f,x), r) &
big_union(L, r, u), j)"
apply (rule L.transrec_replacementI, assumption)
@@ -614,7 +614,7 @@
definition
constructible :: "[i=>o,i] => o" where
- "constructible(M,x) ==
+ "constructible(M,x) \<equiv>
\<exists>i[M]. \<exists>Li[M]. ordinal(M,i) & is_Lset(M,i,Li) & x \<in> Li"
theorem V_equals_L_in_L: