--- a/src/ZF/Constructible/DPow_absolute.thy Wed Feb 05 13:35:32 2003 +0100
+++ b/src/ZF/Constructible/DPow_absolute.thy Thu Feb 06 11:01:05 2003 +0100
@@ -47,7 +47,7 @@
shows
"[|x \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, formula_rec_fm(p,x,z), env) <->
- is_formula_rec(**A, MH, nth(x,env), nth(z,env))"
+ 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])
@@ -62,15 +62,15 @@
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) <-> 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)),
- \<lambda>i x. MH(**Lset(i), 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))]"
+ \<lambda>i x. is_formula_rec(##Lset(i), MH(##Lset(i),x), f(x), h(x))]"
apply (simp (no_asm_use) only: is_formula_rec_def)
apply (intro FOL_reflections function_reflections fun_plus_reflections
depth_reflection is_transrec_reflection MH_reflection)
@@ -90,19 +90,19 @@
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) <->
- is_satisfies(**A, nth(x,env), nth(y,env), nth(z,env))"
+ 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)
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) <-> sats(A, satisfies_fm(i,j,k), env)"
by (simp add: sats_satisfies_fm)
theorem satisfies_reflection:
"REFLECTS[\<lambda>x. is_satisfies(L,f(x),g(x),h(x)),
- \<lambda>i x. is_satisfies(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. is_satisfies(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: is_satisfies_def)
apply (intro formula_rec_reflection satisfies_MH_reflection)
done
@@ -163,19 +163,19 @@
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) <->
- is_DPow_sats(**A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
+ 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) <->
sats(A, DPow_sats_fm(u,x,y,z), env)"
by simp
theorem DPow_sats_reflection:
"REFLECTS[\<lambda>x. is_DPow_sats(L,f(x),g(x),h(x),g'(x)),
- \<lambda>i x. is_DPow_sats(**Lset(i),f(x),g(x),h(x),g'(x))]"
+ \<lambda>i x. is_DPow_sats(##Lset(i),f(x),g(x),h(x),g'(x))]"
apply (unfold is_DPow_sats_def)
apply (intro FOL_reflections function_reflections extra_reflections
satisfies_reflection)
@@ -260,9 +260,9 @@
is_Collect (L, A, is_DPow_sats(L,A,env,p), x)),
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B &
(\<exists>env \<in> Lset(i). \<exists>p \<in> Lset(i).
- mem_formula(**Lset(i),p) & mem_list(**Lset(i),A,env) &
- pair(**Lset(i),env,p,u) &
- is_Collect (**Lset(i), A, is_DPow_sats(**Lset(i),A,env,p), x))]"
+ mem_formula(##Lset(i),p) & mem_list(##Lset(i),A,env) &
+ pair(##Lset(i),env,p,u) &
+ is_Collect (##Lset(i), A, is_DPow_sats(##Lset(i),A,env,p), x))]"
apply (unfold is_Collect_def)
apply (intro FOL_reflections function_reflections mem_formula_reflection
mem_list_reflection DPow_sats_reflection)
@@ -326,7 +326,7 @@
shows
"[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
==> sats(A, Collect_fm(x,p,y), env) <->
- is_Collect(**A, nth(x,env), is_P, nth(y,env))"
+ 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:
@@ -335,7 +335,7 @@
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) <-> sats(A, Collect_fm(i,p,j), env)"
by (simp add: sats_Collect_fm [OF is_P_iff_sats])
@@ -344,9 +344,9 @@
theorem Collect_reflection:
assumes is_P_reflection:
"!!h f g. REFLECTS[\<lambda>x. is_P(L, f(x), g(x)),
- \<lambda>i x. is_P(**Lset(i), 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))]"
+ \<lambda>i x. is_Collect(##Lset(i), f(x), is_P(##Lset(i), x), g(x))]"
apply (simp (no_asm_use) only: is_Collect_def)
apply (intro FOL_reflections is_P_reflection)
done
@@ -377,7 +377,7 @@
shows
"[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
==> sats(A, Replace_fm(x,p,y), env) <->
- is_Replace(**A, nth(x,env), is_P, nth(y,env))"
+ 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:
@@ -387,7 +387,7 @@
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) <-> sats(A, Replace_fm(i,p,j), env)"
by (simp add: sats_Replace_fm [OF is_P_iff_sats])
@@ -396,9 +396,9 @@
theorem Replace_reflection:
assumes is_P_reflection:
"!!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))]"
+ \<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))]"
+ \<lambda>i x. is_Replace(##Lset(i), f(x), is_P(##Lset(i), x), g(x))]"
apply (simp (no_asm_use) only: is_Replace_def)
apply (intro FOL_reflections is_P_reflection)
done
@@ -431,18 +431,18 @@
lemma sats_DPow'_fm [simp]:
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
==> sats(A, DPow'_fm(x,y), env) <->
- is_DPow'(**A, nth(x,env), nth(y,env))"
+ 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) <-> sats(A, DPow'_fm(i,j), env)"
by (simp add: sats_DPow'_fm)
theorem DPow'_reflection:
"REFLECTS[\<lambda>x. is_DPow'(L,f(x),g(x)),
- \<lambda>i x. is_DPow'(**Lset(i),f(x),g(x))]"
+ \<lambda>i x. is_DPow'(##Lset(i),f(x),g(x))]"
apply (simp only: is_DPow'_def)
apply (intro FOL_reflections function_reflections mem_formula_reflection
mem_list_reflection Collect_reflection DPow_sats_reflection)
@@ -534,7 +534,7 @@
"REFLECTS [\<lambda>u. \<exists>v[L]. v \<in> B & (\<exists>gy[L].
v \<in> x & fun_apply(L,g,v,gy) & is_DPow'(L,gy,u)),
\<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B & (\<exists>gy \<in> Lset(i).
- v \<in> x & fun_apply(**Lset(i),g,v,gy) & is_DPow'(**Lset(i),gy,u))]"
+ v \<in> x & fun_apply(##Lset(i),g,v,gy) & is_DPow'(##Lset(i),gy,u))]"
by (intro FOL_reflections function_reflections DPow'_reflection)
lemma strong_rep:
@@ -558,14 +558,14 @@
\<exists>gy[L]. y \<in> x & fun_apply(L,f,y,gy) &
is_DPow'(L,gy,z), r) & big_union(L,r,u), mr, v, y)),
\<lambda>i x. \<exists>v \<in> Lset(i). v \<in> B &
- (\<exists>y \<in> Lset(i). pair(**Lset(i),v,y,x) &
- is_wfrec (**Lset(i), \<lambda>x f u. \<exists>r \<in> Lset(i).
- is_Replace (**Lset(i), x, \<lambda>y z.
- \<exists>gy \<in> Lset(i). y \<in> x & fun_apply(**Lset(i),f,y,gy) &
- is_DPow'(**Lset(i),gy,z), r) &
- big_union(**Lset(i),r,u), mr, v, y))]"
+ (\<exists>y \<in> Lset(i). pair(##Lset(i),v,y,x) &
+ is_wfrec (##Lset(i), \<lambda>x f u. \<exists>r \<in> Lset(i).
+ is_Replace (##Lset(i), x, \<lambda>y z.
+ \<exists>gy \<in> Lset(i). y \<in> x & fun_apply(##Lset(i),f,y,gy) &
+ is_DPow'(##Lset(i),gy,z), r) &
+ big_union(##Lset(i),r,u), mr, v, y))]"
apply (simp only: rex_setclass_is_bex [symmetric])
- --{*Convert @{text "\<exists>y\<in>Lset(i)"} to @{text "\<exists>y[**Lset(i)]"} within the body
+ --{*Convert @{text "\<exists>y\<in>Lset(i)"} to @{text "\<exists>y[##Lset(i)]"} within the body
of the @{term is_wfrec} application. *}
apply (intro FOL_reflections function_reflections
is_wfrec_reflection Replace_reflection DPow'_reflection)
--- a/src/ZF/Constructible/Internalize.thy Wed Feb 05 13:35:32 2003 +0100
+++ b/src/ZF/Constructible/Internalize.thy Thu Feb 06 11:01:05 2003 +0100
@@ -19,18 +19,18 @@
lemma sats_Inl_fm [simp]:
"[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
- ==> sats(A, Inl_fm(x,z), env) <-> is_Inl(**A, nth(x,env), nth(z,env))"
+ ==> sats(A, Inl_fm(x,z), env) <-> is_Inl(##A, nth(x,env), nth(z,env))"
by (simp add: Inl_fm_def is_Inl_def)
lemma Inl_iff_sats:
"[| nth(i,env) = x; nth(k,env) = z;
i \<in> nat; k \<in> nat; env \<in> list(A)|]
- ==> is_Inl(**A, x, z) <-> sats(A, Inl_fm(i,k), env)"
+ ==> is_Inl(##A, x, z) <-> sats(A, Inl_fm(i,k), env)"
by simp
theorem Inl_reflection:
"REFLECTS[\<lambda>x. is_Inl(L,f(x),h(x)),
- \<lambda>i x. is_Inl(**Lset(i),f(x),h(x))]"
+ \<lambda>i x. is_Inl(##Lset(i),f(x),h(x))]"
apply (simp only: is_Inl_def)
apply (intro FOL_reflections function_reflections)
done
@@ -48,18 +48,18 @@
lemma sats_Inr_fm [simp]:
"[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
- ==> sats(A, Inr_fm(x,z), env) <-> is_Inr(**A, nth(x,env), nth(z,env))"
+ ==> sats(A, Inr_fm(x,z), env) <-> is_Inr(##A, nth(x,env), nth(z,env))"
by (simp add: Inr_fm_def is_Inr_def)
lemma Inr_iff_sats:
"[| nth(i,env) = x; nth(k,env) = z;
i \<in> nat; k \<in> nat; env \<in> list(A)|]
- ==> is_Inr(**A, x, z) <-> sats(A, Inr_fm(i,k), env)"
+ ==> is_Inr(##A, x, z) <-> sats(A, Inr_fm(i,k), env)"
by simp
theorem Inr_reflection:
"REFLECTS[\<lambda>x. is_Inr(L,f(x),h(x)),
- \<lambda>i x. is_Inr(**Lset(i),f(x),h(x))]"
+ \<lambda>i x. is_Inr(##Lset(i),f(x),h(x))]"
apply (simp only: is_Inr_def)
apply (intro FOL_reflections function_reflections)
done
@@ -77,17 +77,17 @@
lemma sats_Nil_fm [simp]:
"[| x \<in> nat; env \<in> list(A)|]
- ==> sats(A, Nil_fm(x), env) <-> is_Nil(**A, nth(x,env))"
+ ==> sats(A, Nil_fm(x), env) <-> is_Nil(##A, nth(x,env))"
by (simp add: Nil_fm_def is_Nil_def)
lemma Nil_iff_sats:
"[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
- ==> is_Nil(**A, x) <-> sats(A, Nil_fm(i), env)"
+ ==> is_Nil(##A, x) <-> sats(A, Nil_fm(i), env)"
by simp
theorem Nil_reflection:
"REFLECTS[\<lambda>x. is_Nil(L,f(x)),
- \<lambda>i x. is_Nil(**Lset(i),f(x))]"
+ \<lambda>i x. is_Nil(##Lset(i),f(x))]"
apply (simp only: is_Nil_def)
apply (intro FOL_reflections function_reflections Inl_reflection)
done
@@ -108,18 +108,18 @@
lemma sats_Cons_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, Cons_fm(x,y,z), env) <->
- is_Cons(**A, nth(x,env), nth(y,env), nth(z,env))"
+ is_Cons(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: Cons_fm_def is_Cons_def)
lemma Cons_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_Cons(**A, x, y, z) <-> sats(A, Cons_fm(i,j,k), env)"
+ ==>is_Cons(##A, x, y, z) <-> sats(A, Cons_fm(i,j,k), env)"
by simp
theorem Cons_reflection:
"REFLECTS[\<lambda>x. is_Cons(L,f(x),g(x),h(x)),
- \<lambda>i x. is_Cons(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. is_Cons(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: is_Cons_def)
apply (intro FOL_reflections pair_reflection Inr_reflection)
done
@@ -137,17 +137,17 @@
lemma sats_quasilist_fm [simp]:
"[| x \<in> nat; env \<in> list(A)|]
- ==> sats(A, quasilist_fm(x), env) <-> is_quasilist(**A, nth(x,env))"
+ ==> sats(A, quasilist_fm(x), env) <-> is_quasilist(##A, nth(x,env))"
by (simp add: quasilist_fm_def is_quasilist_def)
lemma quasilist_iff_sats:
"[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
- ==> is_quasilist(**A, x) <-> sats(A, quasilist_fm(i), env)"
+ ==> is_quasilist(##A, x) <-> sats(A, quasilist_fm(i), env)"
by simp
theorem quasilist_reflection:
"REFLECTS[\<lambda>x. is_quasilist(L,f(x)),
- \<lambda>i x. is_quasilist(**Lset(i),f(x))]"
+ \<lambda>i x. is_quasilist(##Lset(i),f(x))]"
apply (simp only: is_quasilist_def)
apply (intro FOL_reflections Nil_reflection Cons_reflection)
done
@@ -174,18 +174,18 @@
lemma sats_hd_fm [simp]:
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
- ==> sats(A, hd_fm(x,y), env) <-> is_hd(**A, nth(x,env), nth(y,env))"
+ ==> sats(A, hd_fm(x,y), env) <-> is_hd(##A, nth(x,env), nth(y,env))"
by (simp add: hd_fm_def is_hd_def)
lemma hd_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> is_hd(**A, x, y) <-> sats(A, hd_fm(i,j), env)"
+ ==> is_hd(##A, x, y) <-> sats(A, hd_fm(i,j), env)"
by simp
theorem hd_reflection:
"REFLECTS[\<lambda>x. is_hd(L,f(x),g(x)),
- \<lambda>i x. is_hd(**Lset(i),f(x),g(x))]"
+ \<lambda>i x. is_hd(##Lset(i),f(x),g(x))]"
apply (simp only: is_hd_def)
apply (intro FOL_reflections Nil_reflection Cons_reflection
quasilist_reflection empty_reflection)
@@ -210,18 +210,18 @@
lemma sats_tl_fm [simp]:
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
- ==> sats(A, tl_fm(x,y), env) <-> is_tl(**A, nth(x,env), nth(y,env))"
+ ==> sats(A, tl_fm(x,y), env) <-> is_tl(##A, nth(x,env), nth(y,env))"
by (simp add: tl_fm_def is_tl_def)
lemma tl_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> is_tl(**A, x, y) <-> sats(A, tl_fm(i,j), env)"
+ ==> is_tl(##A, x, y) <-> sats(A, tl_fm(i,j), env)"
by simp
theorem tl_reflection:
"REFLECTS[\<lambda>x. is_tl(L,f(x),g(x)),
- \<lambda>i x. is_tl(**Lset(i),f(x),g(x))]"
+ \<lambda>i x. is_tl(##Lset(i),f(x),g(x))]"
apply (simp only: is_tl_def)
apply (intro FOL_reflections Nil_reflection Cons_reflection
quasilist_reflection empty_reflection)
@@ -248,18 +248,18 @@
shows
"[|z \<in> nat; env \<in> list(A)|]
==> sats(A, bool_of_o_fm(p,z), env) <->
- is_bool_of_o(**A, P, nth(z,env))"
+ is_bool_of_o(##A, P, nth(z,env))"
by (simp add: bool_of_o_fm_def is_bool_of_o_def p_iff_sats [THEN iff_sym])
lemma is_bool_of_o_iff_sats:
"[| P <-> sats(A, p, env); nth(k,env) = z; k \<in> nat; env \<in> list(A)|]
- ==> is_bool_of_o(**A, P, z) <-> sats(A, bool_of_o_fm(p,k), env)"
+ ==> is_bool_of_o(##A, P, z) <-> sats(A, bool_of_o_fm(p,k), env)"
by (simp add: sats_bool_of_o_fm)
theorem bool_of_o_reflection:
- "REFLECTS [P(L), \<lambda>i. P(**Lset(i))] ==>
+ "REFLECTS [P(L), \<lambda>i. P(##Lset(i))] ==>
REFLECTS[\<lambda>x. is_bool_of_o(L, P(L,x), f(x)),
- \<lambda>i x. is_bool_of_o(**Lset(i), P(**Lset(i),x), f(x))]"
+ \<lambda>i x. is_bool_of_o(##Lset(i), P(##Lset(i),x), f(x))]"
apply (simp (no_asm) only: is_bool_of_o_def)
apply (intro FOL_reflections function_reflections, assumption+)
done
@@ -298,15 +298,15 @@
shows
"[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
==> sats(A, lambda_fm(p,x,y), env) <->
- is_lambda(**A, nth(x,env), is_b, nth(y,env))"
+ is_lambda(##A, nth(x,env), is_b, nth(y,env))"
by (simp add: lambda_fm_def is_lambda_def is_b_iff_sats [THEN iff_sym])
theorem is_lambda_reflection:
assumes is_b_reflection:
"!!f g h. REFLECTS[\<lambda>x. is_b(L, f(x), g(x), h(x)),
- \<lambda>i x. is_b(**Lset(i), f(x), g(x), h(x))]"
+ \<lambda>i x. is_b(##Lset(i), f(x), g(x), h(x))]"
shows "REFLECTS[\<lambda>x. is_lambda(L, A(x), is_b(L,x), f(x)),
- \<lambda>i x. is_lambda(**Lset(i), A(x), is_b(**Lset(i),x), f(x))]"
+ \<lambda>i x. is_lambda(##Lset(i), A(x), is_b(##Lset(i),x), f(x))]"
apply (simp (no_asm_use) only: is_lambda_def)
apply (intro FOL_reflections is_b_reflection pair_reflection)
done
@@ -327,18 +327,18 @@
lemma sats_Member_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, Member_fm(x,y,z), env) <->
- is_Member(**A, nth(x,env), nth(y,env), nth(z,env))"
+ is_Member(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: Member_fm_def is_Member_def)
lemma Member_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_Member(**A, x, y, z) <-> sats(A, Member_fm(i,j,k), env)"
+ ==> is_Member(##A, x, y, z) <-> sats(A, Member_fm(i,j,k), env)"
by (simp add: sats_Member_fm)
theorem Member_reflection:
"REFLECTS[\<lambda>x. is_Member(L,f(x),g(x),h(x)),
- \<lambda>i x. is_Member(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. is_Member(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: is_Member_def)
apply (intro FOL_reflections pair_reflection Inl_reflection)
done
@@ -359,18 +359,18 @@
lemma sats_Equal_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, Equal_fm(x,y,z), env) <->
- is_Equal(**A, nth(x,env), nth(y,env), nth(z,env))"
+ is_Equal(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: Equal_fm_def is_Equal_def)
lemma Equal_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_Equal(**A, x, y, z) <-> sats(A, Equal_fm(i,j,k), env)"
+ ==> is_Equal(##A, x, y, z) <-> sats(A, Equal_fm(i,j,k), env)"
by (simp add: sats_Equal_fm)
theorem Equal_reflection:
"REFLECTS[\<lambda>x. is_Equal(L,f(x),g(x),h(x)),
- \<lambda>i x. is_Equal(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. is_Equal(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: is_Equal_def)
apply (intro FOL_reflections pair_reflection Inl_reflection Inr_reflection)
done
@@ -391,18 +391,18 @@
lemma sats_Nand_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, Nand_fm(x,y,z), env) <->
- is_Nand(**A, nth(x,env), nth(y,env), nth(z,env))"
+ is_Nand(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: Nand_fm_def is_Nand_def)
lemma Nand_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_Nand(**A, x, y, z) <-> sats(A, Nand_fm(i,j,k), env)"
+ ==> is_Nand(##A, x, y, z) <-> sats(A, Nand_fm(i,j,k), env)"
by (simp add: sats_Nand_fm)
theorem Nand_reflection:
"REFLECTS[\<lambda>x. is_Nand(L,f(x),g(x),h(x)),
- \<lambda>i x. is_Nand(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. is_Nand(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: is_Nand_def)
apply (intro FOL_reflections pair_reflection Inl_reflection Inr_reflection)
done
@@ -421,18 +421,18 @@
lemma sats_Forall_fm [simp]:
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
==> sats(A, Forall_fm(x,y), env) <->
- is_Forall(**A, nth(x,env), nth(y,env))"
+ is_Forall(##A, nth(x,env), nth(y,env))"
by (simp add: Forall_fm_def is_Forall_def)
lemma Forall_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> is_Forall(**A, x, y) <-> sats(A, Forall_fm(i,j), env)"
+ ==> is_Forall(##A, x, y) <-> sats(A, Forall_fm(i,j), env)"
by (simp add: sats_Forall_fm)
theorem Forall_reflection:
"REFLECTS[\<lambda>x. is_Forall(L,f(x),g(x)),
- \<lambda>i x. is_Forall(**Lset(i),f(x),g(x))]"
+ \<lambda>i x. is_Forall(##Lset(i),f(x),g(x))]"
apply (simp only: is_Forall_def)
apply (intro FOL_reflections pair_reflection Inr_reflection)
done
@@ -454,18 +454,18 @@
lemma sats_and_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, and_fm(x,y,z), env) <->
- is_and(**A, nth(x,env), nth(y,env), nth(z,env))"
+ is_and(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: and_fm_def is_and_def)
lemma is_and_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_and(**A, x, y, z) <-> sats(A, and_fm(i,j,k), env)"
+ ==> is_and(##A, x, y, z) <-> sats(A, and_fm(i,j,k), env)"
by simp
theorem is_and_reflection:
"REFLECTS[\<lambda>x. is_and(L,f(x),g(x),h(x)),
- \<lambda>i x. is_and(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. is_and(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: is_and_def)
apply (intro FOL_reflections function_reflections)
done
@@ -488,18 +488,18 @@
lemma sats_or_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, or_fm(x,y,z), env) <->
- is_or(**A, nth(x,env), nth(y,env), nth(z,env))"
+ is_or(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: or_fm_def is_or_def)
lemma is_or_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_or(**A, x, y, z) <-> sats(A, or_fm(i,j,k), env)"
+ ==> is_or(##A, x, y, z) <-> sats(A, or_fm(i,j,k), env)"
by simp
theorem is_or_reflection:
"REFLECTS[\<lambda>x. is_or(L,f(x),g(x),h(x)),
- \<lambda>i x. is_or(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. is_or(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: is_or_def)
apply (intro FOL_reflections function_reflections)
done
@@ -521,18 +521,18 @@
lemma sats_is_not_fm [simp]:
"[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
- ==> sats(A, not_fm(x,z), env) <-> is_not(**A, nth(x,env), nth(z,env))"
+ ==> sats(A, not_fm(x,z), env) <-> is_not(##A, nth(x,env), nth(z,env))"
by (simp add: not_fm_def is_not_def)
lemma is_not_iff_sats:
"[| nth(i,env) = x; nth(k,env) = z;
i \<in> nat; k \<in> nat; env \<in> list(A)|]
- ==> is_not(**A, x, z) <-> sats(A, not_fm(i,k), env)"
+ ==> is_not(##A, x, z) <-> sats(A, not_fm(i,k), env)"
by simp
theorem is_not_reflection:
"REFLECTS[\<lambda>x. is_not(L,f(x),g(x)),
- \<lambda>i x. is_not(**Lset(i),f(x),g(x))]"
+ \<lambda>i x. is_not(##Lset(i),f(x),g(x))]"
apply (simp only: is_not_def)
apply (intro FOL_reflections function_reflections)
done
@@ -602,7 +602,7 @@
shows
"[|x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, is_recfun_fm(p,x,y,z), env) <->
- M_is_recfun(**A, MH, nth(x,env), nth(y,env), nth(z,env))"
+ M_is_recfun(##A, MH, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: is_recfun_fm_def M_is_recfun_iff MH_iff_sats [THEN iff_sym])
lemma is_recfun_iff_sats:
@@ -613,7 +613,7 @@
shows
"[| 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)|]
- ==> M_is_recfun(**A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)"
+ ==> M_is_recfun(##A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)"
by (simp add: sats_is_recfun_fm [OF MH_iff_sats])
text{*The additional variable in the premise, namely @{term f'}, is essential.
@@ -622,9 +622,9 @@
theorem is_recfun_reflection:
assumes MH_reflection:
"!!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))]"
+ \<lambda>i x. MH(##Lset(i), f'(x), f(x), g(x), h(x))]"
shows "REFLECTS[\<lambda>x. M_is_recfun(L, MH(L,x), f(x), g(x), h(x)),
- \<lambda>i x. M_is_recfun(**Lset(i), MH(**Lset(i),x), f(x), g(x), h(x))]"
+ \<lambda>i x. M_is_recfun(##Lset(i), MH(##Lset(i),x), f(x), g(x), h(x))]"
apply (simp (no_asm_use) only: M_is_recfun_def)
apply (intro FOL_reflections function_reflections
restriction_reflection MH_reflection)
@@ -663,7 +663,7 @@
shows
"[|x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
==> sats(A, is_wfrec_fm(p,x,y,z), env) <->
- is_wfrec(**A, MH, nth(x,env), nth(y,env), nth(z,env))"
+ is_wfrec(##A, MH, nth(x,env), nth(y,env), nth(z,env))"
apply (frule_tac x=z in lt_length_in_nat, assumption)
apply (frule lt_length_in_nat, assumption)
apply (simp add: is_wfrec_fm_def sats_is_recfun_fm is_wfrec_def MH_iff_sats [THEN iff_sym], blast)
@@ -678,15 +678,15 @@
shows
"[|nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
- ==> is_wfrec(**A, MH, x, y, z) <-> sats(A, is_wfrec_fm(p,i,j,k), env)"
+ ==> is_wfrec(##A, MH, x, y, z) <-> sats(A, is_wfrec_fm(p,i,j,k), env)"
by (simp add: sats_is_wfrec_fm [OF MH_iff_sats])
theorem is_wfrec_reflection:
assumes MH_reflection:
"!!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))]"
+ \<lambda>i x. MH(##Lset(i), f'(x), f(x), g(x), h(x))]"
shows "REFLECTS[\<lambda>x. is_wfrec(L, MH(L,x), f(x), g(x), h(x)),
- \<lambda>i x. is_wfrec(**Lset(i), MH(**Lset(i),x), f(x), g(x), h(x))]"
+ \<lambda>i x. is_wfrec(##Lset(i), MH(##Lset(i),x), f(x), g(x), h(x))]"
apply (simp (no_asm_use) only: is_wfrec_def)
apply (intro FOL_reflections MH_reflection is_recfun_reflection)
done
@@ -712,18 +712,18 @@
lemma sats_cartprod_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, cartprod_fm(x,y,z), env) <->
- cartprod(**A, nth(x,env), nth(y,env), nth(z,env))"
+ cartprod(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: cartprod_fm_def cartprod_def)
lemma cartprod_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)|]
- ==> cartprod(**A, x, y, z) <-> sats(A, cartprod_fm(i,j,k), env)"
+ ==> cartprod(##A, x, y, z) <-> sats(A, cartprod_fm(i,j,k), env)"
by (simp add: sats_cartprod_fm)
theorem cartprod_reflection:
"REFLECTS[\<lambda>x. cartprod(L,f(x),g(x),h(x)),
- \<lambda>i x. cartprod(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. cartprod(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: cartprod_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -751,18 +751,18 @@
lemma sats_sum_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, sum_fm(x,y,z), env) <->
- is_sum(**A, nth(x,env), nth(y,env), nth(z,env))"
+ is_sum(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: sum_fm_def is_sum_def)
lemma sum_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_sum(**A, x, y, z) <-> sats(A, sum_fm(i,j,k), env)"
+ ==> is_sum(##A, x, y, z) <-> sats(A, sum_fm(i,j,k), env)"
by simp
theorem sum_reflection:
"REFLECTS[\<lambda>x. is_sum(L,f(x),g(x),h(x)),
- \<lambda>i x. is_sum(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. is_sum(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: is_sum_def)
apply (intro FOL_reflections function_reflections cartprod_reflection)
done
@@ -780,18 +780,18 @@
lemma sats_quasinat_fm [simp]:
"[| x \<in> nat; env \<in> list(A)|]
- ==> sats(A, quasinat_fm(x), env) <-> is_quasinat(**A, nth(x,env))"
+ ==> sats(A, quasinat_fm(x), env) <-> is_quasinat(##A, nth(x,env))"
by (simp add: quasinat_fm_def is_quasinat_def)
lemma quasinat_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; env \<in> list(A)|]
- ==> is_quasinat(**A, x) <-> sats(A, quasinat_fm(i), env)"
+ ==> is_quasinat(##A, x) <-> sats(A, quasinat_fm(i), env)"
by simp
theorem quasinat_reflection:
"REFLECTS[\<lambda>x. is_quasinat(L,f(x)),
- \<lambda>i x. is_quasinat(**Lset(i),f(x))]"
+ \<lambda>i x. is_quasinat(##Lset(i),f(x))]"
apply (simp only: is_quasinat_def)
apply (intro FOL_reflections function_reflections)
done
@@ -828,7 +828,7 @@
shows
"[|x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|]
==> sats(A, is_nat_case_fm(x,p,y,z), env) <->
- is_nat_case(**A, nth(x,env), is_b, nth(y,env), nth(z,env))"
+ is_nat_case(##A, nth(x,env), is_b, nth(y,env), nth(z,env))"
apply (frule lt_length_in_nat, assumption)
apply (simp add: is_nat_case_fm_def is_nat_case_def is_b_iff_sats [THEN iff_sym])
done
@@ -838,7 +838,7 @@
sats(A, p, Cons(z, Cons(a,env))));
nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
- ==> is_nat_case(**A, x, is_b, y, z) <-> sats(A, is_nat_case_fm(i,p,j,k), env)"
+ ==> is_nat_case(##A, x, is_b, y, z) <-> sats(A, is_nat_case_fm(i,p,j,k), env)"
by (simp add: sats_is_nat_case_fm [of A is_b])
@@ -848,9 +848,9 @@
theorem is_nat_case_reflection:
assumes is_b_reflection:
"!!h f g. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x)),
- \<lambda>i x. is_b(**Lset(i), h(x), f(x), g(x))]"
+ \<lambda>i x. is_b(##Lset(i), h(x), f(x), g(x))]"
shows "REFLECTS[\<lambda>x. is_nat_case(L, f(x), is_b(L,x), g(x), h(x)),
- \<lambda>i x. is_nat_case(**Lset(i), f(x), is_b(**Lset(i), x), g(x), h(x))]"
+ \<lambda>i x. is_nat_case(##Lset(i), f(x), is_b(##Lset(i), x), g(x), h(x))]"
apply (simp (no_asm_use) only: is_nat_case_def)
apply (intro FOL_reflections function_reflections
restriction_reflection is_b_reflection quasinat_reflection)
@@ -884,7 +884,7 @@
shows
"[|v \<in> nat; x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|]
==> sats(A, iterates_MH_fm(p,v,x,y,z), env) <->
- iterates_MH(**A, is_F, nth(v,env), nth(x,env), nth(y,env), nth(z,env))"
+ iterates_MH(##A, is_F, nth(v,env), nth(x,env), nth(y,env), nth(z,env))"
apply (frule lt_length_in_nat, assumption)
apply (simp add: iterates_MH_fm_def iterates_MH_def sats_is_nat_case_fm
is_F_iff_sats [symmetric])
@@ -900,7 +900,7 @@
shows
"[| nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i' \<in> nat; i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
- ==> iterates_MH(**A, is_F, v, x, y, z) <->
+ ==> iterates_MH(##A, is_F, v, x, y, z) <->
sats(A, iterates_MH_fm(p,i',i,j,k), env)"
by (simp add: sats_iterates_MH_fm [OF is_F_iff_sats])
@@ -910,9 +910,9 @@
theorem iterates_MH_reflection:
assumes p_reflection:
"!!f g h. REFLECTS[\<lambda>x. p(L, h(x), f(x), g(x)),
- \<lambda>i x. p(**Lset(i), h(x), f(x), g(x))]"
+ \<lambda>i x. p(##Lset(i), h(x), f(x), g(x))]"
shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L,x), e(x), f(x), g(x), h(x)),
- \<lambda>i x. iterates_MH(**Lset(i), p(**Lset(i),x), e(x), f(x), g(x), h(x))]"
+ \<lambda>i x. iterates_MH(##Lset(i), p(##Lset(i),x), e(x), f(x), g(x), h(x))]"
apply (simp (no_asm_use) only: iterates_MH_def)
apply (intro FOL_reflections function_reflections is_nat_case_reflection
restriction_reflection p_reflection)
@@ -956,7 +956,7 @@
shows
"[|x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
==> sats(A, is_iterates_fm(p,x,y,z), env) <->
- is_iterates(**A, is_F, nth(x,env), nth(y,env), nth(z,env))"
+ is_iterates(##A, is_F, nth(x,env), nth(y,env), nth(z,env))"
apply (frule_tac x=z in lt_length_in_nat, assumption)
apply (frule lt_length_in_nat, assumption)
apply (simp add: is_iterates_fm_def is_iterates_def sats_is_nat_case_fm
@@ -975,7 +975,7 @@
shows
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
- ==> is_iterates(**A, is_F, x, y, z) <->
+ ==> is_iterates(##A, is_F, x, y, z) <->
sats(A, is_iterates_fm(p,i,j,k), env)"
by (simp add: sats_is_iterates_fm [OF is_F_iff_sats])
@@ -985,9 +985,9 @@
theorem is_iterates_reflection:
assumes p_reflection:
"!!f g h. REFLECTS[\<lambda>x. p(L, h(x), f(x), g(x)),
- \<lambda>i x. p(**Lset(i), h(x), f(x), g(x))]"
+ \<lambda>i x. p(##Lset(i), h(x), f(x), g(x))]"
shows "REFLECTS[\<lambda>x. is_iterates(L, p(L,x), f(x), g(x), h(x)),
- \<lambda>i x. is_iterates(**Lset(i), p(**Lset(i),x), f(x), g(x), h(x))]"
+ \<lambda>i x. is_iterates(##Lset(i), p(##Lset(i),x), f(x), g(x), h(x))]"
apply (simp (no_asm_use) only: is_iterates_def)
apply (intro FOL_reflections function_reflections p_reflection
is_wfrec_reflection iterates_MH_reflection)
@@ -1008,7 +1008,7 @@
lemma sats_eclose_n_fm [simp]:
"[| x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
==> sats(A, eclose_n_fm(x,y,z), env) <->
- is_eclose_n(**A, nth(x,env), nth(y,env), nth(z,env))"
+ is_eclose_n(##A, nth(x,env), nth(y,env), nth(z,env))"
apply (frule_tac x=z in lt_length_in_nat, assumption)
apply (frule_tac x=y in lt_length_in_nat, assumption)
apply (simp add: eclose_n_fm_def is_eclose_n_def
@@ -1018,12 +1018,12 @@
lemma eclose_n_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
- ==> is_eclose_n(**A, x, y, z) <-> sats(A, eclose_n_fm(i,j,k), env)"
+ ==> is_eclose_n(##A, x, y, z) <-> sats(A, eclose_n_fm(i,j,k), env)"
by (simp add: sats_eclose_n_fm)
theorem eclose_n_reflection:
"REFLECTS[\<lambda>x. is_eclose_n(L, f(x), g(x), h(x)),
- \<lambda>i x. is_eclose_n(**Lset(i), f(x), g(x), h(x))]"
+ \<lambda>i x. is_eclose_n(##Lset(i), f(x), g(x), h(x))]"
apply (simp only: is_eclose_n_def)
apply (intro FOL_reflections function_reflections is_iterates_reflection)
done
@@ -1046,18 +1046,18 @@
lemma sats_mem_eclose_fm [simp]:
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
- ==> sats(A, mem_eclose_fm(x,y), env) <-> mem_eclose(**A, nth(x,env), nth(y,env))"
+ ==> sats(A, mem_eclose_fm(x,y), env) <-> mem_eclose(##A, nth(x,env), nth(y,env))"
by (simp add: mem_eclose_fm_def mem_eclose_def)
lemma mem_eclose_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> mem_eclose(**A, x, y) <-> sats(A, mem_eclose_fm(i,j), env)"
+ ==> mem_eclose(##A, x, y) <-> sats(A, mem_eclose_fm(i,j), env)"
by simp
theorem mem_eclose_reflection:
"REFLECTS[\<lambda>x. mem_eclose(L,f(x),g(x)),
- \<lambda>i x. mem_eclose(**Lset(i),f(x),g(x))]"
+ \<lambda>i x. mem_eclose(##Lset(i),f(x),g(x))]"
apply (simp only: mem_eclose_def)
apply (intro FOL_reflections finite_ordinal_reflection eclose_n_reflection)
done
@@ -1076,18 +1076,18 @@
lemma sats_is_eclose_fm [simp]:
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
- ==> sats(A, is_eclose_fm(x,y), env) <-> is_eclose(**A, nth(x,env), nth(y,env))"
+ ==> sats(A, is_eclose_fm(x,y), env) <-> is_eclose(##A, nth(x,env), nth(y,env))"
by (simp add: is_eclose_fm_def is_eclose_def)
lemma is_eclose_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> is_eclose(**A, x, y) <-> sats(A, is_eclose_fm(i,j), env)"
+ ==> is_eclose(##A, x, y) <-> sats(A, is_eclose_fm(i,j), env)"
by simp
theorem is_eclose_reflection:
"REFLECTS[\<lambda>x. is_eclose(L,f(x),g(x)),
- \<lambda>i x. is_eclose(**Lset(i),f(x),g(x))]"
+ \<lambda>i x. is_eclose(##Lset(i),f(x),g(x))]"
apply (simp only: is_eclose_def)
apply (intro FOL_reflections mem_eclose_reflection)
done
@@ -1111,18 +1111,18 @@
lemma sats_list_functor_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, list_functor_fm(x,y,z), env) <->
- is_list_functor(**A, nth(x,env), nth(y,env), nth(z,env))"
+ is_list_functor(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: list_functor_fm_def is_list_functor_def)
lemma list_functor_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_list_functor(**A, x, y, z) <-> sats(A, list_functor_fm(i,j,k), env)"
+ ==> is_list_functor(##A, x, y, z) <-> sats(A, list_functor_fm(i,j,k), env)"
by simp
theorem list_functor_reflection:
"REFLECTS[\<lambda>x. is_list_functor(L,f(x),g(x),h(x)),
- \<lambda>i x. is_list_functor(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. is_list_functor(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: is_list_functor_def)
apply (intro FOL_reflections number1_reflection
cartprod_reflection sum_reflection)
@@ -1148,7 +1148,7 @@
lemma sats_list_N_fm [simp]:
"[| x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
==> sats(A, list_N_fm(x,y,z), env) <->
- is_list_N(**A, nth(x,env), nth(y,env), nth(z,env))"
+ is_list_N(##A, nth(x,env), nth(y,env), nth(z,env))"
apply (frule_tac x=z in lt_length_in_nat, assumption)
apply (frule_tac x=y in lt_length_in_nat, assumption)
apply (simp add: list_N_fm_def is_list_N_def sats_is_iterates_fm)
@@ -1157,12 +1157,12 @@
lemma list_N_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
- ==> is_list_N(**A, x, y, z) <-> sats(A, list_N_fm(i,j,k), env)"
+ ==> is_list_N(##A, x, y, z) <-> sats(A, list_N_fm(i,j,k), env)"
by (simp add: sats_list_N_fm)
theorem list_N_reflection:
"REFLECTS[\<lambda>x. is_list_N(L, f(x), g(x), h(x)),
- \<lambda>i x. is_list_N(**Lset(i), f(x), g(x), h(x))]"
+ \<lambda>i x. is_list_N(##Lset(i), f(x), g(x), h(x))]"
apply (simp only: is_list_N_def)
apply (intro FOL_reflections function_reflections
is_iterates_reflection list_functor_reflection)
@@ -1187,18 +1187,18 @@
lemma sats_mem_list_fm [simp]:
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
- ==> sats(A, mem_list_fm(x,y), env) <-> mem_list(**A, nth(x,env), nth(y,env))"
+ ==> sats(A, mem_list_fm(x,y), env) <-> mem_list(##A, nth(x,env), nth(y,env))"
by (simp add: mem_list_fm_def mem_list_def)
lemma mem_list_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> mem_list(**A, x, y) <-> sats(A, mem_list_fm(i,j), env)"
+ ==> mem_list(##A, x, y) <-> sats(A, mem_list_fm(i,j), env)"
by simp
theorem mem_list_reflection:
"REFLECTS[\<lambda>x. mem_list(L,f(x),g(x)),
- \<lambda>i x. mem_list(**Lset(i),f(x),g(x))]"
+ \<lambda>i x. mem_list(##Lset(i),f(x),g(x))]"
apply (simp only: mem_list_def)
apply (intro FOL_reflections finite_ordinal_reflection list_N_reflection)
done
@@ -1217,18 +1217,18 @@
lemma sats_is_list_fm [simp]:
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
- ==> sats(A, is_list_fm(x,y), env) <-> is_list(**A, nth(x,env), nth(y,env))"
+ ==> sats(A, is_list_fm(x,y), env) <-> is_list(##A, nth(x,env), nth(y,env))"
by (simp add: is_list_fm_def is_list_def)
lemma is_list_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> is_list(**A, x, y) <-> sats(A, is_list_fm(i,j), env)"
+ ==> is_list(##A, x, y) <-> sats(A, is_list_fm(i,j), env)"
by simp
theorem is_list_reflection:
"REFLECTS[\<lambda>x. is_list(L,f(x),g(x)),
- \<lambda>i x. is_list(**Lset(i),f(x),g(x))]"
+ \<lambda>i x. is_list(##Lset(i),f(x),g(x))]"
apply (simp only: is_list_def)
apply (intro FOL_reflections mem_list_reflection)
done
@@ -1259,18 +1259,18 @@
lemma sats_formula_functor_fm [simp]:
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
==> sats(A, formula_functor_fm(x,y), env) <->
- is_formula_functor(**A, nth(x,env), nth(y,env))"
+ is_formula_functor(##A, nth(x,env), nth(y,env))"
by (simp add: formula_functor_fm_def is_formula_functor_def)
lemma formula_functor_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> is_formula_functor(**A, x, y) <-> sats(A, formula_functor_fm(i,j), env)"
+ ==> is_formula_functor(##A, x, y) <-> sats(A, formula_functor_fm(i,j), env)"
by simp
theorem formula_functor_reflection:
"REFLECTS[\<lambda>x. is_formula_functor(L,f(x),g(x)),
- \<lambda>i x. is_formula_functor(**Lset(i),f(x),g(x))]"
+ \<lambda>i x. is_formula_functor(##Lset(i),f(x),g(x))]"
apply (simp only: is_formula_functor_def)
apply (intro FOL_reflections omega_reflection
cartprod_reflection sum_reflection)
@@ -1295,7 +1295,7 @@
lemma sats_formula_N_fm [simp]:
"[| x < length(env); y < length(env); env \<in> list(A)|]
==> sats(A, formula_N_fm(x,y), env) <->
- is_formula_N(**A, nth(x,env), nth(y,env))"
+ is_formula_N(##A, nth(x,env), nth(y,env))"
apply (frule_tac x=y in lt_length_in_nat, assumption)
apply (frule lt_length_in_nat, assumption)
apply (simp add: formula_N_fm_def is_formula_N_def sats_is_iterates_fm)
@@ -1304,12 +1304,12 @@
lemma formula_N_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i < length(env); j < length(env); env \<in> list(A)|]
- ==> is_formula_N(**A, x, y) <-> sats(A, formula_N_fm(i,j), env)"
+ ==> is_formula_N(##A, x, y) <-> sats(A, formula_N_fm(i,j), env)"
by (simp add: sats_formula_N_fm)
theorem formula_N_reflection:
"REFLECTS[\<lambda>x. is_formula_N(L, f(x), g(x)),
- \<lambda>i x. is_formula_N(**Lset(i), f(x), g(x))]"
+ \<lambda>i x. is_formula_N(##Lset(i), f(x), g(x))]"
apply (simp only: is_formula_N_def)
apply (intro FOL_reflections function_reflections
is_iterates_reflection formula_functor_reflection)
@@ -1334,17 +1334,17 @@
lemma sats_mem_formula_fm [simp]:
"[| x \<in> nat; env \<in> list(A)|]
- ==> sats(A, mem_formula_fm(x), env) <-> mem_formula(**A, nth(x,env))"
+ ==> sats(A, mem_formula_fm(x), env) <-> mem_formula(##A, nth(x,env))"
by (simp add: mem_formula_fm_def mem_formula_def)
lemma mem_formula_iff_sats:
"[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
- ==> mem_formula(**A, x) <-> sats(A, mem_formula_fm(i), env)"
+ ==> mem_formula(##A, x) <-> sats(A, mem_formula_fm(i), env)"
by simp
theorem mem_formula_reflection:
"REFLECTS[\<lambda>x. mem_formula(L,f(x)),
- \<lambda>i x. mem_formula(**Lset(i),f(x))]"
+ \<lambda>i x. mem_formula(##Lset(i),f(x))]"
apply (simp only: mem_formula_def)
apply (intro FOL_reflections finite_ordinal_reflection formula_N_reflection)
done
@@ -1363,17 +1363,17 @@
lemma sats_is_formula_fm [simp]:
"[| x \<in> nat; env \<in> list(A)|]
- ==> sats(A, is_formula_fm(x), env) <-> is_formula(**A, nth(x,env))"
+ ==> sats(A, is_formula_fm(x), env) <-> is_formula(##A, nth(x,env))"
by (simp add: is_formula_fm_def is_formula_def)
lemma is_formula_iff_sats:
"[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
- ==> is_formula(**A, x) <-> sats(A, is_formula_fm(i), env)"
+ ==> is_formula(##A, x) <-> sats(A, is_formula_fm(i), env)"
by simp
theorem is_formula_reflection:
"REFLECTS[\<lambda>x. is_formula(L,f(x)),
- \<lambda>i x. is_formula(**Lset(i),f(x))]"
+ \<lambda>i x. is_formula(##Lset(i),f(x))]"
apply (simp only: is_formula_def)
apply (intro FOL_reflections mem_formula_reflection)
done
@@ -1415,7 +1415,7 @@
shows
"[|x < length(env); z < length(env); env \<in> list(A)|]
==> sats(A, is_transrec_fm(p,x,z), env) <->
- is_transrec(**A, MH, nth(x,env), nth(z,env))"
+ is_transrec(##A, MH, nth(x,env), nth(z,env))"
apply (frule_tac x=z in lt_length_in_nat, assumption)
apply (frule_tac x=x in lt_length_in_nat, assumption)
apply (simp add: is_transrec_fm_def sats_is_wfrec_fm is_transrec_def MH_iff_sats [THEN iff_sym])
@@ -1432,15 +1432,15 @@
shows
"[|nth(i,env) = x; nth(k,env) = z;
i < length(env); k < length(env); env \<in> list(A)|]
- ==> is_transrec(**A, MH, x, z) <-> sats(A, is_transrec_fm(p,i,k), env)"
+ ==> is_transrec(##A, MH, x, z) <-> sats(A, is_transrec_fm(p,i,k), env)"
by (simp add: sats_is_transrec_fm [OF MH_iff_sats])
theorem is_transrec_reflection:
assumes MH_reflection:
"!!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))]"
+ \<lambda>i x. MH(##Lset(i), f'(x), f(x), g(x), h(x))]"
shows "REFLECTS[\<lambda>x. is_transrec(L, MH(L,x), f(x), h(x)),
- \<lambda>i x. is_transrec(**Lset(i), MH(**Lset(i),x), f(x), h(x))]"
+ \<lambda>i x. is_transrec(##Lset(i), MH(##Lset(i),x), f(x), h(x))]"
apply (simp (no_asm_use) only: is_transrec_def)
apply (intro FOL_reflections function_reflections MH_reflection
is_wfrec_reflection is_eclose_reflection)
--- a/src/ZF/Constructible/L_axioms.thy Wed Feb 05 13:35:32 2003 +0100
+++ b/src/ZF/Constructible/L_axioms.thy Thu Feb 06 11:01:05 2003 +0100
@@ -297,8 +297,8 @@
text{*This version handles an alternative form of the bounded quantifier
in the second argument of @{text REFLECTS}.*}
theorem Rex_reflection':
- "REFLECTS[ \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
- ==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z[**Lset(a)]. Q(a,x,z)]"
+ "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
+ ==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z[##Lset(a)]. Q(a,x,z)]"
apply (unfold setclass_def rex_def)
apply (erule Rex_reflection [unfolded rex_def Bex_def])
done
@@ -306,7 +306,7 @@
text{*As above.*}
theorem Rall_reflection':
"REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
- ==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z[**Lset(a)]. Q(a,x,z)]"
+ ==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z[##Lset(a)]. Q(a,x,z)]"
apply (unfold setclass_def rall_def)
apply (erule Rall_reflection [unfolded rall_def Ball_def])
done
@@ -369,18 +369,18 @@
lemma sats_empty_fm [simp]:
"[| x \<in> nat; env \<in> list(A)|]
- ==> sats(A, empty_fm(x), env) <-> empty(**A, nth(x,env))"
+ ==> sats(A, empty_fm(x), env) <-> empty(##A, nth(x,env))"
by (simp add: empty_fm_def empty_def)
lemma empty_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; env \<in> list(A)|]
- ==> empty(**A, x) <-> sats(A, empty_fm(i), env)"
+ ==> empty(##A, x) <-> sats(A, empty_fm(i), env)"
by simp
theorem empty_reflection:
"REFLECTS[\<lambda>x. empty(L,f(x)),
- \<lambda>i x. empty(**Lset(i),f(x))]"
+ \<lambda>i x. empty(##Lset(i),f(x))]"
apply (simp only: empty_def)
apply (intro FOL_reflections)
done
@@ -412,13 +412,13 @@
lemma sats_upair_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, upair_fm(x,y,z), env) <->
- upair(**A, nth(x,env), nth(y,env), nth(z,env))"
+ upair(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: upair_fm_def upair_def)
lemma upair_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)|]
- ==> upair(**A, x, y, z) <-> sats(A, upair_fm(i,j,k), env)"
+ ==> upair(##A, x, y, z) <-> sats(A, upair_fm(i,j,k), env)"
by (simp add: sats_upair_fm)
text{*Useful? At least it refers to "real" unordered pairs*}
@@ -433,7 +433,7 @@
theorem upair_reflection:
"REFLECTS[\<lambda>x. upair(L,f(x),g(x),h(x)),
- \<lambda>i x. upair(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. upair(##Lset(i),f(x),g(x),h(x))]"
apply (simp add: upair_def)
apply (intro FOL_reflections)
done
@@ -453,18 +453,18 @@
lemma sats_pair_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, pair_fm(x,y,z), env) <->
- pair(**A, nth(x,env), nth(y,env), nth(z,env))"
+ pair(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: pair_fm_def pair_def)
lemma pair_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)|]
- ==> pair(**A, x, y, z) <-> sats(A, pair_fm(i,j,k), env)"
+ ==> pair(##A, x, y, z) <-> sats(A, pair_fm(i,j,k), env)"
by (simp add: sats_pair_fm)
theorem pair_reflection:
"REFLECTS[\<lambda>x. pair(L,f(x),g(x),h(x)),
- \<lambda>i x. pair(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. pair(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: pair_def)
apply (intro FOL_reflections upair_reflection)
done
@@ -484,18 +484,18 @@
lemma sats_union_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, union_fm(x,y,z), env) <->
- union(**A, nth(x,env), nth(y,env), nth(z,env))"
+ union(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: union_fm_def union_def)
lemma union_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)|]
- ==> union(**A, x, y, z) <-> sats(A, union_fm(i,j,k), env)"
+ ==> union(##A, x, y, z) <-> sats(A, union_fm(i,j,k), env)"
by (simp add: sats_union_fm)
theorem union_reflection:
"REFLECTS[\<lambda>x. union(L,f(x),g(x),h(x)),
- \<lambda>i x. union(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. union(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: union_def)
apply (intro FOL_reflections)
done
@@ -516,18 +516,18 @@
lemma sats_cons_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, cons_fm(x,y,z), env) <->
- is_cons(**A, nth(x,env), nth(y,env), nth(z,env))"
+ is_cons(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: cons_fm_def is_cons_def)
lemma cons_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_cons(**A, x, y, z) <-> sats(A, cons_fm(i,j,k), env)"
+ ==> is_cons(##A, x, y, z) <-> sats(A, cons_fm(i,j,k), env)"
by simp
theorem cons_reflection:
"REFLECTS[\<lambda>x. is_cons(L,f(x),g(x),h(x)),
- \<lambda>i x. is_cons(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. is_cons(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: is_cons_def)
apply (intro FOL_reflections upair_reflection union_reflection)
done
@@ -545,18 +545,18 @@
lemma sats_succ_fm [simp]:
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
==> sats(A, succ_fm(x,y), env) <->
- successor(**A, nth(x,env), nth(y,env))"
+ successor(##A, nth(x,env), nth(y,env))"
by (simp add: succ_fm_def successor_def)
lemma successor_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> successor(**A, x, y) <-> sats(A, succ_fm(i,j), env)"
+ ==> successor(##A, x, y) <-> sats(A, succ_fm(i,j), env)"
by simp
theorem successor_reflection:
"REFLECTS[\<lambda>x. successor(L,f(x),g(x)),
- \<lambda>i x. successor(**Lset(i),f(x),g(x))]"
+ \<lambda>i x. successor(##Lset(i),f(x),g(x))]"
apply (simp only: successor_def)
apply (intro cons_reflection)
done
@@ -574,18 +574,18 @@
lemma sats_number1_fm [simp]:
"[| x \<in> nat; env \<in> list(A)|]
- ==> sats(A, number1_fm(x), env) <-> number1(**A, nth(x,env))"
+ ==> sats(A, number1_fm(x), env) <-> number1(##A, nth(x,env))"
by (simp add: number1_fm_def number1_def)
lemma number1_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; env \<in> list(A)|]
- ==> number1(**A, x) <-> sats(A, number1_fm(i), env)"
+ ==> number1(##A, x) <-> sats(A, number1_fm(i), env)"
by simp
theorem number1_reflection:
"REFLECTS[\<lambda>x. number1(L,f(x)),
- \<lambda>i x. number1(**Lset(i),f(x))]"
+ \<lambda>i x. number1(##Lset(i),f(x))]"
apply (simp only: number1_def)
apply (intro FOL_reflections empty_reflection successor_reflection)
done
@@ -606,18 +606,18 @@
lemma sats_big_union_fm [simp]:
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
==> sats(A, big_union_fm(x,y), env) <->
- big_union(**A, nth(x,env), nth(y,env))"
+ big_union(##A, nth(x,env), nth(y,env))"
by (simp add: big_union_fm_def big_union_def)
lemma big_union_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> big_union(**A, x, y) <-> sats(A, big_union_fm(i,j), env)"
+ ==> big_union(##A, x, y) <-> sats(A, big_union_fm(i,j), env)"
by simp
theorem big_union_reflection:
"REFLECTS[\<lambda>x. big_union(L,f(x),g(x)),
- \<lambda>i x. big_union(**Lset(i),f(x),g(x))]"
+ \<lambda>i x. big_union(##Lset(i),f(x),g(x))]"
apply (simp only: big_union_def)
apply (intro FOL_reflections)
done
@@ -633,40 +633,40 @@
lemma sats_subset_fm':
"[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
- ==> sats(A, subset_fm(x,y), env) <-> subset(**A, nth(x,env), nth(y,env))"
+ ==> sats(A, subset_fm(x,y), env) <-> subset(##A, nth(x,env), nth(y,env))"
by (simp add: subset_fm_def Relative.subset_def)
theorem subset_reflection:
"REFLECTS[\<lambda>x. subset(L,f(x),g(x)),
- \<lambda>i x. subset(**Lset(i),f(x),g(x))]"
+ \<lambda>i x. subset(##Lset(i),f(x),g(x))]"
apply (simp only: Relative.subset_def)
apply (intro FOL_reflections)
done
lemma sats_transset_fm':
"[|x \<in> nat; env \<in> list(A)|]
- ==> sats(A, transset_fm(x), env) <-> transitive_set(**A, nth(x,env))"
+ ==> sats(A, transset_fm(x), env) <-> transitive_set(##A, nth(x,env))"
by (simp add: sats_subset_fm' transset_fm_def transitive_set_def)
theorem transitive_set_reflection:
"REFLECTS[\<lambda>x. transitive_set(L,f(x)),
- \<lambda>i x. transitive_set(**Lset(i),f(x))]"
+ \<lambda>i x. transitive_set(##Lset(i),f(x))]"
apply (simp only: transitive_set_def)
apply (intro FOL_reflections subset_reflection)
done
lemma sats_ordinal_fm':
"[|x \<in> nat; env \<in> list(A)|]
- ==> sats(A, ordinal_fm(x), env) <-> ordinal(**A,nth(x,env))"
+ ==> sats(A, ordinal_fm(x), env) <-> ordinal(##A,nth(x,env))"
by (simp add: sats_transset_fm' ordinal_fm_def ordinal_def)
lemma ordinal_iff_sats:
"[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
- ==> ordinal(**A, x) <-> sats(A, ordinal_fm(i), env)"
+ ==> ordinal(##A, x) <-> sats(A, ordinal_fm(i), env)"
by (simp add: sats_ordinal_fm')
theorem ordinal_reflection:
- "REFLECTS[\<lambda>x. ordinal(L,f(x)), \<lambda>i x. ordinal(**Lset(i),f(x))]"
+ "REFLECTS[\<lambda>x. ordinal(L,f(x)), \<lambda>i x. ordinal(##Lset(i),f(x))]"
apply (simp only: ordinal_def)
apply (intro FOL_reflections transitive_set_reflection)
done
@@ -689,18 +689,18 @@
lemma sats_Memrel_fm [simp]:
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
==> sats(A, Memrel_fm(x,y), env) <->
- membership(**A, nth(x,env), nth(y,env))"
+ membership(##A, nth(x,env), nth(y,env))"
by (simp add: Memrel_fm_def membership_def)
lemma Memrel_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> membership(**A, x, y) <-> sats(A, Memrel_fm(i,j), env)"
+ ==> membership(##A, x, y) <-> sats(A, Memrel_fm(i,j), env)"
by simp
theorem membership_reflection:
"REFLECTS[\<lambda>x. membership(L,f(x),g(x)),
- \<lambda>i x. membership(**Lset(i),f(x),g(x))]"
+ \<lambda>i x. membership(##Lset(i),f(x),g(x))]"
apply (simp only: membership_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -723,18 +723,18 @@
lemma sats_pred_set_fm [simp]:
"[| U \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat; env \<in> list(A)|]
==> sats(A, pred_set_fm(U,x,r,B), env) <->
- pred_set(**A, nth(U,env), nth(x,env), nth(r,env), nth(B,env))"
+ pred_set(##A, nth(U,env), nth(x,env), nth(r,env), nth(B,env))"
by (simp add: pred_set_fm_def pred_set_def)
lemma pred_set_iff_sats:
"[| nth(i,env) = U; nth(j,env) = x; nth(k,env) = r; nth(l,env) = B;
i \<in> nat; j \<in> nat; k \<in> nat; l \<in> nat; env \<in> list(A)|]
- ==> pred_set(**A,U,x,r,B) <-> sats(A, pred_set_fm(i,j,k,l), env)"
+ ==> pred_set(##A,U,x,r,B) <-> sats(A, pred_set_fm(i,j,k,l), env)"
by (simp add: sats_pred_set_fm)
theorem pred_set_reflection:
"REFLECTS[\<lambda>x. pred_set(L,f(x),g(x),h(x),b(x)),
- \<lambda>i x. pred_set(**Lset(i),f(x),g(x),h(x),b(x))]"
+ \<lambda>i x. pred_set(##Lset(i),f(x),g(x),h(x),b(x))]"
apply (simp only: pred_set_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -758,18 +758,18 @@
lemma sats_domain_fm [simp]:
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
==> sats(A, domain_fm(x,y), env) <->
- is_domain(**A, nth(x,env), nth(y,env))"
+ is_domain(##A, nth(x,env), nth(y,env))"
by (simp add: domain_fm_def is_domain_def)
lemma domain_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> is_domain(**A, x, y) <-> sats(A, domain_fm(i,j), env)"
+ ==> is_domain(##A, x, y) <-> sats(A, domain_fm(i,j), env)"
by simp
theorem domain_reflection:
"REFLECTS[\<lambda>x. is_domain(L,f(x),g(x)),
- \<lambda>i x. is_domain(**Lset(i),f(x),g(x))]"
+ \<lambda>i x. is_domain(##Lset(i),f(x),g(x))]"
apply (simp only: is_domain_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -792,18 +792,18 @@
lemma sats_range_fm [simp]:
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
==> sats(A, range_fm(x,y), env) <->
- is_range(**A, nth(x,env), nth(y,env))"
+ is_range(##A, nth(x,env), nth(y,env))"
by (simp add: range_fm_def is_range_def)
lemma range_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> is_range(**A, x, y) <-> sats(A, range_fm(i,j), env)"
+ ==> is_range(##A, x, y) <-> sats(A, range_fm(i,j), env)"
by simp
theorem range_reflection:
"REFLECTS[\<lambda>x. is_range(L,f(x),g(x)),
- \<lambda>i x. is_range(**Lset(i),f(x),g(x))]"
+ \<lambda>i x. is_range(##Lset(i),f(x),g(x))]"
apply (simp only: is_range_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -827,18 +827,18 @@
lemma sats_field_fm [simp]:
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
==> sats(A, field_fm(x,y), env) <->
- is_field(**A, nth(x,env), nth(y,env))"
+ is_field(##A, nth(x,env), nth(y,env))"
by (simp add: field_fm_def is_field_def)
lemma field_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> is_field(**A, x, y) <-> sats(A, field_fm(i,j), env)"
+ ==> is_field(##A, x, y) <-> sats(A, field_fm(i,j), env)"
by simp
theorem field_reflection:
"REFLECTS[\<lambda>x. is_field(L,f(x),g(x)),
- \<lambda>i x. is_field(**Lset(i),f(x),g(x))]"
+ \<lambda>i x. is_field(##Lset(i),f(x),g(x))]"
apply (simp only: is_field_def)
apply (intro FOL_reflections domain_reflection range_reflection
union_reflection)
@@ -863,18 +863,18 @@
lemma sats_image_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, image_fm(x,y,z), env) <->
- image(**A, nth(x,env), nth(y,env), nth(z,env))"
+ image(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: image_fm_def Relative.image_def)
lemma image_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)|]
- ==> image(**A, x, y, z) <-> sats(A, image_fm(i,j,k), env)"
+ ==> image(##A, x, y, z) <-> sats(A, image_fm(i,j,k), env)"
by (simp add: sats_image_fm)
theorem image_reflection:
"REFLECTS[\<lambda>x. image(L,f(x),g(x),h(x)),
- \<lambda>i x. image(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. image(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: Relative.image_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -898,18 +898,18 @@
lemma sats_pre_image_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, pre_image_fm(x,y,z), env) <->
- pre_image(**A, nth(x,env), nth(y,env), nth(z,env))"
+ pre_image(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: pre_image_fm_def Relative.pre_image_def)
lemma pre_image_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)|]
- ==> pre_image(**A, x, y, z) <-> sats(A, pre_image_fm(i,j,k), env)"
+ ==> pre_image(##A, x, y, z) <-> sats(A, pre_image_fm(i,j,k), env)"
by (simp add: sats_pre_image_fm)
theorem pre_image_reflection:
"REFLECTS[\<lambda>x. pre_image(L,f(x),g(x),h(x)),
- \<lambda>i x. pre_image(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. pre_image(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: Relative.pre_image_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -933,18 +933,18 @@
lemma sats_fun_apply_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, fun_apply_fm(x,y,z), env) <->
- fun_apply(**A, nth(x,env), nth(y,env), nth(z,env))"
+ fun_apply(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: fun_apply_fm_def fun_apply_def)
lemma fun_apply_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)|]
- ==> fun_apply(**A, x, y, z) <-> sats(A, fun_apply_fm(i,j,k), env)"
+ ==> fun_apply(##A, x, y, z) <-> sats(A, fun_apply_fm(i,j,k), env)"
by simp
theorem fun_apply_reflection:
"REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)),
- \<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. fun_apply(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: fun_apply_def)
apply (intro FOL_reflections upair_reflection image_reflection
big_union_reflection)
@@ -965,18 +965,18 @@
lemma sats_relation_fm [simp]:
"[| x \<in> nat; env \<in> list(A)|]
- ==> sats(A, relation_fm(x), env) <-> is_relation(**A, nth(x,env))"
+ ==> sats(A, relation_fm(x), env) <-> is_relation(##A, nth(x,env))"
by (simp add: relation_fm_def is_relation_def)
lemma relation_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; env \<in> list(A)|]
- ==> is_relation(**A, x) <-> sats(A, relation_fm(i), env)"
+ ==> is_relation(##A, x) <-> sats(A, relation_fm(i), env)"
by simp
theorem is_relation_reflection:
"REFLECTS[\<lambda>x. is_relation(L,f(x)),
- \<lambda>i x. is_relation(**Lset(i),f(x))]"
+ \<lambda>i x. is_relation(##Lset(i),f(x))]"
apply (simp only: is_relation_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -1001,18 +1001,18 @@
lemma sats_function_fm [simp]:
"[| x \<in> nat; env \<in> list(A)|]
- ==> sats(A, function_fm(x), env) <-> is_function(**A, nth(x,env))"
+ ==> sats(A, function_fm(x), env) <-> is_function(##A, nth(x,env))"
by (simp add: function_fm_def is_function_def)
lemma is_function_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; env \<in> list(A)|]
- ==> is_function(**A, x) <-> sats(A, function_fm(i), env)"
+ ==> is_function(##A, x) <-> sats(A, function_fm(i), env)"
by simp
theorem is_function_reflection:
"REFLECTS[\<lambda>x. is_function(L,f(x)),
- \<lambda>i x. is_function(**Lset(i),f(x))]"
+ \<lambda>i x. is_function(##Lset(i),f(x))]"
apply (simp only: is_function_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -1039,13 +1039,13 @@
lemma sats_typed_function_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, typed_function_fm(x,y,z), env) <->
- typed_function(**A, nth(x,env), nth(y,env), nth(z,env))"
+ typed_function(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: typed_function_fm_def typed_function_def)
lemma typed_function_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)|]
- ==> typed_function(**A, x, y, z) <-> sats(A, typed_function_fm(i,j,k), env)"
+ ==> typed_function(##A, x, y, z) <-> sats(A, typed_function_fm(i,j,k), env)"
by simp
lemmas function_reflections =
@@ -1070,7 +1070,7 @@
theorem typed_function_reflection:
"REFLECTS[\<lambda>x. typed_function(L,f(x),g(x),h(x)),
- \<lambda>i x. typed_function(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. typed_function(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: typed_function_def)
apply (intro FOL_reflections function_reflections)
done
@@ -1099,18 +1099,18 @@
lemma sats_composition_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, composition_fm(x,y,z), env) <->
- composition(**A, nth(x,env), nth(y,env), nth(z,env))"
+ composition(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: composition_fm_def composition_def)
lemma composition_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)|]
- ==> composition(**A, x, y, z) <-> sats(A, composition_fm(i,j,k), env)"
+ ==> composition(##A, x, y, z) <-> sats(A, composition_fm(i,j,k), env)"
by simp
theorem composition_reflection:
"REFLECTS[\<lambda>x. composition(L,f(x),g(x),h(x)),
- \<lambda>i x. composition(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. composition(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: composition_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -1139,18 +1139,18 @@
lemma sats_injection_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, injection_fm(x,y,z), env) <->
- injection(**A, nth(x,env), nth(y,env), nth(z,env))"
+ injection(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: injection_fm_def injection_def)
lemma injection_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)|]
- ==> injection(**A, x, y, z) <-> sats(A, injection_fm(i,j,k), env)"
+ ==> injection(##A, x, y, z) <-> sats(A, injection_fm(i,j,k), env)"
by simp
theorem injection_reflection:
"REFLECTS[\<lambda>x. injection(L,f(x),g(x),h(x)),
- \<lambda>i x. injection(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. injection(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: injection_def)
apply (intro FOL_reflections function_reflections typed_function_reflection)
done
@@ -1176,18 +1176,18 @@
lemma sats_surjection_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, surjection_fm(x,y,z), env) <->
- surjection(**A, nth(x,env), nth(y,env), nth(z,env))"
+ surjection(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: surjection_fm_def surjection_def)
lemma surjection_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)|]
- ==> surjection(**A, x, y, z) <-> sats(A, surjection_fm(i,j,k), env)"
+ ==> surjection(##A, x, y, z) <-> sats(A, surjection_fm(i,j,k), env)"
by simp
theorem surjection_reflection:
"REFLECTS[\<lambda>x. surjection(L,f(x),g(x),h(x)),
- \<lambda>i x. surjection(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. surjection(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: surjection_def)
apply (intro FOL_reflections function_reflections typed_function_reflection)
done
@@ -1208,18 +1208,18 @@
lemma sats_bijection_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, bijection_fm(x,y,z), env) <->
- bijection(**A, nth(x,env), nth(y,env), nth(z,env))"
+ bijection(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: bijection_fm_def bijection_def)
lemma bijection_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)|]
- ==> bijection(**A, x, y, z) <-> sats(A, bijection_fm(i,j,k), env)"
+ ==> bijection(##A, x, y, z) <-> sats(A, bijection_fm(i,j,k), env)"
by simp
theorem bijection_reflection:
"REFLECTS[\<lambda>x. bijection(L,f(x),g(x),h(x)),
- \<lambda>i x. bijection(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. bijection(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: bijection_def)
apply (intro And_reflection injection_reflection surjection_reflection)
done
@@ -1244,18 +1244,18 @@
lemma sats_restriction_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, restriction_fm(x,y,z), env) <->
- restriction(**A, nth(x,env), nth(y,env), nth(z,env))"
+ restriction(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: restriction_fm_def restriction_def)
lemma restriction_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)|]
- ==> restriction(**A, x, y, z) <-> sats(A, restriction_fm(i,j,k), env)"
+ ==> restriction(##A, x, y, z) <-> sats(A, restriction_fm(i,j,k), env)"
by simp
theorem restriction_reflection:
"REFLECTS[\<lambda>x. restriction(L,f(x),g(x),h(x)),
- \<lambda>i x. restriction(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. restriction(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: restriction_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -1291,7 +1291,7 @@
lemma sats_order_isomorphism_fm [simp]:
"[| U \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat; env \<in> list(A)|]
==> sats(A, order_isomorphism_fm(U,r,B,s,f), env) <->
- order_isomorphism(**A, nth(U,env), nth(r,env), nth(B,env),
+ order_isomorphism(##A, nth(U,env), nth(r,env), nth(B,env),
nth(s,env), nth(f,env))"
by (simp add: order_isomorphism_fm_def order_isomorphism_def)
@@ -1299,13 +1299,13 @@
"[| nth(i,env) = U; nth(j,env) = r; nth(k,env) = B; nth(j',env) = s;
nth(k',env) = f;
i \<in> nat; j \<in> nat; k \<in> nat; j' \<in> nat; k' \<in> nat; env \<in> list(A)|]
- ==> order_isomorphism(**A,U,r,B,s,f) <->
+ ==> order_isomorphism(##A,U,r,B,s,f) <->
sats(A, order_isomorphism_fm(i,j,k,j',k'), env)"
by simp
theorem order_isomorphism_reflection:
"REFLECTS[\<lambda>x. order_isomorphism(L,f(x),g(x),h(x),g'(x),h'(x)),
- \<lambda>i x. order_isomorphism(**Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
+ \<lambda>i x. order_isomorphism(##Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
apply (simp only: order_isomorphism_def)
apply (intro FOL_reflections function_reflections bijection_reflection)
done
@@ -1332,18 +1332,18 @@
lemma sats_limit_ordinal_fm [simp]:
"[| x \<in> nat; env \<in> list(A)|]
- ==> sats(A, limit_ordinal_fm(x), env) <-> limit_ordinal(**A, nth(x,env))"
+ ==> sats(A, limit_ordinal_fm(x), env) <-> limit_ordinal(##A, nth(x,env))"
by (simp add: limit_ordinal_fm_def limit_ordinal_def sats_ordinal_fm')
lemma limit_ordinal_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; env \<in> list(A)|]
- ==> limit_ordinal(**A, x) <-> sats(A, limit_ordinal_fm(i), env)"
+ ==> limit_ordinal(##A, x) <-> sats(A, limit_ordinal_fm(i), env)"
by simp
theorem limit_ordinal_reflection:
"REFLECTS[\<lambda>x. limit_ordinal(L,f(x)),
- \<lambda>i x. limit_ordinal(**Lset(i),f(x))]"
+ \<lambda>i x. limit_ordinal(##Lset(i),f(x))]"
apply (simp only: limit_ordinal_def)
apply (intro FOL_reflections ordinal_reflection
empty_reflection successor_reflection)
@@ -1367,18 +1367,18 @@
lemma sats_finite_ordinal_fm [simp]:
"[| x \<in> nat; env \<in> list(A)|]
- ==> sats(A, finite_ordinal_fm(x), env) <-> finite_ordinal(**A, nth(x,env))"
+ ==> sats(A, finite_ordinal_fm(x), env) <-> finite_ordinal(##A, nth(x,env))"
by (simp add: finite_ordinal_fm_def sats_ordinal_fm' finite_ordinal_def)
lemma finite_ordinal_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; env \<in> list(A)|]
- ==> finite_ordinal(**A, x) <-> sats(A, finite_ordinal_fm(i), env)"
+ ==> finite_ordinal(##A, x) <-> sats(A, finite_ordinal_fm(i), env)"
by simp
theorem finite_ordinal_reflection:
"REFLECTS[\<lambda>x. finite_ordinal(L,f(x)),
- \<lambda>i x. finite_ordinal(**Lset(i),f(x))]"
+ \<lambda>i x. finite_ordinal(##Lset(i),f(x))]"
apply (simp only: finite_ordinal_def)
apply (intro FOL_reflections ordinal_reflection limit_ordinal_reflection)
done
@@ -1399,18 +1399,18 @@
lemma sats_omega_fm [simp]:
"[| x \<in> nat; env \<in> list(A)|]
- ==> sats(A, omega_fm(x), env) <-> omega(**A, nth(x,env))"
+ ==> sats(A, omega_fm(x), env) <-> omega(##A, nth(x,env))"
by (simp add: omega_fm_def omega_def)
lemma omega_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; env \<in> list(A)|]
- ==> omega(**A, x) <-> sats(A, omega_fm(i), env)"
+ ==> omega(##A, x) <-> sats(A, omega_fm(i), env)"
by simp
theorem omega_reflection:
"REFLECTS[\<lambda>x. omega(L,f(x)),
- \<lambda>i x. omega(**Lset(i),f(x))]"
+ \<lambda>i x. omega(##Lset(i),f(x))]"
apply (simp only: omega_def)
apply (intro FOL_reflections limit_ordinal_reflection)
done
--- a/src/ZF/Constructible/Rank_Separation.thy Wed Feb 05 13:35:32 2003 +0100
+++ b/src/ZF/Constructible/Rank_Separation.thy Thu Feb 06 11:01:05 2003 +0100
@@ -21,7 +21,7 @@
"REFLECTS[\<lambda>x. x\<in>A -->
(\<exists>y[L]. \<exists>p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r),
\<lambda>i x. x\<in>A --> (\<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) & pair(##Lset(i),y,x,p) & p \<in> r)]"
by (intro FOL_reflections function_reflections)
lemma well_ord_iso_separation:
@@ -42,8 +42,8 @@
ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
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) &
- order_isomorphism(**Lset(i),par,r,x,mx,g)]"
+ ordinal(##Lset(i),x) & membership(##Lset(i),x,mx) & pred_set(##Lset(i),A,a,r,par) &
+ order_isomorphism(##Lset(i),par,r,x,mx,g)]"
by (intro FOL_reflections function_reflections fun_plus_reflections)
lemma obase_separation:
@@ -66,9 +66,9 @@
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 --> ~(\<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)))]"
+ 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:
@@ -91,9 +91,9 @@
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).
\<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) &
- order_isomorphism(**Lset(i),par,r,x,mx,g))]"
+ ordinal(##Lset(i),x) & pair(##Lset(i),a,x,z) &
+ membership(##Lset(i),x,mx) & pred_set(##Lset(i),A,a,r,par) &
+ order_isomorphism(##Lset(i),par,r,x,mx,g))]"
by (intro FOL_reflections function_reflections fun_plus_reflections)
lemma omap_replacement:
@@ -135,9 +135,9 @@
lemma wfrank_Reflects:
"REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
~ (\<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) -->
+ \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(##Lset(i),r,rplus) -->
~ (\<exists>f \<in> Lset(i).
- M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y),
+ 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)
@@ -160,10 +160,10 @@
M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
is_range(L,f,y))),
\<lambda>i z. \<exists>x \<in> Lset(i). x \<in> A &
- (\<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
- (\<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) &
- is_range(**Lset(i),f,y)))]"
+ (\<forall>rplus \<in> Lset(i). tran_closure(##Lset(i),r,rplus) -->
+ (\<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) &
+ is_range(##Lset(i),f,y)))]"
by (intro FOL_reflections function_reflections fun_plus_reflections
is_recfun_reflection tran_closure_reflection)
@@ -191,12 +191,12 @@
is_range(L,f,rangef) -->
M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
ordinal(L,rangef)),
- \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
+ \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(##Lset(i),r,rplus) -->
~ (\<forall>f \<in> Lset(i). \<forall>rangef \<in> Lset(i).
- is_range(**Lset(i),f,rangef) -->
- M_is_recfun(**Lset(i), \<lambda>x f y. is_range(**Lset(i),f,y),
+ is_range(##Lset(i),f,rangef) -->
+ M_is_recfun(##Lset(i), \<lambda>x f y. is_range(##Lset(i),f,y),
rplus, x, f) -->
- ordinal(**Lset(i),rangef))]"
+ ordinal(##Lset(i),rangef))]"
by (intro FOL_reflections function_reflections is_recfun_reflection
tran_closure_reflection ordinal_reflection)
--- a/src/ZF/Constructible/Rec_Separation.thy Wed Feb 05 13:35:32 2003 +0100
+++ b/src/ZF/Constructible/Rec_Separation.thy Thu Feb 06 11:01:05 2003 +0100
@@ -56,18 +56,18 @@
lemma sats_rtran_closure_mem_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, rtran_closure_mem_fm(x,y,z), env) <->
- rtran_closure_mem(**A, nth(x,env), nth(y,env), nth(z,env))"
+ rtran_closure_mem(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: rtran_closure_mem_fm_def rtran_closure_mem_def)
lemma rtran_closure_mem_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)|]
- ==> rtran_closure_mem(**A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)"
+ ==> rtran_closure_mem(##A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)"
by (simp add: sats_rtran_closure_mem_fm)
lemma rtran_closure_mem_reflection:
"REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)),
- \<lambda>i x. rtran_closure_mem(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. rtran_closure_mem(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: rtran_closure_mem_def)
apply (intro FOL_reflections function_reflections fun_plus_reflections)
done
@@ -100,18 +100,18 @@
lemma sats_rtran_closure_fm [simp]:
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
==> sats(A, rtran_closure_fm(x,y), env) <->
- rtran_closure(**A, nth(x,env), nth(y,env))"
+ rtran_closure(##A, nth(x,env), nth(y,env))"
by (simp add: rtran_closure_fm_def rtran_closure_def)
lemma rtran_closure_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> rtran_closure(**A, x, y) <-> sats(A, rtran_closure_fm(i,j), env)"
+ ==> rtran_closure(##A, x, y) <-> sats(A, rtran_closure_fm(i,j), env)"
by simp
theorem rtran_closure_reflection:
"REFLECTS[\<lambda>x. rtran_closure(L,f(x),g(x)),
- \<lambda>i x. rtran_closure(**Lset(i),f(x),g(x))]"
+ \<lambda>i x. rtran_closure(##Lset(i),f(x),g(x))]"
apply (simp only: rtran_closure_def)
apply (intro FOL_reflections function_reflections rtran_closure_mem_reflection)
done
@@ -132,18 +132,18 @@
lemma sats_tran_closure_fm [simp]:
"[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
==> sats(A, tran_closure_fm(x,y), env) <->
- tran_closure(**A, nth(x,env), nth(y,env))"
+ tran_closure(##A, nth(x,env), nth(y,env))"
by (simp add: tran_closure_fm_def tran_closure_def)
lemma tran_closure_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> tran_closure(**A, x, y) <-> sats(A, tran_closure_fm(i,j), env)"
+ ==> tran_closure(##A, x, y) <-> sats(A, tran_closure_fm(i,j), env)"
by simp
theorem tran_closure_reflection:
"REFLECTS[\<lambda>x. tran_closure(L,f(x),g(x)),
- \<lambda>i x. tran_closure(**Lset(i),f(x),g(x))]"
+ \<lambda>i x. tran_closure(##Lset(i),f(x),g(x))]"
apply (simp only: tran_closure_def)
apply (intro FOL_reflections function_reflections
rtran_closure_reflection composition_reflection)
@@ -156,7 +156,7 @@
"REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp,
\<lambda>i x. \<exists>w \<in> Lset(i). \<exists>wx \<in> Lset(i). \<exists>rp \<in> Lset(i).
- w \<in> Z & pair(**Lset(i),w,x,wx) & tran_closure(**Lset(i),r,rp) &
+ w \<in> Z & pair(##Lset(i),w,x,wx) & tran_closure(##Lset(i),r,rp) &
wx \<in> rp]"
by (intro FOL_reflections function_reflections fun_plus_reflections
tran_closure_reflection)
@@ -199,10 +199,10 @@
"REFLECTS
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
is_wfrec(L, iterates_MH(L, is_list_functor(L,A), 0), memsn, u, y)),
- \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
- is_wfrec(**Lset(i),
- iterates_MH(**Lset(i),
- is_list_functor(**Lset(i), A), 0), memsn, u, y))]"
+ \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) \<and>
+ is_wfrec(##Lset(i),
+ iterates_MH(##Lset(i),
+ is_list_functor(##Lset(i), A), 0), memsn, u, y))]"
by (intro FOL_reflections function_reflections is_wfrec_reflection
iterates_MH_reflection list_functor_reflection)
@@ -225,7 +225,7 @@
[\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat &
is_iterates(L, is_list_functor(L, A), 0, u, x),
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat &
- is_iterates(**Lset(i), is_list_functor(**Lset(i), A), 0, u, x)]"
+ is_iterates(##Lset(i), is_list_functor(##Lset(i), A), 0, u, x)]"
by (intro FOL_reflections
is_iterates_reflection list_functor_reflection)
@@ -251,10 +251,10 @@
"REFLECTS
[\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) &
is_wfrec(L, iterates_MH(L, is_formula_functor(L), 0), memsn, u, y)),
- \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) &
- is_wfrec(**Lset(i),
- iterates_MH(**Lset(i),
- is_formula_functor(**Lset(i)), 0), memsn, u, y))]"
+ \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) &
+ is_wfrec(##Lset(i),
+ iterates_MH(##Lset(i),
+ is_formula_functor(##Lset(i)), 0), memsn, u, y))]"
by (intro FOL_reflections function_reflections is_wfrec_reflection
iterates_MH_reflection formula_functor_reflection)
@@ -275,7 +275,7 @@
[\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat &
is_iterates(L, is_formula_functor(L), 0, u, x),
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat &
- is_iterates(**Lset(i), is_formula_functor(**Lset(i)), 0, u, x)]"
+ is_iterates(##Lset(i), is_formula_functor(##Lset(i)), 0, u, x)]"
by (intro FOL_reflections
is_iterates_reflection formula_functor_reflection)
@@ -310,7 +310,7 @@
lemma sats_nth_fm [simp]:
"[| x < length(env); y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, nth_fm(x,y,z), env) <->
- is_nth(**A, nth(x,env), nth(y,env), nth(z,env))"
+ is_nth(##A, nth(x,env), nth(y,env), nth(z,env))"
apply (frule lt_length_in_nat, assumption)
apply (simp add: nth_fm_def is_nth_def sats_is_iterates_fm)
done
@@ -318,12 +318,12 @@
lemma nth_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i < length(env); j \<in> nat; k \<in> nat; env \<in> list(A)|]
- ==> is_nth(**A, x, y, z) <-> sats(A, nth_fm(i,j,k), env)"
+ ==> is_nth(##A, x, y, z) <-> sats(A, nth_fm(i,j,k), env)"
by (simp add: sats_nth_fm)
theorem nth_reflection:
"REFLECTS[\<lambda>x. is_nth(L, f(x), g(x), h(x)),
- \<lambda>i x. is_nth(**Lset(i), f(x), g(x), h(x))]"
+ \<lambda>i x. is_nth(##Lset(i), f(x), g(x), h(x))]"
apply (simp only: is_nth_def)
apply (intro FOL_reflections is_iterates_reflection
hd_reflection tl_reflection)
@@ -338,10 +338,10 @@
"REFLECTS
[\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) &
is_wfrec(L, iterates_MH(L, is_tl(L), z), memsn, u, y)),
- \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) &
- is_wfrec(**Lset(i),
- iterates_MH(**Lset(i),
- is_tl(**Lset(i)), z), memsn, u, y))]"
+ \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) &
+ is_wfrec(##Lset(i),
+ iterates_MH(##Lset(i),
+ is_tl(##Lset(i)), z), memsn, u, y))]"
by (intro FOL_reflections function_reflections is_wfrec_reflection
iterates_MH_reflection tl_reflection)
@@ -395,9 +395,9 @@
"REFLECTS
[\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) &
is_wfrec(L, iterates_MH(L, big_union(L), A), memsn, u, y)),
- \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) &
- is_wfrec(**Lset(i),
- iterates_MH(**Lset(i), big_union(**Lset(i)), A),
+ \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) &
+ is_wfrec(##Lset(i),
+ iterates_MH(##Lset(i), big_union(##Lset(i)), A),
memsn, u, y))]"
by (intro FOL_reflections function_reflections is_wfrec_reflection
iterates_MH_reflection)
@@ -419,7 +419,7 @@
[\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat &
is_iterates(L, big_union(L), A, u, x),
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat &
- is_iterates(**Lset(i), big_union(**Lset(i)), A, u, x)]"
+ is_iterates(##Lset(i), big_union(##Lset(i)), A, u, x)]"
by (intro FOL_reflections function_reflections is_iterates_reflection)
lemma eclose_replacement2:
--- a/src/ZF/Constructible/Satisfies_absolute.thy Wed Feb 05 13:35:32 2003 +0100
+++ b/src/ZF/Constructible/Satisfies_absolute.thy Thu Feb 06 11:01:05 2003 +0100
@@ -32,7 +32,7 @@
lemma sats_depth_fm [simp]:
"[| x \<in> nat; y < length(env); env \<in> list(A)|]
==> sats(A, depth_fm(x,y), env) <->
- is_depth(**A, nth(x,env), nth(y,env))"
+ is_depth(##A, nth(x,env), nth(y,env))"
apply (frule_tac x=y in lt_length_in_nat, assumption)
apply (simp add: depth_fm_def is_depth_def)
done
@@ -40,12 +40,12 @@
lemma depth_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j < length(env); env \<in> list(A)|]
- ==> is_depth(**A, x, y) <-> sats(A, depth_fm(i,j), env)"
+ ==> is_depth(##A, x, y) <-> sats(A, depth_fm(i,j), env)"
by (simp add: sats_depth_fm)
theorem depth_reflection:
"REFLECTS[\<lambda>x. is_depth(L, f(x), g(x)),
- \<lambda>i x. is_depth(**Lset(i), f(x), g(x))]"
+ \<lambda>i x. is_depth(##Lset(i), f(x), g(x))]"
apply (simp only: is_depth_def)
apply (intro FOL_reflections function_reflections formula_N_reflection)
done
@@ -111,7 +111,7 @@
shows
"[|x \<in> nat; y < length(env); env \<in> list(A)|]
==> sats(A, formula_case_fm(is_a,is_b,is_c,is_d,x,y), env) <->
- is_formula_case(**A, ISA, ISB, ISC, ISD, nth(x,env), nth(y,env))"
+ is_formula_case(##A, ISA, ISB, ISC, ISD, nth(x,env), nth(y,env))"
apply (frule_tac x=y in lt_length_in_nat, assumption)
apply (simp add: formula_case_fm_def is_formula_case_def
is_a_iff_sats [THEN iff_sym] is_b_iff_sats [THEN iff_sym]
@@ -138,7 +138,7 @@
shows
"[|nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j < length(env); env \<in> list(A)|]
- ==> is_formula_case(**A, ISA, ISB, ISC, ISD, x, y) <->
+ ==> is_formula_case(##A, ISA, ISB, ISC, ISD, x, y) <->
sats(A, formula_case_fm(is_a,is_b,is_c,is_d,i,j), env)"
by (simp add: sats_formula_case_fm [OF is_a_iff_sats is_b_iff_sats
is_c_iff_sats is_d_iff_sats])
@@ -150,18 +150,18 @@
theorem is_formula_case_reflection:
assumes is_a_reflection:
"!!h f g g'. REFLECTS[\<lambda>x. is_a(L, h(x), f(x), g(x), g'(x)),
- \<lambda>i x. is_a(**Lset(i), h(x), f(x), g(x), g'(x))]"
+ \<lambda>i x. is_a(##Lset(i), h(x), f(x), g(x), g'(x))]"
and is_b_reflection:
"!!h f g g'. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x), g'(x)),
- \<lambda>i x. is_b(**Lset(i), h(x), f(x), g(x), g'(x))]"
+ \<lambda>i x. is_b(##Lset(i), h(x), f(x), g(x), g'(x))]"
and is_c_reflection:
"!!h f g g'. REFLECTS[\<lambda>x. is_c(L, h(x), f(x), g(x), g'(x)),
- \<lambda>i x. is_c(**Lset(i), h(x), f(x), g(x), g'(x))]"
+ \<lambda>i x. is_c(##Lset(i), h(x), f(x), g(x), g'(x))]"
and is_d_reflection:
"!!h f g g'. REFLECTS[\<lambda>x. is_d(L, h(x), f(x), g(x)),
- \<lambda>i x. is_d(**Lset(i), h(x), f(x), g(x))]"
+ \<lambda>i x. is_d(##Lset(i), h(x), f(x), g(x))]"
shows "REFLECTS[\<lambda>x. is_formula_case(L, is_a(L,x), is_b(L,x), is_c(L,x), is_d(L,x), g(x), h(x)),
- \<lambda>i x. is_formula_case(**Lset(i), is_a(**Lset(i), x), is_b(**Lset(i), x), is_c(**Lset(i), x), is_d(**Lset(i), x), g(x), h(x))]"
+ \<lambda>i x. is_formula_case(##Lset(i), is_a(##Lset(i), x), is_b(##Lset(i), x), is_c(##Lset(i), x), is_d(##Lset(i), x), g(x), h(x))]"
apply (simp (no_asm_use) only: is_formula_case_def)
apply (intro FOL_reflections function_reflections finite_ordinal_reflection
mem_formula_reflection
@@ -518,18 +518,18 @@
lemma sats_depth_apply_fm [simp]:
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, depth_apply_fm(x,y,z), env) <->
- is_depth_apply(**A, nth(x,env), nth(y,env), nth(z,env))"
+ is_depth_apply(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: depth_apply_fm_def is_depth_apply_def)
lemma depth_apply_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_depth_apply(**A, x, y, z) <-> sats(A, depth_apply_fm(i,j,k), env)"
+ ==> is_depth_apply(##A, x, y, z) <-> sats(A, depth_apply_fm(i,j,k), env)"
by simp
lemma depth_apply_reflection:
"REFLECTS[\<lambda>x. is_depth_apply(L,f(x),g(x),h(x)),
- \<lambda>i x. is_depth_apply(**Lset(i),f(x),g(x),h(x))]"
+ \<lambda>i x. is_depth_apply(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: is_depth_apply_def)
apply (intro FOL_reflections function_reflections depth_reflection
finite_ordinal_reflection)
@@ -565,7 +565,7 @@
lemma sats_satisfies_is_a_fm [simp]:
"[| u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
==> sats(A, satisfies_is_a_fm(u,x,y,z), env) <->
- satisfies_is_a(**A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
+ satisfies_is_a(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
apply (frule_tac x=x in lt_length_in_nat, assumption)
apply (frule_tac x=y in lt_length_in_nat, assumption)
apply (simp add: satisfies_is_a_fm_def satisfies_is_a_def sats_lambda_fm
@@ -575,13 +575,13 @@
lemma satisfies_is_a_iff_sats:
"[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
- ==> satisfies_is_a(**A,nu,nx,ny,nz) <->
+ ==> satisfies_is_a(##A,nu,nx,ny,nz) <->
sats(A, satisfies_is_a_fm(u,x,y,z), env)"
by simp
theorem satisfies_is_a_reflection:
"REFLECTS[\<lambda>x. satisfies_is_a(L,f(x),g(x),h(x),g'(x)),
- \<lambda>i x. satisfies_is_a(**Lset(i),f(x),g(x),h(x),g'(x))]"
+ \<lambda>i x. satisfies_is_a(##Lset(i),f(x),g(x),h(x),g'(x))]"
apply (unfold satisfies_is_a_def)
apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection
nth_reflection is_list_reflection)
@@ -613,7 +613,7 @@
lemma sats_satisfies_is_b_fm [simp]:
"[| u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
==> sats(A, satisfies_is_b_fm(u,x,y,z), env) <->
- satisfies_is_b(**A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
+ satisfies_is_b(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
apply (frule_tac x=x in lt_length_in_nat, assumption)
apply (frule_tac x=y in lt_length_in_nat, assumption)
apply (simp add: satisfies_is_b_fm_def satisfies_is_b_def sats_lambda_fm
@@ -623,13 +623,13 @@
lemma satisfies_is_b_iff_sats:
"[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
- ==> satisfies_is_b(**A,nu,nx,ny,nz) <->
+ ==> satisfies_is_b(##A,nu,nx,ny,nz) <->
sats(A, satisfies_is_b_fm(u,x,y,z), env)"
by simp
theorem satisfies_is_b_reflection:
"REFLECTS[\<lambda>x. satisfies_is_b(L,f(x),g(x),h(x),g'(x)),
- \<lambda>i x. satisfies_is_b(**Lset(i),f(x),g(x),h(x),g'(x))]"
+ \<lambda>i x. satisfies_is_b(##Lset(i),f(x),g(x),h(x),g'(x))]"
apply (unfold satisfies_is_b_def)
apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection
nth_reflection is_list_reflection)
@@ -665,7 +665,7 @@
lemma sats_satisfies_is_c_fm [simp]:
"[| u \<in> nat; v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, satisfies_is_c_fm(u,v,x,y,z), env) <->
- satisfies_is_c(**A, nth(u,env), nth(v,env), nth(x,env),
+ satisfies_is_c(##A, nth(u,env), nth(v,env), nth(x,env),
nth(y,env), nth(z,env))"
by (simp add: satisfies_is_c_fm_def satisfies_is_c_def sats_lambda_fm)
@@ -673,13 +673,13 @@
"[| nth(u,env) = nu; nth(v,env) = nv; nth(x,env) = nx; nth(y,env) = ny;
nth(z,env) = nz;
u \<in> nat; v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
- ==> satisfies_is_c(**A,nu,nv,nx,ny,nz) <->
+ ==> satisfies_is_c(##A,nu,nv,nx,ny,nz) <->
sats(A, satisfies_is_c_fm(u,v,x,y,z), env)"
by simp
theorem satisfies_is_c_reflection:
"REFLECTS[\<lambda>x. satisfies_is_c(L,f(x),g(x),h(x),g'(x),h'(x)),
- \<lambda>i x. satisfies_is_c(**Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
+ \<lambda>i x. satisfies_is_c(##Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
apply (unfold satisfies_is_c_def)
apply (intro FOL_reflections function_reflections is_lambda_reflection
extra_reflections nth_reflection depth_apply_reflection
@@ -721,20 +721,20 @@
lemma sats_satisfies_is_d_fm [simp]:
"[| u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, satisfies_is_d_fm(u,x,y,z), env) <->
- satisfies_is_d(**A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
+ satisfies_is_d(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
by (simp add: satisfies_is_d_fm_def satisfies_is_d_def sats_lambda_fm
sats_bool_of_o_fm)
lemma satisfies_is_d_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)|]
- ==> satisfies_is_d(**A,nu,nx,ny,nz) <->
+ ==> satisfies_is_d(##A,nu,nx,ny,nz) <->
sats(A, satisfies_is_d_fm(u,x,y,z), env)"
by simp
theorem satisfies_is_d_reflection:
"REFLECTS[\<lambda>x. satisfies_is_d(L,f(x),g(x),h(x),g'(x)),
- \<lambda>i x. satisfies_is_d(**Lset(i),f(x),g(x),h(x),g'(x))]"
+ \<lambda>i x. satisfies_is_d(##Lset(i),f(x),g(x),h(x),g'(x))]"
apply (unfold satisfies_is_d_def)
apply (intro FOL_reflections function_reflections is_lambda_reflection
extra_reflections nth_reflection depth_apply_reflection
@@ -773,14 +773,14 @@
lemma sats_satisfies_MH_fm [simp]:
"[| u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, satisfies_MH_fm(u,x,y,z), env) <->
- satisfies_MH(**A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
+ satisfies_MH(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
by (simp add: satisfies_MH_fm_def satisfies_MH_def sats_lambda_fm
sats_formula_case_fm)
lemma satisfies_MH_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)|]
- ==> satisfies_MH(**A,nu,nx,ny,nz) <->
+ ==> satisfies_MH(##A,nu,nx,ny,nz) <->
sats(A, satisfies_MH_fm(u,x,y,z), env)"
by simp
@@ -792,7 +792,7 @@
theorem satisfies_MH_reflection:
"REFLECTS[\<lambda>x. satisfies_MH(L,f(x),g(x),h(x),g'(x)),
- \<lambda>i x. satisfies_MH(**Lset(i),f(x),g(x),h(x),g'(x))]"
+ \<lambda>i x. satisfies_MH(##Lset(i),f(x),g(x),h(x),g'(x))]"
apply (unfold satisfies_MH_def)
apply (intro FOL_reflections satisfies_reflections)
done
@@ -808,9 +808,9 @@
v \<in> lstA \<and> is_nth(L,x,v,nx) \<and> is_nth(L,y,v,ny) \<and>
is_bool_of_o(L, nx \<in> ny, bo) \<and> pair(L,v,bo,u)),
\<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B \<and> (\<exists>bo \<in> Lset(i). \<exists>nx \<in> Lset(i). \<exists>ny \<in> Lset(i).
- v \<in> lstA \<and> is_nth(**Lset(i), x, v, nx) \<and>
- is_nth(**Lset(i), y, v, ny) \<and>
- is_bool_of_o(**Lset(i), nx \<in> ny, bo) \<and> pair(**Lset(i), v, bo, u))]"
+ v \<in> lstA \<and> is_nth(##Lset(i), x, v, nx) \<and>
+ is_nth(##Lset(i), y, v, ny) \<and>
+ is_bool_of_o(##Lset(i), nx \<in> ny, bo) \<and> pair(##Lset(i), v, bo, u))]"
by (intro FOL_reflections function_reflections nth_reflection
bool_of_o_reflection)
@@ -838,9 +838,9 @@
v \<in> lstA \<and> is_nth(L, x, v, nx) \<and> is_nth(L, y, v, ny) \<and>
is_bool_of_o(L, nx = ny, bo) \<and> pair(L, v, bo, u)),
\<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B \<and> (\<exists>bo \<in> Lset(i). \<exists>nx \<in> Lset(i). \<exists>ny \<in> Lset(i).
- v \<in> lstA \<and> is_nth(**Lset(i), x, v, nx) \<and>
- is_nth(**Lset(i), y, v, ny) \<and>
- is_bool_of_o(**Lset(i), nx = ny, bo) \<and> pair(**Lset(i), v, bo, u))]"
+ v \<in> lstA \<and> is_nth(##Lset(i), x, v, nx) \<and>
+ is_nth(##Lset(i), y, v, ny) \<and>
+ is_bool_of_o(##Lset(i), nx = ny, bo) \<and> pair(##Lset(i), v, bo, u))]"
by (intro FOL_reflections function_reflections nth_reflection
bool_of_o_reflection)
@@ -870,9 +870,9 @@
u \<in> list(A) \<and> pair(L, u, notpq, x)),
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and>
(\<exists>rpe \<in> Lset(i). \<exists>rqe \<in> Lset(i). \<exists>andpq \<in> Lset(i). \<exists>notpq \<in> Lset(i).
- fun_apply(**Lset(i), rp, u, rpe) \<and> fun_apply(**Lset(i), rq, u, rqe) \<and>
- is_and(**Lset(i), rpe, rqe, andpq) \<and> is_not(**Lset(i), andpq, notpq) \<and>
- u \<in> list(A) \<and> pair(**Lset(i), u, notpq, x))]"
+ fun_apply(##Lset(i), rp, u, rpe) \<and> fun_apply(##Lset(i), rq, u, rqe) \<and>
+ is_and(##Lset(i), rpe, rqe, andpq) \<and> is_not(##Lset(i), andpq, notpq) \<and>
+ u \<in> list(A) \<and> pair(##Lset(i), u, notpq, x))]"
apply (unfold is_and_def is_not_def)
apply (intro FOL_reflections function_reflections)
done
@@ -903,11 +903,11 @@
number1(L,rpco),
bo) \<and> pair(L,u,bo,x)),
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>bo \<in> Lset(i). u \<in> list(A) \<and>
- is_bool_of_o (**Lset(i),
+ is_bool_of_o (##Lset(i),
\<forall>a \<in> Lset(i). \<forall>co \<in> Lset(i). \<forall>rpco \<in> Lset(i). a \<in> A \<longrightarrow>
- is_Cons(**Lset(i),a,u,co) \<longrightarrow> fun_apply(**Lset(i),rp,co,rpco) \<longrightarrow>
- number1(**Lset(i),rpco),
- bo) \<and> pair(**Lset(i),u,bo,x))]"
+ is_Cons(##Lset(i),a,u,co) \<longrightarrow> fun_apply(##Lset(i),rp,co,rpco) \<longrightarrow>
+ number1(##Lset(i),rpco),
+ bo) \<and> pair(##Lset(i),u,bo,x))]"
apply (unfold is_bool_of_o_def)
apply (intro FOL_reflections function_reflections Cons_reflection)
done
@@ -936,8 +936,8 @@
lemma formula_rec_replacement_Reflects:
"REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L, u, y, x) \<and>
is_wfrec (L, satisfies_MH(L,A), mesa, u, y)),
- \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
- is_wfrec (**Lset(i), satisfies_MH(**Lset(i),A), mesa, u, y))]"
+ \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) \<and>
+ is_wfrec (##Lset(i), satisfies_MH(##Lset(i),A), mesa, u, y))]"
by (intro FOL_reflections function_reflections satisfies_MH_reflection
is_wfrec_reflection)
@@ -965,13 +965,13 @@
satisfies_is_c(L,A,g), satisfies_is_d(L,A,g),
u, c) &
pair(L,u,c,x)),
- \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & mem_formula(**Lset(i),u) &
+ \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & mem_formula(##Lset(i),u) &
(\<exists>c \<in> Lset(i).
is_formula_case
- (**Lset(i), satisfies_is_a(**Lset(i),A), satisfies_is_b(**Lset(i),A),
- satisfies_is_c(**Lset(i),A,g), satisfies_is_d(**Lset(i),A,g),
+ (##Lset(i), satisfies_is_a(##Lset(i),A), satisfies_is_b(##Lset(i),A),
+ satisfies_is_c(##Lset(i),A,g), satisfies_is_d(##Lset(i),A,g),
u, c) &
- pair(**Lset(i),u,c,x))]"
+ pair(##Lset(i),u,c,x))]"
by (intro FOL_reflections function_reflections mem_formula_reflection
is_formula_case_reflection satisfies_is_a_reflection
satisfies_is_b_reflection satisfies_is_c_reflection
--- a/src/ZF/Constructible/Separation.thy Wed Feb 05 13:35:32 2003 +0100
+++ b/src/ZF/Constructible/Separation.thy Thu Feb 06 11:01:05 2003 +0100
@@ -121,7 +121,7 @@
lemma cartprod_Reflects:
"REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)),
\<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). y\<in>B &
- pair(**Lset(i),x,y,z))]"
+ pair(##Lset(i),x,y,z))]"
by (intro FOL_reflections function_reflections)
lemma cartprod_separation:
@@ -136,7 +136,7 @@
lemma image_Reflects:
"REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)),
- \<lambda>i y. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). x\<in>A & pair(**Lset(i),x,y,p))]"
+ \<lambda>i y. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). x\<in>A & pair(##Lset(i),x,y,p))]"
by (intro FOL_reflections function_reflections)
lemma image_separation:
@@ -153,7 +153,7 @@
lemma converse_Reflects:
"REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)),
\<lambda>i z. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i).
- pair(**Lset(i),x,y,p) & pair(**Lset(i),y,x,z))]"
+ pair(##Lset(i),x,y,p) & pair(##Lset(i),y,x,z))]"
by (intro FOL_reflections function_reflections)
lemma converse_separation:
@@ -169,7 +169,7 @@
lemma restrict_Reflects:
"REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)),
- \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). pair(**Lset(i),x,y,z))]"
+ \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). pair(##Lset(i),x,y,z))]"
by (intro FOL_reflections function_reflections)
lemma restrict_separation:
@@ -187,8 +187,8 @@
pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
xy\<in>s & yz\<in>r,
\<lambda>i xz. \<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). \<exists>z\<in>Lset(i). \<exists>xy\<in>Lset(i). \<exists>yz\<in>Lset(i).
- pair(**Lset(i),x,z,xz) & pair(**Lset(i),x,y,xy) &
- pair(**Lset(i),y,z,yz) & xy\<in>s & yz\<in>r]"
+ pair(##Lset(i),x,z,xz) & pair(##Lset(i),x,y,xy) &
+ pair(##Lset(i),y,z,yz) & xy\<in>s & yz\<in>r]"
by (intro FOL_reflections function_reflections)
lemma comp_separation:
@@ -210,7 +210,7 @@
lemma pred_Reflects:
"REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p),
- \<lambda>i y. \<exists>p \<in> Lset(i). p\<in>r & pair(**Lset(i),y,x,p)]"
+ \<lambda>i y. \<exists>p \<in> Lset(i). p\<in>r & pair(##Lset(i),y,x,p)]"
by (intro FOL_reflections function_reflections)
lemma pred_separation:
@@ -225,7 +225,7 @@
lemma Memrel_Reflects:
"REFLECTS[\<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y,
- \<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(**Lset(i),x,y,z) & x \<in> y]"
+ \<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(##Lset(i),x,y,z) & x \<in> y]"
by (intro FOL_reflections function_reflections)
lemma Memrel_separation:
@@ -244,8 +244,8 @@
upair(L,cnbf,cnbf,z)),
\<lambda>i z. \<exists>p \<in> Lset(i). p\<in>A & (\<exists>f \<in> Lset(i). \<exists>b \<in> Lset(i).
\<exists>nb \<in> Lset(i). \<exists>cnbf \<in> Lset(i).
- pair(**Lset(i),f,b,p) & pair(**Lset(i),n,b,nb) &
- is_cons(**Lset(i),nb,f,cnbf) & upair(**Lset(i),cnbf,cnbf,z))]"
+ pair(##Lset(i),f,b,p) & pair(##Lset(i),n,b,nb) &
+ is_cons(##Lset(i),nb,f,cnbf) & upair(##Lset(i),cnbf,cnbf,z))]"
by (intro FOL_reflections function_reflections)
lemma funspace_succ_replacement:
@@ -269,9 +269,9 @@
(\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) &
fx \<noteq> gx),
\<lambda>i x. \<exists>xa \<in> Lset(i). \<exists>xb \<in> Lset(i).
- pair(**Lset(i),x,a,xa) & xa \<in> r & pair(**Lset(i),x,b,xb) & xb \<in> r &
- (\<exists>fx \<in> Lset(i). \<exists>gx \<in> Lset(i). fun_apply(**Lset(i),f,x,fx) &
- fun_apply(**Lset(i),g,x,gx) & fx \<noteq> gx)]"
+ pair(##Lset(i),x,a,xa) & xa \<in> r & pair(##Lset(i),x,b,xb) & xb \<in> r &
+ (\<exists>fx \<in> Lset(i). \<exists>gx \<in> Lset(i). fun_apply(##Lset(i),f,x,fx) &
+ fun_apply(##Lset(i),g,x,gx) & fx \<noteq> gx)]"
by (intro FOL_reflections function_reflections fun_plus_reflections)
lemma is_recfun_separation:
--- a/src/ZF/OrdQuant.thy Wed Feb 05 13:35:32 2003 +0100
+++ b/src/ZF/OrdQuant.thy Thu Feb 06 11:01:05 2003 +0100
@@ -333,16 +333,16 @@
subsubsection{*Sets as Classes*}
-constdefs setclass :: "[i,i] => o" ("**_" [40] 40)
+constdefs setclass :: "[i,i] => o" ("##_" [40] 40)
"setclass(A) == %x. x : A"
lemma setclass_iff [simp]: "setclass(A,x) <-> x : A"
by (simp add: setclass_def)
-lemma rall_setclass_is_ball [simp]: "(\<forall>x[**A]. P(x)) <-> (\<forall>x\<in>A. P(x))"
+lemma rall_setclass_is_ball [simp]: "(\<forall>x[##A]. P(x)) <-> (\<forall>x\<in>A. P(x))"
by auto
-lemma rex_setclass_is_bex [simp]: "(\<exists>x[**A]. P(x)) <-> (\<exists>x\<in>A. P(x))"
+lemma rex_setclass_is_bex [simp]: "(\<exists>x[##A]. P(x)) <-> (\<exists>x\<in>A. P(x))"
by auto