
diff -r 66cebc19ef18 -r a961c2e4dcea Paper.thy
--- a/Paper.thy	Wed Jan 09 13:35:09 2013 +0000
+++ b/Paper.thy	Thu Jan 10 01:46:51 2013 +0000
@@ -3,6 +3,50 @@
 imports UTM
 begin
 
+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{$\_$}>")
+
 declare [[show_question_marks = false]]
 (*>*)
 
@@ -82,9 +126,9 @@
 \cite{AspertiRicciotti12}. They describe a complete formalisation of
 Turing machines in the Matita theorem prover, including a universal
 Turing machine. They report that the informal proofs from which they
-started are not ``sufficiently accurate to be directly used as a
+started are not ``sufficiently accurate to be directly useable as a
 guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For
-our formalisation we followed the proofs from the textbook
+our formalisation we followed mainly the proofs from the textbook
 \cite{Boolos87} and found that the description there is quite
 detailed. Some details are left out however: for example, it is only
 shown how the universal Turing machine is constructed for Turing
@@ -113,18 +157,22 @@
 \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 blank or filled cells (represented 
-by @{term Bk} and @{term Oc}, respectively, in our
+operate on tapes that contain only \emph{blank} or \emph{filled} cells
+(represented by @{term Bk} and @{term Oc}, respectively, in our
 formalisation). Traditionally the content of a cell can be any
-character from a finite alphabet. Although computationally
-equivalennt, the more restrictive notion of Turing machines make
-the reasoning more uniform. Unfortunately, it also makes it
-harder to design programs for 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. 
+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.
 
-\medskip
+\smallskip
 \noindent
 {\bf Contributions:} 
 
@@ -133,16 +181,51 @@
 section {* Turing Machines *}
 
 text {*
-
-  Tapes
+  \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}
-  %%
-  %\end{tikzpicture}
-  %\end{center}
+  \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}
   
-  An action is defined as 
+  \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:
 
   \begin{center}
   \begin{tabular}{rcll}
@@ -150,10 +233,93 @@
   & $\mid$ & @{term "W1"} & write occupied (@{term Oc})\\
   & $\mid$ & @{term L} & move left\\
   & $\mid$ & @{term R} & move right\\
-  & $\mid$ & @{term Nop} & do nothing\\
+  & $\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)}\\
   \end{tabular}
   \end{center}
 
+  \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}
+
+
   For showing the undecidability of the halting problem, we need to consider
   two specific Turing machines.
   




