# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1359148509 0
# Node ID 2e9881578cb28cd87f4ace69d419d6bba54def0b
# Parent  eb589fa73fc14c20556eb68f2c0cb00310653c78
updated paper

diff -r eb589fa73fc1 -r 2e9881578cb2 Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Jan 25 15:57:58 2013 +0100
+++ b/Paper/Paper.thy	Fri Jan 25 21:15:09 2013 +0000
@@ -27,6 +27,7 @@
   tcopy_end ("copy\<^bsub>end\<^esub>") and
   step0 ("step") and
   steps0 ("steps") and
+  exponent ("_\<^bsup>_\<^esup>") and
 (*  abc_lm_v ("lookup") and
   abc_lm_s ("set") and*)
   haltP ("stdhalt") and 
@@ -247,10 +248,12 @@
   constructors, namely @{text Bk} and @{text Oc}.  One way to
   represent such tapes is to use a pair of lists, written @{term "(l,
   r)"}, where @{term l} stands for the tape on the left-hand side of
-  the head and @{term r} for the tape on the right-hand side. We have
-  the convention that the head, abbreviated @{term hd}, of the
-  right-list is the cell on which the head of the Turing machine
-  currently scannes. This can be pictured as follows:
+  the head and @{term r} for the tape on the right-hand side.  We use
+  the notation @{term "Bk \<up> n"} (similarly @{term "Oc \<up> n"}) for lists
+  composed of @{term n} elements of @{term Bk}.  We also have the
+  convention that the head, abbreviated @{term hd}, of the right-list
+  is the cell on which the head of the Turing machine currently
+  scannes. This can be pictured as follows:
   %
   \begin{center}
   \begin{tikzpicture}
@@ -304,7 +307,7 @@
   We slightly deviate
   from the presentation in \cite{Boolos87} 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
+  machines.  Given a tape and an action, we can define the
   following tape updating function:
 
   \begin{center}
@@ -361,7 +364,7 @@
   %cannot be used as it does not preserve types.} This renaming can be
   %quite cumbersome to reason about. 
   We follow the choice made in \cite{AspertiRicciotti12} 
-  representing a state by a natural number and the states in a Turing
+  by representing a state with a natural number and the states in a Turing
   machine program by the initial segment of natural numbers starting from @{text 0}.
   In doing so we can compose two Turing machine programs by
   shifting the states of one by an appropriate amount to a higher
@@ -371,7 +374,7 @@
   an action and a natural number (the next state). A \emph{program} @{term p} of a Turing
   machine is then a list of such pairs. Using as an example the following Turing machine
   program, which consists of four instructions
-
+  %
   \begin{equation}
   \begin{tikzpicture}
   \node [anchor=base] at (0,0) {@{thm dither_def}};
@@ -385,7 +388,7 @@
   \end{tikzpicture}
   \label{dither}
   \end{equation}
-
+  %
   \noindent
   the reader can see we have organised our Turing machine programs so
   that segments of two belong to a state. The first component of such a
@@ -401,8 +404,8 @@
   \cite{AspertiRicciotti12}, we have chosen a very concrete
   representation for programs, because when constructing a universal
   Turing machine, we need to define a coding function for programs.
-  This can be easily done for our programs-as-lists, but is more
-  difficult for the functions used by Asperti and Ricciotti.
+  This can be directly done for our programs-as-lists, but is
+  slightly more difficult for the functions used by Asperti and Ricciotti.
 
   Given a program @{term p}, a state
   and the cell being read by the head, we need to fetch
@@ -525,9 +528,21 @@
   \caption{Copy machine}\label{copy}
   \end{figure}
 
-  {\it 
-  As in \cite{Boolos87} we often need to restrict tapes to be in standard
-  form.}
+  We often need to restrict tapes to be in \emph{standard form}, which means 
+  the left list of the tape is either empty or only contains @{text "Bk"}s, and 
+  the right list contains some ``clusters'' of @{text "Oc"}s separted by single 
+  blanks and can be followed by some blanks. To make this formal we define the 
+  following function
+  
+  \begin{center}
+  foo
+  \end{center}
+
+  \noindent
+  A standard tape is then of the form @{text "(Bk\<^isup>k,\<langle>n\<^isub>1,...,n\<^isub>m\<rangle> @ Bk\<^isup>l)"} for some @{text k},
+  @{text l} and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the 
+  leftmost @{term "Oc"} on the tape.
+
 
   Before we can prove the undecidability of the halting problem for our
   Turing machines, we need to analyse two concrete Turing machine
@@ -549,7 +564,7 @@
   notion of total correctness defined in terms of
   \emph{Hoare-triples}, written @{term "{P} p {Q}"}. They realise the
   idea that a program @{term p} started in state @{term "1::nat"} with
-  a tape satisfying @{term P} will after @{text n} steps halt (have
+  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
@@ -577,7 +592,7 @@
   
   \noindent
   We have set up our Hoare-style reasoning so that we can deal explicitly 
-  with looping and total correctness, rather than have notions for partial 
+  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 simple Hoare-rules for sequentially composed Turing programs. 
@@ -585,8 +600,9 @@
   for example, completely separately from @{term "tcopy_loop"} and @{term "tcopy_end"}.
 
   \begin{center}
-  \begin{tabular}{lcl}
-  \multicolumn{1}{c}{start tape}\\
+  \begin{tabular}{l@ {\hspace{3mm}}lcl}
+  & \multicolumn{1}{c}{start tape}\\[1mm]
+  \raisebox{2.5mm}{halting case:} &
   \begin{tikzpicture}
   \draw[very thick] (-2,0)   -- ( 0.75,0);
   \draw[very thick] (-2,0.5) -- ( 0.75,0.5);
@@ -615,7 +631,8 @@
   \node [anchor=base] at (-1.7,0.2) {\ldots};
   \end{tikzpicture}\\
 
-   \begin{tikzpicture}
+  \raisebox{2.5mm}{non-halting case:} &
+  \begin{tikzpicture}
   \draw[very thick] (-2,0)   -- ( 0.25,0);
   \draw[very thick] (-2,0.5) -- ( 0.25,0.5);
   \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
diff -r eb589fa73fc1 -r 2e9881578cb2 paper.pdf
Binary file paper.pdf has changed
diff -r eb589fa73fc1 -r 2e9881578cb2 thys/uncomputable.thy
--- a/thys/uncomputable.thy	Fri Jan 25 15:57:58 2013 +0100
+++ b/thys/uncomputable.thy	Fri Jan 25 21:15:09 2013 +0000
@@ -64,24 +64,23 @@
   inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
   inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-  "inv_init0 x (l, r) = ((x > 1 \<and> l = Oc \<up> (x - 2) \<and> r = [Oc, Oc, Bk, Oc]) \<or>   
-                         (x = 1 \<and> l = [] \<and> r = [Bk, Oc, Bk, Oc]))"
-| "inv_init1 x (l, r) = (l = [] \<and> r = Oc \<up> x)"
-| "inv_init2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc \<up> i \<and> r = Oc \<up> j)"
-| "inv_init3 x (l, r) = (x > 0 \<and> l = Bk # Oc \<up> x \<and> tl r = [])"
-| "inv_init4 x (l, r) = (x > 0 \<and> ((l = Oc \<up> x \<and> r = [Bk, Oc]) \<or> (l = Oc \<up> (x - 1) \<and> r = [Oc, Bk, Oc])))"
+  "inv_init0 n (l, r) = ((n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc])) \<or>   
+                         (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc])))"
+| "inv_init1 n (l, r) = ((l, r) = ([], Oc \<up> n))"
+| "inv_init2 n (l, r) = (\<exists> i j. i > 0 \<and> i + j = n \<and> (l, r) = (Oc \<up> i, Oc \<up> j))"
+| "inv_init3 n (l, r) = (n > 0 \<and> (l, tl r) = (Bk # Oc \<up> n, []))"
+| "inv_init4 n (l, r) = (n > 0 \<and> ((l, r) = (Oc \<up> n, [Bk, Oc]) \<or> (l, r) = (Oc \<up> (n - 1), [Oc, Bk, Oc])))"
 
 fun inv_init :: "nat \<Rightarrow> config \<Rightarrow> bool"
   where
-  "inv_init x (s, l, r) = 
-        (if s = 0 then inv_init0 x (l, r) 
-         else if s = 1 then inv_init1 x (l, r)
-         else if s = 2 then inv_init2 x (l, r)
-         else if s = 3 then inv_init3 x (l, r)
-         else if s = 4 then inv_init4 x (l, r)
+  "inv_init n (s, l, r) = 
+        (if s = 0 then inv_init0 n (l, r) else
+         if s = 1 then inv_init1 n (l, r) else
+         if s = 2 then inv_init2 n (l, r) else
+         if s = 3 then inv_init3 n (l, r) else
+         if s = 4 then inv_init4 n (l, r) 
          else False)"
 
-declare inv_init.simps[simp del]
 
 
 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> 
@@ -109,20 +108,19 @@
 
 fun init_state :: "config \<Rightarrow> nat"
   where
-  "init_state (s, l, r) = (if s = 0 then 0
-                             else 5 - s)"
+  "init_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
 
 fun init_step :: "config \<Rightarrow> nat"
   where
-  "init_step (s, l, r) = (if s = 2 then length r
-                            else if s = 3 then if r = [] \<or> r = [Bk] then Suc 0 else 0
-                            else if s = 4 then length l
-                            else 0)"
+  "init_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"
   where
-  "init_measure c = 
-   (init_state c, init_step c)"
+  "init_measure c = (init_state c, init_step c)"
 
 
 definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set"
@@ -131,11 +129,11 @@
 
 definition init_LE :: "(config \<times> config) set"
   where
-   "init_LE \<equiv> (inv_image lex_pair init_measure)"
+  "init_LE \<equiv> (inv_image lex_pair init_measure)"
 
 lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]"
-apply(case_tac r, auto, case_tac a, auto)
-done
+by (case_tac r, auto, case_tac a, auto)
+
 
 lemma wf_init_le: "wf init_LE"
 by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def)
@@ -164,11 +162,10 @@
     ultimately show "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) (Suc n), 
       steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<in> init_LE"
       using a 
-    proof(simp)
+    proof(simp del: inv_init.simps)
       assume "inv_init x (s, l, r)" "0 < s"
       thus "(step (s, l, r) (tcopy_init, 0), s, l, r) \<in> init_LE"
-        apply(auto simp: inv_init.simps init_LE_def lex_pair_def step.simps tcopy_init_def numeral 
-          split: if_splits)
+        apply(auto simp: init_LE_def lex_pair_def step.simps tcopy_init_def numeral split: if_splits)
         apply(case_tac r, auto, case_tac a, auto)
         done
     qed
@@ -199,48 +196,31 @@
 
 (* tcopy_loop *)
 
-fun inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_loop1_loop x (l, r) = 
-       (\<exists> i j. i + j + 1 = x \<and> l = Oc\<up>i \<and> r = Oc # Oc # Bk\<up>j @ Oc\<up>j \<and> j > 0)"
-
-fun inv_loop1_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_loop1_exit x (l, r) = 
-      (l = [] \<and> r = Bk # Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )"
-
-fun inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))"
-
-fun inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_loop2 x (l, r) = 
-       (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> l = Oc\<up>i \<and> r = any#Bk\<up>j@Oc\<up>j)"
-
-fun inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_loop3 x (l, r) = 
-         (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = Suc j \<and> l = Bk\<up>k@Oc\<up>i \<and> r = Bk\<up>t@Oc\<up>j)"
-
-fun inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_loop4 x (l, r) = 
-           (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = j \<and> l = Oc\<up>k @ Bk\<up>(Suc j)@Oc\<up>i \<and> r = Oc\<up>t)"
-
-fun inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+fun 
+  inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop1_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-  "inv_loop5_loop x (l, r) = 
-          (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0 \<and> l = Oc\<up>k@Bk\<up>j@Oc\<up>i \<and> r = Oc\<up>t)"
-
-fun inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_loop5_exit x (l, r) = (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and>  l = Bk\<up>(j - 1)@Oc\<up>i \<and> r = Bk # Oc\<up>j)"
-
-fun inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or> 
-                         inv_loop5_exit x (l, r))"
+  "inv_loop0 x (l, r) =  (l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )"
+| "inv_loop1_loop x (l, r) = (\<exists> i j. i + j + 1 = x \<and> l = Oc\<up>i \<and> r = Oc # Oc # Bk\<up>j @ Oc\<up>j \<and> j > 0)"
+| "inv_loop1_exit x (l, r) = (l = [] \<and> r = Bk # Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0)"
+| "inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))"
+| "inv_loop2 x (l, r) = (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> l = Oc\<up>i \<and> r = any#Bk\<up>j@Oc\<up>j)"
+| "inv_loop3 x (l, r) = 
+     (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = Suc j \<and> l = Bk\<up>k@Oc\<up>i \<and> r = Bk\<up>t@Oc\<up>j)"
+| "inv_loop4 x (l, r) = 
+     (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = j \<and> l = Oc\<up>k @ Bk\<up>(Suc j)@Oc\<up>i \<and> r = Oc\<up>t)"
+| "inv_loop5_loop x (l, r) = 
+     (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0 \<and> l = Oc\<up>k@Bk\<up>j@Oc\<up>i \<and> r = Oc\<up>t)"
+| "inv_loop5_exit x (l, r) = (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and>  l = Bk\<up>(j - 1)@Oc\<up>i \<and> r = Bk # Oc\<up>j)"
+| "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or> inv_loop5_exit x (l, r))"
 
 fun inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
   where
@@ -256,11 +236,6 @@
   where
   "inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))"
 
-fun inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_loop0 x (l, r) = 
-      (l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )"
-
 fun inv_loop :: "nat \<Rightarrow> config \<Rightarrow> bool"
   where
   "inv_loop x (s, l, r) = 
@@ -277,21 +252,20 @@
         inv_loop2.simps[simp del] inv_loop3.simps[simp del] 
         inv_loop4.simps[simp del] inv_loop5.simps[simp del] 
         inv_loop6.simps[simp del]
+
 lemma [elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR"
-apply(case_tac t, auto)
-done
-
+by (case_tac t, auto)
 
 lemma [simp]: "inv_loop1 x (b, []) = False"
 by(simp add: inv_loop1.simps)
 
 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
-apply(auto simp: inv_loop2.simps inv_loop3.simps)
-done
+by (auto simp: inv_loop2.simps inv_loop3.simps)
+
 
 lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
-apply(auto simp: inv_loop3.simps)
-done
+by (auto simp: inv_loop3.simps)
+
 
 lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop5 x (b, [Oc])"
 apply(auto simp: inv_loop4.simps inv_loop5.simps)
@@ -1070,10 +1044,10 @@
 
 (* invariants of dither *)
 abbreviation
-  "dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc, Oc]"
+  "dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc, Oc]))"
 
 abbreviation
-  "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc]"
+  "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc]))"
 
 lemma dither_loops_aux: 
   "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or> 
@@ -1330,9 +1304,9 @@
   shows "False"
 proof -
   (* invariants *)
-  def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)"
-  def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)"
-  def P3 \<equiv> "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]"
+  def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([], <[code_tcontra]>)"
+  def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([Bk], <[code_tcontra, code_tcontra]>)"
+  def P3 \<equiv> "\<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc, Oc]))"
 
   (*
   {P1} tcopy {P2}  {P2} H {P3} 
@@ -1349,12 +1323,12 @@
   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 (simp) (rule tcopy_correct2)
   next
     case B_halt (* of H *)
     show "{P2} H {P3}"
       unfolding P2_def P3_def
-      using assms by (rule H_halt_inv)
+      using assms by (simp) (rule H_halt_inv)
   qed (simp)
 
   (* {P3} dither {P3} *)
@@ -1384,9 +1358,9 @@
   shows "False"
 proof - 
   (* invariants *)
-  def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)"
-  def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)"
-  def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]"
+  def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([], <[code_tcontra]>)"
+  def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([Bk], <[code_tcontra, code_tcontra]>)"
+  def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>n. (l, r) = (Bk \<up> n, [Oc]))"
 
   (*
   {P1} tcopy {P2}  {P2} H {P3} 
@@ -1403,12 +1377,12 @@
   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 (simp) (rule tcopy_correct2)
   next
     case B_halt (* of H *)
     then show "{P2} H {P3}"
       unfolding P2_def P3_def
-      using assms by (rule H_unhalt_inv)
+      using assms by (simp) (rule H_unhalt_inv)
   qed (simp)
 
   (* {P3} dither loops *)