# HG changeset patch
# User Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
# Date 1545402624 -3600
# Node ID 93db7414931d9331099e5ec2b57a56f850000940
# Parent  6e1c03614d36b72d2e0b6f8119ecabd8e0114667
More naming of lemmas, cleanup of Abacus and NatBijection

diff -r 6e1c03614d36 -r 93db7414931d thys/Abacus.thy
--- a/thys/Abacus.thy	Fri Dec 21 12:31:36 2018 +0100
+++ b/thys/Abacus.thy	Fri Dec 21 15:30:24 2018 +0100
@@ -362,10 +362,6 @@
     done
 qed
 
-lemma startof_not0[simp]: "0 < start_of ly as"
-apply(simp add: start_of.simps)
-done
-
 lemma startof_ge1[simp]: "Suc 0 \<le> start_of ly as"
 apply(simp add: start_of.simps)
 done
@@ -423,11 +419,6 @@
 apply(subgoal_tac "take (Suc as) xs = take as xs @ [xs ! as]", simp)
 by auto
 
-lemma concat_take_suc_iff: "Suc n \<le> length tps \<Longrightarrow> 
-       concat (take n tps) @ (tps ! n) = concat (take (Suc n) tps)"
-apply(drule_tac concat_suc, simp)
-done
-
 lemma concat_drop_suc_iff: 
    "Suc n < length tps \<Longrightarrow> concat (drop (Suc n) tps) = 
            tps ! Suc n @ concat (drop (Suc (Suc n)) tps)"
@@ -458,9 +449,6 @@
 
 declare append_assoc[simp]
 
-lemma map_of:  "n < length xs \<Longrightarrow> (map f xs) ! n = f (xs ! n)"
-by(auto)
-
 lemma length_tms_of[simp]: "length (tms_of aprog) = length aprog"
 apply(auto simp: tms_of.simps tpairs_of.simps)
 done
@@ -470,7 +458,7 @@
   abc_fetch as aprog = Some ins\<rbrakk>
   \<Longrightarrow> ci ly (start_of ly as) ins = tms_of aprog ! as"
 apply(simp add: tms_of.simps tpairs_of.simps 
-      abc_fetch.simps  map_of del: map_append split: if_splits)
+      abc_fetch.simps del: map_append split: if_splits)
 done
 
 lemma t_split:"\<lbrakk>
@@ -488,41 +476,13 @@
 apply(rule_tac ci_nth, auto)
 done
 
-lemma math_sub: "\<lbrakk>x >= Suc 0; x - 1 = z\<rbrakk> \<Longrightarrow> x + y - Suc 0 = z + y"
-by auto
-
-lemma start_more_one: "as \<noteq> 0 \<Longrightarrow> start_of ly as >= Suc 0"
-apply(induct as, simp add: start_of.simps)
-apply(case_tac as, auto simp: start_of.simps)
-done
-
 lemma div_apart: "\<lbrakk>x mod (2::nat) = 0; y mod 2 = 0\<rbrakk> 
           \<Longrightarrow> (x + y) div 2 = x div 2 + y div 2"
   by(auto)
 
-lemma div_apart_iff: "\<lbrakk>x mod (2::nat) = 0; y mod 2 = 0\<rbrakk> \<Longrightarrow> 
-           (x + y) mod 2 = 0"
-by(auto)
-
 lemma length_layout_of[simp]: "length (layout_of aprog) = length aprog"
 by(auto simp: layout_of.simps)
 
-lemma start_of_ind: "\<lbrakk>as < length aprog; ly = layout_of aprog\<rbrakk> \<Longrightarrow> 
-       start_of ly (Suc as) = start_of ly as + 
-                          length ((tms_of aprog) ! as) div 2"
-  by (auto simp: start_of.simps tms_of.simps layout_of.simps 
-                 tpairs_of.simps ci_length take_Suc take_Suc_conv_app_nth)
-
-lemma concat_take_suc: "Suc n \<le> length xs \<Longrightarrow>
-  concat (take (Suc n) xs) = concat (take n xs) @ (xs ! n)"
-  using concat_suc.
-
-lemma ci_in_set[simp]: 
-  "\<lbrakk>as < length aprog; (abc_fetch as aprog) = Some ins\<rbrakk>
-  \<Longrightarrow> ci (layout_of aprog) 
-  (start_of (layout_of aprog) as) (ins) \<in> set (tms_of aprog)"
-  by(insert ci_nth[of "layout_of aprog" aprog as], simp)
-
 lemma length_tms_of_elem_even[intro]:  "n < length ap \<Longrightarrow> length (tms_of ap ! n) mod 2 = 0"
   apply(cases "ap ! n")
   by (auto simp: tms_of.simps tpairs_of.simps ci.simps length_findnth tinc_b_def tdec_b_def)
@@ -1247,10 +1207,6 @@
 apply(simp add: tape_of_nat_def tape_of_list_def)
 done
 
-lemma tape_empty_list[simp]: " <([]::nat list)> = []"
-apply(simp add: tape_of_list_def)
-done
-
 lemma inv_locate[simp]: "\<lbrakk>inv_locate_b (as, am) (q, aaa, Bk # xs) ires; \<exists>n. xs = Bk\<up>n\<rbrakk>
             \<Longrightarrow> inv_locate_a (as, am) (Suc q, Bk # aaa, xs) ires"
 apply(simp add: inv_locate_b.simps inv_locate_a.simps)
@@ -1338,9 +1294,6 @@
 
 (*inv: from locate_b to after_write*)
 
-lemma not_even_then_odd[simp]: "(a mod 2 \<noteq> 0) = (a mod 2 = Suc 0)  "
-by arith
-
 lemma div_rounding_down[simp]: "(2*q - Suc 0) div 2 = (q - 1)" "(Suc (2*q)) div 2 = q"
 by arith+
 
@@ -1399,10 +1352,7 @@
       done
   qed
 qed
-            
-lemma inv_locate_aI[intro]: "inv_locate_a (as, lm) (0, Bk # Bk # ires, <lm> @ Bk \<up> x) ires"
-apply(auto simp: crsp.simps inv_locate_a.simps at_begin_norm.simps)
-done
+
 lemma inv_locate_a_via_crsp[simp]:
  "crsp ly (as, lm) (s, l, r) ires \<Longrightarrow> inv_locate_a (as, lm) (0, l, r) ires"
 apply(auto simp: crsp.simps inv_locate_a.simps at_begin_norm.simps)
@@ -1524,14 +1474,6 @@
   apply(drule_tac length_equal, simp)
   by (metis (no_types, lifting) add_diff_inverse_nat append.assoc append_eq_append_conv length_append length_replicate list.inject)
 
-lemma inv_after_write_via_locate_b[simp]: "inv_locate_b (as, am) (n, aaa, []) ires \<Longrightarrow> 
-     inv_after_write (as, abc_lm_s am n (Suc (abc_lm_v am n))) 
-                     (s, aaa, [Oc]) ires"
-apply(insert inv_locate_b_2_after_write [of as am n aaa "[]"])
-by(simp)
-
-
-
 (*inv: from after_write to after_move*)
 lemma inv_after_move_Oc_via_write[simp]: "inv_after_write (as, lm) (x, l, Oc # r) ires
                 \<Longrightarrow> inv_after_move (as, lm) (y, Oc # l, r) ires"
@@ -1608,15 +1550,6 @@
 apply(case_tac [!] rn, simp_all)
 done
 
-lemma inv_after_clear_singleton_Bk[simp]: "inv_after_clear (as, lm) (x, l, []) ires\<Longrightarrow> 
-               inv_after_clear (as, lm) (y, l, [Bk]) ires" 
-by(auto simp: inv_after_clear.simps)
-
-lemma inv_on_right_moving_Bk[simp]: "inv_after_clear (as, lm) (x, l, []) ires
-             \<Longrightarrow> inv_on_right_moving (as, lm) (y, Bk # l, []) ires"
-by(insert 
-    inv_after_clear_2_inv_on_right_moving[of as lm n l "[]"], simp)
-
 (*inv: from on_right_moving to on_right_movign*)
 lemma inv_on_right_moving_Oc[simp]: "inv_on_right_moving (as, lm) (x, l, Oc # r) ires
       \<Longrightarrow> inv_on_right_moving (as, lm) (y, Oc # l, r) ires"
@@ -1646,12 +1579,6 @@
 apply(rule_tac x = lm1 in exI, rule_tac x = "[]" in exI, simp)
 done
 
-(*inv: from on_right_moving to after_write*)
-lemma inv_after_write_singleton_Oc[simp]: "inv_on_right_moving (as, lm) (x, l, []) ires
-       \<Longrightarrow> inv_after_write (as, lm) (y, l, [Oc]) ires"
-apply(rule_tac inv_on_right_moving_2_inv_on_right_moving, simp)
-done
-
 (*inv: from on_left_moving to on_left_moving*)
 lemma no_inv_on_left_moving_in_middle_B_Oc[simp]: "inv_on_left_moving_in_middle_B (as, lm) 
                (s, l, Oc # r) ires = False"
@@ -1750,22 +1677,11 @@
 apply(auto simp: inv_on_left_moving_norm.simps)
 done
 
-lemma inv_on_left_moving_Bk[simp]: "inv_on_left_moving (as, lm) (s, l, []) ires\<Longrightarrow> 
-     inv_on_left_moving (as, lm) (6 + 2 * n, l, [Bk]) ires"
-apply(simp add: inv_on_left_moving.simps)
-apply(auto simp: inv_on_left_moving_in_middle_B.simps)
-done
-
 lemma inv_on_left_moving_no_empty[simp]: "inv_on_left_moving (as, lm) (s, l, []) ires = False"
 apply(simp add: inv_on_left_moving.simps)
 apply(simp add: inv_on_left_moving_in_middle_B.simps)
 done
 
-lemma inv_on_left_moving_cases_left[simp]: "inv_on_left_moving (as, lm) (s, l, []) ires
- \<Longrightarrow> (l = [] \<longrightarrow> inv_check_left_moving (as, lm) (s', [], [Bk]) ires) \<and>
-    (l \<noteq> [] \<longrightarrow> inv_check_left_moving (as, lm) (s', tl l, [hd l]) ires)"
-by simp
-
 lemma Bk_plus_one[intro]: "\<exists>rna. Bk # Bk \<up> rn = Bk \<up> rna"
   apply(rule_tac x = "Suc rn" in exI, simp)
   done
@@ -1792,13 +1708,6 @@
      inv_check_left_moving_in_middle (as, lm) (s', [Bk], Oc # r) ires"
 apply(auto simp: inv_check_left_moving_in_middle.simps )
 done
-lemma inv_on_left_moving_in_middle_B_Bk_Oc_via_check[simp]: 
- "inv_check_left_moving_in_middle (as, lm) (s, [], Oc # r) ires
-   \<Longrightarrow> inv_on_left_moving_in_middle_B (as, lm) (s', [], Bk # Oc # r) ires"
-apply(insert 
-inv_check_left_moving_in_middle_2_on_left_moving_in_middle_B[of 
-                  as lm n "[]" r], simp)
-done 
 
 lemma inv_on_left_moving_norm_Oc_Oc_via_middle[simp]: "inv_check_left_moving_in_middle (as, lm) 
                        (s, Oc # list, Oc # r) ires
@@ -2280,31 +2189,8 @@
     by arith
 qed
     
-lemma abc_fetch_contrE[elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e); as < e; 
-  Suc (start_of (layout_of ap) as + 2 * n) = start_of (layout_of ap) e\<rbrakk> \<Longrightarrow> RR"
-  by(drule_tac start_of_ge, auto)
-
-lemma abc_fetch_contrE2[elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e); as > e;
-  Suc (start_of (layout_of ap) as + 2 * n) = start_of (layout_of ap) e\<rbrakk> \<Longrightarrow> RR"
-apply(drule_tac ly = "layout_of ap" in start_of_less[of])
-apply(arith)
-done
-
-lemma abc_fetch_contrE3[elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e);
-  Suc (start_of (layout_of ap) as + 2 * n) = start_of (layout_of ap) e\<rbrakk> \<Longrightarrow> RR"
-apply(subgoal_tac "as = e \<or> as < e \<or> as > e", auto)
-done
-
-lemma fetch_c_Oc[simp]:"fetch (ci (ly) (start_of ly as) (Dec n e)) (Suc (2 * n))  Oc
-  = (R, start_of ly as + 2*n + 1)"
-apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
-done
-
-
 declare dec_inv_1.simps[simp del]
 
-
 lemma start_of_ineq1[simp]: 
  "\<lbrakk>abc_fetch as aprog = Some (Dec n e); ly = layout_of aprog\<rbrakk>
    \<Longrightarrow> (start_of ly e \<noteq> Suc (start_of ly as + 2 * n) \<and>
@@ -2424,11 +2310,6 @@
 apply(auto simp: dec_after_clear.simps dec_right_move.simps split: if_splits)
 done
 
-lemma dec_right_move_Bk_via_clear_empty[simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, []) ires\<rbrakk>
-             \<Longrightarrow> dec_right_move (as, am) (s', Bk # l, []) ires"
-apply(auto simp: dec_after_clear.simps dec_right_move.simps )
-done
-
 lemma dec_right_move_Bk_Bk_via_clear[simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, []) ires\<rbrakk>
              \<Longrightarrow> dec_right_move (as, am) (s', Bk # l, [Bk]) ires"
 apply(auto simp: dec_after_clear.simps dec_right_move.simps split: if_splits)
@@ -2454,12 +2335,6 @@
 apply(simp add: dec_right_move.simps)
 done
 
-lemma dec_check_right_move_Bk_via_move[simp]: "\<lbrakk>dec_right_move (as, am) (s, l, []) ires\<rbrakk>
-             \<Longrightarrow> dec_check_right_move (as, am) (s, Bk # l, []) ires"
-apply(insert dec_right_move_2_check_right_move[of as am s l "[]" s'], 
-      simp)
-done
-
 lemma dec_check_right_move_nonempty[simp]: "dec_check_right_move (as, am) (s, l, r) ires\<Longrightarrow> l \<noteq> []"
 apply(auto simp: dec_check_right_move.simps split: if_splits)
 done
@@ -2504,11 +2379,6 @@
 apply(rule_tac x = "[m]" in exI, auto)
 done
 
-lemma inv_on_left_moving_in_middle_B_Oc_Bk_Bk[simp]: "inv_on_left_moving_in_middle_B (as, [m])
-  (s', Oc # Oc\<up>m @ Bk # Bk # ires, [Bk]) ires"
-apply(simp add: inv_on_left_moving_in_middle_B.simps)
-done
-
 
 lemma inv_on_left_moving_in_middle_B_Oc_Bk_Bks_rev[simp]: "lm1 \<noteq> [] \<Longrightarrow> 
   inv_on_left_moving_in_middle_B (as, lm1 @ [m]) (s', 
@@ -2518,14 +2388,6 @@
 apply(simp add: tape_of_nl_cons split: if_splits)
 done
 
-lemma inv_on_left_moving_in_middle_B_Oc_Bk_Bk_rev[simp]: "lm1 \<noteq> [] \<Longrightarrow> 
-  inv_on_left_moving_in_middle_B (as, lm1 @ [m]) (s', 
-  Oc # Oc\<up> m @ Bk # <rev lm1> @ Bk # Bk # ires, [Bk]) ires"
-apply(simp only: inv_on_left_moving_in_middle_B.simps)
-apply(rule_tac x = "lm1 @ [m ]" in exI, rule_tac x = "[]" in exI, simp)
-apply(simp add: tape_of_nl_cons split: if_splits)
-done
-
 lemma inv_on_left_moving_Bk_tail[simp]: "dec_left_move (as, am) (s, l, Bk # r) ires
        \<Longrightarrow> inv_on_left_moving (as, am) (s', tl l, hd l # Bk # r) ires"
 apply(auto simp: dec_left_move.simps inv_on_left_moving.simps split: if_splits)
@@ -2583,11 +2445,6 @@
 apply(rule_tac x = lm1 in exI, simp)
 done
 
-lemma inv_stop_abc_lm_s_nonempty[simp]: 
- "inv_stop (as, abc_lm_s am n (abc_lm_v am n)) (s, l, r) ires \<Longrightarrow> l \<noteq> []"
-apply(auto simp: inv_stop.simps)
-done
-
 lemma dec_false_1[simp]:
  "\<lbrakk>abc_lm_v am n = 0; inv_locate_b (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
   \<Longrightarrow> False"
@@ -2647,63 +2504,12 @@
 apply(simp_all only: exp_ind Nat.Suc_diff_le del: replicate_Suc, simp_all)
 apply(auto simp: inv_on_left_moving_in_middle_B.simps split: if_splits)
 apply(case_tac [!] m, simp_all)
-done
-
-lemma update_zero_to_zero[simp]: "\<lbrakk>am ! n = (0::nat); n < length am\<rbrakk> \<Longrightarrow> am[n := 0] = am"
-apply(simp add: list_update_same_conv)
-done
-
-lemma abc_lm_v_zero: "\<lbrakk>abc_lm_v (a # list) 0 = 0\<rbrakk> \<Longrightarrow> a = 0"
-apply(simp add: abc_lm_v.simps split: if_splits)
-done
-
-lemma inv_locate_a_via_stop[simp]: 
- "inv_stop (as, abc_lm_s am n 0) 
-          (start_of (layout_of aprog) e, aaa, Oc # xs) ires
-  \<Longrightarrow> inv_locate_a (as, abc_lm_s am n 0) (0, aaa, Oc # xs) ires"
-apply(simp add: inv_locate_a.simps)
-apply(rule disjI1)
-apply(auto simp: inv_stop.simps at_begin_norm.simps)
-done
-
-lemma inv_locate_b_cases_via_stop[simp]: 
- "\<lbrakk>inv_stop (as, abc_lm_s am n 0) 
-          (start_of (layout_of aprog) e, aaa, Oc # xs) ires\<rbrakk>
-  \<Longrightarrow> inv_locate_b (as, am) (0, Oc # aaa, xs) ires \<or> 
-      inv_locate_b (as, abc_lm_s am n 0) (0, Oc # aaa, xs) ires"
-apply(simp)
-done
-
-lemma dec_false2: 
- "inv_stop (as, abc_lm_s am n 0) 
-  (start_of (layout_of aprog) e, aaa, Bk # xs) ires = False"
-apply(auto simp: inv_stop.simps abc_lm_s.simps)
-apply(case_tac [!] am, auto)
-apply(case_tac [!] n, auto simp: tape_of_nl_cons split: if_splits)
-done
-
-lemma dec_false3:
-   "inv_stop (as, abc_lm_s am n 0) 
-              (start_of (layout_of aprog) e, aaa, []) ires = False"
-apply(auto simp: inv_stop.simps abc_lm_s.simps)
-done
+  done
 
 declare dec_inv_1.simps[simp del]
 
 declare inv_locate_n_b.simps [simp del]
-
-lemma inv_locate_n_b_Oc_via_at_begin_fst_bwtn[simp]:
-  "\<lbrakk>0 < abc_lm_v am n; 0 < n; 
-    at_begin_fst_bwtn (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
- \<Longrightarrow> inv_locate_n_b (as, am) (n, Oc # aaa, xs) ires"
-apply(simp add: at_begin_fst_bwtn.simps inv_locate_n_b.simps )
-done
  
-lemma Suc_minus:"length am + tn = n
-       \<Longrightarrow> Suc tn = Suc n - length am "
-apply(arith)
-done
-
 lemma dec_first_on_right_moving_Oc_via_inv_locate_n_b[simp]:
  "\<lbrakk>inv_locate_n_b (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
  \<Longrightarrow> dec_first_on_right_moving n (as, abc_lm_s am n (abc_lm_v am n))  
@@ -3037,10 +2843,6 @@
 apply(simp add: inv_check_left_moving.simps inv_check_left_moving_in_middle.simps)
 done
 
-lemma inv_check_left_moving_nonempty[simp]:
-  "inv_check_left_moving (as, lm) (s, [], Oc # list) ires = False"
-  by auto
-
 lemma inv_locate_n_b_Oc_via_at_begin_norm[simp]:
 "\<lbrakk>0 < abc_lm_v am n; 
   at_begin_norm (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
@@ -3376,14 +3178,6 @@
     done
 qed
 
-lemma fetch_Nops[simp]: 
-  "\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow>
-        fetch (tp @ [(Nop, 0), (Nop, 0)]) (start_of ly (length ap)) b = 
-       (Nop, 0)"
-apply(case_tac b)
-apply(simp_all add: start_of.simps fetch.simps nth_append)
-done
-
 lemma length_tp:
   "\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow> 
   start_of ly (length ap) = Suc (length tp div 2)"
@@ -3511,7 +3305,7 @@
     by(rule_tac tm_append_first_steps_eq, simp_all add: crsp.simps)
   from b have d: "s' > 0 \<and> stpa \<ge> stp"
     by(simp add: crsp.simps)
-  then obtain diff where e: "stpa = stp + diff"   by (metis le_iff_add)
+  then obtain diff where e: "stpa = stp + diff" by (metis le_iff_add)
   obtain s'' l'' r'' where f:
     "steps (1, l, r) (tp @ shift (mopup n) off, 0) stp = (s'', l'', r'') \<and> is_final (s'', l'', r'')"
     using h
diff -r 6e1c03614d36 -r 93db7414931d thys/Abacus_Defs.thy
--- a/thys/Abacus_Defs.thy	Fri Dec 21 12:31:36 2018 +0100
+++ b/thys/Abacus_Defs.thy	Fri Dec 21 15:30:24 2018 +0100
@@ -2,7 +2,7 @@
    Author: Jian Xu, Xingyuan Zhang, and Christian Urban
 *)
 
-header {* Alternative Definitions for Translating Abacus Machines to TMs *}
+chapter {* Alternative Definitions for Translating Abacus Machines to TMs *}
 
 theory Abacus_Defs
 imports Abacus
@@ -13,7 +13,7 @@
 
 fun address :: "abc_prog \<Rightarrow> nat \<Rightarrow> nat"
   where
-  "address p x = (Suc (listsum (take x (layout p)))) "
+  "address p x = (Suc (sum_list (take x (layout p)))) "
 
 abbreviation
   "TMGoto \<equiv> [(Nop, 1), (Nop, 1)]"
diff -r 6e1c03614d36 -r 93db7414931d thys/Abacus_Hoare.thy
--- a/thys/Abacus_Hoare.thy	Fri Dec 21 12:31:36 2018 +0100
+++ b/thys/Abacus_Hoare.thy	Fri Dec 21 15:30:24 2018 +0100
@@ -240,6 +240,7 @@
 apply(rule_tac abc_comp_frist_steps_halt_eq', simp_all)
 done
 
+
 lemma abc_comp_second_step_eq: 
   assumes exec: "abc_step_l (s, lm) (abc_fetch s B) = (sa, lma)"
   shows "abc_step_l (s + length A, lm) (abc_fetch (s + length A) (A [+] B))
diff -r 6e1c03614d36 -r 93db7414931d thys/NatBijection.thy
--- a/thys/NatBijection.thy	Fri Dec 21 12:31:36 2018 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,274 +0,0 @@
-theory NatBijection
-imports Main Parity "~~/src/HOL/Library/Discrete"
-begin
-
-declare One_nat_def[simp del]
-
-fun oddfactor :: "nat \<Rightarrow> nat" where
-  [simp del]: "oddfactor n = (if n = 0 then 0 
-                              else if even n then oddfactor (n div 2) else ((n - 1) div 2))"
-
-fun evenfactor :: "nat \<Rightarrow> nat" where
-  [simp del]: "evenfactor n = (if n = 0 then 0 
-                               else if even n then 2 * evenfactor (n div 2) else 1)"
-
-lemma oddfactor [simp]:
-  "oddfactor 0 = 0"
-  "odd n \<Longrightarrow> oddfactor n = (n - 1) div 2"
-  "even n \<Longrightarrow> oddfactor n = oddfactor (n div 2)"
-by (simp_all add: oddfactor.simps)
-
-lemma evenfactor [simp]:
-  "evenfactor 0 = 0"
-  "odd n \<Longrightarrow> evenfactor n = 1"
-  "even n \<Longrightarrow> evenfactor n = 2 * evenfactor (n div 2)"
-apply(simp_all add: evenfactor.simps)
-apply(case_tac n)
-apply(simp_all)
-done
-
-fun penc :: "(nat \<times> nat) \<Rightarrow> nat" where
-  "penc (m, n) = (2 ^ m) * (2 * n + 1) - 1"
-
-fun pdec :: "nat \<Rightarrow> nat \<times> nat" where
-  "pdec z = (Discrete.log (evenfactor (Suc z)), oddfactor (Suc z))"
-
-lemma q2: "pdec (penc m) = m"
-apply(case_tac m)
-apply(simp)
-apply(simp only: penc.simps pdec.simps)
-apply(case_tac m)
-apply(simp only: penc.simps pdec.simps)
-apply(subst y1)
-apply(subst y2)
-apply(simp)
-done
-
-
-lemma oddfactor_odd:
-  "oddfactor n = 0 \<or> odd (oddfactor n)" 
-apply(induct n rule: nat_less_induct)
-apply(case_tac "n = 0")
-apply(simp)
-apply(case_tac "odd n")
-apply(auto)
-done
-
-lemma bigger: "oddfactor (Suc n) > 0"
-apply(induct n rule: nat_less_induct)
-apply(case_tac "n = 0")
-apply(simp)
-apply(case_tac "odd n")
-apply(auto)
-apply(drule_tac x="n div 2" in spec)
-apply(drule mp)
-apply(auto)
-by (smt numeral_2_eq_2 odd_nat_plus_one_div_two)
-
-fun pencode :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
-  "pencode m n = (2 ^ m) * (2 * n + 1) - 1"
-
-fun pdecode2 :: "nat \<Rightarrow> nat" where
-  "pdecode2 z = (oddfactor (Suc z) - 1) div 2"
-
-fun pdecode1 :: "nat \<Rightarrow> nat" where
-  "pdecode1 z = Discrete.log ((Suc z) div (oddfactor (Suc z)))"
-
-lemma k:
-  "odd n \<Longrightarrow> oddfactor (2 ^ m * n) = n"
-apply(induct m)
-apply(simp_all)
-done
-
-lemma ww: "\<exists>k. n = 2 ^ k * oddfactor n"
-apply(induct n rule: nat_less_induct)
-apply(case_tac "n=0")
-apply(simp)
-apply(case_tac "odd n")
-apply(simp)
-apply(rule_tac x="0" in exI)
-apply(simp)
-apply(simp)
-apply(drule_tac x="n div 2" in spec)
-apply(erule impE)
-apply(simp)
-apply(erule exE)
-apply(rule_tac x="Suc k" in exI)
-apply(simp)
-by (metis div_mult_self2_is_id even_mult_two_ex nat_mult_assoc nat_mult_commute zero_neq_numeral)
-
-
-lemma test: "x = y \<Longrightarrow> 2 * x = 2 * y"
-by simp
-
-lemma m: "0 < n ==> 2 ^ Discrete.log (n div (oddfactor n)) = n div (oddfactor n)"
-apply(induct n rule: nat_less_induct)
-apply(case_tac "n=0")
-apply(simp)
-apply(case_tac "odd n")
-apply(simp)
-apply(drule_tac x="n div 2" in spec)
-apply(drule mp)
-apply(auto)[1]
-apply(drule mp)
-apply (metis One_nat_def Suc_lessI div_2_gt_zero odd_1_nat)
-apply(subst (asm) oddfactor(3)[symmetric])
-apply(simp)
-apply(subst (asm) oddfactor(3)[symmetric])
-apply(simp)
-apply(subgoal_tac "n div 2 div oddfactor n = n div (oddfactor n) div 2")
-prefer 2
-apply (metis div_mult2_eq nat_mult_commute)
-apply(simp only: log_half)
-apply(case_tac "n div oddfactor n = 0")
-apply(simp)
-apply(simp del: oddfactor)
-apply(drule test)
-apply(subst (asm) power.simps(2)[symmetric])
-apply(subgoal_tac "Suc (Discrete.log (n div oddfactor n) - 1) = Discrete.log (n div oddfactor n)")
-prefer 2
-apply (smt log.simps Suc_1 div_less div_mult_self1_is_id log_half log_zero numeral_1_eq_Suc_0 numeral_One odd_1_nat odd_nat_plus_one_div_two one_less_numeral_iff power_one_right semiring_norm(76))
-apply(simp only: One_nat_def)
-apply(subst dvd_mult_div_cancel)
-apply (smt Suc_1 div_by_0 div_mult_self2_is_id oddfactor_odd dvd_power even_Suc even_numeral_nat even_product_nat nat_even_iff_2_dvd power_0 ww)
-apply(simp (no_asm))
-done
-
-lemma m1: "n div oddfactor n * oddfactor n = n"
-apply(induct n rule: nat_less_induct)
-apply(case_tac "n=0")
-apply(simp)
-apply(case_tac "odd n")
-apply(simp)
-apply(simp)
-apply(drule_tac x="n div 2" in spec)
-apply(drule mp)
-apply(auto)[1]
-by (metis add_eq_if diff_add_inverse oddfactor(3) mod_eq_0_iff mult_div_cancel nat_mult_commute ww)
-
-
-lemma m2: "0 < n ==> 2 ^ Discrete.log (n div (oddfactor n)) * (oddfactor n) = n"
-apply(subst m)
-apply(simp)
-apply(subst m1)
-apply(simp)
-done
-
-lemma y1:
-  "pdecode2 (pencode m n) = n"
-apply(simp del: One_nat_def)
-apply(subst k)
-apply(auto)
-done
-
-lemma y2:
-  "pdecode1 (pencode m n) = m"
-apply(simp only: pdecode1.simps pencode.simps)
-apply(subst Suc_diff_1)
-apply(auto)[1]
-apply(subst Suc_diff_1)
-apply(auto)[1]
-apply(subst k)
-apply(auto)[1]
-by (metis Suc_eq_plus1 Suc_neq_Zero comm_semiring_1_class.normalizing_semiring_rules(7) div_mult_self1_is_id log_exp)
-
-lemma yy: 
-  "pencode (pdecode1 m) (pdecode2 m) = m"
-apply(induct m rule: nat_less_induct)
-apply(simp (no_asm))
-apply(case_tac "n = 0")
-apply(simp)
-apply(subst dvd_mult_div_cancel)
-using oddfactor_odd
-apply -
-apply(drule_tac x="Suc n" in meta_spec)
-apply(erule disjE)
-apply(auto)[1]
-apply (metis One_nat_def even_num_iff nat_even_iff_2_dvd odd_pos)
-using bigger
-apply -
-apply(rotate_tac 3)
-apply(drule_tac x="n" in meta_spec)
-apply(simp del: pencode.simps pdecode2.simps pdecode1.simps One_nat_def add: One_nat_def[symmetric])
-apply(subst m2)
-apply(simp)
-apply(simp)
-done
-
-fun penc where
- "penc (m, n) = pencode m n"
-
-fun pdec where
- "pdec m = (pdecode1 m, pdecode2 m)"
-
-lemma q1: "penc (pdec m) = m"
-apply(simp only: penc.simps pdec.simps)
-apply(rule yy)
-done
-
-lemma q2: "pdec (penc m) = m"
-apply(simp only: penc.simps pdec.simps)
-apply(case_tac m)
-apply(simp only: penc.simps pdec.simps)
-apply(subst y1)
-apply(subst y2)
-apply(simp)
-done
-
-lemma inj_penc: "inj_on penc A"
-apply(rule inj_on_inverseI)
-apply(rule q2)
-done
-
-lemma inj_pdec: "inj_on pdec A"
-apply(rule inj_on_inverseI)
-apply(rule q1)
-done
-
-lemma surj_penc: "surj penc"
-apply(rule surjI)
-apply(rule q1)
-done
-
-lemma surj_pdec: "surj pdec"
-apply(rule surjI)
-apply(rule q2)
-done
-
-lemma 
-  "bij pdec"
-by(simp add: bij_def surj_pdec inj_pdec)
-
-lemma 
-  "bij penc"
-by(simp add: bij_def surj_penc inj_penc)
-
-lemma "a \<le> penc (a, 0)"
-apply(induct a)
-apply(simp)
-apply(simp)
-by (smt nat_one_le_power)
-
-lemma "penc(a, 0) \<le> penc (a, b)"
-apply(simp)
-by (metis diff_le_mono le_add1 mult_2_right mult_le_mono1 nat_add_commute nat_mult_1 nat_mult_commute)
-
-lemma "b \<le> penc (a, b)"
-apply(simp)
-proof -
-  have f1: "(1\<Colon>nat) + 1 = 2"
-    by (metis mult_2 nat_mult_1_right)
-  have f2: "\<And>x\<^isub>1 x\<^isub>2. (x\<^isub>1\<Colon>nat) \<le> x\<^isub>1 * x\<^isub>2 \<or> \<not> 1 \<le> x\<^isub>2"
-    by (metis mult_le_mono2 nat_mult_1_right)
-  have "1 + (b + b) \<le> 1 + b \<longrightarrow> b \<le> (1 + (b + b)) * (1 + 1) ^ a - 1"
-    by (metis le_add1 le_trans nat_add_left_cancel_le)
-  hence "(1 + (b + b)) * (1 + 1) ^ a \<le> 1 + b \<longrightarrow> b \<le> (1 + (b + b)) * (1 + 1) ^ a - 1"
-    using f2 by (metis le_add1 le_trans one_le_power)
-  hence "b \<le> 2 ^ a * (b + b + 1) - 1"
-    using f1 by (metis le_diff_conv nat_add_commute nat_le_linear nat_mult_commute)
-  thus "b \<le> 2 ^ a * (2 * b + 1) - 1"
-    by (metis mult_2)
-qed
-
-
-end
\ No newline at end of file
diff -r 6e1c03614d36 -r 93db7414931d thys/Recursive.thy
--- a/thys/Recursive.thy	Fri Dec 21 12:31:36 2018 +0100
+++ b/thys/Recursive.thy	Fri Dec 21 15:30:24 2018 +0100
@@ -170,33 +170,26 @@
 
 declare addition_inv.simps[simp del]
 
+lemma update_zero_to_zero[simp]: "\<lbrakk>am ! n = (0::nat); n < length am\<rbrakk> \<Longrightarrow> am[n := 0] = am"
+apply(simp add: list_update_same_conv)
+  done
+
 lemma addition_inv_init: 
   "\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk> \<Longrightarrow>
                                    addition_inv (0, lm) m n p lm"
-apply(simp add: addition_inv.simps Let_def)
+apply(simp add: addition_inv.simps Let_def )
 apply(rule_tac x = "lm ! m" in exI, simp)
 done
 
-lemma abs_fetch_0[simp]: "abc_fetch 0 (addition m n p) = Some (Dec m 4)"
-by(simp add: abc_fetch.simps addition.simps)
-
-lemma abs_fetch_1[simp]: "abc_fetch (Suc 0) (addition m n p) = Some (Inc n)"
-by(simp add: abc_fetch.simps addition.simps)
-
-lemma abs_fetch_2[simp]: "abc_fetch 2 (addition m n p) = Some (Inc p)"
-by(simp add: abc_fetch.simps addition.simps)
-
-lemma abs_fetch_3[simp]: "abc_fetch 3 (addition m n p) = Some (Goto 0)"
-by(simp add: abc_fetch.simps addition.simps)
-
-lemma abs_fetch_4[simp]: "abc_fetch 4 (addition m n p) = Some (Dec p 7)"
-by(simp add: abc_fetch.simps addition.simps)
-
-lemma abs_fetch_5[simp]: "abc_fetch 5 (addition m n p) = Some (Inc m)"
-by(simp add: abc_fetch.simps addition.simps)
-
-lemma abs_fetch_6[simp]: "abc_fetch 6 (addition m n p) = Some (Goto 4)"
-by(simp add: abc_fetch.simps addition.simps)
+lemma abs_fetch[simp]:
+  "abc_fetch 0 (addition m n p) = Some (Dec m 4)"
+  "abc_fetch (Suc 0) (addition m n p) = Some (Inc n)"
+  "abc_fetch 2 (addition m n p) = Some (Inc p)"
+  "abc_fetch 3 (addition m n p) = Some (Goto 0)"
+  "abc_fetch 4 (addition m n p) = Some (Dec p 7)"
+  "abc_fetch 5 (addition m n p) = Some (Inc m)"
+  "abc_fetch 6 (addition m n p) = Some (Goto 4)"
+by(simp_all add: abc_fetch.simps addition.simps)
 
 lemma exists_small_list_elem1[simp]:
   "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x \<le> lm ! m; 0 < x\<rbrakk>
@@ -288,7 +281,7 @@
                      abc_step_l.simps addition_inv.simps 
                      abc_lm_v.simps abc_lm_s.simps nth_append
                 split: if_splits)
-apply(rule_tac [!] x = x in exI, simp_all add: list_update_overwrite Suc_diff_Suc)
+apply(rule_tac [!] x = x in exI, simp_all add: list_update_overwrite Suc_diff_Suc )
 by (metis list_update_overwrite list_update_swap nat_neq_iff)
 
 lemma  addition_correct': 
@@ -479,21 +472,12 @@
       rule_tac x = "initlm ! n" in exI, simp)
 done
 
-lemma abc_fetch_0[simp]: "abc_fetch 0 (mv_box m n) = Some (Dec m 3)"
-apply(simp add: mv_box.simps abc_fetch.simps)
-done
-
-lemma abc_fetch_1[simp]: "abc_fetch (Suc 0) (mv_box m n) =
-               Some (Inc n)"
-apply(simp add: mv_box.simps abc_fetch.simps)
-done
-
-lemma abc_fetch_2[simp]: "abc_fetch 2 (mv_box m n) = Some (Goto 0)"
-apply(simp add: mv_box.simps abc_fetch.simps)
-done
-
-lemma abc_fetch_3[simp]: "abc_fetch 3 (mv_box m n) = None"
-apply(simp add: mv_box.simps abc_fetch.simps)
+lemma abc_fetch[simp]:
+  "abc_fetch 0 (mv_box m n) = Some (Dec m 3)"
+  "abc_fetch (Suc 0) (mv_box m n) = Some (Inc n)"
+  "abc_fetch 2 (mv_box m n) = Some (Goto 0)"
+  "abc_fetch 3 (mv_box m n) = None"
+apply(simp_all add: mv_box.simps abc_fetch.simps)
 done
 
 lemma replicate_Suc_iff_anywhere: "x # x\<up>b @ ys = x\<up>(Suc b) @ ys"
@@ -2584,7 +2568,7 @@
 apply(arith)
 apply(case_tac "Suc k = length ap", simp)
 apply(rule_tac start_of_less, simp)
-apply(auto simp: tinc_b_def shift.simps start_of_suc_inc length_of.simps startof_not0)
+apply(auto simp: tinc_b_def shift.simps start_of_suc_inc length_of.simps )
 done
 
 lemma findnth_le[elim]: 
@@ -2607,7 +2591,7 @@
 apply(rule_tac start_of_less, simp)
 apply(subgoal_tac "b \<le> start_of (layout_of ap) k + 2*n + 1 \<and> 
      start_of (layout_of ap) k + 2*n + 1 \<le>  start_of (layout_of ap) (Suc k)", auto)
-apply(auto simp: tinc_b_def shift.simps length_of.simps startof_not0 start_of_suc_inc)
+apply(auto simp: tinc_b_def shift.simps length_of.simps  start_of_suc_inc)
 done
 
 lemma start_of_eq: "length ap < as \<Longrightarrow> start_of (layout_of ap) as = start_of (layout_of ap) (length ap)"
@@ -2646,7 +2630,7 @@
 prefer 2
 apply(subgoal_tac "start_of (layout_of ap) (Suc k) = start_of (layout_of ap) k + 2*n + 16
                  \<and> start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap)")
-apply(simp add: startof_not0, rule_tac conjI)
+apply(simp, rule_tac conjI)
 apply(simp add: start_of_suc_dec)
 apply(rule_tac start_of_all_le)
 apply(auto simp: tdec_b_def shift.simps)
@@ -2795,6 +2779,4 @@
     by simp
 qed
 
-unused_thms
-
 end
\ No newline at end of file
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 {*