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 (z3) 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