section ‹Symbol sequence operations› theory Symbol_Ops imports Two_Four_Symbols begin text ‹ While previous sections have focused on ``formatted'' symbol sequences for numbers and lists, in this section we devise some Turing machines dealing with ``unstructured'' arbitrary symbol sequences. The only ``structure'' that is often imposed is that of not containing a blank symbol because when reading a symbol sequence, say from the input tape, a blank would signal the end of the symbol sequence. › subsection ‹Checking for being over an alphabet› text ‹ In this section we devise a Turing machine that checks if a proper symbol sequence is over a given alphabet represented by an upper bound symbol $z$. › abbreviation proper_symbols_lt :: "symbol ⇒ symbol list ⇒ bool" where "proper_symbols_lt z zs ≡ proper_symbols zs ∧ symbols_lt z zs" text ‹ The next Turing machine checks if the symbol sequence (up until the first blank) on tape $j_1$ contains only symbols from $\{2, \dots, z - 1\}$, where $z$ is a parameter of the TM, and writes to tape $j_2$ the number~1 or~0, representing True or False, respectively. It assumes that $j_2$ initially contains at most one symbol. › definition tm_proper_symbols_lt :: "tapeidx ⇒ tapeidx ⇒ symbol ⇒ machine" where "tm_proper_symbols_lt j1 j2 z ≡ tm_write j2 𝟭 ;; WHILE [] ; λrs. rs ! j1 ≠ □ DO IF λrs. rs ! j1 < 2 ∨ rs ! j1 ≥ z THEN tm_write j2 □ ELSE [] ENDIF ;; tm_right j1 DONE ;; tm_cr j1" lemma tm_proper_symbols_lt_tm: assumes "0 < j2" "j1 < k" "j2 < k" and "G ≥ 4" shows "turing_machine k G (tm_proper_symbols_lt j1 j2 z)" using assms tm_write_tm tm_right_tm tm_cr_tm Nil_tm tm_proper_symbols_lt_def turing_machine_loop_turing_machine turing_machine_branch_turing_machine by simp locale turing_machine_proper_symbols_lt = fixes j1 j2 :: tapeidx and z :: symbol begin definition "tm1 ≡ tm_write j2 𝟭" definition "tm2 ≡ IF λrs. rs ! j1 < 2 ∨ rs ! j1 ≥ z THEN tm_write j2 □ ELSE [] ENDIF" definition "tm3 ≡ tm2 ;; tm_right j1" definition "tm4 ≡ WHILE [] ; λrs. rs ! j1 ≠ □ DO tm3 DONE" definition "tm5 ≡ tm1 ;; tm4" definition "tm6 ≡ tm5 ;; tm_cr j1" lemma tm6_eq_tm_proper_symbols_lt: "tm6 = tm_proper_symbols_lt j1 j2 z" unfolding tm6_def tm5_def tm4_def tm3_def tm2_def tm1_def tm_proper_symbols_lt_def by simp context fixes zs :: "symbol list" and tps0 :: "tape list" and k :: nat assumes jk: "k = length tps0" "j1 ≠ j2" "j1 < k" "j2 < k" and zs: "proper_symbols zs" and tps0: "tps0 ! j1 = (⌊zs⌋, 1)" "tps0 ! j2 = (⌊[]⌋, 1)" begin definition "tps1 t ≡ tps0 [j1 := (⌊zs⌋, Suc t), j2 := (if proper_symbols_lt z (take t zs) then ⌊[𝟭]⌋ else ⌊[]⌋, 1)]" lemma tm1 [transforms_intros]: "transforms tm1 tps0 1 (tps1 0)" unfolding tm1_def proof (tform tps: jk tps0) have "(if proper_symbols_lt z (take 0 zs) then ⌊[𝟭]⌋ else ⌊[]⌋, 1) = (⌊[𝟭]⌋, 1)" by simp moreover have "tps0 ! j2 |:=| 𝟭 = (⌊[𝟭]⌋, 1)" using tps0(2) contents_def by auto moreover have "tps0[j1 := (⌊zs⌋, Suc 0)] = tps0" using tps0(1) by (metis One_nat_def list_update_id) ultimately show "tps1 0 = tps0[j2 := tps0 ! j2 |:=| 𝟭]" unfolding tps1_def by auto qed definition "tps2 t ≡ tps0 [j1 := (⌊zs⌋, Suc t), j2 := (if proper_symbols_lt z (take (Suc t) zs) then ⌊[𝟭]⌋ else ⌊[]⌋, 1)]" lemma tm2 [transforms_intros]: assumes "t < length zs" shows "transforms tm2 (tps1 t) 3 (tps2 t)" unfolding tm2_def proof (tform tps: jk tps1_def) have "tps1 t ! j1 = (⌊zs⌋, Suc t)" using tps1_def jk by simp moreover have "read (tps1 t) ! j1 = tps1 t :.: j1" using tapes_at_read' jk tps1_def by (metis (no_types, lifting) length_list_update) ultimately have *: "read (tps1 t) ! j1 = zs ! t" using contents_inbounds assms(1) by simp have j2: "tps1 t ! j2 = (if proper_symbols_lt z (take t zs) then ⌊[𝟭]⌋ else ⌊[]⌋, 1)" using tps1_def jk by simp show "tps2 t = (tps1 t)[j2 := tps1 t ! j2 |:=| □]" if "read (tps1 t) ! j1 < 2 ∨ z ≤ read (tps1 t) ! j1" proof - have c3: "(⌊[𝟭]⌋, 1) |:=| □ = (⌊[]⌋, 1)" using contents_def by auto have "(if proper_symbols_lt z (take t zs) then ⌊[𝟭]⌋ else ⌊[]⌋, 1) |:=| □ = (if proper_symbols_lt z (take (Suc t) zs) then ⌊[𝟭]⌋ else ⌊[]⌋, 1)" proof (cases "proper_symbols_lt z (take t zs)") case True have "zs ! t < 2 ∨ z ≤ zs ! t" using that * by simp then have "¬ proper_symbols_lt z (take (Suc t) zs)" using assms(1) by auto then show ?thesis using c3 by auto next case False then have "¬ proper_symbols_lt z (take (Suc t) zs)" by auto then show ?thesis using c3 False by auto qed then have "tps1 t ! j2 |:=| □ = (if proper_symbols_lt z (take (Suc t) zs) then ⌊[𝟭]⌋ else ⌊[]⌋, 1)" using j2 by simp then show "tps2 t = (tps1 t)[j2 := tps1 t ! j2 |:=| □]" unfolding tps2_def tps1_def using c3 jk(1,4) by simp qed show "tps2 t = tps1 t" if "¬ (read (tps1 t) ! j1 < 2 ∨ z ≤ read (tps1 t) ! j1)" proof - have 1: "zs ! t ≥ 2 ∧ z > zs ! t" using that * by simp show "tps2 t = tps1 t" proof (cases "proper_symbols_lt z (take t zs)") case True have "proper_symbols_lt z (take (Suc t) zs)" using True 1 assms(1) zs by (metis length_take less_antisym min_less_iff_conj nth_take) then show ?thesis using tps1_def tps2_def jk by simp next case False then have "¬ proper_symbols_lt z (take (Suc t) zs)" by auto then show ?thesis using tps1_def tps2_def jk False by auto qed qed qed lemma tm3 [transforms_intros]: assumes "t < length zs" shows "transforms tm3 (tps1 t) 4 (tps1 (Suc t))" unfolding tm3_def proof (tform tps: assms jk tps2_def) have "tps2 t ! j1 |+| 1 = (⌊zs⌋, Suc (Suc t))" using tps2_def jk by simp then show "tps1 (Suc t) = (tps2 t)[j1 := tps2 t ! j1 |+| 1]" unfolding tps1_def tps2_def by (metis (no_types, lifting) jk(2) list_update_overwrite list_update_swap) qed lemma tm4 [transforms_intros]: assumes "ttt = 1 + 6 * length zs" shows "transforms tm4 (tps1 0) ttt (tps1 (length zs))" unfolding tm4_def proof (tform time: assms) show "read (tps1 t) ! j1 ≠ □" if "t < length zs" for t proof - have "tps1 t ! j1 = (⌊zs⌋, Suc t)" using tps1_def jk by simp moreover have "read (tps1 t) ! j1 = tps1 t :.: j1" using tapes_at_read' jk tps1_def by (metis (no_types, lifting) length_list_update) ultimately have "read (tps1 t) ! j1 = zs ! t" using contents_inbounds that by simp then show ?thesis using zs that by auto qed show "¬ read (tps1 (length zs)) ! j1 ≠ □" proof - have "tps1 (length zs) ! j1 = (⌊zs⌋, Suc (length zs))" using tps1_def jk by simp moreover have "read (tps1 (length zs)) ! j1 = tps1 (length zs) :.: j1" using tapes_at_read' jk tps1_def by (metis (no_types, lifting) length_list_update) ultimately show ?thesis by simp qed qed lemma tm5 [transforms_intros]: assumes "ttt = 2 + 6 * length zs" shows "transforms tm5 tps0 ttt (tps1 (length zs))" unfolding tm5_def by (tform time: assms) definition "tps5 ≡ tps0 [j1 := (⌊zs⌋, 1), j2 := (if proper_symbols_lt z zs then ⌊[𝟭]⌋ else ⌊[]⌋, 1)]" definition "tps5' ≡ tps0 [j2 := (if proper_symbols_lt z zs then ⌊[𝟭]⌋ else ⌊[]⌋, 1)]" lemma tm6: assumes "ttt = 5 + 7 * length zs" shows "transforms tm6 tps0 ttt tps5'" unfolding tm6_def proof (tform time: assms tps1_def jk) have *: "tps1 (length zs) ! j1 = (⌊zs⌋, Suc (length zs))" using tps1_def jk by simp show "clean_tape (tps1 (length zs) ! j1)" using * zs by simp have "tps5 = (tps1 (length zs))[j1 := (⌊zs⌋, Suc (length zs)) |#=| 1]" unfolding tps5_def tps1_def by (simp add: list_update_swap[OF jk(2)]) then have "tps5 = (tps1 (length zs))[j1 := tps1 (length zs) ! j1 |#=| 1]" using * by simp moreover have "tps5' = tps5" using tps5'_def tps5_def tps0 jk by (metis list_update_id) ultimately show "tps5' = (tps1 (length zs))[j1 := tps1 (length zs) ! j1 |#=| 1]" by simp qed definition "tps6 ≡ tps0 [j2 := (⌊proper_symbols_lt z zs⌋⇩_{B}, 1)]" lemma tm6': assumes "ttt = 5 + 7 * length zs" shows "transforms tm6 tps0 ttt tps6" proof - have "tps6 = tps5'" using tps6_def tps5'_def canrepr_0 canrepr_1 by auto then show ?thesis using tm6 assms by simp qed end end (* locale *) lemma transforms_tm_proper_symbols_ltI [transforms_intros]: fixes j1 j2 :: tapeidx and z :: symbol fixes zs :: "symbol list" and tps tps' :: "tape list" and k :: nat assumes "k = length tps" "j1 ≠ j2" "j1 < k" "j2 < k" and "proper_symbols zs" assumes "tps ! j1 = (⌊zs⌋, 1)" "tps ! j2 = (⌊[]⌋, 1)" assumes "ttt = 5 + 7 * length zs" assumes "tps' = tps [j2 := (⌊proper_symbols_lt z zs⌋⇩_{B}, 1)]" shows "transforms (tm_proper_symbols_lt j1 j2 z) tps ttt tps'" proof - interpret loc: turing_machine_proper_symbols_lt j1 j2 . show ?thesis using assms loc.tm6_eq_tm_proper_symbols_lt loc.tps6_def loc.tm6' by simp qed subsection ‹The length of the input› text ‹ The Turing machine in this section reads the input tape until the first blank and increments a counter on tape $j$ for every symbol read. In the end it performs a carriage return on the input tape, and tape $j$ contains the length of the input as binary number. For this to work, tape $j$ must initially be empty. › lemma proper_tape_read: assumes "proper_symbols zs" shows "|.| (⌊zs⌋, i) = □ ⟷ i > length zs" proof - have "|.| (⌊zs⌋, i) = □" if "i > length zs" for i using that contents_outofbounds by simp moreover have "|.| (⌊zs⌋, i) ≠ □" if "i ≤ length zs" for i using that contents_inbounds assms contents_def proper_symbols_ne0 by simp ultimately show ?thesis by (meson le_less_linear) qed definition tm_length_input :: "tapeidx ⇒ machine" where "tm_length_input j ≡ WHILE [] ; λrs. rs ! 0 ≠ □ DO tm_incr j ;; tm_right 0 DONE ;; tm_cr 0" lemma tm_length_input_tm: assumes "G ≥ 4" and "0 < j" and "j < k" shows "turing_machine k G (tm_length_input j)" using tm_length_input_def tm_incr_tm assms Nil_tm tm_right_tm tm_cr_tm by (simp add: turing_machine_loop_turing_machine) locale turing_machine_length_input = fixes j :: tapeidx begin definition "tmL1 ≡ tm_incr j" definition "tmL2 ≡ tmL1 ;; tm_right 0" definition "tm1 ≡ WHILE [] ; λrs. rs ! 0 ≠ □ DO tmL2 DONE" definition "tm2 ≡ tm1 ;; tm_cr 0" lemma tm2_eq_tm_length_input: "tm2 = tm_length_input j" unfolding tm2_def tm1_def tmL2_def tmL1_def tm_length_input_def by simp context fixes tps0 :: "tape list" and k :: nat and zs :: "symbol list" assumes jk: "0 < j" "j < k" "length tps0 = k" and zs: "proper_symbols zs" and tps0: "tps0 ! 0 = (⌊zs⌋, 1)" "tps0 ! j = (⌊0⌋⇩_{N}, 1)" begin definition tpsL :: "nat ⇒ tape list" where "tpsL t ≡ tps0[0 := (⌊zs⌋, 1 + t), j := (⌊t⌋⇩_{N}, 1)]" lemma tpsL_eq_tps0: "tpsL 0 = tps0" using tpsL_def tps0 jk by (metis One_nat_def list_update_id plus_1_eq_Suc) definition tpsL1 :: "nat ⇒ tape list" where "tpsL1 t ≡ tps0[0 := (⌊zs⌋, 1 + t), j := (⌊Suc t⌋⇩_{N}, 1)]" definition tpsL2 :: "nat ⇒ tape list" where "tpsL2 t ≡ tps0[0 := (⌊zs⌋, 1 + Suc t), j := (⌊Suc t⌋⇩_{N}, 1)]" lemma tmL1 [transforms_intros]: assumes "t < length zs" and "ttt = 5 + 2 * nlength t" shows "transforms tmL1 (tpsL t) ttt (tpsL1 t)" unfolding tmL1_def by (tform tps: assms(1) tpsL_def tpsL1_def tps0 jk time: assms(2)) lemma tmL2: assumes "t < length zs" and "ttt = 6 + 2 * nlength t" shows "transforms tmL2 (tpsL t) ttt (tpsL (Suc t))" unfolding tmL2_def proof (tform tps: assms(1) tpsL_def tpsL1_def tps0 jk time: assms(2)) have "tpsL1 t ! 0 = (⌊zs⌋, 1 + t)" using tpsL2_def tpsL1_def jk tps0 by simp then have "tpsL2 t = (tpsL1 t)[0 := tpsL1 t ! 0 |#=| Suc (tpsL1 t :#: 0)]" using tpsL2_def tpsL1_def jk tps0 by (smt (z3) fstI list_update_overwrite list_update_swap nat_neq_iff plus_1_eq_Suc prod.sel(2)) then show "tpsL (Suc t) = (tpsL1 t)[0 := tpsL1 t ! 0 |+| 1]" using tpsL2_def tpsL_def tpsL1_def jk tps0 by simp qed lemma tmL2': assumes "t < length zs" and "ttt = 6 + 2 * nlength (length zs)" shows "transforms tmL2 (tpsL t) ttt (tpsL (Suc t))" proof - have "6 + 2 * nlength t ≤ 6 + 2 * nlength (length zs)" using assms(1) nlength_mono by simp then show ?thesis using assms tmL2 transforms_monotone by blast qed lemma tm1: assumes "ttt = length zs * (8 + 2 * nlength (length zs)) + 1" shows "transforms tm1 (tpsL 0) ttt (tpsL (length zs))" unfolding tm1_def proof (tform) let ?t = "6 + 2 * nlength (length zs)" show "⋀t. t < length zs ⟹ transforms tmL2 (tpsL t) ?t (tpsL (Suc t))" using tmL2' by simp have *: "tpsL t ! 0 = (⌊zs⌋, Suc t)" for t using tpsL_def jk by simp then show "⋀t. t < length zs ⟹ read (tpsL t) ! 0 ≠ □" using proper_tape_read[OF zs] tpsL_def jk tapes_at_read' by (metis length_list_update less_Suc_eq_0_disj not_less_eq) show "¬ read (tpsL (length zs)) ! 0 ≠ □" using proper_tape_read[OF zs] tpsL_def jk tapes_at_read' * by (metis length_list_update less_Suc_eq_0_disj less_imp_Suc_add nat_neq_iff not_less_less_Suc_eq) show "length zs * (6 + 2 * nlength (length zs) + 2) + 1 ≤ ttt" using assms by simp qed lemma tmL' [transforms_intros]: assumes "ttt = 10 * length zs ^ 2 + 1" shows "transforms tm1 (tpsL 0) ttt (tpsL (length zs))" proof - let ?ttt = "length zs * (8 + 2 * nlength (length zs)) + 1" have "?ttt ≤ length zs * (8 + 2 * length zs) + 1" using nlength_le_n by simp also have "... ≤ 8 * length zs + 2 * length zs ^ 2 + 1" by (simp add: add_mult_distrib2 power2_eq_square) also have "... ≤ 10 * length zs ^ 2 + 1" using linear_le_pow by simp finally have "?ttt ≤ 10 * length zs ^ 2 + 1" . then show ?thesis using tm1 assms transforms_monotone by simp qed definition tps2 :: "tape list" where "tps2 ≡ tps0[0 := (⌊zs⌋, 1), j := (⌊length zs⌋⇩_{N}, 1)]" lemma tm2: assumes "ttt = 10 * length zs ^ 2 + length zs + 4" shows "transforms tm2 (tpsL 0) ttt tps2" unfolding tm2_def proof (tform time: assms tpsL_def jk tps: tpsL_def tpsL1_def tps0 jk) show "clean_tape (tpsL (length zs) ! 0)" using tpsL_def jk clean_contents_proper[OF zs] by simp have "tpsL (length zs) ! 0 = (⌊zs⌋, Suc (length zs))" using tpsL_def jk by simp then show "tps2 = (tpsL (length zs))[0 := tpsL (length zs) ! 0 |#=| 1]" using tps2_def tpsL_def jk by (simp add: list_update_swap_less) qed definition tps2' :: "tape list" where "tps2' ≡ tps0[j := (⌊length zs⌋⇩_{N}, 1)]" lemma tm2': assumes "ttt = 11 * length zs ^ 2 + 4" shows "transforms tm2 tps0 ttt tps2'" proof - have "10 * length zs ^ 2 + length zs + 4 ≤ ttt" using assms linear_le_pow[of 2 "length zs"] by simp moreover have "tps2 = tps2'" using tps2_def tps2'_def jk tps0 by (metis list_update_id) ultimately show ?thesis using transforms_monotone tm2 tpsL_eq_tps0 by simp qed end end lemma transforms_tm_length_inputI [transforms_intros]: fixes j :: tapeidx fixes tps tps' :: "tape list" and k :: nat and zs :: "symbol list" assumes "0 < j" "j < k" "length tps = k" and "proper_symbols zs" assumes "tps ! 0 = (⌊zs⌋, 1)" "tps ! j = (⌊0⌋⇩_{N}, 1)" assumes "ttt = 11 * length zs ^ 2 + 4" assumes "tps' = tps [j := (⌊length zs⌋⇩_{N}, 1)]" shows "transforms (tm_length_input j) tps ttt tps'" proof - interpret loc: turing_machine_length_input j . show ?thesis using loc.tm2' loc.tps2'_def loc.tm2_eq_tm_length_input assms by simp qed subsection ‹Whether the length is even› text ‹ The next Turing machines reads the symbols on tape $j_1$ until the first blank and alternates between numbers~0 and~1 on tape $j_2$. Then tape $j_2$ contains the parity of the length of the symbol sequence on tape $j_1$. Finally, the TM flips the output once more, so that tape $j_2$ contains a Boolean indicating whether the length was even or not. We assume tape $j_2$ is initially empty, that is, represents the number~0. › definition tm_even_length :: "tapeidx ⇒ tapeidx ⇒ machine" where "tm_even_length j1 j2 ≡ WHILE [] ; λrs. rs ! j1 ≠ □ DO tm_not j2 ;; tm_right j1 DONE ;; tm_not j2 ;; tm_cr j1" lemma tm_even_length_tm: assumes "k ≥ 2" and "G ≥ 4" and "j1 < k" "0 < j2" "j2 < k" shows "turing_machine k G (tm_even_length j1 j2)" using tm_even_length_def tm_right_tm tm_not_tm Nil_tm assms tm_cr_tm turing_machine_loop_turing_machine by simp locale turing_machine_even_length = fixes j1 j2 :: tapeidx begin definition "tmB ≡ tm_not j2 ;; tm_right j1" definition "tmL ≡ WHILE [] ; λrs. rs ! j1 ≠ □ DO tmB DONE" definition "tm2 ≡ tmL ;; tm_not j2" definition "tm3 ≡ tm2 ;; tm_cr j1" lemma tm3_eq_tm_even_length: "tm3 = tm_even_length j1 j2" unfolding tm3_def tm2_def tmL_def tmB_def tm_even_length_def by simp context fixes tps0 :: "tape list" and k :: nat and zs :: "symbol list" assumes zs: "proper_symbols zs" assumes jk: "j1 < k" "j2 < k" "j1 ≠ j2" "length tps0 = k" assumes tps0: "tps0 ! j1 = (⌊zs⌋, 1)" "tps0 ! j2 = (⌊0⌋⇩_{N}, 1)" begin definition tpsL :: "nat ⇒ tape list" where "tpsL t ≡ tps0 [j1 := (⌊zs⌋, Suc t), j2 := (⌊odd t⌋⇩_{B}, 1)]" lemma tpsL0: "tpsL 0 = tps0" unfolding tpsL_def using tps0 jk by (metis (mono_tags, opaque_lifting) One_nat_def even_zero list_update_id) lemma tmL2 [transforms_intros]: "transforms tmB (tpsL t) 4 (tpsL (Suc t))" unfolding tmB_def proof (tform tps: tpsL_def jk) have "(tpsL t) [j2 := (⌊(if odd t then 1 else 0 :: nat) ≠ 1⌋⇩_{B}, 1), j1 := (tpsL t)[j2 := (⌊ (if odd t then 1 else 0 :: nat) ≠ 1 ⌋⇩_{B}, 1)] ! j1 |+| 1] = (tpsL t) [j2 := (⌊odd (Suc t)⌋⇩_{B}, 1), j1 := (tpsL t) ! j1 |+| 1]" using jk by simp also have "... = (tpsL t) [j2 := (⌊odd (Suc t)⌋⇩_{B}, 1), j1 := (⌊zs⌋, Suc (Suc t))]" using tpsL_def jk by simp also have "... = (tpsL t) [j1 := (⌊zs⌋, Suc (Suc t)), j2 := (⌊odd (Suc t)⌋⇩_{B}, 1)]" using jk by (simp add: list_update_swap) also have "... = tps0 [j1 := (⌊zs⌋, Suc (Suc t)), j2 := (⌊odd (Suc t)⌋⇩_{B}, 1)]" using jk tpsL_def by (simp add: list_update_swap) also have "... = tpsL (Suc t)" using tpsL_def by simp finally show "tpsL (Suc t) = (tpsL t) [j2 := (⌊(if odd t then 1 else 0 :: nat) ≠ 1⌋⇩_{B}, 1), j1 := (tpsL t)[j2 := (⌊(if odd t then 1 else 0 :: nat) ≠ 1⌋⇩_{B}, 1)] ! j1 |+| 1]" by simp qed lemma tmL: assumes "ttt = 6 * length zs + 1" shows "transforms tmL (tpsL 0) ttt (tpsL (length zs))" unfolding tmL_def proof (tform time: assms) have "read (tpsL t) ! j1 = tpsL t :.: j1" for t using tpsL_def tapes_at_read' jk by (metis (no_types, lifting) length_list_update) then have "read (tpsL t) ! j1 = ⌊zs⌋ (Suc t)" for t using tpsL_def jk by simp then show "⋀t. t < length zs ⟹ read (tpsL t) ! j1 ≠ □" and "¬ read (tpsL (length zs)) ! j1 ≠ □" using zs by auto qed lemma tmL' [transforms_intros]: assumes "ttt = 6 * length zs + 1" shows "transforms tmL tps0 ttt (tpsL (length zs))" using assms tmL tpsL0 by simp definition tps2 :: "tape list" where "tps2 ≡ tps0 [j1 := (⌊zs⌋, Suc (length zs)), j2 := (⌊even (length zs) ⌋⇩_{B}, 1)]" lemma tm2 [transforms_intros]: assumes "ttt = 6 * length zs + 4" shows "transforms tm2 tps0 ttt tps2" unfolding tm2_def proof (tform tps: tpsL_def jk time: assms) show "tps2 = (tpsL (length zs))[j2 := (⌊(if odd (length zs) then 1 else 0 :: nat) ≠ 1⌋⇩_{B}, 1)]" unfolding tps2_def tpsL_def by (simp add: list_update_swap) qed definition tps3 :: "tape list" where "tps3 ≡ tps0 [j1 := (⌊zs⌋, 1), j2 := (⌊even (length zs)⌋⇩_{B}, 1)]" lemma tm3: assumes "ttt = 7 * length zs + 7" shows "transforms tm3 tps0 ttt tps3" unfolding tm3_def proof (tform tps: tps2_def jk time: assms) show "clean_tape (tps2 ! j1)" using tps2_def jk zs clean_contents_proper by simp have "tps2 ! j1 |#=| 1 = (⌊zs⌋, 1)" using tps2_def jk by simp then show "tps3 = tps2[j1 := tps2 ! j1 |#=| 1]" unfolding tps3_def tps2_def using jk by (simp add: list_update_swap) show "ttt = 6 * length zs + 4 + (tps2 :#: j1 + 2)" using assms tps2_def jk by simp qed definition tps3' :: "tape list" where "tps3' ≡ tps0 [j2 := (⌊even (length zs)⌋⇩_{B}, 1)]" lemma tps3': "tps3' = tps3" using tps3'_def tps3_def tps0 by (metis list_update_id) lemma tm3': assumes "ttt = 7 * length zs + 7" shows "transforms tm3 tps0 ttt tps3'" using tps3' tm3 assms by simp end (* context *) end (* locale *) lemma transforms_tm_even_lengthI [transforms_intros]: fixes j1 j2 :: tapeidx fixes tps tps' :: "tape list" and k :: nat and zs :: "symbol list" assumes "j1 < k" "j2 < k" "j1 ≠ j2" and "proper_symbols zs" and "length tps = k" assumes "tps ! j1 = (⌊zs⌋, 1)" "tps ! j2 = (⌊0⌋⇩_{N}, 1)" assumes "tps' = tps [j2 := (⌊even (length zs)⌋⇩_{B}, 1)]" assumes "ttt = 7 * length zs + 7" shows "transforms (tm_even_length j1 j2) tps ttt tps'" proof - interpret loc: turing_machine_even_length j1 j2 . show ?thesis using assms loc.tps3'_def loc.tm3' loc.tm3_eq_tm_even_length by simp qed subsection ‹Checking for ends-with or empty› text ‹ The next Turing machine implements a slightly idiosyncratic operation that we use in the next section for checking if a symbol sequence represents a list of numbers. The operation consists in checking if the symbol sequence on tape $j_1$ either is empty or ends with the symbol $z$, which is another parameter of the TM. If the condition is met, the number~1 is written to tape $j_2$, otherwise the number~0. › definition tm_empty_or_endswith :: "tapeidx ⇒ tapeidx ⇒ symbol ⇒ machine" where "tm_empty_or_endswith j1 j2 z ≡ tm_right_until j1 {□} ;; tm_left j1 ;; IF λrs. rs ! j1 ∈ {▹, z} THEN tm_setn j2 1 ELSE [] ENDIF ;; tm_cr j1" lemma tm_empty_or_endswith_tm: assumes "k ≥ 2" and "G ≥ 4" and "0 < j2" and "j1 < k" and "j2 < k" shows "turing_machine k G (tm_empty_or_endswith j1 j2 z)" using assms Nil_tm tm_right_until_tm tm_left_tm tm_setn_tm tm_cr_tm turing_machine_branch_turing_machine tm_empty_or_endswith_def by simp locale turing_machine_empty_or_endswith = fixes j1 j2 :: tapeidx and z :: symbol begin definition "tm1 ≡ tm_right_until j1 {□}" definition "tm2 ≡ tm1 ;; tm_left j1" definition "tmI ≡ IF λrs. rs ! j1 ∈ {▹, z} THEN tm_setn j2 1 ELSE [] ENDIF" definition "tm3 ≡ tm2 ;; tmI" definition "tm4 ≡ tm3 ;; tm_cr j1" lemma tm4_eq_tm_empty_or_endswith: "tm4 = tm_empty_or_endswith j1 j2 z" unfolding tm4_def tm3_def tmI_def tm2_def tm1_def tm_empty_or_endswith_def by simp context fixes tps0 :: "tape list" and k :: nat and zs :: "symbol list" assumes jk: "j1 ≠ j2" "j1 < k" "j2 < k" "length tps0 = k" and zs: "proper_symbols zs" and tps0: "tps0 ! j1 = (⌊zs⌋, 1)" "tps0 ! j2 = (⌊0⌋⇩_{N}, 1)" begin definition tps1 :: "tape list" where "tps1 ≡ tps0 [j1 := (⌊zs⌋, Suc (length zs))]" lemma tm1 [transforms_intros]: assumes "ttt = Suc (length zs)" shows "transforms tm1 tps0 ttt tps1" unfolding tm1_def proof (tform time: assms tps: tps0 tps1_def jk) show "rneigh (tps0 ! j1) {0} (length zs)" proof (rule rneighI) show "(tps0 ::: j1) (tps0 :#: j1 + length zs) ∈ {0}" using tps0 by simp show "⋀n'. n' < length zs ⟹ (tps0 ::: j1) (tps0 :#: j1 + n') ∉ {0}" using zs tps0 by auto qed qed definition tps2 :: "tape list" where "tps2 ≡ tps0 [j1 := (⌊zs⌋, length zs)]" lemma tm2 [transforms_intros]: assumes "ttt = 2 + length zs" shows "transforms tm2 tps0 ttt tps2" unfolding tm2_def by (tform time: assms tps: tps1_def tps2_def jk) definition tps3 :: "tape list" where "tps3 ≡ tps0 [j1 := (⌊zs⌋, length zs), j2 := (⌊zs = [] ∨ last zs = z⌋⇩_{B}, 1)]" lemma tmI [transforms_intros]: "transforms tmI tps2 14 tps3" unfolding tmI_def proof (tform tps: tps0 tps2_def jk) have *: "read tps2 ! j1 = ⌊zs⌋ (length zs)" using tps2_def jk tapes_at_read'[of j1 tps2] by simp show "tps3 = tps2[j2 := (⌊1⌋⇩_{N}, 1)]" if "read tps2 ! j1 ∈ {▹, z}" proof - have "zs = [] ∨ last zs = z" using that * contents_inbounds zs by (metis diff_less dual_order.refl insert_iff last_conv_nth length_greater_0_conv proper_symbols_ne1 singletonD zero_less_one) then have "(if zs = [] ∨ last zs = z then 1 else 0) = 1" by simp then show ?thesis using tps2_def tps3_def jk by (smt (verit, best)) qed show "tps3 = tps2" if "read tps2 ! j1 ∉ {▹, z}" proof - have "¬ (zs = [] ∨ last zs = z)" using that * contents_inbounds zs by (metis contents_at_0 dual_order.refl insertCI last_conv_nth length_greater_0_conv list.size(3)) then have "(if zs = [] ∨ last zs = z then 1 else 0) = 0" by simp then show ?thesis using tps2_def tps3_def jk tps0 by (smt (verit, best) list_update_id nth_list_update_neq) qed show "10 + 2 * nlength 0 + 2 * nlength 1 + 2 ≤ 14" using nlength_1_simp by simp qed lemma tm3 [transforms_intros]: assumes "ttt = 16 + length zs" shows "transforms tm3 tps0 ttt tps3" unfolding tm3_def by (tform tps: assms) definition tps4 :: "tape list" where "tps4 ≡ tps0 [j2 := (⌊zs = [] ∨ last zs = z⌋⇩_{B}, 1)]" lemma tm4: assumes "ttt = 18 + 2 * length zs" shows "transforms tm4 tps0 ttt tps4" unfolding tm4_def proof (tform time: assms tps3_def jk tps: tps3_def jk zs) have "tps3 ! j1 |#=| 1 = (⌊zs⌋, 1)" using tps3_def jk zs by simp then show "tps4 = tps3[j1 := tps3 ! j1 |#=| 1]" using tps4_def tps3_def jk tps0(1) by (metis list_update_id list_update_overwrite list_update_swap) qed end (* context *) end (* locale *) lemma transforms_tm_empty_or_endswithI [transforms_intros]: fixes j1 j2 :: tapeidx and z :: symbol fixes tps tps' :: "tape list" and k :: nat and zs :: "symbol list" assumes "j1 ≠ j2" "j1 < k" "j2 < k" and "length tps = k" and "proper_symbols zs" assumes "tps ! j1 = (⌊zs⌋, 1)" "tps ! j2 = (⌊0⌋⇩_{N}, 1)" assumes "ttt = 18 + 2 * length zs" assumes "tps' = tps [j2 := (⌊zs = [] ∨ last zs = z⌋⇩_{B}, 1)]" shows "transforms (tm_empty_or_endswith j1 j2 z) tps ttt tps'" proof - interpret loc: turing_machine_empty_or_endswith j1 j2 z . show ?thesis using assms loc.tps4_def loc.tm4 loc.tm4_eq_tm_empty_or_endswith by simp qed subsection ‹Stripping trailing symbols› text ‹ Stripping the symbol $z$ from the end of a symbol sequence @{term zs} means: › definition rstrip :: "symbol ⇒ symbol list ⇒ symbol list" where "rstrip z zs ≡ take (LEAST i. i ≤ length zs ∧ set (drop i zs) ⊆ {z}) zs" lemma length_rstrip: "length (rstrip z zs) = (LEAST i. i ≤ length zs ∧ set (drop i zs) ⊆ {z})" using rstrip_def wellorder_Least_lemma[where ?P="λi. i ≤ length zs ∧ set (drop i zs) ⊆ {z}"] by simp lemma length_rstrip_le: "length (rstrip z zs) ≤ length zs" using rstrip_def by simp lemma rstrip_stripped: assumes "i ≥ length (rstrip z zs)" and "i < length zs" shows "zs ! i = z" proof - let ?P = "λi. i ≤ length zs ∧ set (drop i zs) ⊆ {z}" have "?P (length zs)" by simp then have "?P i" using assms length_rstrip LeastI[where ?P="?P"] Least_le[where ?P="?P"] by (metis (mono_tags, lifting) dual_order.trans order_less_imp_le set_drop_subset_set_drop) then have "set (drop i zs) ⊆ {z}" by simp then show ?thesis using assms(2) by (metis Cons_nth_drop_Suc drop_eq_Nil2 leD list.set(2) set_empty singleton_insert_inj_eq subset_singletonD) qed lemma rstrip_replicate: "rstrip z (replicate n z) = []" using rstrip_def by (metis (no_types, lifting) Least_eq_0 empty_replicate set_drop_subset set_replicate take_eq_Nil zero_le) lemma rstrip_not_ex: assumes "¬ (∃i<length zs. zs ! i ≠ z)" shows "rstrip z zs = []" using assms rstrip_def by (metis in_set_conv_nth replicate_eqI rstrip_replicate) lemma assumes "∃i<length zs. zs ! i ≠ z" shows rstrip_ex_length: "length (rstrip z zs) > 0" and rstrip_ex_last: "last (rstrip z zs) ≠ z" proof - let ?P = "λi. i ≤ length zs ∧ set (drop i zs) ⊆ {z}" obtain i where i: "i < length zs" "zs ! i ≠ z" using assms by auto then have "¬ set (drop i zs) ⊆ {z}" by (metis Cons_nth_drop_Suc drop_eq_Nil2 leD list.set(2) set_empty singleton_insert_inj_eq' subset_singletonD) then have "¬ set (drop 0 zs) ⊆ {z}" by (metis drop.simps(1) drop_0 set_drop_subset set_empty subset_singletonD) then show len: "length (rstrip z zs) > 0" using length_rstrip by (metis (no_types, lifting) LeastI bot.extremum drop_all dual_order.refl gr0I list.set(1)) let ?j = "length (rstrip z zs) - 1" have 3: "?j < length (rstrip z zs)" using len by simp then have 4: "?j < Least ?P" using length_rstrip by simp have 5: "?P (length (rstrip z zs))" using LeastI_ex[of "?P"] length_rstrip by fastforce show "last (rstrip z zs) ≠ z" proof (rule ccontr) assume "¬ last (rstrip z zs) ≠ z" then have "last (rstrip z zs) = z" by simp then have "rstrip z zs ! ?j = z" using len by (simp add: last_conv_nth) then have 2: "zs ! ?j = z" using len length_rstrip rstrip_def by auto have "?P ?j" proof - have "?j ≤ length zs" using 3 length_rstrip_le by (meson le_eq_less_or_eq order_less_le_trans) moreover have "set (drop ?j zs) ⊆ {z}" using 5 3 2 by (metis Cons_nth_drop_Suc One_nat_def Suc_pred insert_subset len list.simps(15) order_less_le_trans set_eq_subset) ultimately show ?thesis by simp qed then show False using 4 Least_le[of "?P"] by fastforce qed qed text ‹ A Turing machine stripping the non-blank, non-start symbol $z$ from a proper symbol sequence works in the obvious way. First it moves to the end of the symbol sequence, that is, to the first blank. Then it moves left to the first non-$z$ symbol thereby overwriting every symbol with a blank. Finally it performs a ``carriage return''. › definition tm_rstrip :: "symbol ⇒ tapeidx ⇒ machine" where "tm_rstrip z j ≡ tm_right_until j {□} ;; tm_left j ;; tm_lconst_until j j (UNIV - {z}) □ ;; tm_cr j" lemma tm_rstrip_tm: assumes "k ≥ 2" and "G ≥ 4" and "0 < j" and "j < k" shows "turing_machine k G (tm_rstrip z j)" using assms tm_right_until_tm tm_left_tm tm_lconst_until_tm tm_cr_tm tm_rstrip_def by simp locale turing_machine_rstrip = fixes z :: symbol and j :: tapeidx begin definition "tm1 ≡ tm_right_until j {□}" definition "tm2 ≡ tm1 ;; tm_left j" definition "tm3 ≡ tm2 ;; tm_lconst_until j j (UNIV - {z}) □" definition "tm4 ≡ tm3 ;; tm_cr j" lemma tm4_eq_tm_rstrip: "tm4 = tm_rstrip z j" unfolding tm4_def tm3_def tm2_def tm1_def tm_rstrip_def by simp context fixes tps0 :: "tape list" and zs :: "symbol list" and k :: nat assumes z: "z > 1" assumes zs: "proper_symbols zs" assumes jk: "0 < j" "j < k" "length tps0 = k" assumes tps0: "tps0 ! j = (⌊zs⌋, 1)" begin definition "tps1 ≡ tps0 [j := (⌊zs⌋, Suc (length zs))]" lemma tm1 [transforms_intros]: assumes "ttt = Suc (length zs)" shows "transforms tm1 tps0 ttt tps1" unfolding tm1_def proof (tform tps: tps0 tps1_def jk time: assms) have *: "tps0 ! j = (⌊zs⌋, 1)" using tps0 jk by simp show "rneigh (tps0 ! j) {□} (length zs)" using * zs by (intro rneighI) auto qed definition "tps2 ≡ tps0 [j := (⌊zs⌋, length zs)]" lemma tm2 [transforms_intros]: assumes "ttt = length zs + 2" shows "transforms tm2 tps0 ttt tps2" unfolding tm2_def by (tform tps: tps1_def tps2_def jk time: assms) definition "tps3 ≡ tps0 [j := (⌊rstrip z zs⌋, length (rstrip z zs))]" lemma tm3 [transforms_intros]: assumes "ttt = length zs + 2 + Suc (length zs - length (rstrip z zs))" shows "transforms tm3 tps0 ttt tps3" unfolding tm3_def proof (tform tps: tps2_def tps3_def jk time: assms jk tps2_def) let ?n = "length zs - length (rstrip z zs)" have *: "tps2 ! j = (⌊zs⌋, length zs)" using tps2_def jk by simp show "lneigh (tps2 ! j) (UNIV - {z}) ?n" proof (cases "∃i<length zs. zs ! i ≠ z") case True then have 1: "length (rstrip z zs) > 0" using rstrip_ex_length by simp show ?thesis proof (rule lneighI) show "(tps2 ::: j) (tps2 :#: j - ?n) ∈ UNIV - {z}" using * 1 contents_inbounds True length_rstrip length_rstrip_le rstrip_def rstrip_ex_last by (smt (verit, best) DiffI One_nat_def UNIV_I diff_diff_cancel diff_less fst_conv last_conv_nth le_eq_less_or_eq length_greater_0_conv less_Suc_eq_le nth_take singletonD snd_conv) have "⋀n'. n' < ?n ⟹ (tps2 ::: j) (tps2 :#: j - n') = z" using * rstrip_stripped by simp then show "⋀n'. n' < ?n ⟹ (tps2 ::: j) (tps2 :#: j - n') ∉ UNIV - {z}" by simp qed next case False then have 1: "rstrip z zs = []" using rstrip_not_ex by simp show ?thesis proof (rule lneighI) show "(tps2 ::: j) (tps2 :#: j - ?n) ∈ UNIV - {z}" using * 1 z by simp show "⋀n'. n' < ?n ⟹ (tps2 ::: j) (tps2 :#: j - n') ∉ UNIV - {z}" using * rstrip_stripped by simp qed qed have "lconstplant (⌊zs⌋, length zs) □ ?n = (⌊rstrip z zs⌋, length (rstrip z zs))" (is "?lhs = _") proof - have "?lhs = (λi. if length zs - ?n < i ∧ i ≤ length zs then □ else ⌊zs⌋ i, length zs - ?n)" using lconstplant[of "(⌊zs⌋, length zs)" 0 "?n"] by auto moreover have "(λi. if length zs - ?n < i ∧ i ≤ length zs then □ else ⌊zs⌋ i) = ⌊rstrip z zs⌋" proof fix i consider "length zs - ?n < i ∧ i ≤ length zs" | "i > length zs" | "i ≤ length (rstrip z zs)" by linarith then show "(if length zs - ?n < i ∧ i ≤ length zs then □ else ⌊zs⌋ i) = ⌊rstrip z zs⌋ i" proof (cases) case 1 then show ?thesis by auto next case 2 then show ?thesis by (metis contents_outofbounds diff_diff_cancel length_rstrip_le less_imp_diff_less) next case 3 then show ?thesis using contents_def length_rstrip length_rstrip_le rstrip_def by auto qed qed moreover have "length zs - ?n = length (rstrip z zs)" using diff_diff_cancel length_rstrip_le by simp ultimately show ?thesis by simp qed then have "lconstplant (tps2 ! j) □ ?n = (⌊rstrip z zs⌋, length (rstrip z zs))" using tps2_def jk by simp then show "tps3 = tps2 [j := tps2 ! j |-| ?n, j := lconstplant (tps2 ! j) □ ?n]" unfolding tps3_def tps2_def by simp qed definition "tps4 ≡ tps0 [j := (⌊rstrip z zs⌋, 1)]" lemma tm4: assumes "ttt = length zs + 2 + Suc (length zs - length (rstrip z zs)) + length (rstrip z zs) + 2" shows "transforms tm4 tps0 ttt tps4" unfolding tm4_def proof (tform tps: tps3_def tps4_def jk time: assms tps3_def jk) show "clean_tape (tps3 ! j)" using tps3_def jk zs rstrip_def by simp qed lemma tm4': assumes "ttt = 3 * length zs + 5" shows "transforms tm4 tps0 ttt tps4" proof - let ?ttt = "length zs + 2 + Suc (length zs - length (rstrip z zs)) + length (rstrip z zs) + 2" have "?ttt = length zs + 5 + (length zs - length (rstrip z zs)) + length (rstrip z zs)" by simp also have "... ≤ length zs + 5 + length zs + length (rstrip z zs)" by simp also have "... ≤ length zs + 5 + length zs + length zs" using length_rstrip_le by simp also have "... = 3 * length zs + 5" by simp finally have "?ttt ≤ 3 * length zs + 5" . then show ?thesis using assms transforms_monotone tm4 by simp qed end (* context *) end (* locale *) lemma transforms_tm_rstripI [transforms_intros]: fixes z :: symbol and j :: tapeidx fixes tps tps' :: "tape list" and zs :: "symbol list" and k :: nat assumes "z > 1" and "0 < j" "j < k" and "proper_symbols zs" and "length tps = k" assumes "tps ! j = (⌊zs⌋, 1)" assumes "ttt = 3 * length zs + 5" assumes "tps' = tps[j := (⌊rstrip z zs⌋, 1)]" shows "transforms (tm_rstrip z j) tps ttt tps'" proof - interpret loc: turing_machine_rstrip z j . show ?thesis using assms loc.tm4' loc.tps4_def loc.tm4_eq_tm_rstrip by simp qed subsection ‹Writing arbitrary length sequences of the same symbol› text ‹ The next Turing machine accepts a number $n$ on tape $j_1$ and writes the symbol sequence $z^n$ to tape $j_2$. The symbol $z$ is a parameter of the TM. The TM decrements the number on tape $j_1$ until it reaches zero. › definition tm_write_replicate :: "symbol ⇒ tapeidx ⇒ tapeidx ⇒ machine" where "tm_write_replicate z j1 j2 ≡ WHILE [] ; λrs. rs ! j1 ≠ □ DO tm_char j2 z ;; tm_decr j1 DONE ;; tm_cr j2" lemma tm_write_replicate_tm: assumes "0 < j1" and "0 < j2" and "j1 < k" and "j2 < k" and "j1 ≠ j2" and "G ≥ 4" and "z < G" shows "turing_machine k G (tm_write_replicate z j1 j2)" unfolding tm_write_replicate_def using turing_machine_loop_turing_machine Nil_tm tm_char_tm tm_decr_tm tm_cr_tm assms by simp locale turing_machine_write_replicate = fixes j1 j2 :: tapeidx and z :: symbol begin definition "tm1 ≡ tm_char j2 z" definition "tm2 ≡ tm1 ;; tm_decr j1" definition "tmL ≡ WHILE [] ; λrs. rs ! j1 ≠ □ DO tm2 DONE" definition "tm3 ≡ tmL ;; tm_cr j2" lemma tm3_eq_tm_write_replicate: "tm3 = tm_write_replicate z j1 j2" using tm3_def tm2_def tm1_def tm_write_replicate_def tmL_def by simp context fixes tps0 :: "tape list" and k n :: nat assumes jk: "length tps0 = k" "0 < j1" "0 < j2" "j1 ≠ j2" "j1 < k" "j2 < k" and z: "1 < z" assumes tps0: "tps0 ! j1 = (⌊n⌋⇩_{N}, 1)" "tps0 ! j2 = (⌊[]⌋, 1)" begin definition tpsL :: "nat ⇒ tape list" where "tpsL t ≡ tps0 [j1 := (⌊n - t⌋⇩_{N}, 1), j2 := (⌊replicate t z⌋, Suc t)]" lemma tpsL0: "tpsL 0 = tps0" using tpsL_def tps0 jk by (metis One_nat_def diff_zero list_update_id replicate_empty) definition tpsL1 :: "nat ⇒ tape list" where "tpsL1 t ≡ tps0 [j1 := (⌊n - t⌋⇩_{N}, 1), j2 := (⌊replicate (Suc t) z⌋, Suc (Suc t))]" lemma tmL1 [transforms_intros]: "transforms tm1 (tpsL t) 1 (tpsL1 t)" unfolding tm1_def proof (tform tps: tpsL_def tpsL1_def tps0 jk) have "tpsL t :#: j2 = Suc t" using tpsL1_def jk by (metis length_list_update nth_list_update_eq snd_conv tpsL_def) moreover have "tpsL t ::: j2 = ⌊replicate t z⌋" using tpsL1_def jk by (metis fst_conv length_list_update nth_list_update_eq tpsL_def) moreover have "⌊replicate t z⌋(Suc t := z) = ⌊replicate (Suc t) z⌋" using contents_snoc by (metis length_replicate replicate_Suc replicate_append_same) ultimately show "tpsL1 t = (tpsL t)[j2 := tpsL t ! j2 |:=| z |+| 1]" unfolding tpsL1_def tpsL_def by simp qed lemma tmL2: assumes "ttt = 9 + 2 * nlength (n - t)" shows "transforms tm2 (tpsL t) ttt (tpsL (Suc t))" unfolding tm2_def proof (tform tps: assms tpsL_def tpsL1_def tps0 jk) show "tpsL (Suc t) = (tpsL1 t)[j1 := (⌊n - t - 1⌋⇩_{N}, 1)]" unfolding tpsL_def tpsL1_def using jk by (simp add: list_update_swap) qed lemma tmL2' [transforms_intros]: assumes "ttt = 9 + 2 * nlength n" shows "transforms tm2 (tpsL t) ttt (tpsL (Suc t))" proof - have "9 + 2 * nlength (n - t) ≤ 9 + 2 * nlength n" using nlength_mono[of "n - t" n] by simp then show ?thesis using assms tmL2 transforms_monotone by blast qed lemma tmL [transforms_intros]: assumes "ttt = n * (11 + 2 * nlength n) + 1" shows "transforms tmL (tpsL 0) ttt (tpsL n)" unfolding tmL_def proof (tform) let ?t = "9 + 2 * nlength n" show "⋀i. i < n ⟹ read (tpsL i) ! j1 ≠ □" using jk tpsL_def read_ncontents_eq_0 by simp show "¬ read (tpsL n) ! j1 ≠ □" using jk tpsL_def read_ncontents_eq_0 by simp show "n * (9 + 2 * nlength n + 2) + 1 ≤ ttt" using assms by simp qed definition tps3 :: "tape list" where "tps3 ≡ tps0 [j1 := (⌊0⌋⇩_{N}, 1), j2 := (⌊replicate n z⌋, 1)]" lemma tm3: assumes "ttt = n * (12 + 2 * nlength n) + 4" shows "transforms tm3 (tpsL 0) ttt tps3" unfolding tm3_def proof (tform tps: z tpsL_def tps3_def tps0 jk) have "ttt = Suc (n * (11 + 2 * nlength n)) + Suc (Suc (Suc n))" proof - have "Suc (n * (11 + 2 * nlength n)) + Suc (Suc (Suc n)) = n * (11 + 2 * nlength n) + 4 + n" by simp also have "... = n * (12 + 2 * nlength n) + 4" by algebra finally have "Suc (n * (11 + 2 * nlength n)) + Suc (Suc (Suc n)) = ttt" using assms by simp then show ?thesis by simp qed then show "ttt = n * (11 + 2 * nlength n) + 1 + (tpsL n :#: j2 + 2)" using tpsL_def jk by simp qed lemma tm3': assumes "ttt = n * (12 + 2 * nlength n) + 4" shows "transforms tm3 tps0 ttt tps3" using tm3 tpsL0 assms by simp end end lemma transforms_tm_write_replicateI [transforms_intros]: fixes j1 j2 :: tapeidx fixes tps tps' :: "tape list" and ttt k n :: nat assumes "length tps = k" "0 < j1" "0 < j2" "j1 ≠ j2" "j1 < k" "j2 < k" and "1 < z" assumes "tps ! j1 = (⌊n⌋⇩_{N}, 1)" "tps ! j2 = (⌊[]⌋, 1)" assumes "ttt = n * (12 + 2 * nlength n) + 4" assumes "tps' = tps [j1 := (⌊0⌋⇩_{N}, 1), j2 := (⌊replicate n z⌋, 1)]" shows "transforms (tm_write_replicate z j1 j2) tps ttt tps'" proof - interpret loc: turing_machine_write_replicate j1 j2 . show ?thesis using assms loc.tm3' loc.tps3_def loc.tm3_eq_tm_write_replicate by simp qed subsection ‹Extracting the elements of a pair› text ‹ In Section~\ref{s:tm-basic-pair} we defined a pairing function for strings. For example, $\langle \bbbI\bbbI, \bbbO\bbbO\rangle$ is first mapped to $\bbbI\bbbI\#\bbbO\bbbO$ and ultimately represented as $\bbbO\bbbI\bbbO\bbbI\bbbI\bbbI\bbbO\bbbO\bbbO\bbbO$. A Turing machine that is to compute a function for the argument $\langle \bbbI\bbbI, \bbbO\bbbO\rangle$ would receive as input the symbols \textbf{0101110000}. Typically the TM would then extract the two components \textbf{11} and \textbf{00}. In this section we devise TMs to do just that. As it happens, applying the quaternary alphabet decoding function @{const bindecode} (see Section~\ref{s:tm-quaternary}) to such a symbol sequence gets us halfway to extracting the elements of the pair. For example, decoding \textbf{0101110000} yields @{text "𝟭𝟭♯𝟬𝟬"}, and now the TM only has to locate the @{text ♯}. A Turing machine cannot rely on being given a well-formed pair. After decoding, the symbol sequence might have more or fewer than one @{text ♯} symbol or even @{text "¦"} symbols. The following functions @{term first} and @{term second} are designed to extract the first and second element of a symbol sequence representing a pair, and for other symbol sequences at least allow for an efficient implementation. Implementations will come further down in this section. › definition first :: "symbol list ⇒ symbol list" where "first ys ≡ take (if ∃i<length ys. ys ! i ∈ {¦, ♯} then LEAST i. i < length ys ∧ ys ! i ∈ {¦, ♯} else length ys) ys" definition second :: "symbol list ⇒ symbol list" where "second zs ≡ drop (Suc (length (first zs))) zs" lemma firstD: assumes "∃i<length ys. ys ! i ∈ {¦, ♯}" and "m = (LEAST i. i < length ys ∧ ys ! i ∈ {¦, ♯})" shows "m < length ys" and "ys ! m ∈ {¦, ♯}" and "∀i<m. ys ! i ∉ {¦, ♯}" using LeastI_ex[OF assms(1)] assms(2) by simp_all (use less_trans not_less_Least in blast) lemma firstI: assumes "m < length ys" and "ys ! m ∈ {¦, ♯}" and "∀i<m. ys ! i ∉ {¦, ♯}" shows "(LEAST i. i < length ys ∧ ys ! i ∈ {¦, ♯}) = m" using assms by (metis (mono_tags, lifting) LeastI less_linear not_less_Least) lemma length_first_ex: assumes "∃i<length ys. ys ! i ∈ {¦, ♯}" and "m = (LEAST i. i < length ys ∧ ys ! i ∈ {¦, ♯})" shows "length (first ys) = m" proof - have "m < length ys" using assms firstD(1) by presburger moreover have "first ys = take m ys" using assms first_def by simp ultimately show ?thesis by simp qed lemma first_notex: assumes "¬ (∃i<length ys. ys ! i ∈ {¦, ♯})" shows "first ys = ys" using assms first_def by auto lemma length_first: "length (first ys) ≤ length ys" using length_first_ex first_notex first_def by simp lemma length_second_first: "length (second zs) = length zs - Suc (length (first zs))" using second_def by simp lemma length_second: "length (second zs) ≤ length zs" using second_def by simp text ‹ Our next goal is to show that @{const first} and @{const second} really extract the first and second element of a pair. › lemma bindecode_bitenc: fixes x :: string shows "bindecode (string_to_symbols (bitenc x)) = string_to_symbols x" proof (induction x) case Nil then show ?case using less_2_cases_iff by force next case (Cons a x) have "bitenc (a # x) = bitenc [a] @ bitenc x" by simp then have "string_to_symbols (bitenc (a # x)) = string_to_symbols (bitenc [a] @ bitenc x)" by simp then have "string_to_symbols (bitenc (a # x)) = string_to_symbols (bitenc [a]) @ string_to_symbols (bitenc x)" by simp then have "bindecode (string_to_symbols (bitenc (a # x))) = bindecode (string_to_symbols (bitenc [a]) @ string_to_symbols (bitenc x))" by simp also have "... = bindecode (string_to_symbols (bitenc [a])) @ bindecode (string_to_symbols (bitenc x))" using bindecode_append length_bitenc by (metis (no_types, lifting) dvd_triv_left length_map) also have "... = bindecode (string_to_symbols (bitenc [a])) @ string_to_symbols x" using Cons by simp also have "... = string_to_symbols [a] @ string_to_symbols x" using bindecode_def by simp also have "... = string_to_symbols ([a] @ x)" by simp also have "... = string_to_symbols (a # x)" by simp finally show ?case . qed lemma bindecode_string_pair: fixes x u :: string shows "bindecode ⟨x; u⟩ = string_to_symbols x @ [♯] @ string_to_symbols u" proof - have "bindecode ⟨x; u⟩ = bindecode (string_to_symbols (bitenc x @ [True, True] @ bitenc u))" using string_pair_def by simp also have "... = bindecode (string_to_symbols (bitenc x) @ string_to_symbols [𝕀, 𝕀] @ string_to_symbols (bitenc u))" by simp also have "... = bindecode (string_to_symbols (bitenc x)) @ bindecode (string_to_symbols [𝕀, 𝕀]) @ bindecode (string_to_symbols (bitenc u))" proof - have "even (length (string_to_symbols [True, True]))" by simp moreover have "even (length (string_to_symbols (bitenc y)))" for y by (simp add: length_bitenc) ultimately show ?thesis using bindecode_append length_bindecode length_bitenc by (smt (z3) add_mult_distrib2 add_self_div_2 dvd_triv_left length_append length_map mult_2) qed also have "... = string_to_symbols x @ bindecode (string_to_symbols [𝕀, 𝕀]) @ string_to_symbols u" using bindecode_bitenc by simp also have "... = string_to_symbols x @ [♯] @ string_to_symbols u" using bindecode_def by simp finally show ?thesis . qed lemma first_pair: fixes ys :: "symbol list" and x u :: string assumes "ys = bindecode ⟨x; u⟩" shows "first ys = string_to_symbols x" proof - have ys: "ys = string_to_symbols x @ [♯] @ string_to_symbols u" using bindecode_string_pair assms by simp have bs: "bit_symbols (string_to_symbols x)" by simp have "ys ! (length (string_to_symbols x)) = ♯" using ys by (metis append_Cons nth_append_length) then have ex: "ys ! (length (string_to_symbols x)) ∈ {¦, ♯}" by simp have "(LEAST i. i < length ys ∧ ys ! i ∈ {¦, ♯}) = length (string_to_symbols x)" using ex ys bs by (intro firstI) (simp_all add: nth_append) moreover have "length (string_to_symbols x) < length ys" using ys by simp ultimately have "first ys = take (length (string_to_symbols x)) ys" using ex first_def by auto then show "first ys = string_to_symbols x" using ys by simp qed lemma second_pair: fixes ys :: "symbol list" and x u :: string assumes "ys = bindecode ⟨x; u⟩" shows "second ys = string_to_symbols u" proof - have ys: "ys = string_to_symbols x @ [♯] @ string_to_symbols u" using bindecode_string_pair assms by simp let ?m = "length (string_to_symbols x)" have "length (first ys) = ?m" using assms first_pair by presburger moreover have "drop (Suc ?m) ys = string_to_symbols u" using ys by simp ultimately have "drop (Suc (length (first ys))) ys = string_to_symbols u" by simp then show ?thesis using second_def by simp qed subsubsection ‹A Turing machine for extracting the first element› text ‹ Unlike most other Turing machines, the one in this section is not meant to be reusable, but rather to compute a function, namely the function @{const first}. For this reason there are no tape index parameters. Instead, the encoded pair is expected on the input tape, and the output is written to the output tape. \null › lemma bit_symbols_first: assumes "ys = bindecode (string_to_symbols x)" shows "bit_symbols (first ys)" proof (cases "∃i<length ys. ys ! i ∈ {¦, ♯}") case True define m where "m = (LEAST i. i < length ys ∧ ys ! i ∈ {¦, ♯})" then have m: "m < length ys" "ys ! m ∈ {¦, ♯}" "∀i<m. ys ! i ∉ {¦, ♯}" using firstD[OF True] by blast+ have len: "length (first ys) = m" using length_first_ex[OF True] m_def by simp have "bit_symbols (string_to_symbols x)" by simp then have "∀i<length ys. ys ! i ∈ {2..<6}" using assms bindecode2345 by simp then have "∀i<m. ys ! i ∈ {2..<6}" using m(1) by simp then have "∀i<m. ys ! i ∈ {2..<4}" using m(3) by fastforce then show ?thesis using first_def len by auto next case False then have 1: "∀i<length ys. ys ! i ∉ {¦, ♯}" by simp have "bit_symbols (string_to_symbols x)" by simp then have "∀i<length ys. ys ! i ∈ {2..<6}" using assms bindecode2345 by simp then have "∀i<length ys. ys ! i ∈ {2..<4}" using 1 by fastforce then show ?thesis using False first_notex by auto qed definition tm_first :: machine where "tm_first ≡ tm_right_many {0, 1, 2} ;; tm_bindecode 0 2 ;; tm_cp_until 2 1 {□, ¦, ♯}" lemma tm_first_tm: "G ≥ 6 ⟹ k ≥ 3 ⟹ turing_machine k G tm_first" unfolding tm_first_def using tm_cp_until_tm tm_start_tm tm_bindecode_tm tm_right_many_tm by simp locale turing_machine_fst_pair = fixes k :: nat assumes k: "k ≥ 3" begin definition "tm1 ≡ tm_right_many {0, 1, 2}" definition "tm2 ≡ tm1 ;; tm_bindecode 0 2" definition "tm3 ≡ tm2 ;; tm_cp_until 2 1 {□, ¦, ♯}" lemma tm3_eq_tm_first: "tm3 = tm_first" using tm1_def tm2_def tm3_def tm_first_def by simp context fixes xs :: "symbol list" assumes bs: "bit_symbols xs" begin definition "tps0 ≡ snd (start_config k xs)" lemma lentps [simp]: "length tps0 = k" using tps0_def start_config_length k by simp lemma tps0_0: "tps0 ! 0 = (⌊xs⌋, 0)" using tps0_def start_config_def contents_def by auto lemma tps0_gt_0: "j > 0 ⟹ j < k ⟹ tps0 ! j = (⌊[]⌋, 0)" using tps0_def start_config_def contents_def by auto definition "tps1 ≡ tps0 [0 := (⌊xs⌋, 1), 1 := (⌊[]⌋, 1), 2 := (⌊[]⌋, 1)]" lemma tm1 [transforms_intros]: "transforms tm1 tps0 1 tps1" unfolding tm1_def proof (tform) show "tps1 = map (λj. if j ∈ {0, 1, 2} then tps0 ! j |+| 1 else tps0 ! j) [0..<length tps0]" (is "_ = ?rhs") proof (rule nth_equalityI) show "length tps1 = length ?rhs" using tps0_def tps1_def by simp show "tps1 ! j = ?rhs ! j" if "j < length tps1" for j using that tps0_0 tps0_gt_0 tps1_def by simp qed qed definition "tps2 ≡ tps0 [0 := (⌊xs⌋, 1), 1 := (⌊[]⌋, 1), 2 := (⌊bindecode xs⌋, 1)]" lemma tm2 [transforms_intros]: assumes "ttt = 8 + 3 * length xs" shows "transforms tm2 tps0 ttt tps2" unfolding tm2_def by (tform tps: bs k tps1_def assms tps2_def) definition "tps3 ≡ tps0 [0 := (⌊xs⌋, 1), 1 := (⌊first (bindecode xs)⌋, Suc (length (first (bindecode xs)))), 2 := (⌊bindecode xs⌋, Suc (length (first (bindecode xs))))]" lemma tm3: assumes "ttt = 8 + 3 * length xs + Suc (length (first (bindecode xs)))" shows "transforms tm3 tps0 ttt tps3" unfolding tm3_def proof (tform tps: k tps2_def time: assms) let ?ys = "bindecode xs" have tps2: "tps2 ! 2 = (⌊?ys⌋, 1)" using tps2_def k by simp show "rneigh (tps2 ! 2) {□, ¦, ♯} (length (first ?ys))" proof (cases "∃i<length ?ys. ?ys ! i ∈ {¦, ♯}") case ex5: True define m where "m = (LEAST i. i < length ?ys ∧ ?ys ! i ∈ {¦, ♯})" then have m: "m = length (first ?ys)" using length_first_ex ex5 by simp show ?thesis proof (rule rneighI) have "?ys ! m ∈ {¦, ♯}" using firstD m_def ex5 by blast then show "(tps2 ::: 2) (tps2 :#: 2 + length (first ?ys)) ∈ {□, ¦, ♯}" using m tps2 contents_def by simp show "(tps2 ::: 2) (tps2 :#: 2 + i) ∉ {□, ¦, ♯}" if "i < length (first ?ys)" for i proof - have "m < length ?ys" using ex5 firstD(1) length_first_ex m by blast then have "length (first ?ys) < length ?ys" using m by simp then have "i < length ?ys" using that by simp then have "?ys ! i ≠ 0" using proper_bindecode by fastforce moreover have "?ys ! i ∉ {¦, ♯}" using ex5 firstD(3) length_first_ex that by blast ultimately show ?thesis using Suc_neq_Zero ‹i < length (bindecode xs)› tps2 by simp qed qed next case notex5: False then have ys: "?ys = first ?ys" using first_notex by simp show ?thesis proof (rule rneighI) show "(tps2 ::: 2) (tps2 :#: 2 + length (first ?ys)) ∈ {□, ¦, ♯}" using ys tps2 by simp show "(tps2 ::: 2) (tps2 :#: 2 + i) ∉ {□, ¦, ♯}" if "i < length (first ?ys)" for i using notex5 that ys proper_bindecode contents_inbounds by (metis Suc_leI add_gr_0 diff_Suc_1 fst_conv gr_implies_not0 insert_iff plus_1_eq_Suc snd_conv tps2 zero_less_one) qed qed show "tps3 = tps2[2 := tps2 ! 2 |+| length (first ?ys), 1 := implant (tps2 ! 2) (tps2 ! 1) (length (first ?ys))]" (is "_ = ?tps") proof - have 0: "tps3 ! 0 = ?tps ! 0" using tps2_def tps3_def by simp have 1: "tps3 ! 2 = ?tps ! 2" using tps2_def tps3_def k by simp have lentps2: "length tps2 > 2" using k tps2_def by simp have "implant (tps2 ! 2) (tps2 ! 1) (length (first ?ys)) = (⌊first ?ys⌋, Suc (length (first ?ys)))" proof - have len: "length (first ?ys) ≤ length ?ys" using first_def by simp have "