Theory BlanksDoNotMatter
section ‹Trailing Blanks on the input tape do not matter›
theory BlanksDoNotMatter
imports Turing
begin
sledgehammer_params[minimize=false,preplay_timeout=10,timeout=30,strict=true,
provers="e z3 cvc4 vampire "]
subsection ‹Replication of symbols›
abbreviation exponent :: "'a ⇒ nat ⇒ 'a list" ("_ ↑ _" [100, 99] 100)
where "x ↑ n == replicate n x"
lemma hd_repeat_cases:
"P (hd (a ↑ m @ r)) ⟷ (m = 0 ⟶ P (hd r)) ∧ (∀nat. m = Suc nat ⟶ P a)"
by (cases m,auto)
lemma hd_repeat_cases':
"P (hd (a ↑ m @ r)) = (if m = 0 then P (hd r) else P a)"
by auto
lemma
"(if m = 0 then P (hd r) else P a) = ((m = 0 ⟶ P (hd r)) ∧ (∀nat. m = Suc nat ⟶ P a))"
proof -
have "(if m = 0 then P (hd r) else P a) = P (hd (a ↑ m @ r))" by auto
also have "... = ((m = 0 ⟶ P (hd r)) ∧ (∀nat. m = Suc nat ⟶ P a))"
by (simp add: iffI hd_repeat_cases)
finally show ?thesis .
qed
lemma split_head_repeat[simp]:
"Oc # list1 = Bk ↑ j @ list2 ⟷ j = 0 ∧ Oc # list1 = list2"
"Bk # list1 = Oc ↑ j @ list2 ⟷ j = 0 ∧ Bk # list1 = list2"
"Bk ↑ j @ list2 = Oc # list1 ⟷ j = 0 ∧ Oc # list1 = list2"
"Oc ↑ j @ list2 = Bk # list1 ⟷ j = 0 ∧ Bk # list1 = list2"
by(cases j;force)+
lemma Bk_no_Oc_repeatE[elim]: "Bk # list = Oc ↑ t ⟹ RR"
by (cases t, auto)
lemma replicate_Suc_1: "a ↑ (z1 + Suc z2) = (a ↑ z1) @ (a ↑ Suc z2)"
by (meson replicate_add)
lemma replicate_Suc_2: "a ↑ (z1 + Suc z2) = (a ↑ Suc z1) @ (a ↑ z2)"
by (simp add: replicate_add)
subsection ‹Trailing blanks on the left tape do not matter›
text‹In this section we will show that we may add or remove trailing blanks on the
initial left and right portions of the tape at will.
However, we may not add or remove trailing blanks on the tape resulting from the computation.
The resulting tape is completely determined by the contents of the initial tape.›
lemma step_left_tape_ShrinkBkCtx_right_Nil:
assumes "step0 (s,CL@Bk↑ z1 , []) tm = (s',l',r')"
and "za < z1"
shows "∃CL' zb. l' = CL'@Bk↑za@Bk↑zb ∧
(step0 (s,CL@Bk↑za, []) tm = (s',CL'@Bk↑za,r') ∨
step0 (s,CL@Bk↑za, []) tm = (s',CL'@Bk↑(za-1),r'))"
proof (cases "fetch tm (s - 0) (read [])")
case (Pair a s2)
then have A1: "fetch tm (s - 0) (read []) = (a, s2)" .
show ?thesis
proof (cases a)
assume "a = WB"
from ‹a = WB› and assms A1 have "step0 (s, CL@Bk ↑ z1, []) tm = (s2, CL@Bk ↑ z1, [Bk])" by auto
moreover from ‹a = WB› and assms A1 have "step0 (s, CL@Bk↑za, []) tm = (s2,CL@Bk↑za , [Bk])" by auto
ultimately have "Bk↑z1 = Bk↑za@Bk↑(z1-za) ∧ step0 (s, CL@Bk↑za, []) tm = (s2,CL@Bk↑za , [Bk])"
using assms
by (metis le_eq_less_or_eq ordered_cancel_comm_monoid_diff_class.add_diff_inverse replicate_add)
then show ?thesis
using ‹step0 (s, CL @ Bk ↑ z1, []) tm = (s2, CL @ Bk ↑ z1, [Bk])› assms(1) by auto
next
assume "a = WO"
from ‹a = WO› and assms A1 have "step0 (s, CL@Bk ↑ z1, []) tm = (s2, CL@Bk ↑ z1, [Oc])" by auto
moreover from ‹a = WO› and assms A1 have "step0 (s, CL@Bk↑za, []) tm = (s2,CL@Bk↑za , [Oc])" by auto
ultimately have "Bk↑z1 = Bk↑za@Bk↑(z1-za) ∧ step0 (s, CL@Bk↑za, []) tm = (s2,CL@Bk↑za , [Oc])"
using assms
by (metis le_eq_less_or_eq ordered_cancel_comm_monoid_diff_class.add_diff_inverse replicate_add)
then show ?thesis
using ‹step0 (s, CL @ Bk ↑ z1, []) tm = (s2, CL @ Bk ↑ z1, [Oc])› assms(1) by auto
next
assume "a = Nop"
from ‹a = Nop› and assms A1 have "step0 (s, CL@Bk ↑ z1, []) tm = (s2, CL@Bk ↑ z1, [])" by auto
moreover from ‹a = Nop› and assms A1 have "step0 (s, CL@Bk↑za, []) tm = (s2,CL@Bk↑za , [])" by auto
ultimately have "Bk↑z1 = Bk↑za@Bk↑(z1-za) ∧ step0 (s, CL@Bk↑za, []) tm = (s2,CL@Bk↑za , [])"
using assms
by (metis le_eq_less_or_eq ordered_cancel_comm_monoid_diff_class.add_diff_inverse replicate_add)
then show ?thesis
using ‹step0 (s, CL @ Bk ↑ z1, []) tm = (s2, CL @ Bk ↑ z1, [])› assms(1) by auto
next
assume "a = R"
from ‹a = R› and assms A1 have "step0 (s, CL@Bk ↑ z1, []) tm = (s2, [Bk]@CL@Bk↑z1, [])"
by auto
moreover from ‹a = R› and assms A1 have "step0 (s, CL@Bk↑za, []) tm = (s2,[Bk]@CL@Bk↑za, [])" by auto
ultimately have "Bk↑z1 = Bk↑za@Bk↑(z1-za) ∧ step0 (s, CL@Bk↑za, []) tm = (s2,[Bk]@CL@Bk↑za, [])"
using assms
by (metis le_eq_less_or_eq ordered_cancel_comm_monoid_diff_class.add_diff_inverse replicate_add)
then show ?thesis
using ‹step0 (s, CL @ Bk ↑ z1, []) tm = (s2, [Bk] @ CL @ Bk ↑ z1, [])›
by (metis append_Cons append_Nil assms(1) fst_conv snd_conv)
next
assume "a = L"
show ?thesis
proof (cases CL)
case Nil
then have "CL = []" .
then show ?thesis
proof (cases z1)
case 0
then have "z1 = 0" .
with assms and ‹CL = []› show ?thesis by auto
next
case (Suc nat)
then have "z1 = Suc nat" .
from ‹a = L› and ‹CL = []› and ‹z1 = Suc nat› and assms and A1
have "step0 (s, CL@Bk ↑ z1, []) tm = (s2, []@Bk ↑(z1-1), [Bk])"
by auto
moreover from ‹a = L› and ‹CL = []› and A1 have "step0 (s, CL@Bk↑za, []) tm = (s2, []@Bk↑(za-1) , [Bk])" by auto
ultimately have "Bk↑(z1-1) = Bk↑za@Bk↑(z1-1-za) ∧ step0 (s, CL@Bk↑za, []) tm = (s2, []@Bk↑(za-1) , [Bk])"
using assms using ‹z1 = Suc nat›
by (metis diff_Suc_1 le_eq_less_or_eq less_Suc_eq ordered_cancel_comm_monoid_diff_class.add_diff_inverse replicate_add)
with assms and ‹CL = []› and ‹z1 = Suc nat› and ‹step0 (s, CL@Bk↑z1, []) tm = (s2, [] @ Bk ↑ (z1 - 1), [Bk])›
show ?thesis
by auto
qed
next
case (Cons c cs)
then have "CL = c # cs" .
from ‹a = L› and ‹CL = c # cs› and assms and A1
have "step0 (s, CL@Bk ↑ z1, []) tm = (s2, cs@Bk ↑z1, [c])"
by auto
moreover from ‹a = L› and ‹CL = c # cs› and A1
have "step0 (s, CL@Bk↑za, []) tm = (s2, cs@Bk ↑za, [c])" by auto
ultimately have "Bk↑(z1-1) = Bk↑za@Bk↑(z1-1-za) ∧ step0 (s, CL@Bk↑za, []) tm = (s2, cs@Bk ↑za, [c])"
using assms
by (metis One_nat_def Suc_pred add_diff_inverse_nat neq0_conv not_less_eq not_less_zero replicate_add)
with assms and ‹CL = c # cs› and ‹Bk↑(z1-1) = Bk↑za@Bk↑(z1-1-za) ∧ step0 (s, CL@Bk↑za, []) tm = (s2, cs@Bk ↑za, [c])›
show ?thesis
using ‹step0 (s, CL @ Bk ↑ z1, []) tm = (s2, cs @ Bk ↑ z1, [c])›
by (metis fst_conv nat_le_linear not_less ordered_cancel_comm_monoid_diff_class.add_diff_inverse replicate_add snd_conv)
qed
qed
qed
lemma step_left_tape_ShrinkBkCtx_right_Bk:
assumes "step0 (s,CL@Bk↑ z1 , Bk#rs) tm = (s',l',r')"
and "za < z1"
shows "∃CL' zb. l' = CL'@Bk↑za@Bk↑zb ∧
(step0 (s,CL@Bk↑za, Bk#rs) tm = (s',CL'@Bk↑za,r') ∨
step0 (s,CL@Bk↑za, Bk#rs) tm = (s',CL'@Bk↑(za-1),r'))"
proof (cases "fetch tm (s - 0) (read (Bk#rs))")
case (Pair a s2)
then have A1: "fetch tm (s - 0) (read (Bk#rs)) = (a, s2)" .
show ?thesis
proof (cases a)
assume "a = WB"
from ‹a = WB› and assms A1
have "step0 (s, CL@Bk ↑ z1, Bk#rs) tm = (s2, CL@Bk ↑ z1, Bk#rs)"
by (auto simp add: split: if_splits)
moreover from ‹a = WB› and assms A1 have "step0 (s, CL@Bk↑za, Bk#rs) tm = (s2,CL@Bk↑za , Bk#rs)" by auto
ultimately have "Bk↑z1 = Bk↑za@Bk↑(z1-za) ∧ step0 (s, CL@Bk↑za, Bk#rs) tm = (s2,CL@Bk↑za , Bk#rs)"
using assms
by (metis le_eq_less_or_eq ordered_cancel_comm_monoid_diff_class.add_diff_inverse replicate_add)
then show ?thesis
using ‹step0 (s, CL @ Bk ↑ z1, Bk#rs) tm = (s2, CL @ Bk ↑ z1, Bk#rs)› assms(1) by auto
next
assume "a = WO"
from ‹a = WO› and assms A1 have "step0 (s, CL@Bk ↑ z1, Bk#rs) tm = (s2, CL@Bk ↑ z1, Oc#rs)" by auto
moreover from ‹a = WO› and assms A1 have "step0 (s, CL@Bk↑za, Bk#rs) tm = (s2,CL@Bk↑za , Oc#rs)" by auto
ultimately have "Bk↑z1 = Bk↑za@Bk↑(z1-za) ∧ step0 (s, CL@Bk↑za, Bk#rs) tm = (s2,CL@Bk↑za , Oc#rs)"
using assms
by (metis le_eq_less_or_eq ordered_cancel_comm_monoid_diff_class.add_diff_inverse replicate_add)
then show ?thesis
using ‹step0 (s, CL @ Bk ↑ z1, Bk#rs) tm = (s2, CL @ Bk ↑ z1, Oc#rs)› assms(1) by auto
next
assume "a = Nop"
from ‹a = Nop› and assms A1 have "step0 (s, CL@Bk ↑ z1, Bk#rs) tm = (s2, CL@Bk ↑ z1, Bk#rs)" by auto
moreover from ‹a = Nop› and assms A1 have "step0 (s, CL@Bk↑za, Bk#rs) tm = (s2,CL@Bk↑za , Bk#rs)" by auto
ultimately have "Bk↑z1 = Bk↑za@Bk↑(z1-za) ∧ step0 (s, CL@Bk↑za, Bk#rs) tm = (s2,CL@Bk↑za , Bk#rs)"
using assms
by (metis le_eq_less_or_eq ordered_cancel_comm_monoid_diff_class.add_diff_inverse replicate_add)
then show ?thesis
using ‹step0 (s, CL @ Bk ↑ z1, Bk#rs) tm = (s2, CL @ Bk ↑ z1, Bk#rs)› assms(1) by auto
next
assume "a = R"
from ‹a = R› and assms A1 have "step0 (s, CL@Bk ↑ z1, Bk#rs) tm = (s2, [Bk]@CL@Bk↑z1, rs)"
by auto
moreover from ‹a = R› and assms A1 have "step0 (s, CL@Bk↑za, Bk#rs) tm = (s2,[Bk]@CL@Bk↑za, rs)" by auto
ultimately have "Bk↑z1 = Bk↑za@Bk↑(z1-za) ∧ step0 (s, CL@Bk↑za, Bk#rs) tm = (s2,[Bk]@CL@Bk↑za, rs)"
using assms
by (metis le_eq_less_or_eq ordered_cancel_comm_monoid_diff_class.add_diff_inverse replicate_add)
then show ?thesis
using ‹step0 (s, CL @ Bk ↑ z1, Bk#rs) tm = (s2, [Bk] @ CL @ Bk ↑ z1, rs)›
by (metis append_Cons append_Nil assms(1) fst_conv snd_conv)
next
assume "a = L"
show ?thesis
proof (cases CL)
case Nil
then have "CL = []" .
then show ?thesis
proof (cases z1)
case 0
then have "z1 = 0" .
with assms and ‹CL = []› show ?thesis by auto
next
case (Suc nat)
then have "z1 = Suc nat" .
from ‹a = L› and ‹CL = []› and ‹z1 = Suc nat› and assms and A1
have "step0 (s, CL@Bk ↑ z1, Bk#rs) tm = (s2, []@Bk ↑(z1-1), Bk#Bk#rs)"
by auto
moreover from ‹a = L› and ‹CL = []› and A1 have "step0 (s, CL@Bk↑za, Bk#rs) tm = (s2, []@Bk↑(za-1) , Bk#Bk#rs)" by auto
ultimately have "Bk↑(z1-1) = Bk↑za@Bk↑(z1-1-za) ∧ step0 (s, CL@Bk↑za, Bk#rs) tm = (s2, []@Bk↑(za-1) , Bk#Bk#rs)"
using assms using ‹z1 = Suc nat›
by (metis diff_Suc_1 le_eq_less_or_eq less_Suc_eq ordered_cancel_comm_monoid_diff_class.add_diff_inverse replicate_add)
with assms and ‹CL = []› and ‹z1 = Suc nat› and ‹step0 (s, CL@Bk↑z1, Bk#rs) tm = (s2, [] @ Bk ↑ (z1 - 1), Bk#Bk#rs)›
show ?thesis
by auto
qed
next
case (Cons c cs)
then have "CL = c # cs" .
from ‹a = L› and ‹CL = c # cs› and assms and A1
have "step0 (s, CL@Bk ↑ z1, Bk#rs) tm = (s2, cs@Bk ↑z1, c#Bk#rs)"
by auto
moreover from ‹a = L› and ‹CL = c # cs› and A1
have "step0 (s, CL@Bk↑za, Bk#rs) tm = (s2, cs@Bk ↑za, c#Bk#rs)" by auto
ultimately have "Bk↑(z1-1) = Bk↑za@Bk↑(z1-1-za) ∧ step0 (s, CL@Bk↑za, Bk#rs) tm = (s2, cs@Bk ↑za, c#Bk#rs)"
using assms
by (metis One_nat_def Suc_pred add_diff_inverse_nat neq0_conv not_less_eq not_less_zero replicate_add)
with assms and ‹CL = c # cs› and ‹Bk↑(z1-1) = Bk↑za@Bk↑(z1-1-za) ∧ step0 (s, CL@Bk↑za, Bk#rs) tm = (s2, cs@Bk ↑za, c#Bk#rs)›
show ?thesis
using ‹step0 (s, CL @ Bk ↑ z1, Bk#rs) tm = (s2, cs @ Bk ↑ z1, c#Bk#rs)›
by (metis fst_conv nat_le_linear not_less ordered_cancel_comm_monoid_diff_class.add_diff_inverse replicate_add snd_conv)
qed
qed
qed
lemma step_left_tape_ShrinkBkCtx_right_Oc:
assumes "step0 (s,CL@Bk↑ z1 , Oc#rs) tm = (s',l',r')"
and "za < z1"
shows "∃CL' zb. l' = CL'@Bk↑za@Bk↑zb ∧
(step0 (s,CL@Bk↑za, Oc#rs) tm = (s',CL'@Bk↑za,r') ∨
step0 (s,CL@Bk↑za, Oc#rs) tm = (s',CL'@Bk↑(za-1),r'))"
proof (cases "fetch tm (s - 0) (read (Oc#rs))")
case (Pair a s2)
then have A1: "fetch tm (s - 0) (read (Oc#rs)) = (a, s2)" .
show ?thesis
proof (cases a)
assume "a = WB"
from ‹a = WB› and assms A1 have "step0 (s, CL@Bk ↑ z1, Oc#rs) tm = (s2, CL@Bk ↑ z1, Bk#rs)" by auto
moreover from ‹a = WB› and assms A1 have "step0 (s, CL@Bk↑za, Oc#rs) tm = (s2,CL@Bk↑za , Bk#rs)" by auto
ultimately have "Bk↑z1 = Bk↑za@Bk↑(z1-za) ∧ step0 (s, CL@Bk↑za, Oc#rs) tm = (s2,CL@Bk↑za ,Bk#rs)"
using assms
by (metis le_eq_less_or_eq ordered_cancel_comm_monoid_diff_class.add_diff_inverse replicate_add)
then show ?thesis
using ‹step0 (s, CL @ Bk ↑ z1, Oc#rs) tm = (s2, CL @ Bk ↑ z1, Bk#rs)› assms(1) by auto
next
assume "a = WO"
from ‹a = WO› and assms A1 have "step0 (s, CL@Bk ↑ z1, Oc#rs) tm = (s2, CL@Bk ↑ z1, Oc#rs)" by auto
moreover from ‹a = WO› and assms A1 have "step0 (s, CL@Bk↑za, Oc#rs) tm = (s2,CL@Bk↑za , Oc#rs)" by auto
ultimately have "Bk↑z1 = Bk↑za@Bk↑(z1-za) ∧ step0 (s, CL@Bk↑za, Oc#rs) tm = (s2,CL@Bk↑za , Oc#rs)"
using assms
by (metis le_eq_less_or_eq ordered_cancel_comm_monoid_diff_class.add_diff_inverse replicate_add)
then show ?thesis
using ‹step0 (s, CL @ Bk ↑ z1, Oc#rs) tm = (s2, CL @ Bk ↑ z1, Oc#rs)› assms(1) by auto
next
assume "a = Nop"
from ‹a = Nop› and assms A1 have "step0 (s, CL@Bk ↑ z1, Oc#rs) tm = (s2, CL@Bk ↑ z1, Oc#rs)" by auto
moreover from ‹a = Nop› and assms A1 have "step0 (s, CL@Bk↑za, Oc#rs) tm = (s2,CL@Bk↑za , Oc#rs)" by auto
ultimately have "Bk↑z1 = Bk↑za@Bk↑(z1-za) ∧ step0 (s, CL@Bk↑za, Oc#rs) tm = (s2,CL@Bk↑za , Oc#rs)"
using assms
by (metis le_eq_less_or_eq ordered_cancel_comm_monoid_diff_class.add_diff_inverse replicate_add)
then show ?thesis
using ‹step0 (s, CL @ Bk ↑ z1, Oc#rs) tm = (s2, CL @ Bk ↑ z1, Oc#rs)› assms(1) by auto
next
assume "a = R"
from ‹a = R› and assms A1 have "step0 (s, CL@Bk ↑ z1, Oc#rs) tm = (s2, [Oc]@CL@Bk↑z1, rs)"
by auto
moreover from ‹a = R› and assms A1 have "step0 (s, CL@Bk↑za, Oc#rs) tm = (s2,[Oc]@CL@Bk↑za, rs)" by auto
ultimately have "Bk↑z1 = Bk↑za@Bk↑(z1-za) ∧ step0 (s, CL@Bk↑za, Oc#rs) tm = (s2,[Oc]@CL@Bk↑za, rs)"
using assms
by (metis le_eq_less_or_eq ordered_cancel_comm_monoid_diff_class.add_diff_inverse replicate_add)
then show ?thesis
using ‹step0 (s, CL @ Bk ↑ z1, Oc#rs) tm = (s2, [Oc] @ CL @ Bk ↑ z1, rs)›
by (metis append_Cons append_Nil assms(1) fst_conv snd_conv)
next
assume "a = L"
show ?thesis
proof (cases CL)
case Nil
then have "CL = []" .
then show ?thesis
proof (cases z1)
case 0
then have "z1 = 0" .
with assms and ‹CL = []› show ?thesis by auto
next
case (Suc nat)
then have "z1 = Suc nat" .
from ‹a = L› and ‹CL = []› and ‹z1 = Suc nat› and assms and A1
have "step0 (s, CL@Bk ↑ z1, Oc#rs) tm = (s2, []@Bk ↑(z1-1), Bk#Oc#rs)"
by auto
moreover from ‹a = L› and ‹CL = []› and A1 have "step0 (s, CL@Bk↑za, Oc#rs) tm = (s2, []@Bk↑(za-1) , Bk#Oc#rs)" by auto
ultimately have "Bk↑(z1-1) = Bk↑za@Bk↑(z1-1-za) ∧ step0 (s, CL@Bk↑za, Oc#rs) tm = (s2, []@Bk↑(za-1) , Bk#Oc#rs)"
using assms using ‹z1 = Suc nat›
by (metis diff_Suc_1 le_eq_less_or_eq less_Suc_eq ordered_cancel_comm_monoid_diff_class.add_diff_inverse replicate_add)
with assms and ‹CL = []› and ‹z1 = Suc nat› and ‹step0 (s, CL@Bk↑z1, Oc#rs) tm = (s2, [] @ Bk ↑ (z1 - 1), Bk#Oc#rs)›
show ?thesis
by auto
qed
next
case (Cons c cs)
then have "CL = c # cs" .
from ‹a = L› and ‹CL = c # cs› and assms and A1
have "step0 (s, CL@Bk ↑ z1, Oc#rs) tm = (s2, cs@Bk ↑z1, c#Oc#rs)"
by auto
moreover from ‹a = L› and ‹CL = c # cs› and A1
have "step0 (s, CL@Bk↑za, Oc#rs) tm = (s2, cs@Bk ↑za, c#Oc#rs)" by auto
ultimately have "Bk↑(z1-1) = Bk↑za@Bk↑(z1-1-za) ∧ step0 (s, CL@Bk↑za, Oc#rs) tm = (s2, cs@Bk ↑za, c#Oc#rs)"
using assms
by (metis One_nat_def Suc_pred add_diff_inverse_nat neq0_conv not_less_eq not_less_zero replicate_add)
with assms and ‹CL = c # cs› and ‹Bk↑(z1-1) = Bk↑za@Bk↑(z1-1-za) ∧ step0 (s, CL@Bk↑za, Oc#rs) tm = (s2, cs@Bk ↑za, c#Oc#rs)›
show ?thesis
using ‹step0 (s, CL @ Bk ↑ z1, Oc#rs) tm = (s2, cs @ Bk ↑ z1, c#Oc#rs)›
by (metis fst_conv nat_le_linear not_less ordered_cancel_comm_monoid_diff_class.add_diff_inverse replicate_add snd_conv)
qed
qed
qed
corollary step_left_tape_ShrinkBkCtx:
assumes "step0 (s,CL@Bk↑ z1 , r) tm = (s',l',r')"
and "za < z1"
shows "∃zb CL'. l' = CL'@Bk↑za@Bk↑zb ∧
(step0 (s,CL@Bk↑za, r) tm = (s',CL'@Bk↑za,r') ∨
step0 (s,CL@Bk↑za, r) tm = (s',CL'@Bk↑(za-1),r'))"
proof (cases r)
case Nil
then show ?thesis using step_left_tape_ShrinkBkCtx_right_Nil
using assms by blast
next
case (Cons rx rs)
then have "r = rx # rs" .
show ?thesis
proof (cases rx)
case Bk
with assms and ‹r = rx # rs› show ?thesis using step_left_tape_ShrinkBkCtx_right_Bk by blast
next
case Oc
with assms and ‹r = rx # rs› show ?thesis using step_left_tape_ShrinkBkCtx_right_Oc by blast
qed
qed
lemma steps_left_tape_ShrinkBkCtx_arbitrary_CL:
"⟦ steps0 (s, CL@Bk↑z1 , r) tm stp = (s',l',r'); 0 < z1 ⟧ ⟹
∃zb CL'. l' = CL'@Bk↑zb ∧ steps0 (s,CL, r) tm stp = (s',CL',r')"
proof (induct stp arbitrary: s CL z1 r s' l' r' z1)
case 0
assume "steps0 (s, CL @ Bk ↑ z1, r) tm 0 = (s', l', r')" and "0 < z1"
then show ?case
using less_imp_add_positive replicate_add by fastforce
next
fix stp s CL z1 r s' l' r'
assume IV: "⋀s2 CL2 z12 r2 s2' l2' r2'. ⟦steps0 (s2, CL2 @ Bk ↑ z12, r2) tm stp = (s2', l2', r2'); 0 < z12⟧
⟹ ∃zb2' CL2'. l2' = CL2' @ Bk ↑ zb2' ∧
steps0 (s2, CL2, r2) tm stp = (s2', CL2', r2')"
and major: "steps0 (s, CL @ Bk ↑ z1, r) tm (Suc stp) = (s', l', r')"
and minor: "0< z1"
show "∃zb CL'. l' = CL' @ Bk ↑ zb ∧ steps0 (s, CL, r) tm (Suc stp) = (s', CL', r')"
proof -
have F1: "steps0 (s, CL, r) tm (Suc stp) = step0 (steps0 (s, CL, r) tm stp) tm"
by (rule step_red)
have "steps0 (s, CL @ Bk ↑ z1, r) tm (Suc stp) = step0 (steps0 (s, CL @ Bk ↑ z1, r) tm stp) tm"
by (rule step_red)
with major
have F3: "step0 (steps0 (s, CL @ Bk ↑ z1, r) tm stp) tm = (s', l', r')" by auto
show ?thesis
proof (cases z1)
case 0
then have "z1 = 0" .
with minor
show ?thesis by auto
next
case (Suc z1')
then have "z1 = Suc z1'" .
show ?thesis
proof (cases "steps0 (s, CL @ Bk ↑ z1, r) tm stp")
case (fields sx lx rx)
then have C: "steps0 (s, CL @ Bk ↑ z1, r) tm stp = (sx, lx, rx)" .
with minor and IV
have F0: "∃zb2' CL2'. lx = CL2' @ Bk ↑ zb2' ∧
steps0 (s, CL, r) tm stp = (sx, CL2', rx)"
by auto
then obtain zb2' CL2' where
w_zb2'_CL2'_zc2': "lx = CL2' @ Bk ↑ zb2' ∧
steps0 (s, CL, r) tm stp = (sx, CL2', rx)"
by blast
from F3 and C have "step0 (sx,lx,rx) tm = (s',l',r')" by auto
with w_zb2'_CL2'_zc2' have F4: "step0 (sx,CL2' @ Bk ↑ zb2',rx) tm = (s',l',r')" by auto
then have "step0 (sx,CL2' @ Bk ↑ (zb2'),rx) tm = (s',l',r')"
by (simp add: replicate_add)
show ?thesis
proof (cases zb2')
case 0
then show ?thesis
using F1 ‹step0 (sx, lx, rx) tm = (s', l', r')› append_Nil2 replicate_0 w_zb2'_CL2'_zc2' by auto
next
case (Suc zb3')
then have "zb2' = Suc zb3'" .
then show ?thesis
by (metis F1 F4
append_Nil2 diff_is_0_eq'
replicate_0 self_append_conv2 step_left_tape_ShrinkBkCtx w_zb2'_CL2'_zc2'
zero_le_one zero_less_Suc)
qed
qed
qed
qed
qed
lemma step_left_tape_EnlargeBkCtx_eq_Bks:
assumes "step0 (s,Bk↑ z1, r) tm = (s',l',r')"
shows "step0 (s,Bk↑(z1+Suc z2), r) tm = (s',l'@Bk↑Suc z2,r') ∨
step0 (s,Bk↑(z1+Suc z2), r) tm = (s',l'@Bk↑z2,r')"
proof (cases s)
assume "s = 0"
with assms have "step0 (s, Bk↑(z1+Suc z2), r) tm = (s',l'@Bk↑Suc z2,r')"
using replicate_Suc_1 by fastforce
then show ?thesis by auto
next
fix s2
assume "s = Suc s2"
then show ?thesis
proof (cases r)
assume "r = []"
then show "step0 (s, Bk ↑ (z1 + Suc z2), r) tm = (s', l' @ Bk ↑ Suc z2, r') ∨
step0 (s, Bk ↑ (z1 + Suc z2), r) tm = (s', l' @ Bk ↑ z2, r')"
proof (cases "fetch tm (s - 0) (read r)")
case (Pair a s3)
then have "fetch tm (s - 0) (read r) = (a, s3)" .
then show ?thesis
proof (cases a)
case WB
from ‹a = WB› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, Bk↑(z1+Suc z2), r) tm = (s3, Bk↑(z1+Suc z2), [Bk])" by auto
moreover from ‹a = WB› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, Bk ↑ z1, r) tm = (s3, Bk ↑ z1, [Bk])" by auto
ultimately show ?thesis
using assms replicate_Suc_1 by fastforce
next
case WO
from ‹a = WO› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s,Bk↑(z1+Suc z2), r) tm = (s3, Bk↑(z1+Suc z2), [Oc])" by auto
moreover from ‹a = WO› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, Bk ↑ z1, r) tm = (s3, Bk ↑ z1, [Oc])" by auto
ultimately show ?thesis
using assms replicate_Suc_1 by fastforce
next
case L
from ‹a = L› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, Bk↑(z1+Suc z2), r) tm = (s3, Bk ↑ (z1 + z2), [Bk])" by auto
moreover from ‹a = L› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, Bk ↑ z1, r) tm = (s3, Bk ↑ (z1-1), [Bk])" by auto
ultimately show ?thesis
by (metis (no_types, lifting) Pair_inject add_Suc_right add_eq_if
assms diff_is_0_eq' replicate_add zero_le_one)
next
case R
from ‹a = R› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, Bk↑(z1+Suc z2), r) tm = (s3, Bk# Bk↑(z1+Suc z2), [])" by auto
moreover from ‹a = R› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, Bk ↑ z1, r) tm = (s3, Bk# Bk ↑ z1, [])" by auto
ultimately show ?thesis
using assms replicate_Suc_1 by fastforce
next
case Nop
from ‹a = Nop› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, Bk↑(z1+Suc z2), r) tm = (s3, Bk↑(z1+Suc z2), [])" by auto
moreover from ‹a = Nop› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, Bk ↑ z1, r) tm = (s3, Bk ↑ z1, [])" by auto
ultimately show ?thesis
using assms replicate_Suc_1 by fastforce
qed
qed
next
fix ra rrs
assume "r = ra # rrs"
then show "step0 (s, Bk ↑ (z1 + Suc z2), r) tm = (s', l' @ Bk ↑ Suc z2, r') ∨
step0 (s, Bk ↑ (z1 + Suc z2), r) tm = (s', l' @ Bk ↑ z2, r')"
proof (cases "fetch tm (s - 0) (read r)")
case (Pair a s3)
then have "fetch tm (s - 0) (read r) = (a, s3)" .
then show ?thesis
proof (cases a)
case WB
from ‹a = WB› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, Bk↑(z1+Suc z2), r) tm = (s3, Bk↑(z1+Suc z2), Bk# rrs)" by auto
moreover from ‹a = WB› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, Bk ↑ z1, r) tm = (s3, Bk ↑ z1, Bk# rrs)" by auto
ultimately show ?thesis
using assms replicate_Suc_1 by fastforce
next
case WO
from ‹a = WO› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, Bk↑(z1+Suc z2), r) tm = (s3, Bk↑(z1+Suc z2), Oc# rrs)" by auto
moreover from ‹a = WO› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, Bk ↑ z1, r) tm = (s3, Bk ↑ z1, Oc# rrs)" by auto
ultimately show ?thesis
using assms replicate_Suc_1 by fastforce
next
case L
from ‹a = L› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, Bk↑(z1+Suc z2), r) tm = (s3, Bk ↑ (z1 + z2), Bk#ra#rrs)" by auto
moreover from ‹a = L› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, Bk ↑ z1, r) tm = (s3, Bk ↑ (z1-1), Bk#ra#rrs)" by auto
ultimately show ?thesis
by (metis (no_types, lifting) Pair_inject add_Suc_right add_eq_if
assms diff_is_0_eq' replicate_add zero_le_one)
next
case R
from ‹a = R› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, Bk↑(z1+Suc z2), r) tm = (s3, ra# Bk↑(z1+Suc z2), rrs)" by auto
moreover from ‹a = R› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, Bk ↑ z1, r) tm = (s3, ra# Bk ↑ z1,rrs)" by auto
ultimately show ?thesis
using assms replicate_Suc_1 by fastforce
next
case Nop
from ‹a = Nop› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, Bk↑(z1+Suc z2), r) tm = (s3, Bk↑(z1+Suc z2), ra # rrs)" by auto
moreover from ‹a = Nop› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, Bk ↑ z1, r) tm = (s3, Bk ↑ z1, ra # rrs)" by auto
ultimately show ?thesis
using assms replicate_Suc_1 by fastforce
qed
qed
qed
qed
lemma step_left_tape_EnlargeBkCtx_eq_Bk_C_Bks:
assumes "step0 (s,(Bk#C)@Bk↑ z1, r) tm = (s',l',r')"
shows " step0 (s,(Bk#C)@Bk↑(z1+z2), r) tm = (s',l'@Bk↑z2,r')"
proof (cases s)
assume "s = 0"
with assms show "step0 (s, (Bk # C) @ Bk ↑ (z1 + z2), r) tm = (s', l' @ Bk ↑ z2, r')"
by (auto simp add: replicate_add)
next
fix s2
assume "s = Suc s2"
then show "step0 (s, (Bk # C) @ Bk ↑ (z1 + z2), r) tm = (s', l' @ Bk ↑ z2, r')"
proof (cases r)
assume "r = []"
then show ?thesis
proof (cases "fetch tm (s - 0) (read r)")
case (Pair a s3)
then have "fetch tm (s - 0) (read r) = (a, s3)" .
then show ?thesis
proof (cases a)
case WB
from ‹a = WB› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Bk # C) @ Bk ↑ (z1 + z2), r) tm = (s3, (Bk # C) @ Bk ↑ (z1 + z2), [Bk])" by auto
moreover from ‹a = WB› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Bk # C) @ Bk ↑ z1, r) tm = (s3, (Bk # C) @ Bk ↑ z1, [Bk])" by auto
ultimately show ?thesis
using assms
by (auto simp add: replicate_add)
next
case WO
from ‹a = WO› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Bk # C) @ Bk ↑ (z1 + z2), r) tm = (s3, (Bk # C) @ Bk ↑ (z1 + z2), [Oc])" by auto
moreover from ‹a = WO› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Bk # C) @ Bk ↑ z1, r) tm = (s3, (Bk # C) @ Bk ↑ z1, [Oc])" by auto
ultimately show ?thesis
using assms
by (auto simp add: replicate_add)
next
case L
from ‹a = L› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Bk # C) @ Bk ↑ (z1 + z2), r) tm = (s3, (C) @ Bk ↑ (z1 + z2), [Bk])" by auto
moreover from ‹a = L› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Bk # C) @ Bk ↑ z1, r) tm = (s3, (C) @ Bk ↑ z1, [Bk])" by auto
ultimately show ?thesis
using assms
by (auto simp add: replicate_add)
next
case R
from ‹a = R› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Bk # C) @ Bk ↑ (z1 + z2), r) tm = (s3, (Bk# Bk # C) @ Bk ↑ (z1 + z2), [])" by auto
moreover from ‹a = R› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Bk # C) @ Bk ↑ z1, r) tm = (s3, (Bk#Bk # C) @ Bk ↑ z1, [])" by auto
ultimately show ?thesis
using assms
by (auto simp add: replicate_add)
next
case Nop
from ‹a = Nop› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Bk # C) @ Bk ↑ (z1 + z2), r) tm = (s3, (Bk # C) @ Bk ↑ (z1 + z2), [])" by auto
moreover from ‹a = Nop› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Bk # C) @ Bk ↑ z1, r) tm = (s3, (Bk # C) @ Bk ↑ z1, [])" by auto
ultimately show ?thesis
using assms
by (auto simp add: replicate_add)
qed
qed
next
fix ra rrs
assume "r = ra # rrs"
then show "step0 (s, (Bk # C) @ Bk ↑ (z1 + z2), r) tm = (s', l' @ Bk ↑ z2, r')"
proof (cases "fetch tm (s - 0) (read r)")
case (Pair a s3)
then have "fetch tm (s - 0) (read r) = (a, s3)" .
then show ?thesis
proof (cases a)
case WB
from ‹a = WB› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Bk # C) @ Bk ↑ (z1 + z2), r) tm = (s3, (Bk # C) @ Bk ↑ (z1 + z2), Bk# rrs)" by auto
moreover from ‹a = WB› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Bk # C) @ Bk ↑ z1, r) tm = (s3, (Bk # C) @ Bk ↑ z1, Bk# rrs)" by auto
ultimately show ?thesis
using assms
by (auto simp add: replicate_add)
next
case WO
from ‹a = WO› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Bk # C) @ Bk ↑ (z1 + z2), r) tm = (s3, (Bk # C) @ Bk ↑ (z1 + z2), Oc# rrs)" by auto
moreover from ‹a = WO› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Bk # C) @ Bk ↑ z1, r) tm = (s3, (Bk # C) @ Bk ↑ z1, Oc# rrs)" by auto
ultimately show ?thesis
using assms
by (auto simp add: replicate_add)
next
case L
from ‹a = L› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Bk # C) @ Bk ↑ (z1 + z2), r) tm = (s3, (C) @ Bk ↑ (z1 + z2), Bk#ra#rrs)" by auto
moreover from ‹a = L› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Bk # C) @ Bk ↑ z1, r) tm = (s3, (C) @ Bk ↑ z1, Bk#ra#rrs)" by auto
ultimately show ?thesis
using assms
by (auto simp add: replicate_add)
next
case R
from ‹a = R› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Bk # C) @ Bk ↑ (z1 + z2), r) tm = (s3, (ra# Bk # C) @ Bk ↑ (z1 + z2), rrs)" by auto
moreover from ‹a = R› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Bk # C) @ Bk ↑ z1, r) tm = (s3, (ra#Bk # C) @ Bk ↑ z1,rrs)" by auto
ultimately show ?thesis
using assms
by (auto simp add: replicate_add)
next
case Nop
from ‹a = Nop› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Bk # C) @ Bk ↑ (z1 + z2), r) tm = (s3, (Bk # C) @ Bk ↑ (z1 + z2), ra # rrs)" by auto
moreover from ‹a = Nop› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Bk # C) @ Bk ↑ z1, r) tm = (s3, (Bk # C) @ Bk ↑ z1, ra # rrs)" by auto
ultimately show ?thesis
using assms
by (auto simp add: replicate_add)
qed
qed
qed
qed
lemma step_left_tape_EnlargeBkCtx_eq_Oc_C_Bks:
assumes "step0 (s,(Oc#C)@Bk↑ z1, r) tm = (s',l',r')"
shows " step0 (s,(Oc#C)@Bk↑(z1+z2), r) tm = (s',l'@Bk↑z2,r')"
proof (cases s)
assume "s = 0"
with assms show "step0 (s, (Oc # C) @ Bk ↑ (z1 + z2), r) tm = (s', l' @ Bk ↑ z2, r')"
by (auto simp add: replicate_add)
next
fix s2
assume "s = Suc s2"
then show "step0 (s, (Oc # C) @ Bk ↑ (z1 + z2), r) tm = (s', l' @ Bk ↑ z2, r')"
proof (cases r)
assume "r = []"
then show ?thesis
proof (cases "fetch tm (s - 0) (read r)")
case (Pair a s3)
then have "fetch tm (s - 0) (read r) = (a, s3)" .
then show ?thesis
proof (cases a)
case WB
from ‹a = WB› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Oc # C) @ Bk ↑ (z1 + z2), r) tm = (s3, (Oc # C) @ Bk ↑ (z1 + z2), [Bk])" by auto
moreover from ‹a = WB› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Oc # C) @ Bk ↑ z1, r) tm = (s3, (Oc # C) @ Bk ↑ z1, [Bk])" by auto
ultimately show ?thesis
using assms
by (auto simp add: replicate_add)
next
case WO
from ‹a = WO› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Oc # C) @ Bk ↑ (z1 + z2), r) tm = (s3, (Oc # C) @ Bk ↑ (z1 + z2), [Oc])" by auto
moreover from ‹a = WO› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Oc # C) @ Bk ↑ z1, r) tm = (s3, (Oc # C) @ Bk ↑ z1, [Oc])" by auto
ultimately show ?thesis
using assms
by (auto simp add: replicate_add)
next
case L
from ‹a = L› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Oc # C) @ Bk ↑ (z1 + z2), r) tm = (s3, (C) @ Bk ↑ (z1 + z2), [Oc])" by auto
moreover from ‹a = L› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Oc # C) @ Bk ↑ z1, r) tm = (s3, (C) @ Bk ↑ z1, [Oc])" by auto
ultimately show ?thesis
using assms
by (auto simp add: replicate_add)
next
case R
from ‹a = R› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Oc # C) @ Bk ↑ (z1 + z2), r) tm = (s3, (Bk# Oc # C) @ Bk ↑ (z1 + z2), [])" by auto
moreover from ‹a = R› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Oc # C) @ Bk ↑ z1, r) tm = (s3, (Bk#Oc # C) @ Bk ↑ z1, [])" by auto
ultimately show ?thesis
using assms
by (auto simp add: replicate_add)
next
case Nop
from ‹a = Nop› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Oc # C) @ Bk ↑ (z1 + z2), r) tm = (s3, (Oc # C) @ Bk ↑ (z1 + z2), [])" by auto
moreover from ‹a = Nop› ‹r = []› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Oc # C) @ Bk ↑ z1, r) tm = (s3, (Oc # C) @ Bk ↑ z1, [])" by auto
ultimately show ?thesis
using assms
by (auto simp add: replicate_add)
qed
qed
next
fix ra rrs
assume "r = ra # rrs"
then show "step0 (s, (Oc # C) @ Bk ↑ (z1 + z2), r) tm = (s', l' @ Bk ↑ z2, r')"
proof (cases "fetch tm (s - 0) (read r)")
case (Pair a s3)
then have "fetch tm (s - 0) (read r) = (a, s3)" .
then show ?thesis
proof (cases a)
case WB
from ‹a = WB› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Oc # C) @ Bk ↑ (z1 + z2), r) tm = (s3, (Oc # C) @ Bk ↑ (z1 + z2), Bk# rrs)" by auto
moreover from ‹a = WB› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Oc # C) @ Bk ↑ z1, r) tm = (s3, (Oc # C) @ Bk ↑ z1, Bk# rrs)" by auto
ultimately show ?thesis
using assms
by (auto simp add: replicate_add)
next
case WO
from ‹a = WO› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Oc # C) @ Bk ↑ (z1 + z2), r) tm = (s3, (Oc # C) @ Bk ↑ (z1 + z2), Oc# rrs)" by auto
moreover from ‹a = WO› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Oc # C) @ Bk ↑ z1, r) tm = (s3, (Oc # C) @ Bk ↑ z1, Oc# rrs)" by auto
ultimately show ?thesis
using assms
by (auto simp add: replicate_add)
next
case L
from ‹a = L› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Oc # C) @ Bk ↑ (z1 + z2), r) tm = (s3, (C) @ Bk ↑ (z1 + z2), Oc#ra#rrs)" by auto
moreover from ‹a = L› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Oc # C) @ Bk ↑ z1, r) tm = (s3, (C) @ Bk ↑ z1, Oc#ra#rrs)" by auto
ultimately show ?thesis
using assms
by (auto simp add: replicate_add)
next
case R
from ‹a = R› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Oc # C) @ Bk ↑ (z1 + z2), r) tm = (s3, (ra# Oc # C) @ Bk ↑ (z1 + z2), rrs)" by auto
moreover from ‹a = R› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Oc # C) @ Bk ↑ z1, r) tm = (s3, (ra#Oc # C) @ Bk ↑ z1,rrs)" by auto
ultimately show ?thesis
using assms
by (auto simp add: replicate_add)
next
case Nop
from ‹a = Nop› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Oc # C) @ Bk ↑ (z1 + z2), r) tm = (s3, (Oc # C) @ Bk ↑ (z1 + z2), ra # rrs)" by auto
moreover from ‹a = Nop› ‹r = ra # rrs› ‹fetch tm (s - 0) (read r) = (a, s3)›
have "step0 (s, (Oc # C) @ Bk ↑ z1, r) tm = (s3, (Oc # C) @ Bk ↑ z1, ra # rrs)" by auto
ultimately show ?thesis
using assms
by (auto simp add: replicate_add)
qed
qed
qed
qed
lemma step_left_tape_EnlargeBkCtx_eq_C_Bks_Suc:
assumes "step0 (s,C@Bk↑ z1, r) tm = (s',l',r')"
shows "step0 (s,C@Bk↑(z1+ Suc z2), r) tm = (s',l'@Bk↑Suc z2,r') ∨
step0 (s,C@Bk↑(z1+ Suc z2), r) tm = (s',l'@Bk↑z2,r')"
proof (cases C)
case Nil
then have "C = []" .
with assms show ?thesis by (metis append.left_neutral step_left_tape_EnlargeBkCtx_eq_Bks)
next
case (Cons x C')
then have "C = x # C'" .
then show ?thesis
proof (cases x)
case Bk
then have "x = Bk" .
then show ?thesis
using assms local.Cons step_left_tape_EnlargeBkCtx_eq_Bk_C_Bks by blast
next
case Oc
then have "x = Oc" .
then show ?thesis
using assms local.Cons step_left_tape_EnlargeBkCtx_eq_Oc_C_Bks by blast
qed
qed
lemma step_left_tape_EnlargeBkCtx_eq_C_Bks:
assumes "step0 (s,C@Bk↑ z1, r) tm = (s',l',r')"
shows "step0 (s,C@Bk↑(z1+ z2), r) tm = (s',l'@Bk↑z2,r') ∨
step0 (s,C@Bk↑(z1+ z2), r) tm = (s',l'@Bk↑(z2-1),r')"
by (smt (verit) step_left_tape_EnlargeBkCtx_eq_C_Bks_Suc One_nat_def Suc_pred add.right_neutral
append.right_neutral assms neq0_conv replicate_empty)
lemma steps_left_tape_EnlargeBkCtx_arbitrary_CL:
"steps0 (s, CL @ Bk↑z1, r) tm stp = (s', l',r')
⟹
∃z3. z3 ≤ z1 + z2 ∧
steps0 (s, CL @ Bk↑(z1 + z2), r) tm stp = (s',l' @ Bk↑z3 ,r')"
proof (induct stp arbitrary: s CL z1 r z2 s' l' r')
fix s CL z1 r z2 s' l' r'
assume "steps0 (s, CL @ Bk ↑ z1, r) tm 0 = (s', l', r')"
show "∃z3≤z1 + z2. steps0 (s, CL @ Bk ↑ (z1 + z2), r) tm 0 = (s', l' @ Bk ↑ z3, r')"
by (metis ‹steps0 (s, CL @ Bk ↑ z1, r) tm 0 = (s', l', r')›
append.assoc fst_conv le_add2 replicate_add snd_conv steps.simps(1))
next
fix stp s CL z1 r z2 s' l' r'
assume IV: "⋀s CL z1 r z2 s' l' r'. steps0 (s, CL @ Bk ↑ z1, r) tm stp = (s', l', r')
⟹ ∃z3≤z1 + z2. steps0 (s, CL @ Bk ↑ (z1 + z2), r) tm stp = (s', l' @ Bk ↑ z3, r')"
and minor: "steps0 (s, CL @ Bk ↑ z1, r) tm (Suc stp) = (s', l', r')"
show "∃z3≤z1 + z2. steps0 (s, CL @ Bk ↑ (z1 + z2), r) tm (Suc stp) = (s', l' @ Bk ↑ z3, r')"
proof -
have F1: "steps0 (s, CL @ Bk ↑ (z1 + z2), r) tm (Suc stp) = step0 (steps0 (s, CL @ Bk ↑ (z1 + z2), r) tm stp) tm"
by (rule step_red)
have "steps0 (s, CL @ Bk ↑ z1, r) tm (Suc stp) = step0 (steps0 (s, CL @ Bk ↑ z1, r) tm stp) tm"
by (rule step_red)
with minor
have F3: "step0 (steps0 (s, CL @ Bk ↑ z1, r) tm stp) tm = (s', l', r')" by auto
show "∃z3. z3 ≤ z1 + z2 ∧ steps0 (s, CL @ Bk ↑ (z1 + z2), r) tm (Suc stp) = (s', l' @ Bk ↑ z3, r')"
proof (cases "steps0 (s, CL @ Bk ↑ z1, r) tm stp")
case (fields sx lx rx)
then have CL: "steps0 (s, CL @ Bk ↑ z1, r) tm stp = (sx, lx, rx)" .
with IV
have "∃z3'≤z1 + z2. steps0 (s, CL @ Bk ↑ (z1 + z2), r) tm stp = (sx, lx @ Bk ↑ z3', rx)" by auto
then obtain z3' where
w_z3': "z3'≤z1 + z2 ∧
steps0 (s, CL @ Bk ↑ (z1 + z2), r) tm stp = (sx, lx @ Bk ↑ z3', rx)" by blast
moreover
have "step0 (sx,lx@Bk↑z3', rx) tm = (s',l' @ Bk↑(z3') ,r') ∨
step0 (sx,lx@Bk↑z3', rx) tm = (s',l' @ Bk↑(z3'-1),r')"
proof -
from F3 and CL have "step0 (sx, lx@Bk↑0, rx) tm = (s', l', r')" by auto
then have "step0 (sx,lx@Bk↑(0+z3'), rx) tm = (s',l' @ Bk↑(z3') ,r') ∨
step0 (sx,lx@Bk↑(0+z3'), rx) tm = (s',l' @ Bk↑(z3'-1) ,r')"
by (rule step_left_tape_EnlargeBkCtx_eq_C_Bks)
then show "step0 (sx,lx@Bk↑z3', rx) tm = (s',l' @ Bk↑(z3') ,r') ∨
step0 (sx,lx@Bk↑z3', rx) tm = (s',l' @ Bk↑(z3'-1),r')"
by auto
qed
moreover from w_z3' and F1
have "steps0 (s, CL @ Bk ↑ (z1 + z2), r) tm (Suc stp) = step0 (sx, lx @ Bk ↑ z3', rx) tm"
by auto
ultimately
have "steps0 (s, CL @ Bk ↑ (z1 + z2), r) tm (Suc stp) = (s', l' @ Bk ↑ z3', r') ∨
steps0 (s, CL @ Bk ↑ (z1 + z2), r) tm (Suc stp) = (s', l' @ Bk ↑ (z3'-1), r')"
by auto
with w_z3' show ?thesis
by (auto simp add: split: if_splits)
qed
qed
qed
corollary steps_left_tape_EnlargeBkCtx:
" steps0 (s, Bk ↑ k, r) tm stp = (s', Bk ↑ l, r')
⟹
∃z3. z3 ≤ k + z2 ∧
steps0 (s, Bk ↑ (k + z2), r) tm stp = (s',Bk ↑ (l + z3), r')"
proof -
assume "steps0 (s, Bk ↑ k, r) tm stp = (s', Bk ↑ l, r')"
then have "∃z3. z3 ≤ k + z2 ∧
steps0 (s, Bk ↑ (k + z2), r) tm stp = (s',Bk ↑ l @ Bk ↑ z3, r')"
by (metis append_Nil steps_left_tape_EnlargeBkCtx_arbitrary_CL)
then show ?thesis by (simp add: replicate_add)
qed
corollary steps_left_tape_ShrinkBkCtx_to_NIL:
" steps0 (s, Bk ↑ k, r) tm stp = (s', Bk ↑ l, r')
⟹
∃z3. z3 ≤ l ∧
steps0 (s, [], r) tm stp = (s', Bk ↑ z3, r')"
proof -
assume A: "steps0 (s, Bk ↑ k, r) tm stp = (s', Bk ↑ l, r')"
then have F0: "∃zb CL'. Bk ↑ l = CL'@Bk↑zb ∧ steps0 (s,[], r) tm stp = (s',CL',r')"
proof (cases k)
case 0
then show ?thesis
using A append_Nil2 replicate_0 by auto
next
case (Suc nat)
then have "0 < k" by auto
with A show ?thesis
using steps_left_tape_ShrinkBkCtx_arbitrary_CL by auto
qed
then obtain zb CL' where
w: "Bk ↑ l = CL'@Bk↑zb ∧ steps0 (s,[], r) tm stp = (s',CL',r')" by blast
then show ?thesis
by (metis append_same_eq le_add1 length_append length_replicate replicate_add)
qed
lemma steps_left_tape_Nil_imp_All:
"steps0 (s, ([] , r)) p stp = (s', Bk ↑ k, CR @ Bk ↑ l)
⟹
∀z. ∃stp k l. (steps0 (s, (Bk↑z, r)) p stp) = (s', Bk ↑ k, CR @ Bk ↑ l)"
proof
fix z
assume A: "steps0 (s, [], r) p stp = (s', Bk ↑ k, CR @ Bk ↑ l)"
then have "steps0 (s, Bk ↑ 0 , r) p stp = (s', Bk ↑ k, CR @ Bk ↑ l)" by auto
then have "∃z3. z3 ≤ 0 + z ∧
steps0 (s, Bk ↑ (0 + z), r) p stp = (s',Bk ↑ (k + z3), CR @ Bk ↑ l)"
by (rule steps_left_tape_EnlargeBkCtx)
then have "∃z3. steps0 (s, Bk ↑ z, r) p stp = (s',Bk ↑ (k + z3), CR @ Bk ↑ l)"
by auto
then obtain z3 where
"steps0 (s, Bk ↑ z, r) p stp = (s',Bk ↑ (k + z3), CR @ Bk ↑ l)" by blast
then show "∃stp k l. steps0 (s, Bk ↑ z,r) p stp = (s', Bk ↑ k, CR @ Bk ↑ l)"
by auto
qed
lemma ex_steps_left_tape_Nil_imp_All:
"∃stp k l. (steps0 (s, ([] , r)) p stp) = (s', Bk ↑ k, CR @ Bk ↑ l)
⟹
∀z. ∃stp k l. (steps0 (s, (Bk↑z, r)) p stp) = (s', Bk ↑ k, CR @ Bk ↑ l)"
proof
fix z
assume A: "∃stp k l. steps0 (s, [], r) p stp = (s', Bk ↑ k, CR @ Bk ↑ l)"
then obtain stp k l where
"steps0 (s, [], r) p stp = (s', Bk ↑ k, CR @ Bk ↑ l)" by blast
then show "∃stp k l. steps0 (s, Bk ↑ z, r) p stp = (s', Bk ↑ k, CR @ Bk ↑ l)"
using steps_left_tape_Nil_imp_All
by auto
qed
subsection ‹Trailing blanks on the right tape do not matter›
lemma step_left_tape_Nil_imp_all_trailing_right_Nil:
assumes "step0 (s, CL1, [] ) tm = (s', CR1, CR2 )"
shows "step0 (s, CL1, [] @ Bk ↑ y) tm = (s', CR1, CR2 @ Bk ↑ y) ∨
step0 (s, CL1, [] @ Bk ↑ y) tm = (s', CR1, CR2 @ Bk ↑ (y-1))"
proof (cases "fetch tm (s - 0) (read ([] ))")
case (Pair a s2)
then have A1: "fetch tm (s - 0) (read ([])) = (a, s2)" .
show ?thesis
proof (cases a)
assume "a = WB"
from ‹a = WB› and assms A1 have "step0 (s, CL1, [] ) tm = (s2, CL1, [Bk])" by auto
moreover from ‹a = WB› and assms A1 have "step0 (s, CL1, [] @ Bk ↑ y) tm = (s2, CL1, [Bk]@Bk ↑ (y-1))" by auto
ultimately show ?thesis using assms by auto
next
assume "a = WO"
from ‹a = WO› and assms A1 have "step0 (s, CL1, [] ) tm = (s2, CL1, [Oc])" by auto
moreover from ‹a = WO› and assms A1 have "step0 (s, CL1, [] @ Bk ↑ y) tm = (s2, CL1, [Oc] @ Bk ↑ (y-1))" by auto
ultimately show ?thesis using assms by auto
next
assume "a = L"
show ?thesis
proof (cases CL1)
case Nil
then have "CL1 = []" .
from ‹CL1 = []› and ‹a = L› and assms A1 have "step0 (s, CL1, [] ) tm = (s2, CL1, [Bk])"
by auto
moreover from ‹CL1 = []› and ‹a = L› and assms A1
have "step0 (s, CL1, [] @ Bk ↑ y) tm = (s2, CL1, Bk # Bk ↑ y)"
by (auto simp add: split: if_splits)
ultimately show ?thesis using assms by auto
next
case (Cons c cs)
then have "CL1 = c # cs" .
from ‹CL1 = c # cs › and ‹a = L› and assms A1 have "step0 (s, CL1, [] ) tm = (s2, cs, [c])"
by auto
moreover from ‹CL1 = c # cs› and ‹a = L› and assms A1
have "step0 (s, CL1, [] @ Bk ↑ y) tm = (s2, cs, c # Bk ↑ y)"
by (auto simp add: split: if_splits)
ultimately show ?thesis using assms by auto
qed
next
assume "a = Nop"
from ‹a = Nop› and assms and A1 have "step0 (s, CL1, [] ) tm = (s2, CL1, [] )"
by auto
moreover from ‹a = Nop› and assms and A1 have "step0 (s, CL1, [] @ Bk ↑ y) tm = (s2, CL1, [] @ Bk ↑ y)" by auto
ultimately show ?thesis using assms by auto
next
assume "a = R"
from ‹a = R› and assms A1 have "step0 (s, CL1, [] ) tm = (s2, Bk#CL1, [] )"
by auto
moreover from ‹a = R› and assms A1 have "step0 (s, CL1, [] @ Bk ↑ y) tm = (s2, Bk#CL1, []@ Bk ↑ (y-1) )"
by auto
ultimately show ?thesis using assms by auto
qed
qed
lemma step_left_tape_Nil_imp_all_trailing_right_Cons:
assumes "step0 (s, CL1, rx#rs ) tm = (s', CR1, CR2 )"
shows "step0 (s, CL1, rx#rs @ Bk ↑ y) tm = (s', CR1, CR2 @ Bk ↑ y)"
proof (cases "fetch tm (s - 0) (read (rx#rs ))")
case (Pair a s2)
then have A1: "fetch tm (s - 0) (read (rx#rs )) = (a, s2)" .
show ?thesis
proof (cases a)
assume "a = WB"
from ‹a = WB› and assms A1 have "step0 (s, CL1, rx#rs ) tm = (s2, CL1, Bk#rs )" by auto
moreover from ‹a = WB› and assms A1 have "step0 (s, CL1, rx#rs @ Bk ↑ y) tm = (s2, CL1, Bk#rs @ Bk ↑ y)" by auto
ultimately show ?thesis using assms by auto
next
assume "a = WO"
from ‹a = WO› and assms A1 have "step0 (s, CL1, rx#rs ) tm = (s2, CL1, Oc#rs )" by auto
moreover from ‹a = WO› and assms A1 have "step0 (s, CL1, rx#rs @ Bk ↑ y) tm = (s2, CL1, Oc#rs @ Bk ↑ y)" by auto
ultimately show ?thesis using assms by auto
next
assume "a = L"
show ?thesis
proof (cases CL1)
case Nil
then have "CL1 = []" .
show ?thesis
proof -
from ‹a = L› and ‹CL1 = []› and assms A1 have "step0 (s, CL1, rx#rs ) tm = (s2, CL1, Bk#rx#rs )" by auto
moreover from ‹a = L› and ‹CL1 = []› and assms A1 have "step0 (s, CL1, rx#rs @ Bk ↑ y) tm = (s2, CL1, Bk#rx#rs @ Bk ↑ y)" by auto
ultimately show ?thesis using assms by auto
qed
next
case (Cons c cs)
then have "CL1 = c # cs" .
show ?thesis
proof -
from ‹a = L› and ‹CL1 = c # cs› and assms A1 have "step0 (s, CL1, rx#rs ) tm = (s2, cs, c#rx#rs )" by auto
moreover from ‹a = L› and ‹CL1 = c # cs› and assms A1 have "step0 (s, CL1, rx#rs @ Bk ↑ y) tm = (s2, cs, c#rx#rs @ Bk ↑ y)" by auto
ultimately show ?thesis using assms by auto
qed
qed
next
assume "a = R"
from ‹a = R› and assms A1 have "step0 (s, CL1, rx#rs ) tm = (s2, rx#CL1, rs )" by auto
moreover from ‹a = R› and assms A1 have "step0 (s, CL1, rx#rs @ Bk ↑ y) tm = (s2, rx#CL1, rs @ Bk ↑ y)" by auto
ultimately show ?thesis using assms by auto
next
assume "a = Nop"
from ‹a = Nop› and assms A1 have "step0 (s, CL1, rx#rs ) tm = (s2, CL1, rx#rs )"
by (auto simp add: split: if_splits)
moreover from ‹a = Nop› and assms A1 have "step0 (s, CL1, rx#rs @ Bk ↑ y) tm = (s2, CL1, rx#rs @ Bk ↑ y)" by auto
ultimately show ?thesis using assms by auto
qed
qed
lemma step_left_tape_Nil_imp_all_trailing_right:
assumes "step0 (s, CL1, r ) tm = (s', CR1, CR2 )"
shows "step0 (s, CL1, r @ Bk ↑ y) tm = (s', CR1, CR2 @ Bk ↑ y) ∨
step0 (s, CL1, r @ Bk ↑ y) tm = (s', CR1, CR2 @ Bk ↑ (y-1))"
proof (cases r)
case Nil
then show ?thesis using step_left_tape_Nil_imp_all_trailing_right_Nil assms by auto
next
case (Cons a list)
then show ?thesis using step_left_tape_Nil_imp_all_trailing_right_Cons assms by auto
qed
lemma steps_left_tape_Nil_imp_all_trailing_right:
"steps0 (s, CL1, r ) tm stp = (s', CR1, CR2)
⟹
∃x1 x2. y = x1 + x2 ∧
steps0 (s, CL1, r @ Bk ↑ y ) tm stp = (s', CR1, CR2 @ Bk ↑ x2)"
proof (induct stp arbitrary: s CL1 r y s' CR1 CR2)
case 0
then show ?case
by (simp add: "0.prems" steps_left_tape_Nil_imp_All)
next
fix stp s CL1 r y s' CR1 CR2
assume IV: "⋀s CL1 r y s' CR1 CR2. steps0 (s, CL1, r) tm stp = (s', CR1, CR2) ⟹ ∃x1 x2. y = x1 + x2 ∧ steps0 (s, CL1, r @ Bk ↑ y) tm stp = (s', CR1, CR2 @ Bk ↑ x2)"
and major: "steps0 (s, CL1, r) tm (Suc stp) = (s', CR1, CR2)"
show "∃x1 x2. y = x1 + x2 ∧ steps0 (s, CL1, r @ Bk ↑ y) tm (Suc stp) = (s', CR1, CR2 @ Bk ↑ x2)"
proof -
have F1: "steps0 (s, CL1, r @ Bk ↑ y) tm (Suc stp) = step0 (steps0 (s, CL1, r @ Bk ↑ y) tm stp) tm"
by (rule step_red)
have "steps0 (s, CL1, r) tm (Suc stp) = step0 (steps0 (s, CL1, r) tm stp) tm"
by (rule step_red)
with major
have F3: "step0 (steps0 (s, CL1, r) tm stp) tm = (s', CR1, CR2)" by auto
show "∃x1 x2. y = x1 + x2 ∧ steps0 (s, CL1, r @ Bk ↑ y) tm (Suc stp) = (s', CR1, CR2 @ Bk ↑ x2)"
proof (cases y)
case 0
then have "y = 0" .
with major show ?thesis by auto
next
case (Suc y')
then have "y = Suc y'" .
then show ?thesis
proof (cases "steps0 (s, CL1, r) tm stp")
case (fields sx lx rx)
then have C: "steps0 (s, CL1, r) tm stp = (sx, lx, rx)" .
with major and IV have F0: "∃x1' x2'. y = x1' + x2' ∧ steps0 (s, CL1, r @ Bk ↑ y) tm stp = (sx, lx, rx @ Bk ↑ x2')"
by auto
then obtain x1' x2' where w_x1'_x2': " y = x1' + x2' ∧ steps0 (s, CL1, r @ Bk ↑ y) tm stp = (sx, lx, rx @ Bk ↑ x2')" by blast
moreover have "step0 (sx, lx, rx @ Bk ↑ x2') tm = (s', CR1, CR2 @ Bk ↑ x2') ∨
step0 (sx, lx, rx @ Bk ↑ x2') tm = (s', CR1, CR2 @ Bk ↑ (x2'-1))"
proof -
from F3 and C have F5: "step0 (sx, lx, rx) tm = (s', CR1, CR2)" by auto
then have "step0 (sx, lx, rx @ Bk ↑ x2') tm = (s', CR1, CR2 @ Bk ↑ x2') ∨
step0 (sx, lx, rx @ Bk ↑ x2') tm = (s', CR1, CR2 @ Bk ↑ (x2'-1))"
by (rule step_left_tape_Nil_imp_all_trailing_right)
then show "step0 (sx, lx, rx @ Bk ↑ x2') tm = (s', CR1, CR2 @ Bk ↑ x2') ∨
step0 (sx, lx, rx @ Bk ↑ x2') tm = (s', CR1, CR2 @ Bk ↑ (x2'-1))"
by auto
qed
moreover from w_x1'_x2' and F1
have "steps0 (s, CL1, r @ Bk ↑ y) tm (Suc stp) = step0 (sx, lx, rx @ Bk ↑ x2') tm" by auto
ultimately have F5: "y = x1' + x2' ∧
(steps0 (s, CL1, r @ Bk ↑ y) tm (Suc stp) = (s', CR1, CR2 @ Bk ↑ x2') ∨
steps0 (s, CL1, r @ Bk ↑ y) tm (Suc stp) = (s', CR1, CR2 @ Bk ↑ (x2' - 1)))"
by auto
with w_x1'_x2' show ?thesis
proof (cases x2')
case 0
with F5 have "y = x1' + 0 ∧
steps0 (s, CL1, r @ Bk ↑ y) tm (Suc stp) = (s', CR1, CR2 @ Bk ↑ 0)"
by (auto simp add: split: if_splits)
with w_x1'_x2' show ?thesis
by (auto simp add: split: if_splits)
next
case (Suc x2'')
with w_x1'_x2' show ?thesis
using F5 add_Suc_right add_Suc_shift diff_Suc_1 by fastforce
qed
qed
qed
qed
qed
lemma ex_steps_left_tape_Nil_imp_All_left_and_right:
"(∃kr lr. steps0 (1, ([] , r )) p stp = (0, Bk ↑ kr, r' @ Bk ↑ lr))
⟹
∀kl ll. ∃kr lr. steps0 (1, (Bk ↑ kl, r @ Bk ↑ ll)) p stp = (0, Bk ↑ kr, r' @ Bk ↑ lr)"
proof -
assume "(∃kr lr. steps0 (1, ([] , r )) p stp = (0, Bk ↑ kr, r' @ Bk ↑ lr))"
then obtain kr lr where
w_kr_lr: "steps0 (1, ([] , r )) p stp = (0, Bk ↑ kr, r' @ Bk ↑ lr)" by blast
then have "steps0 (1, (Bk ↑ 0 , r )) p stp = (0, Bk ↑ kr, r' @ Bk ↑ lr)"
by auto
then have "⋀kl. ∃z3. z3 ≤ 0 + kl ∧ steps0 (1, Bk ↑ (0 + kl), r) p stp = (0,Bk ↑ (kr + z3), r' @ Bk ↑ lr)"
using steps_left_tape_EnlargeBkCtx
using plus_nat.add_0 w_kr_lr by blast
then have "⋀kl. ∃z3. z3 ≤ kl ∧ steps0 (1, Bk ↑ kl, r) p stp = (0,Bk ↑ (kr + z3), r' @ Bk ↑ lr)"
by auto
then have F0: "⋀kl. ∃z4. steps0 (1, Bk ↑ kl, r ) p stp = (0,Bk ↑ z4 , r' @ Bk ↑ lr)"
by auto
show ?thesis
proof
fix kl
show " ∀ll. ∃kr lr. steps0 (1, Bk ↑ kl, r @ Bk ↑ ll) p stp = (0, Bk ↑ kr, r' @ Bk ↑ lr)"
proof
fix ll
show "∃kr lr. steps0 (1, Bk ↑ kl, r @ Bk ↑ ll) p stp = (0, Bk ↑ kr, r' @ Bk ↑ lr)"
proof -
from F0 have "∃z4. steps0 (1, Bk ↑ kl, r ) p stp = (0,Bk ↑ z4 , r' @ Bk ↑ lr)"
by auto
then obtain z4 where w_z4: "steps0 (1, Bk ↑ kl, r ) p stp = (0,Bk ↑ z4 , r' @ Bk ↑ lr)" by blast
then have "∃x1 x2. ll = x1 + x2 ∧
steps0 (1, Bk ↑ kl , r @ Bk ↑ ll ) p stp = (0, Bk ↑ z4 , r' @ Bk ↑ lr @ Bk ↑ x2)"
using steps_left_tape_Nil_imp_all_trailing_right
using append_assoc by fastforce
then show "∃kr lr. steps0 (1, Bk ↑ kl, r @ Bk ↑ ll) p stp = (0, Bk ↑ kr, r' @ Bk ↑ lr)"
by (metis replicate_add)
qed
qed
qed
qed
end