# Theory Standard_Results

theory Standard_Results
imports Universal
begin

section ‹Kleene normal form and the number of $\mu$-operations›

text ‹Kleene's original normal form theorem~\<^cite>‹"Kleene43"› states that
every partial recursive $f$ can be expressed as $f(x) = u(\mu y[t(i, x, y) = 0]$ for some $i$, where $u$ and $t$ are specially crafted primitive recursive
functions tied to Kleene's definition of partial recursive functions.
Rogers~\<^cite>‹‹p.~29f.› in "Rogers87"› relaxes the theorem by allowing $u$ and $t$
to be any primitive recursive functions of arity one and three, respectively.
Both versions require a separate $t$-predicate for every arity. We will show
a unified version for all arities by treating $x$ as an encoded list of
arguments.

Our universal function @{thm[display,names_short] "r_univ_def"} can represent
all partial recursive functions (see theorem @{thm[source] r_univ}). Moreover
@{term "r_result"}, @{term "r_dec"}, and @{term "r_not"} are primitive
recursive. As such @{term r_univ} could almost serve as the right-hand side
$u(\mu y[t(i, x, y) = 0]$. Its only flaw is that the outer function, the
composition of @{term r_dec} and @{term r_result}, is ternary rather than
unary.›

lemma r_univ_almost_kleene_nf:
"r_univ ≃
(let u = Cn 3 r_dec [r_result];
t = Cn 3 r_not [r_result]
in Cn 2 u [Mn 2 t, Id 2 0, Id 2 1])"
unfolding r_univ_def by (rule exteqI) simp_all

text ‹We can remedy the wrong arity with some encoding and
projecting.›

definition r_nf_t :: recf where
"r_nf_t ≡ Cn 3 r_and
[Cn 3 r_eq [Cn 3 r_pdec2 [Id 3 0], Cn 3 r_prod_encode [Id 3 1, Id 3 2]],
Cn 3 r_not
[Cn 3 r_result
[Cn 3 r_pdec1 [Id 3 0],
Cn 3 r_pdec12 [Id 3 0],
Cn 3 r_pdec22 [Id 3 0]]]]"

lemma r_nf_t_prim: "prim_recfn 3 r_nf_t"
unfolding r_nf_t_def by simp

definition r_nf_u :: recf where
"r_nf_u ≡ Cn 1 r_dec [Cn 1 r_result [r_pdec1, r_pdec12, r_pdec22]]"

lemma r_nf_u_prim: "prim_recfn 1 r_nf_u"
unfolding r_nf_u_def by simp

lemma r_nf_t_0:
assumes "eval r_result [pdec1 y, pdec12 y, pdec22 y] ↓≠ 0"
and "pdec2 y = prod_encode (i, x)"
shows "eval r_nf_t [y, i, x] ↓= 0"
unfolding r_nf_t_def using assms by auto

lemma r_nf_t_1:
assumes "eval r_result [pdec1 y, pdec12 y, pdec22 y] ↓= 0 ∨ pdec2 y ≠ prod_encode (i, x)"
shows "eval r_nf_t [y, i, x] ↓= 1"
unfolding r_nf_t_def using assms r_result_total by auto

text ‹The next function is just as universal as @{term r_univ}, but
satisfies the conditions of the Kleene normal form theorem because the
outer funtion @{term r_nf_u} is unary.›

definition "r_normal_form ≡ Cn 2 r_nf_u [Mn 2 r_nf_t]"

lemma r_normal_form_recfn: "recfn 2 r_normal_form"
unfolding r_normal_form_def using r_nf_u_prim r_nf_t_prim by simp

lemma r_univ_exteq_r_normal_form: "r_univ ≃ r_normal_form"
proof (rule exteqI)
show arity: "arity r_univ = arity r_normal_form"
using r_normal_form_recfn by simp
show "eval r_univ xs = eval r_normal_form xs" if "length xs = arity r_univ" for xs
proof -
have "length xs = 2"
using that by simp
then obtain i x where ix: "[i, x] = xs"
by (smt Suc_length_conv length_0_conv numeral_2_eq_2)
have "eval r_univ [i, x] = eval r_normal_form [i, x]"
proof (cases "∀t. eval r_result [t, i, x] ↓= 0")
case True
then have "eval r_univ [i, x] ↑"
unfolding r_univ_def by simp
moreover have "eval r_normal_form [i, x] ↑"
proof -
have "eval r_nf_t [y, i, x] ↓= 1" for y
using True r_nf_t_1[of y i x] by fastforce
then show ?thesis
unfolding r_normal_form_def using r_nf_u_prim r_nf_t_prim by simp
qed
ultimately show ?thesis by simp
next
case False
then have "∃t. eval r_result [t, i, x] ↓≠ 0"
then obtain t where "eval r_result [t, i, x] ↓≠ 0"
by auto
then have "eval r_nf_t [triple_encode t i x, i, x] ↓= 0"
using r_nf_t_0 by simp
then obtain y where y: "eval (Mn 2 r_nf_t) [i, x] ↓= y"
using r_nf_t_prim Mn_free_imp_total by fastforce
then have "eval r_nf_t [y, i, x] ↓= 0"
using r_nf_t_prim Mn_free_imp_total eval_Mn_convergE(2)[of 2 r_nf_t "[i, x]" y]
by simp
then have r_result: "eval r_result [pdec1 y, pdec12 y, pdec22 y] ↓≠ 0"
and pdec2: "pdec2 y = prod_encode (i, x)"
using r_nf_t_0[of y i x] r_nf_t_1[of y i x] r_result_total by auto
then have "eval r_result [pdec1 y, i, x] ↓≠ 0"
by simp
then obtain v where v:
"eval r_univ [pdec12 y, pdec22 y] ↓= v"
"eval r_result [pdec1 y, pdec12 y, pdec22 y] ↓= Suc v"
using r_result r_result_bivalent'[of "pdec12 y" "pdec22 y" _ "pdec1 y"]
r_result_diverg'[of "pdec12 y" "pdec22 y" "pdec1 y"]
by auto

have "eval r_normal_form [i, x] = eval r_nf_u [y]"
unfolding r_normal_form_def using y r_nf_t_prim r_nf_u_prim by simp
also have "... = eval r_dec [the (eval (Cn 1 r_result [r_pdec1, r_pdec12, r_pdec22]) [y])]"
unfolding r_nf_u_def using r_result by simp
also have "... = eval r_dec [Suc v]"
using v by simp
also have "... ↓= v"
by simp
finally have "eval r_normal_form [i, x] ↓= v" .
moreover have "eval r_univ [i, x] ↓= v"
using v(1) pdec2 by simp
ultimately show ?thesis by simp
qed
with ix show ?thesis by simp
qed
qed

theorem normal_form:
assumes "recfn n f"
obtains i where "∀x. e_length x = n ⟶ eval r_normal_form [i, x] = eval f (list_decode x)"
proof -
have "eval r_normal_form [encode f, x] = eval f (list_decode x)" if "e_length x = n" for x
using r_univ_exteq_r_normal_form assms that exteq_def r_univ' by auto
then show ?thesis using that by auto
qed

text ‹As a consequence of the normal form theorem every partial
recursive function can be represented with exactly one application of the
$\mu$-operator.›

fun count_Mn :: "recf ⇒ nat" where
"count_Mn Z = 0"
| "count_Mn S = 0"
| "count_Mn (Id m n) = 0"
| "count_Mn (Cn n f gs) = count_Mn f + sum_list (map count_Mn gs)"
| "count_Mn (Pr n f g) = count_Mn f + count_Mn g"
| "count_Mn (Mn n f) = Suc (count_Mn f)"

lemma count_Mn_zero_iff_prim: "count_Mn f = 0 ⟷ Mn_free f"
by (induction f) auto

text ‹The normal form has only one $\mu$-recursion.›

lemma count_Mn_normal_form: "count_Mn r_normal_form = 1"
unfolding r_normal_form_def r_nf_u_def r_nf_t_def using count_Mn_zero_iff_prim by simp

lemma one_Mn_suffices:
assumes "recfn n f"
shows "∃g. count_Mn g = 1 ∧ g ≃ f"
proof -
have "n > 0"
using assms wellf_arity_nonzero by auto
obtain i where i:
"∀x. e_length x = n ⟶ eval r_normal_form [i, x] = eval f (list_decode x)"
using normal_form[OF assms(1)] by auto
define g where "g ≡ Cn n r_normal_form [r_constn (n - 1) i, r_list_encode (n - 1)]"
then have "recfn n g"
using r_normal_form_recfn ‹n > 0› by simp
then have "g ≃ f"
using g_def r_list_encode i assms by (intro exteqI) simp_all
moreover have "count_Mn g = 1"
unfolding g_def using count_Mn_normal_form count_Mn_zero_iff_prim by simp
ultimately show ?thesis by auto
qed

text ‹The previous lemma could have been obtained without @{term
"r_normal_form"} directly from @{term "r_univ"}.›

section ‹The $s$-$m$-$n$ theorem›

text ‹For all $m, n > 0$ there is an $(m + 1)$-ary primitive recursive
function $s^m_n$ with
$\varphi_p^{(m + n)}(c_1, \dots,c_m, x_1, \dots, x_n) = \varphi_{s^m_n(p, c_1, \dots,c_m)}^{(n)}(x_1, \dots, x_n)$
for all $p, c_1, \ldots, c_m, x_1, \ldots, x_n$. Here, $\varphi^{(n)}$ is a
function universal for $n$-ary partial recursive functions, which we will
represent by @{term "r_universal n"}›

text ‹The $s^m_n$ functions compute codes of functions. We start simple:
computing codes of the unary constant functions.›

fun code_const1 :: "nat ⇒ nat" where
"code_const1 0 = 0"
| "code_const1 (Suc c) = quad_encode 3 1 1 (singleton_encode (code_const1 c))"

lemma code_const1: "code_const1 c = encode (r_const c)"
by (induction c) simp_all

definition "r_code_const1_aux ≡
Cn 3 r_prod_encode
[r_constn 2 3,
Cn 3 r_prod_encode
[r_constn 2 1,
Cn 3 r_prod_encode
[r_constn 2 1, Cn 3 r_singleton_encode [Id 3 1]]]]"

lemma r_code_const1_aux_prim: "prim_recfn 3 r_code_const1_aux"

lemma r_code_const1_aux:
"eval r_code_const1_aux [i, r, c] ↓= quad_encode 3 1 1 (singleton_encode r)"

definition "r_code_const1 ≡ r_shrink (Pr 1 Z r_code_const1_aux)"

lemma r_code_const1_prim: "prim_recfn 1 r_code_const1"

lemma r_code_const1: "eval r_code_const1 [c] ↓= code_const1 c"
proof -
let ?h = "Pr 1 Z r_code_const1_aux"
have "eval ?h [c, x] ↓= code_const1 c" for x
using r_code_const1_aux r_code_const1_def
by (induction c) (simp_all add: r_code_const1_aux_prim)
then show ?thesis by (simp add: r_code_const1_def r_code_const1_aux_prim)
qed

text ‹Functions that compute codes of higher-arity constant functions:›

definition code_constn :: "nat ⇒ nat ⇒ nat" where
"code_constn n c ≡
if n = 1 then code_const1 c
else quad_encode 3 n (code_const1 c) (singleton_encode (triple_encode 2 n 0))"

lemma code_constn: "code_constn (Suc n) c = encode (r_constn n c)"
unfolding code_constn_def using code_const1 r_constn_def
by (cases "n = 0") simp_all

definition r_code_constn :: "nat ⇒ recf" where
"r_code_constn n ≡
if n = 1 then r_code_const1
else
Cn 1 r_prod_encode
[r_const 3,
Cn 1 r_prod_encode
[r_const n,
Cn 1 r_prod_encode
[r_code_const1,
Cn 1 r_singleton_encode
[Cn 1 r_prod_encode
[r_const 2, Cn 1 r_prod_encode [r_const n, Z]]]]]]"

lemma r_code_constn_prim: "prim_recfn 1 (r_code_constn n)"

lemma r_code_constn: "eval (r_code_constn n) [c] ↓= code_constn n c"
by (auto simp add: r_code_constn_def r_code_const1 code_constn_def r_code_const1_prim)

text ‹Computing codes of $m$-ary projections:›

definition code_id :: "nat ⇒ nat ⇒ nat" where
"code_id m n ≡ triple_encode 2 m n"

lemma code_id: "encode (Id m n) = code_id m n"
unfolding code_id_def by simp

text ‹The functions $s^m_n$ are represented by the following function.
The value $m$ corresponds to the length of @{term "cs"}.›

definition smn :: "nat ⇒ nat ⇒ nat list ⇒ nat" where
"smn n p cs ≡ quad_encode
3
n
(encode (r_universal (n + length cs)))
(list_encode (code_constn n p # map (code_constn n) cs @ map (code_id n) [0..<n]))"

lemma smn:
assumes "n > 0"
shows "smn n p cs = encode
(Cn n
(r_universal (n + length cs))
(r_constn (n - 1) p # map (r_constn (n - 1)) cs @ (map (Id n) [0..<n])))"
proof -
let ?p = "r_constn (n - 1) p"
let ?gs1 = "map (r_constn (n - 1)) cs"
let ?gs2 = "map (Id n) [0..<n]"
let ?gs = "?p # ?gs1 @ ?gs2"
have "map encode ?gs1 = map (code_constn n) cs"
by (intro nth_equalityI; auto; metis code_constn assms Suc_pred)
moreover have "map encode ?gs2 = map (code_id n) [0..<n]"
by (rule nth_equalityI) (auto simp add: code_id_def)
moreover have "encode ?p = code_constn n p"
using assms code_constn[of "n - 1" p] by simp
ultimately have "map encode ?gs =
code_constn n p # map (code_constn n) cs @ map (code_id n) [0..<n]"
by simp
then show ?thesis
unfolding smn_def using assms encode.simps(4) by presburger
qed

text ‹The next function is to help us define @{typ recf}s corresponding
to the $s^m_n$ functions. It maps $m + 1$ arguments $p, c_1, \ldots, c_m$ to
an encoded list of length $m + n + 1$. The list comprises the $m + 1$ codes
of the $n$-ary constants $p, c_1, \ldots, c_m$ and the $n$ codes for all
$n$-ary projections.›

definition r_smn_aux :: "nat ⇒ nat ⇒ recf" where
"r_smn_aux n m ≡
Cn (Suc m)
(r_list_encode (m + n))
(map (λi. Cn (Suc m) (r_code_constn n) [Id (Suc m) i]) [0..<Suc m] @
map (λi. r_constn m (code_id n i)) [0..<n])"

lemma r_smn_aux_prim: "n > 0 ⟹ prim_recfn (Suc m) (r_smn_aux n m)"
by (auto simp add: r_smn_aux_def r_code_constn_prim)

lemma r_smn_aux:
assumes "n > 0" and "length cs = m"
shows "eval (r_smn_aux n m) (p # cs) ↓=
list_encode (map (code_constn n) (p # cs) @ map (code_id n) [0..<n])"
proof -
let ?xs = "map (λi. Cn (Suc m) (r_code_constn n) [Id (Suc m) i]) [0..<Suc m]"
let ?ys = "map (λi. r_constn m (code_id n i)) [0..<n]"
have len_xs: "length ?xs = Suc m" by simp

have map_xs: "map (λg. eval g (p # cs)) ?xs = map Some (map (code_constn n) (p # cs))"
proof (intro nth_equalityI)
show len: "length (map (λg. eval g (p # cs)) ?xs) =
length (map Some (map (code_constn n) (p # cs)))"

have "map (λg. eval g (p # cs)) ?xs ! i = map Some (map (code_constn n) (p # cs)) ! i"
if "i < Suc m" for i
proof -
have "map (λg. eval g (p # cs)) ?xs ! i = (λg. eval g (p # cs)) (?xs ! i)"
using len_xs that by (metis nth_map)
also have "... = eval (Cn (Suc m) (r_code_constn n) [Id (Suc m) i]) (p # cs)"
using that len_xs
by (metis (no_types, lifting) add.left_neutral length_map nth_map nth_upt)
also have "... = eval (r_code_constn n) [the (eval (Id (Suc m) i) (p # cs))]"
using r_code_constn_prim assms(2) that by simp
also have "... = eval (r_code_constn n) [(p # cs) ! i]"
using len that by simp
finally have "map (λg. eval g (p # cs)) ?xs ! i ↓= code_constn n ((p # cs) ! i)"
using r_code_constn by simp
then show ?thesis
using len_xs len that by (metis length_map nth_map)
qed
moreover have "length (map (λg. eval g (p # cs)) ?xs) = Suc m" by simp
ultimately show "⋀i. i < length (map (λg. eval g (p # cs)) ?xs) ⟹
map (λg. eval g (p # cs)) ?xs ! i =
map Some (map (code_constn n) (p # cs)) ! i"
by simp
qed
moreover have "map (λg. eval g (p # cs)) ?ys = map Some (map (code_id n) [0..<n])"
using assms(2) by (intro nth_equalityI; auto)
ultimately have "map (λg. eval g (p # cs)) (?xs @ ?ys) =
map Some (map (code_constn n) (p # cs) @ map (code_id n) [0..<n])"
by (metis map_append)
moreover have "map (λx. the (eval x (p # cs))) (?xs @ ?ys) =
map the (map (λx. eval x (p # cs)) (?xs @ ?ys))"
by simp
ultimately have *: "map (λg. the (eval g (p # cs))) (?xs @ ?ys) =
(map (code_constn n) (p # cs) @ map (code_id n) [0..<n])"
by simp

have "∀i<length ?xs. eval (?xs ! i) (p # cs) = map (λg. eval g (p # cs)) ?xs ! i"
by (metis nth_map)
then have
"∀i<length ?xs. eval (?xs ! i) (p # cs) = map Some (map (code_constn n) (p # cs)) ! i"
using map_xs by simp
then have "∀i<length ?xs. eval (?xs ! i) (p # cs) ↓"
using assms map_xs by (metis length_map nth_map option.simps(3))
then have xs_converg: "∀z∈set ?xs. eval z (p # cs) ↓"
by (metis in_set_conv_nth)

have "∀i<length ?ys. eval (?ys ! i) (p # cs) = map (λx. eval x (p # cs)) ?ys ! i"
by simp
then have
"∀i<length ?ys. eval (?ys ! i) (p # cs) = map Some (map (code_id n) [0..<n]) ! i"
using assms(2) by simp
then have "∀i<length ?ys. eval (?ys ! i) (p # cs) ↓"
by simp
then have "∀z∈set (?xs @ ?ys). eval z (p # cs) ↓"
using xs_converg by auto
moreover have "recfn (length (p # cs)) (Cn (Suc m) (r_list_encode (m + n)) (?xs @ ?ys))"
using assms r_code_constn_prim by auto
ultimately have "eval (r_smn_aux n m) (p # cs) =
eval (r_list_encode (m + n)) (map (λg. the (eval g (p # cs))) (?xs @ ?ys))"
unfolding r_smn_aux_def using assms by simp
then have "eval (r_smn_aux n m) (p # cs) =
eval (r_list_encode (m + n)) (map (code_constn n) (p # cs) @ map (code_id n) [0..<n])"
using * by metis
moreover have "length (?xs @ ?ys) = Suc (m + n)" by simp
ultimately show ?thesis
using r_list_encode * assms(1) by (metis (no_types, lifting) length_map)
qed

text ‹For all $m, n > 0$, the @{typ recf} corresponding to $s^m_n$ is
given by the next function.›

definition r_smn :: "nat ⇒ nat ⇒ recf" where
"r_smn n m ≡
Cn (Suc m) r_prod_encode
[r_constn m 3,
Cn (Suc m) r_prod_encode
[r_constn m n,
Cn (Suc m) r_prod_encode
[r_constn m (encode (r_universal (n + m))), r_smn_aux n m]]]"

lemma r_smn_prim [simp]: "n > 0 ⟹ prim_recfn (Suc m) (r_smn n m)"

lemma r_smn:
assumes "n > 0" and "length cs = m"
shows "eval (r_smn n m) (p # cs) ↓= smn n p cs"
using assms r_smn_def r_smn_aux smn_def r_smn_aux_prim by simp

lemma map_eval_Some_the:
assumes "map (λg. eval g xs) gs = map Some ys"
shows "map (λg. the (eval g xs)) gs = ys"
using assms
by (metis (no_types, lifting) length_map nth_equalityI nth_map option.sel)

text ‹The essential part of the $s$-$m$-$n$ theorem: For all $m, n > 0$
the function $s^m_n$ satisfies
$\varphi_p^{(m + n)}(c_1, \dots,c_m, x_1, \dots, x_n) = \varphi_{s^m_n(p, c_1, \dots,c_m)}^{(n)}(x_1, \dots, x_n)$ for all $p, c_i, x_j$.›

lemma smn_lemma:
assumes "n > 0" and len_cs: "length cs = m" and len_xs: "length xs = n"
shows "eval (r_universal (m + n)) (p # cs @ xs) =
eval (r_universal n) ((the (eval (r_smn n m) (p # cs))) # xs)"
proof -
let ?s = "r_smn n m"
let ?f = "Cn n
(r_universal (n + length cs))
(r_constn (n - 1) p # map (r_constn (n - 1)) cs @ (map (Id n) [0..<n]))"
have "eval ?s (p # cs) ↓= smn n p cs"
using assms r_smn by simp
then have eval_s: "eval ?s (p # cs) ↓= encode ?f"

have "recfn n ?f"
using len_cs assms by auto
then have *: "eval (r_universal n) ((encode ?f) # xs) = eval ?f xs"
using r_universal[of ?f n, OF _ len_xs] by simp

let ?gs = "r_constn (n - 1) p # map (r_constn (n - 1)) cs @ map (Id n) [0..<n]"
have "∀g∈set ?gs. eval g xs ↓"
using len_cs len_xs assms by auto
then have "eval ?f xs =
eval (r_universal (n + length cs)) (map (λg. the (eval g xs)) ?gs)"
using len_cs len_xs assms ‹recfn n ?f› by simp
then have "eval ?f xs = eval (r_universal (m + n)) (map (λg. the (eval g xs)) ?gs)"
then have "eval (r_universal n) ((the (eval ?s (p # cs))) # xs) =
eval (r_universal (m + n)) (map (λg. the (eval g xs)) ?gs)"
using eval_s * by simp
moreover have "map (λg. the (eval g xs)) ?gs = p # cs @ xs"
proof (intro nth_equalityI)
show "length (map (λg. the (eval g xs)) ?gs) = length (p # cs @ xs)"
have len: "length (map (λg. the (eval g xs)) ?gs) = Suc (m + n)"
moreover have "map (λg. the (eval g xs)) ?gs ! i = (p # cs @ xs) ! i"
if "i < Suc (m + n)" for i
proof -
from that consider "i = 0" | "i > 0 ∧ i < Suc m" | "Suc m ≤ i ∧ i < Suc (m + n)"
using not_le_imp_less by auto
then show ?thesis
proof (cases)
case 1
then show ?thesis using assms(1) len_xs by simp
next
case 2
then have "?gs ! i = (map (r_constn (n - 1)) cs) ! (i - 1)"
using len_cs
by (metis One_nat_def Suc_less_eq Suc_pred length_map
less_numeral_extra(3) nth_Cons' nth_append)
then have "map (λg. the (eval g xs)) ?gs ! i =
(λg. the (eval g xs)) ((map (r_constn (n - 1)) cs) ! (i - 1))"
using len by (metis length_map nth_map that)
also have "... = the (eval ((r_constn (n - 1) (cs ! (i - 1)))) xs)"
using 2 len_cs by auto
also have "... = cs ! (i - 1)"
using r_constn len_xs assms(1) by simp
also have "... = (p # cs @ xs) ! i"
using 2 len_cs
by (metis diff_Suc_1 less_Suc_eq_0_disj less_numeral_extra(3) nth_Cons' nth_append)
finally show ?thesis .
next
case 3
then have "?gs ! i = (map (Id n) [0..<n]) ! (i - Suc m)"
using len_cs
by (simp; metis (no_types, lifting) One_nat_def Suc_less_eq add_leE
plus_1_eq_Suc diff_diff_left length_map not_le nth_append
then have "map (λg. the (eval g xs)) ?gs ! i =
(λg. the (eval g xs)) ((map (Id n) [0..<n]) ! (i - Suc m))"
using len by (metis length_map nth_map that)
also have "... = the (eval ((Id n (i - Suc m))) xs)"
using 3 len_cs by auto
also have "... = xs ! (i - Suc m)"
using len_xs 3 by auto
also have "... = (p # cs @ xs) ! i"
using len_cs len_xs 3
by (metis diff_Suc_1 diff_diff_left less_Suc_eq_0_disj not_le nth_Cons'
nth_append plus_1_eq_Suc)
finally show ?thesis .
qed
qed
ultimately show "map (λg. the (eval g xs)) ?gs ! i = (p # cs @ xs) ! i"
if "i < length (map (λg. the (eval g xs)) ?gs)" for i
using that by simp
qed
ultimately show ?thesis by simp
qed

theorem smn_theorem:
assumes "n > 0"
shows "∃s. prim_recfn (Suc m) s ∧
(∀p cs xs. length cs = m ∧ length xs = n ⟶
eval (r_universal (m + n)) (p # cs @ xs) =
eval (r_universal n) ((the (eval s (p # cs))) # xs))"
using smn_lemma exI[of _ "r_smn n m"] assms by simp

text ‹For every numbering, that is, binary partial recursive function,
$\psi$ there is a total recursive function $c$ that translates $\psi$-indices
into $\varphi$-indices.›

lemma numbering_translation:
assumes "recfn 2 psi"
obtains c where
"recfn 1 c"
"total c"
"∀i x. eval psi [i, x] = eval r_phi [the (eval c [i]), x]"
proof -
let ?p = "encode psi"
define c where "c = Cn 1 (r_smn 1 1) [r_const ?p, Id 1 0]"
then have "prim_recfn 1 c" by simp
moreover from this have "total c"
by auto
moreover have "eval r_phi [the (eval c [i]), x] = eval psi [i, x]" for i x
proof -
have "eval c [i] = eval (r_smn 1 1) [?p, i]"
using c_def by simp
then have "eval (r_universal 1) [the (eval c [i]), x] =
eval (r_universal 1) [the (eval (r_smn 1 1) [?p, i]), x]"
by simp
also have "... = eval (r_universal (1 + 1)) (?p # [i] @ [x])"
using smn_lemma[of 1 "[i]" 1 "[x]" ?p] by simp
also have "... = eval (r_universal 2) [?p, i, x]"
also have "... = eval psi [i, x]"
using r_universal[OF assms, of "[i, x]"] by simp
finally have "eval (r_universal 1) [the (eval c [i]), x] = eval psi [i, x]" .
then show ?thesis using r_phi_def by simp
qed
ultimately show ?thesis using that by auto
qed

section ‹Fixed-point theorems›

text ‹Fixed-point theorems (also known as recursion theorems) come in
many shapes. We prove the minimum we need for Chapter~\ref{c:iirf}.›

subsection ‹Rogers's fixed-point theorem›

text ‹In this section we prove a theorem that Rogers~\<^cite>‹"Rogers87"›
credits to Kleene, but admits that it is a special case and not the original
formulation. We follow Wikipedia~\<^cite>‹"wiki-krt"› and call it the Rogers's
fixed-point theorem.›

lemma s11_inj: "inj (λx. smn 1 p [x])"
proof
fix x⇩1 x⇩2 :: nat
assume "smn 1 p [x⇩1] = smn 1 p [x⇩2]"
then have "list_encode [code_constn 1 p, code_constn 1 x⇩1, code_id 1 0] =
list_encode [code_constn 1 p, code_constn 1 x⇩2, code_id 1 0]"
using smn_def by (simp add: prod_encode_eq)
then have "[code_constn 1 p, code_constn 1 x⇩1, code_id 1 0] =
[code_constn 1 p, code_constn 1 x⇩2, code_id 1 0]"
using list_decode_encode by metis
then have "code_constn 1 x⇩1 = code_constn 1 x⇩2" by simp
then show "x⇩1 = x⇩2"
using code_const1 code_constn code_constn_def encode_injective r_constn
by (metis One_nat_def length_Cons list.size(3) option.simps(1))
qed

definition "r_univuniv ≡ Cn 2 r_phi [Cn 2 r_phi [Id 2 0, Id 2 0], Id 2 1]"

lemma r_univuniv_recfn: "recfn 2 r_univuniv"

lemma r_univuniv_converg:
assumes "eval r_phi [x, x] ↓"
shows "eval r_univuniv [x, y] = eval r_phi [the (eval r_phi [x, x]), y]"
unfolding r_univuniv_def using assms r_univuniv_recfn r_phi_recfn by simp

text ‹Strictly speaking this is a generalization of Rogers's theorem in
that it shows the existence of infinitely many fixed-points. In conventional
terms it says that for every total recursive $f$ and $k \in \mathbb{N}$ there is
an $n \geq k$ with $\varphi_n = \varphi_{f(n)}$.›

theorem rogers_fixed_point_theorem:
fixes k :: nat
assumes "recfn 1 f" and "total f"
shows "∃n≥k. ∀x. eval r_phi [n, x] = eval r_phi [the (eval f [n]), x]"
proof -
let ?p = "encode r_univuniv"
define h where "h = Cn 1 (r_smn 1 1) [r_const ?p, Id 1 0]"
then have "prim_recfn 1 h"
by simp
then have "total h"
by blast
have "eval h [x] = eval (Cn 1 (r_smn 1 1) [r_const ?p, Id 1 0]) [x]" for x
unfolding h_def by simp
then have h: "the (eval h [x]) = smn 1 ?p [x]" for x

have "eval r_phi [the (eval h [x]), y] = eval r_univuniv [x, y]" for x y
proof -
have "eval r_phi [the (eval h [x]), y] = eval r_phi [smn 1 ?p [x], y]"
using h by simp
also have "... = eval r_phi [the (eval (r_smn 1 1) [?p, x]), y]"
also have "... = eval (r_universal 2) [?p, x, y]"
using r_phi_def smn_lemma[of 1 "[x]" 1 "[y]" ?p]
by (metis Cons_eq_append_conv One_nat_def Suc_1 length_Cons
less_numeral_extra(1) list.size(3) plus_1_eq_Suc)
finally show "eval r_phi [the (eval h [x]), y] = eval r_univuniv [x, y]"
using r_universal r_univuniv_recfn by simp
qed
then have *: "eval r_phi [the (eval h [x]), y] = eval r_phi [the (eval r_phi [x, x]), y]"
if "eval r_phi [x, x] ↓" for x y
using r_univuniv_converg that by simp

let ?fh = "Cn 1 f [h]"
have "recfn 1 ?fh"
using ‹prim_recfn 1 h› assms by simp
then have "infinite {r. recfn 1 r ∧ r ≃ ?fh}"
using exteq_infinite[of ?fh 1] by simp
then have "infinite (encode  {r. recfn 1 r ∧ r ≃ ?fh})" (is "infinite ?E")
using encode_injective by (meson finite_imageD inj_onI)
then have "infinite ((λx. smn 1 ?p [x])  ?E)"
using s11_inj[of ?p] by (simp add: finite_image_iff inj_on_subset)
moreover have "(λx. smn 1 ?p [x])  ?E = {smn 1 ?p [encode r] |r. recfn 1 r ∧ r ≃ ?fh}"
by auto
ultimately have "infinite {smn 1 ?p [encode r] |r. recfn 1 r ∧ r ≃ ?fh}"
by simp
then obtain n where "n ≥ k" "n ∈ {smn 1 ?p [encode r] |r. recfn 1 r ∧ r ≃ ?fh}"
by (meson finite_nat_set_iff_bounded_le le_cases)
then obtain r where r: "recfn 1 r" "n = smn 1 ?p [encode r]" "recfn 1 r ∧ r ≃ ?fh"
by auto
then have eval_r: "eval r [encode r] = eval ?fh [encode r]"
then have eval_r': "eval r [encode r] = eval f [the (eval h [encode r])]"
using assms ‹total h› ‹prim_recfn 1 h› by simp
then have "eval r [encode r] ↓"
using  ‹prim_recfn 1 h› assms(1,2) by simp
then have "eval r_phi [encode r, encode r] ↓"
by (simp add: ‹recfn 1 r› r_phi)
then have "eval r_phi [the (eval h [encode r]), y] =
eval r_phi [(the (eval r_phi [encode r, encode r])), y]"
for y
using * by simp
then have "eval r_phi [the (eval h [encode r]), y] =
eval r_phi [(the (eval r [encode r])), y]"
for y
by (simp add: ‹recfn 1 r› r_phi)
moreover have "n = the (eval h [encode r])" by (simp add: h r(2))
ultimately have "eval r_phi [n, y] = eval r_phi [the (eval r [encode r]), y]" for y
by simp
then have "eval r_phi [n, y] = eval r_phi [the (eval ?fh [encode r]), y]" for y
using r by (simp add: eval_r)
moreover have "eval ?fh [encode r] = eval f [n]"
using eval_r eval_r' ‹n = the (eval h [encode r])› by auto
ultimately have "eval r_phi [n, y] = eval r_phi [the (eval f [n]), y]" for y
by simp
with ‹n ≥ k› show ?thesis by auto
qed

subsection ‹Kleene's fixed-point theorem›

text ‹The next theorem is what Rogers~\<^cite>‹‹p.~214› in "Rogers87"› calls
Kleene's version of what we call Rogers's fixed-point theorem. More precisely
this would be Kleene's \emph{second} fixed-point theorem, but since we do not
cover the first one, we leave out the number.›

theorem kleene_fixed_point_theorem:
fixes k :: nat
assumes "recfn 2 psi"
shows "∃n≥k. ∀x. eval r_phi [n, x] = eval psi [n, x]"
proof -
from numbering_translation[OF assms] obtain c where c:
"recfn 1 c"
"total c"
"∀i x. eval psi [i, x] = eval r_phi [the (eval c [i]), x]"
by auto
then obtain n where "n ≥ k" and "∀x. eval r_phi [n, x] = eval r_phi [the (eval c [n]), x]"
using rogers_fixed_point_theorem by blast
with c(3) have "∀x. eval r_phi [n, x] = eval psi [n, x]"
by simp
with ‹n ≥ k› show ?thesis by auto
qed

text ‹Kleene's fixed-point theorem can be generalized to arbitrary
arities. But we need to generalize it only to binary functions in order to
show Smullyan's double fixed-point theorem in
Section~\ref{s:smullyan}.›

definition "r_univuniv2 ≡
Cn 3 r_phi [Cn 3 (r_universal 2) [Id 3 0, Id 3 0, Id 3 1], Id 3 2]"

lemma r_univuniv2_recfn: "recfn 3 r_univuniv2"

lemma r_univuniv2_converg:
assumes "eval (r_universal 2) [u, u, x] ↓"
shows "eval r_univuniv2 [u, x, y] = eval r_phi [the (eval (r_universal 2) [u, u, x]), y]"
unfolding r_univuniv2_def using assms r_univuniv2_recfn by simp

theorem kleene_fixed_point_theorem_2:
assumes "recfn 2 f" and "total f"
shows "∃n.
recfn 1 n ∧
total n ∧
(∀x y. eval r_phi [(the (eval n [x])), y] = eval r_phi [(the (eval f [the (eval n [x]), x])), y])"
proof -
let ?p = "encode r_univuniv2"
let ?s = "r_smn 1 2"
define h where "h = Cn 2 ?s [r_dummy 1 (r_const ?p), Id 2 0, Id 2 1]"
then have [simp]: "prim_recfn 2 h" by simp
{
fix u x y
have "eval h [u, x] = eval (Cn 2 ?s [r_dummy 1 (r_const ?p), Id 2 0, Id 2 1]) [u, x]"
using h_def by simp
then have "the (eval h [u, x]) = smn 1 ?p [u, x]"
then have "eval r_phi [the (eval h [u, x]), y] = eval r_phi [smn 1 ?p [u, x], y]"
by simp
also have "... =
eval r_phi
[encode (Cn 1 (r_universal 3) (r_constn 0 ?p # r_constn 0 u # r_constn 0 x # [Id 1 0])),
y]"
using smn[of 1 ?p "[u, x]"] by (simp add: numeral_3_eq_3)
also have "... =
eval r_phi
[encode (Cn 1 (r_universal 3) (r_const ?p # r_const u # r_const x # [Id 1 0])), y]"
(is "_ = eval r_phi [encode ?f, y]")
also have "... = eval ?f [y]"
using r_phi'[of ?f] by auto
also have "... = eval (r_universal 3) [?p, u, x, y]"
using r_univuniv2_recfn r_universal r_phi by auto
also have "... = eval r_univuniv2 [u, x, y]"
using r_universal
finally have "eval r_phi [the (eval h [u, x]), y] =  eval r_univuniv2 [u, x, y]" .
}
then have *: "eval r_phi [the (eval h [u, x]), y] =
eval r_phi [the (eval (r_universal 2) [u, u, x]), y]"
if "eval (r_universal 2) [u, u, x] ↓" for u x y
using r_univuniv2_converg that by simp

let ?fh = "Cn 2 f [h, Id 2 1]"
let ?e = "encode ?fh"
have "recfn 2 ?fh"
using assms by simp
have "total h"
by auto
then have "total ?fh"
using assms Cn_total totalI2[of ?fh] by fastforce

let ?n = "Cn 1 h [r_const ?e, Id 1 0]"
have "recfn 1 ?n"
using assms by simp
moreover have "total ?n"
using ‹total h› totalI1[of ?n] by simp
moreover {
fix x y
have "eval r_phi [(the (eval ?n [x])), y] = eval r_phi [(the (eval h [?e, x])), y]"
by simp
also have "... = eval r_phi [the (eval (r_universal 2) [?e, ?e, x]), y]"
using * r_universal[of _ 2] totalE[of ?fh 2] ‹total ?fh› ‹recfn 2 ?fh›
by (metis length_Cons list.size(3) numeral_2_eq_2)
also have "... = eval r_phi [the (eval f [the (eval h [?e, x]), x]), y]"
proof -
have "eval (r_universal 2) [?e, ?e, x] ↓"
using totalE[OF ‹total ?fh›] ‹recfn 2 ?fh› r_universal
by (metis length_Cons list.size(3) numeral_2_eq_2)
moreover have "eval (r_universal 2) [?e, ?e, x] = eval ?fh [?e, x]"
by (metis ‹recfn 2 ?fh› length_Cons list.size(3) numeral_2_eq_2 r_universal)
then show ?thesis using assms ‹total h› by simp
qed
also have "... =  eval r_phi [(the (eval f [the (eval ?n [x]), x])), y]"
by simp
finally have "eval r_phi [(the (eval ?n [x])), y] =
eval r_phi [(the (eval f [the (eval ?n [x]), x])), y]" .
}
ultimately show ?thesis by blast
qed

subsection ‹Smullyan's double fixed-point theorem\label{s:smullyan}›

theorem smullyan_double_fixed_point_theorem:
assumes "recfn 2 g" and "total g" and "recfn 2 h" and "total h"
shows "∃m n.
(∀x. eval r_phi [m, x] = eval r_phi [the (eval g [m, n]), x]) ∧
(∀x. eval r_phi [n, x] = eval r_phi [the (eval h [m, n]), x])"
proof -
obtain m where
"recfn 1 m" and
"total m" and
m: "∀x y. eval r_phi [the (eval m [x]), y] =
eval r_phi [the (eval g [the (eval m [x]), x]), y]"
using kleene_fixed_point_theorem_2[of g] assms(1,2) by auto
define k where "k = Cn 1 h [m, Id 1 0]"
then have "recfn 1 k"
using ‹recfn 1 m› assms(3) by simp
have "total (Id 1 0)"
then have "total k"
using ‹total m› assms(4) Cn_total k_def ‹recfn 1 k› by simp
obtain n where n: "∀x. eval r_phi [n, x] = eval r_phi [the (eval k [n]), x]"
using rogers_fixed_point_theorem[of k] ‹recfn 1 k› ‹total k› by blast
obtain mm where mm: "eval m [n] ↓= mm"
using ‹total m› ‹recfn 1 m› by fastforce
then have "∀x. eval r_phi [mm, x] = eval r_phi [the (eval g [mm, n]), x]"
by (metis m option.sel)
moreover have "∀x. eval r_phi [n, x] = eval r_phi [the (eval h [mm, n]), x]"
using k_def assms(3) ‹total m› ‹recfn 1 m› mm n by simp
ultimately show ?thesis by blast
qed

section ‹Decidable and recursively enumerable sets\label{s:decidable}›

text ‹We defined @{term decidable} already back in
Section~\ref{s:halting}: @{thm[display] decidable_def}›

text ‹The next theorem is adapted from @{thm[source]
halting_problem_undecidable}.›

theorem halting_problem_phi_undecidable: "¬ decidable {x. eval r_phi [x, x] ↓}"
(is "¬ decidable ?K")
proof
assume "decidable ?K"
then obtain f where "recfn 1 f" and f: "∀x. eval f [x] ↓= (if x ∈ ?K then 1 else 0)"
using decidable_def by auto
define g where "g ≡ Cn 1 r_ifeq_else_diverg [f, Z, Z]"
then have "recfn 1 g"
using ‹recfn 1 f› r_ifeq_else_diverg_recfn by simp
then obtain i where i: "eval r_phi [i, x] = eval g [x]" for x
using r_phi' by auto
from g_def have "eval g [x] = (if x ∉ ?K then Some 0 else None)" for x
using r_ifeq_else_diverg_recfn ‹recfn 1 f› f by simp
then have "eval g [i] ↓ ⟷ i ∉ ?K" by simp
also have "... ⟷ eval r_phi [i, i] ↑" by simp
also have "... ⟷ eval g [i] ↑"
using i by simp
finally have "eval g [i] ↓ ⟷ eval g [i] ↑" .
then show False by auto
qed

lemma decidable_complement: "decidable X ⟹ decidable (- X)"
proof -
assume "decidable X"
then obtain f where f: "recfn 1 f" "∀x. eval f [x] ↓= (if x ∈ X then 1 else 0)"
using decidable_def by auto
define g where "g = Cn 1 r_not [f]"
then have "recfn 1 g"
moreover have "eval g [x] ↓= (if x ∈ X then 0 else 1)" for x
ultimately show ?thesis using decidable_def by auto
qed

text ‹Finite sets are decidable.›

fun r_contains :: "nat list ⇒ recf" where
"r_contains [] = Z"
| "r_contains (x # xs) = Cn 1 r_ifeq [Id 1 0, r_const x, r_const 1, r_contains xs]"

lemma r_contains_prim: "prim_recfn 1 (r_contains xs)"
by (induction xs) auto

lemma r_contains: "eval (r_contains xs) [x] ↓= (if x ∈ set xs then 1 else 0)"
proof (induction xs arbitrary: x)
case Nil
then show ?case by simp
next
case (Cons a xs)
have "eval (r_contains (a # xs)) [x] = eval r_ifeq [x, a, 1, the (eval (r_contains xs) [x])]"
using r_contains_prim prim_recfn_total by simp
also have "... ↓= (if x = a then 1 else if x ∈ set xs then 1 else 0)"
using Cons.IH by simp
also have "... ↓= (if x = a ∨ x ∈ set xs then 1 else 0)"
by simp
finally show ?case by simp
qed

lemma finite_set_decidable: "finite X ⟹ decidable X"
proof -
fix X :: "nat set"
assume "finite X"
then obtain xs where "X = set xs"
using finite_list by auto
then have "∀x. eval (r_contains xs) [x] ↓= (if x ∈ X then 1 else 0)"
using r_contains by simp
then show "decidable X"
using decidable_def r_contains_prim by blast
qed

definition semidecidable :: "nat set ⇒ bool" where
"semidecidable X ≡ (∃f. recfn 1 f ∧ (∀x. eval f [x] = (if x ∈ X then Some 1 else None)))"

text ‹The semidecidable sets are the domains of partial recursive functions.›

lemma semidecidable_iff_domain:
"semidecidable X ⟷ (∃f. recfn 1 f ∧ (∀x. eval f [x] ↓ ⟷ x ∈ X))"
proof
show "semidecidable X ⟹ ∃f. recfn 1 f ∧ (∀x. (eval f [x] ↓) = (x ∈ X))"
using semidecidable_def by (metis option.distinct(1))
show "semidecidable X" if "∃f. recfn 1 f ∧ (∀x. (eval f [x] ↓) = (x ∈ X))" for X
proof -
from that obtain f where f: "recfn 1 f" "∀x. (eval f [x] ↓) = (x ∈ X)"
by auto
let ?g = "Cn 1 (r_const 1) [f]"
have "recfn 1 ?g"
using f(1) by simp
moreover have "∀x. eval ?g [x] = (if x ∈ X then Some 1 else None)"
using f by simp
ultimately show "semidecidable X"
using semidecidable_def by blast
qed
qed

lemma decidable_imp_semidecidable: "decidable X ⟹ semidecidable X"
proof -
assume "decidable X"
then obtain f where f: "recfn 1 f" "∀x. eval f [x] ↓= (if x ∈ X then 1 else 0)"
using decidable_def by auto
define g where "g = Cn 1 r_ifeq_else_diverg [f, r_const 1, r_const 1]"
then have "recfn 1 g"
have "eval g [x] = eval r_ifeq_else_diverg [if x ∈ X then 1 else 0, 1, 1]" for x
then have "⋀x. x ∈ X ⟹ eval g [x] ↓= 1" and "⋀x. x ∉ X ⟹ eval g [x] ↑"
by simp_all
then show ?thesis
using ‹recfn 1 g› semidecidable_def by auto
qed

text ‹A set is recursively enumerable if it is empty or the image of a
total recursive function.›

definition recursively_enumerable :: "nat set ⇒ bool" where
"recursively_enumerable X ≡
X = {} ∨ (∃f. recfn 1 f ∧ total f ∧ X = {the (eval f [x]) |x. x ∈ UNIV})"

theorem recursively_enumerable_iff_semidecidable:
"recursively_enumerable X ⟷ semidecidable X"
proof
show "semidecidable X" if "recursively_enumerable X" for X
proof (cases)
assume "X = {}"
then show ?thesis
using finite_set_decidable decidable_imp_semidecidable
recursively_enumerable_def semidecidable_def
by blast
next
assume "X ≠ {}"
with that obtain f where f: "recfn 1 f" "total f" "X = {the (eval f [x]) |x. x ∈ UNIV}"
using recursively_enumerable_def by blast
define h where "h = Cn 2 r_eq [Cn 2 f [Id 2 0], Id 2 1]"
then have "recfn 2 h"
using f(1) by simp
from h_def have h: "eval h [x, y] ↓= 0 ⟷ the (eval f [x]) = y" for x y
using f(1,2) by simp
from h_def ‹recfn 2 h› totalI2 f(2) have "total h" by simp
define g where "g = Mn 1 h"
then have "recfn 1 g"
using h_def f(1) by simp
then have "eval g [y] =
(if (∃x. eval h [x, y] ↓= 0 ∧ (∀x'<x. eval h [x', y] ↓))
then Some (LEAST x. eval h [x, y] ↓= 0)
else None)" for y
using g_def ‹total h› f(2) by simp
then have "eval g [y] =
(if ∃x. eval h [x, y] ↓= 0
then Some (LEAST x. eval h [x, y] ↓= 0)
else None)" for y
using ‹total h› ‹recfn 2 h› by simp
then have "eval g [y] ↓ ⟷ (∃x. eval h [x, y] ↓= 0)" for y
by simp
with h have "eval g [y] ↓ ⟷ (∃x. the (eval f [x]) = y)" for y
by simp
with f(3) have "eval g [y] ↓ ⟷ y ∈ X" for y
by auto
with ‹recfn 1 g› semidecidable_iff_domain show ?thesis by auto
qed

show "recursively_enumerable X" if "semidecidable X" for X
proof (cases)
assume "X = {}"
then show ?thesis using recursively_enumerable_def by simp
next
assume "X ≠ {}"
then obtain x⇩0 where "x⇩0 ∈ X" by auto
from that semidecidable_iff_domain obtain f where f: "recfn 1 f" "∀x. eval f [x] ↓ ⟷ x ∈ X"
by auto
let ?i = "encode f"
have i: "⋀x. eval f [x] = eval r_phi [?i, x]"
using r_phi' f(1) by simp
with ‹x⇩0 ∈ X› f(2) have "eval r_phi [?i, x⇩0] ↓" by simp
then obtain g where g: "recfn 1 g" "total g" "∀x. eval r_phi [?i, x] ↓ = (∃y. eval g [y] ↓= x)"
using f(1) nonempty_domain_enumerable by blast
with f(2) i have "∀x. x ∈ X = (∃y. eval g [y] ↓= x)"
by simp
then have "∀x. x ∈ X = (∃y. the (eval g [y]) = x)"
using totalE[OF g(2) g(1)]
by (metis One_nat_def length_Cons list.size(3) option.collapse option.sel)
then have "X = {the (eval g [y]) |y. y ∈ UNIV}"
by auto
with g(1,2) show ?thesis using recursively_enumerable_def by auto
qed
qed

text ‹The next goal is to show that a set is decidable iff. it and its
complement are semidecidable. For this we use the concurrent evaluation
function.›

lemma semidecidable_decidable:
assumes "semidecidable X" and "semidecidable (- X)"
shows "decidable X"
proof -
obtain f where f: "recfn 1 f ∧ (∀x. eval f [x] ↓ ⟷ x ∈ X)"
using assms(1) semidecidable_iff_domain by auto
let ?i = "encode f"
obtain g where g: "recfn 1 g ∧ (∀x. eval g [x] ↓ ⟷ x ∈ (- X))"
using assms(2) semidecidable_iff_domain by auto
let ?j = "encode g"
define d where "d = Cn 1 r_pdec1 [Cn 1 r_parallel [r_const ?j, r_const ?i, Id 1 0]]"
then have "recfn 1 d"
have *: "⋀x. eval r_phi [?i, x] = eval f [x]" "⋀x. eval r_phi [?j, x] = eval g [x]"
using f g r_phi' by simp_all
have "eval d [x] ↓= 1" if "x ∈ X" for x
proof -
have "eval f [x] ↓"
using f that by simp
moreover have "eval g [x] ↑"
using g that by blast
ultimately have "eval r_parallel [?j, ?i, x] ↓= prod_encode (1, the (eval f [x]))"
using * r_parallel(3) by simp
with d_def show ?thesis by simp
qed
moreover have "eval d [x] ↓= 0" if "x ∉ X" for x
proof -
have "eval g [x] ↓"
using g that by simp
moreover have "eval f [x] ↑"
using f that by blast
ultimately have "eval r_parallel [?j, ?i, x] ↓= prod_encode (0, the (eval g [x]))"
using * r_parallel(2) by blast
with d_def show ?thesis by simp
qed
ultimately show ?thesis
using decidable_def ‹recfn 1 d› by auto
qed

theorem decidable_iff_semidecidable_complement:
"decidable X ⟷ semidecidable X ∧ semidecidable (- X)"
using semidecidable_decidable decidable_imp_semidecidable decidable_complement
by blast

section ‹Rice's theorem›

definition index_set :: "nat set ⇒ bool" where
"index_set I ≡ ∀i j. i ∈ I ∧ (∀x. eval r_phi [i, x] = eval r_phi [j, x]) ⟶ j ∈ I"

lemma index_set_closed_in:
assumes "index_set I" and "i ∈ I" and "∀x. eval r_phi [i, x] = eval r_phi [j, x]"
shows "j ∈ I"
using index_set_def assms by simp

lemma index_set_closed_not_in:
assumes "index_set I" and "i ∉ I" and "∀x. eval r_phi [i, x] = eval r_phi [j, x]"
shows "j ∉ I"
using index_set_def assms by metis

theorem rice_theorem:
assumes "index_set I" and "I ≠ UNIV" and "I ≠ {}"
shows "¬ decidable I"
proof
assume "decidable I"
then obtain d where d: "recfn 1 d" "∀i. eval d [i] ↓= (if i ∈ I then 1 else 0)"
using decidable_def by auto
obtain j⇩1 j⇩2 where "j⇩1 ∉ I" and "j⇩2 ∈ I"
using assms(2,3) by auto
let ?if = "Cn 2 r_ifz [Cn 2 d [Id 2 0], r_dummy 1 (r_const j⇩2), r_dummy 1 (r_const j⇩1)]"
define psi where "psi = Cn 2 r_phi [?if, Id 2 1] "
then have "recfn 2 psi"
have "eval ?if [x, y] = Some (if x ∈ I then j⇩1 else j⇩2)" for x y
moreover have "eval psi [x, y] = eval (Cn 2 r_phi [?if, Id 2 1]) [x, y]" for x y
using psi_def by simp
ultimately have psi: "eval psi [x, y] = eval r_phi [if x ∈ I then j⇩1 else j⇩2, y]" for x y
then have in_I: "eval psi [x, y] = eval r_phi [j⇩1, y]" if "x ∈ I" for x y
have not_in_I: "eval psi [x, y] = eval r_phi [j⇩2, y]" if "x ∉ I" for x y
obtain n where n: "∀x. eval r_phi [n, x] = eval psi [n, x]"
using kleene_fixed_point_theorem[OF ‹recfn 2 psi›] by auto
show False
proof cases
assume "n ∈ I"
then have "∀x. eval r_phi [n, x] = eval r_phi [j⇩1, x]"
using n in_I by simp
then have "n ∉ I"
using ‹j⇩1 ∉ I› index_set_closed_not_in[OF assms(1)] by simp
with ‹n ∈ I› show False by simp
next
assume "n ∉ I"
then have "∀x. eval r_phi [n, x] = eval r_phi [j⇩2, x]"
using n not_in_I by simp
then have "n ∈ I"
using ‹j⇩2 ∈ I› index_set_closed_in[OF assms(1)] by simp
with ‹n ∉ I› show False by simp
qed
qed

section ‹Partial recursive functions as actual functions\label{s:alternative}›

text ‹A well-formed @{typ recf} describes an algorithm. Usually,
however, partial recursive functions are considered to be partial functions,
that is, right-unique binary relations. This distinction did not matter much
until now, because we were mostly concerned with the \emph{existence} of
partial recursive functions, which is equivalent to the existence of
algorithms. Whenever it did matter, we could use the extensional equivalence
@{term "exteq"}. In Chapter~\ref{c:iirf}, however, we will deal with sets of
functions and sets of sets of functions.

For illustration consider the singleton set containing only the unary zero
function. It could be expressed by @{term "{Z}"}, but this would not contain
@{term[names_short] "Cn 1 (Id 1 0) [Z]"}, which computes the same function.
The alternative representation as @{term "{f. f ≃ Z}"} is not a
singleton set. Another alternative would be to identify partial recursive
functions with the equivalence classes of @{term "exteq"}. This would work
for all arities. But since we will only need unary and binary functions, we
can go for the less general but simpler alternative of regarding partial
recursive functions as certain functions of types @{typ "nat ⇒
nat option"} and @{typ "nat ⇒ nat ⇒ nat option"}.
With this notation we can represent the aforementioned set by @{term
"{λ_. Some (0::nat)}"} and express that the function @{term "λ_.
Some (0::nat)"} is total recursive.

In addition terms get shorter, for instance, @{term "eval r_func [i, x]"}
becomes @{term "func i x"}.›

subsection ‹The definitions›

type_synonym partial1 = "nat ⇒ nat option"

type_synonym partial2 = "nat ⇒ nat ⇒ nat option"

definition total1 :: "partial1 ⇒ bool" where
"total1 f ≡ ∀x. f x ↓"

definition total2 :: "partial2 ⇒ bool" where
"total2 f ≡ ∀x y. f x y ↓"

lemma total1I [intro]: "(⋀x. f x ↓) ⟹ total1 f"
using total1_def by simp

lemma total2I [intro]: "(⋀x y. f x y ↓) ⟹ total2 f"
using total2_def by simp

lemma total1E [dest, simp]: "total1 f ⟹ f x ↓"
using total1_def by simp

lemma total2E [dest, simp]: "total2 f ⟹ f x y ↓"
using total2_def by simp

definition P1 :: "partial1 set" ("𝒫") where
"𝒫 ≡ {λx. eval r [x] |r. recfn 1 r}"

definition P2 :: "partial2 set" ("𝒫⇧2") where
"𝒫⇧2 ≡ {λx y. eval r [x, y] |r. recfn 2 r}"

definition R1 :: "partial1 set" ("ℛ") where
"ℛ ≡ {λx. eval r [x] |r. recfn 1 r ∧ total r}"

definition R2 :: "partial2 set" ("ℛ⇧2") where
"ℛ⇧2 ≡ {λx y. eval r [x, y] |r. recfn 2 r ∧ total r}"

definition Prim1 :: "partial1 set" where
"Prim1 ≡ {λx. eval r [x] |r. prim_recfn 1 r}"

definition Prim2 :: "partial2 set" where
"Prim2 ≡ {λx y. eval r [x, y] |r. prim_recfn 2 r}"

lemma R1_imp_P1 [simp, elim]: "f ∈ ℛ ⟹ f ∈ 𝒫"
using R1_def P1_def by auto

lemma R2_imp_P2 [simp, elim]: "f ∈ ℛ⇧2 ⟹ f ∈ 𝒫⇧2"
using R2_def P2_def by auto

lemma Prim1_imp_R1 [simp, elim]: "f ∈ Prim1 ⟹ f ∈ ℛ"
unfolding Prim1_def R1_def by auto

lemma Prim2_imp_R2 [simp, elim]: "f ∈ Prim2 ⟹ f ∈ ℛ⇧2"
unfolding Prim2_def R2_def by auto

lemma P1E [elim]:
assumes "f ∈ 𝒫"
obtains r where "recfn 1 r" and "∀x. eval r [x] = f x"
using assms P1_def by force

lemma P2E [elim]:
assumes "f ∈ 𝒫⇧2"
obtains r where "recfn 2 r" and "∀x y. eval r [x, y] = f x y"
using assms P2_def by force

lemma P1I [intro]:
assumes "recfn 1 r" and "(λx. eval r [x]) = f"
shows "f ∈ 𝒫"
using assms P1_def by auto

lemma P2I [intro]:
assumes "recfn 2 r" and "⋀x y. eval r [x, y] = f x y"
shows "f ∈ 𝒫⇧2"
proof -
have "(λx y. eval r [x, y]) = f"
using assms(2) by simp
then show ?thesis
using assms(1) P2_def by auto
qed

lemma R1I [intro]:
assumes "recfn 1 r" and "total r" and "⋀x. eval r [x] = f x"
shows "f ∈ ℛ"
unfolding R1_def
using CollectI[of "λf. ∃r. f = (λx. eval r [x]) ∧ recfn 1 r ∧ total r" f] assms
by metis

lemma R1E [elim]:
assumes "f ∈ ℛ"
obtains r where "recfn 1 r" and "total r" and "f = (λx. eval r [x])"
using assms R1_def by auto

lemma R2I [intro]:
assumes "recfn 2 r" and "total r" and "⋀x y. eval r [x, y] = f x y"
shows "f ∈ ℛ⇧2"
unfolding R2_def
using CollectI[of "λf. ∃r. f = (λx y. eval r [x, y]) ∧ recfn 2 r ∧ total r" f] assms
by metis

lemma R1_SOME:
assumes "f ∈ ℛ"
and "r = (SOME r'. recfn 1 r' ∧  total r' ∧ f = (λx. eval r' [x]))"
(is "r = (SOME r'. ?P r')")
shows "recfn 1 r"
and "⋀x. eval r [x] ↓"
and "⋀x. f x = eval r [x]"
and "f = (λx. eval r [x])"
proof -
obtain r' where "?P r'"
using R1E[OF assms(1)] by auto
then show "recfn 1 r" "⋀b. eval r [b] ↓" "⋀x. f x = eval r [x]"
using someI[of ?P r'] assms(2) totalE[of r] by (auto, metis)
then show "f = (λx. eval r [x])" by auto
qed

lemma R2E [elim]:
assumes "f ∈ ℛ⇧2"
obtains r where "recfn 2 r" and "total r" and "f = (λx⇩1 x⇩2. eval r [x⇩1, x⇩2])"
using assms R2_def by auto

lemma R1_imp_total1 [simp]: "f ∈ ℛ ⟹ total1 f"
using total1I by fastforce

lemma R2_imp_total2 [simp]: "f ∈ ℛ⇧2 ⟹ total2 f"
using totalE by fastforce

lemma Prim1I [intro]:
assumes "prim_recfn 1 r" and "⋀x. f x = eval r [x]"
shows "f ∈ Prim1"
using assms Prim1_def by blast

lemma Prim2I [intro]:
assumes "prim_recfn 2 r" and "⋀x y. f x y = eval r [x, y]"
shows "f ∈ Prim2"
using assms Prim2_def by blast

lemma P1_total_imp_R1 [intro]:
assumes "f ∈ 𝒫" and "total1 f"
shows "f ∈ ℛ"
using assms totalI1 by force

lemma P2_total_imp_R2 [intro]:
assumes "f ∈ 𝒫⇧2 " and "total2 f"
shows "f ∈ ℛ⇧2"
using assms totalI2 by force

subsection ‹Some simple properties›

text ‹In order to show that a @{typ partial1} or @{typ partial2}
function is in @{term "𝒫"}, @{term "𝒫⇧2"}, @{term "ℛ"}, @{term
"ℛ⇧2"}, @{term "Prim1"}, or @{term "Prim2"} we will usually have to
find a suitable @{typ recf}. But for some simple or frequent cases this
section provides shortcuts.›

lemma identity_in_R1: "Some ∈ ℛ"
proof -
have "∀x. eval (Id 1 0) [x] ↓= x" by simp
moreover have "recfn 1 (Id 1 0)" by simp
moreover have "total (Id 1 0)"
ultimately show ?thesis by blast
qed

lemma P2_proj_P1 [simp, elim]:
assumes "ψ ∈ 𝒫⇧2"
shows "ψ i ∈ 𝒫"
proof -
from assms obtain u where u: "recfn 2 u" "(λx⇩1 x⇩2. eval u [x⇩1, x⇩2]) = ψ"
by auto
define v where "v ≡ Cn 1 u [r_const i, Id 1 0]"
then have "recfn 1 v" "(λx. eval v [x]) = ψ i"
using u by auto
then show ?thesis by auto
qed

lemma R2_proj_R1 [simp, elim]:
assumes "ψ ∈ ℛ⇧2"
shows "ψ i ∈ ℛ"
proof -
from assms have "ψ ∈ 𝒫⇧2" by simp
then have "ψ i ∈ 𝒫" by auto
moreover have "total1 (ψ i)"
using assms by (simp add: total1I)
ultimately show ?thesis by auto
qed

lemma const_in_Prim1: "(λ_. Some c) ∈ Prim1"
proof -
define r where "r = r_const c"
then have "⋀x. eval r [x] = Some c" by simp
moreover have "recfn 1 r" "Mn_free r"
using r_def by simp_all
ultimately show ?thesis by auto
qed

lemma concat_P1_P1:
assumes "f ∈ 𝒫" and "g ∈ 𝒫"
shows "(λx. if g x ↓ ∧ f (the (g x)) ↓ then Some (the (f (the (g x)))) else None) ∈ 𝒫"
(is "?h ∈ 𝒫")
proof -
obtain rf where rf: "recfn 1 rf" "∀x. eval rf [x] = f x"
using assms(1) by auto
obtain rg where rg: "recfn 1 rg" "∀x. eval rg [x] = g x"
using assms(2) by auto
let ?rh = "Cn 1 rf [rg]"
have "recfn 1 ?rh"
using rf(1) rg(1) by simp
moreover have "eval ?rh [x] = ?h x" for x
using rf rg by simp
ultimately show ?thesis by blast
qed

lemma P1_update_P1:
assumes "f ∈ 𝒫"
shows "f(x:=z) ∈ 𝒫"
proof (cases z)
case None
define re where "re ≡ Mn 1 (r_constn 1 1)"
from assms obtain r where r: "recfn 1 r" "(λu. eval r [u]) = f"
by auto
define r' where "r' = Cn 1 (r_lifz re r) [Cn 1 r_eq [Id 1 0, r_const x], Id 1 0]"
have "recfn 1 r'"
using r(1) r'_def re_def by simp
then have "eval r' [u] = eval (r_lifz re r) [if u = x then 0 else 1, u]" for u
using r'_def by simp
with r(1) have "eval r' [u] = (if u = x then None else eval r [u])" for u
using re_def re_def by simp
with r(2) have "eval r' [u] = (f(x:=None)) u" for u
by auto
then have "(λu. eval r' [u]) = f(x:=None)"
by auto
with None ‹recfn 1 r'› show ?thesis by auto
next
case (Some y)
from assms obtain r where r: "recfn 1 r" "(λu. eval r [u]) `