section ‹Combining Turing machines\label{s:tm-combining}› theory Combinations imports Basics "HOL-Eisbach.Eisbach" begin text ‹ This section describes how we can combine Turing machines in the way of traditional control structures found in structured programming, namely sequences, branching, and iterating. This allows us to build complex Turing machines from simpler ones and analyze their behavior and running time. Thanks to some syntactic sugar the result may even look like a programming language, but it is really more like a ``construction kit'' than a ``true'' programming language with small and big step semantics or Hoare rules. Instead we will merely have some lemmas for proving @{const transforms} statements for the combined machines. The remaining sections of this chapter will provide us with concrete Turing machines to combine. › subsection ‹Relocated machines› text ‹ If we use a Turing machine $M$ as part of another TM and there are $q$ commands before $M$, then $M$'s target states will be off by $q$. This can be fixed by adding $q$ to all target states of all commands in $M$, an operation we call \emph{relocation}. › definition relocate_cmd :: "nat ⇒ command ⇒ command" where "relocate_cmd q cmd rs ≡ (fst (cmd rs) + q, snd (cmd rs))" lemma relocate_cmd_head: "relocate_cmd q cmd rs [~] j = cmd rs [~] j" using relocate_cmd_def by simp lemma sem_relocate_cmd: "sem (relocate_cmd q cmd) cfg = (sem cmd cfg) <+=> q" proof- let ?cmd' = "relocate_cmd q cmd" let ?rs = "read (snd cfg)" have "?cmd' ?rs = (fst (cmd ?rs) + q, snd (cmd ?rs))" by (simp add: relocate_cmd_def) then show ?thesis using sem by (metis (no_types, lifting) fst_conv snd_conv) qed definition relocate :: "nat ⇒ machine ⇒ machine" where "relocate q M ≡ map (relocate_cmd q) M" lemma relocate: assumes "M' = relocate q M" and "i < length M" shows "(M' ! i) r = (fst ((M ! i) r) + q, snd ((M ! i) r))" using assms relocate_def relocate_cmd_def by simp lemma sem_relocate: assumes "M' = relocate q M" and "i < length M" shows "sem (M' ! i) cfg = sem (M ! i) cfg <+=> q" using assms relocate_def sem_relocate_cmd by simp lemma turing_command_relocate_cmd: assumes "turing_command k Q G cmd" shows "turing_command k (Q + q) G (relocate_cmd q cmd)" using assms relocate_cmd_def turing_commandD by auto lemma turing_command_relocate: assumes "M' = relocate q M" and "turing_machine k G M" and "i < length M" shows "turing_command k (length M + q) G (M' ! i)" proof fix gs :: "symbol list" assume gs: "length gs = k" have tc: "turing_command k (length M) G (M ! i)" using turing_machine_def assms(2,3) by simp show "length ([!!] (M' ! i) gs) = length gs" using gs turing_commandD(1)[OF tc] assms(1,3) relocate by simp show "(M' ! i) gs [.] 0 = gs ! 0" if "k > 0" using gs turing_commandD(3)[OF tc] assms(1,3) relocate that by simp show "[*] ((M' ! i) gs) ≤ length M + q" using gs turing_commandD(4)[OF tc] assms(1,3) relocate by simp show "(⋀i. i < length gs ⟹ gs ! i < G) ⟹ j < length gs ⟹ (M' ! i) gs [.] j < G" for j using gs turing_commandD(2)[OF tc] assms(1,3) relocate by simp qed lemma length_relocate: "length (relocate q M) = length M" by (simp add: relocate_def) lemma relocate_jump_targets: assumes "turing_machine k G M" and "M' = relocate q M" and "i < length M" and "length rs = k" shows "fst ((M' ! i) rs) ≤ length M + q" using turing_machine_def relocate_def assms relocate by (metis turing_commandD(4) diff_add_inverse2 fst_conv le_diff_conv nth_mem) lemma relocate_zero: "relocate 0 M = M" unfolding relocate_def relocate_cmd_def by simp subsection ‹Sequences› text ‹ To execute two Turing machines sequentially we concatenate the two machines, relocating the second one by the length of the first one. In this way the halting state of the first machine becomes the start state of the second machine. › definition turing_machine_sequential :: "machine ⇒ machine ⇒ machine" (infixl ";;" 55) where "M1 ;; M2 ≡ M1 @ (relocate (length M1) M2)" text ‹ If the number of tapes and the alphabet size match, the concatenation of two Turing machines is again a Turing machine. › lemma turing_machine_sequential_turing_machine [intro, simp]: assumes "turing_machine k G M1" and "turing_machine k G M2" shows "turing_machine k G (M1 ;; M2)" (is "turing_machine k G ?M") proof show 1: "k ≥ 2" using assms(1) turing_machine_def by simp show 2: "G ≥ 4" using assms(1) turing_machine_def by simp have len: "length ?M = length M1 + length M2" using relocate_def turing_machine_sequential_def by simp show 3: "turing_command k (length ?M) G (?M ! i)" if "i < length ?M" for i proof (cases "i < length M1") case True then show ?thesis using turing_machineD[OF assms(1)] turing_machine_sequential_def len turing_command_mono by (metis (no_types, lifting) le_add1 nth_append) next case False then have "i - (length M1) < length M2" (is "?i < length M2") using False that len by simp then have "turing_command k (length ?M) G ((relocate (length M1) M2) ! ?i)" using assms(2) turing_command_relocate len by (simp add: add.commute) moreover have "?M ! i = (relocate (length M1) M2) ! ?i" using False by (simp add: nth_append turing_machine_sequential_def) ultimately show ?thesis by simp qed qed lemma turing_machine_sequential_empty: "turing_machine_sequential [] M = M" unfolding turing_machine_sequential_def using relocate_zero by simp lemma turing_machine_sequential_nth: assumes "M = M1 ;; M2" and "p < length M2" shows "M ! (p + length M1) = relocate_cmd (length M1) (M2 ! p)" proof- let ?r = "relocate (length M1) M2" have "M = M1 @ ?r" using assms(1) turing_machine_sequential_def by simp then have "M ! (p + length M1) = ?r ! p" by (simp add: nth_append) then show ?thesis using assms(2) relocate_def by simp qed lemma turing_machine_sequential_nth': assumes "M = M1 ;; M2" and "length M1 ≤ q" and "q < length M" shows "M ! q = relocate_cmd (length M1) (M2 ! (q - length M1))" using assms turing_machine_sequential_nth length_relocate turing_machine_sequential_def by (metis (no_types, lifting) add.assoc diff_add length_append less_add_eq_less) lemma "length_turing_machine_sequential": "length (turing_machine_sequential M1 M2) = length M1 + length M2" using turing_machine_sequential_def relocate_def by simp lemma exe_relocate: "exe (M1 ;; M2) (cfg <+=> length M1) = (exe M2 cfg) <+=> length M1 " using sem_relocate_cmd sem_state_indep exe_def turing_machine_sequential_nth length_turing_machine_sequential by (smt (verit, ccfv_SIG) add.commute diff_add_inverse2 fst_conv le_add2 less_diff_conv2 snd_conv) lemma execute_pre_append: assumes "halts M1 cfg" and "fst cfg = 0" and "t ≤ running_time M1 cfg " shows "execute ((M0 ;; M1) @ M2) (cfg <+=> length M0) t = (execute M1 cfg t) <+=> length M0" using assms(3) proof (induction t) case 0 then show ?case by simp next case (Suc t) let ?l0 = "length M0" let ?M = "(M0 ;; M1) @ M2" let ?cfg_t = "execute ?M (cfg <+=> ?l0) t" let ?cfg1_t = "execute M1 cfg t" let ?cmd1 = "M1 ! (fst ?cfg1_t)" let ?cmd = "?M ! (fst ?cfg_t)" have *: "?cfg1_t <+=> ?l0 = ?cfg_t" using Suc by simp then have "fst (?cfg1_t <+=> ?l0) = fst ?cfg_t" by simp then have 2: "fst ?cfg1_t + ?l0 = fst ?cfg_t" by simp from * have sndeq: "snd ?cfg1_t = snd ?cfg_t" by (metis snd_conv) have "fst (execute M1 cfg t) ≤ length M1" using halts_impl_le_length assms(1) halts_def by blast moreover have "fst ?cfg1_t ≠ length M1" using Suc.prems running_time_def wellorder_Least_lemma(2) by fastforce ultimately have 1: "fst ?cfg1_t < length M1" by simp with 2 have "relocate_cmd ?l0 ?cmd1 = (M0 ;; M1) ! (fst ?cfg1_t + ?l0)" by (metis turing_machine_sequential_nth) then have "relocate_cmd ?l0 ?cmd1 = ?M ! (fst ?cfg1_t + ?l0)" by (simp add: "1" nth_append length_turing_machine_sequential) then have 3: "relocate_cmd ?l0 ?cmd1 = ?cmd" using 2 by simp with 1 have "execute M1 cfg (Suc t) = sem ?cmd1 ?cfg1_t" by (simp add: exe_def) then have "(execute M1 cfg (Suc t)) <+=> ?l0 = (sem ?cmd1 ?cfg1_t) <+=> ?l0" by simp then have "(execute M1 cfg (Suc t)) <+=> ?l0 = (sem (relocate_cmd ?l0 ?cmd1) ?cfg1_t)" using sem_relocate_cmd by simp then have rhs: "(execute M1 cfg (Suc t)) <+=> ?l0 = sem ?cmd ?cfg1_t" using 3 by simp have "execute ?M (cfg <+=> ?l0) (Suc t) = exe ?M ?cfg_t" by simp moreover have "fst ?cfg_t < length ?M" using 1 2 by (simp add: length_turing_machine_sequential) ultimately have lhs: "execute ?M (cfg <+=> ?l0) (Suc t) = sem ?cmd ?cfg_t" by (simp add: exe_lt_length) have "sem ?cmd ?cfg_t = sem ?cmd ?cfg1_t" using sem_state_indep sndeq by fastforce with lhs rhs show ?case by simp qed lemma transits_pre_append': assumes "transforms M1 tps t tps'" shows "transits ((M0 ;; M1) @ M2) (length M0, tps) t (length M0 + length M1, tps')" proof- let ?rt = "running_time M1 (0, tps)" let ?M = "(M0 ;; M1) @ M2" have "?rt ≤ t" using assms transforms_running_time by simp have "fst (execute M1 (0, tps) t) = length M1" using assms(1) execute_after_halting_ge halting_config_def transforms_halting_config transforms_running_time by (metis (no_types, opaque_lifting) fst_conv) then have *: "halts M1 (0, tps)" using halts_def by auto have "transits M1 (0, tps) t (length M1, tps')" using assms(1) transits_def by (simp add: transforms_def) then have "execute M1 (0, tps) ?rt = (length M1, tps')" using assms(1) halting_config_def transforms_halting_config by auto moreover have "execute ?M (length M0, tps) ?rt = (execute M1 (0, tps) ?rt) <+=> length M0" using execute_pre_append * by auto ultimately have "execute ?M (length M0, tps) ?rt = (length M1, tps') <+=> length M0" by simp then have "execute ?M (length M0, tps) ?rt = (length M0 + length M1, tps')" by simp then show ?thesis using ‹?rt ≤ t› transits_def by blast qed corollary transits_prepend: assumes "transforms M1 tps t tps'" shows "transits (M0 ;; M1) (length M0, tps) t (length M0 + length M1, tps')" using transits_pre_append' assms by (metis append_Nil2) corollary transits_append: assumes "transforms M1 tps t tps'" shows "transits (M1 @ M2) (0, tps) t (length M1, tps')" using transits_pre_append' turing_machine_sequential_empty assms by (metis gen_length_def length_code list.size(3)) corollary execute_append: assumes "fst cfg = 0" and "halts M1 cfg" and "t ≤ running_time M1 cfg" shows "execute (M1 @ M2) cfg t = execute M1 cfg t" using assms execute_pre_append turing_machine_sequential_empty by (metis add.right_neutral list.size(3) prod.collapse) lemma execute_sequential: assumes "execute M1 cfg1 t1 = cfg1'" and "fst cfg1 = 0" and "t1 = running_time M1 cfg1" and "execute M2 cfg2 t2 = cfg2'" and "cfg1' = cfg2 <+=> length M1" and "halts M1 cfg1" shows "execute (M1 ;; M2) cfg1 (t1 + t2) = cfg2' <+=> length M1" proof- let ?M = "M1 ;; M2" have 1: "execute ?M cfg1 t1 = cfg1'" using execute_append assms turing_machine_sequential_def by simp then have 2: "execute ?M cfg1 (t1 + t2) = execute ?M cfg1' t2" using execute_additive by simp have "execute M2 cfg2 t2 = cfg2' ⟹ execute ?M cfg1' t2 = cfg2' <+=> length M1" for t2 proof (induction t2 arbitrary: cfg2') case 0 then show ?case using 1 assms(5) by simp next case (Suc t2) let ?cfg = "execute M2 cfg2 t2" have "execute ?M cfg1' (Suc t2) = exe ?M (execute ?M cfg1' t2)" by simp then have "execute ?M cfg1' (Suc t2) = exe ?M (?cfg <+=> length M1)" using Suc by simp moreover have "execute M2 cfg2 (Suc t2) = exe M2 ?cfg" by simp ultimately show ?case using exe_relocate Suc.prems by metis qed then show ?thesis using assms(4) 2 by simp qed text ‹ The semantics and running time of the @{text ";;"} operator: › lemma transforms_turing_machine_sequential: assumes "transforms M1 tps1 t1 tps2" and "transforms M2 tps2 t2 tps3" shows "transforms (M1 ;; M2) tps1 (t1 + t2) tps3" proof- let ?M = "M1 ;; M2" let ?cfg1 = "(0, tps1)" let ?cfg1' = "(length M1, tps2)" let ?t1 = "running_time M1 ?cfg1" let ?cfg2 = "(0, tps2)" let ?cfg2' = "(length M2, tps3)" let ?t2 = "running_time M2 ?cfg2" have "fst (execute M1 ?cfg1 ?t1) = length M1" using assms(1) halting_config_def transforms_halting_config by (metis fst_conv) then have *: "halts M1 ?cfg1" using halts_def by auto have "execute M1 ?cfg1 ?t1 = ?cfg1'" using assms(1) halting_config_def transforms_halting_config by auto moreover have "fst ?cfg1 = 0" by simp moreover have "execute M2 ?cfg2 ?t2 = ?cfg2'" using assms(2) halting_config_def transforms_halting_config by auto moreover have "?cfg1' = ?cfg2 <+=> length M1" by simp ultimately have "execute ?M ?cfg1 (?t1 + ?t2) = ?cfg2' <+=> length M1" using execute_sequential * by blast then have "execute ?M ?cfg1 (?t1 + ?t2) = (length ?M, tps3)" by (simp add: length_turing_machine_sequential) then have "transits ?M ?cfg1 (?t1 + ?t2) (length ?M, tps3)" using transits_def by blast moreover have "?t1 + ?t2 ≤ t1 + t2" using add_le_mono assms(1,2) transforms_running_time by blast ultimately have "transits ?M ?cfg1 (t1 + t2) (length ?M, tps3)" using transits_monotone by simp then show ?thesis using transforms_def by simp qed corollary transforms_tm_sequentialI: assumes "transforms M1 tps1 t1 tps2" and "transforms M2 tps2 t2 tps3" and "t12 = t1 + t2" shows "transforms (M1 ;; M2) tps1 t12 tps3" using assms transforms_turing_machine_sequential by simp subsection ‹Branches› text ‹ A branching Turing machine consists of a condition and two Turing machines, one for each of the branches. The condition can be any predicate over the list of symbols read from the tapes. The branching TM thus needs to perform conditional jumps, for which we will have the following command: › definition cmd_jump :: "(symbol list ⇒ bool) ⇒ state ⇒ state ⇒ command" where "cmd_jump cond q1 q2 rs ≡ (if cond rs then q1 else q2, map (λr. (r, Stay)) rs)" lemma turing_command_jump_1: assumes "q1 ≤ q2" and "k > 0" shows "turing_command k q2 G (cmd_jump cond q1 q2)" using assms cmd_jump_def turing_commandI by simp lemma turing_command_jump_2: assumes "q2 ≤ q1" and "k > 0" shows "turing_command k q1 G (cmd_jump cond q1 q2)" using assms cmd_jump_def turing_commandI by simp lemma sem_jump_snd: "snd (sem (cmd_jump cond q1 q2) cfg) = snd cfg" proof- let ?k = "||cfg||" let ?cmd = "cmd_jump cond q1 q2" let ?cfg' = "sem ?cmd cfg" let ?rs = "read (snd cfg)" have 1: "proper_command ?k ?cmd" using cmd_jump_def by simp then have len: "||?cfg'|| = ||cfg||" using sem_num_tapes_raw by simp have "snd ?cfg' ! i = act (snd (?cmd ?rs) ! i) (snd cfg ! i)" if "i < ||cfg||" for i using sem_snd 1 that by simp moreover have "snd (?cmd ?rs) ! i = (?rs!i, Stay)" if "i < ||cfg||" for i using cmd_jump_def by (simp add: read_length that) ultimately have "snd ?cfg' ! i = act (?rs ! i, Stay) (snd cfg ! i)" if "i < ||cfg||" for i using that by simp then have "snd ?cfg' ! i = snd cfg ! i" if "i < ||cfg||" for i using that act_Stay by simp then show "snd ?cfg' = snd cfg" using len nth_equalityI by force qed lemma sem_jump_fst1: assumes "cond (read (snd cfg))" shows "fst (sem (cmd_jump cond q1 q2) cfg) = q1" using cmd_jump_def sem assms by simp lemma sem_jump_fst2: assumes "¬ cond (read (snd cfg))" shows "fst (sem (cmd_jump cond q1 q2) cfg) = q2" using cmd_jump_def sem assms by simp lemma sem_jump: "sem (cmd_jump cond q1 q2) cfg = (if cond (config_read cfg) then q1 else q2, snd cfg)" using sem_def sem_jump_snd cmd_jump_def by simp lemma transits_jump: "transits [cmd_jump cond q1 q2] (0, tps) 1 (if cond (read tps) then q1 else q2, tps)" using transits_def sem_jump exe_def by auto definition turing_machine_branch :: "(symbol list ⇒ bool) ⇒ machine ⇒ machine ⇒ machine" ("IF _ THEN _ ELSE _ ENDIF" 60) where "IF cond THEN M1 ELSE M2 ENDIF ≡ [cmd_jump cond 1 (length M1 + 2)] @ (relocate 1 M1) @ [cmd_jump (λ_. True) (length M1 + length M2 + 2) 0] @ (relocate (length M1 + 2) M2)" lemma turing_machine_branch_len: "length (IF cond THEN M1 ELSE M2 ENDIF) = length M1 + length M2 + 2" unfolding turing_machine_branch_def by (simp add: relocate_def) text ‹ If the Turing machines for both branches have the same number of tapes and the same alphabet size, the branching machine is a Turing machine, too. › lemma turing_machine_branch_turing_machine: assumes "turing_machine k G M1" and "turing_machine k G M2" shows "turing_machine k G (IF cond THEN M1 ELSE M2 ENDIF)" (is "turing_machine _ _ ?M") proof show "k ≥ 2" using assms(2) turing_machine_def by simp show "G ≥ 4" using assms(2) turing_machine_def by simp let ?C1 = "[cmd_jump cond 1 (length M1 + 2)]" let ?C2 = "relocate 1 M1" let ?C3 = "[cmd_jump (λ_. True) (length M1 + length M2 + 2) 0]" let ?C4 = "relocate (length M1 + 2) M2" have parts: "?M = ?C1 @ ?C2 @ ?C3 @ ?C4" using turing_machine_branch_def by simp have len: "length ?M = length M1 + length M2 + 2" using turing_machine_branch_len by simp have "k > 0" using `k ≥ 2` by simp show "turing_command k (length ?M) G (?M ! i)" if "i < length ?M" for i proof - consider "i < length ?C1" | "length ?C1 ≤ i ∧ i < length (?C1 @ ?C2)" | "length (?C1 @ ?C2) ≤ i ∧ i < length (?C1 @ ?C2 @ ?C3)" | "length (?C1 @ ?C2 @ ?C3) ≤ i ∧ i < length ?M" using `i < length ?M` by linarith then show ?thesis proof (cases) case 1 then have "turing_command k (length M1 + 2) G (?C1 ! i)" using turing_command_jump_1 `k > 0` by simp then have "turing_command k (length ?M) G (?C1 ! i)" using turing_command_mono len by simp then show ?thesis using parts 1 by simp next case 2 then have "i - length ?C1 < length ?C2" by auto then have "turing_command k (length M1 + 1) G (?C2 ! (i - length ?C1))" using turing_command_relocate assms length_relocate by metis then have "turing_command k (length ?M) G (?C2 ! (i - length ?C1))" using turing_command_mono len by simp then have "turing_command k (length ?M) G ((?C1 @ ?C2) ! i)" using 2 by simp then show ?thesis using parts 2 by (metis (no_types, lifting) append.assoc nth_append) next case 3 then have "turing_command k (length ?M) G (?C3 ! (i - length (?C1 @ ?C2)))" using turing_command_jump_2 len `k > 0` by simp then have "turing_command k (length ?M) G ((?C1 @ ?C2 @ ?C3) ! i)" using 3 by (metis (no_types, lifting) append.assoc diff_is_0_eq' less_numeral_extra(3) nth_append zero_less_diff) then show ?thesis using parts 3 by (smt (verit, best) append.assoc nth_append) next case 4 then have "i - length (?C1 @ ?C2 @ ?C3) < length ?C4" by (simp add: len less_diff_conv2 length_relocate) then have "turing_command k (length ?M) G (?C4 ! (i - length (?C1 @ ?C2 @ ?C3)))" using turing_command_relocate assms by (smt (verit, ccfv_SIG) add.assoc add.commute len length_relocate) then show ?thesis using parts 4 by (metis (no_types, lifting) append.assoc le_simps(3) not_less_eq_eq nth_append) qed qed qed text ‹ If the condition is true, the branching TM executes $M_1$ and requires two extra steps: one for evaluating the condition and one for the unconditional jump to the halting state. › lemma transforms_branch_true: assumes "transforms M1 tps t tps'" and "cond (read tps)" shows "transforms (IF cond THEN M1 ELSE M2 ENDIF) tps (t + 2) tps'" (is "transforms ?M _ _ _") proof- let ?C1 = "[cmd_jump cond 1 (length M1 + 2)]" let ?C2 = "relocate 1 M1" let ?C3 = "[cmd_jump (λ_. True) (length M1 + length M2 + 2) 0]" let ?C4 = "relocate (length M1 + 2) M2" let ?C34 = "?C3 @ ?C4" have parts: "?M = ?C1 @ ?C2 @ ?C3 @ ?C4" using turing_machine_branch_def by simp then have "?M = ?C1 @ ?C2 @ ?C34" by simp moreover have "?C1 @ ?C2 = ?C1 ;; M1" using turing_machine_sequential_def by simp ultimately have parts2: "?M = (?C1 ;; M1) @ ?C34" by simp have "execute ?M (0, tps) 1 = exe ?M (0, tps)" by simp also have "... = sem (?M ! 0) (0, tps)" using exe_def by (simp add: turing_machine_branch_len) also have "... = sem (?C1 ! 0) (0, tps)" by (simp add: parts) also have "... = sem (cmd_jump cond 1 (length M1 + 2)) (0, tps)" by simp also have "... = (1, tps)" using sem_jump by (simp add: assms(2)) finally have "execute ?M (0, tps) 1 = (1, tps)" . then have phase1: "transits ?M (0, tps) 1 (1, tps)" using transits_def by auto have "length ?C1 = 1" by simp moreover have "transits ((?C1 ;; M1) @ ?C34) (length ?C1, tps) t (length ?C1 + length M1, tps')" using transits_pre_append' assms by blast ultimately have "transits ?M (1, tps) t (1 + length M1, tps')" using parts2 by simp with phase1 have "transits ?M (0, tps) (t + 1) (1 + length M1, tps')" using transits_additive by fastforce then have phase2: "transits ?M (0, tps) (t + 1) (length (?C1 @ ?C2), tps')" by (simp add: relocate_def) let ?cfg = "(length (?C1 @ ?C2), tps')" have *: "?M ! (length (?C1 @ ?C2)) = ?C3 ! 0" using parts by simp then have "execute ?M ?cfg 1 = exe ?M ?cfg" by simp also have "... = sem (cmd_jump (λ_. True) (length M1 + length M2 + 2) 0) ?cfg" using exe_def relocate_def turing_machine_branch_len * by (simp add: Suc_le_lessD) also have "... = (length M1 + length M2 + 2, snd ?cfg)" using sem_jump by simp also have "... = (length ?M, tps')" by (simp add: turing_machine_branch_len) finally have "execute ?M ?cfg 1 = (length ?M, tps')" . then have "transits ?M ?cfg 1 (length ?M, tps')" using transits_def by auto with phase2 have "transits ?M (0, tps) (t + 2) (length ?M, tps')" using transits_additive by fastforce then show ?thesis by (simp add: transforms_def) qed text ‹ If the condition is false, the branching TM executes $M_2$ and requires one extra step to evaluate the condition. › lemma transforms_branch_false: assumes "transforms M2 tps t tps'" and "¬ cond (read tps)" shows "transforms (IF cond THEN M1 ELSE M2 ENDIF) tps (t + 1) tps'" (is "transforms ?M _ _ _") proof- let ?C1 = "[cmd_jump cond 1 (length M1 + 2)]" let ?C2 = "relocate 1 M1" let ?C3 = "[cmd_jump (λ_. True) (length M1 + length M2 + 2) 0]" let ?C4 = "relocate (length M1 + 2) M2" let ?C123 = "?C1 @ ?C2 @ ?C3" have parts: "?M = ?C1 @ ?C2 @ ?C3 @ ?C4" using turing_machine_branch_def by simp moreover have len123: "length ?C123 = length M1 + 2" by (simp add: length_relocate) ultimately have seq: "?M = ?C123 ;; M2" by (simp add: turing_machine_sequential_def) have "execute ?M (0, tps) 1 = exe ?M (0, tps)" by simp also have "... = sem (?M ! 0) (0, tps)" using exe_def by (simp add: turing_machine_branch_len) also have "... = sem (cmd_jump cond 1 (length M1 + 2)) (0, tps)" by (simp add: parts) also have "... = (length M1 + 2, tps)" using assms(2) sem_jump by simp also have "... = (length ?C123, tps)" using len123 by simp finally have "execute ?M (0, tps) 1 = (length ?C123, tps)" . then have phase1: "transits ?M (0, tps) 1 (length ?C123, tps)" using transits_def by blast have "?M ! (length ?C123) = ?C4 ! 0" by (simp add: nth_append parts length_relocate) have "transits (?C123 ;; M2) (length ?C123, tps) t (length ?C123 + length M2, tps')" using transits_prepend assms by blast then have "transits ?M (length ?C123, tps) t (length ?M, tps')" by (simp add: seq length_turing_machine_sequential) with phase1 have "transits ?M (0, tps) (t + 1) (length ?M, tps')" using transits_additive by fastforce then show ?thesis using transforms_def by simp qed text ‹ The behavior and running time of the branching Turing machine: › lemma transforms_branch_full: assumes "c ⟹ transforms M1 tps tT tpsT" and "¬ c ⟹ transforms M2 tps tF tpsF" and "c ⟹ tT + 2 ≤ t" and "¬ c ⟹ tF + 1 ≤ t" and "c = cond (read tps)" and "tps' = (if c then tpsT else tpsF)" shows "transforms (IF cond THEN M1 ELSE M2 ENDIF) tps t tps'" proof - have "transforms (IF cond THEN M1 ELSE M2 ENDIF) tps (if c then tT + 2 else tF + 1) (if c then tpsT else tpsF)" using assms(1,2,5) transforms_branch_true transforms_branch_false by simp moreover have "(if c then tT + 2 else tF + 1) ≤ t" using assms(3,4) by simp ultimately show ?thesis using transforms_monotone assms(6) by presburger qed corollary transforms_branchI: assumes "cond (read tps) ⟹ transforms M1 tps tT tpsT" and "¬ cond (read tps) ⟹ transforms M2 tps tF tpsF" and "cond (read tps) ⟹ tT + 2 ≤ t" and "¬ cond (read tps) ⟹ tF + 1 ≤ t" and "cond (read tps) ⟹ tps' = tpsT" and "¬ cond (read tps) ⟹ tps' = tpsF" shows "transforms (IF cond THEN M1 ELSE M2 ENDIF) tps t tps'" using transforms_branch_full assms by (smt (z3)) subsection ‹Loops› text ‹ The loops are while loops consisting of a head and a body. The body is a Turing machine that is executed in every iteration as long as the condition in the head of the loop evaluates to true. The condition is of the same form as in branching TMs, namely a predicate over the symbols read from the tapes. Sometimes this is not expressive enough, and so we allow a Turing machine as part of the loop head that is run prior to evaluating the condition. In most cases, however, this TM is empty. › definition turing_machine_loop :: "machine ⇒ (symbol list ⇒ bool) ⇒ machine ⇒ machine" ("WHILE _ ; _ DO _ DONE" 60) where "WHILE M1 ; cond DO M2 DONE ≡ M1 @ [cmd_jump cond (length M1 + 1) (length M1 + length M2 + 2)] @ (relocate (length M1 + 1) M2) @ [cmd_jump (λ_. True) 0 0]" text ‹ Intuitively the Turing machine @{term "WHILE M1 ; cond DO M2 DONE"} first executes @{term M1} and then checks the condition @{term cond}. If it is true, it executes @{term M2} and jumps back to the start state; otherwise it jumps to the halting state. › lemma turing_machine_loop_len: "length (WHILE M1 ; cond DO M2 DONE) = length M1 + length M2 + 2" unfolding turing_machine_loop_def by (simp add: relocate_def) text ‹ If both Turing machines have the same number of tapes and alphabet size, then so does the looping Turing machine. › lemma turing_machine_loop_turing_machine: assumes "turing_machine k G M1" and "turing_machine k G M2" shows "turing_machine k G (WHILE M1 ; cond DO M2 DONE)" (is "turing_machine _ _ ?M") proof show 1: "k ≥ 2" using assms(1) turing_machine_def by simp show 2: "G ≥ 4" using assms(1) turing_machine_def by simp let ?C1 = "M1" let ?C2 = "[cmd_jump cond (length M1 + 1) (length M1 + length M2 + 2)]" let ?C3 = "relocate (length M1 + 1) M2" let ?C4 = "[cmd_jump (λ_. True) 0 0]" let ?C34 = "?C3 @ ?C4" have parts: "?M = ?C1 @ ?C2 @ ?C3 @ ?C4" using turing_machine_loop_def by simp have len: "length ?M = length M1 + length M2 + 2" using turing_machine_loop_len by simp have "k > 0" using `k ≥ 2` by simp show "turing_command k (length ?M) G (?M ! i)" if "i < length ?M" for i proof - consider "i < length ?C1" | "length ?C1 ≤ i ∧ i < length (?C1 @ ?C2)" | "length (?C1 @ ?C2) ≤ i ∧ i < length (?C1 @ ?C2 @ ?C3)" | "length (?C1 @ ?C2 @ ?C3) ≤ i ∧ i < length ?M" using `i < length ?M` by linarith then show ?thesis proof (cases) case 1 then have "turing_command k (length M1) G (?C1 ! i)" using turing_machineD(3) assms by simp then have "turing_command k (length ?M) G (?C1 ! i)" using turing_command_mono len by simp then show ?thesis using parts 1 by (simp add: nth_append) next case 2 then have "turing_command k (length M1 + length M2 + 2) G (?C2 ! (i - length ?C1))" using turing_command_jump_1 `0 < k` by simp then have "turing_command k (length ?M) G (?C2 ! (i - length ?C1))" using len by simp then have "turing_command k (length ?M) G ((?C1 @ ?C2) ! i)" using "2" le_add_diff_inverse by (simp add: nth_append) then show ?thesis using 2 parts by (simp add: nth_append) next case 3 then have "turing_command k (length M2 + (length M1 + 1)) G (?C3 ! (i - length (?C1 @ ?C2)))" using turing_command_relocate length_relocate assms(2) by (smt (verit, best) add.commute add.left_commute add_less_cancel_left le_add_diff_inverse length_append) then have "turing_command k (length ?M) G (?C3 ! (i - length (?C1 @ ?C2)))" using turing_command_mono len by simp then have "turing_command k (length ?M) G ((?C1 @ ?C2 @ ?C3) ! i)" using 3 by (simp add: nth_append) then show ?thesis using parts 3 by (smt (verit) append.assoc nth_append) next case 4 then have "turing_command k 0 G (?C4 ! (i - length (?C1 @ ?C2 @ ?C3)))" using turing_command_jump_1 `0 < k` len length_relocate by simp then have "turing_command k (length ?M) G (?C4 ! (i - length (?C1 @ ?C2 @ ?C3)))" using turing_command_mono by blast then show ?thesis using parts 4 by (metis (no_types, lifting) append.assoc nth_append verit_comp_simplify1(3)) qed qed qed lemma transits_turing_machine_loop_cond_false: assumes "transforms M1 tps t1 tps'" and "¬ cond (read tps')" shows "transits (WHILE M1 ; cond DO M2 DONE) (0, tps) (t1 + 1) (length M1 + length M2 + 2, tps')" (is "transits ?M _ _ _") proof- let ?C1 = "M1" let ?C2 = "[cmd_jump cond (length M1 + 1) (length M1 + length M2 + 2)]" let ?C3 = "relocate (length M1 + 1) M2" let ?C4 = "[cmd_jump (λ_. True) 0 0]" let ?C34 = "?C3 @ ?C4" have parts: "?M = ?C1 @ ?C2 @ ?C3 @ ?C4" using turing_machine_loop_def by simp then have "?M = ?C1 @ (?C2 @ ?C3 @ ?C4)" by simp then have "transits ?M (0, tps) t1 (length ?C1, tps')" using assms transits_append by simp moreover have "transits ?M (length M1, tps') 1 (length M1 + length M2 + 2, tps')" proof- have *: "?M ! (length ?C1) = cmd_jump cond (length M1 + 1) (length M1 + length M2 + 2)" using turing_machine_loop_def by simp have "execute ?M (length ?C1, tps') 1 = exe ?M (length ?C1, tps')" by simp also have "... = sem (?M ! (length ?C1)) (length ?C1, tps')" by (simp add: exe_lt_length turing_machine_loop_len) also have "... = sem (cmd_jump cond (length M1 + 1) (length M1 + length M2 + 2)) (length ?C1, tps')" using * by simp also have "... = (length M1 + length M2 + 2, tps')" using sem_jump assms(2) by simp finally have "execute ?M (length ?C1, tps') 1 = (length M1 + length M2 + 2, tps')" . then show ?thesis using transits_def by auto qed ultimately show "transits ?M (0, tps) (t1 + 1) (length M1 + length M2 + 2, tps')" using transits_additive by blast qed lemma transits_turing_machine_loop_cond_true: assumes "transforms M1 tps t1 tps'" and "transforms M2 tps' t2 tps''" and "cond (read tps')" shows "transits (WHILE M1 ; cond DO M2 DONE) (0, tps) (t1 + t2 + 2) (0, tps'')" (is "transits ?M _ _ _") proof- let ?C1 = "M1" let ?C2 = "[cmd_jump cond (length M1 + 1) (length M1 + length M2 + 2)]" let ?C3 = "relocate (length M1 + 1) M2" let ?C4 = "[cmd_jump (λ_. True) 0 0]" let ?C34 = "?C3 @ ?C4" have parts: "?M = ?C1 @ ?C2 @ ?C3 @ ?C4" using turing_machine_loop_def by simp then have "?M = ?C1 @ (?C2 @ ?C3 @ ?C4)" by simp then have "transits ?M (0, tps) t1 (length ?C1, tps')" using assms(1,3) transits_append by simp moreover have "transits ?M (length ?C1, tps') 1 (length ?C1 + 1, tps')" proof- have *: "?M ! (length ?C1) = cmd_jump cond (length M1 + 1) (length M1 + length M2 + 2)" using turing_machine_loop_def by simp have "execute ?M (length ?C1, tps') 1 = exe ?M (length ?C1, tps')" by simp also have "... = sem (?M ! (length ?C1)) (length ?C1, tps')" by (simp add: exe_lt_length turing_machine_loop_len) also have "... = sem (cmd_jump cond (length M1 + 1) (length M1 + length M2 + 2)) (length ?C1, tps')" using * by simp also have "... = (length M1 + 1, tps')" using sem_jump assms(3) by simp finally have "execute ?M (length ?C1, tps') 1 = (length M1 + 1, tps')" . then show ?thesis using transits_def by auto qed ultimately have "transits ?M (0, tps) (t1 + 1) (length M1 + 1, tps')" using transits_additive by blast moreover have "transits ?M (length M1 + 1, tps') t2 (length M1 + length M2 + 1, tps'')" proof- have "?M = ((?C1 @ ?C2) ;; M2) @ ?C4" by (simp add: parts turing_machine_sequential_def) moreover have "length (?C1 @ ?C2) = length M1 + 1" by simp ultimately have "transits ?M (length M1 + 1, tps') t2 (length M1 + 1 + length M2, tps'')" using assms transits_pre_append' by metis then show ?thesis by simp qed ultimately have "transits ?M (0, tps) (t1 + t2 + 1) (length M1 + length M2 + 1, tps'')" using transits_additive by fastforce moreover have "transits ?M (length M1 + length M2 + 1, tps'') 1 (0, tps'')" proof- have *: "?M ! (length M1 + length M2 + 1) = cmd_jump (λ_. True) 0 0" by (simp add: nth_append parts length_relocate) have "execute ?M (length M1 + length M2 + 1, tps'') 1 = exe ?M (length M1 + length M2 + 1, tps'')" by simp also have "... = sem (?M ! (length M1 + length M2 + 1)) (length M1 + length M2 + 1, tps'')" by (simp add: exe_lt_length turing_machine_loop_len) also have "... = sem (cmd_jump (λ_. True) 0 0) (length M1 + length M2 + 1, tps'')" using * by simp also have "... = (0, tps'')" using sem_jump by simp finally have "execute ?M (length M1 + length M2 + 1, tps'') 1 = (0, tps'')" . then show ?thesis using transits_def by auto qed ultimately show "transits ?M (0, tps) (t1 + t2 + 2) (0, tps'')" using transits_additive by fastforce qed text ‹ In this article we will only encounter while loops that are in fact for loops, that is, where the number of iterations is known beforehand. Moreover, using the same time bound for every iteration will lead to a good enough upper bound for the entire loop. The @{const transforms} rule for a loop with $m$ iterations where the running time of both TMs is bounded by a constant: › lemma transforms_loop_for: fixes m t1 t2 :: nat and M1 M2 :: machine and tps :: "nat ⇒ tape list" and tps' :: "nat ⇒ tape list" assumes "⋀i. i ≤ m ⟹ transforms M1 (tps i) t1 (tps' i)" assumes "⋀i. i < m ⟹ transforms M2 (tps' i) t2 (tps (Suc i))" and "⋀i. i < m ⟹ cond (read (tps' i))" and "¬ cond (read (tps' m))" assumes "ttt ≥ m * (t1 + t2 + 2) + t1 + 1" shows "transforms (WHILE M1 ; cond DO M2 DONE) (tps 0) ttt (tps' m)" proof - define M where "M = WHILE M1 ; cond DO M2 DONE" define t where "t = t1 + t2 + 2" have "transits M (0, tps 0) (i * t) (0, tps i)" if "i ≤ m" for i using that proof (induction i) case 0 then show ?case using transits_def by simp next case (Suc i) then have "i < m" by simp then have "transits M (0, tps i) t (0, tps (Suc i))" using M_def t_def assms transits_turing_machine_loop_cond_true by (metis le_eq_less_or_eq) moreover have "transits M (0, tps 0) (i * t) (0, tps i)" using Suc by simp ultimately have "transits M (0, tps 0) (i * t + t) (0, tps (Suc i))" using transits_additive by simp then show ?case by (metis add.commute mult_Suc) qed then have "transits M (0, tps 0) (m * t) (0, tps m)" by simp moreover have "transits M (0, tps m) (t1 + 1) (length M1 + length M2 + 2, tps' m)" using assms(1,4) transits_turing_machine_loop_cond_false M_def by simp ultimately have "transits M (0, tps 0) (m * t + t1 + 1) (length M1 + length M2 + 2, tps' m)" using transits_additive by fastforce then show ?thesis using transforms_def turing_machine_loop_len M_def assms(5) t_def transits_monotone by auto qed text ‹ The rule becomes even simpler in the common case in which the Turing machine in the loop head is empty. › lemma transforms_loop_simple: fixes m t :: nat and M :: machine and tps :: "nat ⇒ tape list" assumes "⋀i. i < m ⟹ transforms M (tps i) t (tps (Suc i))" and "⋀i. i < m ⟹ cond (read (tps i))" and "¬ cond (read (tps m))" assumes "ttt ≥ m * (t + 2) + 1" shows "transforms (WHILE [] ; cond DO M DONE) (tps 0) ttt (tps m)" using transforms_loop_for[where ?tps'=tps and ?cond=cond and ?t1.0=0, OF _ assms(1) _ assms(3)] transforms_Nil assms(2,4) by simp subsection ‹A proof method› text ‹ Statements about the behavior and running time of Turing machines, expressed via the predicate @{const transforms}, are the most common ones we are going to prove. The following proof method applies introduction rules for this predicate. These rules are either the ones we proved for the control structures (sequence, branching, loop) or the ones describing the semantics of concrete Turing machines. The rules of the second kind are collected in the attribute @{text transforms_intros}. Applying such a rule usually leaves three kinds of goals: some simple ones requiring only instantiation of schematic variables; one for the equality of two tape lists; and one for the time bound. For the last two goals the proof method offers parameters @{term tps} and @{term time}, respectively. I have to admit that most of the details of the proof method were determined by trial and error. \null › named_theorems transforms_intros declare transforms_Nil [transforms_intros] method tform uses tps time declares transforms_intros = ( ((rule transforms_tm_sequentialI)+ | rule transforms_branchI | rule transforms_loop_simple | rule transforms_loop_for | rule transforms_intros) ; (rule transforms_intros)? ; (simp only:; fail)? ; ((use tps in simp; fail) | (use time in simp; fail))? ; (match conclusion in "left = right" for left right :: "tape list" ⇒ ‹(fastforce simp add: tps list_update_swap; fail)›)? ; (match conclusion in "left = right" for left right :: nat ⇒ ‹(use time in simp; fail)?›)? ) text ‹ These lemmas are sometimes helpful for proving the equality of tape lists: › lemma list_update_swap_less: "i' < i ⟹ ys[i := x, i' := x'] = ys[i' := x', i := x]" by (simp add: list_update_swap) lemma nth_list_update_neq': "j ≠ i ⟹ xs[i := x] ! j = xs ! j" by simp end