--- a/src/ZF/Constructible/DPow_absolute.thy Tue Mar 06 16:46:27 2012 +0000
+++ b/src/ZF/Constructible/DPow_absolute.thy Tue Mar 06 17:01:37 2012 +0000
@@ -40,13 +40,13 @@
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) <->
+ ==> 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) <->
+ ==> 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])
@@ -55,14 +55,14 @@
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) <->
+ ==> 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) <-> sats(A, formula_rec_fm(p,i,k), env)"
+ ==> 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:
@@ -90,7 +90,7 @@
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) <->
+ ==> 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_satisfies_MH_fm
sats_formula_rec_fm)
@@ -98,7 +98,7 @@
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) <-> sats(A, satisfies_fm(i,j,k), env)"
+ ==> is_satisfies(##A, x, y, z) \<longleftrightarrow> sats(A, satisfies_fm(i,j,k), env)"
by (simp add: sats_satisfies_fm)
theorem satisfies_reflection:
@@ -124,12 +124,12 @@
is_DPow_sats :: "[i=>o,i,i,i,i] => o" where
"is_DPow_sats(M,A,env,p,x) ==
\<forall>n1[M]. \<forall>e[M]. \<forall>sp[M].
- is_satisfies(M,A,p,sp) --> is_Cons(M,x,env,e) -->
- fun_apply(M, sp, e, n1) --> number1(M, n1)"
+ 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) <-> sats(A, p, Cons(x,env))"
+ ==> 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)
@@ -146,8 +146,8 @@
(* is_DPow_sats(M,A,env,p,x) ==
\<forall>n1[M]. \<forall>e[M]. \<forall>sp[M].
- is_satisfies(M,A,p,sp) --> is_Cons(M,x,env,e) -->
- fun_apply(M, sp, e, n1) --> number1(M, n1) *)
+ 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
@@ -164,14 +164,14 @@
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) <->
+ ==> 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) <->
+ ==> is_DPow_sats(##A,nu,nx,ny,nz) \<longleftrightarrow>
sats(A, DPow_sats_fm(u,x,y,z), env)"
by simp
@@ -223,13 +223,13 @@
definition
is_DPow' :: "[i=>o,i,i] => o" where
"is_DPow'(M,A,Z) ==
- \<forall>X[M]. X \<in> Z <->
+ \<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) <-> Z = DPow'(A)"
+ "[|M(A); M(Z)|] ==> 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)
@@ -310,7 +310,7 @@
enclosed within a single quantifier.*}
(* is_Collect :: "[i=>o,i,i=>o,i] => o"
- "is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z <-> x \<in> A & P(x)" *)
+ "is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> A & P(x)" *)
definition
Collect_fm :: "[i, i, i]=>i" where
@@ -325,20 +325,20 @@
lemma sats_Collect_fm:
assumes is_P_iff_sats:
- "!!a. a \<in> A ==> is_P(a) <-> sats(A, p, Cons(a, env))"
+ "!!a. a \<in> A ==> 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) <->
+ ==> 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) <-> sats(A, p, Cons(a, env))"
+ "!!a. a \<in> A ==> 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) <-> sats(A, Collect_fm(i,p,j), env)"
+ ==> 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])
@@ -361,7 +361,7 @@
and not the usual 1, 0! It is enclosed within two quantifiers.*}
(* is_Replace :: "[i=>o,i,[i,i]=>o,i] => o"
- "is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & P(x,u))" *)
+ "is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z \<longleftrightarrow> (\<exists>x[M]. x\<in>A & P(x,u))" *)
definition
Replace_fm :: "[i, i, i]=>i" where
@@ -377,21 +377,21 @@
lemma sats_Replace_fm:
assumes is_P_iff_sats:
"!!a b. [|a \<in> A; b \<in> A|]
- ==> is_P(a,b) <-> sats(A, p, Cons(a,Cons(b,env)))"
+ ==> 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) <->
+ ==> 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) <-> sats(A, p, Cons(a,Cons(b,env)))"
+ ==> 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) <-> sats(A, Replace_fm(i,p,j), env)"
+ ==> 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])
@@ -412,7 +412,7 @@
subsubsection{*The Operator @{term is_DPow'}, Internalized*}
(* "is_DPow'(M,A,Z) ==
- \<forall>X[M]. X \<in> Z <->
+ \<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))" *)
@@ -435,14 +435,14 @@
lemma sats_DPow'_fm [simp]:
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
- ==> sats(A, DPow'_fm(x,y), env) <->
+ ==> 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) <-> sats(A, DPow'_fm(i,j), env)"
+ ==> is_DPow'(##A, x, y) \<longleftrightarrow> sats(A, DPow'_fm(i,j), env)"
by (simp add: sats_DPow'_fm)
theorem DPow'_reflection:
@@ -463,7 +463,7 @@
lemma (in M_DPow) transrec_body_abs:
"[|M(x); M(g); M(z)|]
- ==> transrec_body(M,g,x,y,z) <-> y \<in> x & z = DPow'(g`y)"
+ ==> 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 +
@@ -490,7 +490,7 @@
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) <->
+ ==> 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)
@@ -517,7 +517,7 @@
lemma (in M_Lset) Lset_abs:
"[|Ord(i); M(i); M(z)|]
- ==> is_Lset(M,i,z) <-> z = Lset(i)"
+ ==> 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)