--- a/thys/uncomputable.thy	Wed Jan 23 15:57:35 2013 +0100
+++ b/thys/uncomputable.thy	Wed Jan 23 17:02:23 2013 +0100
@@ -1044,9 +1044,29 @@
     by(erule_tac end_correct)
 qed
 
-section {*
-  The {\em Dithering} Turing Machine 
-*}
+abbreviation
+  "pre_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[n::nat]>)"
+abbreviation
+  "post_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[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)}"
+    by (rule tcopy_correct1) (simp)
+  moreover
+  have "pre_tcopy n \<mapsto> inv_init1 (Suc n)" 
+    by (simp add: assert_imp_def tape_of_nl_abv)
+  moreover
+  have "inv_end0 (Suc n) \<mapsto> post_tcopy n" 
+    by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv)
+  ultimately
+  show "{pre_tcopy n} tcopy {post_tcopy n}" 
+    by (rule Hoare_weak)
+qed
+
+
+section {* The {\em Dithering} Turing Machine *}
 
 text {*
   The {\em Dithering} TM, when the input is @{text "1"}, it will loop forever, otherwise, it will
@@ -1177,12 +1197,11 @@
 
 lemma tinres_ex1: "tinres (Bk \<up> nb) b \<Longrightarrow> \<exists>nb. b = Bk \<up> nb"
   apply(auto simp: tinres_def replicate_add[THEN sym])
-  apply(case_tac "nb \<ge> n")
+  apply(case_tac "nb > n")
   apply(subgoal_tac "\<exists> d. nb = d + n", auto simp: replicate_add)
   apply arith
-  apply(drule_tac length_eq, simp)
-  done
-
+  by (metis Nil_is_append_conv add_diff_inverse append_assoc nat_add_commute replicate_0 replicate_add 
+    self_append_conv2)
 
 text {*
   The following locale specifies that TM @{text "H"} can be used to solve 
@@ -1311,16 +1330,8 @@
   have first: "{P1} (tcopy |+| H) {P3}" 
   proof (cases rule: Hoare_plus_halt_simple)
     case A_halt (* of tcopy *)
-    have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}"
-      by (rule tcopy_correct1) (simp)
-    moreover
-    have "P1 \<mapsto> inv_init1 (Suc code_tcontra)" unfolding P1_def
-      by (simp add: assert_imp_def tape_of_nl_abv)
-    moreover
-    have "inv_end0 (Suc code_tcontra) \<mapsto> P2" unfolding P2_def
-      by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv)
-    ultimately
-    show "{P1} tcopy {P2}" by (rule Hoare_weak)
+    show "{P1} tcopy {P2}" unfolding P1_def P2_def
+      by (rule tcopy_correct2)
   next
     case B_halt
     obtain n i
@@ -1381,16 +1392,8 @@
   have first: "{P1} (tcopy |+| H) {P3}" 
   proof (cases rule: Hoare_plus_halt_simple)
     case A_halt (* of tcopy *)
-    have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}"
-      by (rule tcopy_correct1) (simp)
-    moreover
-    have "P1 \<mapsto> inv_init1 (Suc code_tcontra)" unfolding P1_def
-      by (simp add: assert_imp_def tape_of_nl_abv)
-    moreover
-    have "inv_end0 (Suc code_tcontra) \<mapsto> P2" unfolding P2_def 
-      by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv)
-    ultimately
-    show "{P1} tcopy {P2}" by (rule Hoare_weak)
+    show "{P1} tcopy {P2}" unfolding P1_def P2_def
+      by (rule tcopy_correct2)
   next
     case B_halt
     obtain n i