Some illustration added together with more explanations.
theory recursive
imports Main rec_def abacus
begin
section {*
Compiling from recursive functions to Abacus machines
*}
text {*
Some auxilliary Abacus machines used to construct the result Abacus machines.
*}
text {*
@{text "get_paras_num recf"} returns the arity of recursive function @{text "recf"}.
*}
fun get_paras_num :: "recf \<Rightarrow> nat"
where
"get_paras_num z = 1" |
"get_paras_num s = 1" |
"get_paras_num (id m n) = m" |
"get_paras_num (Cn n f gs) = n" |
"get_paras_num (Pr n f g) = Suc n" |
"get_paras_num (Mn n f) = n"
fun addition :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"
where
"addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7,
Inc m, Goto 4]"
fun empty :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
where
"empty m n = [Dec m 3, Inc n, Goto 0]"
fun abc_inst_shift :: "abc_inst \<Rightarrow> nat \<Rightarrow> abc_inst"
where
"abc_inst_shift (Inc m) n = Inc m" |
"abc_inst_shift (Dec m e) n = Dec m (e + n)" |
"abc_inst_shift (Goto m) n = Goto (m + n)"
fun abc_shift :: "abc_inst list \<Rightarrow> nat \<Rightarrow> abc_inst list"
where
"abc_shift xs n = map (\<lambda> x. abc_inst_shift x n) xs"
fun abc_append :: "abc_inst list \<Rightarrow> abc_inst list \<Rightarrow>
abc_inst list" (infixl "[+]" 60)
where
"abc_append al bl = (let al_len = length al in
al @ abc_shift bl al_len)"
text {*
The compilation of @{text "z"}-operator.
*}
definition rec_ci_z :: "abc_inst list"
where
"rec_ci_z \<equiv> [Goto 1]"
text {*
The compilation of @{text "s"}-operator.
*}
definition rec_ci_s :: "abc_inst list"
where
"rec_ci_s \<equiv> (addition 0 1 2 [+] [Inc 1])"
text {*
The compilation of @{text "id i j"}-operator
*}
fun rec_ci_id :: "nat \<Rightarrow> nat \<Rightarrow> abc_inst list"
where
"rec_ci_id i j = addition j i (i + 1)"
fun mv_boxes :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_inst list"
where
"mv_boxes ab bb 0 = []" |
"mv_boxes ab bb (Suc n) = mv_boxes ab bb n [+] empty (ab + n)
(bb + n)"
fun empty_boxes :: "nat \<Rightarrow> abc_inst list"
where
"empty_boxes 0 = []" |
"empty_boxes (Suc n) = empty_boxes n [+] [Dec n 2, Goto 0]"
fun cn_merge_gs ::
"(abc_inst list \<times> nat \<times> nat) list \<Rightarrow> nat \<Rightarrow> abc_inst list"
where
"cn_merge_gs [] p = []" |
"cn_merge_gs (g # gs) p =
(let (gprog, gpara, gn) = g in
gprog [+] empty gpara p [+] cn_merge_gs gs (Suc p))"
text {*
The compiler of recursive functions, where @{text "rec_ci recf"} return
@{text "(ap, arity, fp)"}, where @{text "ap"} is the Abacus program, @{text "arity"} is the
arity of the recursive function @{text "recf"},
@{text "fp"} is the amount of memory which is going to be
used by @{text "ap"} for its execution.
*}
function rec_ci :: "recf \<Rightarrow> abc_inst list \<times> nat \<times> nat"
where
"rec_ci z = (rec_ci_z, 1, 2)" |
"rec_ci s = (rec_ci_s, 1, 3)" |
"rec_ci (id m n) = (rec_ci_id m n, m, m + 2)" |
"rec_ci (Cn n f gs) =
(let cied_gs = map (\<lambda> g. rec_ci g) (f # gs) in
let (fprog, fpara, fn) = hd cied_gs in
let pstr =
Max (set (Suc n # fn # (map (\<lambda> (aprog, p, n). n) cied_gs))) in
let qstr = pstr + Suc (length gs) in
(cn_merge_gs (tl cied_gs) pstr [+] mv_boxes 0 qstr n [+]
mv_boxes pstr 0 (length gs) [+] fprog [+]
empty fpara pstr [+] empty_boxes (length gs) [+]
empty pstr n [+] mv_boxes qstr 0 n, n, qstr + n))" |
"rec_ci (Pr n f g) =
(let (fprog, fpara, fn) = rec_ci f in
let (gprog, gpara, gn) = rec_ci g in
let p = Max (set ([n + 3, fn, gn])) in
let e = length gprog + 7 in
(empty n p [+] fprog [+] empty n (Suc n) [+]
(([Dec p e] [+] gprog [+]
[Inc n, Dec (Suc n) 3, Goto 1]) @
[Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gprog + 4)]),
Suc n, p + 1))" |
"rec_ci (Mn n f) =
(let (fprog, fpara, fn) = rec_ci f in
let len = length (fprog) in
(fprog @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3),
Goto (len + 1), Inc n, Goto 0], n, max (Suc n) fn) )"
by pat_completeness auto
termination
proof
term size
show "wf (measure size)" by auto
next
fix n f gs x
assume "(x::recf) \<in> set (f # gs)"
thus "(x, Cn n f gs) \<in> measure size"
by(induct gs, auto)
next
fix n f g
show "(f, Pr n f g) \<in> measure size" by auto
next
fix n f g x xa y xb ya
show "(g, Pr n f g) \<in> measure size" by auto
next
fix n f
show "(f, Mn n f) \<in> measure size" by auto
qed
declare rec_ci.simps [simp del] rec_ci_s_def[simp del]
rec_ci_z_def[simp del] rec_ci_id.simps[simp del]
mv_boxes.simps[simp del] abc_append.simps[simp del]
empty.simps[simp del] addition.simps[simp del]
thm rec_calc_rel.induct
declare abc_steps_l.simps[simp del] abc_fetch.simps[simp del]
abc_step_l.simps[simp del]
lemma abc_steps_add:
"abc_steps_l (as, lm) ap (m + n) =
abc_steps_l (abc_steps_l (as, lm) ap m) ap n"
apply(induct m arbitrary: n as lm, simp add: abc_steps_l.simps)
proof -
fix m n as lm
assume ind:
"\<And>n as lm. abc_steps_l (as, lm) ap (m + n) =
abc_steps_l (abc_steps_l (as, lm) ap m) ap n"
show "abc_steps_l (as, lm) ap (Suc m + n) =
abc_steps_l (abc_steps_l (as, lm) ap (Suc m)) ap n"
apply(insert ind[of as lm "Suc n"], simp)
apply(insert ind[of as lm "Suc 0"], simp add: abc_steps_l.simps)
apply(case_tac "(abc_steps_l (as, lm) ap m)", simp)
apply(simp add: abc_steps_l.simps)
apply(case_tac "abc_step_l (a, b) (abc_fetch a ap)",
simp add: abc_steps_l.simps)
done
qed
(*lemmas: rec_ci and rec_calc_rel*)
lemma rec_calc_inj_case_z:
"\<lbrakk>rec_calc_rel z l x; rec_calc_rel z l y\<rbrakk> \<Longrightarrow> x = y"
apply(auto elim: calc_z_reverse)
done
lemma rec_calc_inj_case_s:
"\<lbrakk>rec_calc_rel s l x; rec_calc_rel s l y\<rbrakk> \<Longrightarrow> x = y"
apply(auto elim: calc_s_reverse)
done
lemma rec_calc_inj_case_id:
"\<lbrakk>rec_calc_rel (recf.id nat1 nat2) l x;
rec_calc_rel (recf.id nat1 nat2) l y\<rbrakk> \<Longrightarrow> x = y"
apply(auto elim: calc_id_reverse)
done
lemma rec_calc_inj_case_mn:
assumes ind: "\<And> l x y. \<lbrakk>rec_calc_rel f l x; rec_calc_rel f l y\<rbrakk>
\<Longrightarrow> x = y"
and h: "rec_calc_rel (Mn n f) l x" "rec_calc_rel (Mn n f) l y"
shows "x = y"
apply(insert h)
apply(elim calc_mn_reverse)
apply(case_tac "x > y", simp)
apply(erule_tac x = "y" in allE, auto)
proof -
fix v va
assume "rec_calc_rel f (l @ [y]) 0"
"rec_calc_rel f (l @ [y]) v"
"0 < v"
thus "False"
apply(insert ind[of "l @ [y]" 0 v], simp)
done
next
fix v va
assume
"rec_calc_rel f (l @ [x]) 0"
"\<forall>x<y. \<exists>v. rec_calc_rel f (l @ [x]) v \<and> 0 < v" "\<not> y < x"
thus "x = y"
apply(erule_tac x = "x" in allE)
apply(case_tac "x = y", auto)
apply(drule_tac y = v in ind, simp, simp)
done
qed
lemma rec_calc_inj_case_pr:
assumes f_ind:
"\<And>l x y. \<lbrakk>rec_calc_rel f l x; rec_calc_rel f l y\<rbrakk> \<Longrightarrow> x = y"
and g_ind:
"\<And>x xa y xb ya l xc yb.
\<lbrakk>x = rec_ci f; (xa, y) = x; (xb, ya) = y;
rec_calc_rel g l xc; rec_calc_rel g l yb\<rbrakk> \<Longrightarrow> xc = yb"
and h: "rec_calc_rel (Pr n f g) l x" "rec_calc_rel (Pr n f g) l y"
shows "x = y"
apply(case_tac "rec_ci f")
proof -
fix a b c
assume "rec_ci f = (a, b, c)"
hence ng_ind:
"\<And> l xc yb. \<lbrakk>rec_calc_rel g l xc; rec_calc_rel g l yb\<rbrakk>
\<Longrightarrow> xc = yb"
apply(insert g_ind[of "(a, b, c)" "a" "(b, c)" b c], simp)
done
from h show "x = y"
apply(erule_tac calc_pr_reverse, erule_tac calc_pr_reverse)
apply(erule f_ind, simp, simp)
apply(erule_tac calc_pr_reverse, simp, simp)
proof -
fix la ya ry laa yaa rya
assume k1: "rec_calc_rel g (la @ [ya, ry]) x"
"rec_calc_rel g (la @ [ya, rya]) y"
and k2: "rec_calc_rel (Pr (length la) f g) (la @ [ya]) ry"
"rec_calc_rel (Pr (length la) f g) (la @ [ya]) rya"
from k2 have "ry = rya"
apply(induct ya arbitrary: ry rya)
apply(erule_tac calc_pr_reverse,
erule_tac calc_pr_reverse, simp)
apply(erule f_ind, simp, simp, simp)
apply(erule_tac calc_pr_reverse, simp)
apply(erule_tac rSucy = rya in calc_pr_reverse, simp, simp)
proof -
fix ya ry rya l y ryb laa yb ryc
assume ind:
"\<And>ry rya. \<lbrakk>rec_calc_rel (Pr (length l) f g) (l @ [y]) ry;
rec_calc_rel (Pr (length l) f g) (l @ [y]) rya\<rbrakk> \<Longrightarrow> ry = rya"
and j: "rec_calc_rel (Pr (length l) f g) (l @ [y]) ryb"
"rec_calc_rel g (l @ [y, ryb]) ry"
"rec_calc_rel (Pr (length l) f g) (l @ [y]) ryc"
"rec_calc_rel g (l @ [y, ryc]) rya"
from j show "ry = rya"
apply(insert ind[of ryb ryc], simp)
apply(insert ng_ind[of "l @ [y, ryc]" ry rya], simp)
done
qed
from k1 and this show "x = y"
apply(simp)
apply(insert ng_ind[of "la @ [ya, rya]" x y], simp)
done
qed
qed
lemma Suc_nth_part_eq:
"\<forall>k<Suc (length list). (a # xs) ! k = (aa # list) ! k
\<Longrightarrow> \<forall>k<(length list). (xs) ! k = (list) ! k"
apply(rule allI, rule impI)
apply(erule_tac x = "Suc k" in allE, simp)
done
lemma list_eq_intro:
"\<lbrakk>length xs = length ys; \<forall> k < length xs. xs ! k = ys ! k\<rbrakk>
\<Longrightarrow> xs = ys"
apply(induct xs arbitrary: ys, simp)
apply(case_tac ys, simp, simp)
proof -
fix a xs ys aa list
assume ind:
"\<And>ys. \<lbrakk>length list = length ys; \<forall>k<length ys. xs ! k = ys ! k\<rbrakk>
\<Longrightarrow> xs = ys"
and h: "length xs = length list"
"\<forall>k<Suc (length list). (a # xs) ! k = (aa # list) ! k"
from h show "a = aa \<and> xs = list"
apply(insert ind[of list], simp)
apply(frule Suc_nth_part_eq, simp)
apply(erule_tac x = "0" in allE, simp)
done
qed
lemma rec_calc_inj_case_cn:
assumes ind:
"\<And>x l xa y.
\<lbrakk>x = f \<or> x \<in> set gs; rec_calc_rel x l xa; rec_calc_rel x l y\<rbrakk>
\<Longrightarrow> xa = y"
and h: "rec_calc_rel (Cn n f gs) l x"
"rec_calc_rel (Cn n f gs) l y"
shows "x = y"
apply(insert h, elim calc_cn_reverse)
apply(subgoal_tac "rs = rsa")
apply(rule_tac x = f and l = rsa and xa = x and y = y in ind,
simp, simp, simp)
apply(intro list_eq_intro, simp, rule allI, rule impI)
apply(erule_tac x = k in allE, rule_tac x = k in allE, simp, simp)
apply(rule_tac x = "gs ! k" in ind, simp, simp, simp)
done
lemma rec_calc_inj:
"\<lbrakk>rec_calc_rel f l x;
rec_calc_rel f l y\<rbrakk> \<Longrightarrow> x = y"
apply(induct f arbitrary: l x y rule: rec_ci.induct)
apply(simp add: rec_calc_inj_case_z)
apply(simp add: rec_calc_inj_case_s)
apply(simp add: rec_calc_inj_case_id, simp)
apply(erule rec_calc_inj_case_cn,simp, simp)
apply(erule rec_calc_inj_case_pr, auto)
apply(erule rec_calc_inj_case_mn, auto)
done
lemma calc_rel_reverse_ind_step_ex:
"\<lbrakk>rec_calc_rel (Pr n f g) (lm @ [Suc x]) rs\<rbrakk>
\<Longrightarrow> \<exists> rs. rec_calc_rel (Pr n f g) (lm @ [x]) rs"
apply(erule calc_pr_reverse, simp, simp)
apply(rule_tac x = rk in exI, simp)
done
lemma [simp]: "Suc x \<le> y \<Longrightarrow> Suc (y - Suc x) = y - x"
by arith
lemma calc_pr_para_not_null:
"rec_calc_rel (Pr n f g) lm rs \<Longrightarrow> lm \<noteq> []"
apply(erule calc_pr_reverse, simp, simp)
done
lemma calc_pr_less_ex:
"\<lbrakk>rec_calc_rel (Pr n f g) lm rs; x \<le> last lm\<rbrakk> \<Longrightarrow>
\<exists>rs. rec_calc_rel (Pr n f g) (butlast lm @ [last lm - x]) rs"
apply(subgoal_tac "lm \<noteq> []")
apply(induct x, rule_tac x = rs in exI, simp, simp, erule exE)
apply(rule_tac rs = xa in calc_rel_reverse_ind_step_ex, simp)
apply(simp add: calc_pr_para_not_null)
done
lemma calc_pr_zero_ex:
"rec_calc_rel (Pr n f g) lm rs \<Longrightarrow>
\<exists>rs. rec_calc_rel f (butlast lm) rs"
apply(drule_tac x = "last lm" in calc_pr_less_ex, simp,
erule_tac exE, simp)
apply(erule_tac calc_pr_reverse, simp)
apply(rule_tac x = rs in exI, simp, simp)
done
lemma abc_steps_ind:
"abc_steps_l (as, am) ap (Suc stp) =
abc_steps_l (abc_steps_l (as, am) ap stp) ap (Suc 0)"
apply(insert abc_steps_add[of as am ap stp "Suc 0"], simp)
done
lemma abc_steps_zero: "abc_steps_l asm ap 0 = asm"
apply(case_tac asm, simp add: abc_steps_l.simps)
done
lemma abc_append_nth:
"n < length ap + length bp \<Longrightarrow>
(ap [+] bp) ! n =
(if n < length ap then ap ! n
else abc_inst_shift (bp ! (n - length ap)) (length ap))"
apply(simp add: abc_append.simps nth_append map_nth split: if_splits)
done
lemma abc_state_keep:
"as \<ge> length bp \<Longrightarrow> abc_steps_l (as, lm) bp stp = (as, lm)"
apply(induct stp, simp add: abc_steps_zero)
apply(simp add: abc_steps_ind)
apply(simp add: abc_steps_zero)
apply(simp add: abc_steps_l.simps abc_fetch.simps abc_step_l.simps)
done
lemma abc_halt_equal:
"\<lbrakk>abc_steps_l (0, lm) bp stpa = (length bp, lm1);
abc_steps_l (0, lm) bp stpb = (length bp, lm2)\<rbrakk> \<Longrightarrow> lm1 = lm2"
apply(case_tac "stpa - stpb > 0")
apply(insert abc_steps_add[of 0 lm bp stpb "stpa - stpb"], simp)
apply(insert abc_state_keep[of bp "length bp" lm2 "stpa - stpb"],
simp, simp add: abc_steps_zero)
apply(insert abc_steps_add[of 0 lm bp stpa "stpb - stpa"], simp)
apply(insert abc_state_keep[of bp "length bp" lm1 "stpb - stpa"],
simp)
done
lemma abc_halt_point_ex:
"\<lbrakk>\<exists>stp. abc_steps_l (0, lm) bp stp = (bs, lm');
bs = length bp; bp \<noteq> []\<rbrakk>
\<Longrightarrow> \<exists> stp. (\<lambda> (s, l). s < bs \<and>
(abc_steps_l (s, l) bp (Suc 0)) = (bs, lm'))
(abc_steps_l (0, lm) bp stp) "
apply(erule_tac exE)
proof -
fix stp
assume "bs = length bp"
"abc_steps_l (0, lm) bp stp = (bs, lm')"
"bp \<noteq> []"
thus
"\<exists>stp. (\<lambda>(s, l). s < bs \<and>
abc_steps_l (s, l) bp (Suc 0) = (bs, lm'))
(abc_steps_l (0, lm) bp stp)"
apply(induct stp, simp add: abc_steps_zero, simp)
proof -
fix stpa
assume ind:
"abc_steps_l (0, lm) bp stpa = (length bp, lm')
\<Longrightarrow> \<exists>stp. (\<lambda>(s, l). s < length bp \<and> abc_steps_l (s, l) bp
(Suc 0) = (length bp, lm')) (abc_steps_l (0, lm) bp stp)"
and h: "abc_steps_l (0, lm) bp (Suc stpa) = (length bp, lm')"
"abc_steps_l (0, lm) bp stp = (length bp, lm')"
"bp \<noteq> []"
from h show
"\<exists>stp. (\<lambda>(s, l). s < length bp \<and> abc_steps_l (s, l) bp (Suc 0)
= (length bp, lm')) (abc_steps_l (0, lm) bp stp)"
apply(case_tac "abc_steps_l (0, lm) bp stpa",
case_tac "a = length bp")
apply(insert ind, simp)
apply(subgoal_tac "b = lm'", simp)
apply(rule_tac abc_halt_equal, simp, simp)
apply(rule_tac x = stpa in exI, simp add: abc_steps_ind)
apply(simp add: abc_steps_zero)
apply(rule classical, simp add: abc_steps_l.simps
abc_fetch.simps abc_step_l.simps)
done
qed
qed
lemma abc_append_empty_r[simp]: "[] [+] ab = ab"
apply(simp add: abc_append.simps abc_inst_shift.simps)
apply(induct ab, simp, simp)
apply(case_tac a, simp_all add: abc_inst_shift.simps)
done
lemma abc_append_empty_l[simp]: "ab [+] [] = ab"
apply(simp add: abc_append.simps abc_inst_shift.simps)
done
lemma abc_append_length[simp]:
"length (ap [+] bp) = length ap + length bp"
apply(simp add: abc_append.simps)
done
lemma abc_append_commute: "as [+] bs [+] cs = as [+] (bs [+] cs)"
apply(simp add: abc_append.simps abc_shift.simps abc_inst_shift.simps)
apply(induct cs, simp, simp)
apply(case_tac a, auto simp: abc_inst_shift.simps)
done
lemma abc_halt_point_step[simp]:
"\<lbrakk>a < length bp; abc_steps_l (a, b) bp (Suc 0) = (length bp, lm')\<rbrakk>
\<Longrightarrow> abc_steps_l (length ap + a, b) (ap [+] bp [+] cp) (Suc 0) =
(length ap + length bp, lm')"
apply(simp add: abc_steps_l.simps abc_fetch.simps abc_append_nth)
apply(case_tac "bp ! a",
auto simp: abc_steps_l.simps abc_step_l.simps)
done
lemma abc_step_state_in:
"\<lbrakk>bs < length bp; abc_steps_l (a, b) bp (Suc 0) = (bs, l)\<rbrakk>
\<Longrightarrow> a < length bp"
apply(simp add: abc_steps_l.simps abc_fetch.simps)
apply(rule_tac classical,
simp add: abc_step_l.simps abc_steps_l.simps)
done
lemma abc_append_state_in_exc:
"\<lbrakk>bs < length bp; abc_steps_l (0, lm) bp stpa = (bs, l)\<rbrakk>
\<Longrightarrow> abc_steps_l (length ap, lm) (ap [+] bp [+] cp) stpa =
(length ap + bs, l)"
apply(induct stpa arbitrary: bs l, simp add: abc_steps_zero)
proof -
fix stpa bs l
assume ind:
"\<And>bs l. \<lbrakk>bs < length bp; abc_steps_l (0, lm) bp stpa = (bs, l)\<rbrakk>
\<Longrightarrow> abc_steps_l (length ap, lm) (ap [+] bp [+] cp) stpa =
(length ap + bs, l)"
and h: "bs < length bp"
"abc_steps_l (0, lm) bp (Suc stpa) = (bs, l)"
from h show
"abc_steps_l (length ap, lm) (ap [+] bp [+] cp) (Suc stpa) =
(length ap + bs, l)"
apply(simp add: abc_steps_ind)
apply(case_tac "(abc_steps_l (0, lm) bp stpa)", simp)
proof -
fix a b
assume g: "abc_steps_l (0, lm) bp stpa = (a, b)"
"abc_steps_l (a, b) bp (Suc 0) = (bs, l)"
from h and g have k1: "a < length bp"
apply(simp add: abc_step_state_in)
done
from h and g and k1 show
"abc_steps_l (abc_steps_l (length ap, lm) (ap [+] bp [+] cp) stpa)
(ap [+] bp [+] cp) (Suc 0) = (length ap + bs, l)"
apply(insert ind[of a b], simp)
apply(simp add: abc_steps_l.simps abc_fetch.simps
abc_append_nth)
apply(case_tac "bp ! a", auto simp:
abc_steps_l.simps abc_step_l.simps)
done
qed
qed
lemma [simp]: "abc_steps_l (0, am) [] stp = (0, am)"
apply(induct stp, simp add: abc_steps_zero)
apply(simp add: abc_steps_ind)
apply(simp add: abc_steps_zero abc_steps_l.simps
abc_fetch.simps abc_step_l.simps)
done
lemma abc_append_exc1:
"\<lbrakk>\<exists> stp. abc_steps_l (0, lm) bp stp = (bs, lm');
bs = length bp;
as = length ap\<rbrakk>
\<Longrightarrow> \<exists> stp. abc_steps_l (as, lm) (ap [+] bp [+] cp) stp
= (as + bs, lm')"
apply(case_tac "bp = []", erule_tac exE, simp,
rule_tac x = 0 in exI, simp add: abc_steps_zero)
apply(frule_tac abc_halt_point_ex, simp, simp,
erule_tac exE, erule_tac exE)
apply(rule_tac x = "stpa + Suc 0" in exI)
apply(case_tac "(abc_steps_l (0, lm) bp stpa)",
simp add: abc_steps_ind)
apply(subgoal_tac
"abc_steps_l (length ap, lm) (ap [+] bp [+] cp) stpa
= (length ap + a, b)", simp)
apply(simp add: abc_steps_zero)
apply(rule_tac abc_append_state_in_exc, simp, simp)
done
lemma abc_append_exc3:
"\<lbrakk>\<exists> stp. abc_steps_l (0, am) bp stp = (bs, bm); ss = length ap\<rbrakk>
\<Longrightarrow> \<exists> stp. abc_steps_l (ss, am) (ap [+] bp) stp = (bs + ss, bm)"
apply(erule_tac exE)
proof -
fix stp
assume h: "abc_steps_l (0, am) bp stp = (bs, bm)" "ss = length ap"
thus " \<exists>stp. abc_steps_l (ss, am) (ap [+] bp) stp = (bs + ss, bm)"
proof(induct stp arbitrary: bs bm)
fix bs bm
assume "abc_steps_l (0, am) bp 0 = (bs, bm)"
thus "\<exists>stp. abc_steps_l (ss, am) (ap [+] bp) stp = (bs + ss, bm)"
apply(rule_tac x = 0 in exI, simp add: abc_steps_l.simps)
done
next
fix stp bs bm
assume ind:
"\<And>bs bm. \<lbrakk>abc_steps_l (0, am) bp stp = (bs, bm);
ss = length ap\<rbrakk> \<Longrightarrow>
\<exists>stp. abc_steps_l (ss, am) (ap [+] bp) stp = (bs + ss, bm)"
and g: "abc_steps_l (0, am) bp (Suc stp) = (bs, bm)"
from g show
"\<exists>stp. abc_steps_l (ss, am) (ap [+] bp) stp = (bs + ss, bm)"
apply(insert abc_steps_add[of 0 am bp stp "Suc 0"], simp)
apply(case_tac "(abc_steps_l (0, am) bp stp)", simp)
proof -
fix a b
assume "(bs, bm) = abc_steps_l (a, b) bp (Suc 0)"
"abc_steps_l (0, am) bp (Suc stp) =
abc_steps_l (a, b) bp (Suc 0)"
"abc_steps_l (0, am) bp stp = (a, b)"
thus "?thesis"
apply(insert ind[of a b], simp add: h, erule_tac exE)
apply(rule_tac x = "Suc stp" in exI)
apply(simp only: abc_steps_ind, simp add: abc_steps_zero)
proof -
fix stp
assume "(bs, bm) = abc_steps_l (a, b) bp (Suc 0)"
thus "abc_steps_l (a + length ap, b) (ap [+] bp) (Suc 0)
= (bs + length ap, bm)"
apply(simp add: abc_steps_l.simps abc_steps_zero
abc_fetch.simps split: if_splits)
apply(case_tac "bp ! a",
simp_all add: abc_inst_shift.simps abc_append_nth
abc_steps_l.simps abc_steps_zero abc_step_l.simps)
apply(auto)
done
qed
qed
qed
qed
lemma abc_add_equal:
"\<lbrakk>ap \<noteq> [];
abc_steps_l (0, am) ap astp = (a, b);
a < length ap\<rbrakk>
\<Longrightarrow> (abc_steps_l (0, am) (ap @ bp) astp) = (a, b)"
apply(induct astp arbitrary: a b, simp add: abc_steps_l.simps, simp)
apply(simp add: abc_steps_ind)
apply(case_tac "(abc_steps_l (0, am) ap astp)")
proof -
fix astp a b aa ba
assume ind:
"\<And>a b. \<lbrakk>abc_steps_l (0, am) ap astp = (a, b);
a < length ap\<rbrakk> \<Longrightarrow>
abc_steps_l (0, am) (ap @ bp) astp = (a, b)"
and h: "abc_steps_l (abc_steps_l (0, am) ap astp) ap (Suc 0)
= (a, b)"
"a < length ap"
"abc_steps_l (0, am) ap astp = (aa, ba)"
from h show "abc_steps_l (abc_steps_l (0, am) (ap @ bp) astp)
(ap @ bp) (Suc 0) = (a, b)"
apply(insert ind[of aa ba], simp)
apply(subgoal_tac "aa < length ap", simp)
apply(simp add: abc_steps_l.simps abc_fetch.simps
nth_append abc_steps_zero)
apply(rule abc_step_state_in, auto)
done
qed
lemma abc_add_exc1:
"\<lbrakk>\<exists> astp. abc_steps_l (0, am) ap astp = (as, bm); as = length ap\<rbrakk>
\<Longrightarrow> \<exists> stp. abc_steps_l (0, am) (ap @ bp) stp = (as, bm)"
apply(case_tac "ap = []", simp,
rule_tac x = 0 in exI, simp add: abc_steps_zero)
apply(drule_tac abc_halt_point_ex, simp, simp)
apply(erule_tac exE, case_tac "(abc_steps_l (0, am) ap astp)", simp)
apply(rule_tac x = "Suc astp" in exI, simp add: abc_steps_ind, auto)
apply(frule_tac bp = bp in abc_add_equal, simp, simp, simp)
apply(simp add: abc_steps_l.simps abc_steps_zero
abc_fetch.simps nth_append)
done
declare abc_shift.simps[simp del]
lemma abc_append_exc2:
"\<lbrakk>\<exists> astp. abc_steps_l (0, am) ap astp = (as, bm); as = length ap;
\<exists> bstp. abc_steps_l (0, bm) bp bstp = (bs, bm'); bs = length bp;
cs = as + bs; bp \<noteq> []\<rbrakk>
\<Longrightarrow> \<exists> stp. abc_steps_l (0, am) (ap [+] bp) stp = (cs, bm')"
apply(insert abc_append_exc1[of bm bp bs bm' as ap "[]"], simp)
apply(drule_tac bp = "abc_shift bp (length ap)" in abc_add_exc1, simp)
apply(subgoal_tac "ap @ abc_shift bp (length ap) = ap [+] bp",
simp, auto)
apply(rule_tac x = "stpa + stp" in exI, simp add: abc_steps_add)
apply(simp add: abc_append.simps)
done
lemma exp_length[simp]: "length (a\<^bsup>b\<^esup>) = b"
by(simp add: exponent_def)
lemma exponent_add_iff: "a\<^bsup>b\<^esup> @ a\<^bsup>c \<^esup>@ xs = a\<^bsup>b + c \<^esup>@ xs"
apply(auto simp: exponent_def replicate_add)
done
lemma exponent_cons_iff: "a # a\<^bsup>c \<^esup>@ xs = a\<^bsup>Suc c \<^esup>@ xs"
apply(auto simp: exponent_def replicate_add)
done
lemma [simp]: "length lm = n \<Longrightarrow>
abc_steps_l (Suc 0, lm @ Suc x # 0 # suf_lm)
[Inc n, Dec (Suc n) 3, Goto (Suc 0)] (Suc (Suc 0))
= (3, lm @ Suc x # 0 # suf_lm)"
apply(simp add: abc_steps_l.simps abc_fetch.simps
abc_step_l.simps abc_lm_v.simps abc_lm_s.simps
nth_append list_update_append)
done
lemma [simp]:
"length lm = n \<Longrightarrow>
abc_steps_l (Suc 0, lm @ Suc x # Suc y # suf_lm)
[Inc n, Dec (Suc n) 3, Goto (Suc 0)] (Suc (Suc 0))
= (Suc 0, lm @ Suc x # y # suf_lm)"
apply(simp add: abc_steps_l.simps abc_fetch.simps
abc_step_l.simps abc_lm_v.simps abc_lm_s.simps
nth_append list_update_append)
done
lemma pr_cycle_part_middle_inv:
"\<lbrakk>length lm = n\<rbrakk> \<Longrightarrow>
\<exists> stp. abc_steps_l (0, lm @ x # y # suf_lm)
[Inc n, Dec (Suc n) 3, Goto (Suc 0)] stp
= (3, lm @ Suc x # 0 # suf_lm)"
proof -
assume h: "length lm = n"
hence k1: "\<exists> stp. abc_steps_l (0, lm @ x # y # suf_lm)
[Inc n, Dec (Suc n) 3, Goto (Suc 0)] stp
= (Suc 0, lm @ Suc x # y # suf_lm)"
apply(rule_tac x = "Suc 0" in exI)
apply(simp add: abc_steps_l.simps abc_step_l.simps
abc_lm_v.simps abc_lm_s.simps nth_append
list_update_append abc_fetch.simps)
done
from h have k2:
"\<exists> stp. abc_steps_l (Suc 0, lm @ Suc x # y # suf_lm)
[Inc n, Dec (Suc n) 3, Goto (Suc 0)] stp
= (3, lm @ Suc x # 0 # suf_lm)"
apply(induct y)
apply(rule_tac x = "Suc (Suc 0)" in exI, simp, simp,
erule_tac exE)
apply(rule_tac x = "Suc (Suc 0) + stp" in exI,
simp only: abc_steps_add, simp)
done
from k1 and k2 show
"\<exists> stp. abc_steps_l (0, lm @ x # y # suf_lm)
[Inc n, Dec (Suc n) 3, Goto (Suc 0)] stp
= (3, lm @ Suc x # 0 # suf_lm)"
apply(erule_tac exE, erule_tac exE)
apply(rule_tac x = "stp + stpa" in exI, simp add: abc_steps_add)
done
qed
lemma [simp]:
"length lm = Suc n \<Longrightarrow>
(abc_steps_l (length ap, lm @ x # Suc y # suf_lm)
(ap @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length ap)])
(Suc (Suc (Suc 0))))
= (length ap, lm @ Suc x # y # suf_lm)"
apply(simp add: abc_steps_l.simps abc_fetch.simps abc_step_l.simps
abc_lm_v.simps list_update_append nth_append abc_lm_s.simps)
done
lemma switch_para_inv:
assumes bp_def:"bp = ap @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto ss]"
and h: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md)"
"ss = length ap"
"length lm = Suc n"
shows " \<exists>stp. abc_steps_l (ss, lm @ x # y # suf_lm) bp stp =
(0, lm @ (x + y) # 0 # suf_lm)"
apply(induct y arbitrary: x)
apply(rule_tac x = "Suc 0" in exI,
simp add: bp_def empty.simps abc_steps_l.simps
abc_fetch.simps h abc_step_l.simps
abc_lm_v.simps list_update_append nth_append
abc_lm_s.simps)
proof -
fix y x
assume ind:
"\<And>x. \<exists>stp. abc_steps_l (ss, lm @ x # y # suf_lm) bp stp =
(0, lm @ (x + y) # 0 # suf_lm)"
show "\<exists>stp. abc_steps_l (ss, lm @ x # Suc y # suf_lm) bp stp =
(0, lm @ (x + Suc y) # 0 # suf_lm)"
apply(insert ind[of "Suc x"], erule_tac exE)
apply(rule_tac x = "Suc (Suc (Suc 0)) + stp" in exI,
simp only: abc_steps_add bp_def h)
apply(simp add: h)
done
qed
lemma [simp]:
"length lm = rs_pos \<and> Suc (Suc rs_pos) < a_md \<and> 0 < rs_pos \<Longrightarrow>
a_md - Suc 0 < Suc (Suc (Suc (a_md + length suf_lm -
Suc (Suc (Suc 0)))))"
apply(arith)
done
lemma [simp]:
"Suc (Suc rs_pos) < a_md \<and> 0 < rs_pos \<Longrightarrow>
\<not> a_md - Suc 0 < rs_pos - Suc 0"
apply(arith)
done
lemma [simp]:
"Suc (Suc rs_pos) < a_md \<and> 0 < rs_pos \<Longrightarrow>
\<not> a_md - rs_pos < Suc (Suc (a_md - Suc (Suc rs_pos)))"
apply(arith)
done
lemma butlast_append_last: "lm \<noteq> [] \<Longrightarrow> lm = butlast lm @ [last lm]"
apply(auto)
done
lemma [simp]: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md)
\<Longrightarrow> (Suc (Suc rs_pos)) < a_md"
apply(simp add: rec_ci.simps)
apply(case_tac "rec_ci f", simp)
apply(case_tac "rec_ci g", simp)
apply(arith)
done
(*
lemma pr_para_ge_suc0: "rec_calc_rel (Pr n f g) lm xs \<Longrightarrow> 0 < n"
apply(erule calc_pr_reverse, simp, simp)
done
*)
lemma ci_pr_para_eq: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md)
\<Longrightarrow> rs_pos = Suc n"
apply(simp add: rec_ci.simps)
apply(case_tac "rec_ci g", case_tac "rec_ci f", simp)
done
lemma [intro]:
"\<lbrakk>rec_ci z = (aprog, rs_pos, a_md); rec_calc_rel z lm xs\<rbrakk>
\<Longrightarrow> length lm = rs_pos"
apply(simp add: rec_ci.simps rec_ci_z_def)
apply(erule_tac calc_z_reverse, simp)
done
lemma [intro]:
"\<lbrakk>rec_ci s = (aprog, rs_pos, a_md); rec_calc_rel s lm xs\<rbrakk>
\<Longrightarrow> length lm = rs_pos"
apply(simp add: rec_ci.simps rec_ci_s_def)
apply(erule_tac calc_s_reverse, simp)
done
lemma [intro]:
"\<lbrakk>rec_ci (recf.id nat1 nat2) = (aprog, rs_pos, a_md);
rec_calc_rel (recf.id nat1 nat2) lm xs\<rbrakk> \<Longrightarrow> length lm = rs_pos"
apply(simp add: rec_ci.simps rec_ci_id.simps)
apply(erule_tac calc_id_reverse, simp)
done
lemma [intro]:
"\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
rec_calc_rel (Cn n f gs) lm xs\<rbrakk> \<Longrightarrow> length lm = rs_pos"
apply(erule_tac calc_cn_reverse, simp)
apply(simp add: rec_ci.simps)
apply(case_tac "rec_ci f", simp)
done
lemma [intro]:
"\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
rec_calc_rel (Pr n f g) lm xs\<rbrakk> \<Longrightarrow> length lm = rs_pos"
apply(erule_tac calc_pr_reverse, simp)
apply(drule_tac ci_pr_para_eq, simp, simp)
apply(drule_tac ci_pr_para_eq, simp)
done
lemma [intro]:
"\<lbrakk>rec_ci (Mn n f) = (aprog, rs_pos, a_md);
rec_calc_rel (Mn n f) lm xs\<rbrakk> \<Longrightarrow> length lm = rs_pos"
apply(erule_tac calc_mn_reverse)
apply(simp add: rec_ci.simps)
apply(case_tac "rec_ci f", simp)
done
lemma para_pattern:
"\<lbrakk>rec_ci f = (aprog, rs_pos, a_md); rec_calc_rel f lm xs\<rbrakk>
\<Longrightarrow> length lm = rs_pos"
apply(case_tac f, auto)
done
lemma ci_pr_g_paras:
"\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
rec_ci g = (a, aa, ba);
rec_calc_rel (Pr n f g) (lm @ [x]) rs; x > 0\<rbrakk> \<Longrightarrow>
aa = Suc rs_pos "
apply(erule calc_pr_reverse, simp)
apply(subgoal_tac "length (args @ [k, rk]) = aa", simp)
apply(subgoal_tac "rs_pos = Suc n", simp)
apply(simp add: ci_pr_para_eq)
apply(erule para_pattern, simp)
done
lemma ci_pr_g_md_less:
"\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
rec_ci g = (a, aa, ba)\<rbrakk> \<Longrightarrow> ba < a_md"
apply(simp add: rec_ci.simps)
apply(case_tac "rec_ci f", auto)
done
lemma [intro]: "rec_ci z = (ap, rp, ad) \<Longrightarrow> rp < ad"
by(simp add: rec_ci.simps)
lemma [intro]: "rec_ci s = (ap, rp, ad) \<Longrightarrow> rp < ad"
by(simp add: rec_ci.simps)
lemma [intro]: "rec_ci (recf.id nat1 nat2) = (ap, rp, ad) \<Longrightarrow> rp < ad"
by(simp add: rec_ci.simps)
lemma [intro]: "rec_ci (Cn n f gs) = (ap, rp, ad) \<Longrightarrow> rp < ad"
apply(simp add: rec_ci.simps)
apply(case_tac "rec_ci f", simp)
done
lemma [intro]: "rec_ci (Pr n f g) = (ap, rp, ad) \<Longrightarrow> rp < ad"
apply(simp add: rec_ci.simps)
by(case_tac "rec_ci f", case_tac "rec_ci g", auto)
lemma [intro]: "rec_ci (Mn n f) = (ap, rp, ad) \<Longrightarrow> rp < ad"
apply(simp add: rec_ci.simps)
apply(case_tac "rec_ci f", simp)
apply(arith)
done
lemma ci_ad_ge_paras: "rec_ci f = (ap, rp, ad) \<Longrightarrow> ad > rp"
apply(case_tac f, auto)
done
lemma [elim]: "\<lbrakk>a [+] b = []; a \<noteq> [] \<or> b \<noteq> []\<rbrakk> \<Longrightarrow> RR"
apply(auto simp: abc_append.simps abc_shift.simps)
done
lemma [intro]: "rec_ci z = ([], aa, ba) \<Longrightarrow> False"
by(simp add: rec_ci.simps rec_ci_z_def)
lemma [intro]: "rec_ci s = ([], aa, ba) \<Longrightarrow> False"
by(auto simp: rec_ci.simps rec_ci_s_def addition.simps)
lemma [intro]: "rec_ci (id m n) = ([], aa, ba) \<Longrightarrow> False"
by(auto simp: rec_ci.simps rec_ci_id.simps addition.simps)
lemma [intro]: "rec_ci (Cn n f gs) = ([], aa, ba) \<Longrightarrow> False"
apply(case_tac "rec_ci f", auto simp: rec_ci.simps abc_append.simps)
apply(simp add: abc_shift.simps empty.simps)
done
lemma [intro]: "rec_ci (Pr n f g) = ([], aa, ba) \<Longrightarrow> False"
apply(simp add: rec_ci.simps)
apply(case_tac "rec_ci f", case_tac "rec_ci g")
by(auto)
lemma [intro]: "rec_ci (Mn n f) = ([], aa, ba) \<Longrightarrow> False"
apply(case_tac "rec_ci f", auto simp: rec_ci.simps)
done
lemma rec_ci_not_null: "rec_ci g = (a, aa, ba) \<Longrightarrow> a \<noteq> []"
by(case_tac g, auto)
lemma calc_pr_g_def:
"\<lbrakk>rec_calc_rel (Pr rs_pos f g) (lm @ [Suc x]) rsa;
rec_calc_rel (Pr rs_pos f g) (lm @ [x]) rsxa\<rbrakk>
\<Longrightarrow> rec_calc_rel g (lm @ [x, rsxa]) rsa"
apply(erule_tac calc_pr_reverse, simp, simp)
apply(subgoal_tac "rsxa = rk", simp)
apply(erule_tac rec_calc_inj, auto)
done
lemma ci_pr_md_def:
"\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
rec_ci g = (a, aa, ba); rec_ci f = (ab, ac, bc)\<rbrakk>
\<Longrightarrow> a_md = Suc (max (n + 3) (max bc ba))"
by(simp add: rec_ci.simps)
lemma ci_pr_f_paras:
"\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
rec_calc_rel (Pr n f g) lm rs;
rec_ci f = (ab, ac, bc)\<rbrakk> \<Longrightarrow> ac = rs_pos - Suc 0"
apply(subgoal_tac "\<exists>rs. rec_calc_rel f (butlast lm) rs",
erule_tac exE)
apply(drule_tac f = f and lm = "butlast lm" in para_pattern,
simp, simp)
apply(drule_tac para_pattern, simp)
apply(subgoal_tac "lm \<noteq> []", simp)
apply(erule_tac calc_pr_reverse, simp, simp)
apply(erule calc_pr_zero_ex)
done
lemma ci_pr_md_ge_f: "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
rec_ci f = (ab, ac, bc)\<rbrakk> \<Longrightarrow> Suc bc \<le> a_md"
apply(case_tac "rec_ci g")
apply(simp add: rec_ci.simps, auto)
done
lemma ci_pr_md_ge_g: "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
rec_ci g = (ab, ac, bc)\<rbrakk> \<Longrightarrow> bc < a_md"
apply(case_tac "rec_ci f")
apply(simp add: rec_ci.simps, auto)
done
lemma rec_calc_rel_def0:
"\<lbrakk>rec_calc_rel (Pr n f g) lm rs; rec_calc_rel f (butlast lm) rsa\<rbrakk>
\<Longrightarrow> rec_calc_rel (Pr n f g) (butlast lm @ [0]) rsa"
apply(rule_tac calc_pr_zero, simp)
apply(erule_tac calc_pr_reverse, simp, simp, simp)
done
lemma [simp]: "length (empty m n) = 3"
by (auto simp: empty.simps)
(*
lemma
"\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
rec_calc_rel (Pr n f g) lm rs;
rec_ci g = (a, aa, ba);
rec_ci f = (ab, ac, bc)\<rbrakk>
\<Longrightarrow> \<exists>ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = 3 + length ab \<and> bp = recursive.empty (n - Suc 0) n 3"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "recursive.empty (n - Suc 0) (max (Suc (Suc n)) (max bc ba)) 3 [+] ab" in exI, simp)
apply(rule_tac x = "([Dec (max (Suc (Suc n)) (max bc ba)) (length a + 7)] [+] a [+]
[Inc (n - Suc 0), Dec n 3, Goto (Suc 0)]) @ [Dec (Suc n) 0, Inc n, Goto (length a + 4)]" in exI, simp)
apply(auto simp: abc_append_commute)
done
lemma "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
rec_ci g = (a, aa, ba); rec_ci f = (ab, ac, bc)\<rbrakk>
\<Longrightarrow> \<exists>ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = 3 \<and> bp = ab"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "recursive.empty (n - Suc 0) (max (Suc (Suc n)) (max bc ba)) 3" in exI, simp)
apply(rule_tac x = "recursive.empty (n - Suc 0) n 3 [+]
([Dec (max (Suc (Suc n)) (max bc ba)) (length a + 7)] [+] a
[+] [Inc (n - Suc 0), Dec n 3, Goto (Suc 0)]) @ [Dec (Suc n) 0, Inc n, Goto (length a + 4)]" in exI, auto)
apply(simp add: abc_append_commute)
done
*)
lemma [simp]: "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md); rec_calc_rel (Pr n f g) lm rs\<rbrakk>
\<Longrightarrow> rs_pos = Suc n"
apply(simp add: ci_pr_para_eq)
done
lemma [simp]: "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md); rec_calc_rel (Pr n f g) lm rs\<rbrakk>
\<Longrightarrow> length lm = Suc n"
apply(subgoal_tac "rs_pos = Suc n", rule_tac para_pattern, simp, simp)
apply(case_tac "rec_ci f", case_tac "rec_ci g", simp add: rec_ci.simps)
done
lemma [simp]: "rec_ci (Pr n f g) = (a, rs_pos, a_md) \<Longrightarrow> Suc (Suc n) < a_md"
apply(case_tac "rec_ci f", case_tac "rec_ci g", simp add: rec_ci.simps)
apply arith
done
lemma [simp]: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md) \<Longrightarrow> 0 < rs_pos"
apply(case_tac "rec_ci f", case_tac "rec_ci g")
apply(simp add: rec_ci.simps)
done
lemma [simp]: "Suc (Suc rs_pos) < a_md \<Longrightarrow>
butlast lm @ (last lm - xa) # (rsa::nat) # 0 # 0\<^bsup>a_md - Suc (Suc (Suc rs_pos))\<^esup> @ xa # suf_lm =
butlast lm @ (last lm - xa) # rsa # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ xa # suf_lm"
apply(simp add: exp_ind_def[THEN sym])
done
lemma pr_cycle_part_ind:
assumes g_ind:
"\<And>lm rs suf_lm. rec_calc_rel g lm rs \<Longrightarrow>
\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>ba - aa\<^esup> @ suf_lm) a stp =
(length a, lm @ rs # 0\<^bsup>ba - Suc aa\<^esup> @ suf_lm)"
and ap_def:
"ap = ([Dec (a_md - Suc 0) (length a + 7)] [+]
(a [+] [Inc (rs_pos - Suc 0), Dec rs_pos 3, Goto (Suc 0)])) @
[Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]"
and h: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md)"
"rec_calc_rel (Pr n f g)
(butlast lm @ [last lm - Suc xa]) rsxa"
"Suc xa \<le> last lm"
"rec_ci g = (a, aa, ba)"
"rec_calc_rel (Pr n f g) (butlast lm @ [last lm - xa]) rsa"
"lm \<noteq> []"
shows
"\<exists>stp. abc_steps_l
(0, butlast lm @ (last lm - Suc xa) # rsxa #
0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ Suc xa # suf_lm) ap stp =
(0, butlast lm @ (last lm - xa) # rsa
# 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ xa # suf_lm)"
proof -
have k1: "\<exists>stp. abc_steps_l (0, butlast lm @ (last lm - Suc xa) #
rsxa # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ Suc xa # suf_lm) ap stp =
(length a + 4, butlast lm @ (last lm - xa) # 0 # rsa #
0\<^bsup>a_md - Suc (Suc (Suc rs_pos))\<^esup> @ xa # suf_lm)"
apply(simp add: ap_def, rule_tac abc_add_exc1)
apply(rule_tac as = "Suc 0" and
bm = "butlast lm @ (last lm - Suc xa) #
rsxa # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ xa # suf_lm" in abc_append_exc2,
auto)
proof -
show
"\<exists>astp. abc_steps_l (0, butlast lm @ (last lm - Suc xa) # rsxa
# 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ Suc xa # suf_lm)
[Dec (a_md - Suc 0)(length a + 7)] astp =
(Suc 0, butlast lm @ (last lm - Suc xa) #
rsxa # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ xa # suf_lm)"
apply(rule_tac x = "Suc 0" in exI,
simp add: abc_steps_l.simps abc_step_l.simps
abc_fetch.simps)
apply(subgoal_tac "length lm = Suc n \<and> rs_pos = Suc n \<and>
a_md > Suc (Suc rs_pos)")
apply(simp add: abc_lm_v.simps nth_append abc_lm_s.simps)
apply(insert nth_append[of
"(last lm - Suc xa) # rsxa # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup>"
"Suc xa # suf_lm" "(a_md - rs_pos)"], simp)
apply(simp add: list_update_append del: list_update.simps)
apply(insert list_update_append[of "(last lm - Suc xa) # rsxa #
0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup>"
"Suc xa # suf_lm" "a_md - rs_pos" "xa"], simp)
apply(case_tac a_md, simp, simp)
apply(insert h, simp)
apply(insert para_pattern[of "Pr n f g" aprog rs_pos a_md
"(butlast lm @ [last lm - Suc xa])" rsxa], simp)
done
next
show "\<exists>bstp. abc_steps_l (0, butlast lm @ (last lm - Suc xa) #
rsxa # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ xa # suf_lm) (a [+]
[Inc (rs_pos - Suc 0), Dec rs_pos 3, Goto (Suc 0)]) bstp =
(3 + length a, butlast lm @ (last lm - xa) # 0 # rsa #
0\<^bsup>a_md - Suc (Suc (Suc rs_pos))\<^esup> @ xa # suf_lm)"
apply(rule_tac as = "length a" and
bm = "butlast lm @ (last lm - Suc xa) # rsxa # rsa #
0\<^bsup>a_md - Suc (Suc (Suc rs_pos))\<^esup> @ xa # suf_lm"
in abc_append_exc2, simp_all)
proof -
from h have j1: "aa = Suc rs_pos \<and> a_md > ba \<and> ba > Suc rs_pos"
apply(insert h)
apply(insert ci_pr_g_paras[of n f g aprog rs_pos
a_md a aa ba "butlast lm" "last lm - xa" rsa], simp)
apply(drule_tac ci_pr_md_ge_g, auto)
apply(erule_tac ci_ad_ge_paras)
done
from h have j2: "rec_calc_rel g (butlast lm @
[last lm - Suc xa, rsxa]) rsa"
apply(rule_tac calc_pr_g_def, simp, simp)
done
from j1 and j2 show
"\<exists>astp. abc_steps_l (0, butlast lm @ (last lm - Suc xa) #
rsxa # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ xa # suf_lm) a astp =
(length a, butlast lm @ (last lm - Suc xa) # rsxa # rsa
# 0\<^bsup>a_md - Suc (Suc (Suc rs_pos))\<^esup> @ xa # suf_lm)"
apply(insert g_ind[of
"butlast lm @ (last lm - Suc xa) # [rsxa]" rsa
"0\<^bsup>a_md - ba - Suc 0 \<^esup> @ xa # suf_lm"], simp, auto)
apply(simp add: exponent_add_iff)
apply(rule_tac x = stp in exI, simp add: numeral_3_eq_3)
done
next
from h have j3: "length lm = rs_pos \<and> rs_pos > 0"
apply(rule_tac conjI)
apply(drule_tac lm = "(butlast lm @ [last lm - Suc xa])"
and xs = rsxa in para_pattern, simp, simp, simp)
done
from h have j4: "Suc (last lm - Suc xa) = last lm - xa"
apply(case_tac "last lm", simp, simp)
done
from j3 and j4 show
"\<exists>bstp. abc_steps_l (0, butlast lm @ (last lm - Suc xa) # rsxa #
rsa # 0\<^bsup>a_md - Suc (Suc (Suc rs_pos))\<^esup> @ xa # suf_lm)
[Inc (rs_pos - Suc 0), Dec rs_pos 3, Goto (Suc 0)] bstp =
(3, butlast lm @ (last lm - xa) # 0 # rsa #
0\<^bsup>a_md - Suc (Suc (Suc rs_pos))\<^esup> @ xa # suf_lm)"
apply(insert pr_cycle_part_middle_inv[of "butlast lm"
"rs_pos - Suc 0" "(last lm - Suc xa)" rsxa
"rsa # 0\<^bsup>a_md - Suc (Suc (Suc rs_pos))\<^esup> @ xa # suf_lm"], simp)
done
qed
qed
from h have k2:
"\<exists>stp. abc_steps_l (length a + 4, butlast lm @ (last lm - xa) # 0
# rsa # 0\<^bsup>a_md - Suc (Suc (Suc rs_pos))\<^esup> @ xa # suf_lm) ap stp =
(0, butlast lm @ (last lm - xa) # rsa # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ xa # suf_lm)"
apply(insert switch_para_inv[of ap
"([Dec (a_md - Suc 0) (length a + 7)] [+]
(a [+] [Inc (rs_pos - Suc 0), Dec rs_pos 3, Goto (Suc 0)]))"
n "length a + 4" f g aprog rs_pos a_md
"butlast lm @ [last lm - xa]" 0 rsa
"0\<^bsup>a_md - Suc (Suc (Suc rs_pos))\<^esup> @ xa # suf_lm"])
apply(simp add: h ap_def)
apply(subgoal_tac "length lm = Suc n \<and> Suc (Suc rs_pos) < a_md",
simp)
apply(insert h, simp)
apply(frule_tac lm = "(butlast lm @ [last lm - Suc xa])"
and xs = rsxa in para_pattern, simp, simp)
done
from k1 and k2 show "?thesis"
apply(auto)
apply(rule_tac x = "stp + stpa" in exI, simp add: abc_steps_add)
done
qed
lemma ci_pr_ex1:
"\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
rec_ci g = (a, aa, ba);
rec_ci f = (ab, ac, bc)\<rbrakk>
\<Longrightarrow> \<exists>ap bp. length ap = 6 + length ab \<and>
aprog = ap [+] bp \<and>
bp = ([Dec (a_md - Suc 0) (length a + 7)] [+] (a [+]
[Inc (rs_pos - Suc 0), Dec rs_pos 3, Goto (Suc 0)])) @
[Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "recursive.empty n (max (Suc (Suc (Suc n)))
(max bc ba)) [+] ab [+] recursive.empty n (Suc n)" in exI,
simp)
apply(auto simp add: abc_append_commute add3_Suc)
done
lemma pr_cycle_part:
"\<lbrakk>\<And>lm rs suf_lm. rec_calc_rel g lm rs \<Longrightarrow>
\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>ba - aa\<^esup> @ suf_lm) a stp =
(length a, lm @ rs # 0\<^bsup>ba - Suc aa\<^esup> @ suf_lm);
rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
rec_calc_rel (Pr n f g) lm rs;
rec_ci g = (a, aa, ba);
rec_calc_rel (Pr n f g) (butlast lm @ [last lm - x]) rsx;
rec_ci f = (ab, ac, bc);
lm \<noteq> [];
x \<le> last lm\<rbrakk> \<Longrightarrow>
\<exists>stp. abc_steps_l (6 + length ab, butlast lm @ (last lm - x) #
rsx # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ x # suf_lm) aprog stp =
(6 + length ab, butlast lm @ last lm # rs #
0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ 0 # suf_lm)"
proof -
assume g_ind:
"\<And>lm rs suf_lm. rec_calc_rel g lm rs \<Longrightarrow>
\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>ba - aa\<^esup> @ suf_lm) a stp =
(length a, lm @ rs # 0\<^bsup>ba - Suc aa\<^esup> @ suf_lm)"
and h: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md)"
"rec_calc_rel (Pr n f g) lm rs"
"rec_ci g = (a, aa, ba)"
"rec_calc_rel (Pr n f g) (butlast lm @ [last lm - x]) rsx"
"lm \<noteq> []"
"x \<le> last lm"
"rec_ci f = (ab, ac, bc)"
from h show
"\<exists>stp. abc_steps_l (6 + length ab, butlast lm @ (last lm - x) #
rsx # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ x # suf_lm) aprog stp =
(6 + length ab, butlast lm @ last lm # rs #
0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ 0 # suf_lm)"
proof(induct x arbitrary: rsx, simp_all)
fix rsxa
assume "rec_calc_rel (Pr n f g) lm rsxa"
"rec_calc_rel (Pr n f g) lm rs"
from h and this have "rs = rsxa"
apply(subgoal_tac "lm \<noteq> [] \<and> rs_pos = Suc n", simp)
apply(rule_tac rec_calc_inj, simp, simp)
apply(simp)
done
thus "\<exists>stp. abc_steps_l (6 + length ab, butlast lm @ last lm #
rsxa # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ 0 # suf_lm) aprog stp =
(6 + length ab, butlast lm @ last lm # rs #
0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ 0 # suf_lm)"
by(rule_tac x = 0 in exI, simp add: abc_steps_l.simps)
next
fix xa rsxa
assume ind:
"\<And>rsx. rec_calc_rel (Pr n f g) (butlast lm @ [last lm - xa]) rsx
\<Longrightarrow> \<exists>stp. abc_steps_l (6 + length ab, butlast lm @ (last lm - xa) #
rsx # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ xa # suf_lm) aprog stp =
(6 + length ab, butlast lm @ last lm # rs #
0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ 0 # suf_lm)"
and g: "rec_calc_rel (Pr n f g)
(butlast lm @ [last lm - Suc xa]) rsxa"
"Suc xa \<le> last lm"
"rec_ci (Pr n f g) = (aprog, rs_pos, a_md)"
"rec_calc_rel (Pr n f g) lm rs"
"rec_ci g = (a, aa, ba)"
"rec_ci f = (ab, ac, bc)" "lm \<noteq> []"
from g have k1:
"\<exists> rs. rec_calc_rel (Pr n f g) (butlast lm @ [last lm - xa]) rs"
apply(rule_tac rs = rs in calc_pr_less_ex, simp, simp)
done
from g and this show
"\<exists>stp. abc_steps_l (6 + length ab,
butlast lm @ (last lm - Suc xa) # rsxa #
0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ Suc xa # suf_lm) aprog stp =
(6 + length ab, butlast lm @ last lm # rs #
0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ 0 # suf_lm)"
proof(erule_tac exE)
fix rsa
assume k2: "rec_calc_rel (Pr n f g)
(butlast lm @ [last lm - xa]) rsa"
from g and k2 have
"\<exists>stp. abc_steps_l (6 + length ab, butlast lm @
(last lm - Suc xa) # rsxa #
0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ Suc xa # suf_lm) aprog stp
= (6 + length ab, butlast lm @ (last lm - xa) # rsa #
0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ xa # suf_lm)"
proof -
from g have k2_1:
"\<exists> ap bp. length ap = 6 + length ab \<and>
aprog = ap [+] bp \<and>
bp = ([Dec (a_md - Suc 0) (length a + 7)] [+]
(a [+] [Inc (rs_pos - Suc 0), Dec rs_pos 3,
Goto (Suc 0)])) @
[Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]"
apply(rule_tac ci_pr_ex1, auto)
done
from k2_1 and k2 and g show "?thesis"
proof(erule_tac exE, erule_tac exE)
fix ap bp
assume
"length ap = 6 + length ab \<and>
aprog = ap [+] bp \<and> bp =
([Dec (a_md - Suc 0) (length a + 7)] [+]
(a [+] [Inc (rs_pos - Suc 0), Dec rs_pos 3,
Goto (Suc 0)])) @
[Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]"
from g and this and k2 and g_ind show "?thesis"
apply(insert abc_append_exc3[of
"butlast lm @ (last lm - Suc xa) # rsxa #
0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ Suc xa # suf_lm" bp 0
"butlast lm @ (last lm - xa) # rsa #
0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ xa # suf_lm" "length ap" ap],
simp)
apply(subgoal_tac
"\<exists>stp. abc_steps_l (0, butlast lm @ (last lm - Suc xa)
# rsxa # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ Suc xa #
suf_lm) bp stp =
(0, butlast lm @ (last lm - xa) # rsa #
0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ xa # suf_lm)",
simp, erule_tac conjE, erule conjE)
apply(erule pr_cycle_part_ind, auto)
done
qed
qed
from g and k2 and this show "?thesis"
apply(erule_tac exE)
apply(insert ind[of rsa], simp)
apply(erule_tac exE)
apply(rule_tac x = "stp + stpa" in exI,
simp add: abc_steps_add)
done
qed
qed
qed
lemma ci_pr_length:
"\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
rec_ci g = (a, aa, ba);
rec_ci f = (ab, ac, bc)\<rbrakk>
\<Longrightarrow> length aprog = 13 + length ab + length a"
apply(auto simp: rec_ci.simps)
done
thm empty.simps
term max
fun empty_inv :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool"
where
"empty_inv (as, lm) m n initlm =
(let plus = initlm ! m + initlm ! n in
length initlm > max m n \<and> m \<noteq> n \<and>
(if as = 0 then \<exists> k l. lm = initlm[m := k, n := l] \<and>
k + l = plus \<and> k \<le> initlm ! m
else if as = 1 then \<exists> k l. lm = initlm[m := k, n := l]
\<and> k + l + 1 = plus \<and> k < initlm ! m
else if as = 2 then \<exists> k l. lm = initlm[m := k, n := l]
\<and> k + l = plus \<and> k \<le> initlm ! m
else if as = 3 then lm = initlm[m := 0, n := plus]
else False))"
fun empty_stage1 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat"
where
"empty_stage1 (as, lm) m =
(if as = 3 then 0
else 1)"
fun empty_stage2 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat"
where
"empty_stage2 (as, lm) m = (lm ! m)"
fun empty_stage3 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat"
where
"empty_stage3 (as, lm) m = (if as = 1 then 3
else if as = 2 then 2
else if as = 0 then 1
else 0)"
fun empty_measure :: "((nat \<times> nat list) \<times> nat) \<Rightarrow> (nat \<times> nat \<times> nat)"
where
"empty_measure ((as, lm), m) =
(empty_stage1 (as, lm) m, empty_stage2 (as, lm) m,
empty_stage3 (as, lm) m)"
definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set"
where
"lex_pair = less_than <*lex*> less_than"
definition lex_triple ::
"((nat \<times> (nat \<times> nat)) \<times> (nat \<times> (nat \<times> nat))) set"
where
"lex_triple \<equiv> less_than <*lex*> lex_pair"
definition empty_LE ::
"(((nat \<times> nat list) \<times> nat) \<times> ((nat \<times> nat list) \<times> nat)) set"
where
"empty_LE \<equiv> (inv_image lex_triple empty_measure)"
lemma wf_lex_triple: "wf lex_triple"
by (auto intro:wf_lex_prod simp:lex_triple_def lex_pair_def)
lemma wf_empty_le[intro]: "wf empty_LE"
by(auto intro:wf_inv_image wf_lex_triple simp: empty_LE_def)
declare empty_inv.simps[simp del]
lemma empty_inv_init:
"\<lbrakk>m < length initlm; n < length initlm; m \<noteq> n\<rbrakk> \<Longrightarrow>
empty_inv (0, initlm) m n initlm"
apply(simp add: abc_steps_l.simps empty_inv.simps)
apply(rule_tac x = "initlm ! m" in exI,
rule_tac x = "initlm ! n" in exI, simp)
done
lemma [simp]: "abc_fetch 0 (recursive.empty m n) = Some (Dec m 3)"
apply(simp add: empty.simps abc_fetch.simps)
done
lemma [simp]: "abc_fetch (Suc 0) (recursive.empty m n) =
Some (Inc n)"
apply(simp add: empty.simps abc_fetch.simps)
done
lemma [simp]: "abc_fetch 2 (recursive.empty m n) = Some (Goto 0)"
apply(simp add: empty.simps abc_fetch.simps)
done
lemma [simp]: "abc_fetch 3 (recursive.empty m n) = None"
apply(simp add: empty.simps abc_fetch.simps)
done
lemma [simp]:
"\<lbrakk>m \<noteq> n; m < length initlm; n < length initlm;
k + l = initlm ! m + initlm ! n; k \<le> initlm ! m; 0 < k\<rbrakk>
\<Longrightarrow> \<exists>ka la. initlm[m := k, n := l, m := k - Suc 0] =
initlm[m := ka, n := la] \<and>
Suc (ka + la) = initlm ! m + initlm ! n \<and>
ka < initlm ! m"
apply(rule_tac x = "k - Suc 0" in exI, rule_tac x = l in exI,
simp, auto)
apply(subgoal_tac
"initlm[m := k, n := l, m := k - Suc 0] =
initlm[n := l, m := k, m := k - Suc 0]")
apply(simp add: list_update_overwrite )
apply(simp add: list_update_swap)
apply(simp add: list_update_swap)
done
lemma [simp]:
"\<lbrakk>m \<noteq> n; m < length initlm; n < length initlm;
Suc (k + l) = initlm ! m + initlm ! n;
k < initlm ! m\<rbrakk>
\<Longrightarrow> \<exists>ka la. initlm[m := k, n := l, n := Suc l] =
initlm[m := ka, n := la] \<and>
ka + la = initlm ! m + initlm ! n \<and>
ka \<le> initlm ! m"
apply(rule_tac x = k in exI, rule_tac x = "Suc l" in exI, auto)
done
lemma [simp]:
"\<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) (recursive.empty m n) na) m \<and>
empty_inv (abc_steps_l (0, initlm)
(recursive.empty m n) na) m n initlm \<longrightarrow>
empty_inv (abc_steps_l (0, initlm)
(recursive.empty m n) (Suc na)) m n initlm \<and>
((abc_steps_l (0, initlm) (recursive.empty m n) (Suc na), m),
abc_steps_l (0, initlm) (recursive.empty m n) na, m) \<in> empty_LE"
apply(rule allI, rule impI, simp add: abc_steps_ind)
apply(case_tac "(abc_steps_l (0, initlm) (recursive.empty m n) na)",
simp)
apply(auto split:if_splits simp add:abc_steps_l.simps empty_inv.simps)
apply(auto simp add: empty_LE_def lex_triple_def lex_pair_def
abc_step_l.simps abc_steps_l.simps
empty_inv.simps abc_lm_v.simps abc_lm_s.simps
split: if_splits )
apply(rule_tac x = k in exI, rule_tac x = "Suc l" in exI, simp)
done
lemma empty_inv_halt:
"\<lbrakk>length initlm > max m n; m \<noteq> n\<rbrakk> \<Longrightarrow>
\<exists> stp. (\<lambda> (as, lm). as = 3 \<and>
empty_inv (as, lm) m n initlm)
(abc_steps_l (0::nat, initlm) (empty m n) stp)"
apply(insert halt_lemma2[of empty_LE
"\<lambda> ((as, lm), m). as = (3::nat)"
"\<lambda> stp. (abc_steps_l (0, initlm) (recursive.empty m n) stp, m)"
"\<lambda> ((as, lm), m). empty_inv (as, lm) m n initlm"])
apply(insert wf_empty_le, simp add: empty_inv_init abc_steps_zero)
apply(erule_tac exE)
apply(rule_tac x = na in exI)
apply(case_tac "(abc_steps_l (0, initlm) (recursive.empty m n) na)",
simp, auto)
done
lemma empty_halt_cond:
"\<lbrakk>m \<noteq> n; empty_inv (a, b) m n lm; a = 3\<rbrakk> \<Longrightarrow>
b = lm[n := lm ! m + lm ! n, m := 0]"
apply(simp add: empty_inv.simps, auto)
apply(simp add: list_update_swap)
done
lemma empty_ex:
"\<lbrakk>length lm > max m n; m \<noteq> n\<rbrakk> \<Longrightarrow>
\<exists> stp. abc_steps_l (0::nat, lm) (empty m n) stp
= (3, (lm[n := (lm ! m + lm ! n)])[m := 0::nat])"
apply(drule empty_inv_halt, simp, erule_tac exE)
apply(rule_tac x = stp in exI)
apply(case_tac "abc_steps_l (0, lm) (recursive.empty m n) stp",
simp)
apply(erule_tac empty_halt_cond, auto)
done
lemma [simp]:
"\<lbrakk>a_md = Suc (max (Suc (Suc n)) (max bc ba));
length lm = rs_pos \<and> rs_pos = n \<and> n > 0\<rbrakk>
\<Longrightarrow> n - Suc 0 < length lm +
(Suc (max (Suc (Suc n)) (max bc ba)) - rs_pos + length suf_lm) \<and>
Suc (Suc n) < length lm + (Suc (max (Suc (Suc n)) (max bc ba)) -
rs_pos + length suf_lm) \<and> bc < length lm + (Suc (max (Suc (Suc n))
(max bc ba)) - rs_pos + length suf_lm) \<and> ba < length lm +
(Suc (max (Suc (Suc n)) (max bc ba)) - rs_pos + length suf_lm)"
apply(arith)
done
lemma [simp]:
"\<lbrakk>a_md = Suc (max (Suc (Suc n)) (max bc ba));
length lm = rs_pos \<and> rs_pos = n \<and> n > 0\<rbrakk>
\<Longrightarrow> n - Suc 0 < Suc (length suf_lm + max (Suc (Suc n)) (max bc ba)) \<and>
Suc n < length suf_lm + max (Suc (Suc n)) (max bc ba) \<and>
bc < Suc (length suf_lm + max (Suc (Suc n)) (max bc ba)) \<and>
ba < Suc (length suf_lm + max (Suc (Suc n)) (max bc ba))"
apply(arith)
done
lemma [simp]: "n - Suc 0 \<noteq> max (Suc (Suc n)) (max bc ba)"
apply(arith)
done
lemma [simp]:
"a_md \<ge> Suc bc \<and> rs_pos > 0 \<and> bc \<ge> rs_pos \<Longrightarrow>
bc - (rs_pos - Suc 0) + a_md - Suc bc = Suc (a_md - rs_pos - Suc 0)"
apply(arith)
done
lemma [simp]: "length lm = n \<and> rs_pos = n \<and> 0 < rs_pos \<and>
Suc rs_pos < a_md
\<Longrightarrow> n - Suc 0 < Suc (Suc (a_md + length suf_lm - Suc (Suc 0)))
\<and> n < Suc (Suc (a_md + length suf_lm - Suc (Suc 0)))"
apply(arith)
done
lemma [simp]: "length lm = n \<and> rs_pos = n \<and> 0 < rs_pos \<and>
Suc rs_pos < a_md \<Longrightarrow> n - Suc 0 \<noteq> n"
by arith
lemma ci_pr_ex2:
"\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
rec_calc_rel (Pr n f g) lm rs;
rec_ci g = (a, aa, ba);
rec_ci f = (ab, ac, bc)\<rbrakk>
\<Longrightarrow> \<exists>ap bp. aprog = ap [+] bp \<and>
ap = empty n (max (Suc (Suc (Suc n))) (max bc ba))"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "(ab [+] (recursive.empty n (Suc n) [+]
([Dec (max (n + 3) (max bc ba)) (length a + 7)]
[+] (a [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) @
[Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]))" in exI, auto)
apply(simp add: abc_append_commute add3_Suc)
done
lemma [simp]:
"max (Suc (Suc (Suc n))) (max bc ba) - n <
Suc (max (Suc (Suc (Suc n))) (max bc ba)) - n"
apply(arith)
done
lemma exp_nth[simp]: "n < m \<Longrightarrow> a\<^bsup>m\<^esup> ! n = a"
apply(simp add: exponent_def)
done
lemma [simp]: "length lm = n \<and> rs_pos = n \<and> 0 < n \<Longrightarrow>
lm[n - Suc 0 := 0::nat] = butlast lm @ [0]"
apply(auto)
apply(insert list_update_append[of "butlast lm" "[last lm]"
"length lm - Suc 0" "0"], simp)
done
lemma [simp]: "\<lbrakk>length lm = n; 0 < n\<rbrakk> \<Longrightarrow> lm ! (n - Suc 0) = last lm"
apply(insert nth_append[of "butlast lm" "[last lm]" "n - Suc 0"],
simp)
apply(insert butlast_append_last[of lm], auto)
done
lemma exp_suc_iff: "a\<^bsup>b\<^esup> @ [a] = a\<^bsup>b + Suc 0\<^esup>"
apply(simp add: exponent_def rep_ind del: replicate.simps)
done
lemma less_not_less[simp]: "n > 0 \<Longrightarrow> \<not> n < n - Suc 0"
by auto
lemma [simp]:
"Suc n < length suf_lm + max (Suc (Suc n)) (max bc ba) \<and>
bc < Suc (length suf_lm + max (Suc (Suc n))
(max bc ba)) \<and>
ba < Suc (length suf_lm + max (Suc (Suc n)) (max bc ba))"
by arith
lemma [simp]: "length lm = n \<and> rs_pos = n \<and> n > 0 \<Longrightarrow>
(lm @ 0\<^bsup>Suc (max (Suc (Suc n)) (max bc ba)) - n\<^esup> @ suf_lm)
[max (Suc (Suc n)) (max bc ba) :=
(lm @ 0\<^bsup>Suc (max (Suc (Suc n)) (max bc ba)) - n\<^esup> @ suf_lm) ! (n - Suc 0) +
(lm @ 0\<^bsup>Suc (max (Suc (Suc n)) (max bc ba)) - n\<^esup> @ suf_lm) !
max (Suc (Suc n)) (max bc ba), n - Suc 0 := 0::nat]
= butlast lm @ 0 # 0\<^bsup>max (Suc (Suc n)) (max bc ba) - n\<^esup> @ last lm # suf_lm"
apply(simp add: nth_append exp_nth list_update_append)
apply(insert list_update_append[of "0\<^bsup>(max (Suc (Suc n)) (max bc ba)) - n\<^esup>"
"[0]" "max (Suc (Suc n)) (max bc ba) - n" "last lm"], simp)
apply(simp add: exp_suc_iff Suc_diff_le del: list_update.simps)
done
lemma exp_eq: "(a = b) = (c\<^bsup>a\<^esup> = c\<^bsup>b\<^esup>)"
apply(auto simp: exponent_def)
done
lemma [simp]:
"\<lbrakk>length lm = n; 0 < n; Suc n < a_md\<rbrakk> \<Longrightarrow>
(butlast lm @ rsa # 0\<^bsup>a_md - Suc n\<^esup> @ last lm # suf_lm)
[n := (butlast lm @ rsa # 0\<^bsup>a_md - Suc n\<^esup> @ last lm # suf_lm) !
(n - Suc 0) + (butlast lm @ rsa # (0::nat)\<^bsup>a_md - Suc n\<^esup> @
last lm # suf_lm) ! n, n - Suc 0 := 0]
= butlast lm @ 0 # rsa # 0\<^bsup>a_md - Suc (Suc n)\<^esup> @ last lm # suf_lm"
apply(simp add: nth_append exp_nth list_update_append)
apply(case_tac "a_md - Suc n", simp, simp add: exponent_def)
done
lemma [simp]:
"Suc (Suc rs_pos) \<le> a_md \<and> length lm = rs_pos \<and> 0 < rs_pos
\<Longrightarrow> a_md - Suc 0 <
Suc (Suc (Suc (a_md + length suf_lm - Suc (Suc (Suc 0)))))"
by arith
lemma [simp]:
"Suc (Suc rs_pos) \<le> a_md \<and> length lm = rs_pos \<and> 0 < rs_pos \<Longrightarrow>
\<not> a_md - Suc 0 < rs_pos - Suc 0"
by arith
lemma [simp]: "Suc (Suc rs_pos) \<le> a_md \<Longrightarrow>
\<not> a_md - Suc 0 < rs_pos - Suc 0"
by arith
lemma [simp]: "\<lbrakk>Suc (Suc rs_pos) \<le> a_md\<rbrakk> \<Longrightarrow>
\<not> a_md - rs_pos < Suc (Suc (a_md - Suc (Suc rs_pos)))"
by arith
lemma [simp]:
"Suc (Suc rs_pos) \<le> a_md \<and> length lm = rs_pos \<and> 0 < rs_pos
\<Longrightarrow> (abc_lm_v (butlast lm @ last lm # rs # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @
0 # suf_lm) (a_md - Suc 0) = 0 \<longrightarrow>
abc_lm_s (butlast lm @ last lm # rs # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @
0 # suf_lm) (a_md - Suc 0) 0 =
lm @ rs # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm) \<and>
abc_lm_v (butlast lm @ last lm # rs # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @
0 # suf_lm) (a_md - Suc 0) = 0"
apply(simp add: abc_lm_v.simps nth_append abc_lm_s.simps)
apply(insert nth_append[of "last lm # rs # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup>"
"0 # suf_lm" "(a_md - rs_pos)"], auto)
apply(simp only: exp_suc_iff)
apply(subgoal_tac "a_md - Suc 0 < a_md + length suf_lm", simp)
apply(case_tac "lm = []", auto)
done
lemma pr_prog_ex[simp]: "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
rec_ci g = (a, aa, ba); rec_ci f = (ab, ac, bc)\<rbrakk>
\<Longrightarrow> \<exists>cp. aprog = recursive.empty n (max (n + 3)
(max bc ba)) [+] cp"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "(ab [+] (recursive.empty n (Suc n) [+]
([Dec (max (n + 3) (max bc ba)) (length a + 7)]
[+] (a [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)]))
@ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]))" in exI)
apply(auto simp: abc_append_commute)
done
lemma [simp]: "empty m n \<noteq> []"
by (simp add: empty.simps)
(*
lemma [simp]: "\<lbrakk>rs_pos = n; 0 < rs_pos ; Suc rs_pos < a_md\<rbrakk> \<Longrightarrow>
n - Suc 0 < a_md + length suf_lm"
by arith
*)
lemma [intro]:
"\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
rec_ci f = (ab, ac, bc)\<rbrakk> \<Longrightarrow>
\<exists>ap. (\<exists>cp. aprog = ap [+] ab [+] cp) \<and> length ap = 3"
apply(case_tac "rec_ci g", simp add: rec_ci.simps)
apply(rule_tac x = "empty n
(max (n + 3) (max bc c))" in exI, simp)
apply(rule_tac x = "recursive.empty n (Suc n) [+]
([Dec (max (n + 3) (max bc c)) (length a + 7)]
[+] a [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])
@ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]" in exI,
auto)
apply(simp add: abc_append_commute)
done
lemma [intro]:
"\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
rec_ci g = (a, aa, ba);
rec_ci f = (ab, ac, bc)\<rbrakk> \<Longrightarrow>
\<exists>ap. (\<exists>cp. aprog = ap [+] recursive.empty n (Suc n) [+] cp)
\<and> length ap = 3 + length ab"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "recursive.empty n (max (n + 3)
(max bc ba)) [+] ab" in exI, simp)
apply(rule_tac x = "([Dec (max (n + 3) (max bc ba))
(length a + 7)] [+] a [+]
[Inc n, Dec (Suc n) 3, Goto (Suc 0)]) @
[Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]" in exI)
apply(auto simp: abc_append_commute)
done
(*
lemma [simp]:
"n - Suc 0 < Suc (max (Suc (Suc n)) (max bc ba) + length suf_lm) \<and>
Suc n < max (Suc (Suc n)) (max bc ba) + length suf_lm \<and>
bc < Suc (max (Suc (Suc n)) (max bc ba) + length suf_lm) \<and>
ba < Suc (max (Suc (Suc n)) (max bc ba) + length suf_lm)"
by arith
*)
lemma [intro]:
"\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
rec_ci g = (a, aa, ba);
rec_ci f = (ab, ac, bc)\<rbrakk>
\<Longrightarrow> \<exists>ap. (\<exists>cp. aprog = ap [+] ([Dec (a_md - Suc 0) (length a + 7)]
[+] (a [+] [Inc (rs_pos - Suc 0), Dec rs_pos 3,
Goto (Suc 0)])) @ [Dec (Suc (Suc n)) 0, Inc (Suc n),
Goto (length a + 4)] [+] cp) \<and>
length ap = 6 + length ab"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "recursive.empty n
(max (n + 3) (max bc ba)) [+] ab [+]
recursive.empty n (Suc n)" in exI, simp)
apply(rule_tac x = "[]" in exI, auto)
apply(simp add: abc_append_commute)
done
(*
lemma [simp]: "\<lbrakk>rs_pos = n; 0 < rs_pos ; Suc rs_pos < a_md\<rbrakk> \<Longrightarrow>
n - Suc 0 < Suc (Suc (a_md + length suf_lm - 2)) \<and>
n < Suc (Suc (a_md + length suf_lm - 2))"
by arith
*)
lemma [simp]:
"n < Suc (max (n + 3) (max bc ba) + length suf_lm) \<and>
Suc (Suc n) < max (n + 3) (max bc ba) + length suf_lm \<and>
bc < Suc (max (n + 3) (max bc ba) + length suf_lm) \<and>
ba < Suc (max (n + 3) (max bc ba) + length suf_lm)"
by arith
lemma [simp]: "n \<noteq> max (n + (3::nat)) (max bc ba)"
by arith
lemma [simp]:"length lm = Suc n \<Longrightarrow> lm[n := (0::nat)] = butlast lm @ [0]"
apply(subgoal_tac "\<exists> xs x. lm = xs @ [x]", auto simp: list_update_append)
apply(rule_tac x = "butlast lm" in exI, rule_tac x = "last lm" in exI)
apply(case_tac lm, auto)
done
lemma [simp]: "length lm = Suc n \<Longrightarrow> lm ! n =last lm"
apply(subgoal_tac "lm \<noteq> []")
apply(simp add: last_conv_nth, case_tac lm, simp_all)
done
lemma [simp]: "length lm = Suc n \<Longrightarrow>
(lm @ (0::nat)\<^bsup>max (n + 3) (max bc ba) - n\<^esup> @ suf_lm)
[max (n + 3) (max bc ba) := (lm @ 0\<^bsup>max (n + 3) (max bc ba) - n\<^esup> @ suf_lm) ! n +
(lm @ 0\<^bsup>max (n + 3) (max bc ba) - n\<^esup> @ suf_lm) ! max (n + 3) (max bc ba), n := 0]
= butlast lm @ 0 # 0\<^bsup>max (n + 3) (max bc ba) - Suc n\<^esup> @ last lm # suf_lm"
apply(auto simp: list_update_append nth_append)
apply(subgoal_tac "(0\<^bsup>max (n + 3) (max bc ba) - n\<^esup>) = 0\<^bsup>max (n + 3) (max bc ba) - Suc n\<^esup> @ [0::nat]")
apply(simp add: list_update_append)
apply(simp add: exp_suc_iff)
done
lemma [simp]: "Suc (Suc n) < a_md \<Longrightarrow>
n < Suc (Suc (a_md + length suf_lm - 2)) \<and>
n < Suc (a_md + length suf_lm - 2)"
by(arith)
lemma [simp]: "\<lbrakk>length lm = Suc n; Suc (Suc n) < a_md\<rbrakk>
\<Longrightarrow>(butlast lm @ (rsa::nat) # 0\<^bsup>a_md - Suc (Suc n)\<^esup> @ last lm # suf_lm)
[Suc n := (butlast lm @ rsa # 0\<^bsup>a_md - Suc (Suc n)\<^esup> @ last lm # suf_lm) ! n +
(butlast lm @ rsa # 0\<^bsup>a_md - Suc (Suc n)\<^esup> @ last lm # suf_lm) ! Suc n, n := 0]
= butlast lm @ 0 # rsa # 0\<^bsup>a_md - Suc (Suc (Suc n))\<^esup> @ last lm # suf_lm"
apply(auto simp: list_update_append)
apply(subgoal_tac "(0\<^bsup>a_md - Suc (Suc n)\<^esup>) = (0::nat) # (0\<^bsup>a_md - Suc (Suc (Suc n))\<^esup>)", simp add: nth_append)
apply(simp add: exp_ind_def[THEN sym])
done
lemma pr_case:
assumes nf_ind:
"\<And> lm rs suf_lm. rec_calc_rel f lm rs \<Longrightarrow>
\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>bc - ac\<^esup> @ suf_lm) ab stp =
(length ab, lm @ rs # 0\<^bsup>bc - Suc ac\<^esup> @ suf_lm)"
and ng_ind: "\<And> lm rs suf_lm. rec_calc_rel g lm rs \<Longrightarrow>
\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>ba - aa\<^esup> @ suf_lm) a stp =
(length a, lm @ rs # 0\<^bsup>ba - Suc aa\<^esup> @ suf_lm)"
and h: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md)" "rec_calc_rel (Pr n f g) lm rs"
"rec_ci g = (a, aa, ba)" "rec_ci f = (ab, ac, bc)"
shows "\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp = (length aprog, lm @ rs # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)"
proof -
from h have k1: "\<exists> stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp
= (3, butlast lm @ 0 # 0\<^bsup>a_md - rs_pos - 1\<^esup> @ last lm # suf_lm)"
proof -
have "\<exists>bp cp. aprog = bp [+] cp \<and> bp = empty n
(max (n + 3) (max bc ba))"
apply(insert h, simp)
apply(erule pr_prog_ex, auto)
done
thus "?thesis"
apply(erule_tac exE, erule_tac exE, simp)
apply(subgoal_tac
"\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm)
([] [+] recursive.empty n
(max (n + 3) (max bc ba)) [+] cp) stp =
(0 + 3, butlast lm @ 0 # 0\<^bsup>a_md - Suc rs_pos\<^esup> @
last lm # suf_lm)", simp)
apply(rule_tac abc_append_exc1, simp_all)
apply(insert empty_ex[of "n" "(max (n + 3)
(max bc ba))" "lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm"], simp)
apply(subgoal_tac "a_md = Suc (max (n + 3) (max bc ba))",
simp)
apply(subgoal_tac "length lm = Suc n \<and> rs_pos = Suc n", simp)
apply(insert h)
apply(simp add: para_pattern ci_pr_para_eq)
apply(rule ci_pr_md_def, auto)
done
qed
from h have k2:
"\<exists> stp. abc_steps_l (3, butlast lm @ 0 # 0\<^bsup>a_md - rs_pos - 1\<^esup> @
last lm # suf_lm) aprog stp
= (length aprog, lm @ rs # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)"
proof -
from h have k2_1: "\<exists> rs. rec_calc_rel f (butlast lm) rs"
apply(erule_tac calc_pr_zero_ex)
done
thus "?thesis"
proof(erule_tac exE)
fix rsa
assume k2_2: "rec_calc_rel f (butlast lm) rsa"
from h and k2_2 have k2_2_1:
"\<exists> stp. abc_steps_l (3, butlast lm @ 0 # 0\<^bsup>a_md - rs_pos - 1\<^esup>
@ last lm # suf_lm) aprog stp
= (3 + length ab, butlast lm @ rsa # 0\<^bsup>a_md - rs_pos - 1\<^esup> @
last lm # suf_lm)"
proof -
from h have j1: "
\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = 3 \<and>
bp = ab"
apply(auto)
done
from h have j2: "ac = rs_pos - 1"
apply(drule_tac ci_pr_f_paras, simp, auto)
done
from h and j2 have j3: "a_md \<ge> Suc bc \<and> rs_pos > 0 \<and> bc \<ge> rs_pos"
apply(rule_tac conjI)
apply(erule_tac ab = ab and ac = ac in ci_pr_md_ge_f, simp)
apply(rule_tac context_conjI)
apply(simp_all add: rec_ci.simps)
apply(drule_tac ci_ad_ge_paras, drule_tac ci_ad_ge_paras)
apply(arith)
done
from j1 and j2 show "?thesis"
apply(auto simp del: abc_append_commute)
apply(rule_tac abc_append_exc1, simp_all)
apply(insert nf_ind[of "butlast lm" "rsa"
"0\<^bsup>a_md - bc - Suc 0\<^esup> @ last lm # suf_lm"],
simp add: k2_2 j2, erule_tac exE)
apply(simp add: exponent_add_iff j3)
apply(rule_tac x = "stp" in exI, simp)
done
qed
from h have k2_2_2:
"\<exists> stp. abc_steps_l (3 + length ab, butlast lm @ rsa #
0\<^bsup>a_md - rs_pos - 1\<^esup> @ last lm # suf_lm) aprog stp
= (6 + length ab, butlast lm @ 0 # rsa #
0\<^bsup>a_md - rs_pos - 2\<^esup> @ last lm # suf_lm)"
proof -
from h have "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and>
length ap = 3 + length ab \<and> bp = recursive.empty n (Suc n)"
by auto
thus "?thesis"
proof(erule_tac exE, erule_tac exE, erule_tac exE,
erule_tac exE)
fix ap cp bp apa
assume "aprog = ap [+] bp [+] cp \<and> length ap = 3 +
length ab \<and> bp = recursive.empty n (Suc n)"
thus "?thesis"
apply(simp del: abc_append_commute)
apply(subgoal_tac
"\<exists>stp. abc_steps_l (3 + length ab,
butlast lm @ rsa # 0\<^bsup>a_md - Suc rs_pos\<^esup> @
last lm # suf_lm) (ap [+]
recursive.empty n (Suc n) [+] cp) stp =
((3 + length ab) + 3, butlast lm @ 0 # rsa #
0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ last lm # suf_lm)", simp)
apply(rule_tac abc_append_exc1, simp_all)
apply(insert empty_ex[of n "Suc n"
"butlast lm @ rsa # 0\<^bsup>a_md - Suc rs_pos\<^esup> @
last lm # suf_lm"], simp)
apply(subgoal_tac "length lm = Suc n \<and> rs_pos = Suc n \<and> a_md > Suc (Suc n)", simp)
apply(insert h, simp)
done
qed
qed
from h have k2_3: "lm \<noteq> []"
apply(rule_tac calc_pr_para_not_null, simp)
done
from h and k2_2 and k2_3 have k2_2_3:
"\<exists> stp. abc_steps_l (6 + length ab, butlast lm @
(last lm - last lm) # rsa #
0\<^bsup>a_md - (Suc (Suc rs_pos))\<^esup> @ last lm # suf_lm) aprog stp
= (6 + length ab, butlast lm @ last lm # rs #
0\<^bsup>a_md - Suc (Suc (rs_pos))\<^esup> @ 0 # suf_lm)"
apply(rule_tac x = "last lm" and g = g in pr_cycle_part, auto)
apply(rule_tac ng_ind, simp)
apply(rule_tac rec_calc_rel_def0, simp, simp)
done
from h have k2_2_4:
"\<exists> stp. abc_steps_l (6 + length ab,
butlast lm @ last lm # rs # 0\<^bsup>a_md - rs_pos - 2\<^esup> @
0 # suf_lm) aprog stp
= (13 + length ab + length a,
lm @ rs # 0\<^bsup>a_md - rs_pos - 1\<^esup> @ suf_lm)"
proof -
from h have
"\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and>
length ap = 6 + length ab \<and>
bp = ([Dec (a_md - Suc 0) (length a + 7)] [+]
(a [+] [Inc (rs_pos - Suc 0),
Dec rs_pos 3, Goto (Suc 0)])) @
[Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]"
by auto
thus "?thesis"
apply(auto)
apply(subgoal_tac
"\<exists>stp. abc_steps_l (6 + length ab, butlast lm @
last lm # rs # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ 0 # suf_lm)
(ap [+] ([Dec (a_md - Suc 0) (length a + 7)] [+]
(a [+] [Inc (rs_pos - Suc 0), Dec rs_pos 3,
Goto (Suc 0)])) @ [Dec (Suc (Suc n)) 0, Inc (Suc n),
Goto (length a + 4)] [+] cp) stp =
(6 + length ab + (length a + 7) ,
lm @ rs # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)", simp)
apply(subgoal_tac "13 + (length ab + length a) =
13 + length ab + length a", simp)
apply(arith)
apply(rule abc_append_exc1, simp_all)
apply(rule_tac x = "Suc 0" in exI,
simp add: abc_steps_l.simps abc_fetch.simps
nth_append abc_append_nth abc_step_l.simps)
apply(subgoal_tac "a_md > Suc (Suc rs_pos) \<and>
length lm = rs_pos \<and> rs_pos > 0", simp)
apply(insert h, simp)
apply(subgoal_tac "rs_pos = Suc n", simp, simp)
done
qed
from h have k2_2_5: "length aprog = 13 + length ab + length a"
apply(rule_tac ci_pr_length, simp_all)
done
from k2_2_1 and k2_2_2 and k2_2_3 and k2_2_4 and k2_2_5
show "?thesis"
apply(auto)
apply(rule_tac x = "stp + stpa + stpb + stpc" in exI,
simp add: abc_steps_add)
done
qed
qed
from k1 and k2 show
"\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp
= (length aprog, lm @ rs # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)"
apply(erule_tac exE)
apply(erule_tac exE)
apply(rule_tac x = "stp + stpa" in exI)
apply(simp add: abc_steps_add)
done
qed
thm rec_calc_rel.induct
lemma eq_switch: "x = y \<Longrightarrow> y = x"
by simp
lemma [simp]:
"\<lbrakk>rec_ci f = (a, aa, ba);
rec_ci (Mn n f) = (aprog, rs_pos, a_md)\<rbrakk> \<Longrightarrow> \<exists>bp. aprog = a @ bp"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "[Dec (Suc n) (length a + 5),
Dec (Suc n) (length a + 3), Goto (Suc (length a)),
Inc n, Goto 0]" in exI, auto)
done
lemma ci_mn_para_eq[simp]:
"rec_ci (Mn n f) = (aprog, rs_pos, a_md) \<Longrightarrow> rs_pos = n"
apply(case_tac "rec_ci f", simp add: rec_ci.simps)
done
(*
lemma [simp]: "\<lbrakk>rec_ci f = (a, aa, ba); rec_ci (Mn n f) = (aprog, rs_pos, a_md); rec_calc_rel (Mn n f) lm rs\<rbrakk> \<Longrightarrow> aa = Suc rs_pos"
apply(rule_tac calc_mn_reverse, simp)
apply(insert para_pattern [of f a aa ba "lm @ [rs]" 0], simp)
apply(subgoal_tac "rs_pos = length lm", simp)
apply(drule_tac ci_mn_para_eq, simp)
done
*)
lemma [simp]: "rec_ci f = (a, aa, ba) \<Longrightarrow> aa < ba"
apply(simp add: ci_ad_ge_paras)
done
lemma [simp]: "\<lbrakk>rec_ci f = (a, aa, ba);
rec_ci (Mn n f) = (aprog, rs_pos, a_md)\<rbrakk>
\<Longrightarrow> ba \<le> a_md"
apply(simp add: rec_ci.simps)
by arith
lemma mn_calc_f:
assumes ind:
"\<And>aprog a_md rs_pos rs suf_lm lm.
\<lbrakk>rec_ci f = (aprog, rs_pos, a_md); rec_calc_rel f lm rs\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp
= (length aprog, lm @ [rs] @ 0\<^bsup>a_md - rs_pos - 1\<^esup> @ suf_lm)"
and h: "rec_ci f = (a, aa, ba)"
"rec_ci (Mn n f) = (aprog, rs_pos, a_md)"
"rec_calc_rel f (lm @ [x]) rsx"
"aa = Suc n"
shows "\<exists>stp. abc_steps_l (0, lm @ x # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)
aprog stp = (length a,
lm @ x # rsx # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ suf_lm)"
proof -
from h have k1: "\<exists> ap bp. aprog = ap @ bp \<and> ap = a"
by simp
from h have k2: "rs_pos = n"
apply(erule_tac ci_mn_para_eq)
done
from h and k1 and k2 show "?thesis"
proof(erule_tac exE, erule_tac exE, simp,
rule_tac abc_add_exc1, auto)
fix bp
show
"\<exists>astp. abc_steps_l (0, lm @ x # 0\<^bsup>a_md - Suc n\<^esup> @ suf_lm) a astp
= (length a, lm @ x # rsx # 0\<^bsup>a_md - Suc (Suc n)\<^esup> @ suf_lm)"
apply(insert ind[of a "Suc n" ba "lm @ [x]" rsx
"0\<^bsup>a_md - ba\<^esup> @ suf_lm"], simp add: exponent_add_iff h k2)
apply(subgoal_tac "ba > aa \<and> a_md \<ge> ba \<and> aa = Suc n",
insert h, auto)
done
qed
qed
thm rec_ci.simps
fun mn_ind_inv ::
"nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat list \<Rightarrow> bool"
where
"mn_ind_inv (as, lm') ss x rsx suf_lm lm =
(if as = ss then lm' = lm @ x # rsx # suf_lm
else if as = ss + 1 then
\<exists>y. (lm' = lm @ x # y # suf_lm) \<and> y \<le> rsx
else if as = ss + 2 then
\<exists>y. (lm' = lm @ x # y # suf_lm) \<and> y \<le> rsx
else if as = ss + 3 then lm' = lm @ x # 0 # suf_lm
else if as = ss + 4 then lm' = lm @ Suc x # 0 # suf_lm
else if as = 0 then lm' = lm @ Suc x # 0 # suf_lm
else False
)"
fun mn_stage1 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
where
"mn_stage1 (as, lm) ss n =
(if as = 0 then 0
else if as = ss + 4 then 1
else if as = ss + 3 then 2
else if as = ss + 2 \<or> as = ss + 1 then 3
else if as = ss then 4
else 0
)"
fun mn_stage2 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
where
"mn_stage2 (as, lm) ss n =
(if as = ss + 1 \<or> as = ss + 2 then (lm ! (Suc n))
else 0)"
fun mn_stage3 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
where
"mn_stage3 (as, lm) ss n = (if as = ss + 2 then 1 else 0)"
fun mn_measure :: "((nat \<times> nat list) \<times> nat \<times> nat) \<Rightarrow>
(nat \<times> nat \<times> nat)"
where
"mn_measure ((as, lm), ss, n) =
(mn_stage1 (as, lm) ss n, mn_stage2 (as, lm) ss n,
mn_stage3 (as, lm) ss n)"
definition mn_LE :: "(((nat \<times> nat list) \<times> nat \<times> nat) \<times>
((nat \<times> nat list) \<times> nat \<times> nat)) set"
where "mn_LE \<equiv> (inv_image lex_triple mn_measure)"
thm halt_lemma2
lemma wf_mn_le[intro]: "wf mn_LE"
by(auto intro:wf_inv_image wf_lex_triple simp: mn_LE_def)
declare mn_ind_inv.simps[simp del]
lemma mn_inv_init:
"mn_ind_inv (abc_steps_l (length a, lm @ x # rsx # suf_lm) aprog 0)
(length a) x rsx suf_lm lm"
apply(simp add: mn_ind_inv.simps abc_steps_zero)
done
lemma mn_halt_init:
"rec_ci f = (a, aa, ba) \<Longrightarrow>
\<not> (\<lambda>(as, lm') (ss, n). as = 0)
(abc_steps_l (length a, lm @ x # rsx # suf_lm) aprog 0)
(length a, n)"
apply(simp add: abc_steps_zero)
apply(erule_tac rec_ci_not_null)
done
thm rec_ci.simps
lemma [simp]:
"\<lbrakk>rec_ci f = (a, aa, ba);
rec_ci (Mn n f) = (aprog, rs_pos, a_md)\<rbrakk>
\<Longrightarrow> abc_fetch (length a) aprog =
Some (Dec (Suc n) (length a + 5))"
apply(simp add: rec_ci.simps abc_fetch.simps,
erule_tac conjE, erule_tac conjE, simp)
apply(drule_tac eq_switch, drule_tac eq_switch, simp)
done
lemma [simp]: "\<lbrakk>rec_ci f = (a, aa, ba); rec_ci (Mn n f) = (aprog, rs_pos, a_md)\<rbrakk>
\<Longrightarrow> abc_fetch (Suc (length a)) aprog = Some (Dec (Suc n) (length a + 3))"
apply(simp add: rec_ci.simps abc_fetch.simps, erule_tac conjE, erule_tac conjE, simp)
apply(drule_tac eq_switch, drule_tac eq_switch, simp add: nth_append)
done
lemma [simp]:
"\<lbrakk>rec_ci f = (a, aa, ba);
rec_ci (Mn n f) = (aprog, rs_pos, a_md)\<rbrakk>
\<Longrightarrow> abc_fetch (Suc (Suc (length a))) aprog =
Some (Goto (length a + 1))"
apply(simp add: rec_ci.simps abc_fetch.simps,
erule_tac conjE, erule_tac conjE, simp)
apply(drule_tac eq_switch, drule_tac eq_switch, simp add: nth_append)
done
lemma [simp]:
"\<lbrakk>rec_ci f = (a, aa, ba);
rec_ci (Mn n f) = (aprog, rs_pos, a_md)\<rbrakk>
\<Longrightarrow> abc_fetch (length a + 3) aprog = Some (Inc n)"
apply(simp add: rec_ci.simps abc_fetch.simps,
erule_tac conjE, erule_tac conjE, simp)
apply(drule_tac eq_switch, drule_tac eq_switch, simp add: nth_append)
done
lemma [simp]: "\<lbrakk>rec_ci f = (a, aa, ba); rec_ci (Mn n f) = (aprog, rs_pos, a_md)\<rbrakk>
\<Longrightarrow> abc_fetch (length a + 4) aprog = Some (Goto 0)"
apply(simp add: rec_ci.simps abc_fetch.simps, erule_tac conjE, erule_tac conjE, simp)
apply(drule_tac eq_switch, drule_tac eq_switch, simp add: nth_append)
done
lemma [simp]:
"0 < rsx
\<Longrightarrow> \<exists>y. (lm @ x # rsx # suf_lm)[Suc (length lm) := rsx - Suc 0]
= lm @ x # y # suf_lm \<and> y \<le> rsx"
apply(case_tac rsx, simp, simp)
apply(rule_tac x = nat in exI, simp add: list_update_append)
done
lemma [simp]:
"\<lbrakk>y \<le> rsx; 0 < y\<rbrakk>
\<Longrightarrow> \<exists>ya. (lm @ x # y # suf_lm)[Suc (length lm) := y - Suc 0]
= lm @ x # ya # suf_lm \<and> ya \<le> rsx"
apply(case_tac y, simp, simp)
apply(rule_tac x = nat in exI, simp add: list_update_append)
done
lemma mn_halt_lemma:
"\<lbrakk>rec_ci f = (a, aa, ba);
rec_ci (Mn n f) = (aprog, rs_pos, a_md);
0 < rsx; length lm = n\<rbrakk>
\<Longrightarrow>
\<forall>na. \<not> (\<lambda>(as, lm') (ss, n). as = 0)
(abc_steps_l (length a, lm @ x # rsx # suf_lm) aprog na)
(length a, n)
\<and> mn_ind_inv (abc_steps_l (length a, lm @ x # rsx # suf_lm)
aprog na) (length a) x rsx suf_lm lm
\<longrightarrow> mn_ind_inv (abc_steps_l (length a, lm @ x # rsx # suf_lm) aprog
(Suc na)) (length a) x rsx suf_lm lm
\<and> ((abc_steps_l (length a, lm @ x # rsx # suf_lm) aprog (Suc na),
length a, n),
abc_steps_l (length a, lm @ x # rsx # suf_lm) aprog na,
length a, n) \<in> mn_LE"
apply(rule allI, rule impI, simp add: abc_steps_ind)
apply(case_tac "(abc_steps_l (length a, lm @ x # rsx # suf_lm)
aprog na)", simp)
apply(auto split:if_splits simp add:abc_steps_l.simps
mn_ind_inv.simps abc_steps_zero)
apply(auto simp add: mn_LE_def lex_triple_def lex_pair_def
abc_step_l.simps abc_steps_l.simps mn_ind_inv.simps
abc_lm_v.simps abc_lm_s.simps nth_append
split: if_splits)
apply(drule_tac rec_ci_not_null, simp)
done
lemma mn_halt:
"\<lbrakk>rec_ci f = (a, aa, ba);
rec_ci (Mn n f) = (aprog, rs_pos, a_md);
0 < rsx; length lm = n\<rbrakk>
\<Longrightarrow> \<exists> stp. (\<lambda> (as, lm'). (as = 0 \<and>
mn_ind_inv (as, lm') (length a) x rsx suf_lm lm))
(abc_steps_l (length a, lm @ x # rsx # suf_lm) aprog stp)"
apply(insert wf_mn_le)
apply(insert halt_lemma2[of mn_LE
"\<lambda> ((as, lm'), ss, n). as = 0"
"\<lambda> stp. (abc_steps_l (length a, lm @ x # rsx # suf_lm) aprog stp,
length a, n)"
"\<lambda> ((as, lm'), ss, n). mn_ind_inv (as, lm') ss x rsx suf_lm lm"],
simp)
apply(simp add: mn_halt_init mn_inv_init)
apply(drule_tac x = x and suf_lm = suf_lm in mn_halt_lemma, auto)
apply(rule_tac x = n in exI,
case_tac "(abc_steps_l (length a, lm @ x # rsx # suf_lm)
aprog n)", simp)
done
lemma [simp]: "Suc rs_pos < a_md \<Longrightarrow>
Suc (a_md - Suc (Suc rs_pos)) = a_md - Suc rs_pos"
by arith
term rec_ci
(*
lemma [simp]: "\<lbrakk>rec_ci (Mn n f) = (aprog, rs_pos, a_md); rec_calc_rel (Mn n f) lm rs\<rbrakk> \<Longrightarrow> Suc rs_pos < a_md"
apply(case_tac "rec_ci f")
apply(subgoal_tac "c > b \<and> b = Suc rs_pos \<and> a_md \<ge> c")
apply(arith, auto)
done
*)
lemma mn_ind_step:
assumes ind:
"\<And>aprog a_md rs_pos rs suf_lm lm.
\<lbrakk>rec_ci f = (aprog, rs_pos, a_md);
rec_calc_rel f lm rs\<rbrakk> \<Longrightarrow>
\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp
= (length aprog, lm @ [rs] @ 0\<^bsup>a_md - rs_pos - 1\<^esup> @ suf_lm)"
and h: "rec_ci f = (a, aa, ba)"
"rec_ci (Mn n f) = (aprog, rs_pos, a_md)"
"rec_calc_rel f (lm @ [x]) rsx"
"rsx > 0"
"Suc rs_pos < a_md"
"aa = Suc rs_pos"
shows "\<exists>stp. abc_steps_l (0, lm @ x # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)
aprog stp = (0, lm @ Suc x # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)"
thm abc_add_exc1
proof -
have k1:
"\<exists> stp. abc_steps_l (0, lm @ x # 0\<^bsup>a_md - Suc (rs_pos)\<^esup> @ suf_lm)
aprog stp =
(length a, lm @ x # rsx # 0\<^bsup>a_md - Suc (Suc rs_pos) \<^esup>@ suf_lm)"
apply(insert h)
apply(auto intro: mn_calc_f ind)
done
from h have k2: "length lm = n"
apply(subgoal_tac "rs_pos = n")
apply(drule_tac para_pattern, simp, simp, simp)
done
from h have k3: "a_md > (Suc rs_pos)"
apply(simp)
done
from k2 and h and k3 have k4:
"\<exists> stp. abc_steps_l (length a,
lm @ x # rsx # 0\<^bsup>a_md - Suc (Suc rs_pos) \<^esup>@ suf_lm) aprog stp =
(0, lm @ Suc x # 0\<^bsup>a_md - rs_pos - 1\<^esup> @ suf_lm)"
apply(frule_tac x = x and
suf_lm = "0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ suf_lm" in mn_halt, auto)
apply(rule_tac x = "stp" in exI,
simp add: mn_ind_inv.simps rec_ci_not_null exponent_def)
apply(simp only: replicate.simps[THEN sym], simp)
done
from k1 and k4 show "?thesis"
apply(auto)
apply(rule_tac x = "stp + stpa" in exI, simp add: abc_steps_add)
done
qed
lemma [simp]:
"\<lbrakk>rec_ci f = (a, aa, ba); rec_ci (Mn n f) = (aprog, rs_pos, a_md);
rec_calc_rel (Mn n f) lm rs\<rbrakk> \<Longrightarrow> aa = Suc rs_pos"
apply(rule_tac calc_mn_reverse, simp)
apply(insert para_pattern [of f a aa ba "lm @ [rs]" 0], simp)
apply(subgoal_tac "rs_pos = length lm", simp)
apply(drule_tac ci_mn_para_eq, simp)
done
lemma [simp]: "\<lbrakk>rec_ci (Mn n f) = (aprog, rs_pos, a_md);
rec_calc_rel (Mn n f) lm rs\<rbrakk> \<Longrightarrow> Suc rs_pos < a_md"
apply(case_tac "rec_ci f")
apply(subgoal_tac "c > b \<and> b = Suc rs_pos \<and> a_md \<ge> c")
apply(arith, auto)
done
lemma mn_ind_steps:
assumes ind:
"\<And>aprog a_md rs_pos rs suf_lm lm.
\<lbrakk>rec_ci f = (aprog, rs_pos, a_md); rec_calc_rel f lm rs\<rbrakk> \<Longrightarrow>
\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp =
(length aprog, lm @ [rs] @ 0\<^bsup>a_md - rs_pos - 1\<^esup> @ suf_lm)"
and h: "rec_ci f = (a, aa, ba)"
"rec_ci (Mn n f) = (aprog, rs_pos, a_md)"
"rec_calc_rel (Mn n f) lm rs"
"rec_calc_rel f (lm @ [rs]) 0"
"\<forall>x<rs. (\<exists> v. rec_calc_rel f (lm @ [x]) v \<and> 0 < v)"
"n = length lm"
"x \<le> rs"
shows "\<exists>stp. abc_steps_l (0, lm @ 0 # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)
aprog stp = (0, lm @ x # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)"
apply(insert h, induct x,
rule_tac x = 0 in exI, simp add: abc_steps_zero, simp)
proof -
fix x
assume k1:
"\<exists>stp. abc_steps_l (0, lm @ 0 # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)
aprog stp = (0, lm @ x # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)"
and k2: "rec_ci (Mn (length lm) f) = (aprog, rs_pos, a_md)"
"rec_calc_rel (Mn (length lm) f) lm rs"
"rec_calc_rel f (lm @ [rs]) 0"
"\<forall>x<rs.(\<exists> v. rec_calc_rel f (lm @ [x]) v \<and> v > 0)"
"n = length lm"
"Suc x \<le> rs"
"rec_ci f = (a, aa, ba)"
hence k2:
"\<exists>stp. abc_steps_l (0, lm @ x # 0\<^bsup>a_md - rs_pos - 1\<^esup> @ suf_lm) aprog
stp = (0, lm @ Suc x # 0\<^bsup>a_md - rs_pos - 1\<^esup> @ suf_lm)"
apply(erule_tac x = x in allE)
apply(auto)
apply(rule_tac x = x in mn_ind_step)
apply(rule_tac ind, auto)
done
from k1 and k2 show
"\<exists>stp. abc_steps_l (0, lm @ 0 # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)
aprog stp = (0, lm @ Suc x # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)"
apply(auto)
apply(rule_tac x = "stp + stpa" in exI, simp only: abc_steps_add)
done
qed
lemma [simp]:
"\<lbrakk>rec_ci f = (a, aa, ba);
rec_ci (Mn n f) = (aprog, rs_pos, a_md);
rec_calc_rel (Mn n f) lm rs;
length lm = n\<rbrakk>
\<Longrightarrow> abc_lm_v (lm @ rs # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm) (Suc n) = 0"
apply(auto simp: abc_lm_v.simps nth_append)
done
lemma [simp]:
"\<lbrakk>rec_ci f = (a, aa, ba);
rec_ci (Mn n f) = (aprog, rs_pos, a_md);
rec_calc_rel (Mn n f) lm rs;
length lm = n\<rbrakk>
\<Longrightarrow> abc_lm_s (lm @ rs # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm) (Suc n) 0 =
lm @ rs # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm"
apply(auto simp: abc_lm_s.simps list_update_append)
done
lemma mn_length:
"\<lbrakk>rec_ci f = (a, aa, ba);
rec_ci (Mn n f) = (aprog, rs_pos, a_md)\<rbrakk>
\<Longrightarrow> length aprog = length a + 5"
apply(simp add: rec_ci.simps, erule_tac conjE)
apply(drule_tac eq_switch, drule_tac eq_switch, simp)
done
lemma mn_final_step:
assumes ind:
"\<And>aprog a_md rs_pos rs suf_lm lm.
\<lbrakk>rec_ci f = (aprog, rs_pos, a_md);
rec_calc_rel f lm rs\<rbrakk> \<Longrightarrow>
\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp =
(length aprog, lm @ [rs] @ 0\<^bsup>a_md - rs_pos - 1\<^esup> @ suf_lm)"
and h: "rec_ci f = (a, aa, ba)"
"rec_ci (Mn n f) = (aprog, rs_pos, a_md)"
"rec_calc_rel (Mn n f) lm rs"
"rec_calc_rel f (lm @ [rs]) 0"
shows "\<exists>stp. abc_steps_l (0, lm @ rs # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)
aprog stp = (length aprog, lm @ rs # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)"
proof -
from h and ind have k1:
"\<exists>stp. abc_steps_l (0, lm @ rs # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)
aprog stp = (length a, lm @ rs # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)"
thm mn_calc_f
apply(insert mn_calc_f[of f a aa ba n aprog
rs_pos a_md lm rs 0 suf_lm], simp)
apply(subgoal_tac "aa = Suc n", simp add: exponent_cons_iff)
apply(subgoal_tac "rs_pos = n", simp, simp)
done
from h have k2: "length lm = n"
apply(subgoal_tac "rs_pos = n")
apply(drule_tac f = "Mn n f" in para_pattern, simp, simp, simp)
done
from h and k2 have k3:
"\<exists>stp. abc_steps_l (length a, lm @ rs # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)
aprog stp = (length a + 5, lm @ rs # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)"
apply(rule_tac x = "Suc 0" in exI,
simp add: abc_step_l.simps abc_steps_l.simps)
done
from h have k4: "length aprog = length a + 5"
apply(simp add: mn_length)
done
from k1 and k3 and k4 show "?thesis"
apply(auto)
apply(rule_tac x = "stp + stpa" in exI, simp add: abc_steps_add)
done
qed
lemma mn_case:
assumes ind:
"\<And>aprog a_md rs_pos rs suf_lm lm.
\<lbrakk>rec_ci f = (aprog, rs_pos, a_md); rec_calc_rel f lm rs\<rbrakk> \<Longrightarrow>
\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp =
(length aprog, lm @ [rs] @ 0\<^bsup>a_md - rs_pos - 1\<^esup> @ suf_lm)"
and h: "rec_ci (Mn n f) = (aprog, rs_pos, a_md)"
"rec_calc_rel (Mn n f) lm rs"
shows "\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp
= (length aprog, lm @ [rs] @ 0\<^bsup>a_md - rs_pos - 1\<^esup> @ suf_lm)"
apply(case_tac "rec_ci f", simp)
apply(insert h, rule_tac calc_mn_reverse, simp)
proof -
fix a b c v
assume h: "rec_ci f = (a, b, c)"
"rec_ci (Mn n f) = (aprog, rs_pos, a_md)"
"rec_calc_rel (Mn n f) lm rs"
"rec_calc_rel f (lm @ [rs]) 0"
"\<forall>x<rs. \<exists>v. rec_calc_rel f (lm @ [x]) v \<and> 0 < v"
"n = length lm"
hence k1:
"\<exists>stp. abc_steps_l (0, lm @ 0 # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm) aprog
stp = (0, lm @ rs # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)"
thm mn_ind_steps
apply(auto intro: mn_ind_steps ind)
done
from h have k2:
"\<exists>stp. abc_steps_l (0, lm @ rs # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm) aprog
stp = (length aprog, lm @ rs # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)"
apply(auto intro: mn_final_step ind)
done
from k1 and k2 show
"\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp =
(length aprog, lm @ rs # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)"
apply(auto, insert h)
apply(subgoal_tac "Suc rs_pos < a_md")
apply(rule_tac x = "stp + stpa" in exI,
simp only: abc_steps_add exponent_cons_iff, simp, simp)
done
qed
lemma z_rs: "rec_calc_rel z lm rs \<Longrightarrow> rs = 0"
apply(rule_tac calc_z_reverse, auto)
done
lemma z_case:
"\<lbrakk>rec_ci z = (aprog, rs_pos, a_md); rec_calc_rel z lm rs\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp =
(length aprog, lm @ [rs] @ 0\<^bsup>a_md - rs_pos - 1\<^esup> @ suf_lm)"
apply(simp add: rec_ci.simps rec_ci_z_def, auto)
apply(rule_tac x = "Suc 0" in exI, simp add: abc_steps_l.simps
abc_fetch.simps abc_step_l.simps z_rs)
done
thm addition.simps
thm addition.simps
thm rec_ci_s_def
fun addition_inv :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow>
nat list \<Rightarrow> bool"
where
"addition_inv (as, lm') m n p lm =
(let sn = lm ! n in
let sm = lm ! m in
lm ! p = 0 \<and>
(if as = 0 then \<exists> x. x \<le> lm ! m \<and> lm' = lm[m := x,
n := (sn + sm - x), p := (sm - x)]
else if as = 1 then \<exists> x. x < lm ! m \<and> lm' = lm[m := x,
n := (sn + sm - x - 1), p := (sm - x - 1)]
else if as = 2 then \<exists> x. x < lm ! m \<and> lm' = lm[m := x,
n := (sn + sm - x), p := (sm - x - 1)]
else if as = 3 then \<exists> x. x < lm ! m \<and> lm' = lm[m := x,
n := (sn + sm - x), p := (sm - x)]
else if as = 4 then \<exists> x. x \<le> lm ! m \<and> lm' = lm[m := x,
n := (sn + sm), p := (sm - x)]
else if as = 5 then \<exists> x. x < lm ! m \<and> lm' = lm[m := x,
n := (sn + sm), p := (sm - x - 1)]
else if as = 6 then \<exists> x. x < lm ! m \<and> lm' =
lm[m := Suc x, n := (sn + sm), p := (sm - x - 1)]
else if as = 7 then lm' = lm[m := sm, n := (sn + sm)]
else False))"
fun addition_stage1 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
where
"addition_stage1 (as, lm) m p =
(if as = 0 \<or> as = 1 \<or> as = 2 \<or> as = 3 then 2
else if as = 4 \<or> as = 5 \<or> as = 6 then 1
else 0)"
fun addition_stage2 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
where
"addition_stage2 (as, lm) m p =
(if 0 \<le> as \<and> as \<le> 3 then lm ! m
else if 4 \<le> as \<and> as \<le> 6 then lm ! p
else 0)"
fun addition_stage3 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
where
"addition_stage3 (as, lm) m p =
(if as = 1 then 4
else if as = 2 then 3
else if as = 3 then 2
else if as = 0 then 1
else if as = 5 then 2
else if as = 6 then 1
else if as = 4 then 0
else 0)"
fun addition_measure :: "((nat \<times> nat list) \<times> nat \<times> nat) \<Rightarrow>
(nat \<times> nat \<times> nat)"
where
"addition_measure ((as, lm), m, p) =
(addition_stage1 (as, lm) m p,
addition_stage2 (as, lm) m p,
addition_stage3 (as, lm) m p)"
definition addition_LE :: "(((nat \<times> nat list) \<times> nat \<times> nat) \<times>
((nat \<times> nat list) \<times> nat \<times> nat)) set"
where "addition_LE \<equiv> (inv_image lex_triple addition_measure)"
lemma [simp]: "wf addition_LE"
by(simp add: wf_inv_image wf_lex_triple addition_LE_def)
declare addition_inv.simps[simp del]
lemma addition_inv_init:
"\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk> \<Longrightarrow>
addition_inv (0, lm) m n p lm"
apply(simp add: addition_inv.simps)
apply(rule_tac x = "lm ! m" in exI, simp)
done
thm addition.simps
lemma [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)"
by(simp add: abc_fetch.simps addition.simps)
lemma [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)"
by(simp add: abc_fetch.simps addition.simps)
lemma [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)"
by(simp add: abc_fetch.simps addition.simps)
lemma [simp]: "abc_fetch 6 (addition m n p) = Some (Goto 4)"
by(simp add: abc_fetch.simps addition.simps)
lemma [simp]:
"\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x \<le> lm ! m; 0 < x\<rbrakk>
\<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m - x,
p := lm ! m - x, m := x - Suc 0] =
lm[m := xa, n := lm ! n + lm ! m - Suc xa,
p := lm ! m - Suc xa]"
apply(case_tac x, simp, simp)
apply(rule_tac x = nat in exI, simp add: list_update_swap
list_update_overwrite)
done
lemma [simp]:
"\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\<rbrakk>
\<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m - Suc x,
p := lm ! m - Suc x, n := lm ! n + lm ! m - x]
= lm[m := xa, n := lm ! n + lm ! m - xa,
p := lm ! m - Suc xa]"
apply(rule_tac x = x in exI,
simp add: list_update_swap list_update_overwrite)
done
lemma [simp]:
"\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\<rbrakk>
\<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m - x,
p := lm ! m - Suc x, p := lm ! m - x]
= lm[m := xa, n := lm ! n + lm ! m - xa,
p := lm ! m - xa]"
apply(rule_tac x = x in exI, simp add: list_update_overwrite)
done
lemma [simp]:
"\<lbrakk>m \<noteq> n; p < length lm; lm ! p = (0::nat); m < p; n < p; x < lm ! m\<rbrakk>
\<Longrightarrow> \<exists>xa\<le>lm ! m. lm[m := x, n := lm ! n + lm ! m - x,
p := lm ! m - x] =
lm[m := xa, n := lm ! n + lm ! m - xa,
p := lm ! m - xa]"
apply(rule_tac x = x in exI, simp)
done
lemma [simp]:
"\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p;
x \<le> lm ! m; lm ! m \<noteq> x\<rbrakk>
\<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m,
p := lm ! m - x, p := lm ! m - Suc x]
= lm[m := xa, n := lm ! n + lm ! m,
p := lm ! m - Suc xa]"
apply(rule_tac x = x in exI, simp add: list_update_overwrite)
done
lemma [simp]:
"\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\<rbrakk>
\<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m,
p := lm ! m - Suc x, m := Suc x]
= lm[m := Suc xa, n := lm ! n + lm ! m,
p := lm ! m - Suc xa]"
apply(rule_tac x = x in exI,
simp add: list_update_swap list_update_overwrite)
done
lemma [simp]:
"\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\<rbrakk>
\<Longrightarrow> \<exists>xa\<le>lm ! m. lm[m := Suc x, n := lm ! n + lm ! m,
p := lm ! m - Suc x]
= lm[m := xa, n := lm ! n + lm ! m, p := lm ! m - xa]"
apply(rule_tac x = "Suc x" in exI, simp)
done
lemma addition_halt_lemma:
"\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk> \<Longrightarrow>
\<forall>na. \<not> (\<lambda>(as, lm') (m, p). as = 7)
(abc_steps_l (0, lm) (addition m n p) na) (m, p) \<and>
addition_inv (abc_steps_l (0, lm) (addition m n p) na) m n p lm
\<longrightarrow> addition_inv (abc_steps_l (0, lm) (addition m n p)
(Suc na)) m n p lm
\<and> ((abc_steps_l (0, lm) (addition m n p) (Suc na), m, p),
abc_steps_l (0, lm) (addition m n p) na, m, p) \<in> addition_LE"
apply(rule allI, rule impI, simp add: abc_steps_ind)
apply(case_tac "(abc_steps_l (0, lm) (addition m n p) na)", simp)
apply(auto split:if_splits simp add: addition_inv.simps
abc_steps_zero)
apply(simp_all add: abc_steps_l.simps abc_steps_zero)
apply(auto simp add: addition_LE_def lex_triple_def lex_pair_def
abc_step_l.simps addition_inv.simps
abc_lm_v.simps abc_lm_s.simps nth_append
split: if_splits)
apply(rule_tac x = x in exI, simp)
done
lemma addition_ex:
"\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk> \<Longrightarrow>
\<exists> stp. (\<lambda> (as, lm'). as = 7 \<and> addition_inv (as, lm') m n p lm)
(abc_steps_l (0, lm) (addition m n p) stp)"
apply(insert halt_lemma2[of addition_LE
"\<lambda> ((as, lm'), m, p). as = 7"
"\<lambda> stp. (abc_steps_l (0, lm) (addition m n p) stp, m, p)"
"\<lambda> ((as, lm'), m, p). addition_inv (as, lm') m n p lm"],
simp add: abc_steps_zero addition_inv_init)
apply(drule_tac addition_halt_lemma, simp, simp, simp,
simp, erule_tac exE)
apply(rule_tac x = na in exI,
case_tac "(abc_steps_l (0, lm) (addition m n p) na)", auto)
done
lemma [simp]: "length (addition m n p) = 7"
by (simp add: addition.simps)
lemma [elim]: "addition 0 (Suc 0) 2 = [] \<Longrightarrow> RR"
by(simp add: addition.simps)
lemma [simp]: "(0\<^bsup>2\<^esup>)[0 := n] = [n, 0::nat]"
apply(subgoal_tac "2 = Suc 1",
simp only: replicate.simps exponent_def)
apply(auto)
done
lemma [simp]:
"\<exists>stp. abc_steps_l (0, n # 0\<^bsup>2\<^esup> @ suf_lm)
(addition 0 (Suc 0) 2 [+] [Inc (Suc 0)]) stp =
(8, n # Suc n # 0 # suf_lm)"
apply(rule_tac bm = "n # n # 0 # suf_lm" in abc_append_exc2, auto)
apply(insert addition_ex[of 0 "Suc 0" 2 "n # 0\<^bsup>2\<^esup> @ suf_lm"],
simp add: nth_append numeral_2_eq_2, erule_tac exE)
apply(rule_tac x = stp in exI,
case_tac "(abc_steps_l (0, n # 0\<^bsup>2\<^esup> @ suf_lm)
(addition 0 (Suc 0) 2) stp)",
simp add: addition_inv.simps nth_append list_update_append numeral_2_eq_2)
apply(simp add: nth_append numeral_2_eq_2, erule_tac exE)
apply(rule_tac x = "Suc 0" in exI,
simp add: abc_steps_l.simps abc_fetch.simps
abc_steps_zero abc_step_l.simps abc_lm_s.simps abc_lm_v.simps)
done
lemma s_case:
"\<lbrakk>rec_ci s = (aprog, rs_pos, a_md); rec_calc_rel s lm rs\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp =
(length aprog, lm @ [rs] @ 0\<^bsup>a_md - rs_pos - 1\<^esup> @ suf_lm)"
apply(simp add: rec_ci.simps rec_ci_s_def, auto)
apply(rule_tac calc_s_reverse, auto)
done
lemma [simp]:
"\<lbrakk>n < length lm; lm ! n = rs\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0 # 0 #suf_lm)
(addition n (length lm) (Suc (length lm))) stp
= (7, lm @ rs # 0 # suf_lm)"
apply(insert addition_ex[of n "length lm"
"Suc (length lm)" "lm @ 0 # 0 # suf_lm"])
apply(simp add: nth_append, erule_tac exE)
apply(rule_tac x = stp in exI)
apply(case_tac "abc_steps_l (0, lm @ 0 # 0 # suf_lm) (addition n (length lm)
(Suc (length lm))) stp", simp)
apply(simp add: addition_inv.simps)
apply(insert nth_append[of lm "0 # 0 # suf_lm" "n"], simp)
done
lemma [simp]: "0\<^bsup>2\<^esup> = [0, 0::nat]"
apply(auto simp: exponent_def numeral_2_eq_2)
done
lemma id_case:
"\<lbrakk>rec_ci (id m n) = (aprog, rs_pos, a_md);
rec_calc_rel (id m n) lm rs\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp =
(length aprog, lm @ [rs] @ 0\<^bsup>a_md - rs_pos - 1\<^esup> @ suf_lm)"
apply(simp add: rec_ci.simps rec_ci_id.simps, auto)
apply(rule_tac calc_id_reverse, simp, simp)
done
lemma list_tl_induct:
"\<lbrakk>P []; \<And>a list. P list \<Longrightarrow> P (list @ [a::'a])\<rbrakk> \<Longrightarrow>
P ((list::'a list))"
apply(case_tac "length list", simp)
proof -
fix nat
assume ind: "\<And>a list. P list \<Longrightarrow> P (list @ [a])"
and h: "length list = Suc nat" "P []"
from h show "P list"
proof(induct nat arbitrary: list, case_tac lista, simp, simp)
fix lista a listaa
from h show "P [a]"
by(insert ind[of "[]"], simp add: h)
next
fix nat list
assume nind: "\<And>list. \<lbrakk>length list = Suc nat; P []\<rbrakk> \<Longrightarrow> P list"
and g: "length (list:: 'a list) = Suc (Suc nat)"
from g show "P (list::'a list)"
apply(insert nind[of "butlast list"], simp add: h)
apply(insert ind[of "butlast list" "last list"], simp)
apply(subgoal_tac "butlast list @ [last list] = list", simp)
apply(case_tac "list::'a list", simp, simp)
done
qed
qed
thm list.induct
lemma nth_eq_butlast_nth: "\<lbrakk>length ys > Suc k\<rbrakk> \<Longrightarrow>
ys ! k = butlast ys ! k"
apply(subgoal_tac "\<exists> xs y. ys = xs @ [y]", auto simp: nth_append)
apply(rule_tac x = "butlast ys" in exI, rule_tac x = "last ys" in exI)
apply(case_tac "ys = []", simp, simp)
done
lemma [simp]:
"\<lbrakk>\<forall>k<Suc (length list). rec_calc_rel ((list @ [a]) ! k) lm (ys ! k);
length ys = Suc (length list)\<rbrakk>
\<Longrightarrow> \<forall>k<length list. rec_calc_rel (list ! k) lm (butlast ys ! k)"
apply(rule allI, rule impI)
apply(erule_tac x = k in allE, simp add: nth_append)
apply(subgoal_tac "ys ! k = butlast ys ! k", simp)
apply(rule_tac nth_eq_butlast_nth, arith)
done
thm cn_merge_gs.simps
lemma cn_merge_gs_tl_app:
"cn_merge_gs (gs @ [g]) pstr =
cn_merge_gs gs pstr [+] cn_merge_gs [g] (pstr + length gs)"
apply(induct gs arbitrary: pstr, simp add: cn_merge_gs.simps, simp)
apply(case_tac a, simp add: abc_append_commute)
done
lemma cn_merge_gs_length:
"length (cn_merge_gs (map rec_ci list) pstr) =
(\<Sum>(ap, pos, n)\<leftarrow>map rec_ci list. length ap) + 3 * length list "
apply(induct list arbitrary: pstr, simp, simp)
apply(case_tac "rec_ci a", simp)
done
lemma [simp]: "Suc n \<le> pstr \<Longrightarrow> pstr + x - n > 0"
by arith
lemma [simp]:
"\<lbrakk>Suc (pstr + length list) \<le> a_md;
length ys = Suc (length list);
length lm = n;
Suc n \<le> pstr\<rbrakk>
\<Longrightarrow> (ys ! length list # 0\<^bsup>pstr - Suc n\<^esup> @ butlast ys @
0\<^bsup>a_md - (pstr + length list)\<^esup> @ suf_lm) !
(pstr + length list - n) = (0 :: nat)"
apply(insert nth_append[of "ys ! length list # 0\<^bsup>pstr - Suc n\<^esup> @
butlast ys" "0\<^bsup>a_md - (pstr + length list)\<^esup> @ suf_lm"
"(pstr + length list - n)"], simp add: nth_append)
done
lemma [simp]:
"\<lbrakk>Suc (pstr + length list) \<le> a_md;
length ys = Suc (length list);
length lm = n;
Suc n \<le> pstr\<rbrakk>
\<Longrightarrow> (lm @ last ys # 0\<^bsup>pstr - Suc n\<^esup> @ butlast ys @
0\<^bsup>a_md - (pstr + length list)\<^esup> @ suf_lm)[pstr + length list :=
last ys, n := 0] =
lm @ 0::nat\<^bsup>pstr - n\<^esup> @ ys @ 0\<^bsup>a_md - Suc (pstr + length list)\<^esup> @ suf_lm"
apply(insert list_update_length[of
"lm @ last ys # 0\<^bsup>pstr - Suc n\<^esup> @ butlast ys" 0
"0\<^bsup>a_md - Suc (pstr + length list)\<^esup> @ suf_lm" "last ys"], simp)
apply(simp add: exponent_cons_iff)
apply(insert list_update_length[of "lm"
"last ys" "0\<^bsup>pstr - Suc n\<^esup> @ butlast ys @
last ys # 0\<^bsup>a_md - Suc (pstr + length list)\<^esup> @ suf_lm" 0], simp)
apply(simp add: exponent_cons_iff)
apply(case_tac "ys = []", simp_all add: append_butlast_last_id)
done
lemma cn_merge_gs_ex:
"\<lbrakk>\<And>x aprog a_md rs_pos rs suf_lm lm.
\<lbrakk>x \<in> set gs; rec_ci x = (aprog, rs_pos, a_md);
rec_calc_rel x lm rs\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp
= (length aprog, lm @ [rs] @ 0\<^bsup>a_md - rs_pos - 1\<^esup> @ suf_lm);
pstr + length gs\<le> a_md;
\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k);
length ys = length gs; length lm = n;
pstr \<ge> Max (set (Suc n # map (\<lambda>(aprog, p, n). n) (map rec_ci gs)))\<rbrakk>
\<Longrightarrow> \<exists> stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - n\<^esup> @ suf_lm)
(cn_merge_gs (map rec_ci gs) pstr) stp
= (listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) gs) +
3 * length gs, lm @ 0\<^bsup>pstr - n\<^esup> @ ys @ 0\<^bsup>a_md - (pstr + length gs)\<^esup> @ suf_lm)"
apply(induct gs arbitrary: ys rule: list_tl_induct)
apply(simp add: exponent_add_iff, simp)
proof -
fix a list ys
assume ind: "\<And>x aprog a_md rs_pos rs suf_lm lm.
\<lbrakk>x = a \<or> x \<in> set list; rec_ci x = (aprog, rs_pos, a_md);
rec_calc_rel x lm rs\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp =
(length aprog, lm @ rs # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)"
and ind2:
"\<And>ys. \<lbrakk>\<And>x aprog a_md rs_pos rs suf_lm lm.
\<lbrakk>x \<in> set list; rec_ci x = (aprog, rs_pos, a_md);
rec_calc_rel x lm rs\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp
= (length aprog, lm @ rs # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm);
\<forall>k<length list. rec_calc_rel (list ! k) lm (ys ! k);
length ys = length list\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - n\<^esup> @ suf_lm)
(cn_merge_gs (map rec_ci list) pstr) stp =
(listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) list) +
3 * length list,
lm @ 0\<^bsup>pstr - n\<^esup> @ ys @ 0\<^bsup>a_md - (pstr + length list)\<^esup> @ suf_lm)"
and h: "Suc (pstr + length list) \<le> a_md"
"\<forall>k<Suc (length list).
rec_calc_rel ((list @ [a]) ! k) lm (ys ! k)"
"length ys = Suc (length list)"
"length lm = n"
"Suc n \<le> pstr \<and> (\<lambda>(aprog, p, n). n) (rec_ci a) \<le> pstr \<and>
(\<forall>a\<in>set list. (\<lambda>(aprog, p, n). n) (rec_ci a) \<le> pstr)"
from h have k1:
"\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - n\<^esup> @ suf_lm)
(cn_merge_gs (map rec_ci list) pstr) stp =
(listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) list) +
3 * length list, lm @ 0\<^bsup>pstr - n\<^esup> @ butlast ys @
0\<^bsup>a_md - (pstr + length list)\<^esup> @ suf_lm) "
apply(rule_tac ind2)
apply(rule_tac ind, auto)
done
from k1 and h show
"\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - n\<^esup> @ suf_lm)
(cn_merge_gs (map rec_ci list @ [rec_ci a]) pstr) stp =
(listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) list) +
(\<lambda>(ap, pos, n). length ap) (rec_ci a) + (3 + 3 * length list),
lm @ 0\<^bsup>pstr - n\<^esup> @ ys @ 0\<^bsup>a_md - Suc (pstr + length list)\<^esup> @ suf_lm)"
apply(simp add: cn_merge_gs_tl_app)
thm abc_append_exc2
apply(rule_tac as =
"(\<Sum>(ap, pos, n)\<leftarrow>map rec_ci list. length ap) + 3 * length list"
and bm = "lm @ 0\<^bsup>pstr - n\<^esup> @ butlast ys @
0\<^bsup>a_md - (pstr + length list)\<^esup> @ suf_lm"
and bs = "(\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3"
and bm' = "lm @ 0\<^bsup>pstr - n\<^esup> @ ys @ 0\<^bsup>a_md - Suc (pstr + length list)\<^esup> @
suf_lm" in abc_append_exc2, simp)
apply(simp add: cn_merge_gs_length)
proof -
from h show
"\<exists>bstp. abc_steps_l (0, lm @ 0\<^bsup>pstr - n\<^esup> @ butlast ys @
0\<^bsup>a_md - (pstr + length list)\<^esup> @ suf_lm)
((\<lambda>(gprog, gpara, gn). gprog [+] recursive.empty gpara
(pstr + length list)) (rec_ci a)) bstp =
((\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3,
lm @ 0\<^bsup>pstr - n\<^esup> @ ys @ 0\<^bsup>a_md - Suc (pstr + length list)\<^esup> @ suf_lm)"
apply(case_tac "rec_ci a", simp)
apply(rule_tac as = "length aa" and
bm = "lm @ (ys ! (length list)) #
0\<^bsup>pstr - Suc n\<^esup> @ butlast ys @ 0\<^bsup>a_md - (pstr + length list)\<^esup> @ suf_lm"
and bs = "3" and bm' = "lm @ 0\<^bsup>pstr - n\<^esup> @ ys @
0\<^bsup>a_md - Suc (pstr + length list)\<^esup> @ suf_lm" in abc_append_exc2)
proof -
fix aa b c
assume g: "rec_ci a = (aa, b, c)"
from h and g have k2: "b = n"
apply(erule_tac x = "length list" in allE, simp)
apply(subgoal_tac "length lm = b", simp)
apply(rule para_pattern, simp, simp)
done
from h and g and this show
"\<exists>astp. abc_steps_l (0, lm @ 0\<^bsup>pstr - n\<^esup> @ butlast ys @
0\<^bsup>a_md - (pstr + length list)\<^esup> @ suf_lm) aa astp =
(length aa, lm @ ys ! length list # 0\<^bsup>pstr - Suc n\<^esup> @
butlast ys @ 0\<^bsup>a_md - (pstr + length list)\<^esup> @ suf_lm)"
apply(subgoal_tac "c \<ge> Suc n")
apply(insert ind[of a aa b c lm "ys ! length list"
"0\<^bsup>pstr - c\<^esup> @ butlast ys @ 0\<^bsup>a_md - (pstr + length list)\<^esup> @ suf_lm"], simp)
apply(erule_tac x = "length list" in allE,
simp add: exponent_add_iff)
apply(rule_tac Suc_leI, rule_tac ci_ad_ge_paras, simp)
done
next
fix aa b c
show "length aa = length aa" by simp
next
fix aa b c
assume "rec_ci a = (aa, b, c)"
from h and this show
"\<exists>bstp. abc_steps_l (0, lm @ ys ! length list #
0\<^bsup>pstr - Suc n\<^esup> @ butlast ys @ 0\<^bsup>a_md - (pstr + length list)\<^esup> @ suf_lm)
(recursive.empty b (pstr + length list)) bstp =
(3, lm @ 0\<^bsup>pstr - n\<^esup> @ ys @ 0\<^bsup>a_md - Suc (pstr + length list)\<^esup> @ suf_lm)"
apply(insert empty_ex [of b "pstr + length list"
"lm @ ys ! length list # 0\<^bsup>pstr - Suc n\<^esup> @ butlast ys @
0\<^bsup>a_md - (pstr + length list)\<^esup> @ suf_lm"], simp)
apply(subgoal_tac "b = n")
apply(simp add: nth_append split: if_splits)
apply(erule_tac x = "length list" in allE, simp)
apply(drule para_pattern, simp, simp)
done
next
fix aa b c
show "3 = length (recursive.empty b (pstr + length list))"
by simp
next
fix aa b aaa ba
show "length aa + 3 = length aa + 3" by simp
next
fix aa b c
show "empty b (pstr + length list) \<noteq> []"
by(simp add: empty.simps)
qed
next
show "(\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3 =
length ((\<lambda>(gprog, gpara, gn). gprog [+]
recursive.empty gpara (pstr + length list)) (rec_ci a))"
by(case_tac "rec_ci a", simp)
next
show "listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) list) +
(\<lambda>(ap, pos, n). length ap) (rec_ci a) + (3 + 3 * length list)=
(\<Sum>(ap, pos, n)\<leftarrow>map rec_ci list. length ap) + 3 * length list +
((\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3)" by simp
next
show "(\<lambda>(gprog, gpara, gn). gprog [+]
recursive.empty gpara (pstr + length list)) (rec_ci a) \<noteq> []"
by(case_tac "rec_ci a",
simp add: abc_append.simps abc_shift.simps)
qed
qed
declare drop_abc_lm_v_simp[simp del]
lemma [simp]: "length (mv_boxes aa ba n) = 3*n"
by(induct n, auto simp: mv_boxes.simps)
lemma exp_suc: "a\<^bsup>Suc b\<^esup> = a\<^bsup>b\<^esup> @ [a]"
by(simp add: exponent_def rep_ind del: replicate.simps)
lemma [simp]:
"\<lbrakk>Suc n \<le> ba - aa; length lm2 = Suc n;
length lm3 = ba - Suc (aa + n)\<rbrakk>
\<Longrightarrow> (last lm2 # lm3 @ butlast lm2 @ 0 # lm4) ! (ba - aa) = (0::nat)"
proof -
assume h: "Suc n \<le> ba - aa"
and g: "length lm2 = Suc n" "length lm3 = ba - Suc (aa + n)"
from h and g have k: "ba - aa = Suc (length lm3 + n)"
by arith
from k show
"(last lm2 # lm3 @ butlast lm2 @ 0 # lm4) ! (ba - aa) = 0"
apply(simp, insert g)
apply(simp add: nth_append)
done
qed
lemma [simp]: "length lm1 = aa \<Longrightarrow>
(lm1 @ 0\<^bsup>n\<^esup> @ 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>
(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;
length lm2 = Suc n; length lm3 = ba - Suc (aa + n)\<rbrakk>
\<Longrightarrow> (lm1 @ 0\<^bsup>n\<^esup> @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4) ! (ba + n) = 0"
using nth_append[of "lm1 @ 0\<Colon>'a\<^bsup>n\<^esup> @ last lm2 # lm3 @ butlast lm2"
"(0\<Colon>'a) # lm4" "ba + n"]
apply(simp)
done
lemma [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\<^bsup>n\<^esup> @ last lm2 # lm3 @ butlast lm2 @ (0::nat) # lm4)
[ba + n := last lm2, aa + n := 0] =
lm1 @ 0 # 0\<^bsup>n\<^esup> @ lm3 @ lm2 @ lm4"
using list_update_append[of "lm1 @ 0\<^bsup>n\<^esup> @ last lm2 # lm3 @ butlast lm2" "0 # lm4"
"ba + n" "last lm2"]
apply(simp)
apply(simp add: list_update_append)
apply(simp only: exponent_cons_iff exp_suc, simp)
apply(case_tac lm2, simp, simp)
done
lemma mv_boxes_ex:
"\<lbrakk>n \<le> ba - aa; ba > aa; length lm1 = aa;
length (lm2::nat list) = n; length lm3 = ba - aa - n\<rbrakk>
\<Longrightarrow> \<exists> stp. abc_steps_l (0, lm1 @ lm2 @ lm3 @ 0\<^bsup>n\<^esup> @ lm4)
(mv_boxes aa ba n) stp = (3 * n, lm1 @ 0\<^bsup>n\<^esup> @ lm3 @ lm2 @ lm4)"
apply(induct n arbitrary: lm2 lm3 lm4, simp)
apply(rule_tac x = 0 in exI, simp add: abc_steps_zero,
simp add: mv_boxes.simps del: exp_suc_iff)
apply(rule_tac as = "3 *n" and bm = "lm1 @ 0\<^bsup>n\<^esup> @ last lm2 # lm3 @
butlast lm2 @ 0 # lm4" in abc_append_exc2, simp_all)
apply(simp only: exponent_cons_iff, simp only: exp_suc, simp)
proof -
fix n lm2 lm3 lm4
assume ind:
"\<And>lm2 lm3 lm4. \<lbrakk>length lm2 = n; length lm3 = ba - (aa + n)\<rbrakk> \<Longrightarrow>
\<exists>stp. abc_steps_l (0, lm1 @ lm2 @ lm3 @ 0\<^bsup>n\<^esup> @ lm4)
(mv_boxes aa ba n) stp = (3 * n, lm1 @ 0\<^bsup>n\<^esup> @ lm3 @ lm2 @ lm4)"
and h: "Suc n \<le> ba - aa" "aa < ba" "length (lm1::nat list) = aa"
"length (lm2::nat list) = Suc n"
"length (lm3::nat list) = ba - Suc (aa + n)"
from h show
"\<exists>astp. abc_steps_l (0, lm1 @ lm2 @ lm3 @ 0\<^bsup>n\<^esup> @ 0 # lm4)
(mv_boxes aa ba n) astp =
(3 * n, lm1 @ 0\<^bsup>n\<^esup> @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4)"
apply(insert ind[of "butlast lm2" "last lm2 # lm3" "0 # lm4"],
simp)
apply(subgoal_tac "lm1 @ butlast lm2 @ last lm2 # lm3 @ 0\<^bsup>n\<^esup> @
0 # lm4 = lm1 @ lm2 @ lm3 @ 0\<^bsup>n\<^esup> @ 0 # lm4", simp, simp)
apply(case_tac "lm2 = []", simp, simp)
done
next
fix n lm2 lm3 lm4
assume h: "Suc n \<le> ba - aa"
"aa < ba"
"length (lm1::nat list) = aa"
"length (lm2::nat list) = Suc n"
"length (lm3::nat list) = ba - Suc (aa + n)"
thus " \<exists>bstp. abc_steps_l (0, lm1 @ 0\<^bsup>n\<^esup> @ last lm2 # lm3 @
butlast lm2 @ 0 # lm4)
(recursive.empty (aa + n) (ba + n)) bstp
= (3, lm1 @ 0 # 0\<^bsup>n\<^esup> @ lm3 @ lm2 @ lm4)"
apply(insert empty_ex[of "aa + n" "ba + n"
"lm1 @ 0\<^bsup>n\<^esup> @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4"], simp)
done
qed
(*
lemma [simp]: "\<lbrakk>Suc n \<le> aa - ba;
ba < aa;
length lm2 = aa - Suc (ba + n)\<rbrakk>
\<Longrightarrow> ((0::nat) # lm2 @ 0\<^bsup>n\<^esup> @ last lm3 # lm4) ! (aa - ba)
= last lm3"
proof -
assume h: "Suc n \<le> aa - ba"
and g: " ba < aa" "length lm2 = aa - Suc (ba + n)"
from h and g have k: "aa - ba = Suc (length lm2 + n)"
by arith
thus "((0::nat) # lm2 @ 0\<^bsup>n\<^esup> @ last lm3 # lm4) ! (aa - ba) = last lm3"
apply(simp, simp add: nth_append)
done
qed
*)
lemma [simp]: "\<lbrakk>Suc n \<le> aa - ba; ba < aa; length lm1 = ba;
length lm2 = aa - Suc (ba + n); length lm3 = Suc n\<rbrakk>
\<Longrightarrow> (lm1 @ butlast lm3 @ 0 # lm2 @ 0\<^bsup>n\<^esup> @ last lm3 # lm4) ! (aa + n) = last lm3"
using nth_append[of "lm1 @ butlast lm3 @ 0 # lm2 @ 0\<^bsup>n\<^esup>" "last lm3 # lm4" "aa + n"]
apply(simp)
done
lemma [simp]: "\<lbrakk>Suc n \<le> aa - ba; ba < aa; length lm1 = ba;
length lm2 = aa - Suc (ba + n); length lm3 = Suc n\<rbrakk>
\<Longrightarrow> (lm1 @ butlast lm3 @ 0 # lm2 @ 0\<^bsup>n\<^esup> @ last lm3 # lm4) ! (ba + n) = 0"
apply(simp add: nth_append)
done
lemma [simp]: "\<lbrakk>Suc n \<le> aa - ba; ba < aa; length lm1 = ba;
length lm2 = aa - Suc (ba + n); length lm3 = Suc n\<rbrakk>
\<Longrightarrow> (lm1 @ butlast lm3 @ 0 # lm2 @ 0\<^bsup>n\<^esup> @ last lm3 # lm4)[ba + n := last lm3, aa + n := 0]
= lm1 @ lm3 @ lm2 @ 0 # 0\<^bsup>n\<^esup> @ lm4"
using list_update_append[of "lm1 @ butlast lm3" "(0\<Colon>'a) # lm2 @ 0\<Colon>'a\<^bsup>n\<^esup> @ last lm3 # lm4"]
apply(simp)
using list_update_append[of "lm1 @ butlast lm3 @ last lm3 # lm2 @ 0\<Colon>'a\<^bsup>n\<^esup>"
"last lm3 # lm4" "aa + n" "0"]
apply(simp)
apply(simp only: exp_ind_def[THEN sym] exp_suc, simp)
apply(case_tac lm3, simp, simp)
done
lemma mv_boxes_ex2:
"\<lbrakk>n \<le> aa - ba;
ba < aa;
length (lm1::nat list) = ba;
length (lm2::nat list) = aa - ba - n;
length (lm3::nat list) = n\<rbrakk>
\<Longrightarrow> \<exists> stp. abc_steps_l (0, lm1 @ 0\<^bsup>n\<^esup> @ lm2 @ lm3 @ lm4)
(mv_boxes aa ba n) stp =
(3 * n, lm1 @ lm3 @ lm2 @ 0\<^bsup>n\<^esup> @ lm4)"
apply(induct n arbitrary: lm2 lm3 lm4, simp)
apply(rule_tac x = 0 in exI, simp add: abc_steps_zero,
simp add: mv_boxes.simps del: exp_suc_iff)
apply(rule_tac as = "3 *n" and bm = "lm1 @ butlast lm3 @ 0 # lm2 @
0\<^bsup>n\<^esup> @ last lm3 # lm4" in abc_append_exc2, simp_all)
apply(simp only: exponent_cons_iff, simp only: exp_suc, simp)
proof -
fix n lm2 lm3 lm4
assume ind:
"\<And>lm2 lm3 lm4. \<lbrakk>length lm2 = aa - (ba + n); length lm3 = n\<rbrakk> \<Longrightarrow>
\<exists>stp. abc_steps_l (0, lm1 @ 0\<^bsup>n\<^esup> @ lm2 @ lm3 @ lm4)
(mv_boxes aa ba n) stp =
(3 * n, lm1 @ lm3 @ lm2 @ 0\<^bsup>n\<^esup> @ lm4)"
and h: "Suc n \<le> aa - ba"
"ba < aa"
"length (lm1::nat list) = ba"
"length (lm2::nat list) = aa - Suc (ba + n)"
"length (lm3::nat list) = Suc n"
from h show
"\<exists>astp. abc_steps_l (0, lm1 @ 0\<^bsup>n\<^esup> @ 0 # lm2 @ lm3 @ lm4)
(mv_boxes aa ba n) astp =
(3 * n, lm1 @ butlast lm3 @ 0 # lm2 @ 0\<^bsup>n\<^esup> @ last lm3 # lm4)"
apply(insert ind[of "0 # lm2" "butlast lm3" "last lm3 # lm4"],
simp)
apply(subgoal_tac
"lm1 @ 0\<^bsup>n\<^esup> @ 0 # lm2 @ butlast lm3 @ last lm3 # lm4 =
lm1 @ 0\<^bsup>n\<^esup> @ 0 # lm2 @ lm3 @ lm4", simp, simp)
apply(case_tac "lm3 = []", simp, simp)
done
next
fix n lm2 lm3 lm4
assume h:
"Suc n \<le> aa - ba"
"ba < aa"
"length lm1 = ba"
"length (lm2::nat list) = aa - Suc (ba + n)"
"length (lm3::nat list) = Suc n"
thus
"\<exists>bstp. abc_steps_l (0, lm1 @ butlast lm3 @ 0 # lm2 @ 0\<^bsup>n\<^esup> @
last lm3 # lm4)
(recursive.empty (aa + n) (ba + n)) bstp =
(3, lm1 @ lm3 @ lm2 @ 0 # 0\<^bsup>n\<^esup> @ lm4)"
apply(insert empty_ex[of "aa + n" "ba + n" "lm1 @ butlast lm3 @
0 # lm2 @ 0\<^bsup>n\<^esup> @ last lm3 # lm4"], simp)
done
qed
lemma cn_merge_gs_len:
"length (cn_merge_gs (map rec_ci gs) pstr) =
(\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 3 * length gs"
apply(induct gs arbitrary: pstr, simp, simp)
apply(case_tac "rec_ci a", simp)
done
lemma [simp]: "n < pstr \<Longrightarrow>
Suc (pstr + length ys - n) = Suc (pstr + length ys) - n"
by arith
lemma save_paras':
"\<lbrakk>length lm = n; pstr > n; a_md > pstr + length ys + n\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>pstr - n\<^esup> @ ys @
0\<^bsup>a_md - pstr - length ys\<^esup> @ suf_lm)
(mv_boxes 0 (pstr + Suc (length ys)) n) stp
= (3 * n, 0\<^bsup>pstr\<^esup> @ ys @ 0 # lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm)"
thm mv_boxes_ex
apply(insert mv_boxes_ex[of n "pstr + Suc (length ys)" 0 "[]" "lm"
"0\<^bsup>pstr - n\<^esup> @ ys @ [0]" "0\<^bsup>a_md - pstr - length ys - n - Suc 0\<^esup> @ suf_lm"], simp)
apply(erule_tac exE, rule_tac x = stp in exI,
simp add: exponent_add_iff)
apply(simp only: exponent_cons_iff, simp)
done
lemma [simp]:
"(max ba (Max (insert ba (((\<lambda>(aprog, p, n). n) o rec_ci) ` set gs))))
= (Max (insert ba (((\<lambda>(aprog, p, n). n) o rec_ci) ` set gs)))"
apply(rule min_max.sup_absorb2, auto)
done
lemma [simp]:
"((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs) =
(((\<lambda>(aprog, p, n). n) o rec_ci) ` set gs)"
apply(induct gs)
apply(simp, simp)
done
lemma ci_cn_md_def:
"\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
rec_ci f = (a, aa, ba)\<rbrakk>
\<Longrightarrow> a_md = max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) o
rec_ci) ` set gs))) + Suc (length gs) + n"
apply(simp add: rec_ci.simps, auto)
done
lemma save_paras_prog_ex:
"\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
rec_ci f = (a, aa, ba);
pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs))))\<rbrakk>
\<Longrightarrow> \<exists>ap bp cp.
aprog = ap [+] bp [+] cp \<and>
length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
3 * length gs \<and> bp = mv_boxes 0 (pstr + Suc (length gs)) n"
apply(simp add: rec_ci.simps)
apply(rule_tac x =
"cn_merge_gs (map rec_ci gs) (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) o rec_ci) ` set gs))))" in exI,
simp add: cn_merge_gs_len)
apply(rule_tac x =
"mv_boxes (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))))
0 (length gs) [+] a [+]recursive.empty aa (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
empty_boxes (length gs) [+] recursive.empty (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
mv_boxes (Suc (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci)
` set gs))) + length gs)) 0 n" in exI, auto)
apply(simp add: abc_append_commute)
done
lemma save_paras:
"\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
rs_pos = n;
\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k);
length ys = length gs;
length lm = n;
rec_ci f = (a, aa, ba);
pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs))))\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
3 * length gs, lm @ 0\<^bsup>pstr - n\<^esup> @ ys @
0\<^bsup>a_md - pstr - length ys\<^esup> @ suf_lm) aprog stp =
((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
3 * length gs + 3 * n,
0\<^bsup>pstr\<^esup> @ ys @ 0 # lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm)"
proof -
assume h:
"rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)"
"rs_pos = n"
"\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)"
"length ys = length gs"
"length lm = n"
"rec_ci f = (a, aa, ba)"
and g: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs))))"
from h and g have k1:
"\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and>
length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
3 *length gs \<and> bp = mv_boxes 0 (pstr + Suc (length ys)) n"
apply(drule_tac save_paras_prog_ex, auto)
done
from h have k2:
"\<exists> stp. abc_steps_l (0, lm @ 0\<^bsup>pstr - n\<^esup> @ ys @
0\<^bsup>a_md - pstr - length ys\<^esup> @ suf_lm)
(mv_boxes 0 (pstr + Suc (length ys)) n) stp =
(3 * n, 0\<^bsup>pstr\<^esup> @ ys @ 0 # lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm)"
apply(rule_tac save_paras', simp, simp_all add: g)
apply(drule_tac a = a and aa = aa and ba = ba in
ci_cn_md_def, simp, simp)
done
from k1 show
"\<exists>stp. abc_steps_l ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
3 * length gs, lm @ 0\<^bsup>pstr - n\<^esup> @ ys @
0\<^bsup>a_md - pstr - length ys\<^esup> @ suf_lm) aprog stp =
((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
3 * length gs + 3 * n,
0\<^bsup>pstr\<^esup> @ ys @ 0 # lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm)"
proof(erule_tac exE, erule_tac exE, erule_tac exE, erule_tac exE)
fix ap bp apa cp
assume "aprog = ap [+] bp [+] cp \<and> length ap =
(\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 3 * length gs
\<and> bp = mv_boxes 0 (pstr + Suc (length ys)) n"
from this and k2 show "?thesis"
apply(simp)
apply(rule_tac abc_append_exc1, simp, simp, simp)
done
qed
qed
lemma ci_cn_para_eq:
"rec_ci (Cn n f gs) = (aprog, rs_pos, a_md) \<Longrightarrow> rs_pos = n"
apply(simp add: rec_ci.simps, case_tac "rec_ci f", simp)
done
lemma calc_gs_prog_ex:
"\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
rec_ci f = (a, aa, ba);
Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs)))) = pstr\<rbrakk>
\<Longrightarrow> \<exists>ap bp. aprog = ap [+] bp \<and>
ap = cn_merge_gs (map rec_ci gs) pstr"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "mv_boxes 0 (Suc (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n [+]
mv_boxes (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+]
a [+] recursive.empty aa (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
empty_boxes (length gs) [+] recursive.empty (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
mv_boxes (Suc (max (Suc n) (Max
(insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n"
in exI)
apply(auto simp: abc_append_commute)
done
lemma cn_calc_gs:
assumes ind:
"\<And>x aprog a_md rs_pos rs suf_lm lm.
\<lbrakk>x \<in> set gs;
rec_ci x = (aprog, rs_pos, a_md);
rec_calc_rel x lm rs\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp =
(length aprog, lm @ [rs] @ 0\<^bsup>a_md - rs_pos - 1\<^esup> @ suf_lm)"
and h: "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)"
"\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)"
"length ys = length gs"
"length lm = n"
"rec_ci f = (a, aa, ba)"
"Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs)))) = pstr"
shows
"\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp =
((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 3 * length gs,
lm @ 0\<^bsup>pstr - n\<^esup> @ ys @ 0\<^bsup>a_md -pstr - length ys\<^esup> @ suf_lm) "
proof -
from h have k1:
"\<exists> ap bp. aprog = ap [+] bp \<and> ap =
cn_merge_gs (map rec_ci gs) pstr"
by(erule_tac calc_gs_prog_ex, auto)
from h have j1: "rs_pos = n"
by(simp add: ci_cn_para_eq)
from h have j2: "a_md \<ge> pstr"
by(drule_tac a = a and aa = aa and ba = ba in
ci_cn_md_def, simp, simp)
from h have j3: "pstr > n"
by(auto)
from j1 and j2 and j3 and h have k2:
"\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm)
(cn_merge_gs (map rec_ci gs) pstr) stp
= ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 3 * length gs,
lm @ 0\<^bsup>pstr - n\<^esup> @ ys @ 0\<^bsup>a_md - pstr - length ys\<^esup> @ suf_lm)"
apply(simp)
apply(rule_tac cn_merge_gs_ex, rule_tac ind, simp, simp, auto)
apply(drule_tac a = a and aa = aa and ba = ba in
ci_cn_md_def, simp, simp)
apply(rule min_max.le_supI2, auto)
done
from k1 show "?thesis"
proof(erule_tac exE, erule_tac exE, simp)
fix ap bp
from k2 show
"\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm)
(cn_merge_gs (map rec_ci gs) pstr [+] bp) stp =
(listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) gs) +
3 * length gs,
lm @ 0\<^bsup>pstr - n\<^esup> @ ys @ 0\<^bsup>a_md - (pstr + length ys)\<^esup> @ suf_lm)"
apply(insert abc_append_exc1[of
"lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm"
"(cn_merge_gs (map rec_ci gs) pstr)"
"length (cn_merge_gs (map rec_ci gs) pstr)"
"lm @ 0\<^bsup>pstr - n\<^esup> @ ys @ 0\<^bsup>a_md - pstr - length ys\<^esup> @ suf_lm" 0
"[]" bp], simp add: cn_merge_gs_len)
done
qed
qed
lemma reset_new_paras':
"\<lbrakk>length lm = n;
pstr > 0;
a_md \<ge> pstr + length ys + n;
pstr > length ys\<rbrakk> \<Longrightarrow>
\<exists>stp. abc_steps_l (0, 0\<^bsup>pstr\<^esup> @ ys @ 0 # lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @
suf_lm) (mv_boxes pstr 0 (length ys)) stp =
(3 * length ys, ys @ 0\<^bsup>pstr\<^esup> @ 0 # lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm)"
thm mv_boxes_ex2
apply(insert mv_boxes_ex2[of "length ys" "pstr" 0 "[]"
"0\<^bsup>pstr - length ys\<^esup>" "ys"
"0 # lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm"],
simp add: exponent_add_iff)
done
lemma [simp]:
"\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
rec_calc_rel f ys rs; rec_ci f = (a, aa, ba);
pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs))))\<rbrakk>
\<Longrightarrow> length ys < pstr"
apply(subgoal_tac "length ys = aa", simp)
apply(subgoal_tac "aa < ba \<and> ba \<le> pstr",
rule basic_trans_rules(22), auto)
apply(rule min_max.le_supI2)
apply(auto)
apply(erule_tac para_pattern, simp)
done
lemma reset_new_paras_prog_ex:
"\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
rec_ci f = (a, aa, ba);
Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs)))) = pstr\<rbrakk>
\<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and>
length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
3 *length gs + 3 * n \<and> bp = mv_boxes pstr 0 (length gs)"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "cn_merge_gs (map rec_ci gs) (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
mv_boxes 0 (Suc (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n" in exI,
simp add: cn_merge_gs_len)
apply(rule_tac x = "a [+]
recursive.empty aa (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
empty_boxes (length gs) [+] recursive.empty
(max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n
[+] mv_boxes (Suc (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI,
auto simp: abc_append_commute)
done
lemma reset_new_paras:
"\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
rs_pos = n;
\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k);
length ys = length gs;
length lm = n;
length ys = aa;
rec_ci f = (a, aa, ba);
pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs))))\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
3 * length gs + 3 * n,
0\<^bsup>pstr \<^esup>@ ys @ 0 # lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm) aprog stp =
((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs + 3 * n,
ys @ 0\<^bsup>pstr\<^esup> @ 0 # lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm)"
proof -
assume h:
"rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)"
"rs_pos = n"
"length ys = aa"
"\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)"
"length ys = length gs" "length lm = n"
"rec_ci f = (a, aa, ba)"
and g: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs))))"
thm rec_ci.simps
from h and g have k1:
"\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap =
(\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
3 *length gs + 3 * n \<and> bp = mv_boxes pstr 0 (length ys)"
by(drule_tac reset_new_paras_prog_ex, auto)
from h have k2:
"\<exists> stp. abc_steps_l (0, 0\<^bsup>pstr \<^esup>@ ys @ 0 # lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @
suf_lm) (mv_boxes pstr 0 (length ys)) stp =
(3 * (length ys),
ys @ 0\<^bsup>pstr\<^esup> @ 0 # lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm)"
apply(rule_tac reset_new_paras', simp)
apply(simp add: g)
apply(drule_tac a = a and aa = aa and ba = ba in ci_cn_md_def,
simp, simp add: g, simp)
apply(subgoal_tac "length gs = aa \<and> aa < ba \<and> ba \<le> pstr", arith,
simp add: para_pattern)
apply(insert g, auto intro: min_max.le_supI2)
done
from k1 show
"\<exists>stp. abc_steps_l ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 3
* length gs + 3 * n, 0\<^bsup>pstr\<^esup> @ ys @ 0 # lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @
suf_lm) aprog stp =
((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs +
3 * n, ys @ 0\<^bsup>pstr\<^esup> @ 0 # lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm)"
proof(erule_tac exE, erule_tac exE, erule_tac exE, erule_tac exE)
fix ap bp apa cp
assume "aprog = ap [+] bp [+] cp \<and> length ap =
(\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 3 * length gs +
3 * n \<and> bp = mv_boxes pstr 0 (length ys)"
from this and k2 show "?thesis"
apply(simp)
apply(drule_tac as =
"(\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 3 * length gs +
3 * n" and ap = ap and cp = cp in abc_append_exc1, auto)
apply(rule_tac x = stp in exI, simp add: h)
using h
apply(simp)
done
qed
qed
thm rec_ci.simps
lemma calc_f_prog_ex:
"\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
rec_ci f = (a, aa, ba);
Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs)))) = pstr\<rbrakk>
\<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and>
length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
6 *length gs + 3 * n \<and> bp = a"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "cn_merge_gs (map rec_ci gs) (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
mv_boxes 0 (Suc (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n [+]
mv_boxes (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs)" in exI,
simp add: cn_merge_gs_len)
apply(rule_tac x = "recursive.empty aa (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
empty_boxes (length gs) [+] recursive.empty (max (Suc n) (
Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
mv_boxes (Suc (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI,
auto simp: abc_append_commute)
done
lemma calc_cn_f:
assumes ind:
"\<And>x aprog a_md rs_pos rs suf_lm lm.
\<lbrakk>x \<in> set (f # gs);
rec_ci x = (aprog, rs_pos, a_md);
rec_calc_rel x lm rs\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp =
(length aprog, lm @ [rs] @ 0\<^bsup>a_md - rs_pos - 1\<^esup> @ suf_lm)"
and h: "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)"
"rec_calc_rel (Cn n f gs) lm rs"
"length ys = length gs"
"rec_calc_rel f ys rs"
"length lm = n"
"rec_ci f = (a, aa, ba)"
and p: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs))))"
shows "\<exists>stp. abc_steps_l
((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs + 3 * n,
ys @ 0\<^bsup>pstr\<^esup> @ 0 # lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm) aprog stp =
((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs +
3 * n + length a,
ys @ rs # 0\<^bsup>pstr\<^esup> @ lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm)"
proof -
from h have k1:
"\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and>
length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
6 *length gs + 3 * n \<and> bp = a"
by(drule_tac calc_f_prog_ex, auto)
from h and k1 show "?thesis"
proof (erule_tac exE, erule_tac exE, erule_tac exE, erule_tac exE)
fix ap bp apa cp
assume
"aprog = ap [+] bp [+] cp \<and>
length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
6 * length gs + 3 * n \<and> bp = a"
from h and this show "?thesis"
apply(simp, rule_tac abc_append_exc1, simp_all)
apply(insert ind[of f "a" aa ba ys rs
"0\<^bsup>pstr - ba + length gs \<^esup> @ 0 # lm @
0\<^bsup>a_md - Suc (pstr + length gs + n)\<^esup> @ suf_lm"], simp)
apply(subgoal_tac "ba > aa \<and> aa = length gs\<and> pstr \<ge> ba", simp)
apply(simp add: exponent_add_iff)
apply(case_tac pstr, simp add: p)
apply(simp only: exp_suc, simp)
apply(rule conjI, rule ci_ad_ge_paras, simp, rule conjI)
apply(subgoal_tac "length ys = aa", simp,
rule para_pattern, simp, simp)
apply(insert p, simp)
apply(auto intro: min_max.le_supI2)
done
qed
qed
(*
lemma [simp]:
"\<lbrakk>pstr + length ys + n \<le> a_md; ys \<noteq> []\<rbrakk> \<Longrightarrow>
pstr < a_md + length suf_lm"
apply(case_tac "length ys", simp)
apply(arith)
done
*)
lemma [simp]:
"pstr > length ys
\<Longrightarrow> (ys @ rs # 0\<^bsup>pstr\<^esup> @ lm @
0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm) ! pstr = (0::nat)"
apply(simp add: nth_append)
done
(*
lemma [simp]: "\<lbrakk>length ys < pstr; pstr - length ys = Suc x\<rbrakk>
\<Longrightarrow> pstr - Suc (length ys) = x"
by arith
*)
lemma [simp]: "pstr > length ys \<Longrightarrow>
(ys @ rs # 0\<^bsup>pstr\<^esup> @ lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm)
[pstr := rs, length ys := 0] =
ys @ 0\<^bsup>pstr - length ys\<^esup> @ (rs::nat) # 0\<^bsup>length ys\<^esup> @ lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm"
apply(auto simp: list_update_append)
apply(case_tac "pstr - length ys",simp_all)
using list_update_length[of
"0\<^bsup>pstr - Suc (length ys)\<^esup>" "0" "0\<^bsup>length ys\<^esup> @ lm @
0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm" rs]
apply(simp only: exponent_cons_iff exponent_add_iff, simp)
apply(subgoal_tac "pstr - Suc (length ys) = nat", simp, simp)
done
lemma save_rs':
"\<lbrakk>pstr > length ys\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l (0, ys @ rs # 0\<^bsup>pstr\<^esup> @ lm @
0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm)
(recursive.empty (length ys) pstr) stp =
(3, ys @ 0\<^bsup>pstr - (length ys)\<^esup> @ rs #
0\<^bsup>length ys \<^esup> @ lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm)"
apply(insert empty_ex[of "length ys" pstr
"ys @ rs # 0\<^bsup>pstr\<^esup> @ lm @ 0\<^bsup>a_md - Suc(pstr + length ys + n)\<^esup> @ suf_lm"],
simp)
done
lemma save_rs_prog_ex:
"\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
rec_ci f = (a, aa, ba);
Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs)))) = pstr\<rbrakk>
\<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and>
length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
6 *length gs + 3 * n + length a
\<and> bp = empty aa pstr"
apply(simp add: rec_ci.simps)
apply(rule_tac x =
"cn_merge_gs (map rec_ci gs) (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))))
[+] mv_boxes 0 (Suc (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n [+]
mv_boxes (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))))
0 (length gs) [+] a"
in exI, simp add: cn_merge_gs_len)
apply(rule_tac x =
"empty_boxes (length gs) [+]
recursive.empty (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
mv_boxes (Suc (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))
+ length gs)) 0 n" in exI,
auto simp: abc_append_commute)
done
lemma save_rs:
assumes h:
"rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)"
"rec_calc_rel (Cn n f gs) lm rs"
"\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)"
"length ys = length gs"
"rec_calc_rel f ys rs"
"rec_ci f = (a, aa, ba)"
"length lm = n"
and pdef: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs))))"
shows "\<exists>stp. abc_steps_l
((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs
+ 3 * n + length a, ys @ rs # 0\<^bsup>pstr\<^esup> @ lm @
0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm) aprog stp =
((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs
+ 3 * n + length a + 3,
ys @ 0\<^bsup>pstr - length ys \<^esup> @ rs # 0\<^bsup>length ys\<^esup> @ lm @
0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm)"
proof -
thm rec_ci.simps
from h and pdef have k1:
"\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and>
length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
6 *length gs + 3 * n + length a \<and> bp = empty (length ys) pstr "
apply(subgoal_tac "length ys = aa")
apply(drule_tac a = a and aa = aa and ba = ba in save_rs_prog_ex,
simp, simp, simp)
by(rule_tac para_pattern, simp, simp)
from k1 show
"\<exists>stp. abc_steps_l
((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs + 3 * n
+ length a, ys @ rs # 0\<^bsup>pstr \<^esup>@ lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup>
@ suf_lm) aprog stp =
((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs + 3 * n
+ length a + 3, ys @ 0\<^bsup>pstr - length ys\<^esup> @ rs #
0\<^bsup>length ys\<^esup> @ lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm)"
proof (erule_tac exE, erule_tac exE, erule_tac exE, erule_tac exE)
fix ap bp apa cp
assume "aprog = ap [+] bp [+] cp \<and> length ap =
(\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs +
3 * n + length a \<and> bp = recursive.empty (length ys) pstr"
thus"?thesis"
apply(simp, rule_tac abc_append_exc1, simp_all)
apply(rule_tac save_rs', insert h)
apply(subgoal_tac "length gs = aa \<and> pstr \<ge> ba \<and> ba > aa",
arith)
apply(simp add: para_pattern, insert pdef, auto)
apply(rule_tac min_max.le_supI2, simp)
done
qed
qed
lemma [simp]: "length (empty_boxes n) = 2*n"
apply(induct n, simp, simp)
done
lemma empty_step_ex: "length lm = n \<Longrightarrow>
\<exists>stp. abc_steps_l (0, lm @ Suc x # suf_lm) [Dec n 2, Goto 0] stp
= (0, lm @ x # suf_lm)"
apply(rule_tac x = "Suc (Suc 0)" in exI,
simp add: abc_steps_l.simps abc_step_l.simps abc_fetch.simps
abc_lm_v.simps abc_lm_s.simps nth_append list_update_append)
done
lemma empty_box_ex:
"\<lbrakk>length lm = n\<rbrakk> \<Longrightarrow>
\<exists> stp. abc_steps_l (0, lm @ x # suf_lm) [Dec n 2, Goto 0] stp =
(Suc (Suc 0), lm @ 0 # suf_lm)"
apply(induct x)
apply(rule_tac x = "Suc 0" in exI,
simp add: abc_steps_l.simps abc_fetch.simps abc_step_l.simps
abc_lm_v.simps nth_append abc_lm_s.simps, simp)
apply(drule_tac x = x and suf_lm = suf_lm in empty_step_ex,
erule_tac exE, erule_tac exE)
apply(rule_tac x = "stpa + stp" in exI, simp add: abc_steps_add)
done
lemma [simp]: "drop n lm = a # list \<Longrightarrow> list = drop (Suc n) lm"
apply(induct n arbitrary: lm a list, simp)
apply(case_tac "lm", simp, simp)
done
lemma empty_boxes_ex: "\<lbrakk>length lm \<ge> n\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l (0, lm) (empty_boxes n) stp =
(2*n, 0\<^bsup>n\<^esup> @ drop n lm)"
apply(induct n, simp, simp)
apply(rule_tac abc_append_exc2, auto)
apply(case_tac "drop n lm", simp, simp)
proof -
fix n stp a list
assume h: "Suc n \<le> length lm" "drop n lm = a # list"
thus "\<exists>bstp. abc_steps_l (0, 0\<^bsup>n\<^esup> @ a # list) [Dec n 2, Goto 0] bstp =
(Suc (Suc 0), 0 # 0\<^bsup>n\<^esup> @ drop (Suc n) lm)"
apply(insert empty_box_ex[of "0\<^bsup>n\<^esup>" n a list], simp, erule_tac exE)
apply(rule_tac x = stp in exI, simp, simp only: exponent_cons_iff)
apply(simp add: exponent_def rep_ind del: replicate.simps)
done
qed
lemma empty_paras_prog_ex:
"\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
rec_ci f = (a, aa, ba);
Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs)))) = pstr\<rbrakk>
\<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and>
length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
6 *length gs + 3 * n + length a + 3 \<and> bp = empty_boxes (length gs)"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "cn_merge_gs (map rec_ci gs) (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
mv_boxes 0 (Suc (max (Suc n) (Max
(insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n
[+] mv_boxes (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+]
a [+] recursive.empty aa (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))))"
in exI, simp add: cn_merge_gs_len)
apply(rule_tac x = " recursive.empty (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
mv_boxes (Suc (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI,
auto simp: abc_append_commute)
done
lemma empty_paras:
assumes h:
"rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)"
"rec_calc_rel (Cn n f gs) lm rs"
"\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)"
"length ys = length gs"
"rec_calc_rel f ys rs"
"rec_ci f = (a, aa, ba)"
and pdef: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs))))"
and starts: "ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
6 * length gs + 3 * n + length a + 3"
shows "\<exists>stp. abc_steps_l
(ss, ys @ 0\<^bsup>pstr - length ys\<^esup> @ rs # 0\<^bsup>length ys\<^esup>
@ lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm) aprog stp =
(ss + 2 * length gs, 0\<^bsup>pstr\<^esup> @ rs # 0\<^bsup>length ys \<^esup> @ lm @
0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm)"
proof -
from h and pdef and starts have k1:
"\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and>
length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
6 *length gs + 3 * n + length a + 3
\<and> bp = empty_boxes (length ys)"
by(drule_tac empty_paras_prog_ex, auto)
from h have j1: "aa < ba"
by(simp add: ci_ad_ge_paras)
from h have j2: "length gs = aa"
by(drule_tac f = f in para_pattern, simp, simp)
from h and pdef have j3: "ba \<le> pstr"
apply simp
apply(rule_tac min_max.le_supI2, simp)
done
from k1 show "?thesis"
proof (erule_tac exE, erule_tac exE, erule_tac exE, erule_tac exE)
fix ap bp apa cp
assume "aprog = ap [+] bp [+] cp \<and>
length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
6 * length gs + 3 * n + length a + 3 \<and>
bp = empty_boxes (length ys)"
thus"?thesis"
apply(simp, rule_tac abc_append_exc1, simp_all add: starts h)
apply(insert empty_boxes_ex[of
"length gs" "ys @ 0\<^bsup>pstr - (length gs)\<^esup> @ rs #
0\<^bsup>length gs\<^esup> @ lm @ 0\<^bsup>a_md - Suc (pstr + length gs + n)\<^esup> @ suf_lm"],
simp add: h)
apply(erule_tac exE, rule_tac x = stp in exI,
simp add: exponent_def replicate.simps[THEN sym]
replicate_add[THEN sym] del: replicate.simps)
apply(subgoal_tac "pstr >(length gs)", simp)
apply(subgoal_tac "ba > aa \<and> length gs = aa \<and> pstr \<ge> ba", simp)
apply(simp add: j1 j2 j3)
done
qed
qed
(*
lemma [simp]: " n < pstr \<Longrightarrow>
(0\<^bsup>pstr\<^esup>)[n := rs] @ [0::nat] = 0\<^bsup>n\<^esup> @ rs # 0\<^bsup>pstr - n\<^esup>"
apply(insert list_update_length[of "0\<^bsup>n\<^esup>" 0 "0\<^bsup>pstr - Suc n\<^esup>" rs])
apply(insert exponent_cons_iff[of "0::nat" "pstr - Suc n" "[]"], simp)
apply(insert exponent_add_iff[of "0::nat" n "pstr - n" "[]"], simp)
apply(case_tac "pstr - n", simp, simp only: exp_suc, simp)
apply(subgoal_tac "pstr - Suc n = nat", simp)
by arith
*)
lemma restore_rs_prog_ex:
"\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
rec_ci f = (a, aa, ba);
Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs)))) = pstr;
ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
8 * length gs + 3 * n + length a + 3\<rbrakk>
\<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = ss \<and>
bp = empty pstr n"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "cn_merge_gs (map rec_ci gs) (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
mv_boxes 0 (Suc (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n)
\<circ> rec_ci) ` set gs))) + length gs)) n [+]
mv_boxes (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+]
a [+] recursive.empty aa (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
empty_boxes (length gs)" in exI, simp add: cn_merge_gs_len)
apply(rule_tac x = "mv_boxes (Suc (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))
+ length gs)) 0 n"
in exI, auto simp: abc_append_commute)
done
lemma exp_add: "a\<^bsup>b+c\<^esup> = a\<^bsup>b\<^esup> @ a\<^bsup>c\<^esup>"
apply(simp add: exponent_def replicate_add)
done
lemma [simp]: "n < pstr \<Longrightarrow> (0\<^bsup>pstr\<^esup>)[n := rs] @ [0::nat] = 0\<^bsup>n\<^esup> @ rs # 0\<^bsup>pstr - n\<^esup>"
using list_update_length[of "0\<^bsup>n\<^esup>" "0::nat" "0\<^bsup>pstr - Suc n\<^esup>" rs]
apply(simp add: exp_ind_def[THEN sym] exp_add[THEN sym] exp_suc[THEN sym])
done
lemma restore_rs:
assumes h: "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)"
"rec_calc_rel (Cn n f gs) lm rs"
"\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)"
"length ys = length gs"
"rec_calc_rel f ys rs"
"rec_ci f = (a, aa, ba)"
and pdef: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs))))"
and starts: "ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
8 * length gs + 3 * n + length a + 3"
shows "\<exists>stp. abc_steps_l
(ss, 0\<^bsup>pstr\<^esup> @ rs # 0\<^bsup>length ys \<^esup> @ lm @
0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm) aprog stp =
(ss + 3, 0\<^bsup>n\<^esup> @ rs # 0\<^bsup>pstr - n\<^esup> @ 0\<^bsup>length ys \<^esup> @ lm @
0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm)"
proof -
from h and pdef and starts have k1:
"\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = ss \<and>
bp = empty pstr n"
by(drule_tac restore_rs_prog_ex, auto)
from k1 show "?thesis"
proof (erule_tac exE, erule_tac exE, erule_tac exE, erule_tac exE)
fix ap bp apa cp
assume "aprog = ap [+] bp [+] cp \<and> length ap = ss \<and>
bp = recursive.empty pstr n"
thus"?thesis"
apply(simp, rule_tac abc_append_exc1, simp_all add: starts h)
apply(insert empty_ex[of pstr n "0\<^bsup>pstr\<^esup> @ rs # 0\<^bsup>length gs\<^esup> @
lm @ 0\<^bsup>a_md - Suc (pstr + length gs + n)\<^esup> @ suf_lm"], simp)
apply(subgoal_tac "pstr > n", simp)
apply(erule_tac exE, rule_tac x = stp in exI,
simp add: nth_append list_update_append)
apply(simp add: pdef)
done
qed
qed
lemma [simp]:"xs \<noteq> [] \<Longrightarrow> length xs \<ge> Suc 0"
by(case_tac xs, auto)
lemma [simp]: "n < max (Suc n) (max ba (Max (((\<lambda>(aprog, p, n). n) o
rec_ci) ` set gs)))"
by(simp)
lemma restore_paras_prog_ex:
"\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
rec_ci f = (a, aa, ba);
Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs)))) = pstr;
ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
8 * length gs + 3 * n + length a + 6\<rbrakk>
\<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = ss \<and>
bp = mv_boxes (pstr + Suc (length gs)) (0::nat) n"
apply(simp add: rec_ci.simps)
apply(rule_tac x = "cn_merge_gs (map rec_ci gs) (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))))
[+] mv_boxes 0 (Suc (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))
+ length gs)) n [+] mv_boxes (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+]
a [+] recursive.empty aa (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
empty_boxes (length gs) [+]
recursive.empty (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n" in exI, simp add: cn_merge_gs_len)
apply(rule_tac x = "[]" in exI, auto simp: abc_append_commute)
done
lemma restore_paras:
assumes h: "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)"
"rec_calc_rel (Cn n f gs) lm rs"
"\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)"
"length ys = length gs"
"rec_calc_rel f ys rs"
"rec_ci f = (a, aa, ba)"
and pdef:
"pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs))))"
and starts: "ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
8 * length gs + 3 * n + length a + 6"
shows "\<exists>stp. abc_steps_l (ss, 0\<^bsup>n\<^esup> @ rs # 0\<^bsup>pstr - n+ length ys\<^esup> @
lm @ 0\<^bsup>a_md - Suc (pstr + length ys + n)\<^esup> @ suf_lm)
aprog stp = (ss + 3 * n, lm @ rs # 0\<^bsup>a_md - Suc n\<^esup> @ suf_lm)"
proof -
thm rec_ci.simps
from h and pdef and starts have k1:
"\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = ss \<and>
bp = mv_boxes (pstr + Suc (length gs)) (0::nat) n"
by(drule_tac restore_paras_prog_ex, auto)
from k1 show "?thesis"
proof (erule_tac exE, erule_tac exE, erule_tac exE, erule_tac exE)
fix ap bp apa cp
assume "aprog = ap [+] bp [+] cp \<and> length ap = ss \<and>
bp = mv_boxes (pstr + Suc (length gs)) 0 n"
thus"?thesis"
apply(simp, rule_tac abc_append_exc1, simp_all add: starts h)
apply(insert mv_boxes_ex2[of n "pstr + Suc (length gs)" 0 "[]"
"rs # 0\<^bsup>pstr - n + length gs\<^esup>" "lm"
"0\<^bsup>a_md - Suc (pstr + length gs + n)\<^esup> @ suf_lm"], simp)
apply(subgoal_tac "pstr > n \<and>
a_md > pstr + length gs + n \<and> length lm = n" , simp add: exponent_add_iff h)
using h pdef
apply(simp)
apply(frule_tac a = a and
aa = aa and ba = ba in ci_cn_md_def, simp, simp)
apply(subgoal_tac "length lm = rs_pos",
simp add: ci_cn_para_eq, erule_tac para_pattern, simp)
done
qed
qed
lemma ci_cn_length:
"\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
rec_calc_rel (Cn n f gs) lm rs;
rec_ci f = (a, aa, ba)\<rbrakk>
\<Longrightarrow> length aprog = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
8 * length gs + 6 * n + length a + 6"
apply(simp add: rec_ci.simps, auto simp: cn_merge_gs_len)
done
lemma cn_case:
assumes ind:
"\<And>x aprog a_md rs_pos rs suf_lm lm.
\<lbrakk>x \<in> set (f # gs);
rec_ci x = (aprog, rs_pos, a_md);
rec_calc_rel x lm rs\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp =
(length aprog, lm @ [rs] @ 0\<^bsup>a_md - rs_pos - 1\<^esup> @ suf_lm)"
and h: "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)"
"rec_calc_rel (Cn n f gs) lm rs"
shows "\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp
= (length aprog, lm @ [rs] @ 0\<^bsup>a_md - rs_pos - 1\<^esup> @ suf_lm)"
apply(insert h, case_tac "rec_ci f", rule_tac calc_cn_reverse, simp)
proof -
fix a b c ys
let ?pstr = "Max (set (Suc n # c # (map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs)))))"
let ?gs_len = "listsum (map (\<lambda> (ap, pos, n). length ap)
(map rec_ci (gs)))"
assume g: "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)"
"rec_calc_rel (Cn n f gs) lm rs"
"\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)"
"length ys = length gs"
"rec_calc_rel f ys rs"
"n = length lm"
"rec_ci f = (a, b, c)"
hence k1:
"\<exists> stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp =
(?gs_len + 3 * length gs, lm @ 0\<^bsup>?pstr - n\<^esup> @ ys @
0\<^bsup>a_md - ?pstr - length ys\<^esup> @ suf_lm)"
apply(rule_tac a = a and aa = b and ba = c in cn_calc_gs)
apply(rule_tac ind, auto)
done
thm rec_ci.simps
from g have k2:
"\<exists> stp. abc_steps_l (?gs_len + 3 * length gs, lm @
0\<^bsup>?pstr - n\<^esup> @ ys @ 0\<^bsup>a_md - ?pstr - length ys\<^esup> @ suf_lm) aprog stp =
(?gs_len + 3 * length gs + 3 * n, 0\<^bsup>?pstr\<^esup> @ ys @ 0 # lm @
0\<^bsup>a_md - Suc (?pstr + length ys + n )\<^esup> @ suf_lm)"
thm save_paras
apply(erule_tac ba = c in save_paras, auto intro: ci_cn_para_eq)
done
from g have k3:
"\<exists> stp. abc_steps_l (?gs_len + 3 * length gs + 3 * n,
0\<^bsup>?pstr\<^esup> @ ys @ 0 # lm @ 0\<^bsup>a_md - Suc (?pstr + length ys + n)\<^esup> @ suf_lm) aprog stp =
(?gs_len + 6 * length gs + 3 * n,
ys @ 0\<^bsup>?pstr\<^esup> @ 0 # lm @ 0\<^bsup>a_md - Suc (?pstr + length ys + n)\<^esup> @ suf_lm)"
apply(erule_tac ba = c in reset_new_paras,
auto intro: ci_cn_para_eq)
using para_pattern[of f a b c ys rs]
apply(simp)
done
from g have k4:
"\<exists>stp. abc_steps_l (?gs_len + 6 * length gs + 3 * n,
ys @ 0\<^bsup>?pstr\<^esup> @ 0 # lm @ 0\<^bsup>a_md - Suc (?pstr + length ys + n)\<^esup> @ suf_lm) aprog stp =
(?gs_len + 6 * length gs + 3 * n + length a,
ys @ rs # 0\<^bsup>?pstr \<^esup> @ lm @ 0\<^bsup>a_md - Suc (?pstr + length ys + n)\<^esup> @ suf_lm)"
apply(rule_tac ba = c in calc_cn_f, rule_tac ind, auto)
done
thm rec_ci.simps
from g h have k5:
"\<exists> stp. abc_steps_l (?gs_len + 6 * length gs + 3 * n + length a,
ys @ rs # 0\<^bsup>?pstr \<^esup>@ lm @ 0\<^bsup>a_md - Suc (?pstr + length ys + n)\<^esup> @ suf_lm)
aprog stp =
(?gs_len + 6 * length gs + 3 * n + length a + 3,
ys @ 0\<^bsup>?pstr - length ys\<^esup> @ rs # 0\<^bsup>length ys\<^esup> @ lm @
0\<^bsup>a_md - Suc (?pstr + length ys + n)\<^esup> @ suf_lm)"
apply(rule_tac save_rs, auto simp: h)
done
thm rec_ci.simps
thm empty_boxes.simps
from g have k6:
"\<exists> stp. abc_steps_l (?gs_len + 6 * length gs + 3 * n +
length a + 3, ys @ 0\<^bsup>?pstr - length ys\<^esup> @ rs # 0\<^bsup>length ys\<^esup> @ lm @
0\<^bsup>a_md - Suc (?pstr + length ys + n)\<^esup> @ suf_lm)
aprog stp =
(?gs_len + 8 * length gs + 3 *n + length a + 3,
0\<^bsup>?pstr \<^esup> @ rs # 0\<^bsup>length ys\<^esup> @ lm @
0\<^bsup>a_md -Suc (?pstr + length ys + n)\<^esup> @ suf_lm)"
apply(drule_tac suf_lm = suf_lm in empty_paras, auto)
apply(rule_tac x = stp in exI, simp)
done
from g have k7:
"\<exists> stp. abc_steps_l (?gs_len + 8 * length gs + 3 *n +
length a + 3, 0\<^bsup>?pstr \<^esup> @ rs # 0\<^bsup>length ys\<^esup> @ lm @
0\<^bsup>a_md -Suc (?pstr + length ys + n)\<^esup> @ suf_lm) aprog stp =
(?gs_len + 8 * length gs + 3 * n + length a + 6,
0\<^bsup>n\<^esup> @ rs # 0\<^bsup>?pstr - n\<^esup> @ 0\<^bsup>length ys\<^esup> @ lm @
0\<^bsup>a_md -Suc (?pstr + length ys + n) \<^esup> @ suf_lm)"
apply(drule_tac suf_lm = suf_lm in restore_rs, auto)
apply(rule_tac x = stp in exI, simp)
done
from g have k8: "\<exists> stp. abc_steps_l (?gs_len + 8 * length gs +
3 * n + length a + 6,
0\<^bsup>n\<^esup> @ rs # 0\<^bsup>?pstr - n\<^esup> @ 0\<^bsup>length ys\<^esup> @ lm @
0\<^bsup>a_md -Suc (?pstr + length ys + n) \<^esup> @ suf_lm) aprog stp =
(?gs_len + 8 * length gs + 6 * n + length a + 6,
lm @ rs # 0\<^bsup>a_md - Suc n \<^esup>@ suf_lm)"
apply(drule_tac suf_lm = suf_lm in restore_paras, auto)
apply(simp add: exponent_add_iff)
apply(rule_tac x = stp in exI, simp)
done
from g have j1:
"length aprog = ?gs_len + 8 * length gs + 6 * n + length a + 6"
by(drule_tac a = a and aa = b and ba = c in ci_cn_length,
simp, simp, simp)
from g have j2: "rs_pos = n"
by(simp add: ci_cn_para_eq)
from k1 and k2 and k3 and k4 and k5 and k6 and k7 and k8
and j1 and j2 show
"\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp =
(length aprog, lm @ [rs] @ 0\<^bsup>a_md - rs_pos - 1\<^esup> @ suf_lm)"
apply(auto)
apply(rule_tac x = "stp + stpa + stpb + stpc +
stpd + stpe + stpf + stpg" in exI, simp add: abc_steps_add)
done
qed
text {*
Correctness of the complier (terminate case), which says if the execution of
a recursive function @{text "recf"} terminates and gives result, then
the Abacus program compiled from @{text "recf"} termintes and gives the same result.
Additionally, to facilitate induction proof, we append @{text "anything"} to the
end of Abacus memory.
*}
lemma aba_rec_equality:
"\<lbrakk>rec_ci recf = (ap, arity, fp);
rec_calc_rel recf args r\<rbrakk>
\<Longrightarrow> (\<exists> stp. (abc_steps_l (0, args @ 0\<^bsup>fp - arity\<^esup> @ anything) ap stp) =
(length ap, args@[r]@0\<^bsup>fp - arity - 1\<^esup> @ anything))"
apply(induct arbitrary: ap fp arity r anything args
rule: rec_ci.induct)
prefer 5
proof(case_tac "rec_ci g", case_tac "rec_ci f", simp)
fix n f g ap fp arity r anything args a b c aa ba ca
assume f_ind:
"\<And>ap fp arity r anything args.
\<lbrakk>aa = ap \<and> ba = arity \<and> ca = fp; rec_calc_rel f args r\<rbrakk> \<Longrightarrow>
\<exists>stp. abc_steps_l (0, args @ 0\<^bsup>fp - arity\<^esup> @ anything) ap stp =
(length ap, args @ r # 0\<^bsup>fp - Suc arity\<^esup> @ anything)"
and g_ind:
"\<And>x xa y xb ya ap fp arity r anything args.
\<lbrakk>x = (aa, ba, ca); xa = aa \<and> y = (ba, ca); xb = ba \<and> ya = ca;
a = ap \<and> b = arity \<and> c = fp; rec_calc_rel g args r\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l (0, args @ 0\<^bsup>fp - arity\<^esup> @ anything) ap stp =
(length ap, args @ r # 0\<^bsup>fp - Suc arity\<^esup> @ anything)"
and h: "rec_ci (Pr n f g) = (ap, arity, fp)"
"rec_calc_rel (Pr n f g) args r"
"rec_ci g = (a, b, c)"
"rec_ci f = (aa, ba, ca)"
from h have nf_ind:
"\<And> args r anything. rec_calc_rel f args r \<Longrightarrow>
\<exists>stp. abc_steps_l (0, args @ 0\<^bsup>ca - ba\<^esup> @ anything) aa stp =
(length aa, args @ r # 0\<^bsup>ca - Suc ba\<^esup> @ anything)"
and ng_ind:
"\<And> args r anything. rec_calc_rel g args r \<Longrightarrow>
\<exists>stp. abc_steps_l (0, args @ 0\<^bsup>c - b\<^esup> @ anything) a stp =
(length a, args @ r # 0\<^bsup>c - Suc b \<^esup> @ anything)"
apply(insert f_ind[of aa ba ca], simp)
apply(insert g_ind[of "(aa, ba, ca)" aa "(ba, ca)" ba ca a b c],
simp)
done
from nf_ind and ng_ind and h show
"\<exists>stp. abc_steps_l (0, args @ 0\<^bsup>fp - arity\<^esup> @ anything) ap stp =
(length ap, args @ r # 0\<^bsup>fp - Suc arity\<^esup> @ anything)"
apply(auto intro: nf_ind ng_ind pr_case)
done
next
fix ap fp arity r anything args
assume h:
"rec_ci z = (ap, arity, fp)" "rec_calc_rel z args r"
thus "\<exists>stp. abc_steps_l (0, args @ 0\<^bsup>fp - arity\<^esup> @ anything) ap stp =
(length ap, args @ [r] @ 0\<^bsup>fp - arity - 1\<^esup> @ anything)"
by (rule_tac z_case)
next
fix ap fp arity r anything args
assume h:
"rec_ci s = (ap, arity, fp)"
"rec_calc_rel s args r"
thus
"\<exists>stp. abc_steps_l (0, args @ 0\<^bsup>fp - arity\<^esup> @ anything) ap stp =
(length ap, args @ [r] @ 0\<^bsup>fp - arity - 1\<^esup> @ anything)"
by(erule_tac s_case, simp)
next
fix m n ap fp arity r anything args
assume h: "rec_ci (id m n) = (ap, arity, fp)"
"rec_calc_rel (id m n) args r"
thus "\<exists>stp. abc_steps_l (0, args @ 0\<^bsup>fp - arity\<^esup> @ anything) ap stp
= (length ap, args @ [r] @ 0\<^bsup>fp - arity - 1\<^esup> @ anything)"
by(erule_tac id_case)
next
fix n f gs ap fp arity r anything args
assume ind: "\<And>x ap fp arity r anything args.
\<lbrakk>x \<in> set (f # gs);
rec_ci x = (ap, arity, fp);
rec_calc_rel x args r\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l (0, args @ 0\<^bsup>fp - arity\<^esup> @ anything) ap stp =
(length ap, args @ [r] @ 0\<^bsup>fp - arity - 1\<^esup> @ anything)"
and h: "rec_ci (Cn n f gs) = (ap, arity, fp)"
"rec_calc_rel (Cn n f gs) args r"
from h show
"\<exists>stp. abc_steps_l (0, args @ 0\<^bsup>fp - arity\<^esup> @ anything)
ap stp = (length ap, args @ [r] @ 0\<^bsup>fp - arity - 1\<^esup> @ anything)"
apply(rule_tac cn_case, rule_tac ind, auto)
done
next
fix n f ap fp arity r anything args
assume ind:
"\<And>ap fp arity r anything args.
\<lbrakk>rec_ci f = (ap, arity, fp); rec_calc_rel f args r\<rbrakk> \<Longrightarrow>
\<exists>stp. abc_steps_l (0, args @ 0\<^bsup>fp - arity\<^esup> @ anything) ap stp =
(length ap, args @ [r] @ 0\<^bsup>fp - arity - 1\<^esup> @ anything)"
and h: "rec_ci (Mn n f) = (ap, arity, fp)"
"rec_calc_rel (Mn n f) args r"
from h show
"\<exists>stp. abc_steps_l (0, args @ 0\<^bsup>fp - arity\<^esup> @ anything) ap stp =
(length ap, args @ [r] @ 0\<^bsup>fp - arity - 1\<^esup> @ anything)"
apply(rule_tac mn_case, rule_tac ind, auto)
done
qed
thm abc_append_state_in_exc
lemma abc_append_uhalt1:
"\<lbrakk>\<forall> stp. (\<lambda> (ss, e). ss < length bp) (abc_steps_l (0, lm) bp stp);
p = ap [+] bp [+] cp\<rbrakk>
\<Longrightarrow> \<forall> stp. (\<lambda> (ss, e). ss < length p)
(abc_steps_l (length ap, lm) p stp)"
apply(auto)
apply(erule_tac x = stp in allE, auto)
apply(frule_tac ap = ap and cp = cp in abc_append_state_in_exc, auto)
done
lemma abc_append_unhalt2:
"\<lbrakk>abc_steps_l (0, am) ap stp = (length ap, lm); bp \<noteq> [];
\<forall> stp. (\<lambda> (ss, e). ss < length bp) (abc_steps_l (0, lm) bp stp);
p = ap [+] bp [+] cp\<rbrakk>
\<Longrightarrow> \<forall> stp. (\<lambda> (ss, e). ss < length p) (abc_steps_l (0, am) p stp)"
proof -
assume h:
"abc_steps_l (0, am) ap stp = (length ap, lm)"
"bp \<noteq> []"
"\<forall> stp. (\<lambda> (ss, e). ss < length bp) (abc_steps_l (0, lm) bp stp)"
"p = ap [+] bp [+] cp"
have "\<exists> stp. (abc_steps_l (0, am) p stp) = (length ap, lm)"
using h
thm abc_add_exc1
apply(simp add: abc_append.simps)
apply(rule_tac abc_add_exc1, auto)
done
from this obtain stpa where g1:
"(abc_steps_l (0, am) p stpa) = (length ap, lm)" ..
moreover have g2: "\<forall> stp. (\<lambda> (ss, e). ss < length p)
(abc_steps_l (length ap, lm) p stp)"
using h
apply(erule_tac abc_append_uhalt1, simp)
done
moreover from g1 and g2 have
"\<forall> stp. (\<lambda> (ss, e). ss < length p)
(abc_steps_l (0, am) p (stpa + stp))"
apply(simp add: abc_steps_add)
done
thus "\<forall> stp. (\<lambda> (ss, e). ss < length p)
(abc_steps_l (0, am) p stp)"
apply(rule_tac allI, auto)
apply(case_tac "stp \<ge> stpa")
apply(erule_tac x = "stp - stpa" in allE, simp)
proof -
fix stp a b
assume g3: "abc_steps_l (0, am) p stp = (a, b)"
"\<not> stpa \<le> stp"
thus "a < length p"
using g1 h
apply(case_tac "a < length p", simp, simp)
apply(subgoal_tac "\<exists> d. stpa = stp + d")
using abc_state_keep[of p a b "stpa - stp"]
apply(erule_tac exE, simp add: abc_steps_add)
apply(rule_tac x = "stpa - stp" in exI, simp)
done
qed
qed
text {*
Correctness of the complier (non-terminating case for Mn). There are many cases when a
recursive function does not terminate. For the purpose of Uiversal Turing Machine, we only
need to prove the case for @{text "Mn"} and @{text "Cn"}.
This lemma is for @{text "Mn"}. For @{text "Mn n f"}, this lemma describes what
happens when @{text "f"} always terminates but always does not return zero, so that
@{text "Mn"} has to loop forever.
*}
lemma Mn_unhalt:
assumes mn_rf: "rf = Mn n f"
and compiled_mnrf: "rec_ci rf = (aprog, rs_pos, a_md)"
and compiled_f: "rec_ci f = (aprog', rs_pos', a_md')"
and args: "length lm = n"
and unhalt_condition: "\<forall> y. (\<exists> rs. rec_calc_rel f (lm @ [y]) rs \<and> rs \<noteq> 0)"
shows "\<forall> stp. case abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm)
aprog stp of (ss, e) \<Rightarrow> ss < length aprog"
using mn_rf compiled_mnrf compiled_f args unhalt_condition
proof(rule_tac allI)
fix stp
assume h: "rf = Mn n f"
"rec_ci rf = (aprog, rs_pos, a_md)"
"rec_ci f = (aprog', rs_pos', a_md')"
"\<forall>y. \<exists>rs. rec_calc_rel f (lm @ [y]) rs \<and> rs \<noteq> 0" "length lm = n"
thm mn_ind_step
have "\<exists>stpa \<ge> stp. abc_steps_l (0, lm @ 0 # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm) aprog stpa
= (0, lm @ stp # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)"
proof(induct stp, auto)
show "\<exists>stpa. abc_steps_l (0, lm @ 0 # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)
aprog stpa = (0, lm @ 0 # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)"
apply(rule_tac x = 0 in exI, simp add: abc_steps_l.simps)
done
next
fix stp stpa
assume g1: "stp \<le> stpa"
and g2: "abc_steps_l (0, lm @ 0 # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)
aprog stpa
= (0, lm @ stp # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)"
have "\<exists>rs. rec_calc_rel f (lm @ [stp]) rs \<and> rs \<noteq> 0"
using h
apply(erule_tac x = stp in allE, simp)
done
from this obtain rs where g3:
"rec_calc_rel f (lm @ [stp]) rs \<and> rs \<noteq> 0" ..
hence "\<exists> stpb. abc_steps_l (0, lm @ stp # 0\<^bsup>a_md - Suc rs_pos\<^esup> @
suf_lm) aprog stpb
= (0, lm @ Suc stp # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)"
using h
apply(rule_tac mn_ind_step)
apply(rule_tac aba_rec_equality, simp, simp)
proof -
show "rec_ci f = ((aprog', rs_pos', a_md'))" using h by simp
next
show "rec_ci (Mn n f) = (aprog, rs_pos, a_md)" using h by simp
next
show "rec_calc_rel f (lm @ [stp]) rs" using g3 by simp
next
show "0 < rs" using g3 by simp
next
show "Suc rs_pos < a_md"
using g3 h
apply(auto)
apply(frule_tac f = f in para_pattern, simp, simp)
apply(simp add: rec_ci.simps, auto)
apply(subgoal_tac "Suc (length lm) < a_md'")
apply(arith)
apply(simp add: ci_ad_ge_paras)
done
next
show "rs_pos' = Suc rs_pos"
using g3 h
apply(auto)
apply(frule_tac f = f in para_pattern, simp, simp)
apply(simp add: rec_ci.simps)
done
qed
thus "\<exists>stpa\<ge>Suc stp. abc_steps_l (0, lm @ 0 # 0\<^bsup>a_md - Suc rs_pos\<^esup> @
suf_lm) aprog stpa
= (0, lm @ Suc stp # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)"
using g2
apply(erule_tac exE)
apply(case_tac "stpb = 0", simp add: abc_steps_l.simps)
apply(rule_tac x = "stpa + stpb" in exI, simp add:
abc_steps_add)
using g1
apply(arith)
done
qed
from this obtain stpa where
"stp \<le> stpa \<and> abc_steps_l (0, lm @ 0 # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)
aprog stpa = (0, lm @ stp # 0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm)" ..
thus "case abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp
of (ss, e) \<Rightarrow> ss < length aprog"
apply(case_tac "abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog
stp", simp, case_tac "a \<ge> length aprog",
simp, simp)
apply(subgoal_tac "\<exists> d. stpa = stp + d", erule_tac exE)
apply(subgoal_tac "lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm = lm @ 0 #
0\<^bsup>a_md - Suc rs_pos\<^esup> @ suf_lm", simp add: abc_steps_add)
apply(frule_tac as = a and lm = b and stp = d in abc_state_keep,
simp)
using h
apply(simp add: rec_ci.simps, simp,
simp only: exp_ind_def[THEN sym])
apply(case_tac rs_pos, simp, simp)
apply(rule_tac x = "stpa - stp" in exI, simp, simp)
done
qed
lemma abc_append_cons_eq[intro!]:
"\<lbrakk>ap = bp; cp = dp\<rbrakk> \<Longrightarrow> ap [+] cp = bp [+] dp"
by simp
lemma cn_merge_gs_split:
"\<lbrakk>i < length gs; rec_ci (gs!i) = (ga, gb, gc)\<rbrakk> \<Longrightarrow>
cn_merge_gs (map rec_ci gs) p =
cn_merge_gs (map rec_ci (take i gs)) p [+] ga [+]
empty gb (p + i) [+]
cn_merge_gs (map rec_ci (drop (Suc i) gs)) (p + Suc i)"
apply(induct i arbitrary: gs p, case_tac gs, simp, simp)
apply(case_tac gs, simp, case_tac "rec_ci a",
simp add: abc_append_commute[THEN sym])
done
text {*
Correctness of the complier (non-terminating case for Mn). There are many cases when a
recursive function does not terminate. For the purpose of Uiversal Turing Machine, we only
need to prove the case for @{text "Mn"} and @{text "Cn"}.
This lemma is for @{text "Cn"}. For @{text "Cn f g1 g2 \<dots>gi, gi+1, \<dots> gn"}, this lemma describes what
happens when every one of @{text "g1, g2, \<dots> gi"} terminates, but
@{text "gi+1"} does not terminate, so that whole function @{text "Cn f g1 g2 \<dots>gi, gi+1, \<dots> gn"}
does not terminate.
*}
lemma cn_gi_uhalt:
assumes cn_recf: "rf = Cn n f gs"
and compiled_cn_recf: "rec_ci rf = (aprog, rs_pos, a_md)"
and args_length: "length lm = n"
and exist_unhalt_recf: "i < length gs" "gi = gs ! i"
and complied_unhalt_recf: "rec_ci gi = (ga, gb, gc)" "gb = n"
and all_halt_before_gi: "\<forall> j < i. (\<exists> rs. rec_calc_rel (gs!j) lm rs)"
and unhalt_condition: "\<And> slm. \<forall> stp. case abc_steps_l (0, lm @ 0\<^bsup>gc - gb\<^esup> @ slm)
ga stp of (se, e) \<Rightarrow> se < length ga"
shows " \<forall> stp. case abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suflm) aprog
stp of (ss, e) \<Rightarrow> ss < length aprog"
using cn_recf compiled_cn_recf args_length exist_unhalt_recf complied_unhalt_recf
all_halt_before_gi unhalt_condition
proof(case_tac "rec_ci f", simp)
fix a b c
assume h1: "rf = Cn n f gs"
"rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)"
"length lm = n"
"gi = gs ! i"
"rec_ci (gs!i) = (ga, n, gc)"
"gb = n" "rec_ci f = (a, b, c)"
and h2: "\<forall>j<i. \<exists>rs. rec_calc_rel (gs ! j) lm rs"
"i < length gs"
and ind:
"\<And> slm. \<forall> stp. case abc_steps_l (0, lm @ 0\<^bsup>gc - n\<^esup> @ slm) ga stp of (se, e) \<Rightarrow> se < length ga"
have h3: "rs_pos = n"
using h1
by(rule_tac ci_cn_para_eq, simp)
let ?ggs = "take i gs"
have "\<exists> ys. (length ys = i \<and>
(\<forall> k < i. rec_calc_rel (?ggs ! k) lm (ys ! k)))"
using h2
apply(induct i, simp, simp)
apply(erule_tac exE)
apply(erule_tac x = ia in allE, simp)
apply(erule_tac exE)
apply(rule_tac x = "ys @ [x]" in exI, simp add: nth_append, auto)
apply(subgoal_tac "k = length ys", simp, simp)
done
from this obtain ys where g1:
"(length ys = i \<and> (\<forall> k < i. rec_calc_rel (?ggs ! k)
lm (ys ! k)))" ..
let ?pstr = "Max (set (Suc n # c # map (\<lambda>(aprog, p, n). n)
(map rec_ci (f # gs))))"
have "\<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - n\<^esup> @ suflm)
(cn_merge_gs (map rec_ci ?ggs) ?pstr) stp =
(listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) ?ggs) +
3 * length ?ggs, lm @ 0\<^bsup>?pstr - n\<^esup> @ ys @ 0\<^bsup>a_md -(?pstr + length ?ggs)\<^esup> @
suflm) "
apply(rule_tac cn_merge_gs_ex)
apply(rule_tac aba_rec_equality, simp, simp)
using h1
apply(simp add: rec_ci.simps, auto)
using g1
apply(simp)
using h2 g1
apply(simp)
apply(rule_tac min_max.le_supI2)
apply(rule_tac Max_ge, simp, simp, rule_tac disjI2)
apply(subgoal_tac "aa \<in> set gs", simp)
using h2
apply(rule_tac A = "set (take i gs)" in subsetD,
simp add: set_take_subset, simp)
done
thm cn_merge_gs.simps
from this obtain stpa where g2:
"abc_steps_l (0, lm @ 0\<^bsup>a_md - n\<^esup> @ suflm)
(cn_merge_gs (map rec_ci ?ggs) ?pstr) stpa =
(listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) ?ggs) +
3 * length ?ggs, lm @ 0\<^bsup>?pstr - n\<^esup> @ ys @ 0\<^bsup>a_md -(?pstr + length ?ggs)\<^esup> @
suflm)" ..
moreover have
"\<exists> cp. aprog = (cn_merge_gs
(map rec_ci ?ggs) ?pstr) [+] ga [+] cp"
using h1
apply(simp add: rec_ci.simps)
apply(rule_tac x = "empty n (?pstr + i) [+]
(cn_merge_gs (map rec_ci (drop (Suc i) gs)) (?pstr + Suc i))
[+]mv_boxes 0 (Suc (max (Suc n) (Max (insert c
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) +
length gs)) n [+] mv_boxes (max (Suc n) (Max (insert c
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+]
a [+] recursive.empty b (max (Suc n)
(Max (insert c (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
empty_boxes (length gs) [+] recursive.empty (max (Suc n)
(Max (insert c (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
mv_boxes (Suc (max (Suc n) (Max (insert c
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI)
apply(simp add: abc_append_commute [THEN sym])
apply(auto)
using cn_merge_gs_split[of i gs ga "length lm" gc
"(max (Suc (length lm))
(Max (insert c (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))))"]
h2
apply(simp)
done
from this obtain cp where g3:
"aprog = (cn_merge_gs (map rec_ci ?ggs) ?pstr) [+] ga [+] cp" ..
show "\<forall> stp. case abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suflm)
aprog stp of (ss, e) \<Rightarrow> ss < length aprog"
proof(rule_tac abc_append_unhalt2)
show "abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suflm) (
cn_merge_gs (map rec_ci ?ggs) ?pstr) stpa =
(length ((cn_merge_gs (map rec_ci ?ggs) ?pstr)),
lm @ 0\<^bsup>?pstr - n\<^esup> @ ys @ 0\<^bsup>a_md -(?pstr + length ?ggs)\<^esup> @ suflm)"
using h3 g2
apply(simp add: cn_merge_gs_length)
done
next
show "ga \<noteq> []"
using h1
apply(simp add: rec_ci_not_null)
done
next
show "\<forall>stp. case abc_steps_l (0, lm @ 0\<^bsup>?pstr - n\<^esup> @ ys
@ 0\<^bsup>a_md - (?pstr + length (take i gs))\<^esup> @ suflm) ga stp of
(ss, e) \<Rightarrow> ss < length ga"
using ind[of "0\<^bsup>?pstr -gc\<^esup> @ ys @ 0\<^bsup>a_md - (?pstr + length (take i gs))\<^esup>
@ suflm"]
apply(subgoal_tac "lm @ 0\<^bsup>?pstr - n\<^esup> @ ys
@ 0\<^bsup>a_md - (?pstr + length (take i gs))\<^esup> @ suflm
= lm @ 0\<^bsup>gc - n \<^esup>@
0\<^bsup>?pstr -gc\<^esup> @ ys @ 0\<^bsup>a_md - (?pstr + length (take i gs))\<^esup> @ suflm", simp)
apply(simp add: exponent_def replicate_add[THEN sym])
apply(subgoal_tac "gc > n \<and> ?pstr \<ge> gc")
apply(erule_tac conjE)
apply(simp add: h1)
using h1
apply(auto)
apply(rule_tac min_max.le_supI2)
apply(rule_tac Max_ge, simp, simp)
apply(rule_tac disjI2)
using h2
thm rev_image_eqI
apply(rule_tac x = "gs!i" in rev_image_eqI, simp, simp)
done
next
show "aprog = cn_merge_gs (map rec_ci (take i gs))
?pstr [+] ga [+] cp"
using g3 by simp
qed
qed
lemma abc_rec_halt_eq':
"\<lbrakk>rec_ci re = (ap, ary, fp);
rec_calc_rel re args r\<rbrakk>
\<Longrightarrow> (\<exists> stp. (abc_steps_l (0, args @ 0\<^bsup>fp - ary\<^esup>) ap stp) =
(length ap, args@[r]@0\<^bsup>fp - ary - 1\<^esup>))"
using aba_rec_equality[of re ap ary fp args r "[]"]
by simp
thm abc_step_l.simps
definition dummy_abc :: "nat \<Rightarrow> abc_inst list"
where
"dummy_abc k = [Inc k, Dec k 0, Goto 3]"
lemma abc_rec_halt_eq'':
"\<lbrakk>rec_ci re = (aprog, rs_pos, a_md);
rec_calc_rel re lm rs\<rbrakk>
\<Longrightarrow> (\<exists> stp lm' m. (abc_steps_l (0, lm) aprog stp) =
(length aprog, lm') \<and> abc_list_crsp lm' (lm @ rs # 0\<^bsup>m\<^esup>))"
apply(frule_tac abc_rec_halt_eq', auto)
apply(drule_tac abc_list_crsp_steps)
apply(rule_tac rec_ci_not_null, simp)
apply(erule_tac exE, rule_tac x = stp in exI,
auto simp: abc_list_crsp_def)
done
lemma [simp]: "length (dummy_abc (length lm)) = 3"
apply(simp add: dummy_abc_def)
done
lemma [simp]: "dummy_abc (length lm) \<noteq> []"
apply(simp add: dummy_abc_def)
done
lemma dummy_abc_steps_ex:
"\<exists>bstp. abc_steps_l (0, lm') (dummy_abc (length lm)) bstp =
((Suc (Suc (Suc 0))), abc_lm_s lm' (length lm) (abc_lm_v lm' (length lm)))"
apply(rule_tac x = "Suc (Suc (Suc 0))" in exI)
apply(auto simp: abc_steps_l.simps abc_step_l.simps
dummy_abc_def abc_fetch.simps)
apply(auto simp: abc_lm_s.simps abc_lm_v.simps nth_append)
apply(simp add: butlast_append)
done
lemma [elim]:
"lm @ rs # 0\<^bsup>m\<^esup> = lm' @ 0\<^bsup>n\<^esup> \<Longrightarrow>
\<exists>m. abc_lm_s lm' (length lm) (abc_lm_v lm' (length lm)) =
lm @ rs # 0\<^bsup>m\<^esup>"
proof(cases "length lm' > length lm")
case True
assume h: "lm @ rs # 0\<^bsup>m\<^esup> = lm' @ 0\<^bsup>n\<^esup>" "length lm < length lm'"
hence "m \<ge> n"
apply(drule_tac list_length)
apply(simp)
done
hence "\<exists> d. m = d + n"
apply(rule_tac x = "m - n" in exI, simp)
done
from this obtain d where "m = d + n" ..
from h and this show "?thesis"
apply(auto simp: abc_lm_s.simps abc_lm_v.simps
exponent_def replicate_add)
done
next
case False
assume h:"lm @ rs # 0\<^bsup>m\<^esup> = lm' @ 0\<^bsup>n\<^esup>"
and g: "\<not> length lm < length lm'"
have "take (Suc (length lm)) (lm @ rs # 0\<^bsup>m\<^esup>) =
take (Suc (length lm)) (lm' @ 0\<^bsup>n\<^esup>)"
using h by simp
moreover have "n \<ge> (Suc (length lm) - length lm')"
using h g
apply(drule_tac list_length)
apply(simp)
done
ultimately show
"\<exists>m. abc_lm_s lm' (length lm) (abc_lm_v lm' (length lm)) =
lm @ rs # 0\<^bsup>m\<^esup>"
using g h
apply(simp add: abc_lm_s.simps abc_lm_v.simps
exponent_def min_def)
apply(rule_tac x = 0 in exI,
simp add:replicate_append_same replicate_Suc[THEN sym]
del:replicate_Suc)
done
qed
lemma [elim]:
"abc_list_crsp lm' (lm @ rs # 0\<^bsup>m\<^esup>)
\<Longrightarrow> \<exists>m. abc_lm_s lm' (length lm) (abc_lm_v lm' (length lm))
= lm @ rs # 0\<^bsup>m\<^esup>"
apply(auto simp: abc_list_crsp_def)
apply(simp add: abc_lm_v.simps abc_lm_s.simps)
apply(rule_tac x = "m + n" in exI,
simp add: exponent_def replicate_add)
done
lemma abc_append_dummy_complie:
"\<lbrakk>rec_ci recf = (ap, ary, fp);
rec_calc_rel recf args r;
length args = k\<rbrakk>
\<Longrightarrow> (\<exists> stp m. (abc_steps_l (0, args) (ap [+] dummy_abc k) stp) =
(length ap + 3, args @ r # 0\<^bsup>m\<^esup>))"
apply(drule_tac abc_rec_halt_eq'', auto simp: numeral_3_eq_3)
proof -
fix stp lm' m
assume h: "rec_calc_rel recf args r"
"abc_steps_l (0, args) ap stp = (length ap, lm')"
"abc_list_crsp lm' (args @ r # 0\<^bsup>m\<^esup>)"
thm abc_append_exc2
thm abc_lm_s.simps
have "\<exists>stp. abc_steps_l (0, args) (ap [+]
(dummy_abc (length args))) stp = (length ap + 3,
abc_lm_s lm' (length args) (abc_lm_v lm' (length args)))"
using h
apply(rule_tac bm = lm' in abc_append_exc2,
auto intro: dummy_abc_steps_ex simp: numeral_3_eq_3)
done
thus "\<exists>stp m. abc_steps_l (0, args) (ap [+]
dummy_abc (length args)) stp = (Suc (Suc (Suc (length ap))), args @ r # 0\<^bsup>m\<^esup>)"
using h
apply(erule_tac exE)
apply(rule_tac x = stpa in exI, auto)
done
qed
lemma [simp]: "length (dummy_abc k) = 3"
apply(simp add: dummy_abc_def)
done
lemma [simp]: "length args = k \<Longrightarrow> abc_lm_v (args @ r # 0\<^bsup>m\<^esup>) k = r "
apply(simp add: abc_lm_v.simps nth_append)
done
lemma t_compiled_by_rec:
"\<lbrakk>rec_ci recf = (ap, ary, fp);
rec_calc_rel recf args r;
length args = k;
ly = layout_of (ap [+] dummy_abc k);
mop_ss = start_of ly (length (ap [+] dummy_abc k));
tp = tm_of (ap [+] dummy_abc k)\<rbrakk>
\<Longrightarrow> \<exists> stp m l. steps (Suc 0, Bk # Bk # ires, <args> @ Bk\<^bsup>rn\<^esup>) (tp @ (tMp k (mop_ss - 1))) stp
= (0, Bk\<^bsup>m\<^esup> @ Bk # Bk # ires, Oc\<^bsup>Suc r\<^esup> @ Bk\<^bsup>l\<^esup>)"
using abc_append_dummy_complie[of recf ap ary fp args r k]
apply(simp)
apply(erule_tac exE)+
apply(frule_tac tprog = tp and as = "length ap + 3" and n = k
and ires = ires and rn = rn in abacus_turing_eq_halt, simp_all, simp)
apply(erule_tac exE)+
apply(simp)
apply(rule_tac x = stpa in exI, rule_tac x = ma in exI, rule_tac x = l in exI, simp)
done
thm tms_of.simps
lemma [simp]:
"list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))) xs \<Longrightarrow>
list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))))) xs"
apply(induct xs, simp, simp)
apply(case_tac a, simp)
done
(*
lemma [simp]: "t_correct (tMp n 0)"
apply(simp add: t_correct.simps tMp.simps shift_length mp_up_def iseven_def, auto)
apply(rule_tac x = "2*n + 6" in exI, simp)
apply(induct n, auto simp: mop_bef.simps)
apply(simp add: tshift.simps)
done
*)
lemma tshift_append: "tshift (xs @ ys) n = tshift xs n @ tshift ys n"
apply(simp add: tshift.simps)
done
lemma [simp]: "length (tMp n ss) = 4 * n + 12"
apply(auto simp: tMp.simps tshift_append shift_length mp_up_def)
done
lemma length_tm_even[intro]: "\<exists>x. length (tm_of ap) = 2*x"
apply(subgoal_tac "t_ncorrect (tm_of ap)")
apply(simp add: t_ncorrect.simps, auto)
done
lemma [simp]: "k < length ap \<Longrightarrow> tms_of ap ! k =
ci (layout_of ap) (start_of (layout_of ap) k) (ap ! k)"
apply(simp add: tms_of.simps tpairs_of.simps)
done
lemma [elim]: "\<lbrakk>k < length ap; ap ! k = Inc n;
(a, b) \<in> set (abacus.tshift (abacus.tshift tinc_b (2 * n))
(start_of (layout_of ap) k - Suc 0))\<rbrakk>
\<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)"
apply(subgoal_tac "b \<le> start_of (layout_of ap) (Suc k)")
apply(subgoal_tac "start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap) ")
apply(arith)
apply(case_tac "Suc k = length ap", simp)
apply(rule_tac start_of_le, simp)
apply(auto simp: tinc_b_def tshift.simps start_of.simps
layout_of.simps length_of.simps startof_not0)
done
lemma findnth_le[elim]: "(a, b) \<in> set (abacus.tshift (findnth n) (start_of (layout_of ap) k - Suc 0))
\<Longrightarrow> b \<le> Suc (start_of (layout_of ap) k + 2 * n)"
apply(induct n, simp add: findnth.simps tshift.simps)
apply(simp add: findnth.simps tshift_append, auto)
apply(auto simp: tshift.simps)
done
lemma [elim]: "\<lbrakk>k < length ap; ap ! k = Inc n; (a, b) \<in>
set (abacus.tshift (findnth n) (start_of (layout_of ap) k - Suc 0))\<rbrakk>
\<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)"
apply(subgoal_tac "b \<le> start_of (layout_of ap) (Suc k)")
apply(subgoal_tac "start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap) ")
apply(arith)
apply(case_tac "Suc k = length ap", simp)
apply(rule_tac start_of_le, simp)
apply(subgoal_tac "b \<le> start_of (layout_of ap) k + 2*n + 1 \<and>
start_of (layout_of ap) k + 2*n + 1 \<le> start_of (layout_of ap) (Suc k)", auto)
apply(auto simp: tinc_b_def tshift.simps start_of.simps
layout_of.simps length_of.simps startof_not0)
done
lemma start_of_eq: "length ap < as \<Longrightarrow> start_of (layout_of ap) as = start_of (layout_of ap) (length ap)"
apply(induct as, simp)
apply(case_tac "length ap < as", simp add: start_of.simps)
apply(subgoal_tac "as = length ap")
apply(simp add: start_of.simps)
apply arith
done
lemma start_of_all_le: "start_of (layout_of ap) as \<le> start_of (layout_of ap) (length ap)"
apply(subgoal_tac "as > length ap \<or> as = length ap \<or> as < length ap",
auto simp: start_of_eq start_of_le)
done
lemma [elim]: "\<lbrakk>k < length ap;
ap ! k = Dec n e;
(a, b) \<in> set (abacus.tshift (findnth n) (start_of (layout_of ap) k - Suc 0))\<rbrakk>
\<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)"
apply(subgoal_tac "b \<le> start_of (layout_of ap) k + 2*n + 1 \<and>
start_of (layout_of ap) k + 2*n + 1 \<le> start_of (layout_of ap) (Suc k) \<and>
start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap)", auto)
apply(simp add: tshift.simps start_of.simps
layout_of.simps length_of.simps startof_not0)
apply(rule_tac start_of_all_le)
done
thm length_of.simps
lemma [elim]: "\<lbrakk>k < length ap; ap ! k = Dec n e; (a, b) \<in> set (abacus.tshift (abacus.tshift tdec_b (2 * n))
(start_of (layout_of ap) k - Suc 0))\<rbrakk>
\<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)"
apply(subgoal_tac "2*n + start_of (layout_of ap) k + 16 \<le> start_of (layout_of ap) (length ap) \<and> start_of (layout_of ap) k > 0")
prefer 2
apply(subgoal_tac "2 * n + start_of (layout_of ap) k + 16 = start_of (layout_of ap) (Suc k)
\<and> start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap)")
apply(simp add: startof_not0, rule_tac conjI)
apply(simp add: start_of.simps layout_of.simps length_of.simps)
apply(rule_tac start_of_all_le)
apply(auto simp: tdec_b_def tshift.simps)
done
lemma tms_any_less: "\<lbrakk>k < length ap; (a, b) \<in> set (tms_of ap ! k)\<rbrakk> \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)"
apply(simp)
apply(case_tac "ap!k", simp_all add: ci.simps tshift_append, auto intro: start_of_all_le)
done
lemma concat_in: "i < length (concat xs) \<Longrightarrow> \<exists>k < length xs. concat xs ! i \<in> set (xs ! k)"
apply(induct xs rule: list_tl_induct, simp, simp)
apply(case_tac "i < length (concat list)", simp)
apply(erule_tac exE, rule_tac x = k in exI)
apply(simp add: nth_append)
apply(rule_tac x = "length list" in exI, simp)
apply(simp add: nth_append)
done
lemma [simp]: "length (tms_of ap) = length ap"
apply(simp add: tms_of.simps tpairs_of.simps)
done
lemma in_tms: "i < length (tm_of ap) \<Longrightarrow> \<exists> k < length ap. (tm_of ap ! i) \<in> set (tms_of ap ! k)"
apply(simp add: tm_of.simps)
using concat_in[of i "tms_of ap"]
by simp
lemma all_le_start_of: "list_all (\<lambda>(acn, s). s \<le> start_of (layout_of ap) (length ap)) (tm_of ap)"
apply(simp add: list_all_length)
apply(rule_tac allI, rule_tac impI)
apply(drule_tac in_tms, auto elim: tms_any_less)
done
lemma length_ci: "\<lbrakk>k < length ap; length (ci ly y (ap ! k)) = 2 * qa\<rbrakk>
\<Longrightarrow> layout_of ap ! k = qa"
apply(case_tac "ap ! k")
apply(auto simp: layout_of.simps ci.simps
length_of.simps shift_length tinc_b_def tdec_b_def)
done
lemma [intro]: "length (ci ly y i) mod 2 = 0"
apply(auto simp: ci.simps shift_length tinc_b_def tdec_b_def
split: abc_inst.splits)
done
lemma [intro]: "listsum (map (length \<circ> (\<lambda>(x, y). ci ly x y)) zs) mod 2 = 0"
apply(induct zs rule: list_tl_induct, simp)
apply(case_tac a, simp)
apply(subgoal_tac "length (ci ly aa b) mod 2 = 0")
apply(auto)
done
lemma zip_pre:
"(length ys) \<le> length ap \<Longrightarrow>
zip ys ap = zip ys (take (length ys) (ap::'a list))"
proof(induct ys arbitrary: ap, simp, case_tac ap, simp)
fix a ys ap aa list
assume ind: "\<And>(ap::'a list). length ys \<le> length ap \<Longrightarrow>
zip ys ap = zip ys (take (length ys) ap)"
and h: "length (a # ys) \<le> length ap" "(ap::'a list) = aa # (list::'a list)"
from h show "zip (a # ys) ap = zip (a # ys) (take (length (a # ys)) ap)"
using ind[of list]
apply(simp)
done
qed
lemma start_of_listsum:
"\<lbrakk>k \<le> length ap; length ss = k\<rbrakk> \<Longrightarrow> start_of (layout_of ap) k =
Suc (listsum (map (length \<circ> (\<lambda>(x, y). ci ly x y)) (zip ss ap)) div 2)"
proof(induct k arbitrary: ss, simp add: start_of.simps, simp)
fix k ss
assume ind: "\<And>ss. length ss = k \<Longrightarrow> start_of (layout_of ap) k =
Suc (listsum (map (length \<circ> (\<lambda>(x, y). ci ly x y)) (zip ss ap)) div 2)"
and h: "Suc k \<le> length ap" "length (ss::nat list) = Suc k"
have "\<exists> ys y. ss = ys @ [y]"
using h
apply(rule_tac x = "butlast ss" in exI,
rule_tac x = "last ss" in exI)
apply(case_tac "ss = []", auto)
done
from this obtain ys y where k1: "ss = (ys::nat list) @ [y]"
by blast
from h and this have k2:
"start_of (layout_of ap) k =
Suc (listsum (map (length \<circ> (\<lambda>(x, y). ci ly x y)) (zip ys ap)) div 2)"
apply(rule_tac ind, simp)
done
have k3: "zip ys ap = zip ys (take k ap)"
using zip_pre[of ys ap] k1 h
apply(simp)
done
have k4: "(zip [y] (drop (length ys) ap)) = [(y, ap ! length ys)]"
using k1 h
apply(case_tac "drop (length ys) ap", simp)
apply(subgoal_tac "hd (drop (length ys) ap) = ap ! length ys")
apply(simp)
apply(rule_tac hd_drop_conv_nth, simp)
done
from k1 and h k2 k3 k4 show "start_of (layout_of ap) (Suc k) =
Suc (listsum (map (length \<circ> (\<lambda>(x, y). ci ly x y)) (zip ss ap)) div 2)"
apply(simp add: zip_append1 start_of.simps)
apply(subgoal_tac
"listsum (map (length \<circ> (\<lambda>(x, y). ci ly x y)) (zip ys (take k ap))) mod 2 = 0 \<and>
length (ci ly y (ap!k)) mod 2 = 0")
apply(auto)
apply(rule_tac length_ci, simp, simp)
done
qed
lemma length_start_of_tm: "start_of (layout_of ap) (length ap) = Suc (length (tm_of ap) div 2)"
apply(simp add: tm_of.simps length_concat tms_of.simps tpairs_of.simps)
apply(rule_tac start_of_listsum, simp, simp)
done
lemma tm_even: "length (tm_of ap) mod 2 = 0"
apply(subgoal_tac "t_ncorrect (tm_of ap)", auto)
apply(simp add: t_ncorrect.simps)
done
lemma [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
lemma [simp]: "length mp_up = 12"
apply(simp add: mp_up_def)
done
lemma [elim]: "\<lbrakk>na < 4 * n; tshift (mop_bef n) q ! na = (a, b)\<rbrakk> \<Longrightarrow> b \<le> q + (2 * n + 6)"
apply(induct n, simp, simp add: mop_bef.simps nth_append tshift_append shift_length)
apply(case_tac "na < 4*n", simp, simp)
apply(subgoal_tac "na = 4*n \<or> na = 1 + 4*n \<or> na = 2 + 4*n \<or> na = 3 + 4*n",
auto simp: shift_length)
apply(simp_all add: tshift.simps)
done
lemma mp_up_all_le: "list_all (\<lambda>(acn, s). s \<le> q + (2 * n + 6))
[(R, Suc (Suc (2 * n + q))), (R, Suc (2 * n + q)),
(L, 5 + 2 * n + q), (W0, Suc (Suc (Suc (2 * n + q)))), (R, 4 + 2 * n + q),
(W0, Suc (Suc (Suc (2 * n + q)))), (R, Suc (Suc (2 * n + q))),
(W0, Suc (Suc (Suc (2 * n + q)))), (L, 5 + 2 * n + q),
(L, 6 + 2 * n + q), (R, 0), (L, 6 + 2 * n + q)]"
apply(auto)
done
lemma [intro]: "list_all (\<lambda>(acn, s). s \<le> q + (2 * n + 6)) (tMp n q)"
apply(auto simp: list_all_length tMp.simps tshift_append nth_append shift_length)
apply(auto simp: tshift.simps mp_up_def)
apply(subgoal_tac "na - 4*n \<ge> 0 \<and> na - 4 *n < 12", auto split: nat.splits)
apply(insert mp_up_all_le[of q n])
apply(simp add: list_all_length)
apply(erule_tac x = "na - 4 * n" in allE, simp add: numeral_3_eq_3)
done
lemma t_compiled_correct:
"\<lbrakk>tp = tm_of ap; ly = layout_of ap; mop_ss = start_of ly (length ap)\<rbrakk> \<Longrightarrow>
t_correct (tp @ tMp n (mop_ss - Suc 0))"
using tm_even[of ap] length_start_of_tm[of ap] all_le_start_of[of ap]
apply(auto simp: t_correct.simps iseven_def)
apply(rule_tac x = "q + 2*n + 6" in exI, simp)
done
end