--- a/Paper/Paper.thy	Sun Jan 27 15:46:32 2013 +0000
+++ b/Paper/Paper.thy	Sun Jan 27 17:15:38 2013 +0000
@@ -34,7 +34,7 @@
   tcopy ("copy") and 
   tape_of ("\<langle>_\<rangle>") and 
   tm_comp ("_ \<oplus> _") and 
-  DUMMY  ("\<^raw:\mbox{$\_$}>")
+  DUMMY  ("\<^raw:\mbox{$\_\!\_\,$}>")
 
 declare [[show_question_marks = false]]
 
@@ -315,7 +315,8 @@
 
   \noindent
   We slightly deviate
-  from the presentation in \cite{Boolos87} by using the @{term Nop} operation; however its use
+  from the presentation in \cite{Boolos87} and \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
   following tape updating function:
@@ -522,9 +523,7 @@
   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
-  @{text n} is reached. This is different from the setup in 
-  \cite{AspertiRicciotti12} where an option is returned once a final 
-  state is reached.
+  @{text n} is reached. 
   
   \begin{figure}[t]
   \begin{center}
@@ -668,11 +667,11 @@
   we need to prove correct is the @{term dither} program shown in \eqref{dither} 
   and the other program is @{term "tcopy"} defined as
 
-  \begin{center}
-  \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+  \begin{equation}
+  \mbox{\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
   @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def}
-  \end{tabular}
-  \end{center}
+  \end{tabular}}\label{tcopy}
+  \end{equation}
 
   \noindent
   whose three components are given in Figure~\ref{copy}. To the prove
@@ -776,7 +775,7 @@
   \end{center}
 
   \noindent
-  We can prove the following formal statements
+  We can prove the following Hoare-statements:
  
   \begin{center}
   \begin{tabular}{l}
@@ -786,19 +785,37 @@
   \end{center}
 
   \noindent
-  {\it unfold} The first states that on a tape @{term "(Bk \<up> n,  [Oc, Oc])"}
-  halts in tree steps leaving the tape unchanged. In the other states
-  that @{term dither} started with tape @{term "(Bk \<up> n,  [Oc])"} loops.
-  
+  The first is by a simple calculation. The second is by induction on the
+  number of steps we can perform starting from the input tape.
 
+  The purpose of the @{term tcopy} program defined in \eqref{tcopy} is
+  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.
 
-  In the following we will consider the following Turing machine program
-  that makes a copies a value on the tape.
-
+  \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"]}
+  \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 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
@@ -813,21 +830,10 @@
   measure for the copying TM, which we however omit.
 
   halting problem
+
+  Magnus: invariants -- Section 5.4.5 on page 75.
 *}
 
-text {*
-  \begin{center}
-  \begin{tabular}{@ {}p{3cm}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"]}
-  \end{tabular}
-  \end{center}
-
-
-*}
 
 section {* Abacus Machines *}
 

Binary file paper.pdf has changed

--- a/thys/uncomputable.thy	Sun Jan 27 15:46:32 2013 +0000
+++ b/thys/uncomputable.thy	Sun Jan 27 17:15:38 2013 +0000
@@ -49,7 +49,7 @@
                 (R, 2), (R, 2), (L, 5), (W0, 4),
                 (R, 0), (L, 5)]"
 
-definition 
+idefinition 
   tcopy :: "instr list"
 where
   "tcopy \<equiv> (tcopy_begin |+| tcopy_loop) |+| tcopy_end"
@@ -81,16 +81,13 @@
          if s = 4 then inv_begin4 n (l, r) 
          else False)"
 
-
-
 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> 
   \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia"
 apply(rule_tac x = "Suc i" in exI, simp)
 done
 
 lemma inv_begin_step: 
-  "\<lbrakk>inv_begin x cf; x > 0\<rbrakk>
- \<Longrightarrow> inv_begin x (step cf (tcopy_begin, 0))"
+  "\<lbrakk>inv_begin x cf; x > 0\<rbrakk> \<Longrightarrow> inv_begin x (step cf (tcopy_begin, 0))"
 unfolding tcopy_begin_def
 apply(case_tac cf)
 apply(auto simp: inv_begin.simps step.simps tcopy_begin_def numeral split: if_splits)
@@ -139,7 +136,7 @@
 by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def)
 
 lemma init_halt: 
-  "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)"
+  "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)
 next
@@ -173,13 +170,12 @@
 qed
     
 lemma init_correct: 
-  "x > 0 \<Longrightarrow> {inv_begin1 x} tcopy_begin {inv_begin0 x}"
+  "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 (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)"
-    by(erule_tac init_halt)    
+  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)    
   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)
@@ -1004,7 +1000,7 @@
 
 
 lemma dither_halts_aux: 
-  shows "steps0 (1, Bk \<up> m, [Oc, Oc]) dither 3 = (0, Bk \<up> m, [Oc, Oc])"
+  shows "steps0 (1, Bk \<up> m, [Oc, Oc]) dither 2 = (0, Bk \<up> m, [Oc, Oc])"
 unfolding dither_def
 by (simp add: steps.simps step.simps numeral)