Theory Lists_Lists

section ‹Lists of numbers\label{s:tm-numlist}›

theory Lists_Lists
  imports Arithmetic
begin

text ‹
In the previous section we defined a representation for numbers over the binary
alphabet @{text "{𝟬,𝟭}"}. In this section we first introduce a representation
of lists of numbers as symbol sequences over the alphabet @{text "{𝟬,𝟭,¦}"}.
Then we define Turing machines for some operations over such lists.

As with the arithmetic operations, Turing machines implementing the operations
on lists usually expect the tape heads of the operands to be in position~1 and
guarantee to place the tape heads of the result in position~1. The exception are
Turing machines for iterating over lists; such TMs move the tape head to the
next list element.

A tape containing such representations corresponds to a variable of type @{typ
"nat list"}. A tape in the start configuration corresponds to the empty list of
numbers.
›


subsection ‹Representation as symbol sequence\label{s:tm-numlist-repr}›

text ‹
The obvious idea for representing a list of numbers is to write them one after
another separated by a fresh symbol, such as @{text "¦"}. However since we
represent the number~0 by the empty symbol sequence, this would result in both
the empty list and the list containing only the number~0 to be represented by
the same symbol sequence, namely the empty one. To prevent this we use the
symbol @{text "¦"} not as a separator but as a terminator; that is, we append it
to every number.  Consequently the empty symbol sequence represents the empty
list, whereas the list $[0]$ is represented by the symbol sequence @{text "¦"}.
As another example, the list $[14,0,0,7]$ is represented by
@{text "𝟬𝟭𝟭𝟭¦¦¦𝟭𝟭𝟭¦"}. As a side effect of using terminators instead of
separators, the representation of the concatenation of lists is just the
concatenation of the representations of the individual lists.  Moreover the
length of the representation is simply the sum of the individual representation
lengths. The number of @{text "¦"} symbols equals the number of elements in the
list.
›

text ‹
This is how lists of numbers are represented as symbol sequences:
›

definition numlist :: "nat list ⇒ symbol list" where
  "numlist ns ≡ concat (map (λn. canrepr n @ [¦]) ns)"

lemma numlist_Nil: "numlist [] = []"
  using numlist_def by simp

proposition "numlist [0] = [¦]"
  using numlist_def by (simp add: canrepr_0)

lemma numlist_234: "set (numlist ns) ⊆ {𝟬, 𝟭, ¦}"
proof (induction ns)
  case Nil
  then show ?case
    using numlist_def by simp
next
  case (Cons n ns)
  have "numlist (n # ns) = canrepr n @ [¦] @ concat (map (λn. canrepr n @ [¦]) ns)"
    using numlist_def by simp
  then have "numlist (n # ns) = canrepr n @ [¦] @ numlist ns"
    using numlist_def by simp
  moreover have "set ([¦] @ numlist ns) ⊆ {𝟬, 𝟭, ¦}"
    using Cons by simp
  moreover have "set (canrepr n) ⊆ {𝟬, 𝟭, ¦}"
    using bit_symbols_canrepr by (metis in_set_conv_nth insertCI subsetI)
  ultimately show ?case
    by simp
qed

lemma symbols_lt_numlist: "symbols_lt 5 (numlist ns)"
  using numlist_234
  by (metis empty_iff insert_iff nth_mem numeral_less_iff semiring_norm(68) semiring_norm(76) semiring_norm(79)
    semiring_norm(80) subset_code(1) verit_comp_simplify1(2))

lemma bit_symbols_prefix_eq:
  assumes "(x @ [¦]) @ xs = (y @ [¦]) @ ys" and "bit_symbols x" and "bit_symbols y"
  shows "x = y"
proof -
  have *: "x @ [¦] @ xs = y @ [¦] @ ys"
      (is "?lhs = ?rhs")
    using assms(1) by simp
  show "x = y"
  proof (cases "length x ≤ length y")
    case True
    then have "?lhs ! i = ?rhs ! i" if "i < length x" for i
      using that * by simp
    then have eq: "x ! i = y ! i" if "i < length x" for i
      using that True by (metis Suc_le_eq le_trans nth_append)
    have "?lhs ! (length x) = ¦"
      by (metis Cons_eq_appendI nth_append_length)
    then have "?rhs ! (length x) = ¦"
      using * by metis
    then have "length y ≤ length x"
      using assms(3)
      by (metis linorder_le_less_linear nth_append numeral_eq_iff semiring_norm(85) semiring_norm(87) semiring_norm(89))
    then have "length y = length x"
      using True by simp
    then show ?thesis
      using eq by (simp add: list_eq_iff_nth_eq)
  next
    case False
    then have "?lhs ! i = ?rhs ! i" if "i < length y" for i
      using that * by simp
    have "?rhs ! (length y) = ¦"
      by (metis Cons_eq_appendI nth_append_length)
    then have "?lhs ! (length y) = ¦"
      using * by metis
    then have "x ! (length y) = ¦"
      using False by (simp add: nth_append)
    then have False
      using assms(2) False
      by (metis linorder_le_less_linear numeral_eq_iff semiring_norm(85) semiring_norm(87) semiring_norm(89))
    then show ?thesis
      by simp
  qed
qed

lemma numlist_inj: "numlist ns1 = numlist ns2 ⟹ ns1 = ns2"
proof (induction ns1 arbitrary: ns2)
  case Nil
  then show ?case
    using numlist_def by simp
next
  case (Cons n ns1)
  have 1: "numlist (n # ns1) = (canrepr n @ [¦]) @ numlist ns1"
    using numlist_def by simp
  then have "numlist ns2 = (canrepr n @ [¦]) @ numlist ns1"
    using Cons by simp
  then have "ns2 ≠ []"
    using numlist_Nil by auto
  then have 2: "ns2 = hd ns2 # tl ns2"
    using `ns2 ≠ []` by simp
  then have 3: "numlist ns2 = (canrepr (hd ns2) @ [¦]) @ numlist (tl ns2)"
    using numlist_def by (metis concat.simps(2) list.simps(9))

  have 4: "hd ns2 = n"
    using bit_symbols_prefix_eq 1 3 by (metis Cons.prems canrepr bit_symbols_canrepr)
  then have "numlist ns2 = (canrepr n @ [¦]) @ numlist (tl ns2)"
    using 3 by simp
  then have "numlist ns1 = numlist (tl ns2)"
    using 1 by (simp add: Cons.prems)
  then have "ns1 = tl ns2"
    using Cons by simp
  then show ?case
    using 2 4 by simp
qed

corollary proper_symbols_numlist: "proper_symbols (numlist ns)"
  using numlist_234 nth_mem by fastforce

text ‹
The next property would not hold if we used separators between
elements instead of terminators after elements.
›

lemma numlist_append: "numlist (xs @ ys) = numlist xs @ numlist ys"
  using numlist_def by simp

text ‹
Like @{const nlength} for numbers, we have @{term nllength} for the length of
the representation of a list of numbers.
›

definition nllength :: "nat list ⇒ nat" where
  "nllength ns ≡ length (numlist ns)"

lemma nllength: "nllength ns = (∑n←ns. Suc (nlength n))"
  using nllength_def numlist_def by (induction ns) simp_all

lemma nllength_Nil [simp]: "nllength [] = 0"
  using nllength_def numlist_def by simp

lemma length_le_nllength: "length ns ≤ nllength ns"
  using nllength sum_list_mono[of ns "λ_. 1" "λn. Suc (nlength n)"] sum_list_const[of 1 ns]
  by simp

lemma nllength_le_len_mult_max:
  fixes N :: nat and ns :: "nat list"
  assumes "∀n∈set ns. n ≤ N"
  shows "nllength ns ≤ Suc (nlength N) * length ns"
proof -
  have "nllength ns = (∑n←ns. Suc (nlength n))"
    using nllength by simp
  moreover have "Suc (nlength n) ≤ Suc (nlength N)" if "n ∈ set ns" for n
    using nlength_mono that assms by simp
  ultimately have "nllength ns ≤ (∑n←ns. Suc (nlength N))"
    by (simp add: sum_list_mono)
  then show "nllength ns ≤ Suc (nlength N) * length ns"
    using sum_list_const by metis
qed

lemma nllength_upt_le_len_mult_max:
  fixes a b :: nat
  shows "nllength [a..<b] ≤ Suc (nlength b) * (b - a)"
  using nllength_le_len_mult_max[of "[a..<b]" b] by simp

lemma nllength_le_len_mult_Max: "nllength ns ≤ Suc (nlength (Max (set ns))) * length ns"
  using nllength_le_len_mult_max by simp

lemma member_le_nllength: "n ∈ set ns ⟹ nlength n ≤ nllength ns"
  using nllength by (induction ns) auto

lemma member_le_nllength_1: "n ∈ set ns ⟹ nlength n ≤ nllength ns - 1"
  using nllength by (induction ns) auto

lemma nllength_gr_0: "ns ≠ [] ⟹ 0 < nllength ns"
  using nllength_def numlist_def by simp

lemma nlength_min_le_nllength: "n ∈ set ns ⟹ m ∈ set ns ⟹ nlength (min n m) ≤ nllength ns"
  using member_le_nllength by (simp add: min_def)

lemma take_drop_numlist:
  assumes "i < length ns"
  shows "take (Suc (nlength (ns ! i))) (drop (nllength (take i ns)) (numlist ns)) = canrepr (ns ! i) @ [¦]"
proof -
  have "numlist ns = numlist (take i ns) @ numlist (drop i ns)"
    using numlist_append by (metis append_take_drop_id)
  moreover have "numlist (drop i ns) = numlist [ns ! i] @ numlist (drop (Suc i) ns)"
    using assms numlist_append by (metis Cons_nth_drop_Suc append_Cons self_append_conv2)
  ultimately have "numlist ns = numlist (take i ns) @ numlist [ns ! i] @ numlist (drop (Suc i) ns)"
    by simp
  then have "drop (nllength (take i ns)) (numlist ns) = numlist [ns ! i] @ numlist (drop (Suc i) ns)"
    by (simp add: nllength_def)
  then have "drop (nllength (take i ns)) (numlist ns) = canrepr (ns ! i) @ [¦] @ numlist (drop (Suc i) ns)"
    using numlist_def by simp
  then show ?thesis
    by simp
qed

corollary take_drop_numlist':
  assumes "i < length ns"
  shows "take (nlength (ns ! i)) (drop (nllength (take i ns)) (numlist ns)) = canrepr (ns ! i)"
  using take_drop_numlist[OF assms] by (metis append_assoc append_eq_conv_conj append_take_drop_id)

corollary numlist_take_at_term:
  assumes "i < length ns"
  shows "numlist ns ! (nllength (take i ns) + nlength (ns ! i)) = ¦"
  using assms take_drop_numlist nllength_def numlist_append
  by (smt (verit) append_eq_conv_conj append_take_drop_id lessI nth_append_length nth_append_length_plus nth_take)

lemma numlist_take_at:
  assumes "i < length ns" and "j < nlength (ns ! i)"
  shows "numlist ns ! (nllength (take i ns) + j) = canrepr (ns ! i) ! j"
proof -
  have "ns = take i ns @ [ns ! i] @ drop (Suc i) ns"
    using assms by (metis Cons_eq_appendI append_self_conv2 id_take_nth_drop)
  then have "numlist ns = (numlist (take i ns) @ numlist [ns ! i]) @ numlist (drop (Suc i) ns)"
    using numlist_append by (metis append_assoc)
  moreover have "nllength (take i ns) + j < nllength (take i ns) + nllength [ns ! i]"
    using assms(2) nllength by simp
  ultimately have "numlist ns ! (nllength (take i ns) + j) =
      (numlist (take i ns) @ numlist [ns ! i]) ! (nllength (take i ns) + j)"
    by (metis length_append nllength_def nth_append)
  also have "... = numlist [ns ! i] ! j"
    by (simp add: nllength_def)
  also have "... = (canrepr (ns ! i) @ [¦]) ! j"
    using numlist_def by simp
  also have "... = canrepr (ns ! i) ! j"
    using assms(2) by (simp add: nth_append)
  finally show ?thesis .
qed

lemma nllength_take_Suc:
  assumes "i < length ns"
  shows "nllength (take i ns) + Suc (nlength (ns ! i)) = nllength (take (Suc i) ns)"
proof -
  have "ns = take i ns @ [ns ! i] @ drop (Suc i) ns"
    using assms by (metis Cons_eq_appendI append_self_conv2 id_take_nth_drop)
  then have "numlist ns = numlist (take i ns) @ numlist [ns ! i] @ numlist (drop (Suc i) ns)"
    using numlist_append by metis
  then have "nllength ns = nllength (take i ns) + nllength [ns ! i] + nllength (drop (Suc i) ns)"
    by (simp add: nllength_def)
  moreover have "nllength ns = nllength (take (Suc i) ns) + nllength (drop (Suc i) ns)"
    using numlist_append by (metis append_take_drop_id length_append nllength_def)
  ultimately have "nllength (take (Suc i) ns) = nllength (take i ns) + nllength [ns ! i]"
    by simp
  then show ?thesis
    using nllength by simp
qed

lemma numlist_take_Suc_at_term:
  assumes "i < length ns"
  shows "numlist ns ! (nllength (take (Suc i) ns) - 1) = ¦"
proof -
  have "nllength (take (Suc i) ns) - 1 = nllength (take i ns) + nlength (ns ! i)"
    using nllength_take_Suc assms by (metis add_Suc_right diff_Suc_1)
  then show ?thesis
    using numlist_take_at_term assms by simp
qed

lemma nllength_take:
  assumes "i < length ns"
  shows "nllength (take i ns) + nlength (ns ! i) < nllength ns"
proof -
  have "ns = take i ns @ [ns ! i] @ drop (Suc i) ns"
    using assms by (metis Cons_eq_appendI append_self_conv2 id_take_nth_drop)
  then have "numlist ns = numlist (take i ns) @ numlist [ns ! i] @ numlist (drop (Suc i) ns)"
    using numlist_append by metis
  then have "nllength ns = nllength (take i ns) + nllength [ns ! i] + nllength (drop (Suc i) ns)"
    by (simp add: nllength_def)
  then have "nllength ns ≥ nllength (take i ns) + nllength [ns ! i]"
    by simp
  then have "nllength ns ≥ nllength (take i ns) + Suc (nlength (ns ! i))"
    using nllength by simp
  then show ?thesis
    by simp
qed

text ‹
The contents of a tape starting with the start symbol @{text ▹} followed by the
symbol sequence representing a list of numbers:
›

definition nlcontents :: "nat list ⇒ (nat ⇒ symbol)" ("⌊_⌋⇩N⇩L") where
  "⌊ns⌋⇩N⇩L ≡ ⌊numlist ns⌋"

lemma clean_tape_nlcontents: "clean_tape (⌊ns⌋⇩N⇩L, i)"
  by (simp add: nlcontents_def proper_symbols_numlist)

lemma nlcontents_Nil: "⌊[]⌋⇩N⇩L = ⌊[]⌋"
  using nlcontents_def by (simp add: numlist_Nil)

lemma nlcontents_rneigh_4:
  assumes "i < length ns"
  shows "rneigh (⌊ns⌋⇩N⇩L, Suc (nllength (take i ns))) {¦} (nlength (ns ! i))"
proof (rule rneighI)
  let ?tp = "(⌊ns⌋⇩N⇩L, Suc (nllength (take i ns)))"
  show "fst ?tp (snd ?tp + nlength (ns ! i)) ∈ {¦}"
  proof -
    have "snd ?tp + nlength (ns ! i) ≤ nllength ns"
      using nllength_take assms by (simp add: Suc_leI)
    then have "fst ?tp (snd ?tp + nlength (ns ! i)) = numlist ns ! (nllength (take i ns) + nlength (ns ! i))"
      using nlcontents_def contents_inbounds nllength_def by simp
    then show ?thesis
      using numlist_take_at_term assms by simp
  qed
  show "fst ?tp (snd ?tp + j) ∉ {¦}" if "j < nlength (ns ! i)" for j
  proof -
    have "snd ?tp + nlength (ns ! i) ≤ nllength ns"
      using nllength_take assms by (simp add: Suc_leI)
    then have "snd ?tp + j ≤ nllength ns"
      using that by simp
    then have "fst ?tp (snd ?tp + j) = numlist ns ! (nllength (take i ns) + j)"
      using nlcontents_def contents_inbounds nllength_def by simp
    then have "fst ?tp (snd ?tp + j) = canrepr (ns ! i) ! j"
      using assms that numlist_take_at by simp
    then show ?thesis
      using bit_symbols_canrepr that by fastforce
  qed
qed

lemma nlcontents_rneigh_04:
  assumes "i < length ns"
  shows "rneigh (⌊ns⌋⇩N⇩L, Suc (nllength (take i ns))) {□, ¦} (nlength (ns ! i))"
proof (rule rneighI)
  let ?tp = "(⌊ns⌋⇩N⇩L, Suc (nllength (take i ns)))"
  show "fst ?tp (snd ?tp + nlength (ns ! i)) ∈ {□, ¦}"
  proof -
    have "snd ?tp + nlength (ns ! i) ≤ nllength ns"
      using nllength_take assms by (simp add: Suc_leI)
    then have "fst ?tp (snd ?tp + nlength (ns ! i)) = numlist ns ! (nllength (take i ns) + nlength (ns ! i))"
      using nlcontents_def contents_inbounds nllength_def by simp
    then show ?thesis
      using numlist_take_at_term assms by simp
  qed
  show "fst ?tp (snd ?tp + j) ∉ {□, ¦}" if "j < nlength (ns ! i)" for j
  proof -
    have "snd ?tp + nlength (ns ! i) ≤ nllength ns"
      using nllength_take assms by (simp add: Suc_leI)
    then have "snd ?tp + j ≤ nllength ns"
      using that by simp
    then have "fst ?tp (snd ?tp + j) = numlist ns ! (nllength (take i ns) + j)"
      using nlcontents_def contents_inbounds nllength_def by simp
    then have "fst ?tp (snd ?tp + j) = canrepr (ns ! i) ! j"
      using assms that numlist_take_at by simp
    then show ?thesis
      using bit_symbols_canrepr that by fastforce
  qed
qed

text ‹
A tape storing a list of numbers, with the tape head in the first blank cell
after the symbols:
›

abbreviation nltape :: "nat list ⇒ tape" where
  "nltape ns ≡ (⌊ns⌋⇩N⇩L, Suc (nllength ns))"

text ‹
A tape storing a list of numbers, with the tape head on the first symbol
representing the $i$-th number, unless the $i$-th number is zero, in which case
the tape head is on the terminator symbol of this zero. If $i$ is out of bounds
of the list, the tape head is at the first blank after the list.
›

abbreviation nltape' :: "nat list ⇒ nat ⇒ tape" where
  "nltape' ns i ≡ (⌊ns⌋⇩N⇩L, Suc (nllength (take i ns)))"

lemma nltape'_tape_read: "|.| (nltape' ns i) = □ ⟷ i ≥ length ns"
proof -
  have "|.| (nltape' ns i) = □" if "i ≥ length ns" for i
  proof -
    have "nltape' ns i ≡ (⌊ns⌋⇩N⇩L, Suc (nllength ns))"
      using that by simp
    then show ?thesis
      using nlcontents_def contents_outofbounds nllength_def
      by (metis Suc_eq_plus1 add.left_neutral fst_conv less_Suc0 less_add_eq_less snd_conv)
  qed
  moreover have "|.| (nltape' ns i) ≠ □" if "i < length ns" for i
    using that nlcontents_def contents_inbounds nllength_def nllength_take proper_symbols_numlist
    by (metis Suc_leI add_Suc_right diff_Suc_1 fst_conv less_add_same_cancel1 less_le_trans not_add_less2
      plus_1_eq_Suc snd_conv zero_less_Suc)
  ultimately show ?thesis
    by (meson le_less_linear)
qed


subsection ‹Moving to the next element›

text ‹
The next Turing machine provides a means to iterate over a list of numbers.  If
the TM starts in a configuration where the tape $j_1$ contains a list of numbers
and the tape head is on the first symbol of the $i$-th element of this list,
then after the TM has finished, the $i$-th element will be written on tape
$j_2$ and the tape head on $j_1$ will have advanced by one list element. If
$i$ is the last element of the list, the tape head on $j_1$ will be on a blank
symbol. One can execute this TM in a loop until the tape head reaches a blank.
The TM is generic over a parameter $z$ representing the terminator symbol, so it
can be used for other kinds of lists, too (see Section~\ref{s:tm-numlistlist}).

\null
›

definition tm_nextract :: "symbol ⇒ tapeidx ⇒ tapeidx ⇒ machine" where
  "tm_nextract z j1 j2 ≡
    tm_erase_cr j2 ;;
    tm_cp_until j1 j2 {z} ;;
    tm_cr j2 ;;
    tm_right j1"

lemma tm_nextract_tm:
  assumes "G ≥ 4" and "G > z" and "0 < j2" and "j2 < k" and "j1 < k" and "k ≥ 2"
  shows "turing_machine k G (tm_nextract z j1 j2)"
  unfolding tm_nextract_def
  using assms tm_erase_cr_tm tm_cp_until_tm tm_cr_tm tm_right_tm
  by simp

text ‹
The next locale is for the case @{text "z = ¦"}.

\null
›

locale turing_machine_nextract_4 =
  fixes j1 j2 :: tapeidx
begin

definition "tm1 ≡ tm_erase_cr j2"
definition "tm2 ≡ tm1 ;; tm_cp_until j1 j2 {¦}"
definition "tm3 ≡ tm2 ;; tm_cr j2"
definition "tm4 ≡ tm3 ;; tm_right j1"

lemma tm4_eq_tm_nextract: "tm4 = tm_nextract ¦ j1 j2"
  unfolding tm1_def tm2_def tm3_def tm4_def tm_nextract_def by simp

context
  fixes tps0 :: "tape list" and k idx dummy :: nat and ns :: "nat list"
  assumes jk: "j1 < k" "j2 < k" "0 < j1" "0 < j2" "j1 ≠ j2" "length tps0 = k"
    and idx: "idx < length ns"
    and tps0:
      "tps0 ! j1 = nltape' ns idx"
      "tps0 ! j2 = (⌊dummy⌋⇩N, 1)"
begin

definition "tps1 ≡ tps0[j2 := (⌊0⌋⇩N, 1)]"

lemma tm1 [transforms_intros]:
  assumes "ttt = 7 + 2 * nlength dummy"
  shows "transforms tm1 tps0 ttt tps1"
  unfolding tm1_def
proof (tform tps: jk idx tps0 tps1_def assms)
  show "proper_symbols (canrepr dummy)"
    using proper_symbols_canrepr by simp
  show "tps1 = tps0[j2 := (⌊[]⌋, 1)]"
    using ncontents_0 tps1_def by simp
qed

definition "tps2 ≡ tps0
  [j1 := (⌊ns⌋⇩N⇩L, nllength (take (Suc idx) ns)),
   j2 := (⌊ns ! idx⌋⇩N, Suc (nlength (ns ! idx)))]"

lemma tm2 [transforms_intros]:
  assumes "ttt = 7 + 2 * nlength dummy + Suc (nlength (ns ! idx))"
  shows "transforms tm2 tps0 ttt tps2"
  unfolding tm2_def
proof (tform tps: jk idx tps0 tps2_def tps1_def)
  show "rneigh (tps1 ! j1) {¦} (nlength (ns ! idx))"
    using tps1_def tps0 jk by (simp add: idx nlcontents_rneigh_4)
  show "tps2 = tps1
    [j1 := tps1 ! j1 |+| nlength (ns ! idx),
     j2 := implant (tps1 ! j1) (tps1 ! j2) (nlength (ns ! idx))]"
     (is "?l = ?r")
  proof (rule nth_equalityI)
    show len: "length ?l = length ?r"
      using tps1_def tps2_def by simp
    show "?l ! i = ?r ! i" if "i < length ?l" for i
    proof -
      consider "i = j1" | "i = j2" | "i ≠ j1 ∧ i ≠ j2"
        by auto
      then show ?thesis
      proof (cases)
        case 1
        then show ?thesis
          using tps0 that tps1_def tps2_def jk nllength_take_Suc[OF idx] idx by simp
      next
        case 2
        then have lhs: "?l ! i = (⌊ns ! idx⌋⇩N, Suc (nlength (ns ! idx)))"
          using tps2_def jk by simp
        let ?i = "Suc (nllength (take idx ns))"
        have i1: "?i > 0"
          by simp
        have "nlength (ns ! idx) + (?i - 1) ≤ nllength ns"
          using idx by (simp add: add.commute less_or_eq_imp_le nllength_take)
        then have i2: "nlength (ns ! idx) + (?i - 1) ≤ length (numlist ns)"
          using nllength_def by simp
        have "?r ! i = implant (tps1 ! j1) (tps1 ! j2) (nlength (ns ! idx))"
          using 2 tps1_def jk by simp
        also have "... = implant (⌊ns⌋⇩N⇩L, ?i) (⌊0⌋⇩N, 1) (nlength (ns ! idx))"
          using tps1_def jk tps0 by simp
        also have "... =
          (⌊[] @ (take (nlength (ns ! idx)) (drop (?i - 1) (numlist ns)))⌋,
           Suc (length []) + nlength (ns ! idx))"
          using implant_contents[OF i1 i2] by (metis One_nat_def list.size(3) ncontents_0 nlcontents_def)
        finally have "?r ! i =
          (⌊[] @ (take (nlength (ns ! idx)) (drop (?i - 1) (numlist ns)))⌋,
           Suc (length []) + nlength (ns ! idx))" .
        then have "?r ! i = (⌊take (nlength (ns ! idx)) (drop (nllength (take idx ns)) (numlist ns))⌋, Suc (nlength (ns ! idx)))"
          by simp
        then have "?r ! i = (⌊canrepr (ns ! idx)⌋, Suc (nlength (ns ! idx)))"
          using take_drop_numlist'[OF idx] by simp
        then show ?thesis
          using lhs by simp
      next
        case 3
        then show ?thesis
          using that tps1_def tps2_def jk by simp
      qed
    qed
  qed
  show "ttt = 7 + 2 * nlength dummy + Suc (nlength (ns ! idx))"
    using assms(1) .
qed

definition "tps3 ≡ tps0
  [j1 := (⌊ns⌋⇩N⇩L, nllength (take (Suc idx) ns)),
   j2 := (⌊ns ! idx⌋⇩N, 1)]"

lemma tm3 [transforms_intros]:
  assumes "ttt = 11 + 2 * nlength dummy + 2 * (nlength (ns ! idx))"
  shows "transforms tm3 tps0 ttt tps3"
  unfolding tm3_def
proof (tform tps: jk idx tps0 tps2_def tps3_def time: assms tps2_def jk)
  show "clean_tape (tps2 ! j2)"
    using tps2_def jk clean_tape_ncontents by simp
qed

definition "tps4 ≡ tps0
  [j1 := nltape' ns (Suc idx),
   j2 := (⌊ns ! idx⌋⇩N, 1)]"

lemma tm4:
  assumes "ttt = 12 + 2 * nlength dummy + 2 * (nlength (ns ! idx))"
  shows "transforms tm4 tps0 ttt tps4"
  unfolding tm4_def
proof (tform tps: jk idx tps0 tps3_def tps4_def time: assms)
  show "tps4 = tps3[j1 := tps3 ! j1 |+| 1]"
    using tps3_def tps4_def jk tps0
    by (metis Suc_eq_plus1 fst_conv list_update_overwrite list_update_swap nth_list_update_eq nth_list_update_neq snd_conv)
qed

end  (* context *)

end  (* locale turing_machine_nextract *)

lemma transforms_tm_nextract_4I [transforms_intros]:
  fixes j1 j2 :: tapeidx
  fixes tps tps' :: "tape list" and k idx dummy :: nat and ns :: "nat list"
  assumes "j1 < k" "j2 < k" "0 < j1" "0 < j2" "j1 ≠ j2" "length tps = k"
    and "idx < length ns"
  assumes
    "tps ! j1 = nltape' ns idx"
    "tps ! j2 = (⌊dummy⌋⇩N, 1)"
  assumes "ttt = 12 + 2 * nlength dummy + 2 * (nlength (ns ! idx))"
  assumes "tps' = tps
    [j1 := nltape' ns (Suc idx),
     j2 := (⌊ns ! idx⌋⇩N, 1)]"
  shows "transforms (tm_nextract ¦ j1 j2) tps ttt tps'"
proof -
  interpret loc: turing_machine_nextract_4 j1 j2 .
  show ?thesis
    using assms loc.tm4 loc.tps4_def loc.tm4_eq_tm_nextract by simp
qed


subsection ‹Appending an element›

text ‹
The next Turing machine appends the number on tape $j_2$ to the list of numbers
on tape $j_1$.
›

definition tm_append :: "tapeidx ⇒ tapeidx ⇒ machine" where
  "tm_append j1 j2 ≡
    tm_right_until j1 {□} ;;
    tm_cp_until j2 j1 {□} ;;
    tm_cr j2 ;;
    tm_char j1 ¦"

lemma tm_append_tm:
  assumes "0 < j1" and "G ≥ 5" and "j1 < k" and "j2 < k"
  shows "turing_machine k G (tm_append j1 j2)"
  unfolding tm_append_def
  using assms tm_right_until_tm tm_cp_until_tm tm_right_tm tm_char_tm tm_cr_tm
  by simp

locale turing_machine_append =
  fixes j1 j2 :: tapeidx
begin

definition "tm1 ≡ tm_right_until j1 {□}"
definition "tm2 ≡ tm1 ;; tm_cp_until j2 j1 {□}"
definition "tm3 ≡ tm2 ;; tm_cr j2"
definition "tm4 ≡ tm3 ;; tm_char j1 ¦"

lemma tm4_eq_tm_append: "tm4 = tm_append j1 j2"
  unfolding tm4_def tm3_def tm2_def tm1_def tm_append_def by simp

context
  fixes tps0 :: "tape list" and k i1 n :: nat and ns :: "nat list"
  assumes jk: "length tps0 = k" "j1 < k" "j2 < k" "j1 ≠ j2" "0 < j1"
    and i1: "i1 ≤ Suc (nllength ns)"
    and tps0:
      "tps0 ! j1 = (⌊ns⌋⇩N⇩L, i1)"
      "tps0 ! j2 = (⌊n⌋⇩N, 1)"
begin

lemma k: "k ≥ 2"
  using jk by simp

lemma tm1 [transforms_intros]:
  assumes "ttt = Suc (Suc (nllength ns) - i1)"
    and "tps' = tps0[j1 := nltape ns]"
  shows "transforms tm1 tps0 ttt tps'"
  unfolding tm1_def
proof (tform tps: jk k)
  let ?l = "Suc (nllength ns) - i1"
  show "rneigh (tps0 ! j1) {0} ?l"
  proof (rule rneighI)
    show "(tps0 ::: j1) (tps0 :#: j1 + ?l) ∈ {0}"
      using tps0 jk nlcontents_def nllength_def by simp
    show "(tps0 ::: j1) (tps0 :#: j1 + i) ∉ {0}" if "i < Suc (nllength ns) - i1" for i
    proof -
      have "i1 + i < Suc (nllength ns)"
        using that i1 by simp
      then show ?thesis
        using proper_symbols_numlist nllength_def tps0 nlcontents_def contents_def
        by (metis One_nat_def Suc_le_eq diff_Suc_1 fst_eqD less_Suc_eq_0_disj less_nat_zero_code singletonD snd_eqD)
    qed
  qed
  show "ttt = Suc (Suc (nllength ns) - i1)"
    using assms(1) .
  show "tps' = tps0[j1 := tps0 ! j1 |+| Suc (nllength ns) - i1]"
    using assms(2) tps0 i1 by simp
qed

lemma tm2 [transforms_intros]:
  assumes "ttt = 3 + nllength ns - i1 + nlength n"
    and "tps' = tps0
      [j1 := (⌊numlist ns @ canrepr n⌋, Suc (nllength ns) + nlength n),
       j2 := (⌊n⌋⇩N, Suc (nlength n))]"
  shows "transforms tm2 tps0 ttt tps'"
  unfolding tm2_def
proof (tform tps: jk tps0)
  let ?tps = "tps0[j1 := nltape ns]"
  have j1: "?tps ! j1 = nltape ns"
    by (simp add: jk)
  have j2: "?tps ! j2 = (⌊n⌋⇩N, 1)"
    using tps0 jk by simp
  show "rneigh (tps0[j1 := nltape ns] ! j2) {0} (nlength n)"
  proof (rule rneighI)
    show "(?tps ::: j2) (?tps :#: j2 + nlength n) ∈ {0}"
      using j2 contents_outofbounds by simp
    show "⋀i. i < nlength n ⟹ (?tps ::: j2) (?tps :#: j2 + i) ∉ {0}"
      using j2 tps0 bit_symbols_canrepr by fastforce
  qed
  show "tps' = tps0
    [j1 := nltape ns,
     j2 := ?tps ! j2 |+| nlength n,
     j1 := implant (?tps ! j2) (?tps ! j1) (nlength n)]"
    (is "_ = ?rhs")
  proof -
    have "implant (?tps ! j2) (?tps ! j1) (nlength n) = implant (⌊n⌋⇩N, 1) (nltape ns) (nlength n)"
      using j1 j2 by simp
    also have "... = (⌊numlist ns @ (take (nlength n) (drop (1 - 1) (canrepr n)))⌋, Suc (length (numlist ns)) + nlength n)"
      using implant_contents nlcontents_def nllength_def by simp
    also have "... = (⌊numlist ns @ canrepr n⌋, Suc (length (numlist ns)) + nlength n)"
      by simp
    also have "... = (⌊numlist ns @ canrepr n⌋, Suc (nllength ns) + nlength n)"
      using nllength_def by simp
    also have "... = tps' ! j1"
      by (metis assms(2) jk(1,2,4) nth_list_update_eq nth_list_update_neq)
    finally have "implant (?tps ! j2) (?tps ! j1) (nlength n) = tps' ! j1" .
    then have "tps' ! j1 = implant (?tps ! j2) (?tps ! j1) (nlength n)"
      by simp
    then have "tps' ! j1 = ?rhs ! j1"
      by (simp add: jk)
    moreover have "tps' ! j2 = ?rhs ! j2"
      using assms(2) jk j2 by simp
    moreover have "tps' ! j = ?rhs ! j" if "j < length tps'" "j ≠ j1" "j ≠ j2" for j
      using that assms(2) by simp
    moreover have "length tps' = length ?rhs"
      using assms(2) by simp
    ultimately show ?thesis
      using nth_equalityI by blast
  qed
  show "ttt = Suc (Suc (nllength ns) - i1) + Suc (nlength n)"
    using assms(1) j1 tps0 i1 by simp
qed

definition "tps3 ≡ tps0
    [j1 := (⌊numlist ns @ canrepr n⌋, Suc (nllength ns) + nlength n)]"

lemma tm3 [transforms_intros]:
  assumes "ttt = 6 + nllength ns - i1 + 2 * nlength n"
  shows "transforms tm3 tps0 ttt tps3"
  unfolding tm3_def
proof (tform tps: jk k)
  let ?tp1 = "(⌊numlist ns @ canrepr n⌋, Suc (nllength ns) + nlength n)"
  let ?tp2 = "(⌊n⌋⇩N, Suc (nlength n))"
  show "clean_tape (tps0 [j1 := ?tp1, j2 := ?tp2] ! j2)"
    by (simp add: clean_tape_ncontents jk)
  show "tps3 = tps0[j1 := ?tp1, j2 := ?tp2, j2 := tps0 [j1 := ?tp1, j2 := ?tp2] ! j2 |#=| 1]"
    using tps3_def tps0 jk
    by (metis (no_types, lifting) add_Suc fst_conv length_list_update list_update_id list_update_overwrite
      list_update_swap nth_list_update_eq)
  show "ttt =
    3 + nllength ns - i1 + nlength n + (tps0[j1 := ?tp1, j2 := ?tp2] :#: j2 + 2)"
  proof -
    have "tps0[j1 := ?tp1, j2 := ?tp2] :#: j2 = Suc (nlength n)"
      by (simp add: jk)
    then show ?thesis
      using jk tps0 i1 assms(1) by simp
  qed
qed

definition "tps4 = tps0
    [j1 := (⌊numlist (ns @ [n])⌋, Suc (nllength (ns @ [n])))]"

lemma tm4:
  assumes "ttt = 7 + nllength ns - i1 + 2 * nlength n"
  shows "transforms tm4 tps0 ttt tps4"
  unfolding tm4_def
proof (tform tps: jk tps0 tps3_def)
  show "ttt = 6 + nllength ns - i1 + 2 * nlength n + 1 "
      using i1 assms(1) by simp
  show "tps4 = tps3[j1 := tps3 ! j1 |:=| ¦ |+| 1]"
    (is "tps4 = ?tps")
  proof -
    have "?tps = tps0[j1 := (⌊numlist ns @ canrepr n⌋, Suc (nllength ns + nlength n)) |:=| ¦ |+| 1]"
      using tps3_def by (simp add: jk)
    moreover have "(⌊numlist ns @ canrepr n⌋, Suc (nllength ns + nlength n)) |:=| ¦ |+| 1 =
        (⌊numlist (ns @ [n])⌋, Suc (nllength (ns @ [n])))"
      (is "?lhs = ?rhs")
    proof -
      have "?lhs = (⌊numlist ns @ canrepr n⌋(Suc (nllength ns + nlength n) := ¦), Suc (Suc (nllength ns + nlength n)))"
        by simp
      also have "... = (⌊numlist ns @ canrepr n⌋(Suc (nllength ns + nlength n) := ¦), Suc (nllength (ns @ [n])))"
        using nllength_def numlist_def by simp
      also have "... = (⌊(numlist ns @ canrepr n) @ [¦]⌋, Suc (nllength (ns @ [n])))"
        using contents_snoc by (metis length_append nllength_def)
      also have "... = (⌊numlist ns @ canrepr n @ [¦]⌋, Suc (nllength (ns @ [n])))"
        by simp
      also have "... = (⌊numlist (ns @ [n])⌋, Suc (nllength (ns @ [n])))"
        using numlist_def by simp
      finally show "?lhs = ?rhs" .
    qed
    ultimately show ?thesis
      using tps4_def by auto
  qed
qed

end

end  (* locale turing_machine_append *)

lemma tm_append [transforms_intros]:
  fixes j1 j2 :: tapeidx
  fixes tps :: "tape list" and k i1 n :: nat and ns :: "nat list"
  assumes "0 < j1"
  assumes "length tps = k" "j1 < k" "j2 < k" "j1 ≠ j2" "i1 ≤ Suc (nllength ns)"
    and "tps ! j1 = (⌊ns⌋⇩N⇩L, i1)"
    and "tps ! j2 = (⌊n⌋⇩N, 1)"
  assumes "ttt = 7 + nllength ns - i1 + 2 * nlength n"
    and "tps' = tps
      [j1 := nltape (ns @ [n])]"
  shows "transforms (tm_append j1 j2) tps ttt tps'"
proof -
  interpret loc: turing_machine_append j1 j2 .
  show ?thesis
    using loc.tm4 loc.tm4_eq_tm_append loc.tps4_def assms nlcontents_def by simp
qed


subsection ‹Computing the length›

text ‹
The next Turing machine counts the number of terminator symbols $z$ on tape
$j_1$ and stores the result on tape $j_2$. Thus, if $j_1$ contains a list of
numbers, tape $j_2$ will contain the length of the list.
›

definition tm_count :: "tapeidx ⇒ tapeidx ⇒ symbol ⇒ machine" where
  "tm_count j1 j2 z ≡
    WHILE tm_right_until j1 {□, z} ; λrs. rs ! j1 ≠ □ DO
      tm_incr j2 ;;
      tm_right j1
    DONE ;;
    tm_cr j1"

lemma tm_count_tm:
  assumes "0 < j2" and "j1 < k" and "j2 < k" and "j1 ≠ j2" and "G ≥ 4"
  shows "turing_machine k G (tm_count j1 j2 z)"
  unfolding tm_count_def
  using turing_machine_loop_turing_machine tm_right_until_tm tm_incr_tm tm_cr_tm tm_right_tm assms
  by simp

locale turing_machine_count =
  fixes j1 j2 :: tapeidx
begin

definition "tmC ≡ tm_right_until j1 {□, ¦}"
definition "tmB1 ≡ tm_incr j2"
definition "tmB2 ≡ tmB1 ;; tm_right j1"
definition "tmL ≡ WHILE tmC ; λrs. rs ! j1 ≠ □ DO tmB2 DONE"
definition "tm2 ≡ tmL ;; tm_cr j1"

lemma tm2_eq_tm_count: "tm2 = tm_count j1 j2 ¦"
  unfolding tmB1_def tmB2_def tmC_def tmL_def tm2_def tm_count_def
  by simp

context
  fixes tps0 :: "tape list" and k :: nat and ns :: "nat list"
  assumes jk: "j1 < k" "j2 < k" "0 < j2" "j1 ≠ j2" "length tps0 = k"
    and tps0:
      "tps0 ! j1 = (⌊ns⌋⇩N⇩L, 1)"
      "tps0 ! j2 = (⌊0⌋⇩N, 1)"
begin

definition "tpsL t ≡ tps0
  [j1 := (⌊ns⌋⇩N⇩L, Suc (nllength (take t ns))),
   j2 := (⌊t⌋⇩N, 1)]"

definition "tpsC t ≡ tps0
  [j1 := (⌊ns⌋⇩N⇩L, if t < length ns then nllength (take (Suc t) ns) else Suc (nllength ns)),
   j2 := (⌊t⌋⇩N, 1)]"

lemma tmC:
  assumes "t ≤ length ns"
    and "ttt = Suc (if t = length ns then 0 else nlength (ns ! t))"
  shows "transforms tmC (tpsL t) ttt (tpsC t)"
  unfolding tmC_def
proof (tform tps: jk tpsL_def tpsC_def)
  let ?n = "if t = length ns then 0 else nlength (ns ! t)"
  have *: "tpsL t ! j1 = (⌊ns⌋⇩N⇩L, Suc (nllength (take t ns)))"
    using tpsL_def jk by simp
  show "rneigh (tpsL t ! j1) {□, ¦} ?n"
  proof (cases "t = length ns")
    case True
    then have "tpsL t ! j1 = (⌊ns⌋⇩N⇩L, Suc (nllength ns))" (is "_ = ?tp")
      using * by simp
    moreover from this have "fst ?tp (snd ?tp) ∈ {□, ¦}"
      by (simp add: nlcontents_def nllength_def)
    moreover have "?n = 0"
      using True by simp
    ultimately show ?thesis
      using rneighI by simp
  next
    case False
    then have "tpsL t ! j1 = (⌊ns⌋⇩N⇩L, Suc (nllength (take t ns)))"
      using * by simp
    moreover have "?n = nlength (ns ! t)"
      using False by simp
    ultimately show ?thesis
      using nlcontents_rneigh_04 by (simp add: False assms(1) le_neq_implies_less)
  qed
  show "tpsC t = (tpsL t) [j1 := tpsL t ! j1 |+| (if t = length ns then 0 else nlength (ns ! t))]"
    (is "?l = ?r")
  proof (rule nth_equalityI)
    show "length ?l = length ?r"
      using tpsC_def tpsL_def by simp
    show "?l ! i = ?r ! i" if "i < length ?l" for i
    proof -
      consider "i = j1" | "i = j2" | "i ≠ j1 ∧ i ≠ j2"
        by auto
      then show ?thesis
      proof (cases)
        case 1
        show ?thesis
        proof (cases "t = length ns")
          case True
          then show ?thesis
            using 1 by (simp add: jk(2,4) tpsC_def tpsL_def)
        next
          case False
          then have "t < length ns"
            using assms(1) by simp
          then show ?thesis
            using 1 nllength_take_Suc jk tpsC_def tpsL_def by simp
        qed
      next
        case 2
        then show ?thesis
          by (simp add: jk(2,4,5) tpsC_def tpsL_def)
      next
        case 3
        then show ?thesis
          by (simp add: jk(2,4) tpsC_def tpsL_def)
      qed
    qed
  qed
  show "ttt = Suc (if t = length ns then 0 else nlength (ns ! t))"
    using assms(2) .
qed

lemma tmC' [transforms_intros]:
  assumes "t ≤ length ns"
  shows "transforms tmC (tpsL t) (Suc (nllength ns)) (tpsC t)"
proof -
  have "Suc (if t = length ns then 0 else nlength (ns ! t)) ≤ Suc (if t = length ns then 0 else nllength ns)"
    using assms member_le_nllength by simp
  then have "Suc (if t = length ns then 0 else nlength (ns ! t)) ≤ Suc (nllength ns)"
    by auto
  then show ?thesis
    using tmC transforms_monotone assms by metis
qed

definition "tpsB1 t ≡ tps0
  [j1 := (⌊ns⌋⇩N⇩L, nllength (take (Suc t) ns)),
   j2 := (⌊Suc t⌋⇩N, 1)]"

lemma tmB1 [transforms_intros]:
  assumes "t < length ns" and "ttt = 5 + 2 * nlength t"
  shows "transforms tmB1 (tpsC t) ttt (tpsB1 t)"
  unfolding tmB1_def by (tform tps: jk tpsC_def tpsB1_def assms)

definition "tpsB2 t ≡ tps0
  [j1 := (⌊ns⌋⇩N⇩L, Suc (nllength (take (Suc t) ns))),
   j2 := (⌊Suc t⌋⇩N, 1)]"

lemma tmB2:
  assumes "t < length ns" and "ttt = 6 + 2 * nlength t"
  shows "transforms tmB2 (tpsC t) ttt (tpsB2 t)"
  unfolding tmB2_def by (tform tps: jk tpsB1_def tpsB2_def assms)

lemma tpsB2_eq_tpsL: "tpsB2 t = tpsL (Suc t)"
  using tpsB2_def tpsL_def by simp

lemma tmB2' [transforms_intros]:
  assumes "t < length ns"
  shows "transforms tmB2 (tpsC t) (6 + 2 * nllength ns) (tpsL (Suc t))"
proof -
  have "nlength t ≤ nllength ns"
    using assms(1) length_le_nllength nlength_le_n by (meson le_trans less_or_eq_imp_le)
  then have "6 + 2 * nlength t ≤ 6 + 2 * nllength ns"
    by simp
  then show ?thesis
    using assms tmB2 transforms_monotone tpsB2_eq_tpsL by metis
qed

lemma tmL [transforms_intros]:
  assumes "ttt = 13 * nllength ns ^ 2 + 2"
  shows "transforms tmL (tpsL 0) ttt (tpsC (length ns))"
  unfolding tmL_def
proof (tform)
  show "read (tpsC t) ! j1 ≠ □" if "t < length ns" for t
  proof -
    have "tpsC t ! j1 = (⌊ns⌋⇩N⇩L, if t < length ns then nllength (take (Suc t) ns) else Suc (nllength ns))"
      using tpsC_def jk by simp
    then have *: "tpsC t ! j1 = (⌊ns⌋⇩N⇩L, nllength (take (Suc t) ns))" (is "_ = ?tp")
      using that by simp
    have "fst ?tp (snd ?tp) = ⌊ns⌋⇩N⇩L (nllength (take (Suc t) ns))"
      by simp
    also have "... = ⌊numlist ns⌋ (nllength (take (Suc t) ns))"
      using nlcontents_def by simp
    also have "... = numlist ns ! (nllength (take (Suc t) ns) - 1)"
      using nllength that contents_inbounds nllength_def nllength_take nllength_take_Suc
      by (metis Suc_leI add_Suc_right less_nat_zero_code not_less_eq)
    also have "... = 4"
      using numlist_take_Suc_at_term[OF that] by simp
    finally have "fst ?tp (snd ?tp) = ¦" .
    then have "fst ?tp (snd ?tp) ≠ □"
      by simp
    then show ?thesis
      using * jk(1,5) length_list_update tapes_at_read' tpsC_def by metis
  qed
  show "¬ read (tpsC (length ns)) ! j1 ≠ □"
  proof -
    have "tpsC (length ns) ! j1 = (⌊ns⌋⇩N⇩L, Suc (nllength ns))" (is "_ = ?tp")
      using tpsC_def jk by simp
    moreover have "fst ?tp (snd ?tp) = 0"
      by (simp add: nlcontents_def nllength_def)
    ultimately have "read (tpsC (length ns)) ! j1 = □"
      using jk(1,5) length_list_update tapes_at_read' tpsC_def by metis
    then show ?thesis
      by simp
  qed
  show "length ns * (Suc (nllength ns) + (6 + 2 * nllength ns) + 2) + Suc (nllength ns) + 1 ≤ ttt"
  proof -
    have "length ns * (Suc (nllength ns) + (6 + 2 * nllength ns) + 2) + Suc (nllength ns) + 1 =
        length ns * (9 + 3 * nllength ns) + nllength ns + 2"
      by simp
    also have "... ≤ nllength ns * (9 + 3 * nllength ns) + nllength ns + 2"
      by (simp add: length_le_nllength)
    also have "... = nllength ns * (10 + 3 * nllength ns) + 2"
      by algebra
    also have "... = 10 * nllength ns + 3 * nllength ns ^ 2 + 2"
      by algebra
    also have "... ≤ 10 * nllength ns ^ 2 + 3 * nllength ns ^ 2 + 2"
      by (meson add_mono_thms_linordered_semiring(1) le_eq_less_or_eq mult_le_mono2 power2_nat_le_imp_le)
    also have "... = 13 * nllength ns ^ 2 + 2"
      by simp
    finally show ?thesis
      using assms by simp
  qed
qed

definition "tps2 ≡ tps0
  [j2 := (⌊length ns⌋⇩N, 1)]"

lemma tm2:
  assumes "ttt = 13 * nllength ns ^ 2 + 5 + nllength ns"
  shows "transforms tm2 (tpsL 0) ttt tps2"
  unfolding tm2_def
proof (tform tps: jk tpsC_def tps2_def)
  have *: "tpsC (length ns) ! j1 = (⌊ns⌋⇩N⇩L, Suc (nllength ns))"
    using jk tpsC_def by simp
  then show "clean_tape (tpsC (length ns) ! j1)"
    by (simp add: clean_tape_nlcontents)
  show "tps2 = (tpsC (length ns))[j1 := tpsC (length ns) ! j1 |#=| 1]"
    using jk tps0(1) tps2_def tpsC_def * by (metis fstI list_update_id list_update_overwrite list_update_swap)
  show "ttt = 13 * (nllength ns)⇧2 + 2 + (tpsC (length ns) :#: j1 + 2)"
    using assms * by simp
qed

lemma tpsL_eq_tps0: "tpsL 0 = tps0"
  using tpsL_def tps0 by (metis One_nat_def list_update_id nllength_Nil take0)

lemma tm2':
  assumes "ttt = 14 * nllength ns ^ 2 + 5"
  shows "transforms tm2 tps0 ttt tps2"
proof -
  have "nllength ns ≤ nllength ns ^ 2"
    using power2_nat_le_imp_le by simp
  then have "13 * nllength ns ^ 2 + 5 + nllength ns ≤ ttt"
    using assms by simp
  then show ?thesis
    using assms tm2 transforms_monotone tpsL_eq_tps0 by simp
qed

end  (* context tps0 *)

end  (* locale *)

lemma transforms_tm_count_4I [transforms_intros]:
  fixes j1 j2 :: tapeidx
  fixes tps tps' :: "tape list" and k :: nat and ns :: "nat list"
  assumes "j1 < k" "j2 < k" "0 < j2" "j1 ≠ j2" "length tps = k"
  assumes
    "tps ! j1 = (⌊ns⌋⇩N⇩L, 1)"
    "tps ! j2 = (⌊0⌋⇩N, 1)"
  assumes "ttt = 14 * nllength ns ^ 2 + 5"
  assumes "tps' = tps[j2 := (⌊length ns⌋⇩N, 1)]"
  shows "transforms (tm_count j1 j2 ¦) tps ttt tps'"
proof -
  interpret loc: turing_machine_count j1 j2 .
  show ?thesis
    using loc.tm2_eq_tm_count loc.tm2' loc.tps2_def assms by simp
qed


subsection ‹Extracting the $n$-th element›

text ‹
The next Turing machine expects a list on tape $j_1$ and an index $i$ on $j_2$
and writes the $i$-th element of the list to $j_2$, overwriting $i$.  The TM
does not terminate for out-of-bounds access, which of course we will never
attempt. Again the parameter $z$ is a generic terminator symbol.
›

definition tm_nth_inplace :: "tapeidx ⇒ tapeidx ⇒ symbol ⇒ machine" where
  "tm_nth_inplace j1 j2 z ≡
    WHILE [] ; λrs. rs ! j2 ≠ □ DO
      tm_decr j2 ;;
      tm_right_until j1 {z} ;;
      tm_right j1
    DONE ;;
    tm_cp_until j1 j2 {z} ;;
    tm_cr j2 ;;
    tm_cr j1"

lemma tm_nth_inplace_tm:
  assumes "k ≥ 2" and "G ≥ 4" and "0 < j2" and "j1 < k" and "j2 < k"
  shows "turing_machine k G (tm_nth_inplace j1 j2 ¦)"
  unfolding tm_nth_inplace_def
  using assms tm_decr_tm tm_right_until_tm tm_right_tm tm_cp_until_tm tm_cr_tm Nil_tm
  by (simp add: assms(1) turing_machine_loop_turing_machine)

locale turing_machine_nth_inplace =
  fixes j1 j2 :: tapeidx
begin

definition "tmL1 ≡ tm_decr j2"
definition "tmL2 ≡ tmL1 ;; tm_right_until j1 {¦}"
definition "tmL3 ≡ tmL2 ;; tm_right j1"
definition "tmL ≡ WHILE [] ; λrs. rs ! j2 ≠ □ DO tmL3 DONE"
definition "tm2 ≡ tmL ;; tm_cp_until j1 j2 {¦}"
definition "tm3 ≡ tm2 ;; tm_cr j2"
definition "tm4 ≡ tm3 ;; tm_cr j1"

lemma tm4_eq_tm_nth_inplace: "tm4 = tm_nth_inplace j1 j2 ¦"
  unfolding tmL1_def tmL2_def tmL3_def tmL_def tm2_def tm3_def tm4_def tm_nth_inplace_def
  by simp

context
  fixes tps0 :: "tape list" and k idx :: nat and ns :: "nat list"
  assumes jk: "j1 < k" "j2 < k" "0 < j2" "j1 ≠ j2" "length tps0 = k"
    and idx: "idx < length ns"
    and tps0:
      "tps0 ! j1 = (⌊ns⌋⇩N⇩L, 1)"
      "tps0 ! j2 = (⌊idx⌋⇩N, 1)"
begin

definition "tpsL t ≡ tps0
  [j1 := (⌊ns⌋⇩N⇩L, Suc (nllength (take t ns))),
   j2 := (⌊idx - t⌋⇩N, 1)]"

definition "tpsL1 t ≡ tps0
  [j1 := (⌊ns⌋⇩N⇩L, Suc (nllength (take t ns))),
   j2 := (⌊idx - t - 1⌋⇩N, 1)]"

lemma tmL1 [transforms_intros]:
  assumes "ttt = 8 + 2 * nlength (idx - t)"
  shows "transforms tmL1 (tpsL t) ttt (tpsL1 t)"
  unfolding tmL1_def by (tform tps: tpsL_def tpsL1_def jk time: assms)

definition "tpsL2 t ≡ tps0
  [j1 := (⌊ns⌋⇩N⇩L, nllength (take (Suc t) ns)),
   j2 := (⌊idx - t - 1⌋⇩N, 1)]"

lemma tmL2:
  assumes "t < length ns" and "ttt = 8 + 2 * nlength (idx - t) + Suc (nlength (ns ! t))"
  shows "transforms tmL2 (tpsL t) ttt (tpsL2 t)"
  unfolding tmL2_def
proof (tform tps: jk tpsL1_def tpsL2_def time: assms(2))
  let ?l = "nlength (ns ! t)"
  show "rneigh (tpsL1 t ! j1) {¦} ?l"
  proof -
    have "tpsL1 t ! j1 = (⌊ns⌋⇩N⇩L, Suc (nllength (take t ns)))"
      using tpsL1_def jk by (simp only: nth_list_update_eq nth_list_update_neq)
    then show ?thesis
      using assms(1) nlcontents_rneigh_4 by simp
  qed
  show "tpsL2 t = (tpsL1 t)[j1 := tpsL1 t ! j1 |+| nlength (ns ! t)]"
    (is "?l = ?r")
  proof (rule nth_equalityI)
    show len: "length ?l = length ?r"
      using tpsL1_def tpsL2_def jk by simp
    show "?l ! i = ?r ! i" if "i < length ?l" for i
    proof -
      consider "i = j1" | "i = j2" | "i ≠ j1 ∧ i ≠ j2"
        by auto
      then show ?thesis
      proof (cases)
        case 1
        then show ?thesis
          using that tpsL1_def tpsL2_def jk nllength_take_Suc[OF assms(1)] by simp
      next
        case 2
        then show ?thesis
          using that tpsL1_def tpsL2_def jk
          by (simp only: nth_list_update_eq nth_list_update_neq' length_list_update)
      next
        case 3
        then show ?thesis
          using that tpsL1_def tpsL2_def jk
          by (simp only: nth_list_update_eq jk nth_list_update_neq' length_list_update)
      qed
    qed
  qed
qed

lemma tmL2' [transforms_intros]:
  assumes "t < length ns" and "ttt = 9 + 2 * nlength idx + nlength (Max (set ns))"
  shows "transforms tmL2 (tpsL t) ttt (tpsL2 t)"
proof -
  let ?ttt = "8 + 2 * nlength (idx - t) + Suc (nlength (ns ! t))"
  have "transforms tmL2 (tpsL t) ?ttt (tpsL2 t)"
    using tmL2 assms by simp
  moreover have "ttt ≥ ?ttt"
  proof -
    have "nlength (idx - t) ≤ nlength idx"
      using nlength_mono by simp
    moreover have "nlength (ns ! t) ≤ nlength (Max (set ns))"
      using nlength_mono assms by simp
    ultimately show ?thesis
      using assms(2) by simp
  qed
  ultimately show ?thesis
    using transforms_monotone by simp
qed

definition "tpsL3 t ≡ tps0
  [j1 := (⌊ns⌋⇩N⇩L, Suc (nllength (take (Suc t) ns))),
   j2 := (⌊idx - t - 1⌋⇩N, 1)]"

lemma tmL3:
  assumes "t < length ns" and "ttt = 10 + 2 * nlength idx + nlength (Max (set ns))"
  shows "transforms tmL3 (tpsL t) ttt (tpsL3 t)"
  unfolding tmL3_def
proof (tform tps: jk tpsL2_def tpsL3_def assms(1) time: assms(2))
  show "tpsL3 t = (tpsL2 t)[j1 := tpsL2 t ! j1 |+| 1]"
    using tpsL3_def tpsL2_def jk tps0
    by (metis Groups.add_ac(2) fst_conv list_update_overwrite list_update_swap nth_list_update nth_list_update_neq
      plus_1_eq_Suc snd_conv)
qed

lemma tpsL3_eq_tpsL: "tpsL3 t = tpsL (Suc t)"
  using tpsL3_def tpsL_def by simp

lemma tmL:
  assumes "ttt = idx * (12 + 2 * nlength idx + nlength (Max (set ns))) + 1"
  shows "transforms tmL (tpsL 0) ttt (tpsL idx)"
  unfolding tmL_def
proof (tform)
  let ?t = "10 + 2 * nlength idx + nlength (Max (set ns))"
  show "⋀t. t < idx ⟹ transforms tmL3 (tpsL t) ?t (tpsL (Suc t))"
    using tmL3 tpsL3_eq_tpsL idx by simp
  show "read (tpsL t) ! j2 ≠ □" if "t < idx" for t
  proof -
    have "tpsL t ! j2 = (⌊idx - t⌋⇩N, 1)"
      using tpsL_def jk by simp
    then have "read (tpsL t) ! j2 = ⌊idx - t⌋⇩N 1"
      using tapes_at_read' jk tpsL_def by (metis fst_conv length_list_update snd_conv)
    moreover have "idx - t > 0"
      using that by simp
    ultimately show "read (tpsL t) ! j2 ≠ □"
      using ncontents_1_blank_iff_zero by simp
  qed
  show "¬ read (tpsL idx) ! j2 ≠ □"
  proof -
    have "tpsL idx ! j2 = (⌊idx - idx⌋⇩N, 1)"
      using tpsL_def jk by simp
    then have "read (tpsL idx) ! j2 = ⌊idx - idx⌋⇩N 1"
      using tapes_at_read' jk tpsL_def by (metis fst_conv length_list_update snd_conv)
    then show ?thesis
      using ncontents_1_blank_iff_zero by simp
  qed
  show "idx * (10 + 2 * nlength idx + nlength (Max (set ns)) + 2) + 1 ≤ ttt"
    using assms by simp
qed

definition "tps1 ≡ tps0
  [j1 := (⌊ns⌋⇩N⇩L, Suc (nllength (take idx ns))),
   j2 := (⌊0⌋⇩N, 1)]"

lemma tps1_eq_tpsL: "tps1 = tpsL idx"
  using tps1_def tpsL_def by simp

lemma tps0_eq_tpsL: "tps0 = tpsL 0"
  using tps0 tpsL_def nllength_Nil by (metis One_nat_def list_update_id minus_nat.diff_0 take0)

lemma tmL' [transforms_intros]:
  assumes "ttt = idx * (12 + 2 * nlength idx + nlength (Max (set ns))) + 1"
  shows "transforms tmL tps0 ttt tps1"
  using tmL assms tps0_eq_tpsL tps1_eq_tpsL by simp

definition "tps2 ≡ tps0
  [j1 := (⌊ns⌋⇩N⇩L, nllength (take (Suc idx) ns)),
   j2 := (⌊ns ! idx⌋⇩N, Suc (nlength (ns ! idx)))]"

lemma tm2 [transforms_intros]:
  assumes "ttt = idx * (12 + 2 * nlength idx + nlength (Max (set ns))) + 2 + nlength (ns ! idx)"
  shows "transforms tm2 tps0 ttt tps2"
  unfolding tm2_def
proof (tform tps: jk tps2_def tps1_def time: assms)
  have "tps1 ! j1 = (⌊ns⌋⇩N⇩L, Suc (nllength (take idx ns)))"
    using tps1_def tps0 jk by simp
  then show "rneigh (tps1 ! j1) {¦} (nlength (ns ! idx))"
    by (simp add: idx nlcontents_rneigh_4)
  show "tps2 = tps1
    [j1 := tps1 ! j1 |+| nlength (ns ! idx),
     j2 := implant (tps1 ! j1) (tps1 ! j2) (nlength (ns ! idx))]"
     (is "?l = ?r")
  proof (rule nth_equalityI)
    show len: "length ?l = length ?r"
      using tps1_def tps2_def by simp
    show "?l ! i = ?r ! i" if "i < length ?l" for i
    proof -
      consider "i = j1" | "i = j2" | "i ≠ j1 ∧ i ≠ j2"
        by auto
      then show ?thesis
      proof (cases)
        case 1
        then show ?thesis
          using that tps1_def tps2_def jk nllength_take_Suc idx by simp
      next
        case 2
        then have lhs: "?l ! i = (⌊ns ! idx⌋⇩N, Suc (nlength (ns ! idx)))"
          using tps2_def jk by simp
        let ?i = "Suc (nllength (take idx ns))"
        have i1: "?i > 0"
          by simp
        have "nlength (ns ! idx) + (?i - 1) ≤ nllength ns"
          using idx by (simp add: add.commute less_or_eq_imp_le nllength_take)
        then have i2: "nlength (ns ! idx) + (?i - 1) ≤ length (numlist ns)"
          using nllength_def by simp
        have "?r ! i = implant (tps1 ! j1) (tps1 ! j2) (nlength (ns ! idx))"
          using 2 tps1_def jk by simp
        also have "... = implant (⌊ns⌋⇩N⇩L, ?i) (⌊0⌋⇩N, 1) (nlength (ns ! idx))"
        proof -
          have "tps1 ! j1 = (⌊ns⌋⇩N⇩L, Suc (nllength (take idx ns)))"
            using tps1_def jk by simp
          moreover have "tps1 ! j2 = (⌊0⌋⇩N, 1)"
            using tps1_def jk by simp
          ultimately show ?thesis
            by simp
        qed
        also have "... = (⌊[] @ (take (nlength (ns ! idx)) (drop (?i - 1) (numlist ns)))⌋, Suc (length []) + nlength (ns ! idx))"
          using implant_contents[OF i1 i2] by (metis One_nat_def list.size(3) ncontents_0 nlcontents_def)
        finally have "?r ! i = (⌊[] @ (take (nlength (ns ! idx)) (drop (?i - 1) (numlist ns)))⌋, Suc (length []) + nlength (ns ! idx))" .
        then have "?r ! i = (⌊take (nlength (ns ! idx)) (drop (nllength (take idx ns)) (numlist ns))⌋, Suc (nlength (ns ! idx)))"
          by simp
        then have "?r ! i = (⌊canrepr (ns ! idx)⌋, Suc (nlength (ns ! idx)))"
          using take_drop_numlist'[OF idx] by simp
        then show ?thesis
          using lhs by simp
      next
        case 3
        then show ?thesis
          using that tps1_def tps2_def jk by simp
      qed
    qed
  qed
qed

definition "tps3 ≡ tps0
  [j1 := (⌊ns⌋⇩N⇩L, nllength (take (Suc idx) ns)),
   j2 := (⌊ns ! idx⌋⇩N, 1)]"

lemma tm3 [transforms_intros]:
  assumes "ttt = idx * (12 + 2 * nlength idx + nlength (Max (set ns))) + 5 + 2 * nlength (ns ! idx)"
  shows "transforms tm3 tps0 ttt tps3"
  unfolding tm3_def
  by (tform tps: clean_tape_ncontents jk tps2_def tps3_def time: assms tps2_def jk)

definition "tps4 ≡ tps0
  [j2 := (⌊ns ! idx⌋⇩N, 1)]"

lemma tm4:
  assumes "ttt = idx * (12 + 2 * nlength idx + nlength (Max (set ns))) + 7 + 2 * nlength (ns ! idx) + nllength (take (Suc idx) ns)"
  shows "transforms tm4 tps0 ttt tps4"
  unfolding tm4_def
proof (tform tps: clean_tape_nlcontents jk tps3_def tps4_def time: assms jk tps3_def)
  show "tps4 = tps3[j1 := tps3 ! j1 |#=| 1]"
    using tps4_def tps3_def jk tps0(1) list_update_id[of tps0 j1] by (simp add: list_update_swap)
qed

lemma tm4':
  assumes "ttt = 18 * nllength ns ^ 2 + 12"
  shows "transforms tm4 tps0 ttt tps4"
proof -
  let ?ttt = "idx * (12 + 2 * nlength idx + nlength (Max (set ns))) + 7 + 2 * nlength (ns ! idx) + nllength (take (Suc idx) ns)"

  have 1: "idx ≤ nllength ns"
    using idx length_le_nllength by (meson le_trans less_or_eq_imp_le)
  then have 2: "nlength idx ≤ nllength ns"
    using nlength_mono nlength_le_n by (meson dual_order.trans)
  have "ns ≠ []"
    using idx by auto
  then have 3: "nlength (Max (set ns)) ≤ nllength ns"
    using member_le_nllength by simp
  have 4: "nlength (ns ! idx) ≤ nllength ns"
    using idx member_le_nllength by simp
  have 5: "nllength (take (Suc idx) ns) ≤ nllength ns"
    by (metis Suc_le_eq add_Suc_right idx nllength_take nllength_take_Suc)

  have "?ttt ≤ idx * (12 + 2 * nllength ns + nllength ns) + 7 + 2 * nllength ns + nllength ns"
    using 2 3 4 5 by (meson add_le_mono le_eq_less_or_eq mult_le_mono2)
  also have "... = idx * (12 + 3 * nllength ns) + 7 + 3 * nllength ns"
    by simp
  also have "... ≤ idx * (12 + 3 * nllength ns) + (12 + 3 * nllength ns)"
    by simp
  also have "... = Suc idx * (12 + 3 * nllength ns)"
    by simp
  also have "... ≤ Suc (nllength ns) * (12 + 3 * nllength ns)"
    using 1 by simp
  also have "... = nllength ns * (12 + 3 * nllength ns) + (12 + 3 * nllength ns)"
    by simp
  also have "... = 12 * nllength ns + 3 * nllength ns ^ 2 + 12 + 3 * nllength ns"
    by algebra
  also have "... = 15 * nllength ns + 3 * nllength ns ^ 2 + 12"
    by simp
  also have "... ≤ 18 * nllength ns ^ 2 + 12"
    by (simp add: power2_eq_square)
  finally have "?ttt ≤ 18 * nllength ns ^ 2 + 12" .
  then show ?thesis
    using tm4 transforms_monotone assms by simp
qed

end  (* context tps0 *)

end  (* locale turing_machine_nth_inplace *)

lemma transforms_tm_nth_inplace_4I [transforms_intros]:
  fixes j1 j2 :: tapeidx
  fixes tps tps' :: "tape list" and k idx :: nat and ns :: "nat list"
  assumes "j1 < k" "j2 < k" "0 < j2" "j1 ≠ j2" "length tps = k"
    and "idx < length ns"
  assumes
    "tps ! j1 = (⌊ns⌋⇩N⇩L, 1)"
    "tps ! j2 = (⌊idx⌋⇩N, 1)"
  assumes "ttt = 18 * nllength ns ^ 2 + 12"
  assumes "tps' = tps
    [j2 := (⌊ns ! idx⌋⇩N, 1)]"
  shows "transforms (tm_nth_inplace j1 j2 ¦) tps ttt tps'"
proof -
  interpret loc: turing_machine_nth_inplace j1 j2 .
  show ?thesis
    using assms loc.tm4_eq_tm_nth_inplace loc.tm4' loc.tps4_def by simp
qed

text ‹
The next Turing machine expects a list on tape $j_1$ and an index $i$ on tape
$j_2$. It writes the $i$-th element of the list to tape $j_3$. Like the previous
TM, it will not terminate on out-of-bounds access, and $z$ is a parameter for
the symbol that terminates the list elements.
›

definition tm_nth :: "tapeidx ⇒ tapeidx ⇒ tapeidx ⇒ symbol ⇒ machine" where
  "tm_nth j1 j2 j3 z ≡
    tm_copyn j2 j3 ;;
    tm_nth_inplace j1 j3 z"

lemma tm_nth_tm:
  assumes "k ≥ 2" and "G ≥ 4" and "0 < j2" "0 < j1" "j1 < k" "j2 < k" "0 < j3" "j3 < k" "j2 ≠ j3"
  shows "turing_machine k G (tm_nth j1 j2 j3 ¦)"
  unfolding tm_nth_def using tm_copyn_tm tm_nth_inplace_tm assms by simp

lemma transforms_tm_nth_4I [transforms_intros]:
  fixes j1 j2 j3 :: tapeidx
  fixes tps tps' :: "tape list" and k idx :: nat and ns :: "nat list"
  assumes "j1 < k" "j2 < k" "j3 < k" "0 < j1" "0 < j2" "0 < j3" "j1 ≠ j2" "j2 ≠ j3" "j1 ≠ j3"
    and "length tps = k"
    and "idx < length ns"
  assumes
    "tps ! j1 = (⌊ns⌋⇩N⇩L, 1)"
    "tps ! j2 = (⌊idx⌋⇩N, 1)"
    "tps ! j3 = (⌊0⌋⇩N, 1)"
  assumes "ttt = 21 * nllength ns ^ 2 + 26"
  assumes "tps' = tps
    [j3 := (⌊ns ! idx⌋⇩N, 1)]"
  shows "transforms (tm_nth j1 j2 j3 ¦) tps ttt tps'"
proof -
  let ?ttt = "14 + 3 * (nlength idx + nlength 0) + (18 * (nllength ns)⇧2 + 12)"
  have "transforms (tm_nth j1 j2 j3 ¦) tps ?ttt tps'"
    unfolding tm_nth_def
  proof (tform tps: assms(1-11))
    show "tps ! j2 = (⌊idx⌋⇩N, 1)"
      using assms by simp
    show "tps ! j3 = (⌊0⌋⇩N, 1)"
      using assms by simp
    show "tps[j3 := (⌊idx⌋⇩N, 1)] ! j1 = (⌊ns⌋⇩N⇩L, 1)"
      using assms by simp
    then show "tps' = tps
      [j3 := (⌊idx⌋⇩N, 1),
       j3 := (⌊ns ! idx⌋⇩N, 1)]"
      using assms by (metis One_nat_def list_update_overwrite)
  qed
  moreover have "?ttt ≤ ttt"
  proof -
    have "nlength idx ≤ idx"
      using nlength_le_n by simp
    then have "nlength idx ≤ length ns"
      using assms(11) by simp
    then have "nlength idx ≤ nllength ns"
      using length_le_nllength by (meson order.trans)
    then have "nlength idx ≤ nllength ns ^ 2"
      by (meson