| changeset 115 | 653426ed4b38 |
| parent 112 | fea23f9a9d85 |
| 114:120091653998 | 115:653426ed4b38 |
|---|---|
4 |
4 |
5 theory abacus |
5 theory abacus |
6 imports uncomputable |
6 imports uncomputable |
7 begin |
7 begin |
8 |
8 |
9 (* |
|
10 declare tm_comp.simps [simp add] |
|
11 declare adjust.simps[simp add] |
|
12 declare shift.simps[simp add] |
|
13 declare tm_wf.simps[simp add] |
|
14 declare step.simps[simp add] |
|
15 declare steps.simps[simp add] |
|
16 *) |
|
9 declare replicate_Suc[simp add] |
17 declare replicate_Suc[simp add] |
10 |
18 |
11 text {* |
19 text {* |
12 {\em Abacus} instructions: |
20 {\em Abacus} instructions: |
13 *} |
21 *} |
1721 declare inc_inv.simps[simp del] |
1729 declare inc_inv.simps[simp del] |
1722 |
1730 |
1723 lemma wf_inc_le[intro]: "wf inc_LE" |
1731 lemma wf_inc_le[intro]: "wf inc_LE" |
1724 by(auto intro:wf_inv_image simp: inc_LE_def lex_triple_def lex_pair_def) |
1732 by(auto intro:wf_inv_image simp: inc_LE_def lex_triple_def lex_pair_def) |
1725 |
1733 |
1734 lemma numeral_5_eq_5: "5 = Suc (Suc (Suc (Suc (Suc 0))))" |
|
1735 by arith |
|
1736 |
|
1737 lemma numeral_6_eq_6: "6 = Suc (Suc (Suc (Suc (Suc 1))))" |
|
1738 by arith |
|
1739 |
|
1740 lemma numeral_7_eq_7: "7 = Suc (Suc (Suc (Suc (Suc 2))))" |
|
1741 by arith |
|
1742 |
|
1743 lemma numeral_8_eq_8: "8 = Suc (Suc (Suc (Suc (Suc 3))))" |
|
1744 by arith |
|
1745 |
|
1746 lemma numeral_9_eq_9: "9 = Suc (Suc (Suc (Suc (Suc (Suc 3)))))" |
|
1747 by arith |
|
1748 |
|
1749 lemma numeral_10_eq_10: "10 = Suc (Suc (Suc (Suc (Suc (Suc (Suc 3))))))" |
|
1750 by arith |
|
1726 |
1751 |
1727 lemma inv_locate_b_2_after_write[simp]: |
1752 lemma inv_locate_b_2_after_write[simp]: |
1728 "inv_locate_b (as, am) (n, aaa, Bk # xs) ires |
1753 "inv_locate_b (as, am) (n, aaa, Bk # xs) ires |
1729 \<Longrightarrow> inv_after_write (as, abc_lm_s am n (Suc (abc_lm_v am n))) |
1754 \<Longrightarrow> inv_after_write (as, abc_lm_s am n (Suc (abc_lm_v am n))) |
1730 (s, aaa, Oc # xs) ires" |
1755 (s, aaa, Oc # xs) ires" |
2126 assume "a \<noteq> 10 \<and> Q (a, b, c)" |
2151 assume "a \<noteq> 10 \<and> Q (a, b, c)" |
2127 thus "Q (step (a, b, c) (tinc_b, 0)) \<and> (step (a, b, c) (tinc_b, 0), a, b, c) \<in> inc_LE" |
2152 thus "Q (step (a, b, c) (tinc_b, 0)) \<and> (step (a, b, c) (tinc_b, 0), a, b, c) \<in> inc_LE" |
2128 apply(simp add:Q) |
2153 apply(simp add:Q) |
2129 apply(simp add: inc_inv.simps) |
2154 apply(simp add: inc_inv.simps) |
2130 apply(case_tac c, case_tac [2] aa) |
2155 apply(case_tac c, case_tac [2] aa) |
2131 apply(auto simp: Let_def step.simps tinc_b_def numeral split: if_splits) |
2156 apply(auto simp: Let_def step.simps tinc_b_def numeral_2_eq_2 numeral_3_eq_3 split: if_splits) |
2132 apply(simp_all add: inc_inv.simps inc_LE_def lex_triple_def lex_pair_def inc_measure_def numeral) |
2157 apply(simp_all add: inc_inv.simps inc_LE_def lex_triple_def lex_pair_def inc_measure_def numeral_5_eq_5 |
2158 numeral_6_eq_6 numeral_7_eq_7 numeral_8_eq_8 numeral_9_eq_9) |
|
2133 done |
2159 done |
2134 qed |
2160 qed |
2135 qed |
2161 qed |
2136 |
2162 |
2137 |
2163 |
3654 apply(case_tac c, case_tac [2] aa) |
3680 apply(case_tac c, case_tac [2] aa) |
3655 apply(simp_all add: dec_inv_2.simps Let_def) |
3681 apply(simp_all add: dec_inv_2.simps Let_def) |
3656 apply(simp_all split: if_splits) |
3682 apply(simp_all split: if_splits) |
3657 using fetch layout dec_suc |
3683 using fetch layout dec_suc |
3658 apply(auto simp: step.simps P dec_inv_2.simps Let_def abc_dec_2_LE_def lex_triple_def lex_pair_def lex_square_def |
3684 apply(auto simp: step.simps P dec_inv_2.simps Let_def abc_dec_2_LE_def lex_triple_def lex_pair_def lex_square_def |
3659 fix_add numeral) |
3685 fix_add numeral_3_eq_3) |
3660 done |
3686 done |
3661 qed |
3687 qed |
3662 qed |
3688 qed |
3663 qed |
3689 qed |
3664 |
3690 |