diff -r 0b302c0b449a -r 469c26d19f8e recursive.thy --- a/recursive.thy Wed Feb 06 02:25:00 2013 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5024 +0,0 @@ -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 - - - - - - -