# 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) where
"x ↑ ≡ x = None"

abbreviation convergent :: "nat option ⇒ bool" ("_ ↓"  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]{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 by blast

lemma list_encode_1: "list_encode  = 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 e ≡ if e = 0 then 0 else hd (list_decode e)"

lemma e_hd [simp]:
assumes "list_decode e = x # xs"
shows "e_hd e = x"
using e_hd_def assms by auto

lemma e_hd_0 [simp]: "e_hd 0 = 0"
using e_hd_def by simp

lemma e_hd_neq_0 [simp]:
assumes "e ≠ 0"
shows "e_hd e = hd (list_decode e)"
using e_hd_def assms by simp

definition "r_hd ≡
Cn 1 r_ifz [Cn 1 r_pdec1 [r_dec], Cn 1 r_pdec2 [r_dec], Cn 1 r_pdec12 [r_dec]]"

lemma r_hd_prim [simp]: "prim_recfn 1 r_hd"
unfolding r_hd_def by simp

lemma r_hd [simp]: "eval r_hd [e] ↓= e_hd e"
proof -
have "e_hd e = (if pdec1 (e - 1) = 0 then pdec2 (e - 1) else pdec12 (e - 1))"
proof (cases e)
case 0
then show ?thesis using pdec1_zero pdec2_le by auto
next
case (Suc d)
then show ?thesis by (cases "pdec1 d") (simp_all add: pdec1_zero)
qed
then show ?thesis unfolding r_hd_def by simp
qed

abbreviation e_length :: "nat ⇒ nat" where
"e_length e ≡ length (list_decode e)"

lemma e_length_0: "e_length e = 0 ⟹ e = 0"
by (metis list_encode.simps(1) length_0_conv list_encode_decode)

definition "r_length ≡ Cn 1 r_ifz [Id 1 0, Z, Cn 1 S [Cn 1 r_pdec1 [r_dec]]]"

lemma r_length_prim [simp]: "prim_recfn 1 r_length"
unfolding r_length_def by simp

lemma r_length [simp]: "eval r_length [e] ↓= e_length e"
unfolding r_length_def by (cases e) simp_all

text ‹Accessing an encoded list out of bounds yields zero.›

definition e_nth :: "nat ⇒ nat ⇒ nat" where
"e_nth e n ≡ if e = 0 then 0 else e_tuple_nth (pdec1 (e - 1)) (pdec2 (e - 1)) n"

lemma e_nth [simp]:
"e_nth e n = (if n < e_length e then (list_decode e) ! n else 0)"
by (cases e) (simp_all add: e_nth_def e_tuple_nth_def)

lemma e_hd_nth0: "e_hd e = e_nth e 0"
by (simp add: e_hd_def e_length_0 hd_conv_nth)

definition "r_nth ≡
Cn 2 r_ifz
[Id 2 0,
r_constn 1 0,
Cn 2 r_tuple_nth
[Cn 2 r_pdec1 [r_dummy 1 r_dec], Cn 2 r_pdec2 [r_dummy 1 r_dec], Id 2 1]]"

lemma r_nth_prim [simp]: "prim_recfn 2 r_nth"
unfolding r_nth_def using r_tuple_nth_prim by simp

lemma r_nth [simp]: "eval r_nth [e, n] ↓= e_nth e n"
unfolding r_nth_def e_nth_def using r_tuple_nth_prim by simp

definition "r_rev_aux ≡
Pr 1 r_hd (Cn 3 r_prod_encode [Cn 3 r_nth [Id 3 2, Cn 3 S [Id 3 0]], Id 3 1])"

lemma r_rev_aux_prim: "prim_recfn 2 r_rev_aux"
unfolding r_rev_aux_def by simp

lemma r_rev_aux:
assumes "list_decode e = xs" and "length xs > 0" and "i < length xs"
shows "eval r_rev_aux [i, e] ↓= tuple_encode i (rev (take (Suc i) xs))"
using assms(3)
proof (induction i)
case 0
then show ?case
unfolding r_rev_aux_def using assms e_hd_def r_hd by (auto simp add: take_Suc)
next
case (Suc i)
let ?g = "Cn 3 r_prod_encode [Cn 3 r_nth [Id 3 2, Cn 3 S [Id 3 0]], Id 3 1]"
from Suc have "eval r_rev_aux [Suc i, e] = eval ?g [i, the (eval r_rev_aux [i, e]), e]"
unfolding r_rev_aux_def by simp
also have "... ↓= prod_encode (xs ! (Suc i), tuple_encode i (rev (take (Suc i) xs)))"
using Suc by (simp add: assms(1))
finally show ?case by (simp add: Suc.prems take_Suc_conv_app_nth)
qed

corollary r_rev_aux_full:
assumes "list_decode e = xs" and "length xs > 0"
shows "eval r_rev_aux [length xs - 1, e] ↓= tuple_encode (length xs - 1) (rev xs)"
using r_rev_aux assms by simp

lemma r_rev_aux_total: "eval r_rev_aux [i, e] ↓"
using r_rev_aux_prim totalE by fastforce

definition "r_rev ≡
Cn 1 r_ifz
[Id 1 0,
Z,
Cn 1 S
[Cn 1 r_prod_encode
[Cn 1 r_dec [r_length], Cn 1 r_rev_aux [Cn 1 r_dec [r_length], Id 1 0]]]]"

lemma r_rev_prim [simp]: "prim_recfn 1 r_rev"
unfolding r_rev_def using r_rev_aux_prim by simp

lemma r_rev [simp]: "eval r_rev [e] ↓= list_encode (rev (list_decode e))"
proof -
let ?d = "Cn 1 r_dec [r_length]"
let ?a = "Cn 1 r_rev_aux [?d, Id 1 0]"
let ?p = "Cn 1 r_prod_encode [?d, ?a]"
let ?s = "Cn 1 S [?p]"
have eval_a: "eval ?a [e] = eval r_rev_aux [e_length e - 1, e]"
using r_rev_aux_prim by simp
then have "eval ?s [e] ↓"
using r_rev_aux_prim by (simp add: r_rev_aux_total)
then have *: "eval r_rev [e] ↓= (if e = 0 then 0 else the (eval ?s [e]))"
using r_rev_aux_prim by (simp add: r_rev_def)
show ?thesis
proof (cases "e = 0")
case True
then show ?thesis using * by simp
next
case False
then obtain xs where xs: "xs = list_decode e" "length xs > 0"
using e_length_0 by auto
then have len: "length xs = e_length e" by simp
with eval_a have "eval ?a [e] = eval r_rev_aux [length xs - 1, e]"
by simp
then have "eval ?a [e] ↓= tuple_encode (length xs - 1) (rev xs)"
using xs r_rev_aux_full by simp
then have "eval ?s [e] ↓=
Suc (prod_encode (length xs - 1, tuple_encode (length xs - 1) (rev xs)))"
using len r_rev_aux_prim by simp
then have "eval ?s [e] ↓=
Suc (prod_encode
(length (rev xs) - 1, tuple_encode (length (rev xs) - 1) (rev xs)))"
by simp
moreover have "length (rev xs) > 0"
using xs by simp
ultimately have "eval ?s [e] ↓= list_encode (rev xs)"
by (metis list_encode.elims diff_Suc_1 length_Cons length_greater_0_conv)
then show ?thesis using xs * by simp
qed
qed

abbreviation e_cons :: "nat ⇒ nat ⇒ nat" where
"e_cons e es ≡ list_encode (e # list_decode es)"

lemma e_cons_elementary:
"e_cons e es =
(if es = 0 then Suc (prod_encode (0, e))
else Suc (prod_encode (e_length es, prod_encode (e, pdec2 (es - 1)))))"
proof (cases "es = 0")
case True
then show ?thesis by simp
next
case False
then have "e_length es = Suc (pdec1 (es - 1))"
by (metis list_decode.elims diff_Suc_1 tuple_decode_length)
moreover have "es = e_tl (list_encode (e # list_decode es))"
by (metis list.sel(3) list_decode_encode list_encode_decode)
ultimately show ?thesis
using False e_tl_elementary
by (metis list_decode.simps(2) diff_Suc_1 list_encode_decode prod.sel(1)
prod_encode_inverse snd_conv tuple_decode.simps(2))
qed

definition "r_cons_else ≡
Cn 2 S
[Cn 2 r_prod_encode
[Cn 2 r_length
[Id 2 1], Cn 2 r_prod_encode [Id 2 0, Cn 2 r_pdec2 [Cn 2 r_dec [Id 2 1]]]]]"

lemma r_cons_else_prim: "prim_recfn 2 r_cons_else"
unfolding r_cons_else_def by simp

lemma r_cons_else:
"eval r_cons_else [e, es] ↓=
Suc (prod_encode (e_length es, prod_encode (e, pdec2 (es - 1))))"
unfolding r_cons_else_def by simp

definition "r_cons ≡
Cn 2 r_ifz
[Id 2 1, Cn 2 S [Cn 2 r_prod_encode [r_constn 1 0, Id 2 0]], r_cons_else]"

lemma r_cons_prim [simp]: "prim_recfn 2 r_cons"
unfolding r_cons_def using r_cons_else_prim by simp

lemma r_cons [simp]: "eval r_cons [e, es] ↓= e_cons e es"
unfolding r_cons_def using r_cons_else_prim r_cons_else e_cons_elementary by simp

abbreviation e_snoc :: "nat ⇒ nat ⇒ nat" where
"e_snoc es e ≡ list_encode (list_decode es @ [e])"

lemma e_nth_snoc_small [simp]:
assumes "n < e_length b"
shows "e_nth (e_snoc b z) n = e_nth b n"
using assms by (simp add: nth_append)

lemma e_hd_snoc [simp]:
assumes "e_length b > 0"
shows "e_hd (e_snoc b x) = e_hd b"
proof -
from assms have "b ≠ 0"
using less_imp_neq by force
then have hd: "e_hd b = hd (list_decode b)" by simp
have "e_length (e_snoc b x) > 0" by simp
then have "e_snoc b x ≠ 0"
using not_gr_zero by fastforce
then have "e_hd (e_snoc b x) = hd (list_decode (e_snoc b x))" by simp
with assms hd show ?thesis by simp
qed

definition "r_snoc ≡ Cn 2 r_rev [Cn 2 r_cons [Id 2 1, Cn 2 r_rev [Id 2 0]]]"

lemma r_snoc_prim [simp]: "prim_recfn 2 r_snoc"
unfolding r_snoc_def by simp

lemma r_snoc [simp]: "eval r_snoc [es, e] ↓= e_snoc es e"
unfolding r_snoc_def by simp

abbreviation e_butlast :: "nat ⇒ nat" where
"e_butlast e ≡ list_encode (butlast (list_decode e))"

abbreviation e_take :: "nat ⇒ nat ⇒ nat" where
"e_take n x ≡ list_encode (take n (list_decode x))"

definition "r_take ≡
Cn 2 r_ifle
[Id 2 0, Cn 2 r_length [Id 2 1],
Pr 1 Z (Cn 3 r_snoc [Id 3 1, Cn 3 r_nth [Id 3 2, Id 3 0]]),
Id 2 1]"

lemma r_take_prim [simp]: "prim_recfn 2 r_take"
unfolding r_take_def by simp_all

lemma r_take:
assumes "x = list_encode es"
shows "eval r_take [n, x] ↓= list_encode (take n es)"
proof -
let ?g = "Cn 3 r_snoc [Id 3 1, Cn 3 r_nth [Id 3 2, Id 3 0]]"
let ?h = "Pr 1 Z ?g"
have "total ?h" using Mn_free_imp_total by simp
have "m ≤ length es ⟹ eval ?h [m, x] ↓= list_encode (take m es)" for m
proof (induction m)
case 0
then show ?case using assms r_take_def by (simp add: r_take_def)
next
case (Suc m)
then have "m < length es" by simp
then have "eval ?h [Suc m, x] = eval ?g [m, the (eval ?h [m, x]), x]"
using Suc r_take_def by simp
also have "... = eval ?g [m, list_encode (take m es), x]"
using Suc by simp
also have "... ↓= e_snoc (list_encode (take m es)) (es ! m)"
by (simp add: ‹m < length es› assms)
also have "... ↓= list_encode ((take m es) @ [es ! m])"
using list_decode_encode by simp
also have "... ↓= list_encode (take (Suc m) es)"
by (simp add: ‹m < length es› take_Suc_conv_app_nth)
finally show ?case .
qed
moreover have "eval (Id 2 1) [m, x] ↓= list_encode (take m es)" if "m > length es" for m
using that assms by simp
moreover have "eval r_take [m, x] ↓=
(if m ≤ e_length x then the (eval ?h [m, x]) else the (eval (Id 2 1) [m, x]))"
for m
unfolding r_take_def using ‹total ?h› by simp
ultimately show ?thesis unfolding r_take_def by fastforce
qed

corollary r_take' [simp]: "eval r_take [n, x] ↓= e_take n x"

definition "r_last ≡ Cn 1 r_hd [r_rev]"

lemma r_last_prim [simp]: "prim_recfn 1 r_last"
unfolding r_last_def by simp

lemma r_last [simp]:
assumes "e = list_encode xs" and "length xs > 0"
shows "eval r_last [e] ↓= last xs"
proof -
from assms(2) have "length (rev xs) > 0" by simp
then have "list_encode (rev xs) > 0"
by (metis gr0I list.size(3) list_encode_0)
moreover have "eval r_last [e] = eval r_hd [the (eval r_rev [e])]"
unfolding r_last_def by simp
ultimately show ?thesis using assms hd_rev by auto
qed

definition "r_update_aux ≡
let
f = r_constn 2 0;
g = Cn 5 r_snoc
[Id 5 1, Cn 5 r_ifeq [Id 5 0, Id 5 3, Id 5 4, Cn 5 r_nth [Id 5 2, Id 5 0]]]
in Pr 3 f g"

lemma r_update_aux_recfn: "recfn 4 r_update_aux"
unfolding r_update_aux_def by simp

lemma r_update_aux:
assumes "n ≤ e_length b"
shows "eval r_update_aux [n, b, j, v] ↓= list_encode ((take n (list_decode b))[j:=v])"
using assms
proof (induction n)
case 0
then show ?case unfolding r_update_aux_def by simp
next
case (Suc n)
then have n: "n < e_length b"
by simp
let ?a = "Cn 5 r_nth [Id 5 2, Id 5 0]"
let ?b = "Cn 5 r_ifeq [Id 5 0, Id 5 3, Id 5 4, ?a]"
define g where "g ≡ Cn 5 r_snoc [Id 5 1, ?b]"
then have g: "eval g [n, r, b, j, v] ↓= e_snoc r (if n = j then v else e_nth b n)" for r
by simp

have "Pr 3 (r_constn 2 0) g = r_update_aux"
using r_update_aux_def g_def by simp
then have "eval r_update_aux [Suc n, b, j, v] =
eval g [n, the (eval r_update_aux [n, b, j, v]), b, j, v]"
using r_update_aux_recfn Suc n eval_Pr_converg_Suc
by (metis arity.simps(5) length_Cons list.size(3) nat_less_le
numeral_3_eq_3 option.simps(3))
then have *: "eval r_update_aux [Suc n, b, j, v] ↓= e_snoc
(list_encode ((take n (list_decode b))[j:=v]))
(if n = j then v else e_nth b n)"
using g Suc by simp

consider (j_eq_n) "j = n" | (j_less_n) "j < n" | (j_gt_n) "j > n"
by linarith
then show ?case
proof (cases)
case j_eq_n
moreover from this have "(take (Suc n) (list_decode b))[j:=v] =
(take n (list_decode b))[j:=v] @ [v]"
using n
by (metis length_list_update nth_list_update_eq take_Suc_conv_app_nth take_update_swap)
ultimately show ?thesis using * by simp
next
case j_less_n
moreover from this have "(take (Suc n) (list_decode b))[j:=v] =
(take n (list_decode b))[j:=v] @ [(list_decode b) ! n]"
using n
by (simp add: le_eq_less_or_eq list_update_append min_absorb2 take_Suc_conv_app_nth)
ultimately show ?thesis using * by auto
next
case j_gt_n
moreover from this have "(take (Suc n) (list_decode b))[j:=v] =
(take n (list_decode b))[j:=v] @ [(list_decode b) ! n]"
using n take_Suc_conv_app_nth by auto
ultimately show ?thesis using * by auto
qed
qed

abbreviation e_update :: "nat ⇒ nat ⇒ nat ⇒ nat" where
"e_update b j v ≡ list_encode ((list_decode b)[j:=v])"

definition "r_update ≡
Cn 3 r_update_aux [Cn 3 r_length [Id 3 0], Id 3 0, Id 3 1, Id 3 2]"

lemma r_update_recfn [simp]: "recfn 3 r_update"
unfolding r_update_def using r_update_aux_recfn by simp

lemma r_update [simp]: "eval r_update [b, j, v] ↓= e_update b j v"
unfolding r_update_def using r_update_aux r_update_aux_recfn by simp

lemma e_length_update [simp]: "e_length (e_update b k v) = e_length b"
by simp

definition e_append :: "nat ⇒ nat ⇒ nat" where
"e_append xs ys ≡ list_encode (list_decode xs @ list_decode ys)"

lemma e_length_append: "e_length (e_append xs ys) = e_length xs + e_length ys"
using e_append_def by simp

lemma e_nth_append_small:
assumes "n < e_length xs"
shows "e_nth (e_append xs ys) n = e_nth xs n"
using e_append_def assms by (simp add: nth_append)

lemma e_nth_append_big:
assumes "n ≥ e_length xs"
shows "e_nth (e_append xs ys) n = e_nth ys (n - e_length xs)"
using e_append_def assms e_nth by (simp add: less_diff_conv2 nth_append)

definition "r_append ≡
let
f = Id 2 0;
g = Cn 4 r_snoc [Id 4 1, Cn 4 r_nth [Id 4 3, Id 4 0]]
in Cn 2 (Pr 2 f g) [Cn 2 r_length [Id 2 1], Id 2 0, Id 2 1]"

lemma r_append_prim [simp]: "prim_recfn 2 r_append"
unfolding r_append_def by simp

lemma r_append [simp]: "eval r_append [a, b] ↓= e_append a b"
proof -
define g where "g = Cn 4 r_snoc [Id 4 1, Cn 4 r_nth [Id 4 3, Id 4 0]]"
then have g: "eval g [j, r, a, b] ↓= e_snoc r (e_nth b j)" for j r
by simp
let ?h = "Pr 2 (Id 2 0) g"
have "eval ?h [n, a, b] ↓= list_encode (list_decode a @ (take n (list_decode b)))"
if "n ≤ e_length b" for n
using that g g_def by (induction n) (simp_all add: take_Suc_conv_app_nth)
then show ?thesis
unfolding r_append_def g_def e_append_def by simp
qed

definition e_append_zeros :: "nat ⇒ nat ⇒ nat" where
"e_append_zeros b z ≡ e_append b (list_encode (replicate z 0))"

lemma e_append_zeros_length: "e_length (e_append_zeros b z) = e_length b + z"
using e_append_def e_append_zeros_def by simp

lemma e_nth_append_zeros: "e_nth (e_append_zeros b z) i = e_nth b i"
using e_append_zeros_def e_nth_append_small e_nth_append_big by auto

lemma e_nth_append_zeros_big:
assumes "i ≥ e_length b"
shows "e_nth (e_append_zeros b z) i = 0"
unfolding e_append_zeros_def
using e_nth_append_big[of b i "list_encode (replicate z 0)", OF assms(1)]
by simp

definition "r_append_zeros ≡
r_swap (Pr 1 (Id 1 0) (Cn 3 r_snoc [Id 3 1, r_constn 2 0]))"

lemma r_append_zeros_prim [simp]: "prim_recfn 2 r_append_zeros"
unfolding r_append_zeros_def by simp

lemma r_append_zeros: "eval r_append_zeros [b, z] ↓= e_append_zeros b z"
proof -
let ?r = "Pr 1 (Id 1 0) (Cn 3 r_snoc [Id 3 1, r_constn 2 0])"
have "eval ?r [z, b] ↓= e_append_zeros b z"
using e_append_zeros_def e_append_def
by (induction z) (simp_all add: replicate_append_same)
then show ?thesis by (simp add: r_append_zeros_def)
qed

end

# Theory Universal

section ‹A universal partial recursive function›

theory Universal
imports Partial_Recursive
begin

text ‹The main product of this section is a universal partial recursive
function, which given a code $i$ of an $n$-ary partial recursive function $f$
and an encoded list @{term xs} of $n$ arguments, computes @{term "eval f
xs"}. From this we can derive fixed-arity universal functions satisfying the
usual results such as the $s$-$m$-$n$ theorem. To represent the code $i$, we
need a way to encode @{typ recf}s as natural numbers (Section~\ref{s:recf_enc}). To
construct the universal function, we devise a ternary function taking $i$,
$xs$, and a step bound $t$ and simulating the execution of $f$ on input $xs$ for
$t$ steps. This function is useful in its own right, enabling techniques like
dovetailing or concurrent'' evaluation of partial recursive functions.

The notion of a step'' is not part of the definition of (the evaluation of)
partial recursive functions, but one can simulate the evaluation on an
abstract machine (Section~\ref{s:step}). This machine's configurations can be
encoded as natural numbers, and this leads us to a step function @{typ "nat
⇒ nat"} on encoded configurations (Section~\ref{s:step_enc}).
This function in turn can be computed by a primitive recursive function, from
which we develop the aforementioned ternary function of $i$, @{term xs}, and
$t$ (Section~\ref{s:step_recf}). From this we can finally derive
a universal function (Section~\ref{s:the_universal}).›

subsection ‹A step function\label{s:step}›

text ‹We simulate the stepwise execution of a partial recursive
function in a fairly straightforward way reminiscent of the execution of
function calls in an imperative programming language. A configuration of the
abstract machine is a pair consisting of:
\begin{enumerate}
\item A stack of frames. A frame represents the execution of a function and is
a triple @{term "(f, xs, locals)"} of
\begin{enumerate}
\item a @{typ recf} @{term f} being executed,
\item a @{typ "nat list"} of arguments of @{term f},
\item a @{typ "nat list"} of local variables, which holds intermediate
values when @{term f} is of the form @{term Cn}, @{term Pr}, or @{term Mn}.
\end{enumerate}
\item A register of type @{typ "nat option"} representing the return value of
the last function call: @{term None} signals that in the previous step the
stack was not popped and hence no value was returned, whereas @{term "Some
v"} means that in the previous step a function returned @{term v}.
\end{enumerate}
For computing @{term h} on input @{term xs}, the initial configuration is
@{term "([(h, xs, [])], None)"}. When the computation for a frame ends, it is
popped off the stack, and its return value is put in the register. The entire
computation ends when the stack is empty. In such a final configuration the
register contains the value of @{term h} at @{term xs}. If no final
configuration is ever reached, @{term h} diverges at @{term xs}.

The execution of one step depends on the topmost (that is, active) frame. In
the step when a frame @{term "(h, xs, locals)"} is pushed onto the stack, the
local variables are @{term "locals = []"}. The following happens until the
frame is popped off the stack again (if it ever is):
\begin{itemize}
\item For the base functions @{term "h = Z"}, @{term "h = S"},
@{term[names_short] "h = Id m n"}, the frame is popped off the stack right away,
and the return value is placed in the register.
\item For @{term "h = Cn n f gs"}, for each function $g$ in @{term gs}:
\begin{enumerate}
\item A new frame of the form @{term "(g, xs, [])"} is pushed onto the stack.
\item When (and if) this frame
is eventually popped, the value in the register is @{term "eval g xs"}. This value
is appended to the list @{term locals} of local variables.
\end{enumerate}
When all $g$ in $gs$ have been evaluated in this manner, $f$ is evaluated on the local variables
by pushing @{term "(f, locals, [])"}. The resulting register value is kept
and the active frame for $h$ is popped off the stack.
\item For @{text "h = Pr n f g"}, let @{term "xs = y # ys"}. First @{term "(f,
ys, [])"} is pushed and the return value stored in the @{term
locals}. Then @{term "(g, x # v # ys, [])"} is pushed,
where $x$ is the length of @{term locals} and $v$ the most recently
appended value. The return value is appended to @{term locals}. This is
repeated until the length of @{term locals} reaches @{term y}. Then the most
recently appended local is placed in the register, and the stack is popped.
\item For @{text "h = Mn n f"}, frames @{term "(f, x # xs, [])"} are pushed
for $x = 0, 1, 2, \ldots$ until one of them returns $0$. Then this
$x$ is placed in the register and the stack is popped. Until then $x$ is
stored in @{term locals}. If none of these evaluations return $0$, the
stack never shrinks, and thus the machine never reaches a final state.
\end{itemize}›

type_synonym frame = "recf × nat list × nat list"

type_synonym configuration = "frame list × nat option"

subsubsection ‹Definition of the step function›

fun step :: "configuration ⇒ configuration" where
"step ([], rv) = ([], rv)"
| "step (((Z, _, _) # fs), rv) = (fs, Some 0)"
| "step (((S, xs, _) # fs), rv) = (fs, Some (Suc (hd xs)))"
| "step (((Id m n, xs, _) # fs), rv) = (fs, Some (xs ! n))"
| "step (((Cn n f gs, xs, ls) # fs), rv) =
(if length ls = length gs
then if rv = None
then ((f, ls, []) # (Cn n f gs, xs, ls) # fs, None)
else (fs, rv)
else if rv = None
then if length ls < length gs
then ((gs ! (length ls), xs, []) # (Cn n f gs, xs, ls) # fs, None)
else (fs, rv)   ―‹cannot occur, so don't-care term›
else ((Cn n f gs, xs, ls @ [the rv]) # fs, None))"
| "step (((Pr n f g, xs, ls) # fs), rv) =
(if ls = []
then if rv = None
then ((f, tl xs, []) # (Pr n f g, xs, ls) # fs, None)
else ((Pr n f g, xs, [the rv]) # fs, None)
else if length ls = Suc (hd xs)
then (fs, Some (hd ls))
else if rv = None
then ((g, (length ls - 1) # hd ls # tl xs, []) # (Pr n f g, xs, ls) # fs, None)
else ((Pr n f g, xs, (the rv) # ls) # fs, None))"
| "step (((Mn n f, xs, ls) # fs), rv) =
(if ls = []
then ((f, 0 # xs, []) # (Mn n f, xs, ) # fs, None)
else if rv = Some 0
then (fs, Some (hd ls))
else ((f, (Suc (hd ls)) # xs, []) # (Mn n f, xs, [Suc (hd ls)]) # fs, None))"

definition reachable :: "configuration ⇒ configuration ⇒ bool" where
"reachable x y ≡ ∃t. iterate t step x = y"

lemma step_reachable [intro]:
assumes "step x = y"
shows "reachable x y"
unfolding reachable_def using assms by (metis iterate.simps(1,2) comp_id)

lemma reachable_transitive [trans]:
assumes "reachable x y" and "reachable y z"
shows "reachable x z"
using assms iterate_additive[where ?f=step] reachable_def by metis

lemma reachable_refl: "reachable x x"
unfolding reachable_def by (metis iterate.simps(1) eq_id_iff)

text ‹From a final configuration, that is, when the stack is empty,
only final configurations are reachable.›

lemma step_empty_stack:
assumes "fst x = []"
shows "fst (step x) = []"
using assms by (metis prod.collapse step.simps(1))

lemma reachable_empty_stack:
assumes "fst x = []" and "reachable x y"
shows "fst y = []"
proof -
have "fst (iterate t step x) = []" for t
using assms step_empty_stack by (induction t) simp_all
then show ?thesis
using reachable_def assms(2) by auto
qed

abbreviation nonterminating :: "configuration ⇒ bool" where
"nonterminating x ≡ ∀t. fst (iterate t step x) ≠ []"

lemma reachable_nonterminating:
assumes "reachable x y" and "nonterminating y"
shows "nonterminating x"
proof -
from assms(1) obtain t⇩1 where t1: "iterate t⇩1 step x = y"
using reachable_def by auto
have "fst (iterate t step x) ≠ []" for t
proof (cases "t ≤ t⇩1")
case True
then show ?thesis
using t1 assms(2) reachable_def reachable_empty_stack iterate_additive'
by (metis le_Suc_ex)
next
case False
then have "iterate t step x = iterate (t⇩1 + (t - t⇩1)) step x"
by simp
then have "iterate t step x = iterate (t - t⇩1) step (iterate t⇩1 step x)"
then have "iterate t step x = iterate (t - t⇩1) step y"
using t1 by simp
then show "fst (iterate t step x) ≠ []"
using assms(2) by simp
qed
then show ?thesis ..
qed

text ‹The function @{term step} is underdefined, for example, when the
top frame contains a non-well-formed @{typ recf} or too few arguments. All is
well, though, if every frame contains a well-formed @{typ recf} whose arity
matches the number of arguments. Such stacks will be called
\emph{valid}.›

definition valid :: "frame list ⇒ bool" where
"valid stack ≡ ∀s∈set stack. recfn (length (fst (snd s))) (fst s)"

lemma valid_frame: "valid (s # ss) ⟹ valid ss ∧ recfn (length (fst (snd s))) (fst s)"
using valid_def by simp

lemma valid_ConsE: "valid ((f, xs, locs) # rest) ⟹ valid rest ∧ recfn (length xs) f"
using valid_def by simp

lemma valid_ConsI: "valid rest ⟹ recfn (length xs) f ⟹ valid ((f, xs, locs) # rest)"
using valid_def by simp

text ‹Stacks in initial configurations are valid, and performing a step
maintains the validity of the stack.›

lemma step_valid: "valid stack ⟹ valid (fst (step (stack, rv)))"
proof (cases stack)
case Nil
then show ?thesis using valid_def by simp
next
case (Cons s ss)
assume valid: "valid stack"
then have *: "valid ss ∧ recfn (length (fst (snd s))) (fst s)"
using valid_frame Cons by simp
show ?thesis
proof (cases "fst s")
case Z
then show ?thesis using Cons valid * by (metis fstI prod.collapse step.simps(2))
next
case S
then show ?thesis using Cons valid * by (metis fst_conv prod.collapse step.simps(3))
next
case Id
then show ?thesis using Cons valid * by (metis fstI prod.collapse step.simps(4))
next
case (Cn n f gs)
then obtain xs ls where "s = (Cn n f gs, xs, ls)"
using Cons by (metis prod.collapse)
moreover consider
"length ls = length gs ∧ rv ↑"
| "length ls = length gs ∧ rv ↓"
| "length ls < length gs ∧ rv ↑"
| "length ls ≠ length gs ∧ rv ↓"
| "length ls > length gs ∧ rv ↑"
by linarith
ultimately show ?thesis using valid Cons valid_def by (cases) auto
next
case (Pr n f g)
then obtain xs ls where s: "s = (Pr n f g, xs, ls)"
using Cons by (metis prod.collapse)
consider
"length ls = 0 ∧ rv ↑"
| "length ls = 0 ∧ rv ↓"
| "length ls ≠ 0 ∧ length ls = Suc (hd xs)"
| "length ls ≠ 0 ∧ length ls ≠ Suc (hd xs) ∧ rv ↑"
| "length ls ≠ 0 ∧ length ls ≠ Suc (hd xs) ∧ rv ↓"
by linarith
then show ?thesis using Cons * valid_def s by (cases) auto
next
case (Mn n f)
then obtain xs ls where s: "s = (Mn n f, xs, ls)"
using Cons by (metis prod.collapse)
consider
"length ls = 0"
| "length ls ≠ 0 ∧ rv ↑"
| "length ls ≠ 0 ∧ rv ↓"
by linarith
then show ?thesis using Cons * valid_def s by (cases) auto
qed
qed

corollary iterate_step_valid:
assumes "valid stack"
shows "valid (fst (iterate t step (stack, rv)))"
using assms
proof (induction t)
case 0
then show ?case by simp
next
case (Suc t)
moreover have "iterate (Suc t) step (stack, rv) = step (iterate t step (stack, rv))"
by simp
ultimately show ?case using step_valid valid_def by (metis prod.collapse)
qed

subsubsection ‹Correctness of the step function›

text ‹The function @{term step} works correctly for a @{typ recf} $f$
on arguments @{term xs} in some configuration if (1) in case $f$ converges, @{term
step} reaches a configuration with the topmost frame popped and @{term "eval
f xs"} in the register, and (2) in case $f$ diverges, @{term step} does not
reach a final configuration.›

fun correct :: "configuration ⇒ bool" where
"correct ([], r) = True"
| "correct ((f, xs, ls) # rest, r) =
(if eval f xs ↓ then reachable ((f, xs, ls) # rest, r) (rest, eval f xs)
else nonterminating ((f, xs, ls) # rest, None))"

lemma correct_convergI:
assumes "eval f xs ↓" and "reachable ((f, xs, ls) # rest, None) (rest, eval f xs)"
shows "correct ((f, xs, ls) # rest, None)"
using assms by auto

lemma correct_convergE:
assumes "correct ((f, xs, ls) # rest, None)" and "eval f xs ↓"
shows "reachable ((f, xs, ls) # rest, None) (rest, eval f xs)"
using assms by simp

text ‹The correctness proof for @{term step} is by structural induction
on the @{typ recf} in the top frame. The base cases @{term Z}, @{term S},
and @{term[names_short] Id} are simple. For @{text "X = Cn, Pr, Mn"}, the
lemmas named @{text reachable_X} show which configurations are reachable for
@{typ recf}s of shape @{text X}. Building on those, the lemmas named @{text
step_X_correct} show @{term step}'s correctness for @{text X}.›

lemma reachable_Cn:
assumes "valid (((Cn n f gs), xs, []) # rest)" (is "valid ?stack")
and "⋀xs rest. valid ((f, xs, []) # rest) ⟹ correct ((f, xs, []) # rest, None)"
and "⋀g xs rest.
g ∈ set gs ⟹ valid ((g, xs, []) # rest) ⟹ correct ((g, xs, []) # rest, None)"
and "∀i<k. eval (gs ! i) xs ↓"
and "k ≤ length gs"
shows "reachable
(?stack, None)
((Cn n f gs, xs, take k (map (λg. the (eval g xs)) gs)) # rest, None)"
using assms(4,5)
proof (induction k)
case 0
then show ?case using reachable_refl by simp
next
case (Suc k)
let ?ys = "map (λg. the (eval g xs)) gs"
from Suc have "k < length gs" by simp
have valid: "recfn (length xs) (Cn n f gs)" "valid rest"
using assms(1) valid_ConsE[of "(Cn n f gs)"] by simp_all
from Suc have "reachable (?stack, None) ((Cn n f gs, xs, take k ?ys) # rest, None)"
(is "_ (?stack1, None)")
by simp
also have "reachable ... ((gs ! k, xs, []) # ?stack1, None)"
using step_reachable ‹k < length gs›
by (auto simp: min_absorb2)
also have "reachable ... (?stack1, eval (gs ! k) xs)"
(is "_ (_, ?rv)")
using Suc.prems(1) ‹k < length gs› assms(3) valid valid_ConsI by auto
also have "reachable ... ((Cn n f gs, xs, (take (Suc k) ?ys)) # rest, None)"
(is "_ (?stack2, None)")
proof -
have "step (?stack1, ?rv) = ((Cn n f gs, xs, (take k ?ys) @ [the ?rv]) # rest, None)"
using Suc by auto
also have "... = ((Cn n f gs, xs, (take (Suc k) ?ys)) # rest, None)"
by (simp add: ‹k < length gs› take_Suc_conv_app_nth)
finally show ?thesis
using step_reachable by auto
qed
finally show "reachable (?stack, None) (?stack2, None)" .
qed

lemma step_Cn_correct:
assumes "valid (((Cn n f gs), xs, []) # rest)" (is "valid ?stack")
and "⋀xs rest. valid ((f, xs, []) # rest) ⟹ correct ((f, xs, []) # rest, None)"
and "⋀g xs rest.
g ∈ set gs ⟹ valid ((g, xs, []) # rest) ⟹ correct ((g, xs, []) # rest, None)"
shows "correct (?stack, None)"
proof -
have valid: "recfn (length xs) (Cn n f gs)" "valid rest"
using valid_ConsE[OF assms(1)] by auto
let ?ys = "map (λg. the (eval g xs)) gs"
consider
(diverg_f) "∀g∈set gs. eval g xs ↓" and "eval f ?ys ↑"
| (diverg_gs) "∃g∈set gs. eval g xs ↑"
| (converg) "eval (Cn n f gs) xs ↓"
using valid_ConsE[OF assms(1)] by fastforce
then show ?thesis
proof (cases)
case diverg_f
then have "∀i<length gs. eval (gs ! i) xs ↓" by simp
then have "reachable (?stack, None) ((Cn n f gs, xs, ?ys) # rest, None)"
(is "_ (?stack1, None)")
using reachable_Cn[OF assms, where ?k="length gs"] by simp
also have "reachable ... ((f, ?ys, []) # ?stack1, None)" (is "_ (?stack2, None)")
finally have "reachable (?stack, None) (?stack2, None)" .
moreover have "nonterminating (?stack2, None)"
using diverg_f(2) assms(2)[of ?ys ?stack1] valid_ConsE[OF assms(1)] valid_ConsI
by auto
ultimately have "nonterminating (?stack, None)"
using reachable_nonterminating by simp
moreover have "eval (Cn n f gs) xs ↑"
using diverg_f(2) assms(1) eval_Cn valid_ConsE by presburger
ultimately show ?thesis by simp
next
case diverg_gs
then have ex_i: "∃i<length gs. eval (gs ! i) xs ↑"
using in_set_conv_nth[of _ gs] by auto
define k where "k = (LEAST i. i < length gs ∧ eval (gs ! i) xs ↑)" (is "_ = Least ?P")
then have gs_k: "eval (gs ! k) xs ↑"
using LeastI_ex[OF ex_i] by simp
have "∀i<k. eval (gs ! i) xs ↓"
using k_def not_less_Least[of _ ?P] LeastI_ex[OF ex_i] by simp
moreover from this have "k < length gs"
using ex_i less_le_trans not_le by blast
ultimately have "reachable (?stack, None) ((Cn n f gs, xs, take k ?ys) # rest, None)"
using reachable_Cn[OF assms] by simp
also have "reachable ...
((gs ! (length (take k ?ys)), xs, []) # (Cn n f gs, xs, take k ?ys) # rest, None)"
(is "_ (?stack1, None)")
proof -
have "length (take k ?ys) < length gs"
by (simp add: ‹k < length gs› less_imp_le_nat min_less_iff_disj)
then show ?thesis using step_reachable by auto
qed
finally have "reachable (?stack, None) (?stack1, None)" .
moreover have "nonterminating (?stack1, None)"
proof -
have "recfn (length xs) (gs ! k)"
using ‹k < length gs› valid(1) by simp
then have "correct (?stack1, None)"
using ‹k < length gs› nth_mem valid valid_ConsI
assms(3)[of "gs ! (length (take k ?ys))" xs]
by auto
moreover have "length (take k ?ys) = k"
by (simp add: ‹k < length gs› less_imp_le_nat min_absorb2)
ultimately show ?thesis using gs_k by simp
qed
ultimately have "nonterminating (?stack, None)"
using reachable_nonterminating by simp
moreover have "eval (Cn n f gs) xs ↑"
using diverg_gs valid by fastforce
ultimately show ?thesis by simp
next
case converg
then have f: "eval f ?ys ↓" and g: "⋀g. g ∈ set gs ⟹ eval g xs ↓"
using valid(1) by (metis eval_Cn)+
then have "∀i<length gs. eval (gs ! i) xs ↓"
by simp
then have "reachable (?stack, None) ((Cn n f gs, xs, take (length gs) ?ys) # rest, None)"
using reachable_Cn assms by blast
also have "reachable ... ((Cn n f gs, xs, ?ys) # rest, None)" (is "_ (?stack1, None)")
also have "reachable ... ((f, ?ys, []) # ?stack1, None)"
using step_reachable by auto
also have "reachable ... (?stack1, eval f ?ys)"
using assms(2)[of "?ys"] correct_convergE valid f valid_ConsI by auto
also have "reachable (?stack1, eval f ?ys) (rest, eval f ?ys)"
using f by auto
finally have "reachable (?stack, None) (rest, eval f ?ys)" .
moreover have "eval (Cn n f gs) xs = eval f ?ys"
using g valid(1) by auto
ultimately show ?thesis
using converg correct_convergI by auto
qed
qed

text ‹During the execution of a frame with a partial recursive function
of shape @{term "Pr n f g"} and arguments @{term "x # xs"}, the list of local
variables collects all the function values up to @{term x} in reversed
order. We call such a list a @{term trace} for short.›

definition trace :: "nat ⇒ recf ⇒ recf ⇒ nat list ⇒ nat ⇒ nat list" where
"trace n f g xs x ≡ map (λy. the (eval (Pr n f g) (y # xs))) (rev [0..<Suc x])"

lemma trace_length: "length (trace n f g xs x) = Suc x"
using trace_def by simp

lemma trace_hd: "hd (trace n f g xs x) = the (eval (Pr n f g) (x # xs))"
using trace_def by simp

lemma trace_Suc:
"trace n f g xs (Suc x) = (the (eval (Pr n f g) (Suc x # xs))) # (trace n f g xs x)"
using trace_def by simp

lemma reachable_Pr:
assumes "valid (((Pr n f g), x # xs, []) # rest)" (is "valid ?stack")
and "⋀xs rest. valid ((f, xs, []) # rest) ⟹ correct ((f, xs, []) # rest, None)"
and "⋀xs rest. valid ((g, xs, []) # rest) ⟹ correct ((g, xs, []) # rest, None)"
and "y ≤ x"
and "eval (Pr n f g) (y # xs) ↓"
shows "reachable (?stack, None) ((Pr n f g, x # xs, trace n f g xs y) # rest, None)"
using assms(4,5)
proof (induction y)
case 0
have valid: "recfn (length (x # xs)) (Pr n f g)" "valid rest"
using valid_ConsE[OF assms(1)] by simp_all
then have f: "eval f xs ↓" using 0 by simp
let ?as = "x # xs"
have "reachable (?stack, None) ((f, xs, []) # ((Pr n f g), ?as, []) # rest, None)"
using step_reachable by auto
also have "reachable ... (?stack, eval f xs)"
using assms(2)[of xs "((Pr n f g), ?as, []) # rest"]
correct_convergE[OF _ f] f valid valid_ConsI
by simp
also have "reachable ... ((Pr n f g, ?as, [the (eval f xs)]) # rest, None)"
using step_reachable valid(1) f by auto
finally have "reachable (?stack, None) ((Pr n f g, ?as, [the (eval f xs)]) # rest, None)" .
then show ?case using trace_def valid(1) by simp
next
case (Suc y)
have valid: "recfn (length (x # xs)) (Pr n f g)" "valid rest"
using valid_ConsE[OF assms(1)] by simp_all
let ?ls = "trace n f g xs y"
have lenls: "length ?ls = Suc y"
using trace_length by auto
moreover have hdls: "hd ?ls = the (eval (Pr n f g) (y # xs))"
using Suc trace_hd by auto
ultimately have g:
"eval g (y # hd ?ls # xs) ↓"
"eval (Pr n f g) (Suc y # xs) = eval g (y # hd ?ls # xs)"
using eval_Pr_Suc_converg hdls valid(1) Suc by simp_all
then have "reachable (?stack, None) ((Pr n f g, x # xs, ?ls) # rest, None)"
(is "_ (?stack1, None)")
using Suc valid(1) by fastforce
also have "reachable ... ((g, y # hd ?ls # xs, []) # (Pr n f g, x # xs, ?ls) # rest, None)"
using Suc.prems lenls by fastforce
also have "reachable ... (?stack1, eval g (y # hd ?ls # xs))"
(is "_ (_, ?rv)")
using assms(3) g(1) valid valid_ConsI by auto
also have "reachable ... ((Pr n f g, x # xs, (the ?rv) # ?ls) # rest, None)"
using Suc.prems(1) g(1) lenls by auto
finally have "reachable (?stack, None) ((Pr n f g, x # xs, (the ?rv) # ?ls) # rest, None)" .
moreover have "trace n f g xs (Suc y) = (the ?rv) # ?ls"
using g(2) trace_Suc by simp
ultimately show ?case by simp
qed

lemma step_Pr_correct:
assumes "valid (((Pr n f g), xs, []) # rest)" (is "valid ?stack")
and "⋀xs rest. valid ((f, xs, []) # rest) ⟹ correct ((f, xs, []) # rest, None)"
and "⋀xs rest. valid ((g, xs, []) # rest) ⟹ correct ((g, xs, []) # rest, None)"
shows "correct (?stack, None)"
proof -
have valid: "valid rest" "recfn (length xs) (Pr n f g)"
using valid_ConsE[OF assms(1)] by simp_all
then have "length xs > 0"
by auto
then obtain y ys where y_ys: "xs = y # ys"
using list.exhaust_sel by auto
let ?t = "trace n f g ys"
consider
(converg) "eval (Pr n f g) xs ↓"
| (diverg_f) "eval (Pr n f g) xs ↑" and "eval f ys ↑"
| (diverg) "eval (Pr n f g) xs ↑" and "eval f ys ↓"
by auto
then show ?thesis
proof (cases)
case converg
then have "⋀z. z ≤ y ⟹ reachable (?stack, None) (((Pr n f g), xs, ?t z) # rest, None)"
using assms valid by (simp add: eval_Pr_converg_le reachable_Pr y_ys)
then have "reachable (?stack, None) (((Pr n f g), xs, ?t y) # rest, None)"
by simp
moreover have "reachable (((Pr n f g), xs, ?t y) # rest, None) (rest, Some (hd (?t y)))"
using trace_length step_reachable y_ys by fastforce
ultimately have "reachable (?stack, None) (rest, Some (hd (?t y)))"
using reachable_transitive by blast
then show ?thesis
using assms(1) trace_hd converg y_ys by simp
next
case diverg_f
have *: "step (?stack, None) = ((f, ys, []) # ((Pr n f g), xs, []) # tl ?stack, None)"
(is "_ = (?stack1, None)")
using assms(1,2) y_ys by simp
then have "reachable (?stack, None) (?stack1, None)"
using step_reachable by force
moreover have "nonterminating (?stack1, None)"
using assms diverg_f valid valid_ConsI * by auto
ultimately have "nonterminating (?stack, None)"
using reachable_nonterminating by blast
then show ?thesis using diverg_f(1) assms(1) by simp
next
case diverg
let ?h = "λz. the (eval (Pr n f g) (z # ys))"
let ?Q = "λz. z < y ∧ eval (Pr n f g) (z # ys) ↓"
have "?Q 0"
using assms diverg neq0_conv y_ys valid by fastforce
define zmax where "zmax = Greatest ?Q"
then have "?Q zmax"
using ‹?Q 0› GreatestI_nat[of ?Q 0 y] by simp
have le_zmax: "⋀z. ?Q z ⟹ z ≤ zmax"
using Greatest_le_nat[of ?Q _ y] zmax_def by simp
have len: "length (?t zmax) < Suc y"
by (simp add: ‹?Q zmax› trace_length)
have "eval (Pr n f g) (y # ys) ↓" if "y ≤ zmax" for y
using that zmax_def ‹?Q zmax› assms eval_Pr_converg_le[of n f g ys zmax y] valid y_ys
by simp
then have "reachable (?stack, None) (((Pr n f g), xs, ?t y) # rest, None)"
if "y ≤ zmax" for y
using that ‹?Q zmax› diverg y_ys assms reachable_Pr by simp
then have "reachable (?stack, None) (((Pr n f g), xs, ?t zmax) # rest, None)"
(is "reachable _ (?stack1, None)")
by simp
also have "reachable ...
((g, zmax # ?h zmax # tl xs, []) # (Pr n f g, xs, ?t zmax) # rest, None)"
(is "_ (?stack2, None)")
proof (rule step_reachable)
have "length (?t zmax) ≠ Suc (hd xs)"
using len y_ys by simp
moreover have "hd (?t zmax) = ?h zmax"
using trace_hd by auto
moreover have "length (?t zmax) = Suc zmax"
using trace_length by simp
ultimately show "step (?stack1, None) = (?stack2, None)"
by auto
qed
finally have "reachable (?stack, None) (?stack2, None)" .
moreover have "nonterminating (?stack2, None)"
proof -
have "correct (?stack2, None)"
using y_ys assms valid_ConsI valid by simp
moreover have "eval g (zmax # ?h zmax # ys) ↑"
using ‹?Q zmax› diverg le_zmax len less_Suc_eq trace_length y_ys valid
by fastforce
ultimately show ?thesis using y_ys by simp
qed
ultimately have "nonterminating (?stack, None)"
using reachable_nonterminating by simp
then show ?thesis using diverg assms(1) by simp
qed
qed

lemma reachable_Mn:
assumes "valid ((Mn n f, xs, []) # rest)" (is "valid ?stack")
and "⋀xs rest. valid ((f, xs, []) # rest) ⟹ correct ((f, xs, []) # rest, None)"
and "∀y<z. eval f (y # xs) ∉ {None, Some 0}"
shows "reachable (?stack, None) ((f, z # xs, []) # (Mn n f, xs, [z]) # rest, None)"
using assms(3)
proof (induction z)
case 0
then have "step (?stack, None) = ((f, 0 # xs, []) # (Mn n f, xs, ) # rest, None)"
using assms by simp
then show ?case
using step_reachable assms(1) by force
next
case (Suc z)
have valid: "valid rest" "recfn (length xs) (Mn n f)"
using valid_ConsE[OF assms(1)] by auto
have f: "eval f (z # xs) ∉ {None, Some 0}"
using Suc by simp
have "reachable (?stack, None) ((f, z # xs, []) # (Mn n f, xs, [z]) # rest, None)"
using Suc by simp
also have "reachable ... ((Mn n f, xs, [z]) # rest, eval f (z # xs))"
using f assms(2)[of "z # xs"] valid correct_convergE valid_ConsI by auto
also have "reachable ... ((f, (Suc z) # xs, []) # (Mn n f, xs, [Suc z]) # rest, None)"
(is "_  (?stack1, None)")
using step_reachable f by force
finally have "reachable (?stack, None) (?stack1, None)" .
then show ?case by simp
qed

lemma iterate_step_empty_stack: "iterate t step ([], rv) = ([], rv)"
using step_empty_stack by (induction t) simp_all

lemma reachable_iterate_step_empty_stack:
assumes "reachable cfg ([], rv)"
shows "∃t. iterate t step cfg = ([], rv) ∧ (∀t'<t. fst (iterate t' step cfg) ≠ [])"
proof -
let ?P = "λt. iterate t step cfg = ([], rv)"
from assms have "∃t. ?P t"
moreover define tmin where "tmin = Least ?P"
ultimately have "?P tmin"
using LeastI_ex[of ?P] by simp
have "fst (iterate t' step cfg) ≠ []" if "t' < tmin" for t'
proof
assume "fst (iterate t' step cfg) = []"
then obtain v where v: "iterate t' step cfg = ([], v)"
by (metis prod.exhaust_sel)
then have "iterate t'' step ([], v) = ([], v)" for t''
using iterate_step_empty_stack by simp
then have "iterate (t' + t'') step cfg = ([], v)" for t''
moreover obtain t'' where "t' + t'' = tmin"
using ‹t' < tmin› less_imp_add_positive by auto
ultimately have "iterate tmin step cfg = ([], v)"
by auto
then have "v = rv"
using ‹?P tmin› by simp
then have "iterate t' step cfg = ([], rv)"
using v by simp
moreover have "∀t'<tmin. ¬ ?P t'"
unfolding tmin_def using not_less_Least[of _ ?P] by simp
ultimately show False
using that by simp
qed
then show ?thesis using ‹?P tmin› by auto
qed

lemma step_Mn_correct:
assumes "valid ((Mn n f, xs, []) # rest)" (is "valid ?stack")
and "⋀xs rest. valid ((f, xs, []) # rest) ⟹ correct ((f, xs, []) # rest, None)"
shows "correct (?stack, None)"
proof -
have valid: "valid rest" "recfn (length xs) (Mn n f)"
using valid_ConsE[OF assms(1)] by auto
consider
(diverg) "eval (Mn n f) xs ↑" and "∀z. eval f (z # xs) ↓"
| (diverg_f) "eval (Mn n f) xs ↑" and "∃z. eval f (z # xs) ↑"
| (converg) "eval (Mn n f) xs ↓"
by fast
then show ?thesis
proof (cases)
case diverg
then have "∀z. eval f (z # xs) ≠ Some 0"
using eval_Mn_diverg[OF valid(2)] by simp
then have "∀y<z. eval f (y # xs) ∉ {None, Some 0}" for z
using diverg by simp
then have reach_z:
"⋀z. reachable (?stack, None) ((f, z # xs, []) # (Mn n f, xs, [z]) # rest, None)"
using reachable_Mn[OF assms] diverg by simp

define h :: "nat ⇒ configuration" where
"h z ≡ ((f, z # xs, []) # (Mn n f, xs, [z]) # rest, None)" for z
then have h_inj: "⋀x y. x ≠ y ⟹ h x ≠ h y" and z_neq_Nil: "⋀z. fst (h z) ≠ []"
by simp_all

have z: "∃z⇩0. ∀z>z⇩0. ¬ (∃t'≤t. iterate t' step (?stack, None) = h z)" for t
proof (induction t)
case 0
then show ?case by (metis h_inj le_zero_eq less_not_refl3)
next
case (Suc t)
then show ?case
using h_inj by (metis (no_types, hide_lams) le_Suc_eq less_not_refl3 less_trans)
qed

have "nonterminating (?stack, None)"
proof (rule ccontr)
assume "¬ nonterminating (?stack, None)"
then obtain t where t: "fst (iterate t step (?stack, None)) = []"
by auto
then obtain z⇩0 where "∀z>z⇩0. ¬ (∃t'≤t. iterate t' step (?stack, None) = h z)"
using z by auto
then have not_h: "∀t'≤t. iterate t' step (?stack, None) ≠ h (Suc z⇩0)"
by simp
have "∀t'≥t. fst (iterate t' step (?stack, None)) = []"
by (metis le_Suc_ex prod.exhaust_sel)
then have "∀t'≥t. iterate t' step (?stack, None) ≠ h (Suc z⇩0)"
using z_neq_Nil by auto
then have "∀t'. iterate t' step (?stack, None) ≠ h (Suc z⇩0)"
using not_h nat_le_linear by auto
then have "¬ reachable (?stack, None) (h (Suc z⇩0))"
using reachable_def by simp
then show False
using reach_z[of "Suc z⇩0"] h_def by simp
qed
then show ?thesis using diverg by simp
next
case diverg_f
let ?P = "λz. eval f (z # xs) ↑"
define zmin where "zmin ≡ Least ?P"
then have "∀y<zmin. eval f (y # xs) ∉ {None, Some 0}"
using diverg_f eval_Mn_diverg[OF valid(2)] less_trans not_less_Least[of _ ?P]
by blast
moreover have f_zmin: "eval f (zmin # xs) ↑"
using diverg_f LeastI_ex[of ?P] zmin_def by simp
ultimately have
"reachable (?stack, None) ((f, zmin # xs, []) # (Mn n f, xs, [zmin]) # rest, None)"
(is "reachable _ (?stack1, None)")
using reachable_Mn[OF assms] by simp
moreover have "nonterminating (?stack1, None)"
using f_zmin assms valid diverg_f valid_ConsI by auto
ultimately have "nonterminating (?stack, None)"
using reachable_nonterminating by simp
then show ?thesis using diverg_f by simp
next
case converg
then obtain z where z: "eval (Mn n f) xs ↓= z" by auto
have f_z: "eval f (z # xs) ↓= 0"
and f_less_z: "⋀y. y < z ⟹ eval f (y # xs) ↓≠ 0"
using eval_Mn_convergE(2,3)[OF valid(2) z] by simp_all
then have
"reachable (?stack, None) ((f, z # xs, []) # (Mn n f, xs, [z]) # rest, None)"
using reachable_Mn[OF assms] by simp
also have "reachable ... ((Mn n f, xs, [z]) # rest, eval f (z # xs))"
using assms(2)[of "z # xs"] valid f_z valid_ConsI correct_convergE
by auto
also have "reachable ... (rest, Some z)"
using f_z f_less_z step_reachable by auto
finally have "reachable (?stack, None) (rest, Some z)" .
then show ?thesis using z by simp
qed
qed

theorem step_correct:
assumes "valid ((f, xs, []) # rest)"
shows "correct ((f, xs, []) # rest, None)"
using assms
proof (induction f arbitrary: xs rest)
case Z
then show ?case using valid_ConsE[of Z] step_reachable by auto
next
case S
then show ?case using valid_ConsE[of S] step_reachable by auto
next
case (Id m n)
then show ?case using valid_ConsE[of "Id m n"] by auto
next
case Cn
then show ?case using step_Cn_correct by presburger
next
case Pr
then show ?case using step_Pr_correct by simp
next
case Mn
then show ?case using step_Mn_correct by presburger
qed

subsection ‹Encoding partial recursive functions\label{s:recf_enc}›

text ‹In this section we define an injective, but not surjective,
mapping from @{typ recf}s to natural numbers.›

abbreviation triple_encode :: "nat ⇒ nat ⇒ nat ⇒ nat" where
"triple_encode x y z ≡ prod_encode (x, prod_encode (y, z))"

abbreviation quad_encode :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat" where
"quad_encode w x y z ≡ prod_encode (w, prod_encode (x, prod_encode (y, z)))"

fun encode :: "recf ⇒ nat" where
"encode Z = 0"
| "encode S = 1"
| "encode (Id m n) = triple_encode 2 m n"
| "encode (Cn n f gs) = quad_encode 3 n (encode f) (list_encode (map encode gs))"
| "encode (Pr n f g) = quad_encode 4 n (encode f) (encode g)"
| "encode (Mn n f) = triple_encode 5 n (encode f)"

lemma prod_encode_gr1: "a > 1 ⟹ prod_encode (a, x) > 1"
using le_prod_encode_1 less_le_trans by blast

lemma encode_not_Z_or_S: "encode f = prod_encode (a, b) ⟹ a > 1 ⟹ f ≠ Z ∧ f ≠ S"
by (metis encode.simps(1) encode.simps(2) less_numeral_extra(4) not_one_less_zero
prod_encode_gr1)

lemma encode_injective: "encode f = encode g ⟹ f = g"
proof (induction g arbitrary: f)
case Z
have "⋀a x. a > 1 ⟹ prod_encode (a, x) > 0"
using prod_encode_gr1 by (meson less_one less_trans)
then have "f ≠ Z ⟹ encode f > 0"
by (cases f) auto
then have "encode f = 0 ⟹ f = Z" by fastforce
then show ?case using Z by simp
next
case S
have "⋀a x. a > 1 ⟹ prod_encode (a, x) ≠ Suc 0"
using prod_encode_gr1 by (metis One_nat_def less_numeral_extra(4))
then have "encode f = 1 ⟹ f = S"
by (cases f) auto
then show ?case using S by simp
next
case Id
then obtain z where *: "encode f = prod_encode (2, z)" by simp
show ?case
using Id by (cases f) (simp_all add: * encode_not_Z_or_S prod_encode_eq)
next
case Cn
then obtain z where *: "encode f = prod_encode (3, z)" by simp
show ?case
proof (cases f)
case Z
then show ?thesis using * encode_not_Z_or_S by simp
next
case S
then show ?thesis using * encode_not_Z_or_S by simp
next
case Id
then show ?thesis using * by (simp add: prod_encode_eq)
next
case Cn
then show ?thesis
using * Cn.IH Cn.prems list_decode_encode
by (smt encode.simps(4) fst_conv list.inj_map_strong prod_encode_eq snd_conv)
next
case Pr
then show ?thesis using * by (simp add: prod_encode_eq)
next
case Mn
then show ?thesis using * by (simp add: prod_encode_eq)
qed
next
case Pr
then obtain z where *: "encode f = prod_encode (4, z)" by simp
show ?case
using Pr by (cases f) (simp_all add: * encode_not_Z_or_S prod_encode_eq)
next
case Mn
then obtain z where *: "encode f = prod_encode (5, z)" by simp
show ?case
using Mn by (cases f) (simp_all add: * encode_not_Z_or_S prod_encode_eq)
qed

definition encode_kind :: "nat ⇒ nat" where
"encode_kind e ≡ if e = 0 then 0 else if e = 1 then 1 else pdec1 e"

lemma encode_kind_0: "encode_kind (encode Z) = 0"
unfolding encode_kind_def by simp

lemma encode_kind_1: "encode_kind (encode S) = 1"
unfolding encode_kind_def by simp

lemma encode_kind_2: "encode_kind (encode (Id m n)) = 2"
unfolding encode_kind_def
by (metis encode.simps(1-3) encode_injective fst_conv prod_encode_inverse
recf.simps(16) recf.simps(8))

lemma encode_kind_3: "encode_kind (encode (Cn n f gs)) = 3"
unfolding encode_kind_def
by (metis encode.simps(1,2,4) encode_injective fst_conv prod_encode_inverse
recf.simps(10) recf.simps(18))

lemma encode_kind_4: "encode_kind (encode (Pr n f g)) = 4"
unfolding encode_kind_def
by (metis encode.simps(1,2,5) encode_injective fst_conv prod_encode_inverse
recf.simps(12) recf.simps(20))

lemma encode_kind_5: "encode_kind (encode (Mn n f)) = 5"
unfolding encode_kind_def
by (metis encode.simps(1,2,6) encode_injective fst_conv prod_encode_inverse
recf.simps(14) recf.simps(22))

lemmas encode_kind_n =
encode_kind_0 encode_kind_1 encode_kind_2 encode_kind_3 encode_kind_4 encode_kind_5

lemma encode_kind_Cn:
assumes "encode_kind (encode f) = 3"
shows "∃n f' gs. f = Cn n f' gs"
using assms encode_kind_n by (cases f) auto

lemma encode_kind_Pr:
assumes "encode_kind (encode f) = 4"
shows "∃n f' g. f = Pr n f' g"
using assms encode_kind_n by (cases f) auto

lemma encode_kind_Mn:
assumes "encode_kind (encode f) = 5"
shows "∃n g. f = Mn n g"
using assms encode_kind_n by (cases f) auto

lemma pdec2_encode_Id: "pdec2 (encode (Id m n)) = prod_encode (m, n)"
by simp

lemma pdec2_encode_Pr: "pdec2 (encode (Pr n f g)) = triple_encode n (encode f) (encode g)"
by simp

subsection ‹The step function on encoded configurations\label{s:step_enc}›

text ‹In this section we construct a function @{text "estep :: nat
⇒ nat"} that is equivalent to the function @{text "step ::
configuration ⇒ configuration"} except that it applies to encoded
configurations. We start by defining an encoding for configurations.›

definition encode_frame :: "frame ⇒ nat" where
"encode_frame s ≡
triple_encode (encode (fst s)) (list_encode (fst (snd s))) (list_encode (snd (snd s)))"

lemma encode_frame:
"encode_frame (f, xs, ls) = triple_encode (encode f) (list_encode xs) (list_encode ls)"
unfolding encode_frame_def by simp

abbreviation encode_option :: "nat option ⇒ nat" where
"encode_option x ≡ if x = None then 0 else Suc (the x)"

definition encode_config :: "configuration ⇒ nat" where
"encode_config cfg ≡
prod_encode (list_encode (map encode_frame (fst cfg)), encode_option (snd cfg))"

lemma encode_config:
"encode_config (ss, rv) = prod_encode (list_encode (map encode_frame ss), encode_option rv)"
unfolding encode_config_def by simp

text ‹Various projections from encoded configurations:›

definition e2stack where "e2stack e ≡ pdec1 e"
definition e2rv where "e2rv e ≡ pdec2 e"
definition e2tail where "e2tail e ≡ e_tl (e2stack e)"
definition e2frame where "e2frame e ≡ e_hd (e2stack e)"
definition e2i where "e2i e ≡ pdec1 (e2frame e)"
definition e2xs where "e2xs e ≡ pdec12 (e2frame e)"
definition e2ls where "e2ls e ≡ pdec22 (e2frame e)"
definition e2lenas where "e2lenas e ≡ e_length (e2xs e)"
definition e2lenls where "e2lenls e ≡ e_length (e2ls e)"

lemma e2rv_rv [simp]:
"e2rv (encode_config (ss, rv)) = (if rv ↑ then 0 else Suc (the rv))"
unfolding e2rv_def using encode_config by simp

lemma e2stack_stack [simp]:
"e2stack (encode_config (ss, rv)) = list_encode (map encode_frame ss)"
unfolding e2stack_def using encode_config by simp

lemma e2tail_tail [simp]:
"e2tail (encode_config (s # ss, rv)) = list_encode (map encode_frame ss)"
unfolding e2tail_def using encode_config by fastforce

lemma e2frame_frame [simp]:
"e2frame (encode_config (s # ss, rv)) = encode_frame s"
unfolding e2frame_def using encode_config by fastforce

lemma e2i_f [simp]:
"e2i (encode_config ((f, xs, ls) # ss, rv)) = encode f"
unfolding e2i_def using encode_config e2frame_frame encode_frame by force

lemma e2xs_xs [simp]:
"e2xs (encode_config ((f, xs, ls) # ss, rv)) = list_encode xs"
using e2xs_def e2frame_frame encode_frame by force

lemma e2ls_ls [simp]:
"e2ls (encode_config ((f, xs, ls) # ss, rv)) = list_encode ls"
using e2ls_def e2frame_frame encode_frame by force

lemma e2lenas_lenas [simp]:
"e2lenas (encode_config ((f, xs, ls) # ss, rv)) = length xs"
using e2lenas_def e2frame_frame encode_frame by simp

lemma e2lenls_lenls [simp]:
"e2lenls (encode_config ((f, xs, ls) # ss, rv)) = length ls"
using e2lenls_def e2frame_frame encode_frame by simp

lemma e2stack_0_iff_Nil:
assumes "e = encode_config (ss, rv)"
shows "e2stack e = 0 ⟷  ss = []"
using assms
by (metis list_encode.simps(1) e2stack_stack list_encode_0 map_is_Nil_conv)

lemma e2ls_0_iff_Nil [simp]: "list_decode (e2ls e) = [] ⟷ e2ls e = 0"
by (metis list_decode.simps(1) list_encode_decode)

text ‹We now define @{text eterm} piecemeal by considering the more
complicated cases @{text Cn}, @{text Pr}, and @{text Mn} separately.›

definition "estep_Cn e ≡
if e2lenls e = e_length (pdec222 (e2i e))
then if e2rv e = 0
then prod_encode (e_cons (triple_encode (pdec122 (e2i e)) (e2ls e) 0) (e2stack e), 0)
else prod_encode (e2tail e, e2rv e)
else if e2rv e = 0
then if e2lenls e < e_length (pdec222 (e2i e))
then prod_encode
(e_cons
(triple_encode (e_nth (pdec222 (e2i e)) (e2lenls e)) (e2xs e) 0)
(e2stack e),
0)
else prod_encode (e2tail e, e2rv e)
else prod_encode
(e_cons
(triple_encode (e2i e) (e2xs e) (e_snoc (e2ls e) (e2rv e - 1)))
(e2tail e),
0)"

lemma estep_Cn:
assumes "c = (((Cn n f gs, xs, ls) # fs), rv)"
shows "estep_Cn (encode_config c) = encode_config (step c)"

definition "estep_Pr e ≡
if e2ls e = 0
then if e2rv e = 0
then prod_encode
(e_cons (triple_encode (pdec122 (e2i e)) (e_tl (e2xs e)) 0) (e2stack e),
0)
else prod_encode
(e_cons (triple_encode (e2i e) (e2xs e) (singleton_encode (e2rv e - 1))) (e2tail e),
0)
else if e2lenls e = Suc (e_hd (e2xs e))
then prod_encode (e2tail e, Suc (e_hd (e2ls e)))
else if e2rv e = 0
then prod_encode
(e_cons
(triple_encode
(pdec222 (e2i e))
(e_cons (e2lenls e - 1) (e_cons (e_hd (e2ls e)) (e_tl (e2xs e))))
0)
(e2stack e),
0)
else prod_encode
(e_cons
(triple_encode (e2i e) (e2xs e) (e_cons (e2rv e - 1) (e2ls e))) (e2tail e),
0)"

lemma estep_Pr1:
assumes "c = (((Pr n f g, xs, ls) # fs), rv)"
and "ls ≠ []"
and "length ls ≠ Suc (hd xs)"
and "rv ≠ None"
and "recfn (length xs) (Pr n f g)"
shows "estep_Pr (encode_config c) = encode_config (step c)"
proof -
let ?e = "encode_config c"
from assms(5) have "length xs > 0" by auto
then have eq: "hd xs = e_hd (e2xs ?e)"
using assms e_hd_def by auto
have "step c = ((Pr n f g, xs, (the rv) # ls) # fs, None)"
(is "step c = (?t # ?ss, None)")
using assms by simp
then have "encode_config (step c) =
prod_encode (list_encode (map encode_frame (?t # ?ss)), 0)"
using encode_config by simp
also have "... =
prod_encode (e_cons (encode_frame ?t) (list_encode (map encode_frame (?ss))), 0)"
by simp
also have "... = prod_encode (e_cons (encode_frame ?t) (e2tail ?e), 0)"
using assms(1) by simp
also have "... = prod_encode
(e_cons
(triple_encode (e2i ?e) (e2xs ?e) (e_cons (e2rv ?e - 1) (e2ls ?e)))
(e2tail ?e),
0)"
finally show ?thesis
using assms eq estep_Pr_def by auto
qed

lemma estep_Pr2:
assumes "c = (((Pr n f g, xs, ls) # fs), rv)"
and "ls ≠ []"
and "length ls ≠ Suc (hd xs)"
and "rv = None"
and "recfn (length xs) (Pr n f g)"
shows "estep_Pr (encode_config c) = encode_config (step c)"
proof -
let ?e = "encode_config c"
from assms(5) have "length xs > 0" by auto
then have eq: "hd xs = e_hd (e2xs ?e)"
using assms e_hd_def by auto
have "step c = ((g, (length ls - 1) # hd ls # tl xs, []) # (Pr n f g, xs, ls) # fs, None)"
(is "step c = (?t # ?ss, None)")
using assms by simp
then have "encode_config (step c) =
prod_encode (list_encode (map encode_frame (?t # ?ss)), 0)"
using encode_config by simp
also have "... =
prod_encode (e_cons (encode_frame ?t) (list_encode (map encode_frame (?ss))), 0)"
by simp
also have "... = prod_encode (e_cons (encode_frame ?t) (e2stack ?e), 0)"
using assms(1) by simp
also have "... = prod_encode
(e_cons
(triple_encode
(pdec222 (e2i ?e))
(e_cons (e2lenls ?e - 1) (e_cons (e_hd (e2ls ?e)) (e_tl (e2xs ?e))))
0)
(e2stack ?e),
0)"
using assms(1,2) encode_frame[of g "(length ls - 1) # hd ls # tl xs" "[]"]
pdec2_encode_Pr[of n f g] e2xs_xs e2i_f e2lenls_lenls e2ls_ls e_hd
by (metis list_encode.simps(1) list.collapse list_decode_encode
prod_encode_inverse snd_conv)
finally show ?thesis
using assms eq estep_Pr_def by auto
qed

lemma estep_Pr3:
assumes "c = (((Pr n f g, xs, ls) # fs), rv)"
and "ls ≠ []"
and "length ls = Suc (hd xs)"
and "recfn (length xs) (Pr n f g)"
shows "estep_Pr (encode_config c) = encode_config (step c)"
proof -
let ?e = "encode_config c"
from assms(4) have "length xs > 0" by auto
then have "hd xs = e_hd (e2xs ?e)"
using assms e_hd_def by auto
then have "(length ls = Suc (hd xs)) = (e2lenls ?e = Suc (e_hd (e2xs ?e)))"
using assms by simp
then have *: "estep_Pr ?e = prod_encode (e2tail ?e, Suc (e_hd (e2ls ?e)))"
using assms estep_Pr_def by auto
have "step c = (fs, Some (hd ls))"
using assms(1,2,3) by simp
then have "encode_config (step c) =
prod_encode (list_encode (map encode_frame fs), encode_option (Some (hd ls)))"
using encode_config by simp
also have "... =
prod_encode (list_encode (map encode_frame fs), encode_option (Some (e_hd (e2ls ?e))))"
using assms(1,2) e_hd_def by auto
also have "... = prod_encode (list_encode (map encode_frame fs), Suc (e_hd (e2ls ?e)))"
by simp
also have "... = prod_encode (e2tail ?e, Suc (e_hd (e2ls ?e)))"
using assms(1) by simp
finally have "encode_config (step c) = prod_encode (e2tail ?e, Suc (e_hd (e2ls ?e)))" .
then show ?thesis
using estep_Pr_def * by presburger
qed

lemma estep_Pr4:
assumes "c = (((Pr n f g, xs, ls) # fs), rv)" and "ls = []"
shows "estep_Pr (encode_config c) = encode_config (step c)"
using encode_frame

lemma estep_Pr:
assumes "c = (((Pr n f g, xs, ls) # fs), rv)"
and "recfn (length xs) (Pr n f g)"
shows "estep_Pr (encode_config c) = encode_config (step c)"
using assms estep_Pr1 estep_Pr2 estep_Pr3 estep_Pr4 by auto

definition "estep_Mn e ≡
if e2ls e = 0
then prod_encode
(e_cons
(triple_encode (pdec22 (e2i e)) (e_cons 0 (e2xs e)) 0)
(e_cons
(triple_encode (e2i e) (e2xs e) (singleton_encode 0))
(e2tail e)),
0)
else if e2rv e = 1
then prod_encode (e2tail e, Suc (e_hd (e2ls e)))
else prod_encode
(e_cons
(triple_encode (pdec22 (e2i e)) (e_cons (Suc (e_hd (e2ls e))) (e2xs e)) 0)
(e_cons
(triple_encode (e2i e) (e2xs e) (singleton_encode (Suc (e_hd (e2ls e)))))
(e2tail e)),
0)"

lemma estep_Mn:
assumes "c = (((Mn n f, xs, ls) # fs), rv)"
shows "estep_Mn (encode_config c) = encode_config (step c)"
proof -
let ?e = "encode_config c"
consider "ls ≠ []" and "rv ≠ Some 0" | "ls ≠ []" and "rv = Some 0" | "ls = []"
by auto
then show ?thesis
proof (cases)
case 1
then have step_c: "step c =
((f, (Suc (hd ls)) # xs, []) # (Mn n f, xs, [Suc (hd ls)]) # fs, None)"
(is "step c = ?cfg")
using assms by simp
have "estep_Mn ?e =
prod_encode
(e_cons
(triple_encode (encode f) (e_cons (Suc (hd ls)) (list_encode xs)) 0)
(e_cons
(triple_encode (encode (Mn n f)) (list_encode xs) (singleton_encode (Suc (hd ls))))
(list_encode (map encode_frame fs))),
0)"
using 1 assms e_hd_def estep_Mn_def by auto
also have "... = encode_config ?cfg"
using encode_config by (simp add: encode_frame)
finally show ?thesis
using step_c by simp
next
case 2
have "estep_Mn ?e = prod_encode (e2tail ?e, Suc (e_hd (e2ls ?e)))"
using 2 assms estep_Mn_def by auto
also have "... = prod_encode (e2tail ?e, Suc (hd ls))"
using 2 assms e_hd_def by auto
also have "... = prod_encode (list_encode (map encode_frame fs), Suc (hd ls))"
using assms by simp
also have "... = encode_config (fs, Some (hd ls))"
using encode_config by simp
finally show ?thesis
using 2 assms by simp
next
case 3
then show ?thesis
qed
qed

definition "estep e ≡
if e2stack e = 0 then prod_encode (0, e2rv e)
else if e2i e = 0 then prod_encode (e2tail e, 1)
else if e2i e = 1 then prod_encode (e2tail e, Suc (Suc (e_hd (e2xs e))))
else if encode_kind (e2i e) = 2 then
prod_encode (e2tail e, Suc (e_nth (e2xs e) (pdec22 (e2i e))))
else if encode_kind (e2i e) = 3 then estep_Cn e
else if encode_kind (e2i e) = 4 then estep_Pr e
else if encode_kind (e2i e) = 5 then estep_Mn e
else 0"

lemma estep_Z:
assumes "c = (((Z, xs, ls) # fs), rv)"
shows "estep (encode_config c) = encode_config (step c)"

lemma estep_S:
assumes "c = (((S, xs, ls) # fs), rv)"
and "recfn (length xs) (fst (hd (fst c)))"
shows "estep (encode_config c) = encode_config (step c)"
proof -
let ?e = "encode_config c"
from assms have "length xs > 0" by auto
then have eq: "hd xs = e_hd (e2xs ?e)"
using assms(1) e_hd_def by auto
then have "estep ?e = prod_encode (e2tail ?e, Suc (Suc (e_hd (e2xs ?e))))"
using assms(1) estep_def by simp
moreover have "step c = (fs, Some (Suc (hd xs)))"
using assms(1) by simp
ultimately show ?thesis
using assms(1) eq estep_def encode_config[of fs "Some (Suc (hd xs))"] by simp
qed

lemma estep_Id:
assumes "c = (((Id m n, xs, ls) # fs), rv)"
and "recfn (length xs) (fst (hd (fst c)))"
shows "estep (encode_config c) = encode_config (step c)"
proof -
let ?e = "encode_config c"
from assms have "length xs = m" and "m > 0" by auto
then have eq: "xs ! n = e_nth (e2xs ?e) n"
using assms e_hd_def by auto
moreover have "encode_kind (e2i ?e) = 2"
using assms(1) encode_kind_2 by auto
ultimately have "estep ?e =
prod_encode (e2tail ?e, Suc (e_nth (e2xs ?e) (pdec22 (e2i ?e))))"
using assms estep_def encode_kind_def by auto
moreover have "step c = (fs, Some (xs ! n))"
using assms(1) by simp
ultimately show ?thesis
using assms(1) eq encode_config[of fs "Some (xs ! n)"] by simp
qed

lemma estep:
assumes "valid (fst c)"
shows "estep (encode_config c) = encode_config (step c)"
proof (cases "fst c")
case Nil
then show ?thesis
using estep_def
by (metis list_encode.simps(1) e2rv_def e2stack_stack encode_config_def
map_is_Nil_conv prod.collapse prod_encode_inverse snd_conv step.simps(1))
next
case (Cons s fs)
then obtain f xs ls rv where c: "c = ((f, xs, ls) # fs, rv)"
by (metis prod.exhaust_sel)
with assms valid_def have lenas: "recfn (length xs) f" by simp
show ?thesis
proof (cases f)
case Z
then show ?thesis using estep_Z c by simp
next
case S
then show ?thesis using estep_S c lenas by simp
next
case Id
then show ?thesis using estep_Id c lenas by simp
next
case Cn
then show ?thesis
using estep_Cn c
by (metis e2i_f e2stack_0_iff_Nil encode.simps(1) encode.simps(2) encode_kind_2
encode_kind_3 encode_kind_Cn estep_def list.distinct(1) recf.distinct(13)
recf.distinct(19) recf.distinct(5))
next
case Pr
then show ?thesis
using estep_Pr c lenas
by (metis e2i_f e2stack_0_iff_Nil encode.simps(1) encode.simps(2) encode_kind_2
encode_kind_4 encode_kind_Cn encode_kind_Pr estep_def list.distinct(1) recf.distinct(15)
recf.distinct(21) recf.distinct(25) recf.distinct(7))
next
case Mn
then show ?thesis
using estep_Pr c lenas
by (metis (no_types, lifting) e2i_f e2stack_0_iff_Nil encode.simps(1)
encode.simps(2) encode_kind_2 encode_kind_5 encode_kind_Cn encode_kind_Mn encode_kind_Pr
estep_Mn estep_def list.distinct(1) recf.distinct(17) recf.distinct(23)
recf.distinct(27) recf.distinct(9))
qed
qed

subsection ‹The step function as a partial recursive function\label{s:step_recf}›

text ‹In this section we construct a primitive recursive function
@{term r_step} computing @{term estep}. This will entail defining @{typ
recf}s for many functions defined in the previous section.›

definition "r_e2stack ≡ r_pdec1"

lemma r_e2stack_prim: "prim_recfn 1 r_e2stack"
unfolding r_e2stack_def using r_pdec1_prim by simp

lemma r_e2stack [simp]: "eval r_e2stack [e] ↓= e2stack e"
unfolding r_e2stack_def e2stack_def using r_pdec1_prim by simp

definition "r_e2rv ≡ r_pdec2"

lemma r_e2rv_prim: "prim_recfn 1 r_e2rv"
unfolding r_e2rv_def using r_pdec2_prim by simp

lemma r_e2rv [simp]: "eval r_e2rv [e] ↓= e2rv e"
unfolding r_e2rv_def e2rv_def using r_pdec2_prim by simp

definition "r_e2tail ≡ Cn 1 r_tl [r_e2stack]"

lemma r_e2tail_prim: "prim_recfn 1 r_e2tail"
unfolding r_e2tail_def using r_e2stack_prim r_tl_prim by simp

lemma r_e2tail [simp]: "eval r_e2tail [e] ↓= e2tail e"
unfolding r_e2tail_def e2tail_def using r_e2stack_prim r_tl_prim by simp

definition "r_e2frame ≡ Cn 1 r_hd [r_e2stack]"

lemma r_e2frame_prim: "prim_recfn 1 r_e2frame"
unfolding r_e2frame_def using r_hd_prim r_e2stack_prim by simp

lemma r_e2frame [simp]: "eval r_e2frame [e] ↓= e2frame e"
unfolding r_e2frame_def e2frame_def using r_hd_prim r_e2stack_prim by simp

definition "r_e2i ≡ Cn 1 r_pdec1 [r_e2frame]"

lemma r_e2i_prim: "prim_recfn 1 r_e2i"
unfolding r_e2i_def using r_pdec12_prim r_e2frame_prim by simp

lemma r_e2i [simp]: "eval r_e2i [e] ↓= e2i e"
unfolding r_e2i_def e2i_def using r_pdec12_prim r_e2frame_prim by simp

definition "r_e2xs ≡ Cn 1 r_pdec12 [r_e2frame]"

lemma r_e2xs_prim: "prim_recfn 1 r_e2xs"
unfolding r_e2xs_def using r_pdec122_prim r_e2frame_prim by simp

lemma r_e2xs [simp]: "eval r_e2xs [e] ↓= e2xs e"
unfolding r_e2xs_def e2xs_def using r_pdec122_prim r_e2frame_prim by simp

definition "r_e2ls ≡ Cn 1 r_pdec22 [r_e2frame]"

lemma r_e2ls_prim: "prim_recfn 1 r_e2ls"
unfolding r_e2ls_def using r_pdec222_prim r_e2frame_prim by simp

lemma r_e2ls [simp]: "eval r_e2ls [e] ↓= e2ls e"
unfolding r_e2ls_def e2ls_def using r_pdec222_prim r_e2frame_prim by simp

definition "r_e2lenls ≡ Cn 1 r_length [r_e2ls]"

lemma r_e2lenls_prim: "prim_recfn 1 r_e2lenls"
unfolding r_e2lenls_def using r_length_prim r_e2ls_prim by simp

lemma r_e2lenls [simp]: "eval r_e2lenls [e] ↓= e2lenls e"
unfolding r_e2lenls_def e2lenls_def using r_length_prim r_e2ls_prim by simp

definition "r_kind ≡
Cn 1 r_ifz [Id 1 0, Z, Cn 1 r_ifeq [Id 1 0, r_const 1, r_const 1, r_pdec1]]"

lemma r_kind_prim: "prim_recfn 1 r_kind"
unfolding r_kind_def by simp

lemma r_kind: "eval r_kind [e] ↓= encode_kind e"
unfolding r_kind_def encode_kind_def by simp

lemmas helpers_for_r_step_prim =
r_e2i_prim
r_e2lenls_prim
r_e2ls_prim
r_e2rv_prim
r_e2xs_prim
r_e2stack_prim
r_e2tail_prim
r_e2frame_prim

text ‹We define primitive recursive functions @{term r_step_Id}, @{term
r_step_Cn}, @{term r_step_Pr}, and @{term r_step_Mn}. The last three
correspond to @{term estep_Cn}, @{term estep_Pr}, and @{term estep_Mn} from
the previous section.›

definition "r_step_Id ≡
Cn 1 r_prod_encode [r_e2tail, Cn 1 S [Cn 1 r_nth [r_e2xs, Cn 1 r_pdec22 [r_e2i]]]]"

lemma r_step_Id:
"eval r_step_Id [e] ↓= prod_encode (e2tail e, Suc (e_nth (e2xs e) (pdec22 (e2i e))))"
unfolding r_step_Id_def using helpers_for_r_step_prim by simp

abbreviation r_triple_encode :: "recf ⇒ recf ⇒ recf ⇒ recf" where
"r_triple_encode x y z ≡ Cn 1 r_prod_encode [x, Cn 1 r_prod_encode [y, z]]"

definition "r_step_Cn ≡
Cn 1 r_ifeq
[r_e2lenls,
Cn 1 r_length [Cn 1 r_pdec222 [r_e2i]],
Cn 1 r_ifz
[r_e2rv,
Cn 1 r_prod_encode
[Cn 1 r_cons [r_triple_encode (Cn 1 r_pdec122 [r_e2i]) r_e2ls Z, r_e2stack],
Z],
Cn 1 r_prod_encode [r_e2tail, r_e2rv]],
Cn 1 r_ifz
[r_e2rv,
Cn 1 r_ifless
[r_e2lenls,
Cn 1 r_length [Cn 1 r_pdec222 [r_e2i]],
Cn 1 r_prod_encode
[Cn 1 r_cons
[r_triple_encode (Cn 1 r_nth [Cn 1 r_pdec222 [r_e2i], r_e2lenls]) r_e2xs Z,
r_e2stack],
Z],
Cn 1 r_prod_encode [r_e2tail, r_e2rv]],
Cn 1 r_prod_encode
[Cn 1 r_cons
[r_triple_encode r_e2i r_e2xs (Cn 1 r_snoc [r_e2ls, Cn 1 r_dec [r_e2rv]]),
r_e2tail],
Z]]]"

lemma r_step_Cn_prim: "prim_recfn 1 r_step_Cn"
unfolding r_step_Cn_def using helpers_for_r_step_prim by simp

lemma r_step_Cn: "eval r_step_Cn [e] ↓= estep_Cn e"
unfolding r_step_Cn_def estep_Cn_def using helpers_for_r_step_prim by simp

definition "r_step_Pr ≡
Cn 1 r_ifz
[r_e2ls,
Cn 1 r_ifz
[r_e2rv,
Cn 1 r_prod_encode
[Cn 1 r_cons
[r_triple_encode (Cn 1 r_pdec122 [r_e2i]) (Cn 1 r_tl [r_e2xs]) Z,
r_e2stack],
Z],
Cn 1 r_prod_encode
[Cn 1 r_cons
[r_triple_encode r_e2i r_e2xs (Cn 1 r_singleton_encode [Cn 1 r_dec [r_e2rv]]),
r_e2tail],
Z]],
Cn 1 r_ifeq
[r_e2lenls,
Cn 1 S [Cn 1 r_hd [r_e2xs]],
Cn 1 r_prod_encode [r_e2tail, Cn 1 S [Cn 1 r_hd [r_e2ls]]],
Cn 1 r_ifz
[r_e2rv,
Cn 1 r_prod_encode
[Cn 1 r_cons
[r_triple_encode
(Cn 1 r_pdec222 [r_e2i])
(Cn 1 r_cons
[Cn 1 r_dec [r_e2lenls],
Cn 1 r_cons [Cn 1 r_hd [r_e2ls],
Cn 1 r_tl [r_e2xs]]])
Z,
r_e2stack],
Z],
Cn 1 r_prod_encode
[Cn 1 r_cons
[r_triple_encode r_e2i r_e2xs (Cn 1 r_cons [Cn 1 r_dec [r_e2rv], r_e2ls]),
r_e2tail],
Z]]]]"

lemma r_step_Pr_prim: "prim_recfn 1 r_step_Pr"
unfolding r_step_Pr_def using helpers_for_r_step_prim by simp

lemma r_step_Pr: "eval r_step_Pr [e] ↓= estep_Pr e"
unfolding r_step_Pr_def estep_Pr_def using helpers_for_r_step_prim by simp

definition "r_step_Mn ≡
Cn 1 r_ifz
[r_e2ls,
Cn 1 r_prod_encode
[Cn 1 r_cons
[r_triple_encode (Cn 1 r_pdec22 [r_e2i]) (Cn 1 r_cons [Z, r_e2xs]) Z,
Cn 1 r_cons
[r_triple_encode r_e2i r_e2xs (Cn 1 r_singleton_encode [Z]),
r_e2tail]],
Z],
Cn 1 r_ifeq
[r_e2rv,
r_const 1,
Cn 1 r_prod_encode [r_e2tail, Cn 1 S [Cn 1 r_hd [r_e2ls]]],
Cn 1 r_prod_encode
[Cn 1 r_cons
[r_triple_encode
(Cn 1 r_pdec22 [r_e2i])
(Cn 1 r_cons [Cn 1 S [Cn 1 r_hd [r_e2ls]], r_e2xs])
Z,
Cn 1 r_cons
[r_triple_encode r_e2i r_e2xs (Cn 1 r_singleton_encode [Cn 1 S [Cn 1 r_hd [r_e2ls]]]),
r_e2tail]],
Z]]]"

lemma r_step_Mn_prim: "prim_recfn 1 r_step_Mn"
unfolding r_step_Mn_def using helpers_for_r_step_prim by simp

lemma r_step_Mn: "eval r_step_Mn [e] ↓= estep_Mn e"
unfolding r_step_Mn_def estep_Mn_def using helpers_for_r_step_prim by simp

definition "r_step ≡
Cn 1 r_ifz
[r_e2stack,
Cn 1 r_prod_encode [Z, r_e2rv],
Cn 1 r_ifz
[r_e2i,
Cn 1 r_prod_encode [r_e2tail, r_const 1],
Cn 1 r_ifeq
[r_e2i,
r_const 1,
Cn 1 r_prod_encode [r_e2tail, Cn 1 S [Cn 1 S [Cn 1 r_hd [r_e2xs]]]],
Cn 1 r_ifeq
[Cn 1 r_kind [r_e2i],
r_const 2,
Cn 1 r_prod_encode [r_e2tail, Cn 1 S [Cn 1 r_nth [r_e2xs, Cn 1 r_pdec22 [r_e2i]]]],
Cn 1 r_ifeq
[Cn 1 r_kind [r_e2i],
r_const 3,
r_step_Cn,
Cn 1 r_ifeq
[Cn 1 r_kind [r_e2i],
r_const 4,
r_step_Pr,
Cn 1 r_ifeq
[Cn 1 r_kind [r_e2i], r_const 5, r_step_Mn, Z]]]]]]]"

lemma r_step_prim: "prim_recfn 1 r_step"
unfolding r_step_def
using r_kind_prim r_step_Mn_prim r_step_Pr_prim r_step_Cn_prim helpers_for_r_step_prim
by simp

lemma r_step: "eval r_step [e] ↓= estep e"
unfolding r_step_def estep_def
using r_kind_prim r_step_Mn_prim r_step_Pr_prim r_step_Cn_prim helpers_for_r_step_prim
r_kind r_step_Cn r_step_Pr r_step_Mn
by simp

theorem r_step_equiv_step:
assumes "valid (fst c)"
shows "eval r_step [encode_config c] ↓= encode_config (step c)"
using r_step estep assms by simp

subsection ‹The universal function\label{s:the_universal}›

text ‹The next function computes the configuration after arbitrarily
many steps.›

definition "r_leap ≡
Pr 2
(Cn 2 r_prod_encode
[Cn 2 r_singleton_encode
[Cn 2 r_prod_encode [Id 2 0, Cn 2 r_prod_encode [Id 2 1, r_constn 1 0]]],
r_constn 1 0])
(Cn 4 r_step [Id 4 1])"

lemma r_leap_prim [simp]: "prim_recfn 3 r_leap"
unfolding r_leap_def using r_step_prim by simp

lemma r_leap_total: "eval r_leap [t, i, x] ↓"
using prim_recfn_total[OF r_leap_prim] by simp

lemma r_leap:
assumes "i = encode f" and "recfn (e_length x) f"
shows "eval r_leap [t, i, x] ↓= encode_config (iterate t step ([(f, list_decode x, [])], None))"
proof (induction t)
case 0
then show ?case
unfolding r_leap_def using r_step_prim assms encode_config encode_frame by simp
next
case (Suc t)
let ?c = "([(f, list_decode x, [])], None)"
let ?tc = "iterate t step ?c"
have "valid (fst ?c)"
using valid_def assms by simp
then have valid: "valid (fst ?tc)"
using iterate_step_valid by simp
have "eval r_leap [Suc t, i, x] =
eval (Cn 4 r_step [Id 4 1]) [t, the (eval r_leap [t, i, x]), i, x]"
by (smt One_nat_def Suc_eq_plus1 eq_numeral_Suc eval_Pr_converg_Suc list.size(3) list.size(4) nat_1_add_1 pred_numeral_simps(3) r_leap_def r_leap_prim r_leap_total)
then have "eval r_leap [Suc t, i, x] = eval (Cn 4 r_step [Id 4 1]) [t, encode_config ?tc, i, x]"
using Suc by simp
then have "eval r_leap [Suc t, i, x] = eval r_step [encode_config ?tc]"
using r_step_prim by simp
then have "eval r_leap [Suc t, i, x] ↓= encode_config (step ?tc)"
then show ?case by simp
qed

lemma step_leaves_empty_stack_empty:
assumes "iterate t step ([(f, list_decode x, [])], None) = ([], Some v)"
shows "iterate (t + t') step ([(f, list_decode x, [])], None) = ([], Some v)"
using assms by (induction t') simp_all

text ‹The next function is essentially a convenience wrapper around
@{term r_leap}. It returns zero if the configuration returned by @{term
r_leap} is non-final, and @{term "Suc v"} if the configuration is final with
return value $v$.›

definition "r_result ≡
Cn 3 r_ifz [Cn 3 r_pdec1 [r_leap], Cn 3 r_pdec2 [r_leap], r_constn 2 0]"

lemma r_result_prim [simp]: "prim_recfn 3 r_result"
unfolding r_result_def using r_leap_prim by simp

lemma r_result_total: "total r_result"
using r_result_prim by blast

lemma r_result_empty_stack_None:
assumes "i = encode f"
and "recfn (e_length x) f"
and "iterate t step ([(f, list_decode x, [])], None) = ([], None)"
shows "eval r_result [t, i, x] ↓= 0"
unfolding r_result_def
using assms r_leap e2stack_0_iff_Nil e2stack_def e2stack_stack r_leap_total r_leap_prim
e2rv_def e2rv_rv
by simp

lemma r_result_empty_stack_Some:
assumes "i = encode f"
and "recfn (e_length x) f"
and "iterate t step ([(f, list_decode x, [])], None) = ([], Some v)"
shows "eval r_result [t, i, x] ↓= Suc v"
unfolding r_result_def
using assms r_leap e2stack_0_iff_Nil e2stack_def e2stack_stack r_leap_total r_leap_prim
e2rv_def e2rv_rv
by simp

lemma r_result_empty_stack_stays:
assumes "i = encode f"
and "recfn (e_length x) f"
and "iterate t step ([(f, list_decode x, [])], None) = ([], Some v)"
shows "eval r_result [t + t', i, x] ↓= Suc v"
using assms step_leaves_empty_stack_empty r_result_empty_stack_Some by simp

lemma r_result_nonempty_stack:
assumes "i = encode f"
and "recfn (e_length x) f"
and "fst (iterate t step ([(f, list_decode x, [])], None)) ≠ []"
shows "eval r_result [t, i, x] ↓= 0"
proof -
obtain ss rv where "iterate t step ([(f, list_decode x, [])], None) = (ss, rv)"
by fastforce
moreover from this assms(3) have "ss ≠ []" by simp
ultimately have "eval r_leap [t, i, x] ↓= encode_config (ss, rv)"
using assms r_leap by simp
then have "eval (Cn 3 r_pdec1 [r_leap]) [t, i, x] ↓≠ 0"
using ‹ss ≠ []› r_leap_prim encode_config r_leap_total list_encode_0
by (auto, blast)
then show ?thesis unfolding r_result_def using r_leap_prim by auto
qed

lemma r_result_Suc:
assumes "i = encode f"
and "recfn (e_length x) f"
and "eval r_result [t, i, x] ↓= Suc v"
shows "iterate t step ([(f, list_decode x, [])], None) = ([], Some v)"
(is "?cfg = _")
proof (cases "fst ?cfg")
case Nil
then show ?thesis
using assms r_result_empty_stack_None r_result_empty_stack_Some
by (metis Zero_not_Suc nat.inject option.collapse option.inject prod.exhaust_sel)
next
case Cons
then show ?thesis using assms r_result_nonempty_stack by simp
qed

lemma r_result_converg:
assumes "i = encode f"
and "recfn (e_length x) f"
and "eval f (list_decode x) ↓= v"
shows "∃t.
(∀t'≥t. eval r_result [t', i, x] ↓= Suc v) ∧
(∀t'<t. eval r_result [t', i, x] ↓= 0)"
proof -
let ?xs = "list_decode x"
let ?stack = "[(f, ?xs, [])]"
have "wellf f" using assms(2) by simp
moreover have "length ?xs = arity f"
using assms(2) by simp
ultimately have "correct (?stack, None)"
using step_correct valid_def by simp
with assms(3) have "reachable (?stack, None) ([], Some v)"
by simp
then obtain t where
"iterate t step (?stack, None) = ([], Some v)"
"∀t'<t. fst (iterate t' step (?stack, None)) ≠ []"
using reachable_iterate_step_empty_stack by blast
then have t:
"eval r_result [t, i, x] ↓= Suc v"
"∀t'<t. eval r_result [t', i, x] ↓= 0"
using r_result_empty_stack_Some r_result_nonempty_stack assms(1,2)
by simp_all
then have "eval r_result [t + t', i, x] ↓= Suc v" for t'
using r_result_empty_stack_stays assms r_result_Suc by simp
then have "∀t'≥t. eval r_result [t', i, x] ↓= Suc v"
using le_Suc_ex by blast
with t(2) show ?thesis by auto
qed

lemma r_result_diverg:
assumes "i = encode f"
and "recfn (e_length x) f"
and "eval f (list_decode x) ↑"
shows "eval r_result [t, i, x] ↓= 0"
proof -
let ?xs = "list_decode x"
let ?stack = "[(f, ?xs, [])]"
have "recfn (length ?xs) f"
using assms(2) by auto
then have "correct (?stack, None)"
using step_correct valid_def by simp
with assms(3) have "nonterminating (?stack, None)"
by simp
then show ?thesis
using r_result_nonempty_stack assms(1,2) by simp
qed

text ‹Now we can define the universal partial recursive function. This
function executes @{term r_result} for increasing time bounds, waits for it
to reach a final configuration, and then extracts its result value. If no
final configuration is reached, the universal function diverges.›

definition "r_univ ≡
Cn 2 r_dec [Cn 2 r_result [Mn 2 (Cn 3 r_not [r_result]), Id 2 0, Id 2 1]]"

lemma r_univ_recfn [simp]: "recfn 2 r_univ"
unfolding r_univ_def by simp

theorem r_univ:
assumes "i = encode f" and "recfn (e_length x) f"
shows "eval r_univ [i, x] = eval f (list_decode x)"
proof -
let ?cond = "Cn 3 r_not [r_result]"
let ?while = "Mn 2 ?cond"
let ?res = "Cn 2 r_result [?while, Id 2 0, Id 2 1]"
let ?xs = "list_decode x"
have *: "eval ?cond [t, i, x] ↓= (if eval r_result [t, i, x] ↓= 0 then 1 else 0)" for t
proof -
have "eval ?cond [t, i, x] = eval r_not [the (eval r_result [t, i, x])]"
using r_result_total by simp
moreover have "eval r_result [t, i, x] ↓"
ultimately show ?thesis by auto
qed
show ?thesis
proof (cases "eval f ?xs ↑")
case True
then show ?thesis
unfolding r_univ_def using * r_result_diverg[OF assms] eval_Mn_diverg by simp
next
case False
then obtain v where v: "eval f ?xs ↓= v" by auto
then obtain t where t:
"∀t'≥t. eval r_result [t', i, x] ↓= Suc v"
"∀t'<t. eval r_result [t', i, x] ↓= 0"
using r_result_converg[OF assms] by blast
then have
"∀t'≥t. eval ?cond [t', i, x] ↓= 0"
"∀t'<t. eval ?cond [t', i, x] ↓= 1"
using * by simp_all
then have "eval ?while [i, x] ↓= t"
using eval_Mn_convergI[of 2 ?cond "[i, x]" t] by simp
then have "eval ?res [i, x] = eval r_result [t, i, x]"
by simp
then have "eval ?res [i, x] ↓= Suc v"
using t(1) by simp
then show ?thesis
unfolding r_univ_def using v by simp
qed
qed

theorem r_univ':
assumes "recfn (e_length x) f"
shows "eval r_univ [encode f, x] = eval f (list_decode x)"
using r_univ assms by simp

text ‹Universal functions for every arity can be built from @{term "r_univ"}.›

definition r_universal :: "nat ⇒ recf" where
"r_universal n ≡ Cn (Suc n) r_univ [Id (Suc n) 0, r_shift (r_list_encode (n - 1))]"

lemma r_universal_recfn [simp]: "n > 0 ⟹ recfn (Suc n) (r_universal n)"
unfolding r_universal_def by simp

lemma r_universal:
assumes "recfn n f" and "length xs = n"
shows "eval (r_universal n) (encode f # xs) = eval f xs"
unfolding r_universal_def using wellf_arity_nonzero assms r_list_encode r_univ'
by fastforce

text ‹We will mostly be concerned with computing unary functions. Hence
we introduce separate functions for this case.›

definition "r_result1 ≡
Cn 3 r_result [Id 3 0, Id 3 1, Cn 3 r_singleton_encode [Id 3 2]]"

lemma r_result1_prim [simp]: "prim_recfn 3 r_result1"
unfolding r_result1_def by simp

lemma r_result1_total: "total r_result1"
using Mn_free_imp_total by simp

lemma r_result1 [simp]:
"eval r_result1 [t, i, x] = eval r_result [t, i, singleton_encode x]"
unfolding r_result1_def by simp

text ‹The following function will be our standard Gödel numbering
of all unary partial recursive functions.›

definition "r_phi ≡ r_universal 1"

lemma r_phi_recfn [simp]: "recfn 2 r_phi"
unfolding r_phi_def by simp

theorem r_phi:
assumes "i = encode f" and "recfn 1 f"
shows "eval r_phi [i, x] = eval f [x]"
unfolding r_phi_def using r_universal assms by force

corollary r_phi':
assumes "recfn 1 f"
shows "eval r_phi [encode f, x] = eval f [x]"
using assms r_phi by simp

lemma r_phi'': "eval r_phi [i, x] = eval r_univ [i, singleton_encode x]"
unfolding r_universal_def r_phi_def using r_list_encode by simp

section ‹Applications of the universal function›

text ‹In this section we shall see some ways @{term r_univ} and @{term r_result} can
be used.›

subsection ‹Lazy conditional evaluation›

text ‹With the help of @{term r_univ} we can now define a
\hypertarget{p:r_lifz}{lazy variant} of @{term r_ifz}, in which only one
branch is evaluated.›

definition r_lazyifzero :: "nat ⇒ nat ⇒ nat ⇒ recf" where
"r_lazyifzero n j⇩1 j⇩2 ≡
Cn (Suc (Suc n)) r_univ
[Cn (Suc (Suc n)) r_ifz [Id (Suc (Suc n)) 0, r_constn (Suc n) j⇩1, r_constn (Suc n) j⇩2],
r_shift (r_list_encode n)]"

lemma r_lazyifzero_recfn: "recfn (Suc (Suc n)) (r_lazyifzero n j⇩1 j⇩2)"
using r_lazyifzero_def by simp

lemma r_lazyifzero:
assumes "length xs = Suc n"
and "j⇩1 = encode f⇩1"
and "j⇩2 = encode f⇩2"
and "recfn (Suc n) f⇩1"
and "recfn (Suc n) f⇩2"
shows "eval (r_lazyifzero