Theory Combinations

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))"
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"

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)"
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"
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

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

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"
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"
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

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"
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)"
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
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:
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)))"
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)"
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')"
then have phase2: "transits ?M (0, tps) (t + 1) (length (?C1 @ ?C2), tps')"
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')"
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')"
then show ?thesis
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"
ultimately have seq: "?M = ?C123 ;; M2"
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)"
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')"
with phase1 have "transits ?M (0, tps) (t + 1) (length ?M, tps')"
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)"
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)
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')"
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')"
qed

lemma transits_turing_machine_loop_cond_true:
assumes "transforms M1 tps t1 tps'"
and "transforms M2 tps' t2 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')"
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')"
moreover have "transits ?M (length M1 + 1, tps') t2 (length M1 + length M2 + 1, tps'')"
proof-
have "?M = ((?C1 @ ?C2) ;; M2) @ ?C4"
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'')"
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'')"
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'')"
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))"
then show ?case
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)"
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
›

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]"