# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1359894240 0
# Node ID 4635641e77cbdd522de1741be89cf31206ca8ece
# Parent  36a1a09113971adc5db4ab9bba820cd832b8a98b
updated paper

diff -r 36a1a0911397 -r 4635641e77cb Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Feb 01 14:54:47 2013 +0000
+++ b/Paper/Paper.thy	Sun Feb 03 12:24:00 2013 +0000
@@ -7,6 +7,7 @@
 hide_const (open) s 
 *)
 
+
 hide_const (open) Divides.adjust
 
 abbreviation
@@ -14,6 +15,43 @@
 
 consts DUMMY::'a
 
+
+(* THEOREMS *)
+notation (Rule output)
+  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+
+syntax (Rule output)
+  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
+
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
+  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
+
+  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+
+notation (Axiom output)
+  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
+
+notation (IfThen output)
+  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+syntax (IfThen output)
+  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+
+notation (IfThenNoBox output)
+  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+syntax (IfThenNoBox output)
+  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+  "_asm" :: "prop \<Rightarrow> asms" ("_")
+
+
+context uncomputable
+begin
+
 notation (latex output)
   Cons ("_::_" [48,47] 48) and
   set ("") and
@@ -26,7 +64,8 @@
   tcopy_loop ("cloop") and
   tcopy_end ("cend") and
   step0 ("step") and
-  uncomputable.tcontra ("tcontra") and
+  tcontra ("contra") and
+  code_tcontra ("code contra") and
   steps0 ("steps") and
   exponent ("_\<^bsup>_\<^esup>") and
   haltP ("halts") and 
@@ -83,38 +122,6 @@
 
 declare [[show_question_marks = false]]
 
-(* THEOREMS *)
-notation (Rule output)
-  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
-
-syntax (Rule output)
-  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
-
-  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
-  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
-
-  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
-
-notation (Axiom output)
-  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
-
-notation (IfThen output)
-  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
-syntax (IfThen output)
-  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
-  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
-  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
-
-notation (IfThenNoBox output)
-  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
-syntax (IfThenNoBox output)
-  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
-  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
-  "_asm" :: "prop \<Rightarrow> asms" ("_")
-
 lemma nats2tape:
   shows "<([]::nat list)> = []"
   and "<[n]> = <n>"
@@ -143,6 +150,7 @@
   shows "inv_begin0 n (l, r) = (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc]))"
 using assms by auto
 
+
 (*>*)
 
 section {* Introduction *}
@@ -173,7 +181,7 @@
 matter whether @{text P} is constructed by computable means. We hit on
 this limitation previously when we mechanised the correctness proofs
 of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, but
-were unable to formalise arguments about decidability.
+were unable to formalise arguments about decidability or undecidability.
 
 %The same problem would arise if we had formulated
 %the algorithms as recursive functions, because internally in
@@ -583,7 +591,7 @@
   \noindent Recall our definition of @{term fetch} (shown in
   \eqref{fetch}) with the default value for the @{text 0}-state. In
   case a Turing program takes according to the usual textbook
-  definition \cite{Boolos87} less than @{text n} steps before it
+  definition, say \cite{Boolos87}, less than @{text n} steps before it
   halts, then in our setting the @{term steps}-evaluation does not
   actually halt, but rather transitions to the @{text 0}-state (the
   final state) and remains there performing @{text Nop}-actions until
@@ -786,7 +794,7 @@
   \noindent
   where
   @{term "P' \<mapsto> P"} stands for the fact that for all tapes @{term "tp"},
-  @{term "P' tp"} implies @{term "P tp"}.
+  @{term "P' tp"} implies @{term "P tp"} (similarly for @{text "Q"} and @{text "Q'"}).
 
   Like Asperti and Ricciotti with their notion of realisability, we
   have set up our Hoare-rules so that we can deal explicitly
@@ -994,11 +1002,11 @@
 
   \noindent 
   where we assume @{text "0 < n"} (similar resoning is needed for
-  @{term tcopy_loop} and @{term tcopy_end}). Since the invariant of
+  the Hoare-triples for @{term tcopy_loop} and @{term tcopy_end}). Since the invariant of
   the halting state of @{term tcopy_begin} implies the invariant of
   the starting state of @{term tcopy_loop}, that is @{term "inv_begin0
   n \<mapsto> inv_loop1 n"} holds, and also @{term "inv_loop0 n = inv_end1
-  n"}, we can derive using our Hoare-rules for the correctness 
+  n"}, we can derive the following Hoare-triple for the correctness 
   of @{term tcopy}:
 
   \begin{center}
@@ -1007,7 +1015,7 @@
 
   \noindent
   That means if we start with a tape of the form @{term "([], <n::nat>)"} then 
-  @{term tcopy} will halt with the tape \mbox{@{term "([Bk], <(n::nat, n::nat)>)"}}.
+  @{term tcopy} will halt with the tape \mbox{@{term "([Bk], <(n::nat, n::nat)>)"}}, as desired.
 
   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
@@ -1026,7 +1034,7 @@
   general whether a Turing machine program halts (answer either @{text
   0} for halting and @{text 1} for looping). Given our correctness
   proofs for @{term dither} and @{term tcopy} shown above, this
-  non-existence is relatively straightforward to establish. We first
+  non-existence is now relatively straightforward to establish. We first
   assume there is a coding function, written @{term "code M"}, which
   represents a Turing machine @{term "M"} as a natural number.  No
   further assumptions are made about this coding function. Suppose a
@@ -1034,8 +1042,8 @@
   standard tape @{term "([Bk], <(code M, ns)>)"} returns @{text 0},
   respectively @{text 1}, depending on whether @{text M} halts when
   started with the input tape containing @{term "<ns>"}.  This
-  assumption is formalised as follows---for all @{term M} and natural
-  numbers @{term ns}:
+  assumption is formalised as follows---for all @{term M} and all lists of
+  natural numbers @{term ns}:
 
   \begin{center}
   \begin{tabular}{r}
@@ -1051,34 +1059,69 @@
   The contradiction can be derived using the following Turing machine
 
   \begin{center}
-  @{term "tcontra"} @{text "\<equiv>"} @{term "(tcopy |+| H) |+| dither"}
+  @{thm tcontra_def}
+  \end{center}
+
+  \noindent
+  Suppose @{thm (prem 1) "tcontra_halt"}. Given the invariants 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\<^isub>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>)"}
+  \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}"}}
+    {@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}}
+    \\ @{term "{P\<^isub>3} dither \<up>"}
+   }
+   {@{term "{P\<^isub>1} tcontra \<up>"}}
+  $}
+  \end{tabular}
+  \end{tabular}
   \end{center}
 
   \noindent
-  Let us assume @{thm (prem 2) "uncomputable.tcontra_halt"}
-  Proof
+  This Hoare-pair contradicts our assumption that @{term tcontra} started
+  with @{term "<(code tcontra)>"} halts.
+
+  Suppose @{thm (prem 1) "tcontra_unhalt"}. Again given the invariants on the 
+  left, we can derive the Hoare-triple for @{term tcontra} on the right.
 
-  \begin{center}
-  $\inferrule*{
-    \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {P\<^isub>3}"}}
-    {@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}}
-    \\ @{term "{P\<^isub>3} dither {P\<^isub>3}"}
+  \begin{center}\small
+  \begin{tabular}{@ {}c@ {\hspace{-17mm}}c@ {}}
+  \begin{tabular}[t]{@ {}l@ {}}
+  @{term "Q\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
+  @{term "Q\<^isub>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>)"}
+  \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}"}}
+    {@{term "{Q\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}}
+    \\ @{term "{Q\<^isub>3} dither {Q\<^isub>3}"}
    }
-   {@{term "{P\<^isub>1} tcontra {P\<^isub>3}"}}
-  $
+   {@{term "{Q\<^isub>1} tcontra {Q\<^isub>3}"}}
+  $}
+  \end{tabular}
+  \end{tabular}
   \end{center}
 
-  \begin{center}
-  $\inferrule*{
-    \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {Q\<^isub>3}"}}
-    {@{term "{P\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}}
-    \\ @{term "{Q\<^isub>3} dither \<up>"}
-   }
-   {@{term "{P\<^isub>1} tcontra \<up>"}}
-  $
-  \end{center}
+  \noindent
+  This time the Hoare-triple states that @{term tcontra} terminates 
+  with the ``output'' @{term "<(1::nat)>"}. In both case we come
+  to an contradiction, which means we have to abondon our assumption 
+  that there exists a Turing machine @{term H} which can decide 
+  whether Turing machines terminate.
+  
 
-  Magnus: invariants -- Section 5.4.5 on page 75.
+
 *}
 
 
@@ -1204,6 +1247,9 @@
   a new tape corresponding to the value @{term l} (the number of @{term Oc}s
   clustered on the output tape).
 
+
+  
+  Magnus: invariants -- Section 5.4.5 on page 75.
 *}
 
 
@@ -1220,4 +1266,5 @@
 
 (*<*)
 end
+end
 (*>*)
\ No newline at end of file
diff -r 36a1a0911397 -r 4635641e77cb paper.pdf
Binary file paper.pdf has changed
diff -r 36a1a0911397 -r 4635641e77cb thys/uncomputable.thy
--- a/thys/uncomputable.thy	Fri Feb 01 14:54:47 2013 +0000
+++ b/thys/uncomputable.thy	Sun Feb 03 12:24:00 2013 +0000
@@ -1154,6 +1154,7 @@
     unfolding Hoare_halt_def Hoare_unhalt_def
     by (auto simp add: tape_of_nl_abv)
 qed
+
       
 text {*
   @{text "False"} can finally derived.