(*<*)
theory Paper
imports "../thys/recursive"
begin


hide_const (open) s 



hide_const (open) Divides.adjust

abbreviation
  "update2 p a \<equiv> update a p"

consts DUMMY::'a


(* THEOREMS *)
notation (Rule output)
  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")

syntax (Rule output)
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")

  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")

  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")

notation (Axiom output)
  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")

notation (IfThen output)
  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
syntax (IfThen output)
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")

notation (IfThenNoBox output)
  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
syntax (IfThenNoBox output)
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
  "_asm" :: "prop \<Rightarrow> asms" ("_")


context uncomputable
begin

notation (latex output)
  Cons ("_::_" [48,47] 48) and
  set ("") and
  W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and
  W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
  update2 ("update") and
  tm_wf0 ("wf") and
  (*is_even ("iseven") and*)
  tcopy_begin ("cbegin") and
  tcopy_loop ("cloop") and
  tcopy_end ("cend") and
  step0 ("step") and
  tcontra ("contra") and
  code_tcontra ("code contra") and
  steps0 ("steps") and
  exponent ("_\<^bsup>_\<^esup>") and
  haltP ("halts") and 
  tcopy ("copy") and 
  tape_of ("\<langle>_\<rangle>") and 
  tm_comp ("_ \<oplus> _") and 
  DUMMY  ("\<^raw:\mbox{$\_\!\_\,$}>") and
  inv_begin0 ("I\<^isub>0") and
  inv_begin1 ("I\<^isub>1") and
  inv_begin2 ("I\<^isub>2") and
  inv_begin3 ("I\<^isub>3") and
  inv_begin4 ("I\<^isub>4") and 
  inv_begin ("I\<^bsub>cbegin\<^esub>") and
  inv_loop1 ("J\<^isub>1") and
  inv_loop0 ("J\<^isub>0") and
  inv_end1 ("K\<^isub>1") and
  inv_end0 ("K\<^isub>0") and
  measure_begin_step ("M\<^bsub>cbegin\<^esub>") and
  layout_of ("layout") and
  findnth ("find'_nth") and
  recf.id ("id\<^raw:\makebox[0mm]{\,\,\,\,>\<^isup>_\<^raw:}>\<^isub>_") and
  Pr ("Pr\<^isup>_") and
  Cn ("Cn\<^isup>_") and
  Mn ("Mn\<^isup>_") and
  rec_calc_rel ("eval") and 
  tm_of_rec ("translate")

 
lemma inv_begin_print:
  shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and
        "s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and 
        "s = 2 \<Longrightarrow> inv_begin n (s, tp) = inv_begin2 n tp" and 
        "s = 3 \<Longrightarrow> inv_begin n (s, tp) = inv_begin3 n tp" and 
        "s = 4 \<Longrightarrow> inv_begin n (s, tp) = inv_begin4 n tp" and
        "s \<notin> {0,1,2,3,4} \<Longrightarrow> inv_begin n (s, l, r) = False"
apply(case_tac [!] tp)
by (auto)

lemma inv1: 
  shows "0 < n \<Longrightarrow> inv_begin0 n \<mapsto> inv_loop1 n"
unfolding assert_imp_def
unfolding inv_loop1.simps inv_begin0.simps
apply(auto)
apply(rule_tac x="1" in exI)
apply(auto simp add: replicate.simps)
done

lemma inv2: 
  shows "0 < n \<Longrightarrow> inv_loop0 n = inv_end1 n"
apply(rule ext)
apply(case_tac x)
apply(simp add: inv_end1.simps)
done


lemma measure_begin_print:
  shows "s = 2 \<Longrightarrow> measure_begin_step (s, l, r) = length r" and
        "s = 3 \<Longrightarrow> measure_begin_step (s, l, r) = (if r = [] \<or> r = [Bk] then 1 else 0)" and
        "s = 4 \<Longrightarrow> measure_begin_step (s, l, r) = length l" and 
        "s \<notin> {2,3,4} \<Longrightarrow> measure_begin_step (s, l, r) = 0"
by (simp_all)

declare [[show_question_marks = false]]

lemma nats2tape:
  shows "<([]::nat list)> = []"
  and "<[n]> = <n>"
  and "ns \<noteq> [] \<Longrightarrow> <n#ns> = <(n::nat, ns)>"
  and "<(n, m)> = <n> @ [Bk] @ <m>"
  and "<[n, m]> = <(n, m)>"
  and "<n> = Oc \<up> (n + 1)" 
apply(auto simp add: tape_of_nat_pair tape_of_nl_abv tape_of_nat_abv tape_of_nat_list.simps)
apply(case_tac ns)
apply(auto simp add: tape_of_nat_pair tape_of_nat_abv)
done 

lemmas HR1 = 
  Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^isub>1" and B="p\<^isub>2"]

lemmas HR2 =
  Hoare_plus_unhalt[where ?A="p\<^isub>1" and B="p\<^isub>2"]

lemma inv_begin01:
  assumes "n > 1"
  shows "inv_begin0 n (l, r) = (n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc]))"
using assms by auto                          

lemma inv_begin02:
  assumes "n = 1"
  shows "inv_begin0 n (l, r) = (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc]))"
using assms by auto


lemma layout:
  shows "layout_of [] = []"
  and   "layout_of ((Inc R\<iota>)#is) = (2 * R\<iota> + 9)#(layout_of is)"
  and   "layout_of ((Dec R\<iota> l)#is) = (2 * R\<iota> + 16)#(layout_of is)"
  and   "layout_of ((Goto l)#is) = 1#(layout_of is)"
by(auto simp add: layout_of.simps length_of.simps)


(*>*)

section {* Introduction *}



text {*

%\noindent
%We formalised in earlier work the correctness proofs for two
%algorithms in Isabelle/HOL---one about type-checking in
%LF~\cite{UrbanCheneyBerghofer11} and another about deciding requests
%in access control~\cite{WuZhangUrban12}.  The formalisations
%uncovered a gap in the informal correctness proof of the former and
%made us realise that important details were left out in the informal
%model for the latter. However, in both cases we were unable to
%formalise in Isabelle/HOL computability arguments about the
%algorithms. 


\noindent
Suppose you want to mechanise a proof for whether a predicate @{term
P}, say, is decidable or not. Decidability of @{text P} usually
amounts to showing whether \mbox{@{term "P \<or> \<not>P"}} holds. But this
does \emph{not} work in Isabelle/HOL and other HOL theorem provers,
since they are based on classical logic where the law of excluded
middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always provable no
matter whether @{text P} is constructed by computable means. We hit on
this limitation previously when we mechanised the correctness proofs
of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, but
were unable to formalise arguments about decidability or undecidability.

%The same problem would arise if we had formulated
%the algorithms as recursive functions, because internally in
%Isabelle/HOL, like in all HOL-based theorem provers, functions are
%represented as inductively defined predicates too.

The only satisfying way out of this problem in a theorem prover based
on classical logic is to formalise a theory of computability. Norrish
provided such a formalisation for HOL4. He choose the
$\lambda$-calculus as the starting point for his formalisation because
of its ``simplicity'' \cite[Page 297]{Norrish11}.  Part of his
formalisation is a clever infrastructure for reducing
$\lambda$-terms. He also established the computational equivalence
between the $\lambda$-calculus and recursive functions.  Nevertheless
he concluded that it would be appealing to have formalisations for
more operational models of computations, such as Turing machines or
register machines.  One reason is that many proofs in the literature
use them.  He noted however that \cite[Page 310]{Norrish11}:

\begin{quote}
\it``If register machines are unappealing because of their 
general fiddliness,\\ Turing machines are an even more 
daunting prospect.''
\end{quote}

\noindent
In this paper we take on this daunting prospect and provide a
formalisation of Turing machines, as well as abacus machines (a kind
of register machines) and recursive functions. To see the difficulties
involved with this work, one has to understand that Turing machine
programs can be completely \emph{unstructured}, behaving similar to
Basic programs containing the infamous gotos \cite{Dijkstra68}. This
precludes in the general case a compositional Hoare-style reasoning
about Turing programs.  We provide such Hoare-rules for when it
\emph{is} possible to reason in a compositional manner (which is
fortunately quite often), but also tackle the more complicated case
when we translate abacus programs into Turing programs.  This
reasoning about concrete Turing machine programs is usually
left out in the informal literature, e.g.~\cite{Boolos87}.

%To see the difficulties
%involved with this work, one has to understand that interactive
%theorem provers, like Isabelle/HOL, are at their best when the
%data-structures at hand are ``structurally'' defined, like lists,
%natural numbers, regular expressions, etc. Such data-structures come
%with convenient reasoning infrastructures (for example induction
%principles, recursion combinators and so on).  But this is \emph{not}
%the case with Turing machines (and also not with register machines):
%underlying their definitions are sets of states together with 
%transition functions, all of which are not structurally defined.  This
%means we have to implement our own reasoning infrastructure in order
%to prove properties about them. This leads to annoyingly fiddly
%formalisations.  We noticed first the difference between both,
%structural and non-structural, ``worlds'' when formalising the
%Myhill-Nerode theorem, where regular expressions fared much better
%than automata \cite{WuZhangUrban11}.  However, with Turing machines
%there seems to be no alternative if one wants to formalise the great
%many proofs from the literature that use them.  We will analyse one
%example---undecidability of Wang's tiling problem---in Section~\ref{Wang}. The
%standard proof of this property uses the notion of universal
%Turing machines.

We are not the first who formalised Turing machines: we are aware of
the work by Asperti and Ricciotti \cite{AspertiRicciotti12}. They
describe a complete formalisation of Turing machines in the Matita
theorem prover, including a universal Turing machine. However, they do
\emph{not} formalise the undecidability of the halting problem since
their main focus is complexity, rather than computability theory. They
also report that the informal proofs from which they started are not
``sufficiently accurate to be directly usable as a guideline for
formalization'' \cite[Page 2]{AspertiRicciotti12}. For our
formalisation we follow mainly the proofs from the textbook by Boolos
et al \cite{Boolos87} and found that the description there is quite
detailed. Some details are left out however: for example, constructing
the \emph{copy Turing machine} is left as an exercise to the
reader---a corresponding correctness proof is not mentioned at all; also \cite{Boolos87}
only shows how the universal Turing machine is constructed for Turing
machines computing unary functions. We had to figure out a way to
generalise this result to $n$-ary functions. Similarly, when compiling
recursive functions to abacus machines, the textbook again only shows
how it can be done for 2- and 3-ary functions, but in the
formalisation we need arbitrary functions. But the general ideas for
how to do this are clear enough in \cite{Boolos87}.
%However, one
%aspect that is completely left out from the informal description in
%\cite{Boolos87}, and similar ones we are aware of, is arguments why certain Turing
%machines are correct. We will introduce Hoare-style proof rules
%which help us with such correctness arguments of Turing machines.

The main difference between our formalisation and the one by Asperti
and Ricciotti is that their universal Turing machine uses a different
alphabet than the machines it simulates. They write \cite[Page
23]{AspertiRicciotti12}:

\begin{quote}\it
``In particular, the fact that the universal machine operates with a
different alphabet with respect to the machines it simulates is
annoying.'' 
\end{quote}

\noindent
In this paper we follow the approach by Boolos et al \cite{Boolos87},
which goes back to Post \cite{Post36}, where all Turing machines
operate on tapes that contain only \emph{blank} or \emph{occupied} cells. 
Traditionally the content of a cell can be any
character from a finite alphabet. Although computationally equivalent,
the more restrictive notion of Turing machines in \cite{Boolos87} makes
the reasoning more uniform. In addition some proofs \emph{about} Turing
machines are simpler.  The reason is that one often needs to encode
Turing machines---consequently if the Turing machines are simpler, then the coding
functions are simpler too. Unfortunately, the restrictiveness also makes
it harder to design programs for these Turing machines. In order
to construct a universal Turing machine we therefore do not follow 
\cite{AspertiRicciotti12}, instead follow the proof in
\cite{Boolos87} by translating abacus machines to Turing machines and in
turn recursive functions to abacus machines. The universal Turing
machine can then be constructed as a recursive function.

\smallskip
\noindent
{\bf Contributions:} We formalised in Isabelle/HOL Turing machines following the
description of Boolos et al \cite{Boolos87} where tapes only have blank or
occupied cells. We mechanise the undecidability of the halting problem and
prove the correctness of concrete Turing machines that are needed
in this proof; such correctness proofs are left out in the informal literature.  
For reasoning about Turing machine programs we derive Hoare-rules.
We also construct the universal Turing machine from \cite{Boolos87} by
translating recursive functions to abacus machines and abacus machines to
Turing machines. Since we have set up in Isabelle/HOL a very general computability
model and undecidability result, we are able to formalise other
results: we describe a proof of the computational equivalence
of single-sided Turing machines, which is not given in \cite{Boolos87},
but needed for example for formalising the undecidability proof of 
Wang's tiling problem \cite{Robinson71}.
%We are not aware of any other
%formalisation of a substantial undecidability problem.
*}

section {* Turing Machines *}

text {* \noindent
  Turing machines can be thought of as having a \emph{head},
  ``gliding'' over a potentially infinite tape. Boolos et
  al~\cite{Boolos87} only consider tapes with cells being either blank
  or occupied, which we represent by a datatype having two
  constructors, namely @{text Bk} and @{text Oc}.  One way to
  represent such tapes is to use a pair of lists, written @{term "(l,
  r)"}, where @{term l} stands for the tape on the left-hand side of
  the head and @{term r} for the tape on the right-hand side.  We use
  the notation @{term "Bk \<up> n"} (similarly @{term "Oc \<up> n"}) for lists
  composed of @{term n} elements of @{term Bk}s.  We also have the
  convention that the head, abbreviated @{term hd}, of the right list
  is the cell on which the head of the Turing machine currently
  scans. This can be pictured as follows:
  %
  \begin{center}
  \begin{tikzpicture}[scale=0.9]
  \draw[very thick] (-3.0,0)   -- ( 3.0,0);
  \draw[very thick] (-3.0,0.5) -- ( 3.0,0.5);
  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);
  \draw[very thick] (-0.75,0)   -- (-0.75,0.5);
  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);
  \draw[very thick] (-1.25,0)   -- (-1.25,0.5);
  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);
  \draw[very thick] (-1.75,0)   -- (-1.75,0.5);
  \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);
  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
  \draw[fill]     (1.35,0.1) rectangle (1.65,0.4);
  \draw[fill]     (0.85,0.1) rectangle (1.15,0.4);
  \draw[fill]     (-0.35,0.1) rectangle (-0.65,0.4);
  \draw[fill]     (-1.65,0.1) rectangle (-1.35,0.4);
  \draw (-0.25,0.8) -- (-0.25,-0.8);
  \draw[<->] (-1.25,-0.7) -- (0.75,-0.7);
  \node [anchor=base] at (-0.85,-0.5) {\small left list};
  \node [anchor=base] at (0.40,-0.5) {\small right list};
  \node [anchor=base] at (0.1,0.7) {\small head};
  \node [anchor=base] at (-2.2,0.2) {\ldots};
  \node [anchor=base] at ( 2.3,0.2) {\ldots};
  \end{tikzpicture}
  \end{center}
  
  \noindent
  Note that by using lists each side of the tape is only finite. The
  potential infinity is achieved by adding an appropriate blank or occupied cell 
  whenever the head goes over the ``edge'' of the tape. To 
  make this formal we define five possible \emph{actions} 
  the Turing machine can perform:

  \begin{center}
  \begin{tabular}[t]{@ {}rcl@ {\hspace{2mm}}l}
  @{text "a"} & $::=$  & @{term "W0"} & (write blank, @{term Bk})\\
  & $\mid$ & @{term "W1"} & (write occupied, @{term Oc})\\
  \end{tabular}
  \begin{tabular}[t]{rcl@ {\hspace{2mm}}l}
  & $\mid$ & @{term L} & (move left)\\
  & $\mid$ & @{term R} & (move right)\\
  \end{tabular}
  \begin{tabular}[t]{rcl@ {\hspace{2mm}}l@ {}}
  & $\mid$ & @{term Nop} & (do-nothing operation)\\
  \end{tabular}
  \end{center}

  \noindent
  We slightly deviate
  from the presentation in \cite{Boolos87} (and also \cite{AspertiRicciotti12}) 
  by using the @{term Nop} operation; however its use
  will become important when we formalise halting computations and also universal Turing 
  machines.  Given a tape and an action, we can define the
  following tape updating function:

  \begin{center}
  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
  @{thm (lhs) update.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(1)}\\
  @{thm (lhs) update.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(2)}\\
  @{thm (lhs) update.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(3)}\\
  @{thm (lhs) update.simps(4)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(4)}\\
  @{thm (lhs) update.simps(5)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(5)}\\
  \end{tabular}
  \end{center}

  \noindent
  The first two clauses replace the head of the right list
  with a new @{term Bk} or @{term Oc}, respectively. To see that
  these two clauses make sense in case where @{text r} is the empty
  list, one has to know that the tail function, @{term tl}, is defined
  such that @{term "tl [] == []"} holds. The third clause 
  implements the move of the head one step to the left: we need
  to test if the left-list @{term l} is empty; if yes, then we just prepend a 
  blank cell to the right list; otherwise we have to remove the
  head from the left-list and prepend it to the right list. Similarly
  in the fourth clause for a right move action. The @{term Nop} operation
  leaves the the tape unchanged.

  %Note that our treatment of the tape is rather ``unsymmetric''---we
  %have the convention that the head of the right list is where the
  %head is currently positioned. Asperti and Ricciotti
  %\cite{AspertiRicciotti12} also considered such a representation, but
  %dismiss it as it complicates their definition for \emph{tape
  %equality}. The reason is that moving the head one step to
  %the left and then back to the right might change the tape (in case
  %of going over the ``edge''). Therefore they distinguish four types
  %of tapes: one where the tape is empty; another where the head
  %is on the left edge, respectively right edge, and in the middle
  %of the tape. The reading, writing and moving of the tape is then
  %defined in terms of these four cases.  In this way they can keep the
  %tape in a ``normalised'' form, and thus making a left-move followed
  %by a right-move being the identity on tapes. Since we are not using
  %the notion of tape equality, we can get away with the unsymmetric
  %definition above, and by using the @{term update} function
  %cover uniformly all cases including corner cases.

  Next we need to define the \emph{states} of a Turing machine.  
  %Given
  %how little is usually said about how to represent them in informal
  %presentations, it might be surprising that in a theorem prover we
  %have to select carefully a representation. If we use the naive
  %representation where a Turing machine consists of a finite set of
  %states, then we will have difficulties composing two Turing
  %machines: we would need to combine two finite sets of states,
  %possibly renaming states apart whenever both machines share
  %states.\footnote{The usual disjoint union operation in Isabelle/HOL
  %cannot be used as it does not preserve types.} This renaming can be
  %quite cumbersome to reason about. 
  We follow the choice made in \cite{AspertiRicciotti12} 
  by representing a state with a natural number and the states in a Turing
  machine program by the initial segment of natural numbers starting from @{text 0}.
  In doing so we can compose two Turing machine programs by
  shifting the states of one by an appropriate amount to a higher
  segment and adjusting some ``next states'' in the other. 

  An \emph{instruction} of a Turing machine is a pair consisting of 
  an action and a natural number (the next state). A \emph{program} @{term p} of a Turing
  machine is then a list of such pairs. Using as an example the following Turing machine
  program, which consists of four instructions
  %
  \begin{equation}
  \begin{tikzpicture}
  \node [anchor=base] at (0,0) {@{thm dither_def}};
  \node [anchor=west] at (-1.5,-0.64) 
  {$\underbrace{\hspace{21mm}}_{\text{\begin{tabular}{@ {}l@ {}}1st state\\[-2mm] 
  = starting state\end{tabular}}}$};
  
  \node [anchor=west] at ( 1.1,-0.42) {$\underbrace{\hspace{17mm}}_{\text{2nd state}}$};
  \node [anchor=west] at (-1.5,0.65) {$\overbrace{\hspace{10mm}}^{\text{@{term Bk}-case}}$};
  \node [anchor=west] at (-0.1,0.65) {$\overbrace{\hspace{6mm}}^{\text{@{term Oc}-case}}$};
  \end{tikzpicture}
  \label{dither}
  \end{equation}
  %
  \noindent
  the reader can see we have organised our Turing machine programs so
  that segments of two pairs belong to a state. The first component of such a
  segment determines what action should be taken and which next state
  should be transitioned to in case the head reads a @{term Bk};
  similarly the second component determines what should be done in
  case of reading @{term Oc}. We have the convention that the first
  state is always the \emph{starting state} of the Turing machine.
  The @{text 0}-state is special in that it will be used as the
  ``halting state''.  There are no instructions for the @{text
  0}-state, but it will always perform a @{term Nop}-operation and
  remain in the @{text 0}-state.  Unlike Asperti and Riccioti
  \cite{AspertiRicciotti12}, we have chosen a very concrete
  representation for programs, because when constructing a universal
  Turing machine, we need to define a coding function for programs.
  This can be directly done for our programs-as-lists, but is
  slightly more difficult for the functions used by Asperti and Ricciotti.

  Given a program @{term p}, a state
  and the cell being read by the head, we need to fetch
  the corresponding instruction from the program. For this we define 
  the function @{term fetch}
 
  \begin{equation}\label{fetch}
  \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
  \multicolumn{3}{l}{@{thm fetch.simps(1)[where b=DUMMY]}}\\
  @{thm (lhs) fetch.simps(2)} & @{text "\<equiv>"} & @{text "case nth_of p (2 * s) of"}\\
  \multicolumn{3}{@ {\hspace{4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}\\
  @{thm (lhs) fetch.simps(3)} & @{text "\<equiv>"} & @{text "case nth_of p (2 * s + 1) of"}\\
  \multicolumn{3}{@ {\hspace{4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}
  \end{tabular}}
  \end{equation}

  \noindent
  In this definition the function @{term nth_of} returns the @{text n}th element
  from a list, provided it exists (@{term Some}-case), or if it does not, it
  returns the default action @{term Nop} and the default state @{text 0} 
  (@{term None}-case). We often have to restrict Turing machine programs 
  to be well-formed: a program @{term p} is \emph{well-formed} if it 
  satisfies the following three properties:

  \begin{center}
  @{thm tm_wf.simps[where p="p" and off="0::nat", simplified, THEN eq_reflection]}
  \end{center}

  \noindent
  The first states that @{text p} must have at least an instruction for the starting 
  state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every 
  state, and the third that every next-state is one of the states mentioned in
  the program or being the @{text 0}-state.

  We need to be able to sequentially compose Turing machine programs. Given our
  concrete representation, this is relatively straightforward, if
  slightly fiddly. We use the following two auxiliary functions:

  \begin{center}
  \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
  @{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\
  @{thm (lhs) adjust.simps} @{text "\<equiv>"} @{thm (rhs) adjust.simps}\\
  \end{tabular}
  \end{center}

  \noindent
  The first adds @{text n} to all states, except the @{text 0}-state,
  thus moving all ``regular'' states to the segment starting at @{text
  n}; the second adds @{term "Suc(length p div 2)"} to the @{text
  0}-state, thus redirecting all references to the ``halting state''
  to the first state after the program @{text p}.  With these two
  functions in place, we can define the \emph{sequential composition}
  of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"} as

  \begin{center}
  @{thm tm_comp.simps[where ?p1.0="p\<^isub>1" and ?p2.0="p\<^isub>2", THEN eq_reflection]}
  \end{center}

  \noindent
  %This means @{text "p\<^isub>1"} is executed first. Whenever it originally
  %transitioned to the @{text 0}-state, it will in the composed program transition to the starting
  %state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"}
  %have been shifted in order to make sure that the states of the composed 
  %program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy'' 
  %an initial segment of the natural numbers.

  A \emph{configuration} @{term c} of a Turing machine is a state
  together with a tape. This is written as @{text "(s, (l, r))"}.  We
  say a configuration \emph{is final} if @{term "s = (0::nat)"} and we
  say a predicate @{text P} \emph{holds for} a configuration if @{text
  "P"} holds for the tape @{text "(l, r)"}.  If we have a configuration and a program, we can
  calculate what the next configuration is by fetching the appropriate
  action and next state from the program, and by updating the state
  and tape accordingly.  This single step of execution is defined as
  the function @{term step}

  \begin{center}
  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
  @{text "step (s, (l, r)) p"} & @{text "\<equiv>"} & @{text "let (a, s') = fetch p s (read r)"}\\
  & & @{text "in (s', update (l, r) a)"}
  \end{tabular}
  \end{center}

  \noindent
  where @{term "read r"} returns the head of the list @{text r}, or if
  @{text r} is empty it returns @{term Bk}.  It is impossible in
  Isabelle/HOL to lift the @{term step}-function in order to realise a
  general evaluation function for Turing machines programs. The reason
  is that functions in HOL-based provers need to be terminating, and
  clearly there are programs that are not. We can however define a
  recursive evaluation function that performs exactly @{text n} steps:

  \begin{center}
  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
  @{thm (lhs) steps.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(1)}\\
  @{thm (lhs) steps.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(2)}\\
  \end{tabular}
  \end{center}

  \noindent Recall our definition of @{term fetch} (shown in
  \eqref{fetch}) with the default value for the @{text 0}-state. In
  case a Turing program takes according to the usual textbook
  definition, say \cite{Boolos87}, less than @{text n} steps before it
  halts, then in our setting the @{term steps}-evaluation does not
  actually halt, but rather transitions to the @{text 0}-state (the
  final state) and remains there performing @{text Nop}-actions until
  @{text n} is reached. 
  
  \begin{figure}[t]
  \begin{center}
  \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c}
  \begin{tabular}[t]{@ {}l@ {}}
  @{thm (lhs) tcopy_begin_def} @{text "\<equiv>"}\\
  \hspace{2mm}@{text "["}@{text "(W\<^bsub>Bk\<^esub>, 0), (R, 2), (R, 3),"}\\
  \hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W1, 3), (L, 4),"}\\
  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} 
  \end{tabular}
  &
  \begin{tabular}[t]{@ {}l@ {}}
  @{thm (lhs) tcopy_loop_def} @{text "\<equiv>"}\\
  \hspace{2mm}@{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\
  \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>Bk\<^esub>, 2), (R, 3), (R, 4),"}\\
  \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>Oc\<^esub>, 5), (R, 4), (L, 6),"}\\
  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (L, 6), (L, 1)"}@{text "]"} 
  \end{tabular}
  &
  \begin{tabular}[t]{@ {}l@ {}}
  @{thm (lhs) tcopy_end_def} @{text "\<equiv>"}\\
  \hspace{2mm}@{text "["}@{text "(L, 0), (R, 2), (W\<^bsub>Oc\<^esub>, 3),"}\\
  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (R, 2), (R, 2),"}\\
  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (W\<^bsub>Bk\<^esub>, 4), (R, 0),"}\\
  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5)"}@{text "]"} 
  \end{tabular}
  \end{tabular}\\[2mm]

  \begin{tikzpicture}[scale=0.7]
  \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$};
  \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$};
  \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$};
  \node [anchor=base] at (2.2,-0.6) {\small$\overbrace{@{term "tcopy_begin"}}^{}$};
  \node [anchor=base] at (5.6,-0.6) {\small$\overbrace{@{term "tcopy_loop"}}^{}$};
  \node [anchor=base] at (10.5,-0.6) {\small$\overbrace{@{term "tcopy_end"}}^{}$};


  \begin{scope}[shift={(0.5,0)}]
  \draw[very thick] (-0.25,0)   -- ( 1.25,0);
  \draw[very thick] (-0.25,0.5) -- ( 1.25,0.5);
  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);
  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);
  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);
  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
  \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);
  \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);
  \end{scope}

  \begin{scope}[shift={(2.9,0)}]
  \draw[very thick] (-0.25,0)   -- ( 2.25,0);
  \draw[very thick] (-0.25,0.5) -- ( 2.25,0.5);
  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);
  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);
  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);
  \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);
  \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);
  \draw[rounded corners=1mm] (0.15,-0.1) rectangle (0.85,0.6);
  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
  \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);
  \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);
  \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);
  \end{scope}

  \begin{scope}[shift={(6.8,0)}]
  \draw[very thick] (-0.75,0)   -- ( 3.25,0);
  \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);
  \draw[very thick] (-0.75,0)   -- (-0.75,0.5);
  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);
  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);
  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);
  \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);
  \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);
  \draw[very thick] ( 2.75,0)   -- ( 2.75,0.5);
  \draw[very thick] ( 3.25,0)   -- ( 3.25,0.5);
  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
  \draw[fill]     ( 2.35,0.1) rectangle (2.65,0.4);
  \draw[fill]     ( 2.85,0.1) rectangle (3.15,0.4);
  \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);
  \end{scope}

  \begin{scope}[shift={(11.7,0)}]
  \draw[very thick] (-0.75,0)   -- ( 3.25,0);
  \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);
  \draw[very thick] (-0.75,0)   -- (-0.75,0.5);
  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);
  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);
  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);
  \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);
  \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);
  \draw[very thick] ( 2.75,0)   -- ( 2.75,0.5);
  \draw[very thick] ( 3.25,0)   -- ( 3.25,0.5);
  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
  \draw[fill]     ( 2.35,0.1) rectangle (2.65,0.4);
  \draw[fill]     ( 2.85,0.1) rectangle (3.15,0.4);
  \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);
  \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);
  \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);
  \end{scope}
  \end{tikzpicture}\\[-8mm]\mbox{} 
  \end{center}
  \caption{The three components of the \emph{copy Turing machine} (above). If started 
  (below) with the tape @{term "([], <(2::nat)>)"} the first machine appends @{term "[Bk, Oc]"} at 
  the end of the right tape; the second then ``moves'' all @{term Oc}s except the 
  first from the beginning of the tape to the end; the third ``refills'' the original 
  block of @{term "Oc"}s. The resulting tape is @{term "([Bk], <(2::nat, 2::nat)>)"}.}
  \label{copy}
  \end{figure}


  We often need to restrict tapes to be in standard form, which means 
  the left list of the tape is either empty or only contains @{text "Bk"}s, and 
  the right list contains some ``clusters'' of @{text "Oc"}s separated by single 
  blanks. To make this formal we define the following overloaded function
  encoding natural numbers into lists of @{term "Oc"}s and @{term Bk}s.
  % 
  \begin{equation}
  \mbox{\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
  @{thm (lhs) nats2tape(6)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(6)}\\
  @{thm (lhs) nats2tape(4)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(4)}\\
  \end{tabular}\hspace{6mm}
  \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
  @{thm (lhs) nats2tape(1)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(1)}\\
  @{thm (lhs) nats2tape(2)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(2)}\\
  @{thm (lhs) nats2tape(3)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(3)}
  \end{tabular}}\label{standard}
  \end{equation}
  %
  \noindent
  A \emph{standard tape} is then of the form @{text "(Bk\<^isup>l,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle>)"} for some @{text l} 
  and @{text "n\<^bsub>1...m\<^esub>"}. Note that the head in a standard tape ``points'' to the 
  leftmost @{term "Oc"} on the tape. Note also that the natural number @{text 0} 
  is represented by a single filled cell on a standard tape, @{text 1} by two filled cells and so on.

  Before we can prove the undecidability of the halting problem for
  our Turing machines working on standard tapes, we have to analyse
  two concrete Turing machine programs and establish that they are
  correct---that means they are ``doing what they are supposed to be
  doing''.  Such correctness proofs are usually left out in the
  informal literature, for example \cite{Boolos87}.  The first program
  we need to prove correct is the @{term dither} program shown in
  \eqref{dither} and the second program is @{term "tcopy"} defined as

  \begin{equation}
  \mbox{\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
  @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def}
  \end{tabular}}\label{tcopy}
  \end{equation}

  \noindent
  whose three components are given in Figure~\ref{copy}. For our
  correctness proofs, we introduce the notion of total correctness
  defined in terms of \emph{Hoare-triples}, written @{term "{P} p
  {Q}"}.  They implement the idea that a program @{term
  p} started in state @{term "1::nat"} with a tape satisfying @{term
  P} will after some @{text n} steps halt (have transitioned into the
  halting state) with a tape satisfying @{term Q}. This idea is very
  similar to the notion of \emph{realisability} in \cite{AspertiRicciotti12}. We
  also have \emph{Hoare-pairs} of the form @{term "{P} p \<up>"}
  implementing the case that a program @{term p} started with a tape
  satisfying @{term P} will loop (never transition into the halting
  state). Both notion are formally defined as

  \begin{center}
  \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
  \begin{tabular}[t]{@ {}l@ {}}
  \colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\<equiv>"}\\[1mm]
  \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\
  \hspace{7mm}if @{term "P (l, r)"} holds then\\
  \hspace{7mm}@{text "\<exists>"} @{term n}. such that\\
  \hspace{7mm}@{text "is_final (steps (1, (l, r)) p n)"} \hspace{1mm}@{text "\<and>"}\\
  \hspace{7mm}@{text "Q holds_for (steps (1, (l, r)) p n)"}
  \end{tabular} &
  \begin{tabular}[t]{@ {}l@ {}}
  \colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm]
  \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\ 
  \hspace{7mm}if @{term "P (l, r)"} holds then\\
  \hspace{7mm}@{text "\<forall>"} @{term n}. @{text "\<not> is_final (steps (1, (l, r)) p n)"}
  \end{tabular}
  \end{tabular}
  \end{center}
  
  \noindent
  For our Hoare-triples we can easily prove the following Hoare-consequence rule

  \begin{equation}
  @{thm[mode=Rule] Hoare_consequence}
  \end{equation}

  \noindent
  where
  @{term "P' \<mapsto> P"} stands for the fact that for all tapes @{term "tp"},
  @{term "P' tp"} implies @{term "P tp"} (similarly for @{text "Q"} and @{text "Q'"}).

  Like Asperti and Ricciotti with their notion of realisability, we
  have set up our Hoare-rules so that we can deal explicitly
  with total correctness and non-termination, rather than have
  notions for partial correctness and termination. Although the latter
  would allow us to reason more uniformly (only using Hoare-triples),
  we prefer our definitions because we can derive below some simple
  Hoare-rules for sequentially composed Turing programs.  In this way
  we can reason about the correctness of @{term "tcopy_begin"}, for
  example, completely separately from @{term "tcopy_loop"} and @{term
  "tcopy_end"}.

  It is relatively straightforward to prove that the Turing program 
  @{term "dither"} shown in \eqref{dither} is correct. This program
  should be the ``identity'' when started with a standard tape representing 
  @{text "1"} but loops when started with the @{text 0}-representation instead, as pictured 
  below.


  \begin{center}
  \begin{tabular}{l@ {\hspace{3mm}}lcl}
  & \multicolumn{1}{c}{start tape}\\[1mm]
  \raisebox{2mm}{halting case:} &
  \begin{tikzpicture}[scale=0.8]
  \draw[very thick] (-2,0)   -- ( 0.75,0);
  \draw[very thick] (-2,0.5) -- ( 0.75,0.5);
  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);
  \draw[very thick] (-0.75,0)   -- (-0.75,0.5);
  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);
  \draw[very thick] (-1.25,0)   -- (-1.25,0.5);
  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
  \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);
  \node [anchor=base] at (-1.7,0.2) {\ldots};
  \end{tikzpicture} 
  & \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} &
  \begin{tikzpicture}[scale=0.8]
  \draw[very thick] (-2,0)   -- ( 0.75,0);
  \draw[very thick] (-2,0.5) -- ( 0.75,0.5);
  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);
  \draw[very thick] (-0.75,0)   -- (-0.75,0.5);
  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);
  \draw[very thick] (-1.25,0)   -- (-1.25,0.5);
  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
  \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);
  \node [anchor=base] at (-1.7,0.2) {\ldots};
  \end{tikzpicture}\\

  \raisebox{2mm}{non-halting case:} &
  \begin{tikzpicture}[scale=0.8]
  \draw[very thick] (-2,0)   -- ( 0.25,0);
  \draw[very thick] (-2,0.5) -- ( 0.25,0.5);
  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);
  \draw[very thick] (-0.75,0)   -- (-0.75,0.5);
  \draw[very thick] (-1.25,0)   -- (-1.25,0.5);
  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
  \node [anchor=base] at (-1.7,0.2) {\ldots};
  \end{tikzpicture} 
  & \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} &
  \raisebox{2mm}{loops}
  \end{tabular}
  \end{center}

  \noindent
  We can prove the following Hoare-statements:
 
  \begin{center}
  \begin{tabular}{l}
  @{thm dither_halts}\\
  @{thm dither_loops}
  \end{tabular}
  \end{center}

  \noindent
  The first is by a simple calculation. The second is by an induction on the
  number of steps we can perform starting from the input tape.

  The program @{term tcopy} defined in \eqref{tcopy} has 15 states;
  its purpose is to produce the standard tape @{term "(Bks, <(n,
  n::nat)>)"} when started with @{term "(Bks, <(n::nat)>)"}, that is
  making a copy of a value @{term n} on the tape.  Reasoning about this program
  is substantially harder than about @{term dither}. To ease the
  burden, we derive the following two Hoare-rules for sequentially
  composed programs.

  \begin{center}
  \begin{tabular}{@ {\hspace{-10mm}}c@ {\hspace{14mm}}c@ {}}
  $\inferrule*[Right=@{thm (prem 3) HR1}]
  {@{thm (prem 1) HR1} \\ @{thm (prem 2) HR1}}
  {@{thm (concl) HR1}}
  $ &
  $
  \inferrule*[Right=@{thm (prem 3) HR2}]
  {@{thm (prem 1) HR2} \\ @{thm (prem 2) HR2}}
  {@{thm (concl) HR2}}
  $
  \end{tabular}
  \end{center}

  \noindent
  The first corresponds to the usual Hoare-rule for composition of two
  terminating programs. The second rule gives the conditions for when
  the first program terminates generating a tape for which the second
  program loops.  The side-conditions about @{thm (prem 3) HR2} are
  needed in order to ensure that the redirection of the halting and
  initial state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"}, respectively, match
  up correctly.  These Hoare-rules allow us to prove the correctness
  of @{term tcopy} by considering the correctness of the components
  @{term "tcopy_begin"}, @{term "tcopy_loop"} and @{term "tcopy_end"}
  in isolation. This simplifies the reasoning considerably, for
  example when designing decreasing measures for proving the termination
  of the programs.  We will show the details for the program @{term
  "tcopy_begin"}. For the two other programs we refer the reader to
  our formalisation.

  Given the invariants @{term "inv_begin0"},\ldots,
  @{term "inv_begin4"} shown in Figure~\ref{invbegin}, which
  correspond to each state of @{term tcopy_begin}, we define the
  following invariant for the whole @{term tcopy_begin} program:

  \begin{figure}[t]
  \begin{center}
  \begin{tabular}{@ {}lcl@ {\hspace{-0.5cm}}l@ {}}
  \hline
  @{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\
  @{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\
  @{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\
  @{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}\\
  @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
                                &             & @{thm (rhs) inv_begin02}\smallskip \\
   \hline
  @{thm (lhs) inv_loop1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop1_loop.simps} @{text "\<or>"}\\
                               &             & @{thm (rhs) inv_loop1_exit.simps} & (starting state)\\
  @{thm (lhs) inv_loop0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop0.simps}& (halting state)\smallskip\\
   \hline
  @{thm (lhs) inv_end1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end1.simps} & (starting state)\\
  @{thm (lhs) inv_end0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\
  \hline
  \end{tabular}
  \end{center}
  \caption{The invariants @{term inv_begin0},\ldots,@{term inv_begin4} are for the states of 
  @{term tcopy_begin}. Below, the invariants only for the starting and halting states of
  @{term tcopy_loop} and @{term tcopy_end} are shown. In each invariant the parameter 
  @{term n} stands for the number
  of @{term Oc}s with which the Turing machine is started.}\label{invbegin}
  \end{figure}

  \begin{center}
  \begin{tabular}{rcl}
  @{thm (lhs) inv_begin.simps} & @{text "\<equiv>"} & 
  @{text "if"} @{thm (prem 1) inv_begin_print(1)} @{text then} @{thm (rhs) inv_begin_print(1)}\\
  & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(2)} @{text then} @{thm (rhs) inv_begin_print(2)} \\
 & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(3)} @{text then} @{thm (rhs) inv_begin_print(3)}\\
  & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(4)} @{text then} @{thm (rhs) inv_begin_print(4)}\\
   & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(5)} @{text then} @{thm (rhs) inv_begin_print(5)}\\
  & & @{text else} @{thm (rhs) inv_begin_print(6)}
  \end{tabular}
  \end{center}

  \noindent
  This invariant depends on @{term n} representing the number of
  @{term Oc}s@{text "+1"} (or encoded number) on the tape. It is not hard (26
  lines of automated proof script) to show that for @{term "n >
  (0::nat)"} this invariant is preserved under the computation rules
  @{term step} and @{term steps}. This gives us partial correctness
  for @{term "tcopy_begin"}. 

  We next need to show that @{term "tcopy_begin"} terminates. For this
  we introduce lexicographically ordered pairs @{term "(n, m)"}
  derived from configurations @{text "(s, (l, r))"} whereby @{text n} is
  the state @{text s}, but ordered according to how @{term tcopy_begin} executes
  them, that is @{text "1 > 2 > 3 > 4 > 0"}; in order to have
  a strictly decreasing measure, @{term m} takes the data on the tape into
  account and is calculated according to the following measure function:

  \begin{center}
  \begin{tabular}{rcl}
  @{term measure_begin_step}@{text "(s, (l, r))"} & @{text "\<equiv>"} & 
  @{text "if"} @{thm (prem 1) measure_begin_print(1)} @{text then} @{thm (rhs) measure_begin_print(1)}\\
  & & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(2)} @{text then} 
  @{text "("}@{thm (rhs) measure_begin_print(2)}@{text ")"} \\
 & & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(3)} @{text then} @{thm (rhs) measure_begin_print(3)}\\
  & & @{text else} @{thm (rhs) measure_begin_print(4)}\\
  \end{tabular}
  \end{center}
  
  \noindent
  With this in place, we can show that for every starting tape of the
  form @{term "([], Oc \<up> n)"} with @{term "n > (0::nat)"}, the Turing
  machine @{term "tcopy_begin"} will eventually halt (the measure
  decreases in each step). Taking this and the partial correctness
  proof together, we obtain the Hoare-triple shown on the left for @{term tcopy_begin}:
   

  \begin{center}
  @{thm (concl) begin_correct}\hspace{6mm}
  @{thm (concl) loop_correct}\hspace{6mm}
  @{thm (concl) end_correct}
  \end{center}

  \noindent 
  where we assume @{text "0 < n"} (similar reasoning is needed for
  the Hoare-triples for @{term tcopy_loop} and @{term tcopy_end}). Since the invariant of
  the halting state of @{term tcopy_begin} implies the invariant of
  the starting state of @{term tcopy_loop}, that is @{term "inv_begin0
  n \<mapsto> inv_loop1 n"} holds, and also @{term "inv_loop0 n = inv_end1
  n"}, we can derive the following Hoare-triple for the correctness 
  of @{term tcopy}:

  \begin{center}
  @{thm tcopy_correct}
  \end{center}

  \noindent
  That means if we start with a tape of the form @{term "([], <n::nat>)"} then 
  @{term tcopy} will halt with the tape \mbox{@{term "([Bk], <(n::nat, n::nat)>)"}}, as desired.

  Finally, we are in the position to prove the undecidability of the halting problem.
  A program @{term p} started with a standard tape containing the (encoded) numbers
  @{term ns} will \emph{halt} with a standard tape containing a single (encoded) 
  number is defined as

  \begin{center}
  @{thm haltP_def}
  \end{center}

  \noindent
  This roughly means we considering only Turing machine programs
  representing functions that take some numbers as input and produce a
  single number as output. For undecidability, the property we are
  proving is that there is no Turing machine that can decide in
  general whether a Turing machine program halts (answer either @{text
  0} for halting or @{text 1} for looping). Given our correctness
  proofs for @{term dither} and @{term tcopy} shown above, this
  non-existence is now relatively straightforward to establish. We first
  assume there is a coding function, written @{term "code M"}, which
  represents a Turing machine @{term "M"} as a natural number.  No
  further assumptions are made about this coding function. Suppose a
  Turing machine @{term H} exists such that if started with the
  standard tape @{term "([Bk], <(code M, ns)>)"} returns @{text 0},
  respectively @{text 1}, depending on whether @{text M} halts or not when
  started with the input tape containing @{term "<ns>"}.  This
  assumption is formalised as follows---for all @{term M} and all lists of
  natural numbers @{term ns}:

  \begin{center}
  \begin{tabular}{r}
  @{thm (prem 2) uncomputable.h_case} implies
  @{thm (concl) uncomputable.h_case}\\
  
  @{thm (prem 2) uncomputable.nh_case} implies
  @{thm (concl) uncomputable.nh_case}
  \end{tabular}
  \end{center}

  \noindent
  The contradiction can be derived using the following Turing machine

  \begin{center}
  @{thm tcontra_def}
  \end{center}

  \noindent
  Suppose @{thm (prem 1) "tcontra_halt"} holds. Given the invariants @{text "P\<^isub>1"}\ldots@{text "P\<^isub>3"} 
  shown on the 
  left, we can derive the following Hoare-pair for @{term tcontra} on the right.

  \begin{center}\small
  \begin{tabular}{@ {}c@ {\hspace{-10mm}}c@ {}}
  \begin{tabular}[t]{@ {}l@ {}}
  @{term "P\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
  @{term "P\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
  @{term "P\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"}
  \end{tabular}
  &
  \begin{tabular}[b]{@ {}l@ {}}
  \raisebox{-20mm}{$\inferrule*{
    \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {P\<^isub>3}"}}
    {@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}}
    \\ @{term "{P\<^isub>3} dither \<up>"}
   }
   {@{term "{P\<^isub>1} tcontra \<up>"}}
  $}
  \end{tabular}
  \end{tabular}
  \end{center}

  \noindent
  This Hoare-pair contradicts our assumption that @{term tcontra} started
  with @{term "<(code tcontra)>"} halts.

  Suppose @{thm (prem 1) "tcontra_unhalt"} holds. Again, given the invariants 
  @{text "Q\<^isub>1"}\ldots@{text "Q\<^isub>3"}
  shown on the 
  left, we can derive the Hoare-triple for @{term tcontra} on the right.

  \begin{center}\small
  \begin{tabular}{@ {}c@ {\hspace{-18mm}}c@ {}}
  \begin{tabular}[t]{@ {}l@ {}}
  @{term "Q\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
  @{term "Q\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
  @{term "Q\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"}
  \end{tabular}
  &
  \begin{tabular}[t]{@ {}l@ {}}
  \raisebox{-20mm}{$\inferrule*{
    \inferrule*{@{term "{Q\<^isub>1} tcopy {Q\<^isub>2}"} \\ @{term "{Q\<^isub>2} H {Q\<^isub>3}"}}
    {@{term "{Q\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}}
    \\ @{term "{Q\<^isub>3} dither {Q\<^isub>3}"}
   }
   {@{term "{Q\<^isub>1} tcontra {Q\<^isub>3}"}}
  $}
  \end{tabular}
  \end{tabular}
  \end{center}

  \noindent
  This time the Hoare-triple states that @{term tcontra} terminates 
  with the ``output'' @{term "<(1::nat)>"}. In both case we come
  to a contradiction, which means we have to abandon our assumption 
  that there exists a Turing machine @{term H} which can in general decide 
  whether Turing machines terminate.
*}


section {* Abacus Machines *}

text {*
  \noindent
  Boolos et al \cite{Boolos87} use abacus machines as a stepping stone
  for making it less laborious to write Turing machine
  programs. Abacus machines operate over a set of registers @{text "R\<^isub>0"},
  @{text "R\<^isub>1"}, \ldots{}, @{text "R\<^isub>n"} each being able to hold an arbitrary large natural
  number.  We use natural numbers to refer to registers; we also use a natural number
  to represent a program counter and to represent jumping ``addresses'', for which we 
  use the letter @{text l}. An abacus 
  program is a list of \emph{instructions} defined by the datatype:

  \begin{center}
  \begin{tabular}{rcl@ {\hspace{10mm}}l}
  @{text "i"} & $::=$  & @{term "Inc R\<iota>"} & increment register $R$ by one\\
  & $\mid$ & @{term "Dec R\<iota> l"} & if content of $R$ is non-zero, then decrement it by one\\
  & & & otherwise jump to instruction $l$\\
  & $\mid$ & @{term "Goto l"} & jump to instruction $l$
  \end{tabular}
  \end{center}

  \noindent
  For example the program clearing the register @{text R} (that is setting
  it to @{term "(0::nat)"}) can be defined as follows:

  \begin{center}
  @{thm clear.simps[where n="R\<iota>" and e="l", THEN eq_reflection]}
  \end{center}

  \noindent
  Running such a program means we start with the first instruction
  then execute one instructions after the other, unless there is a jump.  For
  example the second instruction @{term "Goto 0"} means
  we jump back to the first instruction thereby closing the loop.  Like with our
  Turing machines, we fetch instructions from an abacus program such
  that a jump out of ``range'' behaves like a @{term "Nop"}-action. In
  this way it is again easy to define a function @{term steps} that
  executes @{term n} instructions of an abacus program. A \emph{configuration}
  of an abacus machine is the current program counter together with a snapshot of 
  all registers.
  By convention
  the value calculated by an abacus program is stored in the
  last register (the one with the highest index in the program).
  
  The main point of abacus programs is to be able to translate them to 
  Turing machine programs. Registers and their content are represented by
  standard tapes (see definition shown in \eqref{standard}). Because of the jumps in abacus programs, it
  is impossible to build a Turing machine programs out of components 
  using our @{text "\<oplus>"}-operation shown in the previous section.
  To overcome this difficulty, we calculate a \emph{layout} of an
  abacus program as follows

  \begin{center}
  \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
  @{thm (lhs) layout(1)} & @{text "\<equiv>"} & @{thm (rhs) layout(1)}\\
  @{thm (lhs) layout(2)} & @{text "\<equiv>"} & @{thm (rhs) layout(2)}\\
  @{thm (lhs) layout(3)} & @{text "\<equiv>"} & @{thm (rhs) layout(3)}\\
  @{thm (lhs) layout(4)} & @{text "\<equiv>"} & @{thm (rhs) layout(4)}\\
  \end{tabular}
  \end{center}

  \noindent
  This gives us a list of natural numbers specifying how many states
  are needed to translate each abacus instruction. This information
  is needed in order to calculate the state where the Turing program
  code of one abacus instruction ends.
  The @{text Goto}
  instruction is easiest to translate requiring only one state, namely
  the Turing machine program:

  \begin{center}
  @{text "tm_of_Goto l"} @{text "\<equiv>"} @{thm (rhs) tgoto.simps[where n="l"]}
  \end{center}

  \noindent
  where @{term "l"} is the state in the Turing machine program 
  to jump to. For translating the instruction @{term "Inc R\<iota>"}, 
  one has to remember that the content of the registers are encoded
  in the Turing machine as a standard tape. Therefore the translated Turing machine 
  needs to first find the number corresponding to the content of register 
  @{text "R"}. This needs a machine
  with @{term "(2::nat) * R\<iota>"} states and can be constructed as follows: 

  \begin{center}
  \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
  @{thm (lhs) findnth.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) findnth.simps(1)}\\
  @{thm (lhs) findnth.simps(2)} & @{text "\<equiv>"}\\
  \multicolumn{3}{@ {}l@ {}}{\hspace{8mm}@{thm (rhs) findnth.simps(2)}}\\
  \end{tabular}
  \end{center}

  \noindent
  Then we need to increase the ``number'' on the tape by one,
  and adjust the following ``registers''. By adjusting we only need to 
  change the first @{term Oc} of each number to @{term Bk} and the last
  one from @{term Bk} to @{term Oc}.
  Finally, we need to transition the head of the
  Turing machine back into the standard position. This requires a Turing machine
  with 9 states (we omit the details). Similarly for the translation of @{term "Dec R\<iota> l"}, where the 
  translated Turing machine needs to first check whether the content of the
  corresponding register is @{text 0}. For this we have a Turing machine program
  with @{text 16} states (again details are omitted). 

  Finally, having a Turing machine for each abacus instruction we need
  to ``stitch'' the Turing machines together into one so that each
  Turing machine component transitions to next one, just like in
  the abacus programs. One last problem to overcome is that an abacus
  program is assumed to calculate a value stored in the last
  register (the one with the highest register). That means we have to append a Turing machine that
  ``mops up'' the tape (cleaning all @{text Oc}s) except for the
  @{term Oc}s of the last number represented on the tape. This needs
  a Turing machine program with @{text "2 * R + 12"} states, assuming @{text R}
  is the number of registers to be ``cleaned''.

  While generating the Turing machine program for an abacus program is
  not too difficult to formalise, the problem is that it contains
  @{text Goto}s all over the place. The unfortunate result is that we
  cannot use our Hoare-rules for reasoning about sequentially composed
  programs (for this each component needs to be completely independent). Instead we
  have to treat the translated Turing machine as one ``big block'' and 
  prove as invariant that it performs
  the same operations as the abacus program. For this we have to show
  that for each configuration of an abacus machine the @{term
  step}-function is simulated by zero or more steps in our translated
  Turing machine. This leads to a rather large ``monolithic''
  correctness proof (4600 loc and 380 sublemmas) that on the
  conceptual level is difficult to break down into smaller components.
  
  %We were able to simplify the proof somewhat
*}


section {* Recursive Functions and a Universal Turing Machine *}

text {*
  The main point of recursive functions is that we can relatively 
  easily construct a universal Turing machine via a universal 
  function. This is different from Norrish \cite{Norrish11} who gives a universal 
  function for Church numbers, and also from Asperti and Ricciotti 
  \cite{AspertiRicciotti12} who construct a universal Turing machine
  directly, but for simulating Turing machines with a more restricted alphabet.
  \emph{Recursive functions} @{term r} are defined as the datatype

  \begin{center}
  \begin{tabular}{c@ {\hspace{4mm}}c}
  \begin{tabular}{rcl@ {\hspace{4mm}}l}
  @{term r} & @{text "::="} & @{term z} & (zero-functions)\\
            & @{text "|"}   & @{term s} & (successor-function)\\
            & @{text "|"}   & @{term "id n m"} & (projection)\\
  \end{tabular} &
  \begin{tabular}{cl@ {\hspace{4mm}}l}
  @{text "|"} & @{term "Cn n r rs"} & (composition)\\
  @{text "|"} & @{term "Pr n r\<^isub>1 r\<^isub>2"} & (primitive recursion)\\
  @{text "|"} & @{term "Mn n r"} & (minimisation)\\
  \end{tabular}
  \end{tabular}
  \end{center}

  \noindent 
  where @{text n} indicates the function expects @{term n} arguments
  (@{text z} and @{term s} expect one argument), and @{text rs} stands
  for a list of recursive functions. Since we know in each case 
  the arity, say @{term l}, we can define an inductive evaluation relation that  
  relates a recursive function @{text r} and a list @{term ns} of natural numbers of length @{text l},
  to what the result of the recursive function is, say @{text n}---we omit the straightforward
  definition of @{term "rec_calc_rel r ns n"}. Because of space reasons, we also omit the 
  definition of translating
  recursive functions into abacus programs. We can prove the following
  theorem about the translation: Assuming 
  @{thm (prem 1) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]}
  then the following Hoare-triple holds

  \begin{center}
  @{thm (concl) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]}
  \end{center}

  \noindent
  which means that if the recursive function @{text r} with arguments @{text ns} evaluates
  to @{text n}, then the corresponding Turing machine @{term "tm_of_rec r"} if started
  with the standard tape @{term "([Bk, Bk], <ns::nat list>)"} will terminate
  with the standard tape @{term "(Bk \<up> k, <n::nat> @ Bk \<up> l)"} for some @{text k} and @{text l}.

  and the also the definition of the
  universal function (we refer the reader to our formalisation).

  \cite[Page 32]{Boolos87}

  \begin{quote}\it
  ``If the function that is to be computed assigns no value to the arguments that 
  are represented initially on the tape, then the machine either will never halt, 
  or will halt in some nonstandard configuration\ldots''
  \end{quote}
  
  This means that if you encode the plus function but only give one argument,
  then the TM will either loop {\bf or} stop with a non-standard tape

  But in the definition of the universal function the TMs will never stop
  with non-standard tapes. 

  SO the following TM calculates something according to def from chap 8,
  but not with chap 3. For example:
  
  \begin{center}
  @{term "[(L, (0::nat)), (L, 2), (R, 2), (R, 0)]"}
  \end{center}

  If started with @{term "([], [Oc])"} it halts with the
  non-standard tape @{term "([Oc], [])"} according to the definition in Chap 3;
  but with @{term "([], [Oc])"} according to def Chap 8

*}

(*
section {* Wang Tiles\label{Wang} *}

text {*
  Used in texture mapings - graphics
*}
*)

section {* Conclusion *}

text {*
  In previous works we were unable to formalise results about
  computability because in a Isabelle/HOL we cannot represent the
  decidability of a predicate @{text P}, say, as the formula @{term "P
  \<or> \<not>P"}. For reasoning about computability we need to formalise a
  concrete model of computations. We could have followed Norrish
  \cite{Norrish11} using the $\lambda$-calculus as the starting point,
  but then we would have to reimplement his infrastructure for
  reducing $\lambda$-terms on the ML-level. We would still need to
  connect his work to Turing machines for proofs that make use of them
  (for example the proof of Wang's tiling problem \cite{Robinson71}).

  We therefore have formalised Turing machines and the main
  computability results from Chapters 3 to 8 in the textbook by Boolos
  et al \cite{Boolos87}.  For this we did not need to implement
  anything on the ML-level of Isabelle/HOL. While formalising
  \cite{Boolos87} have found an inconsistency in Bolos et al's usage
  of definitions of what function a Turing machine calculates. In
  Chapter 3 they use a definition such that the function is undefined
  if the Turing machine loops \emph{or} halts with a non-standard
  tape. Whereas in Chapter 8 about the universal Turing machine, the
  Turing machines will \emph{not} halt unless the tape is in standard
  form. Following in the footsteps of another paper \cite{Nipkow98}
  formalising the results from a semantics textbook, we could
  therefore have titled our paper ``Boolos et al are (almost)
  Right''. We have not attempted to formalise everything precisely as
  Boolos et al present it, but use definitions that make our
  mechanised proofs manageable. For example our definition of the
  halting state performing @{term Nop}-operations seems to be
  non-standard, but very much suited to a formalisation in a theorem
  prover where the @{term steps}-function need to be total.

  The most closely related work is by Norrish \cite{Norrish11}, and
  Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish formalises
  computability theory using $\lambda$-terms. For this he introduced a
  clever rewriting technology based on combinators and de-Bruijn
  indices for rewriting modulo $\beta$-equivalence (in order to avoid
  explicit $\alpha$-renamings). He mentions that formalising Turing
  machines would be a ``daunting prospect'' \cite[Page
  310]{Norrish11}. While $\lambda$-terms indeed lead to some slick
  mechanised proofs, our experience is that Turing machines are not
  too daunting if one is only concerned with formalising the
  undecidability of the halting problem for Turing machines.  This
  took us around 1500 loc of Isar-proofs, which is just one-and-a-half
  times longer than a mechanised proof pearl about the Myhill-Nerode
  theorem. So our conclusion is it not as daunting as we imagined
  reading the paper by Norrish \cite{Norrish11}. The work involved
  with constructing a universal Turing machine via recursive 
  functions and abacus machines, on the other hand, is not a
  project one wants to undertake too many times (our formalisation
  of abacus machines and their correct translation is approximately 
  4300 loc; \ldots)
  
  Our work was also very much inspired by the formalisation of Turing
  machines by Asperti and Ricciotti \cite{AspertiRicciotti12} in the
  Matita theorem prover. It turns out that their notion of
  realisability and our Hoare-triples are very similar, however we
  differ in some basic definitions for Turing machines. Asperti and
  Ricciotti are interested in providing a mechanised foundation for
  complexity theory. They formalised a universal Turing machine
  (which differs from ours by using a more general alphabet), but did
  not describe an undecidability proof. Given their definitions and
  infrastructure, we expect this should not be too difficult for them.
  
  For us the most interesting aspect of our work are the correctness 
  proofs for some Turing machines. Informal presentation of computability
  theory often leave the constructions of particular Turing machines
  as exercise to the reader, as \cite{Boolos87} for example, deeming it 
  too easy for wasting space. However, as far as we are aware all
  informal presentation leave out any correctness proofs---do the 
  Turing machines really perform the task they are supposed to do. 
  This means we have to find appropriate invariants and measures
  that can be established for showing correctness and termination.
  Whenever we can use Hoare-style reasoning, the invariants are
  relatively straightforward and much smaller than for example 
  the invariants by Myreen for a correctness proof of a garbage
  collector \cite[Page 76]{}. The invariant needed for the abacus proof,
  where Hoare-style reasoning does not work, is similar in size as 
  the one by Myreen and finding a sufficiently strong one took
  us, like Myreen, something on the magnitude of weeks. 

  Our reasoning about the invariants is also not very much 
  supported by the automation in Isabelle. There is however a tantalising 
  connection between our work and recent work \cite{Jensen13}
  on verifying X86 assembly code. They observed a similar phenomenon
  with assembly programs that Hoare-style reasoning is sometimes
  possible, but sometimes not. In order to ease their reasoning they
  introduced a more primitive specification logic, on which
  for special cases Hoare-rules can be provided.
  It remains to be seen whether their specification logic
  for assembly code can make it easier to reason about our Turing
  programs. That would be an attractive result, because Turing 
  machine programs are 

  The code of our formalisation is available from the Mercurial repository at
  \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/tm/}
*}



(*<*)
end
end
(*>*)