Mercurial Mercurial > hg > tm / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Paper/Paper.thy
changeset 87 cf6e89b5f702
parent 86 046c9ecf9150
child 88 904f9351ab94 
--- a/Paper/Paper.thy	Sat Jan 26 12:00:21 2013 +0000
+++ b/Paper/Paper.thy	Sat Jan 26 21:46:12 2013 +0000
@@ -524,30 +524,118 @@
   \begin{figure}[t]
   \begin{center}
   \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c}
-  \begin{tabular}{@ {}l@ {}}
+  \begin{tabular}[t]{@ {}l@ {}}
   @{thm (lhs) tcopy_init_def} @{text "\<equiv>"}\\
-  @{text "["}@{text "(W0, 0), (R, 2), (R, 3),"}\\
-  \phantom{@{text "["}}@{text "(R, 2), (W1, 3), (L, 4),"}\\
-  \phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} 
+  \hspace{2mm}@{text "["}@{text "(W\<^bsub>Bk\<^esub>, 0), (R, 2), (R, 3),"}\\
+  \hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W1, 3), (L, 4),"}\\
+  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} 
+  \end{tabular}
+  &
+  \begin{tabular}[t]{@ {}l@ {}}
+  @{thm (lhs) tcopy_loop_def} @{text "\<equiv>"}\\
+  \hspace{2mm}@{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\
+  \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>Bk\<^esub>, 2), (R, 3), (R, 4),"}\\
+  \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>Oc\<^esub>, 5), (R, 4), (L, 6),"}\\
+  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (L, 6), (L, 1)"}@{text "]"} 
   \end{tabular}
   &
-  \begin{tabular}{@ {}l@ {}}
-  @{thm (lhs) tcopy_loop_def} @{text "\<equiv>"}\\
-  @{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\
-  \phantom{@{text "["}}@{text "(W0, 2), (R, 3), (R, 4),"}\\
-  \phantom{@{text "["}}@{text "(W1, 5), (R, 4), (L, 6),"}\\
-  \phantom{@{text "["}}@{text "(L, 5), (L, 6), (L, 1)"}@{text "]"} 
+  \begin{tabular}[t]{@ {}l@ {}}
+  @{thm (lhs) tcopy_end_def} @{text "\<equiv>"}\\
+  \hspace{2mm}@{text "["}@{text "(L, 0), (R, 2), (W\<^bsub>Oc\<^esub>, 3),"}\\
+  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (R, 2), (R, 2),"}\\
+  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (W\<^bsub>Bk\<^esub>, 4), (R, 0),"}\\
+  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5)"}@{text "]"} 
   \end{tabular}
-  &
-  \begin{tabular}{@ {}p{3.6cm}@ {}}
-  @{thm (lhs) tcopy_end_def} @{text "\<equiv>"}\\
-  @{thm (rhs) tcopy_end_def}
-  \end{tabular}
-  \end{tabular}
+  \end{tabular}\\[2mm]
+
+  \begin{tikzpicture}[scale=0.7]
+  \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$};
+  \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$};
+  \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$};
+  \node [anchor=base] at (2.2,-0.5) {\small@{term "tcopy_init"}};
+  \node [anchor=base] at (5.6,-0.5) {\small@{term "tcopy_loop"}};
+  \node [anchor=base] at (10.5,-0.5) {\small@{term "tcopy_end"}};
+
+
+  \begin{scope}[shift={(0.5,0)}]
+  \draw[very thick] (-0.25,0)   -- ( 1.25,0);
+  \draw[very thick] (-0.25,0.5) -- ( 1.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);
+  \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);
+  \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);
+  \end{scope}
+
+  \begin{scope}[shift={(2.9,0)}]
+  \draw[very thick] (-0.25,0)   -- ( 2.25,0);
+  \draw[very thick] (-0.25,0.5) -- ( 2.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[very thick] ( 1.75,0)   -- ( 1.75,0.5);
+  \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);
+  \draw[rounded corners=1mm] (0.15,-0.1) rectangle (0.85,0.6);
+  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
+  \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);
+  \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);
+  \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);
+  \end{scope}
+
+  \begin{scope}[shift={(6.8,0)}]
+  \draw[very thick] (-0.75,0)   -- ( 3.25,0);
+  \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);
+  \draw[very thick] (-0.75,0)   -- (-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] ( 1.25,0)   -- ( 1.25,0.5);
+  \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);
+  \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);
+  \draw[very thick] ( 2.75,0)   -- ( 2.75,0.5);
+  \draw[very thick] ( 3.25,0)   -- ( 3.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]     ( 2.35,0.1) rectangle (2.65,0.4);
+  \draw[fill]     ( 2.85,0.1) rectangle (3.15,0.4);
+  \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);
+  \end{scope}
+
+  \begin{scope}[shift={(11.7,0)}]
+  \draw[very thick] (-0.75,0)   -- ( 3.25,0);
+  \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);
+  \draw[very thick] (-0.75,0)   -- (-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] ( 1.25,0)   -- ( 1.25,0.5);
+  \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);
+  \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);
+  \draw[very thick] ( 2.75,0)   -- ( 2.75,0.5);
+  \draw[very thick] ( 3.25,0)   -- ( 3.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]     ( 2.35,0.1) rectangle (2.65,0.4);
+  \draw[fill]     ( 2.85,0.1) rectangle (3.15,0.4);
+  \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);
+  \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);
+  \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);
+  \end{scope}
+  \end{tikzpicture}\\[-8mm]\mbox{} 
   \end{center}
-  \caption{Copy machine}\label{copy}
+  \caption{The components of the \emph{copy Turing machine} (above). If started 
+  with the tape @{term "([], <[(3::nat)]>)"} the first machine adds @{term "[Bk, Oc]"} at 
+  the end of the right tape; the second then ``moves'' all @{term Oc}s except the 
+  first from the beginning of the tape to the end; the third ``refills'' the original 
+  block of @{term "Oc"}s. The result is the tape @{term "([Bk], <[(3::nat, 3::nat)]>)"}.}
+  \label{copy}
   \end{figure}
 
+
   We often need to restrict tapes to be in \emph{standard form}, which means 
   the left list of the tape is either empty or only contains @{text "Bk"}s, and 
   the right list contains some ``clusters'' of @{text "Oc"}s separted by single 
@@ -692,9 +780,9 @@
   In the following we will consider the following Turing machine program
   that makes a copies a value on the tape.
 
- 
+   
 
-
+
tm