section ‹Memorizing in states\label{s:tm-memorizing}› theory Memorizing imports Elementary begin text ‹ Some Turing machines are best described by allowing them to memorize values in their states. For example, a TM that adds two binary numbers could memorize the carry bit in states. In the textbook definition of TMs, with arbitrary state space, this can be represented by a state space of the form $Q \times \{0, 1\}$, where 0 and 1 represent the memorized values. In our simplified definition of TMs, where the state space is an interval of natural numbers, this does not work. However, there is a workaround. Since we can have arbitrarily many tapes, we can make the TM store this value on an additional tape. Such a memorization tape could be used to write/read a symbol representing the memorized value. The tape head would never move on such a tape. The behavior of the TM can then depend on the memorized value. By adding several such tapes we can even have more than one value stored simultaneously as well. However, this method increases the number of tapes, and one part of the proof of the Cook-Levin theorem is showing that every TM can be simulated on a two-tape TM (see Chapter~\ref{s:oblivious-two-tape}). How to remove such memorization tapes again without changing the behavior of the TM is the subject of this section. The straightforward idea is to multiply the states by the number of possible values. So if the original TM has $Q$ non-halting states and memorizes $G$ different values, the new TM has $Q\cdot G$ non-halting states. It would be natural to map a pair $(q, g)$ of state and memorized value to $q \cdot G + g$ or to $g \cdot Q + q$. However, there is a small technical problem. The memorization tape is initialized, like all tapes in a start configuration, with the head on the leftmost cell, which contains the start symbol. Thus the initially memorized value is the number~1 representing~$\triangleright$. The new TM must start in the start state, which we have fixed at~0. Thus the state-value pair $(0, 1)$ must be mapped to~0, which neither of the two natural mappings does. Our workaround is to use the mapping $(q, g) \mapsto ((g - 1) \bmod G) \cdot Q + q$. The following function maps a Turing machine $M$ that memorizes one value from $\{0,\dots,G-1\}$ on its last tape to a TM that has one tape less, has $G$ times the number of non-halting states, and behaves just like $M$. The name ``cartesian'' for this function is just a funny term I made up. › definition cartesian :: "machine ⇒ nat ⇒ machine" where "cartesian M G ≡ concat (map (λh. map (λq rs. let (q', as) = (M ! q) (rs @ [(h + 1) mod G]) in (if q' = length M then G * length M else (fst (last as) + G - 1) mod G * length M + q', butlast as)) [0..<length M]) [0..<G])" lemma length_concat_const: assumes "⋀h. length (f h) = c" shows "length (concat (map f [0..<G])) = G * c" using assms by (induction G; simp) lemma length_cartesian: "length (cartesian M G) = G * length M" using cartesian_def by (simp add: length_concat_const) lemma concat_nth: assumes "⋀h. length (f h) = c" and "xs = concat (map f [0..<G])" and "h < G" and "q < c" shows "xs ! (h * c + q) = f h ! q" using assms(2,3) proof (induction G arbitrary: xs) case 0 then show ?case by simp next case (Suc G) then have 1: "xs = concat (map f [0..<G]) @ f G" (is "xs = ?ys @ f G") by simp show ?case proof (cases "h < G") case True then have "h * c ≤ (G - 1) * c" by auto then have "h * c ≤ G * c - c" using True by (simp add: diff_mult_distrib) then have "h * c + q ≤ G * c - c + q" using assms(4) by simp then have "h * c + q < G * c" using assms(4) True ‹h * c ≤ (G - 1) * c› mult_eq_if by force then have "h * c + q < length ?ys" using length_concat_const assms by metis then have "xs ! (h * c + q) = ?ys ! (h * c + q)" using 1 by (simp add: nth_append) then show ?thesis using Suc True by simp next case False then show ?thesis using "1" Suc.prems(2) assms(1) by (metis add_diff_cancel_left' length_concat_const less_SucE not_add_less1 nth_append) qed qed lemma cartesian_at: assumes "M' = cartesian M b" and "h < b" and "q < length M" shows "(M' ! (h * length M + q)) rs = (let (q', as) = (M ! q) (rs @ [(h + 1) mod b]) in (if q' = length M then b * length M else (fst (last as) + b - 1) mod b * length M + q', butlast as))" proof - define f where "f = (λh. map (λq. λrs. let (q', as) = (M ! q) (rs @ [(h + 1) mod b]) in (if q' = length M then b * length M else (fst (last as) + b - 1) mod b * length M + q', butlast as)) [0..<length M])" then have "length (f h) = length M" for h by simp moreover have "M' = concat (map f [0..<b])" using assms(1) cartesian_def f_def by simp ultimately have "M' ! (h * length M + q) = f h ! q" using concat_nth assms(2,3) by blast then show ?thesis using f_def by (simp add: assms(3)) qed lemma concat_nth_ex: assumes "⋀h. length (f h) = c" and "xs = concat (map f [0..<G])" and "j < G * c" shows "∃i h. i < c ∧ h < G ∧ xs ! j = f h ! i" using assms(2,3) proof (induction G arbitrary: xs) case 0 then show ?case by simp next case (Suc G) then have *: "xs = concat (map f [0..<G]) @ f G" (is "xs = ?ys @ f G") by simp show ?case proof (cases "j < G * c") case True then have "∃i h. i < c ∧ h < G ∧ ?ys ! j = f h ! i" using Suc by simp then have "∃i h. i < c ∧ h < Suc G ∧ ?ys ! j = f h ! i" using less_SucI by blast then have "∃i h. i < c ∧ h < Suc G ∧ xs ! j = f h ! i" using True * by (simp add: assms(1) length_concat_const nth_append) then show ?thesis . next case False then have "j ≥ G * c" by simp define h where "h = G" then have h: "h < Suc G" by simp define i where "i = j - G * c" then have i: "i < c" using False Suc.prems(2) by auto have "xs ! j = f h ! i" using assms by (simp add: "*" False h_def i_def length_concat_const nth_append) then show ?thesis using h i by auto qed qed text ‹ The cartesian TM has one tape less than the original TM. › lemma cartesian_num_tapes: assumes "turing_machine (Suc k) G M" and "M' = cartesian M b" and "length rs = k" and "q' < length M'" shows "length (snd ((M' ! q') rs)) = k" proof - define q where "q = q' mod length M" define h where "h = q' div length M" then have "h < b" "q' = h * length M + q" using q_def assms(2) assms(4) length_cartesian less_mult_imp_div_less by auto then have "q < length M" using q_def assms(2,4) length_cartesian by (metis add_lessD1 length_0_conv length_greater_0_conv mod_less_divisor mult_0_right) have "(M' ! q') rs = (let (q', as) = (M ! q) (rs @ [(h + 1) mod b]) in (if q' = length M then b * length M else (fst (last as) + b - 1) mod b * length M + q', butlast as))" using cartesian_at[OF assms(2) `h < b` `q < length M`] `q' = h * length M + q` by simp then have "snd ((M' ! q') rs) = (let (q', as) = (M ! q) (rs @ [(h + 1) mod b]) in butlast as)" by (metis (no_types, lifting) case_prod_unfold snd_conv) then have *: "snd ((M' ! q') rs) = butlast (snd ((M ! q) (rs @ [(h + 1) mod b])))" by (simp add: case_prod_unfold) have "length (rs @ [(h + 1) mod b]) = Suc k" using assms(3) by simp then have "length (snd ((M ! q) (rs @ [(h + 1) mod b]))) = Suc k" using assms(1) ‹q < length M› turing_commandD(1) turing_machine_def nth_mem by metis then show ?thesis using * by simp qed text ‹ The cartesian TM of a TM with alphabet $G$ also has the alphabet $G$ provided it memorizes at most $G$ values. › lemma cartesian_tm: assumes "turing_machine (Suc k) G M" and "M' = cartesian M b" and "k ≥ 2" and "b ≤ G" and "b > 0" shows "turing_machine k G M'" proof show "G ≥ 4" using assms(1) turing_machine_def by simp show "2 ≤ k" using assms(3) . define f where "f = (λh. map (λi rs. let (q, as) = (M ! i) (rs @ [(h + 1) mod b]) in (if q = length M then b * length M else (fst (last as) + b - 1) mod b * length M + q, butlast as)) [0..<length M])" then have 1: "⋀h. length (f h) = length M" by simp have 2: "M' = concat (map f [0..<b])" using f_def assms(2) cartesian_def by simp show "turing_command k (length M') G (M' ! j)" if "j < length M'" for j proof have 3: "j < b * length M" using that by (simp add: assms(2) length_cartesian) with 1 2 concat_nth_ex have "∃i h. i < length M ∧ h < b ∧ M' ! j = f h ! i" by blast then obtain i h where i: "i < length M" and h: "h < b" and cmd: "M' ! j = (λrs. let (q, as) = (M ! i) (rs @ [(h + 1) mod b]) in (if q = length M then b * length M else (fst (last as) + b - 1) mod b * length M + q, butlast as))" using f_def by auto have "(h + 1) mod b < b" using h by auto then have modb: "(h + 1) mod b < G" using assms(4) by linarith have tc: "turing_command (Suc k) (length M) G (M ! i)" using i assms(1) turing_machine_def by simp show goal1: "⋀gs. length gs = k ⟹ length ([!!] (M' ! j) gs) = length gs" proof - fix gs :: "symbol list" assume a: "length gs = k" let ?q = "fst ((M ! i) (gs @ [(h + 1) mod b]))" let ?as = "snd ((M ! i) (gs @ [(h + 1) mod b]))" have "(M' ! j) gs = (if ?q = length M then b * length M else (fst (last ?as) + b - 1) mod b * length M + ?q, butlast ?as)" using cmd by (metis (no_types, lifting) case_prod_unfold) then have "[!!] (M' ! j) gs = butlast ?as" by simp moreover have "length ?as = Suc k" using a turing_commandD(1)[OF tc] by simp ultimately show "length ([!!] (M' ! j) gs) = length gs" by (simp add: a) qed show "(M' ! j) gs [.] ja < G" if "length gs = k" and "(⋀i. i < length gs ⟹ gs ! i < G)" and "ja < length gs" for gs ja proof - let ?q = "fst ((M ! i) (gs @ [(h + 1) mod b]))" let ?as = "snd ((M ! i) (gs @ [(h + 1) mod b]))" have *: "(M' ! j) gs = (if ?q = length M then b * length M else (fst (last ?as) + b - 1) mod b * length M + ?q, butlast ?as)" using cmd by (metis (no_types, lifting) case_prod_unfold) have "length (gs @ [(h + 1) mod b]) = Suc k" using that by simp moreover have "(gs @ [(h + 1) mod b]) ! i < G" if "i < length (gs @ [(h + 1) mod b])" for i using that by (metis ‹⋀i. i < length gs ⟹ gs ! i < G› modb length_append_singleton less_Suc_eq nth_append nth_append_length) ultimately have "(∀j<length (gs @ [(h + 1) mod b]). (M ! i) (gs @ [(h + 1) mod b]) [.] j < G)" using that turing_commandD(2)[OF tc] by simp moreover have "butlast ?as ! ja = ?as ! ja" by (metis * goal1 nth_butlast snd_conv that(1) that(3)) ultimately show ?thesis using "*" that(3) by auto qed show "(M' ! j) gs [.] 0 = gs ! 0" if "length gs = k" and "0 < k" for gs proof - let ?q = "fst ((M ! i) (gs @ [(h + 1) mod b]))" let ?as = "snd ((M ! i) (gs @ [(h + 1) mod b]))" have *: "(M' ! j) gs = (if ?q = length M then b * length M else (fst (last ?as) + b - 1) mod b * length M + ?q, butlast ?as)" using cmd by (metis (no_types, lifting) case_prod_unfold) have "length (gs @ [(h + 1) mod b]) = Suc k" using that by simp then have "(M ! i) (gs @ [(h + 1) mod b]) [.] 0 = gs ! 0" using that turing_commandD(3)[OF tc] by (simp add: nth_append) then show ?thesis using that * by (metis goal1 nth_butlast snd_conv) qed show "[*] ((M' ! j) gs) ≤ length M'" if "length gs = k" for gs proof - let ?q = "[*] ((M ! i) (gs @ [(h + 1) mod b]))" let ?as = "snd ((M ! i) (gs @ [(h + 1) mod b]))" have *: "(M' ! j) gs = (if ?q = length M then b * length M else (fst (last ?as) + b - 1) mod b * length M + ?q, butlast ?as)" using cmd by (metis (no_types, lifting) case_prod_unfold) have "length (gs @ [h]) = Suc k" using that by simp then have "?q ≤ length M" using assms(1) i turing_commandD(4)[OF tc] by (metis length_append_singleton) show ?thesis proof (cases "?q = length M") case True then show ?thesis using * by (simp add: assms(2) length_cartesian) next case False then have "?q < length M" using `?q ≤ length M` by simp then have **: "[*] ((M' ! j) gs) = (fst (last ?as) + b - 1) mod b * length M + ?q" using * by simp have "(fst (last ?as) + b - 1) mod b ≤ b - 1" using h less_imp_Suc_add by fastforce have "(fst (last ?as) + b - 1) mod b * length M ≤ b * length M - length M" using h less_imp_Suc_add by fastforce then have "(fst (last ?as) + b - 1) mod b * length M + ?q ≤ b * length M - length M + ?q" by simp then have "(fst (last ?as) + b - 1) mod b * length M + ?q < b * length M" using `?q < length M` 3 assms(5) by auto then show ?thesis using length_cartesian ** assms(2) by simp qed qed qed qed text ‹ A special case of the previous lemma is $b = G$: › corollary cartesian_tm': assumes "turing_machine (Suc k) G M" and "M' = cartesian M G" and "k ≥ 2" shows "turing_machine k G M'" using assms cartesian_tm by (metis gr0I not_numeral_le_zero order_refl turing_machine_def) text ‹ A cartesian TM assumes essentially the same configurations the original machine does, except that it has one tape less and the states have a greater number. We call these configurations ``squished'', another fancy made-up term alluding to the removal of one tape. \null › definition squish :: "nat ⇒ nat ⇒ config ⇒ config" where "squish G Q cfg ≡ let (q, tps) = cfg in (if q ≥ Q then G * Q else ( |.| (last tps) + G - 1) mod G * Q + q, butlast tps)" lemma squish: "squish G Q cfg = (if fst cfg ≥ Q then G * Q else ( |.| (last (snd cfg)) + G - 1) mod G * Q + fst cfg, butlast (snd cfg))" using squish_def by (simp add: case_prod_beta) lemma squish_head_pos: assumes "||cfg|| > 2" shows "squish G Q cfg <#> 0 = cfg <#> 0" and "squish G Q cfg <#> 1 = cfg <#> 1" using assms squish by (metis One_nat_def Suc_1 Suc_lessD length_butlast less_diff_conv nth_butlast plus_1_eq_Suc snd_conv, metis One_nat_def Suc_1 length_butlast less_diff_conv nth_butlast plus_1_eq_Suc snd_conv) lemma mod_less: fixes q Q h G :: nat assumes "q < Q" and "0 < G" shows "h mod G * Q + q < G * Q" proof - have "h mod G ≤ G - 1" using assms(2) less_Suc_eq_le by fastforce then have "h mod G * Q ≤ (G - 1) * Q" by simp then have "h mod G * Q ≤ G * Q - Q" by (simp add: left_diff_distrib') then have "h mod G * Q + q ≤ G * Q - Q + q" by simp then have "h mod G * Q + q ≤ G * Q - 1" using assms by simp then show ?thesis by (metis One_nat_def Suc_pred add.left_neutral add.right_neutral add_mono_thms_linordered_semiring(1) assms le_simps(2) linorder_not_less mult_pos_pos zero_le) qed lemma squish_halt_state: assumes "G > 0" and "fst cfg ≤ Q" shows "fst (squish G Q cfg) = G * Q ⟷ fst cfg = Q" proof show "fst cfg = Q ⟹ fst (squish G Q cfg) = G * Q" by (simp add: squish) show "fst (squish G Q cfg) = G * Q ⟹ fst cfg = Q" proof (rule ccontr) assume a: "fst (squish G Q cfg) = G * Q" assume "fst cfg ≠ Q" then have "fst cfg < Q" using assms(2) by simp then have "fst (squish G Q cfg) = ( |.| (last (snd cfg)) + G - 1) mod G * Q + fst cfg" using squish by simp also have "... < G * Q" using mod_less[OF `fst cfg < Q` assms(1)] by simp finally have "fst (squish G Q cfg) < G * Q" . with a show False by simp qed qed lemma butlast_replicate: "butlast (replicate k x) = replicate (k - Suc 0) x" by (intro nth_equalityI) (simp_all add: nth_butlast) lemma squish_start_config: "G ≥ 4 ⟹ k ≥ 2 ⟹ squish G Q (start_config (Suc k) zs) = start_config k zs" using squish_def start_config_def by (simp add: butlast_replicate) text ‹ The cartesian Turing machine only works properly if the original TM never moves its head on the last tape. We call a tape of a TM $M$ \emph{immobile} if $M$ never moves the head on the tape. › definition immobile :: "machine ⇒ nat ⇒ nat ⇒ bool" where "immobile M j k ≡ ∀q rs. q < length M ⟶ length rs = k ⟶ (M ! q) rs [~] j = Stay" lemma immobileI [intro]: assumes "⋀q rs. q < length M ⟹ length rs = k ⟹ (M ! q) rs [~] j = Stay" shows "immobile M j k" using immobile_def assms by simp text ‹ If the head never moves on tape $k$, the head will stay in position $0$. › lemma immobile_head_pos_proper: assumes "proper_machine (Suc k) M" and "immobile M k (Suc k)" and "||cfg|| = Suc k" shows "execute M cfg t <#> k = cfg <#> k" proof (induction t) case 0 then show ?case by simp next case (Suc t) have "execute M cfg (Suc t) = exe M (execute M cfg t)" (is "_ = exe M ?cfg") by simp show ?case proof (cases "fst ?cfg ≥ length M") case True then have "exe M ?cfg = ?cfg" using exe_ge_length by simp then show ?thesis by (simp add: Suc.IH) next case False let ?cmd = "M ! (fst ?cfg)" let ?rs = "config_read ?cfg" have "exe M ?cfg = sem ?cmd ?cfg" using False exe_def by simp moreover have "proper_command (Suc k) (M ! (fst ?cfg))" using assms(1) False by simp ultimately have "exe M ?cfg <!> k = act (snd (?cmd ?rs) ! k) (?cfg <!> k)" using assms execute_num_tapes_proper lessI sem_snd by presburger then show ?thesis using False Suc act assms execute_num_tapes_proper immobile_def read_length by simp qed qed lemma immobile_head_pos: assumes "turing_machine (Suc k) G M" and "immobile M k (Suc k)" and "||cfg|| = Suc k" shows "execute M cfg t <#> k = cfg <#> k" proof (induction t) case 0 then show ?case by simp next case (Suc t) have "execute M cfg (Suc t) = exe M (execute M cfg t)" (is "_ = exe M ?cfg") by simp show ?case proof (cases "fst ?cfg ≥ length M") case True then have "exe M ?cfg = ?cfg" using exe_ge_length by simp then show ?thesis by (simp add: Suc.IH) next case False let ?cmd = "M ! (fst ?cfg)" let ?rs = "config_read ?cfg" have "exe M ?cfg = sem ?cmd ?cfg" using False exe_def by simp moreover have "proper_command (Suc k) (M ! (fst ?cfg))" using assms(1) False by (metis turing_commandD(1) linorder_not_le turing_machineD(3)) ultimately have "exe M ?cfg <!> k = act (snd (?cmd ?rs) ! k) (?cfg <!> k)" using assms execute_num_tapes lessI sem_snd by presburger then show ?thesis using False Suc act assms execute_num_tapes immobile_def read_length by simp qed qed text ‹ Sequentially combining two Turing machines with an immobile tape yields a Turing machine with the same immobile tape. › lemma immobile_sequential: assumes "turing_machine k G M1" and "turing_machine k G M2" and "immobile M1 j k" and "immobile M2 j k" shows "immobile (M1 ;; M2) j k" proof let ?M = "M1 ;; M2" fix q :: nat and rs :: "symbol list" assume q: "q < length ?M" and rs: "length rs = k" show "(?M ! q) rs [~] j = Stay" proof (cases "q < length M1") case True then have "?M ! q = M1 ! q" by (simp add: nth_append turing_machine_sequential_def) then show ?thesis using assms(3) immobile_def by (simp add: True rs) next case False then have "?M ! q = relocate_cmd (length M1) (M2 ! (q - length M1))" using q turing_machine_sequential_nth' by simp then show ?thesis using relocate_cmd_head False assms(4) q rs length_turing_machine_sequential immobile_def by simp qed qed text ‹ A loop also keeps a tape immobile. › lemma immobile_loop: assumes "turing_machine k G M1" and "turing_machine k G M2" and "immobile M1 j k" and "immobile M2 j k" and "j < k" shows "immobile (WHILE M1 ; cond DO M2 DONE) j k" proof let ?loop = "WHILE M1 ; cond DO M2 DONE" have "?loop = M1 @ [cmd_jump cond (length M1 + 1) (length M1 + length M2 + 2)] @ (relocate (length M1 + 1) M2) @ [cmd_jump (λ_. True) 0 0]" (is "_ = M1 @ [?a] @ ?bs @ [?c]") using turing_machine_loop_def by simp then have loop: "?loop = (M1 @ [?a]) @ (?bs @ [?c])" by simp fix q :: nat assume q: "q < length ?loop" fix rs :: "symbol list" assume rs: "length rs = k" consider "q < length M1" | "q = length M1" | "length M1 < q ∧ q ≤ length M1 + length M2" | "length M1 + length M2 < q" by linarith then show "(?loop ! q) rs [~] j = Stay" proof (cases) case 1 then have "?loop ! q = M1 ! q" by (simp add: nth_append turing_machine_loop_def) then show ?thesis using assms(3) 1 rs immobile_def by simp next case 2 then have "?loop ! q = cmd_jump cond (length M1 + 1) (length M1 + length M2 + 2)" by (simp add: nth_append turing_machine_loop_def) then show ?thesis using rs cmd_jump_def assms(5) by simp next case 3 then have "?loop ! q = (?bs @ [?c]) ! (q - (length M1 + 1))" using nth_append[of "M1 @ [?a]" "?bs @ [?c]"] loop by simp moreover have "q - (length M1 + 1) < length ?bs" using 3 length_relocate by auto ultimately have "?loop ! q = ?bs ! (q - (length M1 + 1))" by (simp add: nth_append) then show ?thesis using assms(4,5) relocate_cmd_head 3 relocate rs immobile_def by auto next case 4 then have "q = length M1 + length M2 + 1" using q turing_machine_loop_len by simp then have "?loop ! q = ?c" using turing_machine_loop_def by (metis (no_types, lifting) One_nat_def Suc_eq_plus1 append_assoc length_append list.size(3) list.size(4) nth_append_length plus_nat.simps(2) length_relocate) then show ?thesis using rs cmd_jump_def assms(5) by simp qed qed text ‹ An immobile tape stays immobile when further tapes are appended. We only need this for the special case of two-tape Turing machines. › lemma immobile_append_tapes: assumes "j < k" and "j > 1" and "k ≥ 2" and "turing_machine 2 G M" shows "immobile (append_tapes 2 k M) j k" proof let ?M = "append_tapes 2 k M" fix q :: nat assume q: "q < length ?M" fix rs :: "symbol list" assume rs: "length rs = k" have "q < length M" using assms q by (metis length_append_tapes) show "(?M ! q) rs [~] j = Stay" proof - have "(?M ! q) rs = (fst ((M ! q) (take 2 rs)), snd ((M ! q) (take 2 rs)) @ (map (λj. (rs ! j, Stay)) [2..<k]))" using append_tapes_nth by (simp add: append_tapes_nth ‹q < length M› rs) then have "(?M ! q) rs [~] j = snd ((snd ((M ! q) (take 2 rs)) @ (map (λj. (rs ! j, Stay)) [2..<k])) ! j)" using assms by simp also have "... = snd ((map (λj. (rs ! j, Stay)) [2..<k]) ! (j - 2))" proof - have "length (take 2 rs) = 2" using rs assms(3) by simp then have "length ([!!] (M ! q) (take 2 rs)) = 2" using assms rs by (metis turing_commandD(1) ‹q < length M› nth_mem turing_machine_def) then show ?thesis using nth_append[of "snd ((M ! q) (take 2 rs))" "map (λj. (rs ! j, Stay)) [2..<k]" j] assms by simp qed finally show ?thesis using assms(1,2) by simp qed qed text ‹ For the elementary Turing machines we introduced in Section~\ref{s:tm-elementary} all tapes are immobile but the ones given as parameters. › lemma immobile_tm_trans_until: assumes "j ≠ j1" and "j ≠ j2" and "j < k" shows "immobile (tm_trans_until j1 j2 H f) j k" using assms tm_trans_until_def cmd_trans_until_def by auto lemma immobile_tm_ltrans_until: assumes "j ≠ j1" and "j ≠ j2" and "j < k" shows "immobile (tm_ltrans_until j1 j2 H f) j k" using assms tm_ltrans_until_def cmd_ltrans_until_def by auto lemma immobile_tm_left_until: assumes "j ≠ j'" and "j < k" shows "immobile (tm_left_until H j') j k" using assms tm_left_until_def cmd_left_until_def by auto lemma immobile_tm_start: assumes "j ≠ j'" and "j < k" shows "immobile (tm_start j') j k" using tm_start_def immobile_tm_left_until[OF assms] by metis lemma immobile_tm_write: assumes "j < k" shows "immobile (tm_write j' h) j k" using assms tm_write_def cmd_write_def by auto lemma immobile_tm_write_many: assumes "j < k" shows "immobile (tm_write_many J h) j k" using assms tm_write_many_def cmd_write_many_def by auto lemma immobile_tm_right: assumes "j ≠ j'" and "j < k" shows "immobile (tm_right j') j k" using assms tm_right_def cmd_right_def by auto lemma immobile_tm_rtrans: assumes "j ≠ j'" and "j < k" shows "immobile (tm_rtrans j' f) j k" using assms tm_rtrans_def cmd_rtrans_def by auto lemma immobile_tm_left: assumes "j ≠ j'" and "j < k" shows "immobile (tm_left j') j k" using assms tm_left_def cmd_left_def by auto lemma mod_inc_dec: "(h::nat) < G ⟹ ((h + G - 1) mod G + 1) mod G = h" using mod_Suc_eq by auto lemma last_length: "length xs = Suc k ⟹ last xs = xs ! k" by (metis diff_Suc_1 last_conv_nth length_0_conv nat.simps(3)) text ‹ The tapes used for memorizing the values have blank symbols in every cell but possibly for the leftmost cell. In keeping with funny names, we call such tapes @{term onesie} tapes. › definition onesie :: "symbol ⇒ tape" ("⌈_⌉") where "⌈h⌉ ≡ (λx. if x = 0 then h else □, 0)" lemma onesie_1: "⌈▹⌉ = (⌊[]⌋, 0)" unfolding onesie_def contents_def by auto lemma onesie_read [simp]: "|.| ⌈h⌉ = h" using onesie_def by simp lemma onesie_write: "⌈x⌉ |:=| y = ⌈y⌉" using onesie_def by auto lemma act_onesie: "act (h, Stay) ⌈x⌉ = ⌈h⌉" using onesie_def by auto text ‹ We now consider the semantics of cartesian Turing machines. Roughly speaking, a cartesian TM assumes the squished configurations of the original TM. A crucial assumption here is that the original TM only ever memorizes a symbol from a certain range of symbols, with one relaxation: when switching to the halting state, any symbol may be written to the memorization tape. The reason is that there is only one halting state even for the cartesian TM, and thus the halting state is not subject to the mapping of states implemented by the @{const cartesian} operation. In the following lemma, @{text "⌈▹⌉"} is the memorization tape. It has the start symbol because in the start configuration all tapes have the start symbol in the leftmost cell. › lemma cartesian_execute: assumes "turing_machine (Suc k) G M" and "immobile M k (Suc k)" and "k ≥ 2" and "b > 0" and "length tps = k" and "⋀t. execute M (0, tps @ [⌈▹⌉]) t <.> k < b ∨ fst (execute M (0, tps @ [⌈▹⌉]) t) = length M" shows "execute (cartesian M b) (0, tps) t = squish b (length M) (execute M (0, tps @ [⌈▹⌉]) t)" proof (induction t) case 0 then show ?case using squish by simp next case (Suc t) let ?M' = "cartesian M b" have len: "length ?M' = b * length M" using length_cartesian by simp let ?cfg = "execute M (0, tps @ [⌈▹⌉]) t" have 1: "?cfg <#> k = 0" using assms(1,2,5) immobile_head_pos onesie_def by auto have 3: "||?cfg|| = Suc k" using assms(1,5) execute_num_tapes by auto let ?Q = "length M" let ?squish = "squish b ?Q" let ?scfg = "?squish ?cfg" obtain q tps where qtps: "?cfg = (q, tps)" by fastforce have "length tps = Suc k" using 3 qtps by simp then have last: "last tps = tps ! k" using assms(4) by (metis diff_Suc_1 last_conv_nth length_greater_0_conv zero_less_Suc) have "exe ?M' ?scfg = ?squish (exe M ?cfg)" proof (cases "q ≥ length M") case True then have t1: "exe M ?cfg = ?cfg" using exe_def qtps by auto have "?scfg = (b * length M, butlast tps)" using True squish qtps by simp then have "exe ?M' ?scfg = ?scfg" using exe_def len by simp with t1 show ?thesis by simp next case False then have scfg: "?scfg = (( |.| (last tps) + b - 1) mod b * length M + q, butlast tps)" (is "_ = (?q, _)") using squish qtps by simp moreover have q_less: "?q < length ?M'" using mod_less False length_cartesian assms(4) by simp ultimately have 9: "exe ?M' ?scfg = sem (?M' ! ?q) ?scfg" using exe_def by simp let ?cmd' = "?M' ! ?q" let ?h = "( |.| (last tps) + b - 1) mod b" have "q < length M" using False by simp then have 4: "|.| (last tps) < b" using assms last qtps False by (metis fst_conv less_not_refl3 snd_conv) have h_less: "?h < b" using 4 by simp then have "?cmd' ≡ λrs. (let (q', as) = (M ! q) (rs @ [(?h + 1) mod b]) in (if q' = length M then b * length M else (fst (last as) + b - 1) mod b * length M + q', butlast as))" using cartesian_at[OF _ h_less `q < length M`] by presburger then have cmd': "?cmd' ≡ λrs. (let (q', as) = (M ! q) (rs @ [ |.| (last tps)]) in (if q' = length M then b * length M else (fst (last as) + b - 1) mod b * length M + q', butlast as))" using mod_inc_dec[OF 4] by simp let ?rs' = "config_read ?scfg" have 10: "sem ?cmd' ?scfg = (let (newstate, as) = ?cmd' ?rs' in (newstate, map (λ(a, tp). act a tp) (zip as (butlast tps))))" using scfg by (simp add: sem_def) let ?newstate' = "fst (?cmd' ?rs')" let ?as' = "snd (?cmd' ?rs')" have 11: "sem ?cmd' ?scfg = (?newstate', map (λ(a, tp). act a tp) (zip ?as' (butlast tps)))" using 10 by (simp add: case_prod_beta) with 9 have lhs: "exe ?M' ?scfg = (?newstate', map (λ(a, tp). act a tp) (zip ?as' (butlast tps)))" by simp let ?cmd = "M ! q" let ?rs = "config_read ?cfg" let ?newstate = "fst (?cmd ?rs)" let ?as = "snd (?cmd ?rs)" have "?squish (exe M ?cfg) = ?squish (sem ?cmd ?cfg)" using qtps False exe_def by simp also have "... = ?squish (?newstate, map (λ(a, tp). act a tp) (zip ?as (snd ?cfg)))" by (metis sem) also have "... = ?squish (?newstate, map (λ(a, tp). act a tp) (zip ?as tps))" (is "_ = ?squish (_, ?tpsSuc)") using qtps by simp also have "... = (if ?newstate ≥ ?Q then b * ?Q else ( |.| (last ?tpsSuc) + b - 1) mod b * ?Q + ?newstate, butlast ?tpsSuc)" using squish by simp finally have rhs: "?squish (exe M ?cfg) = (if ?newstate ≥ ?Q then b * ?Q else ( |.| (last ?tpsSuc) + b - 1) mod b * ?Q + ?newstate, butlast ?tpsSuc)" . have "read (butlast tps) @ [ |.| (last tps)] = read tps" using `length tps = Suc k` read_def by (metis (no_types, lifting) last_map length_0_conv map_butlast map_is_Nil_conv old.nat.distinct(1) snoc_eq_iff_butlast) then have rs'_read: "?rs' @ [ |.| (last tps)] = read tps" using scfg by simp have fst: "fst (?cmd' ?rs') = (if ?newstate ≥ ?Q then b * ?Q else ( |.| (last ?tpsSuc) + b - 1) mod b * ?Q + ?newstate)" proof - have "fst (?cmd' ?rs') ≡ fst ( (let (q', as) = (M ! q) (?rs' @ [ |.| (last tps)]) in (if q' = length M then b * length M else (fst (last as) + b - 1) mod b * length M + q', butlast as)))" using cmd' by simp then have "fst (?cmd' ?rs') = (if fst ((M ! q) (?rs' @ [ |.| (last tps)])) = length M then b * length M else (fst (last (snd ((M ! q) (?rs' @ [ |.| (last tps)])))) + b - 1) mod b * length M + fst ((M ! q) (?rs' @ [ |.| (last tps)])))" by (auto simp add: Let_def split_beta) then have lhs: "fst (?cmd' ?rs') = (if fst ((M ! q) (read tps)) = length M then b * ?Q else (fst (last (snd ((M ! q) (read tps)))) + b - 1) mod b * ?Q + fst ((M ! q) (read tps)))" using rs'_read by simp have *: "|.| (last (map (λ(a, tp). act a tp) (zip ?as tps))) = fst (last (snd ((M ! q) (read tps))))" proof - have "length ?as = Suc k" using "3" ‹q < length M› assms(1) read_length turing_machine_def by (metis turing_commandD(1) nth_mem) then have "length (map (λ(a, tp). act a tp) (zip ?as tps)) = Suc k" using `length tps = Suc k` by simp then have "last (map (λ(a, tp). act a tp) (zip ?as tps)) = (map (λ(a, tp). act a tp) (zip ?as tps)) ! k" using last_length by blast moreover have "proper_command (Suc k) ?cmd" using ‹q < length M› assms(1) turing_machine_def turing_commandD(1) nth_mem by blast ultimately have 1: "last (map (λ(a, tp). act a tp) (zip ?as tps)) = act (?as ! k) (tps ! k)" using "3" ‹q < length M› assms(1) qtps sem' sem_snd_tm by auto have "snd (?as ! k) = Stay" using assms(2) `length tps = Suc k` "3" ‹q < length M› read_length immobile_def by simp then have "act (?as ! k) (tps ! k) = (tps ! k) |:=| (fst (?as ! k))" by (metis act_Stay' prod.collapse) then have "|.| (act (?as ! k) (tps ! k)) = fst (?as ! k)" by simp with 1 have 2: "|.| (last (map (λ(a, tp). act a tp) (zip ?as tps))) = fst (?as ! k)" by simp have "fst (last (snd ((M ! q) (read tps)))) = fst (last ?as)" using qtps by simp then have "fst (last (snd ((M ! q) (read tps)))) = fst (?as ! k)" using `length ?as = Suc k` by (simp add: last_length) with 2 show ?thesis by simp qed have "(if fst ((M ! q) ?rs) ≥ ?Q then b * ?Q else ( |.| (last ?tpsSuc) + b - 1) mod b * ?Q + fst ((M ! q) ?rs)) = (if fst ((M ! q) (read tps)) ≥ ?Q then b * ?Q else ( |.| (last ?tpsSuc) + b - 1) mod b * ?Q + fst ((M ! q) (read tps)))" using qtps by simp also have "... = (if fst ((M ! q) (read tps)) = ?Q then b * ?Q else ( |.| (last ?tpsSuc) + b - 1) mod b * ?Q + fst ((M ! q) (read tps)))" using assms(1) turing_machine_def by (metis (mono_tags, lifting) "3" turing_commandD(4) ‹q < length M› le_antisym nth_mem prod.sel(2) qtps read_length) also have "... = (if fst ((M ! q) (read tps)) = length M then b * ?Q else (fst (last (snd ((M ! q) (read tps)))) + b - 1) mod b * ?Q + fst ((M ! q) (read tps)))" using * by simp finally show ?thesis using lhs by simp qed have snd: "map (λ(a, tp). act a tp) (zip ?as' (butlast tps)) = butlast (map (λ(a, tp). act a tp) (zip ?as tps))" proof (rule nth_equalityI) let ?lhs = "map (λ(a, tp). act a tp) (zip ?as' (butlast tps))" let ?rhs = "butlast (map (λ(a, tp). act a tp) (zip ?as tps))" have "||?scfg|| = k" using ‹length tps = Suc k› scfg by simp then have "length ?rs' = k" by (simp add: read_length) then have "length ?as' = k" using cartesian_num_tapes q_less assms(1,3) by simp moreover have "length (butlast tps) = k" using `length tps = Suc k` by simp ultimately have "length ?lhs = k" by simp have "length ?as = Suc k" using ‹length tps = Suc k› ‹q < length M› assms(1) qtps read_length turing_machine_def by (metis "3" turing_commandD(1) nth_mem) then have "length ?rhs = k" using `length tps = Suc k` by simp then show "length ?lhs = length ?rhs" using `length ?lhs = k` by simp show "?lhs ! j = ?rhs ! j" if "j < length ?lhs" for j proof - have "j < k" using that `length ?lhs = k` by auto have "length (butlast tps) = k" using ‹length (butlast tps) = k› by blast then have lhs: "?lhs ! j = act (?as' ! j) (tps ! j)" using `j < k` `length ?as' = k` by (simp add: nth_butlast) have rhs: "?rhs ! j = act (?as ! j) (tps ! j)" using `j < k` `length ?as = Suc k` `length tps = Suc k` by (simp add: nth_butlast) have "?as' ! j = snd ( (let (q', as) = (M ! q) (?rs' @ [ |.| (last tps)]) in (if q' = length M then b * length M else (fst (last as) + b - 1) mod b * length M + q', butlast as))) ! j" using cmd' by simp also have "... = snd ( ((if fst ((M ! q) (?rs' @ [ |.| (last tps)])) = length M then b * length M else (fst (last (snd ((M ! q) (?rs' @ [ |.| (last tps)])))) + b - 1) mod b * length M + fst ((M ! q) (?rs' @ [ |.| (last tps)])), butlast (snd ((M ! q) (?rs' @ [ |.| (last tps)])))))) ! j" by (metis (no_types, lifting) case_prod_unfold) also have "... = butlast (snd ((M ! q) (?rs' @ [ |.| (last tps)]))) ! j" by simp finally have "?as' ! j = butlast (snd ((M ! q) (?rs' @ [ |.| (last tps)]))) ! j" . then have as'_j: "?as' ! j = butlast (snd ((M ! q) (read tps))) ! j" using rs'_read by simp have "?as ! j = snd ((M ! q) (read tps)) ! j" using qtps by simp moreover have "?as ! j = (butlast ?as) ! j" using `length ?as = Suc k` `j < k` by (simp add: nth_butlast) ultimately have "?as ! j = butlast (snd ((M ! q) (read tps))) ! j" using qtps by simp then have "?as ! j = ?as' ! j" using as'_j by simp then show ?thesis using lhs rhs by simp qed qed then show ?thesis using fst lhs rhs by simp qed then show ?case by (simp add: Suc.IH) qed text ‹ One assumption of the previous lemma is that the memorization tape can only contain a symbol from a certain range (except in the halting state). One way to achieve this is for the Turing machine to only ever write a symbol from that range to the memorization tape (or switch to the halting state). Formally: › definition bounded_write :: "machine ⇒ nat ⇒ nat ⇒ bool" where "bounded_write M k b ≡ ∀q rs. q < length M ⟶ length rs = Suc k ⟶ (M ! q) rs [.] k < b ∨ fst ((M ! q) rs) = length M" text ‹ The advantage of @{const bounded_write} is that it is a relatively easy to prove property of a Turing machine. With @{const bounded_write} the previous lemma, @{thm [source] cartesian_execute}, turns into the following one, where the assumption $b > 0$ becomes $b > 1$ because initially the memorization tape has the start symbol, represented by the number~1. \null › lemma cartesian_execute_onesie: assumes "turing_machine (Suc k) G M" and "immobile M k (Suc k)" and "k ≥ 2" and "b > 1" and "length tps = k" and "bounded_write M k b" shows "execute (cartesian M b) (0, tps) t = squish b (length M) (execute M (0, tps @ [⌈▹⌉]) t)" proof - have "execute M (0, tps @ [⌈▹⌉]) t <.> k < b ∨ fst (execute M (0, tps @ [⌈▹⌉]) t) = length M" for t proof (induction t) case 0 then show ?case using assms by auto next case (Suc t) let ?tps = "tps @ [⌈▹⌉]" have *: "execute M (0, ?tps) (Suc t) = exe M (execute M (0, ?tps) t)" (is "_ = exe M ?cfg") by simp show ?case proof (cases "fst ?cfg ≥ length M") case True then show ?thesis using * Suc exe_ge_length by presburger next case False let ?rs = "config_read ?cfg" let ?q = "fst ?cfg" let ?tps = "snd ?cfg" have len: "length ?tps = Suc k" using assms(1,5) execute_num_tapes by simp have pos: "?tps :#: k = 0" using assms immobile_head_pos onesie_def by auto have lenrs: "length ?rs = Suc k" using len read_length by simp have **: "exe M ?cfg = sem (M ! ?q) ?cfg" using False exe_lt_length by simp have ***: "sem (M ! ?q) ?cfg <!> k = act ((M ! ?q) ?rs [!] k) (?tps ! k)" proof - have "proper_command (Suc k) (M ! ?q)" by (metis False turing_commandD(1) assms(1) le_less_linear nth_mem turing_machine_def) then show ?thesis using len sem_snd by blast qed have "(M ! ?q) ?rs [~] k = Stay" using assms(2) lenrs False immobile_def by simp then have act: "act ((M ! ?q) ?rs [!] k) (?tps ! k) = (?tps ! k) |:=| ((M ! ?q) ?rs [.] k)" using act_Stay' by (metis prod.collapse) show ?thesis proof (cases "(M ! ?q) ?rs [.] k < b") case True then have "sem (M ! ?q) ?cfg <.> k < b" using pos *** act by simp then show ?thesis using * ** by simp next case halt: False then have "fst ((M ! ?q) ?rs) = length M" using assms(6) bounded_write_def lenrs False le_less_linear by blast then show ?thesis using * ** sem_fst by simp qed qed qed then show ?thesis using cartesian_execute[OF assms(1-3) _ assms(5)] assms(4) by simp qed text ‹ In the following lemma, the term @{term "⌈c⌉"} reflects the fact that in the halting state the memorized symbol can be anything. › lemma cartesian_transforms_onesie: assumes "turing_machine (Suc k) G M" and "immobile M k (Suc k)" and "k ≥ 2" and "b > 1" and "bounded_write M k b" and "length tps = k" and "transforms M (tps @ [⌈▹⌉]) t (tps' @ [⌈c⌉])" shows "transforms (cartesian M b) tps t tps'" proof - have "execute M (0, tps @ [⌈▹⌉]) t = (length M, tps' @ [⌈c⌉])" using transforms_def transits_def by (metis (no_types, lifting) assms(7) execute_after_halting_ge fst_conv) then have "execute (cartesian M b) (0, tps) t = squish b (length M) (length M, tps' @ [⌈c⌉])" using assms cartesian_execute_onesie by simp moreover from this have "fst (execute (cartesian M b) (0, tps) t) = b * length M" using squish_halt_state[of b _ "length M"] One_nat_def assms(4) by simp ultimately have "execute (cartesian M b) (0, tps) t = (b * length M, tps')" using squish by simp then show ?thesis using transforms_def transits_def length_cartesian by auto qed text ‹ A Turing machine with alphabet $G$, when started on a symbol sequence over $G$, is guaranteed to only write symbols from $G$ to any of its tapes, including any memorization tapes. Therefore the last assumption of lemma~@{thm [source] cartesian_execute} is satisfied. So in the case of the start configuration we do not need any extra assumptions such as @{const bounded_write}. This is formalized in the next lemma. The downside is that it can only be applied to ``finished'' TMs but not to reusable TMs, because these do not usually start in the start state. › lemma cartesian_execute_start_config: assumes "turing_machine (Suc k) G M" and "immobile M k (Suc k)" and "k ≥ 2" and "∀i<length zs. zs ! i < G" shows "execute (cartesian M G) (start_config k zs) t = squish G (length M) (execute M (start_config (Suc k) zs) t)" proof - let ?tps = "snd (start_config k zs)" have "snd (start_config (Suc k) zs) = (λi. if i = 0 then 1 else if i ≤ length zs then zs ! (i - 1) else 0, 0) # replicate k (λi. if i = 0 then 1 else 0, 0)" using start_config_def by auto also have "... = (λi. if i = 0 then 1 else if i ≤ length zs then zs ! (i - 1) else 0, 0) # replicate (k - 1) (λi. if i = 0 then 1 else 0, 0) @ [(λi. if i = 0 then 1 else 0, 0)]" using assms(3) by (metis (no_types, lifting) One_nat_def Suc_1 Suc_le_D Suc_pred less_Suc_eq_0_disj replicate_Suc replicate_append_same) also have "... = snd (start_config k zs) @ [(λi. if i = 0 then 1 else 0, 0)]" using start_config_def by auto finally have "snd (start_config (Suc k) zs) = snd (start_config k zs) @ [⌈▹⌉]" using onesie_def by auto then have *: "start_config (Suc k) zs = (0, ?tps @ [⌈▹⌉])" using start_config_def by simp then have "execute M (0, ?tps @ [⌈▹⌉]) t <.> k < G" for t using assms(1,4) by (metis lessI tape_alphabet) moreover have "G ≥ 2" using assms(1) turing_machine_def by simp moreover have "length ?tps = k" using start_config_length assms(3) by simp ultimately have "execute (cartesian M G) (0, ?tps) t = squish G (length M) (execute M (0, ?tps @ [⌈▹⌉]) t)" using cartesian_execute[OF assms(1-3)] by simp moreover have "start_config k zs = (0, ?tps)" using start_config_def by simp ultimately show ?thesis using * by simp qed text ‹ So far we have only considered single memorization tapes. But of course we can have more than one by iterating the @{const cartesian} function. Applying this functions once removes the final memorization tape, but leaves others intact, that is, it maintains immobile tapes: › lemma cartesian_immobile: assumes "turing_machine (Suc k) G M" and "j < k" and "immobile M j (Suc k)" and "M' = cartesian M G" shows "immobile M' j k" proof standard+ fix q :: nat and rs :: "symbol list" assume q: "q < length M'" and rs: "length rs = k" have "q < G * length M" using assms(1,4) q length_cartesian by simp then have "G > 0" using gr0I by fastforce have "length M > 0" using ‹q < G * length M› by auto define h where "h = q div length M" moreover define i where "i = q mod length M" then have "i < length M" using ‹0 < length M› mod_less_divisor by simp have "h < G" using i_def h_def ‹q < G * length M› less_mult_imp_div_less by blast have "q = h * length M + i" using h_def i_def by simp then have "M' ! q = (λrs. (let (q', as) = (M ! i) (rs @ [(h + 1) mod G]) in (if q' = length M then G * length M else (fst (last as) + G - 1) mod G * length M + q', butlast as)))" using assms(1,4) `h < G` `i < length M` cartesian_at by auto then have "(M' ! q) rs = (let (q', as) = (M ! i) (rs @ [(h + 1) mod G]) in (if q' = length M then G * length M else (fst (last as) + G - 1) mod G * length M + q', butlast as))" for rs by simp then have "(M' ! q) rs = (let qas = (M ! i) (rs @ [(h + 1) mod G]) in (if fst qas = length M then G * length M else (fst (last (snd qas)) + G - 1) mod G * length M + fst qas, butlast (snd qas)))" for rs by (metis (no_types, lifting) old.prod.case prod.collapse) then have "(M' ! q) rs = (if (fst ((M ! i) (rs @ [(h + 1) mod G]))) = length M then G * length M else (fst (last (snd ((M ! i) (rs @ [(h + 1) mod G])))) + G - 1) mod G * length M + fst ((M ! i) (rs @ [(h + 1) mod G])), butlast (snd ((M ! i) (rs @ [(h + 1) mod G]))))" for rs by metis then have 1: "snd ((M' ! q) rs) = butlast (snd ((M ! i) (rs @ [(h + 1) mod G])))" for rs by simp have len: "length (rs @ [(h + 1) mod G]) = Suc k" by (simp add: rs) then have 2: "(M ! i) (rs @ [(h + 1) mod G]) [~] j = Stay" using immobile_def assms(3) len ‹i < length M› by blast have "length (snd ((M ! i) (rs @ [(h + 1) mod G]))) = Suc k" using len assms(1) turing_machine_def by (metis turing_commandD(1) ‹i < length M› turing_machineD(3)) then have "butlast (snd ((M ! i) (rs @ [(h + 1) mod G]))) ! j = snd ((M ! i) (rs @ [(h + 1) mod G])) ! j" using assms(2) by (simp add: nth_butlast) then have "snd ((M' ! q) rs) ! j = snd ((M ! i) (rs @ [(h + 1) mod G])) ! j" using 1 by simp then show "(M' ! q) rs [~] j = Stay" using 2 by simp qed text ‹ With the next function, @{term icartesian}, we can strip several memorization tapes off. › fun icartesian :: "nat ⇒ machine ⇒ nat ⇒ machine" where "icartesian 0 M G = M" | "icartesian (Suc k) M G = icartesian k (cartesian M G) G" text ‹ Applying @{const icartesian} maintains the property of being a Turing machine. We show that only for the special case that all tapes but the input and output tapes are memorization tapes. In this case, we end up with a two-tape machine. › lemma icartesian_tm: assumes "turing_machine (k + 2) G M" and "⋀j. j < k ⟹ immobile M (j + 2) (k + 2)" shows "turing_machine 2 G (icartesian k M G)" using assms(1,2) proof (induction k arbitrary: M) case 0 then show ?case by (metis add.left_neutral icartesian.simps(1)) next case (Suc k) let ?M = "cartesian M G" have "turing_machine (Suc (k + 2)) G M" using Suc by simp moreover have "k + 2 ≥ 2" by simp ultimately have "turing_machine (k + 2) G ?M" using ‹turing_machine (Suc (k + 2)) G M› cartesian_tm' by blast moreover have "⋀j. j < k ⟹ immobile ?M (j + 2) (k + 2)" using cartesian_immobile Suc by simp ultimately have "turing_machine 2 G (icartesian k ?M G)" using Suc by simp then show "turing_machine 2 G (icartesian (Suc k) M G)" by simp qed text ‹ At this point we ought to prove something about the semantics of @{const icartesian}. However, we will only need one specific result, which we can only express at the end of Section~\ref{s:oblivious-tm} after we have introduced oblivious Turing machines. › end