1144 aprog = ap [+] bp \<and> |
1144 aprog = ap [+] bp \<and> |
1145 bp = ([Dec (a_md - Suc 0) (length a + 7)] [+] (a [+] |
1145 bp = ([Dec (a_md - Suc 0) (length a + 7)] [+] (a [+] |
1146 [Inc (rs_pos - Suc 0), Dec rs_pos 3, Goto (Suc 0)])) @ |
1146 [Inc (rs_pos - Suc 0), Dec rs_pos 3, Goto (Suc 0)])) @ |
1147 [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]" |
1147 [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]" |
1148 apply(simp add: rec_ci.simps) |
1148 apply(simp add: rec_ci.simps) |
1149 apply(rule_tac x = "Recursive.mv_box n (max (Suc (Suc (Suc n))) |
1149 apply(rule_tac x = "mv_box n (max (Suc (Suc (Suc n))) |
1150 (max bc ba)) [+] ab [+] Recursive.mv_box n (Suc n)" in exI, |
1150 (max bc ba)) [+] ab [+] mv_box n (Suc n)" in exI, |
1151 simp) |
1151 simp) |
1152 apply(auto simp add: abc_append_commute numeral_3_eq_3) |
1152 apply(auto simp add: abc_append_commute numeral_3_eq_3) |
1153 done |
1153 done |
1154 |
1154 |
1155 lemma pr_cycle_part: |
1155 lemma pr_cycle_part: |
1355 apply(simp add: abc_steps_l.simps mv_box_inv.simps) |
1355 apply(simp add: abc_steps_l.simps mv_box_inv.simps) |
1356 apply(rule_tac x = "initlm ! m" in exI, |
1356 apply(rule_tac x = "initlm ! m" in exI, |
1357 rule_tac x = "initlm ! n" in exI, simp) |
1357 rule_tac x = "initlm ! n" in exI, simp) |
1358 done |
1358 done |
1359 |
1359 |
1360 lemma [simp]: "abc_fetch 0 (Recursive.mv_box m n) = Some (Dec m 3)" |
1360 lemma [simp]: "abc_fetch 0 (mv_box m n) = Some (Dec m 3)" |
1361 apply(simp add: mv_box.simps abc_fetch.simps) |
1361 apply(simp add: mv_box.simps abc_fetch.simps) |
1362 done |
1362 done |
1363 |
1363 |
1364 lemma [simp]: "abc_fetch (Suc 0) (Recursive.mv_box m n) = |
1364 lemma [simp]: "abc_fetch (Suc 0) (mv_box m n) = |
1365 Some (Inc n)" |
1365 Some (Inc n)" |
1366 apply(simp add: mv_box.simps abc_fetch.simps) |
1366 apply(simp add: mv_box.simps abc_fetch.simps) |
1367 done |
1367 done |
1368 |
1368 |
1369 lemma [simp]: "abc_fetch 2 (Recursive.mv_box m n) = Some (Goto 0)" |
1369 lemma [simp]: "abc_fetch 2 (mv_box m n) = Some (Goto 0)" |
1370 apply(simp add: mv_box.simps abc_fetch.simps) |
1370 apply(simp add: mv_box.simps abc_fetch.simps) |
1371 done |
1371 done |
1372 |
1372 |
1373 lemma [simp]: "abc_fetch 3 (Recursive.mv_box m n) = None" |
1373 lemma [simp]: "abc_fetch 3 (mv_box m n) = None" |
1374 apply(simp add: mv_box.simps abc_fetch.simps) |
1374 apply(simp add: mv_box.simps abc_fetch.simps) |
1375 done |
1375 done |
1376 |
1376 |
1377 lemma [simp]: |
1377 lemma [simp]: |
1378 "\<lbrakk>m \<noteq> n; m < length initlm; n < length initlm; |
1378 "\<lbrakk>m \<noteq> n; m < length initlm; n < length initlm; |
1403 done |
1403 done |
1404 |
1404 |
1405 lemma [simp]: |
1405 lemma [simp]: |
1406 "\<lbrakk>length initlm > max m n; m \<noteq> n\<rbrakk> \<Longrightarrow> |
1406 "\<lbrakk>length initlm > max m n; m \<noteq> n\<rbrakk> \<Longrightarrow> |
1407 \<forall>na. \<not> (\<lambda>(as, lm) m. as = 3) |
1407 \<forall>na. \<not> (\<lambda>(as, lm) m. as = 3) |
1408 (abc_steps_l (0, initlm) (Recursive.mv_box m n) na) m \<and> |
1408 (abc_steps_l (0, initlm) (mv_box m n) na) m \<and> |
1409 mv_box_inv (abc_steps_l (0, initlm) |
1409 mv_box_inv (abc_steps_l (0, initlm) |
1410 (Recursive.mv_box m n) na) m n initlm \<longrightarrow> |
1410 (mv_box m n) na) m n initlm \<longrightarrow> |
1411 mv_box_inv (abc_steps_l (0, initlm) |
1411 mv_box_inv (abc_steps_l (0, initlm) |
1412 (Recursive.mv_box m n) (Suc na)) m n initlm \<and> |
1412 (mv_box m n) (Suc na)) m n initlm \<and> |
1413 ((abc_steps_l (0, initlm) (Recursive.mv_box m n) (Suc na), m), |
1413 ((abc_steps_l (0, initlm) (mv_box m n) (Suc na), m), |
1414 abc_steps_l (0, initlm) (Recursive.mv_box m n) na, m) \<in> mv_box_LE" |
1414 abc_steps_l (0, initlm) (mv_box m n) na, m) \<in> mv_box_LE" |
1415 apply(rule allI, rule impI, simp add: abc_steps_ind) |
1415 apply(rule allI, rule impI, simp add: abc_steps_ind) |
1416 apply(case_tac "(abc_steps_l (0, initlm) (Recursive.mv_box m n) na)", |
1416 apply(case_tac "(abc_steps_l (0, initlm) (mv_box m n) na)", |
1417 simp) |
1417 simp) |
1418 apply(auto split:if_splits simp add:abc_steps_l.simps mv_box_inv.simps) |
1418 apply(auto split:if_splits simp add:abc_steps_l.simps mv_box_inv.simps) |
1419 apply(auto simp add: mv_box_LE_def lex_triple_def lex_pair_def |
1419 apply(auto simp add: mv_box_LE_def lex_triple_def lex_pair_def |
1420 abc_step_l.simps abc_steps_l.simps |
1420 abc_step_l.simps abc_steps_l.simps |
1421 mv_box_inv.simps abc_lm_v.simps abc_lm_s.simps |
1421 mv_box_inv.simps abc_lm_v.simps abc_lm_s.simps |
1428 \<exists> stp. (\<lambda> (as, lm). as = 3 \<and> |
1428 \<exists> stp. (\<lambda> (as, lm). as = 3 \<and> |
1429 mv_box_inv (as, lm) m n initlm) |
1429 mv_box_inv (as, lm) m n initlm) |
1430 (abc_steps_l (0::nat, initlm) (mv_box m n) stp)" |
1430 (abc_steps_l (0::nat, initlm) (mv_box m n) stp)" |
1431 apply(insert halt_lemma2[of mv_box_LE |
1431 apply(insert halt_lemma2[of mv_box_LE |
1432 "\<lambda> ((as, lm), m). mv_box_inv (as, lm) m n initlm" |
1432 "\<lambda> ((as, lm), m). mv_box_inv (as, lm) m n initlm" |
1433 "\<lambda> stp. (abc_steps_l (0, initlm) (Recursive.mv_box m n) stp, m)" |
1433 "\<lambda> stp. (abc_steps_l (0, initlm) (mv_box m n) stp, m)" |
1434 "\<lambda> ((as, lm), m). as = (3::nat)" |
1434 "\<lambda> ((as, lm), m). as = (3::nat)" |
1435 ]) |
1435 ]) |
1436 apply(insert wf_mv_box_le) |
1436 apply(insert wf_mv_box_le) |
1437 apply(simp add: mv_box_inv_init abc_steps_zero) |
1437 apply(simp add: mv_box_inv_init abc_steps_zero) |
1438 apply(erule_tac exE) |
1438 apply(erule_tac exE) |
1439 apply(rule_tac x = na in exI) |
1439 apply(rule_tac x = na in exI) |
1440 apply(case_tac "(abc_steps_l (0, initlm) (Recursive.mv_box m n) na)", |
1440 apply(case_tac "(abc_steps_l (0, initlm) (mv_box m n) na)", |
1441 simp, auto) |
1441 simp, auto) |
1442 done |
1442 done |
1443 |
1443 |
1444 lemma mv_box_halt_cond: |
1444 lemma mv_box_halt_cond: |
1445 "\<lbrakk>m \<noteq> n; mv_box_inv (a, b) m n lm; a = 3\<rbrakk> \<Longrightarrow> |
1445 "\<lbrakk>m \<noteq> n; mv_box_inv (a, b) m n lm; a = 3\<rbrakk> \<Longrightarrow> |
1452 "\<lbrakk>length lm > max m n; m \<noteq> n\<rbrakk> \<Longrightarrow> |
1452 "\<lbrakk>length lm > max m n; m \<noteq> n\<rbrakk> \<Longrightarrow> |
1453 \<exists> stp. abc_steps_l (0::nat, lm) (mv_box m n) stp |
1453 \<exists> stp. abc_steps_l (0::nat, lm) (mv_box m n) stp |
1454 = (3, (lm[n := (lm ! m + lm ! n)])[m := 0::nat])" |
1454 = (3, (lm[n := (lm ! m + lm ! n)])[m := 0::nat])" |
1455 apply(drule mv_box_inv_halt, simp, erule_tac exE) |
1455 apply(drule mv_box_inv_halt, simp, erule_tac exE) |
1456 apply(rule_tac x = stp in exI) |
1456 apply(rule_tac x = stp in exI) |
1457 apply(case_tac "abc_steps_l (0, lm) (Recursive.mv_box m n) stp", |
1457 apply(case_tac "abc_steps_l (0, lm) (mv_box m n) stp", |
1458 simp) |
1458 simp) |
1459 apply(erule_tac mv_box_halt_cond, auto) |
1459 apply(erule_tac mv_box_halt_cond, auto) |
1460 done |
1460 done |
1461 |
1461 |
1462 lemma [simp]: |
1462 lemma [simp]: |
1508 rec_ci g = (a, aa, ba); |
1508 rec_ci g = (a, aa, ba); |
1509 rec_ci f = (ab, ac, bc)\<rbrakk> |
1509 rec_ci f = (ab, ac, bc)\<rbrakk> |
1510 \<Longrightarrow> \<exists>ap bp. aprog = ap [+] bp \<and> |
1510 \<Longrightarrow> \<exists>ap bp. aprog = ap [+] bp \<and> |
1511 ap = mv_box n (max (Suc (Suc (Suc n))) (max bc ba))" |
1511 ap = mv_box n (max (Suc (Suc (Suc n))) (max bc ba))" |
1512 apply(simp add: rec_ci.simps) |
1512 apply(simp add: rec_ci.simps) |
1513 apply(rule_tac x = "(ab [+] (Recursive.mv_box n (Suc n) [+] |
1513 apply(rule_tac x = "(ab [+] (mv_box n (Suc n) [+] |
1514 ([Dec (max (n + 3) (max bc ba)) (length a + 7)] |
1514 ([Dec (max (n + 3) (max bc ba)) (length a + 7)] |
1515 [+] (a [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) @ |
1515 [+] (a [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) @ |
1516 [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]))" in exI, auto) |
1516 [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]))" in exI, auto) |
1517 apply(simp add: abc_append_commute numeral_3_eq_3) |
1517 apply(simp add: abc_append_commute numeral_3_eq_3) |
1518 done |
1518 done |
1613 apply(case_tac "lm = []", auto) |
1613 apply(case_tac "lm = []", auto) |
1614 done |
1614 done |
1615 |
1615 |
1616 lemma pr_prog_ex[simp]: "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md); |
1616 lemma pr_prog_ex[simp]: "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md); |
1617 rec_ci g = (a, aa, ba); rec_ci f = (ab, ac, bc)\<rbrakk> |
1617 rec_ci g = (a, aa, ba); rec_ci f = (ab, ac, bc)\<rbrakk> |
1618 \<Longrightarrow> \<exists>cp. aprog = Recursive.mv_box n (max (n + 3) |
1618 \<Longrightarrow> \<exists>cp. aprog = mv_box n (max (n + 3) |
1619 (max bc ba)) [+] cp" |
1619 (max bc ba)) [+] cp" |
1620 apply(simp add: rec_ci.simps) |
1620 apply(simp add: rec_ci.simps) |
1621 apply(rule_tac x = "(ab [+] (Recursive.mv_box n (Suc n) [+] |
1621 apply(rule_tac x = "(ab [+] (mv_box n (Suc n) [+] |
1622 ([Dec (max (n + 3) (max bc ba)) (length a + 7)] |
1622 ([Dec (max (n + 3) (max bc ba)) (length a + 7)] |
1623 [+] (a [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) |
1623 [+] (a [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) |
1624 @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]))" in exI) |
1624 @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]))" in exI) |
1625 apply(auto simp: abc_append_commute) |
1625 apply(auto simp: abc_append_commute) |
1626 done |
1626 done |
1637 rec_ci f = (ab, ac, bc)\<rbrakk> \<Longrightarrow> |
1637 rec_ci f = (ab, ac, bc)\<rbrakk> \<Longrightarrow> |
1638 \<exists>ap. (\<exists>cp. aprog = ap [+] ab [+] cp) \<and> length ap = 3" |
1638 \<exists>ap. (\<exists>cp. aprog = ap [+] ab [+] cp) \<and> length ap = 3" |
1639 apply(case_tac "rec_ci g", simp add: rec_ci.simps) |
1639 apply(case_tac "rec_ci g", simp add: rec_ci.simps) |
1640 apply(rule_tac x = "mv_box n |
1640 apply(rule_tac x = "mv_box n |
1641 (max (n + 3) (max bc c))" in exI, simp) |
1641 (max (n + 3) (max bc c))" in exI, simp) |
1642 apply(rule_tac x = "Recursive.mv_box n (Suc n) [+] |
1642 apply(rule_tac x = "mv_box n (Suc n) [+] |
1643 ([Dec (max (n + 3) (max bc c)) (length a + 7)] |
1643 ([Dec (max (n + 3) (max bc c)) (length a + 7)] |
1644 [+] a [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)]) |
1644 [+] a [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)]) |
1645 @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]" in exI, |
1645 @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]" in exI, |
1646 auto) |
1646 auto) |
1647 apply(simp add: abc_append_commute) |
1647 apply(simp add: abc_append_commute) |
1649 |
1649 |
1650 lemma [intro]: |
1650 lemma [intro]: |
1651 "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md); |
1651 "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md); |
1652 rec_ci g = (a, aa, ba); |
1652 rec_ci g = (a, aa, ba); |
1653 rec_ci f = (ab, ac, bc)\<rbrakk> \<Longrightarrow> |
1653 rec_ci f = (ab, ac, bc)\<rbrakk> \<Longrightarrow> |
1654 \<exists>ap. (\<exists>cp. aprog = ap [+] Recursive.mv_box n (Suc n) [+] cp) |
1654 \<exists>ap. (\<exists>cp. aprog = ap [+] mv_box n (Suc n) [+] cp) |
1655 \<and> length ap = 3 + length ab" |
1655 \<and> length ap = 3 + length ab" |
1656 apply(simp add: rec_ci.simps) |
1656 apply(simp add: rec_ci.simps) |
1657 apply(rule_tac x = "Recursive.mv_box n (max (n + 3) |
1657 apply(rule_tac x = "mv_box n (max (n + 3) |
1658 (max bc ba)) [+] ab" in exI, simp) |
1658 (max bc ba)) [+] ab" in exI, simp) |
1659 apply(rule_tac x = "([Dec (max (n + 3) (max bc ba)) |
1659 apply(rule_tac x = "([Dec (max (n + 3) (max bc ba)) |
1660 (length a + 7)] [+] a [+] |
1660 (length a + 7)] [+] a [+] |
1661 [Inc n, Dec (Suc n) 3, Goto (Suc 0)]) @ |
1661 [Inc n, Dec (Suc n) 3, Goto (Suc 0)]) @ |
1662 [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]" in exI) |
1662 [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]" in exI) |
1671 [+] (a [+] [Inc (rs_pos - Suc 0), Dec rs_pos 3, |
1671 [+] (a [+] [Inc (rs_pos - Suc 0), Dec rs_pos 3, |
1672 Goto (Suc 0)])) @ [Dec (Suc (Suc n)) 0, Inc (Suc n), |
1672 Goto (Suc 0)])) @ [Dec (Suc (Suc n)) 0, Inc (Suc n), |
1673 Goto (length a + 4)] [+] cp) \<and> |
1673 Goto (length a + 4)] [+] cp) \<and> |
1674 length ap = 6 + length ab" |
1674 length ap = 6 + length ab" |
1675 apply(simp add: rec_ci.simps) |
1675 apply(simp add: rec_ci.simps) |
1676 apply(rule_tac x = "Recursive.mv_box n |
1676 apply(rule_tac x = "mv_box n |
1677 (max (n + 3) (max bc ba)) [+] ab [+] |
1677 (max (n + 3) (max bc ba)) [+] ab [+] |
1678 Recursive.mv_box n (Suc n)" in exI, simp) |
1678 mv_box n (Suc n)" in exI, simp) |
1679 apply(rule_tac x = "[]" in exI, auto) |
1679 apply(rule_tac x = "[]" in exI, auto) |
1680 apply(simp add: abc_append_commute) |
1680 apply(simp add: abc_append_commute) |
1681 done |
1681 done |
1682 |
1682 |
1683 lemma [simp]: |
1683 lemma [simp]: |
1749 done |
1749 done |
1750 thus "?thesis" |
1750 thus "?thesis" |
1751 apply(erule_tac exE, erule_tac exE, simp) |
1751 apply(erule_tac exE, erule_tac exE, simp) |
1752 apply(subgoal_tac |
1752 apply(subgoal_tac |
1753 "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) |
1753 "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) |
1754 ([] [+] Recursive.mv_box n |
1754 ([] [+] mv_box n |
1755 (max (n + 3) (max bc ba)) [+] cp) stp = |
1755 (max (n + 3) (max bc ba)) [+] cp) stp = |
1756 (0 + 3, butlast lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ |
1756 (0 + 3, butlast lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ |
1757 last lm # suf_lm)", simp) |
1757 last lm # suf_lm)", simp) |
1758 apply(rule_tac abc_append_exc1, simp_all) |
1758 apply(rule_tac abc_append_exc1, simp_all) |
1759 apply(insert mv_box_ex[of "n" "(max (n + 3) |
1759 apply(insert mv_box_ex[of "n" "(max (n + 3) |
1815 0\<up>(a_md - rs_pos - 1) @ last lm # suf_lm) aprog stp |
1815 0\<up>(a_md - rs_pos - 1) @ last lm # suf_lm) aprog stp |
1816 = (6 + length ab, butlast lm @ 0 # rsa # |
1816 = (6 + length ab, butlast lm @ 0 # rsa # |
1817 0\<up>(a_md - rs_pos - 2) @ last lm # suf_lm)" |
1817 0\<up>(a_md - rs_pos - 2) @ last lm # suf_lm)" |
1818 proof - |
1818 proof - |
1819 from h have "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> |
1819 from h have "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> |
1820 length ap = 3 + length ab \<and> bp = Recursive.mv_box n (Suc n)" |
1820 length ap = 3 + length ab \<and> bp = mv_box n (Suc n)" |
1821 by auto |
1821 by auto |
1822 thus "?thesis" |
1822 thus "?thesis" |
1823 proof(erule_tac exE, erule_tac exE, erule_tac exE, |
1823 proof(erule_tac exE, erule_tac exE, erule_tac exE, |
1824 erule_tac exE) |
1824 erule_tac exE) |
1825 fix ap cp bp apa |
1825 fix ap cp bp apa |
1826 assume "aprog = ap [+] bp [+] cp \<and> length ap = 3 + |
1826 assume "aprog = ap [+] bp [+] cp \<and> length ap = 3 + |
1827 length ab \<and> bp = Recursive.mv_box n (Suc n)" |
1827 length ab \<and> bp = mv_box n (Suc n)" |
1828 thus "?thesis" |
1828 thus "?thesis" |
1829 apply(simp del: abc_append_commute) |
1829 apply(simp del: abc_append_commute) |
1830 apply(subgoal_tac |
1830 apply(subgoal_tac |
1831 "\<exists>stp. abc_steps_l (3 + length ab, |
1831 "\<exists>stp. abc_steps_l (3 + length ab, |
1832 butlast lm @ rsa # 0\<up>(a_md - Suc rs_pos) @ |
1832 butlast lm @ rsa # 0\<up>(a_md - Suc rs_pos) @ |
1833 last lm # suf_lm) (ap [+] |
1833 last lm # suf_lm) (ap [+] |
1834 Recursive.mv_box n (Suc n) [+] cp) stp = |
1834 mv_box n (Suc n) [+] cp) stp = |
1835 ((3 + length ab) + 3, butlast lm @ 0 # rsa # |
1835 ((3 + length ab) + 3, butlast lm @ 0 # rsa # |
1836 0\<up>(a_md - Suc (Suc rs_pos)) @ last lm # suf_lm)", simp) |
1836 0\<up>(a_md - Suc (Suc rs_pos)) @ last lm # suf_lm)", simp) |
1837 apply(rule_tac abc_append_exc1, simp_all) |
1837 apply(rule_tac abc_append_exc1, simp_all) |
1838 apply(insert mv_box_ex[of n "Suc n" |
1838 apply(insert mv_box_ex[of n "Suc n" |
1839 "butlast lm @ rsa # 0\<up>(a_md - Suc rs_pos) @ |
1839 "butlast lm @ rsa # 0\<up>(a_md - Suc rs_pos) @ |
2809 apply(simp add: cn_merge_gs_length) |
2809 apply(simp add: cn_merge_gs_length) |
2810 proof - |
2810 proof - |
2811 from h show |
2811 from h show |
2812 "\<exists>bstp. abc_steps_l (0, lm @ 0\<up>(pstr - n) @ butlast ys @ |
2812 "\<exists>bstp. abc_steps_l (0, lm @ 0\<up>(pstr - n) @ butlast ys @ |
2813 0\<up>(a_md - (pstr + length list)) @ suf_lm) |
2813 0\<up>(a_md - (pstr + length list)) @ suf_lm) |
2814 ((\<lambda>(gprog, gpara, gn). gprog [+] Recursive.mv_box gpara |
2814 ((\<lambda>(gprog, gpara, gn). gprog [+] mv_box gpara |
2815 (pstr + length list)) (rec_ci a)) bstp = |
2815 (pstr + length list)) (rec_ci a)) bstp = |
2816 ((\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3, |
2816 ((\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3, |
2817 lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - Suc (pstr + length list)) @ suf_lm)" |
2817 lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - Suc (pstr + length list)) @ suf_lm)" |
2818 apply(case_tac "rec_ci a", simp) |
2818 apply(case_tac "rec_ci a", simp) |
2819 apply(rule_tac as = "length aa" and |
2819 apply(rule_tac as = "length aa" and |
2848 fix aa b c |
2848 fix aa b c |
2849 assume "rec_ci a = (aa, b, c)" |
2849 assume "rec_ci a = (aa, b, c)" |
2850 from h and this show |
2850 from h and this show |
2851 "\<exists>bstp. abc_steps_l (0, lm @ ys ! length list # |
2851 "\<exists>bstp. abc_steps_l (0, lm @ ys ! length list # |
2852 0\<up>(pstr - Suc n) @ butlast ys @ 0\<up>(a_md - (pstr + length list)) @ suf_lm) |
2852 0\<up>(pstr - Suc n) @ butlast ys @ 0\<up>(a_md - (pstr + length list)) @ suf_lm) |
2853 (Recursive.mv_box b (pstr + length list)) bstp = |
2853 (mv_box b (pstr + length list)) bstp = |
2854 (3, lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - Suc (pstr + length list)) @ suf_lm)" |
2854 (3, lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - Suc (pstr + length list)) @ suf_lm)" |
2855 apply(insert mv_box_ex [of b "pstr + length list" |
2855 apply(insert mv_box_ex [of b "pstr + length list" |
2856 "lm @ ys ! length list # 0\<up>(pstr - Suc n) @ butlast ys @ |
2856 "lm @ ys ! length list # 0\<up>(pstr - Suc n) @ butlast ys @ |
2857 0\<up>(a_md - (pstr + length list)) @ suf_lm"], simp) |
2857 0\<up>(a_md - (pstr + length list)) @ suf_lm"], simp) |
2858 apply(subgoal_tac "b = n") |
2858 apply(subgoal_tac "b = n") |
2860 apply(erule_tac x = "length list" in allE, simp) |
2860 apply(erule_tac x = "length list" in allE, simp) |
2861 apply(drule para_pattern, simp, simp) |
2861 apply(drule para_pattern, simp, simp) |
2862 done |
2862 done |
2863 next |
2863 next |
2864 fix aa b c |
2864 fix aa b c |
2865 show "3 = length (Recursive.mv_box b (pstr + length list))" |
2865 show "3 = length (mv_box b (pstr + length list))" |
2866 by simp |
2866 by simp |
2867 next |
2867 next |
2868 fix aa b aaa ba |
2868 fix aa b aaa ba |
2869 show "length aa + 3 = length aa + 3" by simp |
2869 show "length aa + 3 = length aa + 3" by simp |
2870 next |
2870 next |
2873 by(simp add: mv_box.simps) |
2873 by(simp add: mv_box.simps) |
2874 qed |
2874 qed |
2875 next |
2875 next |
2876 show "(\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3 = |
2876 show "(\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3 = |
2877 length ((\<lambda>(gprog, gpara, gn). gprog [+] |
2877 length ((\<lambda>(gprog, gpara, gn). gprog [+] |
2878 Recursive.mv_box gpara (pstr + length list)) (rec_ci a))" |
2878 mv_box gpara (pstr + length list)) (rec_ci a))" |
2879 by(case_tac "rec_ci a", simp) |
2879 by(case_tac "rec_ci a", simp) |
2880 next |
2880 next |
2881 show "listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) list) + |
2881 show "listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) list) + |
2882 (\<lambda>(ap, pos, n). length ap) (rec_ci a) + (3 + 3 * length list)= |
2882 (\<lambda>(ap, pos, n). length ap) (rec_ci a) + (3 + 3 * length list)= |
2883 (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci list. length ap) + 3 * length list + |
2883 (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci list. length ap) + 3 * length list + |
2884 ((\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3)" by simp |
2884 ((\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3)" by simp |
2885 next |
2885 next |
2886 show "(\<lambda>(gprog, gpara, gn). gprog [+] |
2886 show "(\<lambda>(gprog, gpara, gn). gprog [+] |
2887 Recursive.mv_box gpara (pstr + length list)) (rec_ci a) \<noteq> []" |
2887 mv_box gpara (pstr + length list)) (rec_ci a) \<noteq> []" |
2888 by(case_tac "rec_ci a", |
2888 by(case_tac "rec_ci a", |
2889 simp add: abc_append.simps abc_shift.simps) |
2889 simp add: abc_append.simps abc_shift.simps) |
2890 qed |
2890 qed |
2891 qed |
2891 qed |
2892 |
2892 |
2981 "length (lm1::nat list) = aa" |
2981 "length (lm1::nat list) = aa" |
2982 "length (lm2::nat list) = Suc n" |
2982 "length (lm2::nat list) = Suc n" |
2983 "length (lm3::nat list) = ba - Suc (aa + n)" |
2983 "length (lm3::nat list) = ba - Suc (aa + n)" |
2984 thus " \<exists>bstp. abc_steps_l (0, lm1 @ 0\<up>n @ last lm2 # lm3 @ |
2984 thus " \<exists>bstp. abc_steps_l (0, lm1 @ 0\<up>n @ last lm2 # lm3 @ |
2985 butlast lm2 @ 0 # lm4) |
2985 butlast lm2 @ 0 # lm4) |
2986 (Recursive.mv_box (aa + n) (ba + n)) bstp |
2986 (mv_box (aa + n) (ba + n)) bstp |
2987 = (3, lm1 @ 0 # 0\<up>n @ lm3 @ lm2 @ lm4)" |
2987 = (3, lm1 @ 0 # 0\<up>n @ lm3 @ lm2 @ lm4)" |
2988 apply(insert mv_box_ex[of "aa + n" "ba + n" |
2988 apply(insert mv_box_ex[of "aa + n" "ba + n" |
2989 "lm1 @ 0\<up>n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4"], simp) |
2989 "lm1 @ 0\<up>n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4"], simp) |
2990 done |
2990 done |
2991 qed |
2991 qed |
3063 "length (lm2::nat list) = aa - Suc (ba + n)" |
3063 "length (lm2::nat list) = aa - Suc (ba + n)" |
3064 "length (lm3::nat list) = Suc n" |
3064 "length (lm3::nat list) = Suc n" |
3065 thus |
3065 thus |
3066 "\<exists>bstp. abc_steps_l (0, lm1 @ butlast lm3 @ 0 # lm2 @ 0\<up>n @ |
3066 "\<exists>bstp. abc_steps_l (0, lm1 @ butlast lm3 @ 0 # lm2 @ 0\<up>n @ |
3067 last lm3 # lm4) |
3067 last lm3 # lm4) |
3068 (Recursive.mv_box (aa + n) (ba + n)) bstp = |
3068 (mv_box (aa + n) (ba + n)) bstp = |
3069 (3, lm1 @ lm3 @ lm2 @ 0 # 0\<up>n @ lm4)" |
3069 (3, lm1 @ lm3 @ lm2 @ 0 # 0\<up>n @ lm4)" |
3070 apply(insert mv_box_ex[of "aa + n" "ba + n" "lm1 @ butlast lm3 @ |
3070 apply(insert mv_box_ex[of "aa + n" "ba + n" "lm1 @ butlast lm3 @ |
3071 0 # lm2 @ 0\<up>n @ last lm3 # lm4"], simp) |
3071 0 # lm2 @ 0\<up>n @ last lm3 # lm4"], simp) |
3072 done |
3072 done |
3073 qed |
3073 qed |
3131 "cn_merge_gs (map rec_ci gs) (max (Suc n) (Max (insert ba |
3131 "cn_merge_gs (map rec_ci gs) (max (Suc n) (Max (insert ba |
3132 (((\<lambda>(aprog, p, n). n) o rec_ci) ` set gs))))" in exI, |
3132 (((\<lambda>(aprog, p, n). n) o rec_ci) ` set gs))))" in exI, |
3133 simp add: cn_merge_gs_len) |
3133 simp add: cn_merge_gs_len) |
3134 apply(rule_tac x = |
3134 apply(rule_tac x = |
3135 "mv_boxes (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) |
3135 "mv_boxes (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) |
3136 0 (length gs) [+] a [+]Recursive.mv_box aa (max (Suc n) |
3136 0 (length gs) [+] a [+]mv_box aa (max (Suc n) |
3137 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] |
3137 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] |
3138 empty_boxes (length gs) [+] Recursive.mv_box (max (Suc n) |
3138 empty_boxes (length gs) [+] mv_box (max (Suc n) |
3139 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+] |
3139 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+] |
3140 mv_boxes (Suc (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) |
3140 mv_boxes (Suc (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) |
3141 ` set gs))) + length gs)) 0 n" in exI, auto) |
3141 ` set gs))) + length gs)) 0 n" in exI, auto) |
3142 apply(simp add: abc_append_commute) |
3142 apply(simp add: abc_append_commute) |
3143 done |
3143 done |
3216 apply(simp add: rec_ci.simps) |
3216 apply(simp add: rec_ci.simps) |
3217 apply(rule_tac x = "mv_boxes 0 (Suc (max (Suc n) |
3217 apply(rule_tac x = "mv_boxes 0 (Suc (max (Suc n) |
3218 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n [+] |
3218 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n [+] |
3219 mv_boxes (max (Suc n) (Max (insert ba |
3219 mv_boxes (max (Suc n) (Max (insert ba |
3220 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+] |
3220 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+] |
3221 a [+] Recursive.mv_box aa (max (Suc n) |
3221 a [+] mv_box aa (max (Suc n) |
3222 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] |
3222 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] |
3223 empty_boxes (length gs) [+] Recursive.mv_box (max (Suc n) |
3223 empty_boxes (length gs) [+] mv_box (max (Suc n) |
3224 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+] |
3224 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+] |
3225 mv_boxes (Suc (max (Suc n) (Max |
3225 mv_boxes (Suc (max (Suc n) (Max |
3226 (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" |
3226 (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" |
3227 in exI) |
3227 in exI) |
3228 apply(auto simp: abc_append_commute) |
3228 apply(auto simp: abc_append_commute) |
3330 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] |
3330 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] |
3331 mv_boxes 0 (Suc (max (Suc n) (Max (insert ba |
3331 mv_boxes 0 (Suc (max (Suc n) (Max (insert ba |
3332 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n" in exI, |
3332 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n" in exI, |
3333 simp add: cn_merge_gs_len) |
3333 simp add: cn_merge_gs_len) |
3334 apply(rule_tac x = "a [+] |
3334 apply(rule_tac x = "a [+] |
3335 Recursive.mv_box aa (max (Suc n) (Max (insert ba |
3335 mv_box aa (max (Suc n) (Max (insert ba |
3336 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] |
3336 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] |
3337 empty_boxes (length gs) [+] Recursive.mv_box |
3337 empty_boxes (length gs) [+] mv_box |
3338 (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n |
3338 (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n |
3339 [+] mv_boxes (Suc (max (Suc n) (Max (insert ba |
3339 [+] mv_boxes (Suc (max (Suc n) (Max (insert ba |
3340 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI, |
3340 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI, |
3341 auto simp: abc_append_commute) |
3341 auto simp: abc_append_commute) |
3342 done |
3342 done |
3421 mv_boxes 0 (Suc (max (Suc n) (Max (insert ba |
3421 mv_boxes 0 (Suc (max (Suc n) (Max (insert ba |
3422 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n [+] |
3422 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n [+] |
3423 mv_boxes (max (Suc n) (Max (insert ba |
3423 mv_boxes (max (Suc n) (Max (insert ba |
3424 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs)" in exI, |
3424 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs)" in exI, |
3425 simp add: cn_merge_gs_len) |
3425 simp add: cn_merge_gs_len) |
3426 apply(rule_tac x = "Recursive.mv_box aa (max (Suc n) (Max (insert ba |
3426 apply(rule_tac x = "mv_box aa (max (Suc n) (Max (insert ba |
3427 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] |
3427 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] |
3428 empty_boxes (length gs) [+] Recursive.mv_box (max (Suc n) ( |
3428 empty_boxes (length gs) [+] mv_box (max (Suc n) ( |
3429 Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+] |
3429 Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+] |
3430 mv_boxes (Suc (max (Suc n) (Max (insert ba |
3430 mv_boxes (Suc (max (Suc n) (Max (insert ba |
3431 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI, |
3431 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI, |
3432 auto simp: abc_append_commute) |
3432 auto simp: abc_append_commute) |
3433 done |
3433 done |
3521 |
3521 |
3522 lemma save_rs': |
3522 lemma save_rs': |
3523 "\<lbrakk>pstr > length ys\<rbrakk> |
3523 "\<lbrakk>pstr > length ys\<rbrakk> |
3524 \<Longrightarrow> \<exists>stp. abc_steps_l (0, ys @ rs # 0\<up>pstr @ lm @ |
3524 \<Longrightarrow> \<exists>stp. abc_steps_l (0, ys @ rs # 0\<up>pstr @ lm @ |
3525 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) |
3525 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) |
3526 (Recursive.mv_box (length ys) pstr) stp = |
3526 (mv_box (length ys) pstr) stp = |
3527 (3, ys @ 0\<up>(pstr - (length ys)) @ rs # |
3527 (3, ys @ 0\<up>(pstr - (length ys)) @ rs # |
3528 0\<up>length ys @ lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)" |
3528 0\<up>length ys @ lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)" |
3529 apply(insert mv_box_ex[of "length ys" pstr |
3529 apply(insert mv_box_ex[of "length ys" pstr |
3530 "ys @ rs # 0\<up>pstr @ lm @ 0\<up>(a_md - Suc(pstr + length ys + n)) @ suf_lm"], |
3530 "ys @ rs # 0\<up>pstr @ lm @ 0\<up>(a_md - Suc(pstr + length ys + n)) @ suf_lm"], |
3531 simp) |
3531 simp) |
3550 mv_boxes (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) |
3550 mv_boxes (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) |
3551 0 (length gs) [+] a" |
3551 0 (length gs) [+] a" |
3552 in exI, simp add: cn_merge_gs_len) |
3552 in exI, simp add: cn_merge_gs_len) |
3553 apply(rule_tac x = |
3553 apply(rule_tac x = |
3554 "empty_boxes (length gs) [+] |
3554 "empty_boxes (length gs) [+] |
3555 Recursive.mv_box (max (Suc n) (Max (insert ba |
3555 mv_box (max (Suc n) (Max (insert ba |
3556 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+] |
3556 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+] |
3557 mv_boxes (Suc (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) |
3557 mv_boxes (Suc (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) |
3558 + length gs)) 0 n" in exI, |
3558 + length gs)) 0 n" in exI, |
3559 auto simp: abc_append_commute) |
3559 auto simp: abc_append_commute) |
3560 done |
3560 done |
3597 0\<up>length ys @ lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)" |
3597 0\<up>length ys @ lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)" |
3598 proof (erule_tac exE, erule_tac exE, erule_tac exE, erule_tac exE) |
3598 proof (erule_tac exE, erule_tac exE, erule_tac exE, erule_tac exE) |
3599 fix ap bp apa cp |
3599 fix ap bp apa cp |
3600 assume "aprog = ap [+] bp [+] cp \<and> length ap = |
3600 assume "aprog = ap [+] bp [+] cp \<and> length ap = |
3601 (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs + |
3601 (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs + |
3602 3 * n + length a \<and> bp = Recursive.mv_box (length ys) pstr" |
3602 3 * n + length a \<and> bp = mv_box (length ys) pstr" |
3603 thus"?thesis" |
3603 thus"?thesis" |
3604 apply(simp, rule_tac abc_append_exc1, simp_all) |
3604 apply(simp, rule_tac abc_append_exc1, simp_all) |
3605 apply(rule_tac save_rs', insert h) |
3605 apply(rule_tac save_rs', insert h) |
3606 apply(subgoal_tac "length gs = aa \<and> pstr \<ge> ba \<and> ba > aa", |
3606 apply(subgoal_tac "length gs = aa \<and> pstr \<ge> ba \<and> ba > aa", |
3607 arith) |
3607 arith) |
3672 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] |
3672 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] |
3673 mv_boxes 0 (Suc (max (Suc n) (Max |
3673 mv_boxes 0 (Suc (max (Suc n) (Max |
3674 (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n |
3674 (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n |
3675 [+] mv_boxes (max (Suc n) (Max (insert ba |
3675 [+] mv_boxes (max (Suc n) (Max (insert ba |
3676 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+] |
3676 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+] |
3677 a [+] Recursive.mv_box aa (max (Suc n) |
3677 a [+] mv_box aa (max (Suc n) |
3678 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))))" |
3678 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))))" |
3679 in exI, simp add: cn_merge_gs_len) |
3679 in exI, simp add: cn_merge_gs_len) |
3680 apply(rule_tac x = " Recursive.mv_box (max (Suc n) (Max (insert ba |
3680 apply(rule_tac x = " mv_box (max (Suc n) (Max (insert ba |
3681 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+] |
3681 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+] |
3682 mv_boxes (Suc (max (Suc n) (Max (insert ba |
3682 mv_boxes (Suc (max (Suc n) (Max (insert ba |
3683 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI, |
3683 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI, |
3684 auto simp: abc_append_commute) |
3684 auto simp: abc_append_commute) |
3685 done |
3685 done |
3753 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] |
3753 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] |
3754 mv_boxes 0 (Suc (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) |
3754 mv_boxes 0 (Suc (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) |
3755 \<circ> rec_ci) ` set gs))) + length gs)) n [+] |
3755 \<circ> rec_ci) ` set gs))) + length gs)) n [+] |
3756 mv_boxes (max (Suc n) (Max (insert ba |
3756 mv_boxes (max (Suc n) (Max (insert ba |
3757 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+] |
3757 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+] |
3758 a [+] Recursive.mv_box aa (max (Suc n) |
3758 a [+] mv_box aa (max (Suc n) |
3759 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] |
3759 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] |
3760 empty_boxes (length gs)" in exI, simp add: cn_merge_gs_len) |
3760 empty_boxes (length gs)" in exI, simp add: cn_merge_gs_len) |
3761 apply(rule_tac x = "mv_boxes (Suc (max (Suc n) |
3761 apply(rule_tac x = "mv_boxes (Suc (max (Suc n) |
3762 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) |
3762 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) |
3763 + length gs)) 0 n" |
3763 + length gs)) 0 n" |
3796 by(drule_tac restore_rs_prog_ex, auto) |
3796 by(drule_tac restore_rs_prog_ex, auto) |
3797 from k1 show "?thesis" |
3797 from k1 show "?thesis" |
3798 proof (erule_tac exE, erule_tac exE, erule_tac exE, erule_tac exE) |
3798 proof (erule_tac exE, erule_tac exE, erule_tac exE, erule_tac exE) |
3799 fix ap bp apa cp |
3799 fix ap bp apa cp |
3800 assume "aprog = ap [+] bp [+] cp \<and> length ap = ss \<and> |
3800 assume "aprog = ap [+] bp [+] cp \<and> length ap = ss \<and> |
3801 bp = Recursive.mv_box pstr n" |
3801 bp = mv_box pstr n" |
3802 thus"?thesis" |
3802 thus"?thesis" |
3803 apply(simp, rule_tac abc_append_exc1, simp_all add: starts h) |
3803 apply(simp, rule_tac abc_append_exc1, simp_all add: starts h) |
3804 apply(insert mv_box_ex[of pstr n "0\<up>pstr @ rs # 0\<up>length gs @ |
3804 apply(insert mv_box_ex[of pstr n "0\<up>pstr @ rs # 0\<up>length gs @ |
3805 lm @ 0\<up>(a_md - Suc (pstr + length gs + n)) @ suf_lm"], simp) |
3805 lm @ 0\<up>(a_md - Suc (pstr + length gs + n)) @ suf_lm"], simp) |
3806 apply(subgoal_tac "pstr > n", simp) |
3806 apply(subgoal_tac "pstr > n", simp) |
3832 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) |
3832 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) |
3833 [+] mv_boxes 0 (Suc (max (Suc n) |
3833 [+] mv_boxes 0 (Suc (max (Suc n) |
3834 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) |
3834 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) |
3835 + length gs)) n [+] mv_boxes (max (Suc n) |
3835 + length gs)) n [+] mv_boxes (max (Suc n) |
3836 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+] |
3836 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+] |
3837 a [+] Recursive.mv_box aa (max (Suc n) |
3837 a [+] mv_box aa (max (Suc n) |
3838 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] |
3838 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] |
3839 empty_boxes (length gs) [+] |
3839 empty_boxes (length gs) [+] |
3840 Recursive.mv_box (max (Suc n) (Max (insert ba |
3840 mv_box (max (Suc n) (Max (insert ba |
3841 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n" in exI, simp add: cn_merge_gs_len) |
3841 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n" in exI, simp add: cn_merge_gs_len) |
3842 apply(rule_tac x = "[]" in exI, auto simp: abc_append_commute) |
3842 apply(rule_tac x = "[]" in exI, auto simp: abc_append_commute) |
3843 done |
3843 done |
3844 |
3844 |
3845 lemma restore_paras: |
3845 lemma restore_paras: |
4381 (cn_merge_gs (map rec_ci (drop (Suc i) gs)) (?pstr + Suc i)) |
4381 (cn_merge_gs (map rec_ci (drop (Suc i) gs)) (?pstr + Suc i)) |
4382 [+]mv_boxes 0 (Suc (max (Suc n) (Max (insert c |
4382 [+]mv_boxes 0 (Suc (max (Suc n) (Max (insert c |
4383 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + |
4383 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + |
4384 length gs)) n [+] mv_boxes (max (Suc n) (Max (insert c |
4384 length gs)) n [+] mv_boxes (max (Suc n) (Max (insert c |
4385 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+] |
4385 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+] |
4386 a [+] Recursive.mv_box b (max (Suc n) |
4386 a [+] mv_box b (max (Suc n) |
4387 (Max (insert c (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] |
4387 (Max (insert c (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+] |
4388 empty_boxes (length gs) [+] Recursive.mv_box (max (Suc n) |
4388 empty_boxes (length gs) [+] mv_box (max (Suc n) |
4389 (Max (insert c (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+] |
4389 (Max (insert c (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+] |
4390 mv_boxes (Suc (max (Suc n) (Max (insert c |
4390 mv_boxes (Suc (max (Suc n) (Max (insert c |
4391 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI) |
4391 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI) |
4392 apply(simp add: abc_append_commute [THEN sym]) |
4392 apply(simp add: abc_append_commute [THEN sym]) |
4393 apply(auto) |
4393 apply(auto) |