
diff -r 01f688735b9b -r 2cae8a39803e Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Jan 31 11:35:16 2013 +0000
+++ b/Paper/Paper.thy	Fri Feb 01 01:34:37 2013 +0000
@@ -22,16 +22,14 @@
   update2 ("update") and
   tm_wf0 ("wf") and
   (*is_even ("iseven") and*)
-  tcopy_begin ("copy\<^bsub>begin\<^esub>") and
-  tcopy_loop ("copy\<^bsub>loop\<^esub>") and
-  tcopy_end ("copy\<^bsub>end\<^esub>") and
+  tcopy_begin ("cbegin") and
+  tcopy_loop ("cloop") and
+  tcopy_end ("cend") and
   step0 ("step") and
-  uncomputable.tcontra ("C") and
+  uncomputable.tcontra ("tcontra") and
   steps0 ("steps") and
   exponent ("_\<^bsup>_\<^esup>") and
-(*  abc_lm_v ("lookup") and
-  abc_lm_s ("set") and*)
-  haltP ("stdhalt") and 
+  haltP ("halts") and 
   tcopy ("copy") and 
   tape_of ("\<langle>_\<rangle>") and 
   tm_comp ("_ \<oplus> _") and 
@@ -41,7 +39,12 @@
   inv_begin2 ("I\<^isub>2") and
   inv_begin3 ("I\<^isub>3") and
   inv_begin4 ("I\<^isub>4") and 
-  inv_begin ("I\<^bsub>begin\<^esub>")
+  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
+  measure_begin_step ("M\<^bsub>cbegin\<^esub>")
 
  
 lemma inv_begin_print:
@@ -71,6 +74,13 @@
 done
 
 
+lemma measure_begin_print:
+  shows "s = 2 \<Longrightarrow> measure_begin_step (s, l, r) = length r" and
+        "s = 3 \<Longrightarrow> measure_begin_step (s, l, r) = (if r = [] \<or> r = [Bk] then 1 else 0)" and
+        "s = 4 \<Longrightarrow> measure_begin_step (s, l, r) = length l" and 
+        "s \<notin> {2,3,4} \<Longrightarrow> measure_begin_step (s, l, r) = 0"
+by (simp_all)
+
 declare [[show_question_marks = false]]
 
 (* THEOREMS *)
@@ -900,20 +910,28 @@
 
   \begin{figure}[t]
   \begin{center}
-  \begin{tabular}{@ {}lcl@ {\hspace{-2cm}}l@ {}}
-  @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
-                                &             & @{thm (rhs) inv_begin02} \\
+  \begin{tabular}{@ {}lcl@ {\hspace{-0.5cm}}l@ {}}
+  \hline
   @{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\
   @{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\
   @{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\
   @{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}\\
+  @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
+                                &             & @{thm (rhs) inv_begin02}\smallskip \\
+   \hline
   @{thm (lhs) inv_loop1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop1_loop.simps} @{text "\<or>"}\\
-                               &             & @{thm (rhs) inv_loop1_exit.simps}\\
-  @{thm (lhs) inv_loop0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop0.simps}\\
+                               &             & @{thm (rhs) inv_loop1_exit.simps} & (starting state)\\
+  @{thm (lhs) inv_loop0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop0.simps}& (halting state)\smallskip\\
+   \hline
+  @{thm (lhs) inv_end1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end1.simps} & (starting state)\\
+  @{thm (lhs) inv_end0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\
+  \hline
   \end{tabular}
   \end{center}
-  \caption{The invariants for each state of @{term tcopy_begin}. They depend on
-  the number @{term n} of @{term Oc}s with which this Turing machine is started.}\label{invbegin}
+  \caption{The invariants @{term inv_begin0},\ldots,@{term inv_begin4} for the states of 
+  @{term tcopy_begin}. Below, the invariants for the starting and halting states of
+  @{term tcopy_loop} and @{term tcopy_end}. In each invariant the parameter @{term n} stands for the number
+  of @{term Oc}s with which the Turing machine is started.}\label{invbegin}
   \end{figure}
 
   \begin{center}
@@ -932,41 +950,90 @@
   This invariant depends on @{term n} representing the number of
   @{term Oc}s (or encoded number) on the tape. It is not hard (26
   lines of automated proof script) to show that for @{term "n >
-  (0::nat)"} this invariant is preserved under computation rules
-  @{term step} and @{term steps}.
+  (0::nat)"} this invariant is preserved under the computation rules
+  @{term step} and @{term steps}. This gives us partial correctness
+  for @{term "tcopy_begin"}. 
 
-  measure for the copying TM, which we however omit.
+  We next need to show that @{term "tcopy_begin"} terminates. For this
+  we introduce lexicographically ordered pairs @{term "(n, m)"}
+  derived from configurations @{text "(s, (l, r))"}: @{text n} stands
+  for the state ordered according to how @{term tcopy_begin} executes
+  them, that is @{text "1 > 2 > 3 > 4 > 0"}; @{term m} is calculated
+  according to the measure function:
 
-  
   \begin{center}
-  @{thm begin_correct}\\
-  @{thm loop_correct}\\
-  @{thm end_correct}
+  \begin{tabular}{rcl}
+  @{term measure_begin_step}@{text "(s, (l, r))"} & @{text "\<equiv>"} & 
+  @{text "if"} @{thm (prem 1) measure_begin_print(1)} @{text then} @{thm (rhs) measure_begin_print(1)}\\
+  & & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(2)} @{text then} @{thm (rhs) measure_begin_print(2)} \\
+ & & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(3)} @{text then} @{thm (rhs) measure_begin_print(3)}\\
+  & & @{text else} @{thm (rhs) measure_begin_print(4)}\\
+  \end{tabular}
+  \end{center}
+  
+  \noindent
+  With this in place, we can show that for every starting tape of the
+  form @{term "([], Oc \<up> n)"} with @{term "n > (0::nat)"}, the Turing
+  machine @{term "tcopy_begin"} will halt. Taking this and the partial
+  correctness proof together we obtain for @{term tcopy_begin} (similar 
+  resoning is needed for @{term tcopy_loop} and @{term tcopy_end}):
+   
+
+  \begin{center}
+  @{thm (concl) begin_correct}\hspace{6mm}
+  @{thm (concl) loop_correct}\hspace{6mm}
+  @{thm (concl) end_correct}
   \end{center}
 
+  \noindent 
+  where we assume @{text "0 < n"}. Since @{term "inv_begin0 n \<mapsto> inv_loop1 n"} holds
+  and @{term "inv_loop0 n = inv_end1 n"}, we can derive using our Hoare-rules
+  the correctness of @{term tcopy}
 
+  \begin{center}
+  @{thm tcopy_correct}
+  \end{center}
+
+  Finally, we are in the position to prove the undecidability of the halting problem.
+  A program @{term p} started with a standard tape containing the (encoded) numbers
+  @{term ns} will \emph{halt} with a standard tape containging a single (encoded) 
+  number is defined as
 
   \begin{center}
   @{thm haltP_def}
   \end{center}
 
-
-  Undecidability of the halting problem.
-
-  We assume a coding function from Turing machine programs to natural numbers.
-  
+  \noindent
+  This means we considering only Turing machine programs representing functions that take 
+  some numbers as input and produce a single number as output. There is no Turing
+  machine that can decide the halting problem (answer @{text 0} for halting and 
+  @{text 1} for looping). Given our correctness proofs for @{term dither} and @{term tcopy} 
+  this non-existence is relatively straightforward to establish. We first assume there is a coding 
+  function, written @{term code}, from Turing machine programs to natural numbers.
+  Suppose a Turing machine @{term H} exists such that if started with the standard 
+  tape @{term "([Bk], <(code M, ns)>)"} returns @{text 0} or @{text 1} depending
+  on whether @{text M} halts when started with the input tape containing @{term "<ns>"}.
+  This is formalised as follows
+ 
+  \begin{center}
+  \begin{tabular}{r}
   @{thm (prem 2) uncomputable.h_case} implies
-  @{thm (concl) uncomputable.h_case}
+  @{thm (concl) uncomputable.h_case}\\
   
   @{thm (prem 2) uncomputable.nh_case} implies
   @{thm (concl) uncomputable.nh_case}
+  \end{tabular}
+  \end{center}
 
-  Then contradiction
+  \noindent
+  The contradiction can be derived using the following Turing machine
 
   \begin{center}
   @{term "tcontra"} @{text "\<equiv>"} @{term "(tcopy |+| H) |+| dither"}
   \end{center}
 
+  \noindent
+  Let us assume @{thm (prem 2) "uncomputable.tcontra_halt"}
   Proof
 
   \begin{center}




