--- a/Paper/Paper.thy	Mon Apr 22 10:33:40 2013 +0100
+++ b/Paper/Paper.thy	Wed Apr 24 09:49:00 2013 +0100
@@ -191,75 +191,10 @@
 apply(arith)+
 done
 
-(*
-lemma "run tcopy (1, [], <0::nat>) = (0, [Bk], [Oc, Bk, Oc])"
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral nth_of.simps del: run.simps)
-apply(simp only: numeral[symmetric])
-apply(simp)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)
-apply(simp only: numeral[symmetric])
-apply(simp)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)
-apply(simp only: numeral[symmetric])
-apply(simp)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)
-apply(simp only: numeral[symmetric])
-apply(simp)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)
-apply(simp only: numeral[symmetric])
-apply(simp)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)
-apply(simp only: numeral[symmetric])
-apply(simp)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)
-apply(simp only: numeral[symmetric])
-apply(simp)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)
-apply(simp only: numeral[symmetric])
-apply(simp)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)
-apply(simp only: numeral[symmetric])
-apply(simp)
-apply(subst run.simps)
-apply(simp)
+lemma tm_wf_simps:
+  "tm_wf0 p = (2 <=length p \<and> is_even(length p) \<and> (\<forall>(a,s) \<in> set p. s <= (length p) div 2))"
+apply(simp add: tm_wf.simps)
 done
-*)
 
 (*>*)
 
@@ -420,7 +355,7 @@
 turn recursive functions to abacus machines. The universal Turing
 machine can then be constructed by translating from a (universal) recursive function. 
 The part of mechanising the translation of recursive function to register 
-machines has already been done by Zammit in HOL \cite{Zammit99}, 
+machines has already been done by Zammit in HOL4 \cite{Zammit99}, 
 although his register machines use a slightly different instruction
 set than the one described in \cite{Boolos87}.
 
@@ -506,12 +441,8 @@
   \begin{tabular}[t]{@ {}rcl@ {\hspace{2mm}}l}
   @{text "a"} & $::=$  & @{term "W0"} & (write blank, @{term Bk})\\
   & $\mid$ & @{term "W1"} & (write occupied, @{term Oc})\\
-  \end{tabular}
-  \begin{tabular}[t]{rcl@ {\hspace{2mm}}l}
   & $\mid$ & @{term L} & (move left)\\
   & $\mid$ & @{term R} & (move right)\\
-  \end{tabular}
-  \begin{tabular}[t]{rcl@ {\hspace{2mm}}l@ {}}
   & $\mid$ & @{term Nop} & (do-nothing operation)\\
   \end{tabular}
   \end{center}
@@ -645,7 +576,7 @@
   satisfies the following three properties:
 
   \begin{center}
-  @{thm tm_wf.simps[where p="p" and off="0::nat", simplified, THEN eq_reflection]}
+  @{thm tm_wf_simps[where p="p", THEN eq_reflection]}
   \end{center}
 
   \noindent
@@ -903,17 +834,17 @@
   \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
   \begin{tabular}[t]{@ {}l@ {}}
   \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\\
-  \hspace{7mm}@{text "is_final (steps (1, (l, r)) p n)"} \hspace{1mm}@{text "\<and>"}\\
-  \hspace{7mm}@{text "Q holds_for (steps (1, (l, r)) p n)"}
+  \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\
+  \hspace{7mm}if @{term "P tp"} holds then\\
+  \hspace{7mm}@{text "\<exists>"}@{term n}. such that\\
+  \hspace{7mm}@{text "is_final (steps (1, tp) p n)"} \hspace{1mm}@{text "\<and>"}\\
+  \hspace{7mm}@{text "Q holds_for (steps (1, tp) p n)"}
   \end{tabular} &
   \begin{tabular}[t]{@ {}l@ {}}
   \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)"}
+  \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\ 
+  \hspace{7mm}if @{term "P tp"} holds then\\
+  \hspace{7mm}@{text "\<forall>"}@{term n}. @{text "\<not> is_final (steps (1, tp) p n)"}
   \end{tabular}
   \end{tabular}
   \end{center}
@@ -998,7 +929,7 @@
   \end{center}
 
   \noindent
-  We can prove the following Hoare-statements:
+  We can prove the following two Hoare-statements:
  
   \begin{center}
   \begin{tabular}{l}
@@ -1308,7 +1239,7 @@
   Turing machine programs. Registers and their content are represented by
   standard tapes (see definition shown in \eqref{standard}). Because of the jumps in abacus programs, it
   is impossible to build Turing machine programs out of components 
-  using our @{text "\<oplus>"}-operation shown in the previous section.
+  using our @{text ";"}-operation shown in the previous section.
   To overcome this difficulty, we calculate a \emph{layout} of an
   abacus program as follows
 
@@ -1465,13 +1396,13 @@
   other is the ``packed version'' of the arguments of the Turing machine. 
   We can then consider how this universal function is translated to a 
   Turing machine and from this construct the universal Turing machine, 
-  written @{term UTM}. @{text UTM} is defined as 
+  written @{term UTM}. It is defined as 
   the composition of the Turing machine that packages the arguments and
   the translated recursive 
   function @{text UF}:
 
   \begin{center}
-  @{text "UTM \<equiv> arg_coding \<oplus> (translate UF)"}
+  @{text "UTM \<equiv> arg_coding ; (translate UF)"}
   \end{center}
 
   \noindent
@@ -1656,11 +1587,11 @@
   formula @{term "P \<or> \<not>P"}. For reasoning about computability we need
   to formalise a concrete model of computations. We could have
   followed Norrish \cite{Norrish11} using the $\lambda$-calculus as
-  the starting point for computability theory, but then we would have
+  the starting point for formalising computability theory, but then we would have
   to reimplement on the ML-level his infrastructure for rewriting
   $\lambda$-terms modulo $\beta$-equality: HOL4 has a simplifer that
   can rewrite terms modulo an arbitrary equivalence relation, which
-  Isabelle unfortunately does not yet have.  Even though we would
+  Isabelle unfortunately does not yet have.  Even though, we would
   still need to connect $\lambda$-terms somehow to Turing machines for
   proofs that make essential use of them (for example the
   undecidability proof for Wang's tiling problem \cite{Robinson71}).