--- a/Paper/Paper.thy Sat Jan 26 01:36:48 2013 +0000
+++ b/Paper/Paper.thy Sat Jan 26 11:50:40 2013 +0000
@@ -21,7 +21,7 @@
W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
update2 ("update") and
tm_wf0 ("wf") and
- is_even ("iseven") and
+ (*is_even ("iseven") and*)
tcopy_init ("copy\<^bsub>begin\<^esub>") and
tcopy_loop ("copy\<^bsub>loop\<^esub>") and
tcopy_end ("copy\<^bsub>end\<^esub>") and
@@ -32,7 +32,7 @@
abc_lm_s ("set") and*)
haltP ("stdhalt") and
tcopy ("copy") and
- tape_of_nat_list ("\<ulcorner>_\<urcorner>") and
+ tape_of ("\<langle>_\<rangle>") and
tm_comp ("_ \<oplus> _") and
DUMMY ("\<^raw:\mbox{$\_$}>")
@@ -70,7 +70,14 @@
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
"_asm" :: "prop \<Rightarrow> asms" ("_")
-
+lemma nats2tape:
+ shows "<([]::nat list)> = []"
+ and "<[n]> = Oc \<up> (n + 1)"
+ and "ns \<noteq> [] \<Longrightarrow> <n#ns> = Oc \<up> (n + 1) @ [Bk] @ <ns>"
+apply(auto simp add: tape_of_nl_abv tape_of_nat_list.simps)
+apply(case_tac ns)
+apply(auto)
+done
(*>*)
@@ -256,7 +263,7 @@
scannes. This can be pictured as follows:
%
\begin{center}
- \begin{tikzpicture}
+ \begin{tikzpicture}[scale=0.9]
\draw[very thick] (-3.0,0) -- ( 3.0,0);
\draw[very thick] (-3.0,0.5) -- ( 3.0,0.5);
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
@@ -274,8 +281,8 @@
\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};
- \node [anchor=base] at (0.35,-0.5) {\small right list};
+ \node [anchor=base] at (-0.85,-0.5) {\small left list};
+ \node [anchor=base] at (0.40,-0.5) {\small right list};
\node [anchor=base] at (0.1,0.7) {\small head};
\node [anchor=base] at (-2.2,0.2) {\ldots};
\node [anchor=base] at ( 2.3,0.2) {\ldots};
@@ -516,14 +523,24 @@
\begin{figure}[t]
\begin{center}
- \begin{tabular}{@ {}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {}}
- @{thm (lhs) tcopy_init_def} @{text "\<equiv>"} &
- @{thm (lhs) tcopy_loop_def} @{text "\<equiv>"} &
+ \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c}
+ \begin{tabular}{@ {}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 "]"}
+ \end{tabular}
+ &
+ \begin{tabular}{@ {}p{3.6cm}@ {}}
+ @{thm (lhs) tcopy_loop_def} @{text "\<equiv>"}\\
+ @{thm (rhs) tcopy_loop_def}\\
+ \end{tabular}
+ &
+ \begin{tabular}{@ {}p{3.6cm}@ {}}
@{thm (lhs) tcopy_end_def} @{text "\<equiv>"}\\
- @{thm (rhs) tcopy_init_def} &
- @{thm (rhs) tcopy_loop_def} &
@{thm (rhs) tcopy_end_def}
\end{tabular}
+ \end{tabular}
\end{center}
\caption{Copy machine}\label{copy}
\end{figure}
@@ -535,17 +552,17 @@
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
- @{thm (lhs) tape_of_nat_list.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list.simps(1)}\\
- @{thm (lhs) tape_of_nat_list.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list.simps(2)}\\
- @{thm (lhs) tape_of_nat_list.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list.simps(3)}
+ @{thm (lhs) nats2tape(1)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(1)}\\
+ @{thm (lhs) nats2tape(2)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(2)}\\
+ @{thm (lhs) nats2tape(3)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(3)}
\end{tabular}
\end{center}
\noindent
- A standard tape is then of the form @{text "(Bk\<^isup>l,\<langle>n\<^isub>1,...,n\<^isub>m\<rangle>)"} for some @{text l}
+ A standard tape is then of the form @{text "(Bk\<^isup>l,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle>)"} for some @{text l}
and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the
- leftmost @{term "Oc"} on the tape.
-
+ leftmost @{term "Oc"} on the tape. Note also that @{text 0} is represented by
+ a single filled cell, @{text 1} by two filled cells and so on.
Before we can prove the undecidability of the halting problem for our
Turing machines, we need to analyse two concrete Turing machine
@@ -606,7 +623,7 @@
\begin{tabular}{l@ {\hspace{3mm}}lcl}
& \multicolumn{1}{c}{start tape}\\[1mm]
\raisebox{2.5mm}{halting case:} &
- \begin{tikzpicture}
+ \begin{tikzpicture}[scale=0.9]
\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);
@@ -620,7 +637,7 @@
\node [anchor=base] at (-1.7,0.2) {\ldots};
\end{tikzpicture}
& \raisebox{2.5mm}{$\;\;\large\Rightarrow\;\;$} &
- \begin{tikzpicture}
+ \begin{tikzpicture}[scale=0.9]
\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);
@@ -635,7 +652,7 @@
\end{tikzpicture}\\
\raisebox{2.5mm}{non-halting case:} &
- \begin{tikzpicture}
+ \begin{tikzpicture}[scale=0.9]
\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);