Quelle  Composing.thy

section ‹Composing functions\label{s:tm-composing}›

theory Composing
  imports Elementary
begin

text ‹
  a Turing machine $M_1$ computing $f_1$ in time $T_1$ and a TM $M_2$
  $f_2$ in time $T_2$ there is a TM $M$ computing $f_2 \circ f_1$ in
  $O(T_1(n) + \max_{m \le T_1(n)} T_2(m))$. If $T_1$ is monotone
  time bound is $O(T_1 + T_2 \circ T_1)$; if $T_1$ and $T_2$ are
  bounded the running-time of $M$ is polynomially bounded, too.

  Turing machines $M_1$ and $M_2$ can have both a different alphabet and
  of tapes, so generally they cannot be composed by the $;;$ operator. To
  around this we enlarge the alphabet and prepend and append tapes, so $M$ has
  many tapes as $M_1$ and $M_2$ combined. The following function returns the
  Turing machine $M$.

 null
 ›

definition "compose_machines k1 G1 M1 k2 G2 M2 ≡
  enlarged G1 (append_tapes k1 (k1 + k2) M1) ;;
  tm_start 1 ;;
  tm_cp_until 1 k1 {◻} ;;
  tm_erase_cr 1 ;;
  tm_start k1 ;;
  prepend_tapes k1 (enlarged G2 M2) ;;
  tm_cr (k1 + 1) ;;
  tm_cp_until (k1 + 1) 1 {◻}"

locale compose =
  fixes k1 k2 G1 G2 :: nat
    and M1 M2 :: machine
    and T1 T2 :: "nat ==> nat"
    and f1 f2 :: "string ==> string"
  assumes tm_M1: "turing_machine k1 G1 M1"
    and tm_M2: "turing_machine k2 G2 M2"
    and computes1: "computes_in_time k1 M1 f1 T1"
    and computes2: "computes_in_time k2 M2 f2 T2"
begin

definition "tm1 ≡ enlarged G1 (append_tapes k1 (k1 + k2) M1)"
definition "tm2 ≡ tm1 ;; tm_start 1"
definition "tm3 ≡ tm2 ;; tm_cp_until 1 k1 {◻}"
definition "tm4 ≡ tm3 ;; tm_erase_cr 1"
definition "tm5 ≡ tm4 ;; tm_start k1"
definition "tm56 ≡ prepend_tapes k1 (enlarged G2 M2)"
definition "tm6 ≡ tm5 ;; tm56"
definition "tm7 ≡ tm6 ;; tm_cr (k1 + 1)"
definition "tm8 ≡ tm7 ;; tm_cp_until (k1 + 1) 1 {◻}"

definition G :: nat where
  "G ≡ max G1 G2"

lemma G1: "G1 ≤ G" and G2: "G2 ≤ G"
  using G_def by simp_all

lemma k_ge: "k1 ≥ 2" "k2 ≥ 2"
  using tm_M1 tm_M2 turing_machine_def by simp_all

lemma tm1_tm: "turing_machine (k1 + k2) G tm1"
  unfolding tm1_def using turing_machine_enlarged append_tapes_tm tm_M1 G1 by simp

lemma tm2_tm: "turing_machine (k1 + k2) G tm2"
  unfolding tm2_def using tm1_tm tm_start_tm turing_machine_def by blast

lemma tm3_tm: "turing_machine (k1 + k2) G tm3"
  unfolding tm3_def
  using tm2_tm tm_cp_until_tm turing_machine_def k_ge turing_machine_sequential_turing_machine
  by (metis add_leD1 less_add_same_cancel1 less_le_trans less_numeral_extra(1) nat_1_add_1)

lemma tm4_tm: "turing_machine (k1 + k2) G tm4"
  unfolding tm4_def
  using tm3_tm tm_erase_cr_tm turing_machine_def turing_machine_sequential_turing_machine
  by (metis Suc_1 Suc_le_lessD tm_erase_cr_tm zero_less_one)

lemma tm5_tm: "turing_machine (k1 + k2) G tm5"
  unfolding tm5_def
  using tm4_tm tm_start_tm turing_machine_def turing_machine_sequential_turing_machine
  by auto

lemma tm6_tm: "turing_machine (k1 + k2) G tm6"
  unfolding tm6_def
  using tm5_tm tm56_def turing_machine_enlarged prepend_tapes_tm tm_M2 G2
  by simp

lemma tm7_tm: "turing_machine (k1 + k2) G tm7"
  unfolding tm7_def using tm6_tm tm_cr_tm turing_machine_def by blast

lemma tm8_tm: "turing_machine (k1 + k2) G tm8"
  unfolding tm8_def
  using tm7_tm tm_cp_until_tm turing_machine_def turing_machine_sequential_turing_machine k_ge(2)
  by (metis add.commute add_less_cancel_right add_strict_increasing nat_1_add_1
    verit_comp_simplify1(3) zero_less_one)

context
  fixes x :: string
begin

definition "zs ≡ string_to_symbols x"

lemma bit_symbols_zs: "bit_symbols zs"
  using zs_def by simp

abbreviation "n ≡ length x"

lemma length_zs [simp]: "length zs = n"
  using zs_def by simp

definition "tps0 ≡ snd (start_config (k1 + k2) zs)"

definition tps1a :: "tape list" where
  "tps1a ≡ SOME tps. tps ::: 1 = string_to_contents (f1 x) ∧
       transforms M1 (snd (start_config k1 (string_to_symbols x))) (T1 n) tps"

lemma tps1a_aux:
  "tps1a ::: 1 = string_to_contents (f1 x)"
  "transforms M1 (snd (start_config k1 (string_to_symbols x))) (T1 n) tps1a"
  using tps1a_def someI_ex[OF computes_in_timeD[OF computes1, of x]]
  by simp_all

lemma tps1a:
  "tps1a ::: 1 = string_to_contents (f1 x)"
  "transforms M1 (snd (start_config k1 zs)) (T1 n) tps1a"
  using tps1a_aux zs_def by simp_all

lemma length_tps1a [simp]: "length tps1a = k1"
  using tps1a(2) tm_M1 start_config_length execute_num_tapes transforms_def transits_def turing_machine_def
  by (smt (verit, del_insts) Suc_1 add_pos_pos less_le_trans less_numeral_extra(1) plus_1_eq_Suc snd_conv)

definition tps1b :: "tape list" where
  "tps1b ≡ replicate k2 (⌊[]⌋, 0)"

definition tps1 :: "tape list" where
  "tps1 ≡ tps1a @ tps1b"

lemma tps1_at_1: "tps1 ! 1 = tps1a ! 1"
  using tps1_def length_tps1a k_ge by (metis Suc_1 Suc_le_lessD nth_append)

lemma tps1_at_1': "tps1 ::: 1 = string_to_contents (f1 x)"
  using tps1_at_1 tps1a by simp

lemma tps1_pos_le: "tps1 :#: 1 ≤ T1 n"
proof -
  have "execute M1 (start_config k1 zs) (T1 n) = (length M1, tps1a)"
    using transforms_def transits_def tps1a(2)
    by (metis (no_types, lifting) execute_after_halting_ge fst_conv start_config_def snd_conv)
  moreover have "execute M1 (start_config k1 zs) (T1 n) <#> 1 ≤ T1 n"
    using head_pos_le_time[OF tm_M1, of 1] k_ge by fastforce
  ultimately show ?thesis
    using tps1_at_1 by simp
qed

lemma length_f1_x: "length (f1 x) ≤ T1 n"
proof -
  have "execute M1 (start_config k1 zs) (T1 n) = (length M1, tps1a)"
    using transforms_def transits_def tps1a(2)
    by (metis (no_types, lifting) execute_after_halting_ge fst_conv start_config_def snd_conv)
  moreover have "(execute M1 (start_config k1 zs) (T1 n) <:> 1) i = ◻" if "i > T1 n" for i
    using blank_after_time[OF that _ _ tm_M1] k_ge(1) by simp
  ultimately have "(tps1a ::: 1) i = ◻" if "i > T1 n" for i
    using that by simp
  then have "(string_to_contents (f1 x)) i = ◻" if "i > T1 n" for i
    using that tps1a(1) by simp
  then have "length (string_to_symbols (f1 x)) ≤ T1 n"
    by (metis length_map order_refl verit_comp_simplify1(3) zero_neq_numeral zero_neq_one)
  then show ?thesis
    by simp
qed

lemma start_config_append:
  "start_config (k1 + k2) zs = (0, snd (start_config k1 zs) @ tps1b)"
proof
  have "k1 > 0"
    using tm_M1 turing_machine_def by simp
  show "fst (start_config (k1 + k2) zs) = fst (0, snd (start_config k1 zs) @ tps1b)"
    using start_config_def by simp
  show "snd (start_config (k1 + k2) zs) = snd (0, snd (start_config k1 zs) @ tps1b)"
    (is "?l = ?r")
  proof (rule nth_equalityI)
    have len: "||start_config k1 zs|| = k1"
      using start_config_length by (simp add: ‹0 < k1›)
    show "length ?l = length ?r"
      using start_config_length tps1b_def tm_M1 turing_machine_def by simp
    show "?l ! j = ?r ! j" if "j < length ?l" for j
    proof (cases "j < k1")
      case True
      show ?thesis
      proof (cases "j = 0")
        case True
        then show ?thesis
          using start_config_def `k1 > 0` by simp
      next
        case False
        then have 1: "?l ! j = (λi. if i = 0 then ▹ else ◻, 0)"
          using start_config_def `k1 > 0` True by auto
        have "?r ! j = snd (start_config k1 zs) ! j"
          using True len by (simp add: nth_append)
        then have "?r ! j = (λi. if i = 0 then ▹ else ◻, 0)"
          using start_config4 `k1 > 0` False True by simp
        then show ?thesis
          using 1 by simp
      qed
    next
      case False
      then have j: "j < k1 + k2" "k1 ≤ j"
        using that ‹0 < k1› add_gr_0 start_config_length by simp_all
      then have "?r ! j = (⌊[]⌋, 0)"
        using tps1b_def by (simp add: False len nth_append)
      moreover have "?l ! j = (λi. if i = 0 then ▹ else ◻, 0)"
        using start_config4 `k1 > 0` j by simp
      ultimately show ?thesis
        by auto
    qed
  qed
qed

lemma tm1 [transforms_intros]: "transforms tm1 tps0 (T1 n) tps1"
proof -
  let ?M = "append_tapes k1 (k1 + length tps1b) M1"
  have len: "||start_config k1 zs|| = k1"
    using start_config_length[of k1 zs] tm_M1 turing_machine_def by simp
  have "transforms ?M (snd (start_config k1 zs) @ tps1b) (T1 n) (tps1a @ tps1b)"
    using transforms_append_tapes[OF tm_M1 len tps1a(2), of tps1b] .
  moreover have "tps0 = snd (start_config k1 zs) @ tps1b"
    unfolding tps0_def using start_config_append by simp
  ultimately have *: "transforms ?M tps0 (T1 n) tps1"
    using tps1_def by simp

  have "symbols_lt G1 zs"
    using bit_symbols_zs tm_M1 turing_machine_def by auto
  moreover have "turing_machine (k1 + k2) G1 ?M"
    using append_tapes_tm[OF tm_M1, of "k1 + k2"] by (simp add: tps1b_def)
  ultimately have "transforms (enlarged G1 ?M) tps0 (T1 n) tps1"
    using transforms_enlarged * tps0_def by simp
  then show ?thesis
    using tm1_def tps1b_def by simp
qed

lemma clean_string_to_contents: "clean_tape (string_to_contents xs, i)"
  using clean_tape_def by simp

definition tps2 :: "tape list" where
  "tps2 ≡ tps1 [1 := tps1 ! 1 |#=| 0]"

lemma length_tps2 [simp]: "length tps2 = k1 + k2"
  using tps2_def tps1_def by (simp add: tps1b_def)

lemma tm2:
  assumes "t = Suc (T1 n + tps1 :#: Suc 0)"
  shows "transforms tm2 tps0 t tps2"
  unfolding tm2_def
proof (tform tps: assms tps2_def)
  show "1 < length tps1"
    using tm_M1 turing_machine_def tps1_def by simp
  show "clean_tape (tps1 ! 1)"
      using tps1a(1) tps1_at_1 clean_tape_def by simp
qed

corollary tm2' [transforms_intros]:
  assumes "t = Suc (2 * T1 n)"
  shows "transforms tm2 tps0 t tps2"
  using assms tm2 tps1_pos_le transforms_monotone by simp

definition tps3 :: "tape list" where
  "tps3 ≡ tps2 [1 := tps2 ! 1 |#=| (Suc (length (f1 x))), k1 := tps2 ! 1 |#=| (Suc (length (f1 x)))]"

lemma tm3:
  assumes "t = Suc (Suc (2 * T1 n + Suc (length (f1 x))))"
  shows "transforms tm3 tps0 t tps3"
  unfolding tm3_def
proof (tform tps: k_ge)
  have "Suc 0 < k1 + k2" "0 < k2"
    using k_ge by simp_all
  then have *: "tps2 ! 1 = tps1 ! 1 |#=| 0"
    using tps2_def by (simp add: tps1_def tps1b_def)
  let ?i = "Suc (length (f1 x))"
  show "rneigh (tps2 ! 1) {0} ?i"
    using * tps1_at_1 tps1a by (intro rneighI) auto
  show "tps3 = tps2
    [1 := tps2 ! 1 |+| Suc (length (f1 x)),
     k1 := implant (tps2 ! 1) (tps2 ! k1) (Suc (length (f1 x)))]"
  proof -
    have "tps2 ! 1 |#=| (Suc (length (f1 x))) = tps2 ! 1 |#=| Suc (tps2 :#: 1 + length (f1 x))"
      by (metis "*" One_nat_def add_Suc plus_1_eq_Suc snd_conv)
    moreover have "tps2 ! 1 |#=| ?i = implant (tps2 ! 1) (tps2 ! k1) ?i"
    proof
      have 1: "tps2 ! 1 = (string_to_contents (f1 x), 0)"
        using tps1_at_1' * by simp
      have "tps1 ! k1 = (⌊[]⌋, 0)"
        using tps1_def tps1b_def by (simp add: ‹0 < k2› nth_append)
      then have 2: "tps2 ! k1 = (⌊[]⌋, 0)"
        using tps2_def k_ge by simp
      then show "snd (tps2 ! 1 |#=| ?i) = snd (implant (tps2 ! 1) (tps2 ! k1) ?i)"
        using implant by simp
      have "fst (implant (tps2 ! 1) (tps2 ! k1) ?i) i = fst (tps2 ! 1 |#=| ?i) i" for i
        using 1 2 implant by simp
      then show "fst (tps2 ! 1 |#=| ?i) = fst (implant (tps2 ! 1) (tps2 ! k1) ?i)"
        by auto
    qed
    ultimately show ?thesis
      using tps3_def by simp
  qed
  show "t = Suc (2 * T1 n) + Suc (Suc (length (f1 x)))"
    using assms by simp
qed

definition "tps3' ≡ tps1a
  [1 := (string_to_contents (f1 x), Suc (length (f1 x)))] @
   ((string_to_contents (f1 x), Suc (length (f1 x))) #
    replicate (k2 - 1) (⌊[]⌋, 0))"

lemma tps3': "tps3 = tps3'"
proof (rule nth_equalityI)
  have "length tps3 = k1 + k2"
    using tps3_def by simp
  moreover have "length tps3' = k1 + k2"
    using k_ge(2) tps3'_def by simp
  ultimately show "length tps3 = length tps3'"
    by simp
  show "tps3 ! j = tps3' ! j" if "j < length tps3" for j
  proof (cases "j < k1")
    case True
    then have rhs: "tps3' ! j = (tps1a [1 := (string_to_contents (f1 x), Suc (length (f1 x)))]) ! j"
      by (simp add: tps3'_def nth_append)
    show ?thesis
    proof (cases "j = 1")
      case True
      then have "tps3 ! j = tps2 ! 1 |#=| (Suc (length (f1 x)))"
        using tps3_def Suc_1 Suc_n_not_le_n ‹length tps3 = k1 + k2› k_ge(1)
          length_tps2 nth_list_update_eq nth_list_update_neq that
        by auto
      then have "tps3 ! j = tps1 ! 1 |#=| (Suc (length (f1 x)))"
        using tps2_def True ‹length tps3 = k1 + k2› length_tps2 that by auto
      then have "tps3 ! j = (string_to_contents (f1 x), Suc (length (f1 x)))"
        using tps1_at_1 tps1a(1) by simp
      then show ?thesis
        using rhs True k_ge(1) by auto
    next
      case False
      then have "tps3 ! j = tps2 ! j"
        using tps3_def True by simp
      then have "tps3 ! j = tps1 ! j"
        using tps2_def False by simp
      then have "tps3 ! j = tps1a ! j"
        using length_tps1a tps1_def False True by (simp add: nth_append)
      moreover have "tps3' ! j = tps1a ! j"
        using False rhs by simp
      ultimately show ?thesis
        by simp
    qed
  next
    case j_ge: False
    show ?thesis
    proof (cases "j = k1")
      case True
      then have "tps3 ! j = tps2 ! 1 |#=| (Suc (length (f1 x)))"
        using tps3_def that by simp
      then have "tps3 ! j = tps1 ! 1 |#=| (Suc (length (f1 x)))"
        using tps2_def ‹length tps3 = k1 + k2› length_tps2 Suc_1 Suc_le_lessD tm1_tm turing_machine_def
        by simp
      then have "tps3 ! j = (string_to_contents (f1 x), Suc (length (f1 x)))"
        using tps1_at_1 tps1a(1) by simp
      moreover have "tps3' ! j = (string_to_contents (f1 x), Suc (length (f1 x)))"
        using True tps3'_def
        by (metis (no_types, lifting) length_list_update length_tps1a nth_append_length)
      ultimately show ?thesis
        by simp
    next
      case False
      then have "j > k1"
        using j_ge by simp
      then have "tps3' ! j = ((string_to_contents (f1 x), Suc (length (f1 x))) #
          replicate (k2 - 1) (⌊[]⌋, 0)) ! (j - k1)"
        by (simp add: tps3'_def nth_append)
      moreover have "j - k1 < k2"
        by (metis ‹k1 < j› ‹length tps3 = k1 + k2› add.commute less_diff_conv2 less_imp_le that)
      ultimately have *: "tps3' ! j = (⌊[]⌋, 0)"
        by (metis (no_types, lifting) Suc_leI ‹k1 < j› add_leD1 le_add_diff_inverse2 less_diff_conv2
          nth_Cons_pos nth_replicate plus_1_eq_Suc zero_less_diff)
      have "tps3 ! j = tps2 ! j"
        using tps3_def ‹k1 < j› k_ge(1) by simp
      then have "tps3 ! j = tps1 ! j"
        using tps2_def ‹k1 < j› k_ge(1) by simp
      then have "tps3 ! j = tps1b ! (j - k1)"
        using tps1_def by (simp add: j_ge nth_append)
      then have "tps3 ! j = (⌊[]⌋, 0)"
        using tps1b_def by (simp add: ‹j - k1 < k2›)
      then show ?thesis
        using * by simp
    qed
  qed
qed

lemma tm3' [transforms_intros]:
  assumes "t = Suc (Suc (Suc (3 * T1 n)))"
  shows "transforms tm3 tps0 t tps3'"
proof -
  have "transforms tm3 tps0 (Suc (Suc (2 * T1 n + Suc (length (f1 x))))) tps3"
    using tm3 by simp
  moreover have "t ≥ Suc (Suc (2 * T1 n + Suc (length (f1 x))))"
    using assms length_f1_x by simp
  ultimately show ?thesis
    using tps3' transforms_monotone by auto
qed

definition "tps4 ≡
  tps1a [1 := (⌊[]⌋, 1)] @
  ((string_to_contents (f1 x), Suc (length (f1 x))) #
   replicate (k2 - 1) (⌊[]⌋, 0))"

lemma tm4:
  assumes "t = 9 + (3 * T1 n + (Suc (3 * length (string_to_symbols (f1 x)))))"
  shows "transforms tm4 tps0 t tps4"
  unfolding tm4_def
proof (tform)
  show "1 < length tps3'"
    using tps3'_def using tm1_tm turing_machine_def by auto
  let ?zs = "string_to_symbols (f1 x)"
  show "proper_symbols ?zs"
    by simp
  show "tps4 = tps3'[1 := (⌊[]⌋, 1)]"
    using tps4_def tps3'_def k_ge(1) length_tps1a by (simp add: list_update_append1)
  show "tps3' ::: 1 = ⌊string_to_symbols (f1 x)⌋"
  proof -
    have "tps3' ! 1 = (string_to_contents (f1 x), Suc (length (f1 x)))"
      using tps3'_def k_ge(1) length_tps1a by (simp add: nth_append)
    then show ?thesis
      by auto
  qed
  have "tps3' :#: 1 = Suc (length (f1 x))"
    using tps3'_def k_ge(1) length_tps1a by (simp add: nth_append)
  then show "t = Suc (Suc (Suc (3 * T1 n))) +
      (tps3' :#: 1 + 2 * length (string_to_symbols (f1 x)) + 6)"
    using assms by simp
qed

lemma tm4' [transforms_intros]:
  assumes "t = 10 + (6 * T1 n)"
  shows "transforms tm4 tps0 t tps4"
proof (rule transforms_monotone[OF tm4], simp)
  show "10 + (3 * T1 n + 3 * length (f1 x)) ≤ t"
    using length_f1_x assms by simp
qed

definition "tps5 ≡
  tps1a [1 := (⌊[]⌋, 1)] @
  ((string_to_contents (f1 x), 0) #
   replicate (k2 - 1) (⌊[]⌋, 0))"

lemma tm5:
  assumes "t = 11 + (6 * T1 n + tps4 :#: k1)"
  shows "transforms tm5 tps0 t tps5"
  unfolding tm5_def
proof (tform time: assms)
  show "k1 < length tps4"
    using tps4_def length_tps1a by simp
  show "tps5 = tps4[k1 := tps4 ! k1 |#=| 0]"
    using tps4_def tps5_def length_tps1a
    by (metis (no_types, lifting) fst_conv length_list_update list_update_length nth_append_length)
  show "clean_tape (tps4 ! k1)"
    using tps4_def length_tps1a clean_tape_def
    by (smt (verit) Suc_eq_plus1 add.commute add_cancel_right_right
      fst_conv length_list_update nat.distinct(1) nat_1_add_1 nth_append_length numeral_3_eq_3)
qed

abbreviation "ys ≡ string_to_symbols (f1 x)"

abbreviation "m ≡ length (f1 x)"

definition "tps5' ≡
  tps1a [1 := (⌊[]⌋, 1)] @
  snd (start_config k2 ys)"

lemma tps5': "tps5 = tps5'"
  using tps5_def tps5'_def start_config_def by auto

lemma tm5' [transforms_intros]:
  assumes "t = 12 + 7 * T1 n"
  shows "transforms tm5 tps0 t tps5'"
proof -
  have "tps4 :#: k1 = Suc (length (f1 x))"
    using tps4_def
    by (metis (no_types, lifting) length_list_update length_tps1a nth_append_length snd_conv)
  then have "tps4 :#: k1 ≤ Suc (T1 n)"
    using length_f1_x by simp
  then have "t ≥ 11 + (6 * T1 n + tps4 :#: k1)"
    using assms by simp
  then show ?thesis
    using tm5 transforms_monotone tps5' by simp
qed

definition tps6b :: "tape list" where
  "tps6b ≡ SOME tps. tps ::: 1 = string_to_contents (f2 (f1 x)) ∧
       transforms M2 (snd (start_config k2 ys)) (T2 m) tps"

lemma tps6b:
  "tps6b ::: 1 = string_to_contents (f2 (f1 x))"
  "transforms M2 (snd (start_config k2 ys)) (T2 m) tps6b"
  using tps6b_def someI_ex[OF computes_in_timeD[OF computes2, of "f1 x"]]
  by simp_all

lemma tps6b_pos_le: "tps6b :#: 1 ≤ T2 m"
proof -
  have "execute M2 (start_config k2 ys) (T2 m) = (length M2, tps6b)"
    using transforms_def transits_def tps6b(2)
    by (metis (no_types, lifting) execute_after_halting_ge fst_conv start_config_def snd_conv)
  moreover have "execute M2 (start_config k2 ys) (T2 m) <#> 1 ≤ T2 m"
    using head_pos_le_time[OF tm_M2, of 1] k_ge by simp
  ultimately show ?thesis
    by simp
qed

lemma length_tps6b: "length tps6b = k2"
  using tm_M2 execute_num_tapes k_ge(2) tps5' tps5'_def tps5_def tps6b(2) transforms_def transits_def
  by (smt (verit, ccfv_threshold) One_nat_def Suc_diff_Suc length_Cons length_replicate less_le_trans
    minus_nat.diff_0 numeral_2_eq_2 prod.sel(2) same_append_eq zero_less_Suc)

lemma length_f2_f1_x: "length (f2 (f1 x)) ≤ T2 m"
proof -
  have "execute M2 (start_config k2 ys) (T2 m) = (length M2, tps6b)"
    using transforms_def transits_def tps6b(2)
    by (metis (no_types, lifting) execute_after_halting_ge fst_conv start_config_def snd_conv)
  moreover have "(execute M2 (start_config k2 ys) (T2 m) <:> 1) i = 0" if "i > T2 m" for i
    using blank_after_time[OF that _ _ tm_M2] k_ge(2) by simp
  ultimately have "(tps6b ::: 1) i = ◻" if "i > T2 m" for i
    using that by simp
  then have "(string_to_contents (f2 (f1 x))) i = ◻" if "i > T2 m" for i
    using that tps6b(1) by simp
  then have "length (string_to_symbols (f2 (f1 x))) ≤ T2 m"
    by (metis length_map order_refl verit_comp_simplify1(3) zero_neq_numeral zero_neq_one)
  then show ?thesis
    by simp
qed

lemma enlarged_M2: "transforms (enlarged G2 M2) (snd (start_config k2 ys)) (T2 m) tps6b"
proof -
  have "symbols_lt G2 (string_to_symbols (f1 x))"
    using tm_M2 turing_machine_def by simp
  then show ?thesis
    using transforms_enlarged[OF tm_M2 _ tps6b(2)] by simp
qed

lemma enlarged_M2_tm: "turing_machine k2 G (enlarged G2 M2)"
  using turing_machine_enlarged tm_M2 G2 by simp

definition "tps6 ≡ tps1a[1 := (⌊[]⌋, 1)] @ tps6b"

lemma tm56 [transforms_intros]: "transforms tm56 tps5' (T2 m) tps6"
  using transforms_prepend_tapes[OF enlarged_M2_tm _ _ enlarged_M2, of "tps1a [1 := (⌊[]⌋, 1)]" k1]
    tps5'_def tps6_def tm56_def start_config_length k_ge(2)
  by auto

lemma tps6_at_Suc_k1: "tps6 ::: (k1 + 1) = string_to_contents (f2 (f1 x))"
  and tps6_pos_le: "tps6 :#: (k1 + 1) ≤ T2 m"
proof -
  have "tps6 ! (k1 + 1) = tps6b ! 1"
    using tps6_def length_tps1a length_tps6b by (simp add: nth_append)
  then show
    "tps6 ::: (k1 + 1) = string_to_contents (f2 (f1 x))"
    "tps6 :#: (k1 + 1) ≤ T2 m"
    using tps6b(1) tps6b_pos_le by simp_all
qed

lemma tm6 [transforms_intros]:
  assumes "t = 12 + 7 * T1 n + T2 m"
  shows "transforms tm6 tps0 t tps6"
  unfolding tm6_def by (tform tps: assms)

definition "tps7 ≡
  tps1a[1 := (⌊[]⌋, 1)] @
  tps6b[1 := (string_to_contents (f2 (f1 x)), 1)]"

lemma tps7_at_Suc_k1: "tps7 ! (k1 + 1) = (string_to_contents (f2 (f1 x)), 1)"
  using tps7_def k_ge(2) length_tps1a length_tps6b
  by (metis (no_types, lifting) One_nat_def Suc_le_lessD add.commute diff_add_inverse
    length_list_update not_add_less2 nth_append nth_list_update_eq numeral_2_eq_2)

lemma tm7:
  assumes "t = 14 + (7 * T1 n + (T2 m + tps6 :#: Suc k1))"
  shows "transforms tm7 tps0 t tps7"
  unfolding tm7_def
proof (tform time: assms)
  show "k1 + 1 < length tps6"
    using tps6_def k_ge(2) length_tps1a length_tps6b by simp
  show "clean_tape (tps6 ! (k1 + 1))"
    using tps6_at_Suc_k1 clean_tape_def by simp
  show "tps7 = tps6[k1 + 1 := tps6 ! (k1 + 1) |#=| 1]"
  proof -
    have "tps6 ! (k1 + 1) |#=| 1 = (string_to_contents (f2 (f1 x)), 1)"
      using tps6_at_Suc_k1 by simp
    then show ?thesis
      using tps6_def tps7_def length_tps1a length_tps6b k_ge tps7_at_Suc_k1
      by (metis (no_types, lifting) add.commute diff_add_inverse length_list_update
        list_update_append not_add_less2 plus_1_eq_Suc)
  qed
qed

corollary tm7' [transforms_intros]:
  assumes "t = 14 + 7 * T1 n + 2 * T2 m"
  shows "transforms tm7 tps0 t tps7"
proof (rule transforms_monotone[OF tm7], simp)
  show "14 + (7 * T1 n + (T2 (length (f1 x)) + tps6 :#: Suc k1)) ≤ t"
    using assms tps6_pos_le by simp
qed

definition "tps8 ≡
  tps1a[1 := (string_to_contents (f2 (f1 x)), Suc (length (f2 (f1 x))))] @
  tps6b[1 := (string_to_contents (f2 (f1 x)), Suc (length (f2 (f1 x))))]"

lemma tps8_at_1: "tps8 ::: 1 = string_to_contents (f2 (f1 x))"
  using tps8_def length_tps1a k_ge(1)
  by (metis (no_types, lifting) One_nat_def Suc_le_lessD length_list_update nth_append
    nth_list_update_eq numeral_2_eq_2 prod.sel(1))

lemma tm8:
  assumes "t = 15 + 7 * T1 n + 2 * T2 m + length (f2 (f1 x))"
  shows "transforms tm8 tps0 t tps8"
  unfolding tm8_def
proof (tform tps: assms)
  show "k1 + 1 < length tps7"
    using tps7_def length_tps1a length_tps6b k_ge(2) by simp
  show "1 < length tps7"
    using tps7_def length_tps6b k_ge(2) by simp
  let ?n = "length (f2 (f1 x))"
  show "rneigh (tps7 ! (k1 + 1)) {◻} ?n"
  proof (rule rneighI)
   show "(tps7 ::: (k1 + 1)) (tps7 :#: (k1 + 1) + ?n) ∈ {◻}"
     using tps7_at_Suc_k1 by simp
   show "∧n'. n' < ?n ==> (tps7 ::: (k1 + 1)) (tps7 :#: (k1 + 1) + n') ∉ {◻}"
     using tps7_at_Suc_k1 by simp
  qed
  show "tps8 = tps7
    [k1 + 1 := tps7 ! (k1 + 1) |+| ?n,
     1 := implant (tps7 ! (k1 + 1)) (tps7 ! 1) ?n]"
     (is "tps8 = ?tps")
  proof (rule nth_equalityI)
    show "length tps8 = length ?tps"
      using tps8_def tps7_def by simp
    have len: "length tps8 = k1 + k2"
      using tps8_def length_tps6b by simp
    show "tps8 ! j = ?tps ! j" if "j < length tps8" for j
    proof (cases "j < k1")
      case j_less: True
      then have lhs: "tps8 ! j = tps1a[1 := (string_to_contents (f2 (f1 x)), Suc (length (f2 (f1 x))))] ! j"
        using tps8_def length_tps1a length_tps6b k_ge by (simp add: nth_append)
      show ?thesis
      proof (cases "j = 1")
        case True
        then have 1: "?tps ! j = implant (tps7 ! (k1 + 1)) (tps7 ! 1) ?n"
          using ‹1 < length tps7› by simp
        have 2: "tps8 ! j = (string_to_contents (f2 (f1 x)), Suc (length (f2 (f1 x))))"
          using lhs True j_less by simp
        have 3: "tps7 ! 1 = (⌊[]⌋, 1)"
          using tps7_def length_tps1a
          by (metis (no_types, lifting) True j_less length_list_update nth_append nth_list_update_eq)
        have "implant (string_to_contents (f2 (f1 x)), 1) (⌊[]⌋, 1) ?n =
            (string_to_contents (f2 (f1 x)), Suc ?n)"
          using implant contents_def by auto
        then show ?thesis
          using 1 2 3 tps7_at_Suc_k1 by simp
      next
        case False
        then have "?tps ! j = tps7 ! j"
          by (metis One_nat_def Suc_eq_plus1 add.commute j_less not_add_less2 nth_list_update_neq)
        then have "?tps ! j = tps1a ! j"
          using False j_less tps7_def length_tps1a
          by (metis (no_types, lifting) length_list_update nth_append nth_list_update_neq)
        moreover have "tps8 ! j = tps1a ! j"
          using False j_less tps8_def lhs by simp
        ultimately show ?thesis
          by simp
      qed
    next
      case j_ge: False
      then have lhs: "tps8 ! j = tps6b[1 := (string_to_contents (f2 (f1 x)), Suc (length (f2 (f1 x))))] ! (j - k1)"
        using tps8_def length_tps1a length_tps6b k_ge by (simp add: nth_append)
      show ?thesis
      proof (cases "j = Suc k1")
        case True
        then have "tps8 ! j = (string_to_contents (f2 (f1 x)), Suc (length (f2 (f1 x))))"
          using lhs len that length_tps6b by simp
        moreover have "?tps ! j = tps7 ! Suc k1 |+| ?n"
          using True ‹k1 + 1 < length tps7› k_ge(1) by simp
        ultimately show ?thesis
          using tps7_at_Suc_k1 True by simp
      next
        case False
        then have "tps8 ! j = tps6b ! (j - k1)"
          using lhs by simp
        moreover have "?tps ! j = tps7 ! j"
          using False j_ge that k_ge(1) by simp
        ultimately show ?thesis
          using tps7_def j_ge False length_tps1a
          by (metis (no_types, lifting) add.commute add_diff_inverse_nat length_list_update
            nth_append nth_list_update_neq plus_1_eq_Suc)
      qed
    qed
  qed
qed

lemma tm8':
  assumes "t = 15 + 7 * T1 n + 3 * T2 m"
  shows "transforms tm8 tps0 t tps8"
proof (rule transforms_monotone[OF tm8], simp)
  show "15 + 7 * T1 n + 2 * T2 m + length (f2 (f1 x)) ≤ t"
    using length_f2_f1_x assms by simp
qed

lemma tm8'_mono:
  assumes "mono T2"
    and "t = 15 + 7 * T1 n + 3 * T2 (T1 n)"
  shows "transforms tm8 tps0 t tps8"
proof (rule transforms_monotone[OF tm8'], simp)
  have "T2 (T1 n) ≥ T2 m"
    using assms(1) length_f1_x monoE by auto
  then show "15 + 7 * T1 n + 3 * T2 m ≤ t"
    using assms(2) by simp
qed

end  (* context x *)

lemma computes_composed_mono:
  assumes "mono T2" and "T = (λn. 15 + 7 * T1 n + 3 * T2 (T1 n))"
  shows "computes_in_time (k1 + k2) tm8 (f2 ∘ f1) T"
proof
  fix x
  have "tps8 x ::: 1 = string_to_contents (f2 (f1 x))"
    using tps8_at_1 by simp
  moreover have "transforms tm8 (snd (start_config (k1 + k2) (string_to_symbols x))) (T (length x)) (tps8 x)"
    using tm8'_mono assms tps0_def zs_def by simp
  ultimately show "∃tps.
      tps ::: 1 = string_to_contents ((f2 ∘ f1) x) ∧
      transforms tm8 (snd (start_config (k1 + k2) (string_to_symbols x))) (T (length x)) tps"
    by force
qed

end  (* locale compose *)

lemma computes_composed_poly:
  assumes tm_M1: "turing_machine k1 G1 M1"
    and tm_M2: "turing_machine k2 G2 M2"
    and computes1: "computes_in_time k1 M1 f1 T1"
    and computes2: "computes_in_time k2 M2 f2 T2"
  assumes "big_oh_poly T1" and "big_oh_poly T2"
  shows "∃T k G M. big_oh_poly T ∧ turing_machine k G M ∧ computes_in_time k M (f2 ∘ f1) T"
proof -
  obtain d1 :: nat where "big_oh T1 (λn. n ^ d1)"
    using assms(5) big_oh_poly_def by auto
  obtain b c d2 :: nat where cm: "d2 > 0" "∀n. T2 n ≤ b + c * n ^ d2"
    using big_oh_poly_offset[OF assms(6)] by auto
  let ?U = "λn. b + c * n ^ d2"
  have U: "T2 n ≤ ?U n" for n
    using cm by simp
  have "mono ?U"
    by standard (simp add: cm(1))
  have computesU: "computes_in_time k2 M2 f2 ?U"
    using computes_in_time_mono[OF computes2 U] .
  interpret compo: compose k1 k2 G1 G2 M1 M2 T1 ?U f1 f2
    using assms computesU compose.intro by simp
  let ?M = "compo.tm8"
  let ?T = "(λn. 15 + 7 * T1 n + 3 * (b + c * T1 n ^ d2))"
  have "computes_in_time (k1 + k2) ?M (f2 ∘ f1) ?T"
    using compo.computes_composed_mono[OF `mono ?U`, of ?T] by simp
  moreover have "big_oh_poly ?T"
  proof -
    have "big_oh_poly (λn. n ^ d2)"
      using big_oh_poly_poly by simp
    moreover have "(λn. T1 n ^ d2) = (λn. n ^ d2) ∘ T1"
      by auto
    ultimately have "big_oh_poly (λn. T1 n ^ d2)"
      using big_oh_poly_composition[OF assms(5)] by auto
    then have "big_oh_poly (λn. 3 * (b + c * T1 n ^ d2))"
      using big_oh_poly_const big_oh_poly_prod big_oh_poly_sum by simp
    then show ?thesis
      using assms(5) big_oh_poly_const big_oh_poly_prod big_oh_poly_sum by simp
  qed
  moreover have "turing_machine (k1 + k2) compo.G ?M"
    using compo.tm8_tm .
  ultimately show ?thesis
    by auto
qed

end