--- a/Paper/Paper.thy Sat Jul 27 08:23:09 2013 +0200
+++ b/Paper/Paper.thy Tue Sep 03 15:02:52 2013 +0100
@@ -73,23 +73,23 @@
tape_of ("\<langle>_\<rangle>") and
tm_comp ("_ ; _") and
DUMMY ("\<^raw:\mbox{$\_\!\_\,$}>") and
- inv_begin0 ("I\<^isub>0") and
- inv_begin1 ("I\<^isub>1") and
- inv_begin2 ("I\<^isub>2") and
- inv_begin3 ("I\<^isub>3") and
- inv_begin4 ("I\<^isub>4") and
+ inv_begin0 ("I\<^sub>0") and
+ inv_begin1 ("I\<^sub>1") and
+ inv_begin2 ("I\<^sub>2") and
+ inv_begin3 ("I\<^sub>3") and
+ inv_begin4 ("I\<^sub>4") and
inv_begin ("I\<^bsub>cbegin\<^esub>") and
- inv_loop1 ("J\<^isub>1") and
- inv_loop0 ("J\<^isub>0") and
- inv_end1 ("K\<^isub>1") and
- inv_end0 ("K\<^isub>0") and
+ inv_loop1 ("J\<^sub>1") and
+ inv_loop0 ("J\<^sub>0") and
+ inv_end1 ("K\<^sub>1") and
+ inv_end0 ("K\<^sub>0") and
measure_begin_step ("M\<^bsub>cbegin\<^esub>") and
layout_of ("layout") and
findnth ("find'_nth") and
- recf.id ("id\<^raw:\makebox[0mm]{\,\,\,\,>\<^isup>_\<^raw:}>\<^isub>_") and
- Pr ("Pr\<^isup>_") and
- Cn ("Cn\<^isup>_") and
- Mn ("Mn\<^isup>_") and
+ recf.id ("id\<^raw:\makebox[0mm]{\,\,\,\,>\<^sup>_\<^raw:}>\<^sub>_") and
+ Pr ("Pr\<^sup>_") and
+ Cn ("Cn\<^sup>_") and
+ Mn ("Mn\<^sup>_") and
rec_exec ("eval") and
tm_of_rec ("translate") and
listsum ("\<Sigma>")
@@ -145,10 +145,10 @@
done
lemmas HR1 =
- Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^isub>1" and B="p\<^isub>2"]
+ Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^sub>1" and B="p\<^sub>2"]
lemmas HR2 =
- Hoare_plus_unhalt[where ?A="p\<^isub>1" and B="p\<^isub>2"]
+ Hoare_plus_unhalt[where ?A="p\<^sub>1" and B="p\<^sub>2"]
lemma inv_begin01:
assumes "n > 1"
@@ -645,7 +645,7 @@
\end{equation}
%
\noindent
- A \emph{standard tape} is then of the form @{text "(Bk\<^isup>k,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle> @ Bk\<^isup>l)"} for some @{text k},
+ A \emph{standard tape} is then of the form @{text "(Bk\<^sup>k,\<langle>[n\<^sub>1,...,n\<^sub>m]\<rangle> @ Bk\<^sup>l)"} for some @{text k},
@{text l}
and @{text "n\<^bsub>1...m\<^esub>"}. Note that the head in a standard tape ``points'' to the
leftmost @{term "Oc"} on the tape. Note also that the natural number @{text 0}
@@ -670,18 +670,18 @@
0}-state, thus redirecting all references to the ``halting state''
to the first state after the program @{text p}. With these two
functions in place, we can define the \emph{sequential composition}
- of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"} as
+ of two Turing machine programs @{text "p\<^sub>1"} and @{text "p\<^sub>2"} as
\begin{center}
- @{thm tm_comp.simps[where ?p1.0="p\<^isub>1" and ?p2.0="p\<^isub>2", THEN eq_reflection]}
+ @{thm tm_comp.simps[where ?p1.0="p\<^sub>1" and ?p2.0="p\<^sub>2", THEN eq_reflection]}
\end{center}
\noindent
- %This means @{text "p\<^isub>1"} is executed first. Whenever it originally
+ %This means @{text "p\<^sub>1"} is executed first. Whenever it originally
%transitioned to the @{text 0}-state, it will in the composed program transition to the starting
- %state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"}
+ %state of @{text "p\<^sub>2"} instead. All the states of @{text "p\<^sub>2"}
%have been shifted in order to make sure that the states of the composed
- %program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy''
+ %program @{text "p\<^sub>1 \<oplus> p\<^sub>2"} still only ``occupy''
%an initial segment of the natural numbers.
\begin{figure}[t]
@@ -970,7 +970,7 @@
the first program terminates generating a tape for which the second
program loops. The side-conditions about @{thm (prem 3) HR2} are
needed in order to ensure that the redirection of the halting and
- initial state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"}, respectively, match
+ initial state in @{term "p\<^sub>1"} and @{term "p\<^sub>2"}, respectively, match
up correctly. These Hoare-rules allow us to prove the correctness
of @{term tcopy} by considering the correctness of the components
@{term "tcopy_begin"}, @{term "tcopy_loop"} and @{term "tcopy_end"}
@@ -1128,25 +1128,25 @@
\end{center}
\noindent
- Suppose @{thm (prem 1) "tcontra_halt"} holds. Given the invariants @{text "P\<^isub>1"}\ldots@{text "P\<^isub>3"}
+ Suppose @{thm (prem 1) "tcontra_halt"} holds. Given the invariants @{text "P\<^sub>1"}\ldots@{text "P\<^sub>3"}
shown on the
left, we can derive the following Hoare-pair for @{term tcontra} on the right.
\begin{center}\small
\begin{tabular}{@ {}c@ {\hspace{-10mm}}c@ {}}
\begin{tabular}[t]{@ {}l@ {}}
- @{term "P\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
- @{term "P\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
- @{term "P\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"}
+ @{term "P\<^sub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
+ @{term "P\<^sub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
+ @{term "P\<^sub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"}
\end{tabular}
&
\begin{tabular}[b]{@ {}l@ {}}
\raisebox{-20mm}{$\inferrule*{
- \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {P\<^isub>3}"}}
- {@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}}
- \\ @{term "{P\<^isub>3} dither \<up>"}
+ \inferrule*{@{term "{P\<^sub>1} tcopy {P\<^sub>2}"} \\ @{term "{P\<^sub>2} H {P\<^sub>3}"}}
+ {@{term "{P\<^sub>1} (tcopy |+| H) {P\<^sub>3}"}}
+ \\ @{term "{P\<^sub>3} dither \<up>"}
}
- {@{term "{P\<^isub>1} tcontra \<up>"}}
+ {@{term "{P\<^sub>1} tcontra \<up>"}}
$}
\end{tabular}
\end{tabular}
@@ -1157,25 +1157,25 @@
with @{term "<(code tcontra)>"} halts.
Suppose @{thm (prem 1) "tcontra_unhalt"} holds. Again, given the invariants
- @{text "Q\<^isub>1"}\ldots@{text "Q\<^isub>3"}
+ @{text "Q\<^sub>1"}\ldots@{text "Q\<^sub>3"}
shown on the
left, we can derive the Hoare-triple for @{term tcontra} on the right.
\begin{center}\small
\begin{tabular}{@ {}c@ {\hspace{-18mm}}c@ {}}
\begin{tabular}[t]{@ {}l@ {}}
- @{term "Q\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
- @{term "Q\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
- @{term "Q\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"}
+ @{term "Q\<^sub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
+ @{term "Q\<^sub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
+ @{term "Q\<^sub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"}
\end{tabular}
&
\begin{tabular}[t]{@ {}l@ {}}
\raisebox{-20mm}{$\inferrule*{
- \inferrule*{@{term "{Q\<^isub>1} tcopy {Q\<^isub>2}"} \\ @{term "{Q\<^isub>2} H {Q\<^isub>3}"}}
- {@{term "{Q\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}}
- \\ @{term "{Q\<^isub>3} dither {Q\<^isub>3}"}
+ \inferrule*{@{term "{Q\<^sub>1} tcopy {Q\<^sub>2}"} \\ @{term "{Q\<^sub>2} H {Q\<^sub>3}"}}
+ {@{term "{Q\<^sub>1} (tcopy |+| H) {Q\<^sub>3}"}}
+ \\ @{term "{Q\<^sub>3} dither {Q\<^sub>3}"}
}
- {@{term "{Q\<^isub>1} tcontra {Q\<^isub>3}"}}
+ {@{term "{Q\<^sub>1} tcontra {Q\<^sub>3}"}}
$}
\end{tabular}
\end{tabular}
@@ -1196,8 +1196,8 @@
\noindent
Boolos et al \cite{Boolos87} use abacus machines as a stepping stone
for making it less laborious to write Turing machine
- programs. Abacus machines operate over a set of registers @{text "R\<^isub>0"},
- @{text "R\<^isub>1"}, \ldots{}, @{text "R\<^isub>n"} each being able to hold an arbitrary large natural
+ programs. Abacus machines operate over a set of registers @{text "R\<^sub>0"},
+ @{text "R\<^sub>1"}, \ldots{}, @{text "R\<^sub>n"} each being able to hold an arbitrary large natural
number. We use natural numbers to refer to registers; we also use a natural number
to represent a program counter and to represent jumping ``addresses'', for which we
use the letter @{text l}. An abacus
@@ -1354,7 +1354,7 @@
\end{tabular} &
\begin{tabular}{cl@ {\hspace{4mm}}l}
@{text "|"} & @{term "Cn n f fs"} & (composition)\\
- @{text "|"} & @{term "Pr n f\<^isub>1 f\<^isub>2"} & (primitive recursion)\\
+ @{text "|"} & @{term "Pr n f\<^sub>1 f\<^sub>2"} & (primitive recursion)\\
@{text "|"} & @{term "Mn n f"} & (minimisation)\\
\end{tabular}
\end{tabular}