Theory Elementary

section ‹Elementary Turing machines\label{s:tm-elementary}›

theory Elementary
  imports Combinations
begin

text ‹
In this section we devise some simple yet useful Turing machines.  We have
already fully analyzed the empty TM, where start and halting state coincide, in
the lemmas~@{thm [source] computes_Nil_empty}, @{thm [source] Nil_tm}, and @{thm
[source] transforms_Nil}.  The next more complex TMs are those with exactly one
command. They represent TMs with two states: the halting state and the start
state where the action happens. This action might last for one step only, or the
TM may stay in this state for longer; for example, it can move a tape head
rightward to the next blank symbol.  We will also start using the @{text ";;"}
operator to combine some of the one-command TMs.
›

text ‹
Most Turing machines we are going to construct throughout this section and
indeed the entire article are really families of Turing machines that usually
are parameterized by tape indices.
›

type_synonym tapeidx = nat

text ‹
Throughout this article, names of commands are prefixed with @{text cmd_} and
names of Turing machines with @{text tm_}. Usually for a TM named @{term tm_foo}
there is a lemma @{text tm_foo_tm} stating that it really is a Turing machine and
a lemma @{text transforms_tm_fooI} describing its semantics and running time. The
lemma usually receives a @{text transforms_intros} attribute for use with our
proof method.

If @{term "tm_foo"} comprises more than two TMs we will typically analyze the
semantics and running time in a locale named @{text "turing_machine_foo"}. The
first example of this is @{term tm_equals} in
Section~\ref{s:tm-elementary-comparing}.

When it comes to running times, we will have almost no scruples simplifying
upper bounds to have the form $a + b\cdot n^c$ for some constants $a, b, c$,
even if this means, for example, bounding $n \log n$ by $n^2$.
›


subsection ‹Clean tapes›

text ‹
Most of our Turing machines will not change the start symbol in the first cell
of a tape nor will they write the start symbol anywhere else. The only
exceptions are machines that simulate arbitrary other machines. We call tapes
that have the start symbol only in the first cell \emph{clean tapes}.
›

definition clean_tape :: "tape ⇒ bool" where
  "clean_tape tp ≡ ∀i. fst tp i = ▹ ⟷ i = 0"

lemma clean_tapeI:
  assumes "⋀i. fst tp i = ▹ ⟷ i = 0"
  shows "clean_tape tp"
  unfolding clean_tape_def using assms by simp

lemma clean_tapeI':
  assumes "fst tp 0 = ▹" and "⋀i. i > 0 ⟹ fst tp i ≠ ▹"
  shows "clean_tape tp"
  unfolding clean_tape_def using assms by auto

text ‹
A clean configuration is one with only clean tapes.
›

definition clean_config :: "config ⇒ bool" where
  "clean_config cfg ≡ (∀j<||cfg||. ∀i. (cfg <:> j) i = ▹ ⟷ i = 0)"

lemma clean_config_tapes: "clean_config cfg = (∀tp∈set (snd cfg). clean_tape tp)"
  using clean_config_def clean_tape_def by (metis in_set_conv_nth)

lemma clean_configI:
  assumes "⋀j i. j < length tps ⟹ fst (tps ! j) i = ▹ ⟷ i = 0"
  shows "clean_config (q, tps)"
  unfolding clean_config_def using assms by simp

lemma clean_configI':
  assumes "⋀tp i. tp ∈ set tps ⟹ fst tp i = ▹ ⟷ i = 0"
  shows "clean_config (q, tps)"
  using clean_configI assms by simp

lemma clean_configI'':
  assumes "⋀tp. tp ∈ set tps ⟹ (fst tp 0 = ▹ ∧ (∀i>0. fst tp i ≠ ▹))"
  shows "clean_config (q, tps)"
  using clean_configI' assms by blast

lemma clean_configE:
  assumes "clean_config (q, tps)"
  shows "⋀j i. j < length tps ⟹ fst (tps ! j) i = ▹ ⟷ i = 0"
  using clean_config_def assms by simp

lemma clean_configE':
  assumes "clean_config (q, tps)"
  shows "⋀tp i. tp ∈ set tps ⟹ fst tp i = ▹ ⟷ i = 0"
  using clean_configE assms by (metis in_set_conv_nth)

lemma clean_contents_proper [simp]: "proper_symbols zs ⟹ clean_tape (⌊zs⌋, q)"
  using clean_tape_def contents_def proper_symbols_ne1 by simp

lemma contents_clean_tape': "proper_symbols zs ⟹ fst tp = ⌊zs⌋ ⟹ clean_tape tp"
  using contents_def clean_tape_def by (simp add: nat_neq_iff)

text ‹
Some more lemmas about @{const contents}:
›

lemma contents_append_blanks: "⌊ys @ replicate m □⌋ = ⌊ys⌋"
proof
  fix i
  consider
      "i = 0"
    | "0 < i ∧ i ≤ length ys"
    | "length ys < i ∧ i ≤ length ys + m"
    | "length ys + m < i"
    by linarith
  then show "⌊ys @ replicate m □⌋ i = ⌊ys⌋ i"
  proof (cases)
    case 1
    then show ?thesis
      by simp
  next
    case 2
    then show ?thesis
      using contents_inbounds
      by (metis (no_types, opaque_lifting) Suc_diff_1 Suc_le_eq le_add1 le_trans length_append nth_append)
  next
    case 3
    then show ?thesis
      by (smt (verit) Suc_diff_Suc add_diff_inverse_nat contents_def diff_Suc_1 diff_commute leD less_one
        less_or_eq_imp_le nat_add_left_cancel_le not_less_eq nth_append nth_replicate)
  next
    case 4
    then show ?thesis
      by simp
  qed
qed

lemma contents_append_update:
  assumes "length ys = m"
  shows "⌊ys @ [v] @ zs⌋(Suc m := w) = ⌊ys @ [w] @ zs⌋"
proof
  fix i
  consider
      "i = 0"
    | "0 < i ∧ i < Suc m"
    | "i = Suc m"
    | "i > Suc m ∧ i ≤ Suc m + length zs"
    | "i > Suc m + length zs"
    by linarith
  then show "(⌊ys @ [v] @ zs⌋(Suc m := w)) i = ⌊ys @ [w] @ zs⌋ i"
    (is "?l = ?r")
  proof (cases)
    case 1
    then show ?thesis
      by simp
  next
    case 2
    then have "?l = (ys @ [v] @ zs) ! (i - 1)"
      using assms contents_inbounds by simp
    then have *: "?l = ys ! (i - 1)"
      using 2 assms by (metis Suc_diff_1 Suc_le_lessD less_Suc_eq_le nth_append)
    have "?r = (ys @ [w] @ zs) ! (i - 1)"
      using 2 assms contents_inbounds by simp
    then have "?r = ys ! (i - 1)"
      using 2 assms by (metis Suc_diff_1 Suc_le_lessD less_Suc_eq_le nth_append)
    then show ?thesis
      using * by simp
  next
    case 3
    then show ?thesis
      using assms by auto
  next
    case 4
    then have "?l = (ys @ [v] @ zs) ! (i - 1)"
      using assms contents_inbounds by simp
    then have "?l = ((ys @ [v]) @ zs) ! (i - 1)"
      by simp
    then have *: "?l = zs ! (i - 1 - Suc m)"
      using 4 assms by (metis diff_Suc_1 length_append_singleton less_imp_Suc_add not_add_less1 nth_append)
    then have "?r = (ys @ [w] @ zs) ! (i - 1)"
      using 4 assms contents_inbounds by simp
    then have "?r = ((ys @ [w]) @ zs) ! (i - 1)"
      by simp
    then have "?r = zs ! (i - 1 - Suc m)"
      using 4 assms by (metis diff_Suc_1 length_append_singleton less_imp_Suc_add not_add_less1 nth_append)
    then show ?thesis
      using * by simp
  next
    case 5
    then show ?thesis
      using assms by simp
  qed
qed

lemma contents_snoc: "⌊ys⌋(Suc (length ys) := w) = ⌊ys @ [w]⌋"
proof
  fix i
  consider "i = 0" | "0 < i ∧ i ≤ length ys" | "i = Suc (length ys)" | "i > Suc (length ys)"
    by linarith
  then show "(⌊ys⌋(Suc (length ys) := w)) i = ⌊ys @ [w]⌋ i"
  proof (cases)
    case 1
    then show ?thesis
      by simp
  next
    case 2
    then show ?thesis
      by (smt (verit, ccfv_SIG) contents_def diff_Suc_1 ex_least_nat_less fun_upd_apply leD le_Suc_eq
        length_append_singleton less_imp_Suc_add nth_append)
  next
    case 3
    then show ?thesis
      by simp
  next
    case 4
    then show ?thesis
      by simp
  qed
qed

definition config_update_pos :: "config ⇒ nat ⇒ nat ⇒ config" where
  "config_update_pos cfg j p ≡ (fst cfg, (snd cfg)[j:=(cfg <:> j, p)])"

lemma config_update_pos_0: "config_update_pos cfg j (cfg <#> j) = cfg"
  using config_update_pos_def by simp

definition config_update_fwd :: "config ⇒ nat ⇒ nat ⇒ config" where
  "config_update_fwd cfg j d ≡ (fst cfg, (snd cfg)[j:=(cfg <:> j, cfg <#> j + d)])"

lemma config_update_fwd_0: "config_update_fwd cfg j 0 = cfg"
  using config_update_fwd_def by simp

lemma config_update_fwd_additive:
  "config_update_fwd (config_update_fwd cfg j d1) j d2 = (config_update_fwd cfg j (d1 + d2))"
  using config_update_fwd_def
  by (smt (verit) add.commute add.left_commute fst_conv le_less_linear list_update_beyond list_update_overwrite nth_list_update_eq sndI)


subsection ‹Moving tape heads›

text ‹
Among the most simple things a Turing machine can do is moving one of its tape
heads.
›

subsubsection ‹Moving left›

text ‹
The next command makes a TM move its head on tape $j$ one cell to the left
unless, of course, it is in the leftmost cell already.
›

definition cmd_left :: "tapeidx ⇒ command" where
  "cmd_left j ≡ λrs. (1, map (λi. (rs ! i, if i = j then Left else Stay)) [0..<length rs])"

lemma turing_command_left: "turing_command k 1 G (cmd_left j)"
  by (auto simp add: cmd_left_def)

lemma cmd_left': "[*] (cmd_left j rs) = 1"
  using cmd_left_def by simp

lemma cmd_left'': "j < length rs ⟹ (cmd_left j rs) [!] j = (rs ! j, Left)"
  using cmd_left_def by simp

lemma cmd_left''': "i < length rs ⟹ i ≠ j ⟹ (cmd_left j rs) [!] i = (rs ! i, Stay)"
  using cmd_left_def by simp

lemma tape_list_eq:
  assumes "length tps' = length tps"
    and "⋀i. i < length tps ⟹ i ≠ j ⟹ tps' ! i = tps ! i"
    and "tps' ! j = x"
  shows "tps' = tps[j := x]"
  using assms by (smt (verit) length_list_update list_update_beyond not_le nth_equalityI nth_list_update)

lemma sem_cmd_left:
  assumes "j < length tps"
  shows "sem (cmd_left j) (0, tps) = (1, tps[j:=(fst (tps ! j), snd (tps ! j) - 1)])"
proof
  show "fst (sem (cmd_left j)  (0, tps)) = fst (1, tps[j := (fst (tps ! j), snd (tps ! j) - 1)])"
    using cmd_left' sem_fst by simp
  have "snd (sem (cmd_left j) (0, tps)) = tps[j := (fst (tps ! j), snd (tps ! j) - 1)]"
  proof (rule tape_list_eq)
    show "||sem (cmd_left j) (0, tps)|| = length tps"
      using turing_command_left sem_num_tapes2' by (metis snd_eqD)
    show "sem (cmd_left j) (0, tps) <!> i = tps ! i" if "i < length tps" and "i ≠ j" for i
    proof -
      let ?rs = "read tps"
      have "length ?rs = length tps"
        using read_length by simp
      moreover have "sem (cmd_left j) (0, tps) <!> i = act (cmd_left j ?rs [!] i) (tps ! i)"
        by (simp add: cmd_left_def sem_snd that(1))
      ultimately show ?thesis
        using that act_Stay cmd_left''' by simp
    qed
    show "sem (cmd_left j) (0, tps) <!> j = (fst (tps ! j), snd (tps ! j) - 1)"
      using assms act_Left cmd_left_def read_length sem_snd by simp
  qed
  then show "snd (sem (cmd_left j) (0, tps)) = snd (1, tps[j := (fst (tps ! j), snd (tps ! j) - 1)])"
    by simp
qed

definition tm_left :: "tapeidx ⇒ machine" where
  "tm_left j ≡ [cmd_left j]"

lemma tm_left_tm: "k ≥ 2 ⟹ G ≥ 4 ⟹ turing_machine k G (tm_left j)"
  unfolding tm_left_def using turing_command_left by auto

lemma exe_tm_left:
  assumes "j < length tps"
  shows "exe (tm_left j) (0, tps) = (1, tps[j := tps ! j |-| 1])"
  unfolding tm_left_def using sem_cmd_left assms by (simp add: exe_lt_length)

lemma execute_tm_left:
  assumes "j < length tps"
  shows "execute (tm_left j) (0, tps) (Suc 0) = (1, tps[j := tps ! j |-| 1])"
  using assms exe_tm_left by simp

lemma transits_tm_left:
  assumes "j < length tps"
  shows "transits (tm_left j) (0, tps) (Suc 0) (1, tps[j := tps ! j |-| 1])"
  using execute_tm_left assms transitsI by blast

lemma transforms_tm_left:
  assumes "j < length tps"
  shows "transforms (tm_left j) tps (Suc 0) (tps[j := tps ! j |-| 1])"
  using transits_tm_left assms by (simp add: tm_left_def transforms_def)

lemma transforms_tm_leftI [transforms_intros]:
  assumes "j < length tps"
    and "t = 1"
    and "tps' = tps[j := tps ! j |-| 1]"
  shows "transforms (tm_left j) tps t tps'"
  using transits_tm_left assms by (simp add: tm_left_def transforms_def)


subsubsection ‹Moving right›

text ‹
The next command makes the head on tape $j$ move one cell to the right.
›

definition cmd_right :: "tapeidx ⇒ command" where
  "cmd_right j ≡ λrs. (1, map (λi. (rs ! i, if i = j then Right else Stay)) [0..<length rs])"

lemma turing_command_right: "turing_command k 1 G (cmd_right j)"
  by (auto simp add: cmd_right_def)

lemma cmd_right': "[*] (cmd_right j rs) = 1"
  using cmd_right_def by simp

lemma cmd_right'': "j < length rs ⟹ (cmd_right j rs) [!] j = (rs ! j, Right)"
  using cmd_right_def by simp

lemma cmd_right''': "i < length rs ⟹ i ≠ j ⟹ (cmd_right j rs) [!] i = (rs ! i, Stay)"
  using cmd_right_def by simp

lemma sem_cmd_right:
  assumes "j < length tps"
  shows "sem (cmd_right j) (0, tps) = (1, tps[j:=(fst (tps ! j), snd (tps ! j) + 1)])"
proof
  show "fst (sem (cmd_right j)  (0, tps)) = fst (1, tps[j := (fst (tps ! j), snd (tps ! j) + 1)])"
    using cmd_right' sem_fst by simp
  have "snd (sem (cmd_right j) (0, tps)) = tps[j := (fst (tps ! j), snd (tps ! j) + 1)]"
  proof (rule tape_list_eq)
    show "||sem (cmd_right j) (0, tps)|| = length tps"
      using sem_num_tapes3 turing_command_right by (metis snd_conv)
    show "sem (cmd_right j) (0, tps) <!> i = tps ! i" if "i < length tps" and "i ≠ j" for i
    proof -
      let ?rs = "read tps"
      have "length ?rs = length tps"
        using read_length by simp
      moreover have "sem (cmd_right j) (0, tps) <!> i = act (cmd_right j ?rs [!] i) (tps ! i)"
        by (simp add: cmd_right_def sem_snd that(1))
      ultimately show ?thesis
        using that act_Stay cmd_right''' by simp
    qed
    show "sem (cmd_right j) (0, tps) <!> j = (fst (tps ! j), snd (tps ! j) + 1)"
      using assms act_Right cmd_right_def read_length sem_snd by simp
  qed
  then show "snd (sem (cmd_right j) (0, tps)) = snd (1, tps[j := (fst (tps ! j), snd (tps ! j) + 1)])"
    by simp
qed

definition tm_right :: "tapeidx ⇒ machine" where
  "tm_right j ≡ [cmd_right j]"

lemma tm_right_tm: "k ≥ 2 ⟹ G ≥ 4 ⟹ turing_machine k G (tm_right j)"
  unfolding tm_right_def using turing_command_right cmd_right' by auto

lemma exe_tm_right:
  assumes "j < length tps"
  shows "exe (tm_right j) (0, tps) = (1, tps[j:=(fst (tps ! j), snd (tps ! j) + 1)])"
  unfolding tm_right_def using sem_cmd_right assms by (simp add: exe_lt_length)

lemma execute_tm_right:
  assumes "j < length tps"
  shows "execute (tm_right j) (0, tps) (Suc 0) = (1, tps[j:=(fst (tps ! j), snd (tps ! j) + 1)])"
  using assms exe_tm_right by simp

lemma transits_tm_right:
  assumes "j < length tps"
  shows "transits (tm_right j) (0, tps) (Suc 0) (1, tps[j:=(fst (tps ! j), snd (tps ! j) + 1)])"
  using execute_tm_right assms transitsI by blast

lemma transforms_tm_right:
  assumes "j < length tps"
  shows "transforms (tm_right j) tps (Suc 0) (tps[j := tps ! j |+| 1])"
  using transits_tm_right assms by (simp add: tm_right_def transforms_def)

lemma transforms_tm_rightI [transforms_intros]:
  assumes "j < length tps"
    and "t = Suc 0"
    and "tps' = tps[j := tps ! j |+| 1]"
  shows "transforms (tm_right j) tps t tps'"
  using transits_tm_right assms by (simp add: tm_right_def transforms_def)


subsubsection ‹Moving right on several tapes›

text ‹
The next command makes the heads on all tapes from a set $J$ of tapes move one
cell to the right.
›

definition cmd_right_many :: "tapeidx set ⇒ command" where
  "cmd_right_many J ≡ λrs. (1, map (λi. (rs ! i, if i ∈ J then Right else Stay)) [0..<length rs])"

lemma turing_command_right_many: "turing_command k 1 G (cmd_right_many J)"
  by (auto simp add: cmd_right_many_def)

lemma sem_cmd_right_many:
  "sem (cmd_right_many J) (0, tps) = (1, map (λj. if j ∈ J then tps ! j |+| 1 else tps ! j) [0..<length tps])"
proof
  show "fst (sem (cmd_right_many J)  (0, tps)) =
      fst (1, map (λj. if j ∈ J then tps ! j |+| 1 else tps ! j) [0..<length tps])"
    using cmd_right_many_def sem_fst by simp
  have "snd (sem (cmd_right_many J) (0, tps)) =
    map (λj. if j ∈ J then tps ! j |+| 1 else tps ! j) [0..<length tps]"
    (is "?lhs = ?rhs")
  proof (rule nth_equalityI)
    show "length ?lhs = length ?rhs"
      using turing_command_right_many sem_num_tapes2'
      by (metis (no_types, lifting) diff_zero length_map length_upt snd_conv)
    then have len: "length ?lhs = length tps"
      by simp
    show "?lhs ! j = ?rhs ! j" if "j < length ?lhs" for j
    proof (cases "j ∈ J")
      case True
      let ?rs = "read tps"
      have "length ?rs = length tps"
        using read_length by simp
      moreover have "sem (cmd_right_many J) (0, tps) <!> j = act (cmd_right_many J ?rs [!] j) (tps ! j)"
        using cmd_right_many_def sem_snd that True len by auto
      moreover have "?rhs ! j = tps ! j |+| 1"
        using that len True by simp
      ultimately show ?thesis
        using that act_Right cmd_right_many_def True len by simp
    next
      case False
      let ?rs = "read tps"
      have "length ?rs = length tps"
        using read_length by simp
      moreover have "sem (cmd_right_many J) (0, tps) <!> j = act (cmd_right_many J ?rs [!] j) (tps ! j)"
        using cmd_right_many_def sem_snd that False len by auto
      moreover have "?rhs ! j = tps ! j"
        using that len False by simp
      ultimately show ?thesis
        using that act_Stay cmd_right_many_def False len by simp
    qed
  qed
  then show "snd (sem (cmd_right_many J) (0, tps)) =
      snd (1, map (λj. if j ∈ J then tps ! j |+| 1 else tps ! j) [0..<length tps])"
    by simp
qed

definition tm_right_many :: "tapeidx set ⇒ machine" where
  "tm_right_many J ≡ [cmd_right_many J]"

lemma tm_right_many_tm: "k ≥ 2 ⟹ G ≥ 4 ⟹ turing_machine k G (tm_right_many J)"
  unfolding tm_right_many_def using turing_command_right_many by auto

lemma transforms_tm_right_manyI [transforms_intros]:
  assumes "t = Suc 0"
    and "tps' = map (λj. if j ∈ J then tps ! j |+| 1 else tps ! j) [0..<length tps]"
  shows "transforms (tm_right_many J) tps t tps'"
proof -
  have "exe (tm_right_many J) (0, tps) = (1, map (λj. if j ∈ J then tps ! j |+| 1 else tps ! j) [0..<length tps])"
    unfolding tm_right_many_def using sem_cmd_right_many by (simp add: exe_lt_length)
  then have "execute (tm_right_many J) (0, tps) (Suc 0) = (1, map (λj. if j ∈ J then tps ! j |+| 1 else tps ! j) [0..<length tps])"
    by simp
  then have "transits (tm_right_many J) (0, tps) (Suc 0) (1, map (λj. if j ∈ J then tps ! j |+| 1 else tps ! j) [0..<length tps])"
    using transitsI by blast
  then have "transforms (tm_right_many J) tps (Suc 0) (map (λj. if j ∈ J then tps ! j |+| 1 else tps ! j) [0..<length tps])"
    by (simp add: tm_right_many_def transforms_def)
  then show ?thesis
    using assms by (simp add: tm_right_many_def transforms_def)
qed


subsection ‹Copying and translating tape contents›

text ‹
The Turing machines in this section scan a tape $j_1$ and copy the symbols to
another tape $j_2$. Scanning can be performed in either direction, and ``copying''
may include mapping the symbols.
›


subsubsection ‹Copying and translating from one tape to another›

text ‹
The next predicate is true iff.\ on the given tape the next symbol from the set
$H$ of symbols is exactly $n$ cells to the right from the current head position.
Thus, a command that moves the tape head right until it finds a symbol from $H$
takes $n$ steps and moves the head $n$ cells right.
›

definition rneigh :: "tape ⇒ symbol set ⇒ nat ⇒ bool" where
  "rneigh tp H n ≡ fst tp (snd tp + n) ∈ H ∧ (∀n' < n. fst tp (snd tp + n') ∉ H)"

lemma rneighI:
  assumes "fst tp (snd tp + n) ∈ H" and "⋀n'. n' < n ⟹ fst tp (snd tp + n') ∉ H"
  shows "rneigh tp H n"
  using assms rneigh_def by simp

text ‹
The analogous predicate for moving to the left:
›

definition lneigh :: "tape ⇒ symbol set ⇒ nat ⇒ bool" where
  "lneigh tp H n ≡ fst tp (snd tp - n) ∈ H ∧ (∀n' < n. fst tp (snd tp - n') ∉ H)"

lemma lneighI:
  assumes "fst tp (snd tp - n) ∈ H" and "⋀n'. n' < n ⟹ fst tp (snd tp - n') ∉ H"
  shows "lneigh tp H n"
  using assms lneigh_def by simp

text ‹
The next command scans tape $j_1$ rightward until it reaches a symbol from the
set $H$. While doing so it copies the symbols, after applying a mapping $f$, to
tape $j_2$.
›

definition cmd_trans_until :: "tapeidx ⇒ tapeidx ⇒ symbol set ⇒ (symbol ⇒ symbol) ⇒ command" where
  "cmd_trans_until j1 j2 H f ≡ λrs.
    if rs ! j1 ∈ H
    then (1, map (λr. (r, Stay)) rs)
    else (0, map (λi. (if i = j2 then f (rs ! j1) else rs ! i, if i = j1 ∨ i = j2 then Right else Stay)) [0..<length rs])"

text ‹
The analogous command for moving to the left:
›

definition cmd_ltrans_until :: "tapeidx ⇒ tapeidx ⇒ symbol set ⇒ (symbol ⇒ symbol) ⇒ command" where
  "cmd_ltrans_until j1 j2 H f ≡ λrs.
    if rs ! j1 ∈ H
    then (1, map (λr. (r, Stay)) rs)
    else (0, map (λi. (if i = j2 then f (rs ! j1) else rs ! i, if i = j1 ∨ i = j2 then Left else Stay)) [0..<length rs])"

lemma proper_cmd_trans_until: "proper_command k (cmd_trans_until j1 j2 H f)"
  using cmd_trans_until_def by simp

lemma proper_cmd_ltrans_until: "proper_command k (cmd_ltrans_until j1 j2 H f)"
  using cmd_ltrans_until_def by simp

lemma sem_cmd_trans_until_1:
  assumes "j1 < k" and "length tps = k" and "(0, tps) <.> j1 ∈ H"
  shows "sem (cmd_trans_until j1 j2 H f) (0, tps) = (1, tps)"
  using cmd_trans_until_def tapes_at_read read_length assms act_Stay
  by (intro semI[OF proper_cmd_trans_until]) auto

lemma sem_cmd_ltrans_until_1:
  assumes "j1 < k" and "length tps = k" and "(0, tps) <.> j1 ∈ H"
  shows "sem (cmd_ltrans_until j1 j2 H f) (0, tps) = (1, tps)"
  using cmd_ltrans_until_def tapes_at_read read_length assms act_Stay
  by (intro semI[OF proper_cmd_ltrans_until]) auto

lemma sem_cmd_trans_until_2:
  assumes "j1 < k" and "length tps = k" and "(0, tps) <.> j1 ∉ H"
  shows "sem (cmd_trans_until j1 j2 H f) (0, tps) =
    (0, tps[j1 := tps ! j1 |+| 1, j2 := tps ! j2 |:=| (f (tps :.: j1)) |+| 1])"
  using cmd_trans_until_def tapes_at_read read_length assms act_Stay act_Right
  by (intro semI[OF proper_cmd_trans_until]) auto

lemma sem_cmd_ltrans_until_2:
  assumes "j1 < k" and "length tps = k" and "(0, tps) <.> j1 ∉ H"
  shows "sem (cmd_ltrans_until j1 j2 H f) (0, tps) =
    (0, tps[j1 := tps ! j1 |-| 1, j2 := tps ! j2 |:=| (f (tps :.: j1)) |-| 1])"
  using cmd_ltrans_until_def tapes_at_read read_length assms act_Stay act_Left
  by (intro semI[OF proper_cmd_ltrans_until]) auto

definition tm_trans_until :: "tapeidx ⇒ tapeidx ⇒ symbol set ⇒ (symbol ⇒ symbol) ⇒ machine" where
  "tm_trans_until j1 j2 H f ≡ [cmd_trans_until j1 j2 H f]"

definition tm_ltrans_until :: "tapeidx ⇒ tapeidx ⇒ symbol set ⇒ (symbol ⇒ symbol) ⇒ machine" where
  "tm_ltrans_until j1 j2 H f ≡ [cmd_ltrans_until j1 j2 H f]"

lemma tm_trans_until_tm:
  assumes "0 < j2" and "j1 < k" and "j2 < k" and "∀h<G. f h < G" and "k ≥ 2" and "G ≥ 4"
  shows "turing_machine k G (tm_trans_until j1 j2 H f)"
  unfolding tm_trans_until_def cmd_trans_until_def using assms turing_machine_def by auto

lemma tm_ltrans_until_tm:
  assumes "0 < j2" and "j1 < k" and "j2 < k" and "∀h<G. f h < G" and "k ≥ 2" and "G ≥ 4"
  shows "turing_machine k G (tm_ltrans_until j1 j2 H f)"
  unfolding tm_ltrans_until_def cmd_ltrans_until_def using assms turing_machine_def by auto

lemma exe_tm_trans_until_1:
  assumes "j1 < k" and "length tps = k" and "(0, tps) <.> j1 ∈ H"
  shows "exe (tm_trans_until j1 j2 H f) (0, tps) = (1, tps)"
  unfolding tm_trans_until_def using sem_cmd_trans_until_1 assms exe_lt_length by simp

lemma exe_tm_ltrans_until_1:
  assumes "j1 < k" and "length tps = k" and "(0, tps) <.> j1 ∈ H"
  shows "exe (tm_ltrans_until j1 j2 H f) (0, tps) = (1, tps)"
  unfolding tm_ltrans_until_def using sem_cmd_ltrans_until_1 assms exe_lt_length by simp

lemma exe_tm_trans_until_2:
  assumes "j1 < k" and "length tps = k" and "(0, tps) <.> j1 ∉ H"
  shows "exe (tm_trans_until j1 j2 H f) (0, tps) =
    (0, tps[j1 := tps ! j1 |+| 1, j2 := tps ! j2 |:=| (f (tps :.: j1)) |+| 1])"
  unfolding tm_trans_until_def using sem_cmd_trans_until_2 assms exe_lt_length by simp

lemma exe_tm_ltrans_until_2:
  assumes "j1 < k" and "length tps = k" and "(0, tps) <.> j1 ∉ H"
  shows "exe (tm_ltrans_until j1 j2 H f) (0, tps) =
    (0, tps[j1 := tps ! j1 |-| 1, j2 := tps ! j2 |:=| (f (tps :.: j1)) |-| 1])"
  unfolding tm_ltrans_until_def using sem_cmd_ltrans_until_2 assms exe_lt_length by simp

text ‹
Let $tp_1$ and $tp_2$ be two tapes with head positions $i_1$ and $i_2$,
respectively. The next function describes the result of overwriting the symbols
at positions $i_2, \dots, i_2 + n - 1$ on tape $tp_2$ by the symbols at
positions $i_1, \dots, i_1 + n - 1$ on tape $tp_1$ after applying a symbol map
$f$.
›

definition transplant :: "tape ⇒ tape ⇒ (symbol ⇒ symbol)⇒ nat ⇒ tape" where
  "transplant tp1 tp2 f n ≡
     (λi. if snd tp2 ≤ i ∧ i < snd tp2 + n then f (fst tp1 (snd tp1 + i - snd tp2)) else fst tp2 i,
      snd tp2 + n)"

text ‹
The analogous function for moving to the left while copying:
›

definition ltransplant :: "tape ⇒ tape ⇒ (symbol ⇒ symbol)⇒ nat ⇒ tape" where
  "ltransplant tp1 tp2 f n ≡
     (λi. if snd tp2 - n < i ∧ i ≤ snd tp2 then f (fst tp1 (snd tp1 + i - snd tp2)) else fst tp2 i,
      snd tp2 - n)"

lemma transplant_0: "transplant tp1 tp2 f 0 = tp2"
  unfolding transplant_def by standard auto

lemma ltransplant_0: "ltransplant tp1 tp2 f 0 = tp2"
  unfolding ltransplant_def by standard auto

lemma transplant_upd: "transplant tp1 tp2 f n |:=| (f ( |.| (tp1 |+| n))) |+| 1 = transplant tp1 tp2 f (Suc n)"
  unfolding transplant_def by auto

lemma ltransplant_upd:
  assumes "n < snd tp2"
  shows "ltransplant tp1 tp2 f n |:=| (f ( |.| (tp1 |-| n))) |-| 1 = ltransplant tp1 tp2 f (Suc n)"
  unfolding ltransplant_def using assms by fastforce

lemma tapes_ltransplant_upd:
  assumes "t < tps :#: j2" and "t < tps :#: j1" and "j1 < k" and "j2 < k" and "length tps = k"
    and "tps' = tps[j1 := tps ! j1 |-| t, j2 := ltransplant (tps ! j1) (tps ! j2) f t]"
  shows "tps'[j1 := tps' ! j1 |-| 1, j2 := tps' ! j2 |:=| (f (tps' :.: j1)) |-| 1] =
    tps[j1 := tps ! j1 |-| Suc t, j2 := ltransplant (tps ! j1) (tps ! j2) f (Suc t)]"
    (is "?lhs = ?rhs")
proof (rule nth_equalityI)
  show 1: "length ?lhs = length ?rhs"
    using assms by simp
  have len: "length ?lhs = k"
    using assms by simp
  show "?lhs ! j = ?rhs ! j" if "j < length ?lhs" for j
  proof -
    have "j < k"
      using len that by simp
    show ?thesis
    proof (cases "j ≠ j1 ∧ j ≠ j2")
      case True
      then show ?thesis
        using assms by simp
    next
      case j1j2: False
      show ?thesis
      proof (cases "j1 = j2")
        case True
        then have j: "j = j1" "j = j2"
          using j1j2 by simp_all
        have "tps' ! j1 = ltransplant (tps ! j1) (tps ! j2) f t"
          using j assms that by simp
        then have *: "snd (tps' ! j1) = snd (tps ! j1) - t"
          using j ltransplant_def by simp
        then have "fst (tps' ! j1) =
          (λi. if snd (tps ! j2) - t < i ∧ i ≤ snd (tps ! j2) then f (fst (tps ! j1) (snd (tps ! j1) + i - snd (tps ! j2))) else fst (tps ! j2) i)"
          using j ltransplant_def assms by auto
        then have "fst (tps' ! j1) =
          (λi. if snd (tps ! j1) - t < i ∧ i ≤ snd (tps ! j1) then f (fst (tps ! j1) (snd (tps ! j1) + i - snd (tps ! j1))) else fst (tps ! j1) i)"
         using j by auto
        then have "fst (tps' ! j1) (snd (tps ! j1) - t) = fst (tps ! j1) (snd (tps ! j1) - t)"
          by simp
        then have "tps' :.: j1 = fst (tps ! j1) (snd (tps ! j1) - t)"
          using * by simp
        then have "?lhs ! j = (ltransplant (tps ! j1) (tps ! j2) f t) |:=| (f ( |.| (tps ! j1 |-| t))) |-| 1"
          using assms(6) j that by simp
        then have "?lhs ! j = (ltransplant (tps ! j1) (tps ! j2) f (Suc t))"
          using ltransplant_upd assms(1) by simp
        moreover have "?rhs ! j = ltransplant (tps ! j1) (tps ! j2) f (Suc t)"
          using assms(6) that j by simp
        ultimately show ?thesis
          by simp
      next
        case j1_neq_j2: False
        then show ?thesis
        proof (cases "j = j1")
          case True
          then have "?lhs ! j = tps' ! j1 |-| 1"
            using assms j1_neq_j2 by simp
          then have "?lhs ! j = (tps ! j1 |-| t) |-| 1"
            using assms j1_neq_j2 by simp
          moreover have "?rhs ! j = tps ! j1 |-| Suc t"
            using True assms j1_neq_j2 by simp
          ultimately show ?thesis
            by simp
        next
          case False
          then have j: "j = j2"
            using j1j2 by simp
          then have "?lhs ! j = tps' ! j2 |:=| (f (tps' :.: j1)) |-| 1"
            using assms by simp
          then have "?lhs ! j = (ltransplant (tps ! j1) (tps ! j2) f t) |:=| (f (tps' :.: j1)) |-| 1"
            using assms by simp
          then have "?lhs ! j = (ltransplant (tps ! j1) (tps ! j2) f (Suc t))"
            using ltransplant_def assms ltransplant_upd by (smt (verit) j1_neq_j2 nth_list_update_eq nth_list_update_neq)
          moreover have "?rhs ! j = ltransplant (tps ! j1) (tps ! j2) f (Suc t)"
            using assms(6) that j by simp
          ultimately show ?thesis
            by simp
        qed
      qed
    qed
  qed
qed

lemma execute_tm_trans_until_less:
  assumes "j1 < k" and "j2 < k" and "length tps = k" and "rneigh (tps ! j1) H n" and "t ≤ n"
  shows "execute (tm_trans_until j1 j2 H f) (0, tps) t =
    (0, tps[j1 := tps ! j1 |+| t, j2 := transplant (tps ! j1) (tps ! j2) f t])"
  using assms(5)
proof (induction t)
  case 0
  then show ?case
    using transplant_0 by simp
next
  case (Suc t)
  then have "t < n" by simp
  let ?M = "tm_trans_until j1 j2 H f"
  have "execute ?M (0, tps) (Suc t) = exe ?M (execute ?M (0, tps) t)"
    by simp
  also have "... = exe ?M (0, tps[j1 := tps ! j1 |+| t, j2 := transplant (tps ! j1) (tps ! j2) f t])"
      (is "_ = exe ?M (0, ?tps)")
    using Suc by simp
  also have "... = (0, ?tps[j1 := ?tps ! j1 |+| 1, j2 := ?tps ! j2 |:=| (f (?tps :.: j1)) |+| 1])"
  proof (rule exe_tm_trans_until_2[where ?k=k])
    show "j1 < k"
      using assms(1) .
    show "length (tps[j1 := tps ! j1 |+| t, j2 := transplant (tps ! j1) (tps ! j2) f t]) = k"
      using assms by simp
    show "(0, tps[j1 := tps ! j1 |+| t, j2 := transplant (tps ! j1) (tps ! j2) f t]) <.> j1 ∉ H"
      using assms transplant_def rneigh_def ‹t < n›
      by (smt (verit) fst_conv length_list_update less_not_refl2 nth_list_update_eq nth_list_update_neq snd_conv)
  qed
  finally show ?case
    using assms transplant_upd
    by auto
      (smt (verit) add.commute fst_conv transplant_def transplant_upd less_not_refl2 list_update_overwrite list_update_swap
       nth_list_update_eq nth_list_update_neq plus_1_eq_Suc snd_conv)
qed

lemma execute_tm_ltrans_until_less:
  assumes "j1 < k" and "j2 < k" and "length tps = k"
    and "lneigh (tps ! j1) H n"
    and "t ≤ n"
    and "n ≤ tps :#: j1"
    and "n ≤ tps :#: j2"
  shows "execute (tm_ltrans_until j1 j2 H f) (0, tps) t =
    (0, tps[j1 := tps ! j1 |-| t, j2 := ltransplant (tps ! j1) (tps ! j2) f t])"
  using assms(5)
proof (induction t)
  case 0
  then show ?case
    using ltransplant_0 by simp
next
  case (Suc t)
  then have "t < n"
    by simp
  have 1: "t < tps :#: j2"
    using assms(7) Suc by simp
  have 2: "t < tps :#: j1"
    using assms(6) Suc by simp
  let ?M = "tm_ltrans_until j1 j2 H f"
  define tps' where "tps' = tps[j1 := tps ! j1 |-| t, j2 := ltransplant (tps ! j1) (tps ! j2) f t]"
  have "execute ?M (0, tps) (Suc t) = exe ?M (execute ?M (0, tps) t)"
    by simp
  also have "... = exe ?M (0, tps')"
    using Suc tps'_def by simp
  also have "... = (0, tps'[j1 := tps' ! j1 |-| 1, j2 := tps' ! j2 |:=| (f (tps' :.: j1)) |-| 1])"
  proof (rule exe_tm_ltrans_until_2[where ?k=k])
    show "j1 < k"
      using assms(1) .
    show "length tps' = k"
      using assms tps'_def by simp
    show "(0, tps') <.> j1 ∉ H"
      using assms ltransplant_def tps'_def lneigh_def ‹t < n›
      by (smt (verit) fst_conv length_list_update less_not_refl2 nth_list_update_eq nth_list_update_neq snd_conv)
  qed
  finally show ?case
    using tapes_ltransplant_upd[OF 1 2 assms(1,2,3) tps'_def] by simp
qed

lemma execute_tm_trans_until:
  assumes "j1 < k" and "j2 < k" and "length tps = k" and "rneigh (tps ! j1) H n"
  shows "execute (tm_trans_until j1 j2 H f) (0, tps) (Suc n) =
    (1, tps[j1 := tps ! j1 |+| n, j2 := transplant (tps ! j1) (tps ! j2) f n])"
proof -
  let ?M = "tm_trans_until j1 j2 H f"
  have "execute ?M (0, tps) (Suc n) = exe ?M (execute ?M (0, tps) n)"
    by simp
  also have "... = exe ?M (0, tps[j1 := tps ! j1 |+| n, j2 := transplant (tps ! j1) (tps ! j2) f n])"
    using execute_tm_trans_until_less[where ?t=n] assms by simp
  also have "... = (1, tps[j1 := tps ! j1 |+| n, j2 := transplant (tps ! j1) (tps ! j2) f n])"
      (is "_ = (1, ?tps)")
  proof -
    have "length ?tps = k"
      using assms(3) by simp
    moreover have "(0, ?tps) <.> j1 ∈ H"
      using rneigh_def transplant_def assms
      by (smt (verit) fst_conv length_list_update less_not_refl2 nth_list_update_eq nth_list_update_neq snd_conv)
    ultimately show ?thesis
      using exe_tm_trans_until_1 assms by simp
  qed
  finally show ?thesis by simp
qed

lemma execute_tm_ltrans_until:
  assumes "j1 < k" and "j2 < k" and "length tps = k"
    and "lneigh (tps ! j1) H n"
    and "n ≤ tps :#: j1"
    and "n ≤ tps :#: j2"
  shows "execute (tm_ltrans_until j1 j2 H f) (0, tps) (Suc n) =
    (1, tps[j1 := tps ! j1 |-| n, j2 := ltransplant (tps ! j1) (tps ! j2) f n])"
proof -
  let ?M = "tm_ltrans_until j1 j2 H f"
  have "execute ?M (0, tps) (Suc n) = exe ?M (execute ?M (0, tps) n)"
    by simp
  also have "... = exe ?M (0, tps[j1 := tps ! j1 |-| n, j2 := ltransplant (tps ! j1) (tps ! j2) f n])"
    using execute_tm_ltrans_until_less[where ?t=n] assms by simp
  also have "... = (1, tps[j1 := tps ! j1 |-| n, j2 := ltransplant (tps ! j1) (tps ! j2) f n])"
      (is "_ = (1, ?tps)")
  proof -
    have "length ?tps = k"
      using assms(3) by simp
    moreover have "(0, ?tps) <.> j1 ∈ H"
      using lneigh_def ltransplant_def assms
      by (smt (verit, ccfv_threshold) fst_conv length_list_update less_not_refl nth_list_update_eq nth_list_update_neq snd_conv)
    ultimately show ?thesis
      using exe_tm_ltrans_until_1 assms by simp
  qed
  finally show ?thesis by simp
qed

lemma transits_tm_trans_until:
  assumes "j1 < k" and "j2 < k" and "length tps = k" and "rneigh (tps ! j1) H n"
  shows "transits (tm_trans_until j1 j2 H f)
    (0, tps)
    (Suc n)
    (1, tps[j1 := tps ! j1 |+| n, j2 := transplant (tps ! j1) (tps ! j2) f n])"
  using execute_tm_trans_until[OF assms] transitsI[of _ _ "Suc n" _ "Suc n"] by blast

lemma transits_tm_ltrans_until:
  assumes "j1 < k" and "j2 < k" and "length tps = k"
    and "lneigh (tps ! j1) H n"
    and "n ≤ tps :#: j1"
    and "n ≤ tps :#: j2"
  shows "transits (tm_ltrans_until j1 j2 H f)
    (0, tps)
    (Suc n)
    (1, tps[j1 := tps ! j1 |-| n, j2 := ltransplant (tps ! j1) (tps ! j2) f n])"
  using execute_tm_ltrans_until[OF assms] transitsI[of _ _ "Suc n" _ "Suc n"] by blast

lemma transforms_tm_trans_until:
  assumes "j1 < k" and "j2 < k" and "length tps = k" and "rneigh (tps ! j1) H n"
  shows "transforms (tm_trans_until j1 j2 H f)
    tps
    (Suc n)
    (tps[j1 := tps ! j1 |+| n, j2 := transplant (tps ! j1) (tps ! j2) f n])"
  using tm_trans_until_def transforms_def transits_tm_trans_until[OF assms] by simp

lemma transforms_tm_ltrans_until:
  assumes "j1 < k" and "j2 < k" and "length tps = k"
    and "lneigh (tps ! j1) H n"
    and "n ≤ tps :#: j1"
    and "n ≤ tps :#: j2"
  shows "transforms (tm_ltrans_until j1 j2 H f)
    tps
    (Suc n)
    (tps[j1 := tps ! j1 |-| n, j2 := ltransplant (tps ! j1) (tps ! j2) f n])"
  using tm_ltrans_until_def transforms_def transits_tm_ltrans_until[OF assms] by simp

corollary transforms_tm_trans_untilI [transforms_intros]:
  assumes "j1 < k" and "j2 < k" and "length tps = k"
    and "rneigh (tps ! j1) H n"
    and "t = Suc n"
    and "tps' = tps[j1 := tps ! j1 |+| n, j2 := transplant (tps ! j1) (tps ! j2) f n]"
  shows "transforms (tm_trans_until j1 j2 H f) tps t tps'"
  using transforms_tm_trans_until[OF assms(1-4)] assms(5,6) by simp

corollary transforms_tm_ltrans_untilI [transforms_intros]:
  assumes "j1 < k" and "j2 < k" and "length tps = k"
    and "lneigh (tps ! j1) H n"
    and "n ≤ tps :#: j1"
    and "n ≤ tps :#: j2"
    and "t = Suc n"
    and "tps' = tps[j1 := tps ! j1 |-| n, j2 := ltransplant (tps ! j1) (tps ! j2) f n]"
  shows "transforms (tm_ltrans_until j1 j2 H f) tps t tps'"
  using transforms_tm_ltrans_until[OF assms(1-6)] assms(7,8) by simp


subsubsection ‹Copying one tape to another›

text ‹
If we set the symbol map $f$ in @{const tm_trans_until} to the identity
function, we get a Turing machine that simply makes a copy.
›

definition tm_cp_until :: "tapeidx ⇒ tapeidx ⇒ symbol set ⇒ machine" where
  "tm_cp_until j1 j2 H ≡ tm_trans_until j1 j2 H id"

lemma id_symbol: "∀h<G. (id :: symbol ⇒ symbol) h < G"
  by simp

lemma tm_cp_until_tm:
  assumes "0 < j2" and "j1 < k" and "j2 < k" and "G ≥ 4"
  shows "turing_machine k G (tm_cp_until j1 j2 H)"
  unfolding tm_cp_until_def using tm_trans_until_tm id_symbol assms turing_machine_def by simp

abbreviation implant :: "tape ⇒ tape ⇒ nat ⇒ tape" where
  "implant tp1 tp2 n ≡ transplant tp1 tp2 id n"

lemma implant: "implant tp1 tp2 n =
     (λi. if snd tp2 ≤ i ∧ i < snd tp2 + n then fst tp1 (snd tp1 + i - snd tp2) else fst tp2 i,
      snd tp2 + n)"
  using transplant_def by auto

lemma implantI:
  assumes "tp' =
     (λi. if snd tp2 ≤ i ∧ i < snd tp2 + n then fst tp1 (snd tp1 + i - snd tp2) else fst tp2 i,
      snd tp2 + n)"
  shows "implant tp1 tp2 n = tp'"
  using implant assms by simp

lemma fst_snd_pair: "fst t = a ⟹ snd t = b ⟹ t = (a, b)"
  by auto

lemma implantI':
  assumes "fst tp' =
     (λi. if snd tp2 ≤ i ∧ i < snd tp2 + n then fst tp1 (snd tp1 + i - snd tp2) else fst tp2 i)"
    and "snd tp' = snd tp2 + n"
  shows "implant tp1 tp2 n = tp'"
  using implantI fst_snd_pair[OF assms] by simp

lemma implantI'':
  assumes "⋀i. snd tp2 ≤ i ∧ i < snd tp2 + n ⟹ fst tp' i = fst tp1 (snd tp1 + i - snd tp2)"
    and "⋀i. i < snd tp2 ⟹ fst tp' i = fst tp2 i"
    and "⋀i. snd tp2 + n ≤ i ⟹ fst tp' i = fst tp2 i"
  assumes "snd tp' = snd tp2 + n"
  shows "implant tp1 tp2 n = tp'"
  using assms implantI' by (meson linorder_le_less_linear)

lemma implantI''':
  assumes "⋀i. i2 ≤ i ∧ i < i2 + n ⟹ ys i = ys1 (i1 + i - i2)"
    and "⋀i. i < i2 ⟹ ys i = ys2 i"
    and "⋀i. i2 + n ≤ i ⟹ ys i = ys2 i"
  assumes "i = i2 + n"
  shows "implant (ys1, i1) (ys2, i2) n = (ys, i)"
  using assms implantI'' by auto

lemma implant_self: "implant tp tp n = tp |+| n"
  unfolding transplant_def by auto

lemma transforms_tm_cp_untilI [transforms_intros]:
  assumes "j1 < k" and "j2 < k" and "length tps = k"
    and "rneigh (tps ! j1) H n"
    and "t = Suc n"
    and "tps' = tps[j1 := tps ! j1 |+| n, j2 := implant (tps ! j1) (tps ! j2) n]"
  shows "transforms (tm_cp_until j1 j2 H) tps t tps'"
  unfolding tm_cp_until_def using transforms_tm_trans_untilI[OF assms(1-6)] by simp

lemma implant_contents:
  assumes "i > 0" and "n + (i - 1) ≤ length xs"
  shows "implant (⌊xs⌋, i) (⌊ys⌋, Suc (length ys)) n =
     (⌊ys @ (take n (drop (i - 1) xs))⌋, Suc (length ys) + n)"
     (is "?lhs = ?rhs")
proof -
  have lhs: "?lhs =
   (λj. if Suc (length ys) ≤ j ∧ j < Suc (length ys) + n then ⌊xs⌋ (i + j - Suc (length ys)) else ⌊ys⌋ j,
    Suc (length ys) + n)"
    using implant by auto
  let ?zs = "ys @ (take n (drop (i - 1) xs))"
  have lenzs: "length ?zs = length ys + n"
    using assms by simp
  have fst_rhs: "fst ?rhs = (λj. if j = 0 then 1 else if j ≤ length ys + n then ?zs ! (j - 1) else 0)"
    using assms by auto

  have "(λj. if Suc (length ys) ≤ j ∧ j < Suc (length ys) + n then ⌊xs⌋ (i + j - Suc (length ys)) else ⌊ys⌋ j) =
      (λj. if j = 0 then 1 else if j ≤ length ys + n then ?zs ! (j - 1) else 0)"
    (is "?l = ?r")
  proof
    fix j
    consider
        "j = 0"
      | "j > 0 ∧ j ≤ length ys"
      | "j > length ys ∧ j ≤ length ys + n"
      | "j > length ys + n"
      by linarith
    then show "?l j = ?r j"
    proof (cases)
      case 1
      then show ?thesis
        by simp
    next
      case 2
      then show ?thesis
        using assms contents_def by (smt (verit) Suc_diff_1 less_trans_Suc not_add_less1 not_le not_less_eq_eq nth_append)
    next
      case 3
      then have "?r j = ?zs ! (j - 1)"
        by simp
      also have "... = take n (drop (i - 1) xs) ! (j - 1 - length ys)"
        using 3 lenzs
        by (metis add.right_neutral diff_is_0_eq le_add_diff_inverse not_add_less2 not_le not_less_eq nth_append plus_1_eq_Suc)
      also have "... = take n (drop (i - 1) xs) ! (j - Suc (length ys))"
        by simp
      also have "... = xs ! (i - 1 + j - Suc (length ys))"
        using 3 assms by auto
      also have "... = ⌊xs⌋ (i + j - Suc (length ys))"
        using assms contents_def 3 by auto
      also have "... = ?l j"
        using 3 by simp
      finally have "?r j = ?l j" .
      then show ?thesis
        by simp
    next
      case 4
      then show ?thesis
        by simp
    qed
  qed
  then show ?thesis
    using lhs fst_rhs by simp
qed


subsubsection ‹Moving to the next specific symbol›

text ‹
Copying a tape to itself means just moving to the right.
›

definition tm_right_until :: "tapeidx ⇒ symbol set ⇒ machine" where
  "tm_right_until j H ≡ tm_cp_until j j H"

text ‹
Copying a tape to itself does not change the tape. So this is a Turing machine
even for the input tape $j = 0$, unlike @{const tm_cp_until} where
the target tape cannot, in general, be the input tape.
›

lemma tm_right_until_tm:
  assumes "j < k" and "k ≥ 2" and "G ≥ 4"
  shows "turing_machine k G (tm_right_until j H)"
  unfolding tm_right_until_def tm_cp_until_def tm_trans_until_def cmd_trans_until_def
  using assms turing_machine_def
  by auto

lemma transforms_tm_right_untilI [transforms_intros]:
  assumes "j < length tps"
    and "rneigh (tps ! j) H n"
    and "t = Suc n"
    and "tps' = (tps[j := tps ! j |+| n])"
  shows "transforms (tm_right_until j H) tps t tps'"
  using transforms_tm_cp_untilI assms implant_self tm_right_until_def
  by (metis list_update_id nth_list_update_eq)


subsubsection ‹Translating to a constant symbol›

text ‹
Another way to specialize @{const tm_trans_until} and @{const tm_ltrans_until}
is to have a constant function $f$.
›

definition tm_const_until :: "tapeidx ⇒ tapeidx ⇒ symbol set ⇒ symbol ⇒ machine" where
  "tm_const_until j1 j2 H h ≡ tm_trans_until j1 j2 H (λ_. h)"

lemma tm_const_until_tm:
  assumes "0 < j2" and "j1 < k" and "j2 < k" and "h < G" and "k ≥ 2" and "G ≥ 4"
  shows "turing_machine k G (tm_const_until j1 j2 H h)"
  unfolding tm_const_until_def using tm_trans_until_tm assms turing_machine_def by metis

text ‹
Continuing with our fantasy names ending in \emph{-plant}, we name the operation
@{term constplant}.
›

abbreviation constplant :: "tape ⇒ symbol ⇒ nat ⇒ tape" where
  "constplant tp2 h n ≡ transplant (λ_. 0, 0) tp2 (λ_. h) n"

lemma constplant_transplant: "constplant tp2 h n = transplant tp1 tp2 (λ_. h) n"
  using transplant_def by simp

lemma constplant: "constplant tp2 h n =
     (λi. if snd tp2 ≤ i ∧ i < snd tp2 + n then h else fst tp2 i,
      snd tp2 + n)"
  using transplant_def by simp

lemma transforms_tm_const_untilI [transforms_intros]:
  assumes "j1 < k" and "j2 < k" and "length tps = k"
    and "rneigh (tps ! j1) H n"
    and "t = Suc n"
    and "tps' = tps[j1 := tps ! j1 |+| n, j2 := constplant (tps ! j2) h n]"
  shows "transforms (tm_const_until j1 j2 H h) tps t tps'"
  unfolding tm_const_until_def using transforms_tm_trans_untilI assms constplant_transplant by metis

definition tm_lconst_until :: "tapeidx ⇒ tapeidx ⇒ symbol set ⇒ symbol ⇒ machine" where
  "tm_lconst_until j1 j2 H h ≡ tm_ltrans_until j1 j2 H (λ_. h)"

lemma tm_lconst_until_tm:
  assumes "0 < j2" and "j1 < k" and "j2 < k" and "h < G" and "k ≥ 2" and "G ≥ 4"
  shows "turing_machine k G (tm_lconst_until j1 j2 H h)"
  unfolding tm_lconst_until_def using tm_ltrans_until_tm assms turing_machine_def by metis

abbreviation lconstplant :: "tape ⇒ symbol ⇒ nat ⇒ tape" where
  "lconstplant tp2 h n ≡ ltransplant (λ_. 0, 0) tp2 (λ_. h) n"

lemma lconstplant_ltransplant: "lconstplant tp2 h n = ltransplant tp1 tp2 (λ_. h) n"
  using ltransplant_def by simp

lemma lconstplant: "lconstplant tp2 h n =
     (λi. if snd tp2 - n < i ∧ i ≤ snd tp2 then h else fst tp2 i,
      snd tp2 - n)"
  using ltransplant_def by simp

lemma transforms_tm_lconst_untilI [transforms_intros]:
  assumes "0 < j2" and "j1 < k" and "j2 < k" and "length tps = k"
    and "lneigh (tps ! j1) H n"
    and "n ≤ tps :#: j1"
    and "n ≤ tps :#: j2"
    and "t = Suc n"
    and "tps' = tps[j1 := tps ! j1 |-| n, j2 := lconstplant (tps ! j2) h n]"
  shows "transforms (tm_lconst_until j1 j2 H h) tps t tps'"
  unfolding tm_lconst_until_def using transforms_tm_ltrans_untilI assms lconstplant_ltransplant by metis


subsection ‹Writing single symbols›

text ‹
The next command writes a fixed symbol $h$ to tape $j$. It does not move a tape
head.
›

definition cmd_write :: "tapeidx ⇒ symbol ⇒ command" where
  "cmd_write j h rs ≡ (1, map (λi. (if i = j then h else rs ! i, Stay)) [0..<length rs])"

lemma sem_cmd_write: "sem (cmd_write j h) (0, tps) = (1, tps[j := tps ! j |:=| h])"
  using cmd_write_def read_length act_Stay by (intro semI) auto

definition tm_write :: "tapeidx ⇒ symbol ⇒ machine" where
  "tm_write j h ≡ [cmd_write j h]"

lemma tm_write_tm:
  assumes "0 < j" and "j < k" and "h < G" and "G ≥ 4"
  shows "turing_machine k G (tm_write j h)"
  unfolding tm_write_def cmd_write_def using assms turing_machine_def by auto

lemma transforms_tm_writeI [transforms_intros]:
  assumes "tps' = tps[j := tps ! j |:=| h]"
  shows "transforms (tm_write j h) tps 1 tps'"
  unfolding tm_write_def
  using sem_cmd_write exe_lt_length assms tm_write_def transits_def transforms_def
  by auto

text ‹
The next command writes the symbol to tape $j_2$ that results from applying a
function $f$ to the symbol read from tape $j_1$. It does not move any tape heads.
›

definition cmd_trans2 :: "tapeidx ⇒ tapeidx ⇒ (symbol ⇒ symbol) ⇒ command" where
  "cmd_trans2 j1 j2 f rs ≡ (1, map (λi. (if i = j2 then f (rs ! j1) else rs ! i, Stay)) [0..<length rs])"

lemma sem_cmd_trans2:
  assumes "j1 < length tps"
  shows "sem (cmd_trans2 j1 j2 f) (0, tps) = (1, tps[j2 := tps ! j2 |:=| (f (tps :.: j1))])"
  using cmd_trans2_def tapes_at_read assms read_length act_Stay by (intro semI) auto

definition tm_trans2 :: "tapeidx ⇒ tapeidx ⇒ (symbol ⇒ symbol) ⇒ machine" where
  "tm_trans2 j1 j2 f ≡ [cmd_trans2 j1 j2 f]"

lemma tm_trans2_tm:
  assumes "j1 < k" and "0 < j2" and "j2 < k" and "∀h < G. f h < G" and "k ≥ 2" and "G ≥ 4"
  shows "turing_machine k G (tm_trans2 j1 j2 f)"
  unfolding tm_trans2_def cmd_trans2_def using assms turing_machine_def by auto

lemma exe_tm_trans2:
  assumes "j1 < length tps"
  shows "exe (tm_trans2 j1 j2 f) (0, tps) = (1, tps[j2 := tps ! j2 |:=| (f (tps :.: j1))])"
  unfolding tm_trans2_def using sem_cmd_trans2 assms exe_lt_length by simp

lemma execute_tm_trans2:
  assumes "j1 < length tps"
  shows "execute (tm_trans2 j1 j2 f) (0, tps) 1 = (1, tps[j2 := tps ! j2 |:=| (f (tps :.: j1))])"
  using assms exe_tm_trans2 by simp

lemma transits_tm_trans2:
  assumes "j1 < length tps"
  shows "transits (tm_trans2 j1 j2 f) (0, tps) 1 (1, tps[j2 := tps ! j2 |:=| (f (tps :.: j1))])"
  using assms execute_tm_trans2 transits_def by auto

lemma transforms_tm_trans2:
  assumes "j1 < length tps"
  shows "transforms (tm_trans2 j1 j2 f) tps 1 (tps[j2 := tps ! j2 |:=| (f (tps :.: j1))])"
  using tm_trans2_def assms transits_tm_trans2 transforms_def by simp

lemma transforms_tm_trans2I [transforms_intros]:
  assumes "j1 < length tps" and "tps' = tps[j2 := tps ! j2 |:=| (f (tps :.: j1))]"
  shows "transforms (tm_trans2 j1 j2 f) tps 1 tps'"
  using assms transforms_tm_trans2 by simp

text ‹
Equating the two tapes in @{const tm_trans2}, we can map a symbol in-place.
›

definition tm_trans :: "tapeidx ⇒ (symbol ⇒ symbol) ⇒ machine" where
  "tm_trans j f ≡ tm_trans2 j j f"

lemma tm_trans_tm:
  assumes "0 < j" and "j < k" and "∀h < G. f h < G" and "G ≥ 4"
  shows "turing_machine k G (tm_trans j f)"
  unfolding tm_trans_def using tm_trans2_tm assms by simp

lemma transforms_tm_transI [transforms_intros]:
  assumes "j < length tps" and "tps' = tps[j := tps ! j |:=| (f (tps :.: j))]"
  shows "transforms (tm_trans j f) tps 1 tps'"
  using assms transforms_tm_trans2 tm_trans_def by simp

text ‹
The next command is like the previous one, except it also moves the tape head to
the right.
›

definition cmd_rtrans :: "tapeidx ⇒ (symbol ⇒ symbol) ⇒ command" where
  "cmd_rtrans j f rs ≡ (1, map (λi. (if i = j then f (rs ! i) else rs ! i, if i = j then Right else Stay)) [0..<length rs])"

lemma sem_cmd_rtrans:
  assumes "j < length tps"
  shows "sem (cmd_rtrans j f) (0, tps) = (1, tps[j := tps ! j |:=| (f (tps :.: j)) |+| 1])"
  using cmd_rtrans_def tapes_at_read read_length assms act_Stay act_Right
  by (intro semI) auto

definition tm_rtrans :: "tapeidx ⇒ (symbol ⇒ symbol) ⇒ machine" where
  "tm_rtrans j f ≡ [cmd_rtrans j f]"

lemma tm_rtrans_tm:
  assumes "0 < j" and "j < k" and "∀h<G. f h < G" and "k ≥ 2" and "G ≥ 4"
  shows "turing_machine k G (tm_rtrans j f)"
  unfolding tm_rtrans_def cmd_rtrans_def using assms turing_machine_def by auto

lemma exe_tm_rtrans:
  assumes "j < length tps"
  shows "exe (tm_rtrans j f) (0, tps) = (1, tps[j := tps ! j |:=| (f (tps :.: j)) |+| 1])"
  unfolding tm_rtrans_def using sem_cmd_rtrans assms exe_lt_length by simp

lemma execute_tm_rtrans:
  assumes "j < length tps"
  shows "execute (tm_rtrans j f) (0, tps) 1 = (1, tps[j := tps ! j |:=| (f (tps :.: j)) |+| 1])"
  using assms exe_tm_rtrans by simp

lemma transits_tm_rtrans:
  assumes "j < length tps"
  shows "transits (tm_rtrans j f) (0, tps) 1 (1, tps[j := tps ! j |:=| (f (tps :.: j)) |+| 1])"
  using assms execute_tm_rtrans transits_def by auto

lemma transforms_tm_rtrans:
  assumes "j < length tps"
  shows "transforms (tm_rtrans j f) tps 1 (tps[j := tps ! j |:=| (f (tps :.: j)) |+| 1])"
  using assms transits_tm_rtrans transforms_def by (metis One_nat_def length_Cons list.size(3) tm_rtrans_def)

lemma transforms_tm_rtransI [transforms_intros]:
  assumes "j < length tps" and "tps' = tps[j := tps ! j |:=| (f (tps :.: j)) |+| 1]"
  shows "transforms (tm_rtrans j f) tps 1 tps'"
  using assms transforms_tm_rtrans by simp

text ‹
The next command writes a fixed symbol $h$ to all tapes in the set $J$.
›

definition cmd_write_many :: "tapeidx set ⇒ symbol ⇒ command" where
  "cmd_write_many J h rs ≡ (1, map (λi. (if i ∈ J then h else rs ! i, Stay)) [0..<length rs])"

lemma proper_cmd_write_many: "proper_command k (cmd_write_many J h)"
  unfolding cmd_write_many_def by auto

lemma sem_cmd_write_many:
  shows "sem (cmd_write_many J h) (0, tps) =
    (1, map (λj. if j ∈ J then tps ! j |:=| h else tps ! j) [0..<length tps])"
  using cmd_write_many_def read_length act_Stay
  by (intro semI[OF proper_cmd_write_many]) auto

definition tm_write_many :: "tapeidx set ⇒ symbol ⇒ machine" where
  "tm_write_many J h ≡ [cmd_write_many J h]"

lemma tm_write_many_tm:
  assumes "0 ∉ J" and "∀j∈J. j < k" and "h < G" and "k ≥ 2" and "G ≥ 4"
  shows "turing_machine k G (tm_write_many J h)"
  unfolding tm_write_many_def cmd_write_many_def using assms turing_machine_def by auto

lemma exe_tm_write_many: "exe (tm_write_many J h) (0, tps) =
    (1, map (λj. if j ∈ J then tps ! j |:=| h else tps ! j) [0..<length tps])"
  unfolding tm_write_many_def using sem_cmd_write_many exe_lt_length by simp

lemma execute_tm_write_many: "execute (tm_write_many J h) (0, tps) 1 =
    (1, map (λj. if j ∈ J then tps ! j |:=| h else tps ! j) [0..<length tps])"
  using exe_tm_write_many by simp

lemma transforms_tm_write_many:
  "transforms (tm_write_many J h) tps 1 (map (λj. if j ∈ J then tps ! j |:=| h else tps ! j) [0..<length tps])"
  using execute_tm_write_many transits_def transforms_def tm_write_many_def by auto

lemma transforms_tm_write_manyI [transforms_intros]:
  assumes "∀j∈J. j < k"
    and "length tps = k"
    and "length tps' = k"
    and "⋀j. j ∈ J ⟹ tps' ! j = tps ! j |:=| h"
    and "⋀j. j < k ⟹ j ∉ J ⟹ tps' ! j = tps ! j"
  shows "transforms (tm_write_many J h) tps 1 tps'"
proof -
  have "tps' = map (λj. if j ∈ J then tps ! j |:=| h else tps ! j) [0..<length tps]"
    using assms by (intro nth_equalityI) simp_all
  then show ?thesis
    using assms transforms_tm_write_many by auto
qed


subsection ‹Writing a symbol multiple times›

text ‹
In this section we devise a Turing machine that writes the symbol sequence
$h^m$ with a hard-coded symbol $h$ and number $m$ to a tape. The resulting
tape is defined by the next operation:
›

definition overwrite :: "tape ⇒ symbol ⇒ nat ⇒ tape" where
  "overwrite tp h m ≡ (λi. if snd tp ≤ i ∧ i < snd tp + m then h else fst tp i, snd tp + m)"

lemma overwrite_0: "overwrite tp h 0 = tp"
proof -
  have "snd (overwrite tp h 0) = snd tp"
    unfolding overwrite_def by simp
  moreover have "fst (overwrite tp h 0) = fst tp"
    unfolding overwrite_def by auto
  ultimately show ?thesis
    using prod_eqI by blast
qed

lemma overwrite_upd: "(overwrite tp h t) |:=| h |+| 1 = overwrite tp h (Suc t)"
  using overwrite_def by auto

lemma overwrite_upd':
  assumes "j < length tps" and "tps' = tps[j := overwrite (tps ! j) h t]"
  shows "(tps[j := overwrite (tps ! j) h t])[j := tps' ! j |:=| h |+| 1] =
    tps[j := overwrite (tps ! j) h (Suc t)]"
  using assms overwrite_upd by simp

text ‹
The next command writes the symbol $h$ to the tape $j$ and moves the tape head
to the right.
›

definition cmd_char :: "tapeidx ⇒ symbol ⇒ command" where
  "cmd_char j z = cmd_rtrans j (λ_. z)"

lemma turing_command_char:
  assumes "0 < j" and "j < k" and "h < G"
  shows "turing_command k 1 G (cmd_char j h)"
  unfolding cmd_char_def cmd_rtrans_def using assms by auto

definition tm_char :: "tapeidx ⇒ symbol ⇒ machine" where
  "tm_char j z ≡ [cmd_char j z]"

lemma tm_char_tm:
  assumes "0 < j" and "j < k" and "G ≥ 4" and "z < G"
  shows "turing_machine k G (tm_char j z)"
  using assms turing_command_char tm_char_def by auto

lemma transforms_tm_charI [transforms_intros]:
  assumes "j < length tps" and "tps' = tps[j := tps ! j |:=| z |+| 1]"
  shows "transforms (tm_char j z) tps 1 tps'"
  using assms transforms_tm_rtransI tm_char_def cmd_char_def tm_rtrans_def by metis

lemma sem_cmd_char:
  assumes "j < length tps"
  shows "sem (cmd_char j h) (0, tps) = (1, tps[j := tps ! j |:=| h |+| 1])"
  using cmd_char_def cmd_rtrans_def tapes_at_read read_length assms act_Right
  by (intro semI) auto

text ‹
The next TM is a sequence of $m$ @{const cmd_char} commands properly relocated.
It writes a sequence of $m$ times the symbol $h$ to tape $j$.
›

definition tm_write_repeat :: "tapeidx ⇒ symbol ⇒ nat ⇒ machine" where
  "tm_write_repeat j h m ≡ map (λi. relocate_cmd i (cmd_char j h)) [0..<m]"

lemma tm_write_repeat_tm:
  assumes "0 < j" and "j < k" and "h < G" and "k ≥ 2" and "G ≥ 4"
  shows "turing_machine k G (tm_write_repeat j h m)"
proof
  let ?M = "tm_write_repeat j h m"
  show "2 ≤ k" and "4 ≤ G"
    using assms(4,5) .
  show "turing_command k (length ?M) G (?M ! i)" if "i < length ?M" for i
  proof -
    have "?M ! i = relocate_cmd i (cmd_char j h)"
      using that tm_write_repeat_def by simp
    then have "turing_command k (1 + i) G (?M ! i)"
      using assms turing_command_char turing_command_relocate_cmd by metis
    then show ?thesis
      using turing_command_mono that by simp
  qed
qed

lemma exe_tm_write_repeat:
  assumes "j < length tps" and "q < m"
  shows "exe (tm_write_repeat j h m) (q, tps) = (Suc q, tps[j := tps ! j |:=| h |+| 1])"
  using sem_cmd_char assms sem sem_relocate_cmd tm_write_repeat_def by (auto simp add: exe_lt_length)

lemma execute_tm_write_repeat:
  assumes "j < length tps" and "t ≤ m"
  shows "execute (tm_write_repeat j h m) (0, tps) t = (t, tps[j := overwrite (tps ! j) h t])"
  using assms(2)
proof (induction t)
  case 0
  then show ?case using overwrite_0 by simp
next
  case (Suc t)
  then have "t < m" by simp
  have "execute (tm_write_repeat j h m) (0, tps) (Suc t) = exe (tm_write_repeat j h m) (execute (tm_write_repeat j h m) (0, tps) t)"
    by simp
  also have "... = exe (tm_write_repeat j h m) (t, tps[j := overwrite (tps ! j) h t])"
    using Suc by simp
  also have "... = (Suc t, tps[j := overwrite (tps ! j) h (Suc t)])"
    using `t < m` exe_tm_write_repeat assms overwrite_upd' by simp
  finally show ?case .
qed

lemma transforms_tm_write_repeatI [transforms_intros]:
  assumes "j < length tps" and "tps' = tps[j := overwrite (tps ! j) h m]"
  shows "transforms (tm_write_repeat j h m) tps m tps'"
  using assms execute_tm_write_repeat transits_def transforms_def tm_write_repeat_def by auto


subsection ‹Moving to the start of the tape›

text ‹
The next command moves the head on tape $j$ to the left until it reaches
a symbol from the set $H$:
›

definition cmd_left_until :: "symbol set ⇒ tapeidx ⇒ command" where
  "cmd_left_until H j rs ≡
    if rs ! j ∈ H
    then (1, map (λr. (r, Stay)) rs)
    else (0, map (λi. (rs ! i, if i = j then Left else Stay)) [0..<length rs])"

lemma sem_cmd_left_until_1:
  assumes "j < k" and "length tps = k" and "(0, tps) <.> j ∈ H"
  shows "sem (cmd_l