632 ==> M_is_recfun(##A, MH, x, y, z) \<longleftrightarrow> sats(A, is_recfun_fm(p,i,j,k), env)" |
632 ==> M_is_recfun(##A, MH, x, y, z) \<longleftrightarrow> sats(A, is_recfun_fm(p,i,j,k), env)" |
633 by (simp add: sats_is_recfun_fm [OF MH_iff_sats]) |
633 by (simp add: sats_is_recfun_fm [OF MH_iff_sats]) |
634 |
634 |
635 text\<open>The additional variable in the premise, namely @{term f'}, is essential. |
635 text\<open>The additional variable in the premise, namely @{term f'}, is essential. |
636 It lets @{term MH} depend upon @{term x}, which seems often necessary. |
636 It lets @{term MH} depend upon @{term x}, which seems often necessary. |
637 The same thing occurs in @{text is_wfrec_reflection}.\<close> |
637 The same thing occurs in \<open>is_wfrec_reflection\<close>.\<close> |
638 theorem is_recfun_reflection: |
638 theorem is_recfun_reflection: |
639 assumes MH_reflection: |
639 assumes MH_reflection: |
640 "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)), |
640 "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)), |
641 \<lambda>i x. MH(##Lset(i), f'(x), f(x), g(x), h(x))]" |
641 \<lambda>i x. MH(##Lset(i), f'(x), f(x), g(x), h(x))]" |
642 shows "REFLECTS[\<lambda>x. M_is_recfun(L, MH(L,x), f(x), g(x), h(x)), |
642 shows "REFLECTS[\<lambda>x. M_is_recfun(L, MH(L,x), f(x), g(x), h(x)), |