Theory AlphabetEnlargement_ForwardCells
theory AlphabetEnlargement_ForwardCells
imports AlphabetEnlargement_OutputWF
begin
subsection ‹Forward-stage per-tape reconstruction leaves›
text ‹Base of the forward-stage chain
‹ForwardCells → ForwardStep → ForwardStage›. The unified
forward-stage lemma ‹ae_simulates_forward_stage_general› (theory
‹AlphabetEnlargement_ForwardStage›) advances the simulation by one
‹M›-step through eight substeps (‹SS1› through ‹SS8›);
the ‹SS5›--‹SS8› half is packaged as the super-step
‹ae_forward_stage_step_chain› (theory
‹AlphabetEnlargement_ForwardStep›). From the configs
‹c5›--‹c8› that super-step exposes, the lemma then
reconstructs, tape by tape, where each simulated head sits and what its
in-window blocks hold. The nine lemmas in this theory are those
per-tape reconstruction facts.
Each branches on the tape's block position ‹mt_pos c' kk›
into the three regimes (steady ‹≥ 2›, le1 ‹= 1›, le0
‹= 0›) and reads off the ‹c5›--‹c8› intermediate
configs the super-step exposes. They group into the head-position
trajectories (‹ae_fwd_c8_pos_for_*›, ‹ae_fwd_c6_pos_for_*›,
‹ae_fwd_pos_decode_c8›), the in-window cell values
(‹ae_fwd_c8_at_*›), and the per-tape tape-correspondence
(‹ae_fwd_tape_corr_c8›). Each was extracted from the unified
lemma's proof, so its assumption interface is wide: the assumptions are
exactly the data-flow the fact consumed when it was an inline block.›
text ‹Reconstruction leaf of ‹ae_simulates_forward_stage_general› (the
pos-at-least-2 in-window ‹c8› value at block pos minus 1).›
lemma ae_fwd_c8_at_pos_minus_1_ge2:
fixes M :: "('q, 'a) mttm"
and c' c4 c5 c6 c7 c8 :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
and q5 q6 :: 'q
and ofs5 ofs6 :: "nat ⇒ 'c"
and buf5 buf6 :: "nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)"
and dest5 dest6 :: "nat ⇒ ae_dest"
assumes step5: "(c4, c5) ∈ mttm_step (alphabet_enlarge_delta M)"
and c5_state: "mt_state c5 = (q5, ofs5, buf5, dest5, SS6)"
and tape_c4_eq_c': "mt_tape c4 = mt_tape c'"
and buf5_not_le_per_tape:
"∀k<k_tm M. (mt_pos c' k = 0
⟶ fst (buf5 k) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))
∧ (mt_pos c' k = 1
⟶ fst (snd (buf5 k)) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))
∧ (mt_pos c' k ≥ 2
⟶ fst (buf5 k) ≠ LE_block (le_tm M)
∧ fst (snd (buf5 k)) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))"
and c4_pos: "⋀kk. kk < k_tm M ⟹ mt_pos c4 kk = mt_pos c' kk"
and step6_sub: "(c5, c6) ∈ mttm_step (ae_delta_ss6_ss7 M)"
and step6: "(c5, c6) ∈ mttm_step (alphabet_enlarge_delta M)"
and step7: "(c6, c7) ∈ mttm_step (alphabet_enlarge_delta M)"
and c7_state: "mt_state c7 = (q6, ofs6, buf6, dest6, SS8)"
and buf6_eq_buf5: "buf6 = buf5"
and dest6_eq_dest5: "dest6 = dest5"
and step8_sub: "(c7, c8) ∈ mttm_step (ae_delta_ss8_ss1 M)"
and step8: "(c7, c8) ∈ mttm_step (alphabet_enlarge_delta M)"
and c5_pos_for_pos_ge2:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2 ⟹ dest5 kk ≠ AE_Left
⟹ mt_pos c5 kk = mt_pos c' kk - 1"
and c5_pos_for_pos_ge2_dest_left:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2 ⟹ dest5 kk = AE_Left
⟹ mt_pos c5 kk = mt_pos c' kk + 1"
and left_not_le_c'_steady:
"∀k. mt_pos c' k ≥ 2
⟶ mt_tape c' k (mt_pos c' k - 1) ≠ LE_block (le_tm M)"
and c6_pos_for_pos_ge2:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2 ⟹ mt_pos c6 kk = mt_pos c' kk"
and c7_pos_for_pos_ge2:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2
⟹ mt_pos c7 kk = (if dest5 kk = AE_Left
then mt_pos c' kk - 1
else mt_pos c' kk + 1)"
shows "⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2
⟹ mt_tape c8 kk (mt_pos c' kk - 1) = fst (buf5 kk)"
proof -
fix kk
assume kklt: "kk < k_tm M"
assume hge2: "mt_pos c' kk ≥ 2"
obtain ll hh rr where buf5_kk: "buf5 kk = (ll, hh, rr)"
using prod.exhaust by metis
have buf6_kk: "buf6 kk = (ll, hh, rr)"
using buf5_kk buf6_eq_buf5 by simp
have h_ne_LE: "hh ≠ LE_block (le_tm M)"
proof -
have "fst (snd (buf5 kk)) ≠ LE_block (le_tm M)"
using buf5_not_le_per_tape[rule_format, OF kklt] hge2 by blast
thus ?thesis using buf5_kk by simp
qed
have c4_kk_eq: "mt_pos c4 kk = mt_pos c' kk" using c4_pos kklt by simp
have pm1_ne_c4: "(mt_pos c' kk - 1) ≠ mt_pos c4 kk"
using c4_kk_eq hge2 by linarith
have c4_at_pm1_ne_LE:
"mt_tape c4 kk (mt_pos c' kk - 1) ≠ LE_block (le_tm M)"
proof -
have "mt_tape c4 kk (mt_pos c' kk - 1) = mt_tape c' kk (mt_pos c' kk - 1)"
using tape_c4_eq_c' by simp
moreover have "mt_tape c' kk (mt_pos c' kk - 1) ≠ LE_block (le_tm M)"
using left_not_le_c'_steady hge2 by blast
ultimately show ?thesis by simp
qed
show "mt_tape c8 kk (mt_pos c' kk - 1) = fst (buf5 kk)"
proof (cases "dest5 kk")
case AE_Left
have c5_pos_kk: "mt_pos c5 kk = mt_pos c' kk + 1"
using c5_pos_for_pos_ge2_dest_left[OF kklt hge2 AE_Left] .
have pm1_ne_c5: "(mt_pos c' kk - 1) ≠ mt_pos c5 kk"
using c5_pos_kk hge2 by linarith
have c6_pos_kk: "mt_pos c6 kk = mt_pos c' kk"
using c6_pos_for_pos_ge2[OF kklt hge2] .
have pm1_ne_c6: "(mt_pos c' kk - 1) ≠ mt_pos c6 kk"
using c6_pos_kk hge2 by linarith
have c7_at_pm1_eq_c4:
"mt_tape c7 kk (mt_pos c' kk - 1) = mt_tape c4 kk (mt_pos c' kk - 1)"
proof -
have "mt_tape c7 kk (mt_pos c' kk - 1)
= mt_tape c6 kk (mt_pos c' kk - 1)"
using mttm_step_tape_off_head[OF step7 pm1_ne_c6] .
also have "… = mt_tape c5 kk (mt_pos c' kk - 1)"
using mttm_step_tape_off_head[OF step6 pm1_ne_c5] .
also have "… = mt_tape c4 kk (mt_pos c' kk - 1)"
using mttm_step_tape_off_head[OF step5 pm1_ne_c4] .
finally show ?thesis .
qed
have c7_pos_kk: "mt_pos c7 kk = mt_pos c' kk - 1"
using c7_pos_for_pos_ge2[OF kklt hge2] AE_Left by simp
obtain qq tts nn qq' aa8 dr8 where
c7_eq8: "c7 = Config⇩M qq tts nn"
and c8_eq: "c8 = Config⇩M qq'
(λk. (tts k)(nn k := aa8 k))
(λk. go_dir (dr8 k) (nn k))"
and tr_in: "(qq, λk. tts k (nn k), qq', aa8, dr8)
∈ ae_delta_ss8_ss1 M"
using step8_sub by (auto elim: mttm_step.cases)
obtain q ofs buf dest where
qq_eq: "qq = (q, ofs, buf, dest, SS8)"
and aa8_eq:
"aa8 = (λk. if k < k_tm M then fst (ae_ss8_action (le_tm M)
(tts k (nn k)) (buf k) (dest k)) else bl_block (bl_tm M))"
using tr_in by (auto simp: ae_delta_ss8_ss1_def)
have qq_state: "qq = (q6, ofs6, buf6, dest6, SS8)"
using c7_state c7_eq8 by simp
have buf_eq: "buf = buf6" using qq_eq qq_state by simp
have dest_eq: "dest = dest6" using qq_eq qq_state by simp
have nn_kk: "nn kk = mt_pos c7 kk" using c7_eq8 by simp
have nn_kk_val: "nn kk = mt_pos c' kk - 1" using nn_kk c7_pos_kk by simp
have read_ne_LE: "tts kk (nn kk) ≠ LE_block (le_tm M)"
proof -
have "tts kk (nn kk) = mt_tape c7 kk (mt_pos c7 kk)"
using c7_eq8 nn_kk by simp
also have "… = mt_tape c7 kk (mt_pos c' kk - 1)" using c7_pos_kk by simp
also have "… = mt_tape c4 kk (mt_pos c' kk - 1)" using c7_at_pm1_eq_c4 .
finally have "tts kk (nn kk) = mt_tape c4 kk (mt_pos c' kk - 1)" .
thus ?thesis using c4_at_pm1_ne_LE by simp
qed
have dest6_AE_Left: "dest6 kk = AE_Left"
using AE_Left dest6_eq_dest5 by simp
have aa8_kk: "aa8 kk = ll"
using aa8_eq buf_eq dest_eq dest6_AE_Left buf6_kk h_ne_LE read_ne_LE kklt
by simp
have "mt_tape c8 kk (mt_pos c' kk - 1) = aa8 kk"
using c8_eq nn_kk_val by simp
also have "… = ll" using aa8_kk .
also have "… = fst (buf5 kk)" using buf5_kk by simp
finally show ?thesis .
next
case AE_Home
have dest_ne_left: "dest5 kk ≠ AE_Left" using AE_Home by simp
have c5_pos_kk: "mt_pos c5 kk = mt_pos c' kk - 1"
using c5_pos_for_pos_ge2[OF kklt hge2 dest_ne_left] .
obtain qq tts nn qq' aa6 dr6 where
c5_eq6: "c5 = Config⇩M qq tts nn"
and c6_eq: "c6 = Config⇩M qq'
(λk. (tts k)(nn k := aa6 k))
(λk. go_dir (dr6 k) (nn k))"
and tr_in: "(qq, λk. tts k (nn k), qq', aa6, dr6)
∈ ae_delta_ss6_ss7 M"
using step6_sub by (auto elim: mttm_step.cases)
obtain q ofs buf dest where
qq_eq: "qq = (q, ofs, buf, dest, SS6)"
and aa6_eq:
"aa6 = (λk. if k < k_tm M then fst (ae_ss6_action (le_tm M)
(tts k (nn k)) (buf k) (dest k)) else bl_block (bl_tm M))"
using tr_in by (auto simp: ae_delta_ss6_ss7_def)
have qq_state: "qq = (q5, ofs5, buf5, dest5, SS6)"
using c5_state c5_eq6 by simp
have buf_eq: "buf = buf5" using qq_eq qq_state by simp
have dest_eq: "dest = dest5" using qq_eq qq_state by simp
have nn_kk: "nn kk = mt_pos c5 kk" using c5_eq6 by simp
have nn_kk_val: "nn kk = mt_pos c' kk - 1" using nn_kk c5_pos_kk by simp
have c5_at_pm1_eq_c4:
"mt_tape c5 kk (mt_pos c' kk - 1) = mt_tape c4 kk (mt_pos c' kk - 1)"
using mttm_step_tape_off_head[OF step5 pm1_ne_c4] .
have read_ne_LE: "tts kk (nn kk) ≠ LE_block (le_tm M)"
proof -
have "tts kk (nn kk) = mt_tape c5 kk (mt_pos c5 kk)"
using c5_eq6 nn_kk by simp
also have "… = mt_tape c5 kk (mt_pos c' kk - 1)" using c5_pos_kk by simp
also have "… = mt_tape c4 kk (mt_pos c' kk - 1)" using c5_at_pm1_eq_c4 .
finally have "tts kk (nn kk) = mt_tape c4 kk (mt_pos c' kk - 1)" .
thus ?thesis using c4_at_pm1_ne_LE by simp
qed
have aa6_kk: "aa6 kk = ll"
using aa6_eq buf_eq dest_eq AE_Home buf5_kk h_ne_LE read_ne_LE kklt by simp
have c6_at_pm1: "mt_tape c6 kk (mt_pos c' kk - 1) = ll"
proof -
have "mt_tape c6 kk (mt_pos c' kk - 1) = aa6 kk"
using c6_eq nn_kk_val by simp
thus ?thesis using aa6_kk by simp
qed
have c6_pos_kk: "mt_pos c6 kk = mt_pos c' kk"
using c6_pos_for_pos_ge2[OF kklt hge2] .
have pm1_ne_c6: "(mt_pos c' kk - 1) ≠ mt_pos c6 kk"
using c6_pos_kk hge2 by linarith
have c7_pos_kk: "mt_pos c7 kk = mt_pos c' kk + 1"
using c7_pos_for_pos_ge2[OF kklt hge2] AE_Home by simp
have pm1_ne_c7: "(mt_pos c' kk - 1) ≠ mt_pos c7 kk"
using c7_pos_kk by linarith
have "mt_tape c8 kk (mt_pos c' kk - 1) = mt_tape c7 kk (mt_pos c' kk - 1)"
using mttm_step_tape_off_head[OF step8 pm1_ne_c7] .
also have "… = mt_tape c6 kk (mt_pos c' kk - 1)"
using mttm_step_tape_off_head[OF step7 pm1_ne_c6] .
also have "… = ll" using c6_at_pm1 .
also have "… = fst (buf5 kk)" using buf5_kk by simp
finally show ?thesis .
next
case AE_Right
have dest_ne_left: "dest5 kk ≠ AE_Left" using AE_Right by simp
have c5_pos_kk: "mt_pos c5 kk = mt_pos c' kk - 1"
using c5_pos_for_pos_ge2[OF kklt hge2 dest_ne_left] .
obtain qq tts nn qq' aa6 dr6 where
c5_eq6: "c5 = Config⇩M qq tts nn"
and c6_eq: "c6 = Config⇩M qq'
(λk. (tts k)(nn k := aa6 k))
(λk. go_dir (dr6 k) (nn k))"
and tr_in: "(qq, λk. tts k (nn k), qq', aa6, dr6)
∈ ae_delta_ss6_ss7 M"
using step6_sub by (auto elim: mttm_step.cases)
obtain q ofs buf dest where
qq_eq: "qq = (q, ofs, buf, dest, SS6)"
and aa6_eq:
"aa6 = (λk. if k < k_tm M then fst (ae_ss6_action (le_tm M)
(tts k (nn k)) (buf k) (dest k)) else bl_block (bl_tm M))"
using tr_in by (auto simp: ae_delta_ss6_ss7_def)
have qq_state: "qq = (q5, ofs5, buf5, dest5, SS6)"
using c5_state c5_eq6 by simp
have buf_eq: "buf = buf5" using qq_eq qq_state by simp
have dest_eq: "dest = dest5" using qq_eq qq_state by simp
have nn_kk: "nn kk = mt_pos c5 kk" using c5_eq6 by simp
have nn_kk_val: "nn kk = mt_pos c' kk - 1" using nn_kk c5_pos_kk by simp
have c5_at_pm1_eq_c4:
"mt_tape c5 kk (mt_pos c' kk - 1) = mt_tape c4 kk (mt_pos c' kk - 1)"
using mttm_step_tape_off_head[OF step5 pm1_ne_c4] .
have read_ne_LE: "tts kk (nn kk) ≠ LE_block (le_tm M)"
proof -
have "tts kk (nn kk) = mt_tape c5 kk (mt_pos c5 kk)"
using c5_eq6 nn_kk by simp
also have "… = mt_tape c5 kk (mt_pos c' kk - 1)" using c5_pos_kk by simp
also have "… = mt_tape c4 kk (mt_pos c' kk - 1)" using c5_at_pm1_eq_c4 .
finally have "tts kk (nn kk) = mt_tape c4 kk (mt_pos c' kk - 1)" .
thus ?thesis using c4_at_pm1_ne_LE by simp
qed
have aa6_kk: "aa6 kk = ll"
using aa6_eq buf_eq dest_eq AE_Right buf5_kk h_ne_LE read_ne_LE kklt by simp
have c6_at_pm1: "mt_tape c6 kk (mt_pos c' kk - 1) = ll"
proof -
have "mt_tape c6 kk (mt_pos c' kk - 1) = aa6 kk"
using c6_eq nn_kk_val by simp
thus ?thesis using aa6_kk by simp
qed
have c6_pos_kk: "mt_pos c6 kk = mt_pos c' kk"
using c6_pos_for_pos_ge2[OF kklt hge2] .
have pm1_ne_c6: "(mt_pos c' kk - 1) ≠ mt_pos c6 kk"
using c6_pos_kk hge2 by linarith
have c7_pos_kk: "mt_pos c7 kk = mt_pos c' kk + 1"
using c7_pos_for_pos_ge2[OF kklt hge2] AE_Right by simp
have pm1_ne_c7: "(mt_pos c' kk - 1) ≠ mt_pos c7 kk"
using c7_pos_kk by linarith
have "mt_tape c8 kk (mt_pos c' kk - 1) = mt_tape c7 kk (mt_pos c' kk - 1)"
using mttm_step_tape_off_head[OF step8 pm1_ne_c7] .
also have "… = mt_tape c6 kk (mt_pos c' kk - 1)"
using mttm_step_tape_off_head[OF step7 pm1_ne_c6] .
also have "… = ll" using c6_at_pm1 .
also have "… = fst (buf5 kk)" using buf5_kk by simp
finally show ?thesis .
qed
qed
text ‹Reconstruction leaf of ‹ae_simulates_forward_stage_general›: the
per-tape regime-aware ‹ae_tape_correspondence› between the
simulated M-config ‹cM_k› and the post-chain M'-config
‹c8›. Per tape it branches on ‹mt_pos c' kk›
(steady / le1 / le0) and within each regime on the block
‹s›: an in-window cell matches via the buf-lin transfer
coinciding with the ‹c8› in-window value on the ‹buf5›
slot, an off-window cell via ‹cM_k = cM = c'› (M-side) and
‹c8 = c'› (M'-side). ›
lemma ae_fwd_tape_corr_c8:
fixes M :: "('q, 'a) mttm"
and cM cM_k :: "('a, 'q) mt_config"
and c' c4 c5 c6 c7 c8 :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
and buf5 :: "nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)"
and dest5 :: "nat ⇒ ae_dest"
assumes tape_corr: "∀k<k_tm M. ae_tape_correspondence (le_tm M)
(mt_tape cM k) (mt_tape c' k)"
and c_ge_1: "1 ≤ card (UNIV :: 'c set)"
and c4_pos: "⋀kk. kk < k_tm M ⟹ mt_pos c4 kk = mt_pos c' kk"
and c5_pos_for_pos1:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 1 ⟹ dest5 kk ≠ AE_Left
⟹ mt_pos c5 kk = 0"
and c5_pos_for_pos1_dest_left:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 1 ⟹ dest5 kk = AE_Left
⟹ mt_pos c5 kk = 2"
and c7_pos_for_pos1_dest_left:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 1 ⟹ dest5 kk = AE_Left
⟹ mt_pos c7 kk = 0"
and cM_k_zero: "⋀kk. kk < k_tm M ⟹ mt_tape cM_k kk 0 = le_tm M"
and m_tape_off_window_le0:
"⋀kk p. kk < k_tm M ⟹ mt_pos c' kk = 0
⟹ p > card (UNIV :: 'c set)
⟹ mt_tape cM_k kk p = mt_tape cM kk p"
and m_tape_off_window_le1:
"⋀kk p. kk < k_tm M ⟹ mt_pos c' kk = 1
⟹ p > 2 * card (UNIV :: 'c set)
⟹ mt_tape cM_k kk p = mt_tape cM kk p"
and m_tape_off_window_steady:
"⋀kk p. kk < k_tm M ⟹ mt_pos c' kk ≥ 2
⟹ p < (mt_pos c' kk - 2) * card (UNIV :: 'c set) + 1
∨ p ≥ (mt_pos c' kk - 2) * card (UNIV :: 'c set) + 1 + 3 * card (UNIV :: 'c set)
⟹ mt_tape cM_k kk p = mt_tape cM kk p"
and c5_pos_for_pos0:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 0 ⟹ mt_pos c5 kk = 0"
and c5_pos_for_pos_ge2:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2 ⟹ dest5 kk ≠ AE_Left
⟹ mt_pos c5 kk = mt_pos c' kk - 1"
and c5_pos_for_pos_ge2_dest_left:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2 ⟹ dest5 kk = AE_Left
⟹ mt_pos c5 kk = mt_pos c' kk + 1"
and c6_pos_for_pos0:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 0 ⟹ mt_pos c6 kk = 1"
and c6_pos_for_pos_ge2:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2 ⟹ mt_pos c6 kk = mt_pos c' kk"
and c7_pos_for_pos0:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 0
⟹ mt_pos c7 kk = (if dest5 kk = AE_Right then 1 else 0)"
and c7_pos_for_pos_ge2:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2
⟹ mt_pos c7 kk = (if dest5 kk = AE_Left
then mt_pos c' kk - 1
else mt_pos c' kk + 1)"
and c6_pos_for_pos1:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 1 ⟹ mt_pos c6 kk = 1"
and c7_pos_for_pos1:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 1
⟹ mt_pos c7 kk = (if dest5 kk = AE_Left then 0 else 2)"
and c8_tape_off_window:
"⋀kk s. s ≠ mt_pos c4 kk ⟹ s ≠ mt_pos c5 kk
⟹ s ≠ mt_pos c6 kk ⟹ s ≠ mt_pos c7 kk
⟹ mt_tape c8 kk s = mt_tape c' kk s"
and c8_tape_at_one_for_pos0:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 0
⟹ mt_tape c8 kk 1 = snd (snd (buf5 kk))"
and c8_tape_at_one_for_pos1:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 1
⟹ mt_tape c8 kk 1 = fst (snd (buf5 kk))"
and c8_tape_at_two_for_pos1:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 1
⟹ mt_tape c8 kk 2 = snd (snd (buf5 kk))"
and c8_tape_at_pos_for_pos_ge2:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2
⟹ mt_tape c8 kk (mt_pos c' kk) = fst (snd (buf5 kk))"
and c8_tape_at_pos_minus_1_for_pos_ge2:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2
⟹ mt_tape c8 kk (mt_pos c' kk - 1) = fst (buf5 kk)"
and c8_tape_at_pos_plus_1_for_pos_ge2:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2
⟹ mt_tape c8 kk (mt_pos c' kk + 1) = snd (snd (buf5 kk))"
and tape_cM_k_at_one_for_pos0:
"⋀kk i. kk < k_tm M ⟹ mt_pos c' kk = 0
⟹ mt_tape cM_k kk (Suc (c_idx (i :: 'c)))
= (snd (snd (buf5 kk))) i"
and tape_cM_k_at_one_for_pos1:
"⋀kk i. kk < k_tm M ⟹ mt_pos c' kk = 1
⟹ mt_tape cM_k kk (Suc (c_idx (i :: 'c)))
= (fst (snd (buf5 kk))) i"
and tape_cM_k_at_two_for_pos1:
"⋀kk i. kk < k_tm M ⟹ mt_pos c' kk = 1
⟹ mt_tape cM_k kk (Suc (card (UNIV :: 'c set) + c_idx (i :: 'c)))
= (snd (snd (buf5 kk))) i"
and tape_cM_k_at_pos_minus_1_for_pos_ge2:
"⋀kk i. kk < k_tm M ⟹ mt_pos c' kk ≥ 2
⟹ mt_tape cM_k kk ((mt_pos c' kk - 2) * card (UNIV :: 'c set)
+ c_idx (i :: 'c) + 1)
= (fst (buf5 kk)) i"
and tape_cM_k_at_pos_for_pos_ge2:
"⋀kk i. kk < k_tm M ⟹ mt_pos c' kk ≥ 2
⟹ mt_tape cM_k kk ((mt_pos c' kk - 1) * card (UNIV :: 'c set)
+ c_idx (i :: 'c) + 1)
= (fst (snd (buf5 kk))) i"
and tape_cM_k_at_pos_plus_1_for_pos_ge2:
"⋀kk i. kk < k_tm M ⟹ mt_pos c' kk ≥ 2
⟹ mt_tape cM_k kk (mt_pos c' kk * card (UNIV :: 'c set)
+ c_idx (i :: 'c) + 1)
= (snd (snd (buf5 kk))) i"
shows "∀kk<k_tm M. ae_tape_correspondence (le_tm M)
(mt_tape cM_k kk) (mt_tape c8 kk)"
proof -
let ?c = "card (UNIV :: 'c set)"
show ?thesis
proof (intro allI impI)
fix kk
assume kklt: "kk < k_tm M"
show "ae_tape_correspondence (le_tm M)
(mt_tape cM_k kk) (mt_tape c8 kk)"
unfolding ae_tape_correspondence_def
proof (intro conjI allI impI)
show "mt_tape cM_k kk 0 = le_tm M" using cM_k_zero[OF kklt] by simp
next
fix s :: nat and i :: 'c
assume s_ge_1: "s ≥ 1"
let ?p = "(s - 1) * ?c + c_idx i + 1"
have c_idx_lt: "c_idx i < ?c" by (rule c_idx_lt_card)
have c4_kk_eq: "mt_pos c4 kk = mt_pos c' kk" using c4_pos kklt by simp
consider (le0) "mt_pos c' kk = 0"
| (le1) "mt_pos c' kk = 1"
| (steady) "mt_pos c' kk ≥ 2"
by linarith
thus "mt_tape cM_k kk ?p = mt_tape c8 kk s i"
proof cases
case le0
show ?thesis
proof (cases "s = 1")
case True
have p_eq: "?p = Suc (c_idx i)" using True by simp
have lhs: "mt_tape cM_k kk ?p = (snd (snd (buf5 kk))) i"
using p_eq tape_cM_k_at_one_for_pos0[OF kklt le0] by simp
have c8_at_s: "mt_tape c8 kk s = mt_tape c8 kk 1" using True by simp
have c8_at_1: "mt_tape c8 kk 1 = snd (snd (buf5 kk))"
using c8_tape_at_one_for_pos0[OF kklt le0] .
show ?thesis using lhs c8_at_s c8_at_1 by simp
next
case False
have s_ge_2: "s ≥ 2" using s_ge_1 False by linarith
have p_gt_c: "?p > ?c"
proof -
have s_sub_ge: "s - 1 ≥ 1" using s_ge_2 by linarith
have mult_ge: "(s - 1) * ?c ≥ ?c"
using s_sub_ge c_ge_1
by (metis mult.commute mult_le_mono2 mult_numeral_1_right
mult_le_cancel2 nat_mult_1_right)
show ?thesis using mult_ge by linarith
qed
have cM_k_at_p: "mt_tape cM_k kk ?p = mt_tape cM kk ?p"
using m_tape_off_window_le0[OF kklt le0 p_gt_c] .
have tc_at: "mt_tape cM kk ?p = mt_tape c' kk s i"
using tape_corr[rule_format, OF kklt] s_ge_1
unfolding ae_tape_correspondence_def by simp
have s_ne_c4: "s ≠ mt_pos c4 kk"
using c4_kk_eq le0 s_ge_2 by linarith
have s_ne_c5: "s ≠ mt_pos c5 kk"
using c5_pos_for_pos0[OF kklt le0] s_ge_2 by simp
have s_ne_c6: "s ≠ mt_pos c6 kk"
using c6_pos_for_pos0[OF kklt le0] s_ge_2 by simp
have s_ne_c7: "s ≠ mt_pos c7 kk"
proof (cases "dest5 kk = AE_Right")
case True
have "mt_pos c7 kk = 1"
using c7_pos_for_pos0[OF kklt le0] True by simp
thus ?thesis using s_ge_2 by simp
next
case False
have "mt_pos c7 kk = 0"
using c7_pos_for_pos0[OF kklt le0] False by simp
thus ?thesis using s_ge_2 by simp
qed
have c8_at_s: "mt_tape c8 kk s = mt_tape c' kk s"
using c8_tape_off_window[OF s_ne_c4 s_ne_c5 s_ne_c6 s_ne_c7] .
show ?thesis using cM_k_at_p tc_at c8_at_s by simp
qed
next
case le1
show ?thesis
proof (cases "s = 1")
case True
have p_eq: "?p = Suc (c_idx i)" using True by simp
have lhs: "mt_tape cM_k kk ?p = (fst (snd (buf5 kk))) i"
using p_eq tape_cM_k_at_one_for_pos1[OF kklt le1] by simp
have c8_at_s: "mt_tape c8 kk s = mt_tape c8 kk 1" using True by simp
have c8_at_1: "mt_tape c8 kk 1 = fst (snd (buf5 kk))"
using c8_tape_at_one_for_pos1[OF kklt le1] .
show ?thesis using lhs c8_at_s c8_at_1 by simp
next
case False
have s_ge_2: "s ≥ 2" using s_ge_1 False by linarith
show ?thesis
proof (cases "s = 2")
case True
have p_eq: "?p = Suc (?c + c_idx i)" using True by simp
have lhs: "mt_tape cM_k kk ?p = (snd (snd (buf5 kk))) i"
using p_eq tape_cM_k_at_two_for_pos1[OF kklt le1] by simp
have c8_at_s: "mt_tape c8 kk s = mt_tape c8 kk 2" using True by simp
have c8_at_2: "mt_tape c8 kk 2 = snd (snd (buf5 kk))"
using c8_tape_at_two_for_pos1[OF kklt le1] .
show ?thesis using lhs c8_at_s c8_at_2 by simp
next
case False
have s_ge_3: "s ≥ 3" using s_ge_2 False by linarith
have p_gt_2c: "?p > 2 * ?c"
proof -
have s_sub_ge: "s - 1 ≥ 2" using s_ge_3 by linarith
have mult_ge: "(s - 1) * ?c ≥ 2 * ?c"
using s_sub_ge c_ge_1
by (metis mult.commute mult_le_mono2)
show ?thesis using mult_ge by linarith
qed
have cM_k_at_p: "mt_tape cM_k kk ?p = mt_tape cM kk ?p"
using m_tape_off_window_le1[OF kklt le1 p_gt_2c] .
have tc_at: "mt_tape cM kk ?p = mt_tape c' kk s i"
using tape_corr[rule_format, OF kklt] s_ge_1
unfolding ae_tape_correspondence_def by simp
have s_ne_c4: "s ≠ mt_pos c4 kk"
using c4_kk_eq le1 s_ge_3 by linarith
have s_ne_c5: "s ≠ mt_pos c5 kk"
proof (cases "dest5 kk = AE_Left")
case True
have "mt_pos c5 kk = 2"
using c5_pos_for_pos1_dest_left[OF kklt le1 True] .
thus ?thesis using s_ge_3 by simp
next
case False
have "mt_pos c5 kk = 0"
using c5_pos_for_pos1[OF kklt le1 False] .
thus ?thesis using s_ge_3 by simp
qed
have s_ne_c6: "s ≠ mt_pos c6 kk"
using c6_pos_for_pos1[OF kklt le1] s_ge_3 by simp
have s_ne_c7: "s ≠ mt_pos c7 kk"
proof (cases "dest5 kk = AE_Left")
case True
have "mt_pos c7 kk = 0"
using c7_pos_for_pos1_dest_left[OF kklt le1 True] .
thus ?thesis using s_ge_3 by simp
next
case False
have "mt_pos c7 kk = 2"
using c7_pos_for_pos1[OF kklt le1] False by simp
thus ?thesis using s_ge_3 by simp
qed
have c8_at_s: "mt_tape c8 kk s = mt_tape c' kk s"
using c8_tape_off_window[OF s_ne_c4 s_ne_c5 s_ne_c6 s_ne_c7] .
show ?thesis using cM_k_at_p tc_at c8_at_s by simp
qed
qed
next
case steady
show ?thesis
proof (cases "s = mt_pos c' kk - 1")
case True
have p_eq: "?p = (mt_pos c' kk - 2) * ?c + c_idx i + 1"
proof -
have "s - 1 = mt_pos c' kk - 2"
using True steady by linarith
thus ?thesis by simp
qed
have lhs: "mt_tape cM_k kk ?p = (fst (buf5 kk)) i"
using p_eq tape_cM_k_at_pos_minus_1_for_pos_ge2[OF kklt steady] by simp
have c8_at_s: "mt_tape c8 kk s = mt_tape c8 kk (mt_pos c' kk - 1)"
using True by simp
have c8_at_addr: "mt_tape c8 kk (mt_pos c' kk - 1) = fst (buf5 kk)"
using c8_tape_at_pos_minus_1_for_pos_ge2[OF kklt steady] .
show ?thesis using lhs c8_at_s c8_at_addr by simp
next
case ne_pm1: False
show ?thesis
proof (cases "s = mt_pos c' kk")
case True
have p_eq: "?p = (mt_pos c' kk - 1) * ?c + c_idx i + 1"
using True steady by simp
have lhs: "mt_tape cM_k kk ?p = (fst (snd (buf5 kk))) i"
using p_eq tape_cM_k_at_pos_for_pos_ge2[OF kklt steady] by simp
have c8_at_s: "mt_tape c8 kk s = mt_tape c8 kk (mt_pos c' kk)"
using True by simp
have c8_at_addr: "mt_tape c8 kk (mt_pos c' kk) = fst (snd (buf5 kk))"
using c8_tape_at_pos_for_pos_ge2[OF kklt steady] .
show ?thesis using lhs c8_at_s c8_at_addr by simp
next
case ne_pos: False
show ?thesis
proof (cases "s = mt_pos c' kk + 1")
case True
have p_eq: "?p = mt_pos c' kk * ?c + c_idx i + 1"
using True by simp
have lhs: "mt_tape cM_k kk ?p = (snd (snd (buf5 kk))) i"
using p_eq tape_cM_k_at_pos_plus_1_for_pos_ge2[OF kklt steady]
by simp
have c8_at_s: "mt_tape c8 kk s = mt_tape c8 kk (mt_pos c' kk + 1)"
using True by simp
have c8_at_addr:
"mt_tape c8 kk (mt_pos c' kk + 1) = snd (snd (buf5 kk))"
using c8_tape_at_pos_plus_1_for_pos_ge2[OF kklt steady] .
show ?thesis using lhs c8_at_s c8_at_addr by simp
next
case ne_pp1: False
have s_outside: "s + 1 < mt_pos c' kk ∨ s > mt_pos c' kk + 1"
using ne_pm1 ne_pos ne_pp1 steady by linarith
have p_outside:
"?p < (mt_pos c' kk - 2) * ?c + 1
∨ ?p ≥ (mt_pos c' kk - 2) * ?c + 1 + 3 * ?c"
proof -
from s_outside show ?thesis
proof
assume s_lt: "s + 1 < mt_pos c' kk"
have pos_ge3: "mt_pos c' kk ≥ 3" using s_lt s_ge_1 by linarith
have s_sub_le: "s - 1 ≤ mt_pos c' kk - 3"
using s_lt s_ge_1 by linarith
have "(s - 1) * ?c ≤ (mt_pos c' kk - 3) * ?c"
using s_sub_le by (simp add: mult_le_mono1)
hence p_le: "?p ≤ (mt_pos c' kk - 3) * ?c + c_idx i + 1"
by linarith
have c_split: "(mt_pos c' kk - 2) * ?c
= (mt_pos c' kk - 3) * ?c + ?c"
using pos_ge3 by (simp add: algebra_simps diff_mult_distrib)
have "?p < (mt_pos c' kk - 2) * ?c + 1"
using p_le c_split c_idx_lt by linarith
thus ?thesis ..
next
assume s_gt: "s > mt_pos c' kk + 1"
have s_sub_ge: "s - 1 ≥ mt_pos c' kk + 1"
using s_gt by linarith
have "(s - 1) * ?c ≥ (mt_pos c' kk + 1) * ?c"
using s_sub_ge by (rule mult_le_mono1)
hence p_ge: "?p ≥ (mt_pos c' kk + 1) * ?c + 1"
by linarith
have c_split: "(mt_pos c' kk + 1) * ?c
= (mt_pos c' kk - 2) * ?c + 3 * ?c"
using steady by (simp add: algebra_simps diff_mult_distrib)
have "?p ≥ (mt_pos c' kk - 2) * ?c + 1 + 3 * ?c"
using p_ge c_split by linarith
thus ?thesis ..
qed
qed
have cM_k_at_p: "mt_tape cM_k kk ?p = mt_tape cM kk ?p"
using m_tape_off_window_steady[OF kklt steady p_outside] .
have tc_at: "mt_tape cM kk ?p = mt_tape c' kk s i"
using tape_corr[rule_format, OF kklt] s_ge_1
unfolding ae_tape_correspondence_def by simp
have s_ne_c4: "s ≠ mt_pos c4 kk"
using c4_kk_eq ne_pos by simp
have s_ne_c5: "s ≠ mt_pos c5 kk"
proof (cases "dest5 kk = AE_Left")
case True
have "mt_pos c5 kk = mt_pos c' kk + 1"
using c5_pos_for_pos_ge2_dest_left[OF kklt steady True] .
thus ?thesis using ne_pp1 by simp
next
case False
have "mt_pos c5 kk = mt_pos c' kk - 1"
using c5_pos_for_pos_ge2[OF kklt steady False] .
thus ?thesis using ne_pm1 by simp
qed
have s_ne_c6: "s ≠ mt_pos c6 kk"
using c6_pos_for_pos_ge2[OF kklt steady] ne_pos by simp
have s_ne_c7: "s ≠ mt_pos c7 kk"
proof (cases "dest5 kk = AE_Left")
case True
have "mt_pos c7 kk = mt_pos c' kk - 1"
using c7_pos_for_pos_ge2[OF kklt steady] True by simp
thus ?thesis using ne_pm1 by simp
next
case False
have "mt_pos c7 kk = mt_pos c' kk + 1"
using c7_pos_for_pos_ge2[OF kklt steady] False by simp
thus ?thesis using ne_pp1 by simp
qed
have c8_at_s: "mt_tape c8 kk s = mt_tape c' kk s"
using c8_tape_off_window[OF s_ne_c4 s_ne_c5 s_ne_c6 s_ne_c7] .
show ?thesis using cM_k_at_p tc_at c8_at_s by simp
qed
qed
qed
qed
qed
qed
qed
text ‹Reconstruction leaf of ‹ae_simulates_forward_stage_general›:
the in-window ‹c8› value at block 2 for an le1 tape
(‹mt_pos c' kk = 1›). Uniformly ‹c8@2 = rr› (the right
buffer slot). Three-way ‹dest5› case-split: for ‹AE_Left›
SS6 writes ‹r› at ‹c5_pos = 2›; for ‹AE_Home›/‹AE_Right›
SS8 writes ‹r› at ‹c7_pos = 2›; the other substeps are off
cell 2. ›
lemma ae_fwd_c8_at_two_for_pos1:
fixes M :: "('q, 'a) mttm"
and c' c4 c5 c6 c7 c8 :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
and q5 q6 :: 'q
and ofs5 ofs6 :: "nat ⇒ 'c"
and buf5 buf6 :: "nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)"
and dest5 dest6 :: "nat ⇒ ae_dest"
assumes step5: "(c4, c5) ∈ mttm_step (alphabet_enlarge_delta M)"
and c5_state: "mt_state c5 = (q5, ofs5, buf5, dest5, SS6)"
and tape_c4_eq_c': "mt_tape c4 = mt_tape c'"
and buf5_not_le_per_tape:
"∀k<k_tm M. (mt_pos c' k = 0
⟶ fst (buf5 k) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))
∧ (mt_pos c' k = 1
⟶ fst (snd (buf5 k)) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))
∧ (mt_pos c' k ≥ 2
⟶ fst (buf5 k) ≠ LE_block (le_tm M)
∧ fst (snd (buf5 k)) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))"
and right_not_le_c':
"∀k. mt_tape c' k (mt_pos c' k + 1) ≠ LE_block (le_tm M)"
and c4_pos: "⋀kk. kk < k_tm M ⟹ mt_pos c4 kk = mt_pos c' kk"
and c5_pos_for_pos1:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 1 ⟹ dest5 kk ≠ AE_Left
⟹ mt_pos c5 kk = 0"
and step6_sub: "(c5, c6) ∈ mttm_step (ae_delta_ss6_ss7 M)"
and step6: "(c5, c6) ∈ mttm_step (alphabet_enlarge_delta M)"
and step7: "(c6, c7) ∈ mttm_step (alphabet_enlarge_delta M)"
and c7_state: "mt_state c7 = (q6, ofs6, buf6, dest6, SS8)"
and buf6_eq_buf5: "buf6 = buf5"
and dest6_eq_dest5: "dest6 = dest5"
and c5_pos_for_pos1_dest_left:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 1 ⟹ dest5 kk = AE_Left
⟹ mt_pos c5 kk = 2"
and c7_pos_for_pos1_dest_left:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 1 ⟹ dest5 kk = AE_Left
⟹ mt_pos c7 kk = 0"
and step8_sub: "(c7, c8) ∈ mttm_step (ae_delta_ss8_ss1 M)"
and step8: "(c7, c8) ∈ mttm_step (alphabet_enlarge_delta M)"
and c6_pos_for_pos1:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 1 ⟹ mt_pos c6 kk = 1"
and c7_pos_for_pos1:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 1
⟹ mt_pos c7 kk = (if dest5 kk = AE_Left then 0 else 2)"
shows "⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 1
⟹ mt_tape c8 kk 2 = snd (snd (buf5 kk))"
proof -
fix kk
assume kklt: "kk < k_tm M"
assume pos_kk: "mt_pos c' kk = 1"
obtain ll hh rr where buf5_kk: "buf5 kk = (ll, hh, rr)"
using prod.exhaust by metis
have buf6_kk: "buf6 kk = (ll, hh, rr)"
using buf5_kk buf6_eq_buf5 by simp
have h_ne_LE: "hh ≠ LE_block (le_tm M)"
proof -
have "fst (snd (buf5 kk)) ≠ LE_block (le_tm M)"
using buf5_not_le_per_tape[rule_format, OF kklt] pos_kk by blast
thus ?thesis using buf5_kk by simp
qed
have two_ne_c4: "(2 :: nat) ≠ mt_pos c4 kk"
using c4_pos kklt pos_kk by simp
have c4_at_2_ne_LE: "mt_tape c4 kk 2 ≠ LE_block (le_tm M)"
proof -
have "mt_tape c4 kk 2 = mt_tape c' kk 2" using tape_c4_eq_c' by simp
moreover have "mt_tape c' kk (mt_pos c' kk + 1) ≠ LE_block (le_tm M)"
using right_not_le_c' by blast
ultimately have "mt_tape c4 kk 2 = mt_tape c' kk 2
∧ mt_tape c' kk 2 ≠ LE_block (le_tm M)"
using pos_kk by (simp add: numeral_2_eq_2)
thus ?thesis by simp
qed
have c5_at_2: "mt_tape c5 kk 2 = mt_tape c4 kk 2"
using mttm_step_tape_off_head[OF step5 two_ne_c4] .
show "mt_tape c8 kk 2 = snd (snd (buf5 kk))"
proof (cases "dest5 kk")
case AE_Left
have c5_pos_kk: "mt_pos c5 kk = 2"
using c5_pos_for_pos1_dest_left[OF kklt pos_kk AE_Left] .
obtain qq tts nn qq' aa6 dr6 where
c5_eq6: "c5 = Config⇩M qq tts nn"
and c6_eq: "c6 = Config⇩M qq'
(λk. (tts k)(nn k := aa6 k))
(λk. go_dir (dr6 k) (nn k))"
and tr_in: "(qq, λk. tts k (nn k), qq', aa6, dr6)
∈ ae_delta_ss6_ss7 M"
using step6_sub by (auto elim: mttm_step.cases)
obtain q ofs buf dest where
qq_eq: "qq = (q, ofs, buf, dest, SS6)"
and aa6_eq:
"aa6 = (λk. if k < k_tm M then fst (ae_ss6_action (le_tm M)
(tts k (nn k)) (buf k) (dest k)) else bl_block (bl_tm M))"
using tr_in by (auto simp: ae_delta_ss6_ss7_def)
have qq_state: "qq = (q5, ofs5, buf5, dest5, SS6)"
using c5_state c5_eq6 by simp
have buf_eq: "buf = buf5" using qq_eq qq_state by simp
have dest_eq: "dest = dest5" using qq_eq qq_state by simp
have nn_kk: "nn kk = mt_pos c5 kk" using c5_eq6 by simp
have nn_kk_2: "nn kk = 2" using nn_kk c5_pos_kk by simp
have read_ne_LE: "tts kk (nn kk) ≠ LE_block (le_tm M)"
proof -
have "tts kk (nn kk) = mt_tape c5 kk (mt_pos c5 kk)"
using c5_eq6 nn_kk by simp
also have "… = mt_tape c5 kk 2" using c5_pos_kk by simp
also have "… = mt_tape c4 kk 2" using c5_at_2 .
finally have "tts kk (nn kk) = mt_tape c4 kk 2" .
thus ?thesis using c4_at_2_ne_LE by simp
qed
have aa6_kk: "aa6 kk = rr"
using aa6_eq buf_eq dest_eq AE_Left buf5_kk read_ne_LE h_ne_LE kklt by simp
have c6_at_2: "mt_tape c6 kk 2 = rr"
proof -
have "mt_tape c6 kk 2 = aa6 kk" using c6_eq nn_kk_2 by simp
thus ?thesis using aa6_kk by simp
qed
have two_ne_c6_pos: "(2 :: nat) ≠ mt_pos c6 kk"
using c6_pos_for_pos1[OF kklt pos_kk] by simp
have c7_at_2: "mt_tape c7 kk 2 = mt_tape c6 kk 2"
using mttm_step_tape_off_head[OF step7 two_ne_c6_pos] .
have c7_pos_kk: "mt_pos c7 kk = 0"
using c7_pos_for_pos1_dest_left[OF kklt pos_kk AE_Left] .
have two_ne_c7_pos: "(2 :: nat) ≠ mt_pos c7 kk"
using c7_pos_kk by simp
have c8_at_2: "mt_tape c8 kk 2 = mt_tape c7 kk 2"
using mttm_step_tape_off_head[OF step8 two_ne_c7_pos] .
have "mt_tape c8 kk 2 = mt_tape c7 kk 2" using c8_at_2 .
also have "… = mt_tape c6 kk 2" using c7_at_2 .
also have "… = rr" using c6_at_2 .
also have "… = snd (snd (buf5 kk))" using buf5_kk by simp
finally show ?thesis .
next
case AE_Home
have dest_ne_left: "dest5 kk ≠ AE_Left" using AE_Home by simp
have c5_pos_kk: "mt_pos c5 kk = 0"
using c5_pos_for_pos1[OF kklt pos_kk dest_ne_left] .
have two_ne_c5_pos: "(2 :: nat) ≠ mt_pos c5 kk"
using c5_pos_kk by simp
have c6_at_2_eq_c4: "mt_tape c6 kk 2 = mt_tape c4 kk 2"
proof -
have "mt_tape c6 kk 2 = mt_tape c5 kk 2"
using mttm_step_tape_off_head[OF step6 two_ne_c5_pos] .
also have "… = mt_tape c4 kk 2" using c5_at_2 .
finally show ?thesis .
qed
have two_ne_c6_pos: "(2 :: nat) ≠ mt_pos c6 kk"
using c6_pos_for_pos1[OF kklt pos_kk] by simp
have c7_at_2_eq_c4: "mt_tape c7 kk 2 = mt_tape c4 kk 2"
proof -
have "mt_tape c7 kk 2 = mt_tape c6 kk 2"
using mttm_step_tape_off_head[OF step7 two_ne_c6_pos] .
also have "… = mt_tape c4 kk 2" using c6_at_2_eq_c4 .
finally show ?thesis .
qed
have c7_pos_kk: "mt_pos c7 kk = 2"
using c7_pos_for_pos1[OF kklt pos_kk] AE_Home by simp
obtain qq tts nn qq' aa8 dr8 where
c7_eq8: "c7 = Config⇩M qq tts nn"
and c8_eq: "c8 = Config⇩M qq'
(λk. (tts k)(nn k := aa8 k))
(λk. go_dir (dr8 k) (nn k))"
and tr_in: "(qq, λk. tts k (nn k), qq', aa8, dr8)
∈ ae_delta_ss8_ss1 M"
using step8_sub by (auto elim: mttm_step.cases)
obtain q ofs buf dest where
qq_eq: "qq = (q, ofs, buf, dest, SS8)"
and aa8_eq:
"aa8 = (λk. if k < k_tm M then fst (ae_ss8_action (le_tm M)
(tts k (nn k)) (buf k) (dest k)) else bl_block (bl_tm M))"
using tr_in by (auto simp: ae_delta_ss8_ss1_def)
have qq_state: "qq = (q6, ofs6, buf6, dest6, SS8)"
using c7_state c7_eq8 by simp
have buf_eq: "buf = buf6" using qq_eq qq_state by simp
have dest_eq: "dest = dest6" using qq_eq qq_state by simp
have nn_kk: "nn kk = mt_pos c7 kk" using c7_eq8 by simp
have nn_kk_2: "nn kk = 2" using nn_kk c7_pos_kk by simp
have read_ne_LE: "tts kk (nn kk) ≠ LE_block (le_tm M)"
proof -
have "tts kk (nn kk) = mt_tape c7 kk (mt_pos c7 kk)"
using c7_eq8 nn_kk by simp
also have "… = mt_tape c7 kk 2" using c7_pos_kk by simp
also have "… = mt_tape c4 kk 2" using c7_at_2_eq_c4 .
finally have "tts kk (nn kk) = mt_tape c4 kk 2" .
thus ?thesis using c4_at_2_ne_LE by simp
qed
have dest6_AE_Home: "dest6 kk = AE_Home"
using AE_Home dest6_eq_dest5 by simp
have aa8_kk: "aa8 kk = rr"
using aa8_eq buf_eq dest_eq dest6_AE_Home buf6_kk h_ne_LE read_ne_LE kklt
by simp
have "mt_tape c8 kk 2 = aa8 kk" using c8_eq nn_kk_2 by simp
also have "… = rr" using aa8_kk .
also have "… = snd (snd (buf5 kk))" using buf5_kk by simp
finally show ?thesis .
next
case AE_Right
have dest_ne_left: "dest5 kk ≠ AE_Left" using AE_Right by simp
have c5_pos_kk: "mt_pos c5 kk = 0"
using c5_pos_for_pos1[OF kklt pos_kk dest_ne_left] .
have two_ne_c5_pos: "(2 :: nat) ≠ mt_pos c5 kk"
using c5_pos_kk by simp
have c6_at_2_eq_c4: "mt_tape c6 kk 2 = mt_tape c4 kk 2"
proof -
have "mt_tape c6 kk 2 = mt_tape c5 kk 2"
using mttm_step_tape_off_head[OF step6 two_ne_c5_pos] .
also have "… = mt_tape c4 kk 2" using c5_at_2 .
finally show ?thesis .
qed
have two_ne_c6_pos: "(2 :: nat) ≠ mt_pos c6 kk"
using c6_pos_for_pos1[OF kklt pos_kk] by simp
have c7_at_2_eq_c4: "mt_tape c7 kk 2 = mt_tape c4 kk 2"
proof -
have "mt_tape c7 kk 2 = mt_tape c6 kk 2"
using mttm_step_tape_off_head[OF step7 two_ne_c6_pos] .
also have "… = mt_tape c4 kk 2" using c6_at_2_eq_c4 .
finally show ?thesis .
qed
have c7_pos_kk: "mt_pos c7 kk = 2"
using c7_pos_for_pos1[OF kklt pos_kk] AE_Right by simp
obtain qq tts nn qq' aa8 dr8 where
c7_eq8: "c7 = Config⇩M qq tts nn"
and c8_eq: "c8 = Config⇩M qq'
(λk. (tts k)(nn k := aa8 k))
(λk. go_dir (dr8 k) (nn k))"
and tr_in: "(qq, λk. tts k (nn k), qq', aa8, dr8)
∈ ae_delta_ss8_ss1 M"
using step8_sub by (auto elim: mttm_step.cases)
obtain q ofs buf dest where
qq_eq: "qq = (q, ofs, buf, dest, SS8)"
and aa8_eq:
"aa8 = (λk. if k < k_tm M then fst (ae_ss8_action (le_tm M)
(tts k (nn k)) (buf k) (dest k)) else bl_block (bl_tm M))"
using tr_in by (auto simp: ae_delta_ss8_ss1_def)
have qq_state: "qq = (q6, ofs6, buf6, dest6, SS8)"
using c7_state c7_eq8 by simp
have buf_eq: "buf = buf6" using qq_eq qq_state by simp
have dest_eq: "dest = dest6" using qq_eq qq_state by simp
have nn_kk: "nn kk = mt_pos c7 kk" using c7_eq8 by simp
have nn_kk_2: "nn kk = 2" using nn_kk c7_pos_kk by simp
have read_ne_LE: "tts kk (nn kk) ≠ LE_block (le_tm M)"
proof -
have "tts kk (nn kk) = mt_tape c7 kk (mt_pos c7 kk)"
using c7_eq8 nn_kk by simp
also have "… = mt_tape c7 kk 2" using c7_pos_kk by simp
also have "… = mt_tape c4 kk 2" using c7_at_2_eq_c4 .
finally have "tts kk (nn kk) = mt_tape c4 kk 2" .
thus ?thesis using c4_at_2_ne_LE by simp
qed
have dest6_AE_Right: "dest6 kk = AE_Right"
using AE_Right dest6_eq_dest5 by simp
have aa8_kk: "aa8 kk = rr"
using aa8_eq buf_eq dest_eq dest6_AE_Right buf6_kk h_ne_LE read_ne_LE kklt
by simp
have "mt_tape c8 kk 2 = aa8 kk" using c8_eq nn_kk_2 by simp
also have "… = rr" using aa8_kk .
also have "… = snd (snd (buf5 kk))" using buf5_kk by simp
finally show ?thesis .
qed
qed
text ‹Reconstruction leaf of ‹ae_simulates_forward_stage_general›:
the in-window ‹c8› value at block ‹pos + 1› for a
steady tape (‹mt_pos c' kk ≥ 2›). Uniformly
‹c8@(pos+1) = rr› (the right buffer slot). Three-way
‹dest5› case-split: for ‹AE_Left› SS6 writes ‹r› at
‹c5_pos = pos + 1›; for ‹AE_Home›/‹AE_Right› SS8 writes
‹r› at ‹c7_pos = pos + 1›; the other substeps are off
cell ‹pos + 1›. ›
lemma ae_fwd_c8_at_pos_plus_1_ge2:
fixes M :: "('q, 'a) mttm"
and c' c4 c5 c6 c7 c8 :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
and q5 q6 :: 'q
and ofs5 ofs6 :: "nat ⇒ 'c"
and buf5 buf6 :: "nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)"
and dest5 dest6 :: "nat ⇒ ae_dest"
assumes step5: "(c4, c5) ∈ mttm_step (alphabet_enlarge_delta M)"
and c5_state: "mt_state c5 = (q5, ofs5, buf5, dest5, SS6)"
and tape_c4_eq_c': "mt_tape c4 = mt_tape c'"
and buf5_not_le_per_tape:
"∀k<k_tm M. (mt_pos c' k = 0
⟶ fst (buf5 k) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))
∧ (mt_pos c' k = 1
⟶ fst (snd (buf5 k)) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))
∧ (mt_pos c' k ≥ 2
⟶ fst (buf5 k) ≠ LE_block (le_tm M)
∧ fst (snd (buf5 k)) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))"
and right_not_le_c':
"∀k. mt_tape c' k (mt_pos c' k + 1) ≠ LE_block (le_tm M)"
and c4_pos: "⋀kk. kk < k_tm M ⟹ mt_pos c4 kk = mt_pos c' kk"
and step6_sub: "(c5, c6) ∈ mttm_step (ae_delta_ss6_ss7 M)"
and step6: "(c5, c6) ∈ mttm_step (alphabet_enlarge_delta M)"
and step7: "(c6, c7) ∈ mttm_step (alphabet_enlarge_delta M)"
and c7_state: "mt_state c7 = (q6, ofs6, buf6, dest6, SS8)"
and buf6_eq_buf5: "buf6 = buf5"
and dest6_eq_dest5: "dest6 = dest5"
and step8_sub: "(c7, c8) ∈ mttm_step (ae_delta_ss8_ss1 M)"
and step8: "(c7, c8) ∈ mttm_step (alphabet_enlarge_delta M)"
and c5_pos_for_pos_ge2:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2 ⟹ dest5 kk ≠ AE_Left
⟹ mt_pos c5 kk = mt_pos c' kk - 1"
and c5_pos_for_pos_ge2_dest_left:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2 ⟹ dest5 kk = AE_Left
⟹ mt_pos c5 kk = mt_pos c' kk + 1"
and c6_pos_for_pos_ge2:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2 ⟹ mt_pos c6 kk = mt_pos c' kk"
and c7_pos_for_pos_ge2:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2
⟹ mt_pos c7 kk = (if dest5 kk = AE_Left
then mt_pos c' kk - 1
else mt_pos c' kk + 1)"
shows "⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2
⟹ mt_tape c8 kk (mt_pos c' kk + 1) = snd (snd (buf5 kk))"
proof -
fix kk
assume kklt: "kk < k_tm M"
assume hge2: "mt_pos c' kk ≥ 2"
obtain ll hh rr where buf5_kk: "buf5 kk = (ll, hh, rr)"
using prod.exhaust by metis
have buf6_kk: "buf6 kk = (ll, hh, rr)"
using buf5_kk buf6_eq_buf5 by simp
have h_ne_LE: "hh ≠ LE_block (le_tm M)"
proof -
have "fst (snd (buf5 kk)) ≠ LE_block (le_tm M)"
using buf5_not_le_per_tape[rule_format, OF kklt] hge2 by blast
thus ?thesis using buf5_kk by simp
qed
have c4_kk_eq: "mt_pos c4 kk = mt_pos c' kk" using c4_pos kklt by simp
have pp1_ne_c4: "(mt_pos c' kk + 1) ≠ mt_pos c4 kk"
using c4_kk_eq by linarith
have c4_at_pp1_ne_LE:
"mt_tape c4 kk (mt_pos c' kk + 1) ≠ LE_block (le_tm M)"
proof -
have "mt_tape c4 kk (mt_pos c' kk + 1) = mt_tape c' kk (mt_pos c' kk + 1)"
using tape_c4_eq_c' by simp
moreover have "mt_tape c' kk (mt_pos c' kk + 1) ≠ LE_block (le_tm M)"
using right_not_le_c' by blast
ultimately show ?thesis by simp
qed
have c5_at_pp1_eq_c4:
"mt_tape c5 kk (mt_pos c' kk + 1) = mt_tape c4 kk (mt_pos c' kk + 1)"
using mttm_step_tape_off_head[OF step5 pp1_ne_c4] .
show "mt_tape c8 kk (mt_pos c' kk + 1) = snd (snd (buf5 kk))"
proof (cases "dest5 kk")
case AE_Left
have c5_pos_kk: "mt_pos c5 kk = mt_pos c' kk + 1"
using c5_pos_for_pos_ge2_dest_left[OF kklt hge2 AE_Left] .
obtain qq tts nn qq' aa6 dr6 where
c5_eq6: "c5 = Config⇩M qq tts nn"
and c6_eq: "c6 = Config⇩M qq'
(λk. (tts k)(nn k := aa6 k))
(λk. go_dir (dr6 k) (nn k))"
and tr_in: "(qq, λk. tts k (nn k), qq', aa6, dr6)
∈ ae_delta_ss6_ss7 M"
using step6_sub by (auto elim: mttm_step.cases)
obtain q ofs buf dest where
qq_eq: "qq = (q, ofs, buf, dest, SS6)"
and aa6_eq:
"aa6 = (λk. if k < k_tm M then fst (ae_ss6_action (le_tm M)
(tts k (nn k)) (buf k) (dest k)) else bl_block (bl_tm M))"
using tr_in by (auto simp: ae_delta_ss6_ss7_def)
have qq_state: "qq = (q5, ofs5, buf5, dest5, SS6)"
using c5_state c5_eq6 by simp
have buf_eq: "buf = buf5" using qq_eq qq_state by simp
have dest_eq: "dest = dest5" using qq_eq qq_state by simp
have nn_kk: "nn kk = mt_pos c5 kk" using c5_eq6 by simp
have nn_kk_val: "nn kk = mt_pos c' kk + 1" using nn_kk c5_pos_kk by simp
have read_ne_LE: "tts kk (nn kk) ≠ LE_block (le_tm M)"
proof -
have "tts kk (nn kk) = mt_tape c5 kk (mt_pos c5 kk)"
using c5_eq6 nn_kk by simp
also have "… = mt_tape c5 kk (mt_pos c' kk + 1)" using c5_pos_kk by simp
also have "… = mt_tape c4 kk (mt_pos c' kk + 1)" using c5_at_pp1_eq_c4 .
finally have "tts kk (nn kk) = mt_tape c4 kk (mt_pos c' kk + 1)" .
thus ?thesis using c4_at_pp1_ne_LE by simp
qed
have aa6_kk: "aa6 kk = rr"
using aa6_eq buf_eq dest_eq AE_Left buf5_kk read_ne_LE h_ne_LE kklt by simp
have c6_at_pp1: "mt_tape c6 kk (mt_pos c' kk + 1) = rr"
proof -
have "mt_tape c6 kk (mt_pos c' kk + 1) = aa6 kk"
using c6_eq nn_kk_val by simp
thus ?thesis using aa6_kk by simp
qed
have c6_pos_kk: "mt_pos c6 kk = mt_pos c' kk"
using c6_pos_for_pos_ge2[OF kklt hge2] .
have pp1_ne_c6: "(mt_pos c' kk + 1) ≠ mt_pos c6 kk"
using c6_pos_kk by linarith
have c7_pos_kk: "mt_pos c7 kk = mt_pos c' kk - 1"
using c7_pos_for_pos_ge2[OF kklt hge2] AE_Left by simp
have pp1_ne_c7: "(mt_pos c' kk + 1) ≠ mt_pos c7 kk"
using c7_pos_kk hge2 by linarith
have "mt_tape c8 kk (mt_pos c' kk + 1) = mt_tape c7 kk (mt_pos c' kk + 1)"
using mttm_step_tape_off_head[OF step8 pp1_ne_c7] .
also have "… = mt_tape c6 kk (mt_pos c' kk + 1)"
using mttm_step_tape_off_head[OF step7 pp1_ne_c6] .
also have "… = rr" using c6_at_pp1 .
also have "… = snd (snd (buf5 kk))" using buf5_kk by simp
finally show ?thesis .
next
case AE_Home
have dest_ne_left: "dest5 kk ≠ AE_Left" using AE_Home by simp
have c5_pos_kk: "mt_pos c5 kk = mt_pos c' kk - 1"
using c5_pos_for_pos_ge2[OF kklt hge2 dest_ne_left] .
have pp1_ne_c5: "(mt_pos c' kk + 1) ≠ mt_pos c5 kk"
using c5_pos_kk hge2 by linarith
have c6_pos_kk: "mt_pos c6 kk = mt_pos c' kk"
using c6_pos_for_pos_ge2[OF kklt hge2] .
have pp1_ne_c6: "(mt_pos c' kk + 1) ≠ mt_pos c6 kk"
using c6_pos_kk by linarith
have c7_at_pp1_eq_c4:
"mt_tape c7 kk (mt_pos c' kk + 1) = mt_tape c4 kk (mt_pos c' kk + 1)"
proof -
have "mt_tape c7 kk (mt_pos c' kk + 1) = mt_tape c6 kk (mt_pos c' kk + 1)"
using mttm_step_tape_off_head[OF step7 pp1_ne_c6] .
also have "… = mt_tape c5 kk (mt_pos c' kk + 1)"
using mttm_step_tape_off_head[OF step6 pp1_ne_c5] .
also have "… = mt_tape c4 kk (mt_pos c' kk + 1)" using c5_at_pp1_eq_c4 .
finally show ?thesis .
qed
have c7_pos_kk: "mt_pos c7 kk = mt_pos c' kk + 1"
using c7_pos_for_pos_ge2[OF kklt hge2] AE_Home by simp
obtain qq tts nn qq' aa8 dr8 where
c7_eq8: "c7 = Config⇩M qq tts nn"
and c8_eq: "c8 = Config⇩M qq'
(λk. (tts k)(nn k := aa8 k))
(λk. go_dir (dr8 k) (nn k))"
and tr_in: "(qq, λk. tts k (nn k), qq', aa8, dr8)
∈ ae_delta_ss8_ss1 M"
using step8_sub by (auto elim: mttm_step.cases)
obtain q ofs buf dest where
qq_eq: "qq = (q, ofs, buf, dest, SS8)"
and aa8_eq:
"aa8 = (λk. if k < k_tm M then fst (ae_ss8_action (le_tm M)
(tts k (nn k)) (buf k) (dest k)) else bl_block (bl_tm M))"
using tr_in by (auto simp: ae_delta_ss8_ss1_def)
have qq_state: "qq = (q6, ofs6, buf6, dest6, SS8)"
using c7_state c7_eq8 by simp
have buf_eq: "buf = buf6" using qq_eq qq_state by simp
have dest_eq: "dest = dest6" using qq_eq qq_state by simp
have nn_kk: "nn kk = mt_pos c7 kk" using c7_eq8 by simp
have nn_kk_val: "nn kk = mt_pos c' kk + 1" using nn_kk c7_pos_kk by simp
have read_ne_LE: "tts kk (nn kk) ≠ LE_block (le_tm M)"
proof -
have "tts kk (nn kk) = mt_tape c7 kk (mt_pos c7 kk)"
using c7_eq8 nn_kk by simp
also have "… = mt_tape c7 kk (mt_pos c' kk + 1)" using c7_pos_kk by simp
also have "… = mt_tape c4 kk (mt_pos c' kk + 1)" using c7_at_pp1_eq_c4 .
finally have "tts kk (nn kk) = mt_tape c4 kk (mt_pos c' kk + 1)" .
thus ?thesis using c4_at_pp1_ne_LE by simp
qed
have dest6_AE_Home: "dest6 kk = AE_Home"
using AE_Home dest6_eq_dest5 by simp
have aa8_kk: "aa8 kk = rr"
using aa8_eq buf_eq dest_eq dest6_AE_Home buf6_kk h_ne_LE read_ne_LE kklt
by simp
have "mt_tape c8 kk (mt_pos c' kk + 1) = aa8 kk"
using c8_eq nn_kk_val by simp
also have "… = rr" using aa8_kk .
also have "… = snd (snd (buf5 kk))" using buf5_kk by simp
finally show ?thesis .
next
case AE_Right
have dest_ne_left: "dest5 kk ≠ AE_Left" using AE_Right by simp
have c5_pos_kk: "mt_pos c5 kk = mt_pos c' kk - 1"
using c5_pos_for_pos_ge2[OF kklt hge2 dest_ne_left] .
have pp1_ne_c5: "(mt_pos c' kk + 1) ≠ mt_pos c5 kk"
using c5_pos_kk hge2 by linarith
have c6_pos_kk: "mt_pos c6 kk = mt_pos c' kk"
using c6_pos_for_pos_ge2[OF kklt hge2] .
have pp1_ne_c6: "(mt_pos c' kk + 1) ≠ mt_pos c6 kk"
using c6_pos_kk by linarith
have c7_at_pp1_eq_c4:
"mt_tape c7 kk (mt_pos c' kk + 1) = mt_tape c4 kk (mt_pos c' kk + 1)"
proof -
have "mt_tape c7 kk (mt_pos c' kk + 1) = mt_tape c6 kk (mt_pos c' kk + 1)"
using mttm_step_tape_off_head[OF step7 pp1_ne_c6] .
also have "… = mt_tape c5 kk (mt_pos c' kk + 1)"
using mttm_step_tape_off_head[OF step6 pp1_ne_c5] .
also have "… = mt_tape c4 kk (mt_pos c' kk + 1)" using c5_at_pp1_eq_c4 .
finally show ?thesis .
qed
have c7_pos_kk: "mt_pos c7 kk = mt_pos c' kk + 1"
using c7_pos_for_pos_ge2[OF kklt hge2] AE_Right by simp
obtain qq tts nn qq' aa8 dr8 where
c7_eq8: "c7 = Config⇩M qq tts nn"
and c8_eq: "c8 = Config⇩M qq'
(λk. (tts k)(nn k := aa8 k))
(λk. go_dir (dr8 k) (nn k))"
and tr_in: "(qq, λk. tts k (nn k), qq', aa8, dr8)
∈ ae_delta_ss8_ss1 M"
using step8_sub by (auto elim: mttm_step.cases)
obtain q ofs buf dest where
qq_eq: "qq = (q, ofs, buf, dest, SS8)"
and aa8_eq:
"aa8 = (λk. if k < k_tm M then fst (ae_ss8_action (le_tm M)
(tts k (nn k)) (buf k) (dest k)) else bl_block (bl_tm M))"
using tr_in by (auto simp: ae_delta_ss8_ss1_def)
have qq_state: "qq = (q6, ofs6, buf6, dest6, SS8)"
using c7_state c7_eq8 by simp
have buf_eq: "buf = buf6" using qq_eq qq_state by simp
have dest_eq: "dest = dest6" using qq_eq qq_state by simp
have nn_kk: "nn kk = mt_pos c7 kk" using c7_eq8 by simp
have nn_kk_val: "nn kk = mt_pos c' kk + 1" using nn_kk c7_pos_kk by simp
have read_ne_LE: "tts kk (nn kk) ≠ LE_block (le_tm M)"
proof -
have "tts kk (nn kk) = mt_tape c7 kk (mt_pos c7 kk)"
using c7_eq8 nn_kk by simp
also have "… = mt_tape c7 kk (mt_pos c' kk + 1)" using c7_pos_kk by simp
also have "… = mt_tape c4 kk (mt_pos c' kk + 1)" using c7_at_pp1_eq_c4 .
finally have "tts kk (nn kk) = mt_tape c4 kk (mt_pos c' kk + 1)" .
thus ?thesis using c4_at_pp1_ne_LE by simp
qed
have dest6_AE_Right: "dest6 kk = AE_Right"
using AE_Right dest6_eq_dest5 by simp
have aa8_kk: "aa8 kk = rr"
using aa8_eq buf_eq dest_eq dest6_AE_Right buf6_kk h_ne_LE read_ne_LE kklt
by simp
have "mt_tape c8 kk (mt_pos c' kk + 1) = aa8 kk"
using c8_eq nn_kk_val by simp
also have "… = rr" using aa8_kk .
also have "… = snd (snd (buf5 kk))" using buf5_kk by simp
finally show ?thesis .
qed
qed
text ‹Reconstruction leaf of ‹ae_simulates_forward_stage_general›:
the ‹c8› head position for a steady tape
(‹mt_pos c' kk ≥ 2›), as a ‹dest5›-case displacement of
‹mt_pos c' kk› (‹AE_Left› -> ‹pos - 1›, ‹AE_Home› ->
‹pos›, ‹AE_Right› -> ‹pos + 1›). SS8's action reads the
steady-window head cell and steps per the recorded ‹dest›.
›
lemma ae_fwd_c8_pos_for_pos_ge2:
fixes M :: "('q, 'a) mttm"
and c' c4 c5 c6 c7 c8 :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
and q5 q6 :: 'q
and ofs5 ofs6 :: "nat ⇒ 'c"
and buf5 buf6 :: "nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)"
and dest5 dest6 :: "nat ⇒ ae_dest"
assumes step5: "(c4, c5) ∈ mttm_step (alphabet_enlarge_delta M)"
and tape_c4_eq_c': "mt_tape c4 = mt_tape c'"
and buf5_not_le_per_tape:
"∀k<k_tm M. (mt_pos c' k = 0
⟶ fst (buf5 k) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))
∧ (mt_pos c' k = 1
⟶ fst (snd (buf5 k)) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))
∧ (mt_pos c' k ≥ 2
⟶ fst (buf5 k) ≠ LE_block (le_tm M)
∧ fst (snd (buf5 k)) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))"
and right_not_le_c':
"∀k. mt_tape c' k (mt_pos c' k + 1) ≠ LE_block (le_tm M)"
and c4_pos: "⋀kk. kk < k_tm M ⟹ mt_pos c4 kk = mt_pos c' kk"
and step6: "(c5, c6) ∈ mttm_step (alphabet_enlarge_delta M)"
and step7: "(c6, c7) ∈ mttm_step (alphabet_enlarge_delta M)"
and c7_state: "mt_state c7 = (q6, ofs6, buf6, dest6, SS8)"
and buf6_eq_buf5: "buf6 = buf5"
and dest6_eq_dest5: "dest6 = dest5"
and step8_sub: "(c7, c8) ∈ mttm_step (ae_delta_ss8_ss1 M)"
and c5_pos_for_pos_ge2:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2 ⟹ dest5 kk ≠ AE_Left
⟹ mt_pos c5 kk = mt_pos c' kk - 1"
and c5_pos_for_pos_ge2_dest_left:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2 ⟹ dest5 kk = AE_Left
⟹ mt_pos c5 kk = mt_pos c' kk + 1"
and left_not_le_c'_steady:
"∀k. mt_pos c' k ≥ 2
⟶ mt_tape c' k (mt_pos c' k - 1) ≠ LE_block (le_tm M)"
and c6_pos_for_pos_ge2:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2 ⟹ mt_pos c6 kk = mt_pos c' kk"
and c7_pos_for_pos_ge2:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2
⟹ mt_pos c7 kk = (if dest5 kk = AE_Left
then mt_pos c' kk - 1
else mt_pos c' kk + 1)"
shows "⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2
⟹ mt_pos c8 kk = (case dest5 kk of
AE_Left ⇒ mt_pos c' kk - 1
| AE_Home ⇒ mt_pos c' kk
| AE_Right ⇒ mt_pos c' kk + 1)"
proof -
fix kk
assume kklt: "kk < k_tm M"
assume hge2: "mt_pos c' kk ≥ 2"
obtain qq tts nn qq' aa8 dr8 where
c7_eq8: "c7 = Config⇩M qq tts nn"
and c8_eq: "c8 = Config⇩M qq'
(λk. (tts k)(nn k := aa8 k))
(λk. go_dir (dr8 k) (nn k))"
and tr_in: "(qq, λk. tts k (nn k), qq', aa8, dr8)
∈ ae_delta_ss8_ss1 M"
using step8_sub by (auto elim: mttm_step.cases)
obtain q ofs buf dest where
qq_eq: "qq = (q, ofs, buf, dest, SS8)"
and dr8_eq:
"dr8 = (λk. if k < k_tm M then snd (ae_ss8_action (le_tm M)
(tts k (nn k)) (buf k) (dest k)) else dir.N)"
using tr_in by (auto simp: ae_delta_ss8_ss1_def)
have qq_state: "qq = (q6, ofs6, buf6, dest6, SS8)"
using c7_state c7_eq8 by simp
have buf_eq: "buf = buf6" using qq_eq qq_state by simp
have dest_eq: "dest = dest6" using qq_eq qq_state by simp
have nn_kk: "nn kk = mt_pos c7 kk" using c7_eq8 by simp
obtain ll hh rr where buf5_kk: "buf5 kk = (ll, hh, rr)"
using prod.exhaust by metis
have buf6_kk: "buf6 kk = (ll, hh, rr)"
using buf5_kk buf6_eq_buf5 by simp
have h_ne_LE: "hh ≠ LE_block (le_tm M)"
proof -
have "fst (snd (buf5 kk)) ≠ LE_block (le_tm M)"
using buf5_not_le_per_tape[rule_format, OF kklt] hge2 by blast
thus ?thesis using buf5_kk by simp
qed
have c4_kk: "mt_pos c4 kk = mt_pos c' kk" using c4_pos kklt by simp
show "mt_pos c8 kk = (case dest5 kk of
AE_Left ⇒ mt_pos c' kk - 1
| AE_Home ⇒ mt_pos c' kk
| AE_Right ⇒ mt_pos c' kk + 1)"
proof (cases "dest5 kk")
case AE_Left
have c7_kk: "mt_pos c7 kk = mt_pos c' kk - 1"
using c7_pos_for_pos_ge2[OF kklt hge2] AE_Left by simp
have nn_kk_val: "nn kk = mt_pos c' kk - 1" using nn_kk c7_kk by simp
have c5_pos_kk: "mt_pos c5 kk = mt_pos c' kk + 1"
using c5_pos_for_pos_ge2_dest_left[OF kklt hge2 AE_Left] .
have pm1_ne_c6: "(mt_pos c' kk - 1) ≠ mt_pos c6 kk"
using c6_pos_for_pos_ge2[OF kklt hge2] hge2 by linarith
have pm1_ne_c5: "(mt_pos c' kk - 1) ≠ mt_pos c5 kk"
using c5_pos_kk hge2 by linarith
have pm1_ne_c4: "(mt_pos c' kk - 1) ≠ mt_pos c4 kk"
using c4_kk hge2 by linarith
have c7_at_addr:
"mt_tape c7 kk (mt_pos c' kk - 1) = mt_tape c' kk (mt_pos c' kk - 1)"
proof -
have "mt_tape c7 kk (mt_pos c' kk - 1) = mt_tape c6 kk (mt_pos c' kk - 1)"
using mttm_step_tape_off_head[OF step7 pm1_ne_c6] .
also have "… = mt_tape c5 kk (mt_pos c' kk - 1)"
using mttm_step_tape_off_head[OF step6 pm1_ne_c5] .
also have "… = mt_tape c4 kk (mt_pos c' kk - 1)"
using mttm_step_tape_off_head[OF step5 pm1_ne_c4] .
also have "… = mt_tape c' kk (mt_pos c' kk - 1)"
using tape_c4_eq_c' by simp
finally show ?thesis .
qed
have read_ne_LE: "tts kk (nn kk) ≠ LE_block (le_tm M)"
proof -
have "tts kk (nn kk) = mt_tape c7 kk (mt_pos c7 kk)"
using c7_eq8 nn_kk by simp
also have "… = mt_tape c7 kk (mt_pos c' kk - 1)"
using c7_kk by simp
also have "… = mt_tape c' kk (mt_pos c' kk - 1)" using c7_at_addr .
finally have read_eq:
"tts kk (nn kk) = mt_tape c' kk (mt_pos c' kk - 1)" .
have "mt_tape c' kk (mt_pos c' kk - 1) ≠ LE_block (le_tm M)"
using left_not_le_c'_steady hge2 by blast
thus ?thesis using read_eq by simp
qed
have dest6_AE_Left: "dest6 kk = AE_Left"
using AE_Left dest6_eq_dest5 by simp
have dr8_kk: "dr8 kk = dir.N"
using dr8_eq buf_eq dest_eq dest6_AE_Left buf6_kk h_ne_LE read_ne_LE kklt
by simp
have "mt_pos c8 kk = go_dir (dr8 kk) (nn kk)"
using c8_eq by simp
also have "… = nn kk" using dr8_kk by simp
also have "… = mt_pos c' kk - 1" using nn_kk_val .
finally show ?thesis using AE_Left by simp
next
case AE_Home
have c7_kk: "mt_pos c7 kk = mt_pos c' kk + 1"
using c7_pos_for_pos_ge2[OF kklt hge2] AE_Home by simp
have nn_kk_val: "nn kk = mt_pos c' kk + 1" using nn_kk c7_kk by simp
have dest_ne_left: "dest5 kk ≠ AE_Left" using AE_Home by simp
have c5_pos_kk: "mt_pos c5 kk = mt_pos c' kk - 1"
using c5_pos_for_pos_ge2[OF kklt hge2 dest_ne_left] .
have pp1_ne_c6: "(mt_pos c' kk + 1) ≠ mt_pos c6 kk"
using c6_pos_for_pos_ge2[OF kklt hge2] by simp
have pp1_ne_c5: "(mt_pos c' kk + 1) ≠ mt_pos c5 kk"
using c5_pos_kk hge2 by linarith
have pp1_ne_c4: "(mt_pos c' kk + 1) ≠ mt_pos c4 kk"
using c4_kk by simp
have c7_at_addr:
"mt_tape c7 kk (mt_pos c' kk + 1) = mt_tape c' kk (mt_pos c' kk + 1)"
proof -
have "mt_tape c7 kk (mt_pos c' kk + 1) = mt_tape c6 kk (mt_pos c' kk + 1)"
using mttm_step_tape_off_head[OF step7 pp1_ne_c6] .
also have "… = mt_tape c5 kk (mt_pos c' kk + 1)"
using mttm_step_tape_off_head[OF step6 pp1_ne_c5] .
also have "… = mt_tape c4 kk (mt_pos c' kk + 1)"
using mttm_step_tape_off_head[OF step5 pp1_ne_c4] .
also have "… = mt_tape c' kk (mt_pos c' kk + 1)"
using tape_c4_eq_c' by simp
finally show ?thesis .
qed
have read_ne_LE: "tts kk (nn kk) ≠ LE_block (le_tm M)"
proof -
have "tts kk (nn kk) = mt_tape c7 kk (mt_pos c7 kk)"
using c7_eq8 nn_kk by simp
also have "… = mt_tape c7 kk (mt_pos c' kk + 1)"
using c7_kk by simp
also have "… = mt_tape c' kk (mt_pos c' kk + 1)" using c7_at_addr .
finally have read_eq:
"tts kk (nn kk) = mt_tape c' kk (mt_pos c' kk + 1)" .
have "mt_tape c' kk (mt_pos c' kk + 1) ≠ LE_block (le_tm M)"
using right_not_le_c' by blast
thus ?thesis using read_eq by simp
qed
have dest6_AE_Home: "dest6 kk = AE_Home"
using AE_Home dest6_eq_dest5 by simp
have dr8_kk: "dr8 kk = dir.L"
using dr8_eq buf_eq dest_eq dest6_AE_Home buf6_kk h_ne_LE read_ne_LE kklt
by simp
have "mt_pos c8 kk = go_dir (dr8 kk) (nn kk)"
using c8_eq by simp
also have "… = (nn kk) - 1" using dr8_kk by simp
also have "… = (mt_pos c' kk + 1) - 1" using nn_kk_val by simp
also have "… = mt_pos c' kk" by simp
finally show ?thesis using AE_Home by simp
next
case AE_Right
have c7_kk: "mt_pos c7 kk = mt_pos c' kk + 1"
using c7_pos_for_pos_ge2[OF kklt hge2] AE_Right by simp
have nn_kk_val: "nn kk = mt_pos c' kk + 1" using nn_kk c7_kk by simp
have dest_ne_left: "dest5 kk ≠ AE_Left" using AE_Right by simp
have c5_pos_kk: "mt_pos c5 kk = mt_pos c' kk - 1"
using c5_pos_for_pos_ge2[OF kklt hge2 dest_ne_left] .
have pp1_ne_c6: "(mt_pos c' kk + 1) ≠ mt_pos c6 kk"
using c6_pos_for_pos_ge2[OF kklt hge2] by simp
have pp1_ne_c5: "(mt_pos c' kk + 1) ≠ mt_pos c5 kk"
using c5_pos_kk hge2 by linarith
have pp1_ne_c4: "(mt_pos c' kk + 1) ≠ mt_pos c4 kk"
using c4_kk by simp
have c7_at_addr:
"mt_tape c7 kk (mt_pos c' kk + 1) = mt_tape c' kk (mt_pos c' kk + 1)"
proof -
have "mt_tape c7 kk (mt_pos c' kk + 1) = mt_tape c6 kk (mt_pos c' kk + 1)"
using mttm_step_tape_off_head[OF step7 pp1_ne_c6] .
also have "… = mt_tape c5 kk (mt_pos c' kk + 1)"
using mttm_step_tape_off_head[OF step6 pp1_ne_c5] .
also have "… = mt_tape c4 kk (mt_pos c' kk + 1)"
using mttm_step_tape_off_head[OF step5 pp1_ne_c4] .
also have "… = mt_tape c' kk (mt_pos c' kk + 1)"
using tape_c4_eq_c' by simp
finally show ?thesis .
qed
have read_ne_LE: "tts kk (nn kk) ≠ LE_block (le_tm M)"
proof -
have "tts kk (nn kk) = mt_tape c7 kk (mt_pos c7 kk)"
using c7_eq8 nn_kk by simp
also have "… = mt_tape c7 kk (mt_pos c' kk + 1)"
using c7_kk by simp
also have "… = mt_tape c' kk (mt_pos c' kk + 1)" using c7_at_addr .
finally have read_eq:
"tts kk (nn kk) = mt_tape c' kk (mt_pos c' kk + 1)" .
have "mt_tape c' kk (mt_pos c' kk + 1) ≠ LE_block (le_tm M)"
using right_not_le_c' by blast
thus ?thesis using read_eq by simp
qed
have dest6_AE_Right: "dest6 kk = AE_Right"
using AE_Right dest6_eq_dest5 by simp
have dr8_kk: "dr8 kk = dir.N"
using dr8_eq buf_eq dest_eq dest6_AE_Right buf6_kk h_ne_LE read_ne_LE kklt
by simp
have "mt_pos c8 kk = go_dir (dr8 kk) (nn kk)"
using c8_eq by simp
also have "… = nn kk" using dr8_kk by simp
also have "… = mt_pos c' kk + 1" using nn_kk_val .
finally show ?thesis using AE_Right by simp
qed
qed
text ‹Reconstruction leaf of ‹ae_simulates_forward_stage_general›:
the position-decode invariant at ‹c8›. When ‹c8› is at
‹SS1› (the non-halt super-step boundary), each simulated head
‹mt_pos cM_k k› is recovered from the M'-side head
‹mt_pos c8 k› and the recorded offset ‹off k› via
‹ae_decode_pos›. Per-tape regime case-split on
‹mt_pos c' kk› feeding the three ‹c8_pos_for_*› head
trajectories; the ‹idx = SS1› antecedent rules out the halt
branch (which would land at ‹init_stage› = VFwd). ›
lemma ae_fwd_pos_decode_c8:
fixes M :: "('q, 'a) mttm"
and c' c8 :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
and cM_k :: "('a, 'q) mt_config"
and q6 :: 'q
and ofs5 ofs6 :: "nat ⇒ 'c"
and buf5 buf6 :: "nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)"
and dest5 :: "nat ⇒ ae_dest"
assumes ofs6_eq_ofs5: "ofs6 = ofs5"
and c8_state: "mt_state c8 = (q6, if q6 ∈ {t_tm M, r_tm M}
then init_stage (le_tm M)
else (ofs6, buf6, init_dest, SS1))"
and cM_k_window_general:
"∀kk<k_tm M. ae_window_invariant_general
(mt_tape cM_k kk) (mt_pos cM_k kk)
(dest5 kk, ofs5 kk) (buf5 kk)
(mt_pos c' kk) (le_tm M)"
and c8_pos_for_pos0:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 0
⟹ mt_pos c8 kk = (if dest5 kk = AE_Right then 1 else 0)"
and c8_pos_for_pos_ge2:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2
⟹ mt_pos c8 kk = (case dest5 kk of
AE_Left ⇒ mt_pos c' kk - 1
| AE_Home ⇒ mt_pos c' kk
| AE_Right ⇒ mt_pos c' kk + 1)"
and c8_pos_for_pos1:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 1
⟹ mt_pos c8 kk = (case dest5 kk of
AE_Left ⇒ 0
| AE_Home ⇒ 1
| AE_Right ⇒ 2)"
shows "(case mt_state c8 of (_, _, _, _, idx) ⇒ idx = SS1)
⟶ (∀k<k_tm M. mt_pos cM_k k
= ae_decode_pos (mt_pos c8 k)
(case mt_state c8 of (_, off, _, _, _) ⇒ off k))"
proof -
let ?c = "card (UNIV :: 'c set)"
show ?thesis
proof
assume idx_ss1: "case mt_state c8 of (_, _, _, _, idx) ⇒ idx = SS1"
have q6_nhalt: "q6 ∉ {t_tm M, r_tm M}"
proof (rule ccontr)
assume "¬ q6 ∉ {t_tm M, r_tm M}"
hence q6_in: "q6 ∈ {t_tm M, r_tm M}" by simp
hence c8_eq_halt: "mt_state c8 = (q6, init_stage (le_tm M))"
using c8_state by simp
thus False using idx_ss1 by (simp add: init_stage_def)
qed
have c8_nh: "mt_state c8 = (q6, ofs6, buf6, init_dest, SS1)"
using c8_state q6_nhalt by simp
show "∀k<k_tm M. mt_pos cM_k k
= ae_decode_pos (mt_pos c8 k)
(case mt_state c8 of (_, off, _, _, _) ⇒ off k)"
proof (intro allI impI)
fix kk assume kklt: "kk < k_tm M"
have ofs_at_c8:
"(case mt_state c8 of (_, off, _, _, _) ⇒ off kk) = ofs6 kk"
using c8_nh by simp
have ofs5_eq_kk: "ofs5 kk = ofs6 kk" using ofs6_eq_ofs5 by simp
have wi: "ae_window_invariant_general
(mt_tape cM_k kk) (mt_pos cM_k kk)
(dest5 kk, ofs5 kk) (buf5 kk)
(mt_pos c' kk) (le_tm M)"
using cM_k_window_general[rule_format, OF kklt] by simp
consider (le0) "mt_pos c' kk = 0"
| (le1) "mt_pos c' kk = 1"
| (steady) "mt_pos c' kk ≥ 2"
by linarith
thus "mt_pos cM_k kk
= ae_decode_pos (mt_pos c8 kk)
(case mt_state c8 of (_, off, _, _, _) ⇒ off kk)"
proof cases
case le0
have win_le0: "ae_window_invariant_le0
(mt_tape cM_k kk) (mt_pos cM_k kk)
(dest5 kk, ofs5 kk) (buf5 kk) (le_tm M)"
using wi le0 unfolding ae_window_invariant_general_def by simp
show ?thesis
proof (cases "dest5 kk")
case AE_Left
have "False"
using win_le0 AE_Left
unfolding ae_window_invariant_le0_def by simp
thus ?thesis ..
next
case AE_Home
have c8_kk: "mt_pos c8 kk = 0"
using c8_pos_for_pos0[OF kklt le0] AE_Home by simp
have mp_cM_k: "mt_pos cM_k kk = 0"
using win_le0 AE_Home
unfolding ae_window_invariant_le0_def by simp
have decode: "ae_decode_pos 0 (ofs6 kk) = 0"
unfolding ae_decode_pos_def by simp
show ?thesis using c8_kk mp_cM_k decode ofs_at_c8 by simp
next
case AE_Right
have c8_kk: "mt_pos c8 kk = 1"
using c8_pos_for_pos0[OF kklt le0] AE_Right by simp
have mp_cM_k: "mt_pos cM_k kk = Suc (c_idx (ofs5 kk))"
using win_le0 AE_Right
unfolding ae_window_invariant_le0_def by simp
have decode: "ae_decode_pos 1 (ofs6 kk) = Suc (c_idx (ofs6 kk))"
unfolding ae_decode_pos_def by simp
show ?thesis
using c8_kk mp_cM_k decode ofs_at_c8 ofs5_eq_kk by simp
qed
next
case le1
have win_le1: "ae_window_invariant_le1
(mt_tape cM_k kk) (mt_pos cM_k kk)
(dest5 kk, ofs5 kk) (buf5 kk) (le_tm M)"
using wi le1 unfolding ae_window_invariant_general_def by simp
show ?thesis
proof (cases "dest5 kk")
case AE_Left
have c8_kk: "mt_pos c8 kk = 0"
using c8_pos_for_pos1[OF kklt le1] AE_Left by simp
have mp_cM_k: "mt_pos cM_k kk = 0"
using win_le1 AE_Left
unfolding ae_window_invariant_le1_def by simp
have decode: "ae_decode_pos 0 (ofs6 kk) = 0"
unfolding ae_decode_pos_def by simp
show ?thesis using c8_kk mp_cM_k decode ofs_at_c8 by simp
next
case AE_Home
have c8_kk: "mt_pos c8 kk = 1"
using c8_pos_for_pos1[OF kklt le1] AE_Home by simp
have mp_cM_k: "mt_pos cM_k kk = Suc (c_idx (ofs5 kk))"
using win_le1 AE_Home
unfolding ae_window_invariant_le1_def by simp
have decode: "ae_decode_pos 1 (ofs6 kk) = Suc (c_idx (ofs6 kk))"
unfolding ae_decode_pos_def by simp
show ?thesis
using c8_kk mp_cM_k decode ofs_at_c8 ofs5_eq_kk by simp
next
case AE_Right
have c8_kk: "mt_pos c8 kk = 2"
using c8_pos_for_pos1[OF kklt le1] AE_Right by simp
have mp_cM_k:
"mt_pos cM_k kk = Suc (?c + c_idx (ofs5 kk))"
using win_le1 AE_Right
unfolding ae_window_invariant_le1_def by simp
have decode:
"ae_decode_pos 2 (ofs6 kk) = Suc (?c + c_idx (ofs6 kk))"
unfolding ae_decode_pos_def by simp
show ?thesis
using c8_kk mp_cM_k decode ofs_at_c8 ofs5_eq_kk by simp
qed
next
case steady
have win_steady: "ae_window_invariant
(mt_tape cM_k kk) (mt_pos cM_k kk)
(dest5 kk, ofs5 kk) (buf5 kk)
((mt_pos c' kk - 2) * ?c + 1)"
using wi steady unfolding ae_window_invariant_general_def by simp
have mp_cM_k:
"mt_pos cM_k kk
= (mt_pos c' kk - 2) * ?c + 1 + bp_linear (dest5 kk, ofs5 kk)"
using win_steady unfolding ae_window_invariant_def by simp
show ?thesis
proof (cases "dest5 kk")
case AE_Left
have c8_kk: "mt_pos c8 kk = mt_pos c' kk - 1"
using c8_pos_for_pos_ge2[OF kklt steady] AE_Left by simp
have bp_lin: "bp_linear (dest5 kk, ofs5 kk) = c_idx (ofs5 kk)"
using AE_Left unfolding bp_linear_def by simp
have decode:
"ae_decode_pos (mt_pos c' kk - 1) (ofs6 kk)
= (mt_pos c' kk - 2) * ?c + c_idx (ofs6 kk) + 1"
proof -
have "ae_decode_pos (mt_pos c' kk - 1) (ofs6 kk)
= (mt_pos c' kk - 1 - 1) * ?c + c_idx (ofs6 kk) + 1"
using steady unfolding ae_decode_pos_def by simp
also have "… = (mt_pos c' kk - 2) * ?c + c_idx (ofs6 kk) + 1"
using steady by (simp add: numeral_2_eq_2)
finally show ?thesis .
qed
show ?thesis
using c8_kk mp_cM_k bp_lin decode ofs_at_c8 ofs5_eq_kk by simp
next
case AE_Home
have c8_kk: "mt_pos c8 kk = mt_pos c' kk"
using c8_pos_for_pos_ge2[OF kklt steady] AE_Home by simp
have bp_lin: "bp_linear (dest5 kk, ofs5 kk) = ?c + c_idx (ofs5 kk)"
using AE_Home unfolding bp_linear_def by simp
have decode:
"ae_decode_pos (mt_pos c' kk) (ofs6 kk)
= (mt_pos c' kk - 1) * ?c + c_idx (ofs6 kk) + 1"
using steady unfolding ae_decode_pos_def by simp
have addr_eq:
"(mt_pos c' kk - 2) * ?c + 1 + (?c + c_idx (ofs5 kk))
= (mt_pos c' kk - 1) * ?c + c_idx (ofs5 kk) + 1"
proof -
have c_split: "(mt_pos c' kk - 1) * ?c
= (mt_pos c' kk - 2) * ?c + ?c"
using steady by (simp add: algebra_simps diff_mult_distrib)
thus ?thesis by linarith
qed
show ?thesis
using c8_kk mp_cM_k bp_lin decode addr_eq ofs_at_c8 ofs5_eq_kk
by simp
next
case AE_Right
have c8_kk: "mt_pos c8 kk = mt_pos c' kk + 1"
using c8_pos_for_pos_ge2[OF kklt steady] AE_Right by simp
have bp_lin:
"bp_linear (dest5 kk, ofs5 kk) = 2 * ?c + c_idx (ofs5 kk)"
using AE_Right unfolding bp_linear_def by simp
have decode:
"ae_decode_pos (mt_pos c' kk + 1) (ofs6 kk)
= mt_pos c' kk * ?c + c_idx (ofs6 kk) + 1"
unfolding ae_decode_pos_def by simp
have addr_eq:
"(mt_pos c' kk - 2) * ?c + 1 + (2 * ?c + c_idx (ofs5 kk))
= mt_pos c' kk * ?c + c_idx (ofs5 kk) + 1"
proof -
have c_split: "mt_pos c' kk * ?c
= (mt_pos c' kk - 2) * ?c + 2 * ?c"
using steady by (simp add: algebra_simps diff_mult_distrib)
thus ?thesis by linarith
qed
show ?thesis
using c8_kk mp_cM_k bp_lin decode addr_eq ofs_at_c8 ofs5_eq_kk
by simp
qed
qed
qed
qed
qed
text ‹Reconstruction leaf of ‹ae_simulates_forward_stage_general›:
the ‹c8› head position for an le1 tape (‹mt_pos c' kk = 1›),
as a ‹dest5›-case value (‹AE_Left› -> 0, ‹AE_Home› -> 1,
‹AE_Right› -> 2). For ‹AE_Left› SS8 reads the LE-marked
cell 0 at ‹c7_pos = 0› (via ‹tape_c7_zero_le_pos1_dest_left›)
and stays; otherwise SS8 steps from ‹c7_pos› per the recorded
‹dest›. ›
lemma ae_fwd_c8_pos_for_pos1:
fixes M :: "('q, 'a) mttm"
and c' c4 c5 c6 c7 c8 :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
and q5 q6 :: 'q
and ofs5 ofs6 :: "nat ⇒ 'c"
and buf5 buf6 :: "nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)"
and dest5 dest6 :: "nat ⇒ ae_dest"
assumes step5: "(c4, c5) ∈ mttm_step (alphabet_enlarge_delta M)"
and tape_c4_eq_c': "mt_tape c4 = mt_tape c'"
and buf5_not_le_per_tape:
"∀k<k_tm M. (mt_pos c' k = 0
⟶ fst (buf5 k) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))
∧ (mt_pos c' k = 1
⟶ fst (snd (buf5 k)) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))
∧ (mt_pos c' k ≥ 2
⟶ fst (buf5 k) ≠ LE_block (le_tm M)
∧ fst (snd (buf5 k)) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))"
and right_not_le_c':
"∀k. mt_tape c' k (mt_pos c' k + 1) ≠ LE_block (le_tm M)"
and c4_pos: "⋀kk. kk < k_tm M ⟹ mt_pos c4 kk = mt_pos c' kk"
and c5_pos_for_pos1:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 1 ⟹ dest5 kk ≠ AE_Left
⟹ mt_pos c5 kk = 0"
and step6: "(c5, c6) ∈ mttm_step (alphabet_enlarge_delta M)"
and step7: "(c6, c7) ∈ mttm_step (alphabet_enlarge_delta M)"
and c7_state: "mt_state c7 = (q6, ofs6, buf6, dest6, SS8)"
and buf6_eq_buf5: "buf6 = buf5"
and dest6_eq_dest5: "dest6 = dest5"
and c7_pos_for_pos1_dest_left:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 1 ⟹ dest5 kk = AE_Left
⟹ mt_pos c7 kk = 0"
and tape_c7_zero_le_pos1_dest_left:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 1 ⟹ dest5 kk = AE_Left
⟹ mt_tape c7 kk 0 = LE_block (le_tm M)"
and step8_sub: "(c7, c8) ∈ mttm_step (ae_delta_ss8_ss1 M)"
and c6_pos_for_pos1:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 1 ⟹ mt_pos c6 kk = 1"
and c7_pos_for_pos1:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 1
⟹ mt_pos c7 kk = (if dest5 kk = AE_Left then 0 else 2)"
shows "⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 1
⟹ mt_pos c8 kk = (case dest5 kk of
AE_Left ⇒ 0
| AE_Home ⇒ 1
| AE_Right ⇒ 2)"
proof -
fix kk
assume kklt: "kk < k_tm M"
assume pos_kk: "mt_pos c' kk = 1"
obtain qq tts nn qq' aa8 dr8 where
c7_eq8: "c7 = Config⇩M qq tts nn"
and c8_eq: "c8 = Config⇩M qq'
(λk. (tts k)(nn k := aa8 k))
(λk. go_dir (dr8 k) (nn k))"
and tr_in: "(qq, λk. tts k (nn k), qq', aa8, dr8)
∈ ae_delta_ss8_ss1 M"
using step8_sub by (auto elim: mttm_step.cases)
obtain q ofs buf dest where
qq_eq: "qq = (q, ofs, buf, dest, SS8)"
and dr8_eq:
"dr8 = (λk. if k < k_tm M then snd (ae_ss8_action (le_tm M)
(tts k (nn k)) (buf k) (dest k)) else dir.N)"
using tr_in by (auto simp: ae_delta_ss8_ss1_def)
have qq_state: "qq = (q6, ofs6, buf6, dest6, SS8)"
using c7_state c7_eq8 by simp
have buf_eq: "buf = buf6" using qq_eq qq_state by simp
have dest_eq: "dest = dest6" using qq_eq qq_state by simp
have nn_kk: "nn kk = mt_pos c7 kk" using c7_eq8 by simp
obtain ll hh rr where buf5_kk: "buf5 kk = (ll, hh, rr)"
using prod.exhaust by metis
have buf6_kk: "buf6 kk = (ll, hh, rr)"
using buf5_kk buf6_eq_buf5 by simp
have h_ne_LE: "hh ≠ LE_block (le_tm M)"
proof -
have "fst (snd (buf5 kk)) ≠ LE_block (le_tm M)"
using buf5_not_le_per_tape[rule_format, OF kklt] pos_kk by blast
thus ?thesis using buf5_kk by simp
qed
show "mt_pos c8 kk = (case dest5 kk of
AE_Left ⇒ 0
| AE_Home ⇒ 1
| AE_Right ⇒ 2)"
proof (cases "dest5 kk")
case AE_Left
have c7_kk: "mt_pos c7 kk = 0"
using c7_pos_for_pos1_dest_left[OF kklt pos_kk AE_Left] .
have nn_kk_val: "nn kk = 0" using nn_kk c7_kk by simp
have read_LE: "tts kk (nn kk) = LE_block (le_tm M)"
proof -
have "tts kk (nn kk) = mt_tape c7 kk (mt_pos c7 kk)"
using c7_eq8 nn_kk by simp
also have "… = mt_tape c7 kk 0" using c7_kk by simp
also have "… = LE_block (le_tm M)"
using tape_c7_zero_le_pos1_dest_left[OF kklt pos_kk AE_Left] .
finally show ?thesis .
qed
have dr8_kk: "dr8 kk = dir.N" using dr8_eq read_LE kklt by simp
have "mt_pos c8 kk = go_dir (dr8 kk) (nn kk)"
using c8_eq by simp
also have "… = nn kk" using dr8_kk by simp
also have "… = 0" using nn_kk_val .
finally show ?thesis using AE_Left by simp
next
case AE_Home
have c7_kk: "mt_pos c7 kk = 2"
using c7_pos_for_pos1[OF kklt pos_kk] AE_Home by simp
have nn_kk_val: "nn kk = 2" using nn_kk c7_kk by simp
have dest_ne_left: "dest5 kk ≠ AE_Left" using AE_Home by simp
have c5_pos_kk: "mt_pos c5 kk = 0"
using c5_pos_for_pos1[OF kklt pos_kk dest_ne_left] .
have two_ne_c6: "(2 :: nat) ≠ mt_pos c6 kk"
using c6_pos_for_pos1[OF kklt pos_kk] by simp
have two_ne_c5: "(2 :: nat) ≠ mt_pos c5 kk"
using c5_pos_kk by simp
have two_ne_c4: "(2 :: nat) ≠ mt_pos c4 kk"
using c4_pos kklt pos_kk by simp
have c7_at_2: "mt_tape c7 kk 2 = mt_tape c' kk 2"
proof -
have "mt_tape c7 kk 2 = mt_tape c6 kk 2"
using mttm_step_tape_off_head[OF step7 two_ne_c6] .
also have "… = mt_tape c5 kk 2"
using mttm_step_tape_off_head[OF step6 two_ne_c5] .
also have "… = mt_tape c4 kk 2"
using mttm_step_tape_off_head[OF step5 two_ne_c4] .
also have "… = mt_tape c' kk 2" using tape_c4_eq_c' by simp
finally show ?thesis .
qed
have read_ne_LE: "tts kk (nn kk) ≠ LE_block (le_tm M)"
proof -
have "tts kk (nn kk) = mt_tape c7 kk (mt_pos c7 kk)"
using c7_eq8 nn_kk by simp
also have "… = mt_tape c7 kk 2" using c7_kk by simp
also have "… = mt_tape c' kk 2" using c7_at_2 .
finally have read_eq: "tts kk (nn kk) = mt_tape c' kk 2" .
have "mt_tape c' kk (mt_pos c' kk + 1) ≠ LE_block (le_tm M)"
using right_not_le_c' by blast
hence "mt_tape c' kk 2 ≠ LE_block (le_tm M)"
using pos_kk by (simp add: numeral_2_eq_2)
thus ?thesis using read_eq by simp
qed
have dest6_AE_Home: "dest6 kk = AE_Home"
using AE_Home dest6_eq_dest5 by simp
have dr8_kk: "dr8 kk = dir.L"
using dr8_eq buf_eq dest_eq dest6_AE_Home buf6_kk h_ne_LE read_ne_LE kklt
by simp
have "mt_pos c8 kk = go_dir (dr8 kk) (nn kk)"
using c8_eq by simp
also have "… = (nn kk) - 1" using dr8_kk by simp
also have "… = 1" using nn_kk_val by simp
finally show ?thesis using AE_Home by simp
next
case AE_Right
have c7_kk: "mt_pos c7 kk = 2"
using c7_pos_for_pos1[OF kklt pos_kk] AE_Right by simp
have nn_kk_val: "nn kk = 2" using nn_kk c7_kk by simp
have dest_ne_left: "dest5 kk ≠ AE_Left" using AE_Right by simp
have c5_pos_kk: "mt_pos c5 kk = 0"
using c5_pos_for_pos1[OF kklt pos_kk dest_ne_left] .
have two_ne_c6: "(2 :: nat) ≠ mt_pos c6 kk"
using c6_pos_for_pos1[OF kklt pos_kk] by simp
have two_ne_c5: "(2 :: nat) ≠ mt_pos c5 kk"
using c5_pos_kk by simp
have two_ne_c4: "(2 :: nat) ≠ mt_pos c4 kk"
using c4_pos kklt pos_kk by simp
have c7_at_2: "mt_tape c7 kk 2 = mt_tape c' kk 2"
proof -
have "mt_tape c7 kk 2 = mt_tape c6 kk 2"
using mttm_step_tape_off_head[OF step7 two_ne_c6] .
also have "… = mt_tape c5 kk 2"
using mttm_step_tape_off_head[OF step6 two_ne_c5] .
also have "… = mt_tape c4 kk 2"
using mttm_step_tape_off_head[OF step5 two_ne_c4] .
also have "… = mt_tape c' kk 2" using tape_c4_eq_c' by simp
finally show ?thesis .
qed
have read_ne_LE: "tts kk (nn kk) ≠ LE_block (le_tm M)"
proof -
have "tts kk (nn kk) = mt_tape c7 kk (mt_pos c7 kk)"
using c7_eq8 nn_kk by simp
also have "… = mt_tape c7 kk 2" using c7_kk by simp
also have "… = mt_tape c' kk 2" using c7_at_2 .
finally have read_eq: "tts kk (nn kk) = mt_tape c' kk 2" .
have "mt_tape c' kk (mt_pos c' kk + 1) ≠ LE_block (le_tm M)"
using right_not_le_c' by blast
hence "mt_tape c' kk 2 ≠ LE_block (le_tm M)"
using pos_kk by (simp add: numeral_2_eq_2)
thus ?thesis using read_eq by simp
qed
have dest6_AE_Right: "dest6 kk = AE_Right"
using AE_Right dest6_eq_dest5 by simp
have dr8_kk: "dr8 kk = dir.N"
using dr8_eq buf_eq dest_eq dest6_AE_Right buf6_kk h_ne_LE read_ne_LE kklt
by simp
have "mt_pos c8 kk = go_dir (dr8 kk) (nn kk)"
using c8_eq by simp
also have "… = nn kk" using dr8_kk by simp
also have "… = 2" using nn_kk_val .
finally show ?thesis using AE_Right by simp
qed
qed
text ‹Reconstruction leaf of ‹ae_simulates_forward_stage_general›:
the in-window ‹c8› value at block 1 for an le0 tape
(‹mt_pos c' kk = 0›). Uniformly ‹c8@1 = rr› (the right
buffer slot ‹snd (snd (buf5 kk))›); the SS6/SS7/SS8 substeps
write at cells ‹c5_pos = 0› / ‹c6_pos = 1› / ‹c7_pos›,
with cell 1 carrying the buffered right value. ›
lemma ae_fwd_c8_at_one_for_pos0:
fixes M :: "('q, 'a) mttm"
and c' c4 c5 c6 c7 c8 :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
and q5 q6 :: 'q
and ofs5 ofs6 :: "nat ⇒ 'c"
and buf5 buf6 :: "nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)"
and dest5 dest6 :: "nat ⇒ ae_dest"
assumes step5: "(c4, c5) ∈ mttm_step (alphabet_enlarge_delta M)"
and tape_c4_eq_c': "mt_tape c4 = mt_tape c'"
and buf5_not_le_per_tape:
"∀k<k_tm M. (mt_pos c' k = 0
⟶ fst (buf5 k) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))
∧ (mt_pos c' k = 1
⟶ fst (snd (buf5 k)) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))
∧ (mt_pos c' k ≥ 2
⟶ fst (buf5 k) ≠ LE_block (le_tm M)
∧ fst (snd (buf5 k)) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))"
and right_not_le_c':
"∀k. mt_tape c' k (mt_pos c' k + 1) ≠ LE_block (le_tm M)"
and c4_pos: "⋀kk. kk < k_tm M ⟹ mt_pos c4 kk = mt_pos c' kk"
and step6: "(c5, c6) ∈ mttm_step (alphabet_enlarge_delta M)"
and step7_sub: "(c6, c7) ∈ mttm_step (ae_delta_ss7_ss8 M)"
and c6_state: "mt_state c6 = (q6, ofs6, buf6, dest6, SS7)"
and c7_state: "mt_state c7 = (q6, ofs6, buf6, dest6, SS8)"
and buf6_eq_buf5: "buf6 = buf5"
and dest6_eq_dest5: "dest6 = dest5"
and step8_sub: "(c7, c8) ∈ mttm_step (ae_delta_ss8_ss1 M)"
and step8: "(c7, c8) ∈ mttm_step (alphabet_enlarge_delta M)"
and c5_pos_for_pos0:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 0 ⟹ mt_pos c5 kk = 0"
and buf5_h_le_for_pos0:
"∀k<k_tm M. mt_pos c' k = 0 ⟶ fst (snd (buf5 k)) = LE_block (le_tm M)"
and c6_pos_for_pos0:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 0 ⟹ mt_pos c6 kk = 1"
and c7_pos_for_pos0:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 0
⟹ mt_pos c7 kk = (if dest5 kk = AE_Right then 1 else 0)"
shows "⋀kk. kk < k_tm M ⟹ mt_pos c' kk = 0
⟹ mt_tape c8 kk 1 = snd (snd (buf5 kk))"
proof -
fix kk
assume kklt: "kk < k_tm M"
assume pos_kk: "mt_pos c' kk = 0"
obtain qq tts nn qq' aa7 dr7 where
c6_eq7: "c6 = Config⇩M qq tts nn"
and c7_eq: "c7 = Config⇩M qq'
(λk. (tts k)(nn k := aa7 k))
(λk. go_dir (dr7 k) (nn k))"
and tr7_in: "(qq, λk. tts k (nn k), qq', aa7, dr7)
∈ ae_delta_ss7_ss8 M"
using step7_sub by (auto elim: mttm_step.cases)
obtain q7 ofs7 buf7 dest7 where
qq_eq7: "qq = (q7, ofs7, buf7, dest7, SS7)"
and aa7_eq:
"aa7 = (λk. if k < k_tm M then fst (ae_ss7_action (le_tm M)
(tts k (nn k)) (buf7 k) (dest7 k)) else bl_block (bl_tm M))"
using tr7_in by (auto simp: ae_delta_ss7_ss8_def)
have qq_state: "qq = (q6, ofs6, buf6, dest6, SS7)"
using c6_state c6_eq7 by simp
have buf7_eq: "buf7 = buf6" using qq_eq7 qq_state by simp
have dest7_eq: "dest7 = dest6" using qq_eq7 qq_state by simp
have nn7_kk: "nn kk = mt_pos c6 kk" using c6_eq7 by simp
have c6_kk: "mt_pos c6 kk = 1" using c6_pos_for_pos0[OF kklt pos_kk] .
have nn7_kk_1: "nn kk = 1" using nn7_kk c6_kk by simp
have one_ne_c5_pos: "(1 :: nat) ≠ mt_pos c5 kk"
using c5_pos_for_pos0[OF kklt pos_kk] by simp
have one_ne_c4_pos: "(1 :: nat) ≠ mt_pos c4 kk"
using c4_pos kklt pos_kk by simp
have c6_at_1: "mt_tape c6 kk 1 = mt_tape c' kk 1"
proof -
have "mt_tape c6 kk 1 = mt_tape c5 kk 1"
using mttm_step_tape_off_head[OF step6 one_ne_c5_pos] .
also have "… = mt_tape c4 kk 1"
using mttm_step_tape_off_head[OF step5 one_ne_c4_pos] .
also have "… = mt_tape c' kk 1" using tape_c4_eq_c' by simp
finally show ?thesis .
qed
have read7_ne_LE: "tts kk (nn kk) ≠ LE_block (le_tm M)"
proof -
have "tts kk (nn kk) = mt_tape c6 kk (mt_pos c6 kk)"
using c6_eq7 nn7_kk by simp
also have "… = mt_tape c6 kk 1" using c6_kk by simp
also have "… = mt_tape c' kk 1" using c6_at_1 .
finally have read_eq: "tts kk (nn kk) = mt_tape c' kk 1" .
have "mt_tape c' kk (mt_pos c' kk + 1) ≠ LE_block (le_tm M)"
using right_not_le_c' by blast
hence "mt_tape c' kk 1 ≠ LE_block (le_tm M)" using pos_kk by simp
thus ?thesis using read_eq by simp
qed
obtain ll hh rr where buf5_kk: "buf5 kk = (ll, hh, rr)"
using prod.exhaust by metis
have buf6_kk: "buf6 kk = (ll, hh, rr)"
using buf5_kk buf6_eq_buf5 by simp
have hh_le: "hh = LE_block (le_tm M)"
proof -
have "fst (snd (buf5 kk)) = LE_block (le_tm M)"
using buf5_h_le_for_pos0[rule_format, OF kklt] pos_kk by blast
thus ?thesis using buf5_kk by simp
qed
have c7_at_1_eq_rr: "mt_tape c7 kk 1 = rr"
proof -
have aa7_kk: "aa7 kk = rr"
using aa7_eq buf7_eq buf6_kk hh_le read7_ne_LE kklt by simp
have "mt_tape c7 kk 1 = aa7 kk" using c7_eq nn7_kk_1 by simp
thus ?thesis using aa7_kk by simp
qed
show "mt_tape c8 kk 1 = snd (snd (buf5 kk))"
proof (cases "dest5 kk = AE_Right")
case True
have c7_pos_kk: "mt_pos c7 kk = 1"
using c7_pos_for_pos0[OF kklt pos_kk] True by simp
obtain qq8 tts8 nn8 qq8' aa8 dr8 where
c7_eq8: "c7 = Config⇩M qq8 tts8 nn8"
and c8_eq: "c8 = Config⇩M qq8'
(λk. (tts8 k)(nn8 k := aa8 k))
(λk. go_dir (dr8 k) (nn8 k))"
and tr8_in: "(qq8, λk. tts8 k (nn8 k), qq8', aa8, dr8)
∈ ae_delta_ss8_ss1 M"
using step8_sub by (auto elim: mttm_step.cases)
obtain q8 ofs8 buf8 dest8 where
qq8_eq: "qq8 = (q8, ofs8, buf8, dest8, SS8)"
and aa8_eq:
"aa8 = (λk. if k < k_tm M then fst (ae_ss8_action (le_tm M)
(tts8 k (nn8 k)) (buf8 k) (dest8 k)) else bl_block (bl_tm M))"
using tr8_in by (auto simp: ae_delta_ss8_ss1_def)
have qq8_state: "qq8 = (q6, ofs6, buf6, dest6, SS8)"
using c7_state c7_eq8 by simp
have buf8_eq: "buf8 = buf6" using qq8_eq qq8_state by simp
have dest8_eq: "dest8 = dest6" using qq8_eq qq8_state by simp
have nn8_kk: "nn8 kk = mt_pos c7 kk" using c7_eq8 by simp
have nn8_kk_1: "nn8 kk = 1" using nn8_kk c7_pos_kk by simp
have rr_ne_LE: "rr ≠ LE_block (le_tm M)"
proof -
have "snd (snd (buf5 kk)) ≠ LE_block (le_tm M)"
using buf5_not_le_per_tape[rule_format, OF kklt] pos_kk by blast
thus ?thesis using buf5_kk by simp
qed
have read8_ne_LE: "tts8 kk (nn8 kk) ≠ LE_block (le_tm M)"
proof -
have "tts8 kk (nn8 kk) = mt_tape c7 kk (mt_pos c7 kk)"
using c7_eq8 nn8_kk by simp
also have "… = mt_tape c7 kk 1" using c7_pos_kk by simp
also have "… = rr" using c7_at_1_eq_rr .
finally have "tts8 kk (nn8 kk) = rr" .
thus ?thesis using rr_ne_LE by simp
qed
have dest6_eq: "dest6 kk = AE_Right" using True dest6_eq_dest5 by simp
have aa8_kk: "aa8 kk = rr"
using aa8_eq buf8_eq dest8_eq dest6_eq buf6_kk hh_le read8_ne_LE kklt
by simp
have "mt_tape c8 kk 1 = aa8 kk" using c8_eq nn8_kk_1 by simp
also have "… = rr" using aa8_kk .
also have "… = snd (snd (buf5 kk))" using buf5_kk by simp
finally show ?thesis .
next
case False
have c7_pos_kk: "mt_pos c7 kk = 0"
using c7_pos_for_pos0[OF kklt pos_kk] False by simp
have one_ne_c7_pos: "(1 :: nat) ≠ mt_pos c7 kk"
using c7_pos_kk by simp
have "mt_tape c8 kk 1 = mt_tape c7 kk 1"
using mttm_step_tape_off_head[OF step8 one_ne_c7_pos] .
also have "… = rr" using c7_at_1_eq_rr .
also have "… = snd (snd (buf5 kk))" using buf5_kk by simp
finally show ?thesis .
qed
qed
text ‹Reconstruction leaf of ‹ae_simulates_forward_stage_general›:
the ‹c6› head position for a steady tape
(‹mt_pos c' kk ≥ 2›) is unchanged from ‹mt_pos c' kk›.
SS6's action writes at ‹c5_pos› (‹pos \<mp> 1› per
‹dest5›) and steps back, so ‹c6› lands on the home
block ‹pos›; the non-LE window facts rule out the
LE-marker short-circuit. ›
lemma ae_fwd_c6_pos_for_pos_ge2:
fixes M :: "('q, 'a) mttm"
and c' c4 c5 c6 :: "('c :: enum ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
and q5 :: 'q
and ofs5 :: "nat ⇒ 'c"
and buf5 :: "nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)"
and dest5 :: "nat ⇒ ae_dest"
assumes step5: "(c4, c5) ∈ mttm_step (alphabet_enlarge_delta M)"
and c5_state: "mt_state c5 = (q5, ofs5, buf5, dest5, SS6)"
and tape_c4_eq_c': "mt_tape c4 = mt_tape c'"
and buf5_not_le_per_tape:
"∀k<k_tm M. (mt_pos c' k = 0
⟶ fst (buf5 k) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))
∧ (mt_pos c' k = 1
⟶ fst (snd (buf5 k)) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))
∧ (mt_pos c' k ≥ 2
⟶ fst (buf5 k) ≠ LE_block (le_tm M)
∧ fst (snd (buf5 k)) ≠ LE_block (le_tm M)
∧ snd (snd (buf5 k)) ≠ LE_block (le_tm M))"
and right_not_le_c':
"∀k. mt_tape c' k (mt_pos c' k + 1) ≠ LE_block (le_tm M)"
and c4_pos: "⋀kk. kk < k_tm M ⟹ mt_pos c4 kk = mt_pos c' kk"
and step6_sub: "(c5, c6) ∈ mttm_step (ae_delta_ss6_ss7 M)"
and c5_pos_for_pos_ge2:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2 ⟹ dest5 kk ≠ AE_Left
⟹ mt_pos c5 kk = mt_pos c' kk - 1"
and c5_pos_for_pos_ge2_dest_left:
"⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2 ⟹ dest5 kk = AE_Left
⟹ mt_pos c5 kk = mt_pos c' kk + 1"
and left_not_le_c'_steady:
"∀k. mt_pos c' k ≥ 2
⟶ mt_tape c' k (mt_pos c' k - 1) ≠ LE_block (le_tm M)"
shows "⋀kk. kk < k_tm M ⟹ mt_pos c' kk ≥ 2 ⟹ mt_pos c6 kk = mt_pos c' kk"
proof -
fix kk
assume kklt: "kk < k_tm M"
assume hge2: "mt_pos c' kk ≥ 2"
obtain qq tts nn qq' aa6 dr6 where
c5_eq6: "c5 = Config⇩M qq tts nn"
and c6_eq: "c6 = Config⇩M qq'
(λk. (tts k)(nn k := aa6 k))
(λk. go_dir (dr6 k) (nn k))"
and tr_in: "(qq, λk. tts k (nn k), qq', aa6, dr6)
∈ ae_delta_ss6_ss7 M"
using step6_sub by (auto elim: mttm_step.cases)
obtain q ofs buf dest where
qq_eq: "qq = (q, ofs, buf, dest, SS6)"
and dr6_eq:
"dr6 = (λk. if k < k_tm M then snd (ae_ss6_action (le_tm M)
(tts k (nn k)) (buf k) (dest k)) else dir.N)"
using tr_in by (auto simp: ae_delta_ss6_ss7_def)
have qq_state: "qq = (q5, ofs5, buf5, dest5, SS6)"
using c5_state c5_eq6 by simp
have buf_eq: "buf = buf5" using qq_eq qq_state by simp
have dest_eq: "dest = dest5" using qq_eq qq_state by simp
have nn_kk: "nn kk = mt_pos c5 kk" using c5_eq6 by simp
obtain ll hh rr where buf5_kk: "buf5 kk = (ll, hh, rr)"
using prod.exhaust by metis
have h_ne_LE: "hh ≠ LE_block (le_tm M)"
proof -
have "fst (snd (buf5 kk)) ≠ LE_block (le_tm M)"
using buf5_not_le_per_tape[rule_format, OF kklt] hge2 by blast
thus ?thesis using buf5_kk by simp
qed
have c4_kk: "mt_pos c4 kk = mt_pos c' kk" using c4_pos kklt by simp
show "mt_pos c6 kk = mt_pos c' kk"
proof (cases "dest5 kk = AE_Left")
case True
have c5_kk: "mt_pos c5 kk = mt_pos c' kk + 1"
using c5_pos_for_pos_ge2_dest_left[OF kklt hge2 True] .
have nn_kk_val: "nn kk = mt_pos c' kk + 1" using nn_kk c5_kk by simp
have addr_ne_c4_pos: "(mt_pos c' kk + 1) ≠ mt_pos c4 kk"
using c4_kk by simp
have c5_at_addr:
"mt_tape c5 kk (mt_pos c' kk + 1) = mt_tape c' kk (mt_pos c' kk + 1)"
proof -
have "mt_tape c5 kk (mt_pos c' kk + 1)
= mt_tape c4 kk (mt_pos c' kk + 1)"
using mttm_step_tape_off_head[OF step5 addr_ne_c4_pos] .
also have "… = mt_tape c' kk (mt_pos c' kk + 1)"
using tape_c4_eq_c' by simp
finally show ?thesis .
qed
have read_ne_LE: "tts kk (nn kk) ≠ LE_block (le_tm M)"
proof -
have "tts kk (nn kk) = mt_tape c5 kk (mt_pos c5 kk)"
using c5_eq6 nn_kk by simp
also have "… = mt_tape c5 kk (mt_pos c' kk + 1)"
using c5_kk by simp
also have "… = mt_tape c' kk (mt_pos c' kk + 1)"
using c5_at_addr .
finally have read_eq:
"tts kk (nn kk) = mt_tape c' kk (mt_pos c' kk + 1)" .
have "mt_tape c' kk (mt_pos c' kk + 1) ≠ LE_block (le_tm M)"
using right_not_le_c' by blast
thus ?thesis using read_eq by simp
qed
have dr6_kk:
"dr6 kk = (if dest5 kk = AE_Left then dir.L else dir.R)"
using dr6_eq buf_eq dest_eq buf5_kk read_ne_LE h_ne_LE kklt by simp
have dr6_kk_L: "dr6 kk = dir.L" using dr6_kk True by simp
have "mt_pos c6 kk = go_dir (dr6 kk) (nn kk)"
using c6_eq by simp
also have "… = (nn kk) - 1" using dr6_kk_L by simp
also have "… = (mt_pos c' kk + 1) - 1" using nn_kk_val by simp
also have "… = mt_pos c' kk" by simp
finally show ?thesis .
next
case False
have c5_kk: "mt_pos c5 kk = mt_pos c' kk - 1"
using c5_pos_for_pos_ge2[OF kklt hge2 False] .
have nn_kk_val: "nn kk = mt_pos c' kk - 1" using nn_kk c5_kk by simp
have addr_ne_c4_pos: "(mt_pos c' kk - 1) ≠ mt_pos c4 kk"
using c4_kk hge2 by linarith
have c5_at_addr:
"mt_tape c5 kk (mt_pos c' kk - 1) = mt_tape c' kk (mt_pos c' kk - 1)"
proof -
have "mt_tape c5 kk (mt_pos c' kk - 1)
= mt_tape c4 kk (mt_pos c' kk - 1)"
using mttm_step_tape_off_head[OF step5 addr_ne_c4_pos] .
also have "… = mt_tape c' kk (mt_pos c' kk - 1)"
using tape_c4_eq_c' by simp
finally show ?thesis .
qed
have read_ne_LE: "tts kk (nn kk) ≠ LE_block (le_tm M)"
proof -
have "tts kk (nn kk) = mt_tape c5 kk (mt_pos c5 kk)"
using c5_eq6 nn_kk by simp
also have "… = mt_tape c5 kk (mt_pos c' kk - 1)"
using c5_kk by simp
also have "… = mt_tape c' kk (mt_pos c' kk - 1)"
using c5_at_addr .
finally have read_eq:
"tts kk (nn kk) = mt_tape c' kk (mt_pos c' kk - 1)" .
have "mt_tape c' kk (mt_pos c' kk - 1) ≠ LE_block (le_tm M)"
using left_not_le_c'_steady hge2 by blast
thus ?thesis using read_eq by simp
qed
have dr6_kk:
"dr6 kk = (if dest5 kk = AE_Left then dir.L else dir.R)"
using dr6_eq buf_eq dest_eq buf5_kk read_ne_LE h_ne_LE kklt by simp
have dr6_kk_R: "dr6 kk = dir.R" using dr6_kk False by simp
have "mt_pos c6 kk = go_dir (dr6 kk) (nn kk)"
using c6_eq by simp
also have "… = Suc (nn kk)" using dr6_kk_R by simp
also have "… = Suc (mt_pos c' kk - 1)" using nn_kk_val by simp
also have "… = mt_pos c' kk" using hge2 by simp
finally show ?thesis .
qed
qed
end