diff -r 0b302c0b449a -r 469c26d19f8e Attic/recursive.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Attic/recursive.thy Wed Feb 06 02:39:53 2013 +0000 @@ -0,0 +1,5024 @@ +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 \ 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 \ nat \ nat \ 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 \ nat \ abc_prog" + where + "empty m n = [Dec m 3, Inc n, Goto 0]" + +fun abc_inst_shift :: "abc_inst \ nat \ 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 \ nat \ abc_inst list" + where + "abc_shift xs n = map (\ x. abc_inst_shift x n) xs" + +fun abc_append :: "abc_inst list \ abc_inst list \ + 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 \ [Goto 1]" + +text {* + The compilation of @{text "s"}-operator. +*} +definition rec_ci_s :: "abc_inst list" + where + "rec_ci_s \ (addition 0 1 2 [+] [Inc 1])" + + +text {* + The compilation of @{text "id i j"}-operator +*} + +fun rec_ci_id :: "nat \ nat \ abc_inst list" + where + "rec_ci_id i j = addition j i (i + 1)" + + +fun mv_boxes :: "nat \ nat \ nat \ 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 \ 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 \ nat \ nat) list \ nat \ 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 \ abc_inst list \ nat \ 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 (\ g. rec_ci g) (f # gs) in + let (fprog, fpara, fn) = hd cied_gs in + let pstr = + Max (set (Suc n # fn # (map (\ (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) \ set (f # gs)" + thus "(x, Cn n f gs) \ measure size" + by(induct gs, auto) +next + fix n f g + show "(f, Pr n f g) \ measure size" by auto +next + fix n f g x xa y xb ya + show "(g, Pr n f g) \ measure size" by auto +next + fix n f + show "(f, Mn n f) \ 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: + "\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: + "\rec_calc_rel z l x; rec_calc_rel z l y\ \ x = y" +apply(auto elim: calc_z_reverse) +done + +lemma rec_calc_inj_case_s: + "\rec_calc_rel s l x; rec_calc_rel s l y\ \ x = y" +apply(auto elim: calc_s_reverse) +done + +lemma rec_calc_inj_case_id: + "\rec_calc_rel (recf.id nat1 nat2) l x; + rec_calc_rel (recf.id nat1 nat2) l y\ \ x = y" +apply(auto elim: calc_id_reverse) +done + +lemma rec_calc_inj_case_mn: + assumes ind: "\ l x y. \rec_calc_rel f l x; rec_calc_rel f l y\ + \ 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" + "\xv. rec_calc_rel f (l @ [x]) v \ 0 < v" "\ 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: + "\l x y. \rec_calc_rel f l x; rec_calc_rel f l y\ \ x = y" + and g_ind: + "\x xa y xb ya l xc yb. + \x = rec_ci f; (xa, y) = x; (xb, ya) = y; + rec_calc_rel g l xc; rec_calc_rel g l yb\ \ 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: + "\ l xc yb. \rec_calc_rel g l xc; rec_calc_rel g l yb\ + \ 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: + "\ry rya. \rec_calc_rel (Pr (length l) f g) (l @ [y]) ry; + rec_calc_rel (Pr (length l) f g) (l @ [y]) rya\ \ 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: + "\k \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: + "\length xs = length ys; \ k < length xs. xs ! k = ys ! k\ + \ xs = ys" +apply(induct xs arbitrary: ys, simp) +apply(case_tac ys, simp, simp) +proof - + fix a xs ys aa list + assume ind: + "\ys. \length list = length ys; \k + \ xs = ys" + and h: "length xs = length list" + "\k 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: + "\x l xa y. + \x = f \ x \ set gs; rec_calc_rel x l xa; rec_calc_rel x l y\ + \ 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: + "\rec_calc_rel f l x; + rec_calc_rel f l y\ \ 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: + "\rec_calc_rel (Pr n f g) (lm @ [Suc x]) rs\ + \ \ 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 \ y \ Suc (y - Suc x) = y - x" +by arith + +lemma calc_pr_para_not_null: + "rec_calc_rel (Pr n f g) lm rs \ lm \ []" +apply(erule calc_pr_reverse, simp, simp) +done + +lemma calc_pr_less_ex: + "\rec_calc_rel (Pr n f g) lm rs; x \ last lm\ \ + \rs. rec_calc_rel (Pr n f g) (butlast lm @ [last lm - x]) rs" +apply(subgoal_tac "lm \ []") +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 \ + \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 \ + (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 \ length bp \ 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: + "\abc_steps_l (0, lm) bp stpa = (length bp, lm1); + abc_steps_l (0, lm) bp stpb = (length bp, lm2)\ \ 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: + "\\stp. abc_steps_l (0, lm) bp stp = (bs, lm'); + bs = length bp; bp \ []\ + \ \ stp. (\ (s, l). s < bs \ + (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 \ []" + thus + "\stp. (\(s, l). s < bs \ + 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') + \ \stp. (\(s, l). s < length bp \ 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 \ []" + from h show + "\stp. (\(s, l). s < length bp \ 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]: + "\a < length bp; abc_steps_l (a, b) bp (Suc 0) = (length bp, lm')\ + \ 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: + "\bs < length bp; abc_steps_l (a, b) bp (Suc 0) = (bs, l)\ + \ 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: + "\bs < length bp; abc_steps_l (0, lm) bp stpa = (bs, l)\ + \ 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: + "\bs l. \bs < length bp; abc_steps_l (0, lm) bp stpa = (bs, l)\ + \ 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: + "\\ stp. abc_steps_l (0, lm) bp stp = (bs, lm'); + bs = length bp; + as = length ap\ + \ \ 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: + "\\ stp. abc_steps_l (0, am) bp stp = (bs, bm); ss = length ap\ + \ \ 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 " \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 "\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: + "\bs bm. \abc_steps_l (0, am) bp stp = (bs, bm); + ss = length ap\ \ + \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 + "\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: + "\ap \ []; + abc_steps_l (0, am) ap astp = (a, b); + a < length ap\ + \ (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: + "\a b. \abc_steps_l (0, am) ap astp = (a, b); + a < length ap\ \ + 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: + "\\ astp. abc_steps_l (0, am) ap astp = (as, bm); as = length ap\ + \ \ 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: + "\\ astp. abc_steps_l (0, am) ap astp = (as, bm); as = length ap; + \ bstp. abc_steps_l (0, bm) bp bstp = (bs, bm'); bs = length bp; + cs = as + bs; bp \ []\ + \ \ 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 \ + 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 \ + 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: + "\length lm = n\ \ + \ 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: "\ 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: + "\ 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 + "\ 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 \ + (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 " \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: + "\x. \stp. abc_steps_l (ss, lm @ x # y # suf_lm) bp stp = + (0, lm @ (x + y) # 0 # suf_lm)" + show "\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 \ Suc (Suc rs_pos) < a_md \ 0 < rs_pos \ + 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 \ 0 < rs_pos \ + \ a_md - Suc 0 < rs_pos - Suc 0" +apply(arith) +done + +lemma [simp]: + "Suc (Suc rs_pos) < a_md \ 0 < rs_pos \ + \ a_md - rs_pos < Suc (Suc (a_md - Suc (Suc rs_pos)))" +apply(arith) +done + +lemma butlast_append_last: "lm \ [] \ lm = butlast lm @ [last lm]" +apply(auto) +done + +lemma [simp]: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md) + \ (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 \ 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) + \ 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]: + "\rec_ci z = (aprog, rs_pos, a_md); rec_calc_rel z lm xs\ + \ length lm = rs_pos" +apply(simp add: rec_ci.simps rec_ci_z_def) +apply(erule_tac calc_z_reverse, simp) +done + +lemma [intro]: + "\rec_ci s = (aprog, rs_pos, a_md); rec_calc_rel s lm xs\ + \ length lm = rs_pos" +apply(simp add: rec_ci.simps rec_ci_s_def) +apply(erule_tac calc_s_reverse, simp) +done + +lemma [intro]: + "\rec_ci (recf.id nat1 nat2) = (aprog, rs_pos, a_md); + rec_calc_rel (recf.id nat1 nat2) lm xs\ \ length lm = rs_pos" +apply(simp add: rec_ci.simps rec_ci_id.simps) +apply(erule_tac calc_id_reverse, simp) +done + +lemma [intro]: + "\rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); + rec_calc_rel (Cn n f gs) lm xs\ \ 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]: + "\rec_ci (Pr n f g) = (aprog, rs_pos, a_md); + rec_calc_rel (Pr n f g) lm xs\ \ 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]: + "\rec_ci (Mn n f) = (aprog, rs_pos, a_md); + rec_calc_rel (Mn n f) lm xs\ \ 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: + "\rec_ci f = (aprog, rs_pos, a_md); rec_calc_rel f lm xs\ + \ length lm = rs_pos" +apply(case_tac f, auto) +done + +lemma ci_pr_g_paras: + "\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\ \ + 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: + "\rec_ci (Pr n f g) = (aprog, rs_pos, a_md); + rec_ci g = (a, aa, ba)\ \ 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) \ rp < ad" + by(simp add: rec_ci.simps) + +lemma [intro]: "rec_ci s = (ap, rp, ad) \ rp < ad" + by(simp add: rec_ci.simps) + +lemma [intro]: "rec_ci (recf.id nat1 nat2) = (ap, rp, ad) \ rp < ad" + by(simp add: rec_ci.simps) + +lemma [intro]: "rec_ci (Cn n f gs) = (ap, rp, ad) \ 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) \ 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) \ 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) \ ad > rp" +apply(case_tac f, auto) +done + +lemma [elim]: "\a [+] b = []; a \ [] \ b \ []\ \ RR" +apply(auto simp: abc_append.simps abc_shift.simps) +done + +lemma [intro]: "rec_ci z = ([], aa, ba) \ False" +by(simp add: rec_ci.simps rec_ci_z_def) + +lemma [intro]: "rec_ci s = ([], aa, ba) \ False" +by(auto simp: rec_ci.simps rec_ci_s_def addition.simps) + +lemma [intro]: "rec_ci (id m n) = ([], aa, ba) \ False" +by(auto simp: rec_ci.simps rec_ci_id.simps addition.simps) + +lemma [intro]: "rec_ci (Cn n f gs) = ([], aa, ba) \ 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) \ 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) \ False" +apply(case_tac "rec_ci f", auto simp: rec_ci.simps) +done + +lemma rec_ci_not_null: "rec_ci g = (a, aa, ba) \ a \ []" +by(case_tac g, auto) + +lemma calc_pr_g_def: + "\rec_calc_rel (Pr rs_pos f g) (lm @ [Suc x]) rsa; + rec_calc_rel (Pr rs_pos f g) (lm @ [x]) rsxa\ + \ 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: + "\rec_ci (Pr n f g) = (aprog, rs_pos, a_md); + rec_ci g = (a, aa, ba); rec_ci f = (ab, ac, bc)\ + \ a_md = Suc (max (n + 3) (max bc ba))" +by(simp add: rec_ci.simps) + +lemma ci_pr_f_paras: + "\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)\ \ ac = rs_pos - Suc 0" +apply(subgoal_tac "\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 \ []", simp) +apply(erule_tac calc_pr_reverse, simp, simp) +apply(erule calc_pr_zero_ex) +done + +lemma ci_pr_md_ge_f: "\rec_ci (Pr n f g) = (aprog, rs_pos, a_md); + rec_ci f = (ab, ac, bc)\ \ Suc bc \ a_md" +apply(case_tac "rec_ci g") +apply(simp add: rec_ci.simps, auto) +done + +lemma ci_pr_md_ge_g: "\rec_ci (Pr n f g) = (aprog, rs_pos, a_md); + rec_ci g = (ab, ac, bc)\ \ bc < a_md" +apply(case_tac "rec_ci f") +apply(simp add: rec_ci.simps, auto) +done + +lemma rec_calc_rel_def0: + "\rec_calc_rel (Pr n f g) lm rs; rec_calc_rel f (butlast lm) rsa\ + \ 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 + "\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)\ +\ \ap bp cp. aprog = ap [+] bp [+] cp \ length ap = 3 + length ab \ 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 "\rec_ci (Pr n f g) = (aprog, rs_pos, a_md); + rec_ci g = (a, aa, ba); rec_ci f = (ab, ac, bc)\ + \ \ap bp cp. aprog = ap [+] bp [+] cp \ length ap = 3 \ 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]: "\rec_ci (Pr n f g) = (aprog, rs_pos, a_md); rec_calc_rel (Pr n f g) lm rs\ + \ rs_pos = Suc n" +apply(simp add: ci_pr_para_eq) +done + + +lemma [simp]: "\rec_ci (Pr n f g) = (aprog, rs_pos, a_md); rec_calc_rel (Pr n f g) lm rs\ + \ 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) \ 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) \ 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 \ + 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: + "\lm rs suf_lm. rec_calc_rel g lm rs \ + \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 \ last lm" + "rec_ci g = (a, aa, ba)" + "rec_calc_rel (Pr n f g) (butlast lm @ [last lm - xa]) rsa" + "lm \ []" + shows + "\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: "\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 + "\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 \ rs_pos = Suc n \ + 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 "\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 \ a_md > ba \ 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 + "\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 \ 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 + "\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: + "\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 \ 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: + "\rec_ci (Pr n f g) = (aprog, rs_pos, a_md); + rec_ci g = (a, aa, ba); + rec_ci f = (ab, ac, bc)\ +\ \ap bp. length ap = 6 + length ab \ + aprog = ap [+] bp \ + 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: + "\\lm rs suf_lm. rec_calc_rel g lm rs \ + \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 \ []; + x \ last lm\ \ + \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: + "\lm rs suf_lm. rec_calc_rel g lm rs \ + \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 \ []" + "x \ last lm" + "rec_ci f = (ab, ac, bc)" + from h show + "\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 \ [] \ rs_pos = Suc n", simp) + apply(rule_tac rec_calc_inj, simp, simp) + apply(simp) + done + thus "\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: + "\rsx. rec_calc_rel (Pr n f g) (butlast lm @ [last lm - xa]) rsx + \ \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 \ 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 \ []" + from g have k1: + "\ 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 + "\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 + "\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: + "\ ap bp. length ap = 6 + length ab \ + aprog = ap [+] bp \ + 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 \ + aprog = ap [+] bp \ 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 + "\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: + "\rec_ci (Pr n f g) = (aprog, rs_pos, a_md); + rec_ci g = (a, aa, ba); + rec_ci f = (ab, ac, bc)\ + \ length aprog = 13 + length ab + length a" +apply(auto simp: rec_ci.simps) +done + +thm empty.simps +term max +fun empty_inv :: "nat \ nat list \ nat \ nat \ nat list \ bool" + where + "empty_inv (as, lm) m n initlm = + (let plus = initlm ! m + initlm ! n in + length initlm > max m n \ m \ n \ + (if as = 0 then \ k l. lm = initlm[m := k, n := l] \ + k + l = plus \ k \ initlm ! m + else if as = 1 then \ k l. lm = initlm[m := k, n := l] + \ k + l + 1 = plus \ k < initlm ! m + else if as = 2 then \ k l. lm = initlm[m := k, n := l] + \ k + l = plus \ k \ initlm ! m + else if as = 3 then lm = initlm[m := 0, n := plus] + else False))" + +fun empty_stage1 :: "nat \ nat list \ nat \ nat" + where + "empty_stage1 (as, lm) m = + (if as = 3 then 0 + else 1)" + +fun empty_stage2 :: "nat \ nat list \ nat \ nat" + where + "empty_stage2 (as, lm) m = (lm ! m)" + +fun empty_stage3 :: "nat \ nat list \ nat \ 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 \ nat list) \ nat) \ (nat \ nat \ 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 \ nat) \ nat \ nat) set" + where + "lex_pair = less_than <*lex*> less_than" + +definition lex_triple :: + "((nat \ (nat \ nat)) \ (nat \ (nat \ nat))) set" + where + "lex_triple \ less_than <*lex*> lex_pair" + +definition empty_LE :: + "(((nat \ nat list) \ nat) \ ((nat \ nat list) \ nat)) set" + where + "empty_LE \ (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: +"\m < length initlm; n < length initlm; m \ n\ \ + 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]: + "\m \ n; m < length initlm; n < length initlm; + k + l = initlm ! m + initlm ! n; k \ initlm ! m; 0 < k\ + \ \ka la. initlm[m := k, n := l, m := k - Suc 0] = + initlm[m := ka, n := la] \ + Suc (ka + la) = initlm ! m + initlm ! n \ + 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]: + "\m \ n; m < length initlm; n < length initlm; + Suc (k + l) = initlm ! m + initlm ! n; + k < initlm ! m\ + \ \ka la. initlm[m := k, n := l, n := Suc l] = + initlm[m := ka, n := la] \ + ka + la = initlm ! m + initlm ! n \ + ka \ initlm ! m" +apply(rule_tac x = k in exI, rule_tac x = "Suc l" in exI, auto) +done + +lemma [simp]: + "\length initlm > max m n; m \ n\ \ + \na. \ (\(as, lm) m. as = 3) + (abc_steps_l (0, initlm) (recursive.empty m n) na) m \ + empty_inv (abc_steps_l (0, initlm) + (recursive.empty m n) na) m n initlm \ + empty_inv (abc_steps_l (0, initlm) + (recursive.empty m n) (Suc na)) m n initlm \ + ((abc_steps_l (0, initlm) (recursive.empty m n) (Suc na), m), + abc_steps_l (0, initlm) (recursive.empty m n) na, m) \ 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: + "\length initlm > max m n; m \ n\ \ + \ stp. (\ (as, lm). as = 3 \ + empty_inv (as, lm) m n initlm) + (abc_steps_l (0::nat, initlm) (empty m n) stp)" +apply(insert halt_lemma2[of empty_LE + "\ ((as, lm), m). as = (3::nat)" + "\ stp. (abc_steps_l (0, initlm) (recursive.empty m n) stp, m)" + "\ ((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: + "\m \ n; empty_inv (a, b) m n lm; a = 3\ \ + 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: + "\length lm > max m n; m \ n\ \ + \ 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]: + "\a_md = Suc (max (Suc (Suc n)) (max bc ba)); + length lm = rs_pos \ rs_pos = n \ n > 0\ + \ n - Suc 0 < length lm + + (Suc (max (Suc (Suc n)) (max bc ba)) - rs_pos + length suf_lm) \ + Suc (Suc n) < length lm + (Suc (max (Suc (Suc n)) (max bc ba)) - + rs_pos + length suf_lm) \ bc < length lm + (Suc (max (Suc (Suc n)) + (max bc ba)) - rs_pos + length suf_lm) \ ba < length lm + + (Suc (max (Suc (Suc n)) (max bc ba)) - rs_pos + length suf_lm)" +apply(arith) +done + +lemma [simp]: + "\a_md = Suc (max (Suc (Suc n)) (max bc ba)); + length lm = rs_pos \ rs_pos = n \ n > 0\ + \ n - Suc 0 < Suc (length suf_lm + max (Suc (Suc n)) (max bc ba)) \ + Suc n < length suf_lm + max (Suc (Suc n)) (max bc ba) \ + bc < Suc (length suf_lm + max (Suc (Suc n)) (max bc ba)) \ + ba < Suc (length suf_lm + max (Suc (Suc n)) (max bc ba))" +apply(arith) +done + +lemma [simp]: "n - Suc 0 \ max (Suc (Suc n)) (max bc ba)" +apply(arith) +done + +lemma [simp]: + "a_md \ Suc bc \ rs_pos > 0 \ bc \ rs_pos \ + bc - (rs_pos - Suc 0) + a_md - Suc bc = Suc (a_md - rs_pos - Suc 0)" +apply(arith) +done + +lemma [simp]: "length lm = n \ rs_pos = n \ 0 < rs_pos \ + Suc rs_pos < a_md + \ n - Suc 0 < Suc (Suc (a_md + length suf_lm - Suc (Suc 0))) + \ n < Suc (Suc (a_md + length suf_lm - Suc (Suc 0)))" +apply(arith) +done + +lemma [simp]: "length lm = n \ rs_pos = n \ 0 < rs_pos \ + Suc rs_pos < a_md \ n - Suc 0 \ n" +by arith + +lemma ci_pr_ex2: + "\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)\ + \ \ap bp. aprog = ap [+] bp \ + 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 \ a\<^bsup>m\<^esup> ! n = a" +apply(simp add: exponent_def) +done + +lemma [simp]: "length lm = n \ rs_pos = n \ 0 < n \ + 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]: "\length lm = n; 0 < n\ \ 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 \ \ n < n - Suc 0" +by auto + +lemma [simp]: + "Suc n < length suf_lm + max (Suc (Suc n)) (max bc ba) \ + bc < Suc (length suf_lm + max (Suc (Suc n)) + (max bc ba)) \ + ba < Suc (length suf_lm + max (Suc (Suc n)) (max bc ba))" + by arith + +lemma [simp]: "length lm = n \ rs_pos = n \ n > 0 \ +(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]: + "\length lm = n; 0 < n; Suc n < a_md\ \ + (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) \ a_md \ length lm = rs_pos \ 0 < rs_pos + \ a_md - Suc 0 < + Suc (Suc (Suc (a_md + length suf_lm - Suc (Suc (Suc 0)))))" +by arith + +lemma [simp]: + "Suc (Suc rs_pos) \ a_md \ length lm = rs_pos \ 0 < rs_pos \ + \ a_md - Suc 0 < rs_pos - Suc 0" +by arith + +lemma [simp]: "Suc (Suc rs_pos) \ a_md \ + \ a_md - Suc 0 < rs_pos - Suc 0" +by arith + +lemma [simp]: "\Suc (Suc rs_pos) \ a_md\ \ + \ a_md - rs_pos < Suc (Suc (a_md - Suc (Suc rs_pos)))" +by arith + +lemma [simp]: + "Suc (Suc rs_pos) \ a_md \ length lm = rs_pos \ 0 < rs_pos + \ (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 \ + 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) \ + 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]: "\rec_ci (Pr n f g) = (aprog, rs_pos, a_md); + rec_ci g = (a, aa, ba); rec_ci f = (ab, ac, bc)\ + \ \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 \ []" +by (simp add: empty.simps) +(* +lemma [simp]: "\rs_pos = n; 0 < rs_pos ; Suc rs_pos < a_md\ \ + n - Suc 0 < a_md + length suf_lm" +by arith +*) +lemma [intro]: + "\rec_ci (Pr n f g) = (aprog, rs_pos, a_md); + rec_ci f = (ab, ac, bc)\ \ + \ap. (\cp. aprog = ap [+] ab [+] cp) \ 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]: + "\rec_ci (Pr n f g) = (aprog, rs_pos, a_md); + rec_ci g = (a, aa, ba); + rec_ci f = (ab, ac, bc)\ \ + \ap. (\cp. aprog = ap [+] recursive.empty n (Suc n) [+] cp) + \ 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) \ + Suc n < max (Suc (Suc n)) (max bc ba) + length suf_lm \ + bc < Suc (max (Suc (Suc n)) (max bc ba) + length suf_lm) \ + ba < Suc (max (Suc (Suc n)) (max bc ba) + length suf_lm)" +by arith +*) + +lemma [intro]: + "\rec_ci (Pr n f g) = (aprog, rs_pos, a_md); + rec_ci g = (a, aa, ba); + rec_ci f = (ab, ac, bc)\ + \ \ap. (\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) \ + 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]: "\rs_pos = n; 0 < rs_pos ; Suc rs_pos < a_md\ \ + n - Suc 0 < Suc (Suc (a_md + length suf_lm - 2)) \ + n < Suc (Suc (a_md + length suf_lm - 2))" +by arith +*) + +lemma [simp]: + "n < Suc (max (n + 3) (max bc ba) + length suf_lm) \ + Suc (Suc n) < max (n + 3) (max bc ba) + length suf_lm \ + bc < Suc (max (n + 3) (max bc ba) + length suf_lm) \ + ba < Suc (max (n + 3) (max bc ba) + length suf_lm)" +by arith + +lemma [simp]: "n \ max (n + (3::nat)) (max bc ba)" +by arith + +lemma [simp]:"length lm = Suc n \ lm[n := (0::nat)] = butlast lm @ [0]" +apply(subgoal_tac "\ 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 \ lm ! n =last lm" +apply(subgoal_tac "lm \ []") +apply(simp add: last_conv_nth, case_tac lm, simp_all) +done + +lemma [simp]: "length lm = Suc n \ + (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 \ + n < Suc (Suc (a_md + length suf_lm - 2)) \ + n < Suc (a_md + length suf_lm - 2)" +by(arith) + +lemma [simp]: "\length lm = Suc n; Suc (Suc n) < a_md\ + \(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: + "\ lm rs suf_lm. rec_calc_rel f lm rs \ + \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: "\ lm rs suf_lm. rec_calc_rel g lm rs \ + \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 "\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: "\ 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 "\bp cp. aprog = bp [+] cp \ 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 + "\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 \ 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: + "\ 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: "\ 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: + "\ 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: " + \ ap bp cp. aprog = ap [+] bp [+] cp \ length ap = 3 \ + 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 \ Suc bc \ rs_pos > 0 \ bc \ 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: + "\ 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 "\ ap bp cp. aprog = ap [+] bp [+] cp \ + length ap = 3 + length ab \ 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 \ length ap = 3 + + length ab \ bp = recursive.empty n (Suc n)" + thus "?thesis" + apply(simp del: abc_append_commute) + apply(subgoal_tac + "\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 \ rs_pos = Suc n \ a_md > Suc (Suc n)", simp) + apply(insert h, simp) + done + qed + qed + from h have k2_3: "lm \ []" + apply(rule_tac calc_pr_para_not_null, simp) + done + from h and k2_2 and k2_3 have k2_2_3: + "\ 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: + "\ 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 + "\ ap bp cp. aprog = ap [+] bp [+] cp \ + length ap = 6 + length ab \ + 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 + "\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) \ + length lm = rs_pos \ 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 + "\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 \ y = x" +by simp + +lemma [simp]: + "\rec_ci f = (a, aa, ba); + rec_ci (Mn n f) = (aprog, rs_pos, a_md)\ \ \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) \ rs_pos = n" +apply(case_tac "rec_ci f", simp add: rec_ci.simps) +done +(* +lemma [simp]: "\rec_ci f = (a, aa, ba); rec_ci (Mn n f) = (aprog, rs_pos, a_md); rec_calc_rel (Mn n f) lm rs\ \ 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) \ aa < ba" +apply(simp add: ci_ad_ge_paras) +done + +lemma [simp]: "\rec_ci f = (a, aa, ba); + rec_ci (Mn n f) = (aprog, rs_pos, a_md)\ + \ ba \ a_md" +apply(simp add: rec_ci.simps) +by arith + +lemma mn_calc_f: + assumes ind: + "\aprog a_md rs_pos rs suf_lm lm. + \rec_ci f = (aprog, rs_pos, a_md); rec_calc_rel f lm rs\ + \ \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 "\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: "\ ap bp. aprog = ap @ bp \ 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 + "\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 \ a_md \ ba \ aa = Suc n", + insert h, auto) + done + qed +qed +thm rec_ci.simps + +fun mn_ind_inv :: + "nat \ nat list \ nat \ nat \ nat \ nat list \ nat list \ 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 + \y. (lm' = lm @ x # y # suf_lm) \ y \ rsx + else if as = ss + 2 then + \y. (lm' = lm @ x # y # suf_lm) \ y \ 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 \ nat list \ nat \ nat \ 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 \ as = ss + 1 then 3 + else if as = ss then 4 + else 0 +)" + +fun mn_stage2 :: "nat \ nat list \ nat \ nat \ nat" + where + "mn_stage2 (as, lm) ss n = + (if as = ss + 1 \ as = ss + 2 then (lm ! (Suc n)) + else 0)" + +fun mn_stage3 :: "nat \ nat list \ nat \ nat \ nat" + where + "mn_stage3 (as, lm) ss n = (if as = ss + 2 then 1 else 0)" + + +fun mn_measure :: "((nat \ nat list) \ nat \ nat) \ + (nat \ nat \ 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 \ nat list) \ nat \ nat) \ + ((nat \ nat list) \ nat \ nat)) set" + where "mn_LE \ (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) \ + \ (\(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]: + "\rec_ci f = (a, aa, ba); + rec_ci (Mn n f) = (aprog, rs_pos, a_md)\ + \ 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]: "\rec_ci f = (a, aa, ba); rec_ci (Mn n f) = (aprog, rs_pos, a_md)\ + \ 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]: + "\rec_ci f = (a, aa, ba); + rec_ci (Mn n f) = (aprog, rs_pos, a_md)\ + \ 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]: + "\rec_ci f = (a, aa, ba); + rec_ci (Mn n f) = (aprog, rs_pos, a_md)\ + \ 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]: "\rec_ci f = (a, aa, ba); rec_ci (Mn n f) = (aprog, rs_pos, a_md)\ + \ 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 + \ \y. (lm @ x # rsx # suf_lm)[Suc (length lm) := rsx - Suc 0] + = lm @ x # y # suf_lm \ y \ rsx" +apply(case_tac rsx, simp, simp) +apply(rule_tac x = nat in exI, simp add: list_update_append) +done + +lemma [simp]: + "\y \ rsx; 0 < y\ + \ \ya. (lm @ x # y # suf_lm)[Suc (length lm) := y - Suc 0] + = lm @ x # ya # suf_lm \ ya \ rsx" +apply(case_tac y, simp, simp) +apply(rule_tac x = nat in exI, simp add: list_update_append) +done + +lemma mn_halt_lemma: + "\rec_ci f = (a, aa, ba); + rec_ci (Mn n f) = (aprog, rs_pos, a_md); + 0 < rsx; length lm = n\ + \ + \na. \ (\(as, lm') (ss, n). as = 0) + (abc_steps_l (length a, lm @ x # rsx # suf_lm) aprog na) + (length a, n) + \ mn_ind_inv (abc_steps_l (length a, lm @ x # rsx # suf_lm) + aprog na) (length a) x rsx suf_lm lm +\ mn_ind_inv (abc_steps_l (length a, lm @ x # rsx # suf_lm) aprog + (Suc na)) (length a) x rsx suf_lm lm + \ ((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) \ 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: + "\rec_ci f = (a, aa, ba); + rec_ci (Mn n f) = (aprog, rs_pos, a_md); + 0 < rsx; length lm = n\ + \ \ stp. (\ (as, lm'). (as = 0 \ + 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 + "\ ((as, lm'), ss, n). as = 0" + "\ stp. (abc_steps_l (length a, lm @ x # rsx # suf_lm) aprog stp, + length a, n)" + "\ ((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 \ + Suc (a_md - Suc (Suc rs_pos)) = a_md - Suc rs_pos" +by arith + +term rec_ci +(* +lemma [simp]: "\rec_ci (Mn n f) = (aprog, rs_pos, a_md); rec_calc_rel (Mn n f) lm rs\ \ Suc rs_pos < a_md" +apply(case_tac "rec_ci f") +apply(subgoal_tac "c > b \ b = Suc rs_pos \ a_md \ c") +apply(arith, auto) +done +*) +lemma mn_ind_step: + assumes ind: + "\aprog a_md rs_pos rs suf_lm lm. + \rec_ci f = (aprog, rs_pos, a_md); + rec_calc_rel f lm rs\ \ + \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 "\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: + "\ 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: + "\ 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]: + "\rec_ci f = (a, aa, ba); rec_ci (Mn n f) = (aprog, rs_pos, a_md); + rec_calc_rel (Mn n f) lm rs\ \ 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 (Mn n f) = (aprog, rs_pos, a_md); + rec_calc_rel (Mn n f) lm rs\ \ Suc rs_pos < a_md" +apply(case_tac "rec_ci f") +apply(subgoal_tac "c > b \ b = Suc rs_pos \ a_md \ c") +apply(arith, auto) +done + +lemma mn_ind_steps: + assumes ind: + "\aprog a_md rs_pos rs suf_lm lm. + \rec_ci f = (aprog, rs_pos, a_md); rec_calc_rel f lm rs\ \ + \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" + "\x v. rec_calc_rel f (lm @ [x]) v \ 0 < v)" + "n = length lm" + "x \ rs" + shows "\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: + "\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" + "\x v. rec_calc_rel f (lm @ [x]) v \ v > 0)" + "n = length lm" + "Suc x \ rs" + "rec_ci f = (a, aa, ba)" + hence k2: + "\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 + "\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]: +"\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\ + \ 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]: + "\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\ + \ 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: + "\rec_ci f = (a, aa, ba); + rec_ci (Mn n f) = (aprog, rs_pos, a_md)\ + \ 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: + "\aprog a_md rs_pos rs suf_lm lm. + \rec_ci f = (aprog, rs_pos, a_md); + rec_calc_rel f lm rs\ \ + \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 "\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: + "\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: + "\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: + "\aprog a_md rs_pos rs suf_lm lm. + \rec_ci f = (aprog, rs_pos, a_md); rec_calc_rel f lm rs\ \ + \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 "\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" + "\xv. rec_calc_rel f (lm @ [x]) v \ 0 < v" + "n = length lm" + hence k1: + "\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: + "\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 + "\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 \ rs = 0" +apply(rule_tac calc_z_reverse, auto) +done + +lemma z_case: + "\rec_ci z = (aprog, rs_pos, a_md); rec_calc_rel z lm rs\ + \ \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 \ nat list \ nat \ nat \ nat \ + nat list \ bool" + where + "addition_inv (as, lm') m n p lm = + (let sn = lm ! n in + let sm = lm ! m in + lm ! p = 0 \ + (if as = 0 then \ x. x \ lm ! m \ lm' = lm[m := x, + n := (sn + sm - x), p := (sm - x)] + else if as = 1 then \ x. x < lm ! m \ lm' = lm[m := x, + n := (sn + sm - x - 1), p := (sm - x - 1)] + else if as = 2 then \ x. x < lm ! m \ lm' = lm[m := x, + n := (sn + sm - x), p := (sm - x - 1)] + else if as = 3 then \ x. x < lm ! m \ lm' = lm[m := x, + n := (sn + sm - x), p := (sm - x)] + else if as = 4 then \ x. x \ lm ! m \ lm' = lm[m := x, + n := (sn + sm), p := (sm - x)] + else if as = 5 then \ x. x < lm ! m \ lm' = lm[m := x, + n := (sn + sm), p := (sm - x - 1)] + else if as = 6 then \ x. x < lm ! m \ 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 \ nat list \ nat \ nat \ nat" + where + "addition_stage1 (as, lm) m p = + (if as = 0 \ as = 1 \ as = 2 \ as = 3 then 2 + else if as = 4 \ as = 5 \ as = 6 then 1 + else 0)" + +fun addition_stage2 :: "nat \ nat list \ nat \ nat \ nat" + where + "addition_stage2 (as, lm) m p = + (if 0 \ as \ as \ 3 then lm ! m + else if 4 \ as \ as \ 6 then lm ! p + else 0)" + +fun addition_stage3 :: "nat \ nat list \ nat \ nat \ 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 \ nat list) \ nat \ nat) \ + (nat \ nat \ 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 \ nat list) \ nat \ nat) \ + ((nat \ nat list) \ nat \ nat)) set" + where "addition_LE \ (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: + "\m \ n; max m n < p; length lm > p; lm ! p = 0\ \ + 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]: + "\m \ n; p < length lm; lm ! p = 0; m < p; n < p; x \ lm ! m; 0 < x\ + \ \xam \ n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\ + \ \xam \ n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\ + \ \xam \ n; p < length lm; lm ! p = (0::nat); m < p; n < p; x < lm ! m\ + \ \xa\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]: + "\m \ n; p < length lm; lm ! p = 0; m < p; n < p; + x \ lm ! m; lm ! m \ x\ + \ \xam \ n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\ + \ \xam \ n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\ + \ \xa\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: + "\m \ n; max m n < p; length lm > p; lm ! p = 0\ \ + \na. \ (\(as, lm') (m, p). as = 7) + (abc_steps_l (0, lm) (addition m n p) na) (m, p) \ + addition_inv (abc_steps_l (0, lm) (addition m n p) na) m n p lm +\ addition_inv (abc_steps_l (0, lm) (addition m n p) + (Suc na)) m n p lm + \ ((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) \ 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: + "\m \ n; max m n < p; length lm > p; lm ! p = 0\ \ + \ stp. (\ (as, lm'). as = 7 \ 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 + "\ ((as, lm'), m, p). as = 7" + "\ stp. (abc_steps_l (0, lm) (addition m n p) stp, m, p)" + "\ ((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 = [] \ 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]: + "\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: + "\rec_ci s = (aprog, rs_pos, a_md); rec_calc_rel s lm rs\ + \ \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]: + "\n < length lm; lm ! n = rs\ + \ \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: + "\rec_ci (id m n) = (aprog, rs_pos, a_md); + rec_calc_rel (id m n) lm rs\ + \ \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: + "\P []; \a list. P list \ P (list @ [a::'a])\ \ + P ((list::'a list))" +apply(case_tac "length list", simp) +proof - + fix nat + assume ind: "\a list. P list \ 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: "\list. \length list = Suc nat; P []\ \ 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: "\length ys > Suc k\ \ + ys ! k = butlast ys ! k" +apply(subgoal_tac "\ 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]: +"\\k + \ \k(ap, pos, n)\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 \ pstr \ pstr + x - n > 0" +by arith + +lemma [simp]: + "\Suc (pstr + length list) \ a_md; + length ys = Suc (length list); + length lm = n; + Suc n \ pstr\ + \ (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]: + "\Suc (pstr + length list) \ a_md; + length ys = Suc (length list); + length lm = n; + Suc n \ pstr\ + \ (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: + "\\x aprog a_md rs_pos rs suf_lm lm. + \x \ set gs; rec_ci x = (aprog, rs_pos, a_md); + rec_calc_rel x lm rs\ + \ \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\ a_md; + \k Max (set (Suc n # map (\(aprog, p, n). n) (map rec_ci gs)))\ + \ \ 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 ((\(ap, pos, n). length ap) \ 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: "\x aprog a_md rs_pos rs suf_lm lm. + \x = a \ x \ set list; rec_ci x = (aprog, rs_pos, a_md); + rec_calc_rel x lm rs\ + \ \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: + "\ys. \\x aprog a_md rs_pos rs suf_lm lm. + \x \ set list; rec_ci x = (aprog, rs_pos, a_md); + rec_calc_rel x lm rs\ + \ \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); + \k + \ \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 ((\(ap, pos, n). length ap) \ 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) \ a_md" + "\k pstr \ (\(aprog, p, n). n) (rec_ci a) \ pstr \ + (\a\set list. (\(aprog, p, n). n) (rec_ci a) \ pstr)" + from h have k1: + "\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 ((\(ap, pos, n). length ap) \ 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 + "\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 ((\(ap, pos, n). length ap) \ rec_ci) list) + + (\(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 = + "(\(ap, pos, n)\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 = "(\(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 + "\bstp. abc_steps_l (0, lm @ 0\<^bsup>pstr - n\<^esup> @ butlast ys @ + 0\<^bsup>a_md - (pstr + length list)\<^esup> @ suf_lm) + ((\(gprog, gpara, gn). gprog [+] recursive.empty gpara + (pstr + length list)) (rec_ci a)) bstp = + ((\(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 + "\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 \ 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 + "\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) \ []" + by(simp add: empty.simps) + qed + next + show "(\(ap, pos, n). length ap) (rec_ci a) + 3 = + length ((\(gprog, gpara, gn). gprog [+] + recursive.empty gpara (pstr + length list)) (rec_ci a))" + by(case_tac "rec_ci a", simp) + next + show "listsum (map ((\(ap, pos, n). length ap) \ rec_ci) list) + + (\(ap, pos, n). length ap) (rec_ci a) + (3 + 3 * length list)= + (\(ap, pos, n)\map rec_ci list. length ap) + 3 * length list + + ((\(ap, pos, n). length ap) (rec_ci a) + 3)" by simp + next + show "(\(gprog, gpara, gn). gprog [+] + recursive.empty gpara (pstr + length list)) (rec_ci a) \ []" + 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]: + "\Suc n \ ba - aa; length lm2 = Suc n; + length lm3 = ba - Suc (aa + n)\ + \ (last lm2 # lm3 @ butlast lm2 @ 0 # lm4) ! (ba - aa) = (0::nat)" +proof - + assume h: "Suc n \ 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 \ + (lm1 @ 0\<^bsup>n\<^esup> @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4) ! (aa + n) = last lm2" +apply(simp add: nth_append) +done + +lemma [simp]: "\Suc n \ ba - aa; aa < ba\ \ + (ba < Suc (aa + (ba - Suc (aa + n) + n))) = False" +apply arith +done + +lemma [simp]: "\Suc n \ ba - aa; aa < ba; length lm1 = aa; + length lm2 = Suc n; length lm3 = ba - Suc (aa + n)\ + \ (lm1 @ 0\<^bsup>n\<^esup> @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4) ! (ba + n) = 0" +using nth_append[of "lm1 @ 0\'a\<^bsup>n\<^esup> @ last lm2 # lm3 @ butlast lm2" + "(0\'a) # lm4" "ba + n"] +apply(simp) +done + +lemma [simp]: + "\Suc n \ ba - aa; aa < ba; length lm1 = aa; length lm2 = Suc n; + length lm3 = ba - Suc (aa + n)\ + \ (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: + "\n \ ba - aa; ba > aa; length lm1 = aa; + length (lm2::nat list) = n; length lm3 = ba - aa - n\ + \ \ 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: + "\lm2 lm3 lm4. \length lm2 = n; length lm3 = ba - (aa + n)\ \ + \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 \ 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 + "\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 \ ba - aa" + "aa < ba" + "length (lm1::nat list) = aa" + "length (lm2::nat list) = Suc n" + "length (lm3::nat list) = ba - Suc (aa + n)" + thus " \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]: "\Suc n \ aa - ba; + ba < aa; + length lm2 = aa - Suc (ba + n)\ + \ ((0::nat) # lm2 @ 0\<^bsup>n\<^esup> @ last lm3 # lm4) ! (aa - ba) + = last lm3" +proof - + assume h: "Suc n \ 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]: "\Suc n \ aa - ba; ba < aa; length lm1 = ba; + length lm2 = aa - Suc (ba + n); length lm3 = Suc n\ + \ (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]: "\Suc n \ aa - ba; ba < aa; length lm1 = ba; + length lm2 = aa - Suc (ba + n); length lm3 = Suc n\ + \ (lm1 @ butlast lm3 @ 0 # lm2 @ 0\<^bsup>n\<^esup> @ last lm3 # lm4) ! (ba + n) = 0" +apply(simp add: nth_append) +done + + +lemma [simp]: "\Suc n \ aa - ba; ba < aa; length lm1 = ba; + length lm2 = aa - Suc (ba + n); length lm3 = Suc n\ + \ (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\'a) # lm2 @ 0\'a\<^bsup>n\<^esup> @ last lm3 # lm4"] +apply(simp) +using list_update_append[of "lm1 @ butlast lm3 @ last lm3 # lm2 @ 0\'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: + "\n \ aa - ba; + ba < aa; + length (lm1::nat list) = ba; + length (lm2::nat list) = aa - ba - n; + length (lm3::nat list) = n\ + \ \ 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: +"\lm2 lm3 lm4. \length lm2 = aa - (ba + n); length lm3 = n\ \ + \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 \ 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 + "\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 \ aa - ba" + "ba < aa" + "length lm1 = ba" + "length (lm2::nat list) = aa - Suc (ba + n)" + "length (lm3::nat list) = Suc n" + thus + "\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) = + (\(ap, pos, n)\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 \ + Suc (pstr + length ys - n) = Suc (pstr + length ys) - n" +by arith + +lemma save_paras': + "\length lm = n; pstr > n; a_md > pstr + length ys + n\ + \ \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 (((\(aprog, p, n). n) o rec_ci) ` set gs)))) + = (Max (insert ba (((\(aprog, p, n). n) o rec_ci) ` set gs)))" +apply(rule min_max.sup_absorb2, auto) +done + +lemma [simp]: + "((\(aprog, p, n). n) ` rec_ci ` set gs) = + (((\(aprog, p, n). n) o rec_ci) ` set gs)" +apply(induct gs) +apply(simp, simp) +done + +lemma ci_cn_md_def: + "\rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); + rec_ci f = (a, aa, ba)\ + \ a_md = max (Suc n) (Max (insert ba (((\(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: + "\rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); + rec_ci f = (a, aa, ba); + pstr = Max (set (Suc n # ba # map (\(aprog, p, n). n) + (map rec_ci (f # gs))))\ + \ \ap bp cp. + aprog = ap [+] bp [+] cp \ + length ap = (\(ap, pos, n)\map rec_ci gs. length ap) + + 3 * length gs \ 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 + (((\(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 (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) + 0 (length gs) [+] a [+]recursive.empty aa (max (Suc n) + (Max (insert ba (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) [+] + empty_boxes (length gs) [+] recursive.empty (max (Suc n) + (Max (insert ba (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) n [+] + mv_boxes (Suc (max (Suc n) (Max (insert ba (((\(aprog, p, n). n) \ rec_ci) + ` set gs))) + length gs)) 0 n" in exI, auto) +apply(simp add: abc_append_commute) +done + +lemma save_paras: + "\rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); + rs_pos = n; + \k(aprog, p, n). n) + (map rec_ci (f # gs))))\ + \ \stp. abc_steps_l ((\(ap, pos, n)\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 = + ((\(ap, pos, n)\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" + "\k(aprog, p, n). n) + (map rec_ci (f # gs))))" + from h and g have k1: + "\ ap bp cp. aprog = ap [+] bp [+] cp \ + length ap = (\(ap, pos, n)\map rec_ci gs. length ap) + + 3 *length gs \ bp = mv_boxes 0 (pstr + Suc (length ys)) n" + apply(drule_tac save_paras_prog_ex, auto) + done + from h have k2: + "\ 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 + "\stp. abc_steps_l ((\(ap, pos, n)\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 = + ((\(ap, pos, n)\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 \ length ap = + (\(ap, pos, n)\map rec_ci gs. length ap) + 3 * length gs + \ 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) \ rs_pos = n" +apply(simp add: rec_ci.simps, case_tac "rec_ci f", simp) +done + +lemma calc_gs_prog_ex: + "\rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); + rec_ci f = (a, aa, ba); + Max (set (Suc n # ba # map (\(aprog, p, n). n) + (map rec_ci (f # gs)))) = pstr\ + \ \ap bp. aprog = ap [+] bp \ + 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 (((\(aprog, p, n). n) \ rec_ci) ` set gs))) + length gs)) n [+] + mv_boxes (max (Suc n) (Max (insert ba + (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) 0 (length gs) [+] + a [+] recursive.empty aa (max (Suc n) + (Max (insert ba (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) [+] + empty_boxes (length gs) [+] recursive.empty (max (Suc n) + (Max (insert ba (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) n [+] + mv_boxes (Suc (max (Suc n) (Max + (insert ba (((\(aprog, p, n). n) \ rec_ci) ` set gs))) + length gs)) 0 n" + in exI) +apply(auto simp: abc_append_commute) +done + +lemma cn_calc_gs: + assumes ind: + "\x aprog a_md rs_pos rs suf_lm lm. + \x \ set gs; + rec_ci x = (aprog, rs_pos, a_md); + rec_calc_rel x lm rs\ + \ \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)" + "\k(aprog, p, n). n) + (map rec_ci (f # gs)))) = pstr" + shows + "\stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) aprog stp = + ((\(ap, pos, n)\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: + "\ ap bp. aprog = ap [+] bp \ 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 \ 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: + "\stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) + (cn_merge_gs (map rec_ci gs) pstr) stp + = ((\(ap, pos, n)\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 + "\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 ((\(ap, pos, n). length ap) \ 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': + "\length lm = n; + pstr > 0; + a_md \ pstr + length ys + n; + pstr > length ys\ \ + \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]: + "\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 (\(aprog, p, n). n) + (map rec_ci (f # gs))))\ + \ length ys < pstr" +apply(subgoal_tac "length ys = aa", simp) +apply(subgoal_tac "aa < ba \ ba \ 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: + "\rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); + rec_ci f = (a, aa, ba); + Max (set (Suc n # ba # map (\(aprog, p, n). n) + (map rec_ci (f # gs)))) = pstr\ + \ \ ap bp cp. aprog = ap [+] bp [+] cp \ + length ap = (\(ap, pos, n)\map rec_ci gs. length ap) + + 3 *length gs + 3 * n \ 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 (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) [+] + mv_boxes 0 (Suc (max (Suc n) (Max (insert ba + (((\(aprog, p, n). n) \ 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 + (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) [+] + empty_boxes (length gs) [+] recursive.empty + (max (Suc n) (Max (insert ba (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) n + [+] mv_boxes (Suc (max (Suc n) (Max (insert ba + (((\(aprog, p, n). n) \ rec_ci) ` set gs))) + length gs)) 0 n" in exI, + auto simp: abc_append_commute) +done + + +lemma reset_new_paras: + "\rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); + rs_pos = n; + \k(aprog, p, n). n) + (map rec_ci (f # gs))))\ +\ \stp. abc_steps_l ((\(ap, pos, n)\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 = + ((\(ap, pos, n)\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" + "\k(aprog, p, n). n) + (map rec_ci (f # gs))))" + thm rec_ci.simps + from h and g have k1: + "\ ap bp cp. aprog = ap [+] bp [+] cp \ length ap = + (\(ap, pos, n)\map rec_ci gs. length ap) + + 3 *length gs + 3 * n \ bp = mv_boxes pstr 0 (length ys)" + by(drule_tac reset_new_paras_prog_ex, auto) + from h have k2: + "\ 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 \ aa < ba \ ba \ pstr", arith, + simp add: para_pattern) + apply(insert g, auto intro: min_max.le_supI2) + done + from k1 show + "\stp. abc_steps_l ((\(ap, pos, n)\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 = + ((\(ap, pos, n)\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 \ length ap = + (\(ap, pos, n)\map rec_ci gs. length ap) + 3 * length gs + + 3 * n \ bp = mv_boxes pstr 0 (length ys)" + from this and k2 show "?thesis" + apply(simp) + apply(drule_tac as = + "(\(ap, pos, n)\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: + "\rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); + rec_ci f = (a, aa, ba); + Max (set (Suc n # ba # map (\(aprog, p, n). n) + (map rec_ci (f # gs)))) = pstr\ + \ \ ap bp cp. aprog = ap [+] bp [+] cp \ + length ap = (\(ap, pos, n)\map rec_ci gs. length ap) + + 6 *length gs + 3 * n \ 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 + (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) [+] + mv_boxes 0 (Suc (max (Suc n) (Max (insert ba + (((\(aprog, p, n). n) \ rec_ci) ` set gs))) + length gs)) n [+] + mv_boxes (max (Suc n) (Max (insert ba + (((\(aprog, p, n). n) \ 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 + (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) [+] + empty_boxes (length gs) [+] recursive.empty (max (Suc n) ( + Max (insert ba (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) n [+] + mv_boxes (Suc (max (Suc n) (Max (insert ba + (((\(aprog, p, n). n) \ rec_ci) ` set gs))) + length gs)) 0 n" in exI, + auto simp: abc_append_commute) +done + +lemma calc_cn_f: + assumes ind: + "\x aprog a_md rs_pos rs suf_lm lm. + \x \ set (f # gs); + rec_ci x = (aprog, rs_pos, a_md); + rec_calc_rel x lm rs\ + \ \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 (\(aprog, p, n). n) + (map rec_ci (f # gs))))" + shows "\stp. abc_steps_l + ((\(ap, pos, n)\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 = + ((\(ap, pos, n)\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: + "\ ap bp cp. aprog = ap [+] bp [+] cp \ + length ap = (\(ap, pos, n)\map rec_ci gs. length ap) + + 6 *length gs + 3 * n \ 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 \ + length ap = (\(ap, pos, n)\map rec_ci gs. length ap) + + 6 * length gs + 3 * n \ 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 \ aa = length gs\ pstr \ 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]: + "\pstr + length ys + n \ a_md; ys \ []\ \ + pstr < a_md + length suf_lm" +apply(case_tac "length ys", simp) +apply(arith) +done +*) +lemma [simp]: + "pstr > length ys + \ (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]: "\length ys < pstr; pstr - length ys = Suc x\ + \ pstr - Suc (length ys) = x" +by arith +*) +lemma [simp]: "pstr > length ys \ + (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': + "\pstr > length ys\ + \ \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: + "\rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); + rec_ci f = (a, aa, ba); + Max (set (Suc n # ba # map (\(aprog, p, n). n) + (map rec_ci (f # gs)))) = pstr\ + \ \ ap bp cp. aprog = ap [+] bp [+] cp \ + length ap = (\(ap, pos, n)\map rec_ci gs. length ap) + + 6 *length gs + 3 * n + length a + \ 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 + (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) + [+] mv_boxes 0 (Suc (max (Suc n) (Max (insert ba + (((\(aprog, p, n). n) \ rec_ci) ` set gs))) + length gs)) n [+] + mv_boxes (max (Suc n) (Max (insert ba (((\(aprog, p, n). n) \ 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 + (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) n [+] + mv_boxes (Suc (max (Suc n) (Max (insert ba (((\(aprog, p, n). n) \ 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" + "\k(aprog, p, n). n) + (map rec_ci (f # gs))))" + shows "\stp. abc_steps_l + ((\(ap, pos, n)\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 = + ((\(ap, pos, n)\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: + "\ ap bp cp. aprog = ap [+] bp [+] cp \ + length ap = (\(ap, pos, n)\map rec_ci gs. length ap) + + 6 *length gs + 3 * n + length a \ 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 + "\stp. abc_steps_l + ((\(ap, pos, n)\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 = + ((\(ap, pos, n)\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 \ length ap = + (\(ap, pos, n)\map rec_ci gs. length ap) + 6 * length gs + + 3 * n + length a \ 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 \ pstr \ ba \ 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 \ + \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: + "\length lm = n\ \ + \ 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 \ list = drop (Suc n) lm" +apply(induct n arbitrary: lm a list, simp) +apply(case_tac "lm", simp, simp) +done + +lemma empty_boxes_ex: "\length lm \ n\ + \ \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 \ length lm" "drop n lm = a # list" + thus "\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: + "\rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); + rec_ci f = (a, aa, ba); + Max (set (Suc n # ba # map (\(aprog, p, n). n) + (map rec_ci (f # gs)))) = pstr\ + \ \ ap bp cp. aprog = ap [+] bp [+] cp \ + length ap = (\(ap, pos, n)\map rec_ci gs. length ap) + + 6 *length gs + 3 * n + length a + 3 \ 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 (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) [+] + mv_boxes 0 (Suc (max (Suc n) (Max + (insert ba (((\(aprog, p, n). n) \ rec_ci) ` set gs))) + length gs)) n + [+] mv_boxes (max (Suc n) (Max (insert ba + (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) 0 (length gs) [+] + a [+] recursive.empty aa (max (Suc n) + (Max (insert ba (((\(aprog, p, n). n) \ rec_ci) ` set gs))))" + in exI, simp add: cn_merge_gs_len) +apply(rule_tac x = " recursive.empty (max (Suc n) (Max (insert ba + (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) n [+] + mv_boxes (Suc (max (Suc n) (Max (insert ba + (((\(aprog, p, n). n) \ 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" + "\k(aprog, p, n). n) + (map rec_ci (f # gs))))" + and starts: "ss = (\(ap, pos, n)\map rec_ci gs. length ap) + + 6 * length gs + 3 * n + length a + 3" + shows "\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: + "\ ap bp cp. aprog = ap [+] bp [+] cp \ + length ap = (\(ap, pos, n)\map rec_ci gs. length ap) + + 6 *length gs + 3 * n + length a + 3 + \ 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 \ 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 \ + length ap = (\(ap, pos, n)\map rec_ci gs. length ap) + + 6 * length gs + 3 * n + length a + 3 \ + 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 \ length gs = aa \ pstr \ ba", simp) + apply(simp add: j1 j2 j3) + done + qed +qed + +(* +lemma [simp]: " n < pstr \ + (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: + "\rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); + rec_ci f = (a, aa, ba); + Max (set (Suc n # ba # map (\(aprog, p, n). n) + (map rec_ci (f # gs)))) = pstr; + ss = (\(ap, pos, n)\map rec_ci gs. length ap) + + 8 * length gs + 3 * n + length a + 3\ + \ \ ap bp cp. aprog = ap [+] bp [+] cp \ length ap = ss \ + 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 (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) [+] + mv_boxes 0 (Suc (max (Suc n) (Max (insert ba (((\(aprog, p, n). n) + \ rec_ci) ` set gs))) + length gs)) n [+] + mv_boxes (max (Suc n) (Max (insert ba + (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) 0 (length gs) [+] + a [+] recursive.empty aa (max (Suc n) + (Max (insert ba (((\(aprog, p, n). n) \ 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 (((\(aprog, p, n). n) \ 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 \ (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" + "\k(aprog, p, n). n) + (map rec_ci (f # gs))))" + and starts: "ss = (\(ap, pos, n)\map rec_ci gs. length ap) + + 8 * length gs + 3 * n + length a + 3" + shows "\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: + "\ ap bp cp. aprog = ap [+] bp [+] cp \ length ap = ss \ + 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 \ length ap = ss \ + 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 \ [] \ length xs \ Suc 0" +by(case_tac xs, auto) + +lemma [simp]: "n < max (Suc n) (max ba (Max (((\(aprog, p, n). n) o + rec_ci) ` set gs)))" +by(simp) + +lemma restore_paras_prog_ex: + "\rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); + rec_ci f = (a, aa, ba); + Max (set (Suc n # ba # map (\(aprog, p, n). n) + (map rec_ci (f # gs)))) = pstr; + ss = (\(ap, pos, n)\map rec_ci gs. length ap) + + 8 * length gs + 3 * n + length a + 6\ + \ \ ap bp cp. aprog = ap [+] bp [+] cp \ length ap = ss \ + 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 (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) + [+] mv_boxes 0 (Suc (max (Suc n) + (Max (insert ba (((\(aprog, p, n). n) \ rec_ci) ` set gs))) + + length gs)) n [+] mv_boxes (max (Suc n) + (Max (insert ba (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) 0 (length gs) [+] + a [+] recursive.empty aa (max (Suc n) + (Max (insert ba (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) [+] + empty_boxes (length gs) [+] + recursive.empty (max (Suc n) (Max (insert ba + (((\(aprog, p, n). n) \ 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" + "\k(aprog, p, n). n) + (map rec_ci (f # gs))))" + and starts: "ss = (\(ap, pos, n)\map rec_ci gs. length ap) + + 8 * length gs + 3 * n + length a + 6" + shows "\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: + "\ ap bp cp. aprog = ap [+] bp [+] cp \ length ap = ss \ + 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 \ length ap = ss \ + 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 \ + a_md > pstr + length gs + n \ 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: + "\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)\ + \ length aprog = (\(ap, pos, n)\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: + "\x aprog a_md rs_pos rs suf_lm lm. + \x \ set (f # gs); + rec_ci x = (aprog, rs_pos, a_md); + rec_calc_rel x lm rs\ + \ \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 "\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 (\(aprog, p, n). n) + (map rec_ci (f # gs)))))" + let ?gs_len = "listsum (map (\ (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" + "\k 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: + "\ 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: + "\ 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: + "\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: + "\ 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: + "\ 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: + "\ 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: "\ 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 + "\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: + "\rec_ci recf = (ap, arity, fp); + rec_calc_rel recf args r\ + \ (\ 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: + "\ap fp arity r anything args. + \aa = ap \ ba = arity \ ca = fp; rec_calc_rel f args r\ \ + \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: + "\x xa y xb ya ap fp arity r anything args. + \x = (aa, ba, ca); xa = aa \ y = (ba, ca); xb = ba \ ya = ca; + a = ap \ b = arity \ c = fp; rec_calc_rel g args r\ + \ \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: + "\ args r anything. rec_calc_rel f args r \ + \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: + "\ args r anything. rec_calc_rel g args r \ + \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 + "\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 "\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 + "\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 "\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: "\x ap fp arity r anything args. + \x \ set (f # gs); + rec_ci x = (ap, arity, fp); + rec_calc_rel x args r\ + \ \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 + "\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: + "\ap fp arity r anything args. + \rec_ci f = (ap, arity, fp); rec_calc_rel f args r\ \ + \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 + "\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: + "\\ stp. (\ (ss, e). ss < length bp) (abc_steps_l (0, lm) bp stp); + p = ap [+] bp [+] cp\ + \ \ stp. (\ (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: + "\abc_steps_l (0, am) ap stp = (length ap, lm); bp \ []; + \ stp. (\ (ss, e). ss < length bp) (abc_steps_l (0, lm) bp stp); + p = ap [+] bp [+] cp\ + \ \ stp. (\ (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 \ []" + "\ stp. (\ (ss, e). ss < length bp) (abc_steps_l (0, lm) bp stp)" + "p = ap [+] bp [+] cp" + have "\ 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: "\ stp. (\ (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 + "\ stp. (\ (ss, e). ss < length p) + (abc_steps_l (0, am) p (stpa + stp))" + apply(simp add: abc_steps_add) + done + thus "\ stp. (\ (ss, e). ss < length p) + (abc_steps_l (0, am) p stp)" + apply(rule_tac allI, auto) + apply(case_tac "stp \ 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)" + "\ stpa \ stp" + thus "a < length p" + using g1 h + apply(case_tac "a < length p", simp, simp) + apply(subgoal_tac "\ 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: "\ y. (\ rs. rec_calc_rel f (lm @ [y]) rs \ rs \ 0)" + shows "\ stp. case abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suf_lm) + aprog stp of (ss, e) \ 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')" + "\y. \rs. rec_calc_rel f (lm @ [y]) rs \ rs \ 0" "length lm = n" + thm mn_ind_step + have "\stpa \ 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 "\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 \ 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 "\rs. rec_calc_rel f (lm @ [stp]) rs \ rs \ 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 \ rs \ 0" .. + hence "\ 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 "\stpa\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 \ stpa \ 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) \ 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 \ length aprog", + simp, simp) + apply(subgoal_tac "\ 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!]: + "\ap = bp; cp = dp\ \ ap [+] cp = bp [+] dp" +by simp + +lemma cn_merge_gs_split: + "\i < length gs; rec_ci (gs!i) = (ga, gb, gc)\ \ + 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 \gi, gi+1, \ gn"}, this lemma describes what + happens when every one of @{text "g1, g2, \ gi"} terminates, but + @{text "gi+1"} does not terminate, so that whole function @{text "Cn f g1 g2 \gi, gi+1, \ 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: "\ j < i. (\ rs. rec_calc_rel (gs!j) lm rs)" + and unhalt_condition: "\ slm. \ stp. case abc_steps_l (0, lm @ 0\<^bsup>gc - gb\<^esup> @ slm) + ga stp of (se, e) \ se < length ga" + shows " \ stp. case abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suflm) aprog + stp of (ss, e) \ 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: "\jrs. rec_calc_rel (gs ! j) lm rs" + "i < length gs" + and ind: + "\ slm. \ stp. case abc_steps_l (0, lm @ 0\<^bsup>gc - n\<^esup> @ slm) ga stp of (se, e) \ se < length ga" + have h3: "rs_pos = n" + using h1 + by(rule_tac ci_cn_para_eq, simp) + let ?ggs = "take i gs" + have "\ ys. (length ys = i \ + (\ 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 \ (\ k < i. rec_calc_rel (?ggs ! k) + lm (ys ! k)))" .. + let ?pstr = "Max (set (Suc n # c # map (\(aprog, p, n). n) + (map rec_ci (f # gs))))" + have "\stp. abc_steps_l (0, lm @ 0\<^bsup>a_md - n\<^esup> @ suflm) + (cn_merge_gs (map rec_ci ?ggs) ?pstr) stp = + (listsum (map ((\(ap, pos, n). length ap) \ 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 \ 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 ((\(ap, pos, n). length ap) \ rec_ci) ?ggs) + + 3 * length ?ggs, lm @ 0\<^bsup>?pstr - n\<^esup> @ ys @ 0\<^bsup>a_md -(?pstr + length ?ggs)\<^esup> @ + suflm)" .. + moreover have + "\ 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 + (((\(aprog, p, n). n) \ rec_ci) ` set gs))) + + length gs)) n [+] mv_boxes (max (Suc n) (Max (insert c + (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) 0 (length gs) [+] + a [+] recursive.empty b (max (Suc n) + (Max (insert c (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) [+] + empty_boxes (length gs) [+] recursive.empty (max (Suc n) + (Max (insert c (((\(aprog, p, n). n) \ rec_ci) ` set gs)))) n [+] + mv_boxes (Suc (max (Suc n) (Max (insert c + (((\(aprog, p, n). n) \ 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 (((\(aprog, p, n). n) \ 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 "\ stp. case abc_steps_l (0, lm @ 0\<^bsup>a_md - rs_pos\<^esup> @ suflm) + aprog stp of (ss, e) \ 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 \ []" + using h1 + apply(simp add: rec_ci_not_null) + done + next + show "\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) \ 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 \ ?pstr \ 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': + "\rec_ci re = (ap, ary, fp); + rec_calc_rel re args r\ + \ (\ 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 \ abc_inst list" +where +"dummy_abc k = [Inc k, Dec k 0, Goto 3]" + +lemma abc_rec_halt_eq'': + "\rec_ci re = (aprog, rs_pos, a_md); + rec_calc_rel re lm rs\ + \ (\ stp lm' m. (abc_steps_l (0, lm) aprog stp) = + (length aprog, lm') \ 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) \ []" +apply(simp add: dummy_abc_def) +done + +lemma dummy_abc_steps_ex: + "\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> \ + \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 \ n" + apply(drule_tac list_length) + apply(simp) + done + hence "\ 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: "\ 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 \ (Suc (length lm) - length lm')" + using h g + apply(drule_tac list_length) + apply(simp) + done + ultimately show + "\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>) + \ \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: + "\rec_ci recf = (ap, ary, fp); + rec_calc_rel recf args r; + length args = k\ + \ (\ 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 "\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 "\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 \ 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: + "\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)\ + \ \ stp m l. steps (Suc 0, Bk # Bk # ires, @ 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 (\(acn, s). s \ Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))) xs \ + list_all (\(acn, s). s \ 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]: "\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 \ 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]: "\k < length ap; ap ! k = Inc n; + (a, b) \ set (tshift (tshift tinc_b (2 * n)) + (start_of (layout_of ap) k - Suc 0))\ + \ b \ start_of (layout_of ap) (length ap)" +apply(subgoal_tac "b \ start_of (layout_of ap) (Suc k)") +apply(subgoal_tac "start_of (layout_of ap) (Suc k) \ 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) \ set (tshift (findnth n) (start_of (layout_of ap) k - Suc 0)) + \ b \ 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]: "\k < length ap; ap ! k = Inc n; (a, b) \ + set (tshift (findnth n) (start_of (layout_of ap) k - Suc 0))\ + \ b \ start_of (layout_of ap) (length ap)" +apply(subgoal_tac "b \ start_of (layout_of ap) (Suc k)") +apply(subgoal_tac "start_of (layout_of ap) (Suc k) \ 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 \ start_of (layout_of ap) k + 2*n + 1 \ + start_of (layout_of ap) k + 2*n + 1 \ 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 \ 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 \ start_of (layout_of ap) (length ap)" +apply(subgoal_tac "as > length ap \ as = length ap \ as < length ap", + auto simp: start_of_eq start_of_le) +done + +lemma [elim]: "\k < length ap; + ap ! k = Dec n e; + (a, b) \ set (tshift (findnth n) (start_of (layout_of ap) k - Suc 0))\ + \ b \ start_of (layout_of ap) (length ap)" +apply(subgoal_tac "b \ start_of (layout_of ap) k + 2*n + 1 \ + start_of (layout_of ap) k + 2*n + 1 \ start_of (layout_of ap) (Suc k) \ + start_of (layout_of ap) (Suc k) \ 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]: "\k < length ap; ap ! k = Dec n e; (a, b) \ set (tshift (tshift tdec_b (2 * n)) + (start_of (layout_of ap) k - Suc 0))\ + \ b \ start_of (layout_of ap) (length ap)" +apply(subgoal_tac "2*n + start_of (layout_of ap) k + 16 \ start_of (layout_of ap) (length ap) \ 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) + \ start_of (layout_of ap) (Suc k) \ 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: "\k < length ap; (a, b) \ set (tms_of ap ! k)\ \ b \ 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) \ \k < length xs. concat xs ! i \ 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) \ \ k < length ap. (tm_of ap ! i) \ 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 (\(acn, s). s \ 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: "\k < length ap; length (ci ly y (ap ! k)) = 2 * qa\ + \ 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 \ (\(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) \ length ap \ + 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: "\(ap::'a list). length ys \ length ap \ + zip ys ap = zip ys (take (length ys) ap)" + and h: "length (a # ys) \ 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: + "\k \ length ap; length ss = k\ \ start_of (layout_of ap) k = + Suc (listsum (map (length \ (\(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: "\ss. length ss = k \ start_of (layout_of ap) k = + Suc (listsum (map (length \ (\(x, y). ci ly x y)) (zip ss ap)) div 2)" + and h: "Suc k \ length ap" "length (ss::nat list) = Suc k" + have "\ 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 \ (\(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 \ (\(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 \ (\(x, y). ci ly x y)) (zip ys (take k ap))) mod 2 = 0 \ + 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 (\(acn, s). s \ Suc q) xs + \ list_all (\(acn, s). s \ 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]: "\na < 4 * n; tshift (mop_bef n) q ! na = (a, b)\ \ b \ 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 \ na = 1 + 4*n \ na = 2 + 4*n \ na = 3 + 4*n", + auto simp: shift_length) +apply(simp_all add: tshift.simps) +done + +lemma mp_up_all_le: "list_all (\(acn, s). s \ 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 (\(acn, s). s \ 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 \ 0 \ 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: + "\tp = tm_of ap; ly = layout_of ap; mop_ss = start_of ly (length ap)\ \ + 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 + + + + + + +