
diff -r c5e3007fed2a -r cb8754a0568a Paper.thy
--- 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.




