Theory Wellformed
section ‹Well-formedness of lists\label{s:tm-wellformed}›
theory Wellformed
imports Symbol_Ops Lists_Lists
begin
text ‹
In the representations introduced in Section~\ref{s:tm-numlist} and
Section~\ref{s:tm-numlistlist}, not every symbol sequence over @{text "𝟬𝟭¦"}
represents a list of numbers, and not every symbol sequence over @{text
"𝟬𝟭¦♯"} represents a list of lists of numbers. In this section we prove
criteria for symbol sequences to represent such lists and devise Turing machines
to check these criteria efficiently.
›
subsection ‹A criterion for well-formed lists›
text ‹
From the definition of @{const numlist} it is easy to see that a symbol sequence
representing a list of numbers is either empty or not, and that in the latter
case it ends with a @{text "¦"} symbol. Moreover it can only contain the symbols
@{text "𝟬𝟭¦"} and cannot contain the symbol sequence @{text "𝟬¦"} because
canonical number representations cannot end in @{text 𝟬}. That these properties
are not only necessary but also sufficient for the symbol sequence to represent
a list of numbers is shown in this section.
A symbol sequence is well-formed if it represents a list of numbers.
›
definition numlist_wf :: "symbol list ⇒ bool" where
"numlist_wf zs ≡ ∃ns. numlist ns = zs"
lemma numlist_wf_append:
assumes "numlist_wf xs" and "numlist_wf ys"
shows "numlist_wf (xs @ ys)"
proof -
obtain ms ns where "numlist ms = xs" and "numlist ns = ys"
using assms numlist_wf_def by auto
then have "numlist (ms @ ns) = xs @ ys"
using numlist_append by simp
then show ?thesis
using numlist_wf_def by auto
qed
lemma numlist_wf_canonical:
assumes "canonical xs"
shows "numlist_wf (xs @ [¦])"
proof -
obtain n where "canrepr n = xs"
using assms canreprI by blast
then have "numlist [n] = xs @ [¦]"
using numlist_def by simp
then show ?thesis
using numlist_wf_def by auto
qed
text ‹
Well-formed symbol sequences can be unambiguously decoded to lists of numbers.
›
definition zs_numlist :: "symbol list ⇒ nat list" where
"zs_numlist zs ≡ THE ns. numlist ns = zs"
lemma zs_numlist_ex1:
assumes "numlist_wf zs"
shows "∃!ns. numlist ns = zs"
using assms numlist_wf_def numlist_inj by blast
lemma numlist_zs_numlist:
assumes "numlist_wf zs"
shows "numlist (zs_numlist zs) = zs"
using assms zs_numlist_def zs_numlist_ex1 by (smt (verit, del_insts) the_equality)
text ‹
Count the number of occurrences of an element in a list:
›
fun count :: "nat list ⇒ nat ⇒ nat" where
"count [] z = 0" |
"count (x # xs) z = (if x = z then 1 else 0) + count xs z"
lemma count_append: "count (xs @ ys) z = count xs z + count ys z"
by (induction xs) simp_all
lemma count_0: "count xs z = 0 ⟷ (∀x∈set xs. x ≠ z)"
proof
show "count xs z = 0 ⟹ ∀x∈set xs. x ≠ z"
by (induction xs) auto
show "∀x∈set xs. x ≠ z ⟹ count xs z = 0"
by (induction xs) auto
qed
lemma count_gr_0_take:
assumes "count xs z > 0"
shows "∃j.
j < length xs ∧
xs ! j = z ∧
(∀i<j. xs ! i ≠ z) ∧
count (take (Suc j) xs) z = 1 ∧
count (drop (Suc j) xs) z = count xs z - 1"
proof -
let ?P = "λi. i < length xs ∧ xs ! i = z"
have ex: "∃i. ?P i"
using assms(1) count_0 by (metis bot_nat_0.not_eq_extremum in_set_conv_nth)
define j where "j = Least ?P"
have 1: "j < length xs"
using j_def ex by (metis (mono_tags, lifting) LeastI)
moreover have 2: "xs ! j = z"
using j_def ex by (metis (mono_tags, lifting) LeastI)
moreover have 3: "∀i<j. xs ! i ≠ z"
using j_def ex 1 not_less_Least order_less_trans by blast
moreover have 4: "count (take (Suc j) xs) z = 1"
proof -
have "∀x∈set (take j xs). x ≠ z"
using 3 1 by (metis in_set_conv_nth length_take less_imp_le_nat min_absorb2 nth_take)
then have "count (take j xs) z = 0"
using count_0 by simp
moreover have "count [xs ! j] z = 1"
using 2 by simp
moreover have "take (Suc j) xs = take j xs @ [xs ! j]"
using 1 take_Suc_conv_app_nth by auto
ultimately show "count (take (Suc j) xs) z = 1"
using count_append by simp
qed
moreover have "count (drop (Suc j) xs) z = count xs z - 1"
proof -
have "xs = take (Suc j) xs @ drop (Suc j) xs"
using 1 by simp
then show ?thesis
using count_append 4 by (metis add_diff_cancel_left')
qed
ultimately show ?thesis
by auto
qed
definition has2 :: "symbol list ⇒ symbol ⇒ symbol ⇒ bool" where
"has2 xs y z ≡ ∃i<length xs - 1. xs ! i = y ∧ xs ! (Suc i) = z"
lemma not_has2_take:
assumes "¬ has2 xs y z"
shows "¬ has2 (take m xs) y z"
proof (rule ccontr)
let ?ys = "take m xs"
assume "¬ ¬ has2 ?ys y z"
then have "has2 ?ys y z"
by simp
then have "has2 xs y z"
using has2_def by fastforce
then show False
using assms by simp
qed
lemma not_has2_drop:
assumes "¬ has2 xs y z"
shows "¬ has2 (drop m xs) y z"
proof (rule ccontr)
let ?ys = "drop m xs"
assume "¬ ¬ has2 ?ys y z"
then have "has2 ?ys y z"
by simp
then have "has2 xs y z"
using has2_def by fastforce
then show False
using assms by simp
qed
lemma numlist_wf_has2:
assumes "proper_symbols xs" "symbols_lt 5 xs" "¬ has2 xs 𝟬 ¦" "xs ≠ [] ⟶ last xs = ¦"
shows "numlist_wf xs"
using assms
proof (induction "count xs ¦" arbitrary: xs)
case 0
then have "xs = []"
using count_0 by simp
then show ?case
using numlist_wf_def numlist_Nil by blast
next
case (Suc n)
then obtain j :: nat where j:
"j < length xs"
"xs ! j = ¦"
"∀i<j. xs ! i ≠ ¦"
"count (take (Suc j) xs) ¦ = 1"
"count (drop (Suc j) xs) ¦ = count xs ¦ - 1"
by (metis count_gr_0_take zero_less_Suc)
then have "xs ≠ []"
by auto
then have "last xs = ¦"
using Suc.prems by simp
let ?ys = "drop (Suc j) xs"
have "count ?ys ¦ = n"
using j(5) Suc by simp
moreover have "proper_symbols ?ys"
using Suc.prems by simp
moreover have "symbols_lt 5 ?ys"
using Suc.prems by simp
moreover have "¬ has2 ?ys 𝟬 ¦"
using not_has2_drop Suc.prems(3) by simp
moreover have "?ys ≠ [] ⟶ last ?ys = ¦"
using j by (simp add: ‹last xs = ¦›)
ultimately have wf_ys: "numlist_wf ?ys"
using Suc by simp
let ?zs = "take j xs"
have "canonical ?zs"
proof -
have "?zs ! i ≥ 𝟬" if "i < length ?zs" for i
using that Suc.prems(1) j by (metis One_nat_def Suc_1 Suc_leI length_take min_less_iff_conj nth_take)
moreover have "?zs ! i ≤ 𝟭" if "i < length ?zs" for i
proof -
have "?zs ! i < ¦"
using that Suc.prems(1,2) j
by (metis eval_nat_numeral(3) length_take less_Suc_eq_le min_less_iff_conj nat_less_le nth_take)
then show ?thesis
by simp
qed
ultimately have "bit_symbols ?zs"
by fastforce
moreover have "?zs = [] ∨ last ?zs = 𝟭"
proof (cases "?zs = []")
case True
then show ?thesis
by simp
next
case False
then have "last ?zs = ?zs ! (j - 1)"
by (metis add_diff_inverse_nat j(1) last_length length_take less_imp_le_nat less_one
min_absorb2 plus_1_eq_Suc take_eq_Nil)
then have last: "last ?zs = xs ! (j - 1)"
using False by simp
have "xs ! (j - 1) ≠ ¦"
using j(3) False by simp
moreover have "xs ! (j - 1) < ♯"
using Suc.prems(2) j(1) by simp
moreover have "xs ! (j - 1) ≥ 𝟬"
using Suc.prems(1) j(1) by (metis One_nat_def Suc_1 Suc_leI less_imp_diff_less)
moreover have "xs ! (j - 1) ≠ 𝟬"
proof (rule ccontr)
assume "¬ xs ! (j - 1) ≠ 𝟬"
then have "xs ! (j - 1) = 𝟬"
by simp
moreover have "xs ! j = ¦"
using j by simp
ultimately have "has2 xs 𝟬 ¦"
using has2_def j False
by (metis (no_types, lifting) Nat.lessE add_diff_cancel_left' less_Suc_eq_0_disj not_less_eq plus_1_eq_Suc take_eq_Nil)
then show False
using Suc.prems(3) by simp
qed
ultimately have "xs ! (j - 1) = 𝟭"
by simp
then have "last ?zs = 𝟭"
using last by simp
then show ?thesis
by simp
qed
ultimately show "canonical ?zs"
using canonical_def by simp
qed
let ?ts = "take (Suc j) xs"
have "?ts = ?zs @ [¦]"
using j by (metis take_Suc_conv_app_nth)
then have "numlist_wf ?ts"
using numlist_wf_canonical `canonical ?zs` by simp
moreover have "xs = ?ts @ ?ys"
by simp
ultimately show "numlist_wf xs"
using wf_ys numlist_wf_append by fastforce
qed
lemma last_numlist_4: "numlist ns ≠ [] ⟹ last (numlist ns) = ¦"
proof (induction ns)
case Nil
then show ?case
using numlist_def by simp
next
case (Cons n ns)
then show ?case
using numlist_def by (cases "numlist ns = []") simp_all
qed
lemma numlist_not_has2:
assumes "i < length (numlist ns) - 1" and "numlist ns ! i = 𝟬"
shows "numlist ns ! (Suc i) ≠ ¦"
using assms
proof (induction ns arbitrary: i)
case Nil
then show ?case
by (simp add: numlist_Nil)
next
case (Cons n ns)
show "numlist (n # ns) ! (Suc i) ≠ ¦"
proof (cases "i < length (numlist [n])")
case True
have "numlist (n # ns) ! i = (numlist [n] @ numlist ns) ! i"
using numlist_def by simp
then have "numlist (n # ns) ! i = numlist [n] ! i"
using True by (simp add: nth_append)
then have "numlist (n # ns) ! i = (canrepr n @ [¦]) ! i"
using numlist_def by simp
moreover have "numlist (n # ns) ! i = 𝟬"
using Cons by simp
ultimately have "(canrepr n @ [¦]) ! i = 𝟬"
by simp
moreover have "(canrepr n @ [¦]) ! (length (canrepr n @ [¦]) - 1) = ¦"
by simp
ultimately have "i ≠ length (canrepr n @ [¦]) - 1"
by auto
then have *: "i ≠ length (numlist [n]) - 1"
using numlist_def by simp
have 3: "canrepr n ! j = numlist (n # ns) ! j" if "j < nlength n" for j
proof -
have j: "j < length (numlist [n])"
using that numlist_def by simp
have "numlist (n # ns) ! j = (numlist [n] @ numlist ns) ! j"
using numlist_def by simp
then have "numlist (n # ns) ! j = numlist [n] ! j"
using j by (simp add: nth_append)
then have "numlist (n # ns) ! j = (canrepr n @ [¦]) ! j"
using numlist_def by simp
then show ?thesis
by (simp add: nth_append that)
qed
have neq0: "n ≠ 0"
proof -
have "length (numlist [0]) = 1"
using numlist_def by simp
then show ?thesis
using * True by (metis diff_self_eq_0 less_one)
qed
then have "i < length (numlist [n]) - 1"
using * True by simp
then have "i < length (canrepr n @ [¦]) - 1"
using numlist_def by simp
then have "i < length (canrepr n)"
by simp
then have "canrepr n ! i = 𝟬"
by (metis ‹(canrepr n @ [¦]) ! i = 𝟬› nth_append)
moreover have "last (canrepr n) ≠ 𝟬"
using canonical_canrepr canonical_def
by (metis neq0 length_0_conv n_not_Suc_n nlength_0 numeral_2_eq_2 numeral_3_eq_3)
ultimately have "i ≠ nlength n - 1"
by (metis ‹i < nlength n› last_conv_nth less_zeroE list.size(3))
then have "i < nlength n - 1"
using ‹i < nlength n› by linarith
then have "Suc i < nlength n"
by simp
then have "canrepr n ! Suc i ≤ 𝟭"
using bit_symbols_canrepr by fastforce
moreover have "canrepr n ! Suc i = numlist (n # ns) ! Suc i"
using 3 ‹Suc i < nlength n› by blast
ultimately show ?thesis
by simp
next
case False
let ?i = "i - length (numlist [n])"
have "numlist (n # ns) ! i = (numlist [n] @ numlist ns) ! i"
using numlist_def by simp
then have "numlist (n # ns) ! i = numlist ns ! ?i"
using False by (simp add: nth_append)
then have "numlist ns ! ?i = 𝟬"
using Cons by simp
moreover have "?i < length (numlist ns) - 1"
proof -
have "length (numlist (n # ns)) = length (numlist [n]) + length (numlist ns)"
using numlist_def by simp
then show ?thesis
using False Cons by simp
qed
ultimately have "numlist ns ! Suc ?i ≠ ¦"
using Cons by simp
moreover have "numlist (n # ns) ! Suc i = numlist ns ! Suc ?i"
using False numlist_append
by (smt (verit, del_insts) Suc_diff_Suc Suc_lessD append_Cons append_Nil diff_Suc_Suc not_less_eq nth_append)
ultimately show ?thesis
by simp
qed
qed
lemma numlist_wf_has2':
assumes "numlist_wf xs"
shows "proper_symbols_lt 5 xs ∧ ¬ has2 xs 𝟬 ¦ ∧ (xs ≠ [] ⟶ last xs = ¦)"
proof -
obtain ns where ns: "numlist ns = xs"
using numlist_wf_def assms by auto
have "proper_symbols xs"
using proper_symbols_numlist ns by auto
moreover have "symbols_lt 5 xs"
using ns numlist_234
by (smt (verit, best) One_nat_def Suc_1 eval_nat_numeral(3) in_mono insertE less_Suc_eq_le
linorder_le_less_linear nle_le not_less0 nth_mem numeral_less_iff semiring_norm(76)
semiring_norm(89) semiring_norm(90) singletonD)
moreover have "¬ has2 xs 𝟬 ¦"
using numlist_not_has2 ns has2_def by auto
moreover have "xs ≠ [] ⟶ last xs = ¦"
using last_numlist_4 ns by auto
ultimately show ?thesis
by simp
qed
lemma numlist_wf_iff:
"numlist_wf xs ⟷ proper_symbols_lt 5 xs ∧ ¬ has2 xs 𝟬 ¦ ∧ (xs ≠ [] ⟶ last xs = ¦)"
using numlist_wf_has2 numlist_wf_has2' by auto
subsection ‹A criterion for well-formed lists of lists›
text ‹
The criterion for lists of lists of numbers is similar to the one for lists of
numbers. A non-empty symbol sequence must end in @{text ♯}. All symbols must be
from @{text "𝟬𝟭¦♯"} and the sequences @{text "𝟬¦"}, @{text "𝟬♯"}, and @{text
"𝟭♯"} are forbidden.
A symbol sequence is well-formed if it represents a list of lists of numbers.
›
definition numlistlist_wf :: "symbol list ⇒ bool" where
"numlistlist_wf zs ≡ ∃nss. numlistlist nss = zs"
lemma numlistlist_wf_append:
assumes "numlistlist_wf xs" and "numlistlist_wf ys"
shows "numlistlist_wf (xs @ ys)"
proof -
obtain ms ns where "numlistlist ms = xs" and "numlistlist ns = ys"
using assms numlistlist_wf_def by auto
then have "numlistlist (ms @ ns) = xs @ ys"
using numlistlist_append by simp
then show ?thesis
using numlistlist_wf_def by auto
qed
lemma numlistlist_wf_numlist_wf:
assumes "numlist_wf xs"
shows "numlistlist_wf (xs @ [♯])"
proof -
obtain ns where "numlist ns = xs"
using assms numlist_wf_def by auto
then have "numlistlist [ns] = xs @ [♯]"
using numlistlist_def by simp
then show ?thesis
using numlistlist_wf_def by auto
qed
lemma numlistlist_wf_has2:
assumes "proper_symbols xs" "symbols_lt 6 xs" "xs ≠ [] ⟶ last xs = ♯"
and "¬ has2 xs 𝟬 ¦"
and "¬ has2 xs 𝟬 ♯"
and "¬ has2 xs 𝟭 ♯"
shows "numlistlist_wf xs"
using assms
proof (induction "count xs ♯" arbitrary: xs)
case 0
then have "xs = []"
using count_0 by simp
then show ?case
using numlistlist_wf_def numlistlist_Nil by auto
next
case (Suc n)
then obtain j :: nat where j:
"j < length xs"
"xs ! j = ♯"
"∀i<j. xs ! i ≠ ♯"
"count (take (Suc j) xs) ♯ = 1"
"count (drop (Suc j) xs) ♯ = count xs ♯ - 1"
by (metis count_gr_0_take zero_less_Suc)
then have "xs ≠ []"
by auto
then have "last xs = ♯"
using Suc.prems by simp
let ?ys = "drop (Suc j) xs"
have "count ?ys ♯ = n"
using j(5) Suc by simp
moreover have "proper_symbols ?ys"
using Suc.prems(1) by simp
moreover have "symbols_lt 6 ?ys"
using Suc.prems(2) by simp
moreover have "?ys ≠ [] ⟶ last ?ys = ♯"
using j by (simp add: ‹last xs = ♯›)
moreover have "¬ has2 ?ys 𝟬 ¦"
using not_has2_drop Suc.prems(4) by simp
moreover have "¬ has2 ?ys 𝟬 ♯"
using not_has2_drop Suc.prems(5) by simp
moreover have "¬ has2 ?ys 𝟭 ♯"
using not_has2_drop Suc.prems(6) by simp
ultimately have wf_ys: "numlistlist_wf ?ys"
using Suc by simp
let ?zs = "take j xs"
have len: "length ?zs = j"
using j(1) by simp
have "numlist_wf ?zs"
proof -
have "proper_symbols ?zs"
using Suc.prems(1) by simp
moreover have "symbols_lt 5 ?zs"
proof standard+
fix i :: nat
assume "i < length ?zs"
then have "i < j"
using j by simp
then have "?zs ! i < 6"
using Suc.prems(2) j by simp
moreover have "?zs ! i ≠ ♯"
using `i < j` j by simp
ultimately show "?zs ! i < ♯"
by simp
qed
moreover have "¬ has2 ?zs 𝟬 ¦"
using not_has2_take Suc.prems(4) by simp
moreover have "?zs ≠ [] ⟶ last ?zs = ¦"
proof
assume neq_Nil: "?zs ≠ []"
then have "j > 0"
by simp
moreover have "xs ! j = ♯"
using j by simp
ultimately have "xs ! Suc (j - 1) = ♯"
by simp
moreover have "j - 1 < length xs - 1"
by (simp add: Suc_leI ‹0 < j› diff_less_mono j(1))
ultimately have "xs ! (j - 1) ≠ 𝟬" "xs ! (j - 1) ≠ 𝟭"
using Suc.prems has2_def by auto
then have "?zs ! (j - 1) ≠ 𝟬" "?zs ! (j - 1) ≠ 𝟭"
by (simp_all add: ‹0 < j›)
moreover have "?zs ! (j - 1) < ♯"
using `symbols_lt 5 ?zs` `0 < j ` j(1) len
by simp
moreover have "?zs ! (j - 1) ≥ 𝟬"
using `proper_symbols ?zs` len ‹0 < j› by (metis One_nat_def Suc_1 Suc_leI diff_less zero_less_one)
ultimately have "?zs ! (j - 1) = ¦"
by simp
then show "last ?zs = ¦"
using len by (metis last_conv_nth neq_Nil)
qed
ultimately show "numlist_wf ?zs"
using numlist_wf_iff by simp
qed
let ?ts = "take (Suc j) xs"
have "?ts = ?zs @ [♯]"
using j by (metis take_Suc_conv_app_nth)
then have "numlistlist_wf ?ts"
using numlistlist_wf_numlist_wf `numlist_wf ?zs` by simp
moreover have "xs = ?ts @ ?ys"
by simp
ultimately show "numlistlist_wf xs"
using wf_ys numlistlist_wf_append by fastforce
qed
lemma numlistlist_not_has2:
assumes "i < length (numlistlist nss) - 1" and "numlistlist nss ! i = 𝟬"
shows "numlistlist nss ! (Suc i) ≠ ¦"
using assms
proof (induction nss arbitrary: i)
case Nil
then show ?case
by (simp add: numlistlist_Nil)
next
case (Cons ns nss)
show "numlistlist (ns # nss) ! (Suc i) ≠ ¦"
proof (cases "i < length (numlistlist [ns])")
case True
have "numlistlist (ns # nss) ! i = (numlistlist [ns] @ numlistlist nss) ! i"
using numlistlist_def by simp
then have "numlistlist (ns # nss) ! i = numlistlist [ns] ! i"
using True by (simp add: nth_append)
then have "numlistlist (ns # nss) ! i = (numlist ns @ [♯]) ! i"
using numlistlist_def by simp
moreover have "numlistlist (ns # nss) ! i = 𝟬"
using Cons by simp
ultimately have "(numlist ns @ [♯]) ! i = 𝟬"
by simp
moreover have "(numlist ns @ [♯]) ! (length (numlist ns @ [♯]) - 1) = ♯"
by simp
ultimately have "i ≠ length (numlist ns @ [♯]) - 1"
by auto
then have *: "i ≠ length (numlistlist [ns]) - 1"
using numlistlist_def by simp
then have **: "i < length (numlistlist [ns]) - 1"
using True by simp
then have ***: "i < length (numlist ns)"
using numlistlist_def by simp
then have "ns ≠ []"
using numlist_Nil by auto
then have "last (numlist ns) = ¦"
by (metis last_numlist_4 numlist_Nil numlist_inj)
have 3: "numlist ns ! j = numlistlist (ns # nss) ! j" if "j < length (numlist ns)" for j
proof -
have j: "j < length (numlistlist [ns])"
using that numlistlist_def by simp
have "numlistlist (ns # nss) ! j = (numlistlist [ns] @ numlistlist nss) ! j"
using numlistlist_def by simp
then have "numlistlist (ns # nss) ! j = numlistlist [ns] ! j"
using j by (simp add: nth_append)
then have "numlistlist (ns # nss) ! j = (numlist ns @ [♯]) ! j"
using numlistlist_def by simp
then show ?thesis
by (simp add: nth_append that)
qed
have 4: "numlistlist (ns # nss) ! (length (numlist ns)) = ♯"
by (simp add: numlistlist_def)
show ?thesis
proof (cases "i = length (numlist ns) - 1")
case True
then show ?thesis
using 3 4 *** by (metis Suc_le_D Suc_le_eq diff_Suc_1 eval_nat_numeral(3) n_not_Suc_n)
next
case False
then have "i < length (numlist ns) - 1"
using *** by simp
then show ?thesis
using numlist_not_has2 *** 3 ‹ns ≠ []›
by (metis Cons.prems(2) Suc_diff_1 length_greater_0_conv not_less_eq numlist_Nil numlist_inj)
qed
next
case False
then have "i ≥ length (numlistlist [ns])"
by simp
let ?i = "i - length (numlistlist [ns])"
have "numlistlist (ns # nss) ! i = (numlistlist [ns] @ numlistlist nss) ! i"
using numlistlist_def by simp
then have "numlistlist (ns # nss) ! i = numlistlist nss ! ?i"
using False by (simp add: nth_append)
then have "numlistlist nss ! ?i = 𝟬"
using Cons by simp
moreover have "?i < length (numlistlist nss) - 1"
proof -
have "length (numlistlist (ns # nss)) = length (numlistlist [ns]) + length (numlistlist nss)"
using numlistlist_def by simp
then show ?thesis
using False Cons by simp
qed
ultimately have "numlistlist nss ! Suc ?i ≠ ¦"
using Cons by simp
moreover have "numlistlist (ns # nss) ! Suc i = numlistlist nss ! Suc ?i"
using False numlistlist_append
by (smt (verit, del_insts) Suc_diff_Suc Suc_lessD append_Cons append_Nil diff_Suc_Suc not_less_eq nth_append)
ultimately show ?thesis
by simp
qed
qed
lemma numlistlist_not_has2':
assumes "i < length (numlistlist nss) - 1" and "numlistlist nss ! i = 𝟬 ∨ numlistlist nss ! i = 𝟭"
shows "numlistlist nss ! (Suc i) ≠ ♯"
using assms
proof (induction nss arbitrary: i)
case Nil
then show ?case
by (simp add: numlistlist_Nil)
next
case (Cons ns nss)
show "numlistlist (ns # nss) ! (Suc i) ≠ ♯"
proof (cases "i < length (numlistlist [ns])")
case True
have "numlistlist (ns # nss) ! i = (numlistlist [ns] @ numlistlist nss) ! i"
using numlistlist_def by simp
then have "numlistlist (ns # nss) ! i = numlistlist [ns] ! i"
using True by (simp add: nth_append)
then have "numlistlist (ns # nss) ! i = (numlist ns @ [♯]) ! i"
using numlistlist_def by simp
moreover have "numlistlist (ns # nss) ! i = 𝟬 ∨ numlistlist (ns # nss) ! i = 𝟭"
using Cons by simp
ultimately have "(numlist ns @ [♯]) ! i = 𝟬 ∨ (numlist ns @ [♯]) ! i = 𝟭"
by simp
moreover have "(numlist ns @ [♯]) ! (length (numlist ns @ [♯]) - 1) = ♯"
by simp
ultimately have "i ≠ length (numlist ns @ [♯]) - 1"
by auto
then have "i ≠ length (numlistlist [ns]) - 1"
using numlistlist_def by simp
then have "i < length (numlistlist [ns]) - 1"
using True by simp
then have *: "i < length (numlist ns)"
using numlistlist_def by simp
then have "ns ≠ []"
using numlist_Nil by auto
then have "last (numlist ns) = ¦"
by (metis last_numlist_4 numlist_Nil numlist_inj)
have **: "numlist ns ! j = numlistlist (ns # nss) ! j" if "j < length (numlist ns)" for j
proof -
have j: "j < length (numlistlist [ns])"
using that numlistlist_def by simp
have "numlistlist (ns # nss) ! j = (numlistlist [ns] @ numlistlist nss) ! j"
using numlistlist_def by simp
then have "numlistlist (ns # nss) ! j = numlistlist [ns] ! j"
using j by (simp add: nth_append)
then have "numlistlist (ns # nss) ! j = (numlist ns @ [♯]) ! j"
using numlistlist_def by simp
then show ?thesis
by (simp add: nth_append that)
qed
show ?thesis
proof (cases "i = length (numlist ns) - 1")
case True
then show ?thesis
using ‹last (numlist ns) = ¦› ‹ns ≠ []› Cons.prems(2) * ** numlist_Nil numlist_inj
by (metis last_conv_nth num.simps(8) numeral_eq_iff semiring_norm(83) verit_eq_simplify(8))
next
case False
then have "i < length (numlist ns) - 1"
using * by simp
then show ?thesis
using * ** symbols_lt_numlist numlist_not_has2 by (metis Suc_lessI diff_Suc_1 less_irrefl_nat)
qed
next
case False
then have "i ≥ length (numlistlist [ns])"
by simp
let ?i = "i - length (numlistlist [ns])"
have "numlistlist (ns # nss) ! i = (numlistlist [ns] @ numlistlist nss) ! i"
using numlistlist_def by simp
then have "numlistlist (ns # nss) ! i = numlistlist nss ! ?i"
using False by (simp add: nth_append)
then have "numlistlist nss ! ?i = 𝟬 ∨ numlistlist nss ! ?i = 𝟭"
using Cons by simp
moreover have "?i < length (numlistlist nss) - 1"
proof -
have "length (numlistlist (ns # nss)) = length (numlistlist [ns]) + length (numlistlist nss)"
using numlistlist_def by simp
then show ?thesis
using False Cons by simp
qed
ultimately have "numlistlist nss ! Suc ?i ≠ ♯"
using Cons by simp
moreover have "numlistlist (ns # nss) ! Suc i = numlistlist nss ! Suc ?i"
using False numlistlist_append
by (smt (verit, del_insts) Suc_diff_Suc Suc_lessD append_Cons append_Nil diff_Suc_Suc not_less_eq nth_append)
ultimately show ?thesis
by simp
qed
qed
lemma last_numlistlist_5: "numlistlist nss ≠ [] ⟹ last (numlistlist nss) = ♯"
using numlistlist_def by (induction nss) simp_all
lemma numlistlist_wf_has2':
assumes "numlistlist_wf xs"
shows "proper_symbols_lt 6 xs ∧ (xs ≠ [] ⟶ last xs = ♯) ∧ ¬ has2 xs 𝟬 ¦ ∧ ¬ has2 xs 𝟬 ♯ ∧ ¬ has2 xs 𝟭 ♯"
proof -
obtain nss where nss: "numlistlist nss = xs"
using numlistlist_wf_def assms by auto
have "proper_symbols xs"
using nss proper_symbols_numlistlist by auto
moreover have "symbols_lt 6 xs"
using nss symbols_lt_numlistlist by auto
moreover have "xs ≠ [] ⟶ last xs = ♯"
using nss last_numlistlist_5 by auto
moreover have "¬ has2 xs 𝟬 ¦" and "¬ has2 xs 𝟬 ♯" and "¬ has2 xs 𝟭 ♯"
using numlistlist_not_has2 numlistlist_not_has2' has2_def nss by auto
ultimately show ?thesis
by simp
qed
lemma numlistlist_wf_iff:
"numlistlist_wf xs ⟷
proper_symbols_lt 6 xs ∧ (xs ≠ [] ⟶ last xs = ♯) ∧ ¬ has2 xs 𝟬 ¦ ∧ ¬ has2 xs 𝟬 ♯ ∧ ¬ has2 xs 𝟭 ♯"
using numlistlist_wf_has2 numlistlist_wf_has2' by blast
subsection ‹A Turing machine to check for subsequences of length two›
text ‹
In order to implement the well-formedness criteria we need to be able to check a
symbol sequence for subsequences of length two. The next Turing machine has
symbol parameters $y$ and $z$ and checks whether the sequence @{term "[y, z]"}
exists on tape $j_1$. It writes to tape $j_2$ the number~0 or~1 if the sequence
is present or not, respectively.
›
definition tm_not_has2 :: "symbol ⇒ symbol ⇒ tapeidx ⇒ tapeidx ⇒ machine" where
"tm_not_has2 y z j1 j2 ≡
tm_set j2 [𝟬, 𝟬] ;;
WHILE [] ; λrs. rs ! j1 ≠ □ DO
IF λrs. rs ! j2 = 𝟭 ∧ rs ! j1 = z THEN
tm_right j2 ;;
tm_write j2 𝟭 ;;
tm_left j2
ELSE
[]
ENDIF ;;
tm_trans2 j1 j2 (λh. if h = y then 𝟭 else 𝟬) ;;
tm_right j1
DONE ;;
tm_right j2 ;;
IF λrs. rs ! j2 = 𝟭 THEN
tm_set j2 (canrepr 1)
ELSE
tm_set j2 (canrepr 0)
ENDIF ;;
tm_cr j1 ;;
tm_not j2"
lemma tm_not_has2_tm:
assumes "k ≥ 2" and "G ≥ 4" and "0 < j2" and "j1 < k" and "j2 < k"
shows "turing_machine k G (tm_not_has2 y z j1 j2)"
proof -
have "symbols_lt G [𝟬, 𝟬]"
using assms(2) by (simp add: nth_Cons')
moreover have "symbols_lt G (canrepr 0)"
using assms(2) by simp
moreover have "symbols_lt G (canrepr 1)"
using assms(2) canrepr_1 by simp
ultimately show ?thesis
unfolding tm_not_has2_def
using assms tm_right_tm tm_write_tm tm_left_tm tm_cr_tm Nil_tm tm_trans2_tm tm_set_tm
turing_machine_loop_turing_machine turing_machine_branch_turing_machine tm_not_tm
by simp
qed
locale turing_machine_has2 =
fixes y z :: symbol and j1 j2 :: tapeidx
begin
context
fixes tps0 :: "tape list" and xs :: "symbol list" and k :: nat
assumes xs: "proper_symbols xs"
assumes yz: "y > 1" "z > 1"
assumes jk: "j1 < k" "j2 < k" "j1 ≠ j2" "0 < j2" "length tps0 = k"
assumes tps0:
"tps0 ! j1 = (⌊xs⌋, 1)"
"tps0 ! j2 = (⌊[]⌋, 1)"
begin
definition "tm1 ≡ tm_set j2 [𝟬, 𝟬]"
definition "tmT1 ≡ tm_right j2"
definition "tmT2 ≡ tmT1 ;; tm_write j2 𝟭"
definition "tmT3 ≡ tmT2 ;; tm_left j2"
definition "tmL1 ≡ IF λrs. rs ! j2 = 𝟭 ∧ rs ! j1 = z THEN tmT3 ELSE [] ENDIF"
definition "tmL2 ≡ tmL1 ;; tm_trans2 j1 j2 (λh. if h = y then 𝟭 else 𝟬)"
definition "tmL3 ≡ tmL2 ;; tm_right j1"
definition "tmL ≡ WHILE [] ; λrs. rs ! j1 ≠ □ DO tmL3 DONE"
definition "tm2 ≡ tm1 ;; tmL"
definition "tm3 ≡ tm2 ;; tm_right j2"
definition "tm34 ≡ IF λrs. rs ! j2 = 𝟭 THEN tm_set j2 (canrepr 1) ELSE tm_set j2 (canrepr 0) ENDIF"
definition "tm4 ≡ tm3 ;; tm34"
definition "tm5 ≡ tm4 ;; tm_cr j1"
definition "tm6 ≡ tm5 ;; tm_not j2"
lemma tm6_eq_tm_not_has2: "tm6 = tm_not_has2 y z j1 j2"
unfolding tm6_def tm5_def tm4_def tm34_def tm3_def tm2_def tmL_def tmL3_def tmL2_def tmL1_def
tmT3_def tmT2_def tmT1_def tm1_def tm_not_has2_def
by simp
definition tps1 :: "tape list" where
"tps1 ≡ tps0
[j1 := (⌊xs⌋, 1),
j2 := (⌊[𝟬, 𝟬]⌋, 1)]"
lemma tm1: "transforms tm1 tps0 14 tps1"
unfolding tm1_def
proof (tform tps: tps0 tps1_def jk)
show "∀i<length [𝟬, 𝟬]. Suc 0 < [𝟬, 𝟬] ! i"
by (simp add: nth_Cons')
show "tps1 = tps0[j2 := (⌊[𝟬, 𝟬]⌋, 1)]"
using tps1_def tps0 jk by (metis list_update_id)
qed
abbreviation has_at :: "nat ⇒ bool" where
"has_at i ≡ xs ! i = y ∧ xs ! Suc i = z"
definition tpsL :: "nat ⇒ tape list" where
"tpsL t ≡ tps0
[j1 := (⌊xs⌋, Suc t),
j2 := (⌊[if ⌊xs⌋ t = y then 𝟭 else 𝟬, if ∃i<t - 1. has_at i then 𝟭 else 𝟬]⌋, 1)]"
lemma tpsL_eq_tps1: "tpsL 0 = tps1"
unfolding tps1_def tpsL_def using yz jk by simp
lemma tm1' [transforms_intros]: "transforms tm1 tps0 14 (tpsL 0)"
using tm1 tpsL_eq_tps1 by simp
definition tpsT1 :: "nat ⇒ tape list" where
"tpsT1 t ≡ tps0
[j1 := (⌊xs⌋, Suc t),
j2 := (⌊[if ⌊xs⌋ t = y then 𝟭 else 𝟬, if ∃i<t - 1. has_at i then 𝟭 else 𝟬]⌋, 2)]"
definition tpsT2 :: "nat ⇒ tape list" where
"tpsT2 t ≡ tps0
[j1 := (⌊xs⌋, Suc t),
j2 := (⌊[if ⌊xs⌋ t = y then 𝟭 else 𝟬, if ∃i<t. has_at i then 𝟭 else 𝟬]⌋, 2)]"
definition tpsT3 :: "nat ⇒ tape list" where
"tpsT3 t ≡ tps0
[j1 := (⌊xs⌋, Suc t),
j2 := (⌊[if ⌊xs⌋ t = y then 𝟭 else 𝟬, if ∃i<t. has_at i then 𝟭 else 𝟬]⌋, 1)]"
lemma contents_1_update: "(⌊[a, b]⌋, 1) |:=| v = (⌊[v, b]⌋, 1)" for a b v :: symbol
using contents_def by auto
lemma contents_2_update: "(⌊[a, b]⌋, 2) |:=| v = (⌊[a, v]⌋, 2)" for a b v :: symbol
using contents_def by auto
context
fixes t :: nat
assumes then_branch: "⌊xs⌋ t = y" "xs ! t = z"
begin
lemma tmT1 [transforms_intros]: "transforms tmT1 (tpsL t) 1 (tpsT1 t)"
unfolding tmT1_def
proof (tform tps: tpsL_def tpsT1_def jk)
have "tpsL t ! j2 |+| 1 = (⌊[if ⌊xs⌋ t = y then 𝟭 else 𝟬, if ∃i<t - 1. has_at i then 𝟭 else 𝟬]⌋, 2)"
using jk tpsL_def by simp
moreover have "tpsT1 t = (tpsL t)[j2 := (⌊[if ⌊xs⌋ t = y then 𝟭 else 𝟬, if ∃i<t - 1. has_at i then 𝟭 else 𝟬]⌋, 2)]"
unfolding tpsT1_def tpsL_def by simp
ultimately show "tpsT1 t = (tpsL t)[j2 := tpsL t ! j2 |+| 1]"
by presburger
qed
lemma tmT2 [transforms_intros]: "transforms tmT2 (tpsL t) 2 (tpsT2 t)"
unfolding tmT2_def
proof (tform tps: tpsT1_def tpsT2_def jk)
have 1: "tpsT1 t ! j2 = (⌊[if ⌊xs⌋ t = y then 𝟭 else 𝟬, if ∃i<t - 1. has_at i then 𝟭 else 𝟬]⌋, 2)"
using tpsT1_def jk by simp
have 2: "tpsT1 t ! j2 |:=| 𝟭 = (⌊[if ⌊xs⌋ t = y then 𝟭 else 𝟬, 𝟭]⌋, 2)"
using tpsT1_def jk contents_2_update by simp
have 3: "tpsT2 t ! j2 = (⌊[if ⌊xs⌋ t = y then 𝟭 else 𝟬, if ∃i<t. has_at i then 𝟭 else 𝟬]⌋, 2)"
using tpsT2_def jk by simp
have "∃i<t. has_at i"
proof -
have "t > 0"
using then_branch(1) yz(1) by (metis contents_at_0 gr0I less_numeral_extra(4))
then have "y = xs ! (t - 1)"
using then_branch(1) by (metis contents_def nat_neq_iff not_one_less_zero yz(1))
moreover have "z = xs ! t"
using then_branch(2) by simp
ultimately have "has_at (t - 1)"
using `0 < t` by simp
then show "∃i<t. has_at i"
using `0 < t` by (metis Suc_pred' lessI)
qed
then have "(if ∃i<t. has_at i then 𝟭 else 𝟬) = 𝟭"
by simp
then have "tpsT1 t ! j2 |:=| 𝟭 = (⌊[if ⌊xs⌋ t = y then 𝟭 else 𝟬, if ∃i<t. has_at i then 𝟭 else 𝟬]⌋, 2)"
using 2 3 by (smt (verit, ccfv_threshold))
then show "tpsT2 t = (tpsT1 t)[j2 := tpsT1 t ! j2 |:=| 𝟭]"
unfolding tpsT2_def tpsT1_def using jk by simp
qed
lemma tmT3 [transforms_intros]: "transforms tmT3 (tpsL t) 3 (tpsT3 t)"
unfolding tmT3_def by (tform tps: tpsT2_def tpsT3_def jk)
end
lemma tmL1 [transforms_intros]:
assumes "ttt = 5" and "t < length xs"
shows "transforms tmL1 (tpsL t) ttt (tpsT3 t)"
unfolding tmL1_def
proof (tform tps: assms(1) tpsL_def tpsT3_def jk)
have "read (tpsL t) ! j1 = tpsL t :.: j1"
using jk tpsL_def tapes_at_read'[of j1 "tpsL t"] by simp
then have 1: "read (tpsL t) ! j1 = xs ! t"
using jk tpsL_def assms(2) by simp
then show "read (tpsL t) ! j2 = 𝟭 ∧ read (tpsL t) ! j1 = z ⟹ xs ! t = z"
by simp
have "read (tpsL t) ! j2 = tpsL t :.: j2"
using jk tpsL_def tapes_at_read'[of j2 "tpsL t"] by simp
then have 2: "read (tpsL t) ! j2 = (if ⌊xs⌋ t = y then 𝟭 else 𝟬)"
using jk tpsL_def by simp
then show "read (tpsL t) ! j2 = 𝟭 ∧ read (tpsL t) ! j1 = z ⟹ ⌊xs⌋ t = y"
by presburger
show "tpsT3 t = tpsL t" if "¬ (read (tpsL t) ! j2 = 𝟭 ∧ read (tpsL t) ! j1 = z)"
proof -
have "(∃i<t. has_at i) = (∃i<t - 1. has_at i)"
proof (cases "t = 0")
case True
then show ?thesis
by simp
next
case False
have "¬ ((if ⌊xs⌋ t = y then 0::symbol else 1) = 0 ∧ xs ! t = z)"
using 1 2 that by simp
then have "¬ (⌊xs⌋ t = y ∧ xs ! t = z)"
by auto
then have "¬ (has_at (t - 1))"
using False Suc_pred' assms(2) contents_inbounds less_imp_le_nat by simp
moreover have "(∃i<t. has_at i) = (∃i<t - Suc 0. has_at i) ∨ has_at (t - 1)"
using False by (metis One_nat_def add_diff_inverse_nat less_Suc_eq less_one plus_1_eq_Suc)
ultimately show ?thesis
by auto
qed
then have eq: "(if ∃i<t - 1. has_at i then 𝟭 else 𝟬) = (if ∃i<t. has_at i then 𝟭 else 𝟬)"
by simp
show ?thesis
unfolding tpsT3_def tpsL_def by (simp only: eq)
qed
qed
definition tpsL2 :: "nat ⇒ tape list" where
"tpsL2 t ≡ tps0
[j1 := (⌊xs⌋, Suc t),
j2 := (⌊[if ⌊xs⌋ (Suc t) = y then 𝟭 else 𝟬, if ∃i<t. has_at i then 𝟭 else 𝟬]⌋, 1)]"
lemma tmL2 [transforms_intros]:
assumes "ttt = 6" and "t < length xs"
shows "transforms tmL2 (tpsL t) ttt (tpsL2 t)"
unfolding tmL2_def
proof (tform tps: assms tpsL_def tpsT3_def jk)
have "tpsT3 t ! j2 = (⌊[if ⌊xs⌋ t = y then 𝟭 else 𝟬, if ∃i<t. has_at i then 𝟭 else 𝟬]⌋, 1)"
using jk tpsT3_def by simp
then have "tpsT3 t ! j2 |:=| (if tpsT3 t :.: j1 = y then 𝟭 else 𝟬) =
(⌊[if tpsT3 t :.: j1 = y then 𝟭 else 𝟬, if ∃i<t. has_at i then 𝟭 else 𝟬]⌋, 1)"
using contents_1_update by simp
moreover have "tpsT3 t :.: j1 = ⌊xs⌋ (Suc t)"
using assms(2) tpsT3_def jk by simp
ultimately have "tpsT3 t ! j2 |:=| (if tpsT3 t :.: j1 = y then 𝟭 else 𝟬) =
(⌊[if ⌊xs⌋ (Suc t) = y then 𝟭 else 𝟬, if ∃i<t. has_at i then 𝟭 else 𝟬]⌋, 1)"
by auto
moreover have "tpsL2 t = (tpsT3 t)[j2 := (⌊[if ⌊xs⌋ (Suc t) = y then 𝟭 else 𝟬, if ∃i<t. has_at i then 𝟭 else 𝟬]⌋, 1)]"
using tpsL2_def tpsT3_def by simp
ultimately show "tpsL2 t = (tpsT3 t)[j2 := tpsT3 t ! j2 |:=| (if tpsT3 t :.: j1 = y then 𝟭 else 𝟬)]"
by presburger
qed
lemma tmL3 [transforms_intros]:
assumes "ttt = 7" and "t < length xs"
shows "transforms tmL3 (tpsL t) ttt (tpsL (Suc t))"
unfolding tmL3_def
proof (tform tps: assms tpsL_def tpsL2_def jk)
have "tpsL2 t ! j1 = (⌊xs⌋, Suc t)"
using tpsL2_def jk by simp
then show "tpsL (Suc t) = (tpsL2 t)[j1 := tpsL2 t ! j1 |+| 1]"
using tpsL2_def tpsL_def jk by (simp add: list_update_swap)
qed
lemma tmL [transforms_intros]:
assumes "ttt = 9 * length xs + 1"
shows "transforms tmL (tpsL 0) ttt (tpsL (length xs))"
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 = ⌊xs⌋ (Suc t)" for t
using tpsL_def jk by simp
then show "⋀t. t < length xs ⟹ read (tpsL t) ! j1 ≠ □" and "¬ read (tpsL (length xs)) ! j1 ≠ □"
using xs by auto
qed
lemma tm2 [transforms_intros]:
assumes "ttt = 9 * length xs + 15"
shows "transforms tm2 tps0 ttt (tpsL (length xs))"
unfolding tm2_def by (tform tps: assms tpsL_def jk)
definition tps3 :: "tape list" where
"tps3 ≡ tps0
[j1 := (⌊xs⌋, Suc (length xs)),
j2 := (⌊[if ⌊xs⌋ (length xs) = y then 𝟭 else 𝟬, if ∃i<length xs - 1. has_at i then 𝟭 else 𝟬]⌋, 2)]"
lemma tm3 [transforms_intros]:
assumes "ttt = 9 * length xs + 16"
shows "transforms tm3 tps0 ttt tps3"
unfolding tm3_def
proof (tform tps: assms tpsL_def jk)
show "tps3 = (tpsL (length xs))[j2 := tpsL (length xs) ! j2 |+| 1]"
unfolding tps3_def tpsL_def
using jk
by (metis (no_types, lifting) One_nat_def Suc_1 add.right_neutral add_Suc_right fst_conv length_list_update
list_update_overwrite nth_list_update_eq snd_conv)
qed
definition tps4 :: "tape list" where
"tps4 ≡ tps0
[j1 := (⌊xs⌋, Suc (length xs)),
j2 := (⌊∃i<length xs - Suc 0. has_at i⌋⇩B, 1)]"
lemma tm34 [transforms_intros]:
assumes "ttt = 19"
shows "transforms tm34 tps3 ttt tps4"
unfolding tm34_def
proof (tform tps: assms tps4_def tps3_def jk)
let ?pair = "[if ⌊xs⌋ (length xs) = y then 𝟭 else 𝟬, if ∃i<length xs - Suc 0. has_at i then 𝟭 else 𝟬]"
show 1: "proper_symbols ?pair" and "proper_symbols ?pair"
by (simp_all add: nth_Cons')
show "proper_symbols (canrepr 1)"
using proper_symbols_canrepr by simp
have "read tps3 ! j2 = (if ∃i<length xs - Suc 0. has_at i then 𝟭 else 𝟬)"
using jk tps3_def tapes_at_read'[of j2 tps3] by simp
then have *: "read tps3 ! j2 = 𝟭 ⟷ (∃i<length xs - Suc 0. has_at i)"
by simp
show "clean_tape (tps3 ! j2)" "clean_tape (tps3 ! j2)"
using jk tps3_def clean_contents_proper[OF 1] by simp_all
show "tps4 = tps3[j2 := (⌊1⌋⇩N, 1)]" if "read tps3 ! j2 = 𝟭"
proof -
have "∃i<length xs - Suc 0. has_at i"
using that * by simp
then have "(⌊∃i<length xs - Suc 0. has_at i⌋⇩B, 1) = (⌊1⌋⇩N, 1)"
by simp
then have "tps4 = tps0
[j1 := (⌊xs⌋, Suc (length xs)),
j2 := (⌊1⌋⇩N, 1)]"
using tps4_def by simp
then show ?thesis
using tps3_def by simp
qed
show "tps4 = tps3[j2 := (⌊0⌋⇩N, 1)]" if "read tps3 ! j2 ≠ 𝟭"
proof -
have "¬ (∃i<length xs - Suc 0. has_at i)"
using that * by simp
then have "(⌊∃i<length xs - Suc 0. has_at i⌋⇩B, 1) = (⌊0⌋⇩N, 1)"
by auto
then have "tps4 = tps0
[j1 := (⌊xs⌋, Suc (length xs)),
j2 := (⌊0⌋⇩N, 1)]"
using tps4_def by simp
then show ?thesis
using tps3_def by simp
qed
have "tps3 :#: j2 = 2"
using jk tps3_def by simp
then show "8 + tps3 :#: j2 + 2 * length ?pair + Suc (2 * nlength 1) + 2 ≤ ttt"
and "8 + tps3 :#: j2 + 2 * length ?pair + Suc (2 * nlength 0) + 1 ≤ ttt"
using assms nlength_1_simp by simp_all
qed
lemma tm4:
assumes "ttt = 9 * length xs + 35"
shows "transforms tm4 tps0 ttt tps4"
unfolding tm4_def by (tform tps: assms)
definition tps4' :: "tape list" where
"tps4' ≡ tps0
[j1 := (⌊xs⌋, Suc (length xs)),
j2 := (⌊has2 xs y z⌋⇩B, 1)]"
lemma tps4': "tps4 = tps4'"
using has2_def tps4_def tps4'_def by simp
lemma tm4' [transforms_intros]:
assumes "ttt = 9 * length xs + 35"
shows "transforms tm4 tps0 ttt tps4'"
using assms tm4 tps4' by simp
definition tps5 :: "tape list" where
"tps5 ≡ tps0
[j1 := (⌊xs⌋, 1),
j2 := (⌊has2 xs y z ⌋⇩B, 1)]"
lemma tm5:
assumes "ttt = 10 * length xs + 38"
shows "transforms tm5 tps0 ttt tps5"
unfolding tm5_def
proof (tform tps: assms tps4'_def jk)
show "clean_tape (tps4' ! j1)"
using tps4'_def jk xs by simp
have "tps4' ! j1 |#=| 1 = (⌊xs⌋, 1)"
using tps4'_def jk by simp
then show "tps5 = tps4'[j1 := tps4' ! j1 |#=| 1]"
using tps5_def tps4'_def jk by (simp add: list_update_swap)
qed
definition tps5' :: "tape list" where
"tps5' ≡ tps0
[j2 := (⌊has2 xs y z⌋⇩B, 1)]"
lemma tm5' [transforms_intros]:
assumes "ttt = 10 * length xs + 38"
shows "transforms tm5 tps0 ttt tps5'"
proof -
have "tps5 = tps5'"
using tps5_def tps5'_def jk tps0(1) by (metis list_update_id)
then show ?thesis
using assms tm5 by simp
qed
definition tps6 :: "tape list" where
"tps6 ≡ tps0
[j2 := (⌊¬ has2 xs y z⌋⇩B, 1)]"
lemma tm6:
assumes "ttt = 10 * length xs + 41"
shows "transforms tm6 tps0 ttt tps6"
unfolding tm6_def
proof (tform tps: assms tps5'_def jk)
have "tps5'[j2 := (⌊(if has2 xs y z then 1::nat else 0) ≠ 1⌋⇩B, 1)] =
tps5'[j2 := (⌊¬ has2 xs y z⌋⇩B, 1)]"
by simp
also have "... = tps0[j2 := (⌊¬ has2 xs y z⌋⇩B, 1)]"
using tps5'_def by simp
also have "... = tps6"
using tps6_def by simp
finally show "tps6 = tps5'
[j2 := (⌊(if has2 xs y z then 1::nat else 0) ≠ 1⌋⇩B, 1)]"
by simp
qed
end
end
lemma transforms_tm_not_has2I [transforms_intros]:
fixes y z :: symbol and j1 j2 :: tapeidx
fixes tps tps' :: "tape list" and xs :: "symbol list" and ttt k :: nat
assumes "j1 < k" "j2 < k" "j1 ≠ j2" "0 < j2" "length tps = k" "y > 1" "z > 1"
and "proper_symbols xs"
assumes
"tps ! j1 = (⌊xs⌋, 1)"
"tps ! j2 = (⌊[]⌋, 1)"
assumes "ttt = 10 * length xs + 41"
assumes "tps' = tps
[j2 := (⌊¬ has2 xs y z⌋⇩B, 1)]"
shows "transforms (tm_not_has2 y z j1 j2) tps ttt tps'"
proof -
interpret loc: turing_machine_has2 y z j1 j2 .
show ?thesis
using loc.tps6_def loc.tm6 loc.tm6_eq_tm_not_has2 assms by metis
qed
subsection ‹Checking well-formedness for lists›
text ‹
The next Turing machine checks all conditions from the criterion in lemma @{thm
[source] numlist_wf_iff} one after another for the symbols on tape $j_1$ and
writes to tape $j_2$ either the number~1 or~0 depending on whether all
conditions were met. It assumes tape $j_2$ is initialized with~0.
›
definition tm_numlist_wf :: "tapeidx ⇒ tapeidx ⇒ machine" where
"tm_numlist_wf j1 j2 ≡
tm_proper_symbols_lt j1 j2 5 ;;
tm_not_has2 𝟬 ¦ j1 (j2 + 1) ;;
tm_and j2 (j2 + 1) ;;
tm_setn (j2 + 1) 0 ;;
tm_empty_or_endswith j1 (j2 + 1) ¦ ;;
tm_and j2 (j2 + 1) ;;
tm_setn (j2 + 1) 0"
lemma tm_numlist_wf_tm:
assumes "k ≥ 2" and "G ≥ 5" and "0 < j2" "0 < j1" and "j1 < k" "j2 + 1 < k"
shows "turing_machine k G (tm_numlist_wf j1 j2)"
using tm_numlist_wf_def tm_proper_symbols_lt_tm tm_not_has2_tm tm_and_tm tm_setn_tm tm_empty_or_endswith_tm assms
by simp
locale turing_machine_numlist_wf =
fixes j1 j2 :: tapeidx
begin
definition "tm1 ≡ tm_proper_symbols_lt j1 j2 5"
definition "tm2 ≡ tm1 ;; tm_not_has2 𝟬 ¦ j1 (j2 + 1)"
definition "tm3 ≡ tm2 ;; tm_and j2 (j2 + 1)"
definition "tm4 ≡ tm3 ;; tm_setn (j2 + 1) 0"
definition "tm5 ≡ tm4 ;; tm_empty_or_endswith j1 (j2 + 1) ¦"
definition "tm6 ≡ tm5 ;; tm_and j2 (j2 + 1)"
definition "tm7 ≡ tm6 ;; tm_setn (j2 + 1) 0"
lemma tm7_eq_tm_numlist_wf: "tm7 = tm_numlist_wf j1 j2"
unfolding tm7_def tm6_def tm5_def tm4_def tm3_def tm2_def tm1_def tm_numlist_wf_def
by simp
context
fixes tps0 :: "tape list" and zs :: "symbol list" and k :: nat
assumes zs: "proper_symbols zs"
assumes jk: "0 < j1" "j1 < k" "j2 + 1 < k" "j1 ≠ j2" "0 < j2" "j1 ≠ j2 + 1" "length tps0 = k"
assumes tps0:
"tps0 ! j1 = (⌊zs⌋, 1)"
"tps0 ! j2 = (⌊[]⌋, 1)"
"tps0 ! (j2 + 1) = (⌊[]⌋, 1)"
begin
definition "tps1 ≡ tps0
[j2 := (⌊proper_symbols_lt 5 zs⌋⇩B, 1)]"
lemma tm1 [transforms_intros]:
assumes "ttt = 5 + 7 * length zs"
shows "transforms tm1 tps0 ttt tps1"
unfolding tm1_def
by (tform tps: zs tps0 assms tps1_def jk)
definition "tps2 ≡ tps0
[j2 := (⌊proper_symbols_lt 5 zs⌋⇩B, 1),
j2 + 1 := (⌊if has2 zs 𝟬 ¦ then 0 else 1⌋⇩N, 1)]"
lemma tm2 [transforms_intros]:
assumes "ttt = 46 + 17 * length zs"
shows "transforms tm2 tps0 ttt tps2"
unfolding tm2_def
by (tform tps: zs tps0 assms tps1_def tps2_def jk)
definition "tps3 ≡ tps0
[j2 := (⌊proper_symbols_lt 5 zs ∧ ¬ has2 zs 𝟬 ¦⌋⇩B, 1),
j2 + 1 := (⌊if has2 zs 𝟬 ¦ then 0 else 1⌋⇩N, 1)]"
lemma tm3 [transforms_intros]:
assumes "ttt = 46 + 17 * length zs + 3"
shows "transforms tm3 tps0 ttt tps3"
unfolding tm3_def by (tform tps: assms tps2_def tps3_def jk)
definition "tps4 ≡ tps0
[j2 := (⌊proper_symbols_lt 5 zs ∧ ¬ has2 zs 𝟬 ¦⌋⇩B, 1),
j2 + 1 := (⌊0⌋⇩N, 1)]"
lemma tm4:
assumes "ttt = 46 + 17 * length zs + 13 + 2 * nlength (if has2 zs 𝟬 ¦ then 0 else 1)"
shows "transforms tm4 tps0 ttt tps4"
unfolding tm4_def by (tform tps: assms tps3_def tps4_def jk)
lemma tm4' [transforms_intros]:
assumes "ttt = 46 + 17 * length zs + 15"
shows "transforms tm4 tps0 ttt tps4"
using assms nlength_0 nlength_1_simp tm4 transforms_monotone by simp
definition "tps5 ≡ tps0
[j2 := (⌊proper_symbols_lt 5 zs ∧ ¬ has2 zs 𝟬 ¦⌋⇩B, 1),
j2 + 1 := (⌊zs = [] ∨ last zs = ¦⌋⇩B, 1)]"
lemma tm5 [transforms_intros]:
assumes "ttt = 79 + 19 * length zs"
shows "transforms tm5 tps0 ttt tps5"
unfolding tm5_def by (tform tps: tps4_def tps5_def jk zs tps0 assms)
definition "tps6 ≡ tps0
[j2 := (⌊proper_symbols_lt 5 zs ∧ ¬ has2 zs 𝟬 ¦ ∧ (zs = [] ∨ last zs = ¦)⌋⇩B, 1),
j2 + 1 := (⌊zs = [] ∨ last zs = ¦⌋⇩B, 1)]"
lemma tm6 [transforms_intros]:
assumes "ttt = 82 + 19 * length zs"
shows "transforms tm6 tps0 ttt tps6"
unfolding tm6_def by (tform tps: tps5_def tps6_def jk time: assms)
definition "tps7 ≡ tps0
[j2 := (⌊proper_symbols_lt 5 zs ∧ ¬ has2 zs 𝟬 ¦ ∧ (zs = [] ∨ last zs = ¦)⌋⇩B, 1),
j2 + 1 := (⌊0⌋⇩N, 1)]"
lemma tm7:
assumes "ttt = 92 + 19 * length zs + 2 * nlength (if zs = [] ∨ last zs = ¦ then 1 else 0)"
shows "transforms tm7 tps0 ttt tps7"
unfolding tm7_def by (tform tps: assms tps6_def tps7_def jk)
definition "tps7' ≡ tps0
[j2 := (⌊numlist_wf zs⌋⇩B, 1),
j2 + 1 := (⌊0⌋⇩N, 1)]"
lemma tm7':
assumes "ttt = 94 + 19 * length zs"
shows "transforms tm7 tps0 ttt tps7'"
proof -
have "ttt ≥ 92 + 19 * length zs + 2 * nlength (if zs = [] ∨ last zs = ¦ then 1 else 0)"
using assms nlength_1_simp by auto
moreover have "tps7' = tps7"
using tps7'_def tps7_def numlist_wf_iff by auto
ultimately show ?thesis
using transforms_monotone tm7 by simp
qed
definition "tps7'' ≡ tps0
[j2 := (⌊numlist_wf zs⌋⇩B, 1)]"
lemma tm7'' [transforms_intros]:
assumes "ttt = 94 + 19 * length zs"
shows "transforms tm7 tps0 ttt tps7''"
proof -
have "tps7'' = tps7'"
unfolding tps7''_def tps7'_def using tps0 jk canrepr_0
by (metis add_gr_0 less_add_same_cancel1 list_update_id list_update_swap_less zero_less_two)
then show ?thesis
using tm7' assms by simp
qed
end
end
lemma transforms_tm_numlist_wfI [transforms_intros]:
fixes j1 j2 :: tapeidx
fixes tps tps' :: "tape list" and zs :: "symbol list" and ttt k :: nat
assumes "0 < j1" "j1 < k" "j2 + 1 < k" "j1 ≠ j2" "0 < j2" "j1 ≠ j2 + 1" "length tps = k"
and "proper_symbols zs"
assumes
"tps ! j1 = (⌊zs⌋, 1)"
"tps ! j2 = (⌊[]⌋, 1)"
"tps ! (j2 + 1) = (⌊[]⌋, 1)"
assumes "ttt = 94 + 19 * length zs"
assumes "tps' = tps
[j2 := (⌊numlist_wf zs⌋⇩B, 1)]"
shows "transforms (tm_numlist_wf j1 j2) tps ttt tps'"
proof -
interpret loc: turing_machine_numlist_wf j1 j2 .
show ?thesis
using assms loc.tps7''_def loc.tm7'' loc.tm7_eq_tm_numlist_wf by simp
qed
subsection ‹Checking well-formedness for lists of lists›
text ‹
The next Turing machine checks all conditions from the criterion in lemma @{thm
[source] numlistlist_wf_iff} one after another for the symbols on tape $j_1$ and
writes to tape $j_2$ either the number~1 or~0 depending on whether all
conditions were met. It assumes tape $j_2$ is initialized with~0.
›
definition tm_numlistlist_wf :: "tapeidx ⇒ tapeidx ⇒ machine" where
"tm_numlistlist_wf j1 j2 ≡
tm_proper_symbols_lt j1 j2 6 ;;
tm_not_has2 𝟬 ¦ j1 (j2 + 1) ;;
tm_and j2 (j2 + 1) ;;
tm_setn (j2 + 1) 0 ;;
tm_empty_or_endswith j1 (j2 + 1) ♯ ;;
tm_and j2 (j2 + 1) ;;
tm_setn (j2 + 1) 0 ;;
tm_not_has2 𝟬 ♯ j1 (j2 + 1) ;;
tm_and j2 (j2 + 1) ;;
tm_setn (j2 + 1) 0 ;;
tm_not_has2 𝟭 ♯ j1 (j2 + 1) ;;
tm_and j2 (j2 + 1) ;;
tm_setn (j2 + 1) 0"
lemma tm_numlistlist_wf_tm:
assumes "k ≥ 2" and "G ≥ 6" and "0 < j2" "0 < j1" and "j1 < k" "j2 + 1 < k"
shows "turing_machine k G (tm_numlistlist_wf j1 j2)"
using tm_numlistlist_wf_def tm_proper_symbols_lt_tm tm_not_has2_tm tm_and_tm tm_setn_tm tm_empty_or_endswith_tm assms
by simp
locale turing_machine_numlistlist_wf =
fixes j1 j2 :: tapeidx
begin
definition "tm1 ≡ tm_proper_symbols_lt j1 j2 6"
definition "tm2 ≡ tm1 ;; tm_not_has2 𝟬 ¦ j1 (j2 + 1)"
definition "tm3 ≡ tm2 ;; tm_and j2 (j2 + 1)"
definition "tm4 ≡ tm3 ;; tm_setn (j2 + 1) 0"
definition "tm5 ≡ tm4 ;; tm_empty_or_endswith j1 (j2 + 1) ♯"
definition "tm6 ≡ tm5 ;; tm_and j2 (j2 + 1)"
definition "tm7 ≡ tm6 ;; tm_setn (j2 + 1) 0"
definition "tm8 ≡ tm7 ;; tm_not_has2 𝟬 ♯ j1 (j2 + 1)"
definition "tm9 ≡ tm8 ;; tm_and j2 (j2 + 1)"
definition "tm10 ≡ tm9 ;; tm_setn (j2 + 1) 0"
definition "tm11 ≡ tm10 ;; tm_not_has2 𝟭 ♯ j1 (j2 + 1)"
definition "tm12 ≡ tm11 ;; tm_and j2 (j2 + 1)"
definition "tm13 ≡ tm12 ;; tm_setn (j2 + 1) 0"
lemma tm13_eq_tm_numlistlist_wf: "tm13 = tm_numlistlist_wf j1 j2"
unfolding tm13_def tm12_def tm11_def tm10_def tm9_def tm8_def tm7_def tm6_def tm5_def
tm4_def tm3_def tm2_def tm1_def tm_numlistlist_wf_def
by simp
context
fixes tps0 :: "tape list" and zs :: "symbol list" and k :: nat
assumes zs: "proper_symbols zs"
assumes jk: "0 < j1" "j1 < k" "j2 + 1 < k" "j1 ≠ j2" "0 < j2" "j1 ≠ j2