diff -r 2e9881578cb2 -r c470f1705baa thys/uncomputable.thy
--- a/thys/uncomputable.thy	Fri Jan 25 21:15:09 2013 +0000
+++ b/thys/uncomputable.thy	Fri Jan 25 22:03:03 2013 +0000
@@ -197,44 +197,42 @@
 (* tcopy_loop *)
 
 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_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop6_exit :: "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)"
+| "inv_loop1_exit x (l, r) = (l = [] \<and> r = Bk # Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0)"
+| "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_loop6_loop x (l, r) = 
+     (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> k + t + 1 = j \<and> l = Bk\<up>k @ Oc\<up>i \<and> r = Bk\<up>(Suc t) @ Oc\<up>j)"
+| "inv_loop6_exit x (l, r) = 
+     (\<exists> i j. i + j = x \<and> j > 0 \<and> l = Oc\<up>i \<and> r = Oc # Bk\<up>j @ Oc\<up>j)"
+
+fun 
+  inv_loop0 :: "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"
+  inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop6 :: "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 )"
-| "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
-  "inv_loop6_loop x (l, r) = 
-     (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> k + t + 1 = j \<and> l = Bk\<up>k @ Oc\<up>i \<and> r = Bk\<up>(Suc t) @ Oc\<up>j)"
-
-fun inv_loop6_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_loop6_exit x (l, r) = 
-     (\<exists> i j. i + j = x \<and> j > 0 \<and> l = Oc\<up>i \<and> r = Oc # Bk\<up>j @ Oc\<up>j)"
-
-fun inv_loop6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))"
+| "inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))"
 
 fun inv_loop :: "nat \<Rightarrow> config \<Rightarrow> bool"
   where
@@ -257,7 +255,7 @@
 by (case_tac t, auto)
 
 lemma [simp]: "inv_loop1 x (b, []) = False"
-by(simp add: inv_loop1.simps)
+by (simp add: inv_loop1.simps)
 
 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
 by (auto simp: inv_loop2.simps inv_loop3.simps)
@@ -274,29 +272,22 @@
 done
 
 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], [])\<rbrakk> \<Longrightarrow> RR"
-apply(auto simp: inv_loop4.simps inv_loop5.simps)
-done
+by (auto simp: inv_loop4.simps inv_loop5.simps)
 
 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, []); b \<noteq> []\<rbrakk> \<Longrightarrow> RR"
-apply(auto simp: inv_loop4.simps inv_loop5.simps)
-done
+by (auto simp: inv_loop4.simps inv_loop5.simps)
 
 lemma [elim]: "inv_loop6 x ([], []) \<Longrightarrow> RR"
-apply(auto simp: inv_loop6.simps)
-done
+by (auto simp: inv_loop6.simps)
 
-thm inv_loop6_exit.simps
 lemma [elim]: "inv_loop6 x (b, []) \<Longrightarrow> RR" 
-apply(auto simp: inv_loop6.simps)
-done
+by (auto simp: inv_loop6.simps)
 
 lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> b = []"
-apply(auto simp: inv_loop1.simps)
-done
+by (auto simp: inv_loop1.simps)
 
 lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> list = Oc # Bk \<up> x @ Oc \<up> x"
-apply(auto simp: inv_loop1.simps)
-done
+by (auto simp: inv_loop1.simps)
 
 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
 apply(auto simp: inv_loop2.simps inv_loop3.simps)
@@ -304,8 +295,7 @@
 done
 
 lemma [elim]: "Bk # list = Oc \<up> j \<Longrightarrow> RR"
-apply(case_tac j, simp_all)
-done
+by (case_tac j, simp_all)
 
 lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
 apply(auto simp: inv_loop3.simps)
@@ -315,20 +305,16 @@
 done
 
 lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop5 x (b, Oc # list)"
-apply(auto simp: inv_loop4.simps inv_loop5.simps)
-done
+by (auto simp: inv_loop4.simps inv_loop5.simps)
 
 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
-apply(auto simp: inv_loop6.simps inv_loop5.simps)
-done
+by (auto simp: inv_loop6.simps inv_loop5.simps)
 
 lemma [simp]: "inv_loop5_loop x (b, Bk # list) = False"
-apply(auto simp: inv_loop5_loop.simps)
-done
+by (auto simp: inv_loop5.simps)
 
 lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
-apply(auto simp: inv_loop6.simps)
-done
+by (auto simp: inv_loop6.simps)
 
 declare inv_loop5_loop.simps[simp del]  inv_loop5_exit.simps[simp del]
        inv_loop6_loop.simps[simp del]  inv_loop6_exit.simps[simp del]
@@ -346,8 +332,7 @@
 done
 
 lemma [simp]: "inv_loop6_loop x (b, Oc # Bk # list) = False"
-apply(auto simp: inv_loop6_loop.simps)
-done
+by (auto simp: inv_loop6_loop.simps)
 
 lemma [elim]: "\<lbrakk>x > 0; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow> 
   inv_loop6_exit x (tl b, Oc # Bk # list)"
@@ -370,12 +355,10 @@
 done
 
 lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
-apply(simp)
-done
+by (simp)
 
 lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
-apply(simp add: inv_loop6_exit.simps)
-done
+by (simp add: inv_loop6_exit.simps)
 
 lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>
               \<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"
@@ -405,8 +388,7 @@
 done
 
 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (b, Bk # list)"
-apply(auto simp: inv_loop2.simps)
-done
+by (auto simp: inv_loop2.simps)
 
 lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
 apply(auto simp: inv_loop3.simps inv_loop4.simps)
@@ -424,12 +406,10 @@
 done
 
 lemma [simp]: "inv_loop5 x ([], list) = False"
-apply(auto simp: inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps)
-done
+by (auto simp: inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps)
 
 lemma [simp]: "inv_loop5_exit x (b, Oc # list) = False"
-apply(auto simp: inv_loop5_exit.simps)
-done
+by (auto simp: inv_loop5_exit.simps)
 
 lemma [elim]: " \<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk>
   \<Longrightarrow> inv_loop5_exit x (tl b, Bk # Oc # list)"
@@ -448,14 +428,12 @@
 apply(case_tac [!] k, auto)
 done
 
-lemma [elim]: "\<lbrakk>inv_loop5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 
-  inv_loop5 x (tl b, hd b # Oc # list)"
+lemma [elim]: "\<lbrakk>inv_loop5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop5 x (tl b, hd b # Oc # list)"
 apply(simp add: inv_loop5.simps)
 apply(case_tac "hd b", simp_all, auto)
 done
 
-lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Oc # list)\<rbrakk> \<Longrightarrow> 
-               inv_loop1 x ([], Bk # Oc # list)"
+lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_loop1 x ([], Bk # Oc # list)"
 apply(auto simp: inv_loop6.simps inv_loop1.simps 
   inv_loop6_loop.simps inv_loop6_exit.simps)
 done
@@ -467,8 +445,7 @@
 done
 
 lemma inv_loop_step: 
-  "\<lbrakk>inv_loop x cf; x > 0\<rbrakk>
- \<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))"
+  "\<lbrakk>inv_loop x cf; x > 0\<rbrakk> \<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))"
 apply(case_tac cf, case_tac c, case_tac [2] aa)
 apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral split: if_splits)
 done
@@ -517,23 +494,19 @@
    "loop_LE \<equiv> (inv_image lex_triple loop_measure)"
 
 lemma wf_loop_le: "wf loop_LE"
-by(auto intro:wf_inv_image simp: loop_LE_def wf_lex_triple)
+by (auto intro:wf_inv_image simp: loop_LE_def wf_lex_triple)
 
 lemma [simp]: "inv_loop2 x ([], b) = False"
-apply(auto simp: inv_loop2.simps)
-done
+by (auto simp: inv_loop2.simps)
 
 lemma  [simp]: "inv_loop2 x (l', []) = False"
-apply(auto simp: inv_loop2.simps)
-done
+by (auto simp: inv_loop2.simps)
 
 lemma [simp]: "inv_loop3 x (b, []) = False"
-apply(auto simp: inv_loop3.simps)
-done
+by (auto simp: inv_loop3.simps)
 
 lemma [simp]: "inv_loop4 x ([], b) = False"
-apply(auto simp: inv_loop4.simps)
-done
+by (auto simp: inv_loop4.simps)
 
 lemma [elim]: 
   "\<lbrakk>inv_loop4 x (l', []); l' \<noteq> []; x > 0;
@@ -551,17 +524,15 @@
     length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
     \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) < 
     length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
-apply(auto simp: inv_loop4.simps)
-done
+by (auto simp: inv_loop4.simps)
 
 lemma takeWhile_replicate_append: 
   "P a \<Longrightarrow> takeWhile P (a\<up>x @ ys) = a\<up>x @ takeWhile P ys"
-apply(induct x, auto)
-done
+by (induct x, auto)
 
 lemma takeWhile_replicate: 
   "P a \<Longrightarrow> takeWhile P (a\<up>x) = a\<up>x"
-by(induct x, auto)
+by (induct x, auto)
 
 lemma [elim]: 
    "\<lbrakk>inv_loop5 x (l', Bk # list); l' \<noteq> []; 0 < x;
@@ -578,8 +549,7 @@
 done
 
 lemma [elim]: "\<lbrakk>inv_loop1 x (l', Oc # list)\<rbrakk> \<Longrightarrow> hd list = Oc"
-apply(auto simp: inv_loop1.simps)
-done
+by (auto simp: inv_loop1.simps)
 
 lemma [elim]: 
   "\<lbrakk>inv_loop6 x (l', Bk # list); l' \<noteq> []; 0 < x;
@@ -680,43 +650,35 @@
 
 
 (* tcopy_end *)
-  
-fun inv_end1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_end1 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x)"
 
-fun inv_end2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_end2 x (l, r) = (\<exists> i j. i + j = Suc x \<and> x > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Bk\<up>j @ Oc\<up>x)"
-
-fun inv_end3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_end3 x (l, r) =
-        (\<exists> i j. x > 0 \<and> i + j = x \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc # Bk\<up>j@ Oc\<up>x )"
-
-fun inv_end4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_end4 x (l, r) = (\<exists> any. x > 0 \<and> l = Oc\<up>x @ [Bk] \<and> r = any#Oc\<up>x)"
+fun
+  inv_end5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_end5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" 
+where  
+  "inv_end5_loop x (l, r) = 
+     (\<exists> i j. i + j = x \<and> x > 0 \<and> j > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc\<up>j @ Bk # Oc\<up>x)"
+| "inv_end5_exit x (l, r) = (x > 0 \<and> l = [] \<and> r = Bk # Oc\<up>x @ Bk # Oc\<up>x)"
 
-fun inv_end5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_end5_loop x (l, r) = 
-         (\<exists> i j. i + j = x \<and> x > 0 \<and> j > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc\<up>j @ Bk # Oc\<up>x)"
-
-fun inv_end5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_end5_exit x (l, r) = (x > 0 \<and> l = [] \<and> r = Bk # Oc\<up>x @ Bk # Oc\<up>x)"
+fun 
+  inv_end0 :: "nat \<Rightarrow> tape \<Rightarrow>  bool" and
+  inv_end1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_end2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_end3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_end4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+ 
+  inv_end5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" 
+where
+  "inv_end0 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc\<up>x @ Bk # Oc\<up>x)"
+| "inv_end1 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x)"
+| "inv_end2 x (l, r) = (\<exists> i j. i + j = Suc x \<and> x > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Bk\<up>j @ Oc\<up>x)"
+| "inv_end3 x (l, r) =
+     (\<exists> i j. x > 0 \<and> i + j = x \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc # Bk\<up>j@ Oc\<up>x)"
+| "inv_end4 x (l, r) = (\<exists> any. x > 0 \<and> l = Oc\<up>x @ [Bk] \<and> r = any#Oc\<up>x)"
+| "inv_end5 x (l, r) = (inv_end5_loop x (l, r) \<or> inv_end5_exit x (l, r))"
 
-fun inv_end5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_end5 x (l, r) = (inv_end5_loop x (l, r) \<or> inv_end5_exit x (l, r))"
-
-fun inv_end0 :: "nat \<Rightarrow> tape \<Rightarrow>  bool"
-  where
-  "inv_end0 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc\<up>x @ Bk # Oc\<up>x)"
-
-fun inv_end :: "nat \<Rightarrow> config \<Rightarrow> bool"
-  where
+fun 
+  inv_end :: "nat \<Rightarrow> config \<Rightarrow> bool"
+where
   "inv_end x (s, l, r) = (if s = 0 then inv_end0 x (l, r)
                           else if s = 1 then inv_end1 x (l, r)
                           else if s = 2 then inv_end2 x (l, r)
@@ -731,34 +693,26 @@
         inv_end5.simps[simp del]
 
 lemma [simp]:  "inv_end1 x (b, []) = False"
-apply(auto simp: inv_end1.simps)
-done
+by (auto simp: inv_end1.simps)
 
 lemma [simp]: "inv_end2 x (b, []) = False"
-apply(auto simp: inv_end2.simps)
-done
+by (auto simp: inv_end2.simps)
 
 lemma [simp]: "inv_end3 x (b, []) = False"
-apply(auto simp: inv_end3.simps)
-done
+by (auto simp: inv_end3.simps)
 
-thm inv_end4.simps
 lemma [simp]: "inv_end4 x (b, []) = False"
-apply(auto simp: inv_end4.simps)
-done
+by (auto simp: inv_end4.simps)
 
 lemma [simp]: "inv_end5 x (b, []) = False"
-apply(auto simp: inv_end5.simps)
-done
+by (auto simp: inv_end5.simps)
 
 lemma [simp]: "inv_end1 x ([], list) = False"
-apply(auto simp: inv_end1.simps)
-done
+by (auto simp: inv_end1.simps)
 
 lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Bk # list); b \<noteq> []\<rbrakk>
   \<Longrightarrow> inv_end0 x (tl b, hd b # Bk # list)"
-apply(auto simp: inv_end1.simps inv_end0.simps)
-done
+by (auto simp: inv_end1.simps inv_end0.simps)
 
 lemma [elim]: "\<lbrakk>0 < x; inv_end2 x (b, Bk # list)\<rbrakk> 
   \<Longrightarrow> inv_end3 x (b, Oc # list)"
@@ -769,13 +723,11 @@
 done
 
 lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Bk # b, list)"
-apply(auto simp: inv_end2.simps inv_end3.simps)
-done
+by (auto simp: inv_end2.simps inv_end3.simps)
   
 lemma [elim]: "\<lbrakk>0 < x; inv_end4 x ([], Bk # list)\<rbrakk> \<Longrightarrow> 
   inv_end5 x ([], Bk # Bk # list)"
-apply(auto simp: inv_end4.simps inv_end5.simps)
-done
+by (auto simp: inv_end4.simps inv_end5.simps)
  
 lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 
   inv_end5 x (tl b, hd b # Bk # list)"
@@ -789,13 +741,11 @@
 done
 
 lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
-apply(auto simp: inv_end1.simps inv_end2.simps)
-done
+by (auto simp: inv_end1.simps inv_end2.simps)
 
 lemma [elim]: "\<lbrakk>0 < x; inv_end2 x ([], Oc # list)\<rbrakk> \<Longrightarrow>
                inv_end4 x ([], Bk # Oc # list)"
-apply(auto simp: inv_end2.simps inv_end4.simps)
-done
+by (auto simp: inv_end2.simps inv_end4.simps)
 
 lemma [elim]:  "\<lbrakk>0 < x; inv_end2 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
   inv_end4 x (tl b, hd b # Oc # list)"
@@ -804,23 +754,19 @@
 done
 
 lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
-apply(auto simp: inv_end2.simps inv_end3.simps)
-done
+by (auto simp: inv_end2.simps inv_end3.simps)
 
 lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end4 x (b, Bk # list)"
-apply(auto simp: inv_end2.simps inv_end4.simps)
-done
+by (auto simp: inv_end2.simps inv_end4.simps)
 
 lemma [elim]: "\<lbrakk>0 < x; inv_end5 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_end5 x ([], Bk # Oc # list)"
-apply(auto simp: inv_end2.simps inv_end5.simps)
-done
+by (auto simp: inv_end2.simps inv_end5.simps)
 
 declare inv_end5_loop.simps[simp del]
         inv_end5_exit.simps[simp del]
 
 lemma [simp]: "inv_end5_exit x (b, Oc # list) = False"
-apply(auto simp: inv_end5_exit.simps)
-done
+by (auto simp: inv_end5_exit.simps)
 
 lemma [simp]: "inv_end5_loop x (tl b, Bk # Oc # list) = False"
 apply(auto simp: inv_end5_loop.simps)
@@ -851,16 +797,13 @@
 done
 
 lemma inv_end_step:
-  "\<lbrakk>x > 0;
- inv_end x cf\<rbrakk>
- \<Longrightarrow> inv_end x (step cf (tcopy_end, 0))"
+  "\<lbrakk>x > 0; inv_end x cf\<rbrakk> \<Longrightarrow> inv_end x (step cf (tcopy_end, 0))"
 apply(case_tac cf, case_tac c, case_tac [2] aa)
 apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral split: if_splits)
 done
 
 lemma inv_end_steps:
-  "\<lbrakk>x > 0; inv_end x cf\<rbrakk>
-\<Longrightarrow> inv_end x (steps cf (tcopy_end, 0) stp)"
+  "\<lbrakk>x > 0; inv_end x cf\<rbrakk> \<Longrightarrow> inv_end x (steps cf (tcopy_end, 0) stp)"
 apply(induct stp, simp add:steps.simps, simp)
 apply(erule_tac inv_end_step, simp)
 done
@@ -878,8 +821,7 @@
 fun end_stage :: "config \<Rightarrow> nat"
   where
   "end_stage (s, l, r) = 
-          (if s = 2 \<or> s = 3 then (length r)
-           else 0)"
+          (if s = 2 \<or> s = 3 then (length r) else 0)"
 
 fun end_step :: "config \<Rightarrow> nat"
   where
@@ -900,11 +842,10 @@
    "end_LE \<equiv> (inv_image lex_triple end_measure)"
 
 lemma wf_end_le: "wf end_LE"
-by(auto intro:wf_inv_image simp: end_LE_def wf_lex_triple)
+by (auto intro: wf_inv_image simp: end_LE_def wf_lex_triple)
 
 lemma [simp]: "inv_end5 x ([], Oc # list) = False"
-apply(auto simp: inv_end5.simps inv_end5_loop.simps)
-done
+by (auto simp: inv_end5.simps inv_end5_loop.simps)
 
 lemma end_halt: 
   "\<lbrakk>x > 0; inv_end x (Suc 0, l, r)\<rbrakk> \<Longrightarrow> 
@@ -964,18 +905,16 @@
 (* tcopy *)
 
 lemma [intro]: "tm_wf (tcopy_init, 0)"
-by(auto simp: tm_wf.simps tcopy_init_def)
+by (auto simp: tm_wf.simps tcopy_init_def)
 
 lemma [intro]: "tm_wf (tcopy_loop, 0)"
-by(auto simp: tm_wf.simps tcopy_loop_def)
+by (auto simp: tm_wf.simps tcopy_loop_def)
 
 lemma [intro]: "tm_wf (tcopy_end, 0)"
-by(auto simp: tm_wf.simps tcopy_end_def)
+by (auto simp: tm_wf.simps tcopy_end_def)
 
 lemma [intro]: "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)"
-apply(auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length
-                 tm_comp.simps)
-done
+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}"
@@ -1010,9 +949,9 @@
 qed
 
 abbreviation
-  "pre_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[n::nat]>)"
+  "pre_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). ((l, r) = ([], <[n::nat]>))"
 abbreviation
-  "post_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[n, n::nat]>)"
+  "post_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). ((l, r) = ([Bk], <[n, n::nat]>))"
 
 lemma tcopy_correct2:
   shows "{pre_tcopy n} tcopy {post_tcopy n}"
@@ -1087,13 +1026,13 @@
 
 definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool"
   where
-  "haltP p lm \<equiv> \<exists>n a b c. steps (Suc 0, [], <lm>) p n = (0, Bk \<up> a,  Oc \<up> b @ Bk \<up> c)"
+  "haltP p lm \<equiv> \<exists>n a b c. steps (1, [], <lm>) p n = (0, Bk \<up> a,  Oc \<up> b @ Bk \<up> c)"
 
 abbreviation
   "haltP0 p lm \<equiv> haltP (p, 0) lm" 
 
 lemma [intro, simp]: "tm_wf0 tcopy"
-by(auto simp: tcopy_def)
+by (auto simp: tcopy_def)
 
 lemma [intro, simp]: "tm_wf0 dither"
 by (auto simp: tm_wf.simps dither_def)
@@ -1180,85 +1119,20 @@
   The following two assumptions specifies that @{text "H"} does solve the Halting problem.
   *}
   and h_case: 
-  "\<And> M lm. (haltP0 M lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, [], <code M # lm>) H na = (0, Bk \<up> nb, [Oc]))"
+  "\<And> M lm. (haltP0 M lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, [Bk], <code M # lm>) H na = (0, Bk \<up> nb, [Oc]))"
   and nh_case: 
-  "\<And> M lm. (\<not> haltP0 M lm) \<Longrightarrow>
-             \<exists> na nb. (steps0 (1, [],  <code M # lm>) H na = (0, Bk \<up> nb, [Oc, Oc]))"
+  "\<And> M lm. (\<not> haltP0 M lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, [Bk], <code M # lm>) H na = (0, Bk \<up> nb, [Oc, Oc]))"
 begin
 
-lemma h_newcase: 
-  "\<And> M lm. haltP0 M lm \<Longrightarrow> \<exists> na nb. (steps0 (1, Bk \<up> x , <code M # lm>) H na = (0, Bk \<up> nb, [Oc]))"
-proof -
-  fix M lm
-  assume "haltP (M, 0) lm"
-  hence "\<exists> na nb. (steps (1, [], <code M # lm>) (H, 0) na
-            = (0, Bk\<up>nb, [Oc]))"
-    by (rule h_case)
-  from this obtain na nb where 
-    cond1:"(steps (1, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))" by blast
-  thus "\<exists> na nb. (steps (1, Bk\<up>x, <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))"
-  proof(rule_tac x = na in exI, case_tac "steps (1, Bk\<up>x, <code M # lm>) (H, 0) na", simp)
-    fix a b c
-    assume cond2: "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
-    have "tinres (Bk\<up>nb) b \<and> [Oc] = c \<and> 0 = a"
-    proof(rule_tac tinres_steps)
-      show "tinres [] (Bk\<up>x)"
-        apply(simp add: tinres_def)
-        apply(auto)
-        done
-    next
-      show "(steps (1, [], <code M # lm>) (H, 0) na
-            = (0, Bk\<up>nb, [Oc]))"
-        by(simp add: cond1[simplified])
-    next
-      show "steps (1, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
-        by(simp add: cond2[simplified])
-    qed
-    thus "a = 0 \<and> (\<exists>nb. b = (Bk\<up>nb)) \<and> c = [Oc]"
-      by(auto elim: tinres_ex1)
-  qed
-qed
-
-lemma nh_newcase: 
-  "\<And> M lm. \<not> (haltP (M, 0) lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, Bk\<up>x, <code M # lm>) H na = (0, Bk\<up>nb, [Oc, Oc]))"
-proof -
-  fix M lm
-  assume "\<not> haltP (M, 0) lm"
-  hence "\<exists> na nb. (steps (1, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
-    by (rule nh_case)
-  from this obtain na nb where 
-    cond1: "(steps (1, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))" by blast
-  thus "\<exists> na nb. (steps (1, Bk\<up>x, <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
-  proof(rule_tac x = na in exI, case_tac "steps (1, Bk\<up>x, <code M # lm>) (H, 0) na", simp)
-    fix a b c
-    assume cond2: "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
-    have "tinres (Bk\<up>nb) b \<and> [Oc, Oc] = c \<and> 0 = a"
-    proof(rule_tac tinres_steps)
-      show "tinres [] (Bk\<up>x)"
-        apply(auto simp: tinres_def)
-        done
-    next
-      show "(steps (Suc 0, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
-        by(simp add: cond1[simplified])
-    next
-      show "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
-        by(simp add: cond2[simplified])
-    qed
-    thus "a = 0 \<and> (\<exists>nb. b =  Bk\<up>nb) \<and> c = [Oc, Oc]"
-      by(auto elim: tinres_ex1)
-  qed
-qed
-
-
 (* invariants for H *)
 abbreviation
-  "pre_H_inv M n \<equiv> \<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code M, n]>)"
+  "pre_H_inv M n \<equiv> \<lambda>(l::cell list, r::cell list). ((l, r) = ([Bk], <[code M, n]>))"
 
 abbreviation
-  "post_H_halt_inv \<equiv> \<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]"
+  "post_H_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc, Oc]))"
 
 abbreviation
-  "post_H_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]"
+  "post_H_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc]))"
 
 
 lemma H_halt_inv:
@@ -1266,8 +1140,8 @@
   shows "{pre_H_inv M n} H {post_H_halt_inv}"
 proof -
   obtain stp i
-    where "steps0 (1, Bk \<up> 1, <[code M, n]>) H stp = (0, Bk \<up> i, [Oc, Oc])"
-    using nh_newcase[of "M" "[n]" "1", OF assms] by auto 
+    where "steps0 (1, [Bk], <[code M, n]>) H stp = (0, Bk \<up> i, [Oc, Oc])"
+    using nh_case[of "M" "[n]", OF assms] by auto
   then show "{pre_H_inv M n} H {post_H_halt_inv}"
     unfolding Hoare_halt_def
     apply(auto)
@@ -1281,8 +1155,8 @@
   shows "{pre_H_inv M n} H {post_H_unhalt_inv}"
 proof -
   obtain stp i
-    where "steps0 (1, Bk \<up> 1, <[code M, n]>) H stp = (0, Bk \<up> i, [Oc])"
-    using h_newcase[of "M" "[n]" "1", OF assms] by auto 
+    where "steps0 (1, [Bk], <[code M, n]>) H stp = (0, Bk \<up> i, [Oc])"
+    using h_case[of "M" "[n]", OF assms] by auto 
   then show "{pre_H_inv M n} H {post_H_unhalt_inv}"
     unfolding Hoare_halt_def
     apply(auto)
@@ -1323,12 +1197,12 @@
   proof (cases rule: Hoare_plus_halt_simple)
     case A_halt (* of tcopy *)
     show "{P1} tcopy {P2}" unfolding P1_def P2_def
-      by (simp) (rule tcopy_correct2)
+      by (rule tcopy_correct2)
   next
     case B_halt (* of H *)
     show "{P2} H {P3}"
       unfolding P2_def P3_def
-      using assms by (simp) (rule H_halt_inv)
+      using assms by (rule H_halt_inv)
   qed (simp)
 
   (* {P3} dither {P3} *)
@@ -1377,12 +1251,12 @@
   proof (cases rule: Hoare_plus_halt_simple)
     case A_halt (* of tcopy *)
     show "{P1} tcopy {P2}" unfolding P1_def P2_def
-      by (simp) (rule tcopy_correct2)
+      by (rule tcopy_correct2)
   next
     case B_halt (* of H *)
     then show "{P2} H {P3}"
       unfolding P2_def P3_def
-      using assms by (simp) (rule H_unhalt_inv)
+      using assms by (rule H_unhalt_inv)
   qed (simp)
 
   (* {P3} dither loops *)