diff -r 2363eb91d9fd -r 8c7f10b3da7b Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Jan 23 20:18:40 2013 +0100
+++ b/Paper/Paper.thy	Thu Jan 24 00:20:26 2013 +0100
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "../thys/uncomputable" "~~/src/HOL/Library/LaTeXsugar"
+imports "../thys/uncomputable"
 begin
 
 (*
@@ -22,6 +22,7 @@
   W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
   update2 ("update") and
   tm_wf0 ("wf") and
+  is_even ("iseven") and
 (*  abc_lm_v ("lookup") and
   abc_lm_s ("set") and*)
   haltP ("stdhalt") and 
@@ -31,6 +32,41 @@
   DUMMY  ("\<^raw:\mbox{$\_$}>")
 
 declare [[show_question_marks = false]]
+
+(* 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" ("_")
+
+
+
 (*>*)
 
 section {* Introduction *}
@@ -52,13 +88,15 @@
 
 
 \noindent
-Suppose you want to mechanise a proof about whether a predicate @{term P}, say, is
+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. 
+computable means. We hit this limitation previously when we mechanised the correctness
+proofs of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, 
+but were unable to formalise arguments about computability.
 
 %The same problem would arise if we had formulated
 %the algorithms as recursive functions, because internally in
@@ -183,9 +221,12 @@
 We construct the universal Turing machine from \cite{Boolos87} by
 relating 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 the
-undecidability of Wang's tiling problem. We are not aware of any other
-formalisation of a substantial undecidability problem.
+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 formalising the undecidability proof of Wang's tiling problem. {\it citation}
+%We are not aware of any other
+%formalisation of a substantial undecidability problem.
 *}
 
 section {* Turing Machines *}
@@ -311,11 +352,11 @@
   %cannot be used as it does not preserve types.} This renaming can be
   %quite cumbersome to reason about. 
   We followed the choice made in \cite{AspertiRicciotti12} 
-  representing a state by a natural number and the states of a Turing
-  machine by the initial segment of natural numbers starting from @{text 0}.
-  In doing so we can compose two Turing machine by
+  representing a state by a natural number and the states in a Turing
+  machine programme 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. {\it composition here?}
+  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
@@ -356,35 +397,26 @@
   the corresponding instruction from the program. For this we define 
   the function @{term fetch}
  
-  \begin{center}
-  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+  \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{center}
+  \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). In doing so we slightly deviate from the description
-  in \cite{Boolos87}: if their Turing machines transition to a non-existing
-  state, then the computation is halted. We will transition in such cases
-  to the @{text 0}-state.\footnote{\it However, with introducing the
-  notion of \emph{well-formed} Turing machine programs we will later exclude such
-  cases and make the  @{text 0}-state the only ``halting state''. A program 
-  @{term p} is said to be well-formed if it satisfies
-  the following three properties:
+  (@{term None}-case). We often need 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}
-  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-  @{term "t_correct p"} & @{text "\<equiv>"} & @{term "2 <= length p"}\\
-                        & @{text "\<and>"} & @{term "iseven (length p)"}\\
-                        & @{text "\<and>"} & @{term "\<forall> (a, s) \<in> set p. s <= length p div 2"}
-  \end{tabular}
+  @{thm tm_wf.simps[where p="p" and off="0::nat", simplified, THEN eq_reflection]}
   \end{center}
 
   \noindent
@@ -392,7 +424,6 @@
   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.
-  }
 
   A \emph{configuration} @{term c} of a Turing machine is a state together with 
   a tape. This is written as @{text "(s, (l, r))"}. If we have a 
@@ -425,69 +456,14 @@
   \end{center}
 
   \noindent
-  Recall our definition of @{term fetch} with the default value for
+  Recall our definition of @{term fetch} (shown in \ref{fetch}) with the default value for
   the @{text 0}-state. In case a Turing program takes in \cite{Boolos87} less 
   then @{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 and 
   remains there performing @{text Nop}-actions until @{text n} is reached. 
 
-  Given some input tape @{text "(l\<^isub>i,r\<^isub>i)"}, we can define when a program 
-  @{term p} generates a specific  output tape @{text "(l\<^isub>o,r\<^isub>o)"}
-
-  \begin{center}
-  \begin{tabular}{l}
-  @{term "runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\
-  \hspace{6mm}@{text "\<exists>n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n = (0, (l\<^isub>o,r\<^isub>o))"}
-  \end{tabular}
-  \end{center}
-
-  \noindent
-  where @{text 1} stands for the starting state and @{text 0} for our final state.
-  A program @{text p} with input tape @{term "(l\<^isub>i, r\<^isub>i)"} \emph{halts} iff
-
-  \begin{center}
-  @{term "halts p (l\<^isub>i, r\<^isub>i) \<equiv>
-  \<exists>l\<^isub>o r\<^isub>o. runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"}
-  \end{center}
-
-  \noindent
-  Later on we need to consider specific Turing machines that 
-  start with a tape in standard form and halt the computation
-  in standard form. To define a tape in standard form, it is
-  useful to have an operation %@{ term "tape_of_nat_list DUMMY"} 
-  that translates lists of natural numbers into tapes. 
-
-  
-  \begin{center}
-  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-  %@ { thm (lhs) tape_of_nat_list_def2(1)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(1)}\\
-  %@ { thm (lhs) tape_of_nat_list_def2(2)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(2)}\\
-  %@ { thm (lhs) tape_of_nat_list_def2(3)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(3)}\\
-  \end{tabular}
-  \end{center}
-
-  
-
-
-  By this we mean
-
-  \begin{center}
-  %@ {thm haltP_def2[where p="p" and n="n", THEN eq_reflection]}
-  \end{center}
-
-  \noindent
-  This means the Turing machine starts with a tape containg @{text n} @{term Oc}s
-  and the head pointing to the first one; the Turing machine
-  halts with a tape consisting of some @{term Bk}s, followed by a 
-  ``cluster'' of @{term Oc}s and after that by some @{term Bk}s.
-  The head in the output is pointing again at the first @{term Oc}.
-  The intuitive meaning of this definition is to start the Turing machine with a
-  tape corresponding to a value @{term n} and producing
-  a new tape corresponding to the value @{term l} (the number of @{term Oc}s
-  clustered on the output tape).
-
   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 
+  we have to define how to compose two Turing machine programs. Given our setup, this is 
   relatively straightforward, if slightly fiddly. We use the following two
   auxiliary functions:
 
@@ -501,8 +477,8 @@
   \noindent
   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''
+  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"}
@@ -512,12 +488,26 @@
   \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.
+  %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.
+
+  In the following we will consider the following Turing machine program
+  that makes a copies a value on the tape.
+
+  \begin{figure}
+  \begin{center}
+  \begin{tabular}{@ {}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {}}
+  @{thm tcopy_init_def} &
+  @{thm tcopy_loop_def} &
+  @{thm tcopy_end_def}
+  \end{tabular}
+  \end{center}
+  \end{figure}
+
 
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}p{6.9cm}@ {}}
@@ -620,6 +610,62 @@
   lambda-terms. For this he introduced a clever rewriting technology
   based on combinators and de-Bruijn indices for
   rewriting modulo $\beta$-equivalence (to keep it manageable)
+
+
+  
+  Given some input tape @{text "(l\<^isub>i,r\<^isub>i)"}, we can define when a program 
+  @{term p} generates a specific  output tape @{text "(l\<^isub>o,r\<^isub>o)"}
+
+  \begin{center}
+  \begin{tabular}{l}
+  @{term "runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\
+  \hspace{6mm}@{text "\<exists>n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n = (0, (l\<^isub>o,r\<^isub>o))"}
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  where @{text 1} stands for the starting state and @{text 0} for our final state.
+  A program @{text p} with input tape @{term "(l\<^isub>i, r\<^isub>i)"} \emph{halts} iff
+
+  \begin{center}
+  @{term "halts p (l\<^isub>i, r\<^isub>i) \<equiv>
+  \<exists>l\<^isub>o r\<^isub>o. runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"}
+  \end{center}
+
+  \noindent
+  Later on we need to consider specific Turing machines that 
+  start with a tape in standard form and halt the computation
+  in standard form. To define a tape in standard form, it is
+  useful to have an operation %@{ term "tape_of_nat_list DUMMY"} 
+  that translates lists of natural numbers into tapes. 
+
+  
+  \begin{center}
+  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+  %@ { thm (lhs) tape_of_nat_list_def2(1)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(1)}\\
+  %@ { thm (lhs) tape_of_nat_list_def2(2)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(2)}\\
+  %@ { thm (lhs) tape_of_nat_list_def2(3)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(3)}\\
+  \end{tabular}
+  \end{center}
+
+  
+ By this we mean
+
+  \begin{center}
+  %@ {thm haltP_def2[where p="p" and n="n", THEN eq_reflection]}
+  \end{center}
+
+  \noindent
+  This means the Turing machine starts with a tape containg @{text n} @{term Oc}s
+  and the head pointing to the first one; the Turing machine
+  halts with a tape consisting of some @{term Bk}s, followed by a 
+  ``cluster'' of @{term Oc}s and after that by some @{term Bk}s.
+  The head in the output is pointing again at the first @{term Oc}.
+  The intuitive meaning of this definition is to start the Turing machine with a
+  tape corresponding to a value @{term n} and producing
+  a new tape corresponding to the value @{term l} (the number of @{term Oc}s
+  clustered on the output tape).
+
 *}