# Theory STM_Renaming

```section ‹Renamings for Singletape Turing Machines›

theory STM_Renaming
imports
Singletape_TM
begin

locale renaming_of_singletape_tm = singletape_tm Q Σ Γ blank LE δ s t r
for Q :: "'q set" and Σ :: "'a set" and Γ blank LE δ s t r
+ fixes ra :: "'a ⇒ 'b"    (* renaming of tape symbols *)
and rq :: "'q ⇒ 'p"    (* renaming of states *)
assumes ra: "inj_on ra Γ"
and rq: "inj_on rq Q"
begin

abbreviation rd where "rd ≡ map_prod rq (map_prod ra (map_prod rq (map_prod ra (λ d :: dir. d))))"

sublocale ren: singletape_tm "rq ` Q" "ra ` Σ" "ra ` Γ" "ra blank" "ra LE" "rd ` δ" "rq s" "rq t" "rq r"
proof (unfold_locales; (intro finite_imageI imageI image_mono fin_Q fin_Γ tm sQ tQ rQ)?)
show "ra LE ∉ ra ` Σ" using ra tm LE by (simp add: inj_on_image_mem_iff)
show "ra blank ∉ ra ` Σ" using ra tm blank by (simp add: inj_on_image_mem_iff)
show "rq t ≠ rq r" using rq tQ rQ tr by (metis inj_on_contraD)
show "rd ` δ ⊆ (rq ` Q - {rq t, rq r}) × ra ` Γ × rq ` Q × ra ` Γ × UNIV"
using δ_set tQ rQ rq by (auto simp: inj_on_def)
fix p1 p2 b2 d
assume "(p1, ra LE, p2, b2, d) ∈ rd ` δ"
then obtain q1 q2 a1 a2 where mem: "(q1, a1, q2, a2, d) ∈ δ" and
id: "p1 = rq q1" "ra LE = ra a1" "p2 = rq q2" "b2 = ra a2" by auto
from δ[OF mem] id(2) LE ra have "a1 = LE" by (simp add: inj_onD)
with δLE[OF mem[unfolded this]]
show "b2 = ra LE ∧ d ∈ {dir.N, dir.R}" unfolding id by auto
qed

fun rc :: "('a, 'q) st_config ⇒ ('b, 'p) st_config" where
"rc (Config⇩S q tc pos) = Config⇩S (rq q) (ra o tc) pos"

lemma ren_init: "rc (init_config w) = ren.init_config (map ra w)"
unfolding init_config_def ren.init_config_def rc.simps
by auto

lemma ren_step: assumes "(c,c') ∈ step"
shows "(rc c, rc c') ∈ ren.step"
using assms
proof (cases rule: step.cases)
case (step q ts n q' a dir)
from step(3) have mem: "(rq q, ra (ts n), rq q', ra a, dir) ∈ rd ` δ" by force
show ?thesis unfolding step rc.simps
by (intro ren.stepI[OF mem], auto)
qed

lemma ren_steps: assumes "(c,c') ∈ step^*"
shows "(rc c, rc c') ∈ ren.step^*"
using assms by (induct, insert ren_step, force+)

lemma ren_steps_count: assumes "(c,c') ∈ step^^n"
shows "(rc c, rc c') ∈ ren.step^^n"
using assms by (induct n arbitrary: c c', insert ren_step, force+)

lemma ren_Lang_forward: assumes "w ∈ Lang"
shows "map ra w ∈ ren.Lang"
proof -
from assms[unfolded Lang_def, simplified]
obtain w' n where w: "set w ⊆ Σ" and steps: "(init_config w, Config⇩S t w' n) ∈ step^*"
by auto
from ren_steps[OF steps, unfolded ren_init, unfolded rc.simps] w
show "map ra w ∈ ren.Lang" unfolding ren.Lang_def by auto
qed

abbreviation ira where "ira ≡ the_inv_into Γ ra"
abbreviation irq where "irq ≡ the_inv_into Q rq"

interpretation inv: renaming_of_singletape_tm "rq ` Q" "ra ` Σ" "ra ` Γ" "ra blank" "ra LE" "rd ` δ" "rq s" "rq t" "rq r" ira irq
by (unfold_locales, insert ra rq inj_on_the_inv_into, auto)

lemmas inv_simps[simp] = the_inv_into_f_f[OF ra] the_inv_into_f_f[OF rq]

lemma inv_ren_Sigma: "ira ` ra ` Σ = Σ" using inv_simps(1)[OF set_mp[OF Σ_sub_Γ]]
by (smt (verit, best) equalityI imageE image_subset_iff subsetI)

lemma inv_ren_Gamma: "ira ` ra ` Γ = Γ" using inv_simps(1)
by (smt (verit, best) equalityI imageE image_subset_iff subsetI)

lemma inv_ren_t: "irq (rq t) = t" using tQ by simp
lemma inv_ren_s: "irq (rq s) = s" using sQ by simp
lemma inv_ren_r: "irq (rq r) = r" using rQ by simp
lemma inv_ren_blank: "ira (ra blank) = blank" using tm by simp
lemma inv_ren_LE: "ira (ra LE) = LE" using tm by simp

lemma inv_ren_δ: "inv.rd ` rd ` δ = δ"
proof -
{
fix trans :: "('q × 'a × 'q × 'a × dir)"
obtain q a p b d where trans: "trans = (q,a,p,b,d)" by (cases trans, auto)
{
assume t: "trans ∈ δ"
note mem = δ[OF this[unfolded trans]]
from t have "inv.rd (rd trans) ∈ inv.rd ` rd ` δ" by blast
also have "inv.rd (rd trans) = trans" unfolding trans using mem by auto
finally have "trans ∈ inv.rd ` rd ` δ" .
}
moreover
{
assume t: "trans ∈ inv.rd ` rd ` δ"
then obtain t' where t'd: "t' ∈ δ" and tra: "trans = inv.rd (rd t')" by auto
obtain q' a' p' b' d' where t': "t' = (q',a',p',b',d')" by (cases t', auto)
note mem = δ[OF t'd[unfolded t']]
from tra[unfolded trans t'] mem
have id: "q' = q" "a' = a" "p' = p" "b' = b" "d' = d" by auto
with trans t'd t' have "trans ∈ δ" by auto
}
ultimately have "trans ∈ inv.rd ` rd ` δ ⟷ trans ∈ δ" by blast
}
thus ?thesis by blast
qed

lemmas inv_ren = inv_ren_t inv_ren_s inv_ren_r inv_ren_δ inv_ren_Gamma inv_ren_Sigma inv_ren_blank inv_ren_LE

lemma inv_ren_Lang: "inv.ren.Lang = Lang" unfolding inv_ren ..

lemma ren_Lang_backward: assumes "v ∈ ren.Lang"
shows "∃ w. v = map ra w ∧ w ∈ Lang"
proof (intro exI conjI)
let ?w = "map ira v"
from inv.ren_Lang_forward[OF assms, unfolded inv_ren_Lang]
show "?w ∈ Lang" .
show "v = map ra ?w" unfolding map_map o_def
proof (subst map_idI)
fix b
assume "b ∈ set v"
with assms[unfolded ren.Lang_def] Σ_sub_Γ obtain a where a: "a ∈ Γ" and b: "b = ra a" by blast
show "ra (ira b) = b" unfolding b using a by simp
qed auto
qed

lemma ren_Lang: "ren.Lang = map ra ` Lang"
proof
show "map ra ` Lang ⊆ ren.Lang" using ren_Lang_forward by blast
show "ren.Lang ⊆ map ra ` Lang" using ren_Lang_backward by blast
qed

lemma ren_det: assumes "deterministic"
shows "ren.deterministic"
unfolding ren.deterministic_def
proof (intro allI impI, goal_cases)
case (1 q a p1 b1 d1 p2 b2 d2)
let ?t1 = "(q, a, p1, b1, d1)"
let ?t2 = "(q, a, p2, b2, d2)"
from 1 have t1: "inv.rd ?t1 ∈ inv.rd ` rd ` δ" by force
from 1 have t2: "inv.rd ?t2 ∈ inv.rd ` rd ` δ" by force
from t1 t2 have "(irq q, ira a, irq p1, ira b1, d1) ∈ δ"  "(irq q, ira a, irq p2, ira b2, d2) ∈ δ"
unfolding inv_ren by auto
from assms[unfolded deterministic_def, rule_format, OF this]
have id: "irq p1 = irq p2" "ira b1 = ira b2" and d: "d1 = d2" by auto
from inj_onD[OF inv.rq id(1)] ren.δ[OF 1(1)] ren.δ[OF 1(2)]
have p: "p1 = p2" by auto
from inj_onD[OF inv.ra id(2)] ren.δ[OF 1(1)] ren.δ[OF 1(2)]
have b: "b1 = b2" by auto
show ?case unfolding b p d by simp
qed

lemma ren_upper_time: assumes "upper_time_bound f"
shows "ren.upper_time_bound f"
unfolding ren.upper_time_bound_def
proof (intro allI impI)
fix w c n
assume w: "set w ⊆ ra ` Σ" and steps: "(ren.init_config w, c) ∈ ren.step ^^ n"
define v where "v = map ira w"
from w have v: "set v ⊆ Σ" unfolding v_def
using inv_ren_Sigma by fastforce
from inv.ren_steps_count[OF steps]
have "(inv.rc (ren.init_config w), inv.rc c) ∈ inv.ren.step ^^ n" .
also have "inv.ren.step = step" using inv_ren_δ by presburger
also have "inv.rc (ren.init_config w) = init_config v" unfolding v_def using v w
by (simp add: inv.ren_init inv_ren_LE inv_ren_blank inv_ren_s)
finally have "(init_config v, inv.rc c) ∈ step ^^ n" .
with assms[unfolded upper_time_bound_def] v have "n ≤ f (length v)" by simp
thus "n ≤ f (length w)" unfolding v_def by auto
qed

end

lemma tm_renaming: assumes "valid_tm (tm :: ('q,'a)tm)"
and "inj_on (ra :: 'a ⇒ 'b) (Γ_tm tm)"
and "inj_on (rq :: 'q ⇒ 'p) (Q_tm tm)"
shows "∃ tm' :: ('p,'b)tm.
valid_tm tm' ∧
Lang_tm tm' = map ra ` Lang_tm tm ∧
(det_tm tm ⟶ det_tm tm') ∧
(∀ f. upperb_time_tm tm f ⟶ upperb_time_tm tm' f)"
proof (cases tm)
case (TM Q Σ Γ bl le δ s t r)
with assms interpret singletape_tm Q Σ Γ bl le δ s t r by auto
interpret renaming_of_singletape_tm Q Σ Γ bl le δ s t r ra rq
by (unfold_locales, insert assms TM, auto)
let ?tm' = "TM (rq ` Q) (ra ` Σ) (ra ` Γ) (ra bl) (ra le) (rd ` δ) (rq s) (rq t) (rq r)"
show ?thesis
by (rule exI[where x = ?tm'])
(simp add: TM ren.singletape_tm_axioms ren_Lang ren_det ren_upper_time)
qed

end
```