Paper/Paper.thy
changeset 50 816e84ca16d6
parent 49 b388dceee892
child 52 2cb1e4499983
--- a/Paper/Paper.thy	Fri Jan 18 13:03:09 2013 +0000
+++ b/Paper/Paper.thy	Fri Jan 18 13:56:35 2013 +0000
@@ -7,6 +7,9 @@
 hide_const (open) s 
 *)
 
+
+hide_const (open) Divides.adjust
+
 abbreviation
   "update2 p a \<equiv> update a p"
 
@@ -31,6 +34,8 @@
 
 section {* Introduction *}
 
+
+
 text {*
 
 %\noindent
@@ -46,7 +51,7 @@
 
 
 \noindent
-Suppose you want to mechanise a proof whether a predicate @{term P}, say, is
+Suppose you want to mechanise a proof about 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
@@ -61,7 +66,7 @@
 
 The only satisfying way out of this problem in a theorem prover based
 on classical logic is to formalise a theory of computability. Norrish
-provided such a formalisation for the HOL4 theorem prover. He choose
+provided such a formalisation for the HOL4. He choose
 the $\lambda$-calculus as the starting point for his formalisation of
 computability theory, because of its ``simplicity'' \cite[Page
 297]{Norrish11}.  Part of his formalisation is a clever infrastructure
@@ -71,7 +76,7 @@
  to have formalisations for more operational models of
 computations, such as Turing machines or register machines.  One
 reason is that many proofs in the literature use them.  He noted
-however that in the context of theorem provers \cite[Page 310]{Norrish11}:
+however that \cite[Page 310]{Norrish11}:
 
 \begin{quote}
 \it``If register machines are unappealing because of their 
@@ -85,7 +90,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's infamous goto. This precludes in the
+similar to Basic's 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 is possible to
 reason in a compositional manner (which is fortunately quite often), but also tackle 
@@ -152,9 +157,8 @@
 \noindent
 In this paper we follow the approach by Boolos et al \cite{Boolos87},
 which goes back to Post \cite{Post36}, where all Turing machines
-operate on tapes that contain only \emph{blank} or \emph{occupied} cells
-(represented by @{term Bk} and @{term Oc}, respectively, in our
-formalisation). Traditionally the content of a cell can be any
+operate on tapes that contain only \emph{blank} or \emph{occupied} cells. 
+Traditionally the content of a cell can be any
 character from a finite alphabet. Although computationally equivalent,
 the more restrictive notion of Turing machines in \cite{Boolos87} makes
 the reasoning more uniform. In addition some proofs \emph{about} Turing
@@ -186,8 +190,7 @@
 section {* Turing Machines *}
 
 text {* \noindent
-  Turing machines can be thought of as having a read-write-unit, also
-  referred to as \emph{head},
+  Turing machines can be thought of as having a \emph{head},
   ``gliding'' over a potentially infinite tape. Boolos et
   al~\cite{Boolos87} only consider tapes with cells being either blank
   or occupied, which we represent by a datatype having two
@@ -198,7 +201,7 @@
   convention that the head, abbreviated @{term hd}, of the right-list is
   the cell on which the head of the Turing machine currently operates. This can
   be pictured as follows:
-
+  %
   \begin{center}
   \begin{tikzpicture}
   \draw[very thick] (-3.0,0)   -- ( 3.0,0);
@@ -233,12 +236,16 @@
   the Turing machine can perform:
 
   \begin{center}
-  \begin{tabular}{rcl@ {\hspace{5mm}}l}
-  @{text "a"} & $::=$  & @{term "W0"} & write blank (@{term Bk})\\
-  & $\mid$ & @{term "W1"} & write occupied (@{term Oc})\\
-  & $\mid$ & @{term L} & move left\\
-  & $\mid$ & @{term R} & move right\\
-  & $\mid$ & @{term Nop} & do-nothing operation\\
+  \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}
 
@@ -263,15 +270,14 @@
   The first two clauses replace the head of the right-list
   with a new @{term Bk} or @{term Oc}, respectively. To see that
   these two clauses make sense in case where @{text r} is the empty
-  list, one has to know that the tail function, @{term tl}, is defined in
-  Isabelle/HOL
+  list, one has to know that the tail function, @{term tl}, is defined
   such that @{term "tl [] == []"} holds. The third clause 
   implements the move of the head one step to the left: we need
   to test if the left-list @{term l} is empty; if yes, then we just prepend a 
   blank cell to the right-list; otherwise we have to remove the
   head from the left-list and prepend it to the right-list. Similarly
   in the fourth clause for a right move action. The @{term Nop} operation
-  leaves the the tape unchanged (last clause).
+  leaves the the tape unchanged.
 
   %Note that our treatment of the tape is rather ``unsymmetric''---we
   %have the convention that the head of the right-list is where the
@@ -291,23 +297,24 @@
   %definition above, and by using the @{term update} function
   %cover uniformly all cases including corner cases.
 
-  Next we need to define the \emph{states} of a Turing machine.  Given
-  how little is usually said about how to represent them in informal
-  presentations, it might be surprising that in a theorem prover we
-  have to select carefully a representation. If we use the naive
-  representation where a Turing machine consists of a finite set of
-  states, then we will have difficulties composing two Turing
-  machines: we would need to combine two finite sets of states,
-  possibly renaming states apart whenever both machines share
-  states.\footnote{The usual disjoint union operation in Isabelle/HOL
-  cannot be used as it does not preserve types.} This renaming can be
-  quite cumbersome to reason about. Therefore we made the choice of
+  Next we need to define the \emph{states} of a Turing machine.  
+  %Given
+  %how little is usually said about how to represent them in informal
+  %presentations, it might be surprising that in a theorem prover we
+  %have to select carefully a representation. If we use the naive
+  %representation where a Turing machine consists of a finite set of
+  %states, then we will have difficulties composing two Turing
+  %machines: we would need to combine two finite sets of states,
+  %possibly renaming states apart whenever both machines share
+  %states.\footnote{The usual disjoint union operation in Isabelle/HOL
+  %cannot be used as it does not preserve types.} This renaming can be
+  %quite cumbersome to reason about. 
+  We followed the choice made by \cite{AspertiRicciotti12} 
   representing a state by a natural number and the states of a Turing
-  machine will always consist of the initial segment of natural
-  numbers starting from @{text 0} up to the number of states of the
-  machine. In doing so we can compose two Turing machine by
+  machine by the initial segment of natural numbers starting from @{text 0}.
+  In doing so we can compose two Turing machine by
   shifting the states of one by an appropriate amount to a higher
-  segment and adjusting some ``next states'' in the other.
+  segment and adjusting some ``next states'' in the other. {\it composition here?}
 
   An \emph{instruction} @{term i} 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
@@ -333,7 +340,7 @@
   similarly the second component determines what should be done in
   case of reading @{term Oc}. We have the convention that the first
   state is always the \emph{starting state} of the Turing machine.
-  The zeroth state is special in that it will be used as the
+  The @{text 0}-state is special in that it will be used as the
   ``halting state''.  There are no instructions for the @{text
   0}-state, but it will always perform a @{term Nop}-operation and
   remain in the @{text 0}-state.  Unlike Asperti and Riccioti
@@ -352,9 +359,9 @@
   \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{1.4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}\\
+  \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{1.4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}
+  \multicolumn{3}{@ {\hspace{4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}
   \end{tabular}
   \end{center}
 
@@ -365,7 +372,7 @@
   (@{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. However, with introducing the
+  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
@@ -384,6 +391,7 @@
   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 
@@ -485,11 +493,8 @@
 
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
-  @{thm (lhs) shift.simps} @{text "\<equiv>"}\\
-  \hspace{4mm}@{thm (rhs) shift.simps}\\
-  @{thm (lhs) adjust.simps} @{text "\<equiv>"}\\
-  \hspace{4mm}@{text "map (\<lambda> (a, s)."}\\
-  \hspace{14mm}@{text "(a, if s = 0 then length p div 2 + 1 else s)) p"}\\
+  @{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\
+  @{thm (lhs) adjust.simps} @{text "\<equiv>"} @{thm (rhs) adjust.simps}\\
   \end{tabular}
   \end{center}
 
@@ -503,7 +508,7 @@
   of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"}
 
   \begin{center}
-  @{thm tm_comp.simps[THEN eq_reflection]}
+  @{thm tm_comp.simps[where ?p1.0="p\<^isub>1" and ?p2.0="p\<^isub>2", THEN eq_reflection]}
   \end{center}
 
   \noindent