--- a/Paper/Paper.thy	Sun Jan 27 00:09:17 2013 +0000
+++ b/Paper/Paper.thy	Sun Jan 27 14:57:54 2013 +0000
@@ -183,8 +183,8 @@
 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; also the 
-book only shows how the universal Turing machine is constructed for Turing
+the \emph{copy Turing program} 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
@@ -259,7 +259,7 @@
   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}s.  We also have the
-  convention that the head, abbreviated @{term hd}, of the right-list
+  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:
   %
@@ -329,20 +329,20 @@
   \end{center}
 
   \noindent
-  The first two clauses replace the head of the right-list
+  The first two clauses replace the head of the right list
   with a new @{term Bk} or @{term Oc}, respectively. To see that
   these two clauses make sense in case where @{text r} is the empty
   list, one has to know that the tail function, @{term tl}, is defined
   such that @{term "tl [] == []"} holds. The third clause 
   implements the move of the head one step to the left: we need
   to test if the left-list @{term l} is empty; if yes, then we just prepend a 
-  blank cell to the right-list; otherwise we have to remove the
-  head from the left-list and prepend it to the right-list. Similarly
+  blank cell to the right list; otherwise we have to remove the
+  head from the left-list and prepend it to the right list. Similarly
   in the fourth clause for a right move action. The @{term Nop} operation
   leaves the the tape unchanged.
 
   %Note that our treatment of the tape is rather ``unsymmetric''---we
-  %have the convention that the head of the right-list is where the
+  %have the convention that the head of the right list is where the
   %head is currently positioned. Asperti and Ricciotti
   %\cite{AspertiRicciotti12} also considered such a representation, but
   %dismiss it as it complicates their definition for \emph{tape
@@ -629,10 +629,10 @@
   \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 adds @{term "[Bk, Oc]"} at 
+  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 result is the tape @{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}
 

Binary file paper.pdf has changed

--- a/thys/uncomputable.thy	Sun Jan 27 00:09:17 2013 +0000
+++ b/thys/uncomputable.thy	Sun Jan 27 14:57:54 2013 +0000
@@ -30,9 +30,9 @@
 *}
 
 definition 
-  tcopy_init :: "instr list"
+  tcopy_begin :: "instr list"
 where
-  "tcopy_init \<equiv> [(W0, 0), (R, 2), (R, 3), (R, 2),
+  "tcopy_begin \<equiv> [(W0, 0), (R, 2), (R, 3), (R, 2),
                  (W1, 3), (L, 4), (L, 4), (L, 0)]"
 
 definition 
@@ -52,33 +52,33 @@
 definition 
   tcopy :: "instr list"
 where
-  "tcopy \<equiv> (tcopy_init |+| tcopy_loop) |+| tcopy_end"
+  "tcopy \<equiv> (tcopy_begin |+| tcopy_loop) |+| tcopy_end"
 
 
-(* tcopy_init *)
+(* tcopy_begin *)
 
 fun 
-  inv_init0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_init1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_init2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  inv_begin0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_begin1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_begin2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_begin3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_begin4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-  "inv_init0 n (l, r) = ((n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc])) \<or>   
+  "inv_begin0 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])))"
+| "inv_begin1 n (l, r) = ((l, r) = ([], Oc \<up> n))"
+| "inv_begin2 n (l, r) = (\<exists> i j. i > 0 \<and> i + j = n \<and> (l, r) = (Oc \<up> i, Oc \<up> j))"
+| "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_init :: "nat \<Rightarrow> config \<Rightarrow> bool"
+fun inv_begin :: "nat \<Rightarrow> config \<Rightarrow> bool"
   where
-  "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) 
+  "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) 
          else False)"
 
 
@@ -88,22 +88,22 @@
 apply(rule_tac x = "Suc i" in exI, simp)
 done
 
-lemma inv_init_step: 
-  "\<lbrakk>inv_init x cf; x > 0\<rbrakk>
- \<Longrightarrow> inv_init x (step cf (tcopy_init, 0))"
-unfolding tcopy_init_def
+lemma inv_begin_step: 
+  "\<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_init.simps step.simps tcopy_init_def numeral split: if_splits)
-apply(case_tac "hd c", auto simp: inv_init.simps)
+apply(auto simp: inv_begin.simps step.simps tcopy_begin_def numeral split: if_splits)
+apply(case_tac "hd c", auto simp: inv_begin.simps)
 apply(case_tac c, simp_all)
 done
 
-lemma inv_init_steps: 
-  "\<lbrakk>inv_init x (s, l, r); x > 0\<rbrakk>
- \<Longrightarrow> inv_init x (steps (s, l, r) (tcopy_init, 0) stp)"
+lemma inv_begin_steps: 
+  "\<lbrakk>inv_begin x (s, l, r); x > 0\<rbrakk>
+ \<Longrightarrow> inv_begin x (steps (s, l, r) (tcopy_begin, 0) stp)"
 apply(induct stp, simp add: steps.simps)
 apply(auto simp: step_red)
-apply(rule_tac inv_init_step, simp_all)
+apply(rule_tac inv_begin_step, simp_all)
 done
 
 fun init_state :: "config \<Rightarrow> nat"
@@ -135,37 +135,37 @@
 by (case_tac r, auto, case_tac a, auto)
 
 
-lemma wf_init_le: "wf init_LE"
+lemma wf_begin_le: "wf init_LE"
 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_init, 0) stp)"
+  "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)"
 proof(rule_tac LE = init_LE in halt_lemma)
-  show "wf init_LE" by(simp add: wf_init_le)
+  show "wf init_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_init, 0) n) \<longrightarrow>
-        (steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) (Suc n), 
-            steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<in> init_LE"
+  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"
   proof(rule_tac allI, rule_tac impI)
     fix n
-    assume a: "\<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n)"
-    have b: "inv_init x (steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n)"
-      apply(rule_tac inv_init_steps)
-      apply(simp_all add: inv_init.simps h)
+    assume a: "\<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n)"
+    have b: "inv_begin x (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n)"
+      apply(rule_tac inv_begin_steps)
+      apply(simp_all add: inv_begin.simps h)
       done 
-    obtain s l r where c: "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) = (s, l, r)"
-      apply(case_tac "steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n", auto)
+    obtain s l r where c: "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) = (s, l, r)"
+      apply(case_tac "steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n", auto)
       done
-    moreover hence "inv_init x (s, l, r)" 
+    moreover hence "inv_begin x (s, l, r)" 
       using c b by simp
-    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"
+    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"
       using a 
-    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: init_LE_def lex_pair_def step.simps tcopy_init_def numeral split: if_splits)
+    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)
         apply(case_tac r, auto, case_tac a, auto)
         done
     qed
@@ -173,23 +173,23 @@
 qed
     
 lemma init_correct: 
-  "x > 0 \<Longrightarrow> {inv_init1 x} tcopy_init {inv_init0 x}"
+  "x > 0 \<Longrightarrow> {inv_begin1 x} tcopy_begin {inv_begin0 x}"
 proof(rule_tac Hoare_haltI)
   fix l r
   assume h: "0 < x"
-    "inv_init1 x (l, r)"
-  hence "\<exists> stp. is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_init, 0) stp)"
+    "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)    
-  then obtain stp where "is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_init, 0) stp)" ..
-  moreover have "inv_init x (steps (Suc 0, [], Oc\<up>x) (tcopy_init, 0) stp)"
-    apply(rule_tac inv_init_steps)
-    using h by(simp_all add: inv_init.simps)
+  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)
+    using h by(simp_all add: inv_begin.simps)
   ultimately show
-    "\<exists>n. is_final (steps (1, l, r) (tcopy_init, 0) n) \<and> 
-    inv_init0 x holds_for steps (1, l, r) (tcopy_init, 0) n"
+    "\<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"
     using h
     apply(rule_tac x = stp in exI)
-    apply(case_tac "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) stp)", simp add: inv_init.simps)
+    apply(case_tac "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) stp)", simp add: inv_begin.simps)
     done
 qed
 
@@ -644,7 +644,7 @@
     using h
     apply(rule_tac x = stp in exI)
     apply(case_tac "(steps (Suc 0, l, r) (tcopy_loop, 0) stp)", 
-      simp add: inv_init.simps inv_loop.simps)
+      simp add: inv_begin.simps inv_loop.simps)
     done
 qed
 
@@ -904,8 +904,8 @@
 
 (* tcopy *)
 
-lemma [intro]: "tm_wf (tcopy_init, 0)"
-by (auto simp: tm_wf.simps tcopy_init_def)
+lemma [intro]: "tm_wf (tcopy_begin, 0)"
+by (auto simp: tm_wf.simps tcopy_begin_def)
 
 lemma [intro]: "tm_wf (tcopy_loop, 0)"
 by (auto simp: tm_wf.simps tcopy_loop_def)
@@ -917,25 +917,25 @@
 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_init1 x} tcopy {inv_end0 x}"
+  "\<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"
     by(auto simp: inv_end1.simps inv_loop1.simps assert_imp_def)
 next
-  show "tm_wf (tcopy_init |+| tcopy_loop, 0)" by auto
+  show "tm_wf (tcopy_begin |+| tcopy_loop, 0)" by auto
 next
   assume "0 < x"
-  thus "{inv_init1 x} (tcopy_init |+| tcopy_loop) {inv_loop0 x}"
+  thus "{inv_begin1 x} (tcopy_begin |+| tcopy_loop) {inv_loop0 x}"
   proof(rule_tac Hoare_plus_halt)
-    show "inv_init0 x \<mapsto> inv_loop1 x"
-      apply(auto simp: inv_init0.simps inv_loop1.simps assert_imp_def)
+    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_init, 0)" by auto
+    show "tm_wf (tcopy_begin, 0)" by auto
   next
     assume "0 < x"
-    thus "{inv_init1 x} tcopy_init {inv_init0 x}"
+    thus "{inv_begin1 x} tcopy_begin {inv_begin0 x}"
       by(erule_tac init_correct)
   next
     assume "0 < x"
@@ -949,17 +949,17 @@
 qed
 
 abbreviation
-  "pre_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). ((l, r) = ([], <[n::nat]>))"
+  "pre_tcopy n \<equiv> \<lambda>tp. tp = ([]::cell list, <[n::nat]>)"
 abbreviation
-  "post_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). ((l, r) = ([Bk], <[n, n::nat]>))"
+  "post_tcopy n \<equiv> \<lambda>tp. tp= ([Bk], <[n, n::nat]>)"
 
 lemma tcopy_correct2:
   shows "{pre_tcopy n} tcopy {post_tcopy n}"
 proof -
-  have "{inv_init1 (Suc n)} tcopy {inv_end0 (Suc n)}"
+  have "{inv_begin1 (Suc n)} tcopy {inv_end0 (Suc n)}"
     by (rule tcopy_correct1) (simp)
   moreover
-  have "pre_tcopy n \<mapsto> inv_init1 (Suc n)" 
+  have "pre_tcopy n \<mapsto> inv_begin1 (Suc n)" 
     by (simp add: assert_imp_def tape_of_nl_abv)
   moreover
   have "inv_end0 (Suc n) \<mapsto> post_tcopy n" 
@@ -983,23 +983,23 @@
 
 (* invariants of dither *)
 abbreviation
-  "dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc, Oc]))"
+  "dither_halt_inv \<equiv> \<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <1::nat>))"
 
 abbreviation
-  "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc]))"
+  "dither_unhalt_inv \<equiv> \<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <0::nat>))"
 
 lemma dither_loops_aux: 
   "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or> 
    (steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))"
   apply(induct stp)
-  apply(auto simp: steps.simps step.simps dither_def numeral)
+  apply(auto simp: steps.simps step.simps dither_def numeral tape_of_nat_abv)
   done
 
 lemma dither_loops:
   shows "{dither_unhalt_inv} dither \<up>" 
 apply(rule Hoare_unhaltI)
 using dither_loops_aux
-apply(auto simp add: numeral)
+apply(auto simp add: numeral tape_of_nat_abv)
 by (metis Suc_neq_Zero is_final_eq)
 
 
@@ -1012,7 +1012,7 @@
   shows "{dither_halt_inv} dither {dither_halt_inv}" 
 apply(rule Hoare_haltI)
 using dither_halts_aux
-apply(auto)
+apply(auto simp add: tape_of_nat_abv)
 by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases)
 
 
@@ -1024,12 +1024,9 @@
   and the final configuration is standard.
 *}
 
-definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool"
+definition haltP :: "tprog0 \<Rightarrow> nat list \<Rightarrow> bool"
   where
-  "haltP p lm \<equiv> \<exists>n a m. steps (1, [], <lm>) p n = (0, Bk \<up> a,  <m::nat>)"
-
-abbreviation
-  "haltP0 p lm \<equiv> haltP (p, 0) lm" 
+  "haltP p lm \<equiv> {(\<lambda>tp. tp = ([], <lm>))} p {(\<lambda>tp. (\<exists>k m. tp = (Bk \<up> k,  <m::nat>)))}"
 
 lemma [intro, simp]: "tm_wf0 tcopy"
 by (auto simp: tcopy_def)
@@ -1057,52 +1054,31 @@
   The following two assumptions specifies that @{text "H"} does solve the Halting problem.
   *}
   and h_case: 
-  "\<And> M lm. (haltP0 M lm) \<Longrightarrow> \<exists>stp n. (steps0 (1, [Bk], <code M#lm>) H stp = (0, Bk \<up> n, [Oc]))"
+  "\<And> M lm. haltP M lm \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <code M#lm>))} H {(\<lambda>tp. \<exists>n. tp = (Bk \<up> n, <0::nat>))}"
   and nh_case: 
-  "\<And> M lm. (\<not> haltP0 M lm) \<Longrightarrow> \<exists>stp n. (steps0 (1, [Bk], <code M#lm>) H stp = (0, Bk \<up> n, [Oc, Oc]))"
+  "\<And> M lm. \<not> haltP M lm \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <code M#lm>))} H {(\<lambda>tp. \<exists>n. tp = (Bk \<up> n, <1::nat>))}"
 begin
 
 (* invariants for H *)
 abbreviation
-  "pre_H_inv M n \<equiv> \<lambda>(l::cell list, r::cell list). ((l, r) = ([Bk], <[code M, n]>))"
+  "pre_H_inv M n \<equiv> \<lambda>tp. tp = ([Bk], <[code M, n]>)"
 
 abbreviation
-  "post_H_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc, Oc]))"
+  "post_H_halt_inv \<equiv> \<lambda>tp. \<exists>n. tp = (Bk \<up> n, <1::nat>)"
 
 abbreviation
-  "post_H_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc]))"
+  "post_H_unhalt_inv \<equiv> \<lambda>tp. \<exists>n. tp = (Bk \<up> n, <0::nat>)"
 
 
 lemma H_halt_inv:
-  assumes "\<not> haltP0 M [n]" 
+  assumes "\<not> haltP M [n]" 
   shows "{pre_H_inv M n} H {post_H_halt_inv}"
-proof -
-  obtain stp i
-    where "steps0 (1, [Bk], <[code M, n]>) H stp = (0, Bk \<up> i, [Oc, Oc])"
-    using nh_case assms by blast
-  then show "{pre_H_inv M n} H {post_H_halt_inv}"
-    unfolding Hoare_halt_def
-    apply(auto)
-    apply(rule_tac x = stp in exI)
-    apply(auto)
-    done
-qed
+using assms nh_case by auto
 
 lemma H_unhalt_inv:
-  assumes "haltP0 M [n]" 
+  assumes "haltP M [n]" 
   shows "{pre_H_inv M n} H {post_H_unhalt_inv}"
-proof -
-  obtain stp i
-    where "steps0 (1, [Bk], <[code M, n]>) H stp = (0, Bk \<up> i, [Oc])"
-    using h_case assms by blast
-  then show "{pre_H_inv M n} H {post_H_unhalt_inv}"
-    unfolding Hoare_halt_def
-    apply(auto)
-    apply(rule_tac x = stp in exI)
-    apply(auto)
-    done
-qed
-
+using assms h_case by auto
    
 (* TM that produces the contradiction and its code *)
 abbreviation 
@@ -1112,13 +1088,13 @@
 
 (* assume tcontra does not halt on its code *)
 lemma tcontra_unhalt: 
-  assumes "\<not> haltP0 tcontra [code tcontra]"
+  assumes "\<not> haltP tcontra [code tcontra]"
   shows "False"
 proof -
   (* invariants *)
-  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]))"
+  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>))"
 
   (*
   {P1} tcopy {P2}  {P2} H {P3} 
@@ -1140,7 +1116,7 @@
     case B_halt (* of H *)
     show "{P2} H {P3}"
       unfolding P2_def P3_def
-      using assms by (rule H_halt_inv)
+      by (rule H_halt_inv[OF assms])
   qed (simp)
 
   (* {P3} dither {P3} *)
@@ -1159,20 +1135,18 @@
     apply(drule_tac x = n in spec)
     apply(case_tac "steps0 (Suc 0, [], <[code tcontra]>) tcontra n")
     apply(auto)
-    apply(drule_tac x = 1 in spec)
-    apply(simp add: numeral tape_of_nat_abv)
     done
 qed
 
 (* asumme tcontra halts on its code *)
 lemma tcontra_halt: 
-  assumes "haltP0 tcontra [code tcontra]"
+  assumes "haltP tcontra [code tcontra]"
   shows "False"
 proof - 
   (* invariants *)
-  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]))"
+  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>))"
 
   (*
   {P1} tcopy {P2}  {P2} H {P3} 
@@ -1194,7 +1168,7 @@
     case B_halt (* of H *)
     then show "{P2} H {P3}"
       unfolding P2_def P3_def
-      using assms by (rule H_unhalt_inv)
+      by (rule H_unhalt_inv[OF assms])
   qed (simp)
 
   (* {P3} dither loops *)
@@ -1208,8 +1182,8 @@
   with assms show "False"
     unfolding P1_def
     unfolding haltP_def
-    unfolding Hoare_unhalt_def
-    by (auto, metis is_final_eq)  
+    unfolding Hoare_halt_def Hoare_unhalt_def
+    by auto
 qed
       
 text {*