# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1360197964 0
# Node ID 4d7a568bd91177b8116c882daeb1bb5b463f1c02
# Parent  7f5243700f258f98394dd649647169df67b7757b
updated paper

diff -r 7f5243700f25 -r 4d7a568bd911 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Feb 06 14:14:35 2013 +0000
+++ b/Paper/Paper.thy	Thu Feb 07 00:46:04 2013 +0000
@@ -229,7 +229,7 @@
 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
+Basic programs containing the infamous goto \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
@@ -318,22 +318,25 @@
 
 \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.
+{\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. When formalising the universal Turing machine,
+we stumbled upon an inconsistence use of the definition of
+what function a Turing machine calculates. 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 *}
@@ -747,7 +750,8 @@
   \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} 
+  A \emph{standard tape} is then of the form @{text "(Bk\<^isup>k,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle> @ Bk\<^isup>l)"} for some @{text k}, 
+  @{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.
@@ -977,7 +981,7 @@
 
   \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
+  @{term Oc}s 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
diff -r 7f5243700f25 -r 4d7a568bd911 paper.pdf
Binary file paper.pdf has changed
diff -r 7f5243700f25 -r 4d7a568bd911 thys/uncomputable.thy
--- a/thys/uncomputable.thy	Wed Feb 06 14:14:35 2013 +0000
+++ b/thys/uncomputable.thy	Thu Feb 07 00:46:04 2013 +0000
@@ -996,7 +996,7 @@
 
 definition haltP :: "tprog0 \<Rightarrow> nat list \<Rightarrow> bool"
   where
-  "haltP p ns \<equiv> {(\<lambda>tp. tp = ([], <ns>))} p {(\<lambda>tp. (\<exists>k n. tp = (Bk \<up> k,  <n::nat>)))}"
+  "haltP p ns \<equiv> {(\<lambda>tp. tp = ([], <ns>))} p {(\<lambda>tp. (\<exists>k n l. tp = (Bk \<up> k,  <n::nat> @ Bk \<up> l)))}"
 
 lemma [intro, simp]: "tm_wf0 tcopy"
 by (auto simp: tcopy_def)
@@ -1108,7 +1108,7 @@
     apply(drule_tac x = n in spec)
     apply(case_tac "steps0 (Suc 0, [], <code tcontra>) tcontra n")
     apply(auto simp add: tape_of_nl_abv)
-    done
+    by (metis append_Nil2 replicate_0)
 qed
 
 (* asumme tcontra halts on its code *)