420 |
416 |
421 lemma concat_suc: "Suc as \<le> length xs \<Longrightarrow> |
417 lemma concat_suc: "Suc as \<le> length xs \<Longrightarrow> |
422 concat (take (Suc as) xs) = concat (take as xs) @ xs! as" |
418 concat (take (Suc as) xs) = concat (take as xs) @ xs! as" |
423 apply(subgoal_tac "take (Suc as) xs = take as xs @ [xs ! as]", simp) |
419 apply(subgoal_tac "take (Suc as) xs = take as xs @ [xs ! as]", simp) |
424 by auto |
420 by auto |
425 |
|
426 lemma concat_take_suc_iff: "Suc n \<le> length tps \<Longrightarrow> |
|
427 concat (take n tps) @ (tps ! n) = concat (take (Suc n) tps)" |
|
428 apply(drule_tac concat_suc, simp) |
|
429 done |
|
430 |
421 |
431 lemma concat_drop_suc_iff: |
422 lemma concat_drop_suc_iff: |
432 "Suc n < length tps \<Longrightarrow> concat (drop (Suc n) tps) = |
423 "Suc n < length tps \<Longrightarrow> concat (drop (Suc n) tps) = |
433 tps ! Suc n @ concat (drop (Suc (Suc n)) tps)" |
424 tps ! Suc n @ concat (drop (Suc (Suc n)) tps)" |
434 apply(induct tps arbitrary: n, simp, simp) |
425 apply(induct tps arbitrary: n, simp, simp) |
456 apply(rule concat_drop_suc_iff,force) |
447 apply(rule concat_drop_suc_iff,force) |
457 by (simp add: concat_suc) |
448 by (simp add: concat_suc) |
458 |
449 |
459 declare append_assoc[simp] |
450 declare append_assoc[simp] |
460 |
451 |
461 lemma map_of: "n < length xs \<Longrightarrow> (map f xs) ! n = f (xs ! n)" |
|
462 by(auto) |
|
463 |
|
464 lemma length_tms_of[simp]: "length (tms_of aprog) = length aprog" |
452 lemma length_tms_of[simp]: "length (tms_of aprog) = length aprog" |
465 apply(auto simp: tms_of.simps tpairs_of.simps) |
453 apply(auto simp: tms_of.simps tpairs_of.simps) |
466 done |
454 done |
467 |
455 |
468 lemma ci_nth: |
456 lemma ci_nth: |
469 "\<lbrakk>ly = layout_of aprog; |
457 "\<lbrakk>ly = layout_of aprog; |
470 abc_fetch as aprog = Some ins\<rbrakk> |
458 abc_fetch as aprog = Some ins\<rbrakk> |
471 \<Longrightarrow> ci ly (start_of ly as) ins = tms_of aprog ! as" |
459 \<Longrightarrow> ci ly (start_of ly as) ins = tms_of aprog ! as" |
472 apply(simp add: tms_of.simps tpairs_of.simps |
460 apply(simp add: tms_of.simps tpairs_of.simps |
473 abc_fetch.simps map_of del: map_append split: if_splits) |
461 abc_fetch.simps del: map_append split: if_splits) |
474 done |
462 done |
475 |
463 |
476 lemma t_split:"\<lbrakk> |
464 lemma t_split:"\<lbrakk> |
477 ly = layout_of aprog; |
465 ly = layout_of aprog; |
478 abc_fetch as aprog = Some ins\<rbrakk> |
466 abc_fetch as aprog = Some ins\<rbrakk> |
486 apply(subgoal_tac "length (tms_of aprog) = length aprog") |
474 apply(subgoal_tac "length (tms_of aprog) = length aprog") |
487 apply(simp add: abc_fetch.simps split: if_splits, simp) |
475 apply(simp add: abc_fetch.simps split: if_splits, simp) |
488 apply(rule_tac ci_nth, auto) |
476 apply(rule_tac ci_nth, auto) |
489 done |
477 done |
490 |
478 |
491 lemma math_sub: "\<lbrakk>x >= Suc 0; x - 1 = z\<rbrakk> \<Longrightarrow> x + y - Suc 0 = z + y" |
|
492 by auto |
|
493 |
|
494 lemma start_more_one: "as \<noteq> 0 \<Longrightarrow> start_of ly as >= Suc 0" |
|
495 apply(induct as, simp add: start_of.simps) |
|
496 apply(case_tac as, auto simp: start_of.simps) |
|
497 done |
|
498 |
|
499 lemma div_apart: "\<lbrakk>x mod (2::nat) = 0; y mod 2 = 0\<rbrakk> |
479 lemma div_apart: "\<lbrakk>x mod (2::nat) = 0; y mod 2 = 0\<rbrakk> |
500 \<Longrightarrow> (x + y) div 2 = x div 2 + y div 2" |
480 \<Longrightarrow> (x + y) div 2 = x div 2 + y div 2" |
501 by(auto) |
481 by(auto) |
502 |
482 |
503 lemma div_apart_iff: "\<lbrakk>x mod (2::nat) = 0; y mod 2 = 0\<rbrakk> \<Longrightarrow> |
|
504 (x + y) mod 2 = 0" |
|
505 by(auto) |
|
506 |
|
507 lemma length_layout_of[simp]: "length (layout_of aprog) = length aprog" |
483 lemma length_layout_of[simp]: "length (layout_of aprog) = length aprog" |
508 by(auto simp: layout_of.simps) |
484 by(auto simp: layout_of.simps) |
509 |
|
510 lemma start_of_ind: "\<lbrakk>as < length aprog; ly = layout_of aprog\<rbrakk> \<Longrightarrow> |
|
511 start_of ly (Suc as) = start_of ly as + |
|
512 length ((tms_of aprog) ! as) div 2" |
|
513 by (auto simp: start_of.simps tms_of.simps layout_of.simps |
|
514 tpairs_of.simps ci_length take_Suc take_Suc_conv_app_nth) |
|
515 |
|
516 lemma concat_take_suc: "Suc n \<le> length xs \<Longrightarrow> |
|
517 concat (take (Suc n) xs) = concat (take n xs) @ (xs ! n)" |
|
518 using concat_suc. |
|
519 |
|
520 lemma ci_in_set[simp]: |
|
521 "\<lbrakk>as < length aprog; (abc_fetch as aprog) = Some ins\<rbrakk> |
|
522 \<Longrightarrow> ci (layout_of aprog) |
|
523 (start_of (layout_of aprog) as) (ins) \<in> set (tms_of aprog)" |
|
524 by(insert ci_nth[of "layout_of aprog" aprog as], simp) |
|
525 |
485 |
526 lemma length_tms_of_elem_even[intro]: "n < length ap \<Longrightarrow> length (tms_of ap ! n) mod 2 = 0" |
486 lemma length_tms_of_elem_even[intro]: "n < length ap \<Longrightarrow> length (tms_of ap ! n) mod 2 = 0" |
527 apply(cases "ap ! n") |
487 apply(cases "ap ! n") |
528 by (auto simp: tms_of.simps tpairs_of.simps ci.simps length_findnth tinc_b_def tdec_b_def) |
488 by (auto simp: tms_of.simps tpairs_of.simps ci.simps length_findnth tinc_b_def tdec_b_def) |
529 |
489 |
1245 |
1205 |
1246 lemma tape_nat[simp]: "<[x::nat]> = Oc\<up>(Suc x)" |
1206 lemma tape_nat[simp]: "<[x::nat]> = Oc\<up>(Suc x)" |
1247 apply(simp add: tape_of_nat_def tape_of_list_def) |
1207 apply(simp add: tape_of_nat_def tape_of_list_def) |
1248 done |
1208 done |
1249 |
1209 |
1250 lemma tape_empty_list[simp]: " <([]::nat list)> = []" |
|
1251 apply(simp add: tape_of_list_def) |
|
1252 done |
|
1253 |
|
1254 lemma inv_locate[simp]: "\<lbrakk>inv_locate_b (as, am) (q, aaa, Bk # xs) ires; \<exists>n. xs = Bk\<up>n\<rbrakk> |
1210 lemma inv_locate[simp]: "\<lbrakk>inv_locate_b (as, am) (q, aaa, Bk # xs) ires; \<exists>n. xs = Bk\<up>n\<rbrakk> |
1255 \<Longrightarrow> inv_locate_a (as, am) (Suc q, Bk # aaa, xs) ires" |
1211 \<Longrightarrow> inv_locate_a (as, am) (Suc q, Bk # aaa, xs) ires" |
1256 apply(simp add: inv_locate_b.simps inv_locate_a.simps) |
1212 apply(simp add: inv_locate_b.simps inv_locate_a.simps) |
1257 apply(rule_tac disjI2, rule_tac disjI1) |
1213 apply(rule_tac disjI2, rule_tac disjI1) |
1258 apply(simp only: in_middle.simps at_begin_fst_bwtn.simps) |
1214 apply(simp only: in_middle.simps at_begin_fst_bwtn.simps) |
1397 apply(simp_all add: step.simps findnth_LE_def Q findnth_inv.simps mod_2 lex_pair_def split: if_splits) |
1350 apply(simp_all add: step.simps findnth_LE_def Q findnth_inv.simps mod_2 lex_pair_def split: if_splits) |
1398 apply(auto simp: mod_ex1 mod_ex2) |
1351 apply(auto simp: mod_ex1 mod_ex2) |
1399 done |
1352 done |
1400 qed |
1353 qed |
1401 qed |
1354 qed |
1402 |
1355 |
1403 lemma inv_locate_aI[intro]: "inv_locate_a (as, lm) (0, Bk # Bk # ires, <lm> @ Bk \<up> x) ires" |
|
1404 apply(auto simp: crsp.simps inv_locate_a.simps at_begin_norm.simps) |
|
1405 done |
|
1406 lemma inv_locate_a_via_crsp[simp]: |
1356 lemma inv_locate_a_via_crsp[simp]: |
1407 "crsp ly (as, lm) (s, l, r) ires \<Longrightarrow> inv_locate_a (as, lm) (0, l, r) ires" |
1357 "crsp ly (as, lm) (s, l, r) ires \<Longrightarrow> inv_locate_a (as, lm) (0, l, r) ires" |
1408 apply(auto simp: crsp.simps inv_locate_a.simps at_begin_norm.simps) |
1358 apply(auto simp: crsp.simps inv_locate_a.simps at_begin_norm.simps) |
1409 done |
1359 done |
1410 |
1360 |
1522 apply(simp only: Suc_diff_le exp_ind) |
1472 apply(simp only: Suc_diff_le exp_ind) |
1523 apply(subgoal_tac "lm2 = []", simp) |
1473 apply(subgoal_tac "lm2 = []", simp) |
1524 apply(drule_tac length_equal, simp) |
1474 apply(drule_tac length_equal, simp) |
1525 by (metis (no_types, lifting) add_diff_inverse_nat append.assoc append_eq_append_conv length_append length_replicate list.inject) |
1475 by (metis (no_types, lifting) add_diff_inverse_nat append.assoc append_eq_append_conv length_append length_replicate list.inject) |
1526 |
1476 |
1527 lemma inv_after_write_via_locate_b[simp]: "inv_locate_b (as, am) (n, aaa, []) ires \<Longrightarrow> |
|
1528 inv_after_write (as, abc_lm_s am n (Suc (abc_lm_v am n))) |
|
1529 (s, aaa, [Oc]) ires" |
|
1530 apply(insert inv_locate_b_2_after_write [of as am n aaa "[]"]) |
|
1531 by(simp) |
|
1532 |
|
1533 |
|
1534 |
|
1535 (*inv: from after_write to after_move*) |
1477 (*inv: from after_write to after_move*) |
1536 lemma inv_after_move_Oc_via_write[simp]: "inv_after_write (as, lm) (x, l, Oc # r) ires |
1478 lemma inv_after_move_Oc_via_write[simp]: "inv_after_write (as, lm) (x, l, Oc # r) ires |
1537 \<Longrightarrow> inv_after_move (as, lm) (y, Oc # l, r) ires" |
1479 \<Longrightarrow> inv_after_move (as, lm) (y, Oc # l, r) ires" |
1538 apply(auto simp:inv_after_move.simps inv_after_write.simps split: if_splits) |
1480 apply(auto simp:inv_after_move.simps inv_after_write.simps split: if_splits) |
1539 done |
1481 done |
1606 apply(case_tac [!] "lm2::nat list", auto) |
1548 apply(case_tac [!] "lm2::nat list", auto) |
1607 apply(case_tac rn, auto split: if_splits simp: tape_of_nl_cons) |
1549 apply(case_tac rn, auto split: if_splits simp: tape_of_nl_cons) |
1608 apply(case_tac [!] rn, simp_all) |
1550 apply(case_tac [!] rn, simp_all) |
1609 done |
1551 done |
1610 |
1552 |
1611 lemma inv_after_clear_singleton_Bk[simp]: "inv_after_clear (as, lm) (x, l, []) ires\<Longrightarrow> |
|
1612 inv_after_clear (as, lm) (y, l, [Bk]) ires" |
|
1613 by(auto simp: inv_after_clear.simps) |
|
1614 |
|
1615 lemma inv_on_right_moving_Bk[simp]: "inv_after_clear (as, lm) (x, l, []) ires |
|
1616 \<Longrightarrow> inv_on_right_moving (as, lm) (y, Bk # l, []) ires" |
|
1617 by(insert |
|
1618 inv_after_clear_2_inv_on_right_moving[of as lm n l "[]"], simp) |
|
1619 |
|
1620 (*inv: from on_right_moving to on_right_movign*) |
1553 (*inv: from on_right_moving to on_right_movign*) |
1621 lemma inv_on_right_moving_Oc[simp]: "inv_on_right_moving (as, lm) (x, l, Oc # r) ires |
1554 lemma inv_on_right_moving_Oc[simp]: "inv_on_right_moving (as, lm) (x, l, Oc # r) ires |
1622 \<Longrightarrow> inv_on_right_moving (as, lm) (y, Oc # l, r) ires" |
1555 \<Longrightarrow> inv_on_right_moving (as, lm) (y, Oc # l, r) ires" |
1623 apply(auto simp: inv_on_right_moving.simps) |
1556 apply(auto simp: inv_on_right_moving.simps) |
1624 apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, |
1557 apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, |
1644 inv_on_right_moving (as, lm) (y, l, [Bk]) ires" |
1577 inv_on_right_moving (as, lm) (y, l, [Bk]) ires" |
1645 apply(auto simp: inv_on_right_moving.simps) |
1578 apply(auto simp: inv_on_right_moving.simps) |
1646 apply(rule_tac x = lm1 in exI, rule_tac x = "[]" in exI, simp) |
1579 apply(rule_tac x = lm1 in exI, rule_tac x = "[]" in exI, simp) |
1647 done |
1580 done |
1648 |
1581 |
1649 (*inv: from on_right_moving to after_write*) |
|
1650 lemma inv_after_write_singleton_Oc[simp]: "inv_on_right_moving (as, lm) (x, l, []) ires |
|
1651 \<Longrightarrow> inv_after_write (as, lm) (y, l, [Oc]) ires" |
|
1652 apply(rule_tac inv_on_right_moving_2_inv_on_right_moving, simp) |
|
1653 done |
|
1654 |
|
1655 (*inv: from on_left_moving to on_left_moving*) |
1582 (*inv: from on_left_moving to on_left_moving*) |
1656 lemma no_inv_on_left_moving_in_middle_B_Oc[simp]: "inv_on_left_moving_in_middle_B (as, lm) |
1583 lemma no_inv_on_left_moving_in_middle_B_Oc[simp]: "inv_on_left_moving_in_middle_B (as, lm) |
1657 (s, l, Oc # r) ires = False" |
1584 (s, l, Oc # r) ires = False" |
1658 apply(auto simp: inv_on_left_moving_in_middle_B.simps ) |
1585 apply(auto simp: inv_on_left_moving_in_middle_B.simps ) |
1659 done |
1586 done |
1748 |
1675 |
1749 lemma inv_on_left_moving_norm_no_empty[simp]: "inv_on_left_moving_norm (as, lm) (s, l, []) ires = False" |
1676 lemma inv_on_left_moving_norm_no_empty[simp]: "inv_on_left_moving_norm (as, lm) (s, l, []) ires = False" |
1750 apply(auto simp: inv_on_left_moving_norm.simps) |
1677 apply(auto simp: inv_on_left_moving_norm.simps) |
1751 done |
1678 done |
1752 |
1679 |
1753 lemma inv_on_left_moving_Bk[simp]: "inv_on_left_moving (as, lm) (s, l, []) ires\<Longrightarrow> |
|
1754 inv_on_left_moving (as, lm) (6 + 2 * n, l, [Bk]) ires" |
|
1755 apply(simp add: inv_on_left_moving.simps) |
|
1756 apply(auto simp: inv_on_left_moving_in_middle_B.simps) |
|
1757 done |
|
1758 |
|
1759 lemma inv_on_left_moving_no_empty[simp]: "inv_on_left_moving (as, lm) (s, l, []) ires = False" |
1680 lemma inv_on_left_moving_no_empty[simp]: "inv_on_left_moving (as, lm) (s, l, []) ires = False" |
1760 apply(simp add: inv_on_left_moving.simps) |
1681 apply(simp add: inv_on_left_moving.simps) |
1761 apply(simp add: inv_on_left_moving_in_middle_B.simps) |
1682 apply(simp add: inv_on_left_moving_in_middle_B.simps) |
1762 done |
1683 done |
1763 |
|
1764 lemma inv_on_left_moving_cases_left[simp]: "inv_on_left_moving (as, lm) (s, l, []) ires |
|
1765 \<Longrightarrow> (l = [] \<longrightarrow> inv_check_left_moving (as, lm) (s', [], [Bk]) ires) \<and> |
|
1766 (l \<noteq> [] \<longrightarrow> inv_check_left_moving (as, lm) (s', tl l, [hd l]) ires)" |
|
1767 by simp |
|
1768 |
1684 |
1769 lemma Bk_plus_one[intro]: "\<exists>rna. Bk # Bk \<up> rn = Bk \<up> rna" |
1685 lemma Bk_plus_one[intro]: "\<exists>rna. Bk # Bk \<up> rn = Bk \<up> rna" |
1770 apply(rule_tac x = "Suc rn" in exI, simp) |
1686 apply(rule_tac x = "Suc rn" in exI, simp) |
1771 done |
1687 done |
1772 |
1688 |
1790 lemma inv_check_left_moving_in_middle_Bk_Oc[simp]: |
1706 lemma inv_check_left_moving_in_middle_Bk_Oc[simp]: |
1791 "inv_check_left_moving_in_middle (as, lm) (s, [], Oc # r) ires\<Longrightarrow> |
1707 "inv_check_left_moving_in_middle (as, lm) (s, [], Oc # r) ires\<Longrightarrow> |
1792 inv_check_left_moving_in_middle (as, lm) (s', [Bk], Oc # r) ires" |
1708 inv_check_left_moving_in_middle (as, lm) (s', [Bk], Oc # r) ires" |
1793 apply(auto simp: inv_check_left_moving_in_middle.simps ) |
1709 apply(auto simp: inv_check_left_moving_in_middle.simps ) |
1794 done |
1710 done |
1795 lemma inv_on_left_moving_in_middle_B_Bk_Oc_via_check[simp]: |
|
1796 "inv_check_left_moving_in_middle (as, lm) (s, [], Oc # r) ires |
|
1797 \<Longrightarrow> inv_on_left_moving_in_middle_B (as, lm) (s', [], Bk # Oc # r) ires" |
|
1798 apply(insert |
|
1799 inv_check_left_moving_in_middle_2_on_left_moving_in_middle_B[of |
|
1800 as lm n "[]" r], simp) |
|
1801 done |
|
1802 |
1711 |
1803 lemma inv_on_left_moving_norm_Oc_Oc_via_middle[simp]: "inv_check_left_moving_in_middle (as, lm) |
1712 lemma inv_on_left_moving_norm_Oc_Oc_via_middle[simp]: "inv_check_left_moving_in_middle (as, lm) |
1804 (s, Oc # list, Oc # r) ires |
1713 (s, Oc # list, Oc # r) ires |
1805 \<Longrightarrow> inv_on_left_moving_norm (as, lm) (s', list, Oc # Oc # r) ires" |
1714 \<Longrightarrow> inv_on_left_moving_norm (as, lm) (s', list, Oc # Oc # r) ires" |
1806 apply(auto simp: inv_check_left_moving_in_middle.simps |
1715 apply(auto simp: inv_check_left_moving_in_middle.simps |
2278 by(simp add: startof_Suc2) |
2187 by(simp add: startof_Suc2) |
2279 ultimately show "?thesis" |
2188 ultimately show "?thesis" |
2280 by arith |
2189 by arith |
2281 qed |
2190 qed |
2282 |
2191 |
2283 lemma abc_fetch_contrE[elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e); as < e; |
|
2284 Suc (start_of (layout_of ap) as + 2 * n) = start_of (layout_of ap) e\<rbrakk> \<Longrightarrow> RR" |
|
2285 by(drule_tac start_of_ge, auto) |
|
2286 |
|
2287 lemma abc_fetch_contrE2[elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e); as > e; |
|
2288 Suc (start_of (layout_of ap) as + 2 * n) = start_of (layout_of ap) e\<rbrakk> \<Longrightarrow> RR" |
|
2289 apply(drule_tac ly = "layout_of ap" in start_of_less[of]) |
|
2290 apply(arith) |
|
2291 done |
|
2292 |
|
2293 lemma abc_fetch_contrE3[elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e); |
|
2294 Suc (start_of (layout_of ap) as + 2 * n) = start_of (layout_of ap) e\<rbrakk> \<Longrightarrow> RR" |
|
2295 apply(subgoal_tac "as = e \<or> as < e \<or> as > e", auto) |
|
2296 done |
|
2297 |
|
2298 lemma fetch_c_Oc[simp]:"fetch (ci (ly) (start_of ly as) (Dec n e)) (Suc (2 * n)) Oc |
|
2299 = (R, start_of ly as + 2*n + 1)" |
|
2300 apply(auto simp: ci.simps findnth.simps fetch.simps |
|
2301 nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) |
|
2302 done |
|
2303 |
|
2304 |
|
2305 declare dec_inv_1.simps[simp del] |
2192 declare dec_inv_1.simps[simp del] |
2306 |
|
2307 |
2193 |
2308 lemma start_of_ineq1[simp]: |
2194 lemma start_of_ineq1[simp]: |
2309 "\<lbrakk>abc_fetch as aprog = Some (Dec n e); ly = layout_of aprog\<rbrakk> |
2195 "\<lbrakk>abc_fetch as aprog = Some (Dec n e); ly = layout_of aprog\<rbrakk> |
2310 \<Longrightarrow> (start_of ly e \<noteq> Suc (start_of ly as + 2 * n) \<and> |
2196 \<Longrightarrow> (start_of ly e \<noteq> Suc (start_of ly as + 2 * n) \<and> |
2311 start_of ly e \<noteq> Suc (Suc (start_of ly as + 2 * n)) \<and> |
2197 start_of ly e \<noteq> Suc (Suc (start_of ly as + 2 * n)) \<and> |
2422 lemma dec_right_move_Bk_via_clear_Bk[simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, Bk # r) ires\<rbrakk> |
2308 lemma dec_right_move_Bk_via_clear_Bk[simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, Bk # r) ires\<rbrakk> |
2423 \<Longrightarrow> dec_right_move (as, am) (s', Bk # l, r) ires" |
2309 \<Longrightarrow> dec_right_move (as, am) (s', Bk # l, r) ires" |
2424 apply(auto simp: dec_after_clear.simps dec_right_move.simps split: if_splits) |
2310 apply(auto simp: dec_after_clear.simps dec_right_move.simps split: if_splits) |
2425 done |
2311 done |
2426 |
2312 |
2427 lemma dec_right_move_Bk_via_clear_empty[simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, []) ires\<rbrakk> |
|
2428 \<Longrightarrow> dec_right_move (as, am) (s', Bk # l, []) ires" |
|
2429 apply(auto simp: dec_after_clear.simps dec_right_move.simps ) |
|
2430 done |
|
2431 |
|
2432 lemma dec_right_move_Bk_Bk_via_clear[simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, []) ires\<rbrakk> |
2313 lemma dec_right_move_Bk_Bk_via_clear[simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, []) ires\<rbrakk> |
2433 \<Longrightarrow> dec_right_move (as, am) (s', Bk # l, [Bk]) ires" |
2314 \<Longrightarrow> dec_right_move (as, am) (s', Bk # l, [Bk]) ires" |
2434 apply(auto simp: dec_after_clear.simps dec_right_move.simps split: if_splits) |
2315 apply(auto simp: dec_after_clear.simps dec_right_move.simps split: if_splits) |
2435 done |
2316 done |
2436 |
2317 |
2450 |
2331 |
2451 lemma dec_right_move_asif_Bk_singleton[simp]: |
2332 lemma dec_right_move_asif_Bk_singleton[simp]: |
2452 "dec_right_move (as, am) (s, l, []) ires= |
2333 "dec_right_move (as, am) (s, l, []) ires= |
2453 dec_right_move (as, am) (s, l, [Bk]) ires" |
2334 dec_right_move (as, am) (s, l, [Bk]) ires" |
2454 apply(simp add: dec_right_move.simps) |
2335 apply(simp add: dec_right_move.simps) |
2455 done |
|
2456 |
|
2457 lemma dec_check_right_move_Bk_via_move[simp]: "\<lbrakk>dec_right_move (as, am) (s, l, []) ires\<rbrakk> |
|
2458 \<Longrightarrow> dec_check_right_move (as, am) (s, Bk # l, []) ires" |
|
2459 apply(insert dec_right_move_2_check_right_move[of as am s l "[]" s'], |
|
2460 simp) |
|
2461 done |
2336 done |
2462 |
2337 |
2463 lemma dec_check_right_move_nonempty[simp]: "dec_check_right_move (as, am) (s, l, r) ires\<Longrightarrow> l \<noteq> []" |
2338 lemma dec_check_right_move_nonempty[simp]: "dec_check_right_move (as, am) (s, l, r) ires\<Longrightarrow> l \<noteq> []" |
2464 apply(auto simp: dec_check_right_move.simps split: if_splits) |
2339 apply(auto simp: dec_check_right_move.simps split: if_splits) |
2465 done |
2340 done |
2502 (s', Oc # Oc\<up>m @ Bk # Bk # ires, Bk # Bk\<up>rn) ires" |
2377 (s', Oc # Oc\<up>m @ Bk # Bk # ires, Bk # Bk\<up>rn) ires" |
2503 apply(simp add: inv_on_left_moving_in_middle_B.simps) |
2378 apply(simp add: inv_on_left_moving_in_middle_B.simps) |
2504 apply(rule_tac x = "[m]" in exI, auto) |
2379 apply(rule_tac x = "[m]" in exI, auto) |
2505 done |
2380 done |
2506 |
2381 |
2507 lemma inv_on_left_moving_in_middle_B_Oc_Bk_Bk[simp]: "inv_on_left_moving_in_middle_B (as, [m]) |
|
2508 (s', Oc # Oc\<up>m @ Bk # Bk # ires, [Bk]) ires" |
|
2509 apply(simp add: inv_on_left_moving_in_middle_B.simps) |
|
2510 done |
|
2511 |
|
2512 |
2382 |
2513 lemma inv_on_left_moving_in_middle_B_Oc_Bk_Bks_rev[simp]: "lm1 \<noteq> [] \<Longrightarrow> |
2383 lemma inv_on_left_moving_in_middle_B_Oc_Bk_Bks_rev[simp]: "lm1 \<noteq> [] \<Longrightarrow> |
2514 inv_on_left_moving_in_middle_B (as, lm1 @ [m]) (s', |
2384 inv_on_left_moving_in_middle_B (as, lm1 @ [m]) (s', |
2515 Oc # Oc\<up>m @ Bk # <rev lm1> @ Bk # Bk # ires, Bk # Bk\<up>rn) ires" |
2385 Oc # Oc\<up>m @ Bk # <rev lm1> @ Bk # Bk # ires, Bk # Bk\<up>rn) ires" |
2516 apply(simp only: inv_on_left_moving_in_middle_B.simps) |
|
2517 apply(rule_tac x = "lm1 @ [m ]" in exI, rule_tac x = "[]" in exI, simp) |
|
2518 apply(simp add: tape_of_nl_cons split: if_splits) |
|
2519 done |
|
2520 |
|
2521 lemma inv_on_left_moving_in_middle_B_Oc_Bk_Bk_rev[simp]: "lm1 \<noteq> [] \<Longrightarrow> |
|
2522 inv_on_left_moving_in_middle_B (as, lm1 @ [m]) (s', |
|
2523 Oc # Oc\<up> m @ Bk # <rev lm1> @ Bk # Bk # ires, [Bk]) ires" |
|
2524 apply(simp only: inv_on_left_moving_in_middle_B.simps) |
2386 apply(simp only: inv_on_left_moving_in_middle_B.simps) |
2525 apply(rule_tac x = "lm1 @ [m ]" in exI, rule_tac x = "[]" in exI, simp) |
2387 apply(rule_tac x = "lm1 @ [m ]" in exI, rule_tac x = "[]" in exI, simp) |
2526 apply(simp add: tape_of_nl_cons split: if_splits) |
2388 apply(simp add: tape_of_nl_cons split: if_splits) |
2527 done |
2389 done |
2528 |
2390 |
2579 lemma dec_after_clear_tail[simp]: "dec_on_right_moving (as, am) (s, l, []) ires |
2441 lemma dec_after_clear_tail[simp]: "dec_on_right_moving (as, am) (s, l, []) ires |
2580 \<Longrightarrow> dec_after_clear (as, am) (s', tl l, [hd l]) ires" |
2442 \<Longrightarrow> dec_after_clear (as, am) (s', tl l, [hd l]) ires" |
2581 apply(auto simp: dec_on_right_moving.simps dec_after_clear.simps) |
2443 apply(auto simp: dec_on_right_moving.simps dec_after_clear.simps) |
2582 apply(simp_all split: if_splits) |
2444 apply(simp_all split: if_splits) |
2583 apply(rule_tac x = lm1 in exI, simp) |
2445 apply(rule_tac x = lm1 in exI, simp) |
2584 done |
|
2585 |
|
2586 lemma inv_stop_abc_lm_s_nonempty[simp]: |
|
2587 "inv_stop (as, abc_lm_s am n (abc_lm_v am n)) (s, l, r) ires \<Longrightarrow> l \<noteq> []" |
|
2588 apply(auto simp: inv_stop.simps) |
|
2589 done |
2446 done |
2590 |
2447 |
2591 lemma dec_false_1[simp]: |
2448 lemma dec_false_1[simp]: |
2592 "\<lbrakk>abc_lm_v am n = 0; inv_locate_b (as, am) (n, aaa, Oc # xs) ires\<rbrakk> |
2449 "\<lbrakk>abc_lm_v am n = 0; inv_locate_b (as, am) (n, aaa, Oc # xs) ires\<rbrakk> |
2593 \<Longrightarrow> False" |
2450 \<Longrightarrow> False" |
2645 rule_tac x = "Suc 0" in exI, simp add: abc_lm_s.simps) |
2502 rule_tac x = "Suc 0" in exI, simp add: abc_lm_s.simps) |
2646 apply(case_tac mr, simp_all, auto simp: abc_lm_v.simps) |
2503 apply(case_tac mr, simp_all, auto simp: abc_lm_v.simps) |
2647 apply(simp_all only: exp_ind Nat.Suc_diff_le del: replicate_Suc, simp_all) |
2504 apply(simp_all only: exp_ind Nat.Suc_diff_le del: replicate_Suc, simp_all) |
2648 apply(auto simp: inv_on_left_moving_in_middle_B.simps split: if_splits) |
2505 apply(auto simp: inv_on_left_moving_in_middle_B.simps split: if_splits) |
2649 apply(case_tac [!] m, simp_all) |
2506 apply(case_tac [!] m, simp_all) |
2650 done |
2507 done |
2651 |
|
2652 lemma update_zero_to_zero[simp]: "\<lbrakk>am ! n = (0::nat); n < length am\<rbrakk> \<Longrightarrow> am[n := 0] = am" |
|
2653 apply(simp add: list_update_same_conv) |
|
2654 done |
|
2655 |
|
2656 lemma abc_lm_v_zero: "\<lbrakk>abc_lm_v (a # list) 0 = 0\<rbrakk> \<Longrightarrow> a = 0" |
|
2657 apply(simp add: abc_lm_v.simps split: if_splits) |
|
2658 done |
|
2659 |
|
2660 lemma inv_locate_a_via_stop[simp]: |
|
2661 "inv_stop (as, abc_lm_s am n 0) |
|
2662 (start_of (layout_of aprog) e, aaa, Oc # xs) ires |
|
2663 \<Longrightarrow> inv_locate_a (as, abc_lm_s am n 0) (0, aaa, Oc # xs) ires" |
|
2664 apply(simp add: inv_locate_a.simps) |
|
2665 apply(rule disjI1) |
|
2666 apply(auto simp: inv_stop.simps at_begin_norm.simps) |
|
2667 done |
|
2668 |
|
2669 lemma inv_locate_b_cases_via_stop[simp]: |
|
2670 "\<lbrakk>inv_stop (as, abc_lm_s am n 0) |
|
2671 (start_of (layout_of aprog) e, aaa, Oc # xs) ires\<rbrakk> |
|
2672 \<Longrightarrow> inv_locate_b (as, am) (0, Oc # aaa, xs) ires \<or> |
|
2673 inv_locate_b (as, abc_lm_s am n 0) (0, Oc # aaa, xs) ires" |
|
2674 apply(simp) |
|
2675 done |
|
2676 |
|
2677 lemma dec_false2: |
|
2678 "inv_stop (as, abc_lm_s am n 0) |
|
2679 (start_of (layout_of aprog) e, aaa, Bk # xs) ires = False" |
|
2680 apply(auto simp: inv_stop.simps abc_lm_s.simps) |
|
2681 apply(case_tac [!] am, auto) |
|
2682 apply(case_tac [!] n, auto simp: tape_of_nl_cons split: if_splits) |
|
2683 done |
|
2684 |
|
2685 lemma dec_false3: |
|
2686 "inv_stop (as, abc_lm_s am n 0) |
|
2687 (start_of (layout_of aprog) e, aaa, []) ires = False" |
|
2688 apply(auto simp: inv_stop.simps abc_lm_s.simps) |
|
2689 done |
|
2690 |
2508 |
2691 declare dec_inv_1.simps[simp del] |
2509 declare dec_inv_1.simps[simp del] |
2692 |
2510 |
2693 declare inv_locate_n_b.simps [simp del] |
2511 declare inv_locate_n_b.simps [simp del] |
2694 |
|
2695 lemma inv_locate_n_b_Oc_via_at_begin_fst_bwtn[simp]: |
|
2696 "\<lbrakk>0 < abc_lm_v am n; 0 < n; |
|
2697 at_begin_fst_bwtn (as, am) (n, aaa, Oc # xs) ires\<rbrakk> |
|
2698 \<Longrightarrow> inv_locate_n_b (as, am) (n, Oc # aaa, xs) ires" |
|
2699 apply(simp add: at_begin_fst_bwtn.simps inv_locate_n_b.simps ) |
|
2700 done |
|
2701 |
2512 |
2702 lemma Suc_minus:"length am + tn = n |
|
2703 \<Longrightarrow> Suc tn = Suc n - length am " |
|
2704 apply(arith) |
|
2705 done |
|
2706 |
|
2707 lemma dec_first_on_right_moving_Oc_via_inv_locate_n_b[simp]: |
2513 lemma dec_first_on_right_moving_Oc_via_inv_locate_n_b[simp]: |
2708 "\<lbrakk>inv_locate_n_b (as, am) (n, aaa, Oc # xs) ires\<rbrakk> |
2514 "\<lbrakk>inv_locate_n_b (as, am) (n, aaa, Oc # xs) ires\<rbrakk> |
2709 \<Longrightarrow> dec_first_on_right_moving n (as, abc_lm_s am n (abc_lm_v am n)) |
2515 \<Longrightarrow> dec_first_on_right_moving n (as, abc_lm_s am n (abc_lm_v am n)) |
2710 (s, Oc # aaa, xs) ires" |
2516 (s, Oc # aaa, xs) ires" |
2711 apply(auto simp: inv_locate_n_b.simps dec_first_on_right_moving.simps |
2517 apply(auto simp: inv_locate_n_b.simps dec_first_on_right_moving.simps |
3034 lemma inv_check_left_moving_nonemptyE[elim]: |
2840 lemma inv_check_left_moving_nonemptyE[elim]: |
3035 "inv_check_left_moving (as, lm) (s, [], Oc # xs) ires |
2841 "inv_check_left_moving (as, lm) (s, [], Oc # xs) ires |
3036 \<Longrightarrow> RR" |
2842 \<Longrightarrow> RR" |
3037 apply(simp add: inv_check_left_moving.simps inv_check_left_moving_in_middle.simps) |
2843 apply(simp add: inv_check_left_moving.simps inv_check_left_moving_in_middle.simps) |
3038 done |
2844 done |
3039 |
|
3040 lemma inv_check_left_moving_nonempty[simp]: |
|
3041 "inv_check_left_moving (as, lm) (s, [], Oc # list) ires = False" |
|
3042 by auto |
|
3043 |
2845 |
3044 lemma inv_locate_n_b_Oc_via_at_begin_norm[simp]: |
2846 lemma inv_locate_n_b_Oc_via_at_begin_norm[simp]: |
3045 "\<lbrakk>0 < abc_lm_v am n; |
2847 "\<lbrakk>0 < abc_lm_v am n; |
3046 at_begin_norm (as, am) (n, aaa, Oc # xs) ires\<rbrakk> |
2848 at_begin_norm (as, am) (n, aaa, Oc # xs) ires\<rbrakk> |
3047 \<Longrightarrow> inv_locate_n_b (as, am) (n, Oc # aaa, xs) ires" |
2849 \<Longrightarrow> inv_locate_n_b (as, am) (n, Oc # aaa, xs) ires" |
3373 apply(case_tac x) |
3175 apply(case_tac x) |
3374 apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth adjust.simps length_of.simps |
3176 apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth adjust.simps length_of.simps |
3375 split: abc_inst.splits) |
3177 split: abc_inst.splits) |
3376 done |
3178 done |
3377 qed |
3179 qed |
3378 |
|
3379 lemma fetch_Nops[simp]: |
|
3380 "\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow> |
|
3381 fetch (tp @ [(Nop, 0), (Nop, 0)]) (start_of ly (length ap)) b = |
|
3382 (Nop, 0)" |
|
3383 apply(case_tac b) |
|
3384 apply(simp_all add: start_of.simps fetch.simps nth_append) |
|
3385 done |
|
3386 |
3180 |
3387 lemma length_tp: |
3181 lemma length_tp: |
3388 "\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow> |
3182 "\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow> |
3389 start_of ly (length ap) = Suc (length tp div 2)" |
3183 start_of ly (length ap) = Suc (length tp div 2)" |
3390 apply(frule_tac length_tp', simp_all) |
3184 apply(frule_tac length_tp', simp_all) |
3509 hence c: |
3303 hence c: |
3510 "(steps (1, l, r) (tp @ shift (mopup n) off, 0) stpa) = (s', l', r')" |
3304 "(steps (1, l, r) (tp @ shift (mopup n) off, 0) stpa) = (s', l', r')" |
3511 by(rule_tac tm_append_first_steps_eq, simp_all add: crsp.simps) |
3305 by(rule_tac tm_append_first_steps_eq, simp_all add: crsp.simps) |
3512 from b have d: "s' > 0 \<and> stpa \<ge> stp" |
3306 from b have d: "s' > 0 \<and> stpa \<ge> stp" |
3513 by(simp add: crsp.simps) |
3307 by(simp add: crsp.simps) |
3514 then obtain diff where e: "stpa = stp + diff" by (metis le_iff_add) |
3308 then obtain diff where e: "stpa = stp + diff" by (metis le_iff_add) |
3515 obtain s'' l'' r'' where f: |
3309 obtain s'' l'' r'' where f: |
3516 "steps (1, l, r) (tp @ shift (mopup n) off, 0) stp = (s'', l'', r'') \<and> is_final (s'', l'', r'')" |
3310 "steps (1, l, r) (tp @ shift (mopup n) off, 0) stp = (s'', l'', r'') \<and> is_final (s'', l'', r'')" |
3517 using h |
3311 using h |
3518 by(case_tac "steps (1, l, r) (tp @ shift (mopup n) off, 0) stp", auto) |
3312 by(case_tac "steps (1, l, r) (tp @ shift (mopup n) off, 0) stp", auto) |
3519 |
3313 |