chapter ‹Auxiliary Turing machines for reducing $\NP$ languages to \SAT{}\label{s:Aux_TM}› theory Aux_TM_Reducing imports Reducing begin text ‹ In the previous chapter we have seen how to reduce a language $L\in\NP$ to \SAT{} by constructing for every string $x$ a CNF formula $\Phi$ that is satisfiable iff.\ $x\in L$. To complete the Cook-Levin theorem it remains to show that there is a polynomial-time Turing machine that on input $x$ outputs $\Phi$. Constructing such a TM will be the subject of the rest of this article and conclude in the next chapter. This chapter introduces several TMs used in the construction. › section ‹Generating literals› text ‹ Our representation of CNF formulas as lists of lists of numbers is based on a representation of literals as numbers. Our function @{const literal_n} encodes the positive literal $v_i$ as the number $2i + 1$ and the negative literal $\bar v_i$ as $2i$. We already have the Turing machine @{const tm_times2} to cover the second case. Now we build a TM for the first case, that is, for doubling and incrementing. \null › definition tm_times2incr :: "tapeidx ⇒ machine" where "tm_times2incr j ≡ tm_times2 j ;; tm_incr j" lemma tm_times2incr_tm: assumes "0 < j" and "j < k" and "G ≥ 4" shows "turing_machine k G (tm_times2incr j)" unfolding tm_times2incr_def using tm_times2_tm tm_incr_tm assms by simp lemma transforms_tm_times2incrI [transforms_intros]: fixes j :: tapeidx fixes k :: nat and tps tps' :: "tape list" assumes "k ≥ 2" and "j > 0" and "j < k" and "length tps = k" assumes "tps ! j = (⌊n⌋⇩_{N}, 1)" assumes "t = 12 + 4 * nlength n" assumes "tps' = tps[j := (⌊Suc (2 * n)⌋⇩_{N}, 1)]" shows "transforms (tm_times2incr j) tps t tps'" proof - define tt where "tt = 10 + (2 * nlength n + 2 * nlength (2 * n))" have "transforms (tm_times2incr j) tps tt tps'" unfolding tm_times2incr_def by (tform tps: tt_def assms) moreover have "tt ≤ t" proof - have "tt = 10 + 2 * nlength n + 2 * nlength (2 * n)" using tt_def by simp also have "... ≤ 10 + 2 * nlength n + 2 * (Suc (nlength n))" proof - have "nlength (2 * n) ≤ Suc (nlength n)" by (metis eq_imp_le gr0I le_SucI nat_0_less_mult_iff nlength_even_le) then show ?thesis by simp qed also have "... = 12 + 4 * nlength n" by simp finally show ?thesis using assms(6) by simp qed ultimately show ?thesis using transforms_monotone by simp qed lemma literal_n_rename: assumes "v div 2 < length σ" shows "2 * σ ! (v div 2) + v mod 2 = (literal_n ∘ rename σ) (n_literal v)" proof (cases "even v") case True then show ?thesis using n_literal_def assms by simp next case False then show ?thesis using n_literal_def assms by simp presburger qed text ‹ Combining @{const tm_times2} and @{const tm_times2incr}, the next Turing machine accepts a variable index $i$ on tape $j_1$ and a flag $b$ on tape $j_2$ and outputs on tape $j_1$ the encoding of the positive literal $v_i$ or the negative literal $\bar v_i$ if $b$ is positive or zero, respectively. › definition tm_to_literal :: "tapeidx ⇒ tapeidx ⇒ machine" where "tm_to_literal j1 j2 ≡ IF λrs. rs ! j2 = □ THEN tm_times2 j1 ELSE tm_times2incr j1 ENDIF" lemma tm_to_literal_tm: assumes "k ≥ 2" and "G ≥ 4" and "0 < j1" and "j1 < k" and "j2 < k" shows "turing_machine k G (tm_to_literal j1 j2)" unfolding tm_to_literal_def using assms tm_times2_tm tm_times2incr_tm turing_machine_branch_turing_machine by simp lemma transforms_tm_to_literalI [transforms_intros]: fixes j1 j2 :: tapeidx fixes tps tps' :: "tape list" and ttt k i b :: nat assumes "0 < j1" "j1 < k" "j2 < k" "2 ≤ k" "length tps = k" assumes "tps ! j1 = (⌊i⌋⇩_{N}, 1)" "tps ! j2 = (⌊b⌋⇩_{N}, 1)" assumes "ttt = 13 + 4 * nlength i" assumes "tps' = tps [j1 := (⌊2 * i + (if b = 0 then 0 else 1)⌋⇩_{N}, 1)]" shows "transforms (tm_to_literal j1 j2) tps ttt tps'" unfolding tm_to_literal_def proof (tform tps: assms read_ncontents_eq_0) show "5 + 2 * nlength i + 2 ≤ ttt" and "12 + 4 * nlength i + 1 ≤ ttt" using assms(8) by simp_all qed section ‹A Turing machine for relabeling formulas› text ‹ In order to construct $\Phi_9$, we must construct CNF formulas $\chi_t$, which have the form $\rho(\psi)$ or $\rho'(\psi')$. So we need a Turing machine for relabeling formulas. In this section we devise a Turing machine that gets a substitution $\sigma$ and a CNF formula $\phi$ and outputs $\sigma(\phi)$. In order to bound its running time we first prove some bounds on the length of relabeled formulas. › subsection ‹The length of relabeled formulas› text ‹ First we bound the length of the representation of a single relabeled clause. In the following lemma the assumption ensures that the substitution $\sigma$ has a value for every variable in the clause. › lemma nllength_rename: assumes "∀v∈set clause. v div 2 < length σ" shows "nllength (map (literal_n ∘ rename σ) (n_clause clause)) ≤ length clause * Suc (nllength σ)" proof (cases "σ = []") case True then show ?thesis using assms n_clause_def by simp next case False let ?f = "literal_n ∘ rename σ ∘ n_literal" have *: "map (literal_n ∘ rename σ) (n_clause clause) = map ?f clause" using n_clause_def by simp have "nlength (2 * n + 1) ≤ Suc (nlength n)" for n using nlength_times2plus1 by simp then have "nlength (2 * Max (set σ) + 1) ≤ Suc (nlength (Max (set σ)))" by simp moreover have "nlength (Max (set σ)) ≤ nllength σ - 1" using False member_le_nllength_1 by simp ultimately have "nlength (2 * Max (set σ) + 1) ≤ Suc (nllength σ - 1)" by simp then have **: "nlength (2 * Max (set σ) + 1) ≤ nllength σ" using nllength_gr_0 False by simp have "?f n ≤ 2 * (σ ! (n div 2)) + 1" if "n div 2 < length σ" for n using n_literal_def by (cases "even n") simp_all then have "?f v ≤ 2 * (σ ! (v div 2)) + 1" if "v ∈ set clause" for v using assms that by simp moreover have "σ ! (v div 2) ≤ Max (set σ)" if "v ∈ set clause" for v using that assms by simp ultimately have "?f v ≤ 2 * Max (set σ) + 1" if "v ∈ set clause" for v using that by fastforce then have "n ≤ 2 * Max (set σ) + 1" if "n ∈ set (map ?f clause)" for n using that by auto then have "nllength (map ?f clause) ≤ Suc (nlength (2 * Max (set σ) + 1)) * length (map ?f clause)" using nllength_le_len_mult_max by blast also have "... = Suc (nlength (2 * Max (set σ) + 1)) * length clause" by simp also have "... ≤ Suc (nllength σ) * length clause" using ** by simp finally have "nllength (map ?f clause) ≤ Suc (nllength σ) * length clause" . then show ?thesis using * by (metis mult.commute) qed text ‹ Our upper bound for the length of the symbol representation of a relabeled formula is fairly crude. It is basically the length of the string resulting from replacing every symbol of the original formula by the entire substitution. › lemma nlllength_relabel: assumes "∀clause∈set φ. ∀v∈set (clause_n clause). v div 2 < length σ" shows "nlllength (formula_n (relabel σ φ)) ≤ Suc (nllength σ) * nlllength (formula_n φ)" using assms proof (induction φ) case Nil then show ?case by (simp add: relabel_def) next case (Cons clause φ) let ?nclause = "clause_n clause" have "∀v∈set ?nclause. v div 2 < length σ" using Cons.prems by simp then have "nllength (map (literal_n ∘ rename σ) (n_clause ?nclause)) ≤ length ?nclause * Suc (nllength σ)" using nllength_rename by simp then have "nllength (map (literal_n ∘ rename σ) clause) ≤ length clause * Suc (nllength σ)" using clause_n_def n_clause_n by simp moreover have "map (literal_n ∘ rename σ) clause = clause_n (map (rename σ) clause)" using clause_n_def by simp ultimately have *: "nllength (clause_n (map (rename σ) clause)) ≤ length clause * Suc (nllength σ)" by simp have "formula_n (relabel σ (clause # φ)) = clause_n (map (rename σ) clause) # formula_n (relabel σ φ)" by (simp add: formula_n_def relabel_def) then have "nlllength (formula_n (relabel σ (clause # φ))) = nllength (clause_n (map (rename σ) clause)) + 1 + nlllength (formula_n (relabel σ φ))" using nlllength_Cons by simp also have "... ≤ length clause * Suc (nllength σ) + 1 + nlllength (formula_n (relabel σ φ))" using * by simp also have "... ≤ length clause * Suc (nllength σ) + 1 + Suc (nllength σ) * nlllength (formula_n φ)" using Cons by (metis add_mono_thms_linordered_semiring(2) insert_iff list.set(2)) also have "... = 1 + Suc (nllength σ) * (length clause + nlllength (formula_n φ))" by algebra also have "... ≤ Suc (nllength σ) * (1 + length clause + nlllength (formula_n φ))" by simp also have "... ≤ Suc (nllength σ) * (1 + nllength (clause_n clause) + nlllength (formula_n φ))" using length_le_nllength n_clause_def n_clause_n by (metis add_Suc_shift add_le_cancel_right length_map mult_le_mono2 plus_1_eq_Suc) also have "... = Suc (nllength σ) * (nlllength (formula_n (clause # φ)))" using formula_n_def nlllength_Cons by simp finally show ?case . qed text ‹ A simple sufficient condition for the assumption in the previous lemma. › lemma variables_σ: assumes "variables φ ⊆ {..<length σ}" shows "∀clause∈set φ.∀v∈set (clause_n clause). v div 2 < length σ" proof standard+ fix clause :: clause and v :: nat assume clause: "clause ∈ set φ" and v: "v ∈ set (clause_n clause)" obtain i where i: "i < length clause" "v = literal_n (clause ! i)" using v clause_n_def by (metis in_set_conv_nth length_map nth_map) then have clause_i: "clause ! i = n_literal v" using n_literal_n by simp show "v div 2 < length σ" proof (cases "even v") case True then have "clause ! i = Neg (v div 2)" using clause_i n_literal_def by simp then have "∃c∈set φ. Neg (v div 2) ∈ set c" using clause i(1) by (metis nth_mem) then have "v div 2 ∈ variables φ" using variables_def by auto then show ?thesis using assms by auto next case False then have "clause ! i = Pos (v div 2)" using clause_i n_literal_def by simp then have "∃c∈set φ. Pos (v div 2) ∈ set c" using clause i(1) by (metis nth_mem) then have "v div 2 ∈ variables φ" using variables_def by auto then show ?thesis using assms by auto qed qed text ‹ Combining the previous two lemmas yields this upper bound: › lemma nlllength_relabel_variables: assumes "variables φ ⊆ {..<length σ}" shows "nlllength (formula_n (relabel σ φ)) ≤ Suc (nllength σ) * nlllength (formula_n φ)" using assms variables_σ nlllength_relabel by blast subsection ‹Relabeling clauses› text ‹ Relabeling a CNF formula is accomplished by relabeling each of its clauses. In this section we devise a Turing machine for relabeling clauses. The TM accepts on tape $j$ a list of numbers representing a substitution $\sigma$ and on tape $j + 1$ a clause represented as a list of numbers. It outputs on tape $j + 2$ the relabeled clause, consuming the original clause on tape $j + 1$ in the process. › definition tm_relabel_clause :: "tapeidx ⇒ machine" where "tm_relabel_clause j ≡ WHILE [] ; λrs. rs ! (j + 1) ≠ □ DO tm_nextract ¦ (j + 1) (j + 3) ;; tm_mod2 (j + 3) (j + 4) ;; tm_div2 (j + 3) ;; tm_nth_inplace j (j + 3) ¦ ;; tm_to_literal (j + 3) (j + 4) ;; tm_append (j + 2) (j + 3) ;; tm_setn (j + 3) 0 ;; tm_setn (j + 4) 0 DONE ;; tm_cr (j + 2) ;; tm_erase_cr (j + 1)" lemma tm_relabel_clause_tm: assumes "G ≥ 5" and "j + 4 < k" and "0 < j" shows "turing_machine k G (tm_relabel_clause j)" unfolding tm_relabel_clause_def using assms tm_nextract_tm tm_mod2_tm tm_div2_tm tm_nth_inplace_tm tm_to_literal_tm tm_append_tm tm_setn_tm tm_cr_tm tm_erase_cr_tm Nil_tm turing_machine_loop_turing_machine by simp locale turing_machine_relabel_clause = fixes j :: tapeidx begin definition "tm1 ≡ tm_nextract ¦ (j + 1) (j + 3)" definition "tm2 ≡ tm1 ;; tm_mod2 (j + 3) (j + 4)" definition "tm3 ≡ tm2 ;; tm_div2 (j + 3)" definition "tm4 ≡ tm3 ;; tm_nth_inplace j (j + 3) ¦" definition "tm5 ≡ tm4 ;; tm_to_literal (j + 3) (j + 4)" definition "tm6 ≡ tm5 ;; tm_append (j + 2) (j + 3)" definition "tm7 = tm6 ;; tm_setn (j + 3) 0" definition "tm8 ≡ tm7 ;; tm_setn (j + 4) 0" definition "tmL ≡ WHILE [] ; λrs. rs ! (j + 1) ≠ □ DO tm8 DONE" definition "tm9 ≡ tmL ;; tm_cr (j + 2)" definition "tm10 ≡ tm9 ;; tm_erase_cr (j + 1)" lemma tm10_eq_tm_relabel_clause: "tm10 = tm_relabel_clause j" unfolding tm_relabel_clause_def tm3_def tmL_def tm5_def tm4_def tm1_def tm2_def tm6_def tm7_def tm8_def tm9_def tm10_def by simp context fixes tps0 :: "tape list" and k :: nat and σ clause :: "nat list" assumes clause: "∀v∈set clause. v div 2 < length σ" assumes jk: "0 < j" "j + 4 < k" "length tps0 = k" assumes tps0: "tps0 ! j = (⌊σ⌋⇩_{N}⇩_{L}, 1)" "tps0 ! (j + 1) = (⌊clause⌋⇩_{N}⇩_{L}, 1)" "tps0 ! (j + 2) = (⌊[]⌋⇩_{N}⇩_{L}, 1)" "tps0 ! (j + 3) = (⌊0⌋⇩_{N}, 1)" "tps0 ! (j + 4) = (⌊0⌋⇩_{N}, 1)" begin definition "tpsL t ≡ tps0 [j + 1 := nltape' clause t, j + 2 := nltape (take t (map literal_n (map (rename σ) (n_clause clause))))]" lemma tpsL_eq_tps0: "tpsL 0 = tps0" using tpsL_def tps0 jk nllength_Nil by (metis One_nat_def list_update_id take0) definition "tps1 t ≡ tps0 [j + 1 := nltape' clause (Suc t), j + 2 := nltape (take t (map literal_n (map (rename σ) (n_clause clause)))), j + 3 := (⌊clause ! t⌋⇩_{N}, 1)]" lemma tm1 [transforms_intros]: assumes "t < length clause" and "ttt = 12 + 2 * nlength (clause ! t)" shows "transforms tm1 (tpsL t) ttt (tps1 t)" unfolding tm1_def proof (tform tps: assms(1) tpsL_def tps1_def tps0 jk) show "ttt = 12 + 2 * nlength 0 + 2 * nlength (clause ! t)" using assms(2) by simp qed definition "tps2 t ≡ tps0 [j + 1 := nltape' clause (Suc t), j + 2 := nltape (take t (map literal_n (map (rename σ) (n_clause clause)))), j + 3 := (⌊clause ! t⌋⇩_{N}, 1), j + 4 := (⌊(clause ! t) mod 2⌋⇩_{N}, 1)]" lemma tm2 [transforms_intros]: assumes "t < length clause" and "ttt = 13 + 2 * nlength (clause ! t)" shows "transforms tm2 (tpsL t) ttt (tps2 t)" unfolding tm2_def by (tform tps: assms tps1_def tps2_def tps0 jk) definition "tps3 t ≡ tps0 [j + 1 := nltape' clause (Suc t), j + 2 := nltape (take t (map literal_n (map (rename σ) (n_clause clause)))), j + 3 := (⌊clause ! t div 2⌋⇩_{N}, 1), j + 4 := (⌊clause ! t mod 2⌋⇩_{N}, 1)]" lemma tm3 [transforms_intros]: assumes "t < length clause" and "ttt = 16 + 4 * nlength (clause ! t)" shows "transforms tm3 (tpsL t) ttt (tps3 t)" unfolding tm3_def by (tform tps: assms(1) tps2_def tps3_def jk time: assms(2)) definition "tps4 t ≡ tps0 [j + 1 := nltape' clause (Suc t), j + 2 := nltape (take t (map literal_n (map (rename σ) (n_clause clause)))), j + 3 := (⌊σ ! (clause ! t div 2)⌋⇩_{N}, 1), j + 4 := (⌊clause ! t mod 2⌋⇩_{N}, 1)]" lemma tm4 [transforms_intros]: assumes "t < length clause" and "ttt = 28 + 4 * nlength (clause ! t) + 18 * (nllength σ)⇧^{2}" shows "transforms tm4 (tpsL t) ttt (tps4 t)" unfolding tm4_def proof (tform tps: assms(1) tps0 tps3_def tps4_def jk clause time: assms(2)) show "tps4 t = (tps3 t)[j + 3 := (⌊σ ! (clause ! t div 2)⌋⇩_{N}, 1)]" unfolding tps4_def tps3_def by (simp add: list_update_swap[of "j + 3"]) qed definition "tps5 t ≡ tps0 [j + 1 := nltape' clause (Suc t), j + 2 := nltape (take t (map literal_n (map (rename σ) (n_clause clause)))), j + 3 := (⌊2 * (σ ! (clause ! t div 2)) + clause ! t mod 2⌋⇩_{N}, 1), j + 4 := (⌊clause ! t mod 2⌋⇩_{N}, 1)]" lemma tm5 [transforms_intros]: assumes "t < length clause" and "ttt = 41 + 4 * nlength (clause ! t) + 18 * (nllength σ)⇧^{2}+ 4 * nlength (σ ! (clause ! t div 2))" shows "transforms tm5 (tpsL t) ttt (tps5 t)" unfolding tm5_def by (tform tps: assms(1) tps0 tps4_def tps5_def jk time: assms(2)) definition "tps6 t ≡ tps0 [j + 1 := nltape' clause (Suc t), j + 2 := nltape (take (Suc t) (map literal_n (map (rename σ) (n_clause clause)))), j + 3 := (⌊2 * (σ ! (clause ! t div 2)) + clause ! t mod 2⌋⇩_{N}, 1), j + 4 := (⌊clause ! t mod 2⌋⇩_{N}, 1)]" lemma tm6: assumes "t < length clause" and "ttt = 47 + 4 * nlength (clause ! t) + 18 * (nllength σ)⇧^{2}+ 4 * nlength (σ ! (clause ! t div 2)) + 2 * nlength (2 * σ ! (clause ! t div 2) + clause ! t mod 2)" shows "transforms tm6 (tpsL t) ttt (tps6 t)" unfolding tm6_def proof (tform tps: assms(1) tps0 tps5_def tps6_def jk) have "2 * σ ! (clause ! t div 2) + clause ! t mod 2 = (literal_n ∘ rename σ) (n_literal (clause ! t))" using clause assms(1) literal_n_rename by simp then have "2 * σ ! (clause ! t div 2) + clause ! t mod 2 = (map (literal_n ∘ rename σ) (n_clause clause)) ! t" using assms(1) by (simp add: n_clause_def) then have "take t (map (literal_n ∘ rename σ) (n_clause clause)) @ [2 * σ ! (clause ! t div 2) + clause ! t mod 2] = take (Suc t) (map (literal_n ∘ rename σ) (n_clause clause))" by (simp add: assms(1) n_clause_def take_Suc_conv_app_nth) then show "tps6 t = (tps5 t) [j + 2 := nltape (take t (map (literal_n ∘ rename σ) (n_clause clause)) @ [2 * σ ! (clause ! t div 2) + clause ! t mod 2])]" unfolding tps5_def tps6_def by (simp only: list_update_overwrite list_update_swap_less[of "j + 2"]) simp show "ttt = 41 + 4 * nlength (clause ! t) + 18 * (nllength σ)⇧^{2}+ 4 * nlength (σ ! (clause ! t div 2)) + (7 + nllength (take t (map (literal_n ∘ rename σ) (n_clause clause))) - Suc (nllength (take t (map (literal_n ∘ rename σ) (n_clause clause)))) + 2 * nlength (2 * σ ! (clause ! t div 2) + clause ! t mod 2))" using assms(2) by simp qed lemma nlength_σ1: assumes "t < length clause" shows "nlength (clause ! t) ≤ nllength σ" proof - have "clause ! t div 2 < length σ" using clause assms(1) by simp then have "nlength (clause ! t div 2) < length σ" using nlength_le_n by (meson leD le_less_linear order.trans) then have "nlength (clause ! t) ≤ length σ" using canrepr_div_2 by simp then show "nlength (clause ! t) ≤ nllength σ" using length_le_nllength by (meson dual_order.trans mult_le_mono2) qed lemma nlength_σ2: assumes "t < length clause" shows "nlength (σ ! (clause ! t div 2)) ≤ nllength σ" using assms clause member_le_nllength nth_mem by simp lemma nlength_σ3: assumes "t < length clause" shows "nlength (2 * σ ! (clause ! t div 2) + clause ! t mod 2) ≤ Suc (nllength σ)" proof - have "nlength (2 * σ ! (clause ! t div 2) + clause ! t mod 2) ≤ nlength (2 * σ ! (clause ! t div 2) + 1)" using nlength_mono by simp also have "... ≤ Suc (nlength (σ ! (clause ! t div 2)))" using nlength_times2plus1 by (meson dual_order.trans) finally show ?thesis using nlength_σ2 assms by fastforce qed lemma tm6' [transforms_intros]: assumes "t < length clause" and "ttt = 49 + 28 * nllength σ ^ 2" shows "transforms tm6 (tpsL t) ttt (tps6 t)" proof - let ?ttt = "47 + 4 * nlength (clause ! t) + 18 * (nllength σ)⇧^{2}+ 4 * nlength (σ ! (clause ! t div 2)) + 2 * nlength (2 * σ ! (clause ! t div 2) + clause ! t mod 2)" have "?ttt ≤ 47 + 4 * nllength σ + 18 * (nllength σ)⇧^{2}+ 4 * nllength σ + 2 * Suc (nllength σ)" using nlength_σ1 nlength_σ3 nlength_σ2 assms(1) by fastforce also have "... = 49 + 10 * nllength σ + 18 * (nllength σ)⇧^{2}" by simp also have "... ≤ 49 + 10 * nllength σ ^ 2 + 18 * (nllength σ)⇧^{2}" using linear_le_pow by simp also have "... = 49 + 28 * nllength σ ^ 2" by simp finally have "?ttt ≤ 49 + 28 * nllength σ ^ 2" . then show ?thesis using tm6 assms transforms_monotone by blast qed definition "tps7 t ≡ tps0 [j + 1 := nltape' clause (Suc t), j + 2 := nltape (take (Suc t) (map literal_n (map (rename σ) (n_clause clause)))), j + 4 := (⌊clause ! t mod 2⌋⇩_{N}, 1)]" lemma tm7: assumes "t < length clause" and "ttt = 59 + 28 * nllength σ ^ 2 + 2 * nlength (2 * σ ! (clause ! t div 2) + clause ! t mod 2)" shows "transforms tm7 (tpsL t) ttt (tps7 t)" unfolding tm7_def proof (tform tps: assms(1) tps0 tps6_def tps7_def jk time: assms(2)) show "tps7 t = (tps6 t)[j + 3 := (⌊0⌋⇩_{N}, 1)]" using tps6_def tps7_def tps0 jk by (smt (z3) add_left_cancel list_update_id list_update_overwrite list_update_swap num.simps(8) numeral_eq_iff one_eq_numeral_iff semiring_norm(84)) qed lemma tm7' [transforms_intros]: assumes "t < length clause" and "ttt = 61 + 30 * nllength σ ^ 2" shows "transforms tm7 (tpsL t) ttt (tps7 t)" proof - let ?ttt = "59 + 28 * nllength σ ^ 2 + 2 * nlength (2 * σ ! (clause ! t div 2) + clause ! t mod 2)" have "?ttt ≤ 59 + 28 * nllength σ ^ 2 + 2 * Suc (nllength σ)" using nlength_σ3 assms(1) by fastforce also have "... = 61 + 28 * nllength σ ^ 2 + 2 * nllength σ" by simp also have "... ≤ 61 + 30 * nllength σ ^ 2" using linear_le_pow by simp finally have "?ttt ≤ 61 + 30 * nllength σ ^ 2" . then show ?thesis using assms tm7 transforms_monotone by blast qed definition "tps8 t ≡ tps0 [j + 1 := nltape' clause (Suc t), j + 2 := nltape (take (Suc t) (map literal_n (map (rename σ) (n_clause clause))))]" lemma tm8: assumes "t < length clause" and "ttt = 61 + 30 * (nllength σ)⇧^{2}+ (10 + 2 * nlength (clause ! t mod 2))" shows "transforms tm8 (tpsL t) ttt (tps8 t)" unfolding tm8_def proof (tform tps: assms(1) tps0 tps7_def tps8_def jk time: assms(2)) show "tps8 t = (tps7 t)[j + 4 := (⌊0⌋⇩_{N}, 1)]" using tps7_def tps8_def tps0 jk by (smt (z3) add_left_imp_eq list_update_id list_update_overwrite list_update_swap numeral_eq_iff numeral_eq_one_iff semiring_norm(85) semiring_norm(87)) qed lemma tm8' [transforms_intros]: assumes "t < length clause" and "ttt = 71 + 32 * (nllength σ)⇧^{2}" shows "transforms tm8 (tpsL t) ttt (tpsL (Suc t))" proof - have "nlength (clause ! t mod 2) ≤ nllength σ" using assms(1) nlength_σ1 by (meson mod_less_eq_dividend nlength_mono order.trans) then have "nlength (clause ! t mod 2) ≤ nllength σ ^ 2" using linear_le_pow by (metis nat_le_linear power2_nat_le_imp_le verit_la_disequality) then have "61 + 30 * (nllength σ)⇧^{2}+ (10 + 2 * nlength (clause ! t mod 2)) ≤ ttt" using assms(2) by simp then have "transforms tm8 (tpsL t) ttt (tps8 t)" using assms(1) tm8 transforms_monotone by blast moreover have "tps8 t = tpsL (Suc t)" using tps8_def tpsL_def by simp ultimately show ?thesis by simp qed lemma tmL [transforms_intros]: assumes "ttt = length clause * (73 + 32 * (nllength σ)⇧^{2}) + 1" shows "transforms tmL (tpsL 0) ttt (tpsL (length clause))" unfolding tmL_def proof (tform) let ?t = "71 + 32 * (nllength σ)⇧^{2}" show "read (tpsL t) ! (j + 1) ≠ □" if "t < length clause" for t proof - have "tpsL t ! (j + 1) = nltape' clause t" using tpsL_def jk by simp then show ?thesis using nltape'_tape_read that tapes_at_read' tpsL_def jk by (smt (z3) Suc_eq_plus1 leD length_list_update less_add_same_cancel1 less_trans_Suc zero_less_numeral) qed show "¬ read (tpsL (length clause)) ! (j + 1) ≠ □" proof - have "tpsL (length clause) ! (j + 1) = nltape' clause (length clause)" using tpsL_def jk by simp then show ?thesis using nltape'_tape_read tapes_at_read' tpsL_def jk by (smt (z3) Suc_eq_plus1 length_list_update less_add_same_cancel1 less_or_eq_imp_le less_trans_Suc zero_less_numeral) qed show "length clause * (71 + 32 * (nllength σ)⇧^{2}+ 2) + 1 ≤ ttt" using assms(1) by simp qed lemma tpsL_length: "tpsL (length clause) = tps0 [j + 1 := nltape' clause (length clause), j + 2 := nltape (map literal_n (map (rename σ) (n_clause clause)))]" using tpsL_def by (simp add: n_clause_def) definition "tps9 ≡ tps0 [j + 1 := nltape' clause (length clause), j + 2 := (⌊map literal_n (map (rename σ) (n_clause clause))⌋⇩_{N}⇩_{L}, 1)]" lemma tm9: assumes "ttt = 4 + length clause * (73 + 32 * (nllength σ)⇧^{2}) + nllength (map (literal_n ∘ rename σ) (n_clause clause))" shows "transforms tm9 (tpsL 0) ttt tps9" unfolding tm9_def proof (tform tps: tps0 tps9_def tpsL_def jk tpsL_length) show "clean_tape (tpsL (length clause) ! (j + 2))" using tpsL_def jk clean_tape_nlcontents tps0(3) by simp show "ttt = length clause * (73 + 32 * (nllength σ)⇧^{2}) + 1 + (tpsL (length clause) :#: (j + 2) + 2)" using n_clause_def assms jk tpsL_length by fastforce qed lemma tm9' [transforms_intros]: assumes "ttt = 4 + 2 * length clause * (73 + 32 * (nllength σ)⇧^{2})" shows "transforms tm9 tps0 ttt tps9" proof - let ?ttt = "4 + length clause * (73 + 32 * (nllength σ)⇧^{2}) + nllength (map (literal_n ∘ rename σ) (n_clause clause))" have "?ttt ≤ 4 + length clause * (73 + 32 * (nllength σ)⇧^{2}) + length clause * Suc (nllength σ)" using clause nllength_rename by simp also have "... ≤ 4 + length clause * (73 + 32 * (nllength σ)⇧^{2}) + length clause * (Suc (nllength σ ^ 2))" by (simp add: linear_le_pow) also have "... ≤ 4 + length clause * (73 + 32 * (nllength σ)⇧^{2}) + length clause * (73 + nllength σ ^ 2)" by (metis One_nat_def Suc_eq_plus1 Suc_leI add.commute add_left_mono mult_le_mono2 zero_less_numeral) also have "... ≤ 4 + length clause * (73 + 32 * (nllength σ)⇧^{2}) + length clause * (73 + 32 * nllength σ ^ 2)" by simp also have "... = 4 + 2 * length clause * (73 + 32 * (nllength σ)⇧^{2})" by simp finally have "?ttt ≤ 4 + 2 * length clause * (73 + 32 * (nllength σ)⇧^{2})" . then show ?thesis using tm9 assms transforms_monotone tpsL_eq_tps0 by fastforce qed definition "tps10 ≡ tps0 [j + 1 := (⌊[]⌋⇩_{N}⇩_{L}, 1), j + 2 := (⌊map literal_n (map (rename σ) (n_clause clause))⌋⇩_{N}⇩_{L}, 1)]" lemma tm10: assumes "ttt = 11 + 2 * length clause * (73 + 32 * (nllength σ)⇧^{2}) + 3 * nllength clause" shows "transforms tm10 tps0 ttt tps10" unfolding tm10_def proof (tform tps: tps0 tps9_def jk) show "tps9 ::: (j + 1) = ⌊numlist clause⌋" using tps9_def jk tps0(2) nlcontents_def by simp show "proper_symbols (numlist clause)" using proper_symbols_numlist by simp show "tps10 = tps9[j + 1 := (⌊[]⌋, 1)]" by (simp add: jk nlcontents_def tps0 tps10_def tps9_def list_update_swap numlist_Nil) show "ttt = 4 + 2 * length clause * (73 + 32 * (nllength σ)⇧^{2}) + (tps9 :#: (j + 1) + 2 * length (numlist clause) + 6)" using assms tps9_def jk nllength_def by simp qed lemma tm10': assumes "ttt = 11 + 64 * nllength clause * (3 + (nllength σ)⇧^{2})" shows "transforms tm10 tps0 ttt tps10" proof - let ?ttt = "11 + 2 * length clause * (73 + 32 * (nllength σ)⇧^{2}) + 3 * nllength clause" have "?ttt ≤ 11 + 2 * nllength clause * (73 + 32 * (nllength σ)⇧^{2}) + 3 * nllength clause" by (simp add: length_le_nllength) also have "... ≤ 11 + 2 * nllength clause * (73 + 32 * (nllength σ)⇧^{2}) + 2 * 2 * nllength clause" by simp also have "... = 11 + 2 * nllength clause * (75 + 32 * (nllength σ)⇧^{2})" by algebra also have "... ≤ 11 + 2 * nllength clause * (96 + 32 * (nllength σ)⇧^{2})" by simp also have "... = 11 + 2 * 32 * nllength clause * (3 + (nllength σ)⇧^{2})" by simp also have "... = 11 + 64 * nllength clause * (3 + (nllength σ)⇧^{2})" by simp finally have "?ttt ≤ 11 + 64 * nllength clause * (3 + (nllength σ)⇧^{2})" . then show ?thesis using tm10 assms transforms_monotone by blast qed end end (* locale turing_machine_relabel-clause *) lemma transforms_tm_relabel_clauseI [transforms_intros]: fixes j :: tapeidx fixes tps tps' :: "tape list" and ttt k :: nat and σ clause :: "nat list" assumes "0 < j" "j + 4 < k" "length tps = k" and "∀v∈set clause. v div 2 < length σ" assumes "tps ! j = (⌊σ⌋⇩_{N}⇩_{L}, 1)" "tps ! (j + 1) = (⌊clause⌋⇩_{N}⇩_{L}, 1)" "tps ! (j + 2) = (⌊[]⌋⇩_{N}⇩_{L}, 1)" "tps ! (j + 3) = (⌊0⌋⇩_{N}, 1)" "tps ! (j + 4) = (⌊0⌋⇩_{N}, 1)" assumes "ttt = 11 + 64 * nllength clause * (3 + (nllength σ)⇧^{2})" assumes "tps' = tps [j + 1 := (⌊[]⌋⇩_{N}⇩_{L}, 1), j + 2 := (⌊clause_n (map (rename σ) (n_clause clause))⌋⇩_{N}⇩_{L}, 1)]" shows "transforms (tm_relabel_clause j) tps ttt tps'" proof - interpret loc: turing_machine_relabel_clause j . show ?thesis using assms loc.tm10_eq_tm_relabel_clause loc.tps10_def loc.tm10' clause_n_def by simp qed subsection ‹Relabeling CNF formulas› text ‹ A Turing machine can relabel a CNF formula by relabeling each clause using the TM @{const tm_relabel_clause}. The next TM accepts a CNF formula as a list of lists of literals on tape $j_1$ and a substitution $\sigma$ as a list of numbers on tape $j_2 + 1$. It outputs the relabeled formula on tape $j_2$, which initially must be empty. › definition tm_relabel :: "tapeidx ⇒ tapeidx ⇒ machine" where "tm_relabel j1 j2 ≡ WHILE [] ; λrs. rs ! j1 ≠ □ DO tm_nextract ♯ j1 (j2 + 2) ;; tm_relabel_clause (j2 + 1) ;; tm_appendl j2 (j2 + 3) ;; tm_erase_cr (j2 + 3) DONE ;; tm_cr j1 ;; tm_cr j2" lemma tm_relabel_tm: assumes "G ≥ 6" and "j2 + 5 < k" and "0 < j1" and "j1 < j2" shows "turing_machine k G (tm_relabel j1 j2)" unfolding tm_relabel_def using assms tm_cr_tm tm_nextract_tm tm_appendl_tm tm_relabel_clause_tm Nil_tm tm_erase_cr_tm turing_machine_loop_turing_machine by simp locale turing_machine_relabel = fixes j1 j2 :: tapeidx begin definition "tmL1 ≡ tm_nextract ♯ j1 (j2 + 2)" definition "tmL2 ≡ tmL1 ;; tm_relabel_clause (j2 + 1)" definition "tmL3 ≡ tmL2 ;; tm_appendl j2 (j2 + 3)" definition "tmL4 ≡ tmL3 ;; tm_erase_cr (j2 + 3)" definition "tmL ≡ WHILE [] ; λrs. rs ! j1 ≠ □ DO tmL4 DONE" definition "tm2 ≡ tmL ;; tm_cr j1" definition "tm3 ≡ tm2 ;; tm_cr j2" lemma tm3_eq_tm_relabel: "tm3 = tm_relabel j1 j2" unfolding tm_relabel_def tm2_def tmL_def tmL4_def tmL3_def tmL2_def tmL1_def tm3_def by simp context fixes tps0 :: "tape list" and k :: nat and σ :: "nat list" and φ :: formula assumes variables: "variables φ ⊆ {..<length σ}" assumes jk: "0 < j1" "j1 < j2" "j2 + 5 < k" "length tps0 = k" assumes tps0: "tps0 ! j1 = (⌊formula_n φ⌋⇩_{N}⇩_{L}⇩_{L}, 1)" "tps0 ! j2 = (⌊[]⌋⇩_{N}⇩_{L}⇩_{L}, 1)" "tps0 ! (j2 + 1) = (⌊σ⌋⇩_{N}⇩_{L}, 1)" "tps0 ! (j2 + 2) = (⌊[]⌋⇩_{N}⇩_{L}, 1)" "tps0 ! (j2 + 3) = (⌊[]⌋⇩_{N}⇩_{L}, 1)" "tps0 ! (j2 + 4) = (⌊0⌋⇩_{N}, 1)" "tps0 ! (j2 + 5) = (⌊0⌋⇩_{N}, 1)" begin abbreviation nφ :: "nat list list" where "nφ ≡ formula_n φ" definition tpsL :: "nat ⇒ tape list" where "tpsL t ≡ tps0 [j1 := nlltape' nφ t, j2 := nlltape (formula_n (take t (relabel σ φ)))]" lemma tpsL_eq_tps0: "tpsL 0 = tps0" using tps0 tpsL_def formula_n_def nlllength_def numlist_Nil numlist_def numlistlist_def by (metis One_nat_def list.map(1) list.size(3) list_update_id take0) definition tpsL1 :: "nat ⇒ tape list" where "tpsL1 t ≡ tps0 [j1 := nlltape' nφ (Suc t), j2 := nlltape (formula_n (take t (relabel σ φ))), j2 + 2 := (⌊nφ ! t⌋⇩_{N}⇩_{L}, 1)]" lemma tmL1 [transforms_intros]: assumes "ttt = 12 + 2 * nllength (nφ ! t)" and "t < length φ" shows "transforms tmL1 (tpsL t) ttt (tpsL1 t)" unfolding tmL1_def proof (tform tps: tps0 tpsL_def tpsL1_def jk) show "t < length nφ" using assms(2) formula_n_def by simp show "tpsL1 t = (tpsL t) [j1 := nlltape' nφ (Suc t), j2 + 2 := (⌊nφ ! t⌋⇩_{N}⇩_{L}, 1)]" using tpsL1_def tpsL_def by (simp add: jk list_update_swap_less) show "ttt = 12 + 2 * nllength [] + 2 * nllength (nφ ! t)" using assms(1) by simp qed definition tpsL2 :: "nat ⇒ tape list" where "tpsL2 t ≡ tps0 [j1 := nlltape' nφ (Suc t), j2 := nlltape (formula_n (take t (relabel σ φ))), j2 + 2 := (⌊[]⌋⇩_{N}⇩_{L}, 1), j2 + 3 := (⌊clause_n (map (rename σ) (n_clause (nφ ! t)))⌋⇩_{N}⇩_{L}, 1)]" lemma tmL2 [transforms_intros]: assumes "ttt = 23 + 2 * nllength (nφ ! t) + 64 * nllength (nφ ! t) * (3 + (nllength σ)⇧^{2})" and "t < length φ" shows "transforms tmL2 (tpsL t) ttt (tpsL2 t)" unfolding tmL2_def proof (tform tps: assms(2) tps0 tpsL1_def jk) show "∀v∈set (nφ ! t). v div 2 < length σ" using variables_σ variables assms(2) by (metis formula_n_def nth_map nth_mem) have "tpsL1 t ! (j2 + (1 + 2)) = (⌊[]⌋⇩_{N}⇩_{L}, 1)" using tpsL1_def jk tps0 by (simp add: numeral_3_eq_3) then show "tpsL1 t ! (j2 + 1 + 2) = (⌊[]⌋⇩_{N}⇩_{L}, 1)" by (metis add.assoc) have "tpsL1 t ! (j2 + (1 + 3)) = (⌊0⌋⇩_{N}, 1)" using tpsL1_def jk tps0 by simp then show "tpsL1 t ! (j2 + 1 + 3) = (⌊0⌋⇩_{N}, 1)" by (metis add.assoc) have "tpsL1 t ! (j2 + (1 + 4)) = (⌊0⌋⇩_{N}, 1)" using tpsL1_def jk tps0 by simp then show "tpsL1 t ! (j2 + 1 + 4) = (⌊0⌋⇩_{N}, 1)" by (metis add.assoc) have "tpsL2 t = (tpsL1 t) [j2 + (1 + 1) := (⌊[]⌋⇩_{N}⇩_{L}, 1), j2 + (1 + 2) := (⌊clause_n (map (rename σ) (n_clause (nφ ! t)))⌋⇩_{N}⇩_{L}, 1)]" using jk tps0 tpsL1_def tpsL2_def by (simp add: numeral_3_eq_3) then show "tpsL2 t = (tpsL1 t) [j2 + 1 + 1 := (⌊[]⌋⇩_{N}⇩_{L}, 1), j2 + 1 + 2 := (⌊clause_n (map (rename σ) (n_clause (nφ ! t)))⌋⇩_{N}⇩_{L}, 1)]" by (metis add.assoc) show "ttt = 12 + 2 * nllength (nφ ! t) + (11 + 64 * nllength (nφ ! t) * (3 + (nllength σ)⇧^{2}))" using assms(1) by simp qed definition tpsL3 :: "nat ⇒ tape list" where "tpsL3 t ≡ tps0 [j1 := nlltape' nφ (Suc t), j2 := nlltape (formula_n (take t (relabel σ φ)) @ [clause_n (map (rename σ) (n_clause (nφ ! t)))]), j2 + 2 := (⌊[]⌋⇩_{N}⇩_{L}, 1), j2 + 3 := (⌊clause_n (map (rename σ) (n_clause (nφ ! t)))⌋⇩_{N}⇩_{L}, 1)]" lemma tmL3 [transforms_intros]: assumes "ttt = 29 + 2 * nllength (nφ ! t) + 64 * nllength (nφ ! t) * (3 + (nllength σ)⇧^{2}) + 2 * nllength (clause_n (map (rename σ) (n_clause (nφ ! t))))" and "t < length φ" shows "transforms tmL3 (tpsL t) ttt (tpsL3 t)" unfolding tmL3_def proof (tform tps: assms(2) tps0 tpsL2_def jk) show "tpsL3 t = (tpsL2 t) [j2 := nlltape (formula_n (take t (relabel σ φ)) @ [clause_n (map (rename σ) (n_clause (nφ ! t)))])]" unfolding tpsL3_def tpsL2_def by (simp add: list_update_swap_less[of j2]) show "ttt = 23 + 2 * nllength (nφ ! t) + 64 * nllength (nφ ! t) * (3 + (nllength σ)⇧^{2}) + (7 + nlllength (formula_n (take t (relabel σ φ))) - Suc (nlllength (formula_n (take t (relabel σ φ)))) + 2 * nllength (clause_n (map (rename σ) (n_clause (nφ ! t)))))" using assms(1) by simp qed definition tpsL4 :: "nat ⇒ tape list" where "tpsL4 t ≡ tps0 [j1 := nlltape' nφ (Suc t), j2 := nlltape (formula_n (take t (relabel σ φ)) @ [clause_n (map (rename σ) (n_clause (nφ ! t)))]), j2 + 2 := (⌊[]⌋⇩_{N}⇩_{L}, 1)]" lemma tmL4: assumes "ttt = 36 + 2 * nllength (nφ ! t) + 64 * nllength (nφ ! t) * (3 + (nllength σ)⇧^{2}) + 4 * nllength (clause_n (map (rename σ) (n_clause (nφ ! t))))" and "t < length φ" shows "transforms tmL4 (tpsL t) ttt (tpsL4 t)" unfolding tmL4_def proof (tform tps: assms(2) tps0 tpsL3_def jk) let ?zs = "numlist (clause_n (map (rename σ) (n_clause (nφ ! t))))" show "tpsL3 t ::: (j2 + 3) = ⌊?zs⌋" using tpsL3_def nlcontents_def jk by simp show "proper_symbols ?zs" using proper_symbols_numlist by simp have *: "j1 ≠ j2 + 3" using jk by simp have "⌊[]⌋ = ⌊[]⌋⇩_{N}⇩_{L}" using nlcontents_def numlist_Nil by simp then show "tpsL4 t = (tpsL3 t)[j2 + 3 := (⌊[]⌋, 1)]" using tpsL3_def tpsL4_def tps0 jk list_update_id[of tps0 "j2+3"] by (simp add: list_update_swap[OF *] list_update_swap[of _ "j2 + 3"]) show "ttt = 29 + 2 * nllength (nφ ! t) + 64 * nllength (nφ ! t) * (3 + (nllength σ)⇧^{2}) + 2 * nllength (clause_n (map (rename σ) (n_clause (nφ ! t)))) + (tpsL3 t :#: (j2 + 3) + 2 * length (numlist (clause_n (map (rename σ) (n_clause (nφ ! t))))) + 6)" using assms(1) tpsL3_def jk nllength_def by simp qed lemma nllength_1: assumes "t < length φ" shows "nllength (nφ ! t) ≤ nlllength nφ" using assms formula_n_def nlllength_take by (metis le_less_linear length_map less_trans not_add_less2) lemma nllength_2: assumes "t < length φ" shows "nllength (clause_n (map (rename σ) (n_clause (nφ ! t)))) ≤ nlllength (formula_n (relabel σ φ))" (is "?l ≤ ?r") proof - have "?l = nllength (clause_n (map (rename σ) (φ ! t)))" using assms by (simp add: formula_n_def n_clause_n) moreover have "clause_n (map (rename σ) (φ ! t)) ∈ set (formula_n (relabel σ φ))" using assms formula_n_def relabel_def by simp ultimately show ?thesis using member_le_nlllength_1 by fastforce qed definition "tpsL4' t ≡ tps0 [j1 := nlltape' nφ (Suc t), j2 := nlltape (formula_n (take (Suc t) (relabel σ φ)))]" lemma tpsL4: assumes "t < length φ" shows "tpsL4 t = tpsL4' t" proof - have "formula_n (take t (relabel σ φ)) @ [clause_n (map (rename σ) (n_clause (nφ ! t)))] = formula_n (take (Suc t) (relabel σ φ))" using assms formula_n_def relabel_def by (simp add: n_clause_n take_Suc_conv_app_nth) then show ?thesis using tpsL4_def tpsL4'_def jk tps0 by (smt (verit, del_insts) Suc_1 add_Suc_right add_cancel_left_right less_SucI list_update_id list_update_swap not_less_eq numeral_1_eq_Suc_0 numeral_One) qed lemma tpsL4'_eq_tpsL: "tpsL4' t = tpsL (Suc t)" using tpsL_def tpsL4'_def by simp lemma tmL4' [transforms_intros]: assumes "ttt = 36 + 65 * nlllength nφ * (3 + (nllength σ)⇧^{2}) + 4 * nlllength (formula_n (relabel σ φ))" and "t < length φ" shows "transforms tmL4 (tpsL t) ttt (tpsL (Suc t))" proof - let ?ttt = "36 + 2 * nllength (nφ ! t) + 64 * nllength (nφ ! t) * (3 + (nllength σ)⇧^{2}) + 4 * nllength (clause_n (map (rename σ) (n_clause (nφ ! t))))" have "?ttt ≤ 36 + 2 * nlllength nφ + 64 * nlllength nφ * (3 + (nllength σ)⇧^{2}) + 4 * nllength (clause_n (map (rename σ) (n_clause (nφ ! t))))" using nllength_1 assms(2) add_le_mono add_le_mono1 mult_le_mono1 mult_le_mono2 nat_add_left_cancel_le by metis also have "... ≤ 36 + 2 * nlllength nφ + 64 * nlllength nφ * (3 + (nllength σ)⇧^{2}) + 4 * nlllength (formula_n (relabel σ φ))" using nllength_2 assms(2) by simp also have "... ≤ 36 + 65 * nlllength nφ * (3 + (nllength σ)⇧^{2}) + 4 * nlllength (formula_n (relabel σ φ))" by simp finally have "?ttt ≤ 36 + 65 * nlllength nφ * (3 + (nllength σ)⇧^{2}) + 4 * nlllength (formula_n (relabel σ φ))" . then have "transforms tmL4 (tpsL t) ttt (tpsL4 t)" using assms tmL4 transforms_monotone by blast then show ?thesis using assms(2) tpsL4'_eq_tpsL tpsL4 by simp qed lemma tmL: assumes "ttt = length φ * (38 + 65 * nlllength nφ * (3 + (nllength σ)⇧^{2}) + 4 * nlllength (formula_n (relabel σ φ))) + 1" shows "transforms tmL (tpsL 0) ttt (tpsL (length φ))" unfolding tmL_def proof (tform) let ?t = "36 + 65 * nlllength nφ * (3 + (nllength σ)⇧^{2}) + 4 * nlllength (formula_n (relabel σ φ))" show "¬ read (tpsL (length φ)) ! j1 ≠ □" proof - have "tpsL (length φ) ! j1 = nlltape' nφ (length nφ)" using tpsL_def jk formula_n_def by simp then show ?thesis using nlltape'_tape_read[of nφ "length nφ"] tapes_at_read'[of j1 "tpsL (length φ)"] tpsL_def jk by simp qed show "read (tpsL t) ! j1 ≠ □" if "t < length φ" for t proof - have "tpsL t ! j1 = nlltape' nφ t" using tpsL_def jk by simp then show ?thesis using that formula_n_def nlltape'_tape_read[of nφ t] tapes_at_read'[of j1 "tpsL t"] tpsL_def jk by simp qed show "length φ * (?t + 2) + 1 ≤ ttt" using assms(1) by simp qed lemma tmL' [transforms_intros]: assumes "ttt = 107 * nlllength nφ ^ 2 * (3 + nllength σ ^ 2) + 1" shows "transforms tmL (tpsL 0) ttt (tpsL (length φ))" proof - let ?ttt = "length φ * (38 + 65 * nlllength nφ * (3 + (nllength σ)⇧^{2}) + 4 * nlllength (formula_n (relabel σ φ))) + 1" have "?ttt ≤ length φ * (38 + 65 * nlllength nφ * (3 + (nllength σ)⇧^{2}) + 4 * (Suc (nllength σ) * nlllength nφ)) + 1" using nlllength_relabel_variables variables by fastforce also have "... ≤ length φ * (38 + 65 * nlllength nφ * (3 + (nllength σ)⇧^{2}) + 4 * ((3 + nllength σ) * nlllength nφ)) + 1" proof - have "Suc (nllength σ) ≤ 3 + nllength σ" by simp then show ?thesis using add_le_mono le_refl mult_le_mono by presburger qed also have "... ≤ length φ * (38 + 65 * nlllength nφ * (3 + (nllength σ)⇧^{2}) + 4 * ((3 + nllength σ ^ 2) * nlllength nφ)) + 1" using linear_le_pow by simp also have "... = length φ * (38 + 69 * nlllength nφ * (3 + (nllength σ)⇧^{2})) + 1" by simp also have "... ≤ nlllength nφ * (38 + 69 * nlllength nφ * (3 + (nllength σ)⇧^{2})) + 1" using length_le_nlllength formula_n_def by (metis add_mono_thms_linordered_semiring(3) length_map mult_le_mono1) also have "... = 38 * nlllength nφ + (69 * nlllength nφ ^ 2 * (3 + (nllength σ)⇧^{2})) + 1" by algebra also have "... ≤ 38 * nlllength nφ ^ 2 * (3 + nllength σ ^ 2) + (69 * nlllength nφ ^ 2 * (3 + (nllength σ)⇧^{2})) + 1" proof - have "nlllength nφ ≤ nlllength nφ ^ 2 * (3 + nllength σ ^ 2)" using linear_le_pow by (metis One_nat_def Suc_leI add_gr_0 mult_le_mono nat_mult_1_right zero_less_numeral) then show ?thesis by simp qed also have "... = 107 * nlllength nφ ^ 2 * (3 + nllength σ ^ 2) + 1" by simp finally have "?ttt ≤ 107 * nlllength nφ ^ 2 * (3 + nllength σ ^ 2) + 1" . then show ?thesis using tmL assms transforms_monotone by blast qed definition tps1 :: "tape list" where "tps1 ≡ tps0 [j1 := nlltape' nφ (length φ), j2 := nlltape (formula_n (relabel σ φ))]" lemma tps1_eq_tpsL: "tps1 = tpsL (length φ)" using tps1_def tpsL_def jk tps0 relabel_def by simp definition "tps2 ≡ tps0 [j2 := nlltape (formula_n (relabel σ φ))]" lemma tm2 [transforms_intros]: assumes "ttt = Suc (107 * (nlllength nφ)⇧^{2}* (3 + (nllength σ)⇧^{2})) + Suc (Suc (Suc (nlllength nφ)))" shows "transforms tm2 (tpsL 0) ttt tps2" unfolding tm2_def proof (tform tps: tps0 tpsL_def tps1_def jk) have *: "tpsL (length φ) ! j1 = nlltape' nφ (length φ)" using tpsL_def jk by simp then show "clean_tape (tpsL (length φ) ! j1)" using clean_tape_nllcontents by simp have "tpsL (length φ) ! j1 |#=| 1 = nlltape' nφ 0" using * by simp then show "tps2 = (tpsL (length φ))[j1 := tpsL (length φ) ! j1 |#=| 1]" using tps0 jk tps2_def tps1_eq_tpsL tps1_def by (metis (no_types, lifting) One_nat_def list_update_id list_update_overwrite list_update_swap_less nlllength_Nil take0) show "ttt = 107 * (nlllength nφ)⇧^{2}* (3 + (nllength σ)⇧^{2}) + 1 + (tpsL (length φ) :#: j1 + 2)" using assms tpsL_def jk formula_n_def by simp qed definition "tps3 ≡ tps0 [j2 := nlltape' (formula_n (relabel σ φ)) 0]" lemma tm3: assumes "ttt = 7 + (107 * (nlllength nφ)⇧^{2}* (3 + (nllength σ)⇧^{2})) + nlllength nφ + nlllength (formula_n (relabel σ φ))" shows "transforms tm3 (tpsL 0) ttt tps3" unfolding tm3_def proof (tform tps: assms tps0 tps2_def tps3_def jk) show "clean_tape (tps2 ! j2)" using tps2_def jk clean_tape_nllcontents by simp qed lemma tm3' [transforms_intros]: assumes "ttt = 7 + (108 * (nlllength nφ)⇧^{2}* (3 + (nllength σ)⇧^{2}))" shows "transforms tm3 tps0 ttt tps3" proof - let ?ttt = "7 + (107 * (nlllength nφ)⇧^{2}* (3 + (nllength σ)⇧^{2})) + nlllength nφ + nlllength (formula_n (relabel σ φ))" have "?ttt ≤ 7 + (107 * (nlllength nφ)⇧^{2}* (3 + (nllength σ)⇧^{2})) + nlllength nφ + Suc (nllength σ) * nlllength nφ" using variables nlllength_relabel_variables by simp also have "... = 7 + (107 * (nlllength nφ)⇧^{2}* (3 + (nllength σ)⇧^{2})) + (2 + nllength σ) * nlllength nφ" by simp also have "... ≤ 7 + (107 * (nlllength nφ)⇧^{2}* (3 + (nllength σ)⇧^{2})) + (2 + nllength σ ^ 2) * nlllength nφ" using linear_le_pow by simp also have "... ≤ 7 + (107 * (nlllength nφ)⇧^{2}* (3 + (nllength σ)⇧^{2})) + (3 + nllength σ ^ 2) * nlllength nφ" by (metis add_2_eq_Suc add_Suc_shift add_mono_thms_linordered_semiring(2) le_add2 mult.commute mult_le_mono2 numeral_3_eq_3) also have "... ≤ 7 + (107 * (nlllength nφ)⇧^{2}* (3 + (nllength σ)⇧^{2})) + (3 + nllength σ ^ 2) * nlllength nφ ^ 2" using linear_le_pow by simp also have "... = 7 + (108 * (nlllength nφ)⇧^{2}* (3 + (nllength σ)⇧^{2}))" by simp finally have "?ttt ≤ 7 + (108 * (nlllength nφ)⇧^{2}* (3 + (nllength σ)⇧^{2}))" . then show ?thesis using tm3 assms tpsL_eq_tps0 transforms_monotone by simp qed end (* context tps0 *) end (* locale turing_machine_relabel *) lemma transforms_tm_relabelI [transforms_intros]: fixes j1 j2 :: tapeidx fixes tps tps' :: "tape list" and ttt k :: nat and σ :: "nat list" and φ :: formula assumes "0 < j1" and "j1 < j2" and "j2 + 5 < k" and "length tps = k" and "variables φ ⊆ {..<length σ}" assumes "tps ! j1 = (⌊formula_n φ⌋⇩_{N}⇩_{L}⇩_{L}, 1)" "tps ! j2 = (⌊[]⌋⇩_{N}⇩_{L}⇩_{L}, 1)" "tps ! (j2 + 1) = (⌊σ⌋⇩_{N}⇩_{L}, 1)" "tps ! (j2 + 2) = (⌊[]⌋⇩_{N}⇩_{L}, 1)" "tps ! (j2 + 3) = (⌊[]⌋⇩_{N}⇩_{L}, 1)" "tps ! (j2 + 4) = (⌊0⌋⇩_{N}, 1)" "tps ! (j2 + 5) = (⌊0⌋⇩_{N}, 1)" assumes "tps' = tps [j2 := nlltape' (formula_n (relabel σ φ)) 0]" assumes "ttt = 7 + (108 * (nlllength (formula_n φ))⇧^{2}* (3 + (nllength σ)⇧^{2}))" shows "transforms (tm_relabel j1 j2) tps ttt tps'" proof - interpret loc: turing_machine_relabel j1 j2 . show ?thesis using assms loc.tm3_eq_tm_relabel loc.tm3' loc.tps3_def by simp qed section ‹Listing the head positions of a Turing machine› text ‹ The formulas $\chi_t$ used for $\Phi_9$ require the functions $\inputpos$ and $\prev$, or more precisely the substitutions $\rho_t$ and $\rho'_t$ do. In this section we build a TM that simulates a two-tape TM $M$ on some input until it halts. During the simulation it creates two lists: one with the sequence of head positions on $M$'s input tape and one with the sequence of head positions on $M$'s output tape. The first list directly provides $\inputpos$; the second list allows the computation of $\prev$ using the TM @{const tm_prev}. › subsection ‹Simulating and logging head movements› text ‹ At the core of the simulation is the following Turing command. It interprets the tapes $j + 7$ and $j + 8$ as input tape and output tape of a two-tape Turing machine $M$ and the symbol in the first cell of tape $j + 6$ as the state of $M$. It then applies the actions of $M$ in this configuration to the tapes $j + 7$ and $j + 8$ and adapts the state on tape $j + 6$ accordingly. On top of that it writes (``logs'') to tape $j$ the direction in which $M$'s input tape head has moved and to tape $j + 3$ the direction in which $M$'s work tape head has moved. The head movement directions are encoded by the symbols $\Box$, $\triangleright$, and \textbf{0} for Left, Stay, and Right, respectively. The command is parameterized by the TM $M$ and its alphabet size $G$ (and as usual the tape index $j$). The command does nothing if the state on tape $j + 6$ is the halting state or if the symbol read from the simulated tape $j + 7$ or $j + 8$ is outside the alphabet $G$. \null › definition direction_to_symbol :: "direction ⇒ symbol" where "direction_to_symbol d ≡ (case d of Left ⇒ □ | Stay ⇒ ▹ | Right ⇒ 𝟬)" lemma direction_to_symbol_less: "direction_to_symbol d < 3" using direction_to_symbol_def by (cases d) simp_all definition cmd_simulog :: "nat ⇒ machine ⇒ tapeidx ⇒ command" where "cmd_simulog G M j rs ≡ (1, if rs ! (j + 6) ≥ length M ∨ rs ! (j + 7) ≥ G ∨ rs ! (j + 8) ≥ G then map (λz. (z, Stay)) rs else map (λi. let sas = (M ! (rs ! (j + 6))) [rs ! (j + 7), rs ! (j + 8)] in if i = j then (direction_to_symbol (sas [~] 0), Stay) else if i = j + 3 then (direction_to_symbol (sas [~] 1), Stay) else if i = j + 6 then (fst sas, Stay) else if i = j + 7 then sas [!] 0 else if i = j + 8 then sas [!] 1 else (rs ! i, Stay)) [0..<length rs])" lemma turing_command_cmd_simulog: fixes G H :: nat assumes "turing_machine 2 G M" and "k ≥ j + 9" and "j > 0" and "H ≥ Suc (length M)" and "H ≥ G" shows "turing_command k 1 H (cmd_simulog G M j)" proof show "⋀gs. length gs = k ⟹ length ([!!] cmd_simulog G M j gs) = length gs" using cmd_simulog_def by simp have G: "H ≥ 4" using assms(1,5) turing_machine_def by simp show "cmd_simulog G M j rs [.] i < H" if "length rs = k" and "(⋀i. i < length rs ⟹ rs ! i < H)" and "i < length rs" for rs i proof (cases "rs ! (j + 6) ≥ length M ∨ rs ! (j + 7) ≥ G ∨ rs ! (j + 8) ≥ G") case True then show ?thesis using assms that cmd_simulog_def by simp next case False then have inbounds: "rs ! (j + 6) < length M" by simp let ?cmd = "M ! (rs ! (j + 6))" let ?gs = "[rs ! (j + 7), rs ! (j + 8)]" let ?sas = "?cmd ?gs" have lensas: "length (snd ?sas) = 2" using assms(1) inbounds turing_commandD(1) by (metis length_Cons list.size(3) numeral_2_eq_2 turing_machineD(3)) consider "i = j" | "i = j + 3" | "i = j + 6" | "i = j + 7" | "i = j + 8" | "i ≠ j ∧ i ≠ j + 3 ∧ i ≠ j + 6 ∧ i ≠ j + 7 ∧ i ≠ j + 8" by linarith then show ?thesis proof (cases) case 1 then have "cmd_simulog G M j rs [!] i = (direction_to_symbol (?sas [~] 0), Stay)" using cmd_simulog_def False that by simp then have "cmd_simulog G M j rs [.] i < 3" using direction_to_symbol_less by simp then show ?thesis using G by simp next case 2 then have "cmd_simulog G M j rs [!] i = (direction_to_symbol (?sas [~] 1), Stay)" using cmd_simulog_def False that by simp then have "cmd_simulog G M j rs [.] i < 3" using direction_to_symbol_less by simp then show ?thesis using G by simp next case 3 then have "cmd_simulog G M j rs [!] i = (fst ?sas, Stay)" using cmd_simulog_def False that by simp then have "cmd_simulog G M j rs [.] i ≤ length M" using assms inbounds turing_commandD(4) turing_machineD(3) by (metis One_nat_def Suc_1 fst_conv length_Cons list.size(3)) then show ?thesis using assms(4) by simp next case 4 then have "cmd_simulog G M j rs [!] i = ?sas [!] 0" using cmd_simulog_def False that by simp then show ?thesis using 4 assms inbounds turing_machine_def that lensas turing_commandD(3) by (metis One_nat_def Suc_1 length_Cons list.size(3) nth_Cons_0 nth_mem zero_less_numeral) next case 5 then have *: "cmd_simulog G M j rs [!] i = ?sas [!] 1" using cmd_simulog_def False that by simp have "turing_command 2 (length M) G ?cmd" using assms(1) inbounds turing_machine_def by simp moreover have "symbols_lt G ?gs" using False less_2_cases_iff numeral_2_eq_2 by simp ultimately have "?sas [.] 1 < G" using turing_commandD(2) by simp then show ?thesis using assms * by simp next case 6 then have "cmd_simulog G M j rs [!] i = (rs ! i, Stay)" using cmd_simulog_def False that(3) by simp then show ?thesis using that by simp qed qed show "cmd_simulog G M j rs [.] 0 = rs ! 0" if "length rs = k" and "0 < k" for rs proof (cases "rs ! (j + 6) ≥ length M ∨ rs ! (j + 7) ≥ G ∨ rs ! (j + 8) ≥ G") case True then show ?thesis using assms that cmd_simulog_def by simp next case False then show ?thesis using assms that cmd_simulog_def by simp qed show "⋀gs. length gs = k ⟹ [*] (cmd_simulog G M j gs) ≤ 1" using cmd_simulog_def by simp qed text ‹ The logging Turing machine consists only of the logging command. › definition tm_simulog :: "nat ⇒ machine ⇒ tapeidx ⇒ machine" where "tm_simulog G M j ≡ [cmd_simulog G M j]" lemma tm_simulog_tm: fixes H :: nat assumes "turing_machine 2 G M" and "k ≥ j + 9" and "j > 0" and "H