
diff -r 6e1c03614d36 -r 93db7414931d thys/Uncomputable.thy
--- a/thys/Uncomputable.thy	Fri Dec 21 12:31:36 2018 +0100
+++ b/thys/Uncomputable.thy	Fri Dec 21 15:30:24 2018 +0100
@@ -77,7 +77,7 @@
          if s = 4 then inv_begin4 n tp 
          else False)"
 
-lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> 
+lemma inv_begin_step_E: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> 
   \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia"
 by (rule_tac x = "Suc i" in exI, simp)
 
@@ -88,7 +88,7 @@
 using assms
 unfolding tcopy_begin_def
 apply(cases cf)
-apply(auto simp: numeral split: if_splits)
+apply(auto simp: numeral split: if_splits elim:inv_begin_step_E)
 apply(case_tac "hd c")
 apply(auto)
 apply(case_tac c)
@@ -239,75 +239,52 @@
         inv_loop4.simps[simp del] inv_loop5.simps[simp del] 
         inv_loop6.simps[simp del]
 
-lemma [elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR"
+lemma Bk_no_Oc_repeatE[elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR"
 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, [])"
+lemma inv_loop3_Bk_empty_via_2[elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
 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, [])"
+lemma inv_loop3_Bk_empty[elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
 by (auto simp: inv_loop3.simps)
 
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop5 x (b, [Oc])"
+lemma inv_loop5_Oc_empty_via_4[elim]: "\<lbrakk>0 < x; inv_loop4 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop5 x (b, [Oc])"
 apply(auto simp: inv_loop4.simps inv_loop5.simps)
 apply(rule_tac [!] x = i in exI, 
       rule_tac [!] x  = "Suc j" in exI, simp_all)
 done
 
-lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], [])\<rbrakk> \<Longrightarrow> RR"
-by (auto simp: inv_loop4.simps inv_loop5.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, []); b \<noteq> []\<rbrakk> \<Longrightarrow> RR"
-by (auto simp: inv_loop4.simps inv_loop5.simps)
-
-lemma [elim]: "inv_loop6 x ([], []) \<Longrightarrow> RR"
-by (auto simp: inv_loop6.simps)
-
-lemma [elim]: "inv_loop6 x (b, []) \<Longrightarrow> RR" 
-by (auto simp: inv_loop6.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> b = []"
+lemma inv_loop1_Bk[elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> list = Oc # Bk \<up> x @ Oc \<up> x"
 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"
-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)"
+lemma inv_loop3_Bk_via_2[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)
 apply(rule_tac [!] x = i  in exI, rule_tac [!] x = j in exI, simp_all)
 done
 
-lemma [elim]: "Bk # list = Oc \<up> j \<Longrightarrow> RR"
-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)"
+lemma inv_loop3_Bk_move[elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
 apply(auto simp: inv_loop3.simps)
 apply(rule_tac [!] x = i in exI, 
       rule_tac [!] x = j in exI, simp_all)
 apply(case_tac [!] t, auto)
 done
 
-lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop5 x (b, Oc # list)"
+lemma inv_loop5_Oc_via_4_Bk[elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop5 x (b, Oc # list)"
 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)"
+lemma inv_loop6_Bk_via_5[elim]: "\<lbrakk>0 < x; inv_loop5 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
 by (auto simp: inv_loop6.simps inv_loop5.simps)
 
-lemma [simp]: "inv_loop5_loop x (b, Bk # list) = False"
+lemma inv_loop5_loop_no_Bk[simp]: "inv_loop5_loop x (b, Bk # list) = False"
 by (auto simp: inv_loop5.simps)
 
-lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
+lemma inv_loop6_exit_no_Bk[simp]: "inv_loop6_exit x (b, Bk # list) = False"
 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]
 
-lemma [elim]:"\<lbrakk>0 < x; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk> 
+lemma inv_loop6_loopBk_via_5[elim]:"\<lbrakk>0 < x; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk> 
           \<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"
 apply(simp only: inv_loop5_exit.simps inv_loop6_loop.simps )
 apply(erule_tac exE)+
@@ -319,10 +296,10 @@
 apply(case_tac [!] nat, simp_all)
 done
 
-lemma [simp]: "inv_loop6_loop x (b, Oc # Bk # list) = False"
+lemma inv_loop6_loop_no_Oc_Bk[simp]: "inv_loop6_loop x (b, Oc # Bk # list) = False"
 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> 
+lemma inv_loop6_exit_Oc_Bk_via_5[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)"
 apply(simp only: inv_loop5_exit.simps inv_loop6_exit.simps)
 apply(erule_tac exE)+
@@ -331,24 +308,12 @@
 apply(case_tac [!] nat, auto)
 done
 
-lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
+lemma inv_loop6_Bk_tail_via_5[elim]: "\<lbrakk>0 < x; inv_loop5 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
 apply(simp add: inv_loop5.simps inv_loop6.simps)
 apply(case_tac "hd b", simp_all, auto)
 done
 
-lemma  [simp]: "inv_loop6 x ([], Bk # xs) = False"
-apply(simp add: inv_loop6.simps inv_loop6_loop.simps
-                inv_loop6_exit.simps)
-apply(auto)
-done
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
-by (simp)
-
-lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
-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>
+lemma inv_loop6_loop_Bk_Bk_drop[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)"
 apply(simp only: inv_loop6_loop.simps)
 apply(erule_tac exE)+
@@ -357,7 +322,7 @@
 apply(case_tac [!] k, auto)
 done
 
-lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> 
+lemma inv_loop6_exit_Oc_Bk_via_loop6[elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> 
         \<Longrightarrow> inv_loop6_exit x (tl b, Oc # Bk # list)"
 apply(simp only: inv_loop6_loop.simps inv_loop6_exit.simps)
 apply(erule_tac exE)+
@@ -365,20 +330,20 @@
 apply(case_tac [!] k, auto)
 done
 
-lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
+lemma inv_loop6_Bk_tail[elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
 apply(simp add: inv_loop6.simps)
 apply(case_tac "hd b", simp_all, auto)
 done
 
-lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (Oc # b, list)"
+lemma inv_loop2_Oc_via_1[elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (Oc # b, list)"
 apply(auto simp: inv_loop1.simps inv_loop2.simps)
 apply(rule_tac x = "Suc i" in exI, auto)
 done
 
-lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (b, Bk # list)"
+lemma inv_loop2_Bk_via_Oc[elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (b, Bk # list)"
 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)"
+lemma inv_loop4_Oc_via_3[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)
 apply(rule_tac [!] x = i in exI, auto)
 apply(rule_tac [!] x = "Suc 0" in exI, rule_tac [!] x = "j - 1" in exI, auto)
@@ -386,20 +351,17 @@
 apply(case_tac [!] j, auto)
 done
 
-lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
+lemma inv_loop4_Oc_move[elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
 apply(auto simp: inv_loop4.simps)
 apply(rule_tac [!] x = "i" in exI, auto)
 apply(rule_tac [!] x = "Suc k" in exI, rule_tac [!] x = "t - 1" in exI, auto)
 apply(case_tac [!] t, simp_all)
 done
 
-lemma [simp]: "inv_loop5 x ([], list) = False"
-by (auto simp: inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps)
-
-lemma [simp]: "inv_loop5_exit x (b, Oc # list) = False"
+lemma inv_loop5_exit_no_Oc[simp]: "inv_loop5_exit x (b, Oc # list) = False"
 by (auto simp: inv_loop5_exit.simps)
 
-lemma [elim]: " \<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk>
+lemma inv_loop5_exit_Bk_Oc_via_loop[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)"
 apply(simp only: inv_loop5_loop.simps inv_loop5_exit.simps)
 apply(erule_tac exE)+
@@ -407,7 +369,7 @@
 apply(case_tac [!] k, auto)
 done
 
-lemma [elim]: "\<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk> 
+lemma inv_loop5_loop_Oc_Oc_drop[elim]: "\<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk> 
            \<Longrightarrow> inv_loop5_loop x (tl b, Oc # Oc # list)"
 apply(simp only:  inv_loop5_loop.simps)
 apply(erule_tac exE)+
@@ -416,21 +378,43 @@
 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 inv_loop5_Oc_tl[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 inv_loop1_Bk_Oc_via_6[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
+
+lemma inv_loop1_Oc_via_6[elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Oc # list); b \<noteq> []\<rbrakk> 
+           \<Longrightarrow> inv_loop1 x (tl b, hd b # Oc # list)"
 apply(auto simp: inv_loop6.simps inv_loop1.simps 
   inv_loop6_loop.simps inv_loop6_exit.simps)
 done
 
-lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Oc # list); b \<noteq> []\<rbrakk> 
-           \<Longrightarrow> inv_loop1 x (tl b, hd b # Oc # list)"
-apply(auto simp: inv_loop6.simps inv_loop1.simps 
-  inv_loop6_loop.simps inv_loop6_exit.simps)
-done
+
+lemma inv_loop_nonempty[simp]:
+  "inv_loop1 x (b, []) = False"
+  "inv_loop2 x ([], b) = False"
+  "inv_loop2 x (l', []) = False"
+  "inv_loop3 x (b, []) = False"
+  "inv_loop4 x ([], b) = False"
+  "inv_loop5 x ([], list) = False"
+  "inv_loop6 x ([], Bk # xs) = False"
+  by (auto simp: inv_loop1.simps inv_loop2.simps inv_loop3.simps inv_loop4.simps 
+   inv_loop5.simps inv_loop6.simps inv_loop5_exit.simps inv_loop5_loop.simps
+   inv_loop6_loop.simps)
+
+lemma inv_loop_nonemptyE[elim]:
+  "\<lbrakk>inv_loop5 x (b, [])\<rbrakk> \<Longrightarrow> RR" "inv_loop6 x (b, []) \<Longrightarrow> RR" 
+  "\<lbrakk>inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> b = []"
+  by (auto simp: inv_loop4.simps inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps
+ inv_loop6.simps inv_loop6_exit.simps inv_loop6_loop.simps inv_loop1.simps)
+
+lemma inv_loop6_Bk_Bk_drop[elim]: "\<lbrakk>inv_loop6 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
+  by (simp)
 
 lemma inv_loop_step: 
   "\<lbrakk>inv_loop x cf; x > 0\<rbrakk> \<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))"
@@ -476,39 +460,19 @@
 using wf_measure_loop
 by (metis wf_iff_no_infinite_down_chain)
 
-
-
-lemma [simp]: "inv_loop2 x ([], b) = False"
-by (auto simp: inv_loop2.simps)
-
-lemma  [simp]: "inv_loop2 x (l', []) = False"
-by (auto simp: inv_loop2.simps)
-
-lemma [simp]: "inv_loop3 x (b, []) = False"
-by (auto simp: inv_loop3.simps)
-
-lemma [simp]: "inv_loop4 x ([], b) = False"
-by (auto simp: inv_loop4.simps)
-
-
-lemma [elim]: 
-  "\<lbrakk>inv_loop4 x (l', []); l' \<noteq> []; x > 0;
+lemma inv_loop4_not_just_Oc[elim]: 
+  "\<lbrakk>inv_loop4 x (l', []);
   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) \<noteq> 
   length (takeWhile (\<lambda>a. a = Oc) (rev l'))\<rbrakk>
-  \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) < length (takeWhile (\<lambda>a. a = Oc) (rev l'))"
+  \<Longrightarrow> RR"
+  "\<lbrakk>inv_loop4 x (l', Bk # list);
+   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) \<noteq> 
+    length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
+    \<Longrightarrow> RR"
 apply(auto simp: inv_loop4.simps)
 apply(case_tac [!] j, simp_all add: List.takeWhile_tail)
 done
 
-
-lemma [elim]: 
-  "\<lbrakk>inv_loop4 x (l', Bk # list); l' \<noteq> []; 0 < x;
-   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) \<noteq> 
-    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))"
-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"
 by (induct x, auto)
@@ -517,12 +481,11 @@
   "P a \<Longrightarrow> takeWhile P (a\<up>x) = a\<up>x"
 by (induct x, auto)
 
-lemma [elim]: 
-   "\<lbrakk>inv_loop5 x (l', Bk # list); l' \<noteq> []; 0 < x;
+lemma inv_loop5_Bk_E[elim]: 
+   "\<lbrakk>inv_loop5 x (l', Bk # list); l' \<noteq> []; 
    length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq>
    length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
-   \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) < 
-   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
+   \<Longrightarrow> RR"
 apply(auto simp: inv_loop5.simps inv_loop5_exit.simps)
 apply(case_tac [!] j, simp_all)
 apply(case_tac [!] "nat", simp_all)
@@ -531,21 +494,20 @@
 apply(case_tac  nata, simp_all add: List.takeWhile_tail)
 done
 
-lemma [elim]: "\<lbrakk>inv_loop1 x (l', Oc # list)\<rbrakk> \<Longrightarrow> hd list = Oc"
+lemma inv_loop1_hd_Oc[elim]: "\<lbrakk>inv_loop1 x (l', Oc # list)\<rbrakk> \<Longrightarrow> hd list = Oc"
 by (auto simp: inv_loop1.simps)
 
-lemma [elim]: 
-  "\<lbrakk>inv_loop6 x (l', Bk # list); l' \<noteq> []; 0 < x;
+lemma inv_loop6_not_just_Bk[elim]: 
+  "\<lbrakk>inv_loop6 x (l', Bk # list); l' \<noteq> [];
   length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq> 
   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
-  \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) < 
-  length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
+  \<Longrightarrow> RR"
 apply(auto simp: inv_loop6.simps)
 apply(case_tac l', simp_all)
 done
 
-lemma [elim]:
-  "\<lbrakk>inv_loop2 x (l', Oc # list); l' \<noteq> []; 0 < x\<rbrakk> \<Longrightarrow> 
+lemma inv_loop2_OcE[elim]:
+  "\<lbrakk>inv_loop2 x (l', Oc # list); l' \<noteq> []\<rbrakk> \<Longrightarrow> 
   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list)) <
   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
 apply(auto simp: inv_loop2.simps)
@@ -553,22 +515,20 @@
                 takeWhile_replicate)
 done
 
-lemma [elim]: 
-  "\<lbrakk>inv_loop5 x (l', Oc # list); l' \<noteq> []; 0 < x;
+lemma inv_loop5_OcE[elim]: 
+  "\<lbrakk>inv_loop5 x (l', Oc # list); l' \<noteq> [];
   length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) \<noteq> 
   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))\<rbrakk>
-  \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) < 
-  length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
+  \<Longrightarrow> RR"
 apply(auto simp: inv_loop5.simps)
 apply(case_tac l', auto)
 done
 
-lemma[elim]: 
-  "\<lbrakk>inv_loop6 x (l', Oc # list); l' \<noteq> []; 0 < x;
+lemma inv_loop6_OcE[elim]: 
+  "\<lbrakk>inv_loop6 x (l', Oc # list); l' \<noteq> []; 
   length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list))
   \<noteq> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))\<rbrakk>
-  \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) < 
-      length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
+  \<Longrightarrow> RR"
 apply(case_tac l')
 apply(auto simp: inv_loop6.simps)
 done
@@ -668,29 +628,21 @@
         inv_end3.simps[simp del] inv_end4.simps[simp del]
         inv_end5.simps[simp del]
 
-lemma [simp]:  "inv_end1 x (b, []) = False"
-by (auto simp: inv_end1.simps)
-
-lemma [simp]: "inv_end2 x (b, []) = False"
-by (auto simp: inv_end2.simps)
-
-lemma [simp]: "inv_end3 x (b, []) = False"
-by (auto simp: inv_end3.simps)
+lemma inv_end_nonempty[simp]:
+  "inv_end1 x (b, []) = False"
+  "inv_end1 x ([], list) = False"
+  "inv_end2 x (b, []) = False"
+  "inv_end3 x (b, []) = False"
+  "inv_end4 x (b, []) = False"
+  "inv_end5 x (b, []) = False"
+  "inv_end5 x ([], Oc # list) = False"
+by (auto simp: inv_end1.simps inv_end2.simps inv_end3.simps inv_end4.simps inv_end5.simps)
 
-lemma [simp]: "inv_end4 x (b, []) = False"
-by (auto simp: inv_end4.simps)
-
-lemma [simp]: "inv_end5 x (b, []) = False"
-by (auto simp: inv_end5.simps)
-
-lemma [simp]: "inv_end1 x ([], list) = False"
-by (auto simp: inv_end1.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Bk # list); b \<noteq> []\<rbrakk>
+lemma inv_end0_Bk_via_1[elim]: "\<lbrakk>0 < x; inv_end1 x (b, Bk # list); b \<noteq> []\<rbrakk>
   \<Longrightarrow> inv_end0 x (tl b, hd b # Bk # list)"
 by (auto simp: inv_end1.simps inv_end0.simps)
 
-lemma [elim]: "\<lbrakk>0 < x; inv_end2 x (b, Bk # list)\<rbrakk> 
+lemma inv_end3_Oc_via_2[elim]: "\<lbrakk>0 < x; inv_end2 x (b, Bk # list)\<rbrakk> 
   \<Longrightarrow> inv_end3 x (b, Oc # list)"
 apply(auto simp: inv_end2.simps inv_end3.simps)
 apply(rule_tac x = "j - 1" in exI)
@@ -698,65 +650,65 @@
 apply(case_tac x, simp_all)
 done
 
-lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Bk # b, list)"
+lemma inv_end2_Bk_via_3[elim]: "\<lbrakk>0 < x; inv_end3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Bk # b, list)"
 by (auto simp: inv_end2.simps inv_end3.simps)
   
-lemma [elim]: "\<lbrakk>0 < x; inv_end4 x ([], Bk # list)\<rbrakk> \<Longrightarrow> 
+lemma inv_end5_Bk_via_4[elim]: "\<lbrakk>0 < x; inv_end4 x ([], Bk # list)\<rbrakk> \<Longrightarrow> 
   inv_end5 x ([], Bk # Bk # list)"
 by (auto simp: inv_end4.simps inv_end5.simps)
  
-lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 
+lemma inv_end5_Bk_tail_via_4[elim]: "\<lbrakk>0 < x; inv_end4 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 
   inv_end5 x (tl b, hd b # Bk # list)"
 apply(auto simp: inv_end4.simps inv_end5.simps)
 apply(rule_tac x = 1 in exI, simp)
 done
 
-lemma [elim]: "\<lbrakk>0 < x; inv_end5 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end0 x (Bk # b, list)"
+lemma inv_end0_Bk_via_5[elim]: "\<lbrakk>0 < x; inv_end5 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end0 x (Bk # b, list)"
 apply(auto simp: inv_end5.simps inv_end0.simps)
 apply(case_tac [!] j, simp_all)
 done
 
-lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
+lemma inv_end2_Oc_via_1[elim]: "\<lbrakk>0 < x; inv_end1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
 by (auto simp: inv_end1.simps inv_end2.simps)
 
-lemma [elim]: "\<lbrakk>0 < x; inv_end2 x ([], Oc # list)\<rbrakk> \<Longrightarrow>
+lemma inv_end4_Bk_Oc_via_2[elim]: "\<lbrakk>0 < x; inv_end2 x ([], Oc # list)\<rbrakk> \<Longrightarrow>
                inv_end4 x ([], Bk # Oc # list)"
 by (auto simp: inv_end2.simps inv_end4.simps)
 
-lemma [elim]:  "\<lbrakk>0 < x; inv_end2 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
+lemma inv_end4_Oc_via_2[elim]:  "\<lbrakk>0 < x; inv_end2 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
   inv_end4 x (tl b, hd b # Oc # list)"
 apply(auto simp: inv_end2.simps inv_end4.simps)
 apply(case_tac [!] j, simp_all)
 done
 
-lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
+lemma inv_end2_Oc_via_3[elim]: "\<lbrakk>0 < x; inv_end3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
 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)"
+lemma inv_end4_Bk_via_Oc[elim]: "\<lbrakk>0 < x; inv_end4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end4 x (b, Bk # list)"
 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)"
+lemma inv_end5_Bk_drop_Oc[elim]: "\<lbrakk>0 < x; inv_end5 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_end5 x ([], Bk # Oc # list)"
 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"
+lemma inv_end5_exit_no_Oc[simp]: "inv_end5_exit x (b, Oc # list) = False"
 by (auto simp: inv_end5_exit.simps)
 
-lemma [simp]: "inv_end5_loop x (tl b, Bk # Oc # list) = False"
+lemma inv_end5_loop_no_Bk_Oc[simp]: "inv_end5_loop x (tl b, Bk # Oc # list) = False"
 apply(auto simp: inv_end5_loop.simps)
 apply(case_tac [!] j, simp_all)
 done
 
-lemma [elim]:
+lemma inv_end5_exit_Bk_Oc_via_loop[elim]:
   "\<lbrakk>0 < x; inv_end5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk> \<Longrightarrow>
   inv_end5_exit x (tl b, Bk # Oc # list)"
 apply(auto simp: inv_end5_loop.simps inv_end5_exit.simps)
 apply(case_tac [!] i, simp_all)
 done
 
-lemma [elim]: 
+lemma inv_end5_loop_Oc_Oc_drop[elim]: 
   "\<lbrakk>0 < x; inv_end5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow>
   inv_end5_loop x (tl b, Oc # Oc # list)"
 apply(simp only: inv_end5_loop.simps inv_end5_exit.simps)
@@ -766,7 +718,7 @@
 apply(case_tac [!] i, simp_all)
 done
 
-lemma [elim]: "\<lbrakk>0 < x; inv_end5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 
+lemma inv_end5_Oc_tail[elim]: "\<lbrakk>0 < x; inv_end5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 
   inv_end5 x (tl b, hd b # Oc # list)"
 apply(simp add: inv_end2.simps inv_end5.simps)
 apply(case_tac "hd b", simp_all, auto)
@@ -816,9 +768,6 @@
 unfolding end_LE_def
 by (auto)
 
-lemma [simp]: "inv_end5 x ([], Oc # list) = False"
-by (auto simp: inv_end5.simps inv_end5_loop.simps)
-
 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)
@@ -878,14 +827,11 @@
 
 (* tcopy *)
 
-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)
-
-lemma [intro]: "tm_wf (tcopy_end, 0)"
-by (auto simp: tm_wf.simps tcopy_end_def)
+lemma tm_wf_tcopy[intro]:
+  "tm_wf (tcopy_begin, 0)"
+  "tm_wf (tcopy_loop, 0)"
+  "tm_wf (tcopy_end, 0)"
+by (auto simp: tm_wf.simps tcopy_end_def tcopy_loop_def tcopy_begin_def)
 
 lemma tcopy_correct1: 
   assumes "0 < x"
@@ -999,10 +945,10 @@
   where
   "halts p ns \<equiv> {(\<lambda>tp. tp = ([], <ns>))} p {(\<lambda>tp. (\<exists>k n l. tp = (Bk \<up> k,  <n::nat> @ Bk \<up> l)))}"
 
-lemma [intro, simp]: "tm_wf0 tcopy"
+lemma tm_wf0_tcopy[intro, simp]: "tm_wf0 tcopy"
 by (auto simp: tcopy_def)
 
-lemma [intro, simp]: "tm_wf0 dither"
+lemma tm_wf0_dither[intro, simp]: "tm_wf0 dither"
 by (auto simp: tm_wf.simps dither_def)
 
 text {*




