--- 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"