# 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, [0]) # 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 ‹k < length gs›
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, [0]) # 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, opaque_lifting) 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