# Theory Partial_Recursive

chapter ‹Partial recursive functions›

theory Partial_Recursive
imports Main "HOL-Library.Nat_Bijection"
begin

text ‹This chapter lays the foundation for Chapter~\ref{c:iirf}.
Essentially it develops recursion theory up to the point of certain
fixed-point theorems. This in turn requires standard results such as the
existence of a universal function and the $s$-$m$-$n$ theorem. Besides these,
the chapter contains some results, mostly regarding decidability and the
Kleene normal form, that are not strictly needed later. They are included as
relatively low-hanging fruits to round off the chapter.

The formalization of partial recursive functions is very much inspired by the
Universal Turing Machine AFP entry by Xu
et~al.~\<^cite>‹"Universal_Turing_Machine-AFP"›. It models partial recursive
functions as algorithms whose semantics is given by an evaluation function.
This works well for most of this chapter. For the next chapter, however, it
is beneficial to regard partial recursive functions as proper'' partial
functions. To that end, Section~\ref{s:alternative} introduces more
conventional and convenient notation for the common special cases of unary
and binary partial recursive functions.

Especially for the nontrivial proofs I consulted the classical textbook by
Rogers~\<^cite>‹"Rogers87"›, which also partially explains my preferring the
traditional term recursive'' to the more modern computable''.›

section ‹Basic definitions›

subsection ‹Partial recursive functions›

text ‹To represent partial recursive functions we start from the same
datatype as Xu et~al.~\<^cite>‹"Universal_Turing_Machine-AFP"›, more specifically
from Urban's version of the formalization. In fact the datatype @{text recf}
and the function @{text arity} below have been copied verbatim from it.›

datatype recf =
Z
| S
| Id nat nat
| Cn nat recf "recf list"
| Pr nat recf recf
| Mn nat recf

fun arity :: "recf ⇒ nat" where
"arity Z = 1"
| "arity S = 1"
| "arity (Id m n) = m"
| "arity (Cn n f gs) = n"
| "arity (Pr n f g) = Suc n"
| "arity (Mn n f) = n"

text ‹Already we deviate from Xu et~al.\ in that we define a
well-formedness predicate for partial recursive functions. Well-formedness
essentially means arity constraints are respected when combining @{typ
recf}s.›

fun wellf :: "recf ⇒ bool" where
"wellf Z = True"
| "wellf S = True"
| "wellf (Id m n) = (n < m)"
| "wellf (Cn n f gs) =
(n > 0 ∧ (∀g ∈ set gs. arity g = n ∧ wellf g) ∧ arity f = length gs ∧ wellf f)"
| "wellf (Pr n f g) =
(arity g = Suc (Suc n) ∧ arity f = n ∧ wellf f ∧ wellf g)"
| "wellf (Mn n f) = (n > 0 ∧ arity f = Suc n ∧ wellf f)"

lemma wellf_arity_nonzero: "wellf f ⟹ arity f > 0"
by (induction f rule: arity.induct) simp_all

lemma wellf_Pr_arity_greater_1: "wellf (Pr n f g) ⟹ arity (Pr n f g) > 1"
using wellf_arity_nonzero by auto

text ‹For the most part of this chapter this is the meaning of $f$
is an $n$-ary partial recursive function'':›

abbreviation recfn :: "nat ⇒ recf ⇒ bool" where
"recfn n f ≡ wellf f ∧ arity f = n"

text ‹Some abbreviations for working with @{typ "nat option"}:›

abbreviation divergent :: "nat option ⇒ bool" ("_ ↑" [50] 50) where
"x ↑ ≡ x = None"

abbreviation convergent :: "nat option ⇒ bool" ("_ ↓" [50] 50) where
"x ↓ ≡ x ≠ None"

abbreviation convergent_eq :: "nat option ⇒ nat ⇒ bool" (infix "↓=" 50) where
"x ↓= y ≡ x = Some y"

abbreviation convergent_neq :: "nat option ⇒ nat ⇒ bool" (infix "↓≠" 50) where
"x ↓≠ y ≡ x ↓ ∧ x ≠ Some y"

text ‹In prose the terms halt'', terminate'', converge'', and
defined'' will be used interchangeably; likewise for not halt'',
diverge'', and undefined''. In names of lemmas, the abbreviations @{text
converg} and @{text diverg} will be used consistently.›

text ‹Our second major deviation from Xu
et~al.~\<^cite>‹"Universal_Turing_Machine-AFP"› is that we model the semantics of
a @{typ recf} by combining the value and the termination of a function into
one evaluation function with codomain @{typ "nat option"}, rather than
separating both aspects into an evaluation function with codomain @{typ nat}
and a termination predicate.

The value of a well-formed partial recursive function applied to a
correctly-sized list of arguments:›

fun eval_wellf :: "recf ⇒ nat list ⇒ nat option" where
"eval_wellf Z xs ↓= 0"
| "eval_wellf S xs ↓= Suc (xs ! 0)"
| "eval_wellf (Id m n) xs ↓= xs ! n"
| "eval_wellf (Cn n f gs) xs =
(if ∀g ∈ set gs. eval_wellf g xs ↓
then eval_wellf f (map (λg. the (eval_wellf g xs)) gs)
else None)"
| "eval_wellf (Pr n f g) [] = undefined"
| "eval_wellf (Pr n f g) (0 # xs) = eval_wellf f xs"
| "eval_wellf (Pr n f g) (Suc x # xs) =
Option.bind (eval_wellf (Pr n f g) (x # xs)) (λv. eval_wellf g (x # v # xs))"
| "eval_wellf (Mn n f) xs =
(let E = λz. eval_wellf f (z # xs)
in if ∃z. E z ↓= 0 ∧ (∀y<z. E y ↓)
then Some (LEAST z. E z ↓= 0 ∧ (∀y<z. E y ↓))
else None)"

text ‹We define a function value only if the @{typ recf} is well-formed
and its arity matches the number of arguments.›

definition eval :: "recf ⇒ nat list ⇒ nat option" where
"recfn (length xs) f ⟹ eval f xs ≡ eval_wellf f xs"

lemma eval_Z [simp]: "eval Z [x] ↓= 0"

lemma eval_Z' [simp]: "length xs = 1 ⟹ eval Z xs ↓= 0"

lemma eval_S [simp]: "eval S [x] ↓= Suc x"

lemma eval_S' [simp]: "length xs = 1 ⟹ eval S xs ↓= Suc (hd xs)"
using eval_def hd_conv_nth[of xs] by fastforce

lemma eval_Id [simp]:
assumes "n < m" and "m = length xs"
shows "eval (Id m n) xs ↓= xs ! n"
using assms by (simp add: eval_def)

lemma eval_Cn [simp]:
assumes "recfn (length xs) (Cn n f gs)"
shows "eval (Cn n f gs) xs =
(if ∀g∈set gs. eval g xs ↓
then eval f (map (λg. the (eval g xs)) gs)
else None)"
proof -
have "eval (Cn n f gs) xs = eval_wellf (Cn n f gs) xs"
using assms eval_def by blast
moreover have "⋀g. g ∈ set gs ⟹ eval_wellf g xs = eval g xs"
using assms eval_def by simp
ultimately have "eval (Cn n f gs) xs =
(if ∀g∈set gs. eval g xs ↓
then eval_wellf f (map (λg. the (eval g xs)) gs)
else None)"
using map_eq_conv[of "λg. the (eval_wellf g xs)" gs "λg. the (eval g xs)"]
by (auto, metis)
moreover have "⋀ys. length ys = length gs ⟹ eval f ys = eval_wellf f ys"
using assms eval_def by simp
ultimately show ?thesis by auto
qed

lemma eval_Pr_0 [simp]:
assumes "recfn (Suc n) (Pr n f g)" and "n = length xs"
shows "eval (Pr n f g) (0 # xs) = eval f xs"
using assms by (simp add: eval_def)

lemma eval_Pr_diverg_Suc [simp]:
assumes "recfn (Suc n) (Pr n f g)"
and "n = length xs"
and "eval (Pr n f g) (x # xs) ↑"
shows "eval (Pr n f g) (Suc x # xs) ↑"
using assms by (simp add: eval_def)

lemma eval_Pr_converg_Suc [simp]:
assumes "recfn (Suc n) (Pr n f g)"
and "n = length xs"
and "eval (Pr n f g) (x # xs) ↓"
shows "eval (Pr n f g) (Suc x # xs) = eval g (x # the (eval (Pr n f g) (x # xs)) # xs)"
using assms eval_def by auto

assumes "recfn (Suc n) (Pr n f g)"
and "n = length xs"
and "eval (Pr n f g) (x # xs) ↑"
shows "eval (Pr n f g) ((x + y) # xs) ↑"
using assms by (induction y) auto

lemma eval_Pr_converg_le:
assumes "recfn (Suc n) (Pr n f g)"
and "n = length xs"
and "eval (Pr n f g) (x # xs) ↓"
and "y ≤ x"
shows "eval (Pr n f g) (y # xs) ↓"
using assms eval_Pr_diverg_add le_Suc_ex by metis

lemma eval_Pr_Suc_converg:
assumes "recfn (Suc n) (Pr n f g)"
and "n = length xs"
and "eval (Pr n f g) (Suc x # xs) ↓"
shows "eval g (x # (the (eval (Pr n f g) (x # xs))) # xs) ↓"
and "eval (Pr n f g) (Suc x # xs) = eval g (x # the (eval (Pr n f g) (x # xs)) # xs)"
using eval_Pr_converg_Suc[of n f g xs x, OF assms(1,2)]
eval_Pr_converg_le[of n f g xs "Suc x" x, OF assms] assms(3)
by simp_all

lemma eval_Mn [simp]:
assumes "recfn (length xs) (Mn n f)"
shows "eval (Mn n f) xs =
(if (∃z. eval f (z # xs) ↓= 0 ∧ (∀y<z. eval f (y # xs) ↓))
then Some (LEAST z. eval f (z # xs) ↓= 0 ∧ (∀y<z. eval f (y # xs) ↓))
else None)"
using assms eval_def by auto

text ‹For $\mu$-recursion, the condition @{term "(∀y<z. eval_wellf f (y # xs) ↓)"}
inside @{text LEAST} in the definition of @{term eval_wellf} is redundant.›

lemma eval_wellf_Mn:
"eval_wellf (Mn n f) xs =
(if (∃z. eval_wellf f (z # xs) ↓= 0 ∧ (∀y<z. eval_wellf f (y # xs) ↓))
then Some (LEAST z. eval_wellf f (z # xs) ↓= 0)
else None)"
proof -
let ?P = "λz. eval_wellf f (z # xs) ↓= 0 ∧ (∀y<z. eval_wellf f (y # xs) ↓)"
{
assume "∃z. ?P z"
moreover define z where "z = Least ?P"
ultimately have "?P z"
using LeastI[of ?P] by blast
have "(LEAST z. eval_wellf f (z # xs) ↓= 0) = z"
proof (rule Least_equality)
show "eval_wellf f (z # xs) ↓= 0"
using ‹?P z› by simp
show "z ≤ y" if "eval_wellf f (y # xs) ↓= 0" for y
proof (rule ccontr)
assume "¬ z ≤ y"
then have "y < z" by simp
moreover from this have "?P y"
using that ‹?P z› by simp
ultimately show False
using that not_less_Least z_def by blast
qed
qed
}
then show ?thesis by simp
qed

lemma eval_Mn':
assumes "recfn (length xs) (Mn n f)"
shows "eval (Mn n f) xs =
(if (∃z. eval f (z # xs) ↓= 0 ∧ (∀y<z. eval f (y # xs) ↓))
then Some (LEAST z. eval f (z # xs) ↓= 0)
else None)"
using assms eval_def eval_wellf_Mn by auto

text ‹Proving that $\mu$-recursion converges is easier if one does not
have to deal with @{text LEAST} directly.›

lemma eval_Mn_convergI:
assumes "recfn (length xs) (Mn n f)"
and "eval f (z # xs) ↓= 0"
and "⋀y. y < z ⟹ eval f (y # xs) ↓≠ 0"
shows "eval (Mn n f) xs ↓= z"
proof -
let ?P = "λz. eval f (z # xs) ↓= 0 ∧ (∀y<z. eval f (y # xs) ↓)"
have "z = Least ?P"
using Least_equality[of ?P z] assms(2,3) not_le_imp_less by blast
moreover have "?P z" using assms(2,3) by simp
ultimately show "eval (Mn n f) xs ↓= z"
using eval_Mn[OF assms(1)] by meson
qed

text ‹Similarly, reasoning from a $\mu$-recursive function is
simplified somewhat by the next lemma.›

lemma eval_Mn_convergE:
assumes "recfn (length xs) (Mn n f)" and "eval (Mn n f) xs ↓= z"
shows "z = (LEAST z. eval f (z # xs) ↓= 0 ∧ (∀y<z. eval f (y # xs) ↓))"
and "eval f (z # xs) ↓= 0"
and "⋀y. y < z ⟹ eval f (y # xs) ↓≠ 0"
proof -
let ?P = "λz. eval f (z # xs) ↓= 0 ∧ (∀y<z. eval f (y # xs) ↓)"
show "z = Least ?P"
using assms eval_Mn[OF assms(1)]
by (metis (no_types, lifting) option.inject option.simps(3))
moreover have "∃z. ?P z"
using assms eval_Mn[OF assms(1)] by (metis option.distinct(1))
ultimately have "?P z"
using LeastI[of ?P] by blast
then have "eval f (z # xs) ↓= 0 ∧ (∀y<z. eval f (y # xs) ↓)"
by simp
then show "eval f (z # xs) ↓= 0" by simp
show "⋀y. y < z ⟹ eval f (y # xs) ↓≠ 0"
using not_less_Least[of _ ?P] ‹z = Least ?P› ‹?P z› less_trans by blast
qed

lemma eval_Mn_diverg:
assumes "recfn (length xs) (Mn n f)"
shows "¬ (∃z. eval f (z # xs) ↓= 0 ∧ (∀y<z. eval f (y # xs) ↓)) ⟷ eval (Mn n f) xs ↑"
using assms eval_Mn[OF assms(1)] by simp

subsection ‹Extensional equality›

definition exteq :: "recf ⇒ recf ⇒ bool" (infix "≃" 55) where
"f ≃ g ≡ arity f = arity g ∧ (∀xs. length xs = arity f ⟶ eval f xs = eval g xs)"

lemma exteq_refl: "f ≃ f"
using exteq_def by simp

lemma exteq_sym: "f ≃ g ⟹ g ≃ f"
using exteq_def by simp

lemma exteq_trans: "f ≃ g ⟹ g ≃ h ⟹ f ≃ h"
using exteq_def by simp

lemma exteqI:
assumes "arity f = arity g" and "⋀xs. length xs = arity f ⟹ eval f xs = eval g xs"
shows "f ≃ g"
using assms exteq_def by simp

lemma exteqI1:
assumes "arity f = 1" and "arity g = 1" and "⋀x. eval f [x] = eval g [x]"
shows "f ≃ g"
using assms exteqI by (metis One_nat_def Suc_length_conv length_0_conv)

text ‹For every partial recursive function @{term f} there are
infinitely many extensionally equal ones, for example, those that wrap @{term
f} arbitrarily often in the identity function.›

fun wrap_Id :: "recf ⇒ nat ⇒ recf" where
"wrap_Id f 0 = f"
| "wrap_Id f (Suc n) = Cn (arity f) (Id 1 0) [wrap_Id f n]"

lemma recfn_wrap_Id: "recfn a f ⟹ recfn a (wrap_Id f n)"
using wellf_arity_nonzero by (induction n) auto

lemma exteq_wrap_Id: "recfn a f ⟹ f ≃ wrap_Id f n"
proof (induction n)
case 0
then show ?case by (simp add: exteq_refl)
next
case (Suc n)
have "wrap_Id f n ≃ wrap_Id f (Suc n) "
proof (rule exteqI)
show "arity (wrap_Id f n) = arity (wrap_Id f (Suc n))"
using Suc by (simp add: recfn_wrap_Id)
show "eval (wrap_Id f n) xs = eval (wrap_Id f (Suc n)) xs"
if "length xs = arity (wrap_Id f n)" for xs
proof -
have "recfn (length xs) (Cn (arity f) (Id 1 0) [wrap_Id f n])"
using that Suc recfn_wrap_Id by (metis wrap_Id.simps(2))
then show "eval (wrap_Id f n) xs = eval (wrap_Id f (Suc n)) xs"
by auto
qed
qed
then show ?case using Suc exteq_trans by fast
qed

fun depth :: "recf ⇒ nat" where
"depth Z = 0"
| "depth S = 0"
| "depth (Id m n) = 0"
| "depth (Cn n f gs) = Suc (max (depth f) (Max (set (map depth gs))))"
| "depth (Pr n f g) = Suc (max (depth f) (depth g))"
| "depth (Mn n f) = Suc (depth f)"

lemma depth_wrap_Id: "recfn a f ⟹ depth (wrap_Id f n) = depth f + n"
by (induction n) simp_all

lemma wrap_Id_injective:
assumes "recfn a f" and "wrap_Id f n⇩1 = wrap_Id f n⇩2"
shows "n⇩1 = n⇩2"
using assms by (metis add_left_cancel depth_wrap_Id)

lemma exteq_infinite:
assumes "recfn a f"
shows "infinite {g. recfn a g ∧ g ≃ f}" (is "infinite ?R")
proof -
have "inj (wrap_Id f)"
using wrap_Id_injective ‹recfn a f› by (meson inj_onI)
then have "infinite (range (wrap_Id f))"
using finite_imageD by blast
moreover have "range (wrap_Id f) ⊆ ?R"
using assms exteq_sym exteq_wrap_Id recfn_wrap_Id by blast
ultimately show ?thesis by (simp add: infinite_super)
qed

subsection ‹Primitive recursive and total functions›

fun Mn_free :: "recf ⇒ bool" where
"Mn_free Z = True"
| "Mn_free S = True"
| "Mn_free (Id m n) = True"
| "Mn_free (Cn n f gs) = ((∀g ∈ set gs. Mn_free g) ∧ Mn_free f)"
| "Mn_free (Pr n f g) = (Mn_free f ∧ Mn_free g)"
| "Mn_free (Mn n f) = False"

text ‹This is our notion of $n$-ary primitive recursive function:›

abbreviation prim_recfn :: "nat ⇒ recf ⇒ bool" where
"prim_recfn n f ≡ recfn n f ∧ Mn_free f"

definition total :: "recf ⇒ bool" where
"total f ≡ ∀xs. length xs = arity f ⟶ eval f xs ↓"

lemma totalI [intro]:
assumes "⋀xs. length xs = arity f ⟹ eval f xs ↓"
shows "total f"
using assms total_def by simp

lemma totalE [simp]:
assumes "total f" and "recfn n f" and "length xs = n"
shows "eval f xs ↓"
using assms total_def by simp

lemma totalI1 :
assumes "recfn 1 f" and "⋀x. eval f [x] ↓"
shows "total f"
using assms totalI[of f] by (metis One_nat_def length_0_conv length_Suc_conv)

lemma totalI2:
assumes "recfn 2 f" and "⋀x y. eval f [x, y] ↓"
shows "total f"
using assms totalI[of f] by (smt length_0_conv length_Suc_conv numeral_2_eq_2)

lemma totalI3:
assumes "recfn 3 f" and "⋀x y z. eval f [x, y, z] ↓"
shows "total f"
using assms totalI[of f] by (smt length_0_conv length_Suc_conv numeral_3_eq_3)

lemma totalI4:
assumes "recfn 4 f" and "⋀w x y z. eval f [w, x, y, z] ↓"
shows "total f"
proof (rule totalI[of f])
fix xs :: "nat list"
assume "length xs = arity f"
then have "length xs = Suc (Suc (Suc (Suc 0)))"
using assms(1) by simp
then obtain w x y z where "xs = [w, x, y, z]"
by (smt Suc_length_conv length_0_conv)
then show "eval f xs ↓" using assms(2) by simp
qed

lemma Mn_free_imp_total [intro]:
assumes "wellf f" and "Mn_free f"
shows "total f"
using assms
proof (induction f rule: Mn_free.induct)
case (5 n f g)
have "eval (Pr n f g) (x # xs) ↓" if "length (x # xs) = arity (Pr n f g)" for x xs
using 5 that by (induction x) auto
then show ?case by (metis arity.simps(5) length_Suc_conv totalI)
qed (auto simp add: total_def eval_def)

lemma prim_recfn_total: "prim_recfn n f ⟹ total f"
using Mn_free_imp_total by simp

lemma eval_Pr_prim_Suc:
assumes "h = Pr n f g" and "prim_recfn (Suc n) h" and "length xs = n"
shows "eval h (Suc x # xs) = eval g (x # the (eval h (x # xs)) # xs)"
using assms eval_Pr_converg_Suc prim_recfn_total by simp

lemma Cn_total:
assumes "∀g∈set gs. total g" and "total f" and "recfn n (Cn n f gs)"
shows "total (Cn n f gs)"
using assms by (simp add: totalI)

lemma Pr_total:
assumes "total f" and "total g" and "recfn (Suc n) (Pr n f g)"
shows "total (Pr n f g)"
proof -
have "eval (Pr n f g) (x # xs) ↓" if "length xs = n" for x xs
using that assms by (induction x) auto
then show ?thesis
using assms(3) totalI by (metis Suc_length_conv arity.simps(5))
qed

lemma eval_Mn_total:
assumes "recfn (length xs) (Mn n f)" and "total f"
shows "eval (Mn n f) xs =
(if (∃z. eval f (z # xs) ↓= 0)
then Some (LEAST z. eval f (z # xs) ↓= 0)
else None)"
using assms by auto

section ‹Simple functions›

text ‹This section, too, bears some similarity to Urban's formalization
in Xu et~al.~\<^cite>‹"Universal_Turing_Machine-AFP"›, but is more minimalistic in
scope.

As a general naming rule, instances of @{typ recf} and functions
returning such instances get names starting with @{text r_}. Typically, for
an @{text r_xyz} there will be a lemma @{text r_xyz_recfn} or @{text
r_xyz_prim} establishing its (primitive) recursiveness, arity, and
well-formedness. Moreover there will be a lemma @{text r_xyz} describing its
semantics, for which we will sometimes introduce an Isabelle function @{text
xyz}.›

subsection ‹Manipulating parameters›

text ‹Appending dummy parameters:›

definition r_dummy :: "nat ⇒ recf ⇒ recf" where
"r_dummy n f ≡ Cn (arity f + n) f (map (λi. Id (arity f + n) i) [0..<arity f])"

lemma r_dummy_prim [simp]:
"prim_recfn a f ⟹ prim_recfn (a + n) (r_dummy n f)"
using wellf_arity_nonzero by (auto simp add: r_dummy_def)

lemma r_dummy_recfn [simp]:
"recfn a f ⟹ recfn (a + n) (r_dummy n f)"
using wellf_arity_nonzero by (auto simp add: r_dummy_def)

lemma r_dummy [simp]:
"r_dummy n f = Cn (arity f + n) f (map (λi. Id (arity f + n) i) [0..<arity f])"
unfolding r_dummy_def by simp

lemma r_dummy_append:
assumes "recfn (length xs) f" and "length ys = n"
shows "eval (r_dummy n f) (xs @ ys) = eval f xs"
proof -
let ?r = "r_dummy n f"
let ?gs = "map (λi. Id (arity f + n) i) [0..<arity f]"
have "length ?gs = arity f" by simp
moreover have "?gs ! i = (Id (arity f + n) i)" if "i < arity f" for i
moreover have *: "eval_wellf (?gs ! i) (xs @ ys) ↓= xs ! i" if "i < arity f" for i
using that assms by (simp add: nth_append)
ultimately have "map (λg. the (eval_wellf g (xs @ ys))) ?gs = xs"
by (metis (no_types, lifting) assms(1) length_map nth_equalityI nth_map option.sel)
moreover have "∀g ∈ set ?gs. eval_wellf g (xs @ ys) ↓"
using * by simp
moreover have "recfn (length (xs @ ys)) ?r"
using assms r_dummy_recfn by fastforce
ultimately show ?thesis
by (auto simp add: assms eval_def)
qed

text ‹Shrinking a binary function to a unary one is useful when we want
to define a unary function via the @{term Pr} operation, which can only
construct @{typ recf}s of arity two or higher.›

definition r_shrink :: "recf ⇒ recf" where
"r_shrink f ≡ Cn 1 f [Id 1 0, Id 1 0]"

lemma r_shrink_prim [simp]: "prim_recfn 2 f ⟹ prim_recfn 1 (r_shrink f)"

lemma r_shrink_recfn [simp]: "recfn 2 f ⟹ recfn 1 (r_shrink f)"

lemma r_shrink [simp]: "recfn 2 f ⟹ eval (r_shrink f) [x] = eval f [x, x]"

definition r_swap :: "recf ⇒ recf" where
"r_swap f ≡ Cn 2 f [Id 2 1, Id 2 0]"

lemma r_swap_recfn [simp]: "recfn 2 f ⟹ recfn 2 (r_swap f)"

lemma r_swap_prim [simp]: "prim_recfn 2 f ⟹ prim_recfn 2 (r_swap f)"

lemma r_swap [simp]: "recfn 2 f ⟹ eval (r_swap f) [x, y] = eval f [y, x]"

text ‹Prepending one dummy parameter:›

definition r_shift :: "recf ⇒ recf" where
"r_shift f ≡ Cn (Suc (arity f)) f (map (λi. Id (Suc (arity f)) (Suc i)) [0..<arity f])"

lemma r_shift_prim [simp]: "prim_recfn a f ⟹ prim_recfn (Suc a) (r_shift f)"

lemma r_shift_recfn [simp]: "recfn a f ⟹ recfn (Suc a) (r_shift f)"

lemma r_shift [simp]:
assumes "recfn (length xs) f"
shows "eval (r_shift f) (x # xs) = eval f xs"
proof -
let ?r = "r_shift f"
let ?gs = "map (λi. Id (Suc (arity f)) (Suc i)) [0..<arity f]"
have "length ?gs = arity f" by simp
moreover have "?gs ! i = (Id (Suc (arity f)) (Suc i))" if "i < arity f" for i
moreover have *: "eval (?gs ! i) (x # xs) ↓= xs ! i" if "i < arity f" for i
using assms nth_append that by simp
ultimately have "map (λg. the (eval g (x # xs))) ?gs = xs"
by (metis (no_types, lifting) assms length_map nth_equalityI nth_map option.sel)
moreover have "∀g ∈ set ?gs. eval g (x # xs) ≠ None"
using * by simp
ultimately show ?thesis using r_shift_def assms by simp
qed

subsection ‹Arithmetic and logic›

text ‹The unary constants:›

fun r_const :: "nat ⇒ recf" where
"r_const 0 = Z"
| "r_const (Suc c) = Cn 1 S [r_const c]"

lemma r_const_prim [simp]: "prim_recfn 1 (r_const c)"
by (induction c) (simp_all)

lemma r_const [simp]: "eval (r_const c) [x] ↓= c"
by (induction c) simp_all

text ‹Constants of higher arities:›

definition "r_constn n c ≡ if n = 0 then r_const c else r_dummy n (r_const c)"

lemma r_constn_prim [simp]: "prim_recfn (Suc n) (r_constn n c)"
unfolding r_constn_def by simp

lemma r_constn [simp]: "length xs = Suc n ⟹ eval (r_constn n c) xs ↓= c"
unfolding r_constn_def
by simp (metis length_0_conv length_Suc_conv r_const)

text ‹We introduce addition, subtraction, and multiplication, but
interestingly enough we can make do without division.›

definition "r_add ≡ Pr 1 (Id 1 0) (Cn 3 S [Id 3 1])"

unfolding r_add_def by (induction a) simp_all

definition "r_mul ≡ Pr 1 Z (Cn 3 r_add [Id 3 1, Id 3 2])"

lemma r_mul_prim [simp]: "prim_recfn 2 r_mul"
unfolding r_mul_def by simp

lemma r_mul [simp]: "eval r_mul [a, b] ↓= a * b"
unfolding r_mul_def by (induction a) simp_all

definition "r_dec ≡ Cn 1 (Pr 1 Z (Id 3 0)) [Id 1 0, Id 1 0]"

lemma r_dec_prim [simp]: "prim_recfn 1 r_dec"

lemma r_dec [simp]: "eval r_dec [a] ↓= a - 1"
proof -
have "eval (Pr 1 Z (Id 3 0)) [x, y] ↓= x - 1" for x y
by (induction x) simp_all
then show ?thesis by (simp add: r_dec_def)
qed

definition "r_sub ≡ r_swap (Pr 1 (Id 1 0) (Cn 3 r_dec [Id 3 1]))"

lemma r_sub_prim [simp]: "prim_recfn 2 r_sub"
unfolding r_sub_def by simp

lemma r_sub [simp]: "eval r_sub [a, b] ↓= a - b"
proof -
have "eval (Pr 1 (Id 1 0) (Cn 3 r_dec [Id 3 1])) [x, y] ↓= y - x" for x y
by (induction x) simp_all
then show ?thesis unfolding r_sub_def by simp
qed

definition "r_sign ≡ r_shrink (Pr 1 Z (r_constn 2 1))"

lemma r_sign_prim [simp]: "prim_recfn 1 r_sign"
unfolding r_sign_def by simp

lemma r_sign [simp]: "eval r_sign [x] ↓= (if x = 0 then 0 else 1)"
proof -
have "eval (Pr 1 Z (r_constn 2 1)) [x, y] ↓= (if x = 0 then 0 else 1)" for x y
by (induction x) simp_all
then show ?thesis unfolding r_sign_def by simp
qed

text ‹In the logical functions, true will be represented by zero, and
false will be represented by non-zero as argument and by one as
result.›

definition "r_not ≡ Cn 1 r_sub [r_const 1, r_sign]"

lemma r_not_prim [simp]: "prim_recfn 1 r_not"
unfolding r_not_def by simp

lemma r_not [simp]: "eval r_not [x] ↓= (if x = 0 then 1 else 0)"
unfolding r_not_def by simp

definition "r_nand ≡ Cn 2 r_not [r_add]"

lemma r_nand_prim [simp]: "prim_recfn 2 r_nand"
unfolding r_nand_def by simp

lemma r_nand [simp]: "eval r_nand [x, y] ↓= (if x = 0 ∧ y = 0 then 1 else 0)"
unfolding r_nand_def by simp

definition "r_and ≡ Cn 2 r_not [r_nand]"

lemma r_and_prim [simp]: "prim_recfn 2 r_and"
unfolding r_and_def by simp

lemma r_and [simp]: "eval r_and [x, y] ↓= (if x = 0 ∧ y = 0 then 0 else 1)"
unfolding r_and_def by simp

definition "r_or ≡ Cn 2 r_sign [r_mul]"

lemma r_or_prim [simp]: "prim_recfn 2 r_or"
unfolding r_or_def by simp

lemma r_or [simp]: "eval r_or [x, y] ↓= (if x = 0 ∨ y = 0 then 0 else 1)"
unfolding r_or_def by simp

subsection ‹Comparison and conditions›

definition "r_ifz ≡
let ifzero = (Cn 3 r_mul [r_dummy 2 r_not, Id 3 1]);
ifnzero = (Cn 3 r_mul [r_dummy 2 r_sign, Id 3 2])
in Cn 3 r_add [ifzero, ifnzero]"

lemma r_ifz_prim [simp]: "prim_recfn 3 r_ifz"
unfolding r_ifz_def by simp

lemma r_ifz [simp]: "eval r_ifz [cond, val0, val1] ↓= (if cond = 0 then val0 else val1)"
unfolding r_ifz_def by (simp add: Let_def)

definition "r_eq ≡ Cn 2 r_sign [Cn 2 r_add [r_sub, r_swap r_sub]]"

lemma r_eq_prim [simp]: "prim_recfn 2 r_eq"
unfolding r_eq_def by simp

lemma r_eq [simp]: "eval r_eq [x, y] ↓= (if x = y then 0 else 1)"
unfolding r_eq_def by simp

definition "r_ifeq ≡ Cn 4 r_ifz [r_dummy 2 r_eq, Id 4 2, Id 4 3]"

lemma r_ifeq_prim [simp]: "prim_recfn 4 r_ifeq"
unfolding r_ifeq_def by simp

lemma r_ifeq [simp]: "eval r_ifeq [a, b, v⇩0, v⇩1] ↓= (if a = b then v⇩0 else v⇩1)"
unfolding r_ifeq_def using r_dummy_append[of r_eq "[a, b]" "[v⇩0, v⇩1]" 2]
by simp

definition "r_neq ≡ Cn 2 r_not [r_eq]"

lemma r_neq_prim [simp]: "prim_recfn 2 r_neq"
unfolding r_neq_def by simp

lemma r_neq [simp]: "eval r_neq [x, y] ↓= (if x = y then 1 else 0)"
unfolding r_neq_def by simp

definition "r_ifle ≡ Cn 4 r_ifz [r_dummy 2 r_sub, Id 4 2, Id 4 3]"

lemma r_ifle_prim [simp]: "prim_recfn 4 r_ifle"
unfolding r_ifle_def by simp

lemma r_ifle [simp]: "eval r_ifle [a, b, v⇩0, v⇩1] ↓= (if a ≤ b then v⇩0 else v⇩1)"
unfolding r_ifle_def using r_dummy_append[of r_sub "[a, b]" "[v⇩0, v⇩1]" 2]
by simp

definition "r_ifless ≡ Cn 4 r_ifle [Id 4 1, Id 4 0, Id 4 3, Id 4 2]"

lemma r_ifless_prim [simp]: "prim_recfn 4 r_ifless"
unfolding r_ifless_def by simp

lemma r_ifless [simp]: "eval r_ifless [a, b, v⇩0, v⇩1] ↓= (if a < b then v⇩0 else v⇩1)"
unfolding r_ifless_def by simp

definition "r_less ≡ Cn 2 r_ifle [Id 2 1, Id 2 0, r_constn 1 1, r_constn 1 0]"

lemma r_less_prim [simp]: "prim_recfn 2 r_less"
unfolding r_less_def by simp

lemma r_less [simp]: "eval r_less [x, y] ↓= (if x < y then 0 else 1)"
unfolding r_less_def by simp

definition "r_le ≡ Cn 2 r_ifle [Id 2 0, Id 2 1, r_constn 1 0, r_constn 1 1]"

lemma r_le_prim [simp]: "prim_recfn 2 r_le"
unfolding r_le_def by simp

lemma r_le [simp]: "eval r_le [x, y] ↓= (if x ≤ y then 0 else 1)"
unfolding r_le_def by simp

text ‹Arguments are evaluated eagerly. Therefore @{term "r_ifz"}, etc.
cannot be combined with a diverging function to implement a conditionally
diverging function in the naive way. The following function implements a
special case needed in the next section. A \hyperlink{p:r_lifz}{general lazy
version} of @{term "r_ifz"} will be introduced later with the help of a
universal function.›

definition "r_ifeq_else_diverg ≡
Cn 3 r_add [Id 3 2, Mn 3 (Cn 4 r_add [Id 4 0, Cn 4 r_eq [Id 4 1, Id 4 2]])]"

lemma r_ifeq_else_diverg_recfn [simp]: "recfn 3 r_ifeq_else_diverg"
unfolding r_ifeq_else_diverg_def by simp

lemma r_ifeq_else_diverg [simp]:
"eval r_ifeq_else_diverg [a, b, v] = (if a = b then Some v else None)"
unfolding r_ifeq_else_diverg_def by simp

section ‹The halting problem\label{s:halting}›

text ‹Decidability will be treated more thoroughly in
Section~\ref{s:decidable}. But the halting problem is prominent enough to
deserve an early mention.›

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

text ‹No matter how partial recursive functions are encoded as natural
numbers, the set of all codes of functions halting on their own code is
undecidable.›

theorem halting_problem_undecidable:
fixes code :: "nat ⇒ recf"
assumes "⋀f. recfn 1 f ⟹ ∃i. code i = f"
shows "¬ decidable {x. eval (code 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
with assms obtain i where i: "code i = g" 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 (code 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

section ‹Encoding tuples and lists›

text ‹This section is based on the Cantor encoding for pairs. Tuples
are encoded by repeated application of the pairing function, lists by pairing
their length with the code for a tuple. Thus tuples have a fixed length that
must be known when decoding, whereas lists are dynamically sized and know
their current length.›

subsection ‹Pairs and tuples›

subsubsection ‹The Cantor pairing function›

definition "r_triangle ≡ r_shrink (Pr 1 Z (r_dummy 1 (Cn 2 S [r_add])))"

lemma r_triangle_prim: "prim_recfn 1 r_triangle"
unfolding r_triangle_def by simp

lemma r_triangle: "eval r_triangle [n] ↓= Sum {0..n}"
proof -
let ?r = "r_dummy 1 (Cn 2 S [r_add])"
have "eval ?r [x, y, z] ↓= Suc (x + y)" for x y z
using r_dummy_append[of "Cn 2 S [r_add]" "[x, y]" "[z]" 1] by simp
then have "eval (Pr 1 Z ?r) [x, y] ↓= Sum {0..x}" for x y
by (induction x) simp_all
then show ?thesis unfolding r_triangle_def by simp
qed

lemma r_triangle_eq_triangle [simp]: "eval r_triangle [n] ↓= triangle n"
using r_triangle gauss_sum_nat triangle_def by simp

definition "r_prod_encode ≡ Cn 2 r_add [Cn 2 r_triangle [r_add], Id 2 0]"

lemma r_prod_encode_prim [simp]: "prim_recfn 2 r_prod_encode"
unfolding r_prod_encode_def using r_triangle_prim by simp

lemma r_prod_encode [simp]: "eval r_prod_encode [m, n] ↓= prod_encode (m, n)"
unfolding r_prod_encode_def prod_encode_def using r_triangle_prim by simp

text ‹These abbreviations are just two more things borrowed from
Xu~et~al.~\<^cite>‹"Universal_Turing_Machine-AFP"›.›

abbreviation "pdec1 z ≡ fst (prod_decode z)"

abbreviation "pdec2 z ≡ snd (prod_decode z)"

lemma pdec1_le: "pdec1 i ≤ i"
by (metis le_prod_encode_1 prod.collapse prod_decode_inverse)

lemma pdec2_le: "pdec2 i ≤ i"
by (metis le_prod_encode_2 prod.collapse prod_decode_inverse)

lemma pdec_less: "pdec2 i < Suc i"
using pdec2_le by (simp add: le_imp_less_Suc)

lemma pdec1_zero: "pdec1 0 = 0"
using pdec1_le by auto

definition "r_maxletr ≡
Pr 1 Z (Cn 3 r_ifle [r_dummy 2 (Cn 1 r_triangle [S]), Id 3 2, Cn 3 S [Id 3 0], Id 3 1])"

lemma r_maxletr_prim: "prim_recfn 2 r_maxletr"
unfolding r_maxletr_def using r_triangle_prim by simp

lemma not_Suc_Greatest_not_Suc:
assumes "¬ P (Suc x)" and "∃x. P x"
shows "(GREATEST y. y ≤ x ∧ P y) = (GREATEST y. y ≤ Suc x ∧ P y)"
using assms by (metis le_SucI le_Suc_eq)

lemma r_maxletr: "eval r_maxletr [x⇩0, x⇩1] ↓= (GREATEST y. y ≤ x⇩0 ∧ triangle y ≤ x⇩1)"
proof -
let ?g = "Cn 3 r_ifle [r_dummy 2 (Cn 1 r_triangle [S]), Id 3 2, Cn 3 S [Id 3 0], Id 3 1]"
have greatest:
"(if triangle (Suc x⇩0) ≤ x⇩1 then Suc x⇩0 else (GREATEST y. y ≤ x⇩0 ∧ triangle y ≤ x⇩1)) =
(GREATEST y. y ≤ Suc x⇩0 ∧ triangle y ≤ x⇩1)"
for x⇩0 x⇩1
proof (cases "triangle (Suc x⇩0) ≤ x⇩1")
case True
then show ?thesis
using Greatest_equality[of "λy. y ≤ Suc x⇩0 ∧ triangle y ≤ x⇩1"] by fastforce
next
case False
then show ?thesis
using not_Suc_Greatest_not_Suc[of "λy. triangle y ≤ x⇩1" x⇩0] by fastforce
qed
show ?thesis
unfolding r_maxletr_def using r_triangle_prim
proof (induction x⇩0)
case 0
then show ?case
using Greatest_equality[of "λy. y ≤ 0 ∧ triangle y ≤ x⇩1" 0] by simp
next
case (Suc x⇩0)
then show ?case using greatest by simp
qed
qed

definition "r_maxlt ≡ r_shrink r_maxletr"

lemma r_maxlt_prim: "prim_recfn 1 r_maxlt"
unfolding r_maxlt_def using r_maxletr_prim by simp

lemma r_maxlt: "eval r_maxlt [e] ↓= (GREATEST y. triangle y ≤ e)"
proof -
have "y ≤ triangle y" for y
by (induction y) auto
then have "triangle y ≤ e ⟹ y ≤ e" for y e
using order_trans by blast
then have "(GREATEST y. y ≤ e ∧ triangle y ≤ e) = (GREATEST y. triangle y ≤ e)"
by metis
moreover have "eval r_maxlt [e] ↓= (GREATEST y. y ≤ e ∧ triangle y ≤ e)"
using r_maxletr r_shrink r_maxlt_def r_maxletr_prim by fastforce
ultimately show ?thesis by simp
qed

definition "pdec1' e ≡ e - triangle (GREATEST y. triangle y ≤ e)"

definition "pdec2' e ≡ (GREATEST y. triangle y ≤ e) - pdec1' e"

lemma max_triangle_bound: "triangle z ≤ e ⟹ z ≤ e"
by (metis Suc_pred add_leD2 less_Suc_eq triangle_Suc zero_le zero_less_Suc)

lemma triangle_greatest_le: "triangle (GREATEST y. triangle y ≤ e) ≤ e"
using max_triangle_bound GreatestI_nat[of "λy. triangle y ≤ e" 0 e] by simp

lemma prod_encode_pdec': "prod_encode (pdec1' e, pdec2' e) = e"
proof -
let ?P = "λy. triangle y ≤ e"
let ?y = "GREATEST y. ?P y"
have "pdec1' e ≤ ?y"
proof (rule ccontr)
assume "¬ pdec1' e ≤ ?y"
then have "e - triangle ?y > ?y"
using pdec1'_def by simp
then have "?P (Suc ?y)" by simp
moreover have "∀z. ?P z ⟶ z ≤ e"
using max_triangle_bound by simp
ultimately have "Suc ?y ≤ ?y"
using Greatest_le_nat[of ?P "Suc ?y" e] by blast
then show False by simp
qed
then have "pdec1' e + pdec2' e = ?y"
using pdec1'_def pdec2'_def by simp
then have "prod_encode (pdec1' e, pdec2' e) = triangle ?y + pdec1' e"
then show ?thesis using pdec1'_def triangle_greatest_le by simp
qed

lemma pdec':
"pdec1' e = pdec1 e"
"pdec2' e = pdec2 e"
using prod_encode_pdec' prod_encode_inverse by (metis fst_conv, metis snd_conv)

definition "r_pdec1 ≡ Cn 1 r_sub [Id 1 0, Cn 1 r_triangle [r_maxlt]]"

lemma r_pdec1_prim [simp]: "prim_recfn 1 r_pdec1"
unfolding r_pdec1_def using r_triangle_prim r_maxlt_prim by simp

lemma r_pdec1 [simp]: "eval r_pdec1 [e] ↓= pdec1 e"
unfolding r_pdec1_def using r_triangle_prim r_maxlt_prim pdec' pdec1'_def

definition "r_pdec2 ≡ Cn 1 r_sub [r_maxlt, r_pdec1]"

lemma r_pdec2_prim [simp]: "prim_recfn 1 r_pdec2"
unfolding r_pdec2_def using r_maxlt_prim by simp

lemma r_pdec2 [simp]: "eval r_pdec2 [e] ↓= pdec2 e"
unfolding r_pdec2_def using r_maxlt_prim r_maxlt pdec' pdec2'_def by simp

abbreviation "pdec12 i ≡ pdec1 (pdec2 i)"
abbreviation "pdec22 i ≡ pdec2 (pdec2 i)"
abbreviation "pdec122 i ≡ pdec1 (pdec22 i)"
abbreviation "pdec222 i ≡ pdec2 (pdec22 i)"

definition "r_pdec12 ≡ Cn 1 r_pdec1 [r_pdec2]"

lemma r_pdec12_prim [simp]: "prim_recfn 1 r_pdec12"
unfolding r_pdec12_def by simp

lemma r_pdec12 [simp]: "eval r_pdec12 [e] ↓= pdec12 e"
unfolding r_pdec12_def by simp

definition "r_pdec22 ≡ Cn 1 r_pdec2 [r_pdec2]"

lemma r_pdec22_prim [simp]: "prim_recfn 1 r_pdec22"
unfolding r_pdec22_def by simp

lemma r_pdec22 [simp]: "eval r_pdec22 [e] ↓= pdec22 e"
unfolding r_pdec22_def by simp

definition "r_pdec122 ≡ Cn 1 r_pdec1 [r_pdec22]"

lemma r_pdec122_prim [simp]: "prim_recfn 1 r_pdec122"
unfolding r_pdec122_def by simp

lemma r_pdec122 [simp]: "eval r_pdec122 [e] ↓= pdec122 e"
unfolding r_pdec122_def by simp

definition "r_pdec222 ≡ Cn 1 r_pdec2 [r_pdec22]"

lemma r_pdec222_prim [simp]: "prim_recfn 1 r_pdec222"
unfolding r_pdec222_def by simp

lemma r_pdec222 [simp]: "eval r_pdec222 [e] ↓= pdec222 e"
unfolding r_pdec222_def by simp

subsubsection ‹The Cantor tuple function›

text ‹The empty tuple gets no code, whereas singletons are encoded by their
only element and other tuples by recursively applying the pairing function.
This yields, for every $n$, the function @{term "tuple_encode n"}, which is a
bijection between the natural numbers and the lists of length $(n + 1)$.›

fun tuple_encode :: "nat ⇒ nat list ⇒ nat" where
"tuple_encode n [] = undefined"
| "tuple_encode 0 (x # xs) = x"
| "tuple_encode (Suc n) (x # xs) = prod_encode (x, tuple_encode n xs)"

lemma tuple_encode_prod_encode: "tuple_encode 1 [x, y] = prod_encode (x, y)"
by simp

fun tuple_decode where
"tuple_decode 0 i = [i]"
| "tuple_decode (Suc n) i = pdec1 i # tuple_decode n (pdec2 i)"

lemma tuple_encode_decode [simp]:
"tuple_encode (length xs - 1) (tuple_decode (length xs - 1) i) = i"
proof (induction "length xs - 1" arbitrary: xs i)
case 0
then show ?case by simp
next
case (Suc n)
then have "length xs - 1 > 0" by simp
with Suc have *: "tuple_encode n (tuple_decode n j) = j" for j
by (metis diff_Suc_1 length_tl)
from Suc have "tuple_decode (Suc n) i = pdec1 i # tuple_decode n (pdec2 i)"
using tuple_decode.simps(2) by blast
then have "tuple_encode (Suc n) (tuple_decode (Suc n) i) =
tuple_encode (Suc n) (pdec1 i # tuple_decode n (pdec2 i))"
using Suc by simp
also have "... = prod_encode (pdec1 i, tuple_encode n (tuple_decode n (pdec2 i)))"
by simp
also have "... = prod_encode (pdec1 i, pdec2 i)"
using Suc * by simp
also have "... = i" by simp
finally have "tuple_encode (Suc n) (tuple_decode (Suc n) i) = i" .
then show ?case by (simp add: Suc.hyps(2))
qed

lemma tuple_encode_decode' [simp]: "tuple_encode n (tuple_decode n i) = i"
using tuple_encode_decode by (metis Ex_list_of_length diff_Suc_1 length_Cons)

lemma tuple_decode_encode:
assumes "length xs > 0"
shows "tuple_decode (length xs - 1) (tuple_encode (length xs - 1) xs) = xs"
using assms
proof (induction "length xs - 1" arbitrary: xs)
case 0
moreover from this have "length xs = 1" by linarith
ultimately show ?case
by (metis One_nat_def length_0_conv length_Suc_conv tuple_decode.simps(1)
tuple_encode.simps(2))
next
case (Suc n)
let ?t = "tl xs"
let ?i = "tuple_encode (Suc n) xs"
have "length ?t > 0" and "length ?t - 1 = n"
using Suc by simp_all
then have "tuple_decode n (tuple_encode n ?t) = ?t"
using Suc by blast
moreover have "?i = prod_encode (hd xs, tuple_encode n ?t)"
using Suc by (metis hd_Cons_tl length_greater_0_conv tuple_encode.simps(3))
moreover have "tuple_decode (Suc n) ?i = pdec1 ?i # tuple_decode n (pdec2 ?i)"
using tuple_decode.simps(2) by blast
ultimately have "tuple_decode (Suc n) ?i = xs"
using Suc.prems by simp
then show ?case by (simp add: Suc.hyps(2))
qed

lemma tuple_decode_encode' [simp]:
assumes "length xs = Suc n"
shows "tuple_decode n (tuple_encode n xs) = xs"
using assms tuple_decode_encode by (metis diff_Suc_1 zero_less_Suc)

lemma tuple_decode_length [simp]: "length (tuple_decode n i) = Suc n"
by (induction n arbitrary: i) simp_all

lemma tuple_decode_nonzero:
assumes "n > 0"
shows "tuple_decode n i = pdec1 i # tuple_decode (n - 1) (pdec2 i)"
using assms by (metis One_nat_def Suc_pred tuple_decode.simps(2))

text ‹The tuple encoding functions are primitive recursive.›

fun r_tuple_encode :: "nat ⇒ recf" where
"r_tuple_encode 0 = Id 1 0"
| "r_tuple_encode (Suc n) =
Cn (Suc (Suc n)) r_prod_encode [Id (Suc (Suc n)) 0, r_shift (r_tuple_encode n)]"

lemma r_tuple_encode_prim [simp]: "prim_recfn (Suc n) (r_tuple_encode n)"
by (induction n) simp_all

lemma r_tuple_encode:
assumes "length xs = Suc n"
shows "eval (r_tuple_encode n) xs ↓= tuple_encode n xs"
using assms
proof (induction n arbitrary: xs)
case 0
then show ?case
by (metis One_nat_def eval_Id length_Suc_conv nth_Cons_0
r_tuple_encode.simps(1) tuple_encode.simps(2) zero_less_one)
next
case (Suc n)
then obtain y ys where y_ys: "y # ys = xs"
by (metis length_Suc_conv)
with Suc have "eval (r_tuple_encode n) ys ↓= tuple_encode n ys"
by auto
with y_ys have "eval (r_shift (r_tuple_encode n)) xs ↓= tuple_encode n ys"
using Suc.prems r_shift_prim r_tuple_encode_prim by auto
moreover have "eval (Id (Suc (Suc n)) 0) xs ↓= y"
using y_ys Suc.prems by auto
ultimately have "eval (r_tuple_encode (Suc n)) xs ↓= prod_encode (y, tuple_encode n ys)"
using Suc.prems by simp
then show ?case using y_ys by auto
qed

subsubsection ‹Functions on encoded tuples›

text ‹The function for accessing the $n$-th element of a tuple returns
$0$ for out-of-bounds access.›

definition e_tuple_nth :: "nat ⇒ nat ⇒ nat ⇒ nat" where
"e_tuple_nth a i n ≡ if n ≤ a then (tuple_decode a i) ! n else 0"

lemma e_tuple_nth_le [simp]: "n ≤ a ⟹ e_tuple_nth a i n = (tuple_decode a i) ! n"
using e_tuple_nth_def by simp

lemma e_tuple_nth_gr [simp]: "n > a ⟹ e_tuple_nth a i n = 0"
using e_tuple_nth_def by simp

lemma tuple_decode_pdec2: "tuple_decode a (pdec2 es) = tl (tuple_decode (Suc a) es)"
by simp

fun iterate :: "nat ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a)" where
"iterate 0 f = id"
| "iterate (Suc n) f = f ∘ (iterate n f)"

assumes "iterate t⇩1 f x = y" and "iterate t⇩2 f y = z"
shows "iterate (t⇩1 + t⇩2) f x = z"
using assms by (induction t⇩2 arbitrary: z) auto

lemma iterate_additive': "iterate (t⇩1 + t⇩2) f x = iterate t⇩2 f (iterate t⇩1 f x)"

lemma e_tuple_nth_elementary:
assumes "k ≤ a"
shows "e_tuple_nth a i k = (if a = k then (iterate k pdec2 i) else (pdec1 (iterate k pdec2 i)))"
proof -
have *: "tuple_decode (a - k) (iterate k pdec2 i) = drop k (tuple_decode a i)"
using assms
by (induction k) (simp, simp add: Suc_diff_Suc tuple_decode_pdec2 drop_Suc tl_drop)
show ?thesis
proof (cases "a = k")
case True
then have "tuple_decode 0 (iterate k pdec2 i) = drop k (tuple_decode a i)"
using assms * by simp
moreover from this have "drop k (tuple_decode a i) = [tuple_decode a i ! k]"
using assms True by (metis nth_via_drop tuple_decode.simps(1))
ultimately show ?thesis using True by simp
next
case False
with assms have "a - k > 0" by simp
with * have "tuple_decode (a - k) (iterate k pdec2 i) = drop k (tuple_decode a i)"
by simp
then have "pdec1 (iterate k pdec2 i) = hd (drop k (tuple_decode a i))"
using tuple_decode_nonzero ‹a - k > 0› by (metis list.sel(1))
with ‹a - k > 0› have "pdec1 (iterate k pdec2 i) = (tuple_decode a i) ! k"
with False assms show ?thesis by simp
qed
qed

definition "r_nth_inbounds ≡
let r = Pr 1 (Id 1 0) (Cn 3 r_pdec2 [Id 3 1])
in Cn 3 r_ifeq
[Id 3 0,
Id 3 2,
Cn 3 r [Id 3 2, Id 3 1],
Cn 3 r_pdec1 [Cn 3 r [Id 3 2, Id 3 1]]]"

lemma r_nth_inbounds_prim: "prim_recfn 3 r_nth_inbounds"
unfolding r_nth_inbounds_def by (simp add: Let_def)

lemma r_nth_inbounds:
"k ≤ a ⟹ eval r_nth_inbounds [a, i, k] ↓= e_tuple_nth a i k"
"eval r_nth_inbounds [a, i, k] ↓"
proof -
let ?r = "Pr 1 (Id 1 0) (Cn 3 r_pdec2 [Id 3 1])"
let ?h = "Cn 3 ?r [Id 3 2, Id 3 1]"
have "eval ?r [k, i] ↓= iterate k pdec2 i" for k i
using r_pdec2_prim by (induction k) (simp_all)
then have "eval ?h [a, i, k] ↓= iterate k pdec2 i"
using r_pdec2_prim by simp
then have "eval r_nth_inbounds [a, i, k] ↓=
(if a = k then iterate k pdec2 i else pdec1 (iterate k pdec2 i))"
unfolding r_nth_inbounds_def by (simp add: Let_def)
then show "k ≤ a ⟹ eval r_nth_inbounds [a, i, k] ↓= e_tuple_nth a i k"
and "eval r_nth_inbounds [a, i, k] ↓"
using e_tuple_nth_elementary by simp_all
qed

definition "r_tuple_nth ≡
Cn 3 r_ifle [Id 3 2, Id 3 0, r_nth_inbounds, r_constn 2 0]"

lemma r_tuple_nth_prim: "prim_recfn 3 r_tuple_nth"
unfolding r_tuple_nth_def using r_nth_inbounds_prim by simp

lemma r_tuple_nth [simp]: "eval r_tuple_nth [a, i, k] ↓= e_tuple_nth a i k"
unfolding r_tuple_nth_def using r_nth_inbounds_prim r_nth_inbounds by simp

subsection ‹Lists›

subsubsection ‹Encoding and decoding›

text ‹Lists are encoded by pairing the length of the list with the code
for the tuple made up of the list's elements. Then all these codes are
incremented in order to make room for the empty list
(cf.~Rogers~\<^cite>‹‹p.~71› in "Rogers87"›).›

fun list_encode :: "nat list ⇒ nat" where
"list_encode [] = 0"
| "list_encode (x # xs) = Suc (prod_encode (length xs, tuple_encode (length xs) (x # xs)))"

lemma list_encode_0 [simp]: "list_encode xs = 0 ⟷ xs = []"
using list_encode.elims Partial_Recursive.list_encode.simps(1) by blast

lemma list_encode_1: "list_encode [0] = 1"

fun list_decode :: "nat ⇒ nat list" where
"list_decode 0 = []"
| "list_decode (Suc n) = tuple_decode (pdec1 n) (pdec2 n)"

lemma list_encode_decode [simp]: "list_encode (list_decode n) = n"
proof (cases n)
case 0
then show ?thesis by simp
next
case (Suc k)
then have *: "list_decode n = tuple_decode (pdec1 k) (pdec2 k)" (is "_ = ?t")
by simp
then obtain x xs where xxs: "x # xs = ?t"
by (metis tuple_decode.elims)
then have "list_encode ?t = list_encode (x # xs)" by simp
then have 1: "list_encode ?t = Suc (prod_encode (length xs, tuple_encode (length xs) (x # xs)))"
by simp
have 2: "length xs = length ?t - 1"
using xxs by (metis length_tl list.sel(3))
then have 3: "length xs = pdec1 k"
using * by simp
then have "tuple_encode (length ?t - 1) ?t = pdec2 k"
using 2 tuple_encode_decode by metis
then have "list_encode ?t = Suc (prod_encode (pdec1 k, pdec2 k))"
using 1 2 3 xxs by simp
with * Suc show ?thesis by simp
qed

lemma list_decode_encode [simp]: "list_decode (list_encode xs) = xs"
proof (cases xs)
case Nil
then show ?thesis by simp
next
case (Cons y ys)
then have "list_encode xs =
Suc (prod_encode (length ys, tuple_encode (length ys) xs))"
(is "_ = Suc ?i")
by simp
then have "list_decode (Suc ?i) = tuple_decode (pdec1 ?i) (pdec2 ?i)" by simp
moreover have "pdec1 ?i = length ys" by simp
moreover have "pdec2 ?i = tuple_encode (length ys) xs" by simp
ultimately have "list_decode (Suc ?i) =
tuple_decode (length ys) (tuple_encode (length ys) xs)"
by simp
moreover have "length ys = length xs - 1"
using Cons by simp
ultimately have "list_decode (Suc ?i) =
tuple_decode (length xs - 1) (tuple_encode (length xs - 1) xs)"
by simp
then show ?thesis using Cons by simp
qed

abbreviation singleton_encode :: "nat ⇒ nat" where
"singleton_encode x ≡ list_encode [x]"

lemma list_decode_singleton: "list_decode (singleton_encode x) = [x]"
by simp

definition "r_singleton_encode ≡ Cn 1 S [Cn 1 r_prod_encode [Z, Id 1 0]]"

lemma r_singleton_encode_prim [simp]: "prim_recfn 1 r_singleton_encode"
unfolding r_singleton_encode_def by simp

lemma r_singleton_encode [simp]: "eval r_singleton_encode [x] ↓= singleton_encode x"
unfolding r_singleton_encode_def by simp

definition r_list_encode :: "nat ⇒ recf" where
"r_list_encode n ≡ Cn (Suc n) S [Cn (Suc n) r_prod_encode [r_constn n n, r_tuple_encode n]]"

lemma r_list_encode_prim [simp]: "prim_recfn (Suc n) (r_list_encode n)"
unfolding r_list_encode_def by simp

lemma r_list_encode:
assumes "length xs = Suc n"
shows "eval (r_list_encode n) xs ↓= list_encode xs"
proof -
have "eval (r_tuple_encode n) xs ↓"
then have "eval (Cn (Suc n) r_prod_encode [r_constn n n, r_tuple_encode n]) xs ↓"
using assms by simp
then have "eval (r_list_encode n) xs =
eval S [the (eval (Cn (Suc n) r_prod_encode [r_constn n n, r_tuple_encode n]) xs)]"
unfolding r_list_encode_def using assms r_tuple_encode by simp
moreover from assms obtain y ys where "xs = y # ys"
by (meson length_Suc_conv)
ultimately show ?thesis
unfolding r_list_encode_def using assms r_tuple_encode by simp
qed

subsubsection ‹Functions on encoded lists›

text ‹The functions in this section mimic those on type @{typ "nat
list"}. Their names are prefixed by @{text e_} and the names of the
corresponding @{typ recf}s by @{text r_}.›

abbreviation e_tl :: "nat ⇒ nat" where
"e_tl e ≡ list_encode (tl (list_decode e))"

text ‹In order to turn @{term e_tl} into a partial recursive function
we first represent it in a more elementary way.›

lemma e_tl_elementary:
"e_tl e =
(if e = 0 then 0
else if pdec1 (e - 1) = 0 then 0
else Suc (prod_encode (pdec1 (e - 1) - 1, pdec22 (e - 1))))"
proof (cases e)
case 0
then show ?thesis by simp
next
case Suc_d: (Suc d)
then show ?thesis
proof (cases "pdec1 d")
case 0
then show ?thesis using Suc_d by simp
next
case (Suc a)
have *: "list_decode e = tuple_decode (pdec1 d) (pdec2 d)"
using Suc_d by simp
with Suc obtain x xs where xxs: "list_decode e = x # xs" by simp
then have **: "e_tl e = list_encode xs" by simp
have "list_decode (Suc (prod_encode (pdec1 (e - 1) - 1, pdec22 (e - 1)))) =
tuple_decode (pdec1 (e - 1) - 1) (pdec22 (e - 1))"
(is "?lhs = _")
by simp
also have "... = tuple_decode a (pdec22 (e - 1))"
using Suc Suc_d by simp
also have "... = tl (tuple_decode (Suc a) (pdec2 (e - 1)))"
using tuple_decode_pdec2 Suc by presburger
also have "... = tl (tuple_decode (pdec1 (e - 1)) (pdec2 (e - 1)))"
using Suc Suc_d by auto
also have "... = tl (list_decode e)"
using * Suc_d by simp
also have "... = xs"
using xxs by simp
finally have "?lhs = xs" .
then have "list_encode ?lhs = list_encode xs" by simp
then have "Suc (prod_encode (pdec1 (e - 1) - 1, pdec22 (e - 1))) = list_encode xs"
using list_encode_decode by metis
then show ?thesis using ** Suc_d Suc by simp
qed
qed

definition "r_tl ≡
let r = Cn 1 r_pdec1 [r_dec]
in Cn 1 r_ifz
[Id 1 0,
Z,
Cn 1 r_ifz
[r, Z, Cn 1 S [Cn 1 r_prod_encode [Cn 1 r_dec [r], Cn 1 r_pdec22 [r_dec]]]]]"

lemma r_tl_prim [simp]: "prim_recfn 1 r_tl"
unfolding r_tl_def by (simp add: Let_def)

lemma r_tl [simp]: "eval r_tl [e] ↓= e_tl e"
unfolding r_tl_def using e_tl_elementary by (simp add: Let_def)

text ‹We define the head of the empty encoded list to be zero.›

definition e_hd :: "nat ⇒ nat" where
"e_hd