Theory Numerals
section ‹Encoding of Natural Numbers›
theory Numerals
imports ComposedTMs BlanksDoNotMatter
begin
subsection ‹A class for generating numerals›
class tape =
fixes tape_of :: "'a ⇒ cell list" (‹<_>› 100)
instantiation nat::tape begin
definition tape_of_nat where "tape_of_nat (n::nat) ≡ Oc ↑ (Suc n)"
instance by standard
end
type_synonym nat_list = "nat list"
instantiation list::(tape) tape begin
fun tape_of_nat_list :: "('a::tape) list ⇒ cell list"
where
"tape_of_nat_list [] = []" |
"tape_of_nat_list [n] = <n>" |
"tape_of_nat_list (n#ns) = <n> @ Bk # (tape_of_nat_list ns)"
definition tape_of_list where "tape_of_list ≡ tape_of_nat_list"
instance by standard
end
instantiation prod:: (tape, tape) tape begin
fun tape_of_nat_prod :: "('a::tape) × ('b::tape) ⇒ cell list"
where "tape_of_nat_prod (n, m) = <n> @ [Bk] @ <m>"
definition tape_of_prod where "tape_of_prod ≡ tape_of_nat_prod"
instance by standard
end
subsection ‹Some lemmas about numerals used for rewriting›
lemma tape_of_list_empty[simp]: "<[]> = ([]::cell list)" by (simp add: tape_of_list_def)
lemma tape_of_nat_list_cases2: "<(nl::nat list)> = [] ∨ (∃r'. <nl> = Oc # r')"
by (induct rule: tape_of_nat_list.induct)(auto simp add: tape_of_nat_def tape_of_list_def)
subsection ‹Unique decomposition of standard tapes›
text ‹Some lemmas about unique decomposition of tapes in standard halting configuration.
›
lemma OcSuc_lemma: "Oc # Oc ↑ n1 = Oc ↑ n2 ⟹ Suc n1 = n2"
proof (induct n1 arbitrary: n2)
case 0
then have A: "Oc # Oc ↑ 0 = Oc ↑ n2" .
then show ?case
proof -
from A have "[Oc] = Oc ↑ n2" by auto
moreover have "[Oc] = Oc ↑ n2 ⟹ Suc 0 = n2"
by (induct n2)auto
ultimately show ?case by auto
qed
next
fix n1 n2
assume IV1: "⋀n2. Oc # Oc ↑ n1 = Oc ↑ n2 ⟹ Suc n1 = n2"
and IV2: "Oc # Oc ↑ Suc n1 = Oc ↑ n2"
show "Suc (Suc n1) = n2"
proof (cases n2)
case 0
then have "Oc ↑ n2 = []" by auto
with IV2 have False by auto
then show ?thesis by auto
next
case (Suc n3)
then have "n2 = Suc n3" .
with IV2 have "Oc # Oc ↑ Suc n1 = Oc ↑ (Suc n3)" by auto
then have "Oc # Oc # Oc ↑ n1 = Oc # Oc ↑ n3" by auto
then have "Oc # Oc ↑ n1 = Oc ↑ n3" by auto
with IV1 have "Suc n1 = n3" by auto
then have "Suc (Suc n1) = Suc n3" by auto
with ‹n2 = Suc n3› show ?thesis by auto
qed
qed
lemma inj_tape_of_list: "(<n1::nat>) = (<n2::nat>) ⟹ n1 = n2"
by (induct n1 arbitrary: n2) (auto simp add: OcSuc_lemma tape_of_nat_def)
lemma inj_repl_Bk: "Bk ↑ k1 = Bk ↑ k2 ⟹ k1 = k2" by auto
lemma last_of_numeral_is_Oc: "last (<n::nat>) = Oc"
by (auto simp add: tape_of_nat_def)
lemma hd_of_numeral_is_Oc: "hd (<n::nat>) = Oc"
by (auto simp add: tape_of_nat_def)
lemma rev_replicate: "rev (Bk ↑ l1) = (Bk ↑ l1)" by auto
lemma rev_numeral: "rev (<n::nat>) = <n::nat>"
by (induct n)(auto simp add: tape_of_nat_def)
lemma drop_Bk_prefix: "n < l ⟹ hd (drop n ((Bk ↑ l) @ xs)) = Bk"
by (induct n arbitrary: l xs)(auto)
lemma unique_Bk_postfix: "<n1::nat> @ Bk ↑ l1 = <n2::nat> @ Bk ↑ l2 ⟹ l1 = l2"
proof -
assume "<n1::nat> @ Bk ↑ l1 = <n2::nat> @ Bk ↑ l2"
then have "rev (<n1::nat> @ Bk ↑ l1) = rev (<n2::nat> @ Bk ↑ l2)"
by auto
then have "rev (Bk ↑ l1) @ rev (<n1::nat>) = rev (Bk ↑ l2) @ rev (<n2::nat>)" by auto
then have A: "(Bk ↑ l1) @ (<n1::nat>) = (Bk ↑ l2) @ (<n2::nat>)"
by (auto simp add: rev_replicate rev_numeral)
then show "l1 = l2"
proof (cases "l1 = l2")
case True
then show ?thesis by auto
next
case False
then have "l1 < l2 ∨ l2 < l1" by auto
then show ?thesis
proof
assume "l1 < l2 "
then have False
proof -
have "hd (drop l1 (Bk ↑ l1) @ (<n1::nat>)) = hd ( <n1::nat>)" by auto
also have "... = Oc" by (auto simp add: hd_of_numeral_is_Oc)
finally have F1: "hd (drop l1 (Bk ↑ l1) @ (<n1::nat>)) = Oc" .
from ‹l1 < l2›have "hd (drop l1 ((Bk ↑ l2) @ (<n2::nat>))) = Bk"
by (auto simp add: drop_Bk_prefix)
with A have "hd (drop l1 ((Bk ↑ l1) @ (<n1::nat>))) = Bk" by auto
with F1 show False by auto
qed
then show ?thesis by auto
next
assume "l2 < l1"
then have False
proof -
have "hd (drop l2 (Bk ↑ l2) @ (<n2::nat>)) = hd ( <n2::nat>)" by auto
also have "... = Oc" by (auto simp add: hd_of_numeral_is_Oc)
finally have F2: "hd (drop l2 (Bk ↑ l2) @ (<n2::nat>)) = Oc" .
from ‹l2 < l1› have "hd (drop l2 ((Bk ↑ l1) @ (<n1::nat>))) = Bk"
by (auto simp add: drop_Bk_prefix)
with A have "hd (drop l2 ((Bk ↑ l2) @ (<n2::nat>))) = Bk" by auto
with F2 show False by auto
qed
then show ?thesis by auto
qed
qed
qed
lemma unique_decomp_tap:
assumes "(lx, <n1::nat> @ Bk ↑ l1) = (ly, <n2::nat> @ Bk ↑ l2)"
shows "lx=ly ∧ n1=n2 ∧ l1=l2"
proof
from assms show "lx = ly " by auto
next
show "n1 = n2 ∧ l1 = l2"
proof
from assms have major: "<n1::nat> @ Bk ↑ l1 = <n2::nat> @ Bk ↑ l2" by auto
then have "rev (<n1::nat> @ Bk ↑ l1) = rev (<n2::nat> @ Bk ↑ l2)"
by auto
then have "rev (Bk ↑ l1) @ rev (<n1::nat>) = rev (Bk ↑ l2) @ rev (<n2::nat>)" by auto
then have A: "(Bk ↑ l1) @ (<n1::nat>) = (Bk ↑ l2) @ (<n2::nat>)"
by (auto simp add: rev_replicate rev_numeral)
then show "n1 = n2"
proof -
from major have "l1 = l2" by (rule unique_Bk_postfix)
with A have "(<n1::nat>) = (<n2::nat>)" by auto
then show "n1 = n2" by (rule inj_tape_of_list)
qed
next
from assms have major: "<n1::nat> @ Bk ↑ l1 = <n2::nat> @ Bk ↑ l2" by auto
then show "l1 = l2" by (rule unique_Bk_postfix)
qed
qed
lemma unique_decomp_std_tap:
assumes "(Bk ↑ k1, <n1::nat> @ Bk ↑ l1) = (Bk ↑ k2, <n2::nat> @ Bk ↑ l2)"
shows "k1=k2 ∧ n1=n2 ∧ l1=l2"
proof
from assms have "Bk ↑ k1 = Bk ↑ k2" by auto
then show "k1 = k2" by auto
next
show "n1 = n2 ∧ l1 = l2"
proof
from assms have major: "<n1::nat> @ Bk ↑ l1 = <n2::nat> @ Bk ↑ l2" by auto
then have "rev (<n1::nat> @ Bk ↑ l1) = rev (<n2::nat> @ Bk ↑ l2)"
by auto
then have "rev (Bk ↑ l1) @ rev (<n1::nat>) = rev (Bk ↑ l2) @ rev (<n2::nat>)" by auto
then have A: "(Bk ↑ l1) @ (<n1::nat>) = (Bk ↑ l2) @ (<n2::nat>)"
by (auto simp add: rev_replicate rev_numeral)
then show "n1 = n2"
proof -
from major have "l1 = l2" by (rule unique_Bk_postfix)
with A have "(<n1::nat>) = (<n2::nat>)" by auto
then show "n1 = n2" by (rule inj_tape_of_list)
qed
next
from assms have major: "<n1::nat> @ Bk ↑ l1 = <n2::nat> @ Bk ↑ l2" by auto
then show "l1 = l2" by (rule unique_Bk_postfix)
qed
qed
subsection ‹Lists of numerals never contain two consecutive blanks›
definition noDblBk:: "cell list ⇒ bool"
where "noDblBk cs ≡ ∀i. Suc i < length cs ∧ cs!i = Bk ⟶ cs!(Suc i) = Oc"
lemma noDblBk_Bk_Oc_rep: "noDblBk (Oc ↑ n1)"
by (simp add: noDblBk_def )
lemma noDblBk_Bk_imp_Oc: "⟦noDblBk cs; Suc i < length cs; cs!i = Bk ⟧ ⟹ cs!(Suc i) = Oc"
by (auto simp add: noDblBk_def)
lemma noDblBk_imp_noDblBk_Oc_cons: "noDblBk cs ⟹ noDblBk (Oc#cs)"
by (smt (verit) Suc_less_eq Suc_pred add.right_neutral add_Suc_right cell.exhaust list.size(4)
neq0_conv noDblBk_Bk_imp_Oc noDblBk_def nth_Cons_0 nth_Cons_Suc)
lemma noDblBk_Numeral: "noDblBk (<n::nat>)"
by (auto simp add: noDblBk_def tape_of_nat_def)
lemma noDblBk_Nil: "noDblBk []"
by (auto simp add: noDblBk_def)
lemma noDblBk_Singleton: "noDblBk (<[n::nat]>)"
by (auto simp add: noDblBk_def tape_of_nat_def tape_of_list_def)
lemma tape_of_nat_list_cons_eq:"nl ≠ [] ⟹ <(a::nat) # nl> = <a> @ Bk # <nl>"
by (metis list.exhaust tape_of_list_def tape_of_nat_list.simps(3))
lemma noDblBk_cons_cons: "noDblBk(<(x::nat) # xs>) ⟹ noDblBk(<a::nat> @ Bk # <x # xs>)"
proof -
assume F0: "noDblBk (<x # xs>)"
have F1: "hd(<x # xs>) = Oc"
by (metis hd_append hd_of_numeral_is_Oc list.sel(1)
tape_of_nat_list_cons_eq tape_of_list_def tape_of_nat_list.simps(2)
tape_of_nat_list_cases2)
have F2: "<a> = Oc ↑ (Suc a)" by (auto simp add: tape_of_nat_def)
have "noDblBk (<a::nat>)" by (auto simp add: noDblBk_Numeral)
with F0 and F1 and F2 show ?thesis
unfolding noDblBk_def
proof -
assume A1: "∀i. Suc i < length (<x # xs>) ∧ <x # xs> ! i = Bk ⟶ <x # xs> ! Suc i = Oc"
and A2: "hd (<x # xs>) = Oc"
and A3: "<a> = Oc ↑ Suc a"
and A4: "∀i. Suc i < length (<a>) ∧ <a> ! i = Bk ⟶ <a> ! Suc i = Oc"
show "∀i. Suc i < length (<a> @ Bk # <x # xs>) ∧
(<a> @ Bk # <x # xs>) ! i = Bk ⟶ (<a> @ Bk # <x # xs>) ! Suc i = Oc"
proof
fix i
show "Suc i < length (<a> @ Bk # <x # xs>) ∧
(<a> @ Bk # <x # xs>) ! i = Bk ⟶ (<a> @ Bk # <x # xs>) ! Suc i = Oc"
proof
assume "Suc i < length (<a> @ Bk # <x # xs>) ∧ (<a> @ Bk # <x # xs>) ! i = Bk"
then show "(<a> @ Bk # <x # xs>) ! Suc i = Oc"
proof
assume A5: "Suc i < length (<a> @ Bk # <x # xs>)"
and A6: "(<a> @ Bk # <x # xs>) ! i = Bk"
show "(<a> @ Bk # <x # xs>) ! Suc i = Oc"
proof -
from A5 have "Suc i < length (<a>) ∨ Suc i = length (<a>) ∨
Suc i = Suc (length (<a>)) ∨ (Suc (length (<a>)) < Suc i ∧ Suc i < length (<a> @ Bk # <x # xs>))"
by auto
then show ?thesis
proof
assume "Suc i < length (<a>)"
with A1 A2 A3 A4 A5 show ?thesis
by (simp add: nth_append')
next
assume "Suc i = length (<a>) ∨ Suc i = Suc (length (<a>)) ∨ Suc (length (<a>)) < Suc i ∧ Suc i < length (<a> @ Bk # <x # xs>)"
then show "(<a> @ Bk # <x # xs>) ! Suc i = Oc"
proof
assume "Suc i = length (<a>)"
with A1 A2 A3 A4 A5 A6 show "(<a> @ Bk # <x # xs>) ! Suc i = Oc"
by (metis lessI nth_Cons_Suc nth_append' nth_append_length replicate_append_same)
next
assume "Suc i = Suc (length (<a>)) ∨ Suc (length (<a>)) < Suc i ∧ Suc i < length (<a> @ Bk # <x # xs>)"
then show "(<a> @ Bk # <x # xs>) ! Suc i = Oc"
proof
assume "Suc i = Suc (length (<a>))"
with A1 A2 A3 A4 A5 A6 show "(<a> @ Bk # <x # xs>) ! Suc i = Oc"
by (metis One_nat_def Suc_eq_plus1 length_Cons length_append list.collapse list.size(3)
nat_neq_iff nth_Cons_0 nth_Cons_Suc nth_append_length_plus)
next
assume A7: "Suc (length (<a>)) < Suc i ∧ Suc i < length (<a> @ Bk # <x # xs>)"
have F3: "(<a> @ Bk # <x # xs>) = ((<a> @ [Bk]) @ <x # xs>)" by auto
have F4: "⋀n. ((<a> @ [Bk]) @ <x # xs>)! (length (<a> @ [Bk]) + n) = (<x # xs>)!n"
using nth_append_length_plus by blast
from A7 have "∃m. i = Suc (length (<a>)) + m" by arith
then obtain m where w_m: "i = Suc (length (<a>)) + m" by blast
with A7 have F5: "Suc m < length (<x # xs>)" by auto
from w_m F4 have F6: "((<a> @ [Bk]) @ <x # xs>) ! i = (<x # xs>)! m" by auto
with F5 A7 have F7: "((<a> @ [Bk]) @ <x # xs>) ! (Suc i) = (<x # xs>)! (Suc m)"
by (metis F4 add_Suc_right length_append_singleton w_m)
from A6 and F6 have "(<x # xs>)! m = Bk" by auto
with A1 and F5 have "(<x # xs>)! (Suc m) = Oc" by auto
with F7 have "((<a> @ [Bk]) @ <x # xs>) ! (Suc i) = Oc" by auto
with F3 show "(<a> @ Bk # <x # xs>)! (Suc i) = Oc" by auto
qed
qed
qed
qed
qed
qed
qed
qed
qed
theorem noDblBk_tape_of_nat_list: "noDblBk(<nl:: nat list>)"
proof (induct nl)
case Nil
then show ?case
by (auto simp add: noDblBk_def tape_of_nat_def tape_of_list_def)
next
case (Cons a nl)
then have IV: "noDblBk (<nl>)" .
show "noDblBk (<a # nl>)"
proof (cases nl)
case Nil
then show ?thesis
by (auto simp add: noDblBk_def tape_of_nat_def tape_of_list_def)
next
case (Cons x xs)
then have "nl = x # xs" .
show ?thesis
proof -
from ‹nl = x # xs› have "noDblBk (<a # nl>) = noDblBk(<a> @ Bk # <x # xs>)"
by (auto simp add: tape_of_nat_list_cons_eq)
also with IV and ‹nl = x # xs› have "... = True" using noDblBk_cons_cons by auto
finally show ?thesis by auto
qed
qed
qed
lemma hasDblBk_L1: "⟦ CR = rs @ [Bk] @ Bk # rs'; noDblBk CR ⟧ ⟹ False"
by (metis add_diff_cancel_left' append.simps(2)
append_assoc cell.simps(2) length_Cons length_append
length_append_singleton noDblBk_def nth_append_length zero_less_Suc zero_less_diff)
lemma hasDblBk_L2: "⟦ C = Bk # cls; noDblBk C ⟧ ⟹ cls = [] ∨ (∃cls'. cls = Oc#cls')"
by (metis (full_types) append_Cons append_Nil cell.exhaust hasDblBk_L1 neq_Nil_conv)
lemma hasDblBk_L3: "⟦ noDblBk C ; C = C1 @ (Bk#C2) ⟧ ⟹ C2 = [] ∨ (∃C3. C2 = Oc#C3)"
by (metis (full_types) append_Cons append_Nil cell.exhaust hasDblBk_L1 neq_Nil_conv)
lemma hasDblBk_L4:
assumes "noDblBk CL"
and "r = Bk # rs"
and "r = rev ls1 @ Oc # rss"
and "CL = ls1 @ ls2"
shows "ls2 = [] ∨ (∃bs. ls2 = Oc#bs)"
proof -
from ‹r = Bk # rs› have "last ls1 = Bk"
proof (cases ls1)
case Nil
then have "ls1=[]" .
with ‹r = rev ls1 @ Oc # rss› have "r = Oc # rss" by auto
with ‹r = Bk # rs› have False by auto
then show ?thesis by auto
next
case (Cons b bs)
then have "ls1 = b#bs" .
with ‹r = rev ls1 @ Oc # rss› and ‹r = Bk # rs› show ?thesis
by (metis ‹r = rev ls1 @ Oc # rss›
last_appendR last_snoc list.simps(3) rev.simps(2) rev_append rev_rev_ident)
qed
show ?thesis
proof (cases ls2)
case Nil
then show ?thesis by auto
next
case (Cons b bs)
then have "ls2 = b # bs" .
show ?thesis
proof (cases b)
case Bk
then have "b = Bk" .
with ‹ls2 = b # bs› have "ls2 = Bk # bs" by auto
with ‹CL = ls1 @ ls2› have "CL = ls1 @ Bk # bs" by auto
then have "CL = butlast ls1 @ [Bk] @ Bk # ls2"
by (metis ‹last ls1 = Bk› ‹noDblBk CL› ‹r = Bk # rs› ‹r = rev ls1 @ Oc # rss›
append_butlast_last_id append_eq_append_conv2 append_self_conv2
cell.distinct(1) hasDblBk_L1 list.inject rev_is_Nil_conv)
with ‹noDblBk CL› have False
using hasDblBk_L1 by blast
then show ?thesis by auto
next
case Oc
with ‹ls2 = b # bs› show ?thesis by auto
qed
qed
qed
lemma hasDblBk_L5:
assumes "noDblBk CL"
and "r = Bk # rs"
and "r = rev ls1 @ Oc # rss"
and "CL = ls1 @ [Bk]"
shows False
using assms hasDblBk_L4
by blast
lemma noDblBk_cases:
assumes "noDblBk C"
and "C = C1 @ C2"
and "C2 = [] ⟹ P"
and "C2 = [Bk] ⟹ P"
and "⋀C3. C2 = Bk#Oc#C3 ⟹ P"
and "⋀C3. C2 = Oc#C3 ⟹ P"
shows "P"
proof -
have "C2 = [] ∨ C2 = [Bk] ∨ (∃C3. C2 = Bk#Oc#C3 ∨ C2 = Bk#Bk#C3 ∨ C2 = Oc#C3)"
by (metis (full_types) cell.exhaust list.exhaust)
then show ?thesis
using assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) hasDblBk_L3 list.distinct(1) by blast
qed
subsection ‹Unique decomposition of tapes containing lists of numerals›
text ‹A lemma about appending lists of numerals.›
lemma append_numeral_list: "⟦ (nl1::nat list) ≠ []; nl2 ≠ [] ⟧ ⟹ <nl1 @ nl2> = <nl1>@[Bk]@<nl2>"
proof (induct nl1 arbitrary: nl2)
case Nil
then show ?case
by blast
next
fix a::nat
fix nl1::"nat list"
fix nl2::"nat list"
assume IH: "⋀nl2. ⟦nl1 ≠ []; nl2 ≠ []⟧ ⟹ <nl1 @ nl2> = <nl1> @ [Bk] @ <nl2>"
and minor1: "a # nl1 ≠ []"
and minor2: "nl2 ≠ []"
show "<(a # nl1) @ nl2> = <a # nl1> @ [Bk] @ <nl2>"
proof (cases nl1)
assume "nl1 = []"
then show "<(a # nl1) @ nl2> = <a # nl1> @ [Bk] @ <nl2>"
by (metis append_Cons append_Nil minor2 tape_of_list_def tape_of_nat_list.simps(2) tape_of_nat_list_cons_eq)
next
fix na nl1s
assume "nl1 = na # nl1s"
then have "nl1 ≠ []" by auto
have "<(a # nl1) @ nl2> = <a # (nl1 @ nl2)>" by auto
also with ‹nl1 ≠ []› and ‹nl1 = na # nl1s›
have "... = <a>@[Bk]@<(nl1 @ nl2)>"
by (simp add: tape_of_nat_list_cons_eq)
also with ‹nl1 ≠ []› and minor2 and IH
have "... = <a>@[Bk]@ <nl1> @ [Bk] @ <nl2>" by auto
finally have "<(a # nl1) @ nl2> = <a>@[Bk]@ <nl1> @ [Bk] @ <nl2>" by auto
moreover with ‹nl1 ≠ []› and minor2 have "<a # nl1> @ [Bk] @ <nl2> = <a>@[Bk]@ <nl1> @ [Bk] @ <nl2>"
by (simp add: tape_of_nat_list_cons_eq)
ultimately
show "<(a # nl1) @ nl2> = <a # nl1> @ [Bk] @ <nl2>"
by auto
qed
qed
text ‹A lemma about reverting lists of numerals.›
lemma rev_numeral_list: "rev(<nl::nat list>) = <(rev nl)>"
proof (induct nl)
case Nil
then show ?case
by (simp)
next
fix a::nat
fix nl::"nat list"
assume IH: "rev (<nl>) = <rev nl>"
show "rev (<a # nl>) = <rev (a # nl)>"
proof (rule tape_of_nat_list.cases[of nl])
assume "nl = []"
then have "rev (<a # nl>) = rev (<a>)"
by (simp add: tape_of_list_def )
with ‹nl = []› show ?thesis
by (simp add: rev_numeral tape_of_list_def )
next
fix n
assume "nl = [n]"
then have "rev (<a # nl>) = rev (<a#[n]>)" by auto
also have "... = rev (<a>@[Bk]@<nl>)"
by (simp add: ‹nl = [n]› tape_of_list_def tape_of_nat_list_cons_eq)
also have "... = rev(<nl>)@[Bk]@rev(<a>)"
by simp
also with IH have "... = <rev nl>@[Bk]@rev(<a>)" by auto
also with IH ‹nl = [n]› have "... = <rev (a # nl)>"
by (simp add: Cons_eq_append_conv hd_rev rev_numeral tape_of_list_def )
finally show "rev (<a # nl>) = <rev (a # nl)>" by auto
next
fix n v va
assume "nl = n # v # va"
then have "rev (<a # nl>) = rev (<a#n # v # va>)" by auto
also with ‹nl = n # v # va› have "... = rev(<nl>)@[Bk]@rev(<a>)"
by (simp add: tape_of_list_def )
also with IH have "... = <rev nl>@[Bk]@rev(<a>)" by auto
finally have "rev (<a # nl>) = <rev nl>@[Bk]@rev(<a>)" by auto
moreover have "<rev (a # nl)> = <rev nl>@[Bk]@rev(<a>)"
proof -
have "<rev (a # nl)> = <rev nl @ [a]>" by auto
also
from ‹nl = n # v # va› have " <rev nl @ [a]> = <rev nl>@[Bk]@rev(<a>)"
by (metis list.simps(3) append_numeral_list rev_is_Nil_conv rev_numeral tape_of_list_def tape_of_nat_list.simps(2))
finally show "<rev (a # nl)> = <rev nl>@[Bk]@rev(<a>)" by auto
qed
ultimately show ?thesis by auto
qed
qed
text ‹Some more lemmas about unique decomposition of tapes that contain lists of numerals.›
lemma unique_Bk_postfix_numeral_list_Nil: "<[]> @ Bk ↑ l1 = <yl::nat list> @ Bk ↑ l2 ⟹ [] = yl"
proof (induct yl arbitrary: l1 l2)
case Nil
then show ?case by auto
next
fix a
fix yl:: "nat list"
fix l1 l2
assume IV: "⋀l1 l2. <[]> @ Bk ↑ l1 = <yl> @ Bk ↑ l2 ⟹ [] = yl"
and major: "<[]> @ Bk ↑ l1 = <a # yl> @ Bk ↑ l2"
then show "[] = a # yl"
by (metis append.assoc append.simps(1) append.simps(2) cell.distinct(1) list.sel(1) list.simps(3)
replicate_Suc replicate_app_Cons_same tape_of_list_def tape_of_nat_def tape_of_nat_list.elims
tape_of_nat_list.simps(3) tape_of_nat_list_cases2)
qed
lemma nonempty_list_of_numerals_neq_BKs: "<a# xs::nat list> ≠ Bk ↑ l"
by (metis append_Nil append_Nil2 list.simps(3) replicate_0 tape_of_list_def
tape_of_list_empty unique_Bk_postfix_numeral_list_Nil)
lemma unique_Bk_postfix_nonempty_numeral_list:
"⟦ xl ≠ []; yl ≠ []; <xl::nat list> @ Bk ↑ l1 = <yl::nat list> @ Bk ↑ l2 ⟧ ⟹ xl = yl"
proof (induct xl arbitrary: l1 yl l2)
fix l1 yl l2
assume "<[]> @ Bk ↑ l1 = <yl::nat list> @ Bk ↑ l2"
then show "[] = yl"
using unique_Bk_postfix_numeral_list_Nil by auto
next
fix a:: nat
fix xl:: "nat list"
fix l1
fix yl:: "nat list"
fix l2
assume IV: "⋀l1 yl l2. ⟦xl ≠ []; yl ≠ []; <xl> @ Bk ↑ l1 = <yl> @ Bk ↑ l2⟧ ⟹ xl = yl"
and minor_xl: "a # xl ≠ []"
and minor_yl: "yl ≠ []"
and major: "<a # xl> @ Bk ↑ l1 = <yl> @ Bk ↑ l2"
show "a # xl = yl"
proof (cases yl)
case Nil
then show ?thesis
by (metis major tape_of_list_empty unique_Bk_postfix_numeral_list_Nil)
next
fix b:: nat
fix ys:: "nat list"
assume Ayl: "yl = b # ys"
have "a # xl = b # ys"
proof
show "a = b ∧ xl = ys"
proof (cases xl)
case Nil
then have "xl = []" .
from major and ‹yl = b # ys›
have "<a # xl> @ Bk ↑ l1 = <b # ys> @ Bk ↑ l2" by auto
with minor_xl and ‹xl = []› have "<a # xl::nat list> = <a>"
by (simp add: local.Nil tape_of_list_def)
with major and Ayl have "<a> @ Bk ↑ l1 = <b # ys> @ Bk ↑ l2" by auto
show "a = b ∧ xl = ys"
proof (cases ys)
case Nil
then have "ys = []" .
then have "<b # ys> = <b>"
by (simp add: local.Nil tape_of_list_def)
with ‹<a> @ Bk ↑ l1 = <b # ys> @ Bk ↑ l2›
have "<a> @ Bk ↑ l1 = <b> @ Bk ↑ l2" by auto
then have "a = b"
by (metis append_same_eq inj_tape_of_list unique_Bk_postfix)
with ‹xl = []› and ‹ys = []›
show ?thesis by auto
next
fix c
fix ys':: "nat list"
assume "ys = c# ys'"
then have "<b # ys> = <b> @ Bk # <ys>"
by (simp add: Ayl tape_of_list_def)
with ‹<a> @ Bk ↑ l1 = <b # ys> @ Bk ↑ l2›
have "<a> @ Bk ↑ l1 = <b> @ Bk # <ys> @ Bk ↑ l2"
by simp
show "a = b ∧ xl = ys"
proof (cases l1)
case 0
then have "l1 = 0" .
with ‹<a> @ Bk ↑ l1 = <b> @ Bk # <ys> @ Bk ↑ l2›
have "<a> = <b> @ Bk # <ys> @ Bk ↑ l2"
by auto
then have False
by (metis "0" ‹<a> @ Bk ↑ l1 = <b> @ Bk # <ys> @ Bk ↑ l2›
cell.distinct(1) length_Cons length_append length_replicate less_add_same_cancel1
nth_append_length nth_replicate tape_of_nat_def zero_less_Suc)
then show ?thesis by auto
next
case (Suc l1')
then have "l1 = Suc l1'" .
then have "<a> @ Bk ↑ l1 = <a> @ (Bk #Bk ↑ l1')"
by simp
then have F1: "(<a> @ Bk ↑ l1)!(Suc a) = Bk"
by (metis cell.distinct(1) cell.exhaust length_replicate nth_append_length tape_of_nat_def)
have "a < b ∨ a = b ∨ b < a" by arith
then show "a = b ∧ xl = ys"
proof
assume "a < b"
with ‹<a> @ Bk ↑ l1 = <b> @ Bk # <ys> @ Bk ↑ l2›
have "(<b> @ Bk # <ys> @ Bk ↑ l2)!(Suc a) ≠ Bk"
by (simp add: hd_of_numeral_is_Oc nth_append' tape_of_nat_def)
with F1 and ‹<a> @ Bk ↑ l1 = <b> @ Bk # <ys> @ Bk ↑ l2› have False
by (simp add: ‹(<a> @ Bk ↑ l1) ! Suc a = Bk›)
then show "a = b ∧ xl = ys"
by auto
next
assume "a = b ∨ b < a"
then show ?thesis
proof
assume "b < a"
with ‹<a> @ Bk ↑ l1 = <b> @ Bk # <ys> @ Bk ↑ l2›
have "(<a> @ Bk ↑ l1)!(Suc a) ≠ Bk"
by (metis Suc_mono cell.distinct(1) length_replicate nth_append'
nth_append_length nth_replicate tape_of_nat_def)
with F1 have False by auto
then show ?thesis by auto
next
assume "a=b"
then have False
using ‹xl = []› and ‹ys = c# ys'› and ‹<a> @ Bk ↑ l1 = <b> @ Bk # <ys> @ Bk ↑ l2›
using ‹<a> @ Bk ↑ l1 = <a> @ Bk # Bk ↑ l1'› list.distinct(1) list.inject
same_append_eq self_append_conv2 tape_of_list_empty unique_Bk_postfix_numeral_list_Nil
by fastforce
then show ?thesis by auto
qed
qed
qed
qed
next
fix a'::nat
fix xs:: "nat list"
assume "xl = a'#xs"
from major and ‹yl = b # ys›
have "<a # xl> @ Bk ↑ l1 = <b # ys> @ Bk ↑ l2" by auto
from ‹xl = a'#xs› have "<a # xl::nat list> = <a> @ Bk # <xl>"
by (simp add: tape_of_list_def)
with ‹<a # xl> @ Bk ↑ l1 = <b # ys> @ Bk ↑ l2›
have "(<a> @ Bk # <xl>) @ Bk ↑ l1 = <b # ys> @ Bk ↑ l2" by auto
then have F2: "<a> @ [Bk] @ (<xl> @ Bk ↑ l1) = <b # ys> @ Bk ↑ l2" by auto
then have F3: "(<a> @ [Bk] @ (<xl> @ Bk ↑ l1))!(Suc a) = Bk"
by (metis Ayl append.simps(1) append.simps(2) length_replicate nth_append_length
tape_of_nat_def)
show "a = b ∧ xl = ys"
proof (cases ys)
case Nil
then have "ys = []" .
then have "<b # ys> = <b>"
by (simp add: local.Nil tape_of_list_def)
with F2
have "<a> @ [Bk] @ (<xl> @ Bk ↑ l1) = <b> @ Bk ↑ l2" by auto
have "a < b ∨ a = b ∨ b < a" by arith
then have False
proof
assume "a < b"
then have "(<b> @ Bk ↑ l2)!(Suc a) ≠ Bk"
by (simp add: ‹a < b› nth_append' tape_of_nat_def)
with F2 and F3 show False
using ‹<a> @ [Bk] @ <xl> @ Bk ↑ l1 = <b> @ Bk ↑ l2› by auto
next
assume "a = b ∨ b < a"
then show False
proof
assume "b < a"
show False
proof (cases l2)
case 0
then have "l2 = 0" .
then have "<b> @ Bk ↑ l2 = <b>" by auto
with ‹<a> @ [Bk] @ (<xl> @ Bk ↑ l1) = <b> @ Bk ↑ l2›
have "<a> @ [Bk] @ (<xl> @ Bk ↑ l1) = <b>" by auto
with ‹xl = a'#xs› and ‹b < a›
have "length (<a>) < length (<a> @ [Bk] @ (<xl> @ Bk ↑ l1))"
by (metis inj_tape_of_list le_add1 length_append less_irrefl
nat_less_le nth_append' nth_equalityI)
with ‹b < a› have "b < length (<a> @ [Bk] @ (<xl> @ Bk ↑ l1))"
by (simp add: ‹<a> @ [Bk] @ <xl> @ Bk ↑ l1 = <b>› tape_of_nat_def)
with ‹<a> @ [Bk] @ (<xl> @ Bk ↑ l1) = <b>› show False
using Suc_less_SucD ‹b < a› ‹length (<a>) < length (<a> @ [Bk] @ <xl> @ Bk ↑ l1)›
length_replicate not_less_iff_gr_or_eq tape_of_nat_def by auto
next
fix l2'
assume "l2 = Suc l2'"
with ‹<a> @ [Bk] @ (<xl> @ Bk ↑ l1) = <b> @ Bk ↑ l2›
have "<a> @ [Bk] @ (<xl> @ Bk ↑ l1) = <b> @ [Bk] @ Bk ↑ l2'" by auto
from ‹b < a› have "(<b> @ [Bk] @ Bk ↑ l2')!(Suc b) = Bk"
by (metis append_Cons length_replicate nth_append_length tape_of_nat_def)
moreover from ‹b < a› have "(<a> @ [Bk] @ (<xl> @ Bk ↑ l1))!(Suc b) ≠ Bk"
by (simp add: Suc_mono last_of_numeral_is_Oc nth_append' tape_of_nat_def)
ultimately show False
using ‹<a> @ [Bk] @ <xl> @ Bk ↑ l1 = <b> @ [Bk] @ Bk ↑ l2'› by auto
qed
next
assume "a=b"
with ‹<a> @ [Bk] @ (<xl> @ Bk ↑ l1) = <b> @ Bk ↑ l2› and ‹xl = a'#xs›
show False
by (metis append_Nil append_eq_append_conv2 list.sel(3) list.simps(3)
local.Nil same_append_eq tape_of_list_empty tl_append2 tl_replicate
unique_Bk_postfix_numeral_list_Nil)
qed
qed
then show ?thesis by auto
next
fix c
fix ys':: "nat list"
assume "ys = c# ys'"
from ‹ys = c# ys'› have "(<b # ys>) = (<b> @ [Bk] @ <ys>)"
by (simp add: Ayl tape_of_list_def )
with F2 have "<a> @ [Bk] @ (<xl> @ Bk ↑ l1) = <b> @ [Bk] @ <ys> @ Bk ↑ l2" by auto
have "a < b ∨ a = b ∨ b < a" by arith
then show "a = b ∧ xl = ys"
proof
assume "a < b"
with ‹a < b› have "(<b> @ [Bk] @ <ys> @ Bk ↑ l2) !(Suc a) ≠ Bk"
by (simp add: hd_of_numeral_is_Oc nth_append' tape_of_nat_def)
with F3 and ‹<a> @ [Bk] @ (<xl> @ Bk ↑ l1) = <b> @ [Bk] @ <ys> @ Bk ↑ l2›
have False
by auto
then show ?thesis by auto
next
assume "a = b ∨ b < a"
then show ?thesis
proof
assume "b < a"
from ‹b < a› and ‹<a> @ [Bk] @ (<xl> @ Bk ↑ l1) = <b> @ [Bk] @ <ys> @ Bk ↑ l2›
have "(<b> @ [Bk] @ <ys> @ Bk ↑ l2) ! Suc b = Bk"
by (metis append_Cons cell.distinct(1) cell.exhaust length_replicate
nth_append_length tape_of_nat_def)
moreover from ‹b < a› and ‹<a> @ [Bk] @ (<xl> @ Bk ↑ l1) = <b> @ [Bk] @ <ys> @ Bk ↑ l2›
have "(<a> @ [Bk] @ (<xl> @ Bk ↑ l1)) ! Suc b ≠ Bk"
by (metis Suc_mono cell.distinct(1) length_replicate nth_append' nth_replicate tape_of_nat_def)
ultimately have False using ‹<a> @ [Bk] @ (<xl> @ Bk ↑ l1) = <b> @ [Bk] @ <ys> @ Bk ↑ l2›
by auto
then show ?thesis by auto
next
assume "a = b"
with ‹<a> @ [Bk] @ (<xl> @ Bk ↑ l1) = <b> @ [Bk] @ <ys> @ Bk ↑ l2›
have "<xl> @ Bk ↑ l1 = <ys> @ Bk ↑ l2" by auto
moreover from ‹xl = a'#xs› have "xl ≠ []" by auto
moreover from ‹ys = c# ys'› have "ys ≠ []" by auto
ultimately have "xl = ys" using IV by auto
with ‹a = b› show ?thesis
by auto
qed
qed
qed
qed
qed
with ‹yl = b # ys› show ?thesis by auto
qed
qed
corollary unique_Bk_postfix_numeral_list: "<xl::nat list> @ Bk ↑ l1 = <yl::nat list> @ Bk ↑ l2 ⟹ xl = yl"
by (metis append_Nil tape_of_list_def tape_of_list_empty
unique_Bk_postfix_nonempty_numeral_list unique_Bk_postfix_numeral_list_Nil)
text ‹Some more lemmas about noDblBks in lists of numerals.›
lemma numeral_list_head_is_Oc: "(nl::nat list) ≠ [] ⟹ hd (<nl>) = Oc"
proof -
assume A: "(nl::nat list) ≠ []"
then have "(∃r'. <nl> = Oc # r')"
using append_Nil tape_of_list_empty tape_of_nat_list_cases2 unique_Bk_postfix_numeral_list_Nil by fastforce
then obtain r' where w_r': "<nl> = Oc # r'" by blast
then show "hd (<nl>) = Oc" by auto
qed
lemma numeral_list_last_is_Oc: "(nl::nat list) ≠ [] ⟹ last (<nl>) = Oc"
proof -
assume A: "(nl::nat list) ≠ []"
then have "<nl> = <rev (rev nl)>" by auto
also have "... = rev (<rev nl>)" by (auto simp add: rev_numeral_list)
finally have "<nl> = rev (<rev nl>)" by auto
moreover from A have "hd (<rev nl>) = Oc" by (auto simp add: numeral_list_head_is_Oc)
with A have "last (rev (<rev nl>)) = Oc"
by (simp add: last_rev)
ultimately show ?thesis
by (simp add: ‹last (rev (<rev nl>)) = Oc›)
qed
lemma noDblBk_tape_of_nat_list_imp_noDblBk_tl: "noDblBk (<nl>) ⟹ noDblBk (tl (<nl>))"
proof (cases "<nl>")
case Nil
then show ?thesis
by (simp add: local.Nil noDblBk_Nil)
next
fix a nls
assume "noDblBk (<nl>)" and "<nl> = a # nls"
then have "noDblBk (a # nls)" by auto
then have "∀i. Suc i < length (a # nls) ∧ (a # nls) ! i = Bk ⟶ (a # nls) ! Suc i = Oc"
using noDblBk_def by auto
then have "noDblBk (nls)" using noDblBk_def by auto
with ‹<nl> = a # nls› show "noDblBk (tl (<nl>))" using noDblBk_def by auto
qed
lemma noDblBk_tape_of_nat_list_cons_imp_noDblBk_tl: "noDblBk (a # <nl>) ⟹ noDblBk (<nl>)"
proof -
assume "noDblBk (a # <nl>)"
then have "∀i. Suc i < length (a # <nl>) ∧ (a # <nl>) ! i = Bk ⟶ (a # <nl>) ! Suc i = Oc"
using noDblBk_def by auto
then show "noDblBk (<nl>)" using noDblBk_def by auto
qed
lemma noDblBk_tape_of_nat_list_imp_noDblBk_cons_Bk: "(nl::nat list) ≠ [] ⟹ noDblBk ([Bk] @ <nl>)"
proof -
assume "(nl::nat list) ≠ []"
then have major: "<(0::nat) # nl> = <0::nat> @ Bk # <nl>"
using tape_of_nat_list_cons_eq
by auto
moreover have "noDblBk (<(0::nat) # nl>)" by (rule noDblBk_tape_of_nat_list)
ultimately have "noDblBk (<0::nat> @ Bk # <nl>)" by auto
then have "noDblBk (Oc # Bk # <nl>)"
by (simp add: cell.exhaust noDblBk_tape_of_nat_list tape_of_nat_def)
then show ?thesis
using major
by (metis append_eq_Cons_conv empty_replicate list.sel(3) noDblBk_tape_of_nat_list_imp_noDblBk_tl
replicate_Suc self_append_conv2 tape_of_nat_def )
qed
end