1 header {* |
1 header {* |
2 {\em abacus} a kind of register machine |
2 {\em abacus} a kind of register machine |
3 *} |
3 *} |
4 |
4 |
5 theory abacus |
5 theory abacus |
6 imports Main turing_basic |
6 imports uncomputable |
7 begin |
7 begin |
|
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 *) |
|
17 declare replicate_Suc[simp add] |
8 |
18 |
9 text {* |
19 text {* |
10 {\em Abacus} instructions: |
20 {\em Abacus} instructions: |
11 *} |
21 *} |
12 |
22 |
1298 inv_after_left_moving.simps[simp del] |
1308 inv_after_left_moving.simps[simp del] |
1299 inv_stop.simps[simp del] inv_locate_a.simps[simp del] |
1309 inv_stop.simps[simp del] inv_locate_a.simps[simp del] |
1300 inv_locate_b.simps[simp del] |
1310 inv_locate_b.simps[simp del] |
1301 |
1311 |
1302 lemma [intro]: "\<exists>rn. [Bk] = Bk \<up> rn" |
1312 lemma [intro]: "\<exists>rn. [Bk] = Bk \<up> rn" |
1303 apply(rule_tac x = "Suc 0" in exI, simp) |
1313 by (metis replicate_0 replicate_Suc) |
1304 done |
|
1305 |
1314 |
1306 lemma [intro]: "at_begin_norm (as, am) (q, aaa, []) ires |
1315 lemma [intro]: "at_begin_norm (as, am) (q, aaa, []) ires |
1307 \<Longrightarrow> at_begin_norm (as, am) (q, aaa, [Bk]) ires" |
1316 \<Longrightarrow> at_begin_norm (as, am) (q, aaa, [Bk]) ires" |
1308 apply(simp add: at_begin_norm.simps, erule_tac exE, erule_tac exE) |
1317 apply(simp add: at_begin_norm.simps, erule_tac exE, erule_tac exE) |
1309 apply(rule_tac x = lm1 in exI, simp, auto) |
1318 apply(rule_tac x = lm1 in exI, simp, auto) |
1875 lemma inv_on_right_moving_2_inv_on_right_moving[simp]: |
1884 lemma inv_on_right_moving_2_inv_on_right_moving[simp]: |
1876 "inv_on_right_moving (as, lm) (x, l, Bk # r) ires |
1885 "inv_on_right_moving (as, lm) (x, l, Bk # r) ires |
1877 \<Longrightarrow> inv_after_write (as, lm) (y, l, Oc # r) ires" |
1886 \<Longrightarrow> inv_after_write (as, lm) (y, l, Oc # r) ires" |
1878 apply(auto simp: inv_on_right_moving.simps inv_after_write.simps ) |
1887 apply(auto simp: inv_on_right_moving.simps inv_after_write.simps ) |
1879 apply(case_tac mr, auto simp: split: if_splits) |
1888 apply(case_tac mr, auto simp: split: if_splits) |
1880 apply(case_tac [!] mr, simp_all) |
|
1881 done |
1889 done |
1882 |
1890 |
1883 lemma [simp]: "inv_on_right_moving (as, lm) (x, l, []) ires\<Longrightarrow> |
1891 lemma [simp]: "inv_on_right_moving (as, lm) (x, l, []) ires\<Longrightarrow> |
1884 inv_on_right_moving (as, lm) (y, l, [Bk]) ires" |
1892 inv_on_right_moving (as, lm) (y, l, [Bk]) ires" |
1885 apply(auto simp: inv_on_right_moving.simps) |
1893 apply(auto simp: inv_on_right_moving.simps) |