diff -r 5974111de158 -r f1ecb4a68a54 thys/Abacus.thy --- a/thys/Abacus.thy Thu Feb 21 05:33:57 2013 +0000 +++ b/thys/Abacus.thy Thu Feb 21 05:34:39 2013 +0000 @@ -147,14 +147,6 @@ (R, 17), (W0, 13), (L, 15), (L, 14), (R, 16), (L, 14), (R, 0), (W0, 16)]" -text {* - @{text "sete tp e"} attaches the termination edges (edges leading to state @{text "0"}) - of TM @{text "tp"} to the intruction labelled by @{text "e"}. - *} - -fun sete :: "instr list \ nat \ instr list" - where - "sete tp e = map (\ (action, state). (action, if state = 0 then e else state)) tp" text {* @{text "tdec ss n label"} returns the TM which simulates the execution of @@ -165,7 +157,7 @@ fun tdec :: "nat \ nat \ nat \ instr list" where - "tdec ss n e = shift (findnth n) (ss - 1) @ sete (shift (shift tdec_b (2 * n)) (ss - 1)) e" + "tdec ss n e = shift (findnth n) (ss - 1) @ adjust (shift (shift tdec_b (2 * n)) (ss - 1)) e" text {* @{text "tgoto f(label)"} returns the TM simulating the execution of Abacus instruction @@ -255,7 +247,8 @@ 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) + split: abc_inst.splits simp del: adjust.simps) + done subsection {* Representation of Abacus memory by TM tapes *} @@ -2118,7 +2111,7 @@ qed subsection{* Crsp of Dec n e*} -declare sete.simps[simp del] +declare adjust.simps[simp del] type_synonym dec_inv_t = "(nat * nat list) \ config \ cell list \ bool" @@ -2223,13 +2216,13 @@ lemma [simp]: "fetch (ci ly (start_of ly as) (Dec n e)) (Suc (2 * n)) Bk = (W1, start_of ly as + 2 *n)" apply(auto simp: fetch.simps length_ci_dec) -apply(auto simp: ci.simps nth_append length_findnth sete.simps shift.simps tdec_b_def) +apply(auto simp: ci.simps nth_append length_findnth adjust.simps shift.simps tdec_b_def) using startof_not0[of ly as] by simp lemma [simp]: "fetch (ci ly (start_of ly as) (Dec n e)) (Suc (2 * n)) Oc = (R, Suc (start_of ly as) + 2 *n)" apply(auto simp: fetch.simps length_ci_dec) -apply(auto simp: ci.simps nth_append length_findnth sete.simps shift.simps tdec_b_def) +apply(auto simp: ci.simps nth_append length_findnth adjust.simps shift.simps tdec_b_def) done lemma [simp]: @@ -2379,7 +2372,7 @@ lemma [simp]:"fetch (ci (ly) (start_of ly as) (Dec n e)) (Suc (2 * n)) Oc = (R, start_of ly as + 2*n + 1)" apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done lemma [simp]: "(start_of ly as = 0) = False" @@ -2390,7 +2383,7 @@ (start_of ly as) (Dec n e)) (Suc (2 * n)) Bk = (W1, start_of ly as + 2*n)" apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done lemma [simp]: @@ -2398,7 +2391,7 @@ (start_of ly as) (Dec n e)) (Suc (Suc (2 * n))) Oc = (R, start_of ly as + 2*n + 2)" apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done @@ -2406,7 +2399,7 @@ (start_of ly as) (Dec n e)) (Suc (Suc (2 * n))) Bk = (L, start_of ly as + 2*n + 13)" apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done @@ -2414,7 +2407,7 @@ (start_of ly as) (Dec n e)) (Suc (Suc (Suc (2 * n)))) Oc = (R, start_of ly as + 2*n + 2)" apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done @@ -2422,7 +2415,7 @@ (Suc (Suc (Suc (2 * n)))) Bk = (L, start_of ly as + 2*n + 3)" apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done lemma [simp]: @@ -2431,7 +2424,7 @@ = (W0, start_of ly as + 2*n + 3)" apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done lemma [simp]: "fetch (ci (ly) @@ -2439,7 +2432,7 @@ = (R, start_of ly as + 2*n + 4)" apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done lemma [simp]:"fetch (ci (ly) @@ -2447,7 +2440,7 @@ = (R, start_of ly as + 2*n + 5)" apply(subgoal_tac "2*n + 5 = Suc (2*n + 4)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done @@ -2457,7 +2450,7 @@ = (L, start_of ly as + 2*n + 6)" apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done lemma [simp]: @@ -2466,7 +2459,7 @@ = (L, start_of ly as + 2*n + 7)" apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done lemma [simp]:"fetch (ci (ly) @@ -2474,7 +2467,7 @@ = (L, start_of ly as + 2*n + 10)" apply(subgoal_tac "2*n + 7 = Suc (2*n + 6)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done lemma [simp]: @@ -2483,7 +2476,7 @@ = (W1, start_of ly as + 2*n + 7)" apply(subgoal_tac "2*n + 8 = Suc (2*n + 7)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done @@ -2493,7 +2486,7 @@ = (R, start_of ly as + 2*n + 8)" apply(subgoal_tac "2*n + 8 = Suc (2*n + 7)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done lemma [simp]: @@ -2502,7 +2495,7 @@ = (L, start_of ly as + 2*n + 9)" apply(subgoal_tac "2*n + 9 = Suc (2*n + 8)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done lemma [simp]: @@ -2511,7 +2504,7 @@ = (R, start_of ly as + 2*n + 8)" apply(subgoal_tac "2*n + 9 = Suc (2*n + 8)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done @@ -2521,7 +2514,7 @@ = (R, start_of ly as + 2*n + 4)" apply(subgoal_tac "2*n + 10 = Suc (2*n + 9)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done lemma [simp]: "fetch (ci (ly) @@ -2529,7 +2522,7 @@ = (W0, start_of ly as + 2*n + 9)" apply(subgoal_tac "2*n + 10 = Suc (2*n + 9)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done @@ -2539,7 +2532,7 @@ = (L, start_of ly as + 2*n + 10)" apply(subgoal_tac "2*n + 11 = Suc (2*n + 10)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done @@ -2549,7 +2542,7 @@ = (L, start_of ly as + 2*n + 11)" apply(subgoal_tac "2*n + 11 = Suc (2*n + 10)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done lemma [simp]: @@ -2558,7 +2551,7 @@ = (L, start_of ly as + 2*n + 10)" apply(subgoal_tac "2*n + 12 = Suc (2*n + 11)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done @@ -2568,7 +2561,7 @@ = (R, start_of ly as + 2*n + 12)" apply(subgoal_tac "2*n + 12 = Suc (2*n + 11)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done lemma [simp]: @@ -2577,7 +2570,7 @@ = (R, start_of ly as + 2*n + 16)" apply(subgoal_tac "2*n + 13 = Suc (2*n + 12)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done @@ -2587,7 +2580,7 @@ = (L, start_of ly as + 2*n + 13)" apply(subgoal_tac "14 + 2*n = Suc (2*n + 13)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done lemma [simp]: @@ -2596,7 +2589,7 @@ = (L, start_of ly as + 2*n + 14)" apply(subgoal_tac "14 + 2*n = Suc (2*n + 13)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done lemma [simp]: @@ -2605,7 +2598,7 @@ = (L, start_of ly as + 2*n + 13)" apply(subgoal_tac "15 + 2*n = Suc (2*n + 14)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done lemma [simp]: @@ -2614,7 +2607,7 @@ = (R, start_of ly as + 2*n + 15)" apply(subgoal_tac "15 + 2*n = Suc (2*n + 14)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done lemma [simp]: @@ -2624,7 +2617,7 @@ = (R, start_of (ly) e)" apply(subgoal_tac "16 + 2*n = Suc (2*n + 15)", simp only: fetch.simps) apply(auto simp: ci.simps findnth.simps fetch.simps - nth_of.simps shift.simps nth_append tdec_b_def length_findnth sete.simps) + nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps) done declare dec_inv_1.simps[simp del] @@ -3533,7 +3526,7 @@ proof(simp add: ci.simps) let ?off = "start_of ly as - Suc 0" let ?A = "findnth n" - let ?B = "sete (shift (shift tdec_b (2 * n)) ?off) (start_of ly e)" + let ?B = "adjust (shift (shift tdec_b (2 * n)) ?off) (start_of ly e)" have "\ stp la ra. steps (s, l, r) (shift ?A ?off @ ?B, ?off) stp = (start_of ly as + 2*n, la, ra) \ inv_locate_a (as, lm) (n, la, ra) ires" proof - @@ -3693,7 +3686,7 @@ "(map (length \ (\(xa, y). ci (layout_of xs @ [length_of x]) xa y)) (tpairs_of xs)) = (map (length \ (\(x, y). ci (layout_of xs) x y)) (tpairs_of xs)) " apply(auto) -apply(case_tac b, auto simp: ci.simps sete.simps) +apply(case_tac b, auto simp: ci.simps adjust.simps) done lemma length_tp'[simp]: @@ -3721,7 +3714,7 @@ using tp b apply(auto simp: layout_id_cons tm_of.simps tms_of.simps length_concat tpairs_id_cons map_length_ci) apply(case_tac x) - apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth sete.simps length_of.simps + apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth adjust.simps length_of.simps split: abc_inst.splits) done qed