hide_const (open) s

abbreviation 

  "update p a == new_tape a p"

lemma fetch_def2: 

  shows "fetch p 0 b = (Nop, 0)"

  and "fetch p (Suc s) Bk = 

     (case nth_of p (2 * s) of

        Some i \<Rightarrow> i

      | None \<Rightarrow> (Nop, 0))"

  and "fetch p (Suc s) Oc =  

     (case nth_of p ((2 * s) + 1) of

         Some i \<Rightarrow> i

       | None \<Rightarrow> (Nop, 0))"

by (auto split: block.splits simp add: fetch.simps)

lemma new_tape_def2: 

  shows "new_tape W0 (l, r) == (l, Bk#(tl r))" 

  and "new_tape W1 (l, r) == (l, Oc#(tl r))"

  and "new_tape L (l, r) == 

     (if l = [] then ([], Bk#r) else (tl l, (hd l) # r))" 

  and "new_tape R (l, r) ==

     (if r = [] then (Bk#l,[]) else ((hd r)#l, tl r))" 

  and "new_tape Nop (l, r) == (l, r)"

apply -

apply(rule_tac [!] eq_reflection)

apply(auto split: taction.splits simp add: new_tape.simps)

done

lemma tstep_def2:

  shows "tstep (s, l, []) p = (let (ac, ns) = fetch p s Bk in (ns, new_tape ac (l, [])))"

  and "tstep (s, l, x#xs) p = (let (ac, ns) = fetch p s x in (ns, new_tape ac (l, x#xs)))"

by (auto split: prod.split list.split simp add: tstep.simps)

consts DUMMY::'a

notation (latex output)

  Cons ("_::_" [78,77] 73) and

  W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and

  W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and

  DUMMY  ("\<^raw:\mbox{$\_$}>")

started are not ``sufficiently accurate to be directly useable as a

our formalisation we followed mainly the proofs from the textbook

operate on tapes that contain only \emph{blank} or \emph{filled} cells

(represented by @{term Bk} and @{term Oc}, respectively, in our

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 will be simpler.  The reason is that one often need to encode

Turing machines---if the Turing machines are simpler, then the coding

functions are simpler. Unfortunately, the restrictiveness also makes

it harder to design programs for these Turing machines. Therefore in order

to construct a \emph{universal Turing machine} we follow the proof in

\cite{Boolos87} by relating abacus machines to Turing machines and in

turn recursive functions to abacus machines. The universal Turing

machine can then be constructed as recursive function.

\smallskip

  \noindent

  Turing machines can be thought of as having read-write-unit

  ``gliding'' over a potentially infinite tape. Boolos et

  al~\cite{Boolos87} only consider tapes with cells being either blank

  or occupied, which we represent with a datatype having two

  constructors, namely @{text Bk} and @{text Oc}.  One easy 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 of the

  read-write-unit and @{term r} for the tape on the right. We have the

  convention that the head, written @{term hd}, of the right-list is

  the cell on which the read-write-unit currently operates. This can

  be pictured as follows:

  \begin{center}

  \begin{tikzpicture}

  \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 (-0.25,0.8) -- (-0.25,-0.8);

  \draw[<->] (-1.25,-0.7) -- (0.75,-0.7);

  \node [anchor=base] at (-0.8,-0.5) {\small left list};

  \node [anchor=base] at (0.35,-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 cell 

  whenever the read-write unit goes over the ``edge'' of the tape. To 

  make this formal we define five possible \emph{actions} 

  the Turing machine can perform:

  & $\mid$ & @{term Nop} & do-nothing operation\\

  \end{tabular}

  \end{center}

  \noindent

  By using the @{term Nop} operation, we slightly deviate

  from the presentation in \cite{Boolos87}; however its use

  will become important when we formalise universal Turing 

  machines. Given a tape and an action, we can define the

  following updating function:

  \begin{center}

  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

  @{thm (lhs) new_tape_def2(1)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(1)}\\

  @{thm (lhs) new_tape_def2(2)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(2)}\\

  @{thm (lhs) new_tape_def2(3)} & @{text "\<equiv>"} & \\

  \multicolumn{3}{p{3cm}}{\hspace{1cm}@{thm (rhs) new_tape_def2(3)}}\\

  @{thm (lhs) new_tape_def2(4)} & @{text "\<equiv>"} & \\

  \multicolumn{3}{p{2cm}}{\hspace{1cm}@{thm (rhs) new_tape_def2(4)}}\\

  @{thm (lhs) new_tape_def2(5)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(5)}\\

  \noindent

  The first two clauses replace the head of the right-list

  with new @{term Bk} or @{term Oc}, repsectively. To see that

  these 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 read-write unit to the left: we need

  to test if the left-list is empty; if yes, then we just add a 

  blank cell to the right-list; otherwise we have to remove the

  head from the left-list and add it to the right-list. Similarly

  in the clause for the right move. 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 read-write unit is currently possitioned. Asperti and 

  Ricciotti \cite{AspertiRicciotti12} also consider such a 

  representation, but dismiss it as it complicates their

  definition for \emph{tape equality}. The reason is that 

  moving the read-write unit to the left and then back

  to the right can change the tape (in case of going

  over the ``edge''). Therefore they distinguish four 

  cases where the tape is empty as well as the read-write unit

  on the left edge, respectively right edge, or in the

  middle. The reading and moving of the tape is then

  defined in terms of these four cases. Since we are not

  going to use the notion of tape equality, we can

  get away with the definition above and be done with 

  all corner cases.

  Next we need to define the \emph{states} of a Turing machine.  Given

  how little is usually said about how to represent states in informal

  presentaions, it might be surprising that in a theorem prover we have 

  to select carfully a representation. If we use the naive representation

  as a Turing machine consiting of a finite set of states, then we

  will have difficulties composing two Turing machines. We would need

  to somehow combine the two finite sets of states, possibly renaming

  states apart if both machines share states. This renaming can be

  quite cumbersome to reason about. Therefore we made the choice

  of representing a state by a natural number and the states of a 

  Turing machine will always consist of the initial segment

  of natural numbers starting from @{text 0} up to number of states

  of the machine minus @{text 1}. In doing so we can compose

  two Turing machine by ``shifting'' the states of one by an appropriate

  amount to a higher segment.

  An \emph{instruction} of a Turing machine is a pair consisting of a

  natural number (the next state) and an action. A \emph{program} of a Turing

  machine is then a list of such pairs. Given a program @{term p}, a state

  and a cell being read by the read-write unnit, we need to fetch

  the corresponding instruction in the program. For this we define 

  the function @{term fetch}

  \begin{center}

  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

  @{thm (lhs) fetch_def2(1)[where b=DUMMY]} & @{text "\<equiv>"} & @{thm (rhs) fetch_def2(1)}\\

  @{thm (lhs) fetch_def2(2)} & @{text "\<equiv>"} & \\

  \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) fetch_def2(2)}}\\

  @{thm (lhs) fetch_def2(3)} & @{text "\<equiv>"} & \\

  \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) fetch_def2(3)}}\\

  \end{tabular}

  \end{center}