section ‹Existence of two-tape oblivious Turing machines\label{s:oblivious-two-tape}› theory Oblivious_2_Tape imports Oblivious_Polynomial NP begin text ‹ In this section we show that for every polynomial-time multi-tape Turing machine there is a polynomial-time two-tape oblivious Turing machine that computes the same function and halts with its output tape head in cell number~1. Consider a $k$-tape Turing machine $M$ with polynomially bounded running time $T$. We construct a two-tape oblivious Turing machine $S$ simulating $M$ as follows. Lemma @{thm [source] polystructor} from the previous section provides us with a polynomial-time two-tape oblivious TM and a function $f(n) \geq T(n)$ such that the TM outputs $\mathbf{1}^{f(n)}$ for all inputs of length $n$. Executing this TM is the first thing our simulator does. The $f(n)$ symbols~@{text 𝟭} mark the space $S$ is going to use. Every cell $i=0, \dots, f(n) - 1$ of this space is to store a symbol that encodes a $(2k + 2)$-tuple consisting of: \begin{itemize} \item $k$ symbols from $M$'s alphabet representing the contents of all the $i$-th cells on the $k$ tapes of $M$; \item $k$ flags (called ``head flags'') signalling which of the $k$ tape heads of $M$ is in cell $i$; \item a flag (called ``counter flag'') initialized with 0; \item a flag (called ``start flag'') signalling whether $i = 0$. \end{itemize} Together the counter flags are a unary counter from 0 to $f(n)$. They are toggled from left to right. The start flags never change. The symbols and the head flags represent the $k$ tapes of $M$ at some step of the execution. By choice of $f$ the TM $M$ cannot use more than $f(n)$ cells on any tape. So the space marked with @{text 𝟭} symbols on the simulator's output tape suffices. Next the simulator initializes the space of @{text 𝟭} symbols with code symbols representing the start configuration of $M$ for the input given to the simulator. Then the main loop of the simulation performs $f(n)$ iterations. In each iteration $S$ performs one step of $M$'s computation. In order to do this it performs several left-to-right and right-to-left sweeps over all the $f(n)$ cells in the formatted section of the output tape. A sweep will move the output tape head one cell right (respectively left) in each step. In this way the simulator's head positions at any time will only depend on $f(n)$, and hence on $n$. Thus the machine will be oblivious. Moreover $f(n) \ge T(n)$, and so $M$ will be in the halting state after $f(n)$ iterations of the simulation. Counting the iterations to $f(n)$ is achieved via the counter flags. Finally the simulator extracts from each code symbol the symbol corresponding to $M$'s output tape, thus reconstructing the output of $M$ on the simulator's output tape. Thanks to the start flags, the simulator can easily locate the leftmost cell and put the output tape head one to the right of it, as required. The construction heavily uses the memorization-in-states technique (see Chapter~\ref{s:tm-memorizing}). At first the machine features $2k + 1$ memorization tapes in addition to the input tape and output tape. The purpose of those tapes is to store $M$'s state and the symbols under the tape heads of $M$ in the currently simulated step of $M$'s execution, as well as the $k$ symbols to be written write and head movements to be executed by the simulator. › text ‹ The next predicate expresses that a Turing machine halts within a time bound depending on the length of the input. We did not have a need for this fairly basic predicate yet, because so far we were always interested in the halting configuration, too, and so the predicate @{const computes_in_time} sufficed. \null › definition time_bound :: "machine ⇒ nat ⇒ (nat ⇒ nat) ⇒ bool" where "time_bound M k T ≡ ∀zs. bit_symbols zs ⟶ fst (execute M (start_config k zs) (T (length zs))) = length M" lemma time_bound_ge: assumes "time_bound M k T" and "∀n. fmt n ≥ T n" shows "time_bound M k fmt" using time_bound_def assms by (metis execute_after_halting_ge) text ‹ The time bound also bounds the position of all the tape heads. › lemma head_pos_le_time_bound: assumes "turing_machine k G M" and "time_bound M k T" and "bit_symbols zs" and "j < k" shows "execute M (start_config k zs) t <#> j ≤ T (length zs)" using assms time_bound_def[of M k T] execute_after_halting_ge head_pos_le_time[OF assms(1,4)] by (metis (no_types, lifting) nat_le_linear) text ‹ The entire construction will take place in a locale that assumes a polynomial-time $k$-tape Turing machine $M$. › locale two_tape = fixes M :: machine and k G :: nat and T :: "nat ⇒ nat" assumes tm_M: "turing_machine k G M" and poly_T: "big_oh_poly T" and time_bound_T: "time_bound M k T" begin lemma k_ge_2: "k ≥ 2" using tm_M turing_machine_def by simp lemma G_ge_4: "G ≥ 4" using tm_M turing_machine_def by simp text ‹ The construction of the simulator relies on the formatted space on the output tape to be large enough to hold the input. The size of the formatted space depends on the time bound $T$, which might be less than the length of the input. To ensure that the formatted space is large enough we increase the time bound while keeping it polynomial. The new bound is $T'$: › definition T' :: "nat ⇒ nat" where "T' n ≡ T n + n" lemma poly_T': "big_oh_poly T'" proof - have "big_oh_poly (λn. n)" using big_oh_poly_poly[of 1] by simp then show ?thesis using T'_def big_oh_poly_sum[OF poly_T] by presburger qed lemma time_bound_T': "time_bound M k T'" using T'_def time_bound_ge[OF time_bound_T, of T'] by simp subsection ‹Encoding multiple tapes into one› text ‹ The symbols on the output tape of the simulator are supposed to encode a $(2k + 2)$-tuple, where the first $k$ elements assume one of the values in $\{0, \dots, G - 1\}$, whereas the other $k + 2$ are flags with two possible values only. For uniformity we define an encoding where all elements range over $G$ values and that works for tuples of every length. › fun encode :: "nat list ⇒ nat" where "encode [] = 0" | "encode (x # xs) = x + G * encode xs" text ‹ For every $m \in \nat$, the enocoding is a bijective mapping from $\{0, \dots, G - 1\}^m$ to $\{0, \dots, G^m - 1\}$. › lemma encode_surj: assumes "n < G ^ m" shows "∃xs. length xs = m ∧ (∀x∈set xs. x < G) ∧ encode xs = n" using assms proof (induction m arbitrary: n) case 0 then show ?case by simp next case (Suc m) define q where "q = n div G" define r where "r = n mod G" have "q < G ^ m" using Suc q_def by (auto simp add: less_mult_imp_div_less power_commutes) then obtain xs' where xs': "length xs' = m" "∀x∈set xs'. x < G" "encode xs' = q" using Suc by auto have "r < G" using r_def G_ge_4 by simp have "encode (r # xs') = n" using xs'(3) q_def r_def G_ge_4 by simp moreover have "∀x∈set (r # xs'). x < G" using xs'(2) `r < G` by simp moreover have "length (r # xs') = Suc m" using xs'(1) by simp ultimately show ?case by blast qed lemma encode_inj: assumes "∀x∈set xs. x < G" and "length xs = m" and "∀y∈set ys. y < G" and "length ys = m" and "encode xs = encode ys" shows "xs = ys" using assms proof (induction m arbitrary: xs ys) case 0 then show ?case by simp next case (Suc m) obtain x xs' y ys' where xy: "xs = x # xs'" "ys = y # ys'" using Suc by (metis Suc_length_conv) then have len: "length xs' = m" "length ys' = m" using Suc by simp_all have *: "x + G * encode xs' = y + G * encode ys'" using Suc xy by simp moreover have "(x + G * encode xs') mod G = x" by (simp add: Suc.prems(1) xy(1)) moreover have "(y + G * encode ys') mod G = y" by (simp add: Suc.prems(3) xy(2)) ultimately have "x = y" by simp with * have "G * encode xs' = G * encode ys'" by simp then have "encode xs' = encode ys'" using G_ge_4 by simp with len Suc xy have "xs' = ys'" by simp then show ?case using `x = y` xy by simp qed lemma encode_less: assumes "∀x∈set xs. x < G" shows "encode xs < G ^ (length xs)" using assms proof (induction xs) case Nil then show ?case by simp next case (Cons x xs) then have "x < G" by simp have "encode (x # xs) = x + G * encode xs" by simp also have "... ≤ x + G * (G ^ (length xs) - 1)" using Cons by simp also have "... = x + G * G ^ (length xs) - G" by (simp add: right_diff_distrib') also have "... < G * G ^ (length xs)" using `x < G` less_imp_Suc_add by fastforce also have "... = G ^ (Suc (length xs))" by simp finally have "encode (x # xs) < G ^ (length (x # xs))" by simp then show ?case . qed text ‹ Decoding a number into an $m$-tuple of numbers is then a well-defined operation. › definition decode :: "nat ⇒ nat ⇒ nat list" where "decode m n ≡ THE xs. encode xs = n ∧ length xs = m ∧ (∀x∈set xs. x < G)" lemma decode: assumes "n < G ^ m" shows encode_decode: "encode (decode m n) = n" and length_decode: "length (decode m n) = m" and decode_less_G: "∀x∈set (decode m n). x < G" proof - have "∃xs. length xs = m ∧ (∀x∈set xs. x < G) ∧ encode xs = n" using assms encode_surj by simp then have *: "∃!xs. encode xs = n ∧ length xs = m ∧ (∀x∈set xs. x < G)" using encode_inj by auto let ?xs = "decode m n" let ?P = "λxs. encode xs = n ∧ length xs = m ∧ (∀x∈set xs. x < G)" have "encode ?xs = n ∧ length ?xs = m ∧ (∀x∈set ?xs. x < G)" using * theI'[of ?P] decode_def by simp then show "encode (decode m n) = n" and "length (decode m n) = m" and "∀x∈set (decode m n). x < G" by simp_all qed lemma decode_encode: "∀x∈set xs. x < G ⟹ decode (length xs) (encode xs) = xs" proof - fix xs :: "nat list" assume a: "∀x∈set xs. x < G" then have "encode xs < G ^ (length xs)" using encode_less by simp show "decode (length xs) (encode xs) = xs" unfolding decode_def proof (rule the_equality) show "encode xs = encode xs ∧ length xs = length xs ∧ (∀x∈set xs. x < G)" using a by simp show "⋀ys. encode ys = encode xs ∧ length ys = length xs ∧ (∀x∈set ys. x < G) ⟹ ys = xs" using a encode_inj by simp qed qed text ‹ The simulator will access and update components of the encoded symbol. › definition encode_nth :: "nat ⇒ nat ⇒ nat ⇒ nat" where "encode_nth m n j ≡ decode m n ! j" definition encode_upd :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat" where "encode_upd m n j x ≡ encode ((decode m n) [j:=x])" lemma encode_nth_less: assumes "n < G ^ m" and "j < m" shows "encode_nth m n j < G" using assms encode_nth_def decode_less_G length_decode by simp text ‹ For the symbols the simulator actually uses, we fix $m = 2k + 2$ and reserve the symbols $\triangleright$ and $\Box$, effectively shifting the symbols by two. We call the symbols $\{2, \dots, G^{2k+2} + 2\}$ ``code symbols''. › definition enc :: "symbol list ⇒ symbol" where "enc xs ≡ encode xs + 2" definition dec :: "symbol ⇒ symbol list" where "dec n ≡ decode (2 * k + 2) (n - 2)" lemma dec: assumes "n > 1" and "n < G ^ (2 * k + 2) + 2" shows enc_dec: "enc (dec n) = n" and length_dec: "length (dec n) = 2 * k + 2" and dec_less_G: "∀x∈set (dec n). x < G" proof - show "enc (dec n) = n" using enc_def dec_def encode_decode assms by simp show "length (dec n) = 2 * k + 2" using enc_def dec_def length_decode assms by simp show "∀x∈set (dec n). x < G" using enc_def dec_def decode_less_G assms by (metis Suc_leI less_diff_conv2 one_add_one plus_1_eq_Suc) qed lemma dec_enc: "∀x∈set xs. x < G ⟹ length xs = 2 * k + 2 ⟹ dec (enc xs) = xs" unfolding enc_def dec_def using decode_encode by fastforce definition enc_nth :: "nat ⇒ nat ⇒ nat" where "enc_nth n j ≡ dec n ! j" lemma enc_nth: "∀x∈set xs. x < G ⟹ length xs = 2 * k + 2 ⟹ enc_nth (enc xs) j = xs ! j" unfolding enc_nth_def by (simp add: dec_enc) lemma enc_nth_dec: assumes "n > 1" and "n < G ^ (2 * k + 2) + 2" shows "enc_nth n j = (dec n) ! j" using assms enc_nth dec by metis abbreviation is_code :: "nat ⇒ bool" where "is_code n ≡ n < G ^ (2 * k + 2) + 2 ∧ 1 < n" lemma enc_nth_less: assumes "is_code n" and "j < 2 * k + 2" shows "enc_nth n j < G" using assms enc_nth_def by (metis dec_less_G in_set_conv_nth length_dec) lemma enc_less: "∀x∈set xs. x < G ⟹ length xs = 2 * k + 2 ⟹ enc xs < G ^ (2 * k + 2) + 2" using encode_less enc_def by fastforce definition enc_upd :: "nat ⇒ nat ⇒ nat ⇒ nat" where "enc_upd n j x ≡ enc ((dec n) [j:=x])" lemma enc_upd_is_code: assumes "is_code n" and "j < 2 * k + 2" and "x < G" shows "is_code (enc_upd n j x)" proof - let ?ys = "(dec n) [j:=x]" have "∀h∈set (dec n). h < G" using assms(1,2) dec_less_G by auto then have "∀h∈set ?ys. h < G" using assms(3) by (metis in_set_conv_nth length_list_update nth_list_update_eq nth_list_update_neq) moreover have "length ?ys = 2 * k + 2" using assms length_dec by simp ultimately have "enc ?ys < G ^ (2 * k + 2) + 2" using enc_less by simp then show ?thesis using enc_upd_def enc_def by simp qed text ‹ The code symbols require the simulator to have an alphabet of at least size $G^{2k + 2} + 2$. On top of that we want to store on a memorization tape the state that $M$ is in. So the alphabet must have at least @{term "length M + 1"} symbols. Both conditions are met by the simulator having an alphabet of size $G'$: › definition G' :: nat where "G' ≡ G ^ (2 * k + 2) + 2 + length M" lemma G'_ge_6: "G' ≥ 6" proof - have "4 ^ 2 > (5::nat)" by simp then have "G ^ 2 > (5::nat)" using G_ge_4 less_le_trans power2_nat_le_eq_le by blast then have "G ^ (2 * k + 2) > (5::nat)" using k_ge_2 G_ge_4 by (metis (no_types, opaque_lifting) dec_induct le_add2 order_less_le_subst1 pow_mono zero_less_Suc zero_less_numeral) then show ?thesis using G'_def by simp qed corollary G'_ge: "G' ≥ 4" "G' ≥ 5" using G'_ge_6 by simp_all lemma G'_ge_G: "G' ≥ G" proof - have "G ^ 2 ≥ G" by (simp add: power2_nat_le_imp_le) then have "G ^ (2 * k + 2) ≥ G" by simp then show ?thesis using G'_def by linarith qed corollary enc_less_G': "∀x∈set xs. x < G ⟹ length xs = 2 * k + 2 ⟹ enc xs < G'" using enc_less G'_def by fastforce lemma enc_greater: "enc xs > 1" using enc_def by simp subsection ‹Construction of the simulator Turing machine› text ‹ The simulator is a sequence of three Turing machines: The ``formatter'', which initializes the output tape; the loop, which simulates the TM $M$ for polynomially many steps; and a cleanup TM, which makes the output tape look like the output tape of $M$. All these machines are discussed in order in the following subsections. The simulator will start with $2k + 1$ memorization tapes for a total of $2k + 3$ tapes. The simulation action will take place on the output tape. › subsubsection ‹Initializing the simulator's tapes› text ‹ The function @{const T'} is polynomially bounded and therefore there is a polynomial-time two-tape oblivious Turing machine that outputs at least $T'(n)$ symbols~@{text 𝟭} on an input of length $n$, as we have proven in the previous section (lemma~@{thm [source] polystructor}). We now obtain such a Turing machine together with its running time bound and trace. This TM will be one of our blocks for building the simulator TM. We will call it the ``formatter''. \null › definition fmt_es_pM :: "(nat ⇒ nat) × (nat ⇒ (nat × nat) list) × machine" where "fmt_es_pM ≡ SOME tec. turing_machine 2 G' (snd (snd tec)) ∧ big_oh_poly (λn. length ((fst (snd tec)) n)) ∧ big_oh_poly (fst tec) ∧ (∀n. T' n ≤ (fst tec) n) ∧ (∀zs. proper_symbols zs ⟶ traces (snd (snd tec)) (start_tapes_2 zs) ((fst (snd tec)) (length zs)) (one_tapes_2 zs ((fst tec) (length zs))))" lemma polystructor': fixes GG :: nat and g :: "nat ⇒ nat" assumes "big_oh_poly g" and "GG ≥ 5" shows "∃f_es_M. turing_machine 2 GG (snd (snd f_es_M)) ∧ big_oh_poly (λn. length ((fst (snd f_es_M)) n)) ∧ big_oh_poly (fst f_es_M) ∧ (∀n. g n ≤ (fst f_es_M) n) ∧ (∀zs. proper_symbols zs ⟶ traces (snd (snd f_es_M)) (start_tapes_2 zs) ((fst (snd f_es_M)) (length zs)) (one_tapes_2 zs ((fst f_es_M) (length zs))))" using polystructor[OF assms] by auto lemma fmt_es_pM: "turing_machine 2 G' (snd (snd fmt_es_pM)) ∧ big_oh_poly (λn. length ((fst (snd fmt_es_pM)) n)) ∧ big_oh_poly (fst fmt_es_pM) ∧ (∀n. T' n ≤ (fst fmt_es_pM) n) ∧ (∀zs. proper_symbols zs ⟶ traces (snd (snd fmt_es_pM)) (start_tapes_2 zs) ((fst (snd fmt_es_pM)) (length zs)) (one_tapes_2 zs ((fst fmt_es_pM) (length zs))))" using fmt_es_pM_def polystructor'[OF poly_T' G'_ge(2)] someI_ex[of "λtec. turing_machine 2 G' (snd (snd tec)) ∧ big_oh_poly (λn. length ((fst (snd tec)) n)) ∧ big_oh_poly (fst tec) ∧ (∀n. T' n ≤ (fst tec) n) ∧ (∀zs. proper_symbols zs ⟶ traces (snd (snd tec)) (start_tapes_2 zs) ((fst (snd tec)) (length zs)) (one_tapes_2 zs ((fst tec) (length zs))))"] by simp definition fmt :: "nat ⇒ nat" where "fmt ≡ fst fmt_es_pM" definition es_fmt :: "nat ⇒ (nat × nat) list" where "es_fmt ≡ fst (snd fmt_es_pM)" definition tm_fmt :: "machine" where "tm_fmt ≡ snd (snd fmt_es_pM)" text ‹ The formatter TM is @{const tm_fmt}, the number of @{text 𝟭} symbols written to the output tape on input of length $n$ is @{term "fmt n"}, and the trace on inputs of length $n$ is @{term "es_fmt n"}. › lemma fmt: "turing_machine 2 G' tm_fmt" "big_oh_poly (λn. length (es_fmt n))" "big_oh_poly fmt" "⋀n. T' n ≤ fmt n" "⋀zs. proper_symbols zs ⟹ traces tm_fmt (start_tapes_2 zs) (es_fmt (length zs)) (one_tapes_2 zs (fmt (length zs)))" unfolding fmt_def es_fmt_def tm_fmt_def using fmt_es_pM by simp_all lemma fmt_ge_n: "fmt n ≥ n" using fmt(4) T'_def by (metis dual_order.strict_trans2 le_less_linear not_add_less2) text ‹ The formatter is a two-tape TM. The first incarnation of the simulator will have two tapes and $2k + 1$ memorization tapes. So for now we formally need to extend the formatter to $2k + 3$ tapes: › definition "tm1 ≡ append_tapes 2 (2 * k + 3) tm_fmt" lemma tm1_tm: "turing_machine (2 * k + 3) G' tm1" unfolding tm1_def using append_tapes_tm by (simp add: fmt(1)) text ‹ Next we replace all non-blank symbols on the output tape by code symbols representing the tuple of $2k + 2$ zeros. › definition "tm1_2 ≡ tm_const_until 1 1 {□} (enc (replicate k 0 @ replicate k 0 @ [0, 0]))" lemma tm1_2_tm: "turing_machine (2 * k + 3) G' tm1_2" unfolding tm1_2_def using G'_ge proof (intro tm_const_until_tm, auto) show "enc (replicate k 0 @ replicate k 0 @ [0, 0]) < G'" using G_ge_4 by (intro enc_less_G', auto) qed definition "tm2 ≡ tm1 ;; tm1_2" lemma tm2_tm: "turing_machine (2 * k + 3) G' tm2" unfolding tm2_def using tm1_tm tm1_2_tm by simp definition "tm3 ≡ tm2 ;; tm_start 1" lemma tm3_tm: "turing_machine (2 * k + 3) G' tm3" unfolding tm3_def using tm2_tm tm_start_tm G'_ge by simp text ‹ Back at the start symbol of the output tape, we replace it by the code symbol for the tuple $1^k1^k01$. The first $k$ ones represent that initially the $k$ tapes of $M$ have the start symbol (numerically 1) in the leftmost cell. The second run of $k$ ones represent that initially all $k$ tapes have their tape heads in the leftmost cell. The following 0 is the first bit of the unary counter, currently set to zero. The final flag~1 signals that this is the leftmost cell. Unlike the start symbols this signal flag cannot be overwritten by $M$. › definition "tm4 ≡ tm3 ;; tm_write 1 (enc (replicate k 1 @ replicate k 1 @ [0, 1]))" lemma tm3_4_tm: "turing_machine (2 * k + 3) G' (tm_write 1 (enc (replicate k 1 @ replicate k 1 @ [0, 1])))" using G'_ge enc_less_G' G_ge_4 tm_write_tm by simp lemma tm4_tm: "turing_machine (2 * k + 3) G' tm4" unfolding tm4_def using tm3_tm tm3_4_tm by simp definition "tm5 ≡ tm4 ;; tm_right 1" lemma tm5_tm: "turing_machine (2 * k + 3) G' tm5" unfolding tm5_def using tm4_tm by (simp add: G'_ge(1) tm_right_tm) text ‹ So far the simulator's output tape encodes $k$ tapes that are empty but for the start symbols. To represent the start configuration of $M$, we need to copy the contents of the input tape to the output tape. The following TM moves the work head to the first blank while copying the input tape content. Here we exploit $T'(n) \geq n$, which implies that the formatted section is long enough to hold the input. › definition "tm5_6 ≡ tm_trans_until 0 1 {0} (λh. enc (h mod G # replicate (k - 1) 0 @ replicate k 0 @ [0, 0]))" definition "tm6 ≡ tm5 ;; tm5_6" lemma tm5_6_tm: "turing_machine (2 * k + 3) G' tm5_6" unfolding tm5_6_def proof (rule tm_trans_until_tm, auto simp add: G'_ge(1) G_ge_4 k_ge_2 enc_less_G') show "⋀h. h < G' ⟹ enc (h mod G # replicate (k - Suc 0) 0 @ replicate k 0 @ [0, 0]) < G'" using G_ge_4 k_ge_2 enc_less_G' by simp qed lemma tm6_tm: "turing_machine (2 * k + 3) G' tm6" unfolding tm6_def using tm5_tm tm5_6_tm by simp text ‹ Since we have overwritten the leftmost cell of the output tape with some code symbol, we cannot return to it using @{const tm_start}. But we can use @{const tm_left_until} with a special set of symbols: › abbreviation StartSym :: "symbol set" where "StartSym ≡ {y. y < G ^ (2 * k + 2) + 2 ∧ y > 1 ∧ dec y ! (2 * k + 1) = 1}" abbreviation "tm_left_until1 ≡ tm_left_until StartSym 1" lemma tm_left_until1_tm: "turing_machine (2 * k + 3) G' tm_left_until1" using tm_left_until_tm G'_ge(1) k_ge_2 by simp definition "tm7 ≡ tm6 ;; tm_left_until1" lemma tm7_tm: "turing_machine (2 * k + 3) G' tm7" unfolding tm7_def using tm6_tm tm_left_until1_tm by simp text ‹ Tape number $2$ is meant to memorize $M$'s state during the simulation. Initially the state is the start state, that is, zero. › definition "tm8 ≡ tm7 ;; tm_write 2 0" lemma tm8_tm: "turing_machine (2 * k + 3) G' tm8" unfolding tm8_def using tm7_tm tm_write_tm k_ge_2 G'_ge(1) by simp text ‹ We also initialize memorization tapes $3, \dots, 2k + 2$ to zero. This concludes the initialization of the simulator's tapes. › definition "tm9 ≡ tm8 ;; tm_write_many {3..<2 * k + 3} 0" lemma tm9_tm: "turing_machine (2 * k + 3) G' tm9" unfolding tm9_def using tm8_tm tm_write_many_tm k_ge_2 G'_ge(1) by simp subsubsection ‹The loop› text ‹ The core of the simulator is a loop whose body is executed @{term "fmt n"} many times. Each iteration simulates one step of the Turing machine $M$. For the analysis of the loop we describe the $2k + 3$ tapes in the form @{term "[a, b, c] @ map f1 [0..<k] @ map f2 [0..<k]"}. › lemma threeplus2k_2: assumes "3 ≤ j ∧ j < k + 3" shows "([a, b, c] @ map f1 [0..<k] @ map f2 [0..<k]) ! j = f1 (j - 3)" using assms by (simp add: nth_append less_diff_conv2 numeral_3_eq_3) lemma threeplus2k_3: assumes "k + 3 ≤ j ∧ j < 2 * k + 3" shows "([a, b, c] @ map f1 [0..<k] @ map f2 [0..<k]) ! j = f2 (j - k - 3)" using assms by (simp add: nth_append less_diff_conv2 numeral_3_eq_3) text ‹ To ensure the loop runs for @{term "fmt n"} iterations we increment the unary counter in the code symbols in each iteration. The loop terminates when there are no more code symbols with an unset counter flag. The TM that prepares the loop condition sweeps the output tape left-to-right searching for the first symbol that is either blank or has an unset counter flag. The condition then checks for which of the two cases occurred. This is the condition TM: › definition "tmC ≡ tm_right_until 1 {y. y < G ^ (2 * k + 2) + 2 ∧ (y = 0 ∨ dec y ! (2 * k) = 0)}" lemma tmC_tm: "turing_machine (2 * k + 3) G' tmC" using tmC_def tm_right_until_tm using G'_ge(1) by simp text ‹ At the start of the iteration, the memorization tape~2 has the state of $M$, and all other memorization tapes contain $0$. The output tape head is at the leftmost code symbol with unset counter flag. The first order of business is to move back to the beginning of the output tape. › definition "tmL1 ≡ tm_left_until1" lemma tmL1_tm: "turing_machine (2 * k + 3) G' tmL1" unfolding tmL1_def using tm6_tm tm_left_until1_tm by simp text ‹ Then the output tape head sweeps right until it encounters a blank. During the sweep the Turing machine checks for any set head flags, and if it finds the one for tape $j$ set, it memorizes the symbol for tape $j$ on tape $3 + k + j$. The next command performs this operation: › definition cmdL2 :: command where "cmdL2 rs ≡ (if rs ! 1 = □ then (1, zip rs (replicate (2*k+3) Stay)) else (0, [(rs!0, Stay), (rs!1, Right), (rs!2, Stay)] @ (map (λj. (rs ! (j + 3), Stay)) [0..<k]) @ (map (λj. (if 1 < rs ! 1 ∧ rs ! 1 < G^(2*k+2)+2 ∧ enc_nth (rs!1) (k+j) = 1 then enc_nth (rs!1) j else rs!(3+k+j), Stay)) [0..<k])))" lemma cmdL2_at_eq_0: assumes "rs ! 1 = 0" and "j < 2 * k + 3" and "length rs = 2 * k + 3" shows "snd (cmdL2 rs) ! j = (rs ! j, Stay)" using assms by (simp add: cmdL2_def) lemma cmdL2_at_3: assumes "rs ! 1 ≠ □" and "3 ≤ j ∧ j < k + 3" shows "cmdL2 rs [!] j = (rs ! j, Stay)" using cmdL2_def assms threeplus2k_2 by (metis (no_types, lifting) le_add_diff_inverse2 snd_conv) lemma cmdL2_at_4: assumes "rs ! 1 ≠ □" and "k + 3 ≤ j ∧ j < 2 * k + 3" shows "cmdL2 rs [!] j = (if 1 < rs ! 1 ∧ rs ! 1 < G^(2*k+2)+2 ∧ enc_nth (rs ! 1) (j-3) = 1 then enc_nth (rs ! 1) (j-k-3) else rs ! j, Stay)" unfolding cmdL2_def using assms threeplus2k_3[OF assms(2), of "(rs ! 0, Stay)"] by simp lemma cmdL2_at_4'': assumes "rs ! 1 ≠ □" and "k + 3 ≤ j ∧ j < 2 * k + 3" and "¬ (1 < rs ! 1 ∧ rs ! 1 < G^(2*k+2)+2)" shows "cmdL2 rs [!] j = (rs ! j, Stay)" proof - have "cmdL2 rs [!] j = (if 1 < rs ! 1 ∧ rs ! 1 < G^(2*k+2)+2 ∧ enc_nth (rs!1) (j-3) = 1 then enc_nth (rs!1) (j-k-3) else rs!j, Stay)" using assms cmdL2_at_4 by blast then show ?thesis using assms(3) by auto qed lemma turing_command_cmdL2: "turing_command (2 * k + 3) 1 G' cmdL2" proof show "⋀gs. length gs = 2 * k + 3 ⟹ length ([!!] cmdL2 gs) = length gs" unfolding cmdL2_def by simp show "⋀gs. length gs = 2 * k + 3 ⟹ 0 < 2 * k + 3 ⟹ cmdL2 gs [.] 0 = gs ! 0" unfolding cmdL2_def by simp show "cmdL2 gs [.] j < G'" if "length gs = 2 * k + 3" "⋀i. i < length gs ⟹ gs ! i < G'" "j < length gs" for gs j proof (cases "gs ! 1 = 0") case True then have "cmdL2 gs = (1, zip gs (replicate (2*k+3) Stay))" unfolding cmdL2_def by simp have "cmdL2 gs [.] j = gs ! j" using that(1,3) by (simp add: ‹cmdL2 gs = (1, zip gs (replicate (2 * k + 3) Stay))›) then show ?thesis using that(2,3) by simp next case False consider "j = 0" | "j = 1" | "j = 2" | "3 ≤ j ∧ j < k + 3" | "k + 3 ≤ j ∧ j < 2 * k + 3" using ‹j < length gs› ‹length gs = 2 * k + 3› by linarith then show ?thesis proof (cases) case 1 then show ?thesis by (simp add: cmdL2_def that(1) that(2)) next case 2 then show ?thesis unfolding cmdL2_def using False that by auto next case 3 then show ?thesis unfolding cmdL2_def using False that by auto next case 4 then have "snd (cmdL2 gs) ! j = (gs ! j, Stay)" unfolding cmdL2_def using False that threeplus2k_2[OF 4, of "(gs ! 0, Stay)"] by simp then show ?thesis using that by (simp add: ‹snd (cmdL2 gs) ! j = (gs ! j, Stay)›) next case 5 show ?thesis proof (cases "1 < gs ! 1 ∧ gs ! 1 < G ^ (2*k+2) + 2") case True then have *: "cmdL2 gs [.] j = (if enc_nth (gs ! 1) (j-3) = 1 then enc_nth (gs ! 1) (j-k-3) else gs ! j)" using 5 False by (simp add: cmdL2_at_4) let ?n = "gs ! 1" have len: "length (dec ?n) = 2 * k + 2" and less_G: "∀x∈set (dec ?n). x < G" using True length_dec dec_less_G by (simp, blast) have **: "enc_nth ?n (j-k-3) = dec ?n ! (j-k-3)" using enc_nth_dec True by simp then have "dec ?n ! (j-k-3) < G" using less_G 5 len by auto then have "dec ?n ! (j-k-3) < G'" using G'_ge_G by simp moreover have "gs ! j < G'" using that by simp ultimately show ?thesis using * ** by simp next case 6: False have "cmdL2 gs [!] j = (gs ! j, Stay)" using cmdL2_at_4''[OF False 5 6] by simp then show ?thesis using that by (simp add: ‹snd (cmdL2 gs) ! j = (gs ! j, Stay)›) qed qed qed show "⋀gs. length gs = 2 * k + 3 ⟹ [*] (cmdL2 gs) ≤ 1" using cmdL2_def by simp qed definition "tmL1_2 ≡ [cmdL2]" lemma tmL1_2_tm: "turing_machine (2 * k + 3) G' tmL1_2" using tmL1_2_def using turing_command_cmdL2 G'_ge by auto definition "tmL2 ≡ tmL1 ;; tmL1_2" lemma tmL2_tm: "turing_machine (2 * k + 3) G' tmL2" by (simp add: tmL1_2_tm tmL1_tm tmL2_def) text ‹ The memorization tapes $3, \dots, 2 + k$ will store the head movements for tapes $0, \dots, k - 1$ of $M$. The directions are encoded as symbols thus: › definition direction_to_symbol :: "direction ⇒ symbol" where "direction_to_symbol m ≡ (case m of Left ⇒ □ | Stay ⇒ ▹ | Right ⇒ 𝟬)" lemma direction_to_symbol_less: "direction_to_symbol m < 3" using direction_to_symbol_def by (cases m) simp_all text ‹ At this point in the iteration the memorization tapes $k + 3, \dots, 2k+2$ contain the symbols under the $k$ tape heads of $M$, and tape $2$ contains the state $M$ is in. Therefore all information is available to determine the actions $M$ is taking in the step currently simulated. The next command has the entire behavior of $M$ ``hard-coded'' and causes the actions to be stored on memorization tapes $3, \dots, 2k+2$: the output symbols on the tapes $k + 3, \dots, 2k + 2$, and the $k$ head movements on the tapes $3, \dots, k + 2$. The follow-up state will again be memorized on tape $2$. All this happens in one step of the simulator machine. › definition cmdL3 :: command where "cmdL3 rs ≡ (1, [(rs ! 0, Stay), (rs ! 1, Stay), (if rs ! 2 < length M ∧ (∀h∈set (drop (k + 3) rs). h < G) then fst ((M ! (rs ! 2)) (drop (k + 3) rs)) else rs ! 2, Stay)] @ map (λj. (if rs ! 2 < length M ∧ (∀h∈set (drop (k + 3) rs). h < G) then direction_to_symbol ((M ! (rs ! 2)) (drop (k + 3) rs) [~] j) else 1, Stay)) [0..<k] @ map (λj. (if rs ! 2 < length M ∧ (∀h∈set (drop (k + 3) rs). h < G) then ((M ! (rs ! 2)) (drop (k + 3) rs) [.] j) else rs ! (k + 3 + j), Stay)) [0..<k])" lemma cmdL3_at_2a: assumes "gs ! 2 < length M ∧ (∀h∈set (drop (k + 3) gs). h < G)" shows "cmdL3 gs [!] 2 = (fst ((M ! (gs ! 2)) (drop (k + 3) gs)), Stay)" using cmdL3_def assms by simp lemma cmdL3_at_2b: assumes "¬ (gs ! 2 < length M ∧ (∀h∈set (drop (k + 3) gs). h < G))" shows "cmdL3 gs [!] 2 = (gs ! 2, Stay)" using cmdL3_def assms by auto lemma cmdL3_at_3a: assumes "3 ≤ j ∧ j < k + 3" and "gs ! 2 < length M ∧ (∀h∈set (drop (k + 3) gs). h < G)" shows "cmdL3 gs [!] j = (direction_to_symbol ((M ! (gs ! 2)) (drop (k + 3) gs) [~] (j - 3)), Stay)" using cmdL3_def assms(2) threeplus2k_2[OF assms(1), of "(gs ! 0, Stay)"] by simp lemma cmdL3_at_3b: assumes "3 ≤ j ∧ j < k + 3" and "¬ (gs ! 2 < length M ∧ (∀h∈set (drop (k + 3) gs). h < G))" shows "cmdL3 gs [!] j = (1, Stay)" using cmdL3_def assms(2) threeplus2k_2[OF assms(1), of "(gs ! 0, Stay)"] by auto lemma cmdL3_at_4a: assumes "k + 3 ≤ j ∧ j < 2 * k + 3" and "gs ! 2 < length M ∧ (∀h∈set (drop (k + 3) gs). h < G)" shows "cmdL3 gs [!] j = ((M ! (gs ! 2)) (drop (k + 3) gs) [.] (j - k - 3), Stay)" using cmdL3_def assms(2) threeplus2k_3[OF assms(1), of "(gs ! 0, Stay)"] by simp lemma cmdL3_at_4b: assumes "k + 3 ≤ j ∧ j < 2 * k + 3" and "¬ (gs ! 2 < length M ∧ (∀h∈set (drop (k + 3) gs). h < G))" shows "cmdL3 gs [!] j = (gs ! j, Stay)" using assms cmdL3_def threeplus2k_3[OF assms(1), of "(gs ! 0, Stay)"] by auto lemma cmdL3_if_comm: assumes "length gs = 2 * k + 3" and "gs ! 2 < length M ∧ (∀h∈set (drop (k + 3) gs). h < G)" shows "length ([!!] (M ! (gs ! 2)) (drop (k + 3) gs)) = k" and "⋀j. j < k ⟹ (M ! (gs ! 2)) (drop (k + 3) gs) [.] j < G" proof - let ?rs = "drop (k + 3) gs" let ?cmd = "M ! (gs ! 2)" have *: "turing_command k (length M) G ?cmd" using assms(2) tm_M turing_machineD(3) by simp then show "length ([!!] ?cmd ?rs) = k" using turing_commandD(1) assms(1) by simp have "⋀i. i < length ?rs ⟹ ?rs ! i < G" using assms(2) nth_mem by blast then show "⋀j. j < k ⟹ (M ! (gs ! 2)) (drop (k + 3) gs) [.] j < G" using * turing_commandD(2) assms by simp qed lemma turing_command_cmdL3: "turing_command (2 * k + 3) 1 G' cmdL3" proof show "⋀gs. length gs = 2 * k + 3 ⟹ length ([!!] cmdL3 gs) = length gs" using cmdL3_def by simp show "⋀gs. length gs = 2 * k + 3 ⟹ 0 < 2 * k + 3 ⟹ cmdL3 gs [.] 0 = gs ! 0" using cmdL3_def by simp show "cmdL3 gs [.] j < G'" if "length gs = 2 * k + 3" "⋀i. i < length gs ⟹ gs ! i < G'" "j < length gs" for gs j proof - consider "j = 0" | "j = 1" | "j = 2" | "3 ≤ j ∧ j < k + 3" | "k + 3 ≤ j ∧ j < 2 * k + 3" using ‹j < length gs› ‹length gs = 2 * k + 3› by linarith then show ?thesis proof (cases) case 1 then show ?thesis using that cmdL3_def by simp next case 2 then show ?thesis using that cmdL3_def by simp next case 3 then show ?thesis proof (cases "gs ! 2 < length M ∧ (∀h∈set (drop (k + 3) gs). h < G)") case True have "length (drop (k + 3) gs) = k" using that(1) by simp then have "fst ((M ! (gs ! 2)) (drop (k + 3) gs)) ≤ length M" using True turing_commandD(4) tm_M turing_machineD(3) by blast moreover have "cmdL3 gs [.] j = fst ((M ! (gs ! 2)) (drop (k + 3) gs))" using cmdL3_def True 3 by simp ultimately show ?thesis using G'_def by simp next case False then have "cmdL3 gs [.] j = gs ! 2" using cmdL3_def 3 by auto then show ?thesis using 3 that(2,3) by simp qed next case 4 then show ?thesis proof (cases "gs ! 2 < length M ∧ (∀h∈set (drop (k + 3) gs). h < G)") case True then have "cmdL3 gs [.] j = direction_to_symbol ((M ! (gs ! 2)) (drop (k + 3) gs) [~] (j - 3))" using cmdL3_at_3a 4 by simp then have "cmdL3 gs [.] j < 3" using direction_to_symbol_less by simp then show ?thesis using G'_ge by simp next case False then show ?thesis using cmdL3_at_3b[OF 4] G'_ge by simp qed next case 5 then show ?thesis proof (cases "gs ! 2 < length M ∧ (∀h∈set (drop (k + 3) gs). h < G)") case True then have "cmdL3 gs [.] j = (M ! (gs ! 2)) (drop (k + 3) gs) [.] (j - k - 3)" using cmdL3_at_4a[OF 5] by simp then have "cmdL3 gs [.] j < G" using cmdL3_if_comm True 5 that(1) by auto then show ?thesis using G'_ge_G by simp next case False then have "cmdL3 gs [.] j = gs ! j" using cmdL3_at_4b[OF 5] by simp then show ?thesis using that by simp qed qed qed show "⋀gs. length gs = 2 * k + 3 ⟹ [*] (cmdL3 gs) ≤ 1" using cmdL3_def by simp qed definition "tmL2_3 ≡ [cmdL3]" lemma tmL2_3_tm: "turing_machine (2 * k + 3) G' tmL2_3" unfolding tmL2_3_def using G'_ge(1) turing_command_cmdL3 by auto definition "tmL3 ≡ tmL2 ;; tmL2_3" lemma tmL3_tm: "turing_machine (2 * k + 3) G' tmL3" by (simp add: tmL2_3_tm tmL2_tm tmL3_def) text ‹ Next the output tape head sweeps left to the beginning of the tape, otherwise doing nothing. › definition "tmL4 ≡ tmL3 ;; tm_left_until1" lemma tmL4_tm: "turing_machine (2 * k + 3) G' tmL4" using tmL3_tm tmL4_def tmL1_def tm_left_until1_tm by simp text ‹ The next four commands @{term cmdL4}, @{term cmdL5}, @{term cmdL6}, @{term cmdL7} are parameterized by $jj = 0, \dots, k - 1$. Their job is applying the write operation and head movement for tape $jj$ of $M$. The entire block of commands will then be executed $k$ times, once for each $jj$. The first of these commands sweeps right again and applies the write operation for tape $jj$, which is memorized on tape $3 + k + jj$. To this end it checks for head flags and updates the code symbol component $jj$ with the contents of tape $3+k+jj$ when the head flag for tape $jj$ is set. › definition "cmdL5 jj rs ≡ if rs ! 1 = □ then (1, zip rs (replicate (2*k+3) Stay)) else (0, [(rs ! 0, Stay), (if is_code (rs ! 1) ∧ rs ! (3+k+jj) < G ∧ enc_nth (rs ! 1) (k+jj) = 1 then enc_upd (rs ! 1) jj (rs ! (3+k+jj)) else rs ! 1, Right), (rs ! 2, Stay)] @ (map (λj. (rs ! (j + 3), Stay)) [0..<k]) @ (map (λj. (rs ! (3 + k + j), Stay)) [0..<k]))" lemma cmdL5_eq_0: assumes "j < 2 * k + 3" and "length gs = 2 * k + 3" and "gs ! 1 = 0" shows "cmdL5 jj gs [!] j = (gs ! j, Stay)" unfolding cmdL5_def using assms by simp lemma cmdL5_at_0: assumes "gs ! 1 ≠ 0" shows "cmdL5 jj gs [!] 0 = (gs ! 0, Stay)" unfolding cmdL5_def using assms by simp lemma cmdL5_at_1: assumes "gs ! 1 ≠ 0" and "is_code (gs ! 1) ∧ gs ! (3+k+jj) < G ∧ enc_nth (gs!1) (k+jj) = 1" shows "cmdL5 jj gs [!] 1 = (enc_upd (gs!1) jj (gs!(3+k+jj)), Right)" unfolding cmdL5_def using assms by simp lemma cmdL5_at_1_else: assumes "gs ! 1 ≠ 0" and "¬ (is_code (gs ! 1) ∧ gs ! (3+k+jj) < G ∧ enc_nth (gs!1) (k+jj) = 1)" shows "cmdL5 jj gs [!] 1 = (gs ! 1, Right)" unfolding cmdL5_def using assms by auto lemma cmdL5_at_2: assumes "gs ! 1 ≠ 0" shows "cmdL5 jj gs [!] 2 = (gs ! 2, Stay)" unfolding cmdL5_def using assms by simp lemma cmdL5_at_3: assumes "gs ! 1 ≠ 0" and "3 ≤ j ∧ j < 3 + k" shows "cmdL5 jj gs [!] j = (gs ! j, Stay)" unfolding cmdL5_def using assms threeplus2k_2[where ?a="(gs ! 0, Stay)"] by simp lemma cmdL5_at_4: assumes "gs ! 1 ≠ 0" and "3 + k ≤ j ∧ j < 2 * k + 3" shows "cmdL5 jj gs [!] j = (gs ! j, Stay)" unfolding cmdL5_def using assms threeplus2k_3[where ?a="(gs ! 0, Stay)"] by simp lemma turing_command_cmdL5: assumes "jj < k" shows "turing_command (2 * k + 3) 1 G' (cmdL5 jj)" proof show "length gs = 2 * k + 3 ⟹ length ([!!] cmdL5 jj gs) = length gs" for gs unfolding cmdL5_def by (cases "gs!1=0") simp_all show goal2: "length gs = 2 * k + 3 ⟹ 0 < 2 * k + 3 ⟹ cmdL5 jj gs [.] 0 = gs ! 0" for gs unfolding cmdL5_def by (cases "gs ! 1=0") simp_all show "cmdL5 jj gs [.] j < G'" if "length gs = 2 * k + 3" "⋀i. i < length gs ⟹ gs ! i < G'" "j < length gs" for gs j proof (cases "gs ! 1 = 0") case True then show ?thesis using that cmdL5_eq_0 by simp next case False consider "j = 0" | "j = 1" | "j = 2" | "3 ≤ j ∧ j < k + 3" | "k + 3 ≤ j ∧ j < 2 * k + 3" using `length gs = 2 * k + 3` `j < length gs` by linarith then show ?thesis proof (cases) case 1 then show ?thesis using that goal2 by simp next case 2 show ?thesis proof (cases "1 < gs ! 1 ∧ gs ! 1 < G^(2*k+2)+2 ∧ gs ! (3+k+jj) < G ∧ enc_nth (gs ! 1) (k+jj) = 1") case True then have *: "cmdL5 jj gs [.] j = enc_upd (gs ! 1) jj (gs ! (3+k+jj))" using 2 cmdL5_at_1[OF False] by simp let ?n = "gs ! 1" let ?xs = "dec ?n" let ?ys = "(dec ?n) [jj:=gs!(3+k+jj)]" have "gs ! (3+k+jj) < G" using True by simp moreover have "∀h∈set (dec ?n). h < G" using True dec_less_G by auto ultimately have "∀h∈set ?ys. h < G" by (metis in_set_conv_nth length_list_update nth_list_update_eq nth_list_update_neq) moreover have "length ?ys = 2 * k + 2" using True length_dec by simp ultimately have "enc ?ys < G ^ (2 * k + 2) + 2" using enc_less by simp then show ?thesis using * by (simp add: enc_upd_def G'_def) next case b: False then show ?thesis using that cmdL5_at_1_else[OF False] 2 by simp qed next case 3 then show ?thesis using that cmdL5_at_2[OF False] by simp next case 4 then show ?thesis using that cmdL5_at_3[OF False] by simp next case 5 then show ?thesis using that cmdL5_at_4[OF False] by simp qed qed show "⋀gs. length gs = 2 * k + 3 ⟹ [*] (cmdL5 jj gs) ≤ 1" using cmdL5_def by (metis (no_types, lifting) One_nat_def fst_conv le_eq_less_or_eq plus_1_eq_Suc trans_le_add2) qed definition tmL45 :: "nat ⇒ machine" where "tmL45 jj ≡ [cmdL5 jj]" lemma tmL45_tm: assumes "jj < k" shows "turing_machine (2 * k + 3) G' (tmL45 jj)" using assms G'_ge turing_command_cmdL5 tmL45_def by auto text ‹ We move the output tape head one cell to the left. › definition "tmL46 jj ≡ tmL45 jj ;; tm_left 1" lemma tmL46_tm: assumes "jj < k" shows "turing_machine (2 * k + 3) G' (tmL46 jj)" using assms G'_ge tm_left_tm tmL45_tm tmL46_def tmL45_def by simp text ‹ The next command sweeps left and applies the head movement for tape $jj$ if this is a movement to the left. To this end it checks for a set head flag in component $k + jj$ of the code symbol and clears it. It also memorizes that it just cleared the head flag by changing the symbol on memorization tape $3 + jj$ to the number $3$, which is not used to encode any actual head movement. In the next step of the sweep it will recognize this $3$ and set the head flag in component $k + jj$ of the code symbol. The net result is that the head flag for tape $jj$ has moved one cell to the left. › abbreviation is_beginning :: "symbol ⇒ bool" where "is_beginning y ≡ is_code y ∧ dec y ! (2 * k + 1) = 1" definition cmdL7 :: "nat ⇒ command" where "cmdL7 jj rs ≡ (if is_beginning (rs ! 1) then 1 else 0, if rs ! (3 + jj) = □ ∧ enc_nth (rs ! 1) (k + jj) = 1 ∧ is_code (rs ! 1) ∧ ¬ is_beginning (rs ! 1) then [(rs ! 0, Stay), (enc_upd (rs ! 1) (k + jj) 0, Left), (rs ! 2, Stay)] @ (map (λj. (if j = jj then 3 else rs ! (j + 3), Stay)) [0..<k]) @ (map (λj. (rs ! (3 + k + j), Stay)) [0..<k]) else if rs ! (3 + jj) = 3 ∧ is_code (rs ! 1) then [(rs ! 0, Stay), (enc_upd (rs ! 1) (k + jj) 1, Left), (rs ! 2, Stay)] @ (map (λj. (if j = jj then 0 else rs ! (j + 3), Stay)) [0..<k]) @ (map (λj. (rs ! (3 + k + j), Stay)) [0..<k]) else [(rs ! 0, Stay), (rs ! 1, Left), (rs ! 2, Stay)] @ (map (λj. (rs ! (j + 3), Stay)) [0..<k]) @ (map (λj. (rs ! (3 + k + j), Stay)) [0..<k]))" abbreviation "condition7a gs jj ≡ gs ! (3 + jj) = 0 ∧ enc_nth (gs ! 1) (k + jj) = 1 ∧ is_code (gs ! 1) ∧ ¬ is_beginning (gs ! 1)" abbreviation "condition7b gs jj ≡ ¬ condition7a gs jj ∧ gs ! (3 + jj) = 3 ∧ is_code (gs ! 1)" abbreviation "condition7c gs jj ≡ ¬ condition7a gs jj ∧ ¬ condition7b gs jj" lemma turing_command_cmdL7: assumes "jj < k" shows "turing_command (2 * k + 3) 1 G' (cmdL7 jj)" proof show "length ([!!] cmdL7 jj gs) = length gs" if "length gs = 2 * k + 3" for gs proof - consider "condition7a gs jj" | "condition7b gs jj" | "condition7c gs jj" by blast then show ?thesis unfolding cmdL7_def using that by (cases) simp_all qed show goal2: "0 < 2 * k + 3 ⟹ cmdL7 jj gs [.] 0 = gs ! 0" if "length gs = 2 * k + 3" for gs proof - consider "condition7a gs jj" | "condition7b gs jj" | "condition7c gs jj" by blast then show ?thesis unfolding cmdL7_def using that by (cases) simp_all qed show "cmdL7 jj gs [.] j < G'" if gs: "j < length gs" "length gs = 2 * k + 3" "⋀i. i < length gs ⟹ gs ! i < G'" for gs j proof - consider "condition7a gs jj" | "condition7b gs jj" | "condition7c gs jj" by blast then show ?thesis proof (cases) case 1 then have *: "snd (cmdL7 jj gs) = [(gs ! 0, Stay), (enc_upd (gs ! 1) (k + jj) 0, Left), (gs ! 2, Stay)] @ (map (λj. (if j = jj then 3 else gs ! (j + 3), Stay)) [0..<k]) @ (map (λj. (gs ! (3 + k + j), Stay)) [0..<k])" unfolding cmdL7_def by simp consider "j = 0" | "j = 1" | "j = 2" | "3 ≤ j ∧ j < k + 3" | "k + 3 ≤ j ∧ j < 2 * k + 3" using gs by linarith then show ?thesis proof (cases) case 1 then show ?thesis using that by (simp add: goal2) next case 2 then have "is_code (gs ! 1)" using 1 by blast moreover have "k + jj < 2 * k + 2" using assms by simp moreover have "0 < G" using G_ge_4 by simp ultimately have "is_code (enc_upd (gs ! 1) (k + jj) 0)" using enc_upd_is_code by simp then have "is_code (cmdL7 jj gs [.] j)" using * 2 by simp then show ?thesis using G'_ge_G G'_def by simp next case 3 then show ?thesis using * gs by simp next case 4 then show ?thesis using * gs G'_ge threeplus2k_2[where ?a="(gs ! 0, Stay)"] by simp next case 5 then show ?thesis using * gs G'_ge threeplus2k_3[where ?a="(gs ! 0, Stay)"] by simp qed next case case2: 2 then have *: "snd (cmdL7 jj gs) = [(gs ! 0, Stay), (enc_upd (gs ! 1) (k + jj) 1, Left), (gs ! 2, Stay)] @ (map (λj. (if j = jj then 0 else gs ! (j + 3), Stay)) [0..<k]) @ (map (λj. (gs ! (3 + k + j), Stay)) [0..<k])" unfolding cmdL7_def by simp consider "j = 0" | "j = 1" | "j = 2" | "3 ≤ j ∧ j < k + 3" | "k + 3 ≤ j ∧ j < 2 * k + 3" using gs by linarith then show ?thesis proof (cases) case 1 then show ?thesis using that by (simp add: goal2) next case 2 then have "is_code (gs ! 1)" using case2 by simp moreover have "k + jj < 2 * k + 2" using assms by simp moreover have "1 < G" using G_ge_4 by simp ultimately have "is_code (enc_upd (gs ! 1) (k + jj) 1)" using enc_upd_is_code by simp then have "is_code (cmdL7 jj gs [.] j)" using * 2 by simp then show ?thesis using G'_ge_G G'_def by simp next case 3 then show ?thesis using * gs by simp next case 4 then show ?thesis using * gs G'_ge threeplus2k_2[where ?a="(gs ! 0, Stay)"] by simp next case 5 then show ?thesis using * gs G'_ge threeplus2k_3[where ?a="(gs ! 0, Stay)"] by simp qed next case case3: 3 then have *: "snd (cmdL7 jj gs) = [(gs ! 0, Stay), (gs ! 1, Left), (gs ! 2, Stay)] @ (map (λj. (gs ! (j + 3), Stay)) [0..<k]) @ (map (λj. (gs ! (3 + k + j), Stay)) [0..<k])" unfolding cmdL7_def by auto consider "j = 0" | "j = 1" | "j = 2" | "3 ≤ j ∧ j < k + 3" | "k + 3 ≤ j ∧ j < 2 * k + 3" using gs by linarith then show ?thesis using * gs G'_ge threeplus2k_2[where ?a="(gs ! 0, Stay)"] threeplus2k_3[where ?a="(gs ! 0, Stay)"] by (cases) simp_all qed qed show "⋀gs. length gs = 2 * k + 3 ⟹ [*] (cmdL7 jj gs) ≤ 1" using cmdL7_def by simp qed definition tmL67 :: "nat ⇒ machine" where "tmL67 jj ≡ [cmdL7 jj]" lemma tmL67_tm: assumes "jj < k" shows "turing_machine (2 * k + 3) G' (tmL67 jj)" using assms G'_ge tmL67_def turing_command_cmdL7 by auto definition "tmL47 jj ≡ tmL46 jj ;; tmL67 jj" lemma tmL47_tm: assumes "jj < k" shows "turing_machine (2 * k + 3) G' (tmL47 jj)" using assms G'_ge tm_left_tm tmL46_tm tmL47_def tmL67_tm by simp text ‹ Next we are sweeping right again and perform the head movement for tape $jj$ if this is a movement to the right. This works the same as the left movements in @{const cmdL7}. › definition cmdL8 :: "nat ⇒ command" where "cmdL8 jj rs ≡ (if rs ! 1 = □ then 1 else 0, if rs ! (3 + jj) = 2 ∧ enc_nth (rs ! 1) (k + jj) = 1 ∧ is_code (rs ! 1) then [(rs ! 0, Stay), (enc_upd (rs ! 1) (k + jj) 0, Right), (rs ! 2, Stay)] @ (map (λj. (if j = jj then 3 else rs ! (j + 3), Stay)) [0..<k]) @ (map (λj. (rs ! (3 + k + j), Stay)) [0..<k]) else if rs ! (3 + jj) = 3 ∧ is_code (rs ! 1) then [(rs ! 0, Stay), (enc_upd (rs ! 1) (k + jj) 1, Right), (rs ! 2, Stay)] @ (map (λj. (if j = jj then 2 else rs ! (j + 3), Stay)) [0..<k]) @ (map (λj. (rs ! (3 + k + j), Stay)) [0..<k]) else if rs ! 1 = 0 then [(rs ! 0, Stay), (rs ! 1, Stay), (rs ! 2, Stay)] @ (map (λj. (rs ! (j + 3), Stay)) [0..<k]) @ (map (λj. (rs ! (3 + k + j), Stay)) [0..<k]) else [(rs ! 0, Stay), (rs ! 1, Right), (rs ! 2, Stay)] @ (map (λj. (rs ! (j + 3), Stay)) [0..<k]) @ (map (λj. (rs ! (3 + k + j), Stay)) [0..<k]))" abbreviation "condition8a gs jj ≡ gs ! (3 + jj) = 2 ∧ enc_nth (gs ! 1) (k + jj) = 1 ∧ is_code (gs ! 1)" abbreviation "condition8b gs jj ≡ ¬ condition8a gs jj ∧ gs ! (3 + jj) = 3 ∧ is_code (gs ! 1)" abbreviation "condition8c gs jj ≡ ¬ condition8a gs jj ∧ ¬ condition8b gs jj ∧ gs ! 1 = 0" abbreviation "condition8d gs jj ≡ ¬ condition8a gs jj ∧ ¬ condition8b gs jj ∧ ¬ condition8c gs jj" lemma turing_command_cmdL8: assumes "jj < k" shows "turing_command (2 * k + 3) 1 G' (cmdL8 jj)" proof show "length ([!!] cmdL8 jj gs) = length gs" if "length gs = 2 * k + 3" for gs proof - consider "condition8a gs jj" | "condition8b gs jj" | "condition8c gs jj" | "condition8d gs jj" by blast then show ?thesis unfolding cmdL8_def using that by (cases) simp_all qed show goal2: "0 < 2 * k + 3 ⟹ cmdL8 jj gs [.] 0 = gs ! 0" if "length gs = 2 * k + 3" for gs proof - consider "condition8a gs jj" | "condition8b gs jj" | "condition8c gs jj" | "condition8d gs jj" by blast then show ?thesis unfolding cmdL8_def using that by (cases) simp_all qed show "cmdL8 jj gs [.] j < G'" if gs: "j < length gs" "length gs = 2 * k + 3" "⋀i. i < length gs ⟹ gs ! i < G'" for gs j proof - consider "condition8a gs jj" | "condition8b gs jj" | "condition8c gs jj" | "condition8d gs jj" by blast then show ?thesis proof (cases) case 1 then have *: "snd (cmdL8 jj gs) = [(gs ! 0, Stay), (enc_upd (gs ! 1) (k + jj) 0, Right), (gs ! 2, Stay)] @ (map (λj. (if j = jj then 3 else gs ! (j + 3), Stay)) [0..<k]) @ (map (λj. (gs ! (3 + k + j), Stay)) [0..<k])" unfolding cmdL8_def by simp consider "j = 0" | "j = 1" | "j = 2" | "3 ≤ j ∧ j < k + 3" | "k + 3 ≤ j ∧ j < 2 * k + 3" using gs by linarith then show ?thesis proof (cases) case 1 then show ?thesis using that by (simp add: goal2) next case 2 then have "is_code (gs ! 1)" using 1 by blast moreover have "k + jj < 2 * k + 2" using assms by simp moreover have "0 < G" using G_ge_4 by simp ultimately have "is_code (enc_upd (gs ! 1) (k + jj) 0)" using enc_upd_is_code by simp then have "is_code (cmdL8 jj gs [.] j)" using * 2 by simp then show ?thesis using G'_ge_G G'_def by simp next case 3 then show ?thesis using * gs by simp next case 4 then show ?thesis using * gs G'_ge threeplus2k_2[where ?a="(gs ! 0, Stay)"] by simp next case 5 then show ?thesis using * gs G'_ge threeplus2k_3[where ?a="(gs ! 0, Stay)"] by simp qed next case case2: 2 then have *: "snd (cmdL8 jj gs) = [(gs ! 0, Stay), (enc_upd (gs ! 1) (k + jj) 1, Right), (gs ! 2, Stay)] @ (map (λj. (if j = jj then 2 else gs ! (j + 3), Stay)) [0..<k]) @ (map (λj. (gs ! (3 + k + j), Stay)) [0..<k])" unfolding cmdL8_def by simp consider "j = 0" | "j = 1" | "j = 2" | "3 ≤ j ∧ j < k + 3" | "k + 3 ≤ j ∧ j < 2 * k + 3" using gs by linarith then show ?thesis proof (cases) case 1 then show ?thesis using that by (simp add: goal2) next case 2 then have "is_code (gs ! 1)" using case2 by simp moreover have "k + jj < 2 * k + 2" using assms by simp moreover have "1 < G" using G_ge_4 by simp ultimately have "is_code (enc_upd (gs ! 1) (k + jj) 1)" using enc_upd_is_code by simp then have "is_code (cmdL8 jj gs [.] j)" using * 2 by simp then show ?thesis using G'_ge_G G'_def by simp next case 3 then show ?thesis using * gs by simp next case 4 then show ?thesis using * gs G'_ge threeplus2k_2[where ?a="(gs ! 0, Stay)"] by simp next case 5 then show ?thesis using * gs G'_ge threeplus2k_3[where ?a="(gs ! 0, Stay)"] by simp qed next case 3 then have *: "snd (cmdL8 jj gs) = [(gs ! 0, Stay), (gs ! 1, Stay), (gs ! 2, Stay)] @ (map (λj. (gs ! (j + 3), Stay)) [0..<k]) @ (map (λj. (gs ! (3 + k + j), Stay)) [0..<k])" unfolding cmdL8_def by auto consider "j = 0" | "j = 1" | "j = 2" | "3 ≤ j ∧ j < k + 3" | "k + 3 ≤ j ∧ j < 2 * k + 3" using gs by linarith then show ?thesis using * gs G'_ge threeplus2k_2[where ?a="(gs ! 0, Stay)"] threeplus2k_3[where ?a="(gs ! 0, Stay)"] by (cases) simp_all next case 4 then have *: "snd (cmdL8 jj gs) = [(gs ! 0, Stay), (gs ! 1, Right), (gs ! 2, Stay)] @ (map (λj. (gs ! (j + 3), Stay)) [0..<k]) @ (map (λj. (gs ! (3 + k + j), Stay)) [0..<k])" unfolding cmdL8_def by auto consider "j = 0" | "j = 1" | "j = 2" | "3 ≤ j ∧ j < k + 3" | "k + 3 ≤ j ∧ j < 2 * k + 3" using gs by linarith then show ?thesis using * gs G'_ge threeplus2k_2[where ?a="(gs ! 0, Stay)"] threeplus2k_3[where ?a="(gs ! 0, Stay)"] by (cases) simp_all qed qed show "⋀gs. length gs = 2 * k + 3 ⟹ [*] (cmdL8 jj gs) ≤ 1" using cmdL8_def by simp qed definition tmL78 :: "nat ⇒ machine" where "tmL78 jj ≡ [cmdL8 jj]" lemma tmL78_tm: assumes "jj < k" shows "turing_machine (2 * k + 3) G' (tmL78 jj)" using assms G'_ge tmL78_def turing_command_cmdL8 by auto definition "tmL48 jj ≡ tmL47 jj ;; tmL78 jj" lemma tmL48_tm: assumes "jj < k" shows "turing_machine (2 * k + 3) G' (tmL48 jj)" using assms G'_ge tm_left_tm tmL47_tm tmL48_def tmL78_tm by simp text ‹ The last command in the command sequence is moving back to the beginning of the output tape. › definition "tmL49 jj ≡ tmL48 jj ;; tm_left_until1" text ‹ The Turing machine @{term "tmL49 jj"} is then repeated for the parameters $jj = 0, \dots, k - 1$ in order to simulate the actions of $M$ on all tapes. › lemma tmL49_tm: "jj < k ⟹ turing_machine (2 * k + 3) G' (tmL49 jj)" using tmL48_tm tmL49_def tmL1_def tm_left_until1_tm by simp fun tmL49_upt :: "nat ⇒ machine" where "tmL49_upt 0 = []" | "tmL49_upt (Suc j) = tmL49_upt j ;; tmL49 j" lemma tmL49_upt_tm: assumes "j ≤ k" shows "turing_machine (2 * k + 3) G' (tmL49_upt j)" using assms proof (induction j) case 0 then show ?case using G'_ge(1) turing_machine_def by simp next case (Suc j) then