--- 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)