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 ::  where
"numlist ns  concat (map (λn. canrepr n @ [¦]) ns)"

lemma numlist_Nil:
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 = (nns. Suc (nlength n))"
using nllength_def numlist_def by (induction ns) simp_all

lemma nllength_Nil [simp]:
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 "nset ns. n  N"
shows "nllength ns  Suc (nlength N) * length ns"
proof -
have "nllength ns = (nns. 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  (nns. Suc (nlength N))"
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)"
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"
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)"
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)"
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)" ("_NL") where
"nsNL  numlist ns"

lemma clean_tape_nlcontents: "clean_tape (nsNL, i)"

lemma nlcontents_Nil:
using nlcontents_def by (simp add: numlist_Nil)

lemma nlcontents_rneigh_4:
assumes "i < length ns"
shows "rneigh (nsNL, Suc (nllength (take i ns))) {¦} (nlength (ns ! i))"
proof (rule rneighI)
let ?tp = "(nsNL, 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 (nsNL, Suc (nllength (take i ns))) {, ¦} (nlength (ns ! i))"
proof (rule rneighI)
let ?tp = "(nsNL, 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  (nsNL, 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  (nsNL, 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  (nsNL, Suc (nllength ns))"
using that by simp
then show ?thesis
using nlcontents_def contents_outofbounds nllength_def
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
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 ::  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 = (dummyN, 1)"
begin

definition "tps1  tps0[j2 := (0N, 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 := (nsNL, nllength (take (Suc idx) ns)),
j2 := (ns ! idxN, 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 ! idxN, 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"
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 (nsNL, ?i) (0N, 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 := (nsNL, nllength (take (Suc idx) ns)),
j2 := (ns ! idxN, 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 ! idxN, 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 = (dummyN, 1)"
assumes "ttt = 12 + 2 * nlength dummy + 2 * (nlength (ns ! idx))"
assumes "tps' = tps
[j1 := nltape' ns (Suc idx),
j2 := (ns ! idxN, 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 ::  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 = (nsNL, i1)"
"tps0 ! j2 = (nN, 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 := (nN, 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"
have j2: "?tps ! j2 = (nN, 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 (nN, 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"
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 = "(nN, Suc (nlength n))"
show "clean_tape (tps0 [j1 := ?tp1, j2 := ?tp2] ! j2)"
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)"
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 = (nsNL, i1)"
and "tps ! j2 = (nN, 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 ::  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 = (nsNL, 1)"
"tps0 ! j2 = (0N, 1)"
begin

definition "tpsL t  tps0
[j1 := (nsNL, Suc (nllength (take t ns))),
j2 := (tN, 1)]"

definition "tpsC t  tps0
[j1 := (nsNL, if t < length ns then nllength (take (Suc t) ns) else Suc (nllength ns)),
j2 := (tN, 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 = (nsNL, 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 = (nsNL, Suc (nllength ns))" (is "_ = ?tp")
using * by simp
moreover from this have "fst ?tp (snd ?tp)  {, ¦}"
moreover have "?n = 0"
using True by simp
ultimately show ?thesis
using rneighI by simp
next
case False
then have "tpsL t ! j1 = (nsNL, 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 := (nsNL, nllength (take (Suc t) ns)),
j2 := (Suc tN, 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 := (nsNL, Suc (nllength (take (Suc t) ns))),
j2 := (Suc tN, 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 = (nsNL, 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 = (nsNL, nllength (take (Suc t) ns))" (is "_ = ?tp")
using that by simp
have "fst ?tp (snd ?tp) = nsNL (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 = (nsNL, Suc (nllength ns))" (is "_ = ?tp")
using tpsC_def jk by simp
moreover have "fst ?tp (snd ?tp) = 0"
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"
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 nsN, 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 = (nsNL, Suc (nllength ns))"
using jk tpsC_def by simp
then show "clean_tape (tpsC (length ns) ! j1)"
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 = (nsNL, 1)"
"tps ! j2 = (0N, 1)"
assumes "ttt = 14 * nllength ns ^ 2 + 5"
assumes "tps' = tps[j2 := (length nsN, 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 ::  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

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 = (nsNL, 1)"
"tps0 ! j2 = (idxN, 1)"
begin

definition "tpsL t  tps0
[j1 := (nsNL, Suc (nllength (take t ns))),
j2 := (idx - tN, 1)]"

definition "tpsL1 t  tps0
[j1 := (nsNL, Suc (nllength (take t ns))),
j2 := (idx - t - 1N, 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 := (nsNL, nllength (take (Suc t) ns)),
j2 := (idx - t - 1N, 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 = (nsNL, 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 := (nsNL, Suc (nllength (take (Suc t) ns))),
j2 := (idx - t - 1N, 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 - tN, 1)"
using tpsL_def jk by simp
then have "read (tpsL t) ! j2 = idx - tN 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 - idxN, 1)"
using tpsL_def jk by simp
then have "read (tpsL idx) ! j2 = idx - idxN 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 := (nsNL, Suc (nllength (take idx ns))),
j2 := (0N, 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 := (nsNL, nllength (take (Suc idx) ns)),
j2 := (ns ! idxN, 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 = (nsNL, Suc (nllength (take idx ns)))"
using tps1_def tps0 jk by simp
then show "rneigh (tps1 ! j1) {¦} (nlength (ns ! idx))"
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 ! idxN, 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"
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 (nsNL, ?i) (0N, 1) (nlength (ns ! idx))"
proof -
have "tps1 ! j1 = (nsNL, Suc (nllength (take idx ns)))"
using tps1_def jk by simp
moreover have "tps1 ! j2 = (0N, 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 := (nsNL, nllength (take (Suc idx) ns)),
j2 := (ns ! idxN, 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 ! idxN, 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"
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 = (nsNL, 1)"
"tps ! j2 = (idxN, 1)"
assumes "ttt = 18 * nllength ns ^ 2 + 12"
assumes "tps' = tps
[j2 := (ns ! idxN, 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 ::  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 = (nsNL, 1)"
"tps ! j2 = (idxN, 1)"
"tps ! j3 = (0N, 1)"
assumes "ttt = 21 * nllength ns ^ 2 + 26"
assumes "tps' = tps
[j3 := (ns ! idxN, 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 = (idxN, 1)"
using assms by simp
show "tps ! j3 = (0N, 1)"
using assms by simp
show "tps[j3 := (idxN, 1)] ! j1 = (nsNL, 1)"
using assms by simp
then show "tps' = tps
[j3 := (idxN, 1),
j3 := (ns ! idxN, 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