--- 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 \<Rightarrow> nat \<Rightarrow> instr list"
- where
- "sete tp e = map (\<lambda> (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 \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 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) \<Rightarrow> config \<Rightarrow> cell list \<Rightarrow> 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 "\<exists> stp la ra. steps (s, l, r) (shift ?A ?off @ ?B, ?off) stp = (start_of ly as + 2*n, la, ra)
\<and> inv_locate_a (as, lm) (n, la, ra) ires"
proof -
@@ -3693,7 +3686,7 @@
"(map (length \<circ> (\<lambda>(xa, y). ci (layout_of xs @ [length_of x]) xa y)) (tpairs_of xs)) =
(map (length \<circ> (\<lambda>(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