Theory AlphabetReduction_ForwardWrite
theory AlphabetReduction_ForwardWrite
imports AlphabetReduction_ForwardRead
begin
subsection ‹Write phase composition›
text ‹Relation-generic write back-walk loop scaffold. The walk
leaf (‹ar_write_walk_step›) is the ‹leaf› hypothesis; the
union- and sub-relation back-loops are thin instantiations.
Throughout, ‹b› abbreviates ‹block_width Γ› (the per-symbol cell width).›
lemma ar_write_back_loop_gen:
fixes M :: "('q, 'a) mttm"
and c0 :: "(sym4, 'q × 'a ar_stage) mt_config"
and R' :: "(sym4, 'q × 'a ar_stage) mt_config rel"
assumes leaf:
"⋀cc i. ⟦ valid_mttm M;
mt_state cc = (q, AR_SimWrite, tk, i, buf, dvec, posk);
q ∈ Q_tm M;
posk tk ≠ AR_AtLE;
mt_tape cc tk (mt_pos cc tk) ≠ LE4;
Suc i ≤ block_width (Γ_tm M);
ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk);
∀j ≥ k_tm M. mt_tape cc j (mt_pos cc j) = BLANK4;
ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk) ⟧
⟹ ∃c''. (cc, c'') ∈ R'
∧ mt_state c'' = (q, AR_SimWrite, tk, Suc i, buf, dvec, posk)
∧ mt_tape c'' = mt_tape cc
∧ mt_pos c'' = (mt_pos cc)(tk := mt_pos cc tk - 1)"
and vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and poskproper: "posk tk ≠ AR_AtLE"
and stg: "mt_state c0 = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pos_base: "mt_pos c0 tk = base + block_width (Γ_tm M)"
and notLE: "⋀m. ⟦ 1 ≤ m; m ≤ block_width (Γ_tm M) ⟧
⟹ mt_tape c0 tk (base + m) ≠ LE4"
and pad0: "∀j ≥ k_tm M. mt_tape c0 j (mt_pos c0 j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c'. (c0, c') ∈ R' ^^ block_width (Γ_tm M)
∧ mt_state c' = (q, AR_SimWrite, tk, block_width (Γ_tm M),
buf, dvec, posk)
∧ mt_pos c' tk = base
∧ mt_tape c' = mt_tape c0
∧ (∀k'. k' ≠ tk ⟶ mt_pos c' k' = mt_pos c0 k')"
proof -
let ?k = "block_width (Γ_tm M)"
let ?P = "λj c.
mt_state c = (q, AR_SimWrite, tk, j, buf, dvec, posk)
∧ mt_pos c tk = base + (?k - j)
∧ mt_tape c = mt_tape c0
∧ (∀k'. k' ≠ tk ⟶ mt_pos c k' = mt_pos c0 k')"
have mybase: "?P 0 c0" using stg pos_base by simp
have mystep:
"⋀j cc. ⟦ j < ?k; ?P j cc ⟧
⟹ ∃c''. (cc, c'') ∈ R'
∧ ?P (Suc j) c''"
proof -
fix j cc
assume jlt: "j < ?k" and Pj: "?P j cc"
from Pj have st_cc:
"mt_state cc = (q, AR_SimWrite, tk, j, buf, dvec, posk)"
and pos_cc: "mt_pos cc tk = base + (?k - j)"
and tape_cc: "mt_tape cc = mt_tape c0"
and other_cc: "∀k'. k' ≠ tk ⟶ mt_pos cc k' = mt_pos c0 k'"
by simp_all
have tk_lt: "tk < k_tm M" using src0 by (simp add: ar_stage_bounded_def)
have pad_cc: "∀j' ≥ k_tm M. mt_tape cc j' (mt_pos cc j') = BLANK4"
proof (intro allI impI)
fix j' assume jge: "k_tm M ≤ j'"
have jne: "j' ≠ tk" using jge tk_lt by simp
have "mt_tape cc j' (mt_pos cc j') = mt_tape c0 j' (mt_pos c0 j')"
using tape_cc other_cc jne by simp
thus "mt_tape cc j' (mt_pos cc j') = BLANK4" using pad0 jge by simp
qed
have src_cc: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, j, buf, dvec, posk)"
using src0 by (simp add: ar_stage_bounded_def)
have mge1: "1 ≤ ?k - j" using jlt by simp
have mlek: "?k - j ≤ ?k" by simp
have suc_le: "Suc j ≤ ?k" using jlt by simp
have jlt2: "j < 2 * ?k" using jlt by simp
have ksub: "?k - j = Suc (?k - Suc j)" using jlt by simp
have vsrc_cc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, j, buf, dvec, posk)"
using jlt2 buf_valid by (simp add: ar_valid_stage_def)
have notLE_cc: "mt_tape cc tk (mt_pos cc tk) ≠ LE4"
using tape_cc pos_cc notLE[OF mge1 mlek] by simp
obtain c'' where
bstep: "(cc, c'') ∈ R'"
and bst_state: "mt_state c'' = (q, AR_SimWrite, tk, Suc j, buf, dvec, posk)"
and bst_tape: "mt_tape c'' = mt_tape cc"
and bst_pos: "mt_pos c'' = (mt_pos cc)(tk := mt_pos cc tk - 1)"
using leaf
[OF vM st_cc qQ poskproper notLE_cc suc_le vsrc_cc pad_cc src_cc]
by blast
have pos_eq: "mt_pos c'' tk = base + (?k - Suc j)"
using bst_pos pos_cc ksub by simp
have tape_eq: "mt_tape c'' = mt_tape c0" using bst_tape tape_cc by simp
have other_eq: "∀k'. k' ≠ tk ⟶ mt_pos c'' k' = mt_pos c0 k'"
using bst_pos other_cc by simp
show "∃c''. (cc, c'') ∈ R'
∧ ?P (Suc j) c''"
using bstep bst_state pos_eq tape_eq other_eq by blast
qed
have loop:
"∃c'. (c0, c') ∈ R' ^^ ?k
∧ ?P ?k c'"
by (rule relpow_invariant_chain
[where P = ?P and n = ?k, OF mystep mybase])
obtain c' where
chain: "(c0, c') ∈ R' ^^ ?k"
and Pfin: "?P ?k c'"
using loop by blast
show ?thesis
proof (intro exI[where x = c'] conjI)
show "(c0, c') ∈ R' ^^ ?k" by (rule chain)
show "mt_state c' = (q, AR_SimWrite, tk, ?k, buf, dvec, posk)"
using Pfin by simp
show "mt_pos c' tk = base" using Pfin by simp
show "mt_tape c' = mt_tape c0" using Pfin by simp
show "∀k'. k' ≠ tk ⟶ mt_pos c' k' = mt_pos c0 k'" using Pfin by simp
qed
qed
text ‹The write back-walk loop, proper tape. From an
‹AR_SimWrite› stage at bit-counter ‹0› with the head at
the block end ‹base + b› (where the read phase left it) and
‹buf tk› a proper symbol, the head walks ‹L› across the
‹b›-cell block back to ‹base = sim_pos p›, reaching
bit-counter ‹b›. Tape unchanged (the back-walk only moves);
this is the simpler of the two write loops, the analogue of
‹ar_read_bit_loop› with a constant-tape invariant. Each
‹ar_write_walk_step› needs its current cell ‹≠ LE4›;
the visited cells are ‹base + 1 … base + b› (all proper
positions), supplied by ‹notLE›. Chain length ‹b›.›
lemma ar_write_back_loop:
fixes M :: "('q, 'a) mttm"
and c0 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and poskproper: "posk tk ≠ AR_AtLE"
and stg: "mt_state c0 = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pos_base: "mt_pos c0 tk = base + block_width (Γ_tm M)"
and notLE: "⋀m. ⟦ 1 ≤ m; m ≤ block_width (Γ_tm M) ⟧
⟹ mt_tape c0 tk (base + m) ≠ LE4"
and pad0: "∀j ≥ k_tm M. mt_tape c0 j (mt_pos c0 j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c'. (c0, c') ∈ (mttm_step (alphabet_reduce_delta M))
^^ block_width (Γ_tm M)
∧ mt_state c' = (q, AR_SimWrite, tk, block_width (Γ_tm M),
buf, dvec, posk)
∧ mt_pos c' tk = base
∧ mt_tape c' = mt_tape c0
∧ (∀k'. k' ≠ tk ⟶ mt_pos c' k' = mt_pos c0 k')"
by (rule ar_write_back_loop_gen
[OF ar_write_walk_step vM qQ kge2 poskproper stg buf_valid pos_base notLE
pad0 src0])
text ‹The write forward bit-write loop, proper tape. From an
‹AR_SimWrite› stage at bit-counter ‹b› with the head back
at ‹base› (where ‹ar_write_back_loop› left it), the head
walks ‹R› across the block writing each cell, reaching
bit-counter ‹b + (b - 1)› with the head at ‹base + (b -
1)›. Unlike the read loops this loop ∗‹mutates› the
tape: its invariant carries a partially-overwritten tape (cells
‹base … base + j - 1› already hold the new
‹write_bit› image, the rest hold old content), and each
‹ar_write_bit_step›'s ‹≠ LE4› guard reads the
∗‹not-yet-written› current cell ‹base + j›, which
still holds old content (supplied ‹≠ LE4› by
‹notLE›). Writes the first ‹b - 1› cells; the last is
the boundary step's job. Chain length ‹b - 1›.›
text ‹Relation-generic write forward-walk loop scaffold. The
bit-writing leaf (‹ar_write_bit_step›) is the ‹leaf›
hypothesis; the union- and sub-relation forward-loops are thin
instantiations.›
lemma ar_write_fwd_loop_gen:
fixes M :: "('q, 'a) mttm"
and c0 :: "(sym4, 'q × 'a ar_stage) mt_config"
and R' :: "(sym4, 'q × 'a ar_stage) mt_config rel"
assumes leaf:
"⋀cc i. ⟦ valid_mttm M;
mt_state cc = (q, AR_SimWrite, tk, i, buf, dvec, posk);
q ∈ Q_tm M;
posk tk ≠ AR_AtLE;
mt_tape cc tk (mt_pos cc tk) ≠ LE4;
block_width (Γ_tm M) ≤ i;
Suc i < 2 * block_width (Γ_tm M);
ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk);
∀j ≥ k_tm M. mt_tape cc j (mt_pos cc j) = BLANK4;
ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk) ⟧
⟹ ∃c''. (cc, c'') ∈ R'
∧ mt_state c'' = (q, AR_SimWrite, tk, Suc i, buf, dvec, posk)
∧ mt_tape c'' = (mt_tape cc)(tk :=
(mt_tape cc tk)(mt_pos cc tk
:= write_bit (Γ_tm M) (bl_tm M) (buf tk)
(i - block_width (Γ_tm M))))
∧ mt_pos c'' = (mt_pos cc)(tk := Suc (mt_pos cc tk))"
and vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and poskproper: "posk tk ≠ AR_AtLE"
and stg: "mt_state c0 = (q, AR_SimWrite, tk, block_width (Γ_tm M),
buf, dvec, posk)"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pos_base: "mt_pos c0 tk = base"
and notLE: "⋀m. m < block_width (Γ_tm M)
⟹ mt_tape c0 tk (base + m) ≠ LE4"
and pad0: "∀j ≥ k_tm M. mt_tape c0 j (mt_pos c0 j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, block_width (Γ_tm M), buf, dvec, posk)"
shows "∃c'. (c0, c') ∈ R' ^^ (block_width (Γ_tm M) - 1)
∧ mt_state c' = (q, AR_SimWrite, tk,
block_width (Γ_tm M) + (block_width (Γ_tm M) - 1),
buf, dvec, posk)
∧ mt_pos c' tk = base + (block_width (Γ_tm M) - 1)
∧ mt_tape c' tk = (λpos.
if base ≤ pos ∧ pos < base + (block_width (Γ_tm M) - 1)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c0 tk pos)
∧ (∀k'. k' ≠ tk ⟶ mt_tape c' k' = mt_tape c0 k')
∧ (∀k'. k' ≠ tk ⟶ mt_pos c' k' = mt_pos c0 k')"
proof -
let ?k = "block_width (Γ_tm M)"
let ?G = "Γ_tm M" and ?bl = "bl_tm M"
let ?wb = "λm. write_bit ?G ?bl (buf tk) m"
let ?tape = "λj pos. if base ≤ pos ∧ pos < base + j
then ?wb (pos - base) else mt_tape c0 tk pos"
let ?P = "λj c.
mt_state c = (q, AR_SimWrite, tk, ?k + j, buf, dvec, posk)
∧ mt_pos c tk = base + j
∧ mt_tape c tk = ?tape j
∧ (∀k'. k' ≠ tk ⟶ mt_tape c k' = mt_tape c0 k')
∧ (∀k'. k' ≠ tk ⟶ mt_pos c k' = mt_pos c0 k')"
have mybase: "?P 0 c0"
proof -
have "?tape 0 = mt_tape c0 tk" by (rule ext) auto
thus ?thesis using stg pos_base by simp
qed
have mystep:
"⋀j cc. ⟦ j < ?k - 1; ?P j cc ⟧
⟹ ∃c''. (cc, c'') ∈ R'
∧ ?P (Suc j) c''"
proof -
fix j cc
assume jlt: "j < ?k - 1" and Pj: "?P j cc"
from Pj have st_cc:
"mt_state cc = (q, AR_SimWrite, tk, ?k + j, buf, dvec, posk)"
and pos_cc: "mt_pos cc tk = base + j"
and tape_cc: "mt_tape cc tk = ?tape j"
and otape_cc: "∀k'. k' ≠ tk ⟶ mt_tape cc k' = mt_tape c0 k'"
and opos_cc: "∀k'. k' ≠ tk ⟶ mt_pos cc k' = mt_pos c0 k'"
by simp_all
have tk_lt: "tk < k_tm M" using src0 by (simp add: ar_stage_bounded_def)
have pad_cc: "∀j' ≥ k_tm M. mt_tape cc j' (mt_pos cc j') = BLANK4"
proof (intro allI impI)
fix j' assume jge: "k_tm M ≤ j'"
have jne: "j' ≠ tk" using jge tk_lt by simp
have "mt_tape cc j' (mt_pos cc j') = mt_tape c0 j' (mt_pos c0 j')"
using otape_cc opos_cc jne by simp
thus "mt_tape cc j' (mt_pos cc j') = BLANK4" using pad0 jge by simp
qed
have src_cc: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, ?k + j, buf, dvec, posk)"
using src0 by (simp add: ar_stage_bounded_def)
have jltk: "j < ?k" using jlt by simp
have ilo: "?k ≤ ?k + j" by simp
have ihi: "Suc (?k + j) < 2 * ?k" using jlt by simp
have idx: "?k + j - ?k = j" by simp
have vsrc_cc: "ar_valid_stage ?G ?bl
(AR_SimWrite, tk, ?k + j, buf, dvec, posk)"
using ihi buf_valid by (simp add: ar_valid_stage_def)
have cell_cur: "mt_tape cc tk (mt_pos cc tk) = mt_tape c0 tk (base + j)"
using tape_cc pos_cc by simp
have notLE_cc: "mt_tape cc tk (mt_pos cc tk) ≠ LE4"
using cell_cur notLE[OF jltk] by simp
obtain c'' where
bstep: "(cc, c'') ∈ R'"
and bst_state: "mt_state c'' = (q, AR_SimWrite, tk, Suc (?k + j),
buf, dvec, posk)"
and bst_tape: "mt_tape c'' = (mt_tape cc)(tk :=
(mt_tape cc tk)(mt_pos cc tk := ?wb (?k + j - ?k)))"
and bst_pos: "mt_pos c'' = (mt_pos cc)(tk := Suc (mt_pos cc tk))"
using leaf
[OF vM st_cc qQ poskproper notLE_cc ilo ihi vsrc_cc pad_cc src_cc]
by blast
have state_eq: "mt_state c'' = (q, AR_SimWrite, tk, ?k + Suc j, buf, dvec, posk)"
using bst_state by simp
have pos_eq: "mt_pos c'' tk = base + Suc j"
using bst_pos pos_cc by simp
have lhs: "mt_tape c'' tk = (?tape j)(base + j := ?wb j)"
using bst_tape tape_cc pos_cc idx by simp
have tape_eq: "mt_tape c'' tk = ?tape (Suc j)"
proof (rule ext)
fix pos
show "mt_tape c'' tk pos = ?tape (Suc j) pos"
proof (cases "pos = base + j")
case True
thus ?thesis using lhs by simp
next
case False
have "mt_tape c'' tk pos = ?tape j pos" using lhs False by simp
thus ?thesis using False by (auto simp: less_Suc_eq)
qed
qed
have otape_eq: "∀k'. k' ≠ tk ⟶ mt_tape c'' k' = mt_tape c0 k'"
using bst_tape otape_cc by simp
have opos_eq: "∀k'. k' ≠ tk ⟶ mt_pos c'' k' = mt_pos c0 k'"
using bst_pos opos_cc by simp
show "∃c''. (cc, c'') ∈ R'
∧ ?P (Suc j) c''"
using bstep state_eq pos_eq tape_eq otape_eq opos_eq by blast
qed
have loop:
"∃c'. (c0, c') ∈ R' ^^ (?k - 1)
∧ ?P (?k - 1) c'"
by (rule relpow_invariant_chain
[where P = ?P and n = "?k - 1", OF mystep mybase])
obtain c' where
chain: "(c0, c') ∈ R' ^^ (?k - 1)"
and Pfin: "?P (?k - 1) c'"
using loop by blast
show ?thesis
proof (intro exI[where x = c'] conjI)
show "(c0, c') ∈ R' ^^ (?k - 1)"
by (rule chain)
show "mt_state c' = (q, AR_SimWrite, tk, ?k + (?k - 1), buf, dvec, posk)"
using Pfin by simp
show "mt_pos c' tk = base + (?k - 1)" using Pfin by simp
show "mt_tape c' tk = (λpos.
if base ≤ pos ∧ pos < base + (?k - 1)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c0 tk pos)"
using Pfin by simp
show "∀k'. k' ≠ tk ⟶ mt_tape c' k' = mt_tape c0 k'" using Pfin by simp
show "∀k'. k' ≠ tk ⟶ mt_pos c' k' = mt_pos c0 k'" using Pfin by simp
qed
qed
lemma ar_write_fwd_loop:
fixes M :: "('q, 'a) mttm"
and c0 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and poskproper: "posk tk ≠ AR_AtLE"
and stg: "mt_state c0 = (q, AR_SimWrite, tk, block_width (Γ_tm M),
buf, dvec, posk)"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pos_base: "mt_pos c0 tk = base"
and notLE: "⋀m. m < block_width (Γ_tm M)
⟹ mt_tape c0 tk (base + m) ≠ LE4"
and pad0: "∀j ≥ k_tm M. mt_tape c0 j (mt_pos c0 j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, block_width (Γ_tm M), buf, dvec, posk)"
shows "∃c'. (c0, c') ∈ (mttm_step (alphabet_reduce_delta M))
^^ (block_width (Γ_tm M) - 1)
∧ mt_state c' = (q, AR_SimWrite, tk,
block_width (Γ_tm M) + (block_width (Γ_tm M) - 1),
buf, dvec, posk)
∧ mt_pos c' tk = base + (block_width (Γ_tm M) - 1)
∧ mt_tape c' tk = (λpos.
if base ≤ pos ∧ pos < base + (block_width (Γ_tm M) - 1)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c0 tk pos)
∧ (∀k'. k' ≠ tk ⟶ mt_tape c' k' = mt_tape c0 k')
∧ (∀k'. k' ≠ tk ⟶ mt_pos c' k' = mt_pos c0 k')"
by (rule ar_write_fwd_loop_gen
[OF ar_write_bit_step vM qQ kge2 poskproper stg buf_valid pos_base notLE
pad0 src0])
text ‹The proper-cell single-tape write prefix: the part of a
proper-cell single-tape write shared by the non-last
(‹boundary›) and last (‹finish›) variants. From an
‹AR_SimWrite› stage at bit-counter ‹0› with the head at
the block end ‹base + b› and ‹buf tk› a proper symbol,
it fires the back-walk loop (‹ar_write_back_loop›, head to
‹base›) and the forward bit-write loop
(‹ar_write_fwd_loop›, writing the first ‹b - 1›
cells), reaching bit-counter ‹b + (b - 1)› with the head at
‹base + (b - 1)›. The remaining last-cell step (boundary or
finish) is added by the consumer. The two segment costs compose by
‹relpow_add› on ‹relcompI› (chain length ‹b + (b
- 1)›). The ‹notLE› hypothesis (every block cell and the
next-block lead cell ‹≠ LE4›) feeds both loops.›
text ‹Relation-generic write proper-prefix scaffold. The two
loop helpers (back, forward) are the ‹leaf_back› and
‹leaf_fwd› hypotheses; the union- and sub-relation prefixes
are thin instantiations.›
lemma ar_write_proper_prefix_gen:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
and R' :: "(sym4, 'q × 'a ar_stage) mt_config rel"
assumes leaf_back:
"⋀cc. ⟦ valid_mttm M; q ∈ Q_tm M; 2 ≤ block_width (Γ_tm M);
posk tk ≠ AR_AtLE;
mt_state cc = (q, AR_SimWrite, tk, 0, buf, dvec, posk);
∀k. buf k ∈ Γ_tm M ∪ {bl_tm M};
mt_pos cc tk = base + block_width (Γ_tm M);
⋀m. ⟦ 1 ≤ m; m ≤ block_width (Γ_tm M) ⟧
⟹ mt_tape cc tk (base + m) ≠ LE4;
∀j ≥ k_tm M. mt_tape cc j (mt_pos cc j) = BLANK4;
ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk) ⟧
⟹ ∃c1. (cc, c1) ∈ R' ^^ block_width (Γ_tm M)
∧ mt_state c1 = (q, AR_SimWrite, tk, block_width (Γ_tm M),
buf, dvec, posk)
∧ mt_pos c1 tk = base
∧ mt_tape c1 = mt_tape cc
∧ (∀k'. k' ≠ tk ⟶ mt_pos c1 k' = mt_pos cc k')"
and leaf_fwd:
"⋀cc. ⟦ valid_mttm M; q ∈ Q_tm M; 2 ≤ block_width (Γ_tm M);
posk tk ≠ AR_AtLE;
mt_state cc = (q, AR_SimWrite, tk, block_width (Γ_tm M), buf, dvec, posk);
∀k. buf k ∈ Γ_tm M ∪ {bl_tm M};
mt_pos cc tk = base;
⋀m. m < block_width (Γ_tm M) ⟹ mt_tape cc tk (base + m) ≠ LE4;
∀j ≥ k_tm M. mt_tape cc j (mt_pos cc j) = BLANK4;
ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, block_width (Γ_tm M), buf, dvec, posk) ⟧
⟹ ∃c2. (cc, c2) ∈ R' ^^ (block_width (Γ_tm M) - 1)
∧ mt_state c2 = (q, AR_SimWrite, tk,
block_width (Γ_tm M) + (block_width (Γ_tm M) - 1), buf, dvec, posk)
∧ mt_pos c2 tk = base + (block_width (Γ_tm M) - 1)
∧ mt_tape c2 tk = (λpos.
if base ≤ pos ∧ pos < base + (block_width (Γ_tm M) - 1)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape cc tk pos)
∧ (∀k'. k' ≠ tk ⟶ mt_tape c2 k' = mt_tape cc k')
∧ (∀k'. k' ≠ tk ⟶ mt_pos c2 k' = mt_pos cc k')"
and vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and poskproper: "posk tk ≠ AR_AtLE"
and stg: "mt_state c' = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pos_base: "mt_pos c' tk = base + block_width (Γ_tm M)"
and notLE: "⋀m. m ≤ block_width (Γ_tm M)
⟹ mt_tape c' tk (base + m) ≠ LE4"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c2. (c', c2) ∈ R' ^^ (block_width (Γ_tm M) + (block_width (Γ_tm M) - 1))
∧ mt_state c2 = (q, AR_SimWrite, tk,
block_width (Γ_tm M) + (block_width (Γ_tm M) - 1),
buf, dvec, posk)
∧ mt_tape c2 = (mt_tape c')(tk := (λpos.
if base ≤ pos ∧ pos < base + (block_width (Γ_tm M) - 1)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c' tk pos))
∧ mt_pos c2 = (mt_pos c')(tk := base + (block_width (Γ_tm M) - 1))"
proof -
let ?k = "block_width (Γ_tm M)"
let ?R = R'
have notLE_back: "⋀m. ⟦ 1 ≤ m; m ≤ ?k ⟧
⟹ mt_tape c' tk (base + m) ≠ LE4"
using notLE by blast
obtain c1 where
ch1: "(c', c1) ∈ ?R ^^ ?k"
and st1: "mt_state c1 = (q, AR_SimWrite, tk, ?k, buf, dvec, posk)"
and pos1: "mt_pos c1 tk = base"
and tape1: "mt_tape c1 = mt_tape c'"
and opos1: "∀k'. k' ≠ tk ⟶ mt_pos c1 k' = mt_pos c' k'"
using leaf_back[OF vM qQ kge2 poskproper stg buf_valid pos_base notLE_back
pad0 src0]
by blast
have notLE_fwd: "⋀m. m < ?k ⟹ mt_tape c1 tk (base + m) ≠ LE4"
proof -
fix m :: nat assume mlt: "m < ?k"
have mle: "m ≤ ?k" using mlt by simp
show "mt_tape c1 tk (base + m) ≠ LE4"
using notLE[OF mle] tape1 by simp
qed
have tk_lt: "tk < k_tm M" using src0 by (simp add: ar_stage_bounded_def)
have pad_c1: "∀j ≥ k_tm M. mt_tape c1 j (mt_pos c1 j) = BLANK4"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have jne: "j ≠ tk" using jge tk_lt by simp
have "mt_tape c1 j (mt_pos c1 j) = mt_tape c' j (mt_pos c' j)"
using tape1 opos1 jne by simp
thus "mt_tape c1 j (mt_pos c1 j) = BLANK4" using pad0 jge by simp
qed
have src_c1: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, block_width (Γ_tm M), buf, dvec, posk)"
using src0 by (simp add: ar_stage_bounded_def)
obtain c2 where
ch2: "(c1, c2) ∈ ?R ^^ (?k - 1)"
and st2: "mt_state c2 = (q, AR_SimWrite, tk, ?k + (?k - 1), buf, dvec, posk)"
and pos2: "mt_pos c2 tk = base + (?k - 1)"
and tape2: "mt_tape c2 tk = (λpos.
if base ≤ pos ∧ pos < base + (?k - 1)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c1 tk pos)"
and otape2: "∀k'. k' ≠ tk ⟶ mt_tape c2 k' = mt_tape c1 k'"
and opos2: "∀k'. k' ≠ tk ⟶ mt_pos c2 k' = mt_pos c1 k'"
using leaf_fwd[OF vM qQ kge2 poskproper st1 buf_valid pos1 notLE_fwd
pad_c1 src_c1]
by blast
have ch12: "(c', c2) ∈ ?R ^^ (?k + (?k - 1))"
proof -
have "(c', c2) ∈ ?R ^^ ?k O ?R ^^ (?k - 1)" using ch1 ch2 by (rule relcompI)
thus ?thesis by (simp add: relpow_add)
qed
have tape_final: "mt_tape c2 = (mt_tape c')(tk := (λpos.
if base ≤ pos ∧ pos < base + (?k - 1)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c' tk pos))"
proof (rule ext)
fix k'
show "mt_tape c2 k' = ((mt_tape c')(tk := (λpos.
if base ≤ pos ∧ pos < base + (?k - 1)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c' tk pos))) k'"
proof (cases "k' = tk")
case True
have "mt_tape c2 tk = (λpos.
if base ≤ pos ∧ pos < base + (?k - 1)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c' tk pos)"
proof (rule ext)
fix pos
show "mt_tape c2 tk pos = (if base ≤ pos ∧ pos < base + (?k - 1)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c' tk pos)"
using tape2 tape1 by simp
qed
thus ?thesis using True by simp
next
case False
have "mt_tape c2 k' = mt_tape c1 k'" using otape2 False by simp
also have "… = mt_tape c' k'" using tape1 by simp
finally show ?thesis using False by simp
qed
qed
have pos_final: "mt_pos c2 = (mt_pos c')(tk := base + (?k - 1))"
proof (rule ext)
fix k'
show "mt_pos c2 k' = ((mt_pos c')(tk := base + (?k - 1))) k'"
proof (cases "k' = tk")
case True thus ?thesis using pos2 by simp
next
case False
have "mt_pos c2 k' = mt_pos c1 k'" using opos2 False by simp
also have "… = mt_pos c' k'" using opos1 False by simp
finally show ?thesis using False by simp
qed
qed
show ?thesis
proof (intro exI[where x = c2] conjI)
show "(c', c2) ∈ ?R ^^ (?k + (?k - 1))" by (rule ch12)
show "mt_state c2 = (q, AR_SimWrite, tk, ?k + (?k - 1), buf, dvec, posk)"
by (rule st2)
show "mt_tape c2 = (mt_tape c')(tk := (λpos.
if base ≤ pos ∧ pos < base + (?k - 1)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c' tk pos))"
by (rule tape_final)
show "mt_pos c2 = (mt_pos c')(tk := base + (?k - 1))" by (rule pos_final)
qed
qed
lemma ar_write_proper_prefix:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and poskproper: "posk tk ≠ AR_AtLE"
and stg: "mt_state c' = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pos_base: "mt_pos c' tk = base + block_width (Γ_tm M)"
and notLE: "⋀m. m ≤ block_width (Γ_tm M)
⟹ mt_tape c' tk (base + m) ≠ LE4"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c2. (c', c2) ∈ (mttm_step (alphabet_reduce_delta M))
^^ (block_width (Γ_tm M) + (block_width (Γ_tm M) - 1))
∧ mt_state c2 = (q, AR_SimWrite, tk,
block_width (Γ_tm M) + (block_width (Γ_tm M) - 1),
buf, dvec, posk)
∧ mt_tape c2 = (mt_tape c')(tk := (λpos.
if base ≤ pos ∧ pos < base + (block_width (Γ_tm M) - 1)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c' tk pos))
∧ mt_pos c2 = (mt_pos c')(tk := base + (block_width (Γ_tm M) - 1))"
by (rule ar_write_proper_prefix_gen
[OF ar_write_back_loop ar_write_fwd_loop
vM qQ kge2 poskproper stg buf_valid pos_base notLE pad0 src0])
text ‹Extend a written block prefix by its last cell. Both
proper-write finishers reach a tape whose first ‹b - 1› block
cells already hold the new ‹write_bit› image; the boundary /
finish step writes the last cell ‹base + (b - 1)›. This
‹fun_upd› closes the gap: updating the ‹b - 1›-prefix
function at ‹base + (b - 1)› with ‹f (b - 1)› yields
the full ‹b›-cell write. Pure list/function arithmetic, shared
by ‹ar_write_proper_step› and
‹ar_write_proper_finish_step›.›
lemma write_block_extend:
fixes k base :: nat and f g :: "nat ⇒ sym4"
assumes "0 < k"
shows "((λpos. if base ≤ pos ∧ pos < base + (k - 1)
then f (pos - base) else g pos)
(base + (k - 1) := f (k - 1)))
= (λpos. if base ≤ pos ∧ pos < base + k
then f (pos - base) else g pos)"
proof -
obtain kk where k: "k = Suc kk" using assms by (cases k) auto
show ?thesis
proof (rule ext)
fix pos
show "((λpos. if base ≤ pos ∧ pos < base + (k - 1)
then f (pos - base) else g pos)
(base + (k - 1) := f (k - 1))) pos
= (if base ≤ pos ∧ pos < base + k then f (pos - base) else g pos)"
proof (cases "pos = base + (k - 1)")
case True
thus ?thesis using k by simp
next
case False
thus ?thesis using k by (auto simp: less_Suc_eq)
qed
qed
qed
text ‹The proper-cell single-tape write, non-last tape: the prefix
followed by the bit-boundary step (‹ar_write_bit_boundary_step›),
writing the last block cell ‹base + (b - 1)› and landing at the
next tape's ‹AR_SimWrite› (‹k_succ tk›, counter
‹0›). After the ‹2b›-step walk the ‹b›-cell
block at ‹base› spells out ‹write_bit (buf tk)› (the
encoded new symbol), every other cell unchanged, and the head returns
to the block end ‹base + b›. Chain length ‹2b›.›
text ‹Relation-generic write proper-step scaffold. The prefix
walk and the closing bit-boundary step are the ‹leaf_prefix›
and ‹leaf_boundary› hypotheses; union and sub versions are
thin instantiations.›
lemma ar_write_proper_step_gen:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
and R' :: "(sym4, 'q × 'a ar_stage) mt_config rel"
assumes leaf_prefix:
"⋀cc. ⟦ valid_mttm M; q ∈ Q_tm M; 2 ≤ block_width (Γ_tm M);
posk tk ≠ AR_AtLE;
mt_state cc = (q, AR_SimWrite, tk, 0, buf, dvec, posk);
∀k. buf k ∈ Γ_tm M ∪ {bl_tm M};
mt_pos cc tk = base + block_width (Γ_tm M);
⋀m. m ≤ block_width (Γ_tm M)
⟹ mt_tape cc tk (base + m) ≠ LE4;
∀j ≥ k_tm M. mt_tape cc j (mt_pos cc j) = BLANK4;
ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk) ⟧
⟹ ∃c2. (cc, c2) ∈ R' ^^ (block_width (Γ_tm M) + (block_width (Γ_tm M) - 1))
∧ mt_state c2 = (q, AR_SimWrite, tk,
block_width (Γ_tm M) + (block_width (Γ_tm M) - 1), buf, dvec, posk)
∧ mt_tape c2 = (mt_tape cc)(tk := (λpos.
if base ≤ pos ∧ pos < base + (block_width (Γ_tm M) - 1)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape cc tk pos))
∧ mt_pos c2 = (mt_pos cc)(tk := base + (block_width (Γ_tm M) - 1))"
and leaf_boundary:
"⋀cc i. ⟦ valid_mttm M;
mt_state cc = (q, AR_SimWrite, tk, i, buf, dvec, posk);
q ∈ Q_tm M;
posk tk ≠ AR_AtLE;
mt_tape cc tk (mt_pos cc tk) ≠ LE4;
¬ is_last_k M tk;
Suc i = 2 * block_width (Γ_tm M);
ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk);
∀j ≥ k_tm M. mt_tape cc j (mt_pos cc j) = BLANK4;
ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk) ⟧
⟹ ∃c''. (cc, c'') ∈ R'
∧ mt_state c'' = (q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)
∧ mt_tape c'' = (mt_tape cc)(tk :=
(mt_tape cc tk)(mt_pos cc tk :=
write_bit (Γ_tm M) (bl_tm M) (buf tk)
(i - block_width (Γ_tm M))))
∧ mt_pos c'' = (mt_pos cc)(tk := Suc (mt_pos cc tk))"
and vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and notlast: "¬ is_last_k M tk"
and poskproper: "posk tk ≠ AR_AtLE"
and stg: "mt_state c' = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pos_base: "mt_pos c' tk = base + block_width (Γ_tm M)"
and notLE: "⋀m. m ≤ block_width (Γ_tm M)
⟹ mt_tape c' tk (base + m) ≠ LE4"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ R' ^^ (2 * block_width (Γ_tm M))
∧ mt_state c'' = (q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)
∧ mt_tape c'' = (mt_tape c')(tk := (λpos.
if base ≤ pos ∧ pos < base + block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c' tk pos))
∧ mt_pos c'' = (mt_pos c')(tk := base + block_width (Γ_tm M))"
proof -
let ?k = "block_width (Γ_tm M)"
let ?R = R'
let ?wb = "λm. write_bit (Γ_tm M) (bl_tm M) (buf tk) m"
let ?part = "λpos. if base ≤ pos ∧ pos < base + (?k - 1)
then ?wb (pos - base) else mt_tape c' tk pos"
let ?full = "λpos. if base ≤ pos ∧ pos < base + ?k
then ?wb (pos - base) else mt_tape c' tk pos"
have kpos: "0 < ?k" using kge2 by simp
obtain kk where kdef: "?k = Suc kk" using kge2 by (cases ?k) auto
obtain c2 where
ch_pre: "(c', c2) ∈ ?R ^^ (?k + (?k - 1))"
and st2: "mt_state c2 = (q, AR_SimWrite, tk, ?k + (?k - 1), buf, dvec, posk)"
and tape2: "mt_tape c2 = (mt_tape c')(tk := ?part)"
and pos2: "mt_pos c2 = (mt_pos c')(tk := base + (?k - 1))"
using leaf_prefix[OF vM qQ kge2 poskproper stg buf_valid pos_base notLE
pad0 src0]
by blast
have c2tk: "mt_tape c2 tk = ?part" using tape2 by simp
have pos2_tk: "mt_pos c2 tk = base + (?k - 1)" using pos2 by simp
have ihi: "Suc (?k + (?k - 1)) = 2 * ?k" using kdef by simp
have lt2: "?k + (?k - 1) < 2 * ?k" using kdef by simp
have vsrc2: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, ?k + (?k - 1), buf, dvec, posk)"
using lt2 buf_valid by (simp add: ar_valid_stage_def)
have cell_cur: "mt_tape c2 tk (mt_pos c2 tk) = mt_tape c' tk (base + (?k - 1))"
proof -
have "mt_tape c2 tk (base + (?k - 1)) = mt_tape c' tk (base + (?k - 1))"
using c2tk by simp
thus ?thesis using pos2_tk by simp
qed
have km1le: "?k - 1 ≤ ?k" by simp
have notLE2: "mt_tape c2 tk (mt_pos c2 tk) ≠ LE4"
using cell_cur notLE[OF km1le] by simp
have tk_lt: "tk < k_tm M" using src0 by (simp add: ar_stage_bounded_def)
have pad_c2: "∀j ≥ k_tm M. mt_tape c2 j (mt_pos c2 j) = BLANK4"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have jne: "j ≠ tk" using jge tk_lt by simp
have "mt_tape c2 j (mt_pos c2 j) = mt_tape c' j (mt_pos c' j)"
using tape2 pos2 jne by simp
thus "mt_tape c2 j (mt_pos c2 j) = BLANK4" using pad0 jge by simp
qed
have src_c2: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, block_width (Γ_tm M) + (block_width (Γ_tm M) - 1),
buf, dvec, posk)"
using src0 by (simp add: ar_stage_bounded_def)
obtain c3 where
s3: "(c2, c3) ∈ ?R"
and st3: "mt_state c3 = (q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)"
and tape3: "mt_tape c3 = (mt_tape c2)(tk :=
(mt_tape c2 tk)(mt_pos c2 tk := ?wb (?k + (?k - 1) - ?k)))"
and pos3: "mt_pos c3 = (mt_pos c2)(tk := Suc (mt_pos c2 tk))"
using leaf_boundary[OF vM st2 qQ poskproper notLE2 notlast ihi vsrc2
pad_c2 src_c2]
by blast
have ch_full: "(c', c3) ∈ ?R ^^ (2 * ?k)"
proof -
have h: "(c', c3) ∈ ?R ^^ Suc (?k + (?k - 1))"
by (rule relpow_Suc_I[OF ch_pre s3])
from h show ?thesis by (simp only: ihi)
qed
have tape3_tk: "mt_tape c3 tk = (?part(base + (?k - 1) := ?wb (?k - 1)))"
using tape3 pos2_tk c2tk by simp
have tape3_tk_full: "mt_tape c3 tk = ?full"
using tape3_tk write_block_extend[OF kpos, of base ?wb "mt_tape c' tk"] by simp
have tape_final: "mt_tape c3 = (mt_tape c')(tk := ?full)"
proof (rule ext)
fix k'
show "mt_tape c3 k' = ((mt_tape c')(tk := ?full)) k'"
proof (cases "k' = tk")
case True thus ?thesis using tape3_tk_full by simp
next
case False
have "mt_tape c3 k' = mt_tape c2 k'" using tape3 False by simp
also have "… = mt_tape c' k'" using tape2 False by simp
finally show ?thesis using False by simp
qed
qed
have pos_final: "mt_pos c3 = (mt_pos c')(tk := base + ?k)"
proof -
have "mt_pos c3 = (mt_pos c2)(tk := Suc (mt_pos c2 tk))" by (rule pos3)
also have "… = (mt_pos c2)(tk := base + ?k)" using pos2_tk kdef by simp
also have "… = (mt_pos c')(tk := base + ?k)" using pos2 by simp
finally show ?thesis .
qed
show ?thesis
proof (intro exI[where x = c3] conjI)
show "(c', c3) ∈ R' ^^ (2 * ?k)"
by (rule ch_full)
show "mt_state c3 = (q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)"
by (rule st3)
show "mt_tape c3 = (mt_tape c')(tk := (λpos.
if base ≤ pos ∧ pos < base + ?k
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c' tk pos))"
by (rule tape_final)
show "mt_pos c3 = (mt_pos c')(tk := base + ?k)" by (rule pos_final)
qed
qed
lemma ar_write_proper_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and notlast: "¬ is_last_k M tk"
and poskproper: "posk tk ≠ AR_AtLE"
and stg: "mt_state c' = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pos_base: "mt_pos c' tk = base + block_width (Γ_tm M)"
and notLE: "⋀m. m ≤ block_width (Γ_tm M)
⟹ mt_tape c' tk (base + m) ≠ LE4"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ (mttm_step (alphabet_reduce_delta M))
^^ (2 * block_width (Γ_tm M))
∧ mt_state c'' = (q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)
∧ mt_tape c'' = (mt_tape c')(tk := (λpos.
if base ≤ pos ∧ pos < base + block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c' tk pos))
∧ mt_pos c'' = (mt_pos c')(tk := base + block_width (Γ_tm M))"
by (rule ar_write_proper_step_gen
[OF ar_write_proper_prefix ar_write_bit_boundary_step
vM qQ kge2 notlast poskproper stg buf_valid pos_base notLE
pad0 src0])
text ‹The proper-cell single-tape write, last tape: as
‹ar_write_proper_step› but ‹tk› is the last tape, so after
the last-cell write (‹ar_write_bit_finish_step›) the phase
transitions to ‹AR_SimAdvance› with the current-tape field reset
to ‹k_unidx 0› (all tapes written). Same ‹b›-cell block
write and head return to ‹base + b›. Chain length ‹2b›.›
text ‹Relation-generic write proper-finish-step scaffold. As
‹ar_write_proper_step_gen› but the closing leaf is the
last-tape finish (transition to ‹AR_SimAdvance›); the prefix
and finish helpers are the ‹leaf_prefix› and
‹leaf_finish› hypotheses.›
lemma ar_write_proper_finish_step_gen:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
and R' :: "(sym4, 'q × 'a ar_stage) mt_config rel"
assumes leaf_prefix:
"⋀cc. ⟦ valid_mttm M; q ∈ Q_tm M; 2 ≤ block_width (Γ_tm M);
posk tk ≠ AR_AtLE;
mt_state cc = (q, AR_SimWrite, tk, 0, buf, dvec, posk);
∀k. buf k ∈ Γ_tm M ∪ {bl_tm M};
mt_pos cc tk = base + block_width (Γ_tm M);
⋀m. m ≤ block_width (Γ_tm M)
⟹ mt_tape cc tk (base + m) ≠ LE4;
∀j ≥ k_tm M. mt_tape cc j (mt_pos cc j) = BLANK4;
ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk) ⟧
⟹ ∃c2. (cc, c2) ∈ R' ^^ (block_width (Γ_tm M) + (block_width (Γ_tm M) - 1))
∧ mt_state c2 = (q, AR_SimWrite, tk,
block_width (Γ_tm M) + (block_width (Γ_tm M) - 1), buf, dvec, posk)
∧ mt_tape c2 = (mt_tape cc)(tk := (λpos.
if base ≤ pos ∧ pos < base + (block_width (Γ_tm M) - 1)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape cc tk pos))
∧ mt_pos c2 = (mt_pos cc)(tk := base + (block_width (Γ_tm M) - 1))"
and leaf_finish:
"⋀cc i. ⟦ valid_mttm M;
mt_state cc = (q, AR_SimWrite, tk, i, buf, dvec, posk);
q ∈ Q_tm M;
posk tk ≠ AR_AtLE;
mt_tape cc tk (mt_pos cc tk) ≠ LE4;
is_last_k M tk;
Suc i = 2 * block_width (Γ_tm M);
ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk);
∀j ≥ k_tm M. mt_tape cc j (mt_pos cc j) = BLANK4;
ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk) ⟧
⟹ ∃c''. (cc, c'') ∈ R'
∧ mt_state c'' = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)
∧ mt_tape c'' = (mt_tape cc)(tk :=
(mt_tape cc tk)(mt_pos cc tk :=
write_bit (Γ_tm M) (bl_tm M) (buf tk)
(i - block_width (Γ_tm M))))
∧ mt_pos c'' = (mt_pos cc)(tk := Suc (mt_pos cc tk))"
and vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and last: "is_last_k M tk"
and poskproper: "posk tk ≠ AR_AtLE"
and stg: "mt_state c' = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pos_base: "mt_pos c' tk = base + block_width (Γ_tm M)"
and notLE: "⋀m. m ≤ block_width (Γ_tm M)
⟹ mt_tape c' tk (base + m) ≠ LE4"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ R' ^^ (2 * block_width (Γ_tm M))
∧ mt_state c'' = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)
∧ mt_tape c'' = (mt_tape c')(tk := (λpos.
if base ≤ pos ∧ pos < base + block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c' tk pos))
∧ mt_pos c'' = (mt_pos c')(tk := base + block_width (Γ_tm M))"
proof -
let ?k = "block_width (Γ_tm M)"
let ?R = R'
let ?wb = "λm. write_bit (Γ_tm M) (bl_tm M) (buf tk) m"
let ?part = "λpos. if base ≤ pos ∧ pos < base + (?k - 1)
then ?wb (pos - base) else mt_tape c' tk pos"
let ?full = "λpos. if base ≤ pos ∧ pos < base + ?k
then ?wb (pos - base) else mt_tape c' tk pos"
have kpos: "0 < ?k" using kge2 by simp
obtain kk where kdef: "?k = Suc kk" using kge2 by (cases ?k) auto
obtain c2 where
ch_pre: "(c', c2) ∈ ?R ^^ (?k + (?k - 1))"
and st2: "mt_state c2 = (q, AR_SimWrite, tk, ?k + (?k - 1), buf, dvec, posk)"
and tape2: "mt_tape c2 = (mt_tape c')(tk := ?part)"
and pos2: "mt_pos c2 = (mt_pos c')(tk := base + (?k - 1))"
using leaf_prefix[OF vM qQ kge2 poskproper stg buf_valid pos_base notLE
pad0 src0]
by blast
have c2tk: "mt_tape c2 tk = ?part" using tape2 by simp
have pos2_tk: "mt_pos c2 tk = base + (?k - 1)" using pos2 by simp
have ihi: "Suc (?k + (?k - 1)) = 2 * ?k" using kdef by simp
have lt2: "?k + (?k - 1) < 2 * ?k" using kdef by simp
have vsrc2: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, ?k + (?k - 1), buf, dvec, posk)"
using lt2 buf_valid by (simp add: ar_valid_stage_def)
have cell_cur: "mt_tape c2 tk (mt_pos c2 tk) = mt_tape c' tk (base + (?k - 1))"
proof -
have "mt_tape c2 tk (base + (?k - 1)) = mt_tape c' tk (base + (?k - 1))"
using c2tk by simp
thus ?thesis using pos2_tk by simp
qed
have km1le: "?k - 1 ≤ ?k" by simp
have notLE2: "mt_tape c2 tk (mt_pos c2 tk) ≠ LE4"
using cell_cur notLE[OF km1le] by simp
have tk_lt: "tk < k_tm M" using src0 by (simp add: ar_stage_bounded_def)
have pad_c2: "∀j ≥ k_tm M. mt_tape c2 j (mt_pos c2 j) = BLANK4"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have jne: "j ≠ tk" using jge tk_lt by simp
have "mt_tape c2 j (mt_pos c2 j) = mt_tape c' j (mt_pos c' j)"
using tape2 pos2 jne by simp
thus "mt_tape c2 j (mt_pos c2 j) = BLANK4" using pad0 jge by simp
qed
have src_c2: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, block_width (Γ_tm M) + (block_width (Γ_tm M) - 1),
buf, dvec, posk)"
using src0 by (simp add: ar_stage_bounded_def)
obtain c3 where
s3: "(c2, c3) ∈ ?R"
and st3: "mt_state c3 = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)"
and tape3: "mt_tape c3 = (mt_tape c2)(tk :=
(mt_tape c2 tk)(mt_pos c2 tk := ?wb (?k + (?k - 1) - ?k)))"
and pos3: "mt_pos c3 = (mt_pos c2)(tk := Suc (mt_pos c2 tk))"
using leaf_finish[OF vM st2 qQ poskproper notLE2 last ihi vsrc2
pad_c2 src_c2]
by blast
have ch_full: "(c', c3) ∈ ?R ^^ (2 * ?k)"
proof -
have h: "(c', c3) ∈ ?R ^^ Suc (?k + (?k - 1))"
by (rule relpow_Suc_I[OF ch_pre s3])
from h show ?thesis by (simp only: ihi)
qed
have tape3_tk: "mt_tape c3 tk = (?part(base + (?k - 1) := ?wb (?k - 1)))"
using tape3 pos2_tk c2tk by simp
have tape3_tk_full: "mt_tape c3 tk = ?full"
using tape3_tk write_block_extend[OF kpos, of base ?wb "mt_tape c' tk"] by simp
have tape_final: "mt_tape c3 = (mt_tape c')(tk := ?full)"
proof (rule ext)
fix k'
show "mt_tape c3 k' = ((mt_tape c')(tk := ?full)) k'"
proof (cases "k' = tk")
case True thus ?thesis using tape3_tk_full by simp
next
case False
have "mt_tape c3 k' = mt_tape c2 k'" using tape3 False by simp
also have "… = mt_tape c' k'" using tape2 False by simp
finally show ?thesis using False by simp
qed
qed
have pos_final: "mt_pos c3 = (mt_pos c')(tk := base + ?k)"
proof -
have "mt_pos c3 = (mt_pos c2)(tk := Suc (mt_pos c2 tk))" by (rule pos3)
also have "… = (mt_pos c2)(tk := base + ?k)" using pos2_tk kdef by simp
also have "… = (mt_pos c')(tk := base + ?k)" using pos2 by simp
finally show ?thesis .
qed
show ?thesis
proof (intro exI[where x = c3] conjI)
show "(c', c3) ∈ R' ^^ (2 * ?k)"
by (rule ch_full)
show "mt_state c3 = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)"
by (rule st3)
show "mt_tape c3 = (mt_tape c')(tk := (λpos.
if base ≤ pos ∧ pos < base + ?k
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c' tk pos))"
by (rule tape_final)
show "mt_pos c3 = (mt_pos c')(tk := base + ?k)" by (rule pos_final)
qed
qed
lemma ar_write_proper_finish_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and last: "is_last_k M tk"
and poskproper: "posk tk ≠ AR_AtLE"
and stg: "mt_state c' = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pos_base: "mt_pos c' tk = base + block_width (Γ_tm M)"
and notLE: "⋀m. m ≤ block_width (Γ_tm M)
⟹ mt_tape c' tk (base + m) ≠ LE4"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ (mttm_step (alphabet_reduce_delta M))
^^ (2 * block_width (Γ_tm M))
∧ mt_state c'' = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)
∧ mt_tape c'' = (mt_tape c')(tk := (λpos.
if base ≤ pos ∧ pos < base + block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base)
else mt_tape c' tk pos))
∧ mt_pos c'' = (mt_pos c')(tk := base + block_width (Γ_tm M))"
by (rule ar_write_proper_finish_step_gen
[OF ar_write_proper_prefix ar_write_bit_finish_step
vM qQ kge2 last poskproper stg buf_valid pos_base notLE
pad0 src0])
text ‹The unified single-tape write, non-last tape: the LE/proper
dispatch, the AR analogue of ‹ar_read_tape_step›. From an
‹AR_SimWrite› stage at bit-counter ‹0›, dispatch on
‹posk tk = AR_AtLE› (which the caller pins to ‹p = 0›,
‹M›'s head on the marker): the LE arm
(‹ar_write_le_step›, ‹1› step) leaves the tape and head
untouched and hands off; the proper arm (‹ar_write_proper_step›,
‹2b› steps) overwrites the ‹b›-cell block at ‹sim_pos
p› with ‹write_bit (buf tk)›. In ∗‹both›
arms every head is unchanged (the LE arm is all-‹N›; the proper
arm back-walks then returns to the block end), so the conclusion is
‹mt_pos c'' = mt_pos c'› uniformly. The proper-arm
‹≠ LE4› facts come from the input correspondence
‹tcorr› (block-‹p› cells and the block-‹(p+1)›
lead cell, all ‹cell_repr› cells via
‹cell_repr_nth_not_LE4›).›
text ‹Relation-generic write single-tape step scaffold (non-last).
The two cases (‹p = 0› le-step, ‹p ≠ 0› proper-step)
are the ‹leaf_le› and ‹leaf_proper› hypotheses; union and
sub versions are thin instantiations.›
lemma ar_write_tape_step_gen:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
and tM :: "nat ⇒ 'a"
and R' :: "(sym4, 'q × 'a ar_stage) mt_config rel"
assumes leaf_le:
"⋀cc. ⟦ valid_mttm M;
mt_state cc = (q, AR_SimWrite, tk, 0, buf, dvec, posk);
q ∈ Q_tm M;
posk tk = AR_AtLE;
¬ is_last_k M tk;
ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk);
∀j ≥ k_tm M. mt_tape cc j (mt_pos cc j) = BLANK4;
ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk) ⟧
⟹ ∃c''. (cc, c'') ∈ R'
∧ mt_state c'' = (q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)
∧ mt_tape c'' = mt_tape cc
∧ mt_pos c'' = mt_pos cc"
and leaf_proper:
"⋀cc base'. ⟦ valid_mttm M; q ∈ Q_tm M; 2 ≤ block_width (Γ_tm M);
¬ is_last_k M tk;
posk tk ≠ AR_AtLE;
mt_state cc = (q, AR_SimWrite, tk, 0, buf, dvec, posk);
∀k. buf k ∈ Γ_tm M ∪ {bl_tm M};
mt_pos cc tk = base' + block_width (Γ_tm M);
⋀m. m ≤ block_width (Γ_tm M)
⟹ mt_tape cc tk (base' + m) ≠ LE4;
∀j ≥ k_tm M. mt_tape cc j (mt_pos cc j) = BLANK4;
ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk) ⟧
⟹ ∃c''. (cc, c'') ∈ R' ^^ (2 * block_width (Γ_tm M))
∧ mt_state c'' = (q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)
∧ mt_tape c'' = (mt_tape cc)(tk := (λpos.
if base' ≤ pos ∧ pos < base' + block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base')
else mt_tape cc tk pos))
∧ mt_pos c'' = (mt_pos cc)(tk := base' + block_width (Γ_tm M))"
and vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and notlast: "¬ is_last_k M tk"
and stg: "mt_state c' = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and tcorr: "ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
tM (mt_tape c' tk)"
and ppos: "mt_pos c' tk = (if p = 0 then Suc 0
else sim_pos (block_width (Γ_tm M)) p + block_width (Γ_tm M))"
and poskle: "posk tk = AR_AtLE ⟷ p = 0"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ R' ^^ (if p = 0 then 1 else 2 * block_width (Γ_tm M))
∧ mt_state c'' = (q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)
∧ mt_tape c'' = (if p = 0 then mt_tape c'
else (mt_tape c')(tk := (λpos.
if sim_pos (block_width (Γ_tm M)) p ≤ pos
∧ pos < sim_pos (block_width (Γ_tm M)) p + block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf tk)
(pos - sim_pos (block_width (Γ_tm M)) p)
else mt_tape c' tk pos)))
∧ mt_pos c'' = mt_pos c'"
proof -
let ?k = "block_width (Γ_tm M)"
let ?R = R'
have kpos: "0 < ?k" using kge2 by simp
show ?thesis
proof (cases "p = 0")
case True
have poskLE: "posk tk = AR_AtLE" using poskle True by simp
obtain c'' where
step: "(c', c'') ∈ ?R"
and st: "mt_state c'' = (q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)"
and tp: "mt_tape c'' = mt_tape c'"
and ps: "mt_pos c'' = mt_pos c'"
using leaf_le[OF vM stg qQ poskLE notlast vsrc pad0 src0] by blast
show ?thesis
proof (intro exI[where x = c''] conjI)
show "(c', c'') ∈ ?R ^^ (if p = 0 then 1 else 2 * ?k)"
using step True by simp
show "mt_state c'' = (q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)"
by (rule st)
show "mt_tape c'' = (if p = 0 then mt_tape c'
else (mt_tape c')(tk := (λpos.
if sim_pos ?k p ≤ pos ∧ pos < sim_pos ?k p + ?k
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - sim_pos ?k p)
else mt_tape c' tk pos)))"
using tp True by simp
show "mt_pos c'' = mt_pos c'" by (rule ps)
qed
next
case False
hence pge1: "1 ≤ p" by simp
have poskproper: "posk tk ≠ AR_AtLE" using poskle False by simp
let ?base = "sim_pos ?k p"
have pos_base: "mt_pos c' tk = ?base + ?k" using ppos False by simp
have notLE: "⋀m. m ≤ ?k ⟹ mt_tape c' tk (?base + m) ≠ LE4"
proof -
fix m assume mle: "m ≤ ?k"
show "mt_tape c' tk (?base + m) ≠ LE4"
proof (cases "m < ?k")
case True
have "mt_tape c' tk (?base + m)
= cell_repr (Γ_tm M) (bl_tm M) (tM p) ! m"
using tcorr pge1 True unfolding ar_tape_correspondence_def by blast
thus ?thesis using cell_repr_nth_not_LE4[OF True] by simp
next
case False
hence meq: "m = ?k" using mle by simp
obtain pp where pp: "p = Suc pp" using pge1 by (cases p) auto
have psuc1: "1 ≤ Suc p" by simp
have base_succ: "?base + ?k = sim_pos ?k (Suc p)"
using pp by (simp add: sim_pos_def)
have corr_succ: "∀j < ?k. mt_tape c' tk (sim_pos ?k (Suc p) + j)
= cell_repr (Γ_tm M) (bl_tm M) (tM (Suc p)) ! j"
using tcorr psuc1 unfolding ar_tape_correspondence_def by blast
have "mt_tape c' tk (?base + m)
= cell_repr (Γ_tm M) (bl_tm M) (tM (Suc p)) ! 0"
using meq base_succ corr_succ[rule_format, OF kpos] by simp
thus ?thesis using cell_repr_nth_not_LE4[OF kpos] by simp
qed
qed
obtain c'' where
step: "(c', c'') ∈ ?R ^^ (2 * ?k)"
and st: "mt_state c'' = (q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)"
and tp: "mt_tape c'' = (mt_tape c')(tk := (λpos.
if ?base ≤ pos ∧ pos < ?base + ?k
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - ?base)
else mt_tape c' tk pos))"
and ps: "mt_pos c'' = (mt_pos c')(tk := ?base + ?k)"
using leaf_proper[OF vM qQ kge2 notlast poskproper stg buf_valid
pos_base notLE pad0 src0]
by blast
have ps': "mt_pos c'' = mt_pos c'"
proof -
have "(mt_pos c')(tk := ?base + ?k) = mt_pos c'"
using pos_base by (rule fun_upd_idem)
thus ?thesis using ps by simp
qed
show ?thesis
proof (intro exI[where x = c''] conjI)
show "(c', c'') ∈ ?R ^^ (if p = 0 then 1 else 2 * ?k)"
using step False by simp
show "mt_state c'' = (q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)"
by (rule st)
show "mt_tape c'' = (if p = 0 then mt_tape c'
else (mt_tape c')(tk := (λpos.
if sim_pos ?k p ≤ pos ∧ pos < sim_pos ?k p + ?k
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - sim_pos ?k p)
else mt_tape c' tk pos)))"
using tp False by simp
show "mt_pos c'' = mt_pos c'" by (rule ps')
qed
qed
qed
lemma ar_write_tape_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
and tM :: "nat ⇒ 'a"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and notlast: "¬ is_last_k M tk"
and stg: "mt_state c' = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and tcorr: "ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
tM (mt_tape c' tk)"
and ppos: "mt_pos c' tk = (if p = 0 then Suc 0
else sim_pos (block_width (Γ_tm M)) p + block_width (Γ_tm M))"
and poskle: "posk tk = AR_AtLE ⟷ p = 0"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ (mttm_step (alphabet_reduce_delta M))
^^ (if p = 0 then 1 else 2 * block_width (Γ_tm M))
∧ mt_state c'' = (q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)
∧ mt_tape c'' = (if p = 0 then mt_tape c'
else (mt_tape c')(tk := (λpos.
if sim_pos (block_width (Γ_tm M)) p ≤ pos
∧ pos < sim_pos (block_width (Γ_tm M)) p + block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf tk)
(pos - sim_pos (block_width (Γ_tm M)) p)
else mt_tape c' tk pos)))
∧ mt_pos c'' = mt_pos c'"
by (rule ar_write_tape_step_gen
[OF ar_write_le_step ar_write_proper_step
vM qQ kge2 notlast stg tcorr ppos poskle buf_valid vsrc
pad0 src0])
text ‹The unified single-tape write, last tape: as
‹ar_write_tape_step› but ‹tk› is the last tape, so both
arms transition to ‹AR_SimAdvance› (current-tape field reset to
‹k_unidx 0›, all tapes written): the LE arm via
‹ar_write_le_finish_step›, the proper arm via
‹ar_write_proper_finish_step›. Same tape edit and head
invariance.›
text ‹Relation-generic write single-tape finish-step scaffold
(last tape). As ‹ar_write_tape_step_gen› but both cases use
the last-tape finish leaves (transition to ‹AR_SimAdvance›);
the le-finish and proper-finish helpers are the ‹leaf_le› and
‹leaf_proper› hypotheses.›
lemma ar_write_tape_finish_step_gen:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
and tM :: "nat ⇒ 'a"
and R' :: "(sym4, 'q × 'a ar_stage) mt_config rel"
assumes leaf_le:
"⋀cc. ⟦ valid_mttm M;
mt_state cc = (q, AR_SimWrite, tk, 0, buf, dvec, posk);
q ∈ Q_tm M;
posk tk = AR_AtLE;
is_last_k M tk;
ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk);
∀j ≥ k_tm M. mt_tape cc j (mt_pos cc j) = BLANK4;
ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk) ⟧
⟹ ∃c''. (cc, c'') ∈ R'
∧ mt_state c'' = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)
∧ mt_tape c'' = mt_tape cc
∧ mt_pos c'' = mt_pos cc"
and leaf_proper:
"⋀cc base'. ⟦ valid_mttm M; q ∈ Q_tm M; 2 ≤ block_width (Γ_tm M);
is_last_k M tk;
posk tk ≠ AR_AtLE;
mt_state cc = (q, AR_SimWrite, tk, 0, buf, dvec, posk);
∀k. buf k ∈ Γ_tm M ∪ {bl_tm M};
mt_pos cc tk = base' + block_width (Γ_tm M);
⋀m. m ≤ block_width (Γ_tm M)
⟹ mt_tape cc tk (base' + m) ≠ LE4;
∀j ≥ k_tm M. mt_tape cc j (mt_pos cc j) = BLANK4;
ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk) ⟧
⟹ ∃c''. (cc, c'') ∈ R' ^^ (2 * block_width (Γ_tm M))
∧ mt_state c'' = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)
∧ mt_tape c'' = (mt_tape cc)(tk := (λpos.
if base' ≤ pos ∧ pos < base' + block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - base')
else mt_tape cc tk pos))
∧ mt_pos c'' = (mt_pos cc)(tk := base' + block_width (Γ_tm M))"
and vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and last: "is_last_k M tk"
and stg: "mt_state c' = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and tcorr: "ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
tM (mt_tape c' tk)"
and ppos: "mt_pos c' tk = (if p = 0 then Suc 0
else sim_pos (block_width (Γ_tm M)) p + block_width (Γ_tm M))"
and poskle: "posk tk = AR_AtLE ⟷ p = 0"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ R' ^^ (if p = 0 then 1 else 2 * block_width (Γ_tm M))
∧ mt_state c'' = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)
∧ mt_tape c'' = (if p = 0 then mt_tape c'
else (mt_tape c')(tk := (λpos.
if sim_pos (block_width (Γ_tm M)) p ≤ pos
∧ pos < sim_pos (block_width (Γ_tm M)) p + block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf tk)
(pos - sim_pos (block_width (Γ_tm M)) p)
else mt_tape c' tk pos)))
∧ mt_pos c'' = mt_pos c'"
proof -
let ?k = "block_width (Γ_tm M)"
let ?R = R'
have kpos: "0 < ?k" using kge2 by simp
show ?thesis
proof (cases "p = 0")
case True
have poskLE: "posk tk = AR_AtLE" using poskle True by simp
obtain c'' where
step: "(c', c'') ∈ ?R"
and st: "mt_state c'' = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)"
and tp: "mt_tape c'' = mt_tape c'"
and ps: "mt_pos c'' = mt_pos c'"
using leaf_le[OF vM stg qQ poskLE last vsrc pad0 src0] by blast
show ?thesis
proof (intro exI[where x = c''] conjI)
show "(c', c'') ∈ ?R ^^ (if p = 0 then 1 else 2 * ?k)"
using step True by simp
show "mt_state c'' = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)"
by (rule st)
show "mt_tape c'' = (if p = 0 then mt_tape c'
else (mt_tape c')(tk := (λpos.
if sim_pos ?k p ≤ pos ∧ pos < sim_pos ?k p + ?k
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - sim_pos ?k p)
else mt_tape c' tk pos)))"
using tp True by simp
show "mt_pos c'' = mt_pos c'" by (rule ps)
qed
next
case False
hence pge1: "1 ≤ p" by simp
have poskproper: "posk tk ≠ AR_AtLE" using poskle False by simp
let ?base = "sim_pos ?k p"
have pos_base: "mt_pos c' tk = ?base + ?k" using ppos False by simp
have notLE: "⋀m. m ≤ ?k ⟹ mt_tape c' tk (?base + m) ≠ LE4"
proof -
fix m assume mle: "m ≤ ?k"
show "mt_tape c' tk (?base + m) ≠ LE4"
proof (cases "m < ?k")
case True
have "mt_tape c' tk (?base + m)
= cell_repr (Γ_tm M) (bl_tm M) (tM p) ! m"
using tcorr pge1 True unfolding ar_tape_correspondence_def by blast
thus ?thesis using cell_repr_nth_not_LE4[OF True] by simp
next
case False
hence meq: "m = ?k" using mle by simp
obtain pp where pp: "p = Suc pp" using pge1 by (cases p) auto
have psuc1: "1 ≤ Suc p" by simp
have base_succ: "?base + ?k = sim_pos ?k (Suc p)"
using pp by (simp add: sim_pos_def)
have corr_succ: "∀j < ?k. mt_tape c' tk (sim_pos ?k (Suc p) + j)
= cell_repr (Γ_tm M) (bl_tm M) (tM (Suc p)) ! j"
using tcorr psuc1 unfolding ar_tape_correspondence_def by blast
have "mt_tape c' tk (?base + m)
= cell_repr (Γ_tm M) (bl_tm M) (tM (Suc p)) ! 0"
using meq base_succ corr_succ[rule_format, OF kpos] by simp
thus ?thesis using cell_repr_nth_not_LE4[OF kpos] by simp
qed
qed
obtain c'' where
step: "(c', c'') ∈ ?R ^^ (2 * ?k)"
and st: "mt_state c'' = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)"
and tp: "mt_tape c'' = (mt_tape c')(tk := (λpos.
if ?base ≤ pos ∧ pos < ?base + ?k
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - ?base)
else mt_tape c' tk pos))"
and ps: "mt_pos c'' = (mt_pos c')(tk := ?base + ?k)"
using leaf_proper[OF vM qQ kge2 last poskproper stg buf_valid
pos_base notLE pad0 src0]
by blast
have ps': "mt_pos c'' = mt_pos c'"
proof -
have "(mt_pos c')(tk := ?base + ?k) = mt_pos c'"
using pos_base by (rule fun_upd_idem)
thus ?thesis using ps by simp
qed
show ?thesis
proof (intro exI[where x = c''] conjI)
show "(c', c'') ∈ ?R ^^ (if p = 0 then 1 else 2 * ?k)"
using step False by simp
show "mt_state c'' = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)"
by (rule st)
show "mt_tape c'' = (if p = 0 then mt_tape c'
else (mt_tape c')(tk := (λpos.
if sim_pos ?k p ≤ pos ∧ pos < sim_pos ?k p + ?k
then write_bit (Γ_tm M) (bl_tm M) (buf tk) (pos - sim_pos ?k p)
else mt_tape c' tk pos)))"
using tp False by simp
show "mt_pos c'' = mt_pos c'" by (rule ps')
qed
qed
qed
lemma ar_write_tape_finish_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
and tM :: "nat ⇒ 'a"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and last: "is_last_k M tk"
and stg: "mt_state c' = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and tcorr: "ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
tM (mt_tape c' tk)"
and ppos: "mt_pos c' tk = (if p = 0 then Suc 0
else sim_pos (block_width (Γ_tm M)) p + block_width (Γ_tm M))"
and poskle: "posk tk = AR_AtLE ⟷ p = 0"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
and pad0: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ (mttm_step (alphabet_reduce_delta M))
^^ (if p = 0 then 1 else 2 * block_width (Γ_tm M))
∧ mt_state c'' = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)
∧ mt_tape c'' = (if p = 0 then mt_tape c'
else (mt_tape c')(tk := (λpos.
if sim_pos (block_width (Γ_tm M)) p ≤ pos
∧ pos < sim_pos (block_width (Γ_tm M)) p + block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf tk)
(pos - sim_pos (block_width (Γ_tm M)) p)
else mt_tape c' tk pos)))
∧ mt_pos c'' = mt_pos c'"
by (rule ar_write_tape_finish_step_gen
[OF ar_write_le_finish_step ar_write_proper_finish_step
vM qQ kge2 last stg tcorr ppos poskle buf_valid vsrc
pad0 src0])
text ‹The write-phase prefix walk: from the write boundary
(current-tape field ‹k_unidx 0›, bit-counter
‹0›, the head positions the read phase left), iterate the
unified non-last per-tape write ‹ar_write_tape_step› over the
first ‹j› tapes (‹j ≤ k_tm M - 1›, all non-last),
landing back at ‹AR_SimWrite› on tape ‹k_unidx j›.
Dual to ‹ar_read_prefix›: the read kept the tape constant and
varied ‹buf›/‹posk›; the write keeps
‹buf›/‹posk›/positions constant and varies the
∗‹tape›. The descriptor splits on ‹k_idx k <
j›: visited tapes carry their overwritten block
(‹?out›, the ‹write_bit› image for proper tapes, or
the unchanged tape for ‹LE› tapes); the rest are unchanged.
Each per-tape step's ‹tcorr› / position entry facts hold
because the current tape is not yet visited
(‹mt_tape c k_unidx j = mt_tape c0 (k_unidx j)›). Variable
per-tape cost (‹1› or ‹2b›), aggregate bounded by
‹j ⋅ 2b›.›
text ‹Relation-generic write prefix walk scaffold. The single
per-tape helper (‹ar_write_tape_step›) is the ‹leaf›
hypothesis, quantified over the per-tape config, tape index,
tape-content function, and position; union and sub versions are
thin instantiations.›
lemma ar_write_prefix_gen:
fixes M :: "('q, 'a) mttm"
and cM :: "('a, 'q) mt_config"
and c0 :: "(sym4, 'q × 'a ar_stage) mt_config"
and R' :: "(sym4, 'q × 'a ar_stage) mt_config rel"
assumes leaf:
"⋀cc tk' tM' p'.
⟦ valid_mttm M; q ∈ Q_tm M; 2 ≤ block_width (Γ_tm M);
¬ is_last_k M tk';
mt_state cc = (q, AR_SimWrite, tk', 0, buf, dvec, posk);
ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
tM' (mt_tape cc tk');
mt_pos cc tk' = (if p' = 0 then Suc 0
else sim_pos (block_width (Γ_tm M)) p' + block_width (Γ_tm M));
posk tk' = AR_AtLE ⟷ p' = 0;
∀k. buf k ∈ Γ_tm M ∪ {bl_tm M};
ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk', 0, buf, dvec, posk);
∀j ≥ k_tm M. mt_tape cc j (mt_pos cc j) = BLANK4;
ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk', 0, buf, dvec, posk) ⟧
⟹ ∃c''. (cc, c'') ∈ R' ^^ (if p' = 0 then 1 else 2 * block_width (Γ_tm M))
∧ mt_state c'' = (q, AR_SimWrite, k_succ tk', 0, buf, dvec, posk)
∧ mt_tape c'' = (if p' = 0 then mt_tape cc
else (mt_tape cc)(tk' := (λpos.
if sim_pos (block_width (Γ_tm M)) p' ≤ pos
∧ pos < sim_pos (block_width (Γ_tm M)) p' + block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf tk')
(pos - sim_pos (block_width (Γ_tm M)) p')
else mt_tape cc tk' pos)))
∧ mt_pos c'' = mt_pos cc"
and vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and stg0: "mt_state c0 = (q, AR_SimWrite, 0, 0, buf, dvec, posk)"
and tcorr: "∀k < k_tm M. ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(mt_tape cM k) (mt_tape c0 k)"
and ppos: "∀k < k_tm M. mt_pos c0 k = (if mt_pos cM k = 0 then Suc 0
else sim_pos (block_width (Γ_tm M)) (mt_pos cM k)
+ block_width (Γ_tm M))"
and poskle: "∀k < k_tm M. posk k = AR_AtLE ⟷ mt_pos cM k = 0"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pad0: "∀j ≥ k_tm M. mt_tape c0 j (mt_pos c0 j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, 0, 0, buf, dvec, posk)"
shows "j ≤ k_tm M - 1 ⟹
(∃c m. (c0, c) ∈ R' ^^ m
∧ m ≤ j * (2 * block_width (Γ_tm M))
∧ mt_state c = (q, AR_SimWrite, k_unidx j, 0, buf, dvec, posk)
∧ mt_tape c = (λk. if k_idx k < j
then (if mt_pos cM k = 0 then mt_tape c0 k
else (λpos. if sim_pos (block_width (Γ_tm M)) (mt_pos cM k) ≤ pos
∧ pos < sim_pos (block_width (Γ_tm M)) (mt_pos cM k)
+ block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf k)
(pos - sim_pos (block_width (Γ_tm M)) (mt_pos cM k))
else mt_tape c0 k pos))
else mt_tape c0 k)
∧ mt_pos c = mt_pos c0)"
proof (induction j)
case 0
let ?k = "block_width (Γ_tm M)"
have "(c0, c0) ∈ R' ^^ 0" by simp
moreover have "mt_tape c0 = (λk. if k_idx k < 0
then (if mt_pos cM k = 0 then mt_tape c0 k
else (λpos. if sim_pos ?k (mt_pos cM k) ≤ pos
∧ pos < sim_pos ?k (mt_pos cM k) + ?k
then write_bit (Γ_tm M) (bl_tm M) (buf k)
(pos - sim_pos ?k (mt_pos cM k))
else mt_tape c0 k pos))
else mt_tape c0 k)"
by simp
ultimately show ?case
using stg0 by (intro exI[where x = c0] exI[where x = 0]) (simp add: k_unidx_zero)
next
case (Suc j)
have sucle: "Suc j ≤ k_tm M - 1" by (rule Suc.prems)
have jcard: "j < k_tm M" using sucle by simp
have sjcard: "Suc j < k_tm M" using sucle by simp
have jle: "j ≤ k_tm M - 1" using sucle by simp
let ?k = "block_width (Γ_tm M)"
let ?tk = "k_unidx j"
let ?p = "mt_pos cM ?tk"
let ?out = "λk. if mt_pos cM k = 0 then mt_tape c0 k
else (λpos. if sim_pos ?k (mt_pos cM k) ≤ pos
∧ pos < sim_pos ?k (mt_pos cM k) + ?k
then write_bit (Γ_tm M) (bl_tm M) (buf k)
(pos - sim_pos ?k (mt_pos cM k))
else mt_tape c0 k pos)"
let ?tape = "λi. (λk. if k_idx k < i then ?out k else mt_tape c0 k)"
have tkidx: "k_idx ?tk = j" by (rule k_idx_unidx[OF jcard])
have notlast: "¬ is_last_k M ?tk"
using is_last_k_unidx[OF jcard] sjcard by simp
have ksucc: "k_succ ?tk = k_unidx (Suc j)" by (rule k_succ_unidx[OF sjcard])
have inj: "inj_on k_idx UNIV" by (rule k_idx_inj)
have kne: "⋀k. k_idx k = j ⟹ k = ?tk"
proof -
fix k assume "k_idx k = j"
hence "k_idx k = k_idx ?tk" using tkidx by simp
thus "k = ?tk" using inj_on_eq_iff[OF inj UNIV_I UNIV_I] by simp
qed
obtain c m where
cm_rel: "(c0, c) ∈ R' ^^ m"
and m_le: "m ≤ j * (2 * ?k)"
and c_st: "mt_state c = (q, AR_SimWrite, ?tk, 0, buf, dvec, posk)"
and c_tp: "mt_tape c = ?tape j"
and c_ps: "mt_pos c = mt_pos c0"
using Suc.IH[OF jle] by blast
have tc_tk: "mt_tape c ?tk = mt_tape c0 ?tk" using c_tp tkidx by simp
have tk_active: "?tk < k_tm M" using jcard by (simp add: k_unidx_def)
have tk_corr: "ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(mt_tape cM ?tk) (mt_tape c ?tk)"
using tcorr[rule_format, OF tk_active] tc_tk by simp
have tk_ppos: "mt_pos c ?tk
= (if ?p = 0 then Suc 0 else sim_pos ?k ?p + ?k)"
using c_ps ppos[rule_format, OF tk_active] by simp
have tk_poskle: "posk ?tk = AR_AtLE ⟷ ?p = 0"
by (rule poskle[rule_format, OF tk_active])
have tk_vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, ?tk, 0, buf, dvec, posk)"
using kge2 buf_valid by (auto simp: ar_valid_stage_def)
have tail_idx: "⋀j'. k_tm M ≤ j' ⟹ ¬ k_idx j' < j"
using jcard unfolding k_idx_def by linarith
have pad_c: "∀j' ≥ k_tm M. mt_tape c j' (mt_pos c j') = BLANK4"
proof (intro allI impI)
fix j' assume jge: "k_tm M ≤ j'"
have "mt_tape c j' (mt_pos c j') = mt_tape c0 j' (mt_pos c0 j')"
using c_tp c_ps tail_idx[OF jge] by simp
thus "mt_tape c j' (mt_pos c j') = BLANK4" using pad0 jge by simp
qed
have src_c: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, ?tk, 0, buf, dvec, posk)"
using src0 tk_active by (auto simp: ar_stage_bounded_def)
obtain c' where
step: "(c, c') ∈ R' ^^ (if ?p = 0 then 1 else 2 * ?k)"
and c'_st: "mt_state c' = (q, AR_SimWrite, k_succ ?tk, 0, buf, dvec, posk)"
and c'_tp: "mt_tape c' = (if ?p = 0 then mt_tape c
else (mt_tape c)(?tk := (λpos.
if sim_pos ?k ?p ≤ pos ∧ pos < sim_pos ?k ?p + ?k
then write_bit (Γ_tm M) (bl_tm M) (buf ?tk)
(pos - sim_pos ?k ?p)
else mt_tape c ?tk pos)))"
and c'_ps: "mt_pos c' = mt_pos c"
using leaf[OF vM qQ kge2 notlast c_st tk_corr tk_ppos tk_poskle
buf_valid tk_vsrc pad_c src_c]
by blast
have tape_eq: "mt_tape c' = ?tape (Suc j)"
proof (rule ext)
fix k
show "mt_tape c' k = ?tape (Suc j) k"
proof (cases "k = ?tk")
case True
show ?thesis
proof (cases "?p = 0")
case True
have "mt_tape c' k = mt_tape c0 ?tk"
using c'_tp ‹k = ?tk› ‹?p = 0› tc_tk by simp
moreover have "?tape (Suc j) k = mt_tape c0 ?tk"
using ‹k = ?tk› tkidx ‹?p = 0› by simp
ultimately show ?thesis by simp
next
case False
show ?thesis
proof (rule ext)
fix pos
have lhs: "mt_tape c' k pos
= (if sim_pos ?k ?p ≤ pos ∧ pos < sim_pos ?k ?p + ?k
then write_bit (Γ_tm M) (bl_tm M) (buf ?tk) (pos - sim_pos ?k ?p)
else mt_tape c ?tk pos)"
using c'_tp ‹k = ?tk› ‹?p ≠ 0› by simp
have rhs: "?tape (Suc j) k pos
= (if sim_pos ?k ?p ≤ pos ∧ pos < sim_pos ?k ?p + ?k
then write_bit (Γ_tm M) (bl_tm M) (buf ?tk) (pos - sim_pos ?k ?p)
else mt_tape c0 ?tk pos)"
using ‹k = ?tk› tkidx ‹?p ≠ 0› by simp
show "mt_tape c' k pos = ?tape (Suc j) k pos"
using lhs rhs tc_tk by simp
qed
qed
next
case False
hence kidx_ne: "k_idx k ≠ j" using kne by blast
have "mt_tape c' k = mt_tape c k"
using c'_tp False by (cases "?p = 0") simp_all
also have "… = ?tape j k" using c_tp by simp
also have "… = ?tape (Suc j) k" using kidx_ne by (simp add: less_Suc_eq)
finally show ?thesis .
qed
qed
have chain: "(c0, c') ∈ R' ^^ (m + (if ?p = 0 then 1 else 2 * ?k))"
proof -
have "(c0, c') ∈ R' ^^ m
O R' ^^ (if ?p = 0 then 1 else 2 * ?k)"
using cm_rel step by (rule relcompI)
thus ?thesis by (simp add: relpow_add)
qed
have bound: "m + (if ?p = 0 then 1 else 2 * ?k) ≤ Suc j * (2 * ?k)"
using m_le kge2 by (cases "?p = 0") auto
show ?case
proof (intro exI[where x = c']
exI[where x = "m + (if ?p = 0 then 1 else 2 * ?k)"] conjI)
show "(c0, c') ∈ R' ^^ (m + (if ?p = 0 then 1 else 2 * ?k))" by (rule chain)
show "m + (if ?p = 0 then 1 else 2 * ?k) ≤ Suc j * (2 * ?k)"
by (rule bound)
show "mt_state c' = (q, AR_SimWrite, k_unidx (Suc j), 0, buf, dvec, posk)"
using c'_st ksucc by simp
show "mt_tape c' = (λk. if k_idx k < Suc j
then (if mt_pos cM k = 0 then mt_tape c0 k
else (λpos. if sim_pos ?k (mt_pos cM k) ≤ pos
∧ pos < sim_pos ?k (mt_pos cM k) + ?k
then write_bit (Γ_tm M) (bl_tm M) (buf k)
(pos - sim_pos ?k (mt_pos cM k))
else mt_tape c0 k pos))
else mt_tape c0 k)"
using tape_eq by simp
show "mt_pos c' = mt_pos c0" using c'_ps c_ps by simp
qed
qed
lemma ar_write_prefix:
fixes M :: "('q, 'a) mttm"
and cM :: "('a, 'q) mt_config"
and c0 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and stg0: "mt_state c0 = (q, AR_SimWrite, 0, 0, buf, dvec, posk)"
and tcorr: "∀k < k_tm M. ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(mt_tape cM k) (mt_tape c0 k)"
and ppos: "∀k < k_tm M. mt_pos c0 k = (if mt_pos cM k = 0 then Suc 0
else sim_pos (block_width (Γ_tm M)) (mt_pos cM k)
+ block_width (Γ_tm M))"
and poskle: "∀k < k_tm M. posk k = AR_AtLE ⟷ mt_pos cM k = 0"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pad0: "∀j ≥ k_tm M. mt_tape c0 j (mt_pos c0 j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, 0, 0, buf, dvec, posk)"
shows "j ≤ k_tm M - 1 ⟹
(∃c m. (c0, c) ∈ (mttm_step (alphabet_reduce_delta M)) ^^ m
∧ m ≤ j * (2 * block_width (Γ_tm M))
∧ mt_state c = (q, AR_SimWrite, k_unidx j, 0, buf, dvec, posk)
∧ mt_tape c = (λk. if k_idx k < j
then (if mt_pos cM k = 0 then mt_tape c0 k
else (λpos. if sim_pos (block_width (Γ_tm M)) (mt_pos cM k) ≤ pos
∧ pos < sim_pos (block_width (Γ_tm M)) (mt_pos cM k)
+ block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf k)
(pos - sim_pos (block_width (Γ_tm M)) (mt_pos cM k))
else mt_tape c0 k pos))
else mt_tape c0 k)
∧ mt_pos c = mt_pos c0)"
by (rule ar_write_prefix_gen
[OF ar_write_tape_step vM qQ kge2 stg0 tcorr ppos poskle buf_valid
pad0 src0])
text ‹The full write phase: the prefix walk over the first
‹k_tm M - 1› tapes followed by the unified last-tape write
‹ar_write_tape_finish_step›, landing at ‹AR_SimAdvance›
(current-tape field ‹k_unidx 0›) with every proper tape's
‹b›-cell block overwritten by ‹write_bit (buf k)› (the
encoded ‹M›-write symbol) and every ‹LE› tape and head
position unchanged. Aggregate cost ‹≤ k_tm M ⋅ 2b›.
The split tape descriptor collapses to the full per-tape overwrite on
the last tape (every other tape has index ‹< k_tm M - 1›).›
text ‹Relation-generic full write phase scaffold. The two
helpers (prefix walk, last-tape finish) are the ‹leaf_prefix›
and ‹leaf_finish› hypotheses; union and sub versions are thin
instantiations.›
lemma ar_write_phase_gen:
fixes M :: "('q, 'a) mttm"
and cM :: "('a, 'q) mt_config"
and c0 :: "(sym4, 'q × 'a ar_stage) mt_config"
and R' :: "(sym4, 'q × 'a ar_stage) mt_config rel"
assumes leaf_prefix:
"⋀jj. ⟦ valid_mttm M; q ∈ Q_tm M; 2 ≤ block_width (Γ_tm M);
mt_state c0 = (q, AR_SimWrite, 0, 0, buf, dvec, posk);
∀k < k_tm M. ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(mt_tape cM k) (mt_tape c0 k);
∀k < k_tm M. mt_pos c0 k = (if mt_pos cM k = 0 then Suc 0
else sim_pos (block_width (Γ_tm M)) (mt_pos cM k)
+ block_width (Γ_tm M));
∀k < k_tm M. posk k = AR_AtLE ⟷ mt_pos cM k = 0;
∀k. buf k ∈ Γ_tm M ∪ {bl_tm M};
∀j ≥ k_tm M. mt_tape c0 j (mt_pos c0 j) = BLANK4;
ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, 0, 0, buf, dvec, posk);
jj ≤ k_tm M - 1 ⟧
⟹ (∃c m. (c0, c) ∈ R' ^^ m
∧ m ≤ jj * (2 * block_width (Γ_tm M))
∧ mt_state c = (q, AR_SimWrite, k_unidx jj, 0, buf, dvec, posk)
∧ mt_tape c = (λk. if k_idx k < jj
then (if mt_pos cM k = 0 then mt_tape c0 k
else (λpos. if sim_pos (block_width (Γ_tm M)) (mt_pos cM k) ≤ pos
∧ pos < sim_pos (block_width (Γ_tm M)) (mt_pos cM k)
+ block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf k)
(pos - sim_pos (block_width (Γ_tm M)) (mt_pos cM k))
else mt_tape c0 k pos))
else mt_tape c0 k)
∧ mt_pos c = mt_pos c0)"
and leaf_finish:
"⋀cc tk' tM' p'.
⟦ valid_mttm M; q ∈ Q_tm M; 2 ≤ block_width (Γ_tm M);
is_last_k M tk';
mt_state cc = (q, AR_SimWrite, tk', 0, buf, dvec, posk);
ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
tM' (mt_tape cc tk');
mt_pos cc tk' = (if p' = 0 then Suc 0
else sim_pos (block_width (Γ_tm M)) p' + block_width (Γ_tm M));
posk tk' = AR_AtLE ⟷ p' = 0;
∀k. buf k ∈ Γ_tm M ∪ {bl_tm M};
ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk', 0, buf, dvec, posk);
∀j ≥ k_tm M. mt_tape cc j (mt_pos cc j) = BLANK4;
ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk', 0, buf, dvec, posk) ⟧
⟹ ∃c''. (cc, c'') ∈ R' ^^ (if p' = 0 then 1 else 2 * block_width (Γ_tm M))
∧ mt_state c'' = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)
∧ mt_tape c'' = (if p' = 0 then mt_tape cc
else (mt_tape cc)(tk' := (λpos.
if sim_pos (block_width (Γ_tm M)) p' ≤ pos
∧ pos < sim_pos (block_width (Γ_tm M)) p' + block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf tk')
(pos - sim_pos (block_width (Γ_tm M)) p')
else mt_tape cc tk' pos)))
∧ mt_pos c'' = mt_pos cc"
and vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and stg0: "mt_state c0 = (q, AR_SimWrite, 0, 0, buf, dvec, posk)"
and tcorr: "∀k < k_tm M. ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(mt_tape cM k) (mt_tape c0 k)"
and ppos: "∀k < k_tm M. mt_pos c0 k = (if mt_pos cM k = 0 then Suc 0
else sim_pos (block_width (Γ_tm M)) (mt_pos cM k)
+ block_width (Γ_tm M))"
and poskle: "∀k < k_tm M. posk k = AR_AtLE ⟷ mt_pos cM k = 0"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pad0: "∀j ≥ k_tm M. mt_tape c0 j (mt_pos c0 j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, 0, 0, buf, dvec, posk)"
shows "∃c m. (c0, c) ∈ R' ^^ m
∧ m ≤ k_tm M * (2 * block_width (Γ_tm M))
∧ mt_state c = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)
∧ mt_tape c = (λk. if k < k_tm M
then (if mt_pos cM k = 0 then mt_tape c0 k
else (λpos. if sim_pos (block_width (Γ_tm M)) (mt_pos cM k) ≤ pos
∧ pos < sim_pos (block_width (Γ_tm M)) (mt_pos cM k)
+ block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf k)
(pos - sim_pos (block_width (Γ_tm M)) (mt_pos cM k))
else mt_tape c0 k pos))
else mt_tape c0 k)
∧ mt_pos c = mt_pos c0"
proof -
let ?k = "block_width (Γ_tm M)"
let ?N = "k_tm M"
let ?m1 = "?N - 1"
let ?tl = "k_unidx ?m1"
let ?p = "mt_pos cM ?tl"
let ?out = "λk. if mt_pos cM k = 0 then mt_tape c0 k
else (λpos. if sim_pos ?k (mt_pos cM k) ≤ pos
∧ pos < sim_pos ?k (mt_pos cM k) + ?k
then write_bit (Γ_tm M) (bl_tm M) (buf k)
(pos - sim_pos ?k (mt_pos cM k))
else mt_tape c0 k pos)"
let ?tape = "λi. (λk. if k_idx k < i then ?out k else mt_tape c0 k)"
have card1: "0 < ?N" using vM by (cases M) auto
have m1suc: "?N = Suc ?m1" using card1 by simp
have m1card: "?m1 < ?N" using card1 by simp
have m1lt: "?m1 < k_tm M" using card1 by simp
have tl_eq: "?tl = ?m1" by (simp add: k_unidx_def)
have tlidx: "k_idx ?tl = ?m1" by (rule k_idx_unidx[OF m1card])
have tl_active: "?tl < k_tm M" using m1lt tl_eq by simp
have islast: "is_last_k M ?tl" using is_last_k_unidx[OF m1card] m1suc by simp
have cond: "(k < ?m1) = (k < k_tm M)" if "k ≠ ?m1" for k
using that m1suc by (auto simp: less_Suc_eq)
obtain c1 m1 where
c1_rel: "(c0, c1) ∈ R' ^^ m1"
and m1_le: "m1 ≤ ?m1 * (2 * ?k)"
and c1_st: "mt_state c1 = (q, AR_SimWrite, ?tl, 0, buf, dvec, posk)"
and c1_tp: "mt_tape c1 = ?tape ?m1"
and c1_ps: "mt_pos c1 = mt_pos c0"
using leaf_prefix[OF vM qQ kge2 stg0 tcorr ppos poskle buf_valid pad0 src0,
of ?m1]
by auto
have tc_tl: "mt_tape c1 ?tl = mt_tape c0 ?tl" using c1_tp tlidx by simp
have tl_corr: "ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(mt_tape cM ?tl) (mt_tape c1 ?tl)"
using tcorr[rule_format, OF tl_active] tc_tl by simp
have tl_ppos: "mt_pos c1 ?tl
= (if ?p = 0 then Suc 0 else sim_pos ?k ?p + ?k)"
using c1_ps ppos[rule_format, OF tl_active] by simp
have tl_poskle: "posk ?tl = AR_AtLE ⟷ ?p = 0"
by (rule poskle[rule_format, OF tl_active])
have tl_vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, ?tl, 0, buf, dvec, posk)"
using kge2 buf_valid by (auto simp: ar_valid_stage_def)
have tail_idx: "⋀j. k_tm M ≤ j ⟹ ¬ k_idx j < ?m1"
using m1suc unfolding k_idx_def by linarith
have pad_c1: "∀j ≥ k_tm M. mt_tape c1 j (mt_pos c1 j) = BLANK4"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have "mt_tape c1 j (mt_pos c1 j) = mt_tape c0 j (mt_pos c0 j)"
using c1_tp c1_ps tail_idx[OF jge] by simp
thus "mt_tape c1 j (mt_pos c1 j) = BLANK4" using pad0 jge by simp
qed
have src_c1: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, ?tl, 0, buf, dvec, posk)"
using src0 tl_active by (auto simp: ar_stage_bounded_def)
obtain c2 where
step: "(c1, c2) ∈ R' ^^ (if ?p = 0 then 1 else 2 * ?k)"
and c2_st: "mt_state c2 = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)"
and c2_tp: "mt_tape c2 = (if ?p = 0 then mt_tape c1
else (mt_tape c1)(?tl := (λpos.
if sim_pos ?k ?p ≤ pos ∧ pos < sim_pos ?k ?p + ?k
then write_bit (Γ_tm M) (bl_tm M) (buf ?tl)
(pos - sim_pos ?k ?p)
else mt_tape c1 ?tl pos)))"
and c2_ps: "mt_pos c2 = mt_pos c1"
using leaf_finish[OF vM qQ kge2 islast c1_st tl_corr tl_ppos
tl_poskle buf_valid tl_vsrc pad_c1 src_c1]
by blast
have tape_full: "mt_tape c2 = (λk. if k < k_tm M then ?out k else mt_tape c0 k)"
proof (rule ext)
fix k
show "mt_tape c2 k = (if k < k_tm M then ?out k else mt_tape c0 k)"
proof (cases "k = ?tl")
case True
have out_tl: "mt_tape c2 k = ?out k"
proof (cases "?p = 0")
case True
have "mt_tape c2 k = mt_tape c0 ?tl"
using c2_tp ‹k = ?tl› ‹?p = 0› tc_tl by simp
moreover have "?out k = mt_tape c0 ?tl"
using ‹k = ?tl› ‹?p = 0› by simp
ultimately show ?thesis by simp
next
case False
show ?thesis
proof (rule ext)
fix pos
have lhs: "mt_tape c2 k pos
= (if sim_pos ?k ?p ≤ pos ∧ pos < sim_pos ?k ?p + ?k
then write_bit (Γ_tm M) (bl_tm M) (buf ?tl) (pos - sim_pos ?k ?p)
else mt_tape c1 ?tl pos)"
using c2_tp ‹k = ?tl› ‹?p ≠ 0› by simp
have rhs: "?out k pos
= (if sim_pos ?k ?p ≤ pos ∧ pos < sim_pos ?k ?p + ?k
then write_bit (Γ_tm M) (bl_tm M) (buf ?tl) (pos - sim_pos ?k ?p)
else mt_tape c0 ?tl pos)"
using ‹k = ?tl› ‹?p ≠ 0› by simp
show "mt_tape c2 k pos = ?out k pos"
using lhs rhs tc_tl by simp
qed
qed
show ?thesis using out_tl ‹k = ?tl› tl_eq m1lt by simp
next
case False
hence kne: "k ≠ ?m1" using tl_eq by simp
show ?thesis
proof (cases "k < ?m1")
case True
have klt: "k < k_tm M" using True m1lt by simp
have "mt_tape c2 k = mt_tape c1 k"
using c2_tp ‹k ≠ ?tl› by (cases "?p = 0") simp_all
also have "… = ?out k" using c1_tp True by (simp add: k_idx_def)
finally show ?thesis using klt by simp
next
case False
have kge: "¬ k < k_tm M" using False kne cond[OF kne] by simp
have "mt_tape c2 k = mt_tape c1 k"
using c2_tp ‹k ≠ ?tl› by (cases "?p = 0") simp_all
also have "… = mt_tape c0 k" using c1_tp False by (simp add: k_idx_def)
finally show ?thesis using kge by simp
qed
qed
qed
have chain: "(c0, c2) ∈ R' ^^ (m1 + (if ?p = 0 then 1 else 2 * ?k))"
proof -
have "(c0, c2) ∈ R' ^^ m1
O R' ^^ (if ?p = 0 then 1 else 2 * ?k)"
using c1_rel step by (rule relcompI)
thus ?thesis by (simp add: relpow_add)
qed
have bound: "m1 + (if ?p = 0 then 1 else 2 * ?k) ≤ ?N * (2 * ?k)"
proof -
obtain Nm where Nm: "?N = Suc Nm" using card1 by (cases ?N) auto
have e1: "?N * (2 * ?k) = (2 * ?k) + Nm * (2 * ?k)" by (simp add: Nm)
have e2: "m1 ≤ Nm * (2 * ?k)" using m1_le Nm by simp
have e3: "(if ?p = 0 then 1 else 2 * ?k) ≤ 2 * ?k" using kge2 by simp
show ?thesis using e1 e2 e3 by linarith
qed
show ?thesis
proof (intro exI[where x = c2]
exI[where x = "m1 + (if ?p = 0 then 1 else 2 * ?k)"] conjI)
show "(c0, c2) ∈ R' ^^ (m1 + (if ?p = 0 then 1 else 2 * ?k))" by (rule chain)
show "m1 + (if ?p = 0 then 1 else 2 * ?k) ≤ ?N * (2 * ?k)" by (rule bound)
show "mt_state c2 = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)"
by (rule c2_st)
show "mt_tape c2 = (λk. if k < k_tm M
then (if mt_pos cM k = 0 then mt_tape c0 k
else (λpos. if sim_pos ?k (mt_pos cM k) ≤ pos
∧ pos < sim_pos ?k (mt_pos cM k) + ?k
then write_bit (Γ_tm M) (bl_tm M) (buf k)
(pos - sim_pos ?k (mt_pos cM k))
else mt_tape c0 k pos))
else mt_tape c0 k)"
using tape_full by simp
show "mt_pos c2 = mt_pos c0" using c2_ps c1_ps by simp
qed
qed
lemma ar_write_phase:
fixes M :: "('q, 'a) mttm"
and cM :: "('a, 'q) mt_config"
and c0 :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and qQ: "q ∈ Q_tm M"
and kge2: "2 ≤ block_width (Γ_tm M)"
and stg0: "mt_state c0 = (q, AR_SimWrite, 0, 0, buf, dvec, posk)"
and tcorr: "∀k < k_tm M. ar_tape_correspondence (Γ_tm M) (le_tm M) (bl_tm M)
(mt_tape cM k) (mt_tape c0 k)"
and ppos: "∀k < k_tm M. mt_pos c0 k = (if mt_pos cM k = 0 then Suc 0
else sim_pos (block_width (Γ_tm M)) (mt_pos cM k)
+ block_width (Γ_tm M))"
and poskle: "∀k < k_tm M. posk k = AR_AtLE ⟷ mt_pos cM k = 0"
and buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
and pad0: "∀j ≥ k_tm M. mt_tape c0 j (mt_pos c0 j) = BLANK4"
and src0: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, 0, 0, buf, dvec, posk)"
shows "∃c m. (c0, c) ∈ (mttm_step (alphabet_reduce_delta M)) ^^ m
∧ m ≤ k_tm M * (2 * block_width (Γ_tm M))
∧ mt_state c = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)
∧ mt_tape c = (λk. if k < k_tm M
then (if mt_pos cM k = 0 then mt_tape c0 k
else (λpos. if sim_pos (block_width (Γ_tm M)) (mt_pos cM k) ≤ pos
∧ pos < sim_pos (block_width (Γ_tm M)) (mt_pos cM k)
+ block_width (Γ_tm M)
then write_bit (Γ_tm M) (bl_tm M) (buf k)
(pos - sim_pos (block_width (Γ_tm M)) (mt_pos cM k))
else mt_tape c0 k pos))
else mt_tape c0 k)
∧ mt_pos c = mt_pos c0"
by (rule ar_write_phase_gen
[OF ar_write_prefix ar_write_tape_finish_step
vM qQ kge2 stg0 tcorr ppos poskle buf_valid pad0 src0])
end