--- a/Paper/Paper.thy	Tue Jan 29 16:37:38 2013 +0000
+++ b/Paper/Paper.thy	Wed Jan 30 02:26:56 2013 +0000
@@ -35,7 +35,41 @@
   tcopy ("copy") and 
   tape_of ("\<langle>_\<rangle>") and 
   tm_comp ("_ \<oplus> _") and 
-  DUMMY  ("\<^raw:\mbox{$\_\!\_\,$}>")
+  DUMMY  ("\<^raw:\mbox{$\_\!\_\,$}>") and
+  inv_begin0 ("I\<^isub>0") and
+  inv_begin1 ("I\<^isub>1") and
+  inv_begin2 ("I\<^isub>2") and
+  inv_begin3 ("I\<^isub>3") and
+  inv_begin4 ("I\<^isub>4") and 
+  inv_begin ("I\<^bsub>begin\<^esub>")
+
+ 
+lemma inv_begin_print:
+  shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and
+        "s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and 
+        "s = 2 \<Longrightarrow> inv_begin n (s, tp) = inv_begin2 n tp" and 
+        "s = 3 \<Longrightarrow> inv_begin n (s, tp) = inv_begin3 n tp" and 
+        "s = 4 \<Longrightarrow> inv_begin n (s, tp) = inv_begin4 n tp" and
+        "s \<notin> {0,1,2,3,4} \<Longrightarrow> inv_begin n (s, l, r) = False"
+apply(case_tac [!] tp)
+by (auto)
+
+lemma inv1: 
+  shows "0 < n \<Longrightarrow> inv_begin0 n \<mapsto> inv_loop1 n"
+unfolding assert_imp_def
+unfolding inv_loop1.simps inv_begin0.simps
+apply(auto)
+apply(rule_tac x="1" in exI)
+apply(auto simp add: replicate.simps)
+done
+
+lemma inv2: 
+  shows "0 < n \<Longrightarrow> inv_loop0 n = inv_end1 n"
+apply(rule ext)
+apply(case_tac x)
+apply(simp add: inv_end1.simps)
+done
+
 
 declare [[show_question_marks = false]]
 
@@ -73,12 +107,15 @@
 
 lemma nats2tape:
   shows "<([]::nat list)> = []"
-  and "<[n]> = Oc \<up> (n + 1)"
-  and "ns \<noteq> [] \<Longrightarrow> <n#ns> = Oc \<up> (n + 1) @ [Bk] @ <ns>"
-apply(auto simp add: tape_of_nl_abv tape_of_nat_list.simps)
+  and "<[n]> = <n>"
+  and "ns \<noteq> [] \<Longrightarrow> <n#ns> = <(n::nat, ns)>"
+  and "<(n, m)> = <n> @ [Bk] @ <m>"
+  and "<[n, m]> = <(n, m)>"
+  and "<n> = Oc \<up> (n + 1)" 
+apply(auto simp add: tape_of_nat_pair tape_of_nl_abv tape_of_nat_abv tape_of_nat_list.simps)
 apply(case_tac ns)
-apply(auto)
-done
+apply(auto simp add: tape_of_nat_pair tape_of_nat_abv)
+done 
 
 lemmas HR1 = 
   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"]
@@ -86,6 +123,16 @@
 lemmas HR2 =
   Hoare_plus_unhalt_simple[where ?P1.0="P" and ?P2.0="Q" and ?A="p\<^isub>1" and B="p\<^isub>2"]
 
+lemma inv_begin01:
+  assumes "n > 1"
+  shows "inv_begin0 n (l, r) = (n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc]))"
+using assms by auto                          
+
+lemma inv_begin02:
+  assumes "n = 1"
+  shows "inv_begin0 n (l, r) = (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc]))"
+using assms by auto
+
 (*>*)
 
 section {* Introduction *}
@@ -179,26 +226,27 @@
 %standard proof of this property uses the notion of universal
 %Turing machines.
 
-We are not the first who formalised Turing machines: we are aware 
-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 
-halting problem since their main focus is complexity, rather than
-computability theory. They also report that the informal proofs from which they
-started are not ``sufficiently accurate to be directly usable as a
-guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For
-our formalisation we follow mainly the proofs from the textbook
+We are not the first who formalised Turing machines: we are aware 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 halting problem since
+their main focus is complexity, rather than computability theory. They
+also report that the informal proofs from which they started are not
+``sufficiently accurate to be directly usable as a guideline for
+formalization'' \cite[Page 2]{AspertiRicciotti12}. For 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 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
-recursive functions to abacus machines, the textbook again only shows
-how it can be done for 2- and 3-ary functions, but in the
-formalisation we need arbitrary functions. But the general ideas for
-how to do this are clear enough in \cite{Boolos87}. 
+the \emph{copy Turing machine} and its correctness proof are 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 recursive functions to
+abacus machines, the textbook again only shows how it can be done for
+2- and 3-ary functions, but in the formalisation we need arbitrary
+functions. But the general ideas for how to do this are clear enough
+in \cite{Boolos87}.
 %However, one
 %aspect that is completely left out from the informal description in
 %\cite{Boolos87}, and similar ones we are aware of, is arguments why certain Turing
@@ -443,7 +491,7 @@
   In this definition the function @{term nth_of} returns the @{text n}th element
   from a list, provided it exists (@{term Some}-case), or if it does not, it
   returns the default action @{term Nop} and the default state @{text 0} 
-  (@{term None}-case). We often need to restrict Turing machine programs 
+  (@{term None}-case). We often have to restrict Turing machine programs 
   to be well-formed: a program @{term p} is \emph{well-formed} if it 
   satisfies the following three properties:
 
@@ -638,10 +686,10 @@
   \end{tikzpicture}\\[-8mm]\mbox{} 
   \end{center}
   \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 
+  (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]>)"}.}
+  block of @{term "Oc"}s. The resulting tape is @{term "([Bk], <(2::nat, 2::nat)>)"}.}
   \label{copy}
   \end{figure}
 
@@ -649,10 +697,14 @@
   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. To make this formal we define the following function
+  blanks. To make this formal we define the following overloaded function
   
   \begin{center}
-  \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+  \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+  @{thm (lhs) nats2tape(6)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(6)}\\
+  @{thm (lhs) nats2tape(4)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(4)}\\
+  \end{tabular}\hspace{6mm}
+  \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
   @{thm (lhs) nats2tape(1)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(1)}\\
   @{thm (lhs) nats2tape(2)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(2)}\\
   @{thm (lhs) nats2tape(3)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(3)}
@@ -666,10 +718,10 @@
   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
+  Turing machines, we have to analyse two concrete Turing machine
   programs and establish that they are correct---that means they are
   ``doing what they are supposed to be doing''.  Such correctness proofs are usually left
-  out in the informal literature, for example \cite{Boolos87}.  One program 
+  out in the informal literature, for example \cite{Boolos87}.  The first program 
   we need to prove correct is the @{term dither} program shown in \eqref{dither} 
   and the other program is @{term "tcopy"} defined as
 
@@ -680,19 +732,18 @@
   \end{equation}
 
   \noindent
-  whose three components are given in Figure~\ref{copy}. To the prove
-  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}.  
-  They implement the 
-  idea that a program @{term p} started in state @{term "1::nat"} with
-  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>"}
-  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
+  whose three components are given in Figure~\ref{copy}. We introduce
+  the notion of total correctness defined in terms of
+  \emph{Hoare-triples}, written @{term "{P} p {Q}"} (this notion is
+  very similar to \emph{realisability} in \cite{AspertiRicciotti12}).
+  The Hoare-triples implement the idea that a program @{term p}
+  started in state @{term "1::nat"} with 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>"} 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
 
   \begin{center}
   \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
@@ -796,11 +847,11 @@
   number of steps we can perform starting from the input tape.
 
   The program @{term tcopy} defined in \eqref{tcopy} has 15 states;
-  its purpose is to produce the standard tape @{term "(DUMMY, <[n,
-  n::nat]>)"} when started with @{term "(DUMMY, <[n::nat]>)"}, that is
+  its purpose 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 prove the following two Hoare-rules for sequentially
+  burden, we derive the following two Hoare-rules for sequentially
   composed programs.
 
   \begin{center}
@@ -825,23 +876,56 @@
   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 the components @{term "tcopy_begin"}, @{term "tcopy_loop"} 
+  and @{term "tcopy_end"} in isolation. We will show the details for 
+  the program @{term "tcopy_begin"}. Given the invariants @{term "inv_begin0"},\ldots, @{term "inv_begin4"} 
+  shown in Figure~\ref{invbegin},
+  we define the following invariant for @{term "tcopy_begin"}.
 
-  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 the details for 
-  the program @{term "tcopy_begin"}. We found the following invariants for each
-  state:
+  \begin{figure}
+  \begin{center}
+  \begin{tabular}{@ {}lcl@ {\hspace{-2cm}}l@ {}}
+  @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
+                                &             & @{thm (rhs) inv_begin02} \\
+  @{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\
+  @{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\
+  @{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\
+  @{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}
+  \end{tabular}
+  \end{center}
+  \caption{The invariants for each state of @{term tcopy_begin}. They depend on
+  the number @{term n} of @{term Oc}s with which this Turing machine is started.}\label{invbegin}
+  \end{figure}
 
   \begin{center}
-  @{thm inv_begin0.simps}\\
-  @{thm inv_begin1.simps}\\
-  @{thm inv_begin2.simps}\\
-  @{thm inv_begin3.simps}\\
-  @{thm inv_begin4.simps}
+  \begin{tabular}{rcl}
+  @{thm (lhs) inv_begin.simps} & @{text "\<equiv>"} & 
+  @{text "if"} @{thm (prem 1) inv_begin_print(1)} @{text then} @{thm (rhs) inv_begin_print(1)}\\
+  & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(2)} @{text then} @{thm (rhs) inv_begin_print(2)} \\
+ & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(3)} @{text then} @{thm (rhs) inv_begin_print(3)}\\
+  & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(4)} @{text then} @{thm (rhs) inv_begin_print(4)}\\
+   & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(5)} @{text then} @{thm (rhs) inv_begin_print(5)}\\
+  & & @{text else} @{thm (rhs) inv_begin_print(6)}
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  This definition depends on @{term n}, which represents the number
+  of @{term Oc}s on the tape. It is not hard (26 lines of automated proof script)
+  to show that for @{term "n > (0::nat)"} this invariant is preserved under @{term step} and @{term steps}.
+  
+
+  measure for the copying TM, which we however omit.
+
+  
+  \begin{center}
+  @{thm begin_correct}\\
+  @{thm loop_correct}\\
+  @{thm end_correct}
   \end{center}
 
 
-  measure for the copying TM, which we however omit.
 
   \begin{center}
   @{thm haltP_def[where lm="ns"]}

--- a/ROOT.ML	Tue Jan 29 16:37:38 2013 +0000
+++ b/ROOT.ML	Wed Jan 30 02:26:56 2013 +0000
@@ -14,8 +14,8 @@
 no_document 
 use_thys ["thys/turing_basic",
           "thys/turing_hoare", 
-	  "thys/uncomputable", 
+	  "thys/uncomputable"(*, 
 	  "thys/abacus", 
 	  "thys/rec_def", 
 	  "thys/recursive",
-          "thys/UF"]
+          "thys/UF"*)]

Binary file paper.pdf has changed

--- a/thys/turing_basic.thy	Tue Jan 29 16:37:38 2013 +0000
+++ b/thys/turing_basic.thy	Wed Jan 30 02:26:56 2013 +0000
@@ -179,30 +179,28 @@
 abbreviation
   "tm_wf0 p \<equiv> tm_wf (p, 0)"
 
-lemma halt_lemma: 
-  "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
-by (metis wf_iff_no_infinite_down_chain)
-
 abbreviation exponent :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100)
   where "x \<up> n == replicate n x"
 
 consts tape_of :: "'a \<Rightarrow> cell list" ("<_>" 100)
 
-fun tape_of_nat_list :: "nat list \<Rightarrow> cell list" 
+defs (overloaded)
+  tape_of_nat_abv: "<(n::nat)> \<equiv> Oc \<up> (Suc n)"
+
+fun tape_of_nat_list :: "'a list \<Rightarrow> cell list" 
   where 
   "tape_of_nat_list [] = []" |
-  "tape_of_nat_list [n] = Oc\<up>(Suc n)" |
-  "tape_of_nat_list (n#ns) = Oc\<up>(Suc n) @ Bk # (tape_of_nat_list ns)"
+  "tape_of_nat_list [n] = <n>" |
+  "tape_of_nat_list (n#ns) = <n> @ Bk # (tape_of_nat_list ns)"
 
-fun tape_of_nat_pair :: "nat \<times> nat \<Rightarrow> cell list" 
+fun tape_of_nat_pair :: "'a \<times> 'b \<Rightarrow> cell list" 
   where 
-  "tape_of_nat_pair (n, m) = Oc\<up>(Suc n) @ [Bk] @ Oc\<up>(Suc m)" 
+  "tape_of_nat_pair (n, m) = <n> @ [Bk] @ <m>" 
 
 
 defs (overloaded)
-  tape_of_nl_abv: "<ns> \<equiv> tape_of_nat_list ns"
-  tape_of_nat_abv: "<(n::nat)> \<equiv> Oc\<up>(Suc n)"
-  tape_of_nat_pair: "<p> \<equiv> tape_of_nat_pair p"
+  tape_of_nl_abv: "<(ns::'a list)> \<equiv> tape_of_nat_list ns"
+  tape_of_nat_pair: "<(np::'a\<times>'b)> \<equiv> tape_of_nat_pair np"
 
 fun 
   shift :: "instr list \<Rightarrow> nat \<Rightarrow> instr list"

--- a/thys/uncomputable.thy	Tue Jan 29 16:37:38 2013 +0000
+++ b/thys/uncomputable.thy	Wed Jan 30 02:26:56 2013 +0000
@@ -63,14 +63,16 @@
 | "inv_begin3 n (l, r) = (n > 0 \<and> (l, tl r) = (Bk # Oc \<up> n, []))"
 | "inv_begin4 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_begin :: "nat \<Rightarrow> config \<Rightarrow> bool"
   where
-  "inv_begin n (s, l, r) = 
-        (if s = 0 then inv_begin0 n (l, r) else
-         if s = 1 then inv_begin1 n (l, r) else
-         if s = 2 then inv_begin2 n (l, r) else
-         if s = 3 then inv_begin3 n (l, r) else
-         if s = 4 then inv_begin4 n (l, r) 
+  "inv_begin n (s, tp) = 
+        (if s = 0 then inv_begin0 n tp else
+         if s = 1 then inv_begin1 n tp else
+         if s = 2 then inv_begin2 n tp else
+         if s = 3 then inv_begin3 n tp else
+         if s = 4 then inv_begin4 n tp 
          else False)"
 
 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> 
@@ -120,8 +122,13 @@
 lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]"
 by (case_tac r, auto, case_tac a, auto)
 
+
+lemma halt_lemma: 
+  "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
+by (metis wf_iff_no_infinite_down_chain)
+
 lemma begin_halt: 
-  "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (1, [], Oc\<up>x) tcopy_begin stp)"
+  "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (1, [], Oc \<up> x) tcopy_begin stp)"
 proof(rule_tac LE = begin_LE in halt_lemma) 
   show "wf begin_LE" unfolding begin_LE_def by (auto) 
 next
@@ -155,22 +162,22 @@
 qed
     
 lemma begin_correct: 
-  "0 < x \<Longrightarrow> {inv_begin1 x} tcopy_begin {inv_begin0 x}"
+  "0 < n \<Longrightarrow> {inv_begin1 n} tcopy_begin {inv_begin0 n}"
 proof(rule_tac Hoare_haltI)
   fix l r
-  assume h: "0 < x" "inv_begin1 x (l, r)"
-  hence "\<exists> stp. is_final (steps0 (1, [], Oc \<up> x) tcopy_begin stp)"
+  assume h: "0 < n" "inv_begin1 n (l, r)"
+  then have "\<exists> stp. is_final (steps0 (1, [], Oc \<up> n) tcopy_begin stp)"
     by (rule_tac begin_halt)    
-  then obtain stp where "is_final (steps (1, [], Oc\<up>x) (tcopy_begin, 0) stp)" ..
-  moreover have "inv_begin x (steps (1, [], Oc\<up>x) (tcopy_begin, 0) stp)"
+  then obtain stp where "is_final (steps0 (1, [], Oc \<up> n) tcopy_begin stp)" ..
+  moreover have "inv_begin n (steps0 (1, [], Oc \<up> n) tcopy_begin stp)"
     apply(rule_tac inv_begin_steps)
     using h by(simp_all add: inv_begin.simps)
   ultimately show
-    "\<exists>n. is_final (steps (1, l, r) (tcopy_begin, 0) n) \<and> 
-    inv_begin0 x holds_for steps (1, l, r) (tcopy_begin, 0) n"
+    "\<exists>stp. is_final (steps0 (1, l, r) tcopy_begin stp) \<and> 
+    inv_begin0 n holds_for steps (1, l, r) (tcopy_begin, 0) stp"
     using h
     apply(rule_tac x = stp in exI)
-    apply(case_tac "(steps (1, [], Oc \<up> x) (tcopy_begin, 0) stp)", simp add: inv_begin.simps)
+    apply(case_tac "(steps0 (1, [], Oc \<up> n) tcopy_begin stp)", simp add: inv_begin.simps)
     done
 qed
 
@@ -893,8 +900,11 @@
     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)
+    unfolding assert_imp_def
+    unfolding inv_begin0.simps inv_loop1.simps
+    unfolding inv_loop1_loop.simps inv_loop1_exit.simps
+    apply(auto simp add: numeral Cons_eq_append_conv)
+    by (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)
@@ -922,10 +932,10 @@
     by (rule tcopy_correct1) (simp)
   moreover
   have "pre_tcopy n = inv_begin1 (Suc n)" 
-    by (auto simp add: tape_of_nl_abv)
+    by (auto simp add: tape_of_nl_abv tape_of_nat_abv)
   moreover
   have "inv_end0 (Suc n) = post_tcopy n" 
-    by (auto simp add: inv_end0.simps tape_of_nl_abv)
+    by (auto simp add: inv_end0.simps tape_of_nat_abv tape_of_nl_abv)
   ultimately
   show "{pre_tcopy n} tcopy {post_tcopy n}" 
     by simp