--- a/Paper/Paper.thy	Thu Jan 24 18:59:49 2013 +0100
+++ b/Paper/Paper.thy	Fri Jan 25 15:57:58 2013 +0100
@@ -133,14 +133,15 @@
 formalisation of Turing machines, as well as abacus machines (a kind
 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 involving 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 fortunately quite often), but also tackle 
-the more complicated case when we translate abacus programs into 
-Turing programs.  This reasoning about Turing machine programs is
-usually completely left out in the informal literature, e.g.~\cite{Boolos87}.
+programs can be completely \emph{unstructured}, behaving similar to
+Basic programs involving 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
+fortunately quite often), but also tackle the more complicated case
+when we translate abacus programs into Turing programs.  This
+reasoning about concrete Turing machine programs is usually
+left out in the informal literature, e.g.~\cite{Boolos87}.
 
 %To see the difficulties
 %involved with this work, one has to understand that interactive
@@ -230,7 +231,8 @@
 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}
+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.
 *}
@@ -266,6 +268,7 @@
   \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[fill]     (-1.65,0.1) rectangle (-1.35,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};
@@ -522,7 +525,9 @@
   \caption{Copy machine}\label{copy}
   \end{figure}
 
-  {\it tapes in standard form}
+  {\it 
+  As in \cite{Boolos87} we often need to restrict tapes to be in standard
+  form.}
 
   Before we can prove the undecidability of the halting problem for our
   Turing machines, we need to analyse two concrete Turing machine
@@ -530,7 +535,7 @@
   ``doing what they are supposed to be doing''.  Such correctness proofs are usually left
   out in the informal literature, for example \cite{Boolos87}.  One program 
   we need to prove correct is the @{term dither} program shown in \eqref{dither} 
-  and the other program is @{term "tcopy"} is defined as
+  and the other program is @{term "tcopy"} defined as
 
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
@@ -554,7 +559,7 @@
   \begin{center}
   \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
   \begin{tabular}[t]{@ {}l@ {}}
-  @{thm (lhs) Hoare_halt_def} @{text "\<equiv>"}\\[1mm]
+  \colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\<equiv>"}\\[1mm]
   \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\
   \hspace{7mm}if @{term "P (l, r)"} holds then\\
   \hspace{7mm}@{text "\<exists>"} @{term n}. such that\\
@@ -562,7 +567,7 @@
   \hspace{7mm}@{text "Q holds_for (steps (1, (l, r)) p n)"}
   \end{tabular} &
   \begin{tabular}[t]{@ {}l@ {}}
-  @{thm (lhs) Hoare_unhalt_def} @{text "\<equiv>"}\\[1mm]
+  \colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm]
   \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\ 
   \hspace{7mm}if @{term "P (l, r)"} holds then\\
   \hspace{7mm}@{text "\<forall>"} @{term n}. @{text "\<not> is_final (steps (1, (l, r)) p n)"}
@@ -577,9 +582,57 @@
   more uniformly (only using Hoare-triples), we prefer our definitions because 
   we can derive simple Hoare-rules for sequentially composed Turing programs. 
   In this way we can reason about the correctness of @{term "tcopy_init"},
-  for example, completely separately from @{term "tcopy_loop"}.
+  for example, completely separately from @{term "tcopy_loop"} and @{term "tcopy_end"}.
 
-  It is rather straightforward to prove that the Turing program 
+  \begin{center}
+  \begin{tabular}{lcl}
+  \multicolumn{1}{c}{start tape}\\
+  \begin{tikzpicture}
+  \draw[very thick] (-2,0)   -- ( 0.75,0);
+  \draw[very thick] (-2,0.5) -- ( 0.75,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[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
+  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
+  \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);
+  \node [anchor=base] at (-1.7,0.2) {\ldots};
+  \end{tikzpicture} 
+  & \raisebox{2.5mm}{$\;\;\large\Rightarrow\;\;$} &
+  \begin{tikzpicture}
+  \draw[very thick] (-2,0)   -- ( 0.75,0);
+  \draw[very thick] (-2,0.5) -- ( 0.75,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[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
+  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
+  \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);
+  \node [anchor=base] at (-1.7,0.2) {\ldots};
+  \end{tikzpicture}\\
+
+   \begin{tikzpicture}
+  \draw[very thick] (-2,0)   -- ( 0.25,0);
+  \draw[very thick] (-2,0.5) -- ( 0.25,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] (-1.25,0)   -- (-1.25,0.5);
+  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
+  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
+  \node [anchor=base] at (-1.7,0.2) {\ldots};
+  \end{tikzpicture} 
+  & \raisebox{2.5mm}{$\;\;\large\Rightarrow\;\;$} &
+  \raisebox{2.5mm}{loops}
+  \end{tabular}
+  \end{center}
+
+
+  It is straightforward to prove that the Turing program 
   @{term "dither"} satisfies the following correctness properties
 
   \begin{center}

--- a/Paper/document/root.bib	Thu Jan 24 18:59:49 2013 +0100
+++ b/Paper/document/root.bib	Fri Jan 25 15:57:58 2013 +0100
@@ -74,4 +74,25 @@
   number    = {3},
   year      = {1968},
   pages     = {147-148}
-}
\ No newline at end of file
+}
+
+
+
+@Book{Berger66,
+  author = 	 {R.~Berger},
+  title = 	 {{T}he {U}ndecidability of the {D}omino {P}roblem},
+  journal = 	 {Memoirs of the American Mathematical Society},
+  year = 	 {1966}
+}
+
+
+@Article{Robinson71,
+  author = 	 {R.~M.~Robinson},
+  title = 	 {{U}ndecidability and {N}onperiodicity for {T}ilings of the {P}lane},
+  journal = 	 {Inventiones Mathematicae},
+  year = 	 {1971},
+  volume = 	 {12},
+  pages = 	 {177--209}
+}
+
+

--- a/Paper/document/root.tex	Thu Jan 24 18:59:49 2013 +0100
+++ b/Paper/document/root.tex	Fri Jan 25 15:57:58 2013 +0100
@@ -10,6 +10,7 @@
 \usepackage{pdfsetup}
 \usepackage{tikz}
 \usepackage{pgf}
+\usepackage{color}
 
 %% for testing
 \usepackage{endnotes}
@@ -19,6 +20,9 @@
 \urlstyle{rm}
 \isabellestyle{it}
 
+% gray boxes
+\definecolor{mygrey}{rgb}{.80,.80,.80}
+
 % mathpatir
 \mprset{sep=0.8em}
 \mprset{center=false}

Binary file paper.pdf has changed

--- a/thys/uncomputable.thy	Thu Jan 24 18:59:49 2013 +0100
+++ b/thys/uncomputable.thy	Fri Jan 25 15:57:58 2013 +0100
@@ -1075,47 +1075,36 @@
 abbreviation
   "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc]"
 
-lemma dither_unhalt_state: 
+lemma dither_loops_aux: 
   "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or> 
    (steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))"
   apply(induct stp)
-  apply(simp add: steps.simps)
-  apply(simp add: step_red)
-  apply(auto simp: step.simps fetch.simps dither_def numeral)
+  apply(auto simp: steps.simps step.simps dither_def numeral)
   done
 
-lemma dither_unhalt_rs: 
-  shows "\<not> is_final (steps0 (1, Bk \<up> m, [Oc]) dither stp)"
-using dither_unhalt_state[of m stp]
-by auto
-
 lemma dither_loops:
   shows "{dither_unhalt_inv} dither \<up>" 
 apply(rule Hoare_unhaltI)
-using dither_unhalt_rs
-apply(auto)
-done
+using dither_loops_aux
+apply(auto simp add: numeral)
+by (metis Suc_neq_Zero is_final_eq)
+
 
-lemma dither_halt_rs: 
-  "\<exists>stp. steps0 (1, Bk \<up> m, [Oc, Oc]) dither stp = (0, Bk \<up> m, [Oc, Oc])"
+lemma dither_halts_aux: 
+  shows "steps0 (1, Bk \<up> m, [Oc, Oc]) dither 3 = (0, Bk \<up> m, [Oc, Oc])"
 unfolding dither_def
-apply(rule_tac x = "3" in exI)
-apply(simp add: steps.simps step.simps fetch.simps numeral)
-done 
-
+by (simp add: steps.simps step.simps numeral)
 
 lemma dither_halts:
   shows "{dither_halt_inv} dither {dither_halt_inv}" 
 apply(rule Hoare_haltI)
-using dither_halt_rs
+using dither_halts_aux
 apply(auto)
 by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases)
 
 
 
-section {*
-  The final diagnal arguments to show the undecidability of Halting problem.
-*}
+section {* The diagnal argument below shows the undecidability of Halting problem *}
 
 text {*
   @{text "haltP tp x"} means TM @{text "tp"} terminates on input @{text "x"}
@@ -1124,8 +1113,7 @@
 
 definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool"
   where
-  "haltP p lm = (\<exists>n a b c. steps (Suc 0, [], <lm>) p n = (0, Bk\<up>a,  Oc\<up>b @ Bk\<up>c))"
-
+  "haltP p lm \<equiv> \<exists>n a b c. steps (Suc 0, [], <lm>) p n = (0, Bk \<up> a,  Oc \<up> b @ Bk \<up> c)"
 
 abbreviation
   "haltP0 p lm \<equiv> haltP (p, 0) lm"