--- 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"
--- a/thys/UF.thy Wed Jan 14 09:08:51 2015 +0000
+++ b/thys/UF.thy Wed Dec 19 16:10:58 2018 +0100
@@ -2,10 +2,10 @@
Author: Jian Xu, Xingyuan Zhang, and Christian Urban
*)
-header {* Construction of a Universal Function *}
+chapter {* Construction of a Universal Function *}
theory UF
-imports Rec_Def GCD Abacus
+imports Rec_Def HOL.GCD Abacus
begin
text {*
@@ -289,9 +289,6 @@
arity.simps[simp del] Sigma.simps[simp del]
rec_sigma.simps[simp del]
-lemma [simp]: "arity z = 1"
- by(simp add: arity.simps)
-
lemma rec_pr_0_simp_rewrite: "
rec_exec (Pr n f g) (xs @ [0]) = rec_exec f xs"
by(simp add: rec_exec.simps)
@@ -341,7 +338,7 @@
take_Suc_conv_app_nth)
qed
-lemma [simp]: "primerec f n \<Longrightarrow> arity f = n"
+lemma arity_primerec[simp]: "primerec f n \<Longrightarrow> arity f = n"
apply(case_tac f)
apply(auto simp: arity.simps )
apply(erule_tac prime_mn_reverse)
@@ -527,30 +524,28 @@
apply(rule_tac Min_le, auto)
done
-lemma [simp]: "{x. x \<le> Suc w \<and> Rr (xs @ [x])}
+lemma expand_conj_in_set: "{x. x \<le> Suc w \<and> Rr (xs @ [x])}
= (if Rr (xs @ [Suc w]) then insert (Suc w)
{x. x \<le> w \<and> Rr (xs @ [x])}
else {x. x \<le> w \<and> Rr (xs @ [x])})"
by(auto, case_tac "x = Suc w", auto)
-lemma [simp]: "Minr Rr xs w \<le> w \<Longrightarrow> Minr Rr xs (Suc w) = Minr Rr xs w"
-apply(simp add: Minr.simps, auto)
-apply(case_tac "\<forall>x\<le>w. \<not> Rr (xs @ [x])", auto)
-done
-
-lemma [simp]: "\<forall>x\<le>w. \<not> Rr (xs @ [x]) \<Longrightarrow>
+lemma Minr_strip_Suc[simp]: "Minr Rr xs w \<le> w \<Longrightarrow> Minr Rr xs (Suc w) = Minr Rr xs w"
+by(cases "\<forall>x\<le>w. \<not> Rr (xs @ [x])",auto simp add: Minr.simps expand_conj_in_set)
+
+lemma x_empty_set[simp]: "\<forall>x\<le>w. \<not> Rr (xs @ [x]) \<Longrightarrow>
{x. x \<le> w \<and> Rr (xs @ [x])} = {} "
by auto
-lemma [simp]: "\<lbrakk>Minr Rr xs w = Suc w; Rr (xs @ [Suc w])\<rbrakk> \<Longrightarrow>
+lemma Minr_is_Suc[simp]: "\<lbrakk>Minr Rr xs w = Suc w; Rr (xs @ [Suc w])\<rbrakk> \<Longrightarrow>
Minr Rr xs (Suc w) = Suc w"
-apply(simp add: Minr.simps)
+apply(simp add: Minr.simps expand_conj_in_set)
apply(case_tac "\<forall>x\<le>w. \<not> Rr (xs @ [x])", auto)
done
-lemma [simp]: "\<lbrakk>Minr Rr xs w = Suc w; \<not> Rr (xs @ [Suc w])\<rbrakk> \<Longrightarrow>
+lemma Minr_is_Suc_Suc[simp]: "\<lbrakk>Minr Rr xs w = Suc w; \<not> Rr (xs @ [Suc w])\<rbrakk> \<Longrightarrow>
Minr Rr xs (Suc w) = Suc (Suc w)"
-apply(simp add: Minr.simps)
+apply(simp add: Minr.simps expand_conj_in_set)
apply(case_tac "\<forall>x\<le>w. \<not> Rr (xs @ [x])", auto)
apply(subgoal_tac "Min {x. x \<le> w \<and> Rr (xs @ [x])} \<in>
{x. x \<le> w \<and> Rr (xs @ [x])}", simp)
@@ -612,50 +607,45 @@
declare numeral_3_eq_3[simp]
-lemma [intro]: "primerec rec_pred (Suc 0)"
+lemma primerec_rec_pred_1[intro]: "primerec rec_pred (Suc 0)"
apply(simp add: rec_pred_def)
apply(rule_tac prime_cn, auto)
apply(case_tac i, auto intro: prime_id)
done
-lemma [intro]: "primerec rec_minus (Suc (Suc 0))"
+lemma primerec_rec_minus_2[intro]: "primerec rec_minus (Suc (Suc 0))"
apply(auto simp: rec_minus_def)
done
-lemma [intro]: "primerec (constn n) (Suc 0)"
+lemma primerec_constn_1[intro]: "primerec (constn n) (Suc 0)"
apply(induct n)
apply(auto simp: constn.simps intro: prime_z prime_cn prime_s)
done
-lemma [intro]: "primerec rec_sg (Suc 0)"
+lemma primerec_rec_sg_1[intro]: "primerec rec_sg (Suc 0)"
apply(simp add: rec_sg_def)
apply(rule_tac k = "Suc (Suc 0)" in prime_cn, auto)
apply(case_tac i, auto)
apply(case_tac ia, auto intro: prime_id)
done
-lemma [simp]: "length (get_fstn_args m n) = n"
- apply(induct n)
- apply(auto simp: get_fstn_args.simps)
- done
-
-lemma primerec_getpren[elim]: "\<lbrakk>i < n; n \<le> m\<rbrakk> \<Longrightarrow> primerec (get_fstn_args m n ! i) m"
+lemma primerec_getpren[elim]: "\<lbrakk>i < n; n \<le> m\<rbrakk> \<Longrightarrow> primerec (get_fstn_args m n ! i) m"
apply(induct n, auto simp: get_fstn_args.simps)
apply(case_tac "i = n", auto simp: nth_append intro: prime_id)
done
-lemma [intro]: "primerec rec_add (Suc (Suc 0))"
+lemma primerec_rec_add_2[intro]: "primerec rec_add (Suc (Suc 0))"
apply(simp add: rec_add_def)
apply(rule_tac prime_pr, auto)
done
-lemma [intro]:"primerec rec_mult (Suc (Suc 0))"
+lemma primerec_rec_mult_2[intro]:"primerec rec_mult (Suc (Suc 0))"
apply(simp add: rec_mult_def )
apply(rule_tac prime_pr, auto intro: prime_z)
apply(case_tac i, auto intro: prime_id)
done
-lemma [elim]: "\<lbrakk>primerec rf n; n \<ge> Suc (Suc 0)\<rbrakk> \<Longrightarrow>
+lemma primerec_ge_2_elim[elim]: "\<lbrakk>primerec rf n; n \<ge> Suc (Suc 0)\<rbrakk> \<Longrightarrow>
primerec (rec_accum rf) n"
apply(auto simp: rec_accum.simps)
apply(simp add: nth_append, auto)
@@ -670,11 +660,11 @@
apply(auto, simp add: nth_append, auto)
done
-lemma [simp]: "Rr (xs @ [0]) \<Longrightarrow>
+lemma min_P0[simp]: "Rr (xs @ [0]) \<Longrightarrow>
Min {x. x = (0::nat) \<and> Rr (xs @ [x])} = 0"
by(rule_tac Min_eqI, simp, simp, simp)
-lemma [intro]: "primerec rec_not (Suc 0)"
+lemma primerec_rec_not_1[intro]: "primerec rec_not (Suc 0)"
apply(simp add: rec_not_def)
apply(rule prime_cn, auto)
apply(case_tac i, auto intro: prime_id)
@@ -825,24 +815,24 @@
declare rec_maxr.simps[simp del] Maxr.simps[simp del]
declare le_lemma[simp]
-lemma [simp]: "(min (Suc (Suc (Suc (x)))) (x)) = x"
+lemma min_with_suc3[simp]: "(min (Suc (Suc (Suc (x)))) (x)) = x"
by simp
declare numeral_2_eq_2[simp]
-lemma [intro]: "primerec rec_disj (Suc (Suc 0))"
+lemma primerec_rec_disj_2[intro]: "primerec rec_disj (Suc (Suc 0))"
apply(simp add: rec_disj_def, auto)
apply(auto)
apply(case_tac ia, auto intro: prime_id)
done
-lemma [intro]: "primerec rec_less (Suc (Suc 0))"
+lemma primerec_rec_less_2[intro]: "primerec rec_less (Suc (Suc 0))"
apply(simp add: rec_less_def, auto)
apply(auto)
apply(case_tac ia , auto intro: prime_id)
done
-lemma [intro]: "primerec rec_eq (Suc (Suc 0))"
+lemma primerec_rec_eq_2[intro]: "primerec rec_eq (Suc (Suc 0))"
apply(simp add: rec_eq_def)
apply(rule_tac prime_cn, auto)
apply(case_tac i, auto)
@@ -850,13 +840,13 @@
apply(case_tac [!] i, auto intro: prime_id)
done
-lemma [intro]: "primerec rec_le (Suc (Suc 0))"
+lemma primerec_rec_le_2[intro]: "primerec rec_le (Suc (Suc 0))"
apply(simp add: rec_le_def)
apply(rule_tac prime_cn, auto)
apply(case_tac i, auto)
done
-lemma [simp]:
+lemma take_butlast_list_plus_two[simp]:
"length ys = Suc n \<Longrightarrow> (take n ys @ [ys ! n, ys ! n]) =
ys @ [ys ! n]"
apply(simp)
@@ -868,11 +858,11 @@
lemma Maxr_Suc_simp:
"Maxr Rr xs (Suc w) =(if Rr (xs @ [Suc w]) then Suc w
else Maxr Rr xs w)"
-apply(auto simp: Maxr.simps Max.insert)
+apply(auto simp: Maxr.simps expand_conj_in_set)
apply(rule_tac Max_eqI, auto)
done
-lemma [simp]: "min (Suc n) n = n" by simp
+lemma min_Suc_1[simp]: "min (Suc n) n = n" by simp
lemma Sigma_0: "\<forall> i \<le> n. (f (xs @ [i]) = 0) \<Longrightarrow>
Sigma f (xs @ [n]) = 0"
@@ -880,7 +870,7 @@
apply(simp add: Sigma_Suc_simp_rewrite)
done
-lemma [elim]: "\<forall>k<Suc w. f (xs @ [k]) = Suc 0
+lemma Sigma_Suc[elim]: "\<forall>k<Suc w. f (xs @ [k]) = Suc 0
\<Longrightarrow> Sigma f (xs @ [w]) = Suc w"
apply(induct w)
apply(simp add: Sigma.simps, simp)
@@ -1058,28 +1048,23 @@
text {*
The following lemmas shows more directly the menaing of @{text "quo"}:
*}
-lemma [elim!]: "y > 0 \<Longrightarrow> quo [x, y] = x div y"
-proof(simp add: quo.simps Maxr.simps, auto,
- rule_tac Max_eqI, simp, auto)
+lemma quo_is_div: "y > 0 \<Longrightarrow> quo [x, y] = x div y"
+proof -
+ {
fix xa ya
assume h: "y * ya \<le> x" "y > 0"
hence "(y * ya) div y \<le> x div y"
by(insert div_le_mono[of "y * ya" x y], simp)
- from this and h show "ya \<le> x div y" by simp
-next
- fix xa
- show "y * (x div y) \<le> x"
- apply(subgoal_tac "y * (x div y) + x mod y = x")
- apply(rule_tac k = "x mod y" in add_leD1, simp)
- apply(simp)
- done
+ from this and h have "ya \<le> x div y" by simp}
+ thus ?thesis by(simp add: quo.simps Maxr.simps, auto,
+ rule_tac Max_eqI, simp, auto)
qed
-lemma [intro]: "quo [x, 0] = 0"
+lemma quo_zero[intro]: "quo [x, 0] = 0"
by(simp add: quo.simps Maxr.simps)
lemma quo_div: "quo [x, y] = x div y"
-by(case_tac "y=0", auto)
+by(case_tac "y=0", auto elim!:quo_is_div)
text {*
@{text "rec_noteq"} is the recursive function testing whether its
@@ -1120,13 +1105,13 @@
(0),id (Suc (Suc 0)) (Suc (0)),
id (Suc (Suc 0)) (0)]"
-lemma [intro]: "primerec rec_conj (Suc (Suc 0))"
+lemma primerec_rec_conj_2[intro]: "primerec rec_conj (Suc (Suc 0))"
apply(simp add: rec_conj_def)
apply(rule_tac prime_cn, auto)+
apply(case_tac i, auto intro: prime_id)
done
-lemma [intro]: "primerec rec_noteq (Suc (Suc 0))"
+lemma primerec_rec_noteq_2[intro]: "primerec rec_noteq (Suc (Suc 0))"
apply(simp add: rec_noteq_def)
apply(rule_tac prime_cn, auto)+
apply(case_tac i, auto intro: prime_id)
@@ -1189,13 +1174,7 @@
The correctness of @{text "rec_mod"}:
*}
lemma mod_lemma: "\<And> x y. rec_exec rec_mod [x, y] = (x mod y)"
-proof(simp add: rec_exec.simps rec_mod_def quo_lemma2)
- fix x y
- show "x - x div y * y = x mod (y::nat)"
- using mod_div_equality2[of y x]
- apply(subgoal_tac "y * (x div y) = (x div y ) * y", arith, simp)
- done
-qed
+ by(simp add: rec_exec.simps rec_mod_def quo_lemma2 minus_div_mult_eq_mod)
text{* lemmas for embranch function*}
type_synonym ftype = "nat list \<Rightarrow> nat"
@@ -1604,7 +1583,7 @@
"fac 0 = 1" |
"fac (Suc x) = (Suc x) * fac x"
-lemma [simp]: "rec_exec rec_dummyfac [0, 0] = Suc 0"
+lemma rec_exec_rec_dummyfac_0: "rec_exec rec_dummyfac [0, 0] = Suc 0"
by(simp add: rec_dummyfac_def rec_exec.simps)
lemma rec_cn_simp: "rec_exec (Cn n f gs) xs =
@@ -1648,7 +1627,7 @@
Cn 2 rec_prime [id 2 1]]
in Cn 1 (rec_Minr Rr) [id 1 0, Cn 1 s [rec_fac]])"
-lemma [simp]: "n < Suc (n!)"
+lemma n_le_fact[simp]: "n < Suc (n!)"
apply(induct n, simp)
apply(simp add: fac.simps)
apply(case_tac n, auto simp: fac.simps)
@@ -1667,7 +1646,7 @@
apply(rule_tac x = u in exI, simp, auto)
done
-lemma [intro]: "0 < n!"
+lemma fact_pos[intro]: "0 < n!"
apply(induct n)
apply(auto simp: fac.simps)
done
@@ -1740,7 +1719,7 @@
primerec (ys ! 0) n; primerec (ys ! 1) n\<rbrakk> \<Longrightarrow> primerec (ys ! i) n"
by(case_tac i, auto)
-lemma [intro]: "primerec rec_prime (Suc 0)"
+lemma primerec_rec_prime_1[intro]: "primerec rec_prime (Suc 0)"
apply(auto simp: rec_prime_def, auto)
apply(rule_tac primerec_all_iff, auto, auto)
apply(rule_tac primerec_all_iff, auto, auto simp:
@@ -1835,7 +1814,7 @@
declare lo.simps[simp del]
-lemma [elim]: "primerec rf n \<Longrightarrow> n > 0"
+lemma primerec_then_ge_0[elim]: "primerec rf n \<Longrightarrow> n > 0"
apply(induct rule: primerec.induct, auto)
done
@@ -1846,7 +1825,7 @@
apply(auto, auto simp: nth_append)
done
-lemma [intro!]: "\<lbrakk>primerec rf n; n > 0\<rbrakk> \<Longrightarrow> primerec (rec_maxr rf) n"
+lemma primerec_rec_maxr[intro!]: "\<lbrakk>primerec rf n; n > 0\<rbrakk> \<Longrightarrow> primerec (rec_maxr rf) n"
apply(simp add: rec_maxr.simps)
apply(rule_tac prime_cn, auto)
apply(rule_tac primerec_all_iff, auto, auto simp: nth_append)
@@ -1859,23 +1838,10 @@
apply(case_tac i, auto, case_tac nat, simp, simp add: numeral_2_eq_2)
done
-lemma [intro]: "primerec rec_quo (Suc (Suc 0))"
-apply(simp add: rec_quo_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_mod (Suc (Suc 0))"
-apply(simp add: rec_mod_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_power (Suc (Suc 0))"
-apply(simp add: rec_power_def numeral_2_eq_2 numeral_3_eq_3)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
+lemma primerec_2[intro]:
+"primerec rec_quo (Suc (Suc 0))" "primerec rec_mod (Suc (Suc 0))"
+"primerec rec_power (Suc (Suc 0))"
+ by(force simp: prime_cn prime_id rec_mod_def rec_quo_def rec_power_def prime_pr numeral)+
text {*
@{text "rec_lo"} is the recursive function used to implement @{text "Lo"}.
@@ -1919,14 +1885,12 @@
done
qed
-lemma [simp]: "Max {ya. ya = 0 \<and> loR [0, y, ya]} = 0"
+lemma MaxloR0[simp]: "Max {ya. ya = 0 \<and> loR [0, y, ya]} = 0"
apply(rule_tac Max_eqI, auto simp: loR.simps)
done
-lemma [simp]: "Suc 0 < y \<Longrightarrow> Suc (Suc 0) < y * y"
-apply(induct y, simp)
-apply(case_tac y, simp, simp)
-done
+lemma two_less_square[simp]: "Suc 0 < y \<Longrightarrow> Suc (Suc 0) < y * y"
+ by(induct y, auto)
lemma less_mult: "\<lbrakk>x > 0; y > Suc 0\<rbrakk> \<Longrightarrow> x < y * x"
apply(case_tac y, simp, simp)
@@ -1942,17 +1906,16 @@
lemma le_mult: "y \<noteq> (0::nat) \<Longrightarrow> x \<le> x * y"
by(induct y, simp, simp)
-lemma uplimit_loR: "\<lbrakk>Suc 0 < x; Suc 0 < y; loR [x, y, xa]\<rbrakk> \<Longrightarrow>
- xa \<le> x"
-apply(simp add: loR.simps)
-apply(rule_tac classical, auto)
-apply(subgoal_tac "xa < y^xa")
-apply(subgoal_tac "y^xa \<le> y^xa * q", simp)
-apply(rule_tac le_mult, case_tac q, simp, simp)
-apply(rule_tac x_less_exp, simp)
-done
-
-lemma [simp]: "\<lbrakk>xa \<le> x; loR [x, y, xa]; Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow>
+lemma uplimit_loR:
+ assumes "Suc 0 < x" "Suc 0 < y" "loR [x, y, xa]"
+ shows "xa \<le> x"
+proof -
+ have "Suc 0 < x \<Longrightarrow> Suc 0 < y \<Longrightarrow> y ^ xa dvd x \<Longrightarrow> xa \<le> x"
+ by (meson Suc_lessD le_less_trans nat_dvd_not_less nat_le_linear x_less_exp)
+ thus ?thesis using assms by(auto simp: loR.simps)
+qed
+
+lemma loR_set_strengthen[simp]: "\<lbrakk>xa \<le> x; loR [x, y, xa]; Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow>
{u. loR [x, y, u]} = {ya. ya \<le> x \<and> loR [x, y, ya]}"
apply(rule_tac Collect_cong, auto)
apply(erule_tac uplimit_loR, simp, simp)
@@ -2043,20 +2006,20 @@
by simp
qed
-lemma [simp]: "\<lbrakk>Suc 0 < y; lgR [x, y, xa]\<rbrakk> \<Longrightarrow> xa \<le> x"
+lemma lgR_ok: "\<lbrakk>Suc 0 < y; lgR [x, y, xa]\<rbrakk> \<Longrightarrow> xa \<le> x"
apply(simp add: lgR.simps)
apply(subgoal_tac "y^xa > xa", simp)
apply(erule x_less_exp)
done
-lemma [simp]: "\<lbrakk>Suc 0 < x; Suc 0 < y; lgR [x, y, xa]\<rbrakk> \<Longrightarrow>
+lemma lgR_set_strengthen[simp]: "\<lbrakk>Suc 0 < x; Suc 0 < y; lgR [x, y, xa]\<rbrakk> \<Longrightarrow>
{u. lgR [x, y, u]} = {ya. ya \<le> x \<and> lgR [x, y, ya]}"
-apply(rule_tac Collect_cong, auto)
+apply(rule_tac Collect_cong, auto simp:lgR_ok)
done
lemma maxr_lg: "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow> Maxr lgR [x, y] x = lg x y"
apply(simp add: lg.simps Maxr.simps, auto)
-apply(erule_tac x = xa in allE, simp)
+apply(erule_tac x = xa in allE, auto simp:lgR_ok)
done
lemma lg_lemma': "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow> rec_exec rec_lg [x, y] = lg x y"
@@ -2445,7 +2408,7 @@
apply(case_tac nat, auto simp: numeral_3_eq_3 numeral_4_eq_4)
done
-lemma [intro]: "primerec rec_scan (Suc 0)"
+lemma primerec_rec_scan_1[intro]: "primerec rec_scan (Suc 0)"
apply(auto simp: rec_scan_def, auto)
done
@@ -2682,7 +2645,7 @@
done
qed
-lemma [elim]:
+lemma nonempty_listE:
"Suc 0 \<le> length xs \<Longrightarrow>
(map ((\<lambda>a. rec_exec a (m # xs)) \<circ>
(\<lambda>i. recf.id (Suc (length xs)) (i)))
@@ -2703,7 +2666,7 @@
"(map ((\<lambda>a. rec_exec a (m # xs)) \<circ>
(\<lambda>i. recf.id (Suc (length xs)) (i)))
[Suc 0..<length xs] @ [(m # xs) ! length xs]) = xs", simp)
-apply(auto, case_tac xs, auto)
+apply(auto elim:nonempty_listE, case_tac xs, auto)
done
definition rec_newconf:: "recf"
@@ -2878,180 +2841,135 @@
lemma primerec_not0: "primerec f n \<Longrightarrow> n > 0"
by(induct f n rule: primerec.induct, auto)
-lemma [elim]: "primerec f 0 \<Longrightarrow> RR"
+lemma primerec_not0E[elim]: "primerec f 0 \<Longrightarrow> RR"
apply(drule_tac primerec_not0, simp)
done
-lemma [simp]: "length xs = Suc n \<Longrightarrow> length (butlast xs) = n"
-apply(subgoal_tac "\<exists> y ys. xs = ys @ [y]", auto)
+lemma length_butlast[simp]: "length xs = Suc n \<Longrightarrow> length (butlast xs) = n"
+apply(subgoal_tac "\<exists> y ys. xs = ys @ [y]",force)
apply(rule_tac x = "last xs" in exI)
apply(rule_tac x = "butlast xs" in exI)
apply(case_tac "xs = []", auto)
done
text {*
- The lemma relates the interpreter of primitive fucntions with
+ The lemma relates the interpreter of primitive functions with
the calculation relation of general recursive functions.
*}
declare numeral_2_eq_2[simp] numeral_3_eq_3[simp]
-lemma [intro]: "primerec rec_right (Suc 0)"
-apply(simp add: rec_right_def rec_lo_def Let_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_pi (Suc 0)"
-apply(simp add: rec_pi_def rec_dummy_pi_def
- rec_np_def rec_fac_def rec_prime_def
- rec_Minr.simps Let_def get_fstn_args.simps
- arity.simps
- rec_all.simps rec_sigma.simps rec_accum.simps)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-apply(simp add: rec_dummyfac_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
+lemma primerec_rec_right_1[intro]: "primerec rec_right (Suc 0)"
+ by(auto simp: rec_right_def rec_lo_def Let_def;force)
+
+lemma primerec_rec_pi_helper:
+ "\<forall>i<Suc (Suc 0). primerec ([recf.id (Suc 0) 0, recf.id (Suc 0) 0] ! i) (Suc 0)"
+ by fastforce
+
+lemmas primerec_rec_pi_helpers =
+ primerec_rec_pi_helper primerec_constn_1 primerec_rec_sg_1 primerec_rec_not_1 primerec_rec_conj_2
+
+lemma primrec_dummyfac:
+ "\<forall>i<Suc (Suc 0).
+ primerec
+ ([recf.id (Suc 0) 0,
+ Cn (Suc 0) s
+ [Cn (Suc 0) rec_dummyfac
+ [recf.id (Suc 0) 0, recf.id (Suc 0) 0]]] !
+ i)
+ (Suc 0)"
+ by(auto simp: rec_dummyfac_def;force)
+
+lemma primerec_rec_pi_1[intro]: "primerec rec_pi (Suc 0)"
+ apply(simp add: rec_pi_def rec_dummy_pi_def
+ rec_np_def rec_fac_def rec_prime_def
+ rec_Minr.simps Let_def get_fstn_args.simps
+ arity.simps
+ rec_all.simps rec_sigma.simps rec_accum.simps)
+ apply(tactic {* resolve_tac @{context} [@{thm prime_cn}, @{thm prime_pr}] 1*}
+ ;(simp add:primerec_rec_pi_helpers primrec_dummyfac)?)+
+ by fastforce+
+
+lemma primerec_rec_trpl[intro]: "primerec rec_trpl (Suc (Suc (Suc 0)))"
+apply(simp add: rec_trpl_def)
+apply(tactic {* resolve_tac @{context} [@{thm prime_cn},
@{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
done
-lemma [intro]: "primerec rec_trpl (Suc (Suc (Suc 0)))"
-apply(simp add: rec_trpl_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro!]: "\<lbrakk>0 < vl; n \<le> vl\<rbrakk> \<Longrightarrow> primerec (rec_listsum2 vl n) vl"
+lemma primerec_rec_listsum2[intro!]: "\<lbrakk>0 < vl; n \<le> vl\<rbrakk> \<Longrightarrow> primerec (rec_listsum2 vl n) vl"
apply(induct n)
apply(simp_all add: rec_strt'.simps Let_def rec_listsum2.simps)
-apply(tactic {* resolve_tac [@{thm prime_cn},
+apply(tactic {* resolve_tac @{context} [@{thm prime_cn},
@{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
done
-lemma [elim]: "\<lbrakk>0 < vl; n \<le> vl\<rbrakk> \<Longrightarrow> primerec (rec_strt' vl n) vl"
+lemma primerec_rec_strt': "\<lbrakk>0 < vl; n \<le> vl\<rbrakk> \<Longrightarrow> primerec (rec_strt' vl n) vl"
apply(induct n)
apply(simp_all add: rec_strt'.simps Let_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
+apply(tactic {* resolve_tac @{context} [@{thm prime_cn},
@{thm prime_id}, @{thm prime_pr}] 1*}, auto+)
done
-lemma [elim]: "vl > 0 \<Longrightarrow> primerec (rec_strt vl) vl"
+lemma primerec_rec_strt: "vl > 0 \<Longrightarrow> primerec (rec_strt vl) vl"
apply(simp add: rec_strt.simps rec_strt'.simps)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [elim]:
+by(tactic {* resolve_tac @{context} [@{thm prime_cn},
+ @{thm prime_id}, @{thm prime_pr}] 1*}; force elim:primerec_rec_strt')
+
+lemma primerec_map_vl:
"i < vl \<Longrightarrow> primerec ((map (\<lambda>i. recf.id (Suc vl) (i))
[Suc 0..<vl] @ [recf.id (Suc vl) (vl)]) ! i) (Suc vl)"
apply(induct i, auto simp: nth_append)
done
-lemma [intro]: "primerec rec_newleft0 ((Suc (Suc 0)))"
-apply(simp add: rec_newleft_def rec_embranch.simps
- Let_def arity.simps rec_newleft0_def
- rec_newleft1_def rec_newleft2_def rec_newleft3_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newleft1 ((Suc (Suc 0)))"
-apply(simp add: rec_newleft_def rec_embranch.simps
- Let_def arity.simps rec_newleft0_def
- rec_newleft1_def rec_newleft2_def rec_newleft3_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newleft2 ((Suc (Suc 0)))"
-apply(simp add: rec_newleft_def rec_embranch.simps
- Let_def arity.simps rec_newleft0_def
- rec_newleft1_def rec_newleft2_def rec_newleft3_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newleft3 ((Suc (Suc 0)))"
-apply(simp add: rec_newleft_def rec_embranch.simps
- Let_def arity.simps rec_newleft0_def
+lemma primerec_recs[intro]:
+ "primerec rec_newleft0 (Suc (Suc 0))"
+ "primerec rec_newleft1 (Suc (Suc 0))"
+"primerec rec_newleft2 (Suc (Suc 0))"
+"primerec rec_newleft3 ((Suc (Suc 0)))"
+"primerec rec_newleft (Suc (Suc (Suc 0)))"
+"primerec rec_left (Suc 0)"
+"primerec rec_actn (Suc (Suc (Suc 0)))"
+"primerec rec_stat (Suc 0)"
+"primerec rec_newstat (Suc (Suc (Suc 0)))"
+apply(simp_all add: rec_newleft_def rec_embranch.simps rec_left_def rec_lo_def rec_entry_def
+ rec_actn_def Let_def arity.simps rec_newleft0_def rec_stat_def rec_newstat_def
rec_newleft1_def rec_newleft2_def rec_newleft3_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newleft (Suc (Suc (Suc 0)))"
-apply(simp add: rec_newleft_def rec_embranch.simps
- Let_def arity.simps)
-apply(rule_tac prime_cn, auto+)
-done
-
-lemma [intro]: "primerec rec_left (Suc 0)"
-apply(simp add: rec_left_def rec_lo_def rec_entry_def Let_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_actn (Suc (Suc (Suc 0)))"
-apply(simp add: rec_left_def rec_lo_def rec_entry_def
- Let_def rec_actn_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_stat (Suc 0)"
-apply(simp add: rec_left_def rec_lo_def rec_entry_def Let_def
- rec_actn_def rec_stat_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newstat (Suc (Suc (Suc 0)))"
-apply(simp add: rec_left_def rec_lo_def rec_entry_def
- Let_def rec_actn_def rec_stat_def rec_newstat_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newrght (Suc (Suc (Suc 0)))"
+apply(tactic {* resolve_tac @{context} [@{thm prime_cn},
+ @{thm prime_id}, @{thm prime_pr}] 1*};force)+
+ done
+
+lemma primerec_rec_newrght[intro]: "primerec rec_newrght (Suc (Suc (Suc 0)))"
apply(simp add: rec_newrght_def rec_embranch.simps
Let_def arity.simps rec_newrgt0_def
rec_newrgt1_def rec_newrgt2_def rec_newrgt3_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newconf (Suc (Suc 0))"
-apply(simp add: rec_newconf_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "0 < vl \<Longrightarrow> primerec (rec_inpt (Suc vl)) (Suc vl)"
-apply(simp add: rec_inpt_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
+apply(tactic {* resolve_tac @{context} [@{thm prime_cn},
+ @{thm prime_id}, @{thm prime_pr}] 1*};force)+
done
-lemma [intro]: "primerec rec_conf (Suc (Suc (Suc 0)))"
-apply(simp add: rec_conf_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-apply(auto simp: numeral_4_eq_4)
+lemma primerec_rec_newconf[intro]: "primerec rec_newconf (Suc (Suc 0))"
+apply(simp add: rec_newconf_def)
+by(tactic {* resolve_tac @{context} [@{thm prime_cn},
+ @{thm prime_id}, @{thm prime_pr}] 1*};force)
+
+lemma primerec_rec_inpt[intro]: "0 < vl \<Longrightarrow> primerec (rec_inpt (Suc vl)) (Suc vl)"
+apply(simp add: rec_inpt_def)
+apply(tactic {* resolve_tac @{context} [@{thm prime_cn},
+ @{thm prime_id}, @{thm prime_pr}] 1*}; fastforce elim:primerec_rec_strt primerec_map_vl)
done
-lemma [intro]: "primerec rec_lg (Suc (Suc 0))"
-apply(simp add: rec_lg_def Let_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_nonstop (Suc (Suc (Suc 0)))"
-apply(simp add: rec_nonstop_def rec_NSTD_def rec_stat_def
+lemma primerec_rec_conf[intro]: "primerec rec_conf (Suc (Suc (Suc 0)))"
+apply(simp add: rec_conf_def)
+by(tactic {* resolve_tac @{context} [@{thm prime_cn},
+ @{thm prime_id}, @{thm prime_pr}] 1*};force simp: numeral)
+
+lemma primerec_recs2[intro]:
+ "primerec rec_lg (Suc (Suc 0))"
+ "primerec rec_nonstop (Suc (Suc (Suc 0)))"
+apply(simp_all add: rec_lg_def rec_nonstop_def rec_NSTD_def rec_stat_def
rec_lo_def Let_def rec_left_def rec_right_def rec_newconf_def
rec_newstat_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
+by(tactic {* resolve_tac @{context} [@{thm prime_cn},
+ @{thm prime_id}, @{thm prime_pr}] 1*};fastforce)+
lemma primerec_terminate:
"\<lbrakk>primerec f x; length xs = x\<rbrakk> \<Longrightarrow> terminate f xs"
@@ -3087,9 +3005,7 @@
and ind2: "\<And>xs. length xs = Suc (Suc n) \<Longrightarrow> terminate g xs"
and h: "primerec f n" " primerec g (Suc (Suc n))" " m = Suc n" "length (xs::nat list) = m"
have "\<forall>y<last xs. terminate g (butlast xs @ [y, rec_exec (Pr n f g) (butlast xs @ [y])])"
- using h
- apply(auto)
- by(rule_tac ind2, simp)
+ using h ind2 by(auto)
moreover have "terminate f (butlast xs)"
using ind1[of "butlast xs"] h
by simp
@@ -3128,20 +3044,12 @@
The correctness of @{text "rec_valu"}.
*}
lemma value_lemma: "rec_exec rec_valu [r] = valu r"
-apply(simp add: rec_exec.simps rec_valu_def lg_lemma)
-done
-
-lemma [intro]: "primerec rec_valu (Suc 0)"
-apply(simp add: rec_valu_def)
-apply(rule_tac k = "Suc (Suc 0)" in prime_cn)
-apply(auto simp: prime_s)
-proof -
- show "primerec rec_lg (Suc (Suc 0))" by auto
-next
- show "Suc (Suc 0) = Suc (Suc 0)" by simp
-next
- show "primerec (constn (Suc (Suc 0))) (Suc 0)" by auto
-qed
+ by(simp add: rec_exec.simps rec_valu_def lg_lemma)
+
+lemma primerec_rec_valu_1[intro]: "primerec rec_valu (Suc 0)"
+ unfolding rec_valu_def
+ apply(rule prime_cn[of _ "Suc (Suc 0)"])
+ by auto auto
declare valu.simps[simp del]
@@ -3153,14 +3061,14 @@
"rec_F = Cn (Suc (Suc 0)) rec_valu [Cn (Suc (Suc 0)) rec_right [Cn (Suc (Suc 0))
rec_conf ([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])]]"
-lemma get_fstn_args_nth:
+lemma get_fstn_args_nth[simp]:
"k < n \<Longrightarrow> (get_fstn_args m n ! k) = id m (k)"
apply(induct n, simp)
apply(case_tac "k = n", simp_all add: get_fstn_args.simps
nth_append)
done
-lemma [simp]:
+lemma get_fstn_args_is_id[simp]:
"\<lbrakk>ys \<noteq> [];
k < length ys\<rbrakk> \<Longrightarrow>
(get_fstn_args (length ys) (length ys) ! k) =
@@ -3268,9 +3176,9 @@
subsection {* Relating interperter functions to the execution of TMs *}
-lemma [simp]: "bl2wc [] = 0" by(simp add: bl2wc.simps bl2nat.simps)
-
-lemma [simp]: "\<lbrakk>fetch tp 0 b = (nact, ns)\<rbrakk> \<Longrightarrow> action_map nact = 4"
+lemma bl2wc_0[simp]: "bl2wc [] = 0" by(simp add: bl2wc.simps bl2nat.simps)
+
+lemma fetch_action_map_4[simp]: "\<lbrakk>fetch tp 0 b = (nact, ns)\<rbrakk> \<Longrightarrow> action_map nact = 4"
apply(simp add: fetch.simps)
done
@@ -3295,7 +3203,7 @@
declare godel_code.simps[simp del]
-lemma [simp]: "0 < godel_code' nl n"
+lemma godel_code'_nonzero[simp]: "0 < godel_code' nl n"
apply(induct nl arbitrary: n)
apply(auto simp: godel_code'.simps)
done
@@ -3308,14 +3216,14 @@
apply(auto simp: godel_code.simps)
done
-lemma [elim]:
+lemma godel_code_1_iff[elim]:
"\<lbrakk>i < length nl; \<not> Suc 0 < godel_code nl\<rbrakk> \<Longrightarrow> nl ! i = 0"
using godel_code_great[of nl] godel_code_eq_1[of nl]
apply(simp)
done
lemma prime_coprime: "\<lbrakk>Prime x; Prime y; x\<noteq>y\<rbrakk> \<Longrightarrow> coprime x y"
-proof(simp only: Prime.simps coprime_nat, auto simp: dvd_def,
+proof (simp only: Prime.simps coprime_def, auto simp: dvd_def,
rule_tac classical, simp)
fix d k ka
assume case_ka: "\<forall>u<d * ka. \<forall>v<d * ka. u * v \<noteq> d * ka"
@@ -3323,10 +3231,7 @@
and h: "(0::nat) < d" "d \<noteq> Suc 0" "Suc 0 < d * ka"
"ka \<noteq> k" "Suc 0 < d * k"
from h have "k > Suc 0 \<or> ka >Suc 0"
- apply(auto)
- apply(case_tac ka, simp, simp)
- apply(case_tac k, simp, simp)
- done
+ by (cases ka;cases k;force+)
from this show "False"
proof(erule_tac disjE)
assume "(Suc 0::nat) < k"
@@ -3402,7 +3307,7 @@
apply(simp)
done
-lemma [intro]: "Prime (Suc (Suc 0))"
+lemma prime_2[intro]: "Prime (Suc (Suc 0))"
apply(auto simp: Prime.simps)
apply(case_tac u, simp, case_tac nat, simp, simp)
done
@@ -3431,15 +3336,10 @@
done
lemma Pi_power_coprime: "i \<noteq> j \<Longrightarrow> coprime ((Pi i)^m) ((Pi j)^n)"
-by(rule_tac coprime_exp2_nat, erule_tac Pi_coprime)
+ unfolding coprime_power_right_iff coprime_power_left_iff using Pi_coprime by auto
lemma coprime_dvd_mult_nat2: "\<lbrakk>coprime (k::nat) n; k dvd n * m\<rbrakk> \<Longrightarrow> k dvd m"
-apply(erule_tac coprime_dvd_mult_nat)
-apply(simp add: dvd_def, auto)
-apply(rule_tac x = ka in exI)
-apply(subgoal_tac "n * m = m * n", simp)
-apply(simp add: nat_mult_commute)
-done
+ unfolding coprime_dvd_mult_right_iff.
declare godel_code'.simps[simp del]
@@ -3504,7 +3404,7 @@
lemma Pi_coprime_pre:
"length ps \<le> i \<Longrightarrow> coprime (Pi (Suc i)) (godel_code' ps (Suc 0))"
-proof(induct "length ps" arbitrary: ps, simp add: godel_code'.simps)
+proof(induct "length ps" arbitrary: ps)
fix x ps
assume ind:
"\<And>ps. \<lbrakk>x = length ps; length ps \<le> i\<rbrakk> \<Longrightarrow>
@@ -3518,20 +3418,19 @@
godel_code' (butlast ps) (Suc 0) * Pi (length ps)^(last ps)"
using godel_code'_butlast_last_id[of ps 0] h
by(case_tac ps, simp, simp)
- from g have
+ from g have "coprime (Pi (Suc i)) (Pi (length ps) ^ last ps)"
+ unfolding coprime_power_right_iff using Pi_coprime h(2) by auto
+ with g have
"coprime (Pi (Suc i)) (godel_code' (butlast ps) (Suc 0) *
Pi (length ps)^(last ps)) "
- proof(rule_tac coprime_mult_nat, simp)
- show "coprime (Pi (Suc i)) (Pi (length ps) ^ last ps)"
- apply(rule_tac coprime_exp_nat, rule prime_coprime, auto)
- using Pi_notEq[of "Suc i" "length ps"] h by simp
- qed
+ unfolding coprime_mult_right_iff coprime_power_right_iff by auto
+
from this and k show "coprime (Pi (Suc i)) (godel_code' ps (Suc 0))"
by simp
-qed
+qed (auto simp add: godel_code'.simps)
lemma Pi_coprime_suf: "i < j \<Longrightarrow> coprime (Pi i) (godel_code' ps j)"
-proof(induct "length ps" arbitrary: ps, simp add: godel_code'.simps)
+proof(induct "length ps" arbitrary: ps)
fix x ps
assume ind:
"\<And>ps. \<lbrakk>x = length ps; i < j\<rbrakk> \<Longrightarrow>
@@ -3547,13 +3446,11 @@
from g have
"coprime (Pi i) (godel_code' (butlast ps) j *
Pi (length ps + j - 1)^last ps)"
- apply(rule_tac coprime_mult_nat, simp)
- using Pi_power_coprime[of i "length ps + j - 1" 1 "last ps"] h
- apply(auto)
- done
+ using Pi_power_coprime[of i "length ps + j - 1" 1 "last ps"] h
+ by(auto)
from k and this show "coprime (Pi i) (godel_code' ps j)"
by auto
-qed
+qed (simp add: godel_code'.simps)
lemma godel_finite:
"finite {u. Pi (Suc i) ^ u dvd godel_code' nl (Suc 0)}"
@@ -3619,26 +3516,14 @@
assume mult_dvd:
"Pi (Suc i) ^ y dvd ?pref * Pi (Suc i) ^ nl ! i * ?suf'"
hence "Pi (Suc i) ^ y dvd ?pref * Pi (Suc i) ^ nl ! i"
- proof(rule_tac coprime_dvd_mult_nat)
- show "coprime (Pi (Suc i)^y) ?suf'"
- proof -
- have "coprime (Pi (Suc i) ^ y) (?suf'^(Suc 0))"
- apply(rule_tac coprime_exp2_nat)
- apply(rule_tac Pi_coprime_suf, simp)
- done
- thus "?thesis" by simp
- qed
+ proof -
+ have "coprime (Pi (Suc i)^y) ?suf'" by (simp add: Pi_coprime_suf)
+ thus ?thesis using coprime_dvd_mult_left_iff mult_dvd by blast
qed
hence "Pi (Suc i) ^ y dvd Pi (Suc i) ^ nl ! i"
proof(rule_tac coprime_dvd_mult_nat2)
- show "coprime (Pi (Suc i) ^ y) ?pref"
- proof -
- have "coprime (Pi (Suc i)^y) (?pref^Suc 0)"
- apply(rule_tac coprime_exp2_nat)
- apply(rule_tac Pi_coprime_pre, simp)
- done
- thus "?thesis" by simp
- qed
+ have "coprime (Pi (Suc i)^y) (?pref^Suc 0)" using Pi_coprime_pre by simp
+ thus "coprime (Pi (Suc i) ^ y) ?pref" by simp
qed
hence "Pi (Suc i) ^ y \<le> Pi (Suc i) ^ nl ! i "
apply(rule_tac dvd_imp_le, auto)
@@ -3654,7 +3539,7 @@
by(rule_tac godel_code_in, simp)
qed
-lemma [simp]:
+lemma godel_code'_set[simp]:
"{u. Pi (Suc i) ^ u dvd (Suc (Suc 0)) ^ length nl *
godel_code' nl (Suc 0)} =
{u. Pi (Suc i) ^ u dvd godel_code' nl (Suc 0)}"
@@ -3662,17 +3547,9 @@
apply(rule_tac n = " (Suc (Suc 0)) ^ length nl" in
coprime_dvd_mult_nat2)
proof -
- fix u
- show "coprime (Pi (Suc i) ^ u) ((Suc (Suc 0)) ^ length nl)"
- proof(rule_tac coprime_exp2_nat)
- have "Pi 0 = (2::nat)"
- apply(simp add: Pi.simps)
- done
- moreover have "coprime (Pi (Suc i)) (Pi 0)"
- apply(rule_tac Pi_coprime, simp)
- done
- ultimately show "coprime (Pi (Suc i)) (Suc (Suc 0))" by simp
- qed
+ have "Pi 0 = (2::nat)" by(simp add: Pi.simps)
+ show "coprime (Pi (Suc i) ^ u) ((Suc (Suc 0)) ^ length nl)" for u
+ using Pi_coprime Pi.simps(1) by force
qed
lemma godel_code_get_nth:
@@ -3680,10 +3557,6 @@
Max {u. Pi (Suc i) ^ u dvd godel_code nl} = nl ! i"
by(simp add: godel_code.simps godel_code'_get_nth)
-lemma "trpl l st r = godel_code' [l, st, r] 0"
-apply(simp add: trpl.simps godel_code'.simps)
-done
-
lemma mod_dvd_simp: "(x mod y = (0::nat)) = (y dvd x)"
by(simp add: dvd_def, auto)
@@ -3694,10 +3567,10 @@
done
-lemma [elim]: "Pi n = 0 \<Longrightarrow> RR"
+lemma Pi_nonzeroE[elim]: "Pi n = 0 \<Longrightarrow> RR"
using Pi_not_0[of n] by simp
-lemma [elim]: "Pi n = Suc 0 \<Longrightarrow> RR"
+lemma Pi_not_oneE[elim]: "Pi n = Suc 0 \<Longrightarrow> RR"
using Pi_gr_1[of n] by simp
lemma finite_power_dvd:
@@ -3725,15 +3598,9 @@
have "Pi m ^ y dvd Pi m ^ l"
proof -
have "Pi m ^ y dvd Pi m ^ l * Pi n ^ st"
- using h g
- apply(rule_tac n = "Pi k^r" in coprime_dvd_mult_nat)
- apply(rule Pi_power_coprime, simp, simp)
- done
- thus "Pi m^y dvd Pi m^l"
- apply(rule_tac n = " Pi n ^ st" in coprime_dvd_mult_nat)
- using g
- apply(rule_tac Pi_power_coprime, simp, simp)
- done
+ using h g Pi_power_coprime
+ by (simp add: coprime_dvd_mult_left_iff)
+ thus "Pi m^y dvd Pi m^l" using g Pi_power_coprime coprime_dvd_mult_left_iff by blast
qed
thus "y \<le> (l::nat)"
apply(rule_tac a = "Pi m" in power_le_imp_le_exp)
@@ -3751,7 +3618,7 @@
apply(case_tac "Pi m ^ l * Pi n ^ st * Pi k ^ r", auto)
done
-lemma [simp]: "left (trpl l st r) = l"
+lemma left_trpl_fst[simp]: "left (trpl l st r) = l"
apply(simp add: left.simps trpl.simps lo.simps loR.simps mod_dvd_simp)
apply(auto simp: conf_decode1)
apply(case_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r")
@@ -3759,7 +3626,7 @@
apply(erule_tac x = l in allE, auto)
done
-lemma [simp]: "stat (trpl l st r) = st"
+lemma stat_trpl_snd[simp]: "stat (trpl l st r) = st"
apply(simp add: stat.simps trpl.simps lo.simps
loR.simps mod_dvd_simp, auto)
apply(subgoal_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r
@@ -3770,7 +3637,7 @@
apply(erule_tac x = st in allE, auto)
done
-lemma [simp]: "rght (trpl l st r) = r"
+lemma rght_trpl_trd[simp]: "rght (trpl l st r) = r"
apply(simp add: rght.simps trpl.simps lo.simps
loR.simps mod_dvd_simp, auto)
apply(subgoal_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r
@@ -3938,7 +3805,7 @@
by simp
qed
-lemma [simp]: "fetch tp 0 b = (nact, ns) \<Longrightarrow> ns = 0"
+lemma fetch_zero_zero[simp]: "fetch tp 0 b = (nact, ns) \<Longrightarrow> ns = 0"
by(simp add: fetch.simps)
lemma Five_Suc: "5 = Suc 4" by simp
@@ -4029,11 +3896,11 @@
qed
-lemma [intro!]:
+lemma tpl_eqI[intro!]:
"\<lbrakk>a = a'; b = b'; c = c'\<rbrakk> \<Longrightarrow> trpl a b c = trpl a' b' c'"
by simp
-lemma [simp]: "bl2wc [Bk] = 0"
+lemma bl2wc_Bk[simp]: "bl2wc [Bk] = 0"
by(simp add: bl2wc.simps bl2nat.simps)
lemma bl2nat_double: "bl2nat xs (Suc n) = 2 * bl2nat xs n"
@@ -4058,45 +3925,17 @@
qed
-lemma [simp]: "2 * bl2wc (tl c) = bl2wc c - bl2wc c mod 2 "
-apply(case_tac c, simp, case_tac a)
-apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double)
-done
-
-lemma [simp]:
+lemma bl2wc_simps[simp]:
"bl2wc (Oc # tl c) = Suc (bl2wc c) - bl2wc c mod 2 "
-apply(case_tac c, case_tac [2] a, simp)
-apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double)
-done
-
-lemma [simp]: "bl2wc (Bk # c) = 2*bl2wc (c)"
-apply(simp add: bl2wc.simps bl2nat.simps bl2nat_double)
-done
-
-lemma [simp]: "bl2wc [Oc] = Suc 0"
- by(simp add: bl2wc.simps bl2nat.simps)
-
-lemma [simp]: "b \<noteq> [] \<Longrightarrow> bl2wc (tl b) = bl2wc b div 2"
-apply(case_tac b, simp, case_tac a)
-apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double)
-done
-
-lemma [simp]: "b \<noteq> [] \<Longrightarrow> bl2wc ([hd b]) = bl2wc b mod 2"
-apply(case_tac b, simp, case_tac a)
-apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double)
-done
-
-lemma [simp]: "\<lbrakk>b \<noteq> []\<rbrakk> \<Longrightarrow> bl2wc (hd b # c) = 2 * bl2wc c + bl2wc b mod 2"
-apply(case_tac b, simp, case_tac a)
-apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double)
-done
-
-lemma [simp]: " 2 * (bl2wc c div 2) = bl2wc c - bl2wc c mod 2"
- by(simp add: mult_div_cancel)
-
-lemma [simp]: "bl2wc (Oc # list) mod 2 = Suc 0"
- by(simp add: bl2wc.simps bl2nat.simps bl2nat_double)
-
+ "bl2wc (Bk # c) = 2*bl2wc (c)"
+ "2 * bl2wc (tl c) = bl2wc c - bl2wc c mod 2 "
+ "bl2wc [Oc] = Suc 0"
+ "c \<noteq> [] \<Longrightarrow> bl2wc (tl c) = bl2wc c div 2"
+ "c \<noteq> [] \<Longrightarrow> bl2wc [hd c] = bl2wc c mod 2"
+ "c \<noteq> [] \<Longrightarrow> bl2wc (hd c # d) = 2 * bl2wc d + bl2wc c mod 2"
+ "2 * (bl2wc c div 2) = bl2wc c - bl2wc c mod 2"
+ "bl2wc (Oc # list) mod 2 = Suc 0"
+ by(cases c;cases "hd c";force simp: bl2wc.simps bl2nat.simps bl2nat_double)+
declare code.simps[simp del]
declare nth_of.simps[simp del]
@@ -4136,21 +3975,15 @@
done
qed
-lemma [simp]: "bl2nat (Oc # Oc\<up>x) 0 = (2 * 2 ^ x - Suc 0)"
-apply(induct x)
-apply(simp add: bl2nat.simps)
-apply(simp add: bl2nat.simps bl2nat_double exp_ind)
-done
-
-lemma [simp]: "bl2nat (Oc\<up>y) 0 = 2^y - Suc 0"
+lemma bl2nat_simps[simp]: "bl2nat (Oc # Oc\<up>x) 0 = (2 * 2 ^ x - Suc 0)"
+ "bl2nat (Bk\<up>x) n = 0"
+ by(induct x;force simp: bl2nat.simps bl2nat_double exp_ind)+
+
+lemma bl2nat_exp_zero[simp]: "bl2nat (Oc\<up>y) 0 = 2^y - Suc 0"
apply(induct y, auto simp: bl2nat.simps bl2nat_double)
apply(case_tac "(2::nat)^y", auto)
done
-lemma [simp]: "bl2nat (Bk\<up>l) n = 0"
-apply(induct l, auto simp: bl2nat.simps bl2nat_double exp_ind)
-done
-
lemma bl2nat_cons_bk: "bl2nat (ks @ [Bk]) 0 = bl2nat ks 0"
apply(induct ks, auto simp: bl2nat.simps)
apply(case_tac a, auto simp: bl2nat.simps bl2nat_double)
@@ -4200,9 +4033,8 @@
lemma tape_of_nat_list_butlast_last:
"ys \<noteq> [] \<Longrightarrow> <ys @ [y]> = <ys> @ Bk # Oc\<up>Suc y"
apply(induct ys, simp, simp)
-apply(case_tac "ys = []", simp add: tape_of_nl_abv tape_of_nat_abv
- tape_of_nat_list.simps)
-apply(simp add: tape_of_nl_cons tape_of_nat_abv)
+apply(case_tac "ys = []", simp add: tape_of_list_def tape_of_nat_def)
+apply(simp add: tape_of_nl_cons tape_of_nat_def)
done
lemma listsum2_append:
@@ -4244,8 +4076,8 @@
thus "length (<xs @ [x]>) =
Suc (listsum2 (map Suc xs @ [Suc x]) (length xs) + x + length xs)"
apply(case_tac "xs = []")
- apply(simp add: tape_of_nl_abv listsum2.simps
- tape_of_nat_list.simps tape_of_nat_abv)
+ apply(simp add: tape_of_list_def listsum2.simps
+ tape_of_nat_list.simps tape_of_nat_def)
apply(simp add: tape_of_nat_list_butlast_last)
using listsum2_append[of "length xs" "map Suc xs" "[Suc x]"]
apply(simp)
@@ -4267,7 +4099,7 @@
apply(simp)
done
-lemma [simp]:
+lemma trpl_code_simp[simp]:
"trpl_code (steps0 (Suc 0, Bk\<up>l, <lm>) tp 0) =
rec_exec rec_conf [code tp, bl2wc (<lm>), 0]"
apply(simp add: steps.simps rec_exec.simps conf_lemma conf.simps
@@ -4354,12 +4186,12 @@
qed
qed
-lemma [simp]: "bl2wc (Bk\<up> m) = 0"
+lemma bl2wc_Bk_0[simp]: "bl2wc (Bk\<up> m) = 0"
apply(induct m)
apply(simp, simp)
done
-lemma [simp]: "bl2wc (Oc\<up> rs@Bk\<up> n) = bl2wc (Oc\<up> rs)"
+lemma bl2wc_Oc_then_Bk[simp]: "bl2wc (Oc\<up> rs@Bk\<up> n) = bl2wc (Oc\<up> rs)"
apply(induct rs, simp,
simp add: bl2wc.simps bl2nat.simps bl2nat_double)
done
@@ -4438,10 +4270,10 @@
qed
qed
-lemma [simp]: "actn m 0 r = 4"
+lemma actn_0_is_4[simp]: "actn m 0 r = 4"
by(simp add: actn.simps)
-lemma [simp]: "newstat m 0 r = 0"
+lemma newstat_0_0[simp]: "newstat m 0 r = 0"
by(simp add: newstat.simps)
declare step_red[simp del]
@@ -4536,7 +4368,7 @@
apply(auto)
done
-lemma [elim]: "x > Suc 0 \<Longrightarrow> Max {u. x ^ u dvd x ^ r} = r"
+lemma max_divisors: "x > Suc 0 \<Longrightarrow> Max {u. x ^ u dvd x ^ r} = r"
proof(rule_tac Max_eqI)
assume "x > Suc 0"
thus "finite {u. x ^ u dvd x ^ r}"
@@ -4555,10 +4387,16 @@
show "r \<in> {u. x ^ u dvd x ^ r}" by simp
qed
-lemma lo_power: "x > Suc 0 \<Longrightarrow> lo (x ^ r) x = r"
-apply(auto simp: lo.simps loR.simps mod_dvd_simp)
-apply(case_tac "x^r", simp_all)
-done
+lemma lo_power:
+ assumes "x > Suc 0" shows "lo (x ^ r) x = r"
+proof -
+ have "\<not> Suc 0 < x ^ r \<Longrightarrow> r = 0" using assms
+ by (metis Suc_lessD Suc_lessI nat_power_eq_Suc_0_iff zero_less_power)
+ moreover have "\<forall>xa. \<not> x ^ xa dvd x ^ r \<Longrightarrow> r = 0"
+ using dvd_refl assms by(cases "x^r";blast)
+ ultimately show ?thesis using assms
+ by(auto simp: lo.simps loR.simps mod_dvd_simp elim:max_divisors)
+qed
lemma lo_rgt: "lo (trpl 0 0 r) (Pi 2) = r"
apply(simp add: trpl.simps lo_power)
--- a/thys/UTM.thy Wed Jan 14 09:08:51 2015 +0000
+++ b/thys/UTM.thy Wed Dec 19 16:10:58 2018 +0100
@@ -2,10 +2,10 @@
Author: Jian Xu, Xingyuan Zhang, and Christian Urban
*)
-header {* Construction of a Universal Turing Machine *}
+chapter {* Construction of a Universal Turing Machine *}
theory UTM
-imports Recursive Abacus UF GCD Turing_Hoare
+imports Recursive Abacus UF HOL.GCD Turing_Hoare
begin
section {* Wang coding of input arguments *}
@@ -684,23 +684,6 @@
declare wcode_backto_standard_pos.simps[simp del]
-lemma [simp]: "<0::nat> = [Oc]"
-apply(simp add: tape_of_nat_abv tape_of_nat_list.simps)
-done
-
-lemma tape_of_Suc_nat: "<Suc (a ::nat)> = replicate a Oc @ [Oc, Oc]"
-apply(simp only: tape_of_nat_abv exp_ind, simp)
-done
-
-lemma [simp]: "length (<a::nat>) = Suc a"
-apply(simp add: tape_of_nat_abv tape_of_nat_list.simps)
-done
-
-lemma [simp]: "<[a::nat]> = <a>"
-apply(simp add: tape_of_nat_abv tape_of_nl_abv
- tape_of_nat_list.simps)
-done
-
lemma bin_wc_eq: "bl_bin xs = bl2wc xs"
proof(induct xs)
show " bl_bin [] = bl2wc []"
@@ -715,16 +698,6 @@
done
qed
-lemma bl_bin_nat_Suc:
- "bl_bin (<Suc a>) = bl_bin (<a>) + 2^(Suc a)"
-apply(simp add: tape_of_nat_abv bl_bin.simps)
-apply(induct a, auto simp: bl_bin.simps)
-done
-
-lemma [simp]: " rev (a\<up>(aa)) = a\<up>(aa)"
-apply(simp)
-done
-
lemma tape_of_nl_append_one: "lm \<noteq> [] \<Longrightarrow> <lm @ [a]> = <lm> @ Bk # Oc\<up>Suc a"
apply(induct lm, auto simp: tape_of_nl_cons split:if_splits)
done
@@ -735,12 +708,11 @@
apply(simp add: exp_ind[THEN sym])
done
-lemma [simp]: "a\<up>(Suc 0) = [a]"
+lemma exp_1[simp]: "a\<up>(Suc 0) = [a]"
by(simp)
lemma tape_of_nl_cons_app1: "(<a # xs @ [b]>) = (Oc\<up>(Suc a) @ Bk # (<xs@ [b]>))"
-apply(case_tac xs, simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
-apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
+apply(case_tac xs; simp add: tape_of_list_def tape_of_nat_list.simps tape_of_nat_def)
done
lemma bl_bin_bk_oc[simp]:
@@ -752,18 +724,17 @@
done
lemma tape_of_nat[simp]: "(<a::nat>) = Oc\<up>(Suc a)"
-apply(simp add: tape_of_nat_abv)
+apply(simp add: tape_of_nat_def)
done
lemma tape_of_nl_cons_app2: "(<c # xs @ [b]>) = (<c # xs> @ Bk # Oc\<up>(Suc b))"
-proof(induct "length xs" arbitrary: xs c,
- simp add: tape_of_nl_abv tape_of_nat_list.simps)
+proof(induct "length xs" arbitrary: xs c, simp add: tape_of_list_def)
fix x xs c
assume ind: "\<And>xs c. x = length xs \<Longrightarrow> <c # xs @ [b]> =
<c # xs> @ Bk # Oc\<up>(Suc b)"
and h: "Suc x = length (xs::nat list)"
show "<c # xs @ [b]> = <c # xs> @ Bk # Oc\<up>(Suc b)"
- proof(case_tac xs, simp add: tape_of_nl_abv tape_of_nat_list.simps)
+ proof(case_tac xs, simp add: tape_of_list_def tape_of_nat_list.simps)
fix a list
assume g: "xs = a # list"
hence k: "<a # list @ [b]> = <a # list> @ Bk # Oc\<up>(Suc b)"
@@ -772,16 +743,16 @@
apply(simp)
done
from g and k show "<c # xs @ [b]> = <c # xs> @ Bk # Oc\<up>(Suc b)"
- apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)
+ apply(simp add: tape_of_list_def tape_of_nat_list.simps)
done
qed
qed
-lemma [simp]: "length (<aa # a # list>) = Suc (Suc aa) + length (<a # list>)"
-apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)
+lemma length_2_elems[simp]: "length (<aa # a # list>) = Suc (Suc aa) + length (<a # list>)"
+apply(simp add: tape_of_list_def tape_of_nat_list.simps)
done
-lemma [simp]: "bl_bin (Oc\<up>(Suc aa) @ Bk # tape_of_nat_list (a # lista) @ [Bk, Oc]) =
+lemma bl_bin_addition[simp]: "bl_bin (Oc\<up>(Suc aa) @ Bk # tape_of_nat_list (a # lista) @ [Bk, Oc]) =
bl_bin (Oc\<up>(Suc aa) @ Bk # tape_of_nat_list (a # lista)) +
2* 2^(length (Oc\<up>(Suc aa) @ Bk # tape_of_nat_list (a # lista)))"
using bl_bin_bk_oc[of "Oc\<up>(Suc aa) @ Bk # tape_of_nat_list (a # lista)"]
@@ -790,23 +761,22 @@
declare replicate_Suc[simp del]
-lemma [simp]:
+lemma bl_bin_2[simp]:
"bl_bin (<aa # list>) + (4 * rs + 4) * 2 ^ (length (<aa # list>) - Suc 0)
= bl_bin (Oc\<up>(Suc aa) @ Bk # <list @ [0]>) + rs * (2 * 2 ^ (aa + length (<list @ [0]>)))"
-
apply(case_tac "list", simp add: add_mult_distrib)
apply(simp add: tape_of_nl_cons_app2 add_mult_distrib)
-apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)
+apply(simp add: tape_of_list_def tape_of_nat_list.simps)
done
lemma tape_of_nl_app_Suc: "((<list @ [Suc ab]>)) = (<list @ [ab]>) @ [Oc]"
apply(induct list)
-apply(simp add: tape_of_nl_abv tape_of_nat_list.simps exp_ind)
+apply(simp add: tape_of_list_def tape_of_nat_list.simps exp_ind)
apply(case_tac list)
-apply(simp_all add:tape_of_nl_abv tape_of_nat_list.simps exp_ind)
+apply(simp_all add:tape_of_list_def tape_of_nat_list.simps exp_ind)
done
-lemma [simp]: "bl_bin (Oc # Oc\<up>(aa) @ Bk # <list @ [ab]> @ [Oc])
+lemma bl_bin_3[simp]: "bl_bin (Oc # Oc\<up>(aa) @ Bk # <list @ [ab]> @ [Oc])
= bl_bin (Oc # Oc\<up>(aa) @ Bk # <list @ [ab]>) +
2^(length (Oc # Oc\<up>(aa) @ Bk # <list @ [ab]>))"
apply(simp add: bin_wc_eq)
@@ -814,7 +784,7 @@
using bl2nat_cons_oc[of "Oc # Oc\<up>(aa) @ Bk # <list @ [ab]>"]
apply(simp)
done
-lemma [simp]: "bl_bin (Oc # Oc\<up>(aa) @ Bk # <list @ [ab]>) + (4 * 2 ^ (aa + length (<list @ [ab]>)) +
+lemma bl_bin_4[simp]: "bl_bin (Oc # Oc\<up>(aa) @ Bk # <list @ [ab]>) + (4 * 2 ^ (aa + length (<list @ [ab]>)) +
4 * (rs * 2 ^ (aa + length (<list @ [ab]>)))) =
bl_bin (Oc # Oc\<up>(aa) @ Bk # <list @ [Suc ab]>) +
rs * (2 * 2 ^ (aa + length (<list @ [Suc ab]>)))"
@@ -863,82 +833,37 @@
definition wcode_double_case_le :: "(config \<times> config) set"
where "wcode_double_case_le \<equiv> (inv_image lex_pair wcode_double_case_measure)"
-lemma [intro]: "wf lex_pair"
+lemma wf_lex_pair[intro]: "wf lex_pair"
by(auto intro:wf_lex_prod simp:lex_pair_def)
lemma wf_wcode_double_case_le[intro]: "wf wcode_double_case_le"
by(auto intro:wf_inv_image simp: wcode_double_case_le_def )
-lemma [simp]: "fetch t_wcode_main (Suc 0) Bk = (L, Suc 0)"
-apply(simp add: t_wcode_main_def t_wcode_main_first_part_def
- fetch.simps nth_of.simps)
-done
-
-lemma [simp]: "fetch t_wcode_main (Suc 0) Oc = (L, Suc (Suc 0))"
-apply(simp add: t_wcode_main_def t_wcode_main_first_part_def
- fetch.simps nth_of.simps)
-done
-
-lemma [simp]: "fetch t_wcode_main (Suc (Suc 0)) Oc = (R, 3)"
-apply(simp add: t_wcode_main_def t_wcode_main_first_part_def
- fetch.simps nth_of.simps)
-done
-
-lemma [simp]: "fetch t_wcode_main (Suc (Suc (Suc 0))) Bk = (R, 4)"
-apply(simp add: t_wcode_main_def t_wcode_main_first_part_def
- fetch.simps nth_of.simps)
-done
-
-lemma [simp]: "fetch t_wcode_main (Suc (Suc (Suc 0))) Oc = (W0, 3)"
-apply(simp add: t_wcode_main_def t_wcode_main_first_part_def
- fetch.simps nth_of.simps)
-done
-
-lemma [simp]: "fetch t_wcode_main 4 Bk = (R, 4)"
-apply(subgoal_tac "4 = Suc 3")
-apply(simp only: t_wcode_main_def t_wcode_main_first_part_def
- fetch.simps nth_of.simps, auto)
-done
-
-lemma [simp]: "fetch t_wcode_main 4 Oc = (R, 5)"
-apply(subgoal_tac "4 = Suc 3")
-apply(simp only: t_wcode_main_def t_wcode_main_first_part_def
- fetch.simps nth_of.simps, auto)
-done
-
-lemma [simp]: "fetch t_wcode_main 5 Oc = (R, 5)"
-apply(subgoal_tac "5 = Suc 4")
-apply(simp only: t_wcode_main_def t_wcode_main_first_part_def
- fetch.simps nth_of.simps, auto)
-done
-
-lemma [simp]: "fetch t_wcode_main 5 Bk = (W1, 6)"
-apply(subgoal_tac "5 = Suc 4")
-apply(simp only: t_wcode_main_def t_wcode_main_first_part_def
- fetch.simps nth_of.simps, auto)
-done
-
-lemma [simp]: "fetch t_wcode_main 6 Bk = (R, 13)"
-apply(subgoal_tac "6 = Suc 5")
-apply(simp only: t_wcode_main_def t_wcode_main_first_part_def
- fetch.simps nth_of.simps, auto)
-done
-
-lemma [simp]: "fetch t_wcode_main 6 Oc = (L, 6)"
-apply(subgoal_tac "6 = Suc 5")
-apply(simp only: t_wcode_main_def t_wcode_main_first_part_def
- fetch.simps nth_of.simps, auto)
-done
-
-lemma [elim]: "Bk\<up>(mr) = [] \<Longrightarrow> mr = 0"
-apply(case_tac mr, auto)
-done
-
-lemma [simp]: "wcode_on_left_moving_1 ires rs (b, []) = False"
-apply(simp add: wcode_on_left_moving_1.simps wcode_on_left_moving_1_B.simps
- wcode_on_left_moving_1_O.simps)
-done
-
+lemma fetch_t_wcode_main[simp]:
+ "fetch t_wcode_main (Suc 0) Bk = (L, Suc 0)"
+ "fetch t_wcode_main (Suc 0) Oc = (L, Suc (Suc 0))"
+ "fetch t_wcode_main (Suc (Suc 0)) Oc = (R, 3)"
+ "fetch t_wcode_main (Suc (Suc 0)) Bk = (L, 7)"
+ "fetch t_wcode_main (Suc (Suc (Suc 0))) Bk = (R, 4)"
+ "fetch t_wcode_main (Suc (Suc (Suc 0))) Oc = (W0, 3)"
+ "fetch t_wcode_main 4 Bk = (R, 4)"
+ "fetch t_wcode_main 4 Oc = (R, 5)"
+ "fetch t_wcode_main 5 Oc = (R, 5)"
+ "fetch t_wcode_main 5 Bk = (W1, 6)"
+ "fetch t_wcode_main 6 Bk = (R, 13)"
+ "fetch t_wcode_main 6 Oc = (L, 6)"
+ "fetch t_wcode_main 7 Oc = (R, 8)"
+ "fetch t_wcode_main 7 Bk = (R, 0)"
+ "fetch t_wcode_main 8 Bk = (R, 9)"
+ "fetch t_wcode_main 9 Bk = (R, 10)"
+ "fetch t_wcode_main 9 Oc = (W0, 9)"
+ "fetch t_wcode_main 10 Bk = (R, 10)"
+ "fetch t_wcode_main 10 Oc = (R, 11)"
+ "fetch t_wcode_main 11 Bk = (W1, 12)"
+ "fetch t_wcode_main 11 Oc = (R, 11)"
+ "fetch t_wcode_main 12 Oc = (L, 12)"
+ "fetch t_wcode_main 12 Bk = (R, t_twice_len + 14)"
+by(auto simp: t_wcode_main_def t_wcode_main_first_part_def fetch.simps numeral)
declare wcode_on_checking_1.simps[simp del]
@@ -949,12 +874,13 @@
wcode_goon_right_moving_1.simps wcode_backto_standard_pos.simps
-lemma [simp]: "wcode_on_left_moving_1 ires rs (b, r) \<Longrightarrow> b \<noteq> []"
-apply(simp add: wcode_double_case_inv_simps, auto)
-done
-
-
-lemma [elim]: "\<lbrakk>wcode_on_left_moving_1 ires rs (b, Bk # list);
+lemma wcode_on_left_moving_1[simp]:
+ "wcode_on_left_moving_1 ires rs (b, []) = False"
+ "wcode_on_left_moving_1 ires rs (b, r) \<Longrightarrow> b \<noteq> []"
+by(auto simp: wcode_on_left_moving_1.simps wcode_on_left_moving_1_B.simps
+ wcode_on_left_moving_1_O.simps)
+
+lemma wcode_on_left_moving_1E[elim]: "\<lbrakk>wcode_on_left_moving_1 ires rs (b, Bk # list);
tl b = aa \<and> hd b # Bk # list = ba\<rbrakk> \<Longrightarrow>
wcode_on_left_moving_1 ires rs (aa, ba)"
apply(simp only: wcode_on_left_moving_1.simps wcode_on_left_moving_1_O.simps
@@ -973,7 +899,7 @@
declare replicate_Suc[simp]
-lemma [elim]:
+lemma wcode_on_moving_1_Elim[elim]:
"\<lbrakk>wcode_on_left_moving_1 ires rs (b, Oc # list); tl b = aa \<and> hd b # Oc # list = ba\<rbrakk>
\<Longrightarrow> wcode_on_checking_1 ires rs (aa, ba)"
apply(simp only: wcode_double_case_inv_simps)
@@ -982,43 +908,28 @@
apply(case_tac mr, simp, auto)
done
-lemma [simp]: "wcode_on_checking_1 ires rs (b, []) = False"
-apply(auto simp: wcode_double_case_inv_simps)
-done
-
-lemma [simp]: "wcode_on_checking_1 ires rs (b, Bk # list) = False"
-apply(auto simp: wcode_double_case_inv_simps)
-done
-
-lemma [elim]: "\<lbrakk>wcode_on_checking_1 ires rs (b, Oc # ba);Oc # b = aa \<and> list = ba\<rbrakk>
+lemma wcode_on_checking_1_Elim[elim]: "\<lbrakk>wcode_on_checking_1 ires rs (b, Oc # ba);Oc # b = aa \<and> list = ba\<rbrakk>
\<Longrightarrow> wcode_erase1 ires rs (aa, ba)"
apply(simp only: wcode_double_case_inv_simps)
apply(erule_tac exE)+
apply(rule_tac x = ln in exI, rule_tac x = rn in exI, simp)
done
-
-lemma [simp]: "wcode_on_checking_1 ires rs (b, []) = False"
-apply(simp add: wcode_double_case_inv_simps)
-done
-
-lemma [simp]: "wcode_on_checking_1 ires rs ([], Bk # list) = False"
+lemma wcode_on_checking_1_simp[simp]:
+ "wcode_on_checking_1 ires rs (b, []) = False"
+ "wcode_on_checking_1 ires rs (b, Bk # list) = False"
+by(auto simp: wcode_double_case_inv_simps)
+
+lemma wcode_erase1_nonempty_snd[simp]: "wcode_erase1 ires rs (b, []) = False"
apply(simp add: wcode_double_case_inv_simps)
done
-lemma [simp]: "wcode_erase1 ires rs (b, []) = False"
-apply(simp add: wcode_double_case_inv_simps)
-done
-
-lemma [simp]: "wcode_on_right_moving_1 ires rs (b, []) = False"
+lemma wcode_on_right_moving_1_nonempty_snd[simp]: "wcode_on_right_moving_1 ires rs (b, []) = False"
apply(simp add: wcode_double_case_inv_simps)
done
-lemma [simp]: "wcode_on_right_moving_1 ires rs (b, []) = False"
-apply(simp add: wcode_double_case_inv_simps)
-done
-
-lemma [elim]: "\<lbrakk>wcode_on_right_moving_1 ires rs (b, Bk # ba); Bk # b = aa \<and> list = b\<rbrakk> \<Longrightarrow>
+lemma wcode_on_right_moving_1_BkE[elim]:
+ "\<lbrakk>wcode_on_right_moving_1 ires rs (b, Bk # ba); Bk # b = aa \<and> list = b\<rbrakk> \<Longrightarrow>
wcode_on_right_moving_1 ires rs (aa, ba)"
apply(simp only: wcode_double_case_inv_simps)
apply(erule_tac exE)+
@@ -1028,7 +939,7 @@
apply(case_tac mr, simp, simp)
done
-lemma [elim]:
+lemma wcode_on_right_moving_1_OcE[elim]:
"\<lbrakk>wcode_on_right_moving_1 ires rs (b, Oc # ba); Oc # b = aa \<and> list = ba\<rbrakk>
\<Longrightarrow> wcode_goon_right_moving_1 ires rs (aa, ba)"
apply(simp only: wcode_double_case_inv_simps)
@@ -1039,12 +950,7 @@
apply(case_tac ml, simp, case_tac nat, simp, simp)
done
-lemma [simp]:
- "wcode_on_right_moving_1 ires rs (b, []) \<Longrightarrow> False"
-apply(simp add: wcode_double_case_inv_simps)
-done
-
-lemma [elim]: "\<lbrakk>wcode_erase1 ires rs (b, Bk # ba); Bk # b = aa \<and> list = ba; c = Bk # ba\<rbrakk>
+lemma wcode_erase1_BkE[elim]: "\<lbrakk>wcode_erase1 ires rs (b, Bk # ba); Bk # b = aa \<and> list = ba; c = Bk # ba\<rbrakk>
\<Longrightarrow> wcode_on_right_moving_1 ires rs (aa, ba)"
apply(simp only: wcode_double_case_inv_simps)
apply(erule_tac exE)+
@@ -1052,14 +958,14 @@
rule_tac x = rn in exI, simp add: exp_ind del: replicate_Suc)
done
-lemma [elim]: "\<lbrakk>wcode_erase1 ires rs (aa, Oc # list); b = aa \<and> Bk # list = ba\<rbrakk> \<Longrightarrow>
+lemma wcode_erase1_OcE[elim]: "\<lbrakk>wcode_erase1 ires rs (aa, Oc # list); b = aa \<and> Bk # list = ba\<rbrakk> \<Longrightarrow>
wcode_erase1 ires rs (aa, ba)"
apply(simp only: wcode_double_case_inv_simps)
apply(erule_tac exE)+
apply(rule_tac x = ln in exI, rule_tac x = rn in exI, auto)
done
-lemma [elim]: "\<lbrakk>wcode_goon_right_moving_1 ires rs (aa, []); b = aa \<and> [Oc] = ba\<rbrakk>
+lemma wcode_goon_right_moving_1_emptyE[elim]: "\<lbrakk>wcode_goon_right_moving_1 ires rs (aa, []); b = aa \<and> [Oc] = ba\<rbrakk>
\<Longrightarrow> wcode_backto_standard_pos ires rs (aa, ba)"
apply(simp only: wcode_double_case_inv_simps)
apply(erule_tac exE)+
@@ -1069,7 +975,7 @@
rule_tac x = rn in exI, simp)
done
-lemma [elim]:
+lemma wcode_goon_right_moving_1_BkE[elim]:
"\<lbrakk>wcode_goon_right_moving_1 ires rs (aa, Bk # list); b = aa \<and> Oc # list = ba\<rbrakk>
\<Longrightarrow> wcode_backto_standard_pos ires rs (aa, ba)"
apply(simp only: wcode_double_case_inv_simps)
@@ -1081,7 +987,7 @@
apply(case_tac mr, simp, case_tac rn, simp, simp_all)
done
-lemma [elim]: "\<lbrakk>wcode_goon_right_moving_1 ires rs (b, Oc # ba); Oc # b = aa \<and> list = ba\<rbrakk>
+lemma wcode_goon_right_moving_1_OcE[elim]: "\<lbrakk>wcode_goon_right_moving_1 ires rs (b, Oc # ba); Oc # b = aa \<and> list = ba\<rbrakk>
\<Longrightarrow> wcode_goon_right_moving_1 ires rs (aa, ba)"
apply(simp only: wcode_double_case_inv_simps)
apply(erule_tac exE)+
@@ -1091,12 +997,8 @@
apply(case_tac mr, simp, case_tac rn, simp_all)
done
-lemma [elim]: "\<lbrakk>wcode_backto_standard_pos ires rs (b, []); Bk # b = aa\<rbrakk> \<Longrightarrow> False"
-apply(auto simp: wcode_double_case_inv_simps wcode_backto_standard_pos_O.simps
- wcode_backto_standard_pos_B.simps)
-done
-
-lemma [elim]: "\<lbrakk>wcode_backto_standard_pos ires rs (b, Bk # ba); Bk # b = aa \<and> list = ba\<rbrakk>
+
+lemma wcode_backto_standard_pos_BkE[elim]: "\<lbrakk>wcode_backto_standard_pos ires rs (b, Bk # ba); Bk # b = aa \<and> list = ba\<rbrakk>
\<Longrightarrow> wcode_before_double ires rs (aa, ba)"
apply(simp only: wcode_double_case_inv_simps wcode_backto_standard_pos_B.simps
wcode_backto_standard_pos_O.simps wcode_before_double.simps)
@@ -1107,17 +1009,17 @@
apply(case_tac [!] mr, simp_all)
done
-lemma [simp]: "wcode_backto_standard_pos ires rs ([], Oc # list) = False"
+lemma wcode_backto_standard_pos_no_Oc[simp]: "wcode_backto_standard_pos ires rs ([], Oc # list) = False"
apply(auto simp: wcode_backto_standard_pos.simps wcode_backto_standard_pos_B.simps
wcode_backto_standard_pos_O.simps)
done
-lemma [simp]: "wcode_backto_standard_pos ires rs (b, []) = False"
+lemma wcode_backto_standard_pos_nonempty_snd[simp]: "wcode_backto_standard_pos ires rs (b, []) = False"
apply(auto simp: wcode_backto_standard_pos.simps wcode_backto_standard_pos_B.simps
wcode_backto_standard_pos_O.simps)
done
-lemma [elim]: "\<lbrakk>wcode_backto_standard_pos ires rs (b, Oc # list); tl b = aa; hd b # Oc # list = ba\<rbrakk>
+lemma wcode_backto_standard_pos_OcE[elim]: "\<lbrakk>wcode_backto_standard_pos ires rs (b, Oc # list); tl b = aa; hd b # Oc # list = ba\<rbrakk>
\<Longrightarrow> wcode_backto_standard_pos ires rs (aa, ba)"
apply(simp only: wcode_backto_standard_pos.simps wcode_backto_standard_pos_B.simps
wcode_backto_standard_pos_O.simps)
@@ -1210,10 +1112,6 @@
by simp
qed
-lemma t_twice_len_ge: "Suc 0 \<le> length t_twice div 2"
-apply(simp add: t_twice_def mopup.simps t_twice_compile_def)
-done
-
declare start_of.simps[simp del]
lemma twice_lemma: "rec_exec rec_twice [rs] = 2*rs"
@@ -1242,7 +1140,7 @@
by(simp add: abc_twice_def)
qed
thus "?thesis"
- apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv rec_exec.simps twice_lemma)
+ apply(simp add: tape_of_list_def tape_of_nat_def rec_exec.simps twice_lemma)
done
qed
@@ -1368,7 +1266,7 @@
declare tm_wf.simps[simp del]
-lemma [simp]: " tm_wf (t_twice_compile, 0)"
+lemma tm_wf_t_twice_compile [simp]: "tm_wf (t_twice_compile, 0)"
apply(simp only: t_twice_compile_def)
apply(rule_tac wf_tm_from_abacus, simp)
done
@@ -1399,7 +1297,7 @@
by metis
qed
-lemma [intro]: "length t_wcode_main_first_part mod 2 = 0"
+lemma length_t_wcode_main_first_part_even[intro]: "length t_wcode_main_first_part mod 2 = 0"
apply(auto simp: t_wcode_main_first_part_def)
done
@@ -1428,10 +1326,9 @@
done
lemma mopup_mod2: "length (mopup k) mod 2 = 0"
-apply(auto simp: mopup.simps)
-by arith
-
-lemma [simp]: "fetch t_wcode_main (Suc (t_twice_len + length t_wcode_main_first_part div 2)) Oc
+ by(auto simp: mopup.simps)
+
+lemma fetch_t_wcode_main_Oc[simp]: "fetch t_wcode_main (Suc (t_twice_len + length t_wcode_main_first_part div 2)) Oc
= (L, Suc 0)"
apply(subgoal_tac "length (t_twice) mod 2 = 0")
apply(simp add: t_wcode_main_def nth_append fetch.simps t_wcode_main_first_part_def
@@ -1452,7 +1349,7 @@
apply(simp add: exp_ind[THEN sym])
done
-lemma wcode_main_first_part_len:
+lemma wcode_main_first_part_len[simp]:
"length t_wcode_main_first_part = 24"
apply(simp add: t_wcode_main_first_part_def)
done
@@ -1659,117 +1556,21 @@
where "wcode_fourtimes_case_le \<equiv> (inv_image lex_pair wcode_fourtimes_case_measure)"
lemma wf_wcode_fourtimes_case_le[intro]: "wf wcode_fourtimes_case_le"
-by(auto intro:wf_inv_image simp: wcode_fourtimes_case_le_def)
-
-lemma [simp]: "fetch t_wcode_main (Suc (Suc 0)) Bk = (L, 7)"
-apply(simp add: t_wcode_main_def fetch.simps
- t_wcode_main_first_part_def nth_of.simps)
-done
-
-lemma [simp]: "fetch t_wcode_main 7 Oc = (R, 8)"
-apply(subgoal_tac "7 = Suc 6")
-apply(simp only: t_wcode_main_def fetch.simps
- t_wcode_main_first_part_def nth_of.simps)
-apply(auto)
-done
-
-lemma [simp]: "fetch t_wcode_main 8 Bk = (R, 9)"
-apply(subgoal_tac "8 = Suc 7")
-apply(simp only: t_wcode_main_def fetch.simps
- t_wcode_main_first_part_def nth_of.simps)
-apply(auto)
-done
-
-
-lemma [simp]: "fetch t_wcode_main 9 Bk = (R, 10)"
-apply(subgoal_tac "9 = Suc 8")
-apply(simp only: t_wcode_main_def fetch.simps
- t_wcode_main_first_part_def nth_of.simps)
-apply(auto)
-done
-
-lemma [simp]: "fetch t_wcode_main 9 Oc = (W0, 9)"
-apply(subgoal_tac "9 = Suc 8")
-apply(simp only: t_wcode_main_def fetch.simps
- t_wcode_main_first_part_def nth_of.simps)
-apply(auto)
-done
-
-lemma [simp]: "fetch t_wcode_main 10 Bk = (R, 10)"
-apply(subgoal_tac "10 = Suc 9")
-apply(simp only: t_wcode_main_def fetch.simps
- t_wcode_main_first_part_def nth_of.simps)
-apply(auto)
-done
-
-lemma [simp]: "fetch t_wcode_main 10 Oc = (R, 11)"
-apply(subgoal_tac "10 = Suc 9")
-apply(simp only: t_wcode_main_def fetch.simps
- t_wcode_main_first_part_def nth_of.simps)
-apply(auto)
-done
-
-lemma [simp]: "fetch t_wcode_main 11 Bk = (W1, 12)"
-apply(subgoal_tac "11 = Suc 10")
-apply(simp only: t_wcode_main_def fetch.simps
- t_wcode_main_first_part_def nth_of.simps)
-apply(auto)
-done
-
-lemma [simp]: "fetch t_wcode_main 11 Oc = (R, 11)"
-apply(subgoal_tac "11 = Suc 10")
-apply(simp only: t_wcode_main_def fetch.simps
- t_wcode_main_first_part_def nth_of.simps)
-apply(auto)
-done
-
-lemma [simp]: "fetch t_wcode_main 12 Oc = (L, 12)"
-apply(subgoal_tac "12 = Suc 11")
-apply(simp only: t_wcode_main_def fetch.simps
- t_wcode_main_first_part_def nth_of.simps)
-apply(auto)
-done
-
-lemma [simp]: "fetch t_wcode_main 12 Bk = (R, t_twice_len + 14)"
-apply(subgoal_tac "12 = Suc 11")
-apply(simp only: t_wcode_main_def fetch.simps
- t_wcode_main_first_part_def nth_of.simps)
-apply(auto)
-done
-
-lemma [simp]: "wcode_on_left_moving_2 ires rs (b, []) = False"
-apply(auto simp: wcode_fourtimes_invs)
-done
-
-lemma [simp]: "wcode_on_checking_2 ires rs (b, []) = False"
-apply(auto simp: wcode_fourtimes_invs)
-done
-
-lemma [simp]: "wcode_goon_checking ires rs (b, []) = False"
-apply(auto simp: wcode_fourtimes_invs)
-done
-
-lemma [simp]: "wcode_right_move ires rs (b, []) = False"
-apply(auto simp: wcode_fourtimes_invs)
-done
-
-lemma [simp]: "wcode_erase2 ires rs (b, []) = False"
-apply(auto simp: wcode_fourtimes_invs)
-done
-
-lemma [simp]: "wcode_on_right_moving_2 ires rs (b, []) = False"
-apply(auto simp: wcode_fourtimes_invs)
-done
-
-lemma [simp]: "wcode_backto_standard_pos_2 ires rs (b, []) = False"
-apply(auto simp: wcode_fourtimes_invs)
-done
-
-lemma [simp]: "wcode_on_left_moving_2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
-apply(simp add: wcode_fourtimes_invs, auto)
-done
-
-lemma [simp]: "wcode_on_left_moving_2 ires rs (b, Bk # list) \<Longrightarrow> wcode_on_left_moving_2 ires rs (tl b, hd b # Bk # list)"
+by(auto simp: wcode_fourtimes_case_le_def)
+
+lemma nonempty_snd [simp]:
+ "wcode_on_left_moving_2 ires rs (b, []) = False"
+ "wcode_on_checking_2 ires rs (b, []) = False"
+ "wcode_goon_checking ires rs (b, []) = False"
+ "wcode_right_move ires rs (b, []) = False"
+ "wcode_erase2 ires rs (b, []) = False"
+ "wcode_on_right_moving_2 ires rs (b, []) = False"
+ "wcode_backto_standard_pos_2 ires rs (b, []) = False"
+ "wcode_on_checking_2 ires rs (b, Oc # list) = False"
+ by(auto simp: wcode_fourtimes_invs)
+
+lemma wcode_on_left_moving_2[simp]:
+ "wcode_on_left_moving_2 ires rs (b, Bk # list) \<Longrightarrow> wcode_on_left_moving_2 ires rs (tl b, hd b # Bk # list)"
apply(simp only: wcode_fourtimes_invs)
apply(erule_tac disjE)
apply(erule_tac exE)+
@@ -1782,55 +1583,32 @@
apply(simp)
done
-lemma [simp]: "wcode_on_checking_2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
-apply(auto simp: wcode_fourtimes_invs)
-done
-
-lemma [simp]: "wcode_on_checking_2 ires rs (b, Bk # list)
+lemma wcode_goon_checking_via_2 [simp]: "wcode_on_checking_2 ires rs (b, Bk # list)
\<Longrightarrow> wcode_goon_checking ires rs (tl b, hd b # Bk # list)"
apply(simp only: wcode_fourtimes_invs)
apply(auto)
-done
-
-lemma [simp]: "wcode_goon_checking ires rs (b, Bk # list) = False"
-apply(simp add: wcode_fourtimes_invs)
-done
-
-lemma [simp]: " wcode_right_move ires rs (b, Bk # list) \<Longrightarrow> b\<noteq> []"
-apply(simp add: wcode_fourtimes_invs)
-done
-
-lemma [simp]: "wcode_right_move ires rs (b, Bk # list) \<Longrightarrow> wcode_erase2 ires rs (Bk # b, list)"
+ done
+
+lemma wcode_erase2_via_move [simp]: "wcode_right_move ires rs (b, Bk # list) \<Longrightarrow> wcode_erase2 ires rs (Bk # b, list)"
apply(auto simp:wcode_fourtimes_invs )
apply(rule_tac x = ln in exI, rule_tac x = rn in exI, simp)
-done
-
-lemma [simp]: "wcode_erase2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
-apply(auto simp: wcode_fourtimes_invs)
-done
-
-lemma [simp]: "wcode_erase2 ires rs (b, Bk # list) \<Longrightarrow> wcode_on_right_moving_2 ires rs (Bk # b, list)"
+ done
+lemma wcode_on_right_moving_2_via_erase2[simp]:
+ "wcode_erase2 ires rs (b, Bk # list) \<Longrightarrow> wcode_on_right_moving_2 ires rs (Bk # b, list)"
apply(auto simp:wcode_fourtimes_invs )
apply(rule_tac x = "Suc (Suc 0)" in exI, simp add: exp_ind)
apply(rule_tac x = "Suc (Suc ln)" in exI, simp add: exp_ind del: replicate_Suc)
done
-lemma [simp]: "wcode_on_right_moving_2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
-apply(auto simp:wcode_fourtimes_invs )
-done
-
-lemma [simp]: "wcode_on_right_moving_2 ires rs (b, Bk # list)
+lemma wcode_on_right_moving_2_move_Bk[simp]: "wcode_on_right_moving_2 ires rs (b, Bk # list)
\<Longrightarrow> wcode_on_right_moving_2 ires rs (Bk # b, list)"
apply(auto simp: wcode_fourtimes_invs)
apply(rule_tac x = "Suc ml" in exI, simp)
apply(rule_tac x = "mr - 1" in exI, case_tac mr,auto)
-done
-
-lemma [simp]: "wcode_goon_right_moving_2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
-apply(auto simp: wcode_fourtimes_invs)
-done
-
-lemma [simp]: "wcode_goon_right_moving_2 ires rs (b, Bk # list) \<Longrightarrow>
+ done
+
+lemma wcode_backto_standard_pos_2_via_right[simp]:
+ "wcode_goon_right_moving_2 ires rs (b, Bk # list) \<Longrightarrow>
wcode_backto_standard_pos_2 ires rs (b, Oc # list)"
apply(simp add: wcode_fourtimes_invs, auto)
apply(rule_tac x = ml in exI, auto)
@@ -1838,27 +1616,16 @@
apply(case_tac mr, simp_all)
apply(rule_tac x = "rn - 1" in exI, simp)
apply(case_tac rn, simp, simp)
-done
-
-lemma [simp]: "wcode_backto_standard_pos_2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
-apply(simp add: wcode_fourtimes_invs, auto)
-done
-
-lemma [simp]: "wcode_on_left_moving_2 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
-apply(simp add: wcode_fourtimes_invs, auto)
-done
-
-lemma [simp]: "wcode_on_left_moving_2 ires rs (b, Oc # list) \<Longrightarrow>
+ done
+
+lemma wcode_on_checking_2_via_left[simp]: "wcode_on_left_moving_2 ires rs (b, Oc # list) \<Longrightarrow>
wcode_on_checking_2 ires rs (tl b, hd b # Oc # list)"
apply(auto simp: wcode_fourtimes_invs)
apply(case_tac [!] mr, simp_all)
-done
-
-lemma [simp]: "wcode_goon_right_moving_2 ires rs (b, []) \<Longrightarrow> b \<noteq> []"
-apply(auto simp: wcode_fourtimes_invs)
-done
-
-lemma [simp]: "wcode_goon_right_moving_2 ires rs (b, []) \<Longrightarrow>
+ done
+
+lemma wcode_backto_standard_pos_2_empty_via_right[simp]:
+ "wcode_goon_right_moving_2 ires rs (b, []) \<Longrightarrow>
wcode_backto_standard_pos_2 ires rs (b, [Oc])"
apply(simp only: wcode_fourtimes_invs)
apply(erule_tac exE)+
@@ -1867,18 +1634,7 @@
rule_tac x = ln in exI, rule_tac x = rn in exI, simp)
done
-lemma "wcode_backto_standard_pos_2 ires rs (b, Bk # list)
- \<Longrightarrow> (\<exists>ln. b = Bk # Bk\<up>(ln) @ Oc # ires) \<and> (\<exists>rn. list = Oc\<up>(Suc (Suc rs)) @ Bk\<up>(rn))"
-apply(auto simp: wcode_fourtimes_invs)
-apply(case_tac [!] mr, auto)
-done
-
-
-lemma [simp]: "wcode_on_checking_2 ires rs (b, Oc # list) \<Longrightarrow> False"
-apply(simp add: wcode_fourtimes_invs)
-done
-
-lemma [simp]: "wcode_goon_checking ires rs (b, Oc # list) \<Longrightarrow>
+lemma wcode_goon_checking_cases[simp]: "wcode_goon_checking ires rs (b, Oc # list) \<Longrightarrow>
(b = [] \<longrightarrow> wcode_right_move ires rs ([Oc], list)) \<and>
(b \<noteq> [] \<longrightarrow> wcode_right_move ires rs (Oc # b, list))"
apply(simp only: wcode_fourtimes_invs)
@@ -1886,25 +1642,17 @@
apply(auto)
done
-lemma [simp]: "wcode_right_move ires rs (b, Oc # list) = False"
+lemma wcode_right_move_no_Oc[simp]: "wcode_right_move ires rs (b, Oc # list) = False"
apply(auto simp: wcode_fourtimes_invs)
done
-lemma [simp]: " wcode_erase2 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
-apply(simp add: wcode_fourtimes_invs)
-done
-
-lemma [simp]: "wcode_erase2 ires rs (b, Oc # list)
+lemma wcode_erase2_Bk_via_Oc[simp]: "wcode_erase2 ires rs (b, Oc # list)
\<Longrightarrow> wcode_erase2 ires rs (b, Bk # list)"
apply(auto simp: wcode_fourtimes_invs)
done
-lemma [simp]: "wcode_on_right_moving_2 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
-apply(simp only: wcode_fourtimes_invs)
-apply(auto)
-done
-
-lemma [simp]: "wcode_on_right_moving_2 ires rs (b, Oc # list)
+lemma wcode_goon_right_moving_2_Oc_move[simp]:
+ "wcode_on_right_moving_2 ires rs (b, Oc # list)
\<Longrightarrow> wcode_goon_right_moving_2 ires rs (Oc # b, list)"
apply(auto simp: wcode_fourtimes_invs)
apply(case_tac mr, simp_all)
@@ -1913,33 +1661,23 @@
apply(case_tac ml, simp, case_tac nat, simp_all)
done
-lemma [simp]: "wcode_goon_right_moving_2 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
-apply(simp only:wcode_fourtimes_invs, auto)
-done
-
-lemma [simp]: "wcode_backto_standard_pos_2 ires rs (b, Bk # list)
+lemma wcode_backto_standard_pos_2_exists[simp]: "wcode_backto_standard_pos_2 ires rs (b, Bk # list)
\<Longrightarrow> (\<exists>ln. b = Bk # Bk\<up>(ln) @ Oc # ires) \<and> (\<exists>rn. list = Oc\<up>(Suc (Suc rs)) @ Bk\<up>(rn))"
apply(simp add: wcode_fourtimes_invs, auto)
apply(case_tac [!] mr, simp_all)
done
-lemma [simp]: "wcode_on_checking_2 ires rs (b, Oc # list) = False"
-apply(simp add: wcode_fourtimes_invs)
-done
-
-lemma [simp]: "wcode_goon_right_moving_2 ires rs (b, Oc # list) \<Longrightarrow>
+lemma wcode_goon_right_moving_2_move_Oc[simp]: "wcode_goon_right_moving_2 ires rs (b, Oc # list) \<Longrightarrow>
wcode_goon_right_moving_2 ires rs (Oc # b, list)"
apply(simp only:wcode_fourtimes_invs, auto)
apply(rule_tac x = "Suc ml" in exI, simp)
apply(rule_tac x = "mr - 1" in exI)
apply(case_tac mr, case_tac rn, auto)
-done
-
-lemma [simp]: "wcode_backto_standard_pos_2 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
-apply(simp only: wcode_fourtimes_invs, auto)
-done
-
-lemma [simp]: "wcode_backto_standard_pos_2 ires rs (b, Oc # list)
+ done
+
+
+lemma wcode_backto_standard_pos_2_Oc_mv_hd[simp]:
+ "wcode_backto_standard_pos_2 ires rs (b, Oc # list)
\<Longrightarrow> wcode_backto_standard_pos_2 ires rs (tl b, hd b # Oc # list)"
apply(simp only: wcode_fourtimes_invs)
apply(erule_tac disjE)
@@ -1949,6 +1687,24 @@
apply(rule_tac x = "Suc mr" in exI, simp)
done
+lemma nonempty_fst[simp]:
+ "wcode_on_left_moving_2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+ "wcode_on_checking_2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+ "wcode_goon_checking ires rs (b, Bk # list) = False"
+ "wcode_right_move ires rs (b, Bk # list) \<Longrightarrow> b\<noteq> []"
+ "wcode_erase2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+ "wcode_on_right_moving_2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+ "wcode_goon_right_moving_2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+ "wcode_backto_standard_pos_2 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+ "wcode_on_left_moving_2 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+ "wcode_goon_right_moving_2 ires rs (b, []) \<Longrightarrow> b \<noteq> []"
+ "wcode_erase2 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+ "wcode_on_right_moving_2 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+ "wcode_goon_right_moving_2 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+ "wcode_backto_standard_pos_2 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+ by(auto simp: wcode_fourtimes_invs)
+
+
lemma wcode_fourtimes_case_first_correctness:
shows "let P = (\<lambda> (st, l, r). st = t_twice_len + 14) in
let Q = (\<lambda> (st, l, r). wcode_fourtimes_case_inv st ires rs (l, r)) in
@@ -1997,18 +1753,13 @@
where
"t_fourtimes_len = (length t_fourtimes div 2)"
-lemma t_fourtimes_len_gr: "t_fourtimes_len > 0"
-apply(simp add: t_fourtimes_len_def t_fourtimes_def mopup.simps t_fourtimes_compile_def)
-done
-
-lemma [intro]: "primerec rec_fourtimes (Suc 0)"
+lemma primerec_rec_fourtimes_1[intro]: "primerec rec_fourtimes (Suc 0)"
apply(auto simp: rec_fourtimes_def numeral_4_eq_4 constn.simps)
by auto
lemma fourtimes_lemma: "rec_exec rec_fourtimes [rs] = 4 * rs"
by(simp add: rec_exec.simps rec_fourtimes_def)
-
lemma t_fourtimes_correct:
"\<exists>stp ln rn. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
(tm_of abc_fourtimes @ shift (mopup 1) (length (tm_of abc_fourtimes) div 2)) stp =
@@ -2031,7 +1782,7 @@
by(simp add: abc_fourtimes_def)
qed
thus "?thesis"
- apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv fourtimes_lemma)
+ apply(simp add: tape_of_list_def tape_of_nat_def fourtimes_lemma)
done
qed
@@ -2067,9 +1818,8 @@
by metis
qed
-lemma [intro]: "length t_twice mod 2 = 0"
-apply(auto simp: t_twice_def t_twice_compile_def)
-by (metis mopup_mod2)
+lemma length_t_twice_even[intro]: "is_even (length t_twice)"
+ by(auto simp: t_twice_def t_twice_compile_def intro!:mopup_mod2)
lemma t_fourtimes_append_pre:
"steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) t_fourtimes stp
@@ -2084,25 +1834,12 @@
= ((Suc t_fourtimes_len) + length (t_wcode_main_first_part @
shift t_twice (length t_wcode_main_first_part div 2) @ [(L, 1), (L, 1)]) div 2,
Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))"
-apply(rule_tac tm_append_shift_append_steps, simp_all)
-apply(auto simp: t_wcode_main_first_part_def)
-done
-
-
-lemma [simp]: "length t_wcode_main_first_part = 24"
-apply(simp add: t_wcode_main_first_part_def)
-done
-
-lemma [simp]: "(26 + length t_twice) div 2 = (length t_twice) div 2 + 13"
-apply(simp add: t_twice_def t_twice_def)
-done
-
-lemma [simp]: "((26 + length (shift t_twice 12)) div 2)
- = (length (shift t_twice 12) div 2 + 13)"
-apply(simp add: t_twice_def)
-done
-
-lemma [simp]: "t_twice_len + 14 = 14 + length (shift t_twice 12) div 2"
+ using length_t_twice_even
+ by(intro tm_append_shift_append_steps, auto)
+
+lemma split_26_even[simp]: "(26 + l::nat) div 2 = l div 2 + 13" by(simp)
+
+lemma t_twice_len_plust_14[simp]: "t_twice_len + 14 = 14 + length (shift t_twice 12) div 2"
apply(simp add: t_twice_def t_twice_len_def)
done
@@ -2125,43 +1862,34 @@
apply(simp add: t_twice_len_def)
done
-lemma t_wcode_main_len: "length t_wcode_main = length t_twice + length t_fourtimes + 28"
-apply(simp add: t_wcode_main_def)
-done
-
-lemma even_twice_len: "length t_twice mod 2 = 0"
-apply(auto simp: t_twice_def t_twice_compile_def)
-by (metis mopup_mod2)
-
lemma even_fourtimes_len: "length t_fourtimes mod 2 = 0"
apply(auto simp: t_fourtimes_def t_fourtimes_compile_def)
by (metis mopup_mod2)
-lemma [simp]: "2 * (length t_twice div 2) = length t_twice"
-using even_twice_len
-by arith
-
-lemma [simp]: "2 * (length t_fourtimes div 2) = length t_fourtimes"
+lemma t_twice_even[simp]: "2 * (length t_twice div 2) = length t_twice"
+using length_t_twice_even by arith
+
+lemma t_fourtimes_even[simp]: "2 * (length t_fourtimes div 2) = length t_fourtimes"
using even_fourtimes_len
by arith
-lemma [simp]: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) Oc
+lemma fetch_t_wcode_14_Oc: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) Oc
= (L, Suc 0)"
apply(subgoal_tac "14 = Suc 13")
apply(simp only: fetch.simps add_Suc nth_of.simps t_wcode_main_def)
-apply(simp add:length_append length_shift Parity.two_times_even_div_two even_twice_len t_fourtimes_len_def nth_append)
+apply(simp add:length_t_twice_even t_fourtimes_len_def nth_append)
by arith
-lemma [simp]: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) Bk
+lemma fetch_t_wcode_14_Bk: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) Bk
= (L, Suc 0)"
apply(subgoal_tac "14 = Suc 13")
apply(simp only: fetch.simps add_Suc nth_of.simps t_wcode_main_def)
-apply(simp add:length_append length_shift Parity.two_times_even_div_two even_twice_len t_fourtimes_len_def nth_append)
+apply(simp add:length_t_twice_even t_fourtimes_len_def nth_append)
by arith
-lemma [simp]: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) b
+lemma fetch_t_wcode_14 [simp]: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) b
= (L, Suc 0)"
-apply(case_tac b, simp_all)
+apply(case_tac b, simp_all add:fetch_t_wcode_14_Bk fetch_t_wcode_14_Oc)
done
lemma wcode_jump2:
@@ -2224,7 +1952,7 @@
from stp1 stp2 stp3 show "?thesis"
apply(rule_tac x = "stpa + stpb + stpc" in exI,
rule_tac x = lnc in exI, rule_tac x = rnc in exI)
- apply(simp add: steps_add)
+ apply(simp)
done
qed
@@ -2309,27 +2037,8 @@
wcode_on_checking_3.simps wcode_goon_checking_3.simps
wcode_on_left_moving_3.simps wcode_stop.simps
-lemma [simp]: "fetch t_wcode_main 7 Bk = (R, 0)"
-apply(subgoal_tac "7 = Suc 6")
-apply(simp only: fetch.simps t_wcode_main_def nth_append nth_of.simps
- t_wcode_main_first_part_def)
-apply(auto)
-done
-
-lemma [simp]: "wcode_on_left_moving_3 ires rs (b, []) = False"
-apply(simp only: wcode_halt_invs)
-apply(simp)
-done
-
-lemma [simp]: "wcode_on_checking_3 ires rs (b, []) = False"
-apply(simp add: wcode_halt_invs)
-done
-
-lemma [simp]: "wcode_goon_checking_3 ires rs (b, []) = False"
-apply(simp add: wcode_halt_invs)
-done
-
-lemma [simp]: "wcode_on_left_moving_3 ires rs (b, Bk # list)
+
+lemma wcode_on_left_moving_3_mv_Bk[simp]: "wcode_on_left_moving_3 ires rs (b, Bk # list)
\<Longrightarrow> wcode_on_left_moving_3 ires rs (tl b, hd b # Bk # list)"
apply(simp only: wcode_halt_invs)
apply(erule_tac disjE)
@@ -2344,43 +2053,34 @@
apply(simp)
done
-lemma [simp]: "wcode_goon_checking_3 ires rs (b, Bk # list) \<Longrightarrow>
+lemma wcode_goon_checking_3_cases[simp]: "wcode_goon_checking_3 ires rs (b, Bk # list) \<Longrightarrow>
(b = [] \<longrightarrow> wcode_stop ires rs ([Bk], list)) \<and>
(b \<noteq> [] \<longrightarrow> wcode_stop ires rs (Bk # b, list))"
apply(auto simp: wcode_halt_invs)
done
-lemma [simp]: "wcode_on_left_moving_3 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
-apply(auto simp: wcode_halt_invs)
-done
-
-lemma [simp]: "wcode_on_left_moving_3 ires rs (b, Oc # list) \<Longrightarrow>
+lemma wcode_on_checking_3_mv_Oc[simp]: "wcode_on_left_moving_3 ires rs (b, Oc # list) \<Longrightarrow>
wcode_on_checking_3 ires rs (tl b, hd b # Oc # list)"
apply(simp add:wcode_halt_invs, auto)
apply(case_tac [!] mr, simp_all)
done
-lemma [simp]: "wcode_on_checking_3 ires rs (b, Oc # list) = False"
-apply(auto simp: wcode_halt_invs)
-done
-
-lemma [simp]: "wcode_on_left_moving_3 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
-apply(simp add: wcode_halt_invs, auto)
-done
-
-lemma [simp]: "wcode_on_checking_3 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
-apply(auto simp: wcode_halt_invs)
-done
-
-lemma [simp]: "wcode_on_checking_3 ires rs (b, Bk # list) \<Longrightarrow>
+lemma wcode_3_nonempty[simp]:
+ "wcode_on_left_moving_3 ires rs (b, []) = False"
+ "wcode_on_checking_3 ires rs (b, []) = False"
+ "wcode_goon_checking_3 ires rs (b, []) = False"
+ "wcode_on_left_moving_3 ires rs (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+ "wcode_on_checking_3 ires rs (b, Oc # list) = False"
+ "wcode_on_left_moving_3 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+ "wcode_on_checking_3 ires rs (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+ "wcode_goon_checking_3 ires rs (b, Oc # list) = False"
+ by(auto simp: wcode_halt_invs)
+
+lemma wcode_goon_checking_3_mv_Bk[simp]: "wcode_on_checking_3 ires rs (b, Bk # list) \<Longrightarrow>
wcode_goon_checking_3 ires rs (tl b, hd b # Bk # list)"
apply(auto simp: wcode_halt_invs)
done
-lemma [simp]: "wcode_goon_checking_3 ires rs (b, Oc # list) = False"
-apply(simp add: wcode_goon_checking_3.simps)
-done
-
lemma t_halt_case_correctness:
shows "let P = (\<lambda> (st, l, r). st = 0) in
let Q = (\<lambda> (st, l, r). wcode_halt_case_inv st ires rs (l, r)) in
@@ -2418,7 +2118,7 @@
qed
declare wcode_halt_case_inv.simps[simp del]
-lemma [intro]: "\<exists> xs. (<rev list @ [aa::nat]> :: cell list) = Oc # xs"
+lemma leading_Oc[intro]: "\<exists> xs. (<rev list @ [aa::nat]> :: cell list) = Oc # xs"
apply(case_tac "rev list", simp)
apply(simp add: tape_of_nl_cons)
done
@@ -2436,15 +2136,11 @@
rule_tac x = rn in exI, simp)
done
-lemma bl_bin_one: "bl_bin [Oc] = Suc 0"
+lemma bl_bin_one[simp]: "bl_bin [Oc] = 1"
apply(simp add: bl_bin.simps)
done
-lemma [simp]: "bl_bin [Oc] = 1"
-apply(simp add: bl_bin.simps)
-done
-
-lemma [intro]: "2 * 2 ^ a = Suc (Suc (2 * bl_bin (Oc \<up> a)))"
+lemma twice_power[intro]: "2 * 2 ^ a = Suc (Suc (2 * bl_bin (Oc \<up> a)))"
apply(induct a, auto simp: bl_bin.simps)
done
declare replicate_Suc[simp del]
@@ -2508,14 +2204,14 @@
"\<exists>stp ln rn.
steps0 (Suc 0, Bk # Bk\<up>(lna) @ rev (<a::nat>) @ Bk # Bk # ires, Bk # Oc\<up>(Suc (2 * rs + 2)) @ Bk\<up>(rna)) t_wcode_main stp =
(0, Bk # ires, Bk # Oc # Bk\<up>(ln) @ Bk # Bk # Oc\<up>(bl_bin (<a>) + (2*rs + 2) * 2 ^ a) @ Bk\<up>(rn))"
- using ind2[of lna ires "2*rs + 2" rna] by(simp add: tape_of_nl_abv tape_of_nat_abv)
+ using ind2[of lna ires "2*rs + 2" rna] by(simp add: tape_of_list_def tape_of_nat_def)
from this obtain stpb lnb rnb where stp2:
"steps0 (Suc 0, Bk # Bk\<up>(lna) @ rev (<a>) @ Bk # Bk # ires, Bk # Oc\<up>(Suc (2 * rs + 2)) @ Bk\<up>(rna)) t_wcode_main stpb =
(0, Bk # ires, Bk # Oc # Bk\<up>(lnb) @ Bk # Bk # Oc\<up>(bl_bin (<a>) + (2*rs + 2) * 2 ^ a) @ Bk\<up>(rnb))"
by blast
from stp1 and stp2 show "?thesis"
apply(rule_tac x = "stpa + stpb" in exI,
- rule_tac x = lnb in exI, rule_tac x = rnb in exI, simp add: tape_of_nat_abv)
+ rule_tac x = lnb in exI, rule_tac x = rnb in exI, simp add: tape_of_nat_def)
apply(simp add: bl_bin.simps replicate_Suc)
apply(auto)
done
@@ -2781,9 +2477,6 @@
definition wcode_prepare_le :: "(config \<times> config) set"
where "wcode_prepare_le \<equiv> (inv_image lex_triple wcode_prepare_measure)"
-lemma [intro]: "wf lex_pair"
-by(auto intro:wf_lex_prod simp:lex_pair_def)
-
lemma wf_wcode_prepare_le[intro]: "wf wcode_prepare_le"
by(auto intro:wf_inv_image simp: wcode_prepare_le_def
lex_triple_def)
@@ -2799,103 +2492,48 @@
wprepare_add_one2.simps
declare wprepare_inv.simps[simp del]
-lemma [simp]: "fetch t_wcode_prepare (Suc 0) Bk = (W1, 2)"
-apply(simp add: fetch.simps t_wcode_prepare_def nth_of.simps)
-done
-
-lemma [simp]: "fetch t_wcode_prepare (Suc 0) Oc = (L, 1)"
-apply(simp add: fetch.simps t_wcode_prepare_def nth_of.simps)
-done
-
-lemma [simp]: "fetch t_wcode_prepare (Suc (Suc 0)) Bk = (L, 3)"
-apply(simp add: fetch.simps t_wcode_prepare_def nth_of.simps)
-done
-
-lemma [simp]: "fetch t_wcode_prepare (Suc (Suc 0)) Oc = (R, 2)"
-apply(simp add: fetch.simps t_wcode_prepare_def nth_of.simps)
-done
-
-lemma [simp]: "fetch t_wcode_prepare (Suc (Suc (Suc 0))) Bk = (R, 4)"
-apply(simp add: fetch.simps t_wcode_prepare_def nth_of.simps)
-done
-
-lemma [simp]: "fetch t_wcode_prepare (Suc (Suc (Suc 0))) Oc = (W0, 3)"
-apply(simp add: fetch.simps t_wcode_prepare_def nth_of.simps)
-done
-
-lemma [simp]: "fetch t_wcode_prepare 4 Bk = (R, 4)"
-apply(subgoal_tac "4 = Suc 3")
-apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps)
-apply(auto)
-done
-
-lemma [simp]: "fetch t_wcode_prepare 4 Oc = (R, 5)"
-apply(subgoal_tac "4 = Suc 3")
-apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps)
-apply(auto)
-done
-
-
-lemma [simp]: "fetch t_wcode_prepare 5 Oc = (R, 5)"
-apply(subgoal_tac "5 = Suc 4")
-apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps)
-apply(auto)
-done
-
-lemma [simp]: "fetch t_wcode_prepare 5 Bk = (R, 6)"
-apply(subgoal_tac "5 = Suc 4")
-apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps)
-apply(auto)
-done
-
-lemma [simp]: "fetch t_wcode_prepare 6 Oc = (R, 5)"
-apply(subgoal_tac "6 = Suc 5")
-apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps)
-apply(auto)
-done
-
-lemma [simp]: "fetch t_wcode_prepare 6 Bk = (R, 7)"
-apply(subgoal_tac "6 = Suc 5")
-apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps)
-apply(auto)
-done
-
-lemma [simp]: "fetch t_wcode_prepare 7 Oc = (L, 0)"
-apply(subgoal_tac "7 = Suc 6")
-apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps)
-apply(auto)
-done
-
-lemma [simp]: "fetch t_wcode_prepare 7 Bk = (W1, 7)"
-apply(subgoal_tac "7 = Suc 6")
-apply(simp_all only: fetch.simps t_wcode_prepare_def nth_of.simps)
-apply(auto)
-done
-
-lemma [simp]: "lm \<noteq> [] \<Longrightarrow> wprepare_add_one m lm (b, []) = False"
+
+lemma fetch_t_wcode_prepare[simp]:
+ "fetch t_wcode_prepare (Suc 0) Bk = (W1, 2)"
+ "fetch t_wcode_prepare (Suc 0) Oc = (L, 1)"
+ "fetch t_wcode_prepare (Suc (Suc 0)) Bk = (L, 3)"
+ "fetch t_wcode_prepare (Suc (Suc 0)) Oc = (R, 2)"
+ "fetch t_wcode_prepare (Suc (Suc (Suc 0))) Bk = (R, 4)"
+ "fetch t_wcode_prepare (Suc (Suc (Suc 0))) Oc = (W0, 3)"
+ "fetch t_wcode_prepare 4 Bk = (R, 4)"
+ "fetch t_wcode_prepare 4 Oc = (R, 5)"
+ "fetch t_wcode_prepare 5 Oc = (R, 5)"
+ "fetch t_wcode_prepare 5 Bk = (R, 6)"
+ "fetch t_wcode_prepare 6 Oc = (R, 5)"
+ "fetch t_wcode_prepare 6 Bk = (R, 7)"
+ "fetch t_wcode_prepare 7 Oc = (L, 0)"
+ "fetch t_wcode_prepare 7 Bk = (W1, 7)"
+ unfolding fetch.simps t_wcode_prepare_def nth_of.simps
+ numeral by auto
+
+lemma wprepare_add_one_nonempty_snd[simp]: "lm \<noteq> [] \<Longrightarrow> wprepare_add_one m lm (b, []) = False"
apply(simp add: wprepare_invs)
done
-lemma [simp]: "lm \<noteq> [] \<Longrightarrow> wprepare_goto_first_end m lm (b, []) = False"
+lemma wprepare_goto_first_end_nonempty_snd[simp]: "lm \<noteq> [] \<Longrightarrow> wprepare_goto_first_end m lm (b, []) = False"
apply(simp add: wprepare_invs)
done
-lemma [simp]: "lm \<noteq> [] \<Longrightarrow> wprepare_erase m lm (b, []) = False"
+lemma wprepare_erase_nonempty_snd[simp]: "lm \<noteq> [] \<Longrightarrow> wprepare_erase m lm (b, []) = False"
apply(simp add: wprepare_invs)
done
-lemma [simp]: "lm \<noteq> [] \<Longrightarrow> wprepare_goto_start_pos m lm (b, []) = False"
+lemma wprepare_goto_start_pos_nonempty_snd[simp]: "lm \<noteq> [] \<Longrightarrow> wprepare_goto_start_pos m lm (b, []) = False"
apply(simp add: wprepare_invs)
done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start m lm (b, [])\<rbrakk> \<Longrightarrow> b \<noteq> []"
+lemma wprepare_loop_start_empty_nonempty_fst[simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start m lm (b, [])\<rbrakk> \<Longrightarrow> b \<noteq> []"
apply(simp add: wprepare_invs)
done
-lemma rev_eq: "rev xs = rev ys \<Longrightarrow> xs = ys"
-by auto
-
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start m lm (b, [])\<rbrakk> \<Longrightarrow>
+lemma rev_eq: "rev xs = rev ys \<Longrightarrow> xs = ys" by auto
+
+lemma wprepare_loop_goon_Bk_empty_snd[simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start m lm (b, [])\<rbrakk> \<Longrightarrow>
wprepare_loop_goon m lm (Bk # b, [])"
apply(simp only: wprepare_invs)
apply(erule_tac disjE)
@@ -2905,118 +2543,110 @@
apply(rule_tac rev_eq, simp add: tape_of_nl_rev)
done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_goon m lm (b, [])\<rbrakk> \<Longrightarrow> b \<noteq> []"
+lemma wprepare_loop_goon_nonempty_fst[simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_goon m lm (b, [])\<rbrakk> \<Longrightarrow> b \<noteq> []"
apply(simp only: wprepare_invs, auto)
done
-lemma [simp]:"\<lbrakk>lm \<noteq> []; wprepare_loop_goon m lm (b, [])\<rbrakk> \<Longrightarrow>
+lemma wprepare_add_one2_Bk_empty[simp]:"\<lbrakk>lm \<noteq> []; wprepare_loop_goon m lm (b, [])\<rbrakk> \<Longrightarrow>
wprepare_add_one2 m lm (Bk # b, [])"
apply(simp only: wprepare_invs, auto split: if_splits)
done
-lemma [simp]: "wprepare_add_one2 m lm (b, []) \<Longrightarrow> b \<noteq> []"
+lemma wprepare_add_one2_nonempty_fst[simp]: "wprepare_add_one2 m lm (b, []) \<Longrightarrow> b \<noteq> []"
apply(simp only: wprepare_invs, auto)
done
-lemma [simp]: "wprepare_add_one2 m lm (b, []) \<Longrightarrow> wprepare_add_one2 m lm (b, [Oc])"
+lemma wprepare_add_one2_Oc[simp]: "wprepare_add_one2 m lm (b, []) \<Longrightarrow> wprepare_add_one2 m lm (b, [Oc])"
apply(simp only: wprepare_invs, auto)
done
-lemma [simp]: "Bk # list = <(m::nat) # lm> @ ys = False"
+lemma Bk_not_tape_start[simp]: "(Bk # list = <(m::nat) # lm> @ ys) = False"
apply(case_tac lm, auto simp: tape_of_nl_cons replicate_Suc)
done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_add_one m lm (b, Bk # list)\<rbrakk>
+lemma wprepare_goto_first_end_cases[simp]:
+ "\<lbrakk>lm \<noteq> []; wprepare_add_one m lm (b, Bk # list)\<rbrakk>
\<Longrightarrow> (b = [] \<longrightarrow> wprepare_goto_first_end m lm ([], Oc # list)) \<and>
(b \<noteq> [] \<longrightarrow> wprepare_goto_first_end m lm (b, Oc # list))"
apply(simp only: wprepare_invs)
apply(auto simp: tape_of_nl_cons split: if_splits)
apply(rule_tac x = 0 in exI, simp add: replicate_Suc)
-apply(case_tac lm, simp, simp add: tape_of_nl_abv tape_of_nat_list.simps replicate_Suc)
+apply(case_tac lm, simp, simp add: tape_of_list_def tape_of_nat_list.simps replicate_Suc)
done
-lemma [simp]: "wprepare_goto_first_end m lm (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+lemma wprepare_goto_first_end_Bk_nonempty_fst[simp]:
+ "wprepare_goto_first_end m lm (b, Bk # list) \<Longrightarrow> b \<noteq> []"
apply(simp only: wprepare_invs , auto simp: replicate_Suc)
done
declare replicate_Suc[simp]
-lemma [simp]: "wprepare_goto_first_end m lm (b, Bk # list) \<Longrightarrow>
+lemma wprepare_erase_elem_Bk_rest[simp]: "wprepare_goto_first_end m lm (b, Bk # list) \<Longrightarrow>
wprepare_erase m lm (tl b, hd b # Bk # list)"
apply(simp only: wprepare_invs, auto)
apply(case_tac mr, simp_all)
apply(case_tac mr, auto)
done
-lemma [simp]: "wprepare_erase m lm (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+lemma wprepare_erase_Bk_nonempty_fst[simp]: "wprepare_erase m lm (b, Bk # list) \<Longrightarrow> b \<noteq> []"
apply(simp only: wprepare_invs, auto)
done
-lemma [simp]: "wprepare_erase m lm (b, Bk # list) \<Longrightarrow>
+lemma wprepare_goto_start_pos_Bk[simp]: "wprepare_erase m lm (b, Bk # list) \<Longrightarrow>
wprepare_goto_start_pos m lm (Bk # b, list)"
apply(simp only: wprepare_invs, auto)
done
-lemma [simp]: "\<lbrakk>wprepare_add_one m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
+lemma wprepare_add_one_Bk_nonempty_snd[simp]: "\<lbrakk>wprepare_add_one m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
apply(simp only: wprepare_invs)
-apply(case_tac lm, simp_all add: tape_of_nl_abv
- tape_of_nat_list.simps tape_of_nat_abv, auto)
+apply(case_tac lm, simp_all add: tape_of_list_def tape_of_nat_def, auto)
done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_goto_first_end m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
+lemma wprepare_goto_first_end_nonempty_snd_tl[simp]:
+ "\<lbrakk>lm \<noteq> []; wprepare_goto_first_end m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
apply(simp only: wprepare_invs, auto)
apply(case_tac mr, simp_all)
-done
-
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_goto_first_end m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> b \<noteq> []"
+ done
+
+lemma wprepare_erase_Bk_nonempty_list[simp]: "\<lbrakk>lm \<noteq> []; wprepare_erase m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
apply(simp only: wprepare_invs, auto)
done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_erase m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
-apply(simp only: wprepare_invs, auto)
-done
-
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_erase m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> b \<noteq> []"
-apply(simp only: wprepare_invs, auto)
-done
-
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_goto_start_pos m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
-apply(simp only: wprepare_invs, auto)
-apply(case_tac lm, simp, case_tac list)
-apply(simp_all add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
-done
-
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_goto_start_pos m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> b \<noteq> []"
+
+lemma wprepare_goto_start_pos_Bk_nonempty[simp]: "\<lbrakk>lm \<noteq> []; wprepare_goto_start_pos m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
+ by(cases lm;cases list;simp only: wprepare_invs, auto)
+
+lemma wprepare_goto_start_pos_Bk_nonempty_fst[simp]: "\<lbrakk>lm \<noteq> []; wprepare_goto_start_pos m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> b \<noteq> []"
apply(simp only: wprepare_invs)
apply(auto)
done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_goon m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> b \<noteq> []"
+lemma wprepare_loop_goon_Bk_nonempty[simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_goon m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> b \<noteq> []"
apply(simp only: wprepare_invs, auto)
done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_goon m lm (b, Bk # list)\<rbrakk> \<Longrightarrow>
+lemma wprepare_loop_goon_wprepare_add_one2_cases[simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_goon m lm (b, Bk # list)\<rbrakk> \<Longrightarrow>
(list = [] \<longrightarrow> wprepare_add_one2 m lm (Bk # b, [])) \<and>
(list \<noteq> [] \<longrightarrow> wprepare_add_one2 m lm (Bk # b, list))"
-apply(simp only: wprepare_invs, simp)
-apply(case_tac list, simp_all split: if_splits, auto)
+ unfolding wprepare_invs
+apply(cases list;auto split:nat.split if_splits)
apply(case_tac [1-3] mr, simp_all add: )
apply(case_tac mr, simp_all)
apply(case_tac [1-2] mr, simp_all add: )
-apply(case_tac rn, simp, case_tac nat, auto simp: )
+apply(case_tac rn, force, case_tac nat, auto simp: )
done
-lemma [simp]: "wprepare_add_one2 m lm (b, Bk # list) \<Longrightarrow> b \<noteq> []"
+lemma wprepare_add_one2_nonempty[simp]: "wprepare_add_one2 m lm (b, Bk # list) \<Longrightarrow> b \<noteq> []"
apply(simp only: wprepare_invs, simp)
done
-lemma [simp]: "wprepare_add_one2 m lm (b, Bk # list) \<Longrightarrow>
+lemma wprepare_add_one2_cases[simp]: "wprepare_add_one2 m lm (b, Bk # list) \<Longrightarrow>
(list = [] \<longrightarrow> wprepare_add_one2 m lm (b, [Oc])) \<and>
(list \<noteq> [] \<longrightarrow> wprepare_add_one2 m lm (b, Oc # list))"
apply(simp only: wprepare_invs, auto)
done
-lemma [simp]: "wprepare_goto_first_end m lm (b, Oc # list)
+lemma wprepare_goto_first_end_cases_Oc[simp]: "wprepare_goto_first_end m lm (b, Oc # list)
\<Longrightarrow> (b = [] \<longrightarrow> wprepare_goto_first_end m lm ([Oc], list)) \<and>
(b \<noteq> [] \<longrightarrow> wprepare_goto_first_end m lm (Oc # b, list))"
apply(simp only: wprepare_invs, auto)
@@ -3027,41 +2657,30 @@
apply(rule_tac x = "mr - 1" in exI, simp)
done
-lemma [simp]: "wprepare_erase m lm (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+lemma wprepare_erase_nonempty[simp]: "wprepare_erase m lm (b, Oc # list) \<Longrightarrow> b \<noteq> []"
apply(simp only: wprepare_invs, auto simp: )
done
-lemma [simp]: "wprepare_erase m lm (b, Oc # list)
+lemma wprepare_erase_Bk[simp]: "wprepare_erase m lm (b, Oc # list)
\<Longrightarrow> wprepare_erase m lm (b, Bk # list)"
apply(simp only:wprepare_invs, auto simp: )
done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_goto_start_pos m lm (b, Bk # list)\<rbrakk>
+lemma wprepare_goto_start_pos_Bk_move[simp]: "\<lbrakk>lm \<noteq> []; wprepare_goto_start_pos m lm (b, Bk # list)\<rbrakk>
\<Longrightarrow> wprepare_goto_start_pos m lm (Bk # b, list)"
apply(simp only:wprepare_invs, auto)
apply(case_tac [!] lm, simp, simp_all)
done
-lemma [simp]: "wprepare_loop_start m lm (b, aa) \<Longrightarrow> b \<noteq> []"
+lemma wprepare_loop_start_b_nonempty[simp]: "wprepare_loop_start m lm (b, aa) \<Longrightarrow> b \<noteq> []"
apply(simp only:wprepare_invs, auto)
done
-lemma [elim]: "Bk # list = Oc\<up>(mr) @ Bk\<up>(rn) \<Longrightarrow> \<exists>rn. list = Bk\<up>(rn)"
+lemma exists_exp_of_Bk[elim]: "Bk # list = Oc\<up>(mr) @ Bk\<up>(rn) \<Longrightarrow> \<exists>rn. list = Bk\<up>(rn)"
apply(case_tac mr, simp_all)
apply(case_tac rn, simp_all)
done
-lemma rev_equal_iff: "x = y \<Longrightarrow> rev x = rev y"
-by simp
-
-lemma tape_of_nl_false1:
- "lm \<noteq> [] \<Longrightarrow> rev b @ [Bk] \<noteq> Bk\<up>(ln) @ Oc # Oc\<up>(m) @ Bk # Bk # <lm::nat list>"
-apply(auto)
-apply(drule_tac rev_equal_iff, simp add: tape_of_nl_rev)
-apply(case_tac "rev lm")
-apply(case_tac [2] list, auto simp: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
-done
-
-lemma [simp]: "wprepare_loop_start_in_middle m lm (b, [Bk]) = False"
+lemma wprepare_loop_start_in_middle_Bk_False[simp]: "wprepare_loop_start_in_middle m lm (b, [Bk]) = False"
apply(simp add: wprepare_loop_start_in_middle.simps, auto)
apply(case_tac mr, simp_all add: )
done
@@ -3072,11 +2691,11 @@
wprepare_loop_goon_in_middle.simps[simp del]
wprepare_loop_goon_on_rightmost.simps[simp del]
-lemma [simp]: "wprepare_loop_goon_in_middle m lm (Bk # b, []) = False"
+lemma wprepare_loop_goon_in_middle_Bk_False[simp]: "wprepare_loop_goon_in_middle m lm (Bk # b, []) = False"
apply(simp add: wprepare_loop_goon_in_middle.simps, auto)
done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start m lm (b, [Bk])\<rbrakk> \<Longrightarrow>
+lemma wprepare_loop_goon_Bk[simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start m lm (b, [Bk])\<rbrakk> \<Longrightarrow>
wprepare_loop_goon m lm (Bk # b, [])"
apply(simp only: wprepare_invs, simp)
apply(simp add: wprepare_loop_goon_on_rightmost.simps
@@ -3087,13 +2706,13 @@
apply(simp add: exp_ind replicate_Suc[THEN sym] del: replicate_Suc)
done
-lemma [simp]: "wprepare_loop_start_on_rightmost m lm (b, Bk # a # lista)
+lemma wprepare_loop_goon_in_middle_Bk_False2[simp]: "wprepare_loop_start_on_rightmost m lm (b, Bk # a # lista)
\<Longrightarrow> wprepare_loop_goon_in_middle m lm (Bk # b, a # lista) = False"
apply(auto simp: wprepare_loop_start_on_rightmost.simps
wprepare_loop_goon_in_middle.simps)
done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start_on_rightmost m lm (b, Bk # a # lista)\<rbrakk>
+lemma wprepare_loop_goon_on_rightbmost_Bk_False[simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start_on_rightmost m lm (b, Bk # a # lista)\<rbrakk>
\<Longrightarrow> wprepare_loop_goon_on_rightmost m lm (Bk # b, a # lista)"
apply(simp only: wprepare_loop_start_on_rightmost.simps
wprepare_loop_goon_on_rightmost.simps, auto)
@@ -3102,20 +2721,20 @@
apply(simp add: replicate_Suc[THEN sym] exp_ind del: replicate_Suc)
done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start_in_middle m lm (b, Bk # a # lista)\<rbrakk>
+lemma wprepare_loop_goon_on_rightbmost_Bk_False_2[simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start_in_middle m lm (b, Bk # a # lista)\<rbrakk>
\<Longrightarrow> wprepare_loop_goon_on_rightmost m lm (Bk # b, a # lista) = False"
apply(simp add: wprepare_loop_start_in_middle.simps
wprepare_loop_goon_on_rightmost.simps, auto)
apply(case_tac mr, simp_all add: )
apply(case_tac "lm1::nat list", simp_all, case_tac list, simp)
-apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv )
+apply(simp add: tape_of_list_def tape_of_nat_list.simps tape_of_nat_def )
apply(case_tac [!] rna, simp_all add: )
apply(case_tac mr, simp_all add: )
apply(case_tac lm1, simp, case_tac list, simp)
-apply(simp_all add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
+apply(simp_all add: tape_of_list_def tape_of_nat_list.simps tape_of_nat_def)
done
-lemma [simp]:
+lemma wprepare_loop_goon_in_middle_Bk_False3[simp]:
"\<lbrakk>lm \<noteq> []; wprepare_loop_start_in_middle m lm (b, Bk # a # lista)\<rbrakk>
\<Longrightarrow> wprepare_loop_goon_in_middle m lm (Bk # b, a # lista)"
apply(simp add: wprepare_loop_start_in_middle.simps
@@ -3125,10 +2744,10 @@
apply(case_tac lm1, simp)
apply(rule_tac x = "Suc aa" in exI, simp)
apply(rule_tac x = list in exI)
-apply(case_tac list, simp_all add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
+apply(case_tac list, simp_all add: tape_of_list_def tape_of_nat_def)
done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start m lm (b, Bk # a # lista)\<rbrakk> \<Longrightarrow>
+lemma wprepare_loop_goon_Bk2[simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start m lm (b, Bk # a # lista)\<rbrakk> \<Longrightarrow>
wprepare_loop_goon m lm (Bk # b, a # lista)"
apply(simp add: wprepare_loop_start.simps
wprepare_loop_goon.simps)
@@ -3148,20 +2767,16 @@
(hd b \<noteq> Oc \<longrightarrow> (b = [] \<longrightarrow> wprepare_add_one m lm ([], Bk # Oc # list)) \<and>
(b \<noteq> [] \<longrightarrow> wprepare_add_one m lm (tl b, hd b # Oc # list)))"
apply(simp only: wprepare_add_one.simps, auto)
-done
-
-lemma [simp]: "wprepare_loop_start m lm (b, Oc # list) \<Longrightarrow> b \<noteq> []"
-apply(simp)
-done
-
-lemma [simp]: "wprepare_loop_start_on_rightmost m lm (b, Oc # list) \<Longrightarrow>
+ done
+
+lemma wprepare_loop_start_on_rightmost_Oc[simp]: "wprepare_loop_start_on_rightmost m lm (b, Oc # list) \<Longrightarrow>
wprepare_loop_start_on_rightmost m lm (Oc # b, list)"
apply(simp add: wprepare_loop_start_on_rightmost.simps, auto)
apply(rule_tac x = rn in exI, auto)
apply(case_tac mr, simp_all add: )
done
-lemma [simp]: "wprepare_loop_start_in_middle m lm (b, Oc # list) \<Longrightarrow>
+lemma wprepare_loop_start_in_middle_Oc[simp]: "wprepare_loop_start_in_middle m lm (b, Oc # list) \<Longrightarrow>
wprepare_loop_start_in_middle m lm (Oc # b, list)"
apply(simp add: wprepare_loop_start_in_middle.simps, auto)
apply(rule_tac x = rn in exI, auto)
@@ -3176,18 +2791,18 @@
apply(erule_tac disjE, simp_all )
done
-lemma [simp]: "wprepare_loop_goon m lm (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+lemma wprepare_loop_goon_Oc_nonempty[simp]: "wprepare_loop_goon m lm (b, Oc # list) \<Longrightarrow> b \<noteq> []"
apply(simp add: wprepare_loop_goon.simps
wprepare_loop_goon_in_middle.simps
wprepare_loop_goon_on_rightmost.simps)
apply(auto)
done
-lemma [simp]: "wprepare_goto_start_pos m lm (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+lemma wprepare_goto_start_pos_Oc_nonempty[simp]: "wprepare_goto_start_pos m lm (b, Oc # list) \<Longrightarrow> b \<noteq> []"
apply(simp add: wprepare_goto_start_pos.simps)
done
-lemma [simp]: "wprepare_loop_goon_on_rightmost m lm (b, Oc # list) = False"
+lemma wprepare_loop_goon_on_rightmost_Oc_False[simp]: "wprepare_loop_goon_on_rightmost m lm (b, Oc # list) = False"
apply(simp add: wprepare_loop_goon_on_rightmost.simps)
done
@@ -3209,26 +2824,26 @@
apply(rule_tac x = "a#lista" in exI, simp)
done
-lemma [simp]: "wprepare_loop_goon_in_middle m lm (b, Oc # list) \<Longrightarrow>
+lemma wprepare_loop_goon_in_middle_cases[simp]: "wprepare_loop_goon_in_middle m lm (b, Oc # list) \<Longrightarrow>
wprepare_loop_start_on_rightmost m lm (Oc # b, list) \<or>
wprepare_loop_start_in_middle m lm (Oc # b, list)"
apply(simp add: wprepare_loop_goon_in_middle.simps split: if_splits)
apply(case_tac lm1, simp_all add: wprepare_loop1 wprepare_loop2)
done
-lemma [simp]: "wprepare_loop_goon m lm (b, Oc # list)
+lemma wprepare_loop_start_Oc[simp]: "wprepare_loop_goon m lm (b, Oc # list)
\<Longrightarrow> wprepare_loop_start m lm (Oc # b, list)"
apply(simp add: wprepare_loop_goon.simps
wprepare_loop_start.simps)
done
-lemma [simp]: "wprepare_add_one m lm (b, Oc # list)
+lemma wprepare_add_one_b[simp]: "wprepare_add_one m lm (b, Oc # list)
\<Longrightarrow> b = [] \<longrightarrow> wprepare_add_one m lm ([], Bk # Oc # list)"
apply(auto)
apply(simp add: wprepare_add_one.simps)
done
-lemma [simp]: "wprepare_goto_start_pos m [a] (b, Oc # list)
+lemma wprepare_loop_start_on_rightmost_Oc2[simp]: "wprepare_goto_start_pos m [a] (b, Oc # list)
\<Longrightarrow> wprepare_loop_start_on_rightmost m [a] (Oc # b, list) "
apply(auto simp: wprepare_goto_start_pos.simps
wprepare_loop_start_on_rightmost.simps)
@@ -3236,7 +2851,7 @@
apply(simp add: replicate_Suc[THEN sym] exp_ind del: replicate_Suc)
done
-lemma [simp]: "wprepare_goto_start_pos m (a # aa # listaa) (b, Oc # list)
+lemma wprepare_loop_start_in_middle_2_Oc[simp]: "wprepare_goto_start_pos m (a # aa # listaa) (b, Oc # list)
\<Longrightarrow>wprepare_loop_start_in_middle m (a # aa # listaa) (Oc # b, list)"
apply(auto simp: wprepare_goto_start_pos.simps
wprepare_loop_start_in_middle.simps)
@@ -3246,20 +2861,20 @@
apply(simp add: tape_of_nl_cons)
done
-lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_goto_start_pos m lm (b, Oc # list)\<rbrakk>
+lemma wprepare_loop_start_Oc2[simp]: "\<lbrakk>lm \<noteq> []; wprepare_goto_start_pos m lm (b, Oc # list)\<rbrakk>
\<Longrightarrow> wprepare_loop_start m lm (Oc # b, list)"
apply(case_tac lm, simp_all)
apply(case_tac lista, simp_all add: wprepare_loop_start.simps)
done
-lemma [simp]: "wprepare_add_one2 m lm (b, Oc # list) \<Longrightarrow> b \<noteq> []"
+lemma wprepare_add_one2_Oc_nonempty[simp]: "wprepare_add_one2 m lm (b, Oc # list) \<Longrightarrow> b \<noteq> []"
apply(auto simp: wprepare_add_one2.simps)
done
lemma add_one_2_stop:
"wprepare_add_one2 m lm (b, Oc # list)
\<Longrightarrow> wprepare_stop m lm (tl b, hd b # Oc # list)"
-apply(simp add: wprepare_stop.simps wprepare_add_one2.simps)
+apply(simp add: wprepare_add_one2.simps)
done
declare wprepare_stop.simps[simp del]
@@ -3285,7 +2900,7 @@
simp add: step_red step.simps)
apply(case_tac c, simp, case_tac [2] aa)
apply(simp_all add: wprepare_inv.simps wcode_prepare_le_def lex_triple_def lex_pair_def
- split: if_splits)
+ split: if_splits) (* slow *)
apply(simp_all add: start_2_goon start_2_start
add_one_2_add_one add_one_2_stop)
apply(auto simp: wprepare_add_one2.simps)
@@ -3304,35 +2919,33 @@
done
qed
-lemma [intro]: "tm_wf (t_wcode_prepare, 0)"
+lemma tm_wf_t_wcode_prepare[intro]: "tm_wf (t_wcode_prepare, 0)"
apply(simp add:tm_wf.simps t_wcode_prepare_def)
-done
-
-lemma t_correct_shift:
- "list_all (\<lambda>(acn, st). (st \<le> y)) tp \<Longrightarrow>
- list_all (\<lambda>(acn, st). (st \<le> y + off)) (shift tp off) "
-apply(auto simp: List.list_all_length)
-apply(erule_tac x = n in allE, simp add: length_shift)
-apply(case_tac "tp!n", auto simp: shift.simps)
-done
-
-lemma [intro]: "(28 + (length t_twice_compile + length t_fourtimes_compile)) mod 2 = 0"
-apply(auto simp: t_twice_compile_def t_fourtimes_compile_def)
-by arith
-
-lemma [elim]: "(a, b) \<in> set t_wcode_main_first_part \<Longrightarrow>
+ done
+
+lemma is_28_even[intro]: "(28 + (length t_twice_compile + length t_fourtimes_compile)) mod 2 = 0"
+ by(auto simp: t_twice_compile_def t_fourtimes_compile_def)
+
+lemma b_le_28[elim]: "(a, b) \<in> set t_wcode_main_first_part \<Longrightarrow>
b \<le> (28 + (length t_twice_compile + length t_fourtimes_compile)) div 2"
apply(auto simp: t_wcode_main_first_part_def t_twice_def)
done
-lemma tm_wf_change_termi: "tm_wf (tp, 0) \<Longrightarrow>
- list_all (\<lambda>(acn, st). (st \<le> Suc (length tp div 2))) (adjust0 tp)"
-apply(auto simp: tm_wf.simps List.list_all_length)
-apply(case_tac "tp!n", auto simp: adjust.simps split: if_splits)
-apply(erule_tac x = "(a, b)" in ballE, auto)
-by (metis in_set_conv_nth)
+lemma tm_wf_change_termi:
+ assumes "tm_wf (tp, 0)"
+ shows "list_all (\<lambda>(acn, st). (st \<le> Suc (length tp div 2))) (adjust0 tp)"
+proof -
+ { fix acn st n
+ assume "tp ! n = (acn, st)" "n < length tp" "0 < st"
+ hence "(acn, st)\<in>set tp" by (metis nth_mem)
+ with assms tm_wf.simps have "st \<le> length tp div 2 + 0" by auto
+ hence "st \<le> Suc (length tp div 2)" by auto
+ }
+ thus ?thesis
+ by(auto simp: tm_wf.simps List.list_all_length adjust.simps split: if_splits prod.split)
+qed
lemma tm_wf_shift:
"list_all (\<lambda>(acn, st). (st \<le> y)) tp \<Longrightarrow>
@@ -3344,11 +2957,11 @@
declare length_tp'[simp del]
-lemma [simp]: "length (mopup (Suc 0)) = 16"
+lemma length_mopup_1[simp]: "length (mopup (Suc 0)) = 16"
apply(auto simp: mopup.simps)
done
-lemma [elim]: "(a, b) \<in> set (shift (adjust0 t_twice_compile) 12) \<Longrightarrow>
+lemma twice_plus_28_elim[elim]: "(a, b) \<in> set (shift (adjust0 t_twice_compile) 12) \<Longrightarrow>
b \<le> (28 + (length t_twice_compile + length t_fourtimes_compile)) div 2"
apply(simp add: t_twice_compile_def t_fourtimes_compile_def)
proof -
@@ -3364,8 +2977,11 @@
ultimately have "list_all (\<lambda>(acn, st). (st \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2))
(shift (adjust0 t_twice_compile) 12)"
proof(auto simp add: mod_ex1 del: adjust.simps)
- fix q qa
- assume h: "length (tm_of abc_twice) = 2 * q" "length (tm_of abc_fourtimes) = 2 * qa"
+ assume "even (length (tm_of abc_twice))"
+ then obtain q where q:"length (tm_of abc_twice) = 2 * q" by auto
+ assume "even (length (tm_of abc_fourtimes))"
+ then obtain qa where qa:"length (tm_of abc_fourtimes) = 2 * qa" by auto
+ note h = q qa
hence "list_all (\<lambda>(acn, st). st \<le> (18 + (q + qa)) + 12) (shift (adjust0 t_twice_compile) 12)"
proof(rule_tac tm_wf_shift t_twice_compile_def)
have "list_all (\<lambda>(acn, st). st \<le> Suc (length t_twice_compile div 2)) (adjust0 t_twice_compile)"
@@ -3375,9 +2991,8 @@
apply(simp add: t_twice_compile_def, auto simp: List.list_all_length)
done
qed
- thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa))
- (shift
- (adjust t_twice_compile (Suc (length t_twice_compile div 2))) 12)"
+ thus "list_all (\<lambda>(acn, st). st \<le> 30 + (length (tm_of abc_twice) div 2 + length (tm_of abc_fourtimes) div 2))
+ (shift (adjust0 t_twice_compile) 12)" using h
by simp
qed
thus "b \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2"
@@ -3388,25 +3003,26 @@
done
qed
-lemma [elim]: "(a, b) \<in> set (shift (adjust0 t_fourtimes_compile) (t_twice_len + 13))
+lemma length_plus_28_elim2[elim]: "(a, b) \<in> set (shift (adjust0 t_fourtimes_compile) (t_twice_len + 13))
\<Longrightarrow> b \<le> (28 + (length t_twice_compile + length t_fourtimes_compile)) div 2"
apply(simp add: t_twice_compile_def t_fourtimes_compile_def t_twice_len_def)
proof -
assume g: "(a, b)
\<in> set (shift
- (adjust
- (tm_of abc_fourtimes @
- shift (mopup (Suc 0)) (length (tm_of abc_fourtimes) div 2))
- (Suc ((length (tm_of abc_fourtimes) + 16) div 2)))
- (length t_twice div 2 + 13))"
+ (adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) (length (tm_of abc_fourtimes) div 2))
+ (Suc ((length (tm_of abc_fourtimes) + 16) div 2)))
+ (length t_twice div 2 + 13))"
moreover have "length (tm_of abc_twice) mod 2 = 0" by auto
moreover have "length (tm_of abc_fourtimes) mod 2 = 0" by auto
ultimately have "list_all (\<lambda>(acn, st). (st \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2))
(shift (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0))
(length (tm_of abc_fourtimes) div 2))) (length t_twice div 2 + 13))"
proof(auto simp: mod_ex1 t_twice_def t_twice_compile_def)
- fix q qa
- assume h: "length (tm_of abc_twice) = 2 * q" "length (tm_of abc_fourtimes) = 2 * qa"
+ assume "even (length (tm_of abc_twice))"
+ then obtain q where q:"length (tm_of abc_twice) = 2 * q" by auto
+ assume "even (length (tm_of abc_fourtimes))"
+ then obtain qa where qa:"length (tm_of abc_fourtimes) = 2 * qa" by auto
+ note h = q qa
hence "list_all (\<lambda>(acn, st). st \<le> (9 + qa + (21 + q)))
(shift (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)) (21 + q))"
proof(rule_tac tm_wf_shift t_twice_compile_def)
@@ -3424,11 +3040,12 @@
apply(simp)
done
qed
- thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa))
- (shift
- (adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)
- (9 + qa))
- (21 + q))"
+ thus "list_all
+ (\<lambda>(acn, st). st \<le> 30 + (length (tm_of abc_twice) div 2 + length (tm_of abc_fourtimes) div 2))
+ (shift
+ (adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) (length (tm_of abc_fourtimes) div 2))
+ (9 + length (tm_of abc_fourtimes) div 2))
+ (21 + length (tm_of abc_twice) div 2))"
apply(subgoal_tac "qa + q = q + qa")
apply(simp add: h)
apply(simp)
@@ -3441,20 +3058,14 @@
done
qed
-lemma [intro]: "tm_wf (t_wcode_main, 0)"
-apply(auto simp: t_wcode_main_def tm_wf.simps
+lemma tm_wf_t_wcode_main[intro]: "tm_wf (t_wcode_main, 0)"
+by(auto simp: t_wcode_main_def tm_wf.simps
t_twice_def t_fourtimes_def del: List.list_all_iff)
-done
declare tm_comp.simps[simp del]
lemma tm_wf_comp: "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)"
-apply(auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length
- tm_comp.simps)
-done
-
-lemma [intro]: "tm_wf (t_wcode_prepare |+| t_wcode_main, 0)"
-apply(rule_tac tm_wf_comp, auto)
-done
+ by(auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length
+ tm_comp.simps) auto
lemma prepare_mainpart_lemma:
"args \<noteq> [] \<Longrightarrow>
@@ -3517,40 +3128,32 @@
where
"tinres xs ys = (\<exists>n. xs = ys @ Bk \<up> n \<or> ys = xs @ Bk \<up> n)"
-lemma [simp]: "tinres r r' \<Longrightarrow>
+lemma tinres_fetch_congr[simp]: "tinres r r' \<Longrightarrow>
fetch t ss (read r) =
fetch t ss (read r')"
apply(simp add: fetch.simps, auto split: if_splits simp: tinres_def)
apply(case_tac [!] n, simp_all)
done
-lemma [intro]: "\<exists> n. (a::cell)\<up>(n) = []"
-by auto
-
-lemma [simp]: "\<lbrakk>tinres r r'; r \<noteq> []; r' \<noteq> []\<rbrakk> \<Longrightarrow> hd r = hd r'"
+lemma nonempty_hd_tinres[simp]: "\<lbrakk>tinres r r'; r \<noteq> []; r' \<noteq> []\<rbrakk> \<Longrightarrow> hd r = hd r'"
apply(auto simp: tinres_def)
done
-lemma [intro]: "hd (Bk\<up>(Suc n)) = Bk"
-apply(simp add: )
-done
-
-lemma [simp]: "\<lbrakk>tinres r []; r \<noteq> []\<rbrakk> \<Longrightarrow> hd r = Bk"
-apply(auto simp: tinres_def)
-done
-
-lemma [simp]: "\<lbrakk>tinres [] r'; r' \<noteq> []\<rbrakk> \<Longrightarrow> hd r' = Bk"
-apply(auto simp: tinres_def)
-done
-
-lemma [intro]: "\<exists>na. tl r = tl (r @ Bk\<up>(n)) @ Bk\<up>(na) \<or> tl (r @ Bk\<up>(n)) = tl r @ Bk\<up>(na)"
+lemma tinres_nonempty[simp]:
+ "\<lbrakk>tinres r []; r \<noteq> []\<rbrakk> \<Longrightarrow> hd r = Bk"
+ "\<lbrakk>tinres [] r'; r' \<noteq> []\<rbrakk> \<Longrightarrow> hd r' = Bk"
+ "\<lbrakk>tinres r []; r \<noteq> []\<rbrakk> \<Longrightarrow> tinres (tl r) []"
+ "tinres r r' \<Longrightarrow> tinres (b # r) (b # r')"
+ by(auto simp: tinres_def)
+
+lemma ex_move_tl[intro]: "\<exists>na. tl r = tl (r @ Bk\<up>(n)) @ Bk\<up>(na) \<or> tl (r @ Bk\<up>(n)) = tl r @ Bk\<up>(na)"
apply(case_tac r, simp)
apply(case_tac n, simp, simp)
apply(rule_tac x = nat in exI, simp)
apply(rule_tac x = n in exI, simp)
done
-lemma [simp]: "tinres r r' \<Longrightarrow> tinres (tl r) (tl r')"
+lemma tinres_tails[simp]: "tinres r r' \<Longrightarrow> tinres (tl r) (tl r')"
apply(auto simp: tinres_def)
apply(case_tac r', simp)
apply(case_tac n, simp_all)
@@ -3558,39 +3161,22 @@
apply(rule_tac x = n in exI, simp)
done
-lemma [simp]: "\<lbrakk>tinres r []; r \<noteq> []\<rbrakk> \<Longrightarrow> tinres (tl r) []"
-apply(case_tac r, auto simp: tinres_def)
-apply(case_tac n, simp_all add: )
-apply(rule_tac x = nat in exI, simp)
-done
-
-lemma [simp]: "\<lbrakk>tinres [] r'\<rbrakk> \<Longrightarrow> tinres [] (tl r')"
-apply(case_tac r', auto simp: tinres_def)
-apply(case_tac n, simp_all add: )
-apply(rule_tac x = nat in exI, simp)
-done
-
-lemma [simp]: "tinres r r' \<Longrightarrow> tinres (b # r) (b # r')"
-apply(auto simp: tinres_def)
-done
-
-lemma [simp]: "tinres r [] \<Longrightarrow> tinres (Bk # tl r) [Bk]"
-apply(auto simp: tinres_def)
-done
-
-lemma [simp]: "tinres r [] \<Longrightarrow> tinres (Oc # tl r) [Oc]"
-apply(auto simp: tinres_def)
-done
-
-lemma tinres_step2:
- "\<lbrakk>tinres r r'; step0 (ss, l, r) t = (sa, la, ra); step0 (ss, l, r') t = (sb, lb, rb)\<rbrakk>
- \<Longrightarrow> la = lb \<and> tinres ra rb \<and> sa = sb"
-apply(case_tac "ss = 0", simp add: step_0)
-apply(simp add: step.simps [simp del], auto)
-apply(case_tac [!] "fetch t ss (read r')", simp)
-apply(auto simp: update.simps)
-apply(case_tac [!] a, auto split: if_splits)
-done
+lemma tinres_empty[simp]:
+ "\<lbrakk>tinres [] r'\<rbrakk> \<Longrightarrow> tinres [] (tl r')"
+ "tinres r [] \<Longrightarrow> tinres (Bk # tl r) [Bk]"
+ "tinres r [] \<Longrightarrow> tinres (Oc # tl r) [Oc]"
+ by(auto simp: tinres_def)
+
+lemma tinres_step2:
+ assumes "tinres r r'" "step0 (ss, l, r) t = (sa, la, ra)" "step0 (ss, l, r') t = (sb, lb, rb)"
+ shows "la = lb \<and> tinres ra rb \<and> sa = sb"
+proof (cases "fetch t ss (read r')")
+ case (Pair a b)
+ have sa:"sa = sb" using assms Pair by(force simp: step.simps)
+ have "la = lb \<and> tinres ra rb" using assms Pair
+ by(cases a, auto simp: step.simps split: if_splits)
+ thus ?thesis using sa by auto
+qed
lemma tinres_steps2:
"\<lbrakk>tinres r r'; steps0 (ss, l, r) t stp = (sa, la, ra); steps0 (ss, l, r') t stp = (sb, lb, rb)\<rbrakk>
@@ -3624,85 +3210,29 @@
(W1, 2), (Nop, 7), (L, 9), (W0, 8), (L, 9), (L, 10),
(L, 11), (L, 10), (R, 0), (L, 11)]"
-lemma [simp]: "fetch t_wcode_adjust (Suc 0) Bk = (W1, 1)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps)
-done
-
-lemma [simp]: "fetch t_wcode_adjust (Suc 0) Oc = (R, 2)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps)
-done
-
-lemma [simp]: "fetch t_wcode_adjust (Suc (Suc 0)) Oc = (R, 3)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps)
-done
-
-lemma [simp]: "fetch t_wcode_adjust (Suc (Suc (Suc 0))) Oc = (R, 4)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps)
-done
-
-lemma [simp]: "fetch t_wcode_adjust (Suc (Suc (Suc 0))) Bk = (R, 3)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps)
-done
-
-lemma [simp]: "fetch t_wcode_adjust 4 Bk = (L, 8)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_4_eq_4)
-done
-
-lemma [simp]: "fetch t_wcode_adjust 4 Oc = (L, 5)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_4_eq_4)
-done
-
-lemma [simp]: "fetch t_wcode_adjust 5 Oc = (W0, 5)"
-apply(simp only: fetch.simps t_wcode_adjust_def nth_of.simps numeral_5_eq_5, simp)
-done
-
-lemma [simp]: "fetch t_wcode_adjust 5 Bk = (L, 6)"
-apply(simp only: fetch.simps t_wcode_adjust_def nth_of.simps numeral_5_eq_5, auto)
-done
-
-lemma [simp]: "fetch t_wcode_adjust 6 Oc = (R, 7)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_6_eq_6)
-done
-
-lemma [simp]: "fetch t_wcode_adjust 6 Bk = (L, 6)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_6_eq_6)
-done
-
-lemma [simp]: "fetch t_wcode_adjust 7 Bk = (W1, 2)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_7_eq_7)
-done
-
-lemma [simp]: "fetch t_wcode_adjust 8 Bk = (L, 9)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_8_eq_8)
-done
-
-lemma [simp]: "fetch t_wcode_adjust 8 Oc = (W0, 8)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_8_eq_8)
-done
-
-lemma [simp]: "fetch t_wcode_adjust 9 Oc = (L, 10)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_9_eq_9)
-done
-
-lemma [simp]: "fetch t_wcode_adjust 9 Bk = (L, 9)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_9_eq_9)
-done
-
-lemma [simp]: "fetch t_wcode_adjust 10 Bk = (L, 11)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_10_eq_10)
-done
-
-lemma [simp]: "fetch t_wcode_adjust 10 Oc = (L, 10)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps eval_nat_numeral)
-done
-
-lemma [simp]: "fetch t_wcode_adjust 11 Oc = (L, 11)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps eval_nat_numeral)
-done
-
-lemma [simp]: "fetch t_wcode_adjust 11 Bk = (R, 0)"
-apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps eval_nat_numeral)
-done
+lemma fetch_t_wcode_adjust[simp]:
+ "fetch t_wcode_adjust (Suc 0) Bk = (W1, 1)"
+ "fetch t_wcode_adjust (Suc 0) Oc = (R, 2)"
+ "fetch t_wcode_adjust (Suc (Suc 0)) Oc = (R, 3)"
+ "fetch t_wcode_adjust (Suc (Suc (Suc 0))) Oc = (R, 4)"
+ "fetch t_wcode_adjust (Suc (Suc (Suc 0))) Bk = (R, 3)"
+ "fetch t_wcode_adjust 4 Bk = (L, 8)"
+ "fetch t_wcode_adjust 4 Oc = (L, 5)"
+ "fetch t_wcode_adjust 5 Oc = (W0, 5)"
+ "fetch t_wcode_adjust 5 Bk = (L, 6)"
+ "fetch t_wcode_adjust 6 Oc = (R, 7)"
+ "fetch t_wcode_adjust 6 Bk = (L, 6)"
+ "fetch t_wcode_adjust 7 Bk = (W1, 2)"
+ "fetch t_wcode_adjust 8 Bk = (L, 9)"
+ "fetch t_wcode_adjust 8 Oc = (W0, 8)"
+ "fetch t_wcode_adjust 9 Oc = (L, 10)"
+ "fetch t_wcode_adjust 9 Bk = (L, 9)"
+ "fetch t_wcode_adjust 10 Bk = (L, 11)"
+ "fetch t_wcode_adjust 10 Oc = (L, 10)"
+ "fetch t_wcode_adjust 11 Oc = (L, 11)"
+ "fetch t_wcode_adjust 11 Bk = (R, 0)"
+by(auto simp: fetch.simps t_wcode_adjust_def nth_of.simps numeral)
+
fun wadjust_start :: "nat \<Rightarrow> nat \<Rightarrow> tape \<Rightarrow> bool"
where
@@ -3913,7 +3443,7 @@
definition wadjust_le :: "((nat \<times> config) \<times> nat \<times> config) set"
where "wadjust_le \<equiv> (inv_image lex_square wadjust_measure)"
-lemma [intro]: "wf lex_square"
+lemma wf_lex_square[intro]: "wf lex_square"
by(auto intro:wf_lex_prod simp: Abacus.lex_pair_def lex_square_def
Abacus.lex_triple_def)
@@ -3921,141 +3451,97 @@
by(auto intro:wf_inv_image simp: wadjust_le_def
Abacus.lex_triple_def Abacus.lex_pair_def)
-lemma [simp]: "wadjust_start m rs (c, []) = False"
+lemma wadjust_start_snd_nonempty[simp]: "wadjust_start m rs (c, []) = False"
apply(auto simp: wadjust_start.simps)
done
-lemma [simp]: "wadjust_loop_right_move m rs (c, []) \<Longrightarrow> c \<noteq> []"
+lemma wadjust_loop_right_move_fst_nonempty[simp]: "wadjust_loop_right_move m rs (c, []) \<Longrightarrow> c \<noteq> []"
apply(auto simp: wadjust_loop_right_move.simps)
done
-lemma [simp]: "wadjust_loop_right_move m rs (c, [])
- \<Longrightarrow> wadjust_loop_check m rs (Bk # c, [])"
-apply(simp only: wadjust_loop_right_move.simps wadjust_loop_check.simps)
-apply(auto)
-done
-
-lemma [simp]: "wadjust_loop_check m rs (c, []) \<Longrightarrow> c \<noteq> []"
+lemma wadjust_loop_check_fst_nonempty[simp]: "wadjust_loop_check m rs (c, []) \<Longrightarrow> c \<noteq> []"
apply(simp only: wadjust_loop_check.simps, auto)
done
-lemma [simp]: "wadjust_loop_start m rs (c, []) = False"
+lemma wadjust_loop_start_snd_nonempty[simp]: "wadjust_loop_start m rs (c, []) = False"
apply(simp add: wadjust_loop_start.simps)
done
-lemma [simp]: "wadjust_loop_right_move m rs (c, []) \<Longrightarrow>
- wadjust_loop_right_move m rs (Bk # c, [])"
-apply(simp only: wadjust_loop_right_move.simps)
-apply(erule_tac exE)+
-apply(auto)
-done
-
-lemma [simp]: "wadjust_loop_check m rs (c, []) \<Longrightarrow> wadjust_erase2 m rs (tl c, [hd c])"
+lemma wadjust_erase2_singleton[simp]: "wadjust_loop_check m rs (c, []) \<Longrightarrow> wadjust_erase2 m rs (tl c, [hd c])"
apply(simp only: wadjust_loop_check.simps wadjust_erase2.simps, auto)
done
-lemma [simp]: " wadjust_loop_erase m rs (c, [])
- \<Longrightarrow> (c = [] \<longrightarrow> wadjust_loop_on_left_moving m rs ([], [Bk])) \<and>
- (c \<noteq> [] \<longrightarrow> wadjust_loop_on_left_moving m rs (tl c, [hd c]))"
-apply(simp add: wadjust_loop_erase.simps)
-done
-
-lemma [simp]: "wadjust_loop_on_left_moving m rs (c, []) = False"
-apply(auto simp: wadjust_loop_on_left_moving.simps)
-done
-
-
-lemma [simp]: "wadjust_loop_right_move2 m rs (c, []) = False"
-apply(auto simp: wadjust_loop_right_move2.simps)
-done
-
-lemma [simp]: "wadjust_erase2 m rs ([], []) = False"
-apply(auto simp: wadjust_erase2.simps)
-done
-
-lemma [simp]: "wadjust_on_left_moving_B m rs
+lemma wadjust_loop_on_left_moving_snd_nonempty[simp]:
+ "wadjust_loop_on_left_moving m rs (c, []) = False"
+"wadjust_loop_right_move2 m rs (c, []) = False"
+"wadjust_erase2 m rs ([], []) = False"
+ by(auto simp: wadjust_loop_on_left_moving.simps
+ wadjust_loop_right_move2.simps
+ wadjust_erase2.simps)
+
+lemma wadjust_on_left_moving_B_Bk1[simp]: "wadjust_on_left_moving_B m rs
(Oc # Oc # Oc\<up>(rs) @ Bk # Oc # Oc\<up>(m), [Bk])"
apply(simp add: wadjust_on_left_moving_B.simps, auto)
done
-lemma [simp]: "wadjust_on_left_moving_B m rs
+lemma wadjust_on_left_moving_B_Bk2[simp]: "wadjust_on_left_moving_B m rs
(Bk\<up>(n) @ Bk # Oc # Oc # Oc\<up>(rs) @ Bk # Oc # Oc\<up>(m), [Bk])"
apply(simp add: wadjust_on_left_moving_B.simps , auto)
apply(rule_tac x = "Suc n" in exI, simp add: exp_ind del: replicate_Suc)
done
-lemma [simp]: "\<lbrakk>wadjust_erase2 m rs (c, []); c \<noteq> []\<rbrakk> \<Longrightarrow>
+lemma wadjust_on_left_moving_singleton[simp]: "\<lbrakk>wadjust_erase2 m rs (c, []); c \<noteq> []\<rbrakk> \<Longrightarrow>
wadjust_on_left_moving m rs (tl c, [hd c])"
apply(simp only: wadjust_erase2.simps)
apply(erule_tac exE)+
apply(case_tac ln, simp_all add: wadjust_on_left_moving.simps)
done
-lemma [simp]: "wadjust_erase2 m rs (c, [])
+lemma wadjust_erase2_cases[simp]: "wadjust_erase2 m rs (c, [])
\<Longrightarrow> (c = [] \<longrightarrow> wadjust_on_left_moving m rs ([], [Bk])) \<and>
(c \<noteq> [] \<longrightarrow> wadjust_on_left_moving m rs (tl c, [hd c]))"
apply(auto)
done
-lemma [simp]: "wadjust_on_left_moving m rs ([], []) = False"
-apply(simp add: wadjust_on_left_moving.simps
+lemma wadjust_on_left_moving_nonempty[simp]:
+ "wadjust_on_left_moving m rs ([], []) = False"
+ "wadjust_on_left_moving_O m rs (c, []) = False"
+apply(auto simp: wadjust_on_left_moving.simps
wadjust_on_left_moving_O.simps wadjust_on_left_moving_B.simps)
done
-lemma [simp]: "wadjust_on_left_moving_O m rs (c, []) = False"
-apply(simp add: wadjust_on_left_moving_O.simps)
-done
-
-lemma [simp]: " \<lbrakk>wadjust_on_left_moving_B m rs (c, []); c \<noteq> []; hd c = Bk\<rbrakk> \<Longrightarrow>
+lemma wadjust_on_left_moving_B_singleton_Bk[simp]:
+ " \<lbrakk>wadjust_on_left_moving_B m rs (c, []); c \<noteq> []; hd c = Bk\<rbrakk> \<Longrightarrow>
wadjust_on_left_moving_B m rs (tl c, [Bk])"
apply(simp add: wadjust_on_left_moving_B.simps, auto)
apply(case_tac [!] ln, simp_all)
done
-lemma [simp]: "\<lbrakk>wadjust_on_left_moving_B m rs (c, []); c \<noteq> []; hd c = Oc\<rbrakk> \<Longrightarrow>
+lemma wadjust_on_left_moving_B_singleton_Oc[simp]:
+ "\<lbrakk>wadjust_on_left_moving_B m rs (c, []); c \<noteq> []; hd c = Oc\<rbrakk> \<Longrightarrow>
wadjust_on_left_moving_O m rs (tl c, [Oc])"
apply(simp add: wadjust_on_left_moving_B.simps wadjust_on_left_moving_O.simps, auto)
apply(case_tac [!] ln, simp_all add: )
-done
-
-lemma [simp]: "\<lbrakk>wadjust_on_left_moving m rs (c, []); c \<noteq> []\<rbrakk> \<Longrightarrow>
+ done
+
+lemma wadjust_on_left_moving_singleton2[simp]:
+ "\<lbrakk>wadjust_on_left_moving m rs (c, []); c \<noteq> []\<rbrakk> \<Longrightarrow>
wadjust_on_left_moving m rs (tl c, [hd c])"
apply(simp add: wadjust_on_left_moving.simps)
apply(case_tac "hd c", simp_all)
done
-lemma [simp]: "wadjust_on_left_moving m rs (c, [])
- \<Longrightarrow> (c = [] \<longrightarrow> wadjust_on_left_moving m rs ([], [Bk])) \<and>
- (c \<noteq> [] \<longrightarrow> wadjust_on_left_moving m rs (tl c, [hd c]))"
-apply(auto)
-done
-
-lemma [simp]: "wadjust_goon_left_moving m rs (c, []) = False"
-apply(auto simp: wadjust_goon_left_moving.simps wadjust_goon_left_moving_B.simps
- wadjust_goon_left_moving_O.simps)
-done
-
-lemma [simp]: "wadjust_backto_standard_pos m rs (c, []) = False"
-apply(auto simp: wadjust_backto_standard_pos.simps
+lemma wadjust_nonempty[simp]: "wadjust_goon_left_moving m rs (c, []) = False"
+"wadjust_backto_standard_pos m rs (c, []) = False"
+ by(auto simp: wadjust_goon_left_moving.simps wadjust_goon_left_moving_B.simps
+ wadjust_goon_left_moving_O.simps wadjust_backto_standard_pos.simps
wadjust_backto_standard_pos_B.simps wadjust_backto_standard_pos_O.simps)
-done
-
-lemma [simp]:
- "wadjust_start m rs (c, Bk # list) \<Longrightarrow>
- (c = [] \<longrightarrow> wadjust_start m rs ([], Oc # list)) \<and>
- (c \<noteq> [] \<longrightarrow> wadjust_start m rs (c, Oc # list))"
-apply(auto simp: wadjust_start.simps)
-done
-
-lemma [simp]: "wadjust_loop_start m rs (c, Bk # list) = False"
+
+lemma wadjust_loop_start_no_Bk[simp]: "wadjust_loop_start m rs (c, Bk # list) = False"
apply(auto simp: wadjust_loop_start.simps)
done
-lemma [simp]: "wadjust_loop_right_move m rs (c, b) \<Longrightarrow> c \<noteq> []"
-apply(simp only: wadjust_loop_right_move.simps, auto)
-done
-
-lemma [simp]: "wadjust_loop_right_move m rs (c, Bk # list)
+lemma wadjust_loop_right_move_Bk[simp]: "wadjust_loop_right_move m rs (c, Bk # list)
\<Longrightarrow> wadjust_loop_right_move m rs (Bk # c, list)"
apply(simp only: wadjust_loop_right_move.simps)
apply(erule_tac exE)+
@@ -4066,24 +3552,20 @@
apply(rule_tac x = nat in exI, auto)
done
-lemma [simp]: "wadjust_loop_check m rs (c, b) \<Longrightarrow> c \<noteq> []"
+lemma wadjust_loop_check_nonempty[simp]: "wadjust_loop_check m rs (c, b) \<Longrightarrow> c \<noteq> []"
apply(simp only: wadjust_loop_check.simps, auto)
done
-lemma [simp]: "wadjust_loop_check m rs (c, Bk # list)
+lemma wadjust_erase2_via_loop_check_Bk[simp]: "wadjust_loop_check m rs (c, Bk # list)
\<Longrightarrow> wadjust_erase2 m rs (tl c, hd c # Bk # list)"
apply(auto simp: wadjust_loop_check.simps wadjust_erase2.simps)
apply(case_tac [!] mr, simp_all)
done
-lemma [simp]: "wadjust_loop_erase m rs (c, b) \<Longrightarrow> c \<noteq> []"
-apply(simp only: wadjust_loop_erase.simps, auto)
-done
-
declare wadjust_loop_on_left_moving_O.simps[simp del]
wadjust_loop_on_left_moving_B.simps[simp del]
-lemma [simp]: "\<lbrakk>wadjust_loop_erase m rs (c, Bk # list); hd c = Bk\<rbrakk>
+lemma wadjust_loop_on_left_moving_B_via_erase[simp]: "\<lbrakk>wadjust_loop_erase m rs (c, Bk # list); hd c = Bk\<rbrakk>
\<Longrightarrow> wadjust_loop_on_left_moving_B m rs (tl c, Bk # Bk # list)"
apply(simp only: wadjust_loop_erase.simps
wadjust_loop_on_left_moving_B.simps)
@@ -4094,28 +3576,22 @@
apply(simp add: exp_ind [THEN sym])
done
-lemma [simp]: "\<lbrakk>wadjust_loop_erase m rs (c, Bk # list); c \<noteq> []; hd c = Oc\<rbrakk> \<Longrightarrow>
+lemma wadjust_loop_on_left_moving_O_Bk_via_erase[simp]:
+ "\<lbrakk>wadjust_loop_erase m rs (c, Bk # list); c \<noteq> []; hd c = Oc\<rbrakk> \<Longrightarrow>
wadjust_loop_on_left_moving_O m rs (tl c, Oc # Bk # list)"
apply(simp only: wadjust_loop_erase.simps wadjust_loop_on_left_moving_O.simps,
auto)
apply(case_tac [!] ln, simp_all add: )
done
-lemma [simp]: "\<lbrakk>wadjust_loop_erase m rs (c, Bk # list); c \<noteq> []\<rbrakk> \<Longrightarrow>
+lemma wadjust_loop_on_left_moving_Bk_via_erase[simp]: "\<lbrakk>wadjust_loop_erase m rs (c, Bk # list); c \<noteq> []\<rbrakk> \<Longrightarrow>
wadjust_loop_on_left_moving m rs (tl c, hd c # Bk # list)"
apply(case_tac "hd c", simp_all add:wadjust_loop_on_left_moving.simps)
done
-lemma [simp]: "wadjust_loop_on_left_moving m rs (c, b) \<Longrightarrow> c \<noteq> []"
-apply(simp add: wadjust_loop_on_left_moving.simps
-wadjust_loop_on_left_moving_O.simps wadjust_loop_on_left_moving_B.simps, auto)
-done
-
-lemma [simp]: "wadjust_loop_on_left_moving_O m rs (c, Bk # list) = False"
-apply(simp add: wadjust_loop_on_left_moving_O.simps)
-done
-
-lemma [simp]: "\<lbrakk>wadjust_loop_on_left_moving_B m rs (c, Bk # list); hd c = Bk\<rbrakk>
+
+lemma wadjust_loop_on_left_moving_B_Bk_move[simp]:
+ "\<lbrakk>wadjust_loop_on_left_moving_B m rs (c, Bk # list); hd c = Bk\<rbrakk>
\<Longrightarrow> wadjust_loop_on_left_moving_B m rs (tl c, Bk # Bk # list)"
apply(simp only: wadjust_loop_on_left_moving_B.simps)
apply(erule_tac exE)+
@@ -4124,7 +3600,8 @@
apply(rule_tac x = "Suc nr" in exI, auto simp: )
done
-lemma [simp]: "\<lbrakk>wadjust_loop_on_left_moving_B m rs (c, Bk # list); hd c = Oc\<rbrakk>
+lemma wadjust_loop_on_left_moving_O_Oc_move[simp]:
+ "\<lbrakk>wadjust_loop_on_left_moving_B m rs (c, Bk # list); hd c = Oc\<rbrakk>
\<Longrightarrow> wadjust_loop_on_left_moving_O m rs (tl c, Oc # Bk # list)"
apply(simp only: wadjust_loop_on_left_moving_O.simps
wadjust_loop_on_left_moving_B.simps)
@@ -4133,17 +3610,35 @@
apply(case_tac nl, simp_all add: , auto)
done
-lemma [simp]: "wadjust_loop_on_left_moving m rs (c, Bk # list)
+lemma wadjust_loop_on_left_moving_O_noBk[simp]:
+ "wadjust_loop_on_left_moving_O m rs (c, Bk # list) = False"
+apply(simp add: wadjust_loop_on_left_moving_O.simps)
+done
+lemma wadjust_loop_on_left_moving_Bk_move[simp]:
+ "wadjust_loop_on_left_moving m rs (c, Bk # list)
\<Longrightarrow> wadjust_loop_on_left_moving m rs (tl c, hd c # Bk # list)"
apply(simp add: wadjust_loop_on_left_moving.simps)
apply(case_tac "hd c", simp_all)
done
-lemma [simp]: "wadjust_loop_right_move2 m rs (c, b) \<Longrightarrow> c \<noteq> []"
-apply(simp only: wadjust_loop_right_move2.simps, auto)
-done
-
-lemma [simp]: "wadjust_loop_right_move2 m rs (c, Bk # list) \<Longrightarrow> wadjust_loop_start m rs (c, Oc # list)"
+lemma wadjust_loop_erase_nonempty[simp]: "wadjust_loop_erase m rs (c, b) \<Longrightarrow> c \<noteq> []"
+"wadjust_loop_on_left_moving m rs (c, b) \<Longrightarrow> c \<noteq> []"
+"wadjust_loop_right_move2 m rs (c, b) \<Longrightarrow> c \<noteq> []"
+"wadjust_erase2 m rs (c, Bk # list) \<Longrightarrow> c \<noteq> []"
+"wadjust_on_left_moving m rs (c,b) \<Longrightarrow> c \<noteq> []"
+"wadjust_on_left_moving_O m rs (c, Bk # list) = False"
+"wadjust_goon_left_moving m rs (c, b) \<Longrightarrow> c \<noteq> []"
+ by(auto simp: wadjust_loop_erase.simps wadjust_loop_on_left_moving.simps
+ wadjust_loop_on_left_moving_O.simps wadjust_loop_on_left_moving_B.simps
+ wadjust_loop_right_move2.simps wadjust_erase2.simps
+ wadjust_on_left_moving.simps
+ wadjust_on_left_moving_O.simps
+ wadjust_on_left_moving_B.simps wadjust_goon_left_moving.simps
+ wadjust_goon_left_moving_B.simps
+ wadjust_goon_left_moving_O.simps)
+
+lemma wadjust_loop_start_Oc_via_Bk_move[simp]:
+"wadjust_loop_right_move2 m rs (c, Bk # list) \<Longrightarrow> wadjust_loop_start m rs (c, Oc # list)"
apply(auto simp: wadjust_loop_right_move2.simps wadjust_loop_start.simps)
apply(case_tac ln, simp_all add: )
apply(rule_tac x = 0 in exI, simp)
@@ -4152,13 +3647,9 @@
apply(rule_tac x = "Suc nat" in exI, simp add: exp_ind del: replicate_Suc)
apply(rule_tac x = rn in exI, auto)
apply(rule_tac x = "Suc ml" in exI, auto )
-done
-
-lemma [simp]: "wadjust_erase2 m rs (c, Bk # list) \<Longrightarrow> c \<noteq> []"
-apply(auto simp:wadjust_erase2.simps )
-done
-
-lemma [simp]: "wadjust_erase2 m rs (c, Bk # list) \<Longrightarrow>
+ done
+
+lemma wadjust_on_left_moving_Bk_via_erase[simp]: "wadjust_erase2 m rs (c, Bk # list) \<Longrightarrow>
wadjust_on_left_moving m rs (tl c, hd c # Bk # list)"
apply(auto simp: wadjust_erase2.simps)
apply(case_tac ln, simp_all add: wadjust_on_left_moving.simps
@@ -4167,88 +3658,39 @@
apply(rule_tac x = "(Suc (Suc rn))" in exI, simp add: )
apply(rule_tac x = "Suc nat" in exI, simp add: exp_ind del: replicate_Suc)
apply(rule_tac x = "(Suc (Suc rn))" in exI, simp add: )
-done
-
-lemma [simp]: "wadjust_on_left_moving m rs (c,b) \<Longrightarrow> c \<noteq> []"
-apply(simp only:wadjust_on_left_moving.simps
- wadjust_on_left_moving_O.simps
- wadjust_on_left_moving_B.simps
- , auto)
-done
-
-lemma [simp]: "wadjust_on_left_moving_O m rs (c, Bk # list) = False"
-apply(simp add: wadjust_on_left_moving_O.simps)
-done
-
-lemma [simp]: "\<lbrakk>wadjust_on_left_moving_B m rs (c, Bk # list); hd c = Bk\<rbrakk>
+ done
+
+
+lemma wadjust_on_left_moving_B_Bk_drop_one: "\<lbrakk>wadjust_on_left_moving_B m rs (c, Bk # list); hd c = Bk\<rbrakk>
\<Longrightarrow> wadjust_on_left_moving_B m rs (tl c, Bk # Bk # list)"
apply(auto simp: wadjust_on_left_moving_B.simps)
apply(case_tac ln, simp_all)
done
-lemma [simp]: "\<lbrakk>wadjust_on_left_moving_B m rs (c, Bk # list); hd c = Oc\<rbrakk>
+lemma wadjust_on_left_moving_B_Bk_drop_Oc: "\<lbrakk>wadjust_on_left_moving_B m rs (c, Bk # list); hd c = Oc\<rbrakk>
\<Longrightarrow> wadjust_on_left_moving_O m rs (tl c, Oc # Bk # list)"
apply(auto simp: wadjust_on_left_moving_O.simps
wadjust_on_left_moving_B.simps)
apply(case_tac ln, simp_all add: )
done
-lemma [simp]: "wadjust_on_left_moving m rs (c, Bk # list) \<Longrightarrow>
+lemma wadjust_on_left_moving_B_drop[simp]: "wadjust_on_left_moving m rs (c, Bk # list) \<Longrightarrow>
wadjust_on_left_moving m rs (tl c, hd c # Bk # list)"
-apply(simp add: wadjust_on_left_moving.simps)
-apply(case_tac "hd c", simp_all)
-done
-
-lemma [simp]: "wadjust_goon_left_moving m rs (c, b) \<Longrightarrow> c \<noteq> []"
-apply(simp add: wadjust_goon_left_moving.simps
- wadjust_goon_left_moving_B.simps
- wadjust_goon_left_moving_O.simps , auto)
-done
-
-lemma [simp]: "wadjust_goon_left_moving_O m rs (c, Bk # list) = False"
+ by(cases "hd c", auto simp:wadjust_on_left_moving.simps wadjust_on_left_moving_B_Bk_drop_one
+ wadjust_on_left_moving_B_Bk_drop_Oc)
+
+lemma wadjust_goon_left_moving_O_no_Bk[simp]: "wadjust_goon_left_moving_O m rs (c, Bk # list) = False"
apply(simp add: wadjust_goon_left_moving_O.simps, auto)
apply(case_tac mr, simp_all add: )
done
-lemma [simp]: "\<lbrakk>wadjust_goon_left_moving_B m rs (c, Bk # list); hd c = Bk\<rbrakk>
- \<Longrightarrow> wadjust_backto_standard_pos_B m rs (tl c, Bk # Bk # list)"
-apply(auto simp: wadjust_goon_left_moving_B.simps
- wadjust_backto_standard_pos_B.simps )
-done
-
-lemma [simp]: "\<lbrakk>wadjust_goon_left_moving_B m rs (c, Bk # list); hd c = Oc\<rbrakk>
- \<Longrightarrow> wadjust_backto_standard_pos_O m rs (tl c, Oc # Bk # list)"
-apply(auto simp: wadjust_goon_left_moving_B.simps
- wadjust_backto_standard_pos_O.simps)
-done
-
-lemma [simp]: "wadjust_goon_left_moving m rs (c, Bk # list) \<Longrightarrow>
+lemma wadjust_backto_standard_pos_via_left_Bk[simp]:
+ "wadjust_goon_left_moving m rs (c, Bk # list) \<Longrightarrow>
wadjust_backto_standard_pos m rs (tl c, hd c # Bk # list)"
-apply(case_tac "hd c", simp_all add: wadjust_backto_standard_pos.simps
- wadjust_goon_left_moving.simps)
-done
-
-lemma [simp]: "wadjust_backto_standard_pos m rs (c, Bk # list) \<Longrightarrow>
- (c = [] \<longrightarrow> wadjust_stop m rs ([Bk], list)) \<and> (c \<noteq> [] \<longrightarrow> wadjust_stop m rs (Bk # c, list))"
-apply(auto simp: wadjust_backto_standard_pos.simps
- wadjust_backto_standard_pos_B.simps
- wadjust_backto_standard_pos_O.simps wadjust_stop.simps)
-apply(case_tac [!] mr, simp_all add: )
-done
-
-lemma [simp]: "wadjust_start m rs (c, Oc # list)
- \<Longrightarrow> (c = [] \<longrightarrow> wadjust_loop_start m rs ([Oc], list)) \<and>
- (c \<noteq> [] \<longrightarrow> wadjust_loop_start m rs (Oc # c, list))"
-apply(auto simp:wadjust_loop_start.simps wadjust_start.simps )
-apply(rule_tac x = ln in exI, rule_tac x = rn in exI,
- rule_tac x = "Suc 0" in exI, simp)
-done
-
-lemma [simp]: "wadjust_loop_start m rs (c, b) \<Longrightarrow> c \<noteq> []"
-apply(simp add: wadjust_loop_start.simps, auto)
-done
-
-lemma [simp]: "wadjust_loop_start m rs (c, Oc # list)
+by(case_tac "hd c", simp_all add: wadjust_backto_standard_pos.simps wadjust_goon_left_moving.simps
+ wadjust_goon_left_moving_B.simps wadjust_backto_standard_pos_O.simps)
+
+lemma wadjust_loop_right_move_Oc[simp]: "wadjust_loop_start m rs (c, Oc # list)
\<Longrightarrow> wadjust_loop_right_move m rs (Oc # c, list)"
apply(simp add: wadjust_loop_start.simps wadjust_loop_right_move.simps, auto)
apply(rule_tac x = ml in exI, rule_tac x = mr in exI,
@@ -4256,7 +3698,7 @@
apply(rule_tac x = "Suc ln" in exI, simp add: exp_ind del: replicate_Suc)
done
-lemma [simp]: "wadjust_loop_right_move m rs (c, Oc # list) \<Longrightarrow>
+lemma wadjust_loop_check_Oc[simp]: "wadjust_loop_right_move m rs (c, Oc # list) \<Longrightarrow>
wadjust_loop_check m rs (Oc # c, list)"
apply(simp add: wadjust_loop_right_move.simps
wadjust_loop_check.simps, auto)
@@ -4266,7 +3708,7 @@
apply(case_tac [!] nr, simp_all)
done
-lemma [simp]: "wadjust_loop_check m rs (c, Oc # list) \<Longrightarrow>
+lemma wadjust_loop_erase_move_Oc[simp]: "wadjust_loop_check m rs (c, Oc # list) \<Longrightarrow>
wadjust_loop_erase m rs (tl c, hd c # Oc # list)"
apply(simp only: wadjust_loop_check.simps wadjust_loop_erase.simps)
apply(erule_tac exE)+
@@ -4274,45 +3716,41 @@
apply(case_tac mr, simp_all add: )
done
-lemma [simp]: "wadjust_loop_erase m rs (c, Oc # list) \<Longrightarrow>
+lemma wadjust_loop_erase_Bk_via_Oc[simp]: "wadjust_loop_erase m rs (c, Oc # list) \<Longrightarrow>
wadjust_loop_erase m rs (c, Bk # list)"
apply(auto simp: wadjust_loop_erase.simps)
done
-lemma [simp]: "wadjust_loop_on_left_moving_B m rs (c, Oc # list) = False"
+lemma wadjust_loop_on_left_moving_B_no_Oc[simp]: "wadjust_loop_on_left_moving_B m rs (c, Oc # list) = False"
apply(auto simp: wadjust_loop_on_left_moving_B.simps)
apply(case_tac nr, simp_all add: )
done
-lemma [simp]: "wadjust_loop_on_left_moving m rs (c, Oc # list)
+lemma wadjust_loop_right_move2_via_left_moving[simp]:
+ "wadjust_loop_on_left_moving m rs (c, Oc # list)
\<Longrightarrow> wadjust_loop_right_move2 m rs (Oc # c, list)"
apply(simp add:wadjust_loop_on_left_moving.simps)
apply(auto simp: wadjust_loop_on_left_moving_O.simps
wadjust_loop_right_move2.simps)
done
-lemma [simp]: "wadjust_loop_right_move2 m rs (c, Oc # list) = False"
+lemma wadjust_loop_right_move2_no_Oc[simp]: "wadjust_loop_right_move2 m rs (c, Oc # list) = False"
apply(auto simp: wadjust_loop_right_move2.simps )
apply(case_tac ln, simp_all add: )
done
-lemma [simp]: "wadjust_erase2 m rs (c, Oc # list)
- \<Longrightarrow> (c = [] \<longrightarrow> wadjust_erase2 m rs ([], Bk # list))
- \<and> (c \<noteq> [] \<longrightarrow> wadjust_erase2 m rs (c, Bk # list))"
-apply(auto simp: wadjust_erase2.simps )
-done
-
-lemma [simp]: "wadjust_on_left_moving_B m rs (c, Oc # list) = False"
+lemma wadjust_on_left_moving_B_no_Oc[simp]:
+ "wadjust_on_left_moving_B m rs (c, Oc # list) = False"
apply(auto simp: wadjust_on_left_moving_B.simps)
done
-lemma [simp]: "\<lbrakk>wadjust_on_left_moving_O m rs (c, Oc # list); hd c = Bk\<rbrakk> \<Longrightarrow>
+lemma wadjust_goon_left_moving_B_Bk_Oc: "\<lbrakk>wadjust_on_left_moving_O m rs (c, Oc # list); hd c = Bk\<rbrakk> \<Longrightarrow>
wadjust_goon_left_moving_B m rs (tl c, Bk # Oc # list)"
apply(auto simp: wadjust_on_left_moving_O.simps
wadjust_goon_left_moving_B.simps )
done
-lemma [simp]: "\<lbrakk>wadjust_on_left_moving_O m rs (c, Oc # list); hd c = Oc\<rbrakk>
+lemma wadjust_goon_left_moving_O_Oc_Oc: "\<lbrakk>wadjust_on_left_moving_O m rs (c, Oc # list); hd c = Oc\<rbrakk>
\<Longrightarrow> wadjust_goon_left_moving_O m rs (tl c, Oc # Oc # list)"
apply(auto simp: wadjust_on_left_moving_O.simps
wadjust_goon_left_moving_O.simps )
@@ -4320,31 +3758,18 @@
done
-lemma [simp]: "wadjust_on_left_moving m rs (c, Oc # list) \<Longrightarrow>
+lemma wadjust_goon_left_moving_Oc[simp]: "wadjust_on_left_moving m rs (c, Oc # list) \<Longrightarrow>
wadjust_goon_left_moving m rs (tl c, hd c # Oc # list)"
-apply(simp add: wadjust_on_left_moving.simps
- wadjust_goon_left_moving.simps)
-apply(case_tac "hd c", simp_all)
-done
-
-lemma [simp]: "wadjust_on_left_moving m rs (c, Oc # list) \<Longrightarrow>
- wadjust_goon_left_moving m rs (tl c, hd c # Oc # list)"
-apply(simp add: wadjust_on_left_moving.simps
- wadjust_goon_left_moving.simps)
-apply(case_tac "hd c", simp_all)
-done
-
-lemma [simp]: "wadjust_goon_left_moving_B m rs (c, Oc # list) = False"
-apply(auto simp: wadjust_goon_left_moving_B.simps)
-done
-
-lemma [simp]: "\<lbrakk>wadjust_goon_left_moving_O m rs (c, Oc # list); hd c = Bk\<rbrakk>
+ by(cases "hd c"; force simp: wadjust_on_left_moving.simps wadjust_goon_left_moving.simps
+ wadjust_goon_left_moving_B_Bk_Oc wadjust_goon_left_moving_O_Oc_Oc)+
+
+lemma left_moving_Bk_Oc[simp]: "\<lbrakk>wadjust_goon_left_moving_O m rs (c, Oc # list); hd c = Bk\<rbrakk>
\<Longrightarrow> wadjust_goon_left_moving_B m rs (tl c, Bk # Oc # list)"
apply(auto simp: wadjust_goon_left_moving_O.simps wadjust_goon_left_moving_B.simps)
apply(case_tac [!] ml, auto simp: )
done
-lemma [simp]: "\<lbrakk>wadjust_goon_left_moving_O m rs (c, Oc # list); hd c = Oc\<rbrakk> \<Longrightarrow>
+lemma left_moving_Oc_Oc[simp]: "\<lbrakk>wadjust_goon_left_moving_O m rs (c, Oc # list); hd c = Oc\<rbrakk> \<Longrightarrow>
wadjust_goon_left_moving_O m rs (tl c, Oc # Oc # list)"
apply(auto simp: wadjust_goon_left_moving_O.simps wadjust_goon_left_moving_B.simps)
apply(rule_tac x = "ml - 1" in exI, simp)
@@ -4352,48 +3777,54 @@
apply(rule_tac x = "Suc mr" in exI, auto simp: )
done
-lemma [simp]: "wadjust_goon_left_moving m rs (c, Oc # list) \<Longrightarrow>
+lemma wadjust_goon_left_moving_B_no_Oc[simp]:
+ "wadjust_goon_left_moving_B m rs (c, Oc # list) = False"
+apply(auto simp: wadjust_goon_left_moving_B.simps)
+ done
+
+lemma wadjust_goon_left_moving_Oc_move[simp]: "wadjust_goon_left_moving m rs (c, Oc # list) \<Longrightarrow>
wadjust_goon_left_moving m rs (tl c, hd c # Oc # list)"
-apply(simp add: wadjust_goon_left_moving.simps)
-apply(case_tac "hd c", simp_all)
-done
-
-lemma [simp]: "wadjust_backto_standard_pos_B m rs (c, Oc # list) = False"
+by(cases "hd c",auto simp: wadjust_goon_left_moving.simps)
+
+lemma wadjust_backto_standard_pos_B_no_Oc[simp]:
+ "wadjust_backto_standard_pos_B m rs (c, Oc # list) = False"
apply(simp add: wadjust_backto_standard_pos_B.simps)
done
-lemma [simp]: "wadjust_backto_standard_pos_O m rs (c, Bk # xs) = False"
+lemma wadjust_backto_standard_pos_O_no_Bk[simp]:
+ "wadjust_backto_standard_pos_O m rs (c, Bk # xs) = False"
apply(simp add: wadjust_backto_standard_pos_O.simps, auto)
apply(case_tac mr, simp_all add: )
done
-lemma [simp]: "wadjust_backto_standard_pos_O m rs ([], Oc # list) \<Longrightarrow>
+lemma wadjust_backto_standard_pos_B_Bk_Oc[simp]:
+ "wadjust_backto_standard_pos_O m rs ([], Oc # list) \<Longrightarrow>
wadjust_backto_standard_pos_B m rs ([], Bk # Oc # list)"
apply(auto simp: wadjust_backto_standard_pos_O.simps
wadjust_backto_standard_pos_B.simps)
done
-lemma [simp]:
+lemma wadjust_backto_standard_pos_B_Bk_Oc_via_O[simp]:
"\<lbrakk>wadjust_backto_standard_pos_O m rs (c, Oc # list); c \<noteq> []; hd c = Bk\<rbrakk>
\<Longrightarrow> wadjust_backto_standard_pos_B m rs (tl c, Bk # Oc # list)"
apply(simp add:wadjust_backto_standard_pos_O.simps
wadjust_backto_standard_pos_B.simps, auto)
done
-lemma [simp]: "\<lbrakk>wadjust_backto_standard_pos_O m rs (c, Oc # list); c \<noteq> []; hd c = Oc\<rbrakk>
+lemma wadjust_backto_standard_pos_B_Oc_Oc_via_O[simp]: "\<lbrakk>wadjust_backto_standard_pos_O m rs (c, Oc # list); c \<noteq> []; hd c = Oc\<rbrakk>
\<Longrightarrow> wadjust_backto_standard_pos_O m rs (tl c, Oc # Oc # list)"
apply(simp add: wadjust_backto_standard_pos_O.simps, auto)
apply(case_tac ml, simp_all add: , auto)
done
-lemma [simp]: "wadjust_backto_standard_pos m rs (c, Oc # list)
+lemma wadjust_backto_standard_pos_cases[simp]: "wadjust_backto_standard_pos m rs (c, Oc # list)
\<Longrightarrow> (c = [] \<longrightarrow> wadjust_backto_standard_pos m rs ([], Bk # Oc # list)) \<and>
(c \<noteq> [] \<longrightarrow> wadjust_backto_standard_pos m rs (tl c, hd c # Oc # list))"
apply(auto simp: wadjust_backto_standard_pos.simps)
apply(case_tac "hd c", simp_all)
done
-lemma [simp]: "wadjust_loop_right_move m rs (c, []) = False"
+lemma wadjust_loop_right_move_nonempty_snd[simp]: "wadjust_loop_right_move m rs (c, []) = False"
apply(simp only: wadjust_loop_right_move.simps)
apply(rule_tac iffI)
apply(erule_tac exE)+
@@ -4401,11 +3832,11 @@
apply(case_tac mr, simp_all add: )
done
-lemma [simp]: "wadjust_loop_erase m rs (c, []) = False"
+lemma wadjust_loop_erase_nonempty_snd[simp]: "wadjust_loop_erase m rs (c, []) = False"
apply(simp only: wadjust_loop_erase.simps, auto)
done
-lemma [simp]: "\<lbrakk>Suc (Suc rs) = a; wadjust_loop_erase m rs (c, Bk # list)\<rbrakk>
+lemma wadjust_loop_erase_cases2[simp]: "\<lbrakk>Suc (Suc rs) = a; wadjust_loop_erase m rs (c, Bk # list)\<rbrakk>
\<Longrightarrow> a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev (tl c) @ hd c # Bk # list))))
< a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Bk # list)))) \<or>
a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev (tl c) @ hd c # Bk # list)))) =
@@ -4413,17 +3844,7 @@
apply(simp only: wadjust_loop_erase.simps)
apply(rule_tac disjI2)
apply(case_tac c, simp, simp)
-done
-
-lemma [simp]:
- "\<lbrakk>Suc (Suc rs) = a; wadjust_loop_on_left_moving m rs (c, Bk # list)\<rbrakk>
- \<Longrightarrow> a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev (tl c) @ hd c # Bk # list))))
- < a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Bk # list)))) \<or>
- a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev (tl c) @ hd c # Bk # list)))) =
- a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Bk # list))))"
-apply(subgoal_tac "c \<noteq> []")
-apply(case_tac c, simp_all)
-done
+ done
lemma dropWhile_exp1: "dropWhile (\<lambda>a. a = Oc) (Oc\<up>(n) @ xs) = dropWhile (\<lambda>a. a = Oc) xs"
apply(induct n, simp_all add: )
@@ -4432,19 +3853,39 @@
apply(induct n, simp_all add: )
done
-lemma [simp]: "\<lbrakk>Suc (Suc rs) = a; wadjust_loop_right_move2 m rs (c, Bk # list)\<rbrakk>
- \<Longrightarrow> a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Oc # list))))
+lemma wadjust_correctness_helper_1:
+ assumes "Suc (Suc rs) = a" " wadjust_loop_right_move2 m rs (c, Bk # list)"
+ shows "a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Oc # list))))
< a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Bk # list))))"
-apply(simp add: wadjust_loop_right_move2.simps, auto)
-apply(simp add: dropWhile_exp1 takeWhile_exp1)
-apply(case_tac ln, simp, simp add: )
-done
-
-lemma [simp]: "wadjust_loop_check m rs ([], b) = False"
+proof -
+ have "ml + mr = Suc rs \<Longrightarrow> 0 < mr \<Longrightarrow>
+ rs - (ml + length (takeWhile (\<lambda>a. a = Oc) list))
+ < Suc rs -
+ (ml +
+ length
+ (takeWhile (\<lambda>a. a = Oc)
+ (Bk \<up> ln @ Bk # Bk # Oc \<up> mr @ Bk \<up> rn))) "
+ for ml mr ln rn
+ by(cases ln, auto)
+ thus ?thesis using assms
+ by (auto simp: wadjust_loop_right_move2.simps dropWhile_exp1 takeWhile_exp1)
+qed
+
+lemma wadjust_correctness_helper_2:
+ "\<lbrakk>Suc (Suc rs) = a; wadjust_loop_on_left_moving m rs (c, Bk # list)\<rbrakk>
+ \<Longrightarrow> a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev (tl c) @ hd c # Bk # list))))
+ < a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Bk # list)))) \<or>
+ a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev (tl c) @ hd c # Bk # list)))) =
+ a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Bk # list))))"
+ apply(subgoal_tac "c \<noteq> []")
+ apply(case_tac c, simp_all)
+ done
+
+lemma wadjust_loop_check_empty_false[simp]: "wadjust_loop_check m rs ([], b) = False"
apply(simp add: wadjust_loop_check.simps)
done
-lemma [simp]: "\<lbrakk>Suc (Suc rs) = a; wadjust_loop_check m rs (c, Oc # list)\<rbrakk>
+lemma wadjust_loop_check_cases: "\<lbrakk>Suc (Suc rs) = a; wadjust_loop_check m rs (c, Oc # list)\<rbrakk>
\<Longrightarrow> a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev (tl c) @ hd c # Oc # list))))
< a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Oc # list)))) \<or>
a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev (tl c) @ hd c # Oc # list)))) =
@@ -4452,7 +3893,7 @@
apply(case_tac "c", simp_all)
done
-lemma [simp]:
+lemma wadjust_loop_erase_cases_or:
"\<lbrakk>Suc (Suc rs) = a; wadjust_loop_erase m rs (c, Oc # list)\<rbrakk>
\<Longrightarrow> a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Bk # list))))
< a - length (takeWhile (\<lambda>a. a = Oc) (tl (dropWhile (\<lambda>a. a = Oc) (rev c @ Oc # list)))) \<or>
@@ -4464,20 +3905,22 @@
apply(simp add: dropWhile_exp1 takeWhile_exp1)
done
+lemmas wadjust_correctness_helpers = wadjust_correctness_helper_2 wadjust_correctness_helper_1 wadjust_loop_erase_cases_or wadjust_loop_check_cases
+
declare numeral_2_eq_2[simp del]
-lemma [simp]: "wadjust_start m rs (c, Bk # list)
+lemma wadjust_start_Oc[simp]: "wadjust_start m rs (c, Bk # list)
\<Longrightarrow> wadjust_start m rs (c, Oc # list)"
apply(auto simp: wadjust_start.simps)
done
-lemma [simp]: "wadjust_backto_standard_pos m rs (c, Bk # list)
+lemma wadjust_stop_Bk[simp]: "wadjust_backto_standard_pos m rs (c, Bk # list)
\<Longrightarrow> wadjust_stop m rs (Bk # c, list)"
apply(auto simp: wadjust_backto_standard_pos.simps
wadjust_stop.simps wadjust_backto_standard_pos_B.simps)
done
-lemma [simp]: "wadjust_start m rs (c, Oc # list)
+lemma wadjust_loop_start_Oc[simp]: "wadjust_start m rs (c, Oc # list)
\<Longrightarrow> wadjust_loop_start m rs (Oc # c, list)"
apply(auto simp: wadjust_start.simps wadjust_loop_start.simps)
apply(rule_tac x = ln in exI, simp)
@@ -4485,7 +3928,7 @@
apply(rule_tac x = 1 in exI, simp)
done
-lemma [simp]:" wadjust_erase2 m rs (c, Oc # list)
+lemma erase2_Bk_if_Oc[simp]:" wadjust_erase2 m rs (c, Oc # list)
\<Longrightarrow> wadjust_erase2 m rs (c, Bk # list)"
apply(auto simp: wadjust_erase2.simps)
done
@@ -4507,13 +3950,14 @@
next
show "\<forall> n. \<not> ?P (?f n) \<and> ?Q (?f n) \<longrightarrow>
?Q (?f (Suc n)) \<and> (?f (Suc n), ?f n) \<in> wadjust_le"
- apply(rule_tac allI, rule_tac impI, case_tac "?f n", simp)
- apply(simp add: step.simps)
- apply(case_tac d, case_tac [2] aa, simp_all)
+ apply(rule_tac allI, rule_tac impI, case_tac "?f n")
+ apply((case_tac d, case_tac [2] aa); simp add: step.simps)
apply(simp_all only: wadjust_inv.simps split: if_splits)
apply(simp_all)
apply(simp_all add: wadjust_inv.simps wadjust_le_def
+ wadjust_correctness_helpers
Abacus.lex_triple_def Abacus.lex_pair_def lex_square_def split: if_splits)
+
done
next
show "?Q (?f 0)"
@@ -4529,16 +3973,13 @@
done
qed
-lemma [intro]: "tm_wf (t_wcode_adjust, 0)"
+lemma tm_wf_t_wcode_adjust[intro]: "tm_wf (t_wcode_adjust, 0)"
apply(auto simp: t_wcode_adjust_def tm_wf.simps)
done
-declare tm_comp.simps[simp del]
-
-lemma [simp]: "args \<noteq> [] \<Longrightarrow> bl_bin (<args::nat list>) > 0"
-apply(case_tac args)
-apply(auto simp: tape_of_nl_cons bl_bin.simps split: if_splits)
-done
+lemma bl_bin_nonzero[simp]: "args \<noteq> [] \<Longrightarrow> bl_bin (<args::nat list>) > 0"
+ by(cases args)
+ (auto simp: tape_of_nl_cons bl_bin.simps)
lemma wcode_lemma_pre':
"args \<noteq> [] \<Longrightarrow>
@@ -4625,7 +4066,7 @@
\<exists> stp ln rn. steps0 (Suc 0, [], <m # args>) (t_wcode) stp =
(0, [Bk], <[m ,bl_bin (<args>)]> @ Bk\<up>(rn))"
using wcode_lemma_1[of args m]
-apply(simp add: t_wcode_def tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
+apply(simp add: t_wcode_def tape_of_list_def tape_of_nat_list.simps tape_of_nat_def)
done
section {* The universal TM *}
@@ -4661,22 +4102,18 @@
"UTM_pre = t_wcode |+| t_utm"
lemma tinres_step1:
- "\<lbrakk>tinres l l'; step (ss, l, r) (t, 0) = (sa, la, ra);
- step (ss, l', r) (t, 0) = (sb, lb, rb)\<rbrakk>
- \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"
-apply(case_tac ss, case_tac [!]r, case_tac [!] "a::cell")
-apply(auto simp: step.simps fetch.simps nth_of.simps
- split: if_splits )
-apply(case_tac [!] "t ! (2 * nat)",
- auto simp: tinres_def split: if_splits)
-apply(case_tac [1-8] a, auto split: if_splits)
-apply(case_tac [!] "t ! (2 * nat)",
- auto simp: tinres_def split: if_splits)
-apply(case_tac [1-4] a, auto split: if_splits)
-apply(case_tac [!] "t ! Suc (2 * nat)",
- auto simp: if_splits)
-apply(case_tac [!] aa, auto split: if_splits)
-done
+ assumes "tinres l l'" "step (ss, l, r) (t, 0) = (sa, la, ra)"
+ "step (ss, l', r) (t, 0) = (sb, lb, rb)"
+ shows "tinres la lb \<and> ra = rb \<and> sa = sb"
+proof(cases "r")
+ case Nil
+ then show ?thesis using assms
+ by (cases "(fetch t ss Bk)";cases "fst (fetch t ss Bk)";auto simp:step.simps split:if_splits)
+next
+ case (Cons a list)
+ then show ?thesis using assms
+ by (cases "(fetch t ss a)";cases "fst (fetch t ss a)";auto simp:step.simps split:if_splits)
+qed
lemma tinres_steps1:
"\<lbrakk>tinres l l'; steps (ss, l, r) (t, 0) stp = (sa, la, ra);
@@ -4694,17 +4131,12 @@
"step (steps (ss, l', r) (t, 0) stp) (t, 0) = (sb, lb, rb)" "steps (ss, l, r) (t, 0) stp = (a, b, c)"
"steps (ss, l', r) (t, 0) stp = (aa, ba, ca)"
have "tinres b ba \<and> c = ca \<and> a = aa"
- apply(rule_tac ind, simp_all add: h)
- done
+ using ind h by metis
thus "tinres la lb \<and> ra = rb \<and> sa = sb"
- apply(rule_tac l = b and l' = ba and r = c and ss = a
- and t = t in tinres_step1)
- using h
- apply(simp, simp, simp)
- done
+ using tinres_step1 h by metis
qed
-lemma [simp]:
+lemma tinres_some_exp[simp]:
"tinres (Bk \<up> m @ [Bk, Bk]) la \<Longrightarrow> \<exists>m. la = Bk \<up> m"
apply(auto simp: tinres_def)
apply(case_tac n, simp add: exp_ind)
@@ -4780,16 +4212,11 @@
done
qed
-lemma [intro]: "tm_wf (t_wcode, 0)"
-apply(simp add: t_wcode_def)
-apply(rule_tac tm_wf_comp)
-apply(rule_tac tm_wf_comp, auto)
-done
-
-lemma [intro]: "tm_wf (t_utm, 0)"
-apply(simp only: t_utm_def F_tprog_def)
-apply(rule_tac wf_tm_from_abacus, auto)
-done
+lemma tm_wf_t_wcode[intro]: "tm_wf (t_wcode, 0)"
+ apply(simp add: t_wcode_def)
+ apply(rule_tac tm_wf_comp)
+ apply(rule_tac tm_wf_comp, auto)
+ done
lemma UTM_halt_lemma_pre:
assumes wf_tm: "tm_wf (tp, 0)"
@@ -4825,7 +4252,7 @@
Oc # Oc \<up> code tp @ Bk # Oc # Oc \<up> bl_bin (<args>) @ Bk \<up> rn) t_utm n"
using t_utm_halt_eq[of tp i "args" stp m rs k rn] assms
apply(auto simp: bin_wc_eq)
- apply(rule_tac x = stpa in exI, simp add: tape_of_nl_abv tape_of_nat_abv)
+ apply(rule_tac x = stpa in exI, simp add: tape_of_list_def tape_of_nat_def)
done
qed
qed
@@ -4860,7 +4287,7 @@
apply(simp add: NSTD.simps trpl_code.simps)
done
-lemma [simp]: "\<forall>m. b \<noteq> Bk\<up>(m) \<Longrightarrow> 0 < bl2wc b"
+lemma nonzero_bl2wc[simp]: "\<forall>m. b \<noteq> Bk\<up>(m) \<Longrightarrow> 0 < bl2wc b"
apply(rule classical, simp)
apply(induct b, erule_tac x = 0 in allE, simp)
apply(simp add: bl2wc.simps, case_tac a, simp_all
@@ -4873,7 +4300,7 @@
apply(simp add: NSTD.simps trpl_code.simps)
done
-lemma [elim]: "Suc (2 * x) = 2 * y \<Longrightarrow> RR"
+lemma even_not_odd[elim]: "Suc (2 * x) = 2 * y \<Longrightarrow> RR"
apply(induct x arbitrary: y, simp, simp)
apply(case_tac y, simp, simp)
done
@@ -5200,7 +4627,7 @@
thus "False"
using h
apply(erule_tac x = n in allE)
- apply(simp add: tape_of_nl_abv bin_wc_eq tape_of_nat_abv)
+ apply(simp add: tape_of_list_def bin_wc_eq tape_of_nat_def)
done
qed
qed
@@ -5258,7 +4685,7 @@
(Suc 0, [Bk], Oc \<up> Suc (code p) @ Bk # Oc \<up> Suc (bl_bin (<args>)) @ Bk \<up> rn) t_utm n"
using t_utm_halt_eq[of p i "args" stp m rs k rn] assms k
apply(auto simp: bin_wc_eq, auto)
- apply(rule_tac x = stpa in exI, simp add: tape_of_nl_abv tape_of_nat_abv)
+ apply(rule_tac x = stpa in exI, simp add: tape_of_list_def tape_of_nat_def)
done
qed
next
@@ -5286,7 +4713,7 @@
shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM {(\<lambda>tp. (\<exists> m k. tp = (Bk\<up>m, <n> @ Bk\<up>k)))}"
using UTM_halt_lemma[OF assms(1) _ assms(2), where i="0"]
using assms(3)
-apply(simp add: tape_of_nat_abv)
+apply(simp add: tape_of_nat_def)
done
@@ -5318,7 +4745,7 @@
shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM \<up>"
using UTM_unhalt_lemma[OF assms(1), where i="0"]
using assms(2-3)
-apply(simp add: tape_of_nat_abv)
+apply(simp add: tape_of_nat_def)
done
-end
\ No newline at end of file
+end
\ No newline at end of file