# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1359340737 0
# Node ID f2bda6ba49528593b846b14147df82b2bda459e5
# Parent  b9d0dd18c81e5a0cee478a5424f60a5feba834b6
updated paper

diff -r b9d0dd18c81e -r f2bda6ba4952 Paper/Paper.thy
--- a/Paper/Paper.thy	Sun Jan 27 20:01:13 2013 +0000
+++ b/Paper/Paper.thy	Mon Jan 28 02:38:57 2013 +0000
@@ -26,6 +26,7 @@
   tcopy_loop ("copy\<^bsub>loop\<^esub>") and
   tcopy_end ("copy\<^bsub>end\<^esub>") and
   step0 ("step") and
+  uncomputable.tcontra ("C") and
   steps0 ("steps") and
   exponent ("_\<^bsup>_\<^esup>") and
 (*  abc_lm_v ("lookup") and
@@ -79,6 +80,12 @@
 apply(auto)
 done
 
+lemmas HR1 = 
+  Hoare_plus_halt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?Q2.0="Q\<^isub>2" and ?A="p\<^isub>1" and B="p\<^isub>2"]
+
+lemmas HR2 =
+  Hoare_plus_unhalt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?A="p\<^isub>1" and B="p\<^isub>2"]
+
 (*>*)
 
 section {* Introduction *}
@@ -118,17 +125,16 @@
 
 The only satisfying way out of this problem in a theorem prover based
 on classical logic is to formalise a theory of computability. Norrish
-provided such a formalisation for the HOL. He choose
-the $\lambda$-calculus as the starting point for his formalisation of
-computability theory, because of its ``simplicity'' \cite[Page
-297]{Norrish11}.  Part of his formalisation is a clever infrastructure
-for reducing $\lambda$-terms. He also established the computational
-equivalence between the $\lambda$-calculus and recursive functions.
-Nevertheless he concluded that it would be appealing
- to have formalisations for more operational models of
-computations, such as Turing machines or register machines.  One
-reason is that many proofs in the literature use them.  He noted
-however that \cite[Page 310]{Norrish11}:
+provided such a formalisation for HOL4. He choose the
+$\lambda$-calculus as the starting point for his formalisation because
+of its ``simplicity'' \cite[Page 297]{Norrish11}.  Part of his
+formalisation is a clever infrastructure for reducing
+$\lambda$-terms. He also established the computational equivalence
+between the $\lambda$-calculus and recursive functions.  Nevertheless
+he concluded that it would be appealing to have formalisations for
+more operational models of computations, such as Turing machines or
+register machines.  One reason is that many proofs in the literature
+use them.  He noted however that \cite[Page 310]{Norrish11}:
 
 \begin{quote}
 \it``If register machines are unappealing because of their 
@@ -185,7 +191,7 @@
 our formalisation we follow mainly the proofs from the textbook
 \cite{Boolos87} and found that the description there is quite
 detailed. Some details are left out however: for example, constructing
-the \emph{copy Turing program} is left as an excerise to the reader; also 
+the \emph{copy Turing machine} is left as an excerise to the reader; also 
 \cite{Boolos87} only shows how the universal Turing machine is constructed for Turing
 machines computing unary functions. We had to figure out a way to
 generalise this result to $n$-ary functions. Similarly, when compiling
@@ -315,7 +321,7 @@
 
   \noindent
   We slightly deviate
-  from the presentation in \cite{Boolos87} and \cite{AspertiRicciotti12} 
+  from the presentation in \cite{Boolos87} (and also \cite{AspertiRicciotti12}) 
   by using the @{term Nop} operation; however its use
   will become important when we formalise halting computations and also universal Turing 
   machines.  Given a tape and an action, we can define the
@@ -675,7 +681,7 @@
 
   \noindent
   whose three components are given in Figure~\ref{copy}. To the prove
-  correctness of these Turing machine programs, we introduce the
+  the correctness of Turing machine programs, we introduce the
   notion of total correctness defined in terms of
   \emph{Hoare-triples}, written @{term "{P} p {Q}"}. They are very similar
   to the notion of \emph{realisability} in \cite{AspertiRicciotti12}.  
@@ -684,7 +690,7 @@
   a tape satisfying @{term P} will after some @{text n} steps halt (have
   transitioned into the halting state) with a tape satisfying @{term
   Q}. We also have \emph{Hoare-pairs} of the form @{term "{P} p \<up>"}
-  realising the case that a program @{term p} started with a tape
+  implementing the case that a program @{term p} started with a tape
   satisfying @{term P} will loop (never transition into the halting
   state). Both notion are formally defined as
 
@@ -709,13 +715,13 @@
   
   \noindent
   Like Asperti and Ricciotti with their notion of realisability, we
-  have set up our Hoare-style reasoning so that we can deal explicitly
+  have set up our Hoare-rules so that we can deal explicitly
   with total correctness and non-terminantion, rather than have
   notions for partial correctness and termination. Although the latter
   would allow us to reason more uniformly (only using Hoare-triples),
-  we prefer our definitions because we can derive (below) simple
+  we prefer our definitions because we can derive simple
   Hoare-rules for sequentially composed Turing programs.  In this way
-  we can reason about the correctness of @{term "tcopy_init"}, for
+  we can reason about the correctness of @{term "tcopy_begin"}, for
   example, completely separately from @{term "tcopy_loop"} and @{term
   "tcopy_end"}.
 
@@ -792,44 +798,84 @@
   to produce the standard tape @{term "(DUMMY, <[n, n::nat]>)"} when
   started with @{term "(DUMMY, <[n::nat]>)"}, that is making a copy of
   a value on the tape.  Reasoning about this program is substantially
-  harder than about @{term dither}. To ease the burden, we can prove
-  the following Hoare-rules for sequentially composed programs.
+  harder than about @{term dither}. To ease the burden, we prove
+  the following two Hoare-rules for sequentially composed programs.
 
   \begin{center}
-  \begin{tabular}{@ {}p{3cm}@ {\hspace{9mm}}p{3cm}@ {}}
-  @{thm[mode=Rule] 
-  Hoare_plus_halt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?Q2.0="Q\<^isub>2" and ?A="p\<^isub>1" and B="p\<^isub>2"]}
-  &
-  @{thm[mode=Rule] 
-  Hoare_plus_unhalt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?A="p\<^isub>1" and B="p\<^isub>2"]}
+  \begin{tabular}{@ {\hspace{-10mm}}c@ {\hspace{9mm}}c@ {}}
+  $\inferrule*[Right=@{thm (prem 4) HR1}]
+  {@{thm (prem 1) HR1} \\ @{thm (prem 3) HR1} \\ @{thm (prem 2) HR1}}
+  {@{thm (concl) HR1}}
+  $ &
+  $
+  \inferrule*[Right=@{thm (prem 4) HR2}]
+  {@{thm (prem 1) HR2} \\ @{thm (prem 3) HR2} \\ @{thm (prem 2) HR2}}
+  {@{thm (concl) HR2}}
+  $
   \end{tabular}
   \end{center}
-   
+
   \noindent
-  The first corresponds to the usual Hoare-rule for composition of imperative
-  programs, where @{term "Q\<^isub>1 \<mapsto> P\<^isub>2"} means @{term "Q\<^isub>1"} implies @{term "P\<^isub>2"} for 
-  all tapes @{term "(l, r)"}. The second rule covers the case where rughly the 
-  first program terminates generating a tape for which the second program
-  loops. These are two cases we need in our proof for undecidability.
-  
+  The first corresponds to the usual Hoare-rule for composition of two
+  terminating programs. The premise @{term "Q\<^isub>1 \<mapsto> P\<^isub>2"} means that
+  @{term "Q\<^isub>1"} implies @{term "P\<^isub>2"} for all tapes @{term "(l,
+  r)"}. The second rule covers the case where the first program
+  terminates generating a tape for which the second program loops.
+  The side-condition about @{thm (prem 4) HR2} is needed in both rules
+  in order to ensure that the redirection of the halting and initial
+  state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"} match up correctly.
+
+
   The Hoare-rules above allow us to prove the correctness of @{term tcopy}
   by considering the correctness of @{term "tcopy_begin"}, @{term "tcopy_loop"} 
   and @{term "tcopy_end"} in isolation. We will show some details for the 
   the program @{term "tcopy_begin"}. 
 
 
-  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. copying TM and dithering TM
-
-  correctness of the copying TM
-
   measure for the copying TM, which we however omit.
 
-  halting problem
+  \begin{center}
+  @{thm haltP_def[where lm="ns"]}
+  \end{center}
+
+
+  Undecidability of the halting problem.
+
+  We assume a coding function from Turing machine programs to natural numbers.
+  
+  @{thm (prem 2) uncomputable.h_case} implies
+  @{thm (concl) uncomputable.h_case}
+  
+  @{thm (prem 2) uncomputable.nh_case} implies
+  @{thm (concl) uncomputable.nh_case}
+
+  Then contradiction
+
+  \begin{center}
+  @{term "tcontra"} @{text "\<equiv>"} @{term "(tcopy |+| H) |+| dither"}
+  \end{center}
+
+  Proof
+
+  \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}"}
+   }
+   {@{term "{P\<^isub>1} tcontra {P\<^isub>3}"}}
+  $
+  \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}
 
   Magnus: invariants -- Section 5.4.5 on page 75.
 *}
diff -r b9d0dd18c81e -r f2bda6ba4952 Paper/document/root.tex
--- a/Paper/document/root.tex	Sun Jan 27 20:01:13 2013 +0000
+++ b/Paper/document/root.tex	Mon Jan 28 02:38:57 2013 +0000
@@ -24,7 +24,7 @@
 \definecolor{mygrey}{rgb}{.80,.80,.80}
 
 % mathpatir
-\mprset{sep=0.8em}
+\mprset{sep=0.7em}
 \mprset{center=false}
 \mprset{flushleft=true}
 
diff -r b9d0dd18c81e -r f2bda6ba4952 paper.pdf
Binary file paper.pdf has changed
diff -r b9d0dd18c81e -r f2bda6ba4952 thys/turing_basic.thy
--- a/thys/turing_basic.thy	Sun Jan 27 20:01:13 2013 +0000
+++ b/thys/turing_basic.thy	Mon Jan 28 02:38:57 2013 +0000
@@ -233,6 +233,11 @@
   shows "length (A |+| B) = length A + length B"
 by auto
 
+lemma tm_comp_wf[intro]: 
+  "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)"
+by (auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length tm_comp.simps)
+
+
 lemma tm_comp_step: 
   assumes unfinal: "\<not> is_final (step0 c A)"
   shows "step0 c (A |+| B) = step0 c A"
diff -r b9d0dd18c81e -r f2bda6ba4952 thys/turing_hoare.thy
--- a/thys/turing_hoare.thy	Sun Jan 27 20:01:13 2013 +0000
+++ b/thys/turing_hoare.thy	Mon Jan 28 02:38:57 2013 +0000
@@ -29,10 +29,11 @@
 
 (* halting case *)
 definition
-  Hoare_halt :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" [50, 49] 50)
+  Hoare_halt :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)
 where
   "{P} p {Q} \<equiv> \<forall>tp. P tp \<longrightarrow> (\<exists>n. is_final (steps0 (1, tp) p n) \<and> Q holds_for (steps0 (1, tp) p n))"
 
+
 (* not halting case *)
 definition
   Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" [50, 49] 50)
diff -r b9d0dd18c81e -r f2bda6ba4952 thys/uncomputable.thy
--- a/thys/uncomputable.thy	Sun Jan 27 20:01:13 2013 +0000
+++ b/thys/uncomputable.thy	Mon Jan 28 02:38:57 2013 +0000
@@ -881,11 +881,10 @@
   fix l r
   assume h: "0 < x"
     "inv_end1 x (l, r)"
-  hence "\<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)"
-    apply(rule_tac end_halt, simp_all add: inv_end.simps)
-    done
-  then obtain stp where "is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)" ..
-  moreover have "inv_end x (steps (Suc 0, l, r) (tcopy_end, 0) stp)"
+  then have "\<exists> stp. is_final (steps0 (1, l, r) tcopy_end stp)"
+    by (simp add: end_halt inv_end.simps)
+  then obtain stp where "is_final (steps0 (1, l, r) tcopy_end stp)" ..
+  moreover have "inv_end x (steps0 (1, l, r) tcopy_end stp)"
     apply(rule_tac inv_end_steps)
     using h by(simp_all add: inv_end.simps)
   ultimately show
@@ -893,8 +892,8 @@
     inv_end0 x holds_for steps (1, l, r) (tcopy_end, 0) n"        
     using h
     apply(rule_tac x = stp in exI)
-    apply(case_tac "(steps (Suc 0, l, r) (tcopy_end, 0) stp)", 
-      simp add:  inv_end.simps)
+    apply(case_tac "(steps0 (1, l, r) tcopy_end stp)") 
+    apply(simp add: inv_end.simps)
     done
 qed
 
@@ -909,39 +908,32 @@
 lemma [intro]: "tm_wf (tcopy_end, 0)"
 by (auto simp: tm_wf.simps tcopy_end_def)
 
-lemma [intro]: "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)"
-by (auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length tm_comp.simps)
-
 lemma tcopy_correct1: 
-  "\<lbrakk>x > 0\<rbrakk> \<Longrightarrow> {inv_begin1 x} tcopy {inv_end0 x}"
-proof(simp add: tcopy_def, rule_tac Hoare_plus_halt)
-  show "inv_loop0 x \<mapsto> inv_end1 x"
+  assumes "0 < x"
+  shows "{inv_begin1 x} tcopy {inv_end0 x}"
+proof -
+  have "{inv_begin1 x} tcopy_begin {inv_begin0 x}"
+    by (metis assms init_correct) 
+  moreover
+  have "{inv_loop1 x} tcopy_loop {inv_loop0 x}"
+    by (metis assms loop_correct) 
+  moreover
+  have "inv_begin0 x \<mapsto> inv_loop1 x"
+    by (auto simp: inv_begin0.simps inv_loop1.simps assert_imp_def)
+       (rule_tac x = "Suc 0" in exI, auto)
+  ultimately 
+  have "{inv_begin1 x} (tcopy_begin |+| tcopy_loop) {inv_loop0 x}"
+    by (rule_tac Hoare_plus_halt) (auto)
+  moreover 
+  have "{inv_end1 x} tcopy_end {inv_end0 x}"
+    by (metis assms end_correct) 
+  moreover 
+  have "inv_loop0 x \<mapsto> inv_end1 x"
     by(auto simp: inv_end1.simps inv_loop1.simps assert_imp_def)
-next
-  show "tm_wf (tcopy_begin |+| tcopy_loop, 0)" by auto
-next
-  assume "0 < x"
-  thus "{inv_begin1 x} (tcopy_begin |+| tcopy_loop) {inv_loop0 x}"
-  proof(rule_tac Hoare_plus_halt)
-    show "inv_begin0 x \<mapsto> inv_loop1 x"
-      apply(auto simp: inv_begin0.simps inv_loop1.simps assert_imp_def)
-      apply(rule_tac x = "Suc 0" in exI, auto)
-      done
-  next
-    show "tm_wf (tcopy_begin, 0)" by auto
-  next
-    assume "0 < x"
-    thus "{inv_begin1 x} tcopy_begin {inv_begin0 x}"
-      by(erule_tac init_correct)
-  next
-    assume "0 < x"
-    thus "{inv_loop1 x} tcopy_loop {inv_loop0 x}"
-      by(erule_tac loop_correct)
-  qed
-next
-  assume "0 < x"
-  thus "{inv_end1 x} tcopy_end {inv_end0 x}"
-    by(erule_tac end_correct)
+  ultimately 
+  show "{inv_begin1 x} tcopy {inv_end0 x}"
+    unfolding tcopy_def
+    by (rule_tac Hoare_plus_halt) (auto)
 qed
 
 abbreviation
@@ -949,20 +941,20 @@
 abbreviation
   "post_tcopy n \<equiv> \<lambda>tp. tp= ([Bk], <[n, n::nat]>)"
 
-lemma tcopy_correct2:
+lemma tcopy_correct:
   shows "{pre_tcopy n} tcopy {post_tcopy n}"
 proof -
   have "{inv_begin1 (Suc n)} tcopy {inv_end0 (Suc n)}"
     by (rule tcopy_correct1) (simp)
   moreover
-  have "pre_tcopy n \<mapsto> inv_begin1 (Suc n)" 
-    by (simp add: assert_imp_def tape_of_nl_abv)
+  have "pre_tcopy n = inv_begin1 (Suc n)" 
+    by (auto simp add: tape_of_nl_abv)
   moreover
-  have "inv_end0 (Suc n) \<mapsto> post_tcopy n" 
-    by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv)
+  have "inv_end0 (Suc n) = post_tcopy n" 
+    by (auto simp add: inv_end0.simps tape_of_nl_abv)
   ultimately
   show "{pre_tcopy n} tcopy {post_tcopy n}" 
-    by (rule Hoare_weaken)
+    by simp
 qed
 
 
@@ -1022,7 +1014,7 @@
 
 definition haltP :: "tprog0 \<Rightarrow> nat list \<Rightarrow> bool"
   where
-  "haltP p lm \<equiv> {(\<lambda>tp. tp = ([], <lm>))} p {(\<lambda>tp. (\<exists>k m. tp = (Bk \<up> k,  <m::nat>)))}"
+  "haltP p lm \<equiv> {(\<lambda>tp. tp = ([], <lm>))} p {(\<lambda>tp. (\<exists>k n. tp = (Bk \<up> k,  <n::nat>)))}"
 
 lemma [intro, simp]: "tm_wf0 tcopy"
 by (auto simp: tcopy_def)
@@ -1077,7 +1069,8 @@
 using assms h_case by auto
    
 (* TM that produces the contradiction and its code *)
-abbreviation 
+
+definition
   "tcontra \<equiv> (tcopy |+| H) |+| dither"
 abbreviation
   "code_tcontra \<equiv> code tcontra"
@@ -1106,8 +1099,8 @@
   have first: "{P1} (tcopy |+| H) {P3}" 
   proof (cases rule: Hoare_plus_halt_simple)
     case A_halt (* of tcopy *)
-    show "{P1} tcopy {P2}" unfolding P1_def P2_def
-      by (rule tcopy_correct2)
+    show "{P1} tcopy {P2}" unfolding P1_def P2_def 
+      by (rule tcopy_correct)
   next
     case B_halt (* of H *)
     show "{P2} H {P3}"
@@ -1121,6 +1114,7 @@
   
   (* {P1} tcontra {P3} *)
   have "{P1} tcontra {P3}" 
+    unfolding tcontra_def
     by (rule Hoare_plus_halt_simple[OF first second H_wf])
 
   with assms show "False"
@@ -1142,37 +1136,38 @@
   (* invariants *)
   def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)"
   def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)"
-  def P3 \<equiv> "\<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <0::nat>))"
+  def Q3 \<equiv> "\<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <0::nat>))"
 
   (*
-  {P1} tcopy {P2}  {P2} H {P3} 
+  {P1} tcopy {P2}  {P2} H {Q3} 
   ----------------------------
-     {P1} (tcopy |+| H) {P3}     {P3} dither loops
+     {P1} (tcopy |+| H) {Q3}     {Q3} dither loops
   ------------------------------------------------
                {P1} tcontra loops
   *)
 
   have H_wf: "tm_wf0 (tcopy |+| H)" by auto
 
-  (* {P1} (tcopy |+| H) {P3} *)
-  have first: "{P1} (tcopy |+| H) {P3}" 
+  (* {P1} (tcopy |+| H) {Q3} *)
+  have first: "{P1} (tcopy |+| H) {Q3}" 
   proof (cases rule: Hoare_plus_halt_simple)
     case A_halt (* of tcopy *)
     show "{P1} tcopy {P2}" unfolding P1_def P2_def
-      by (rule tcopy_correct2)
+      by (rule tcopy_correct)
   next
     case B_halt (* of H *)
-    then show "{P2} H {P3}"
-      unfolding P2_def P3_def
+    then show "{P2} H {Q3}"
+      unfolding P2_def Q3_def
       by (rule H_unhalt_inv[OF assms])
   qed (simp)
 
   (* {P3} dither loops *)
-  have second: "{P3} dither \<up>" unfolding P3_def 
+  have second: "{Q3} dither \<up>" unfolding Q3_def 
     by (rule dither_loops)
   
   (* {P1} tcontra loops *)
   have "{P1} tcontra \<up>" 
+    unfolding tcontra_def
     by (rule Hoare_plus_unhalt_simple[OF first second H_wf])
 
   with assms show "False"