section ‹Elementary Turing machines\label{s:tm-elementary}› theory Elementary imports Combinations begin text ‹ In this section we devise some simple yet useful Turing machines. We have already fully analyzed the empty TM, where start and halting state coincide, in the lemmas~@{thm [source] computes_Nil_empty}, @{thm [source] Nil_tm}, and @{thm [source] transforms_Nil}. The next more complex TMs are those with exactly one command. They represent TMs with two states: the halting state and the start state where the action happens. This action might last for one step only, or the TM may stay in this state for longer; for example, it can move a tape head rightward to the next blank symbol. We will also start using the @{text ";;"} operator to combine some of the one-command TMs. › text ‹ Most Turing machines we are going to construct throughout this section and indeed the entire article are really families of Turing machines that usually are parameterized by tape indices. › type_synonym tapeidx = nat text ‹ Throughout this article, names of commands are prefixed with @{text cmd_} and names of Turing machines with @{text tm_}. Usually for a TM named @{term tm_foo} there is a lemma @{text tm_foo_tm} stating that it really is a Turing machine and a lemma @{text transforms_tm_fooI} describing its semantics and running time. The lemma usually receives a @{text transforms_intros} attribute for use with our proof method. If @{term "tm_foo"} comprises more than two TMs we will typically analyze the semantics and running time in a locale named @{text "turing_machine_foo"}. The first example of this is @{term tm_equals} in Section~\ref{s:tm-elementary-comparing}. When it comes to running times, we will have almost no scruples simplifying upper bounds to have the form $a + b\cdot n^c$ for some constants $a, b, c$, even if this means, for example, bounding $n \log n$ by $n^2$. › subsection ‹Clean tapes› text ‹ Most of our Turing machines will not change the start symbol in the first cell of a tape nor will they write the start symbol anywhere else. The only exceptions are machines that simulate arbitrary other machines. We call tapes that have the start symbol only in the first cell \emph{clean tapes}. › definition clean_tape :: "tape ⇒ bool" where "clean_tape tp ≡ ∀i. fst tp i = ▹ ⟷ i = 0" lemma clean_tapeI: assumes "⋀i. fst tp i = ▹ ⟷ i = 0" shows "clean_tape tp" unfolding clean_tape_def using assms by simp lemma clean_tapeI': assumes "fst tp 0 = ▹" and "⋀i. i > 0 ⟹ fst tp i ≠ ▹" shows "clean_tape tp" unfolding clean_tape_def using assms by auto text ‹ A clean configuration is one with only clean tapes. › definition clean_config :: "config ⇒ bool" where "clean_config cfg ≡ (∀j<||cfg||. ∀i. (cfg <:> j) i = ▹ ⟷ i = 0)" lemma clean_config_tapes: "clean_config cfg = (∀tp∈set (snd cfg). clean_tape tp)" using clean_config_def clean_tape_def by (metis in_set_conv_nth) lemma clean_configI: assumes "⋀j i. j < length tps ⟹ fst (tps ! j) i = ▹ ⟷ i = 0" shows "clean_config (q, tps)" unfolding clean_config_def using assms by simp lemma clean_configI': assumes "⋀tp i. tp ∈ set tps ⟹ fst tp i = ▹ ⟷ i = 0" shows "clean_config (q, tps)" using clean_configI assms by simp lemma clean_configI'': assumes "⋀tp. tp ∈ set tps ⟹ (fst tp 0 = ▹ ∧ (∀i>0. fst tp i ≠ ▹))" shows "clean_config (q, tps)" using clean_configI' assms by blast lemma clean_configE: assumes "clean_config (q, tps)" shows "⋀j i. j < length tps ⟹ fst (tps ! j) i = ▹ ⟷ i = 0" using clean_config_def assms by simp lemma clean_configE': assumes "clean_config (q, tps)" shows "⋀tp i. tp ∈ set tps ⟹ fst tp i = ▹ ⟷ i = 0" using clean_configE assms by (metis in_set_conv_nth) lemma clean_contents_proper [simp]: "proper_symbols zs ⟹ clean_tape (⌊zs⌋, q)" using clean_tape_def contents_def proper_symbols_ne1 by simp lemma contents_clean_tape': "proper_symbols zs ⟹ fst tp = ⌊zs⌋ ⟹ clean_tape tp" using contents_def clean_tape_def by (simp add: nat_neq_iff) text ‹ Some more lemmas about @{const contents}: › lemma contents_append_blanks: "⌊ys @ replicate m □⌋ = ⌊ys⌋" proof fix i consider "i = 0" | "0 < i ∧ i ≤ length ys" | "length ys < i ∧ i ≤ length ys + m" | "length ys + m < i" by linarith then show "⌊ys @ replicate m □⌋ i = ⌊ys⌋ i" proof (cases) case 1 then show ?thesis by simp next case 2 then show ?thesis using contents_inbounds by (metis (no_types, opaque_lifting) Suc_diff_1 Suc_le_eq le_add1 le_trans length_append nth_append) next case 3 then show ?thesis by (smt (z3) Suc_diff_Suc add_diff_inverse_nat contents_def diff_Suc_1 diff_commute leD less_one less_or_eq_imp_le nat_add_left_cancel_le not_less_eq nth_append nth_replicate) next case 4 then show ?thesis by simp qed qed lemma contents_append_update: assumes "length ys = m" shows "⌊ys @ [v] @ zs⌋(Suc m := w) = ⌊ys @ [w] @ zs⌋" proof fix i consider "i = 0" | "0 < i ∧ i < Suc m" | "i = Suc m" | "i > Suc m ∧ i ≤ Suc m + length zs" | "i > Suc m + length zs" by linarith then show "(⌊ys @ [v] @ zs⌋(Suc m := w)) i = ⌊ys @ [w] @ zs⌋ i" (is "?l = ?r") proof (cases) case 1 then show ?thesis by simp next case 2 then have "?l = (ys @ [v] @ zs) ! (i - 1)" using assms contents_inbounds by simp then have *: "?l = ys ! (i - 1)" using 2 assms by (metis Suc_diff_1 Suc_le_lessD less_Suc_eq_le nth_append) have "?r = (ys @ [w] @ zs) ! (i - 1)" using 2 assms contents_inbounds by simp then have "?r = ys ! (i - 1)" using 2 assms by (metis Suc_diff_1 Suc_le_lessD less_Suc_eq_le nth_append) then show ?thesis using * by simp next case 3 then show ?thesis using assms by auto next case 4 then have "?l = (ys @ [v] @ zs) ! (i - 1)" using assms contents_inbounds by simp then have "?l = ((ys @ [v]) @ zs) ! (i - 1)" by simp then have *: "?l = zs ! (i - 1 - Suc m)" using 4 assms by (metis diff_Suc_1 length_append_singleton less_imp_Suc_add not_add_less1 nth_append) then have "?r = (ys @ [w] @ zs) ! (i - 1)" using 4 assms contents_inbounds by simp then have "?r = ((ys @ [w]) @ zs) ! (i - 1)" by simp then have "?r = zs ! (i - 1 - Suc m)" using 4 assms by (metis diff_Suc_1 length_append_singleton less_imp_Suc_add not_add_less1 nth_append) then show ?thesis using * by simp next case 5 then show ?thesis using assms by simp qed qed lemma contents_snoc: "⌊ys⌋(Suc (length ys) := w) = ⌊ys @ [w]⌋" proof fix i consider "i = 0" | "0 < i ∧ i ≤ length ys" | "i = Suc (length ys)" | "i > Suc (length ys)" by linarith then show "(⌊ys⌋(Suc (length ys) := w)) i = ⌊ys @ [w]⌋ i" proof (cases) case 1 then show ?thesis by simp next case 2 then show ?thesis by (smt (verit, ccfv_SIG) contents_def diff_Suc_1 ex_least_nat_less fun_upd_apply leD le_Suc_eq length_append_singleton less_imp_Suc_add nth_append) next case 3 then show ?thesis by simp next case 4 then show ?thesis by simp qed qed definition config_update_pos :: "config ⇒ nat ⇒ nat ⇒ config" where "config_update_pos cfg j p ≡ (fst cfg, (snd cfg)[j:=(cfg <:> j, p)])" lemma config_update_pos_0: "config_update_pos cfg j (cfg <#> j) = cfg" using config_update_pos_def by simp definition config_update_fwd :: "config ⇒ nat ⇒ nat ⇒ config" where "config_update_fwd cfg j d ≡ (fst cfg, (snd cfg)[j:=(cfg <:> j, cfg <#> j + d)])" lemma config_update_fwd_0: "config_update_fwd cfg j 0 = cfg" using config_update_fwd_def by simp lemma config_update_fwd_additive: "config_update_fwd (config_update_fwd cfg j d1) j d2 = (config_update_fwd cfg j (d1 + d2))" using config_update_fwd_def by (smt add.commute add.left_commute fst_conv le_less_linear list_update_beyond list_update_overwrite nth_list_update_eq sndI) subsection ‹Moving tape heads› text ‹ Among the most simple things a Turing machine can do is moving one of its tape heads. › subsubsection ‹Moving left› text ‹ The next command makes a TM move its head on tape $j$ one cell to the left unless, of course, it is in the leftmost cell already. › definition cmd_left :: "tapeidx ⇒ command" where "cmd_left j ≡ λrs. (1, map (λi. (rs ! i, if i = j then Left else Stay)) [0..<length rs])" lemma turing_command_left: "turing_command k 1 G (cmd_left j)" by (auto simp add: cmd_left_def) lemma cmd_left': "[*] (cmd_left j rs) = 1" using cmd_left_def by simp lemma cmd_left'': "j < length rs ⟹ (cmd_left j rs) [!] j = (rs ! j, Left)" using cmd_left_def by simp lemma cmd_left''': "i < length rs ⟹ i ≠ j ⟹ (cmd_left j rs) [!] i = (rs ! i, Stay)" using cmd_left_def by simp lemma tape_list_eq: assumes "length tps' = length tps" and "⋀i. i < length tps ⟹ i ≠ j ⟹ tps' ! i = tps ! i" and "tps' ! j = x" shows "tps' = tps[j := x]" using assms by (smt length_list_update list_update_beyond not_le nth_equalityI nth_list_update) lemma sem_cmd_left: assumes "j < length tps" shows "sem (cmd_left j) (0, tps) = (1, tps[j:=(fst (tps ! j), snd (tps ! j) - 1)])" proof show "fst (sem (cmd_left j) (0, tps)) = fst (1, tps[j := (fst (tps ! j), snd (tps ! j) - 1)])" using cmd_left' sem_fst by simp have "snd (sem (cmd_left j) (0, tps)) = tps[j := (fst (tps ! j), snd (tps ! j) - 1)]" proof (rule tape_list_eq) show "||sem (cmd_left j) (0, tps)|| = length tps" using turing_command_left sem_num_tapes2' by (metis snd_eqD) show "sem (cmd_left j) (0, tps) <!> i = tps ! i" if "i < length tps" and "i ≠ j" for i proof - let ?rs = "read tps" have "length ?rs = length tps" using read_length by simp moreover have "sem (cmd_left j) (0, tps) <!> i = act (cmd_left j ?rs [!] i) (tps ! i)" by (simp add: cmd_left_def sem_snd that(1)) ultimately show ?thesis using that act_Stay cmd_left''' by simp qed show "sem (cmd_left j) (0, tps) <!> j = (fst (tps ! j), snd (tps ! j) - 1)" using assms act_Left cmd_left_def read_length sem_snd by simp qed then show "snd (sem (cmd_left j) (0, tps)) = snd (1, tps[j := (fst (tps ! j), snd (tps ! j) - 1)])" by simp qed definition tm_left :: "tapeidx ⇒ machine" where "tm_left j ≡ [cmd_left j]" lemma tm_left_tm: "k ≥ 2 ⟹ G ≥ 4 ⟹ turing_machine k G (tm_left j)" unfolding tm_left_def using turing_command_left by auto lemma exe_tm_left: assumes "j < length tps" shows "exe (tm_left j) (0, tps) = (1, tps[j := tps ! j |-| 1])" unfolding tm_left_def using sem_cmd_left assms by (simp add: exe_lt_length) lemma execute_tm_left: assumes "j < length tps" shows "execute (tm_left j) (0, tps) (Suc 0) = (1, tps[j := tps ! j |-| 1])" using assms exe_tm_left by simp lemma transits_tm_left: assumes "j < length tps" shows "transits (tm_left j) (0, tps) (Suc 0) (1, tps[j := tps ! j |-| 1])" using execute_tm_left assms transitsI by blast lemma transforms_tm_left: assumes "j < length tps" shows "transforms (tm_left j) tps (Suc 0) (tps[j := tps ! j |-| 1])" using transits_tm_left assms by (simp add: tm_left_def transforms_def) lemma transforms_tm_leftI [transforms_intros]: assumes "j < length tps" and "t = 1" and "tps' = tps[j := tps ! j |-| 1]" shows "transforms (tm_left j) tps t tps'" using transits_tm_left assms by (simp add: tm_left_def transforms_def) subsubsection ‹Moving right› text ‹ The next command makes the head on tape $j$ move one cell to the right. › definition cmd_right :: "tapeidx ⇒ command" where "cmd_right j ≡ λrs. (1, map (λi. (rs ! i, if i = j then Right else Stay)) [0..<length rs])" lemma turing_command_right: "turing_command k 1 G (cmd_right j)" by (auto simp add: cmd_right_def) lemma cmd_right': "[*] (cmd_right j rs) = 1" using cmd_right_def by simp lemma cmd_right'': "j < length rs ⟹ (cmd_right j rs) [!] j = (rs ! j, Right)" using cmd_right_def by simp lemma cmd_right''': "i < length rs ⟹ i ≠ j ⟹ (cmd_right j rs) [!] i = (rs ! i, Stay)" using cmd_right_def by simp lemma sem_cmd_right: assumes "j < length tps" shows "sem (cmd_right j) (0, tps) = (1, tps[j:=(fst (tps ! j), snd (tps ! j) + 1)])" proof show "fst (sem (cmd_right j) (0, tps)) = fst (1, tps[j := (fst (tps ! j), snd (tps ! j) + 1)])" using cmd_right' sem_fst by simp have "snd (sem (cmd_right j) (0, tps)) = tps[j := (fst (tps ! j), snd (tps ! j) + 1)]" proof (rule tape_list_eq) show "||sem (cmd_right j) (0, tps)|| = length tps" using sem_num_tapes3 turing_command_right by (metis snd_conv) show "sem (cmd_right j) (0, tps) <!> i = tps ! i" if "i < length tps" and "i ≠ j" for i proof - let ?rs = "read tps" have "length ?rs = length tps" using read_length by simp moreover have "sem (cmd_right j) (0, tps) <!> i = act (cmd_right j ?rs [!] i) (tps ! i)" by (simp add: cmd_right_def sem_snd that(1)) ultimately show ?thesis using that act_Stay cmd_right''' by simp qed show "sem (cmd_right j) (0, tps) <!> j = (fst (tps ! j), snd (tps ! j) + 1)" using assms act_Right cmd_right_def read_length sem_snd by simp qed then show "snd (sem (cmd_right j) (0, tps)) = snd (1, tps[j := (fst (tps ! j), snd (tps ! j) + 1)])" by simp qed definition tm_right :: "tapeidx ⇒ machine" where "tm_right j ≡ [cmd_right j]" lemma tm_right_tm: "k ≥ 2 ⟹ G ≥ 4 ⟹ turing_machine k G (tm_right j)" unfolding tm_right_def using turing_command_right cmd_right' by auto lemma exe_tm_right: assumes "j < length tps" shows "exe (tm_right j) (0, tps) = (1, tps[j:=(fst (tps ! j), snd (tps ! j) + 1)])" unfolding tm_right_def using sem_cmd_right assms by (simp add: exe_lt_length) lemma execute_tm_right: assumes "j < length tps" shows "execute (tm_right j) (0, tps) (Suc 0) = (1, tps[j:=(fst (tps ! j), snd (tps ! j) + 1)])" using assms exe_tm_right by simp lemma transits_tm_right: assumes "j < length tps" shows "transits (tm_right j) (0, tps) (Suc 0) (1, tps[j:=(fst (tps ! j), snd (tps ! j) + 1)])" using execute_tm_right assms transitsI by blast lemma transforms_tm_right: assumes "j < length tps" shows "transforms (tm_right j) tps (Suc 0) (tps[j := tps ! j |+| 1])" using transits_tm_right assms by (simp add: tm_right_def transforms_def) lemma transforms_tm_rightI [transforms_intros]: assumes "j < length tps" and "t = Suc 0" and "tps' = tps[j := tps ! j |+| 1]" shows "transforms (tm_right j) tps t tps'" using transits_tm_right assms by (simp add: tm_right_def transforms_def) subsubsection ‹Moving right on several tapes› text ‹ The next command makes the heads on all tapes from a set $J$ of tapes move one cell to the right. › definition cmd_right_many :: "tapeidx set ⇒ command" where "cmd_right_many J ≡ λrs. (1, map (λi. (rs ! i, if i ∈ J then Right else Stay)) [0..<length rs])" lemma turing_command_right_many: "turing_command k 1 G (cmd_right_many J)" by (auto simp add: cmd_right_many_def) lemma sem_cmd_right_many: "sem (cmd_right_many J) (0, tps) = (1, map (λj. if j ∈ J then tps ! j |+| 1 else tps ! j) [0..<length tps])" proof show "fst (sem (cmd_right_many J) (0, tps)) = fst (1, map (λj. if j ∈ J then tps ! j |+| 1 else tps ! j) [0..<length tps])" using cmd_right_many_def sem_fst by simp have "snd (sem (cmd_right_many J) (0, tps)) = map (λj. if j ∈ J then tps ! j |+| 1 else tps ! j) [0..<length tps]" (is "?lhs = ?rhs") proof (rule nth_equalityI) show "length ?lhs = length ?rhs" using turing_command_right_many sem_num_tapes2' by (metis (no_types, lifting) diff_zero length_map length_upt snd_conv) then have len: "length ?lhs = length tps" by simp show "?lhs ! j = ?rhs ! j" if "j < length ?lhs" for j proof (cases "j ∈ J") case True let ?rs = "read tps" have "length ?rs = length tps" using read_length by simp moreover have "sem (cmd_right_many J) (0, tps) <!> j = act (cmd_right_many J ?rs [!] j) (tps ! j)" using cmd_right_many_def sem_snd that True len by auto moreover have "?rhs ! j = tps ! j |+| 1" using that len True by simp ultimately show ?thesis using that act_Right cmd_right_many_def True len by simp next case False let ?rs = "read tps" have "length ?rs = length tps" using read_length by simp moreover have "sem (cmd_right_many J) (0, tps) <!> j = act (cmd_right_many J ?rs [!] j) (tps ! j)" using cmd_right_many_def sem_snd that False len by auto moreover have "?rhs ! j = tps ! j" using that len False by simp ultimately show ?thesis using that act_Stay cmd_right_many_def False len by simp qed qed then show "snd (sem (cmd_right_many J) (0, tps)) = snd (1, map (λj. if j ∈ J then tps ! j |+| 1 else tps ! j) [0..<length tps])" by simp qed definition tm_right_many :: "tapeidx set ⇒ machine" where "tm_right_many J ≡ [cmd_right_many J]" lemma tm_right_many_tm: "k ≥ 2 ⟹ G ≥ 4 ⟹ turing_machine k G (tm_right_many J)" unfolding tm_right_many_def using turing_command_right_many by auto lemma transforms_tm_right_manyI [transforms_intros]: assumes "t = Suc 0" and "tps' = map (λj. if j ∈ J then tps ! j |+| 1 else tps ! j) [0..<length tps]" shows "transforms (tm_right_many J) tps t tps'" proof - have "exe (tm_right_many J) (0, tps) = (1, map (λj. if j ∈ J then tps ! j |+| 1 else tps ! j) [0..<length tps])" unfolding tm_right_many_def using sem_cmd_right_many by (simp add: exe_lt_length) then have "execute (tm_right_many J) (0, tps) (Suc 0) = (1, map (λj. if j ∈ J then tps ! j |+| 1 else tps ! j) [0..<length tps])" by simp then have "transits (tm_right_many J) (0, tps) (Suc 0) (1, map (λj. if j ∈ J then tps ! j |+| 1 else tps ! j) [0..<length tps])" using transitsI by blast then have "transforms (tm_right_many J) tps (Suc 0) (map (λj. if j ∈ J then tps ! j |+| 1 else tps ! j) [0..<length tps])" by (simp add: tm_right_many_def transforms_def) then show ?thesis using assms by (simp add: tm_right_many_def transforms_def) qed subsection ‹Copying and translating tape contents› text ‹ The Turing machines in this section scan a tape $j_1$ and copy the symbols to another tape $j_2$. Scanning can be performed in either direction, and ``copying'' may include mapping the symbols. › subsubsection ‹Copying and translating from one tape to another› text ‹ The next predicate is true iff.\ on the given tape the next symbol from the set $H$ of symbols is exactly $n$ cells to the right from the current head position. Thus, a command that moves the tape head right until it finds a symbol from $H$ takes $n$ steps and moves the head $n$ cells right. › definition rneigh :: "tape ⇒ symbol set ⇒ nat ⇒ bool" where "rneigh tp H n ≡ fst tp (snd tp + n) ∈ H ∧ (∀n' < n. fst tp (snd tp + n') ∉ H)" lemma rneighI: assumes "fst tp (snd tp + n) ∈ H" and "⋀n'. n' < n ⟹ fst tp (snd tp + n') ∉ H" shows "rneigh tp H n" using assms rneigh_def by simp text ‹ The analogous predicate for moving to the left: › definition lneigh :: "tape ⇒ symbol set ⇒ nat ⇒ bool" where "lneigh tp H n ≡ fst tp (snd tp - n) ∈ H ∧ (∀n' < n. fst tp (snd tp - n') ∉ H)" lemma lneighI: assumes "fst tp (snd tp - n) ∈ H" and "⋀n'. n' < n ⟹ fst tp (snd tp - n') ∉ H" shows "lneigh tp H n" using assms lneigh_def by simp text ‹ The next command scans tape $j_1$ rightward until it reaches a symbol from the set $H$. While doing so it copies the symbols, after applying a mapping $f$, to tape $j_2$. › definition cmd_trans_until :: "tapeidx ⇒ tapeidx ⇒ symbol set ⇒ (symbol ⇒ symbol) ⇒ command" where "cmd_trans_until j1 j2 H f ≡ λrs. if rs ! j1 ∈ H then (1, map (λr. (r, Stay)) rs) else (0, map (λi. (if i = j2 then f (rs ! j1) else rs ! i, if i = j1 ∨ i = j2 then Right else Stay)) [0..<length rs])" text ‹ The analogous command for moving to the left: › definition cmd_ltrans_until :: "tapeidx ⇒ tapeidx ⇒ symbol set ⇒ (symbol ⇒ symbol) ⇒ command" where "cmd_ltrans_until j1 j2 H f ≡ λrs. if rs ! j1 ∈ H then (1, map (λr. (r, Stay)) rs) else (0, map (λi. (if i = j2 then f (rs ! j1) else rs ! i, if i = j1 ∨ i = j2 then Left else Stay)) [0..<length rs])" lemma proper_cmd_trans_until: "proper_command k (cmd_trans_until j1 j2 H f)" using cmd_trans_until_def by simp lemma proper_cmd_ltrans_until: "proper_command k (cmd_ltrans_until j1 j2 H f)" using cmd_ltrans_until_def by simp lemma sem_cmd_trans_until_1: assumes "j1 < k" and "length tps = k" and "(0, tps) <.> j1 ∈ H" shows "sem (cmd_trans_until j1 j2 H f) (0, tps) = (1, tps)" using cmd_trans_until_def tapes_at_read read_length assms act_Stay by (intro semI[OF proper_cmd_trans_until]) auto lemma sem_cmd_ltrans_until_1: assumes "j1 < k" and "length tps = k" and "(0, tps) <.> j1 ∈ H" shows "sem (cmd_ltrans_until j1 j2 H f) (0, tps) = (1, tps)" using cmd_ltrans_until_def tapes_at_read read_length assms act_Stay by (intro semI[OF proper_cmd_ltrans_until]) auto lemma sem_cmd_trans_until_2: assumes "j1 < k" and "length tps = k" and "(0, tps) <.> j1 ∉ H" shows "sem (cmd_trans_until j1 j2 H f) (0, tps) = (0, tps[j1 := tps ! j1 |+| 1, j2 := tps ! j2 |:=| (f (tps :.: j1)) |+| 1])" using cmd_trans_until_def tapes_at_read read_length assms act_Stay act_Right by (intro semI[OF proper_cmd_trans_until]) auto lemma sem_cmd_ltrans_until_2: assumes "j1 < k" and "length tps = k" and "(0, tps) <.> j1 ∉ H" shows "sem (cmd_ltrans_until j1 j2 H f) (0, tps) = (0, tps[j1 := tps ! j1 |-| 1, j2 := tps ! j2 |:=| (f (tps :.: j1)) |-| 1])" using cmd_ltrans_until_def tapes_at_read read_length assms act_Stay act_Left by (intro semI[OF proper_cmd_ltrans_until]) auto definition tm_trans_until :: "tapeidx ⇒ tapeidx ⇒ symbol set ⇒ (symbol ⇒ symbol) ⇒ machine" where "tm_trans_until j1 j2 H f ≡ [cmd_trans_until j1 j2 H f]" definition tm_ltrans_until :: "tapeidx ⇒ tapeidx ⇒ symbol set ⇒ (symbol ⇒ symbol) ⇒ machine" where "tm_ltrans_until j1 j2 H f ≡ [cmd_ltrans_until j1 j2 H f]" lemma tm_trans_until_tm: assumes "0 < j2" and "j1 < k" and "j2 < k" and "∀h<G. f h < G" and "k ≥ 2" and "G ≥ 4" shows "turing_machine k G (tm_trans_until j1 j2 H f)" unfolding tm_trans_until_def cmd_trans_until_def using assms turing_machine_def by auto lemma tm_ltrans_until_tm: assumes "0 < j2" and "j1 < k" and "j2 < k" and "∀h<G. f h < G" and "k ≥ 2" and "G ≥ 4" shows "turing_machine k G (tm_ltrans_until j1 j2 H f)" unfolding tm_ltrans_until_def cmd_ltrans_until_def using assms turing_machine_def by auto lemma exe_tm_trans_until_1: assumes "j1 < k" and "length tps = k" and "(0, tps) <.> j1 ∈ H" shows "exe (tm_trans_until j1 j2 H f) (0, tps) = (1, tps)" unfolding tm_trans_until_def using sem_cmd_trans_until_1 assms exe_lt_length by simp lemma exe_tm_ltrans_until_1: assumes "j1 < k" and "length tps = k" and "(0, tps) <.> j1 ∈ H" shows "exe (tm_ltrans_until j1 j2 H f) (0, tps) = (1, tps)" unfolding tm_ltrans_until_def using sem_cmd_ltrans_until_1 assms exe_lt_length by simp lemma exe_tm_trans_until_2: assumes "j1 < k" and "length tps = k" and "(0, tps) <.> j1 ∉ H" shows "exe (tm_trans_until j1 j2 H f) (0, tps) = (0, tps[j1 := tps ! j1 |+| 1, j2 := tps ! j2 |:=| (f (tps :.: j1)) |+| 1])" unfolding tm_trans_until_def using sem_cmd_trans_until_2 assms exe_lt_length by simp lemma exe_tm_ltrans_until_2: assumes "j1 < k" and "length tps = k" and "(0, tps) <.> j1 ∉ H" shows "exe (tm_ltrans_until j1 j2 H f) (0, tps) = (0, tps[j1 := tps ! j1 |-| 1, j2 := tps ! j2 |:=| (f (tps :.: j1)) |-| 1])" unfolding tm_ltrans_until_def using sem_cmd_ltrans_until_2 assms exe_lt_length by simp text ‹ Let $tp_1$ and $tp_2$ be two tapes with head positions $i_1$ and $i_2$, respectively. The next function describes the result of overwriting the symbols at positions $i_2, \dots, i_2 + n - 1$ on tape $tp_2$ by the symbols at positions $i_1, \dots, i_1 + n - 1$ on tape $tp_1$ after applying a symbol map $f$. › definition transplant :: "tape ⇒ tape ⇒ (symbol ⇒ symbol)⇒ nat ⇒ tape" where "transplant tp1 tp2 f n ≡ (λi. if snd tp2 ≤ i ∧ i < snd tp2 + n then f (fst tp1 (snd tp1 + i - snd tp2)) else fst tp2 i, snd tp2 + n)" text ‹ The analogous function for moving to the left while copying: › definition ltransplant :: "tape ⇒ tape ⇒ (symbol ⇒ symbol)⇒ nat ⇒ tape" where "ltransplant tp1 tp2 f n ≡ (λi. if snd tp2 - n < i ∧ i ≤ snd tp2 then f (fst tp1 (snd tp1 + i - snd tp2)) else fst tp2 i, snd tp2 - n)" lemma transplant_0: "transplant tp1 tp2 f 0 = tp2" unfolding transplant_def by standard auto lemma ltransplant_0: "ltransplant tp1 tp2 f 0 = tp2" unfolding ltransplant_def by standard auto lemma transplant_upd: "transplant tp1 tp2 f n |:=| (f ( |.| (tp1 |+| n))) |+| 1 = transplant tp1 tp2 f (Suc n)" unfolding transplant_def by auto lemma ltransplant_upd: assumes "n < snd tp2" shows "ltransplant tp1 tp2 f n |:=| (f ( |.| (tp1 |-| n))) |-| 1 = ltransplant tp1 tp2 f (Suc n)" unfolding ltransplant_def using assms by fastforce lemma tapes_ltransplant_upd: assumes "t < tps :#: j2" and "t < tps :#: j1" and "j1 < k" and "j2 < k" and "length tps = k" and "tps' = tps[j1 := tps ! j1 |-| t, j2 := ltransplant (tps ! j1) (tps ! j2) f t]" shows "tps'[j1 := tps' ! j1 |-| 1, j2 := tps' ! j2 |:=| (f (tps' :.: j1)) |-| 1] = tps[j1 := tps ! j1 |-| Suc t, j2 := ltransplant (tps ! j1) (tps ! j2) f (Suc t)]" (is "?lhs = ?rhs") proof (rule nth_equalityI) show 1: "length ?lhs = length ?rhs" using assms by simp have len: "length ?lhs = k" using assms by simp show "?lhs ! j = ?rhs ! j" if "j < length ?lhs" for j proof - have "j < k" using len that by simp show ?thesis proof (cases "j ≠ j1 ∧ j ≠ j2") case True then show ?thesis using assms by simp next case j1j2: False show ?thesis proof (cases "j1 = j2") case True then have j: "j = j1" "j = j2" using j1j2 by simp_all have "tps' ! j1 = ltransplant (tps ! j1) (tps ! j2) f t" using j assms that by simp then have *: "snd (tps' ! j1) = snd (tps ! j1) - t" using j ltransplant_def by simp then have "fst (tps' ! j1) = (λi. if snd (tps ! j2) - t < i ∧ i ≤ snd (tps ! j2) then f (fst (tps ! j1) (snd (tps ! j1) + i - snd (tps ! j2))) else fst (tps ! j2) i)" using j ltransplant_def assms by auto then have "fst (tps' ! j1) = (λi. if snd (tps ! j1) - t < i ∧ i ≤ snd (tps ! j1) then f (fst (tps ! j1) (snd (tps ! j1) + i - snd (tps ! j1))) else fst (tps ! j1) i)" using j by auto then have "fst (tps' ! j1) (snd (tps ! j1) - t) = fst (tps ! j1) (snd (tps ! j1) - t)" by simp then have "tps' :.: j1 = fst (tps ! j1) (snd (tps ! j1) - t)" using * by simp then have "?lhs ! j = (ltransplant (tps ! j1) (tps ! j2) f t) |:=| (f ( |.| (tps ! j1 |-| t))) |-| 1" using assms(6) j that by simp then have "?lhs ! j = (ltransplant (tps ! j1) (tps ! j2) f (Suc t))" using ltransplant_upd assms(1) by simp moreover have "?rhs ! j = ltransplant (tps ! j1) (tps ! j2) f (Suc t)" using assms(6) that j by simp ultimately show ?thesis by simp next case j1_neq_j2: False then show ?thesis proof (cases "j = j1") case True then have "?lhs ! j = tps' ! j1 |-| 1" using assms j1_neq_j2 by simp then have "?lhs ! j = (tps ! j1 |-| t) |-| 1" using assms j1_neq_j2 by simp moreover have "?rhs ! j = tps ! j1 |-| Suc t" using True assms j1_neq_j2 by simp ultimately show ?thesis by simp next case False then have j: "j = j2" using j1j2 by simp then have "?lhs ! j = tps' ! j2 |:=| (f (tps' :.: j1)) |-| 1" using assms by simp then have "?lhs ! j = (ltransplant (tps ! j1) (tps ! j2) f t) |:=| (f (tps' :.: j1)) |-| 1" using assms by simp then have "?lhs ! j = (ltransplant (tps ! j1) (tps ! j2) f (Suc t))" using ltransplant_def assms ltransplant_upd by (smt (z3) j1_neq_j2 nth_list_update_eq nth_list_update_neq) moreover have "?rhs ! j = ltransplant (tps ! j1) (tps ! j2) f (Suc t)" using assms(6) that j by simp ultimately show ?thesis by simp qed qed qed qed qed lemma execute_tm_trans_until_less: assumes "j1 < k" and "j2 < k" and "length tps = k" and "rneigh (tps ! j1) H n" and "t ≤ n" shows "execute (tm_trans_until j1 j2 H f) (0, tps) t = (0, tps[j1 := tps ! j1 |+| t, j2 := transplant (tps ! j1) (tps ! j2) f t])" using assms(5) proof (induction t) case 0 then show ?case using transplant_0 by simp next case (Suc t) then have "t < n" by simp let ?M = "tm_trans_until j1 j2 H f" have "execute ?M (0, tps) (Suc t) = exe ?M (execute ?M (0, tps) t)" by simp also have "... = exe ?M (0, tps[j1 := tps ! j1 |+| t, j2 := transplant (tps ! j1) (tps ! j2) f t])" (is "_ = exe ?M (0, ?tps)") using Suc by simp also have "... = (0, ?tps[j1 := ?tps ! j1 |+| 1, j2 := ?tps ! j2 |:=| (f (?tps :.: j1)) |+| 1])" proof (rule exe_tm_trans_until_2[where ?k=k]) show "j1 < k" using assms(1) . show "length (tps[j1 := tps ! j1 |+| t, j2 := transplant (tps ! j1) (tps ! j2) f t]) = k" using assms by simp show "(0, tps[j1 := tps ! j1 |+| t, j2 := transplant (tps ! j1) (tps ! j2) f t]) <.> j1 ∉ H" using assms transplant_def rneigh_def ‹t < n› by (smt fst_conv length_list_update less_not_refl2 nth_list_update_eq nth_list_update_neq snd_conv) qed finally show ?case using assms transplant_upd by auto (smt add.commute fst_conv transplant_def transplant_upd less_not_refl2 list_update_overwrite list_update_swap nth_list_update_eq nth_list_update_neq plus_1_eq_Suc snd_conv) qed lemma execute_tm_ltrans_until_less: assumes "j1 < k" and "j2 < k" and "length tps = k" and "lneigh (tps ! j1) H n" and "t ≤ n" and "n ≤ tps :#: j1" and "n ≤ tps :#: j2" shows "execute (tm_ltrans_until j1 j2 H f) (0, tps) t = (0, tps[j1 := tps ! j1 |-| t, j2 := ltransplant (tps ! j1) (tps ! j2) f t])" using assms(5) proof (induction t) case 0 then show ?case using ltransplant_0 by simp next case (Suc t) then have "t < n" by simp have 1: "t < tps :#: j2" using assms(7) Suc by simp have 2: "t < tps :#: j1" using assms(6) Suc by simp let ?M = "tm_ltrans_until j1 j2 H f" define tps' where "tps' = tps[j1 := tps ! j1 |-| t, j2 := ltransplant (tps ! j1) (tps ! j2) f t]" have "execute ?M (0, tps) (Suc t) = exe ?M (execute ?M (0, tps) t)" by simp also have "... = exe ?M (0, tps')" using Suc tps'_def by simp also have "... = (0, tps'[j1 := tps' ! j1 |-| 1, j2 := tps' ! j2 |:=| (f (tps' :.: j1)) |-| 1])" proof (rule exe_tm_ltrans_until_2[where ?k=k]) show "j1 < k" using assms(1) . show "length tps' = k" using assms tps'_def by simp show "(0, tps') <.> j1 ∉ H" using assms ltransplant_def tps'_def lneigh_def ‹t < n› by (smt fst_conv length_list_update less_not_refl2 nth_list_update_eq nth_list_update_neq snd_conv) qed finally show ?case using tapes_ltransplant_upd[OF 1 2 assms(1,2,3) tps'_def] by simp qed lemma execute_tm_trans_until: assumes "j1 < k" and "j2 < k" and "length tps = k" and "rneigh (tps ! j1) H n" shows "execute (tm_trans_until j1 j2 H f) (0, tps) (Suc n) = (1, tps[j1 := tps ! j1 |+| n, j2 := transplant (tps ! j1) (tps ! j2) f n])" proof - let ?M = "tm_trans_until j1 j2 H f" have "execute ?M (0, tps) (Suc n) = exe ?M (execute ?M (0, tps) n)" by simp also have "... = exe ?M (0, tps[j1 := tps ! j1 |+| n, j2 := transplant (tps ! j1) (tps ! j2) f n])" using execute_tm_trans_until_less[where ?t=n] assms by simp also have "... = (1, tps[j1 := tps ! j1 |+| n, j2 := transplant (tps ! j1) (tps ! j2) f n])" (is "_ = (1, ?tps)") proof - have "length ?tps = k" using assms(3) by simp moreover have "(0, ?tps) <.> j1 ∈ H" using rneigh_def transplant_def assms by (smt fst_conv length_list_update less_not_refl2 nth_list_update_eq nth_list_update_neq snd_conv) ultimately show ?thesis using exe_tm_trans_until_1 assms by simp qed finally show ?thesis by simp qed lemma execute_tm_ltrans_until: assumes "j1 < k" and "j2 < k" and "length tps = k" and "lneigh (tps ! j1) H n" and "n ≤ tps :#: j1" and "n ≤ tps :#: j2" shows "execute (tm_ltrans_until j1 j2 H f) (0, tps) (Suc n) = (1, tps[j1 := tps ! j1 |-| n, j2 := ltransplant (tps ! j1) (tps ! j2) f n])" proof - let ?M = "tm_ltrans_until j1 j2 H f" have "execute ?M (0, tps) (Suc n) = exe ?M (execute ?M (0, tps) n)" by simp also have "... = exe ?M (0, tps[j1 := tps ! j1 |-| n, j2 := ltransplant (tps ! j1) (tps ! j2) f n])" using execute_tm_ltrans_until_less[where ?t=n] assms by simp also have "... = (1, tps[j1 := tps ! j1 |-| n, j2 := ltransplant (tps ! j1) (tps ! j2) f n])" (is "_ = (1, ?tps)") proof - have "length ?tps = k" using assms(3) by simp moreover have "(0, ?tps) <.> j1 ∈ H" using lneigh_def ltransplant_def assms by (smt (verit, ccfv_threshold) fst_conv length_list_update less_not_refl nth_list_update_eq nth_list_update_neq snd_conv) ultimately show ?thesis using exe_tm_ltrans_until_1 assms by simp qed finally show ?thesis by simp qed lemma transits_tm_trans_until: assumes "j1 < k" and "j2 < k" and "length tps = k" and "rneigh (tps ! j1) H n" shows "transits (tm_trans_until j1 j2 H f) (0, tps) (Suc n) (1, tps[j1 := tps ! j1 |+| n, j2 := transplant (tps ! j1) (tps ! j2) f n])" using execute_tm_trans_until[OF assms] transitsI[of _ _ "Suc n" _ "Suc n"] by blast lemma transits_tm_ltrans_until: assumes "j1 < k" and "j2 < k" and "length tps = k" and "lneigh (tps ! j1) H n" and "n ≤ tps :#: j1" and "n ≤ tps :#: j2" shows "transits (tm_ltrans_until j1 j2 H f) (0, tps) (Suc n) (1, tps[j1 := tps ! j1 |-| n, j2 := ltransplant (tps ! j1) (tps ! j2) f n])" using execute_tm_ltrans_until[OF assms] transitsI[of _ _ "Suc n" _ "Suc n"] by blast lemma transforms_tm_trans_until: assumes "j1 < k" and "j2 < k" and "length tps = k" and "rneigh (tps ! j1) H n" shows "transforms (tm_trans_until j1 j2 H f) tps (Suc n) (tps[j1 := tps ! j1 |+| n, j2 := transplant (tps ! j1) (tps ! j2) f n])" using tm_trans_until_def transforms_def transits_tm_trans_until[OF assms] by simp lemma transforms_tm_ltrans_until: assumes "j1 < k" and "j2 < k" and "length tps = k" and "lneigh (tps ! j1) H n" and "n ≤ tps :#: j1" and "n ≤ tps :#: j2" shows "transforms (tm_ltrans_until j1 j2 H f) tps (Suc n) (tps[j1 := tps ! j1 |-| n, j2 := ltransplant (tps ! j1) (tps ! j2) f n])" using tm_ltrans_until_def transforms_def transits_tm_ltrans_until[OF assms] by simp corollary transforms_tm_trans_untilI [transforms_intros]: assumes "j1 < k" and "j2 < k" and "length tps = k" and "rneigh (tps ! j1) H n" and "t = Suc n" and "tps' = tps[j1 := tps ! j1 |+| n, j2 := transplant (tps ! j1) (tps ! j2) f n]" shows "transforms (tm_trans_until j1 j2 H f) tps t tps'" using transforms_tm_trans_until[OF assms(1-4)] assms(5,6) by simp corollary transforms_tm_ltrans_untilI [transforms_intros]: assumes "j1 < k" and "j2 < k" and "length tps = k" and "lneigh (tps ! j1) H n" and "n ≤ tps :#: j1" and "n ≤ tps :#: j2" and "t = Suc n" and "tps' = tps[j1 := tps ! j1 |-| n, j2 := ltransplant (tps ! j1) (tps ! j2) f n]" shows "transforms (tm_ltrans_until j1 j2 H f) tps t tps'" using transforms_tm_ltrans_until[OF assms(1-6)] assms(7,8) by simp subsubsection ‹Copying one tape to another› text ‹ If we set the symbol map $f$ in @{const tm_trans_until} to the identity function, we get a Turing machine that simply makes a copy. › definition tm_cp_until :: "tapeidx ⇒ tapeidx ⇒ symbol set ⇒ machine" where "tm_cp_until j1 j2 H ≡ tm_trans_until j1 j2 H id" lemma id_symbol: "∀h<G. (id :: symbol ⇒ symbol) h < G" by simp lemma tm_cp_until_tm: assumes "0 < j2" and "j1 < k" and "j2 < k" and "G ≥ 4" shows "turing_machine k G (tm_cp_until j1 j2 H)" unfolding tm_cp_until_def using tm_trans_until_tm id_symbol assms turing_machine_def by simp abbreviation implant :: "tape ⇒ tape ⇒ nat ⇒ tape" where "implant tp1 tp2 n ≡ transplant tp1 tp2 id n" lemma implant: "implant tp1 tp2 n = (λi. if snd tp2 ≤ i ∧ i < snd tp2 + n then fst tp1 (snd tp1 + i - snd tp2) else fst tp2 i, snd tp2 + n)" using transplant_def by auto lemma implantI: assumes "tp' = (λi. if snd tp2 ≤ i ∧ i < snd tp2 + n then fst tp1 (snd tp1 + i - snd tp2) else fst tp2 i, snd tp2 + n)" shows "implant tp1 tp2 n = tp'" using implant assms by simp lemma fst_snd_pair: "fst t = a ⟹ snd t = b ⟹ t = (a, b)" by auto lemma implantI': assumes "fst tp' = (λi. if snd tp2 ≤ i ∧ i < snd tp2 + n then fst tp1 (snd tp1 + i - snd tp2) else fst tp2 i)" and "snd tp' = snd tp2 + n" shows "implant tp1 tp2 n = tp'" using implantI fst_snd_pair[OF assms] by simp lemma implantI'': assumes "⋀i. snd tp2 ≤ i ∧ i < snd tp2 + n ⟹ fst tp' i = fst tp1 (snd tp1 + i - snd tp2)" and "⋀i. i < snd tp2 ⟹ fst tp' i = fst tp2 i" and "⋀i. snd tp2 + n ≤ i ⟹ fst tp' i = fst tp2 i" assumes "snd tp' = snd tp2 + n" shows "implant tp1 tp2 n = tp'" using assms implantI' by (meson linorder_le_less_linear) lemma implantI''': assumes "⋀i. i2 ≤ i ∧ i < i2 + n ⟹ ys i = ys1 (i1 + i - i2)" and "⋀i. i < i2 ⟹ ys i = ys2 i" and "⋀i. i2 + n ≤ i ⟹ ys i = ys2 i" assumes "i = i2 + n" shows "implant (ys1, i1) (ys2, i2) n = (ys, i)" using assms implantI'' by auto lemma implant_self: "implant tp tp n = tp |+| n" unfolding transplant_def by auto lemma transforms_tm_cp_untilI [transforms_intros]: assumes "j1 < k" and "j2 < k" and "length tps = k" and "rneigh (tps ! j1) H n" and "t = Suc n" and "tps' = tps[j1 := tps ! j1 |+| n, j2 := implant (tps ! j1) (tps ! j2) n]" shows "transforms (tm_cp_until j1 j2 H) tps t tps'" unfolding tm_cp_until_def using transforms_tm_trans_untilI[OF assms(1-6)] by simp lemma implant_contents: assumes "i > 0" and "n + (i - 1) ≤ length xs" shows "implant (⌊xs⌋, i) (⌊ys⌋, Suc (length ys)) n = (⌊ys @ (take n (drop (i - 1) xs))⌋, Suc (length ys) + n)" (is "?lhs = ?rhs") proof - have lhs: "?lhs = (λj. if Suc (length ys) ≤ j ∧ j < Suc (length ys) + n then ⌊xs⌋ (i + j - Suc (length ys)) else ⌊ys⌋ j, Suc (length ys) + n)" using implant by auto let ?zs = "ys @ (take n (drop (i - 1) xs))" have lenzs: "length ?zs = length ys + n" using assms by simp have fst_rhs: "fst ?rhs = (λj. if j = 0 then 1 else if j ≤ length ys + n then ?zs ! (j - 1) else 0)" using assms by auto have "(λj. if Suc (length ys) ≤ j ∧ j < Suc (length ys) + n then ⌊xs⌋ (i + j - Suc (length ys)) else ⌊ys⌋ j) = (λj. if j = 0 then 1 else if j ≤ length ys + n then ?zs ! (j - 1) else 0)" (is "?l = ?r") proof fix j consider "j = 0" | "j > 0 ∧ j ≤ length ys" | "j > length ys ∧ j ≤ length ys + n" | "j > length ys + n" by linarith then show "?l j = ?r j" proof (cases) case 1 then show ?thesis by simp next case 2 then show ?thesis using assms contents_def by (smt (z3) Suc_diff_1 less_trans_Suc not_add_less1 not_le not_less_eq_eq nth_append) next case 3 then have "?r j = ?zs ! (j - 1)" by simp also have "... = take n (drop (i - 1) xs) ! (j - 1 - length ys)" using 3 lenzs by (metis add.right_neutral diff_is_0_eq le_add_diff_inverse not_add_less2 not_le not_less_eq nth_append plus_1_eq_Suc) also have "... = take n (drop (i - 1) xs) ! (j - Suc (length ys))" by simp also have "... = xs ! (i - 1 + j - Suc (length ys))" using 3 assms by auto also have "... = ⌊xs⌋ (i + j - Suc (length ys))" using assms contents_def 3 by auto also have "... = ?l j" using 3 by simp finally have "?r j = ?l j" . then show ?thesis by simp next case 4 then show ?thesis by simp qed qed then show ?thesis using lhs fst_rhs by simp qed subsubsection ‹Moving to the next specific symbol› text ‹ Copying a tape to itself means just moving to the right. › definition tm_right_until :: "tapeidx ⇒ symbol set ⇒ machine" where "tm_right_until j H ≡ tm_cp_until j j H" text ‹ Copying a tape to itself does not change the tape. So this is a Turing machine even for the input tape $j = 0$, unlike @{const tm_cp_until} where the target tape cannot, in general, be the input tape. › lemma tm_right_until_tm: assumes "j < k" and "k ≥ 2" and "G ≥ 4" shows "turing_machine k G (tm_right_until j H)" unfolding tm_right_until_def tm_cp_until_def tm_trans_until_def cmd_trans_until_def using assms turing_machine_def by auto lemma transforms_tm_right_untilI [transforms_intros]: assumes "j < length tps" and "rneigh (tps ! j) H n" and "t = Suc n" and "tps' = (tps[j := tps ! j |+| n])" shows "transforms (tm_right_until j H) tps t tps'" using transforms_tm_cp_untilI assms implant_self tm_right_until_def by (metis list_update_id nth_list_update_eq) subsubsection ‹Translating to a constant symbol› text ‹ Another way to specialize @{const tm_trans_until} and @{const tm_ltrans_until} is to have a constant function $f$. › definition tm_const_until :: "tapeidx ⇒ tapeidx ⇒ symbol set ⇒ symbol ⇒ machine" where "tm_const_until j1 j2 H h ≡ tm_trans_until j1 j2 H (λ_. h)" lemma tm_const_until_tm: assumes "0 < j2" and "j1 < k" and "j2 < k" and "h < G" and "k ≥ 2" and "G ≥ 4" shows "turing_machine k G (tm_const_until j1 j2 H h)" unfolding tm_const_until_def using tm_trans_until_tm assms turing_machine_def by metis text ‹ Continuing with our fantasy names ending in \emph{-plant}, we name the operation @{term constplant}. › abbreviation constplant :: "tape ⇒ symbol ⇒ nat ⇒ tape" where "constplant tp2 h n ≡ transplant (λ_. 0, 0) tp2 (λ_. h) n" lemma constplant_transplant: "constplant tp2 h n = transplant tp1 tp2 (λ_. h) n" using transplant_def by simp lemma constplant: "constplant tp2 h n = (λi. if snd tp2 ≤ i ∧ i < snd tp2 + n then h else fst tp2 i, snd tp2 + n)" using transplant_def by simp lemma transforms_tm_const_untilI [transforms_intros]: assumes "j1 < k" and "j2 < k" and "length tps = k" and "rneigh (tps ! j1) H n" and "t = Suc n" and "tps' = tps[j1 := tps ! j1 |+| n, j2 := constplant (tps ! j2) h n]" shows "transforms (tm_const_until j1 j2 H h) tps t tps'" unfolding tm_const_until_def using transforms_tm_trans_untilI assms constplant_transplant by metis definition tm_lconst_until :: "tapeidx ⇒ tapeidx ⇒ symbol set ⇒ symbol ⇒ machine" where "tm_lconst_until j1 j2 H h ≡ tm_ltrans_until j1 j2 H (λ_. h)" lemma tm_lconst_until_tm: assumes "0 < j2" and "j1 < k" and "j2 < k" and "h < G" and "k ≥ 2" and "G ≥ 4" shows "turing_machine k G (tm_lconst_until j1 j2 H h)" unfolding tm_lconst_until_def using tm_ltrans_until_tm assms turing_machine_def by metis abbreviation lconstplant :: "tape ⇒ symbol ⇒ nat ⇒ tape" where "lconstplant tp2 h n ≡ ltransplant (λ_. 0, 0) tp2 (λ_. h) n" lemma lconstplant_ltransplant: "lconstplant tp2 h n = ltransplant tp1 tp2 (λ_. h) n" using ltransplant_def by simp lemma lconstplant: "lconstplant tp2 h n = (λi. if snd tp2 - n < i ∧ i ≤ snd tp2 then h else fst tp2 i, snd tp2 - n)" using ltransplant_def by simp lemma transforms_tm_lconst_untilI [transforms_intros]: assumes "0 < j2" and "j1 < k" and "j2 < k" and "length tps = k" and "lneigh (tps ! j1) H n" and "n ≤ tps :#: j1" and "n ≤ tps :#: j2" and "t = Suc n" and "tps' = tps[j1 := tps ! j1 |-| n, j2 := lconstplant (tps ! j2) h n]" shows "transforms (tm_lconst_until j1 j2 H h) tps t tps'" unfolding tm_lconst_until_def using transforms_tm_ltrans_untilI assms lconstplant_ltransplant by metis subsection ‹Writing single symbols› text ‹ The next command writes a fixed symbol $h$ to tape $j$. It does not move a tape head. › definition cmd_write :: "tapeidx ⇒ symbol ⇒ command" where "cmd_write j h rs ≡ (1, map (λi. (if i = j then h else rs ! i, Stay)) [0..<length rs])" lemma sem_cmd_write: "sem (cmd_write j h) (0, tps) = (1, tps[j := tps ! j |:=| h])" using cmd_write_def read_length act_Stay by (intro semI) auto definition tm_write :: "tapeidx ⇒ symbol ⇒ machine" where "tm_write j h ≡ [cmd_write j h]" lemma tm_write_tm: assumes "0 < j" and "j < k" and "h < G" and "G ≥ 4" shows "turing_machine k G (tm_write j h)" unfolding tm_write_def cmd_write_def using assms turing_machine_def by auto lemma transforms_tm_writeI [transforms_intros]: assumes "tps' = tps[j := tps ! j |:=| h]" shows "transforms (tm_write j h) tps 1 tps'" unfolding tm_write_def using sem_cmd_write exe_lt_length assms tm_write_def transits_def transforms_def by auto text ‹ The next command writes the symbol to tape $j_2$ that results from applying a function $f$ to the symbol read from tape $j_1$. It does not move any tape heads. › definition cmd_trans2 :: "tapeidx ⇒ tapeidx ⇒ (symbol ⇒ symbol) ⇒ command" where "cmd_trans2 j1 j2 f rs ≡ (1, map (λi. (if i = j2 then f (rs ! j1) else rs ! i, Stay)) [0..<length rs])" lemma sem_cmd_trans2: assumes "j1 < length tps" shows "sem (cmd_trans2 j1 j2 f) (0, tps) = (1, tps[j2 := tps ! j2 |:=| (f (tps :.: j1))])" using cmd_trans2_def tapes_at_read assms read_length act_Stay by (intro semI) auto definition tm_trans2 :: "tapeidx ⇒ tapeidx ⇒ (symbol ⇒ symbol) ⇒ machine" where "tm_trans2 j1 j2 f ≡ [cmd_trans2 j1 j2 f]" lemma tm_trans2_tm: assumes "j1 < k" and "0 < j2" and "j2 < k" and "∀h < G. f h < G" and "k ≥ 2" and "G ≥ 4" shows "turing_machine k G (tm_trans2 j1 j2 f)" unfolding tm_trans2_def cmd_trans2_def using assms turing_machine_def by auto lemma exe_tm_trans2: assumes "j1 < length tps" shows "exe (tm_trans2 j1 j2 f) (0, tps) = (1, tps[j2 := tps ! j2 |:=| (f (tps :.: j1))])" unfolding tm_trans2_def using sem_cmd_trans2 assms exe_lt_length by simp lemma execute_tm_trans2: assumes "j1 < length tps" shows "execute (tm_trans2 j1 j2 f) (0, tps) 1 = (1, tps[j2 := tps ! j2 |:=| (f (tps :.: j1))])" using assms exe_tm_trans2 by simp lemma transits_tm_trans2: assumes "j1 < length tps" shows "transits (tm_trans2 j1 j2 f) (0, tps) 1 (1, tps[j2 := tps ! j2 |:=| (f (tps :.: j1))])" using assms execute_tm_trans2 transits_def by auto lemma transforms_tm_trans2: assumes "j1 < length tps" shows "transforms (tm_trans2 j1 j2 f) tps 1 (tps[j2 := tps ! j2 |:=| (f (tps :.: j1))])" using tm_trans2_def assms transits_tm_trans2 transforms_def by simp lemma transforms_tm_trans2I [transforms_intros]: assumes "j1 < length tps" and "tps' = tps[j2 := tps ! j2 |:=| (f (tps :.: j1))]" shows "transforms (tm_trans2 j1 j2 f) tps 1 tps'" using assms transforms_tm_trans2 by simp text ‹ Equating the two tapes in @{const tm_trans2}, we can map a symbol in-place. › definition tm_trans :: "tapeidx ⇒ (symbol ⇒ symbol) ⇒ machine" where "tm_trans j f ≡ tm_trans2 j j f" lemma tm_trans_tm: assumes "0 < j" and "j < k" and "∀h < G. f h < G" and "G ≥ 4" shows "turing_machine k G (tm_trans j f)" unfolding tm_trans_def using tm_trans2_tm assms by simp lemma transforms_tm_transI [transforms_intros]: assumes "j < length tps" and "tps' = tps[j := tps ! j |:=| (f (tps :.: j))]" shows "transforms (tm_trans j f) tps 1 tps'" using assms transforms_tm_trans2 tm_trans_def by simp text ‹ The next command is like the previous one, except it also moves the tape head to the right. › definition cmd_rtrans :: "tapeidx ⇒ (symbol ⇒ symbol) ⇒ command" where "cmd_rtrans j f rs ≡ (1, map (λi. (if i = j then f (rs ! i) else rs ! i, if i = j then Right else Stay)) [0..<length rs])" lemma sem_cmd_rtrans: assumes "j < length tps" shows "sem (cmd_rtrans j f) (0, tps) = (1, tps[j := tps ! j |:=| (f (tps :.: j)) |+| 1])" using cmd_rtrans_def tapes_at_read read_length assms act_Stay act_Right by (intro semI) auto definition tm_rtrans :: "tapeidx ⇒ (symbol ⇒ symbol) ⇒ machine" where "tm_rtrans j f ≡ [cmd_rtrans j f]" lemma tm_rtrans_tm: assumes "0 < j" and "j < k" and "∀h<G. f h < G" and "k ≥ 2" and "G ≥ 4" shows "turing_machine k G (tm_rtrans j f)" unfolding tm_rtrans_def cmd_rtrans_def using assms turing_machine_def by auto lemma exe_tm_rtrans: assumes "j < length tps" shows "exe (tm_rtrans j f) (0, tps) = (1, tps[j := tps ! j |:=| (f (tps :.: j)) |+| 1])" unfolding tm_rtrans_def using sem_cmd_rtrans assms exe_lt_length by simp lemma execute_tm_rtrans: assumes "j < length tps" shows "execute (tm_rtrans j f) (0, tps) 1 = (1, tps[j := tps ! j |:=| (f (tps :.: j)) |+| 1])" using assms exe_tm_rtrans by simp lemma transits_tm_rtrans: assumes "j < length tps" shows "transits (tm_rtrans j f) (0, tps) 1 (1, tps[j := tps ! j |:=| (f (tps :.: j)) |+| 1])" using assms execute_tm_rtrans transits_def by auto lemma transforms_tm_rtrans: assumes "j < length tps" shows "transforms (tm_rtrans j f) tps 1 (tps[j := tps ! j |:=| (f (tps :.: j)) |+| 1])" using assms transits_tm_rtrans transforms_def by (metis One_nat_def length_Cons list.size(3) tm_rtrans_def) lemma transforms_tm_rtransI [transforms_intros]: assumes "j < length tps" and "tps' = tps[j := tps ! j |:=| (f (tps :.: j)) |+| 1]" shows "transforms (tm_rtrans j f) tps 1 tps'" using assms transforms_tm_rtrans by simp text ‹ The next command writes a fixed symbol $h$ to all tapes in the set $J$. › definition cmd_write_many :: "tapeidx set ⇒ symbol ⇒ command" where "cmd_write_many J h rs ≡ (1, map (λi. (if i ∈ J then h else rs ! i, Stay)) [0..<length rs])" lemma proper_cmd_write_many: "proper_command k (cmd_write_many J h)" unfolding cmd_write_many_def by auto lemma sem_cmd_write_many: shows "sem (cmd_write_many J h) (0, tps) = (1, map (λj. if j ∈ J then tps ! j |:=| h else tps ! j) [0..<length tps])" using cmd_write_many_def read_length act_Stay by (intro semI[OF proper_cmd_write_many]) auto definition tm_write_many :: "tapeidx set ⇒ symbol ⇒ machine" where "tm_write_many J h ≡ [cmd_write_many J h]" lemma tm_write_many_tm: assumes "0 ∉ J" and "∀j∈J. j < k" and "h < G" and "k ≥ 2" and "G ≥ 4" shows "turing_machine k G (tm_write_many J h)" unfolding tm_write_many_def cmd_write_many_def using assms turing_machine_def by auto lemma exe_tm_write_many: "exe (tm_write_many J h) (0, tps) = (1, map (λj. if j ∈ J then tps ! j |:=| h else tps ! j) [0..<length tps])" unfolding tm_write_many_def using sem_cmd_write_many exe_lt_length by simp lemma execute_tm_write_many: "execute (tm_write_many J h) (0, tps) 1 = (1, map (λj. if j ∈ J then tps ! j |:=| h else tps ! j) [0..<length tps])" using exe_tm_write_many by simp lemma transforms_tm_write_many: "transforms (tm_write_many J h) tps 1 (map (λj. if j ∈ J then tps ! j |:=| h else tps ! j) [0..<length tps])" using execute_tm_write_many transits_def transforms_def tm_write_many_def by auto lemma transforms_tm_write_manyI [transforms_intros]: assumes "∀j∈J. j < k" and "length tps = k" and "length tps' = k" and "⋀j. j ∈ J ⟹ tps' ! j = tps ! j |:=| h" and "⋀j. j < k ⟹ j ∉ J ⟹ tps' ! j = tps ! j" shows "transforms (tm_write_many J h) tps 1 tps'" proof - have "tps' = map (λj. if j ∈ J then tps ! j |:=| h else tps ! j) [0..<length tps]" using assms by (intro nth_equalityI) simp_all then show ?thesis using assms transforms_tm_write_many by auto qed subsection ‹Writing a symbol multiple times› text ‹ In this section we devise a Turing machine that writes the symbol sequence $h^m$ with a hard-coded symbol $h$ and number $m$ to a tape. The resulting tape is defined by the next operation: › definition overwrite :: "tape ⇒ symbol ⇒ nat ⇒ tape" where "overwrite tp h m ≡ (λi. if snd tp ≤ i ∧ i < snd tp + m then h else fst tp i, snd tp + m)" lemma overwrite_0: "overwrite tp h 0 = tp" proof - have "snd (overwrite tp h 0) = snd tp" unfolding overwrite_def by simp moreover have "fst (overwrite tp h 0) = fst tp" unfolding overwrite_def by auto ultimately show ?thesis using prod_eqI by blast qed lemma overwrite_upd: "(overwrite tp h t) |:=| h |+| 1 = overwrite tp h (Suc t)" using overwrite_def by auto lemma overwrite_upd': assumes "j < length tps" and "tps' = tps[j := overwrite (tps ! j) h t]" shows "(tps[j := overwrite (tps ! j) h t])[j := tps' ! j |:=| h |+| 1] = tps[j := overwrite (tps ! j) h (Suc t)]" using assms overwrite_upd by simp text ‹ The next command writes the symbol $h$ to the tape $j$ and moves the tape head to the right. › definition cmd_char :: "tapeidx ⇒ symbol ⇒ command" where "cmd_char j z = cmd_rtrans j (λ_. z)" lemma turing_command_char: assumes "0 < j" and "j < k" and "h < G" shows "turing_command k 1 G (cmd_char j h)" unfolding cmd_char_def cmd_rtrans_def using assms by auto definition tm_char :: "tapeidx ⇒ symbol ⇒ machine" where "tm_char j z ≡ [cmd_char j z]" lemma tm_char_tm: assumes "0 < j" and "j < k" and "G ≥ 4" and "z < G" shows "turing_machine k G (tm_char j z)" using assms turing_command_char tm_char_def by auto lemma transforms_tm_charI [transforms_intros]: assumes "j < length tps" and "tps' = tps[j := tps ! j |:=| z |+| 1]" shows "transforms (tm_char j z) tps 1 tps'" using assms transforms_tm_rtransI tm_char_def cmd_char_def tm_rtrans_def by metis lemma sem_cmd_char: assumes "j < length tps" shows "sem (cmd_char j h) (0, tps) = (1, tps[j := tps ! j |:=| h |+| 1])" using cmd_char_def cmd_rtrans_def tapes_at_read read_length assms act_Right by (intro semI) auto text ‹ The next TM is a sequence of $m$ @{const cmd_char} commands properly relocated. It writes a sequence of $m$ times the symbol $h$ to tape $j$. › definition tm_write_repeat :: "tapeidx ⇒ symbol ⇒ nat ⇒ machine" where "tm_write_repeat j h m ≡ map (λi. relocate_cmd i (cmd_char j h)) [0..<m]" lemma tm_write_repeat_tm: assumes "0 < j" and "j < k" and "h < G" and "k ≥ 2" and "G ≥ 4" shows "turing_machine k G (tm_write_repeat j h m)" proof let ?M = "tm_write_repeat j h m" show "2 ≤ k" and "4 ≤ G" using assms(4,5) . show "turing_command k (length ?M) G (?M ! i)" if "i < length ?M" for i proof - have "?M ! i = relocate_cmd i (cmd_char j h)" using that tm_write_repeat_def by simp then have "turing_command k (1 + i) G (?M ! i)" using assms turing_command_char turing_command_relocate_cmd by metis then show ?thesis using turing_command_mono that by simp qed qed lemma exe_tm_write_repeat: assumes "j < length tps" and "q < m" shows "exe (tm_write_repeat j h m) (q, tps) = (Suc q, tps[j := tps ! j |:=| h |+| 1])" using sem_cmd_char assms sem sem_relocate_cmd tm_write_repeat_def by (auto simp add: exe_lt_length) lemma execute_tm_write_repeat: assumes "j < length tps" and "t ≤ m" shows "execute (tm_write_repeat j h m) (0, tps) t = (t, tps[j := overwrite (tps ! j) h t])" using assms(2) proof (induction t) case 0 then show ?case using overwrite_0 by simp next case (Suc t) then have "t < m" by simp have "execute (tm_write_repeat j h m) (0, tps) (Suc t) = exe (tm_write_repeat j h m) (execute (tm_write_repeat j h m) (0, tps) t)" by simp also have "... = exe (tm_write_repeat j h m) (t, tps[j := overwrite (tps ! j) h t])" using Suc by simp also have "... = (Suc t, tps[j := overwrite (tps ! j) h (Suc t)])" using `t < m` exe_tm_write_repeat assms overwrite_upd' by simp finally show ?case . qed lemma transforms_tm_write_repeatI [transforms_intros]: assumes "j < length tps" and "tps' = tps[j := overwrite (tps ! j) h m]" shows "transforms (tm_write_repeat j h m) tps m tps'" using assms execute_tm_write_repeat transits_def transforms_def tm_write_repeat_def by auto subsection ‹Moving to the start of the tape› text ‹ The next command moves the head on tape $j$ to the left until it reaches a symbol from the set $H$: › definition cmd_left_until :: "symbol set ⇒ tapeidx ⇒ command" where "cmd_left_until H j rs ≡ if rs ! j ∈ H then (1, map (λr. (r, Stay)) rs) else (0, map (λi. (rs ! i, if i = j then Left else Stay)) [0..<length rs])" lemma sem_cmd_left_until_1: assumes "j < k" and "length tps = k" and "(0, tps) <.> j ∈ H" shows "sem (cmd_left_until H j) (0, tps) = (1, tps)" <