# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1358057945 0
# Node ID 8f8db701f69fef4f03fb991076f6ff91601c0bfc
# Parent  c9b689bb415669c25415585f15100611630db3cd
updated contribution section

diff -r c9b689bb4156 -r 8f8db701f69f Paper.thy
--- a/Paper.thy	Sat Jan 12 08:16:15 2013 +0000
+++ b/Paper.thy	Sun Jan 13 06:19:05 2013 +0000
@@ -171,8 +171,8 @@
 there seems to be no alternative if one wants to formalise the great
 many proofs from the literature that use them.  We will analyse one
 example---undecidability of Wang's tiling problem---in Section~\ref{Wang}. The
-standard proof of this property uses the notion of \emph{universal
-Turing machines}.
+standard proof of this property uses the notion of universal
+Turing machines.
 
 We are not the first who formalised Turing machines in a theorem
 prover: we are aware of the preliminary work by Asperti and Ricciotti
@@ -220,7 +220,7 @@
 Turing machines---consequently if the Turing machines are simpler, then the coding
 functions are simpler too. Unfortunately, the restrictiveness also makes
 it harder to design programs for these Turing machines. In order
-to construct a \emph{universal Turing machine} we therefore do not follow 
+to construct a universal Turing machine we therefore do not follow 
 \cite{AspertiRicciotti12}, instead follow the proof in
 \cite{Boolos87} by relating abacus machines to Turing machines and in
 turn recursive functions to abacus machines. The universal Turing
@@ -228,8 +228,17 @@
 
 \smallskip
 \noindent
-{\bf Contributions:} 
-
+{\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.  
+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.
 *}
 
 section {* Turing Machines *}
diff -r c9b689bb4156 -r 8f8db701f69f paper.pdf
Binary file paper.pdf has changed