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 t1 where t1: "iterate t1 step x = y"
    using reachable_def by auto
  have "fst (iterate t step x)  []" for t
  proof (cases "t  t1")
    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 (t1 + (t - t1)) step x"
      by simp
    then have "iterate t step x = iterate (t - t1) step (iterate t1 step x)"
      by (simp add: iterate_additive')
    then have "iterate t step x = iterate (t - t1) 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  sset 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) "gset gs. eval g xs " and "eval f ?ys "
    | (diverg_gs) "gset 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)")
      by (simp add: step_reachable)
    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)")
      by (simp add: reachable_refl)
    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"
    by (simp add: reachable_def)
  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''
      using v iterate_additive by fast
    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: "z0. z>z0. ¬ (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 z0 where "z>z0. ¬ (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 z0)"
        by simp
      have "t't. fst (iterate t' step (?stack, None)) = []"
        using t iterate_step_empty_stack iterate_additive'[of t]
        by (metis le_Suc_ex prod.exhaust_sel)
      then have "t't. iterate t' step (?stack, None)  h (Suc z0)"
        using z_neq_Nil by auto
      then have "t'. iterate t' step (?stack, None)  h (Suc z0)"
        using not_h nat_le_linear by auto
      then have "¬ reachable (?stack, None) (h (Suc z0))"
        using reachable_def by simp
      then show False
        using reach_z[of "Suc z0"] 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)"
  using encode_frame by (simp add: assms estep_Cn_def, simp add: encode_config assms)

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)"
    by (simp add: assms encode_frame)
  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
  by (simp add: assms estep_Pr_def, simp add: encode_config assms)

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
      using assms encode_frame by (simp add: estep_Mn_def, simp add: encode_config)
  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)"
  using encode_frame by (simp add: assms estep_def, simp add: encode_config assms)

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