
diff -r d5a0e25c4742 -r a9003e6d0463 thys/Recursive.thy
--- a/thys/Recursive.thy	Wed Jan 14 09:08:51 2015 +0000
+++ b/thys/Recursive.thy	Wed Dec 19 16:10:58 2018 +0100
@@ -165,9 +165,8 @@
                           ((nat \<times> nat list) \<times> nat \<times> nat)) set"
   where "addition_LE \<equiv> (inv_image lex_triple addition_measure)"
 
-lemma [simp]: "wf addition_LE"
-by(auto simp: wf_inv_image addition_LE_def lex_triple_def
-             lex_pair_def)
+lemma wf_additon_LE[simp]: "wf addition_LE"
+  by(auto simp: addition_LE_def lex_triple_def lex_pair_def)
 
 declare addition_inv.simps[simp del]
 
@@ -178,28 +177,28 @@
 apply(rule_tac x = "lm ! m" in exI, simp)
 done
 
-lemma [simp]: "abc_fetch 0 (addition m n p) = Some (Dec m 4)"
+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 [simp]: "abc_fetch (Suc 0) (addition m n p) = Some (Inc n)"
+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 [simp]: "abc_fetch 2 (addition m n p) = Some (Inc p)"
+lemma abs_fetch_2[simp]: "abc_fetch 2 (addition m n p) = Some (Inc p)"
 by(simp add: abc_fetch.simps addition.simps)
 
-lemma [simp]: "abc_fetch 3 (addition m n p) = Some (Goto 0)"
+lemma abs_fetch_3[simp]: "abc_fetch 3 (addition m n p) = Some (Goto 0)"
 by(simp add: abc_fetch.simps addition.simps)
 
-lemma [simp]: "abc_fetch 4 (addition m n p) = Some (Dec p 7)"
+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 [simp]: "abc_fetch 5 (addition m n p) = Some (Inc m)"
+lemma abs_fetch_5[simp]: "abc_fetch 5 (addition m n p) = Some (Inc m)"
 by(simp add: abc_fetch.simps addition.simps)
 
-lemma [simp]: "abc_fetch 6 (addition m n p) = Some (Goto 4)"
+lemma abs_fetch_6[simp]: "abc_fetch 6 (addition m n p) = Some (Goto 4)"
 by(simp add: abc_fetch.simps addition.simps)
 
-lemma [simp]:
+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>
  \<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m - x, 
                     p := lm ! m - x, m := x - Suc 0] =
@@ -210,7 +209,7 @@
                                          list_update_overwrite)
 done
 
-lemma [simp]:
+lemma exists_small_list_elem2[simp]:
   "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\<rbrakk>
    \<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m - Suc x,
                       p := lm ! m - Suc x, n := lm ! n + lm ! m - x]
@@ -220,7 +219,7 @@
       simp add: list_update_swap list_update_overwrite)
 done
 
-lemma [simp]: 
+lemma exists_small_list_elem3[simp]: 
   "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\<rbrakk>
    \<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m - x, 
                           p := lm ! m - Suc x, p := lm ! m - x]
@@ -229,7 +228,7 @@
 apply(rule_tac x = x in exI, simp add: list_update_overwrite)
 done
 
-lemma [simp]: 
+lemma exists_small_list_elem4[simp]: 
   "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = (0::nat); m < p; n < p; x < lm ! m\<rbrakk>
   \<Longrightarrow> \<exists>xa\<le>lm ! m. lm[m := x, n := lm ! n + lm ! m - x,
                                    p := lm ! m - x] = 
@@ -238,7 +237,7 @@
 apply(rule_tac x = x in exI, simp)
 done
 
-lemma [simp]: 
+lemma exists_small_list_elem5[simp]: 
   "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p;
     x \<le> lm ! m; lm ! m \<noteq> x\<rbrakk>
   \<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m, 
@@ -248,7 +247,7 @@
 apply(rule_tac x = x in exI, simp add: list_update_overwrite)
 done
 
-lemma [simp]:
+lemma exists_small_list_elem6[simp]:
   "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\<rbrakk>
   \<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m,
                              p := lm ! m - Suc x, m := Suc x]
@@ -258,7 +257,7 @@
      simp add: list_update_swap list_update_overwrite)
 done
 
-lemma [simp]: 
+lemma exists_small_list_elem7[simp]: 
   "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\<rbrakk>
   \<Longrightarrow> \<exists>xa\<le>lm ! m. lm[m := Suc x, n := lm ! n + lm ! m, 
                              p := lm ! m - Suc x] 
@@ -311,8 +310,8 @@
 by(auto simp: addition.simps)
 
 lemma addition_correct:
-  "\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk>
-   \<Longrightarrow> {\<lambda> a. a = lm} (addition m n p) {\<lambda> nl. addition_inv (7, nl) m n p lm}"
+  assumes "m \<noteq> n" "max m n < p" "length lm > p" "lm ! p = 0"
+  shows "{\<lambda> a. a = lm} (addition m n p) {\<lambda> nl. addition_inv (7, nl) m n p lm}"
 using assms
 proof(rule_tac abc_Hoare_haltI, simp)
   fix lma
@@ -480,27 +479,27 @@
       rule_tac x = "initlm ! n" in exI, simp)
 done
 
-lemma [simp]: "abc_fetch 0 (mv_box m n) = Some (Dec m 3)"
+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 [simp]: "abc_fetch (Suc 0) (mv_box m n) =
+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 [simp]: "abc_fetch 2 (mv_box m n) = Some (Goto 0)"
+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 [simp]: "abc_fetch 3 (mv_box m n) = None"
+lemma abc_fetch_3[simp]: "abc_fetch 3 (mv_box m n) = None"
 apply(simp add: mv_box.simps abc_fetch.simps)
 done
 
 lemma replicate_Suc_iff_anywhere: "x # x\<up>b @ ys = x\<up>(Suc b) @ ys"
 by simp
 
-lemma [simp]: 
+lemma exists_smaller_in_list0[simp]: 
   "\<lbrakk>m \<noteq> n; m < length initlm; n < length initlm;
     k + l = initlm ! m + initlm ! n; k \<le> initlm ! m; 0 < k\<rbrakk>
  \<Longrightarrow> \<exists>ka la. initlm[m := k, n := l, m := k - Suc 0] = 
@@ -517,7 +516,7 @@
 apply(simp add: list_update_swap)
 done
 
-lemma [simp]:
+lemma exists_smaller_in_list1[simp]:
   "\<lbrakk>m \<noteq> n; m < length initlm; n < length initlm; 
     Suc (k + l) = initlm ! m + initlm ! n;
     k < initlm ! m\<rbrakk>
@@ -528,7 +527,7 @@
 apply(rule_tac x = k in exI, rule_tac x = "Suc l" in exI, auto)
 done
 
-lemma [simp]: 
+lemma abc_steps_prop[simp]: 
   "\<lbrakk>length initlm > max m n; m \<noteq> n\<rbrakk> \<Longrightarrow> 
    \<forall>na. \<not> (\<lambda>(as, lm) m. as = 3) 
     (abc_steps_l (0, initlm) (mv_box m n) na) m \<and> 
@@ -598,7 +597,7 @@
 
 declare list_update.simps(2)[simp del]
 
-lemma [simp]:
+lemma zero_case_rec_exec[simp]:
   "\<lbrakk>length xs < gf; gf \<le> ft; n < length gs\<rbrakk>
   \<Longrightarrow> (rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)
   [ft + n - length xs := rec_exec (gs ! n) xs, 0 := 0] =
@@ -676,8 +675,9 @@
         hence c: "length xs = ga"
           using a param_pattern by metis  
         have d: "gf > ga" using footprint_ge a by simp
-        have e: "ft \<ge> gf" using ft a h
-          by(simp,  rule_tac min_max.le_supI2, rule_tac Max_ge, simp, 
+        have e: "ft \<ge> gf"
+          using ft a h Max_ge image_eqI
+          by(simp, rule_tac max.coboundedI2, rule_tac Max_ge, simp, 
             rule_tac insertI2,  
             rule_tac f = "(\<lambda>(aprog, p, n). n)" and x = "rec_ci (gs!n)" in image_eqI, simp, 
             rule_tac x = "gs!n" in image_eqI, simp, simp)
@@ -780,7 +780,7 @@
 lemma exp_suc: "a\<up>Suc b = a\<up>b @ [a]"
 by(simp add: exp_ind del: replicate.simps)
 
-lemma [simp]: 
+lemma last_0[simp]: 
   "\<lbrakk>Suc n \<le> ba - aa;  length lm2 = Suc n;
     length lm3 = ba - Suc (aa + n)\<rbrakk>
   \<Longrightarrow> (last lm2 # lm3 @ butlast lm2 @ 0 # lm4) ! (ba - aa) = (0::nat)"
@@ -796,25 +796,25 @@
     done
 qed
 
-lemma [simp]: "length lm1 = aa \<Longrightarrow>
+lemma butlast_last[simp]: "length lm1 = aa \<Longrightarrow>
       (lm1 @ 0\<up>n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4) ! (aa + n) = last lm2"
 apply(simp add: nth_append)
 done
 
-lemma [simp]: "\<lbrakk>Suc n \<le> ba - aa; aa < ba\<rbrakk> \<Longrightarrow> 
+lemma arith_as_simp[simp]: "\<lbrakk>Suc n \<le> ba - aa; aa < ba\<rbrakk> \<Longrightarrow> 
                     (ba < Suc (aa + (ba - Suc (aa + n) + n))) = False"
 apply arith
 done
 
-lemma [simp]: "\<lbrakk>Suc n \<le> ba - aa; aa < ba; length lm1 = aa; 
+lemma butlast_elem[simp]: "\<lbrakk>Suc n \<le> ba - aa; aa < ba; length lm1 = aa; 
        length lm2 = Suc n; length lm3 = ba - Suc (aa + n)\<rbrakk>
      \<Longrightarrow> (lm1 @ 0\<up>n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4) ! (ba + n) = 0"
-using nth_append[of "lm1 @ (0\<Colon>'a)\<up>n @ last lm2 # lm3 @ butlast lm2" 
-                     "(0\<Colon>'a) # lm4" "ba + n"]
+using nth_append[of "lm1 @ (0::'a)\<up>n @ last lm2 # lm3 @ butlast lm2" 
+                     "(0::'a) # lm4" "ba + n"]
 apply(simp)
 done
 
-lemma [simp]: 
+lemma update_butlast_eq0[simp]: 
  "\<lbrakk>Suc n \<le> ba - aa; aa < ba; length lm1 = aa; length lm2 = Suc n;
                  length lm3 = ba - Suc (aa + n)\<rbrakk>
   \<Longrightarrow> (lm1 @ 0\<up>n @ last lm2 # lm3 @ butlast lm2 @ (0::nat) # lm4)
@@ -822,18 +822,17 @@
   lm1 @ 0 # 0\<up>n @ lm3 @ lm2 @ lm4"
 using list_update_append[of "lm1 @ 0\<up>n @ last lm2 # lm3 @ butlast lm2" "0 # lm4" 
                             "ba + n" "last lm2"]
-apply(simp)
-apply(simp add: list_update_append list_update.simps replicate_Suc_iff_anywhere exp_suc
-  del: replicate_Suc)
+apply(simp add: list_update_append list_update.simps(2-) replicate_Suc_iff_anywhere exp_suc
+           del: replicate_Suc)
 apply(case_tac lm2, simp, simp)
 done
 
-lemma [simp]:
+lemma update_butlast_eq1[simp]:
   "\<lbrakk>Suc (length lm1 + n) \<le> ba; length lm2 = Suc n; length lm3 = ba - Suc (length lm1 + n); 
   \<not> ba - Suc (length lm1) < ba - Suc (length lm1 + n); \<not> ba + n - length lm1 < n\<rbrakk>
     \<Longrightarrow> (0::nat) \<up> n @ (last lm2 # lm3 @ butlast lm2 @ 0 # lm4)[ba - length lm1 := last lm2, 0 := 0] =
   0 # 0 \<up> n @ lm3 @ lm2 @ lm4"
-apply(subgoal_tac "ba - length lm1 = Suc n + length lm3", simp add: list_update.simps list_update_append)
+apply(subgoal_tac "ba - length lm1 = Suc n + length lm3", simp add: list_update.simps(2-) list_update_append)
 apply(simp add: replicate_Suc_iff_anywhere exp_suc del: replicate_Suc)
 apply(case_tac lm2, simp, simp)
 apply(auto)
@@ -892,7 +891,7 @@
    by(simp add: mv_boxes.simps)
 qed
     
-lemma [simp]:
+lemma update_butlast_eq2[simp]:
   "\<lbrakk>Suc n \<le> aa - length lm1; length lm1 < aa; 
   length lm2 = aa - Suc (length lm1 + n); 
   length lm3 = Suc n; 
@@ -980,9 +979,9 @@
     by(simp add: replicate_merge_anywhere)
 qed
 
-lemma [intro]: 
-  "length gs \<le> ffp \<Longrightarrow> length gs \<le> max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
- apply(rule_tac min_max.le_supI2)
+lemma length_le_max_insert_rec_ci[intro]: 
+  "length gs \<le> ffp \<Longrightarrow> length gs \<le> max x1 (Max (insert ffp (x2 ` x3 ` set gs)))"
+ apply(rule_tac max.coboundedI2)
  apply(simp add: Max_ge_iff)
 done
 
@@ -1006,10 +1005,8 @@
     by(simp add: replicate_merge_anywhere le_add_diff_inverse)
 qed
    
-lemma [intro]: "ffp \<le> max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
-apply(rule_tac min_max.le_supI2)
-apply(rule_tac Max_ge, auto)
-done
+lemma le_max_insert[intro]: "ffp \<le> max x0 (Max (insert ffp (x1 ` x2 ` set gs)))"
+  by (rule max.coboundedI2) auto
 
 declare max_less_iff_conj[simp del]
 
@@ -1046,7 +1043,7 @@
     by(simp)
 qed
 
-lemma [simp]: "length (empty_boxes n) = 2*n"
+lemma length_empty_boxes[simp]: "length (empty_boxes n) = 2*n"
 apply(induct n, simp, simp)
 done
 
@@ -1101,17 +1098,17 @@
     show "{\<lambda>nl. nl = 0 \<up> n @ drop n lm} [Dec n 2, Goto 0] {\<lambda>nl. nl = 0 # 0 \<up> n @ drop (Suc n) lm}"
       using empty_one_box_correct[of n "lm ! n" "drop (Suc n) lm"]
       using h
-      by(simp add: nth_drop')
+      by(simp add: Cons_nth_drop_Suc)
   qed
   thus "?case"
     by(simp add: empty_boxes.simps)
 qed
 
-lemma [simp]: "length gs \<le> ffp \<Longrightarrow>
-    length gs + (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) - length gs) =
-    max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
+lemma insert_dominated[simp]: "length gs \<le> ffp \<Longrightarrow>
+    length gs + (max xs (Max (insert ffp (x1 ` x2 ` set gs))) - length gs) =
+    max xs (Max (insert ffp (x1 ` x2 ` set gs)))"
 apply(rule_tac le_add_diff_inverse)
-apply(rule_tac min_max.le_supI2)
+apply(rule_tac max.coboundedI2)
 apply(simp add: Max_ge_iff)
 done
 
@@ -1317,14 +1314,14 @@
     done
 qed
 
-lemma [simp]: 
+lemma mv_box_correct_simp[simp]: 
   "\<lbrakk>length xs = n; ft = max (n+3) (max fft gft)\<rbrakk> 
  \<Longrightarrow> {\<lambda>nl. nl = xs @ 0 # 0 \<up> (ft - n) @ anything} mv_box n ft 
        {\<lambda>nl. nl = xs @ 0 # 0 \<up> (ft - n) @ anything}"
 using mv_box_correct[of n ft "xs @ 0 # 0 \<up> (ft - n) @ anything"]
 by(auto)
 
-lemma [simp]: "length xs < max (length xs + 3) (max fft gft)"
+lemma length_under_max[simp]: "length xs < max (length xs + 3) fft"
 by auto
 
 lemma save_init_rs: 
@@ -1336,13 +1333,13 @@
 apply(case_tac "(max (length xs + 3) (max fft gft))", simp_all add: list_update.simps Suc_diff_le)
 done
 
-lemma [simp]: "n + (2::nat) < max (n + 3) (max fft gft)"
+lemma less_then_max_plus2[simp]: "n + (2::nat) < max (n + 3) x"
 by auto
 
-lemma [simp]: "n < max (n + (3::nat)) (max fft gft)"
+lemma less_then_max_plus3[simp]: "n < max (n + (3::nat)) x"
 by auto
 
-lemma [simp]:
+lemma mv_box_max_plus_3_correct[simp]:
   "length xs = n \<Longrightarrow> 
   {\<lambda>nl. nl = xs @ x # 0 \<up> (max (n + (3::nat)) (max fft gft) - n) @ anything} mv_box n (max (n + 3) (max fft gft))
   {\<lambda>nl. nl = xs @ 0 \<up> (max (n + 3) (max fft gft) - n) @ x # anything}"
@@ -1373,13 +1370,13 @@
     by simp
 qed
 
-lemma [simp]: "max n (Suc n) < Suc (Suc (max (n + 3) (max fft gft) + length anything - Suc 0))"
+lemma max_less_suc_suc[simp]: "max n (Suc n) < Suc (Suc (max (n + 3) x + anything - Suc 0))"
 by arith    
 
-lemma [simp]: "Suc n < max (n + 3) (max fft gft)"
+lemma suc_less_plus_3[simp]: "Suc n < max (n + 3) x"
 by arith
 
-lemma [simp]:
+lemma mv_box_ok_suc_simp[simp]:
   "length xs = n
  \<Longrightarrow> {\<lambda>nl. nl = xs @ rec_exec f xs # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ x # anything} mv_box n (Suc n)
     {\<lambda>nl. nl = xs @ 0 # rec_exec f xs # 0 \<up> (max (n + 3) (max fft gft) - Suc (Suc n)) @ x # anything}"
@@ -1462,11 +1459,11 @@
 apply(rule_tac abc_append_frist_steps_halt_eq', simp_all)
 done
 
-lemma [simp]: "Suc (Suc (max (length xs + 3) (max fft gft) - Suc (Suc (length xs))))
-           = max (length xs + 3) (max fft gft) - (length xs)"
+lemma suc_suc_max_simp[simp]: "Suc (Suc (max (xs + 3) fft - Suc (Suc ( xs))))
+           = max ( xs + 3) fft - ( xs)"
 by arith
 
-lemma [simp]: "\<lbrakk>ft = max (n + 3) (max fft gft); length xs = n\<rbrakk> \<Longrightarrow>
+lemma contract_dec_ft_length_plus_7[simp]: "\<lbrakk>ft = max (n + 3) (max fft gft); length xs = n\<rbrakk> \<Longrightarrow>
      {\<lambda>nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything}
      [Dec ft (length gap + 7)] 
      {\<lambda>nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything}"
@@ -1506,9 +1503,8 @@
     then obtain stp where 
       "abc_steps_l (0, xs @ Suc x # y # anything) [Dec (Suc n) 2, Goto 0] stp = (2, xs @ Suc x # 0 # anything)"
       using h
-      apply(auto simp: abc_Hoare_halt_def)
-      by(case_tac "abc_steps_l (0, xs @ Suc x # y # anything) [Dec (Suc (length xs)) 2, Goto 0] n",   
-            simp_all add: numeral_2_eq_2)   
+      apply(auto simp: abc_Hoare_halt_def numeral_2_eq_2)
+      by (metis (mono_tags, lifting) abc_final.simps abc_holds_for.elims(2) length_Cons list.size(3))
     moreover have "abc_steps_l (0, xs @ Suc x # Suc y # anything) [Dec (Suc n) 2, Goto 0] 2 = 
                  (0, xs @ Suc x # y # anything)"
       using h
@@ -1526,7 +1522,7 @@
 using adjust_paras'[of xs n x y anything]
 by(simp add: abc_comp.simps abc_shift.simps numeral_2_eq_2 numeral_3_eq_3)
 
-lemma [simp]: "\<lbrakk>rec_ci g = (gap, gar, gft); \<forall>y<x. terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]);
+lemma rec_ci_SucSuc_n[simp]: "\<lbrakk>rec_ci g = (gap, gar, gft); \<forall>y<x. terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]);
         length xs = n; Suc y\<le>x\<rbrakk> \<Longrightarrow> gar = Suc (Suc n)"
   apply(erule_tac x = y in allE, simp)
   apply(drule_tac param_pattern, auto)
@@ -1583,7 +1579,7 @@
 apply(simp add: rec_exec.simps)
 done
 
-lemma [simp]: "Suc (max (n + 3) (max fft gft) - Suc (Suc (Suc n))) = max (n + 3) (max fft gft) - Suc (Suc n)"
+lemma suc_max_simp[simp]: "Suc (max (n + 3) fft - Suc (Suc (Suc n))) = max (n + 3) fft - Suc (Suc n)"
 by arith
 
 lemma pr_loop:
@@ -1691,7 +1687,7 @@
     by(auto, rule_tac x = "stp + stpa" in exI, simp add: abc_steps_add replicate_Suc_iff_anywhere del: replicate_Suc)
 qed
 
-lemma [simp]: 
+lemma abc_lm_s_simp0[simp]: 
   "length xs = n \<Longrightarrow> abc_lm_s (xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) 
   (max fft gft) - Suc (Suc n)) @ 0 # anything) (max (n + 3) (max fft gft)) 0 =
     xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ anything"
@@ -1702,11 +1698,11 @@
 apply(simp add: exp_suc[THEN sym] Suc_diff_Suc  del: replicate_Suc)
 done
 
-lemma [simp]:
-  "(xs @ x # rec_exec (Pr (length xs) f g) (xs @ [x]) # 0 \<up> (max (length xs + 3)
+lemma index_at_zero_elem[simp]:
+  "(xs @ x # re # 0 \<up> (max (length xs + 3)
   (max fft gft) - Suc (Suc (length xs))) @ 0 # anything) !
     max (length xs + 3) (max fft gft) = 0"
-using nth_append_length[of "xs @ x # rec_exec (Pr (length xs) f g) (xs @ [x]) #
+using nth_append_length[of "xs @ x # re #
   0 \<up> (max (length xs + 3) (max fft gft) - Suc (Suc (length xs)))" 0  anything]
 by(simp)
 
@@ -1920,14 +1916,14 @@
 
 declare mn_ind_inv.simps[simp del]
 
-lemma [simp]: 
+lemma put_in_tape_small_enough0[simp]: 
   "0 < rsx \<Longrightarrow> 
  \<exists>y. (xs @ x # rsx # anything)[Suc (length xs) := rsx - Suc 0] = xs @ x # y # anything \<and> y \<le> rsx"
 apply(rule_tac x = "rsx - 1" in exI)
 apply(simp add: list_update_append list_update.simps)
 done
 
-lemma [simp]: 
+lemma put_in_tape_small_enough1[simp]: 
   "\<lbrakk>y \<le> rsx; 0 < y\<rbrakk>
             \<Longrightarrow> \<exists>ya. (xs @ x # y # anything)[Suc (length xs) := y - Suc 0] = xs @ x # ya # anything \<and> ya \<le> rsx"
 apply(rule_tac x = "y - 1" in exI)
@@ -1939,9 +1935,9 @@
 
 lemma rec_ci_not_null[simp]: "(rec_ci f \<noteq> ([], a, b))"
 apply(case_tac f, auto simp: rec_ci_z_def rec_ci_s_def rec_ci.simps addition.simps rec_ci_id.simps)
-apply(case_tac "rec_ci recf", auto simp: mv_box.simps)
-apply(case_tac "rec_ci recf1", case_tac "rec_ci recf2", simp)
-apply(case_tac "rec_ci recf", simp)
+apply(case_tac "rec_ci x42", auto simp: mv_box.simps)
+apply(case_tac "rec_ci x52", case_tac "rec_ci x53", simp)
+apply(case_tac "rec_ci x62", simp)
 done
 
 lemma mn_correct:
@@ -2231,12 +2227,12 @@
   "\<lbrakk>abc_list_crsp lma lmb; \<exists> n. lma = lmb @ 0\<up>n \<or> lmb = lma @ 0\<up>n \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
 by(auto simp: abc_list_crsp_def)
 
-lemma [simp]: 
+lemma abc_list_crsp_simp[simp]: 
   "\<lbrakk>abc_list_crsp lma lmb; m < length lma; m < length lmb\<rbrakk> \<Longrightarrow>
           abc_list_crsp (lma[m := n]) (lmb[m := n])"
 by(auto simp: abc_list_crsp_def list_update_append)
 
-lemma [simp]: 
+lemma abc_list_crsp_simp2[simp]: 
   "\<lbrakk>abc_list_crsp lma lmb; m < length lma; \<not> m < length lmb\<rbrakk> \<Longrightarrow> 
   abc_list_crsp (lma[m := n]) (lmb @ 0 \<up> (m - length lmb) @ [n])"
 apply(auto simp: abc_list_crsp_def list_update_append)
@@ -2245,7 +2241,7 @@
 apply(simp add: upd_conv_take_nth_drop min_absorb1)
 done
 
-lemma [simp]:
+lemma abc_list_crsp_simp3[simp]:
   "\<lbrakk>abc_list_crsp lma lmb; \<not> m < length lma; m < length lmb\<rbrakk> \<Longrightarrow> 
   abc_list_crsp (lma @ 0 \<up> (m - length lma) @ [n]) (lmb[m := n])"
 apply(auto simp: abc_list_crsp_def list_update_append)
@@ -2254,7 +2250,7 @@
 apply(simp add: upd_conv_take_nth_drop min_absorb1)
 done
 
-lemma [simp]: "\<lbrakk>abc_list_crsp lma lmb; \<not> m < length lma; \<not> m < length lmb\<rbrakk> \<Longrightarrow> 
+lemma abc_list_crsp_simp4[simp]: "\<lbrakk>abc_list_crsp lma lmb; \<not> m < length lma; \<not> m < length lmb\<rbrakk> \<Longrightarrow> 
   abc_list_crsp (lma @ 0 \<up> (m - length lma) @ [n]) (lmb @ 0 \<up> (m - length lmb) @ [n])"
   by(auto simp: abc_list_crsp_def list_update_append replicate_merge_anywhere)
 
@@ -2285,13 +2281,9 @@
     "\<And>a lm'. aa = a \<and> b = lm' \<Longrightarrow> 
      \<exists>lma. abc_steps_l (0, lm) aprog stp = (a, lma) \<and>
                                           abc_list_crsp lm' lma"
-    and h: "abc_steps_l (0, lm @ 0\<up>m) aprog (Suc stp) = (a, lm')" 
+    and h: "abc_step_l (aa, b) (abc_fetch aa aprog) = (a, lm')" 
            "abc_steps_l (0, lm @ 0\<up>m) aprog stp = (aa, b)" 
            "aprog \<noteq> []"
-  hence g1: "abc_steps_l (0, lm @ 0\<up>m) aprog (Suc stp)
-          = abc_step_l (aa, b) (abc_fetch aa aprog)"
-    apply(rule_tac abc_step_red, simp)
-    done
   have "\<exists>lma. abc_steps_l (0, lm) aprog stp = (aa, lma) \<and> 
               abc_list_crsp b lma"
     apply(rule_tac ind, simp)
@@ -2304,7 +2296,7 @@
     apply(rule_tac abc_step_red, simp)
     done
   show "\<exists>lma. abc_steps_l (0, lm) aprog (Suc stp) = (a, lma) \<and> abc_list_crsp lm' lma"
-    using g1 g2 g3 h
+    using g2 g3 h
     apply(auto)
     apply(case_tac "abc_step_l (aa, b) (abc_fetch aa aprog)",
           case_tac "abc_step_l (aa, lma) (abc_fetch aa aprog)", simp)
@@ -2343,7 +2335,7 @@
 apply(rule_tac list_crsp_simp2, auto)
 done
 
-lemma [simp]:
+lemma find_exponent_rec_exec[simp]:
   assumes a: "args @ [rec_exec f args] = lm @ 0 \<up> n"
   and b: "length args < length lm"
   shows "\<exists>m. lm = args @ rec_exec f args # 0 \<up> m"
@@ -2353,7 +2345,7 @@
 apply(drule_tac length_equal, simp)
 done
 
-lemma [simp]: 
+lemma find_exponent_complex[simp]: 
 "\<lbrakk>args @ [rec_exec f args] = lm @ 0 \<up> n; \<not> length args < length lm\<rbrakk>
   \<Longrightarrow> \<exists>m. (lm @ 0 \<up> (length args - length lm) @ [Suc 0])[length args := 0] =
   args @ rec_exec f args # 0 \<up> m"
@@ -2421,7 +2413,7 @@
       by simp
     moreover have "?ft \<ge> gft"
       using g compile2
-      apply(rule_tac min_max.le_supI2, rule_tac Max_ge, simp, rule_tac insertI2)
+      apply(rule_tac max.coboundedI2, rule_tac Max_ge, simp, rule_tac insertI2)
       apply(rule_tac  x = "rec_ci (gs ! i)" in image_eqI, simp)
       by(rule_tac x = "gs!i"  in image_eqI, simp, simp)
     then have b:"?Q_tmp = ?Q"
@@ -2526,12 +2518,12 @@
   fix ap ar fp
   assume "rec_ci recf = (ap, ar, fp)"
   thus "\<exists>stp m l. steps0 (Suc 0, [Bk, Bk], <args>) 
-    (tm_of (ap [+] dummy_abc ar) @ shift (mopup ar) (listsum (layout_of (ap [+] dummy_abc ar)))) stp =
+    (tm_of (ap [+] dummy_abc ar) @ shift (mopup ar) (sum_list (layout_of (ap [+] dummy_abc ar)))) stp =
     (0, Bk # Bk # Bk \<up> m, Oc # Oc \<up> rec_exec recf args @ Bk \<up> l)"
     using recursive_compile_to_tm_correct1[of recf ap ar fp args "tm_of (ap [+] dummy_abc (length args))" "[]" 0]
       assms param_pattern[of recf args ap ar fp]
-    by(simp add: replicate_Suc[THEN sym] replicate_Suc_iff_anywhere del: replicate_Suc tm_of_rec_def, 
-      simp add: exp_suc del: replicate_Suc)
+    by(simp add: replicate_Suc[THEN sym] replicate_Suc_iff_anywhere del: replicate_Suc, 
+       simp add: exp_suc del: replicate_Suc)
 qed
 
 lemma recursive_compile_to_tm_correct3: 
@@ -2541,12 +2533,12 @@
 using recursive_compile_to_tm_correct2[OF assms]
 apply(auto simp add: Hoare_halt_def)
 apply(rule_tac x = stp in exI)
-apply(auto simp add: tape_of_nat_abv)
+apply(auto simp add: tape_of_nat_def)
 apply(rule_tac x = "Suc (Suc m)" in exI)
 apply(simp)
 done 
 
-lemma [simp]:
+lemma list_all_suc_many[simp]:
   "list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))) xs \<Longrightarrow>
   list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))))) xs"
 apply(induct xs, simp, simp)
@@ -2557,7 +2549,7 @@
 apply(simp add: shift.simps)
 done
 
-lemma [simp]: "length (shift (mopup n) ss) = 4 * n + 12"
+lemma length_shift_mopup[simp]: "length (shift (mopup n) ss) = 4 * n + 12"
 apply(auto simp: mopup.simps shift_append mopup_b_def)
 done
 
@@ -2565,7 +2557,7 @@
 apply(simp add: tm_of.simps)
 done
 
-lemma [simp]: "k < length ap \<Longrightarrow> tms_of ap ! k  = 
+lemma tms_of_at_index[simp]: "k < length ap \<Longrightarrow> tms_of ap ! k  = 
  ci (layout_of ap) (start_of (layout_of ap) k) (ap ! k)"
 apply(simp add: tms_of.simps tpairs_of.simps)
 done
@@ -2668,7 +2660,6 @@
 apply(erule_tac inc_state_all_le, simp_all)
 apply(erule_tac findnth_state_all_le2, simp_all)
 apply(rule_tac start_of_all_le)
-apply(rule_tac dec_state_all_le, simp_all)
 apply(rule_tac start_of_all_le)
 done
 
@@ -2682,7 +2673,7 @@
 apply(simp add: nth_append)
 done 
 
-lemma [simp]: "length (tms_of ap) = length ap"
+lemma length_tms_of[simp]: "length (tms_of ap) = length ap"
 apply(simp add: tms_of.simps tpairs_of.simps)
 done
 
@@ -2709,12 +2700,12 @@
   length_of.simps tinc_b_def tdec_b_def length_findnth adjust.simps)
 done
 
-lemma [intro]: "length (ci ly y i) mod 2 = 0"
+lemma ci_even[intro]: "length (ci ly y i) mod 2 = 0"
 apply(case_tac i, auto simp: ci.simps length_findnth
   tinc_b_def adjust.simps tdec_b_def)
 done
 
-lemma [intro]: "listsum (map (length \<circ> (\<lambda>(x, y). ci ly x y)) zs) mod 2 = 0"
+lemma sum_list_ci_even[intro]: "sum_list (map (length \<circ> (\<lambda>(x, y). ci ly x y)) zs) mod 2 = 0"
 apply(induct zs rule: rev_induct, simp)
 apply(case_tac x, simp)
 apply(subgoal_tac "length (ci ly a b) mod 2 = 0")
@@ -2740,13 +2731,11 @@
 apply(simp add: tm_of.simps)
 done
 
-lemma [elim]: "list_all (\<lambda>(acn, s). s \<le> Suc q) xs
+lemma list_all_add_6E[elim]: "list_all (\<lambda>(acn, s). s \<le> Suc q) xs
         \<Longrightarrow> list_all (\<lambda>(acn, s). s \<le> q + (2 * n + 6)) xs"
-apply(simp add: list_all_length)
-apply(auto)
-done
+by(auto simp: list_all_length)
 
-lemma [simp]: "length mopup_b = 12"
+lemma mopup_b_12[simp]: "length mopup_b = 12"
 apply(simp add: mopup_b_def)
 done
 
@@ -2756,43 +2745,43 @@
   (W0, Suc (Suc (Suc (2 * n + q)))), (R, Suc (Suc (2 * n + q))),
   (W0, Suc (Suc (Suc (2 * n + q)))), (L, 5 + 2 * n + q),
   (L, 6 + 2 * n + q), (R, 0),  (L, 6 + 2 * n + q)]"
-apply(auto)
-done
+by(auto)
 
-lemma [simp]: "(a, b) \<in> set (mopup_a n) \<Longrightarrow> b \<le> 2 * n + 6"
+lemma mopup_le6[simp]: "(a, b) \<in> set (mopup_a n) \<Longrightarrow> b \<le> 2 * n + 6"
 apply(induct n, auto simp: mopup_a.simps)
 done
 
-lemma [simp]: "(a, b) \<in> set (shift (mopup n) (listsum (layout_of ap)))
-  \<Longrightarrow> b \<le> (2 * listsum (layout_of ap) + length (mopup n)) div 2"
+lemma shift_le2[simp]: "(a, b) \<in> set (shift (mopup n) x)
+  \<Longrightarrow> b \<le> (2 * x + length (mopup n)) div 2"
 apply(auto simp: mopup.simps shift_append shift.simps)
-apply(auto simp: mopup_a.simps mopup_b_def)
+apply(auto simp: mopup_b_def)
 done
 
-lemma [intro]: " 2 \<le> 2 * listsum (layout_of ap) + length (mopup n)"
+lemma mopup_ge2[intro]: " 2 \<le> x + length (mopup n)"
 apply(simp add: mopup.simps)
 done
 
-lemma [intro]: " (2 * listsum (layout_of ap) + length (mopup n)) mod 2 = 0"
-apply(auto simp: mopup.simps)
-apply arith
-done
+lemma mopup_even[intro]: " (2 * x + length (mopup n)) mod 2 = 0"
+by(auto simp: mopup.simps)
 
-lemma [simp]: "b \<le> Suc x
+lemma mopup_div_2[simp]: "b \<le> Suc x
           \<Longrightarrow> b \<le> (2 * x + length (mopup n)) div 2"
-apply(auto simp: mopup.simps)
-done
+by(auto simp: mopup.simps)
 
-lemma wf_tm_from_abacus: 
-  "tp = tm_of ap \<Longrightarrow> 
-    tm_wf (tp @ shift( mopup n) (length tp div 2), 0)"
- using length_start_of_tm[of ap] all_le_start_of[of ap]
-apply(auto simp: tm_wf.simps List.list_all_iff)
-apply(case_tac n)
-apply(simp add: mopup.simps)
-apply(simp add: mopup.simps)
-apply (metis mod_mult_right_eq mod_mult_self2 mod_mult_self2_is_0 mult_2_right nat_mult_commute numeral_Bit0)
-sorry
+lemma wf_tm_from_abacus: assumes "tp = tm_of ap"
+  shows "tm_wf0 (tp @ shift (mopup n) (length tp div 2))"
+proof -
+  have "is_even (length (mopup n))" for n using tm_wf.simps by blast
+  moreover have "(aa, ba) \<in> set (mopup n) \<Longrightarrow> ba \<le> length (mopup n) div 2" for aa ba
+    by (metis (no_types, lifting) add_cancel_left_right case_prodD tm_wf.simps wf_mopup)
+  moreover have "(\<forall>x\<in>set (tm_of ap). case x of (acn, s) \<Rightarrow> s \<le> Suc (sum_list (layout_of ap))) \<Longrightarrow>
+           (a, b) \<in> set (tm_of ap) \<Longrightarrow> b \<le> sum_list (layout_of ap) + length (mopup n) div 2"
+    for a b s
+    by (metis (no_types, lifting) add_Suc add_cancel_left_right case_prodD div_mult_mod_eq le_SucE mult_2_right not_numeral_le_zero tm_wf.simps trans_le_add1 wf_mopup)
+  ultimately show ?thesis unfolding assms
+    using length_start_of_tm[of ap] all_le_start_of[of ap] tm_wf.simps 
+  by(auto simp: List.list_all_iff shift.simps)
+qed
 
 lemma wf_tm_from_recf:
   assumes compile: "tp = tm_of_rec recf"




