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

diff -r f2bda6ba4952 -r aeaf1374dc67 Paper/Paper.thy
--- a/Paper/Paper.thy	Mon Jan 28 02:38:57 2013 +0000
+++ b/Paper/Paper.thy	Tue Jan 29 12:37:06 2013 +0000
@@ -81,10 +81,10 @@
 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"]
+  Hoare_plus_halt_simple[where ?P1.0="P" and ?P2.0="Q" and ?P3.0="R\<iota>" 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"]
+  Hoare_plus_unhalt_simple[where ?P1.0="P" and ?P2.0="Q" and ?A="p\<^isub>1" and B="p\<^isub>2"]
 
 (*>*)
 
@@ -180,7 +180,7 @@
 %Turing machines.
 
 We are not the first who formalised Turing machines: we are aware 
-of the preliminary work by Asperti and Ricciotti
+of the work by Asperti and Ricciotti
 \cite{AspertiRicciotti12}. They describe a complete formalisation of
 Turing machines in the Matita theorem prover, including a universal
 Turing machine. However, they do \emph{not} formalise the undecidability of the 
@@ -637,8 +637,8 @@
   \end{scope}
   \end{tikzpicture}\\[-8mm]\mbox{} 
   \end{center}
-  \caption{The components of the \emph{copy Turing machine} (above). If started 
-  with the tape @{term "([], <[2::nat]>)"} the first machine appends @{term "[Bk, Oc]"} at 
+  \caption{The three components of the \emph{copy Turing machine} (above). If started 
+  (below) with the tape @{term "([], <[2::nat]>)"} the first machine appends @{term "[Bk, Oc]"} at 
   the end of the right tape; the second then ``moves'' all @{term Oc}s except the 
   first from the beginning of the tape to the end; the third ``refills'' the original 
   block of @{term "Oc"}s. The resulting tape is @{term "([Bk], <[2::nat, 2::nat]>)"}.}
@@ -662,8 +662,8 @@
   \noindent
   A standard tape is then of the form @{text "(Bk\<^isup>l,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle>)"} for some @{text l} 
   and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the 
-  leftmost @{term "Oc"} on the tape. Note also that @{text 0} is represented by
-  a single filled cell, @{text 1} by two filled cells and so on.
+  leftmost @{term "Oc"} on the tape. Note also that the natural number @{text 0} 
+  is represented by a single filled cell on a standard tape, @{text 1} by two filled cells and so on.
 
   Before we can prove the undecidability of the halting problem for our
   Turing machines, we need to analyse two concrete Turing machine
@@ -728,7 +728,8 @@
   It is realatively straightforward to prove that the Turing program 
   @{term "dither"} shown in \eqref{dither} is correct. This program
   should be the ``identity'' when started with a standard tape representing 
-  @{text "1"} but loop when started with @{text 0} instead.
+  @{text "1"} but loop when started with @{text 0} instead, as pictured 
+  below.
 
 
   \begin{center}
@@ -802,14 +803,14 @@
   the following two Hoare-rules for sequentially composed programs.
 
   \begin{center}
-  \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}}
+  \begin{tabular}{@ {\hspace{-10mm}}c@ {\hspace{14mm}}c@ {}}
+  $\inferrule*[Right=@{thm (prem 3) HR1}]
+  {@{thm (prem 1) 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}}
+  \inferrule*[Right=@{thm (prem 3) HR2}]
+  {@{thm (prem 1) HR2} \\ @{thm (prem 2) HR2}}
   {@{thm (concl) HR2}}
   $
   \end{tabular}
@@ -817,18 +818,16 @@
 
   \noindent
   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
+  terminating programs. The second rule is for cases 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
+  The side-condition about @{thm (prem 3) 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 
+  and @{term "tcopy_end"} in isolation. We will show the details for the 
   the program @{term "tcopy_begin"}. 
 
 
diff -r f2bda6ba4952 -r aeaf1374dc67 Paper/document/root.tex
--- a/Paper/document/root.tex	Mon Jan 28 02:38:57 2013 +0000
+++ b/Paper/document/root.tex	Tue Jan 29 12:37:06 2013 +0000
@@ -24,7 +24,7 @@
 \definecolor{mygrey}{rgb}{.80,.80,.80}
 
 % mathpatir
-\mprset{sep=0.7em}
+\mprset{sep=0.9em}
 \mprset{center=false}
 \mprset{flushleft=true}
 
diff -r f2bda6ba4952 -r aeaf1374dc67 paper.pdf
Binary file paper.pdf has changed
diff -r f2bda6ba4952 -r aeaf1374dc67 thys/turing_hoare.thy
--- a/thys/turing_hoare.thy	Mon Jan 28 02:38:57 2013 +0000
+++ b/thys/turing_hoare.thy	Tue Jan 29 12:37:06 2013 +0000
@@ -36,7 +36,7 @@
 
 (* not halting case *)
 definition
-  Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" [50, 49] 50)
+  Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" 50)
 where
   "{P} p \<up> \<equiv> \<forall>tp. P tp \<longrightarrow> (\<forall> n . \<not> (is_final (steps0 (1, tp) p n)))"
 
diff -r f2bda6ba4952 -r aeaf1374dc67 thys/uncomputable.thy
--- a/thys/uncomputable.thy	Mon Jan 28 02:38:57 2013 +0000
+++ b/thys/uncomputable.thy	Tue Jan 29 12:37:06 2013 +0000
@@ -103,47 +103,47 @@
 apply(rule_tac inv_begin_step, simp_all)
 done
 
-fun init_state :: "config \<Rightarrow> nat"
+fun begin_state :: "config \<Rightarrow> nat"
   where
-  "init_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
+  "begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
 
-fun init_step :: "config \<Rightarrow> nat"
+fun begin_step :: "config \<Rightarrow> nat"
   where
-  "init_step (s, l, r) = 
+  "begin_step (s, l, r) = 
         (if s = 2 then length r else
          if s = 3 then (if r = [] \<or> r = [Bk] then 1 else 0) else
          if s = 4 then length l 
          else 0)"
 
-fun init_measure :: "config \<Rightarrow> nat \<times> nat"
+fun begin_measure :: "config \<Rightarrow> nat \<times> nat"
   where
-  "init_measure c = (init_state c, init_step c)"
+  "begin_measure c = (begin_state c, begin_step c)"
 
 
 definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set"
   where
   "lex_pair \<equiv> less_than <*lex*> less_than"
 
-definition init_LE :: "(config \<times> config) set"
+definition begin_LE :: "(config \<times> config) set"
   where
-  "init_LE \<equiv> (inv_image lex_pair init_measure)"
+  "begin_LE \<equiv> (inv_image lex_pair begin_measure)"
 
 lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]"
 by (case_tac r, auto, case_tac a, auto)
 
 
-lemma wf_begin_le: "wf init_LE"
-by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def)
+lemma wf_begin_le: "wf begin_LE"
+by(auto intro:wf_inv_image simp:begin_LE_def lex_pair_def)
 
-lemma init_halt: 
+lemma begin_halt: 
   "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (Suc 0, [], Oc\<up>x) tcopy_begin stp)"
-proof(rule_tac LE = init_LE in halt_lemma) 
-  show "wf init_LE" by(simp add: wf_begin_le)
+proof(rule_tac LE = begin_LE in halt_lemma) 
+  show "wf begin_LE" by(simp add: wf_begin_le)
 next
   assume h: "0 < x"
   show "\<forall>n. \<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow>
         (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), 
-            steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> init_LE"
+            steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
   proof(rule_tac allI, rule_tac impI)
     fix n
     assume a: "\<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n)"
@@ -157,25 +157,25 @@
     moreover hence "inv_begin x (s, l, r)" 
       using c b by simp
     ultimately show "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), 
-      steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> init_LE"
+      steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
       using a 
     proof(simp del: inv_begin.simps)
       assume "inv_begin x (s, l, r)" "0 < s"
-      thus "(step (s, l, r) (tcopy_begin, 0), s, l, r) \<in> init_LE"
-        apply(auto simp: init_LE_def lex_pair_def step.simps tcopy_begin_def numeral split: if_splits)
+      thus "(step (s, l, r) (tcopy_begin, 0), s, l, r) \<in> begin_LE"
+        apply(auto simp: begin_LE_def lex_pair_def step.simps tcopy_begin_def numeral split: if_splits)
         apply(case_tac r, auto, case_tac a, auto)
         done
     qed
   qed
 qed
     
-lemma init_correct: 
+lemma begin_correct: 
   "0 < x \<Longrightarrow> {inv_begin1 x} tcopy_begin {inv_begin0 x}"
 proof(rule_tac Hoare_haltI)
   fix l r
   assume h: "0 < x" "inv_begin1 x (l, r)"
   hence "\<exists> stp. is_final (steps0 (Suc 0, [], Oc \<up> x) tcopy_begin stp)"
-    by (rule_tac init_halt)    
+    by (rule_tac begin_halt)    
   then obtain stp where "is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)" ..
   moreover have "inv_begin x (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)"
     apply(rule_tac inv_begin_steps)
@@ -913,7 +913,7 @@
   shows "{inv_begin1 x} tcopy {inv_end0 x}"
 proof -
   have "{inv_begin1 x} tcopy_begin {inv_begin0 x}"
-    by (metis assms init_correct) 
+    by (metis assms begin_correct) 
   moreover
   have "{inv_loop1 x} tcopy_loop {inv_loop0 x}"
     by (metis assms loop_correct) 
@@ -970,10 +970,10 @@
   "dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] "
 
 (* invariants of dither *)
-abbreviation
+abbreviation (input)
   "dither_halt_inv \<equiv> \<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <1::nat>))"
 
-abbreviation
+abbreviation (input)
   "dither_unhalt_inv \<equiv> \<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <0::nat>))"
 
 lemma dither_loops_aux: 
@@ -1083,7 +1083,7 @@
   (* 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, <1::nat>))"
+  def P3 \<equiv> "\<lambda>tp. \<exists>n. tp = (Bk \<up> n, <1::nat>)"
 
   (*
   {P1} tcopy {P2}  {P2} H {P3} 
@@ -1136,7 +1136,7 @@
   (* invariants *)
   def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)"
   def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)"
-  def Q3 \<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 {Q3}