--- a/Paper.thy	Thu Jan 10 08:28:25 2013 +0000
+++ b/Paper.thy	Thu Jan 10 08:58:31 2013 +0000
@@ -36,12 +36,15 @@
 apply(auto split: taction.splits simp add: new_tape.simps)
 done
 
+
+abbreviation 
+  "read r == if (r = []) then Bk else hd r"
+
 lemma tstep_def2:
-  shows "tstep (s, l, []) p == (let (ac, ns) = fetch p s Bk in (ns, new_tape ac (l, [])))"
-  and "tstep (s, l, x#xs) p == (let (ac, ns) = fetch p s x in (ns, new_tape ac (l, x#xs)))"
+  shows "tstep (s, l, r) p == (let (a, s') = fetch p s (read r) in (s', new_tape a (l, r)))"
 apply -
 apply(rule_tac [!] eq_reflection)
-by (auto split: prod.split list.split simp add: tstep.simps)
+by (auto split: if_splits prod.split list.split simp add: tstep.simps)
 
 consts DUMMY::'a
 
@@ -49,6 +52,8 @@
   Cons ("_::_" [78,77] 73) and
   W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and
   W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
+  tstep ("step") and
+  steps ("nsteps") and
   DUMMY  ("\<^raw:\mbox{$\_$}>")
 
 declare [[show_question_marks = false]]
@@ -306,8 +311,8 @@
   two Turing machine by ``shifting'' the states of one by an appropriate
   amount to a higher segment.
 
-  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
+  An \emph{instruction} @{term i} of a Turing machine is a pair consisting of a
+  natural number (the next state) and an action. A \emph{program} @{term p} of a Turing
   machine is then a list of such pairs. Given a program @{term p}, a state
   and the cell being read by the read-write unit, we need to fetch
   the corresponding instruction from the program. For this we define 
@@ -337,20 +342,44 @@
 
 
   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
+  a tape. This is written as the triple @{term "(s, l, r)"}. 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}
+
+  No evaluator in HOL, because of totality.
+
+  \begin{center}
+  @{thm steps.simps(1)}\\
+  @{thm steps.simps(2)}\\
   \end{center}
 
+  \emph{well-formedness} of a Turing program
+
+  programs halts
+
+  shift and change of a p
+
+  composition of two ps
+
+  assertion holds for all tapes
+
+  Hoare rule for composition
+
   For showing the undecidability of the halting problem, we need to consider
-  two specific Turing machines.
-  
+  two specific Turing machines. copying TM and dithering TM
+
+  correctness of the copying TM
 
-  No evaluator in HOL, because of totality.
+  measure for the copying TM, which we however omit.
+
+  standard configuration
+
+  halting problem
 *}
 
 section {* Abacus Machines *}