tm: comparison thys/Recursive.thy

equal deleted inserted replaced

-:d5a0e25c4742
+:a9003e6d0463
 definition addition_LE :: "(((nat \<times> nat list) \<times> nat \<times> nat) \<times>
 ((nat \<times> nat list) \<times> nat \<times> nat)) set"
 where "addition_LE \<equiv> (inv_image lex_triple addition_measure)"
-lemma [simp]: "wf addition_LE"
+lemma wf_additon_LE[simp]: "wf addition_LE"
-by(auto simp: wf_inv_image addition_LE_def lex_triple_def
+by(auto simp: addition_LE_def lex_triple_def lex_pair_def)
-lex_pair_def)
 declare addition_inv.simps[simp del]
 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(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] =
 lm[m := xa, n := lm ! n + lm ! m - Suc xa,
 p := lm ! m - Suc xa]"
 apply(case_tac x, simp, simp)
 apply(rule_tac x = nat in exI, simp add: list_update_swap
 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]
 = lm[m := xa, n := lm ! n + lm ! m - xa,
 p := lm ! m - Suc xa]"
 apply(rule_tac x = x in exI,
 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]
 = lm[m := xa, n := lm ! n + lm ! m - xa,
 p := lm ! m - xa]"
 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] =
 lm[m := xa, n := lm ! n + lm ! m - xa,
 p := lm ! m - xa]"
 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,
 p := lm ! m - x, p := lm ! m - Suc x]
 = lm[m := xa, n := lm ! n + lm ! m,
 p := lm ! m - Suc xa]"
 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]
 = lm[m := Suc xa, n := lm ! n + lm ! m,
 p := lm ! m - Suc xa]"
 apply(rule_tac x = x in exI,
 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]
 = lm[m := xa, n := lm ! n + lm ! m, p := lm ! m - xa]"
 apply(rule_tac x = "Suc x" in exI, simp)
 lemma length_addition[simp]: "length (addition a b c) = 7"
 by(auto simp: addition.simps)
 lemma addition_correct:
-"\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk>
+assumes "m \<noteq> n" "max m n < p" "length lm > p" "lm ! p = 0"
-\<Longrightarrow> {\<lambda> a. a = lm} (addition m n p) {\<lambda> nl. addition_inv (7, nl) m n p lm}"
+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
 assume "m \<noteq> n" "m < p \<and> n < p" "p < length lm" "lm ! p = 0"
 then have "\<exists> stp. (\<lambda> (as, lm'). as = 7 \<and> addition_inv (as, lm') m n p lm)
 apply(simp add: abc_steps_l.simps mv_box_inv.simps)
 apply(rule_tac x = "initlm ! m" in exI,
 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] =
 initlm[m := ka, n := la] \<and>
 Suc (ka + la) = initlm ! m + initlm ! n \<and>
 apply(simp add: list_update_overwrite )
 apply(simp add: list_update_swap)
 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>
 \<Longrightarrow> \<exists>ka la. initlm[m := k, n := l, n := Suc l] =
 initlm[m := ka, n := la] \<and>
 ka + la = initlm ! m + initlm ! n \<and>
 ka \<le> initlm ! m"
 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>
 mv_box_inv (abc_steps_l (0, initlm)
 (mv_box m n) na) m n initlm \<longrightarrow>
 apply(rule_tac x = stp in exI, simp)
 done
 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] =
 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ rec_exec (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything"
 using list_update_append[of "rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs)"
 using a g_newcond h x
 by(erule_tac x = "gs!n" in ballE, simp_all)
 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
+have e: "ft \<ge> gf"
-by(simp,  rule_tac min_max.le_supI2, rule_tac Max_ge, simp,
+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)
 show "{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @
 map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything} gp [+] mv_box ga (ft + n)
 by(induct n, auto simp: mv_boxes.simps)
 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)"
 proof -
 assume h: "Suc n \<le> ba - aa"
 apply(simp, insert g)
 apply(simp add: nth_append)
 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"
+using nth_append[of "lm1 @ (0::'a)\<up>n @ last lm2 # lm3 @ butlast lm2"
-"(0\<Colon>'a) # lm4" "ba + n"]
+"(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)
 [ba + n := last lm2, aa + n := 0] =
 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(2-) replicate_Suc_iff_anywhere exp_suc
-apply(simp add: list_update_append list_update.simps replicate_Suc_iff_anywhere exp_suc
+del: replicate_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)
 done
 qed
 thus "?case"
 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;
 \<not> aa - Suc (length lm1) < aa - Suc (length lm1 + n);
 \<not> aa + n - length lm1 < n\<rbrakk>
 by(rule_tac mv_boxes_correct, auto)
 thus "?thesis"
 by(simp add: replicate_merge_anywhere)
 qed
-lemma [intro]:
+lemma length_le_max_insert_rec_ci[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)))"
+"length gs \<le> ffp \<Longrightarrow> length gs \<le> max x1 (Max (insert ffp (x2 ` x3 ` set gs)))"
-apply(rule_tac min_max.le_supI2)
+apply(rule_tac max.coboundedI2)
 apply(simp add: Max_ge_iff)
 done
 lemma restore_new_paras:
 "ffp \<ge> length gs
 ultimately show "?thesis"
 using j
 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)))"
+lemma le_max_insert[intro]: "ffp \<le> max x0 (Max (insert ffp (x1 ` x2 ` set gs)))"
-apply(rule_tac min_max.le_supI2)
+by (rule max.coboundedI2) auto
-apply(rule_tac Max_ge, auto)
-done
 declare max_less_iff_conj[simp del]
 lemma save_rs:
 "\<lbrakk>far = length gs;
 by(simp add: list_update_append list_update.simps replicate_Suc_iff_anywhere del: replicate_Suc)
 ultimately show "?thesis"
 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
 lemma empty_one_box_correct:
 "{\<lambda>nl. nl = 0 \<up> n @ x # lm} [Dec n 2, Goto 0] {\<lambda>nl. nl = 0 # 0 \<up> n @ lm}"
 by(rule_tac ind, simp)
 next
 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>
+lemma insert_dominated[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) =
+length gs + (max xs (Max (insert ffp (x1 ` x2 ` set gs))) - length gs) =
-max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set 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
 lemma clean_paras:
 apply(auto simp: rec_ci.simps abc_comp_commute)
 apply(rule_tac compile_cn_correct', simp_all)
 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:
 "\<lbrakk>length xs = n; ft = max (n+3) (max fft gft)\<rbrakk>
 \<Longrightarrow>  {\<lambda>nl. nl = xs @ rec_exec f xs # 0 \<up> (ft - n) @ anything} mv_box n (Suc n)
 using mv_box_correct[of n "Suc n" "xs @ rec_exec f xs # 0 \<up> (ft - n) @ anything"]
 apply(auto simp: list_update_append list_update.simps nth_append split: if_splits)
 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}"
 proof -
 assume h: "length xs = n"
 apply(simp)
 using b
 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}"
 using mv_box_correct[of n "Suc n" "xs @ rec_exec f xs # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ x # anything"]
 apply(simp add: nth_append list_update_append list_update.simps)
 apply(case_tac "A = []")
 apply(rule_tac x = 0 in exI, simp add: abc_steps_l.simps abc_exec_null)
 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))))
+lemma suc_suc_max_simp[simp]: "Suc (Suc (max (xs + 3) fft - Suc (Suc ( xs))))
-= max (length xs + 3) (max fft gft) - (length 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}"
 apply(simp add: abc_Hoare_halt_def)
 apply(rule_tac x = 1 in exI)
 have "length xs = n \<Longrightarrow>
 {\<lambda>nl. nl = xs @ Suc x # y # anything} [Dec (Suc n) 2, Goto 0] {\<lambda>nl. nl = xs @ Suc x # 0 # anything}" by fact
 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)
+apply(auto simp: abc_Hoare_halt_def numeral_2_eq_2)
-by(case_tac "abc_steps_l (0, xs @ Suc x # y # anything) [Dec (Suc (length xs)) 2, Goto 0] n",
+by (metis (mono_tags, lifting) abc_final.simps abc_holds_for.elims(2) length_Cons list.size(3))
-simp_all add: numeral_2_eq_2)
 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
 by(simp add: abc_steps_l.simps numeral_2_eq_2 abc_step_l.simps abc_fetch.simps
 abc_lm_v.simps abc_lm_s.simps nth_append list_update_append list_update.simps)
 "length xs = n \<Longrightarrow> {\<lambda>nl. nl = xs @ x # y # anything}  [Inc n, Dec (Suc n) 3, Goto (Suc 0)]
 {\<lambda>nl. nl = xs @ Suc x # 0 # anything}"
 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)
 done
 apply(induct y)
 apply(simp add: rec_exec.simps)
 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:
 assumes code: "code = ([Dec (max (n + 3) (max fft gft)) (length gap + 7)] [+] (gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) @
 [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]"
 ultimately show "?thesis"
 using code ft
 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"
 apply(simp add: abc_lm_s.simps)
 using list_update_length[of "xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc (Suc n))"
 0 anything 0]
 apply(auto simp: Suc_diff_Suc)
 apply(simp add: exp_suc[THEN sym] Suc_diff_Suc  del: replicate_Suc)
 done
-lemma [simp]:
+lemma index_at_zero_elem[simp]:
-"(xs @ x # rec_exec (Pr (length xs) f g) (xs @ [x]) # 0 \<up> (max (length xs + 3)
+"(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)
 lemma pr_loop_correct:
 assumes less: "y \<le> x"
 lemma wf_mn_le[intro]: "wf mn_LE"
 by(auto intro:wf_inv_image wf_lex_triple simp: mn_LE_def)
 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)
 apply(simp add: list_update_append list_update.simps)
 done
 lemma abc_comp_null[simp]: "(A [+] B = []) = (A = [] \<and> B = [])"
 by(auto simp: abc_comp.simps abc_shift.simps)
 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 x42", auto simp: mv_box.simps)
-apply(case_tac "rec_ci recf1", case_tac "rec_ci recf2", simp)
+apply(case_tac "rec_ci x52", case_tac "rec_ci x53", simp)
-apply(case_tac "rec_ci recf", simp)
+apply(case_tac "rec_ci x62", simp)
 done
 lemma mn_correct:
 assumes compile: "rec_ci rf = (fap, far, fft)"
 and ge: "0 < rsx"
 lemma abc_list_crsp_elim:
 "\<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)
 apply(rule_tac x = "na + length lmb - Suc m" in exI)
 apply(rule_tac disjI1)
 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)
 apply(rule_tac x = "na + length lma - Suc m" in exI)
 apply(rule_tac disjI2)
 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)
 lemma abc_list_crsp_lm_s:
 "abc_list_crsp lma lmb \<Longrightarrow>
 fix stp a lm' aa b
 assume ind:
 "\<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)
 done
 from this obtain lma where g2:
 hence g3: "abc_steps_l (0, lm) aprog (Suc stp)
 = abc_step_l (aa, lma) (abc_fetch aa aprog)"
 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)
 apply(rule_tac abc_list_crsp_step, auto)
 done
 apply(case_tac "abc_steps_l (0, args @ 0 \<up> (ft - arity)) ap n", auto)
 apply(drule_tac abc_list_crsp_steps, auto)
 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"
 using assms
 apply(case_tac n, simp)
 apply(rule_tac x = 0 in exI, simp)
 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"
 apply(case_tac n, simp_all add: exp_suc list_update_append list_update.simps del: replicate_Suc)
 apply(subgoal_tac "length args = Suc (length lm)", simp)
 using g_unhalt[of "0 \<up> (?ft - (length args) - (gft - gar)) @
 map (\<lambda>i. rec_exec i args) (take i gs) @ 0 \<up> (length gs - i) @ 0 \<up> Suc (length args) @ anything"]
 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"
 using compile2
 apply(rule_tac arg_cong)
 (0, Bk\<up>Suc (Suc m), Oc\<up>Suc (rec_exec recf args) @ Bk\<up>l)"
 proof(case_tac "rec_ci recf", simp add: tm_of_rec.simps)
 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,
+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:
 assumes termi: "terminate recf args"
 shows "{\<lambda> tp. tp =([Bk, Bk], <args>)} (tm_of_rec recf)
 {\<lambda> tp. \<exists> k l. tp = (Bk\<up> k, <rec_exec recf args> @ Bk \<up> l)}"
 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)
 apply(case_tac a, simp)
 done
 lemma shift_append: "shift (xs @ ys) n = shift xs n @ shift ys n"
 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
 lemma length_tm_even[intro]: "length (tm_of ap) mod 2 = 0"
 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
 lemma start_of_suc_inc:
 apply(case_tac "ap!k", auto simp: tms_of.simps tpairs_of.simps ci.simps shift_append adjust.simps)
 apply(erule_tac findnth_state_all_le1, simp_all)
 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
 lemma concat_in: "i < length (concat xs) \<Longrightarrow>
 \<exists>k < length xs. concat xs ! i \<in> set (xs ! k)"
 apply(simp add: nth_append)
 apply(rule_tac x = "length xs" in exI, simp)
 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
 declare length_concat[simp]
 apply(case_tac "ap ! k")
 apply(auto simp: layout_of.simps ci.simps
 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")
 apply(auto)
 done
 lemma length_start_of_tm: "start_of (layout_of ap) (length ap) = Suc (length (tm_of ap)  div 2)"
 using tpa_states[of "tm_of ap"  "length ap" ap]
 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)
+by(auto simp: list_all_length)
-apply(auto)
-done
+lemma mopup_b_12[simp]: "length mopup_b = 12"
-lemma [simp]: "length mopup_b = 12"
 apply(simp add: mopup_b_def)
 done
 lemma mp_up_all_le: "list_all  (\<lambda>(acn, s). s \<le> q + (2 * n + 6))
 [(R, Suc (Suc (2 * n + q))), (R, Suc (2 * n + q)),
 (L, 5 + 2 * n + q), (W0, Suc (Suc (Suc (2 * n + q)))), (R, 4 + 2 * n + q),
 (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)
+by(auto)
-done
+lemma mopup_le6[simp]: "(a, b) \<in> set (mopup_a n) \<Longrightarrow> b \<le> 2 * n + 6"
-lemma [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)))
+lemma shift_le2[simp]: "(a, b) \<in> set (shift (mopup n) x)
-\<Longrightarrow> b \<le> (2 * listsum (layout_of ap) + length (mopup n)) div 2"
+\<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"
+lemma mopup_even[intro]: " (2 * x + length (mopup n)) mod 2 = 0"
-apply(auto simp: mopup.simps)
+by(auto simp: mopup.simps)
-apply arith
-done
+lemma mopup_div_2[simp]: "b \<le> Suc x
-lemma [simp]: "b \<le> Suc x
 \<Longrightarrow> b \<le> (2 * x + length (mopup n)) div 2"
-apply(auto simp: mopup.simps)
+by(auto simp: mopup.simps)
-done
+lemma wf_tm_from_abacus: assumes "tp = tm_of ap"
-lemma wf_tm_from_abacus:
+shows "tm_wf0 (tp @ shift (mopup n) (length tp div 2))"
-"tp = tm_of ap \<Longrightarrow>
+proof -
-tm_wf (tp @ shift( mopup n) (length tp div 2), 0)"
+have "is_even (length (mopup n))" for n using tm_wf.simps by blast
-using length_start_of_tm[of ap] all_le_start_of[of ap]
+moreover have "(aa, ba) \<in> set (mopup n) \<Longrightarrow> ba \<le> length (mopup n) div 2" for aa ba
-apply(auto simp: tm_wf.simps List.list_all_iff)
+by (metis (no_types, lifting) add_cancel_left_right case_prodD tm_wf.simps wf_mopup)
-apply(case_tac n)
+moreover have "(\<forall>x\<in>set (tm_of ap). case x of (acn, s) \<Rightarrow> s \<le> Suc (sum_list (layout_of ap))) \<Longrightarrow>
-apply(simp add: mopup.simps)
+(a, b) \<in> set (tm_of ap) \<Longrightarrow> b \<le> sum_list (layout_of ap) + length (mopup n) div 2"
-apply(simp add: mopup.simps)
+for a b s
-apply (metis mod_mult_right_eq mod_mult_self2 mod_mult_self2_is_0 mult_2_right nat_mult_commute numeral_Bit0)
+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)
-sorry
+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"
 shows "tm_wf0 tp"
 proof -

changeset 288	a9003e6d0463
parent 285	447b433b67fa
child 290	6e1c03614d36