--- a/thys/Abacus.thy Sun Feb 10 20:56:08 2013 +0000
+++ b/thys/Abacus.thy Mon Feb 11 00:08:54 2013 +0000
@@ -1,60 +1,26 @@
-header {*
- {\em abacus} a kind of register machine
-*}
-
theory Abacus
imports Uncomputable
begin
-(*
-declare tm_comp.simps [simp add]
-declare adjust.simps[simp add]
-declare shift.simps[simp add]
-declare tm_wf.simps[simp add]
-declare step.simps[simp add]
-declare steps.simps[simp add]
-*)
declare replicate_Suc[simp add]
-text {*
- {\em Abacus} instructions:
-*}
+(* Abacus instructions *)
datatype abc_inst =
- -- {* @{text "Inc n"} increments the memory cell (or register) with address @{text "n"} by one.
- *}
Inc nat
- -- {*
- @{text "Dec n label"} decrements the memory cell with address @{text "n"} by one.
- If cell @{text "n"} is already zero, no decrements happens and the executio jumps to
- the instruction labeled by @{text "label"}.
- *}
| Dec nat nat
- -- {*
- @{text "Goto label"} unconditionally jumps to the instruction labeled by @{text "label"}.
- *}
| Goto nat
-
-text {*
- Abacus programs are defined as lists of Abacus instructions.
-*}
type_synonym abc_prog = "abc_inst list"
-section {*
- Sample Abacus programs
- *}
-
-text {*
- Abacus for addition and clearance.
-*}
+section {* Some Sample Abacus programs *}
+
+(* Abacus for addition and clearance *)
fun plus_clear :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"
where
"plus_clear m n e = [Dec m e, Inc n, Goto 0]"
-text {*
- Abacus for clearing memory untis.
-*}
+(* Abacus for clearing memory untis *)
fun clear :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
where
"clear n e = [Dec n e, Goto 0]"
@@ -72,17 +38,8 @@
where
"expo n m1 m2 p e = [Inc n, Dec m1 e] @ mult m2 n n p 2"
-
-text {*
- The state of Abacus machine.
- *}
type_synonym abc_state = nat
-(* text {*
- The memory of Abacus machine is defined as a function from address to contents.
-*}
-type_synonym abc_mem = "nat \<Rightarrow> nat" *)
-
text {*
The memory of Abacus machine is defined as a list of contents, with
every units addressed by index into the list.
@@ -312,33 +269,16 @@
fun tm_of :: "abc_prog \<Rightarrow> instr list"
where "tm_of ap = concat (tms_of ap)"
-text {*
- The following two functions specify the well-formedness of complied TM.
-*}
-(*
-fun t_ncorrect :: "tprog \<Rightarrow> bool"
- where
- "t_ncorrect tp = (length tp mod 2 = 0)"
-
-fun abc2t_correct :: "abc_prog \<Rightarrow> bool"
- where
- "abc2t_correct ap = list_all (\<lambda> (n, tm).
- t_ncorrect (ci (layout_of ap) n tm)) (tpairs_of ap)"
-*)
-
lemma length_findnth:
"length (findnth n) = 4 * n"
-apply(induct n, auto)
-done
+by (induct n, auto)
lemma ci_length : "length (ci ns n ai) div 2 = length_of ai"
apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth
split: abc_inst.splits)
done
-subsection {*
- Representation of Abacus memory by TM tape
-*}
+subsection {* Representation of Abacus memory by TM tapes *}
text {*
@{text "crsp acf tcf"} meams the abacus configuration @{text "acf"}
@@ -353,28 +293,6 @@
declare crsp.simps[simp del]
-subsection {*
- A more general definition of TM execution.
-*}
-
-(*
-fun nnth_of :: "(taction \<times> nat) list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (taction \<times> nat)"
- where
- "nnth_of p s b = (if 2*s < length p
- then (p ! (2*s + b)) else (Nop, 0))"
-
-thm nth_of.simps
-
-fun nfetch :: "tprog \<Rightarrow> nat \<Rightarrow> block \<Rightarrow> taction \<times> nat"
- where
- "nfetch p 0 b = (Nop, 0)" |
- "nfetch p (Suc s) b =
- (case b of
- Bk \<Rightarrow> nnth_of p s 0 |
- Oc \<Rightarrow> nnth_of p s 1)"
-*)
-
-
text {*
The type of invarints expressing correspondence between
Abacus configuration and TM configuration.
@@ -388,10 +306,6 @@
ci.simps [simp del] length_of.simps[simp del]
layout_of.simps[simp del]
-(*
-subsection {* The compilation of @{text "Inc n"} *}
-*)
-
text {*
The lemmas in this section lead to the correctness of
the compilation of @{text "Inc n"} instruction.
@@ -2327,29 +2241,6 @@
else l = Oc\<up>ml @ Bk # <rev lm1> @ Bk # Bk # ires) \<and>
(r = Oc\<up>mr @ [Bk] @ <lm2>@ Bk\<up>rn \<or> (lm2 = [] \<and> r = Oc\<up>mr))
)"
-(*
-fun dec_inv_1 :: "layout \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> dec_inv_t"
- where
- "dec_inv_1 ly n e (as, am) (s, l, r) ires =
- (let ss = start_of ly as in
- let am' = abc_lm_s am n (abc_lm_v am n - Suc 0) in
- let am'' = abc_lm_s am n (abc_lm_v am n) in
- if s = start_of ly e then inv_stop (as, am'') (s, l, r) ires
- else if s = ss then False
- else if s = ss + 2 * n then
- inv_locate_a (as, am) (n, l, r) ires
- \<or> inv_locate_a (as, am'') (n, l, r) ires
- else if s = ss + 2 * n + 1 then
- inv_locate_b (as, am) (n, l, r) ires
- else if s = ss + 2 * n + 13 then
- inv_on_left_moving (as, am'') (s, l, r) ires
- else if s = ss + 2 * n + 14 then
- inv_check_left_moving (as, am'') (s, l, r) ires
- else if s = ss + 2 * n + 15 then
- inv_after_left_moving (as, am'') (s, l, r) ires
- else False)"
-*)
-
fun dec_inv_1 :: "layout \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> dec_inv_t"
where
@@ -2832,50 +2723,6 @@
apply(auto simp: inv_locate_b.simps in_middle.simps split: if_splits)
done
-(*
-
-lemma inv_locate_b_2_on_left_moving_b[simp]:
- "inv_locate_b (as, am) (n, l, []) ires
- \<Longrightarrow> inv_on_left_moving (as,
- abc_lm_s am n (abc_lm_v am n)) (s, [], [Bk]) ires"
-apply(auto simp: inv_locate_b.simps inv_on_left_moving.simps inv_on_left_moving_in_middle_B.simps
- in_middle.simps split: if_splits)
-apply(drule_tac length_equal, simp)
-
-apply(insert inv_locate_b_2_on_left_moving[of as am n l "[]" ires s])
-apply(simp only: inv_on_left_moving.simps, simp)
-apply(subgoal_tac "\<not> inv_on_left_moving_in_middle_B
- (as, abc_lm_s am n (abc_lm_v am n)) (s, tl l, [hd l]) ires", simp)
-*)
-
-(*
-lemma [simp]:
- "inv_locate_b (as, am) (n, l, []) ires; l \<noteq> []\<rbrakk>
- \<Longrightarrow> inv_on_left_moving (as, abc_lm_s am n
- (abc_lm_v am n)) (s, tl l, [hd l]) ires"
-apply(auto simp: inv_locate_b.simps inv_on_left_moving.simps inv_on_left_moving_in_middle_B.simps
- in_middle.simps split: if_splits)
-apply(drule_tac length_equal, simp)
-
-apply(insert inv_locate_b_2_on_left_moving[of as am n l "[]" ires s])
-apply(simp only: inv_on_left_moving.simps, simp)
-apply(subgoal_tac "\<not> inv_on_left_moving_in_middle_B
- (as, abc_lm_s am n (abc_lm_v am n)) (s, tl l, [hd l]) ires", simp)
-
-apply(insert inv_locate_b_2_on_left_moving[of as am n l "[]" ires s])
-apply(simp only: inv_on_left_moving.simps, simp)
-apply(subgoal_tac "\<not> inv_on_left_moving_in_middle_B
- (as, abc_lm_s am n (abc_lm_v am n)) (s, tl l, [hd l]) ires", simp)
-apply(simp only: inv_on_left_moving_norm.simps)
-apply(erule_tac exE)+
-apply(erule_tac conjE)+
-apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI,
- rule_tac x = m in exI, rule_tac x = ml in exI,
- rule_tac x = mr in exI, simp)
-apply(case_tac mr, simp, simp, case_tac nat, auto intro: nil_2_nil)
-done
-*)
-
lemma [simp]:
"\<lbrakk>dec_first_on_right_moving n (as, am) (s, aaa, Oc # xs) ires\<rbrakk>
\<Longrightarrow> dec_first_on_right_moving n (as, am) (s', Oc # aaa, xs) ires"
@@ -3051,14 +2898,6 @@
apply(auto simp: dec_left_move.simps inv_on_left_moving.simps split: if_splits)
done
-(*
-lemma [simp]: "inv_on_left_moving_in_middle_B (as, lm1 @ [m])
- (s', Oc # Oc\<^bsup>m\<^esup> @ Bk # <rev lm1> @ Bk\<^bsup>ln\<^esup>, [Bk]) ires"
-apply(auto simp: inv_on_left_moving_in_middle_B.simps)
-apply(rule_tac x = "lm1 @ [m]" in exI, rule_tac x = "[]" in exI, auto)
-done
-*)
-
lemma [simp]: "dec_left_move (as, am) (s, l, []) ires
\<Longrightarrow> inv_on_left_moving (as, am) (s', tl l, [hd l]) ires"
apply(auto simp: dec_left_move.simps inv_on_left_moving.simps split: if_splits)
@@ -3848,33 +3687,6 @@
and crsp: "crsp ly (as, lm) (s, l, r) ires"
shows "\<exists> stp. crsp ly (abc_steps_l (as, lm) ap n)
(steps (s, l, r) (tp, 0) stp) ires"
-(*
-proof(induct n)
- case 0
- have "crsp ly (abc_steps_l (as, lm) ap 0) (steps (s, l, r) (tp, 0) 0) ires"
- using crsp by(simp add: steps.simps abc_steps_l.simps)
- thus "?case"
- by(rule_tac x = 0 in exI, simp)
-next
- case (Suc n)
- obtain as' lm' where a: "abc_steps_l (as, lm) ap n = (as', lm')"
- by(case_tac "abc_steps_l (as, lm) ap n", auto)
- have "\<exists>stp\<ge>n. crsp ly (abc_steps_l (as, lm) ap n) (steps (s, l, r) (tp, 0) stp) ires"
- by fact
- from this a obtain stpa where b:
- "stpa\<ge>n \<and> crsp ly (as', lm') (steps (s, l, r) (tp, 0) stpa) ires" by auto
- obtain s' l' r' where "steps (s, l, r) (tp, 0) stpa = (s', l', r')"
- by(case_tac "steps (s, l, r) (tp, 0) stpa")
- then have "stpa\<ge>n \<and> crsp ly (as', lm') (s', l', r') ires" using b by simp
- from a and this show "?case"
- proof(cases "abc_fetch as' ap")
- case None
-
-
-
- have "crsp ly (abc_steps_l (as, lm) ap 0) (steps (s, l, r) (tp, 0) stp) ires"
- apply(simp add: steps.simps abc_steps_l.simps)
-*)
using crsp
apply(induct n)
apply(rule_tac x = 0 in exI)
@@ -3970,43 +3782,7 @@
apply(case_tac b)
apply(simp_all add: start_of.simps fetch.simps nth_append)
done
-(*
-lemma tp_correct:
- assumes layout: "ly = layout_of ap"
- and compile: "tp = tm_of ap"
- and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires"
- and abc_halt: "abc_steps_l (0, lm) ap stp = (length ap, am)"
- shows "\<exists> stp k. steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp = (0, Bk # Bk # ires, <am> @ Bk\<up>k)"
- using assms
-proof -
- have "\<exists> stp k. steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp =
- (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)"
- proof -
- have "\<exists> stp k. steps (Suc 0, l, r) (tp, 0) stp =
- (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)"
- using assms
- apply(rule_tac tp_correct', simp_all)
- done
- from this obtain stp k where "steps (Suc 0, l, r) (tp, 0) stp =
- (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)" by blast
- thus "?thesis"
- apply(rule_tac x = stp in exI, rule_tac x = k in exI)
- apply(drule_tac tm_append_first_steps_eq, simp_all)
- done
- qed
- from this obtain stp k where
- "steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp =
- (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)"
- by blast
- thus "\<exists>stp k. steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp
- = (0, Bk # Bk # ires, <am> @ Bk \<up> k)"
- using assms
- apply(rule_tac x = "stp + Suc 0" in exI)
- apply(simp add: steps_add)
- apply(auto simp: step.simps)
- done
-qed
- *)
+
(********for mopup***********)
fun mopup_a :: "nat \<Rightarrow> instr list"
where