diff -r 4b35e0e0784b -r c9b689bb4156 Paper.thy
--- a/Paper.thy	Sat Jan 12 02:14:29 2013 +0000
+++ b/Paper.thy	Sat Jan 12 08:16:15 2013 +0000
@@ -94,6 +94,7 @@
   abc_lm_s ("set") and
   haltP ("stdhalt") and 
   tshift ("shift") and 
+  tcopy ("copy") and 
   change_termi_state ("adjust") and
   tape_of_nat_list ("\<ulcorner>_\<urcorner>") and 
   t_add ("_ \<oplus> _") and 
@@ -178,14 +179,14 @@
 \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 \emph{not} ``sufficiently accurate to be directly useable as a
+started are \emph{not} ``sufficiently accurate to be directly usable as a
 guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For
 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
 machines computing unary functions. We had to figure out a way to
-generalize this result to $n$-ary functions. Similarly, when compiling
+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
@@ -311,7 +312,7 @@
 
   \noindent
   The first two clauses replace the head of the right-list
-  with a new @{term Bk} or @{term Oc}, repsectively. To see that
+  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 in
   Isabelle/HOL
@@ -339,12 +340,12 @@
   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 uniformely all cases including corner cases.
+  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 carfully a representation. If we use the naive
+  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,
@@ -534,7 +535,7 @@
 
   Before we can prove the undecidability of the halting problem for Turing machines, 
   we have to define how to compose two Turing machines. Given our setup, this is 
-  relatively straightforward, if slightly fiddly. We have the following two
+  relatively straightforward, if slightly fiddly. We use the following two
   auxiliary functions:
 
   \begin{center}
@@ -548,13 +549,31 @@
   \end{center}
 
   \noindent
-  With this we can define the \emph{sequential composition} of two
-  Turing machines @{text "M\<^isub>1"} and @{text "M\<^isub>2"}
+  The first adds @{text n} to all states, exept the @{text 0}-state,
+  thus moving all ``regular'' states to the segment starting at @{text
+  n}; the second adds @{term "length p div 2 + 1"} to the @{text
+  0}-state, thus ridirecting 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"}
 
   \begin{center}
-  @{thm t_add.simps[where ?t1.0="M\<^isub>1" and ?t2.0="M\<^isub>2", THEN eq_reflection]}
+  @{thm t_add.simps[where ?t1.0="p\<^isub>1" and ?t2.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.
+
+  \begin{center}
+  \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}p{6.9cm}@ {}}
+  @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def}
+  \end{tabular}
+  \end{center}
 
 
   assertion holds for all tapes