tm: comparison Paper/Paper.thy

equal deleted inserted replaced

-:7d29c3c09bea
+:a21fb87bb0bd
 exponent ("_\<^bsup>_\<^esup>") and
 tcopy ("copy") and
 tape_of ("\<langle>_\<rangle>") and
 tm_comp ("_ ; _") and
 DUMMY  ("\<^raw:\mbox{$\_\!\_\,$}>") and
-inv_begin0 ("I\<^isub>0") and
+inv_begin0 ("I\<^sub>0") and
-inv_begin1 ("I\<^isub>1") and
+inv_begin1 ("I\<^sub>1") and
-inv_begin2 ("I\<^isub>2") and
+inv_begin2 ("I\<^sub>2") and
-inv_begin3 ("I\<^isub>3") and
+inv_begin3 ("I\<^sub>3") and
-inv_begin4 ("I\<^isub>4") and
+inv_begin4 ("I\<^sub>4") and
 inv_begin ("I\<^bsub>cbegin\<^esub>") and
-inv_loop1 ("J\<^isub>1") and
+inv_loop1 ("J\<^sub>1") and
-inv_loop0 ("J\<^isub>0") and
+inv_loop0 ("J\<^sub>0") and
-inv_end1 ("K\<^isub>1") and
+inv_end1 ("K\<^sub>1") and
-inv_end0 ("K\<^isub>0") 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
+recf.id ("id\<^raw:\makebox[0mm]{\,\,\,\,>\<^sup>_\<^raw:}>\<^sub>_") and
-Pr ("Pr\<^isup>_") and
+Pr ("Pr\<^sup>_") and
-Cn ("Cn\<^isup>_") and
+Cn ("Cn\<^sup>_") and
-Mn ("Mn\<^isup>_") and
+Mn ("Mn\<^sup>_") and
 rec_exec ("eval") and
 tm_of_rec ("translate") and
 listsum ("\<Sigma>")
 apply(case_tac ns)
 apply(auto simp add: tape_of_nat_pair tape_of_nat_abv)
 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"
 shows "inv_begin0 n (l, r) = (n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc]))"
 using assms by auto
 @{thm (lhs) nats2tape(3)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(3)}
 \end{tabular}}\label{standard}
 \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}
 is represented by a single filled cell on a standard tape, @{text 1} by two filled cells and so on.
 thus moving all ``regular'' states to the segment starting at @{text
 n}; the second adds @{term "Suc(length p div 2)"} to the @{text
 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]
 \begin{center}
 \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c}
 The first corresponds to the usual Hoare-rule for composition of two
 terminating programs. The second rule gives the conditions for when
 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"}
 in isolation. This simplifies the reasoning considerably, for
 example when designing decreasing measures for proving the termination
 \begin{center}
 @{thm tcontra_def}
 \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\<^sub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
-@{term "P\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
+@{term "P\<^sub>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>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}"}}
+\inferrule*{@{term "{P\<^sub>1} tcopy {P\<^sub>2}"} \\ @{term "{P\<^sub>2} H {P\<^sub>3}"}}
-{@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}}
+{@{term "{P\<^sub>1} (tcopy |+| H) {P\<^sub>3}"}}
-\\ @{term "{P\<^isub>3} dither \<up>"}
+\\ @{term "{P\<^sub>3} dither \<up>"}
 }
-{@{term "{P\<^isub>1} tcontra \<up>"}}
+{@{term "{P\<^sub>1} tcontra \<up>"}}
 $}
 \end{tabular}
 \end{tabular}
 \end{center}
 \noindent
 This Hoare-pair contradicts our assumption that @{term tcontra} started
 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\<^sub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
-@{term "Q\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
+@{term "Q\<^sub>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>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}"}}
+\inferrule*{@{term "{Q\<^sub>1} tcopy {Q\<^sub>2}"} \\ @{term "{Q\<^sub>2} H {Q\<^sub>3}"}}
-{@{term "{Q\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}}
+{@{term "{Q\<^sub>1} (tcopy |+| H) {Q\<^sub>3}"}}
-\\ @{term "{Q\<^isub>3} dither {Q\<^isub>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}
 \end{center}
 text {*
 \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"},
+programs. Abacus machines operate over a set of registers @{text "R\<^sub>0"},
-@{text "R\<^isub>1"}, \ldots{}, @{text "R\<^isub>n"} each being able to hold an arbitrary large natural
+@{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
 program is a list of \emph{instructions} defined by the datatype:
 & @{text "|"}   & @{term s} & (successor-function)\\
 & @{text "|"}   & @{term "id n m"} & (projection)\\
 \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}
 \end{center}

changeset 284	a21fb87bb0bd
parent 239	ac3309722536