diff -r 8a3e63163910 -r 582916f289ea thys/Abacus.thy --- 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 \ nat \ nat \ 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 \ nat \ 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 \ 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 \ 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 \ bool" - where - "t_ncorrect tp = (length tp mod 2 = 0)" - -fun abc2t_correct :: "abc_prog \ bool" - where - "abc2t_correct ap = list_all (\ (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 \ nat) list \ nat \ nat \ (taction \ 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 \ nat \ block \ taction \ nat" - where - "nfetch p 0 b = (Nop, 0)" | - "nfetch p (Suc s) b = - (case b of - Bk \ nnth_of p s 0 | - Oc \ 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\ml @ Bk # @ Bk # Bk # ires) \ (r = Oc\mr @ [Bk] @ @ Bk\rn \ (lm2 = [] \ r = Oc\mr)) )" -(* -fun dec_inv_1 :: "layout \ nat \ nat \ 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 - \ 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 \ nat \ nat \ 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 - \ 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 "\ 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 \ []\ - \ 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 "\ 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 "\ 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]: "\dec_first_on_right_moving n (as, am) (s, aaa, Oc # xs) ires\ \ 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 # @ 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 \ 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 "\ 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 "\stp\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\n \ 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\n \ 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 "\ stp k. steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp = (0, Bk # Bk # ires, @ Bk\k)" - using assms -proof - - have "\ stp k. steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp = - (start_of ly (length ap), Bk # Bk # ires, @ Bk\k)" - proof - - have "\ stp k. steps (Suc 0, l, r) (tp, 0) stp = - (start_of ly (length ap), Bk # Bk # ires, @ Bk\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, @ Bk\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, @ Bk\k)" - by blast - thus "\stp k. steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp - = (0, Bk # Bk # ires, @ Bk \ 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 \ instr list" where