--- a/Paper/Paper.thy Thu Feb 21 05:33:57 2013 +0000
+++ b/Paper/Paper.thy Thu Feb 21 05:34:39 2013 +0000
@@ -65,6 +65,7 @@
tcontra ("contra") and
code_tcontra ("code contra") and
steps0 ("steps") and
+ adjust0 ("adjust") and
exponent ("_\<^bsup>_\<^esup>") and
tcopy ("copy") and
tape_of ("\<langle>_\<rangle>") and
@@ -163,6 +164,11 @@
and "layout_of ((Goto l)#is) = 1#(layout_of is)"
by(auto simp add: layout_of.simps length_of.simps)
+
+lemma adjust_simps:
+ shows "adjust0 p = map (\<lambda>(a, s). (a, if s = 0 then (Suc (length p div 2)) else s)) p"
+by(simp add: adjust.simps)
+
fun clear :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
where
"clear n e = [Dec n e, Goto 0]"
@@ -552,7 +558,7 @@
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
@{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\
- @{thm (lhs) adjust.simps} @{text "\<equiv>"} @{thm (rhs) adjust.simps}\\
+ @{thm (lhs) adjust_simps} @{text "\<equiv>"} @{thm (rhs) adjust_simps}\\
\end{tabular}
\end{center}
Binary file paper.pdf has changed
--- 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
--- a/thys/Recursive.thy Thu Feb 21 05:33:57 2013 +0000
+++ b/thys/Recursive.thy Thu Feb 21 05:34:39 2013 +0000
@@ -4909,7 +4909,7 @@
lemma tms_any_less:
"\<lbrakk>k < length ap; (a, b) \<in> set (tms_of ap ! k)\<rbrakk> \<Longrightarrow>
b \<le> start_of (layout_of ap) (length ap)"
-apply(case_tac "ap!k", auto simp: tms_of.simps tpairs_of.simps ci.simps shift_append sete.simps)
+apply(case_tac "ap!k", auto simp: tms_of.simps tpairs_of.simps ci.simps shift_append adjust.simps)
apply(erule_tac findnth_state_all_le1, simp_all)
apply(erule_tac inc_state_all_le, simp_all)
apply(erule_tac findnth_state_all_le2, simp_all)
@@ -4951,12 +4951,12 @@
\<Longrightarrow> layout_of ap ! k = qa"
apply(case_tac "ap ! k")
apply(auto simp: layout_of.simps ci.simps
- length_of.simps tinc_b_def tdec_b_def length_findnth sete.simps)
+ length_of.simps tinc_b_def tdec_b_def length_findnth adjust.simps)
done
lemma [intro]: "length (ci ly y i) mod 2 = 0"
apply(case_tac i, auto simp: ci.simps length_findnth
- tinc_b_def sete.simps tdec_b_def)
+ tinc_b_def adjust.simps tdec_b_def)
done
lemma [intro]: "listsum (map (length \<circ> (\<lambda>(x, y). ci ly x y)) zs) mod 2 = 0"
--- a/thys/Turing.thy Thu Feb 21 05:33:57 2013 +0000
+++ b/thys/Turing.thy Thu Feb 21 05:34:39 2013 +0000
@@ -205,16 +205,19 @@
"shift p n = (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)"
fun
- adjust :: "instr list \<Rightarrow> instr list"
+ adjust :: "instr list \<Rightarrow> nat \<Rightarrow> instr list"
where
- "adjust p = map (\<lambda> (a, s). (a, if s = 0 then (Suc (length p div 2)) else s)) p"
+ "adjust p e = map (\<lambda> (a, s). (a, if s = 0 then e else s)) p"
+
+abbreviation
+ "adjust0 p \<equiv> adjust p (Suc (length p div 2))"
lemma length_shift [simp]:
shows "length (shift p n) = length p"
by simp
lemma length_adjust [simp]:
- shows "length (adjust p) = length p"
+ shows "length (adjust p n) = length p"
by (induct p) (auto)
@@ -222,7 +225,7 @@
fun
tm_comp :: "instr list \<Rightarrow> instr list \<Rightarrow> instr list" ("_ |+| _" [0, 0] 100)
where
- "tm_comp p1 p2 = ((adjust p1) @ (shift p2 (length p1 div 2)))"
+ "tm_comp p1 p2 = ((adjust0 p1) @ (shift p2 (length p1 div 2)))"
lemma tm_comp_length:
shows "length (A |+| B) = length A + length B"
--- a/thys/UTM.thy Thu Feb 21 05:33:57 2013 +0000
+++ b/thys/UTM.thy Thu Feb 21 05:34:39 2013 +0000
@@ -543,7 +543,7 @@
definition t_twice :: "instr list"
where
- "t_twice = adjust t_twice_compile"
+ "t_twice = adjust0 t_twice_compile"
definition t_fourtimes_compile :: "instr list"
where
@@ -551,7 +551,7 @@
definition t_fourtimes :: "instr list"
where
- "t_fourtimes = adjust t_fourtimes_compile"
+ "t_fourtimes = adjust0 t_fourtimes_compile"
definition t_twice_len :: "nat"
where
@@ -1266,7 +1266,7 @@
lemma adjust_fetch0:
"\<lbrakk>0 < a; a \<le> length ap div 2; fetch ap a b = (aa, 0)\<rbrakk>
- \<Longrightarrow> fetch (adjust ap) a b = (aa, Suc (length ap div 2))"
+ \<Longrightarrow> fetch (adjust0 ap) a b = (aa, Suc (length ap div 2))"
apply(case_tac b, auto simp: fetch.simps nth_of.simps nth_map
split: if_splits)
apply(case_tac [!] a, auto simp: fetch.simps nth_of.simps)
@@ -1274,7 +1274,7 @@
lemma adjust_fetch_norm:
"\<lbrakk>st > 0; st \<le> length tp div 2; fetch ap st b = (aa, ns); ns \<noteq> 0\<rbrakk>
- \<Longrightarrow> fetch (Turing.adjust ap) st b = (aa, ns)"
+ \<Longrightarrow> fetch (adjust0 ap) st b = (aa, ns)"
apply(case_tac b, auto simp: fetch.simps nth_of.simps nth_map
split: if_splits)
apply(case_tac [!] st, auto simp: fetch.simps nth_of.simps)
@@ -1286,7 +1286,7 @@
assumes exec: "step0 (st,l,r) ap = (st', l', r')"
and wf_tm: "tm_wf (ap, 0)"
and notfinal: "st' > 0"
- shows "step0 (st, l, r) (adjust ap) = (st', l', r')"
+ shows "step0 (st, l, r) (adjust0 ap) = (st', l', r')"
using assms
proof -
have "st > 0"
@@ -1300,7 +1300,7 @@
nth_of.simps adjust.simps tm_wf.simps split: if_splits)
apply(auto simp: mod_ex2)
done
- ultimately have "fetch (adjust ap) st (read r) = fetch ap st (read r)"
+ ultimately have "fetch (adjust0 ap) st (read r) = fetch ap st (read r)"
using assms
apply(case_tac "fetch ap st (read r)")
apply(drule_tac adjust_fetch_norm, simp_all)
@@ -1317,7 +1317,7 @@
assumes exec: "steps0 (st,l,r) ap stp = (st', l', r')"
and wf_tm: "tm_wf (ap, 0)"
and notfinal: "st' > 0"
- shows "steps0 (st, l, r) (adjust ap) stp = (st', l', r')"
+ shows "steps0 (st, l, r) (adjust0 ap) stp = (st', l', r')"
using exec notfinal
proof(induct stp arbitrary: st' l' r')
case 0
@@ -1326,7 +1326,7 @@
next
case (Suc stp st' l' r')
have ind: "\<And>st' l' r'. \<lbrakk>steps0 (st, l, r) ap stp = (st', l', r'); 0 < st'\<rbrakk>
- \<Longrightarrow> steps0 (st, l, r) (Turing.adjust ap) stp = (st', l', r')" by fact
+ \<Longrightarrow> steps0 (st, l, r) (adjust0 ap) stp = (st', l', r')" by fact
have h: "steps0 (st, l, r) ap (Suc stp) = (st', l', r')" by fact
have g: "0 < st'" by fact
obtain st'' l'' r'' where a: "steps0 (st, l, r) ap stp = (st'', l'', r'')"
@@ -1336,7 +1336,7 @@
apply(simp add: step_red)
apply(case_tac st'', auto)
done
- hence b: "steps0 (st, l, r) (Turing.adjust ap) stp = (st'', l'', r'')"
+ hence b: "steps0 (st, l, r) (adjust0 ap) stp = (st'', l'', r'')"
using a
by(rule_tac ind, simp_all)
thus "?case"
@@ -1349,7 +1349,7 @@
lemma adjust_halt_eq:
assumes exec: "steps0 (1, l, r) ap stp = (0, l', r')"
and tm_wf: "tm_wf (ap, 0)"
- shows "\<exists> stp. steps0 (Suc 0, l, r) (adjust ap) stp =
+ shows "\<exists> stp. steps0 (Suc 0, l, r) (adjust0 ap) stp =
(Suc (length ap div 2), l', r')"
proof -
have "\<exists> stp. \<not> is_final (steps0 (1, l, r) ap stp) \<and> (steps0 (1, l, r) ap (Suc stp) = (0, l', r'))"
@@ -1358,7 +1358,7 @@
then obtain stpa where a:
"\<not> is_final (steps0 (1, l, r) ap stpa) \<and> (steps0 (1, l, r) ap (Suc stpa) = (0, l', r'))" ..
obtain sa la ra where b:"steps0 (1, l, r) ap stpa = (sa, la, ra)" by (metis prod_cases3)
- hence c: "steps0 (Suc 0, l, r) (adjust ap) stpa = (sa, la, ra)"
+ hence c: "steps0 (Suc 0, l, r) (adjust0 ap) stpa = (sa, la, ra)"
using assms a
apply(rule_tac adjust_steps_eq, simp_all)
done
@@ -1371,7 +1371,7 @@
using b a
apply(simp add: step_red step.simps)
done
- have k: "fetch (adjust ap) sa (read ra) = (ac, Suc (length ap div 2))"
+ have k: "fetch (adjust0 ap) sa (read ra) = (ac, Suc (length ap div 2))"
using a b c d e f
apply(rule_tac adjust_fetch0, simp_all)
done
@@ -1402,14 +1402,14 @@
(tm_of abc_twice @ shift (mopup (Suc 0)) ((length (tm_of abc_twice) div 2))) stp =
(0, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))" by blast
hence "\<exists> stp. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
- (adjust t_twice_compile) stp
+ (adjust0 t_twice_compile) stp
= (Suc (length t_twice_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))"
apply(rule_tac stp = stp in adjust_halt_eq)
apply(simp add: t_twice_compile_def, auto)
done
then obtain stpb where
"steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
- (adjust t_twice_compile) stpb
+ (adjust0 t_twice_compile) stpb
= (Suc (length t_twice_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))" ..
thus "?thesis"
apply(simp add: t_twice_def t_twice_len_def)
@@ -2079,14 +2079,14 @@
(tm_of abc_fourtimes @ shift (mopup 1) ((length (tm_of abc_fourtimes) div 2))) stp =
(0, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))" by blast
hence "\<exists> stp. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
- (adjust t_fourtimes_compile) stp
+ (adjust0 t_fourtimes_compile) stp
= (Suc (length t_fourtimes_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))"
apply(rule_tac stp = stp in adjust_halt_eq)
apply(simp add: t_fourtimes_compile_def, auto)
done
then obtain stpb where
"steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
- (adjust t_fourtimes_compile) stpb
+ (adjust0 t_fourtimes_compile) stpb
= (Suc (length t_fourtimes_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))" ..
thus "?thesis"
apply(simp add: t_fourtimes_def t_fourtimes_len_def)
@@ -3356,7 +3356,7 @@
lemma tm_wf_change_termi: "tm_wf (tp, 0) \<Longrightarrow>
- list_all (\<lambda>(acn, st). (st \<le> Suc (length tp div 2))) (adjust tp)"
+ list_all (\<lambda>(acn, st). (st \<le> Suc (length tp div 2))) (adjust0 tp)"
apply(auto simp: tm_wf.simps List.list_all_length)
apply(case_tac "tp!n", auto simp: adjust.simps split: if_splits)
apply(erule_tac x = "(a, b)" in ballE, auto)
@@ -3376,28 +3376,36 @@
apply(auto simp: mopup.simps)
done
-lemma [elim]: "(a, b) \<in> set (shift (Turing.adjust t_twice_compile) 12) \<Longrightarrow>
+lemma [elim]: "(a, b) \<in> set (shift (adjust0 t_twice_compile) 12) \<Longrightarrow>
b \<le> (28 + (length t_twice_compile + length t_fourtimes_compile)) div 2"
apply(simp add: t_twice_compile_def t_fourtimes_compile_def)
proof -
- assume g: "(a, b) \<in> set (shift (Turing.adjust (tm_of abc_twice @ shift (mopup (Suc 0)) (length (tm_of abc_twice) div 2))) 12)"
+ assume g: "(a, b)
+ \<in> set (shift
+ (adjust
+ (tm_of abc_twice @
+ shift (mopup (Suc 0)) (length (tm_of abc_twice) div 2))
+ (Suc ((length (tm_of abc_twice) + 16) div 2)))
+ 12)"
moreover have "length (tm_of abc_twice) mod 2 = 0" by auto
moreover have "length (tm_of abc_fourtimes) mod 2 = 0" by auto
ultimately have "list_all (\<lambda>(acn, st). (st \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2))
- (shift (Turing.adjust t_twice_compile) 12)"
- proof(auto simp: mod_ex1)
+ (shift (adjust0 t_twice_compile) 12)"
+ proof(auto simp add: mod_ex1 del: adjust.simps)
fix q qa
assume h: "length (tm_of abc_twice) = 2 * q" "length (tm_of abc_fourtimes) = 2 * qa"
- hence "list_all (\<lambda>(acn, st). st \<le> (18 + (q + qa)) + 12) (shift (Turing.adjust t_twice_compile) 12)"
+ hence "list_all (\<lambda>(acn, st). st \<le> (18 + (q + qa)) + 12) (shift (adjust0 t_twice_compile) 12)"
proof(rule_tac tm_wf_shift t_twice_compile_def)
- have "list_all (\<lambda>(acn, st). st \<le> Suc (length t_twice_compile div 2)) (adjust t_twice_compile)"
+ have "list_all (\<lambda>(acn, st). st \<le> Suc (length t_twice_compile div 2)) (adjust0 t_twice_compile)"
by(rule_tac tm_wf_change_termi, auto)
- thus "list_all (\<lambda>(acn, st). st \<le> 18 + (q + qa)) (Turing.adjust t_twice_compile)"
+ thus "list_all (\<lambda>(acn, st). st \<le> 18 + (q + qa)) (adjust0 t_twice_compile)"
using h
apply(simp add: t_twice_compile_def, auto simp: List.list_all_length)
done
qed
- thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa)) (shift (Turing.adjust t_twice_compile) 12)"
+ thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa))
+ (shift
+ (adjust t_twice_compile (Suc (length t_twice_compile div 2))) 12)"
by simp
qed
thus "b \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2"
@@ -3408,37 +3416,50 @@
done
qed
-lemma [elim]: "(a, b) \<in> set (shift (Turing.adjust t_fourtimes_compile) (t_twice_len + 13))
+lemma [elim]: "(a, b) \<in> set (shift (adjust0 t_fourtimes_compile) (t_twice_len + 13))
\<Longrightarrow> b \<le> (28 + (length t_twice_compile + length t_fourtimes_compile)) div 2"
apply(simp add: t_twice_compile_def t_fourtimes_compile_def t_twice_len_def)
proof -
- assume g: "(a, b) \<in> set (shift (Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0))
- (length (tm_of abc_fourtimes) div 2))) (length t_twice div 2 + 13))"
+ assume g: "(a, b)
+ \<in> set (shift
+ (adjust
+ (tm_of abc_fourtimes @
+ shift (mopup (Suc 0)) (length (tm_of abc_fourtimes) div 2))
+ (Suc ((length (tm_of abc_fourtimes) + 16) div 2)))
+ (length t_twice div 2 + 13))"
moreover have "length (tm_of abc_twice) mod 2 = 0" by auto
moreover have "length (tm_of abc_fourtimes) mod 2 = 0" by auto
ultimately have "list_all (\<lambda>(acn, st). (st \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2))
- (shift (Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0))
+ (shift (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0))
(length (tm_of abc_fourtimes) div 2))) (length t_twice div 2 + 13))"
proof(auto simp: mod_ex1 t_twice_def t_twice_compile_def)
fix q qa
assume h: "length (tm_of abc_twice) = 2 * q" "length (tm_of abc_fourtimes) = 2 * qa"
hence "list_all (\<lambda>(acn, st). st \<le> (9 + qa + (21 + q)))
- (shift (Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)) (21 + q))"
+ (shift (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)) (21 + q))"
proof(rule_tac tm_wf_shift t_twice_compile_def)
have "list_all (\<lambda>(acn, st). st \<le> Suc (length (tm_of abc_fourtimes @ shift
- (mopup (Suc 0)) qa) div 2)) (adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa))"
+ (mopup (Suc 0)) qa) div 2)) (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa))"
apply(rule_tac tm_wf_change_termi)
using wf_fourtimes h
apply(simp add: t_fourtimes_compile_def)
- done
- thus "list_all (\<lambda>(acn, st). st \<le> 9 + qa) ((Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)))"
+ done
+ thus "list_all (\<lambda>(acn, st). st \<le> 9 + qa)
+ (adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)
+ (Suc (length (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa) div
+ 2)))"
using h
apply(simp)
done
qed
- thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa)) (shift (Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)) (21 + q))"
+ thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa))
+ (shift
+ (adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)
+ (9 + qa))
+ (21 + q))"
apply(subgoal_tac "qa + q = q + qa")
- apply(simp, simp)
+ apply(simp add: h)
+ apply(simp)
done
qed
thus "b \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2"
@@ -3515,7 +3536,7 @@
apply(auto simp: Hoare_halt_def)
apply(rule_tac x = n in exI)
apply(case_tac "(steps0 (Suc 0, [], <m # args>)
- (Turing.adjust t_wcode_prepare @ shift t_wcode_main (length t_wcode_prepare div 2)) n)")
+ (adjust0 t_wcode_prepare @ shift t_wcode_main (length t_wcode_prepare div 2)) n)")
apply(auto simp: tm_comp.simps)
done
qed
@@ -4613,7 +4634,7 @@
*}
definition t_wcode :: "instr list"
where
- "t_wcode = (t_wcode_prepare |+| t_wcode_main) |+| t_wcode_adjust"
+ "t_wcode = (t_wcode_prepare |+| t_wcode_main) |+| t_wcode_adjust "
text {*