# Theory Two_Four_Symbols

section βΉMapping between a binary and a quaternary alphabet\label{s:tm-quaternary}βΊ

theory Two_Four_Symbols
imports Arithmetic
begin

text βΉ
Functions are defined over bit strings. For Turing machines these bits are
represented by the symbols \textbf{0} and \textbf{1}. Sometimes we want a TM to
receive a pair of bit strings or output a list of numbers. Or we might want the
TM to interpret the input as a list of lists of numbers. All these objects can
naturally be represented over a four-symbol (quaternary) alphabet, as we have
seen for pairs in Section~\ref{s:tm-basic-pair} and for the lists in
Sections~\ref{s:tm-numlist} and~\ref{s:tm-numlistlist}.

To accommodate the aforementioned use cases, we define a straightforward mapping
between the binary alphabet \textbf{01} and the quaternary alphabet @{text
"π¬π­Β¦β―"} and devise Turing machines to encode and decode symbol sequences.
βΊ

subsection βΉEncoding and decoding\label{s:tm-quaternary-encoding}βΊ

text βΉ
The encoding maps:

\begin{tabular}{lcl}
@{text π¬} & $\mapsto$ & @{text "π¬π¬"}\\
@{text π­} & $\mapsto$ & @{text "π¬π­"}\\
@{text "Β¦"} & $\mapsto$ & @{text "π­π¬"}\\
@{text β―} & $\mapsto$ & @{text "π­π­"}\\
\end{tabular}
βΊ

text βΉ
For example, the list $[6,0,1]$ is represented by the symbols @{text
"π¬π­π­Β¦Β¦π­Β¦"}, which is encoded as @{text "π¬π¬π¬π­π¬π­π­π¬π­π¬π¬π­π­π¬"}.
Pairing this sequence with the symbol sequence @{text "π¬π­π­π¬"} yields @{text
"π¬π¬π¬π­π¬π­π­π¬π­π¬π¬π­π­π¬β―π¬π­π­π¬"}, which is encoded as @{text
"π¬π¬π¬π¬π¬π¬π¬π­π¬π¬π¬π­π¬π­π¬π¬π¬π­π¬π¬π¬π¬π¬π­π¬π­π¬π¬π­π­π¬π¬π¬π­π¬π­π¬π¬"}.

\null
βΊ

definition binencode :: "symbol list β symbol list" where
"binencode ys β‘ concat (map (Ξ»y. [tosym ((y - 2) div 2), tosym ((y - 2) mod 2)]) ys)"

lemma length_binencode [simp]: "length (binencode ys) = 2 * length ys"
using binencode_def by (induction ys) simp_all

lemma binencode_snoc:
"binencode (zs @ [π¬]) = binencode zs @ [π¬, π¬]"
"binencode (zs @ [π­]) = binencode zs @ [π¬, π­]"
"binencode (zs @ [Β¦]) = binencode zs @ [π­, π¬]"
"binencode (zs @ [β―]) = binencode zs @ [π­, π­]"
using binencode_def by simp_all

lemma binencode_at_even:
assumes "i < length ys"
shows "binencode ys ! (2 * i) = 2 + (ys ! i - 2) div 2"
using assms
proof (induction ys arbitrary: i)
case Nil
then show ?case
by simp
next
case (Cons y ys)
have *: "binencode (y # ys) = [2 + (y - 2) div 2, 2 + (y - 2) mod 2] @ binencode ys"
using binencode_def by simp
show ?case
proof (cases "i = 0")
case True
then show ?thesis
using * by simp
next
case False
then have "binencode (y # ys) ! (2 * i) = binencode ys ! (2 * i - 2)"
using *
by (metis One_nat_def length_Cons less_one list.size(3) mult_2 nat_mult_less_cancel_disj
nth_append numerals(2) plus_1_eq_Suc)
also have "... = binencode ys ! (2 * (i - 1))"
using False by (simp add: right_diff_distrib')
also have "... = 2 + (ys ! (i - 1) - 2) div 2"
using False Cons by simp
also have "... = 2 + ((y # ys) ! i - 2) div 2"
using False by simp
finally show ?thesis .
qed
qed

lemma binencode_at_odd:
assumes "i < length ys"
shows "binencode ys ! (2 * i + 1) = 2 + (ys ! i - 2) mod 2"
using assms
proof (induction ys arbitrary: i)
case Nil
then show ?case
by simp
next
case (Cons y ys)
have *: "binencode (y # ys) = [2 + (y - 2) div 2, 2 + (y - 2) mod 2] @ binencode ys"
using binencode_def by simp
show ?case
proof (cases "i = 0")
case True
then show ?thesis
using * by simp
next
case False
then have "binencode (y # ys) ! (2 * i + 1) = binencode ys ! (2 * i + 1 - 2)"
using * by simp
also have "... = binencode ys ! (2 * (i - 1) + 1)"
using False
also have "... = 2 + (ys ! (i - 1) - 2) mod 2"
using False Cons by simp
also have "... = 2 + ((y # ys) ! i - 2) mod 2"
using False by simp
finally show ?thesis .
qed
qed

text βΉ
While @{const binencode} is defined for arbitrary symbol sequences, we only
consider sequences over @{text "π¬π­Β¦β―"} to be binencodable.
βΊ

abbreviation binencodable :: "symbol list β bool" where
"binencodable ys β‘ βi<length ys. 2 β€ ys ! i β§ ys ! i < 6"

lemma binencodable_append:
assumes "binencodable xs" and "binencodable ys"
shows "binencodable (xs @ ys)"
using assms prop_list_append by (simp add: nth_append)

lemma bit_symbols_binencode:
assumes "binencodable ys"
shows "bit_symbols (binencode ys)"
proof -
have "2 β€ binencode ys ! i β§ binencode ys ! i β€ 3" if "i < length (binencode ys)" for i
proof (cases "even i")
case True
then have len: "i div 2 < length ys"
using length_binencode that by simp
moreover have "2 * (i div 2) = i"
using True by simp
ultimately have "binencode ys ! i = 2 + (ys ! (i div 2) - 2) div 2"
using binencode_at_even[of "i div 2" ys] by simp
moreover have "2 β€ ys ! (i div 2) β§ ys ! (i div 2) < 6"
using len assms by simp
ultimately show ?thesis
by auto
next
case False
then have len: "i div 2 < length ys"
using length_binencode that by simp
moreover have "2 * (i div 2) + 1 = i"
using False by simp
ultimately have "binencode ys ! i = 2 + (ys ! (i div 2) - 2) mod 2"
using binencode_at_odd[of "i div 2" ys] by simp
moreover have "2 β€ ys ! (i div 2) β§ ys ! (i div 2) < 6"
using len assms by simp
ultimately show ?thesis
by simp
qed
then show ?thesis
by fastforce
qed

text βΉ
An encoded symbol sequence is of even length. When decoding a symbol sequence of
odd length, we ignore the last symbol. For example, @{text "π¬π­π­π­π¬π¬"} and
@{text "π¬π­π­π­π¬π¬π­"} are both decoded to @{text "π­β―π¬"}.

The bit symbol sequence @{term "[a, b]"} is decoded to this symbol:
βΊ

abbreviation decsym :: "symbol β symbol β symbol" where
"decsym a b β‘ tosym (2 * todigit a + todigit b)"

definition bindecode :: "symbol list β symbol list" where
"bindecode zs β‘ map (Ξ»i. decsym (zs ! (2 * i)) (zs ! (Suc (2 * i)))) [0..<length zs div 2]"

lemma length_bindecode [simp]: "length (bindecode zs) = length zs div 2"
using bindecode_def by simp

lemma bindecode_at:
assumes "i < length zs div 2"
shows "bindecode zs ! i = decsym (zs ! (2 * i)) (zs ! (Suc (2 * i)))"
using assms bindecode_def by simp

lemma proper_bindecode: "proper_symbols (bindecode zs)"
using bindecode_at by simp

lemma bindecode2345:
assumes "bit_symbols zs"
shows "βi<length (bindecode zs). bindecode zs ! i β {2..<6}"
using assms bindecode_at by simp

lemma bindecode_odd:
assumes "length zs = 2 * n + 1"
shows "bindecode zs = bindecode (take (2 * n) zs)"
proof -
have 1: "take (2 * n) zs ! (2 * i) = zs ! (2 * i)" if "i < n" for i
using assms that by simp
have 2: "take (2 * n) zs ! (Suc (2 * i)) = zs ! (Suc (2 * i))" if "i < n" for i
using assms that by simp
have "bindecode (take (2 * n) zs) =
map (Ξ»i. decsym ((take (2 * n) zs) ! (2 * i)) ((take (2 * n) zs) ! (Suc (2 * i)))) [0..<length (take (2 * n) zs) div 2]"
using bindecode_def by simp
also have "... = map (Ξ»i. decsym ((take (2 * n) zs) ! (2 * i)) ((take (2 * n) zs) ! (Suc (2 * i)))) [0..<n]"
using assms by (simp add: min_absorb2)
also have "... = map (Ξ»i. decsym (zs ! (2 * i)) (zs ! (Suc (2 * i)))) [0..<n]"
by simp
also have "... = map (Ξ»i. decsym (zs ! (2 * i)) (zs ! (Suc (2 * i)))) [0..<length zs div 2]"
using assms by simp
also have "... = bindecode zs"
using bindecode_def by simp
finally show ?thesis
by simp
qed

lemma bindecode_append:
assumes "even (length ys)" and "even (length zs)"
shows "bindecode (ys @ zs) = bindecode ys @ bindecode zs"
(is "?lhs = ?rhs")
proof (rule nth_equalityI)
show 1: "length ?lhs = length ?rhs"
using assms by simp
show "?lhs ! i = ?rhs ! i" if "i < length ?lhs" for i
proof (cases "i < length ys div 2")
case True
have "?lhs ! i = decsym ((ys @ zs) ! (2 * i)) ((ys @ zs) ! (Suc (2 * i)))"
using that bindecode_at length_bindecode by simp
also have "... = decsym (ys ! (2 * i)) ((ys @ zs) ! (Suc (2 * i)))"
using True assms(1)
by (metis Suc_1 dvd_mult_div_cancel nat_mult_less_cancel_disj nth_append zero_less_Suc)
also have "... = decsym (ys ! (2 * i)) (ys ! (Suc (2 * i)))"
using True assms(1)
by (metis Suc_1 Suc_lessI Suc_mult_less_cancel1 dvd_mult_div_cancel dvd_triv_left even_Suc nth_append)
also have "... = bindecode ys ! i"
using True bindecode_at by simp
also have "... = ?rhs ! i"
finally show ?thesis .
next
case False
let ?l = "length ys"
have l: "length (bindecode ys) = ?l div 2"
by simp
have "?lhs ! i = decsym ((ys @ zs) ! (2 * i)) ((ys @ zs) ! (Suc (2 * i)))"
using that bindecode_at length_bindecode by simp
also have "... = decsym (zs ! (2 * i - ?l)) ((ys @ zs) ! (Suc (2 * i)))"
using False assms
by (metis dvd_mult_div_cancel nat_mult_less_cancel_disj nth_append)
also have "... = decsym (zs ! (2 * i - ?l)) (zs ! (Suc (2 * i) - ?l))"
using False assms
by (metis (no_types, lifting) Suc_eq_plus1 add_lessD1 dvd_mult_div_cancel nat_mult_less_cancel_disj nth_append)
also have "... = bindecode zs ! (i - ?l div 2)"
using False bindecode_at that assms 1
dvd_mult_div_cancel le_less_linear mult_2 plus_1_eq_Suc right_diff_distrib')
also have "... = (bindecode ys @ bindecode zs) ! i"
using l False by (simp add: nth_append)
finally show ?thesis .
qed
qed

lemma bindecode_take_snoc:
assumes "i < length zs div 2"
shows "bindecode (take (2 * i) zs) @ [decsym (zs ! (2*i)) (zs ! (Suc (2*i)))] = bindecode (take (2 * Suc i) zs)"
proof -
let ?ys = "take (2 * i) zs"
let ?zs = "take 2 (drop (2 * i) zs)"
have "?zs ! 0 = zs ! (2 * i)"
using assms by simp
moreover have "?zs ! 1 = zs ! (Suc (2 * i))"
using assms by simp
moreover have "length ?zs = 2"
using assms by simp
ultimately have "?zs = [zs ! (2 * i), zs ! (Suc (2 * i))]"
by (metis (no_types, lifting) Cons_nth_drop_Suc One_nat_def Suc_1 diff_Suc_1 drop0
length_0_conv length_drop lessI list.inject zero_less_Suc)
moreover have "take (2 * i + 2) zs = ?ys @ ?zs"
ultimately have "take (2 * Suc i) zs = ?ys @ [zs ! (2 * i), zs ! (Suc (2 * i))]"
by simp
moreover have "even (length ?ys)"
proof -
have "length ?ys = 2 * i"
using assms by simp
then show ?thesis
by simp
qed
ultimately have "bindecode (take (2 * Suc i) zs) = bindecode ?ys @ bindecode [zs ! (2 * i), zs ! (Suc (2 * i))]"
using bindecode_append by simp
then show ?thesis
using bindecode_def by simp
qed

lemma bindecode_encode:
assumes "binencodable ys"
shows "bindecode (binencode ys) = ys"
proof (rule nth_equalityI)
show 1: "length (bindecode (binencode ys)) = length ys"
using binencode_def bindecode_def by fastforce
show "bindecode (binencode ys) ! i = ys ! i" if "i < length (bindecode (binencode ys))" for i
proof -
have len: "i < length ys"
using that 1 by simp
let ?zs = "binencode ys"
have "i < length ?zs div 2"
using len by simp
then have "bindecode ?zs ! i = decsym (?zs ! (2 * i)) (?zs ! (Suc (2 * i)))"
using bindecode_def by simp
also have "... = decsym (2 + (ys ! i - 2) div 2) (2 + (ys ! i - 2) mod 2)"
using binencode_at_even[OF len] binencode_at_odd[OF len] by simp
also have "... = ys ! i"
proof -
have "ys ! i = 2 β¨ ys ! i = 3 β¨ ys ! i = 4 β¨ ys ! i = 5"
using assms len
less_Suc_eq numeral_3_eq_3 numeral_Bit0 verit_comp_simplify1(3))
then show ?thesis
by auto
qed
finally show "bindecode ?zs ! i = ys ! i" .
qed
qed

lemma binencode_decode:
assumes "bit_symbols zs" and "even (length zs)"
shows "binencode (bindecode zs) = zs"
proof (rule nth_equalityI)
let ?ys = "bindecode zs"
show 1: "length (binencode ?ys) = length zs"
using binencode_def bindecode_def assms(2) by fastforce
show "binencode ?ys ! i = zs ! i" if "i < length (binencode ?ys)" for i
proof -
have ilen: "i < length zs"
using 1 that by simp
show ?thesis
proof (cases "even i")
case True
let ?j = "i div 2"
have jlen: "?j < length zs div 2"
using ilen by (simp add: assms(2) less_mult_imp_div_less)
then have ysj: "?ys ! ?j = decsym (zs ! (2 * ?j)) (zs ! (Suc (2 * ?j)))"
using bindecode_def by simp
have "binencode ?ys ! i = binencode ?ys ! (2 * ?j)"
also have "... = 2 + (?ys ! ?j - 2) div 2"
using binencode_at_even jlen by simp
also have "... = zs ! (2 * ?j)"
using ysj True assms(1) ilen by auto
also have "... = zs ! i"
using True by simp
finally show "binencode ?ys ! i = zs ! i" .
next
case False
let ?j = "i div 2"
have jlen: "?j < length zs div 2"
using ilen by (simp add: assms(2) less_mult_imp_div_less)
then have ysj: "?ys ! ?j = decsym (zs ! (2 * ?j)) (zs ! (Suc (2 * ?j)))"
using bindecode_def by simp
have "binencode ?ys ! i = binencode ?ys ! (2 * ?j + 1)"
also have "... = 2 + (?ys ! ?j - 2) mod 2"
using binencode_at_odd jlen by simp
also have "... = zs ! (2 * ?j + 1)"
using ysj False assms(1) ilen by auto
also have "... = zs ! i"
using False by simp
finally show "binencode ?ys ! i = zs ! i" .
qed
qed
qed

lemma binencode_inj:
assumes "binencodable xs" and "binencodable ys" and "binencode xs = binencode ys"
shows "xs = ys"
using assms bindecode_encode by metis

subsection βΉTuring machines for encoding and decodingβΊ

text βΉ
The next Turing machine implements @{const binencode} for @{const binencodable}
symbol sequences. It expects a symbol sequence @{term zs} on tape $j_1$ and
writes @{term "binencode zs"} to tape $j_2$.
βΊ

definition tm_binencode :: "tapeidx β tapeidx β machine" where
"tm_binencode j1 j2 β‘
WHILE [] ; Ξ»rs. rs ! j1 β  β‘ DO
IF Ξ»rs. rs ! j1 = π¬ THEN
tm_print j2 [π¬, π¬]
ELSE
IF Ξ»rs. rs ! j1 = π­ THEN
tm_print j2 [π¬, π­]
ELSE
IF Ξ»rs. rs ! j1 = Β¦ THEN
tm_print j2 [π­, π¬]
ELSE
tm_print j2 [π­, π­]
ENDIF
ENDIF
ENDIF ;;
tm_right j1
DONE"

lemma tm_binencode_tm:
assumes "k β₯ 2" and "G β₯ 4" and "j1 < k" and "j2 < k" and "0 < j2"
shows "turing_machine k G (tm_binencode j1 j2)"
proof -
have *: "symbols_lt G [π¬, π¬]" "symbols_lt G [π¬, π­]" "symbols_lt G [π­, π¬]" "symbols_lt G [π­, π­]"
using assms(2) by (simp_all add: nth_Cons')
then have "turing_machine k G (tm_print j2 [π¬, π¬])"
using tm_print_tm[OF assms(5,4,2)] assms by blast
moreover have "turing_machine k G (tm_print j2 [π¬, π­])"
using * tm_print_tm[OF assms(5,4,2)] assms by blast
moreover have "turing_machine k G (tm_print j2 [π­, π¬])"
using * tm_print_tm[OF assms(5,4,2)] assms by blast
moreover have "turing_machine k G (tm_print j2 [π­, π­])"
using * tm_print_tm[OF assms(5,4,2)] assms by blast
ultimately show ?thesis
unfolding tm_binencode_def
using turing_machine_loop_turing_machine Nil_tm turing_machine_branch_turing_machine tm_right_tm assms
by simp
qed

locale turing_machine_binencode =
fixes j1 j2 :: tapeidx
begin

definition "tm1 β‘ IF Ξ»rs. rs ! j1 = Β¦ THEN tm_print j2 [π­, π¬] ELSE tm_print j2 [π­, π­] ENDIF"
definition "tm2 β‘ IF Ξ»rs. rs ! j1 = π­ THEN tm_print j2 [π¬, π­] ELSE tm1 ENDIF"
definition "tm3 β‘ IF Ξ»rs. rs ! j1 = π¬ THEN tm_print j2 [π¬, π¬] ELSE tm2 ENDIF"
definition "tm4 β‘ tm3 ;; tm_right j1"
definition "tm5 β‘ WHILE [] ; Ξ»rs. rs ! j1 β  β‘ DO tm4 DONE"

lemma tm5_eq_tm_binencode: "tm5 = tm_binencode j1 j2"
using tm5_def tm4_def tm3_def tm2_def tm1_def tm_binencode_def by simp

context
fixes k :: nat and tps0 :: "tape list" and zs :: "symbol list"
assumes jk: "k = length tps0" "j1 β  j2" "0 < j2" "j1 < k" "j2 < k"
assumes zs: "binencodable zs"
assumes tps0:
"tps0 ! j1 = (βzsβ, 1)"
"tps0 ! j2 = (β[]β, 1)"
begin

definition tpsL :: "nat β tape list" where
"tpsL t β‘ tps0
[j1 := (βzsβ, Suc t),
j2 := (βbinencode (take t zs)β, Suc (2 * t))]"

lemma tpsL_0: "tpsL 0 = tps0"
unfolding tpsL_def using tps0 jk
by (metis One_nat_def length_0_conv length_binencode list_update_id mult_0_right take0)

definition tpsL1 :: "nat β tape list" where
"tpsL1 t β‘ tps0
[j1 := (βzsβ, Suc t),
j2 := (βbinencode (take (Suc t) zs)β, Suc (2 * t) + 2)]"

assumes "t < length zs"
shows "read (tpsL t) ! j1 = zs ! t"
proof -
have "tpsL t ! j1 = (βzsβ, Suc t)"
using tpsL_def jk by simp
moreover have "j1 < length (tpsL t)"
using tpsL_def jk by simp
ultimately show "read (tpsL t) ! j1 = zs ! t"
by (metis Suc_leI contents_inbounds diff_Suc_1 fst_conv snd_conv zero_less_Suc)
qed

lemma tm1 [transforms_intros]:
assumes "t < length zs" and "zs ! t = Β¦ β¨ zs ! t = β―"
shows "transforms tm1 (tpsL t) 4 (tpsL1 t)"
unfolding tm1_def
proof (tform tps: jk tpsL_def)
have 1: "tpsL t ! j2 = (βbinencode (take t zs)β, Suc (2 * t))"
using tpsL_def jk by simp
have 2: "length (binencode (take t zs)) = 2 * t"
using assms(1) by simp
have "inscribe (tpsL t ! j2) [π­, π¬] = (βbinencode (take t zs) @ [π­, π¬]β, Suc (2 * t) + 2)"
using inscribe_contents 1 2
by (metis (no_types, lifting) One_nat_def Suc_1 Suc_eq_plus1 add_Suc_shift list.size(3) list.size(4))
moreover have "binencode (take t zs) @ [π­, π¬] = binencode (take (Suc t) zs)" if "zs ! t = Β¦"
using that assms(1) binencode_snoc by (metis take_Suc_conv_app_nth)
ultimately have 5: "inscribe (tpsL t ! j2) [π­, π¬] = (βbinencode (take (Suc t) zs)β, Suc (2 * t) + 2)"
if "zs ! t = Β¦"
using that by simp
have "inscribe (tpsL t ! j2) [π­, π­] = (βbinencode (take t zs) @ [π­, π­]β, Suc (2 * t) + 2)"
using inscribe_contents 1 2
by (metis (no_types, lifting) One_nat_def Suc_1 Suc_eq_plus1 add_Suc_shift list.size(3) list.size(4))
moreover have "binencode (take t zs) @ [π­, π­] = binencode (take (Suc t) zs)" if "zs ! t = 5"
using that assms(1) binencode_snoc by (metis take_Suc_conv_app_nth)
ultimately have 6: "inscribe (tpsL t ! j2) [π­, π­] = (βbinencode (take (Suc t) zs)β, Suc (2 * t) + 2)"
if "zs ! t = β―"
using that by simp
have 7: "tpsL1 t = (tpsL t)[j2 := (βbinencode (take (Suc t) zs)β, Suc (2 * t) + 2)]"
unfolding tpsL1_def tpsL_def by (simp only: list_update_overwrite)
then have 8: "tpsL1 t = (tpsL t)[j2 := inscribe (tpsL t ! j2) [π­, π¬]]" if "zs ! t = Β¦"
using that 5 by simp
have 9: "tpsL1 t = (tpsL t)[j2 := inscribe (tpsL t ! j2) [π­, π­]]" if "zs ! t = β―"
using that 6 7 by simp
show "read (tpsL t) ! j1 = Β¦ βΉ
tpsL1 t = (tpsL t)[j2 := inscribe (tpsL t ! j2) [π­, π¬]]"
using read_tpsL[OF assms(1)] 8 by simp
show "read (tpsL t) ! j1 β  Β¦ βΉ
tpsL1 t = (tpsL t)[j2 := inscribe (tpsL t ! j2) [π­, π­]]"
using read_tpsL[OF assms(1)] 9 assms(2) by simp
qed

lemma tm2 [transforms_intros]:
assumes "t < length zs" and "zs ! t = Β¦ β¨ zs ! t = β― β¨ zs ! t = π­"
shows "transforms tm2 (tpsL t) 5 (tpsL1 t)"
unfolding tm2_def
proof (tform tps: tpsL_def jk assms(1))
have 1: "tpsL t ! j2 = (βbinencode (take t zs)β, Suc (2 * t))"
using tpsL_def jk by simp
have 2: "length (binencode (take t zs)) = 2 * t"
using assms(1) by simp
show "read (tpsL t) ! j1 β  π­ βΉ zs ! t = Β¦ β¨ zs ! t = β―"
using read_tpsL[OF assms(1)] assms(2) by simp
show "tpsL1 t = (tpsL t)[j2 := inscribe (tpsL t ! j2) [π¬, π­]]" if "read (tpsL t) ! j1 = π­"
proof -
have *: "zs ! t = π­"
using read_tpsL[OF assms(1)] that by simp
have "inscribe (tpsL t ! j2) [π¬, π­] = (βbinencode (take t zs) @ [2, π­]β, Suc (2 * t) + 2)"
using inscribe_contents 1 2
by (metis (no_types, lifting) One_nat_def Suc_1 Suc_eq_plus1 add_Suc_shift list.size(3) list.size(4))
moreover have "binencode (take t zs) @ [π¬, π­] = binencode (take (Suc t) zs)"
using * assms(1) binencode_snoc by (metis take_Suc_conv_app_nth)
ultimately have "inscribe (tpsL t ! j2) [π¬, π­] = (βbinencode (take (Suc t) zs)β, Suc (2 * t) + 2)"
by simp
moreover have "tpsL1 t = (tpsL t)[j2 := (βbinencode (take (Suc t) zs)β, Suc (2 * t) + 2)]"
unfolding tpsL1_def tpsL_def by (simp only: list_update_overwrite)
ultimately show "tpsL1 t = (tpsL t)[j2 := inscribe (tpsL t ! j2) [π¬, π­]]"
using that by simp
qed
qed

lemma tm3 [transforms_intros]:
assumes "t < length zs"
shows "transforms tm3 (tpsL t) 6 (tpsL1 t)"
unfolding tm3_def
proof (tform tps: jk assms tpsL_def)
have 1: "tpsL t ! j2 = (βbinencode (take t zs)β, Suc (2 * t))"
using tpsL_def jk by simp
have 2: "length (binencode (take t zs)) = 2 * t"
using assms by simp
show "read (tpsL t) ! j1 β  π¬ βΉ zs ! t = Β¦ β¨ zs ! t = β― β¨ zs ! t = π­"
using assms zs read_tpsL by auto
show "tpsL1 t = (tpsL t)[j2 := inscribe (tpsL t ! j2) [π¬, π¬]]" if "read (tpsL t) ! j1 = π¬"
proof -
have *: "zs ! t = π¬"
using read_tpsL[OF assms] that by simp
have "inscribe (tpsL t ! j2) [π¬, π¬] = (βbinencode (take t zs) @ [π¬, π¬]β, Suc (2 * t) + 2)"
using inscribe_contents 1 2
by (metis (no_types, lifting) One_nat_def Suc_1 Suc_eq_plus1 add_Suc_shift list.size(3) list.size(4))
moreover have "binencode (take t zs) @ [π¬, π¬] = binencode (take (Suc t) zs)"
using * assms binencode_snoc by (metis take_Suc_conv_app_nth)
ultimately have "inscribe (tpsL t ! j2) [π¬, π¬] = (βbinencode (take (Suc t) zs)β, Suc (2 * t) + 2)"
by simp
moreover have "tpsL1 t = (tpsL t)[j2 := (βbinencode (take (Suc t) zs)β, Suc (2 * t) + 2)]"
unfolding tpsL1_def tpsL_def by (simp only: list_update_overwrite)
ultimately show "tpsL1 t = (tpsL t)[j2 := inscribe (tpsL t ! j2) [π¬, π¬]]"
using that by simp
qed
qed

lemma tm4 [transforms_intros]:
assumes "t < length zs"
shows "transforms tm4 (tpsL t) 7 (tpsL (Suc t))"
unfolding tm4_def
proof (tform tps: assms tpsL1_def jk)
have *: "tpsL1 t ! j1 = (βzsβ, Suc t)"
using tpsL1_def jk by simp
show "tpsL (Suc t) = (tpsL1 t)[j1 := tpsL1 t ! j1 |+| 1]"
using tpsL_def tpsL1_def using jk * by (auto simp add: list_update_swap[of _ j1])
qed

lemma tm5:
assumes "ttt = 9 * length zs + 1"
shows "transforms tm5 (tpsL 0) ttt (tpsL (length zs))"
unfolding tm5_def
proof (tform)
show "βt. t < length zs βΉ read (tpsL t) ! j1 β  β‘"
show "Β¬ read (tpsL (length zs)) ! j1 β  β‘"
proof -
have "tpsL (length zs) ! j1 = (βzsβ, Suc (length zs))"
using tpsL_def jk by simp
moreover have "j1 < length (tpsL (length zs))"
using tpsL_def jk by simp
ultimately have "read (tpsL (length zs)) ! j1 = tape_read (βzsβ, Suc (length zs))"
also have "... = β‘"
using contents_outofbounds by simp
finally show ?thesis
by simp
qed
show "length zs * (7 + 2) + 1 β€ ttt"
using assms by simp
qed

lemma tpsL: "tpsL (length zs) = tps0
[j1 := (βzsβ, Suc (length zs)),
j2 := (βbinencode zsβ, Suc (2 * (length zs)))]"
unfolding tpsL_def using tps0 jk by simp

lemma tm5':
assumes "ttt = 9 * length zs + 1"
shows "transforms tm5 tps0 ttt (tpsL (length zs))"
using assms tm5 tpsL_0 by simp

end

end  (* locale turing_machine_binencode *)

lemma transforms_tm_binencodeI [transforms_intros]:
fixes j1 j2 :: tapeidx
fixes tps tps' :: "tape list" and ttt k :: nat and zs :: "symbol list"
assumes "k = length tps" "j1 β  j2" "0 < j2" "j1 < k" "j2 < k"
and "binencodable zs"
assumes
"tps ! j1 = (βzsβ, 1)"
"tps ! j2 = (β[]β, 1)"
assumes "ttt = 9 * length zs + 1"
assumes "tps' β‘ tps
[j1 := (βzsβ, Suc (length zs)),
j2 := (βbinencode zsβ, Suc (2 * (length zs)))]"
shows "transforms (tm_binencode j1 j2) tps ttt tps'"
proof -
interpret loc: turing_machine_binencode j1 j2 .
show ?thesis
using assms loc.tm5' loc.tm5_eq_tm_binencode loc.tpsL by simp
qed

text βΉ
The next command reads chunks of two symbols over @{text "π¬π­"} from one tape
and writes to another tape the corresponding symbol over @{text "π¬π­Β¦β―"}.  The
first symbol of each chunk is memorized on the last tape.  If the end of the
input (that is, a blank symbol) is encountered, the command stops without
writing another symbol.
βΊ

definition cmd_bindec :: "tapeidx β tapeidx β command" where
"cmd_bindec j1 j2 rs β‘
if rs ! j1 = 0 then (1, map (Ξ»z. (z, Stay)) rs)
else (0,
map (Ξ»i.
if last rs = βΉ
then if i = j1 then (rs ! i, Right)
else if i = j2 then (rs ! i, Stay)
else if i = length rs - 1 then (tosym (todigit (rs ! j1)), Stay)
else (rs ! i, Stay)
else if i = j1 then (rs ! i, Right)
else if i = j2 then (decsym (last rs) (rs ! j1), Right)
else if i = length rs - 1 then (1, Stay)
else (rs ! i, Stay))
[0..<length rs])"

text βΉ
The Turing machine performing the decoding:
βΊ

definition tm_bindec :: "tapeidx β tapeidx β machine" where
"tm_bindec j1 j2 = [cmd_bindec j1 j2]"

context
fixes j1 j2 :: tapeidx and k :: nat
assumes j_less: "j1 < k" "j2 < k"
and j_gt: "0 < j2"
begin

lemma turing_command_bindec:
assumes "G β₯ 6"
shows "turing_command (Suc k) 1 G (cmd_bindec j1 j2)"
proof
show "βgs. length gs = Suc k βΉ length ([!!] cmd_bindec j1 j2 gs) = length gs"
using cmd_bindec_def by simp
show "cmd_bindec j1 j2 gs [.] j < G"
if "length gs = Suc k" "βi. i < length gs βΉ gs ! i < G" "j < length gs"
for gs j
proof (cases "gs ! j1 = β‘")
case True
then show ?thesis
using that cmd_bindec_def by simp
next
case else: False
show ?thesis
proof (cases "last gs = βΉ")
case True
then have "snd (cmd_bindec j1 j2 gs) = map (Ξ»i.
if i = j1 then (gs ! i, Right)
else if i = j2 then (gs ! i, Stay)
else if i = length gs - 1 then (todigit (gs ! j1) + 2, Stay)
else (gs ! i, Stay)) [0..<length gs]"
using cmd_bindec_def else by simp
then have "cmd_bindec j1 j2 gs [!] j =
(if j = j1 then (gs ! j, Right)
else if j = j2 then (gs ! j, Stay)
else if j = length gs - 1 then (todigit (gs ! j1) + 2, Stay)
else (gs ! j, Stay))"
using that(3) by simp
then have "cmd_bindec j1 j2 gs [.] j =
(if j = j1 then gs ! j
else if j = j2 then gs ! j
else if j = length gs - 1 then todigit (gs ! j1) + 2
else gs ! j)"
by simp
then show ?thesis
using that assms by simp
next
case False
then have "snd (cmd_bindec j1 j2 gs) = map (Ξ»i.
if i = j1 then (gs ! i, Right)
else if i = j2 then (2 * todigit (last gs) + todigit (gs ! j1) + 2, Right)
else if i = length gs - 1 then (1, Stay)
else (gs ! i, Stay)) [0..<length gs]"
using cmd_bindec_def else by simp
then have "cmd_bindec j1 j2 gs [!] j =
(if j = j1 then (gs ! j, Right)
else if j = j2 then (2 * todigit (last gs) + todigit (gs ! j1) + 2, Right)
else if j = length gs - 1 then (1, Stay)
else (gs ! j, Stay))"
using that(3) by simp
then have "cmd_bindec j1 j2 gs [.] j =
(if j = j1 then gs ! j
else if j = j2 then 2 * todigit (last gs) + todigit (gs ! j1) + 2
else if j = length gs - 1 then 1
else gs ! j)"
by simp
moreover have "last gs < G"
using that assms
by (metis add_lessD1 diff_less last_conv_nth length_greater_0_conv less_numeral_extra(1)
less_numeral_extra(4) list.size(3) plus_1_eq_Suc)
ultimately show ?thesis
using that assms by simp
qed
qed
show "cmd_bindec j1 j2 gs [.] 0 = gs ! 0" if "length gs = Suc k" "0 < Suc k" for gs
proof (cases "last gs = 1")
case True
moreover have "0 < length gs" "0 β  length gs - 1"
using that j_less by simp_all
ultimately show ?thesis
using cmd_bindec_def by simp
next
case False
moreover have "0 < length gs" "0 β  j2" "0 β  length gs - 1"
using that j_gt j_less by simp_all
ultimately show ?thesis
using cmd_bindec_def by simp
qed
show "βgs. length gs = Suc k βΉ [*] (cmd_bindec j1 j2 gs) β€ 1"
using cmd_bindec_def by simp
qed

lemma tm_bindec_tm: "G β₯ 6 βΉ turing_machine (Suc k) G (tm_bindec j1 j2)"
unfolding tm_bindec_def using j_less(2) j_gt turing_command_bindec cmd_bindec_def by auto

context
fixes tps :: "tape list" and zs :: "symbol list"
assumes j1_neq: "j1 β  j2"
and lentps: "Suc k = length tps"
and bs: "bit_symbols zs"
begin

lemma sem_cmd_bindec_gt:
assumes "tps ! j1 = (βzsβ, i)"
and "i > length zs"
shows "sem (cmd_bindec j1 j2) (0, tps) = (1, tps)"
proof (rule semI)
show "proper_command (Suc k) (cmd_bindec j1 j2)"
using cmd_bindec_def by simp
show "length tps = Suc k"
using lentps by simp
show "length tps = Suc k"
using lentps by simp
have "read tps ! j1 = β‘"
using assms by (metis contents_outofbounds fst_conv j_less(1) lentps less_Suc_eq snd_conv tapes_at_read')
moreover from this show "fst (cmd_bindec j1 j2 (read tps)) = 1"
ultimately show "βj. j < Suc k βΉ act (cmd_bindec j1 j2 (read tps) [!] j) (tps ! j) = tps ! j"
using assms cmd_bindec_def act_Stay lentps read_length by simp
qed

lemma sem_cmd_bindec_1:
assumes "tps ! k = ββΉβ"
and "tps ! j1 = (βzsβ, i)"
and "i > 0"
and "i β€ length zs"
and "tps' = tps [j1 := tps ! j1 |+| 1, k := βtodigit (tps :.: j1) + 2β]"
shows "sem (cmd_bindec j1 j2) (0, tps) = (0, tps')"
proof (rule semI)
show "proper_command (Suc k) (cmd_bindec j1 j2)"
using cmd_bindec_def by simp
show "length tps = Suc k"
using lentps by simp
show "length tps' = Suc k"
using lentps assms(5) by simp
using assms(2,3,4) bs j_less(1) tapes_at_read'[of j1 tps] contents_inbounds[OF assms(3,4)] lentps
proper_symbols_ne0[OF proper_bit_symbols[OF bs]]
by (metis One_nat_def Suc_less_eq Suc_pred fst_conv le_imp_less_Suc less_SucI snd_eqD)
then show "fst (cmd_bindec j1 j2 (read tps)) = 0"
using cmd_bindec_def by simp
show "act (cmd_bindec j1 j2 (read tps) [!] j) (tps ! j) = tps' ! j"
if "j < Suc k" for j
proof -
have "last ?rs = 1"
by (metis (mono_tags, lifting) last_length lessI)
then have *: "snd (cmd_bindec j1 j2 ?rs) = map (Ξ»i.
if i = j1 then (?rs ! i, Right)
else if i = j2 then (?rs ! i, Stay)
else if i = length ?rs - 1 then (if ?rs ! j1 = π­ then π­ else π¬, Stay)
else (?rs ! i, Stay)) [0..<length ?rs]"
have "length ?rs = Suc k"
then have len: "j < length ?rs"
using that by simp
have k: "k = length ?rs - 1"
by (simp add: βΉlength ?rs = Suc kβΊ)
consider "j = j1" | "j β  j1 β§ j = j2" | "j β  j1 β§ j β  j2 β§ j = k" | "j β  j1 β§ j β  j2 β§ j β  k"
by auto
then show ?thesis
proof (cases)
case 1
then have "cmd_bindec j1 j2 ?rs [!] j = (?rs ! j1, Right)"
using * len by simp
then show ?thesis
using act_Right 1 assms(5) j_less(1) lentps by simp
next
case 2
then have "cmd_bindec j1 j2 ?rs [!] j = (?rs ! j2, Stay)"
using * len by simp
then show ?thesis
using 2 act_Stay assms(5) j_less(2) lentps by simp
next
case 3
then have "cmd_bindec j1 j2 ?rs [!] j = (todigit (?rs ! j1) + 2, Stay)"
using k * len by simp
then show ?thesis
using 3 assms(1,5) act_onesie j_less(1) lentps tapes_at_read'
by (metis length_list_update less_Suc_eq nth_list_update)
next
case 4
then have "cmd_bindec j1 j2 ?rs [!] j = (?rs ! j, Stay)"
using k * len that by simp
then show ?thesis
using 4 act_Stay assms(5) lentps that by simp
qed
qed
qed

lemma sem_cmd_bindec_23:
assumes "tps ! k = βsβ"
and "s = π¬ β¨ s = π­"
and "tps ! j1 = (βzsβ, i)"
and "i > 0"
and "i β€ length zs"
and "tps' = tps
[j1 := tps ! j1 |+| 1,
j2 := tps ! j2 |:=| decsym s (tps :.: j1) |+| 1,
k := ββΉβ]"
shows "sem (cmd_bindec j1 j2) (0, tps) = (0, tps')"
proof (rule semI)
show "proper_command (Suc k) (cmd_bindec j1 j2)"
using cmd_bindec_def by simp
show "length tps = Suc k"
using lentps by simp
show "length tps' = Suc k"
using lentps assms(6) by simp
using assms(3-5) bs tapes_at_read'[of j1 tps] contents_inbounds[OF assms(4,5)] lentps
by (metis One_nat_def Suc_less_eq Suc_pred fst_conv j_less(1) le_imp_less_Suc
less_imp_le_nat not_one_less_zero proper_bit_symbols snd_conv)
show "fst (cmd_bindec j1 j2 (read tps)) = 0"
show "act (cmd_bindec j1 j2 (read tps) [!] j) (tps ! j) = tps' ! j"
if "j < Suc k" for j
proof -
have "last ?rs β  1"
by (metis Suc_1 diff_Suc_1 last_conv_nth lessI list.size(3) n_not_Suc_n numeral_One
numeral_eq_iff old.nat.distinct(1) semiring_norm(86))
then have *: "snd (cmd_bindec j1 j2 ?rs) = map (Ξ»i.
if i = j1 then (?rs ! i, Right)
else if i = j2 then (2 * todigit (last ?rs) + todigit (?rs ! j1) + 2, Right)
else if i = length ?rs - 1 then (1, Stay)
else (?rs ! i, Stay)) [0..<length ?rs]"
have lenrs: "length ?rs = Suc k"
then have len: "j < length ?rs"
using that by simp
have k: "k = length ?rs - 1"
consider "j = j1" | "j β  j1 β§ j = j2" | "j β  j1 β§ j β  j2 β§ j = k" | "j β  j1 β§ j β  j2 β§ j β  k"
by auto
then show ?thesis
proof (cases)
case 1
then show ?thesis
using * len act_Right assms(6) j_less(1) j1_neq lentps by simp
next
case 2
then have "cmd_bindec j1 j2 ?rs [!] j = (2 * todigit (last ?rs) + todigit (?rs ! j1) + 2, Right)"
using * len by simp
moreover have "last ?rs = s"
by (metis last_conv_nth length_0_conv lentps lessI old.nat.distinct(1))
moreover have "?rs ! j1 = tps :.: j1"
using j_less(1) lentps tapes_at_read' by simp
ultimately show ?thesis
using 2 assms(6) act_Right' j_less lentps by simp
next
case 3
then show ?thesis
using * len k act_onesie assms(1,6) lentps by simp
next
case 4
then have "cmd_bindec j1 j2 ?rs [!] j = (?rs ! j, Stay)"
using k * len by simp
then show ?thesis
using 4 act_Stay assms(6) lentps that by simp
qed
qed
qed

end  (* tps zs *)

lemma transits_tm_bindec:
fixes tps :: "tape list" and zs :: "symbol list"
assumes j1_neq: "j1 β  j2"
and j1j2: "0 < j2" "j1 < k" "j2 < k"
and lentps: "Suc k = length tps"
and bs: "bit_symbols zs"
assumes "tps ! k = ββΉβ"
and "tps ! j1 = (βzsβ, 2 * i + 1)"
and "tps ! j2 = (βbindecode (take (2 * i) zs)β, Suc i)"
and "i < length zs div 2"
and "tps' = tps
[j1 := (βzsβ, 2 * (Suc i) + 1),
j2 := (βbindecode (take (2 * Suc i) zs)β, Suc (Suc i))]"
shows "transits (tm_bindec j1 j2) (0, tps) 2 (0, tps')"
proof -
define tps1 where "tps1 = tps
[j1 := (βzsβ, 2 * i + 2),
k := βtodigit (tps :.: j1) + 2β]"
let ?i = "2 * i + 1"
let ?M = "tm_bindec j1 j2"
have ilen: "?i < length zs"
using assms(10) by simp
have "exe ?M (0, tps) = sem (cmd_bindec j1 j2) (0, tps)"
using tm_bindec_def exe_lt_length by simp
also have "... =
(if ?i β€ length zs then 0 else 1,
tps[j1 := tps ! j1 |+| 1, k := βtodigit (tps :.: j1) + 2β])"
using ilen bs assms(7,8) sem_cmd_bindec_1 j1_neq lentps by simp
also have "... = (0, tps[j1 := tps ! j1 |+| 1, k := βtodigit (tps :.: j1) + 2β])"
using ilen by simp
also have "... = (0, tps1)"
using tps1_def assms by simp
finally have step1: "exe ?M (0, tps) = (0, tps1)" .

let ?s = "tps1 :.: k"
have "tps :.: j1 = zs ! (2 * i)"
using assms(8) ilen by simp
then have "?s = todigit (zs ! (2 * i)) + 2"
using tps1_def lentps by simp
then have "?s = zs ! (2 * i)"
moreover have "tps1 :.: j1 = zs ! ?i"
using tps1_def ilen lentps j1j2 by simp
ultimately have *: "decsym ?s (tps1 :.: j1) = decsym (zs ! (2*i)) (zs ! (Suc (2*i)))"
by simp

have "exe ?M (0, tps1) = sem (cmd_bindec j1 j2) (0, tps1)"
using tm_bindec_def exe_lt_length by simp
also have "... =
(if Suc ?i β€ length zs then 0 else 1,
tps1[j1 := tps1 ! j1 |+| 1, j2 := tps1 ! j2 |:=| 2 * todigit ?s + todigit (tps1 :.: j1) + 2 |+| 1, k := ββΉβ])"
proof -
have 1: "tps1 ! k = β?sβ"
using tps1_def lentps by simp
have 2: "?s = 2 β¨ ?s = 3"
using tps1_def lentps by simp
have 3: "tps1 ! j1 = (βzsβ, Suc ?i)"
using tps1_def lentps Suc_1 add_Suc_right j_less(1) less_Suc_eq nat_neq_iff nth_list_update_eq nth_list_update_neq
by simp
have 4: "Suc ?i > 0"
by simp
have 5: "Suc k = length tps1"
show ?thesis
using ilen sem_cmd_bindec_23[of tps1 zs ?s "Suc ?i", OF j1_neq 5 bs 1 2 3 4] by simp
qed
also have "... =
(0, tps1[j1 := tps1 ! j1 |+| 1, j2 := tps1 ! j2 |:=| decsym ?s (tps1 :.: j1) |+| 1, k := ββΉβ])"
using assms(10) length_binencode by simp
also have "... =
(0, tps1[j1 := tps1 ! j1 |+| 1, j2 := tps1 ! j2 |:=| decsym (zs ! (2*i)) (zs ! (Suc (2*i))) |+| 1, k := ββΉβ])"
(is "_ = (0, ?tps)")
using * by simp
also have "... = (0, tps')"
proof -
have len': "length tps' = Suc k"
using assms lentps by simp
have len1: "length tps1 = Suc k"
using assms lentps tps1_def by simp
have 1: "?tps ! k = tps' ! k"
using assms(7,11) by (simp add: j_less(1) j_less(2) len1 nat_neq_iff)
have 2: "?tps ! j1 = tps' ! j1"
using assms(11) j1_neq j_less(1) lentps tps1_def by simp
have "?tps ! j2 = tps1 ! j2 |:=| decsym (zs ! (2*i)) (zs ! (Suc (2*i))) |+| 1"
by (simp add: j_less(2) len1 less_Suc_eq nat_neq_iff)
also have "... = tps ! j2 |:=| decsym (zs ! (2*i)) (zs ! (Suc (2*i))) |+| 1"
using tps1_def j1_neq j_less(2) len1 by force
also have "... = (βbindecode (take (2 * i) zs)β, Suc i) |:=| decsym (zs ! (2*i)) (zs ! (Suc (2*i))) |+| 1"
using assms(9) j1_neq j_less(2) len1 tps1_def by simp
also have "... = (βbindecode (take (2 * i) zs)β(Suc i := decsym (zs ! (2*i)) (zs ! (Suc (2*i)))), Suc (Suc i))"
by simp
also have "... = (βbindecode (take (2 * i) zs) @ [decsym (zs ! (2*i)) (zs ! (Suc (2*i)))]β, Suc (Suc i))"
using contents_snoc[of "bindecode (take (2 * i) zs)"] ilen length_bindecode
proof -
have "length (bindecode (take (2 * i) zs)) = i"
using ilen length_bindecode by simp
then show ?thesis
using contents_snoc[of "bindecode (take (2 * i) zs)"] by simp
qed
also have "... = (βbindecode (take (2 * Suc i) zs)β, Suc (Suc i))"
using bindecode_take_snoc ilen by simp
also have *: "... = tps' ! j2"
by (metis assms(11) j_less(2) length_list_update lentps less_Suc_eq nth_list_update_eq)
finally have "?tps ! j2 = tps' ! j2" .
with 1 2 assms(11) * show ?thesis
unfolding tps1_def
by (smt (verit) j_less(1) j_less(2) lentps less_Suc_eq list_update_id list_update_overwrite list_update_swap nat_neq_iff nth_list_update_eq nth_list_update_neq)
qed
finally have "exe ?M (0, tps1) = (0, tps')" .
then have "execute ?M (0, tps) 2 = (0, tps')"
using step1 by (simp add: numeral_2_eq_2)
then show "transits (tm_bindec j1 j2) (0, tps) 2 (0, tps')"
using execute_imp_transits by blast
qed

context
fixes tps :: "tape list" and zs :: "symbol list"
assumes j1_neq: "j1 β  j2"
and j1j2: "0 < j2" "j1 < k" "j2 < k"
and lentps: "Suc k = length tps"
and bs: "bit_symbols zs"
begin

lemma transits_tm_bindec':
assumes "tps ! k = ββΉβ"
and "tps ! j1 = (βzsβ, 1)"
and "tps ! j2 = (β[]β, 1)"
and "i β€ length zs div 2"
and "tps' = tps
[j1 := (βzsβ, 2 * i + 1),
j2 := (βbindecode (take (2 * i) zs)β, Suc i)]"
shows "transits (tm_bindec j1 j2) (0, tps) (2 * i) (0, tps')"
using assms(4,5)
proof (induction i arbitrary: tps')
case 0
then show ?case
using assms(2,3) by (metis One_nat_def add.commute div_mult_self1_is_m execute.simps(1)
le_numeral_extra(3) length_bindecode length_greater_0_conv list.size(3) list_update_id
mult_0_right plus_1_eq_Suc take0 transits_def zero_less_numeral)
next
case (Suc i)
define tpsi where "tpsi = tps
[j1 := (βzsβ, 2 * i + 1),
j2 := (βbindecode (take (2*i) zs)β, Suc i)]"
then have "transits (tm_bindec j1 j2) (0, tps) (2 * i) (0, tpsi)"
using Suc by simp
moreover have "transits (tm_bindec j1 j2) (0, tpsi) 2 (0, tps')"
proof -
have 1: "tpsi ! k = ββΉβ"
using tpsi_def by (simp add: assms(1) j_less(1) j_less(2) less_not_refl3)
have 2: "tpsi ! j1 = (βzsβ, 2 * i + 1)"
using tpsi_def by (metis j1_neq j_less(1) lentps less_Suc_eq nth_list_update_eq nth_list_update_neq)
have 3: "tpsi ! j2 = (βbindecode (take (2 * i) zs)β, Suc i)"
using tpsi_def by (metis j_less(2) length_list_update lentps less_Suc_eq nth_list_update_eq)
have 4: "i < length zs div 2"
using Suc by simp
have 5: "tps' = tpsi
[j1 := (βzsβ, 2 * (Suc i) + 1),
j2 := (βbindecode (take (2 * Suc i) zs)β, Suc (Suc i))]"
using Suc tpsi_def by (metis (no_types, opaque_lifting) list_update_overwrite list_update_swap)
have 6: "Suc k = length tpsi"
using tpsi_def lentps by simp
show ?thesis
using transits_tm_bindec[OF j1_neq j1j2 6 bs 1 2 3 4 5] .
qed
ultimately show "transits (tm_bindec j1 j2) (0, tps) (2 * (Suc i)) (0, tps')"
qed

corollary transits_tm_bindec'':
assumes "tps ! k = ββΉβ"
and "tps ! j1 = (βzsβ, 1)"
and "tps ! j2 = (β[]β, 1)"
and "l = length zs div 2"
and "tps' = tps
[j1 := (βzsβ, 2 * l + 1),
j2 := (βbindecode (take (2 * l) zs)β, Suc l)]"
shows "transits (tm_bindec j1 j2) (0, tps) (2 * l) (0, tps')"
using assms transits_tm_bindec' by simp

text βΉIn case the input is of odd length, that is, malformed:βΊ

lemma transforms_tm_bindec_odd:
assumes "tps ! k = ββΉβ"
and "tps ! j1 = (βzsβ, 1)"
and "tps ! j2 = (β[]β, 1)"
and "tps' = tps
[j1 := (βzsβ, 2 * l + 2),
j2 := (βbindecode zsβ, Suc l),
k := βtodigit (last zs) + 2β]"
and "l = length zs div 2"
and "Suc (2 * l) = length zs"
shows "transforms (tm_bindec j1 j2) tps (2 * l + 2) tps'"
proof -
let ?ys = "bindecode (take (2 * l) zs)"
let ?i = "2 * l + 1"
let ?M = "tm_bindec j1 j2"
have ys: "?ys = bindecode zs"
using bindecode_odd assms(6) by (metis Suc_eq_plus1)
have "zs β  []"
using assms(6) by auto
define tps1 where "tps1 = tps
[j1 := (βzsβ, 2 * l + 1),
j2 := (β?ysβ, Suc l)]"
define tps2 where "tps2 = tps
[j1 := (βzsβ, 2 * l + 2),
j2 := (βbindecode zsβ, Suc l),
k := βtodigit (tps1 :.: j1) + 2β]"
have "transits ?M (0, tps) (2 * l) (0, tps1)"
using tps1_def assms transits_tm_bindec'' by simp
moreover have "execute ?M (0, tps1) 1 = (0, tps2)"
proof -
have "execute ?M (0, tps1) 1 = exe ?M (0, tps1)"
by simp
also have "... = sem (cmd_bindec j1 j2) (0, tps1)"
using exe_lt_length tm_bindec_def by simp
also have "... = (0, tps1[j1 := tps1 ! j1 |+| 1, k := βtodigit (tps1 :.: j1) + 2β])"
(is "_ = (0, ?tps)")
proof -
have "tps1 ! j1 = (βzsβ, ?i)"
using lentps tps1_def j1_neq j_less by simp
moreover have "?i > 0"
by simp
moreover have "tps1 ! k = tps ! k"
using tps1_def by (simp add: j_less(1) j_less(2) nat_neq_iff)
moreover have "?i β€ length zs"
ultimately have "sem (cmd_bindec j1 j2) (0, tps1) = (0, ?tps)"
using sem_cmd_bindec_1 assms(1,4) bit_symbols_binencode bs j1_neq lentps tps1_def
by (metis length_list_update)
then show ?thesis
by simp
qed
also have "... = (0, tps2)"
proof -
have "tps2 ! j1 = ?tps ! j1"
using tps1_def tps2_def j1_neq j_less(1) lentps by simp
moreover have "tps2 ! j2 = ?tps ! j2"
using tps1_def tps2_def j1_neq j_less(2) lentps ys by simp
ultimately have "tps2 = ?tps"
using tps2_def tps1_def j_less(1) lentps
by (smt (verit) list_update_id list_update_overwrite list_update_swap)
then show ?thesis
by simp
qed
finally show ?thesis .
qed
ultimately have "transits ?M (0, tps) (2 * l + 1) (0, tps2)"
moreover have "execute ?M (0, tps2) 1 = (1, tps')"
proof -
have "execute ?M (0, tps2) 1 = exe ?M (0, tps2)"
by simp
also have "... = sem (cmd_bindec j1 j2) (0, tps2)"
using exe_lt_length tm_bindec_def by simp
also have "... = (1, tps2)"
proof -
have "2 * l + 2 > length zs"
using assms(5,6) by simp
moreover have "tps2 ! j1 = (βzsβ, 2 * l + 2)"
using tps2_def j1_neq j_less(1) lentps by simp
ultimately show ?thesis
using sem_cmd_bindec_gt[of tps2 zs "2 * l + 2"]
by (metis bs j1_neq length_list_update lentps tps2_def)
qed
moreover have "tps2 = tps'"
proof -
have "tps1 :.: j1 = last zs"
using tps1_def assms βΉzs β  []βΊ contents_inbounds
by (metis Suc_leI add.commute fst_conv j1_neq j_less(1) last_conv_nth lentps less_Suc_eq
nth_list_update_eq nth_list_update_neq plus_1_eq_Suc snd_conv zero_less_Suc)
then show ?thesis
using tps2_def assms(4) by simp
qed
ultimately show ?thesis
by simp
qed
ultimately have "transits ?M (0, tps) (2 * l + 2) (1, tps')"
then show "transforms (tm_bindec j1 j2) tps (2 * l + 2) tps'"
using transforms_def tm_bindec_def by simp
qed

text βΉ
In case the input is of even length, that is, properly encoded:
βΊ

lemma transforms_tm_bindec_even:
assumes "tps ! k = ββΉβ"
and "tps ! j1 = (βzsβ, 1)"
and "tps ! j2 = (β[]β, 1)"
and "tps' = tps
[j1 := (βzsβ, 2 * l + 1),
j2 := (βbindecode zsβ, Suc l)]"
and "l = length zs div 2"
and "2 * l = length zs"
shows "transforms (tm_bindec j1 j2) tps (2 * l + 1) tps'"
proof -
let ?ys = "bindecode (take (2 * l) zs)"
let ?i = "2 * l + 1"
let ?M = "tm_bindec j1 j2"
have ys: "?ys = bindecode zs"
using assms(6) by simp
have "transits ?M (0, tps) (2 * l) (0, tps')"
using assms transits_tm_bindec'' by simp
moreover have "execute ?M (0, tps') 1 = (1, tps')"
proof -
have "execute ?M (0, tps') 1 = exe ?M (0, tps')"
using assms(4) by simp
also have "... = sem (cmd_bindec j1 j2) (0, tps')"
using exe_lt_length tm_bindec_def by simp
also have "... = (1, tps')"
proof -
have "tps' ! j1 = (βzsβ, ?i)"
using lentps assms(4) j1_neq j_less by simp
moreover have "?i > length zs"
using assms(6) by simp
moreover have "tps' ! k = tps ! k"
using assms(4) by (simp add: j_less(1) j_less(2) nat_neq_iff)
ultimately have "sem (cmd_bindec j1 j2) (0, tps') = (1, tps')"
using sem_cmd_bindec_gt assms(1,4) bit_symbols_binencode bs j1_neq lentps assms(4)
by simp
then show ?thesis
by simp
qed
finally show ?thesis .
qed
ultimately have "transits ?M (0, tps) (2 * l + 1) (1, tps')"
then show "transforms (tm_bindec j1 j2) tps (2 * l + 1) tps'"
using tm_bindec_def transforms_def by simp
qed

lemma transforms_tm_bindec:
assumes "tps ! k = ββΉβ"
and "tps ! j1 = (βzsβ, 1)"
and "tps ! j2 = (β[]β, 1)"
and "tps' = tps
[j1 := (βzsβ, Suc (length zs)),
j2 := (βbindecode zsβ, Suc (length zs div 2)),
k := βif even (length zs) then 1 else (todigit (last zs) + 2)β]"
shows "transforms (tm_bindec j1 j2) tps (Suc (length zs)) tps'"
proof (cases "even (length zs)")
case True
then show ?thesis
using transforms_tm_bindec_even[OF assms(1-3)] assms(1,4) j_less(1) j_less(2)
by (smt (verit) Suc_eq_plus1 dvd_mult_div_cancel list_update_id list_update_swap nat_neq_iff)
next
case False
then show ?thesis
using assms(4) transforms_tm_bindec_odd[OF assms(1-3)] by simp
qed

end  (* context tps zs *)

end  (* context j1 j2 k *)

text βΉ
Next we eliminate the memorization tape from @{const tm_bindec}.
βΊ

lemma transforms_cartesian_bindec:
assumes "G β₯ (6 :: nat)"
assumes "j1 β  j2"
and j1j2: "0 < j2" "j1 < k" "j2 < k"
and "k = length tps"
and "bit_symbols zs"
assumes "tps ! j1 = (βzsβ, 1)"
and "tps ! j2 = (β[]β, 1)"
assumes "t = Suc (length zs)"
and "tps' = tps
[j1 := (βzsβ, Suc (length zs)),
j2 := (βbindecode zsβ, Suc (length zs div 2))]"
shows "transforms (cartesian (tm_bindec j1 j2) 4) tps t tps'"
proof (rule cartesian_transforms_onesie)
show "turing_machine (Suc k) G (tm_bindec j1 j2)"
using tm_bindec_tm assms(1) j1j2 by simp
show "immobile (tm_bindec j1 j2) k (Suc k)"
proof (standard+)
fix q :: nat and rs :: "symbol list"
assume "q < length (tm_bindec j1 j2)" "length rs = Suc k"
then have *: "tm_bindec j1 j2 ! q = cmd_bindec j1 j2"
using tm_bindec_def by simp
moreover have "cmd_bindec j1 j2 rs [~] k = Stay"
using cmd_bindec_def length rs = Suc k j1j2
by (smt (verit, best) add_diff_inverse_nat diff_zero length_upt lessI less_nat_zero_code
nat_neq_iff nth_map nth_upt prod.sel(2))
ultimately show "(tm_bindec j1 j2 ! q) rs [~] k = Stay"
using * by simp
qed
show "2 β€ k"
using j1j2 by linarith
show "(1::nat) < 4"
by simp
show "length tps = k"
using assms(3,6) by simp
show "bounded_write (tm_bindec j1 j2) k 4"
proof -
{ fix q :: nat and rs :: "symbol list"
assume q: "q < length (tm_bindec j1 j2)" and rs: "length rs = Suc k"
then have "tm_bindec j1 j2 ! q = cmd_bindec j1 j2"
using tm_bindec_def by simp
have "cmd_bindec j1 j2 rs [.] (length rs - 1) < 4 β¨ fst (cmd_bindec j1 j2 rs) = 1"
proof (cases "rs ! j1 = 0")
case True
then show ?thesis
using cmd_bindec_def by simp
next
case else: False
show ?thesis
proof (cases "last rs = 1")
case True
then have "snd (cmd_bindec j1 j2 rs) = map (Ξ»i.
if i = j1 then (rs ! i, Right)
else if i = j2 then (rs ! i, Stay)
else if i = length rs - 1 then (todigit (rs ! j1) + 2, Stay)
else (rs ! i, Stay)) [0..<length rs]"
using else cmd_bindec_def by simp
then have "snd (cmd_bindec j1 j2 rs) ! k = (todigit (rs ! j1) + 2, Stay)"
using rs j1j2
by (smt (verit) add.left_neutral diff_Suc_1 diff_zero length_upt lessI nat_neq_iff nth_map nth_upt)
then show ?thesis
using rs by simp
next
case False
then have "snd (cmd_bindec j1 j2 rs) = map (Ξ»i.
if i = j1 then (rs ! i, Right)
else if i = j2 then (2 * todigit (last rs) + todigit (rs ! j1) + 2, Right)
else if i = length rs - 1 then (1, Stay)
else (rs ! i, Stay)) [0..<length rs]"
using else cmd_bindec_def by simp
then have "snd (cmd_bindec j1 j2 rs) ! k = (1, Stay)"
using rs j1j2
by (smt (verit) add.left_neutral diff_Suc_1 diff_zero length_upt lessI nat_neq_iff nth_map nth_upt)
then show ?thesis
using rs by simp
qed
qed
}</