--- a/Paper.thy Thu Jan 10 07:34:08 2013 +0000
+++ b/Paper.thy Thu Jan 10 08:27:42 2013 +0000
@@ -10,15 +10,17 @@
lemma fetch_def2:
- shows "fetch p 0 b = (Nop, 0)"
- and "fetch p (Suc s) Bk =
+ shows "fetch p 0 b == (Nop, 0)"
+ and "fetch p (Suc s) Bk ==
(case nth_of p (2 * s) of
Some i \<Rightarrow> i
| None \<Rightarrow> (Nop, 0))"
- and "fetch p (Suc s) Oc =
+ and "fetch p (Suc s) Oc ==
(case nth_of p ((2 * s) + 1) of
Some i \<Rightarrow> i
| None \<Rightarrow> (Nop, 0))"
+apply -
+apply(rule_tac [!] eq_reflection)
by (auto split: block.splits simp add: fetch.simps)
lemma new_tape_def2:
@@ -258,44 +260,45 @@
\noindent
The first two clauses replace the head of the right-list
with new a @{term Bk} or @{term Oc}, repsectively. To see that
- these clauses make sense in case where @{text r} is the empty
+ these tow clauses make sense in case where @{text r} is the empty
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 read-write unit to the left: we need
- to test if the left-list is empty; if yes, then we just add a
+ implements the move of the read-write unit 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 add it to the right-list. Similarly
- in the clause for the right move. The @{term Nop} operation
+ head from the left-list and prepend it to the right-list. Similarly
+ in the clause for a right move action. The @{term Nop} operation
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 read-write unit is currently possitioned. Asperti and
- Ricciotti \cite{AspertiRicciotti12} also consider such a
- representation, but dismiss it as it complicates their
- definition for \emph{tape equality}. The reason is that
- moving the read-write unit to the left and then back
- to the right can change the tape (in case of going
- over the ``edge''). Therefore they distinguish four
- cases where the tape is empty as well as the read-write unit
- on the left edge, respectively right edge, or in the
- middle. The reading and moving of the tape is then
- defined in terms of these four cases. Since we are not
- going to use the notion of tape equality, we can
- get away with the definition above and be done with
- all corner cases.
+ have the convention that the head of the right-list is where the
+ read-write unit is currently positioned. Asperti and Ricciotti
+ \cite{AspertiRicciotti12} also consider such a representation, but
+ dismiss it as it complicates their definition for \emph{tape
+ equality}. The reason is that moving the read-write unit one step to
+ the left and then back to the right might change the tape (in case
+ of going over the ``edge''). Therefore they distinguish four types
+ of tapes: one where the tape is empty; another where the read-write
+ unit is on the left edge, respectively right edge, and in the middle
+ of the tape. The reading, writing and moving of the tape is then
+ defined in terms of these four cases. In this way they can keep the
+ tape in a ``normalised'' form, and thus making a left-move followed
+ by a right-move being the identity on tapes. Since we are not using
+ the notion of tape equality, we can get away with the unsymmetric
+ definition above and by using the @{term update} function
+ cover uniformely all cases including the corner cases.
Next we need to define the \emph{states} of a Turing machine. Given
- how little is usually said about how to represent states in informal
+ how little is usually said about how to represent them in informal
presentaions, it might be surprising that in a theorem prover we have
to select carfully a representation. If we use the naive representation
- as a Turing machine consiting of a finite set of states, then we
- will have difficulties composing two Turing machines. We would need
- to somehow combine the two finite sets of states, possibly renaming
- states apart if both machines share states. This renaming can be
- quite cumbersome to reason about. Therefore we made the choice
- of representing a state by a natural number and the states of a
- Turing machine will always consist of the initial segment
+ where a Turing machine consists of a finite set of states, then we
+ will have difficulties composing two Turing machines. In this case we
+ would need to combine two finite sets of states, possibly requiring
+ renaming states apart whenever both machines share states. This
+ renaming can be quite cumbersome to reason about. Therefore we made
+ the choice of 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 number of states
of the machine minus @{text 1}. In doing so we can compose
two Turing machine by ``shifting'' the states of one by an appropriate
@@ -304,20 +307,42 @@
An \emph{instruction} of a Turing machine is a pair consisting of a
natural number (the next state) and an action. A \emph{program} of a Turing
machine is then a list of such pairs. Given a program @{term p}, a state
- and a cell being read by the read-write unnit, we need to fetch
- the corresponding instruction in the program. For this we define
+ and the cell being read by the read-write unit, we need to fetch
+ the corresponding instruction from the program. For this we define
the function @{term fetch}
\begin{center}
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
- @{thm (lhs) fetch_def2(1)[where b=DUMMY]} & @{text "\<equiv>"} & @{thm (rhs) fetch_def2(1)}\\
+ \multicolumn{3}{l}{@{thm fetch_def2(1)[where b=DUMMY]}}\\
@{thm (lhs) fetch_def2(2)} & @{text "\<equiv>"} & \\
- \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) fetch_def2(2)}}\\
+ \multicolumn{3}{@ {\hspace{1cm}}l}{@{text "case nth_of p (2 * s) of"}}\\
+ \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) |"}}\\
+ \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \<Rightarrow> i"}}\\
@{thm (lhs) fetch_def2(3)} & @{text "\<equiv>"} & \\
- \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) fetch_def2(3)}}\\
+ \multicolumn{3}{@ {\hspace{1cm}}l}{@{text "case nth_of p (2 * s + 1) of"}}\\
+ \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) |"}}\\
+ \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \<Rightarrow> i"}}
\end{tabular}
\end{center}
+ start state
+
+ What is tinres? What is it used for?
+
+ \begin{center}
+ @{thm dither_def}
+ \end{center}
+
+
+ A \emph{configuration} @{term c} of a Turing machine is a state together with
+ a tape. If we have a configuration and a program, we can calculate
+ what the next configuration is by fetching the appropriate next state
+ and action from the program. Such a single step of execution can be defined as
+
+ \begin{center}
+ @{thm tstep_def2(1)}\\
+ @{thm tstep_def2(2)}\\
+ \end{center}
For showing the undecidability of the halting problem, we need to consider
two specific Turing machines.