# Theory Temporal

```theory Temporal
imports MDL NFA Window
begin

fun state_cnt :: "('a, 'b :: timestamp) regex ⇒ nat" where
| "state_cnt (Symbol phi) = 2"
| "state_cnt (Plus r s) = 1 + state_cnt r + state_cnt s"
| "state_cnt (Times r s) = state_cnt r + state_cnt s"
| "state_cnt (Star r) = 1 + state_cnt r"

lemma state_cnt_pos: "state_cnt r > 0"
by (induction r rule: state_cnt.induct) auto

fun collect_subfmlas :: "('a, 'b :: timestamp) regex ⇒ ('a, 'b) formula list ⇒
('a, 'b) formula list" where
"collect_subfmlas (Lookahead φ) phis = (if φ ∈ set phis then phis else phis @ [φ])"
| "collect_subfmlas (Symbol φ) phis = (if φ ∈ set phis then phis else phis @ [φ])"
| "collect_subfmlas (Plus r s) phis = collect_subfmlas s (collect_subfmlas r phis)"
| "collect_subfmlas (Times r s) phis = collect_subfmlas s (collect_subfmlas r phis)"
| "collect_subfmlas (Star r) phis = collect_subfmlas r phis"

lemma bf_collect_subfmlas: "bounded_future_regex r ⟹ phi ∈ set (collect_subfmlas r phis) ⟹
phi ∈ set phis ∨ bounded_future_fmla phi"
by (induction r phis rule: collect_subfmlas.induct) (auto split: if_splits)

lemma collect_subfmlas_atms: "set (collect_subfmlas r phis) = set phis ∪ atms r"
by (induction r phis rule: collect_subfmlas.induct) (auto split: if_splits)

lemma collect_subfmlas_set: "set (collect_subfmlas r phis) = set (collect_subfmlas r []) ∪ set phis"
proof (induction r arbitrary: phis)
case (Plus r1 r2)
show ?case
using Plus(1)[of phis] Plus(2)[of "collect_subfmlas r1 phis"]
Plus(2)[of "collect_subfmlas r1 []"]
by auto
next
case (Times r1 r2)
show ?case
using Times(1)[of phis] Times(2)[of "collect_subfmlas r1 phis"]
Times(2)[of "collect_subfmlas r1 []"]
by auto
next
case (Star r)
show ?case
using Star[of phis]
by auto
qed auto

lemma collect_subfmlas_size: "x ∈ set (collect_subfmlas r []) ⟹ size x < size r"
proof (induction r)
case (Plus r1 r2)
then show ?case
by (auto simp: collect_subfmlas_set[of r2 "collect_subfmlas r1 []"])
next
case (Times r1 r2)
then show ?case
by (auto simp: collect_subfmlas_set[of r2 "collect_subfmlas r1 []"])
next
case (Star r)
then show ?case
by fastforce
qed (auto split: if_splits)

lemma collect_subfmlas_app: "∃phis'. collect_subfmlas r phis = phis @ phis'"
by (induction r phis rule: collect_subfmlas.induct) auto

lemma length_collect_subfmlas: "length (collect_subfmlas r phis) ≥ length phis"
by (induction r phis rule: collect_subfmlas.induct) auto

fun pos :: "'a ⇒ 'a list ⇒ nat option" where
"pos a [] = None"
| "pos a (x # xs) =
(if a = x then Some 0 else (case pos a xs of Some n ⇒ Some (Suc n) | _ ⇒ None))"

lemma pos_sound: "pos a xs = Some i ⟹ i < length xs ∧ xs ! i = a"
by (induction a xs arbitrary: i rule: pos.induct) (auto split: if_splits option.splits)

lemma pos_complete: "pos a xs = None ⟹ a ∉ set xs"
by (induction a xs rule: pos.induct) (auto split: if_splits option.splits)

fun build_nfa_impl :: "('a, 'b :: timestamp) regex ⇒ (state × state × ('a, 'b) formula list) ⇒
transition list" where
"build_nfa_impl (Lookahead φ) (q0, qf, phis) = (case pos φ phis of
Some n ⇒ [eps_trans qf n]
| None ⇒ [eps_trans qf (length phis)])"
| "build_nfa_impl (Symbol φ) (q0, qf, phis) = (case pos φ phis of
Some n ⇒ [eps_trans (Suc q0) n, symb_trans qf]
| None ⇒ [eps_trans (Suc q0) (length phis), symb_trans qf])"
| "build_nfa_impl (Plus r s) (q0, qf, phis) = (
let ts_r = build_nfa_impl r (q0 + 1, qf, phis);
ts_s = build_nfa_impl s (q0 + 1 + state_cnt r, qf, collect_subfmlas r phis) in
split_trans (q0 + 1) (q0 + 1 + state_cnt r) # ts_r @ ts_s)"
| "build_nfa_impl (Times r s) (q0, qf, phis) = (
let ts_r = build_nfa_impl r (q0, q0 + state_cnt r, phis);
ts_s = build_nfa_impl s (q0 + state_cnt r, qf, collect_subfmlas r phis) in
ts_r @ ts_s)"
| "build_nfa_impl (Star r) (q0, qf, phis) = (
let ts_r = build_nfa_impl r (q0 + 1, q0, phis) in
split_trans (q0 + 1) qf # ts_r)"

lemma build_nfa_impl_state_cnt: "length (build_nfa_impl r (q0, qf, phis)) = state_cnt r"
by (induction r "(q0, qf, phis)" arbitrary: q0 qf phis rule: build_nfa_impl.induct)
(auto split: option.splits)

lemma build_nfa_impl_not_Nil: "build_nfa_impl r (q0, qf, phis) ≠ []"
by (induction r "(q0, qf, phis)" arbitrary: q0 qf phis rule: build_nfa_impl.induct)
(auto split: option.splits)

lemma build_nfa_impl_state_set: "t ∈ set (build_nfa_impl r (q0, qf, phis)) ⟹
state_set t ⊆ {q0..<q0 + length (build_nfa_impl r (q0, qf, phis))} ∪ {qf}"
by (induction r "(q0, qf, phis)" arbitrary: q0 qf phis t rule: build_nfa_impl.induct)
(fastforce simp add: build_nfa_impl_state_cnt state_cnt_pos build_nfa_impl_not_Nil
split: option.splits)+

lemma build_nfa_impl_fmla_set: "t ∈ set (build_nfa_impl r (q0, qf, phis)) ⟹
n ∈ fmla_set t ⟹ n < length (collect_subfmlas r phis)"
proof (induction r "(q0, qf, phis)" arbitrary: q0 qf phis t rule: build_nfa_impl.induct)
case (1 φ q0 qf phis)
then show ?case
using pos_sound pos_complete by (force split: option.splits)
next
case (2 φ q0 qf phis)
then show ?case
using pos_sound pos_complete by (force split: option.splits)
next
case (3 r s q0 qf phis)
then show ?case
using length_collect_subfmlas dual_order.strict_trans1 by fastforce
next
case (4 r s q0 qf phis)
then show ?case
using length_collect_subfmlas dual_order.strict_trans1 by fastforce
next
case (5 r q0 qf phis)
then show ?case
using length_collect_subfmlas dual_order.strict_trans1 by fastforce
qed

context MDL
begin

definition "IH r q0 qf phis transs bss bs i ≡
let n = length (collect_subfmlas r phis) in
transs = build_nfa_impl r (q0, qf, phis) ∧ (∀cs ∈ set bss. length cs ≥ n) ∧ length bs ≥ n ∧
qf ∉ NFA.SQ q0 (build_nfa_impl r (q0, qf, phis)) ∧
(∀k < n. (bs ! k ⟷ sat (collect_subfmlas r phis ! k) (i + length bss))) ∧
(∀j < length bss. ∀k < n. ((bss ! j) ! k ⟷ sat (collect_subfmlas r phis ! k) (i + j)))"

lemma nfa_correct: "IH r q0 qf phis transs bss bs i ⟹
NFA.run_accept_eps q0 qf transs {q0} bss bs ⟷ (i, i + length bss) ∈ match r"
proof (induct r arbitrary: q0 qf phis transs bss bs i rule: regex_induct)
have qf_not_in_SQ: "qf ∉ NFA.SQ q0 transs"
using Lookahead unfolding IH_def by (auto simp: Let_def)
have qf_not_q0_Suc_q0: "qf ∉ {q0}"
by (auto simp: NFA.SQ_def split: option.splits)
have transs_def: "transs = build_nfa_impl (Lookahead φ) (q0, qf, phis)"
by (auto simp: Let_def IH_def)
interpret base: nfa q0 qf transs
apply unfold_locales
using build_nfa_impl_state_set build_nfa_impl_not_Nil qf_not_in_SQ
unfolding IH_def NFA.Q_def NFA.SQ_def transs_def
by (auto split: option.splits)
define n where "n ≡ case pos φ phis of Some n ⇒ n | _ ⇒ length phis"
then have collect: "n < length (collect_subfmlas (Lookahead φ) phis)"
"(collect_subfmlas (Lookahead φ) phis) ! n = φ"
using pos_sound pos_complete by (force split: option.splits)+
have "⋀cs q. base.step_eps cs q0 q ⟷ n < length cs ∧ cs ! n ∧ q = qf" "⋀cs q. ¬base.step_eps cs qf q"
using base.q0_sub_SQ qf_not_in_SQ
by (auto simp: NFA.step_eps_def transs_def n_def split: option.splits)
then have base_eps: "base.step_eps_closure_set {q0} cs = (if n < length cs ∧ cs ! n then {q0, qf} else {q0})" for cs
using NFA.step_eps_closure_set_unfold[where ?X="{qf}"]
using NFA.step_eps_closure_set_step_id[where ?R="{q0}"]
using NFA.step_eps_closure_set_step_id[where ?R="{qf}"]
by auto
have base_delta: "base.delta {q0} cs = {}" for cs
unfolding NFA.delta_def NFA.step_symb_set_def base_eps
by (auto simp: NFA.step_symb_def NFA.SQ_def transs_def split: option.splits)
show ?case
proof (cases bss)
case Nil
have sat: "n < length bs ∧ bs ! n ⟷ sat φ i"
by (auto simp: Let_def IH_def Nil)
show ?thesis
using qf_not_q0_Suc_q0
unfolding NFA.run_accept_eps_def NFA.run_def NFA.accept_eps_def Nil
by (auto simp: base_eps sat)
next
case bss_def: (Cons cs css)
show ?thesis
using NFA.run_accept_eps_empty
unfolding NFA.run_accept_eps_def NFA.run_def NFA.accept_eps_def bss_def
by (auto simp: bss_def base_delta)
qed
next
case (Symbol φ)
have qf_not_in_SQ: "qf ∉ NFA.SQ q0 transs"
using Symbol unfolding IH_def by (auto simp: Let_def)
have qf_not_q0_Suc_q0: "qf ∉ {q0, Suc q0}"
using Symbol unfolding IH_def
by (auto simp: NFA.SQ_def split: option.splits)
have transs_def: "transs = build_nfa_impl (Symbol φ) (q0, qf, phis)"
using Symbol(1)
by (auto simp: Let_def IH_def)
interpret base: nfa q0 qf transs
apply unfold_locales
using build_nfa_impl_state_set build_nfa_impl_not_Nil qf_not_in_SQ
unfolding IH_def NFA.Q_def NFA.SQ_def transs_def
by (auto split: option.splits)
define n where "n ≡ case pos φ phis of Some n ⇒ n | _ ⇒ length phis"
then have collect: "n < length (collect_subfmlas (Symbol φ) phis)"
"(collect_subfmlas (Symbol φ) phis) ! n = φ"
using pos_sound pos_complete by (force split: option.splits)+
have "⋀cs q. base.step_eps cs q0 q ⟷ n < length cs ∧ cs ! n ∧ q = Suc q0" "⋀cs q. ¬base.step_eps cs (Suc q0) q"
using base.q0_sub_SQ
by (auto simp: NFA.step_eps_def transs_def n_def split: option.splits)
then have base_eps: "base.step_eps_closure_set {q0} cs = (if n < length cs ∧ cs ! n then {q0, Suc q0} else {q0})" for cs
using NFA.step_eps_closure_set_unfold[where ?X="{Suc q0}"]
using NFA.step_eps_closure_set_step_id[where ?R="{q0}"]
using NFA.step_eps_closure_set_step_id[where ?R="{Suc q0}"]
by auto
have base_delta: "base.delta {q0} cs = (if n < length cs ∧ cs ! n then {qf} else {})" for cs
unfolding NFA.delta_def NFA.step_symb_set_def base_eps
by (auto simp: NFA.step_symb_def NFA.SQ_def transs_def split: option.splits)
show ?case
proof (cases bss)
case Nil
show ?thesis
using qf_not_q0_Suc_q0
unfolding NFA.run_accept_eps_def NFA.run_def NFA.accept_eps_def Nil
by (auto simp: base_eps)
next
case bss_def: (Cons cs css)
have sat: "n < length cs ∧ cs ! n ⟷ sat φ i"
using Symbol(1) collect
by (auto simp: Let_def IH_def bss_def)
show ?thesis
proof (cases css)
case Nil
show ?thesis
unfolding NFA.run_accept_eps_def NFA.run_def NFA.accept_eps_def bss_def Nil
by (auto simp: base_delta sat NFA.step_eps_closure_set_def NFA.step_eps_closure_def)
next
case css_def: (Cons ds dss)
have "base.delta {} ds = {}" "base.delta {qf} ds = {}"
using base.step_eps_closure_qf qf_not_in_SQ step_symb_dest
by (fastforce simp: NFA.delta_def NFA.step_eps_closure_set_def NFA.step_symb_set_def)+
then show ?thesis
using NFA.run_accept_eps_empty
unfolding NFA.run_accept_eps_def NFA.run_def NFA.accept_eps_def bss_def css_def
by (auto simp: base_delta)
qed
qed
next
case (Plus r s)
obtain phis' where collect: "collect_subfmlas (Plus r s) phis =
collect_subfmlas r phis @ phis'"
using collect_subfmlas_app by auto
have qf_not_in_SQ: "qf ∉ NFA.SQ q0 (build_nfa_impl (Plus r s) (q0, qf, phis))"
using Plus unfolding IH_def by auto
interpret base: nfa q0 qf "build_nfa_impl (Plus r s) (q0, qf, phis)"
apply unfold_locales
using build_nfa_impl_state_set build_nfa_impl_not_Nil qf_not_in_SQ
unfolding NFA.Q_def NFA.SQ_def build_nfa_impl_state_cnt by fast+
interpret left: nfa "q0 + 1" qf "build_nfa_impl r (q0 + 1, qf, phis)"
apply unfold_locales
using build_nfa_impl_state_set build_nfa_impl_not_Nil qf_not_in_SQ
unfolding NFA.Q_def NFA.SQ_def build_nfa_impl_state_cnt
by fastforce+
interpret right: nfa "q0 + 1 + state_cnt r" qf
"build_nfa_impl s (q0 + 1 + state_cnt r, qf, collect_subfmlas r phis)"
apply unfold_locales
using build_nfa_impl_state_set build_nfa_impl_not_Nil qf_not_in_SQ
unfolding NFA.Q_def NFA.SQ_def build_nfa_impl_state_cnt
by fastforce+
from Plus(3) have "IH r (q0 + 1) qf phis (build_nfa_impl r (q0 + 1, qf, phis)) bss bs i"
unfolding Let_def IH_def collect
using left.qf_not_in_SQ
by (auto simp: nth_append)
then have left_IH: "left.run_accept_eps {q0 + 1} bss bs ⟷
(i, i + length bss) ∈ match r"
using Plus(1) build_nfa_impl_state_cnt
by auto
have "IH s (q0 + 1 + state_cnt r) qf (collect_subfmlas r phis)
(build_nfa_impl s (q0 + 1 + state_cnt r, qf, collect_subfmlas r phis)) bss bs i"
using right.qf_not_in_SQ IH_def Plus
by (auto simp: Let_def)
then have right_IH: "right.run_accept_eps {q0 + 1 + state_cnt r} bss bs ⟷
(i, i + length bss) ∈ match s"
using Plus(2) build_nfa_impl_state_cnt
by auto
interpret cong: nfa_cong_Plus q0 "q0 + 1" "q0 + 1 + state_cnt r" qf qf qf
"build_nfa_impl (Plus r s) (q0, qf, phis)" "build_nfa_impl r (q0 + 1, qf, phis)"
"build_nfa_impl s (q0 + 1 + state_cnt r, qf, collect_subfmlas r phis)"
apply unfold_locales
unfolding NFA.SQ_def build_nfa_impl_state_cnt
NFA.step_eps_def NFA.step_symb_def
by (auto simp add: nth_append build_nfa_impl_state_cnt)
show ?case
using cong.run_accept_eps_cong left_IH right_IH Plus
by (auto simp: Let_def IH_def)
next
case (Times r s)
obtain phis' where collect: "collect_subfmlas (Times r s) phis =
collect_subfmlas r phis @ phis'"
using collect_subfmlas_app by auto
have transs_def: "transs = build_nfa_impl (Times r s) (q0, qf, phis)"
using Times unfolding IH_def by (auto simp: Let_def)
have qf_not_in_SQ: "qf ∉ NFA.SQ q0 (build_nfa_impl (Times r s) (q0, qf, phis))"
using Times unfolding IH_def by auto
interpret base: nfa q0 qf "build_nfa_impl (Times r s) (q0, qf, phis)"
apply unfold_locales
using build_nfa_impl_state_set build_nfa_impl_not_Nil qf_not_in_SQ
unfolding NFA.Q_def NFA.SQ_def build_nfa_impl_state_cnt by fast+
interpret left: nfa "q0" "q0 + state_cnt r" "build_nfa_impl r (q0, q0 + state_cnt r, phis)"
apply unfold_locales
using build_nfa_impl_state_set build_nfa_impl_not_Nil qf_not_in_SQ
unfolding NFA.Q_def NFA.SQ_def build_nfa_impl_state_cnt
by fastforce+
interpret right: nfa "q0 + state_cnt r" qf
"build_nfa_impl s (q0 + state_cnt r, qf, collect_subfmlas r phis)"
apply unfold_locales
using build_nfa_impl_state_set build_nfa_impl_not_Nil qf_not_in_SQ
unfolding NFA.Q_def NFA.SQ_def build_nfa_impl_state_cnt
by fastforce+
from Times(3) have left_IH: "IH r q0 (q0 + state_cnt r) phis
(build_nfa_impl r (q0 , q0 + state_cnt r, phis)) bss bs i"
unfolding Let_def IH_def collect
using left.qf_not_in_SQ
by (auto simp: nth_append)
from Times(3) have left_IH_take: "⋀n. n < length bss ⟹
IH r q0 (q0 + state_cnt r) phis
(build_nfa_impl r (q0, q0 + state_cnt r, phis)) (take n bss) (hd (drop n bss)) i"
unfolding Let_def IH_def collect
using left.qf_not_in_SQ
apply (auto simp: nth_append min_absorb2 hd_drop_conv_nth)
have left_IH_match: "left.run_accept_eps {q0} bss bs ⟷
(i, i + length bss) ∈ match r"
using Times(1) build_nfa_impl_state_cnt left_IH
by auto
have left_IH_match_take: "⋀n. n < length bss ⟹
left.run_accept_eps {q0} (take n bss) (hd (drop n bss)) ⟷ (i, i + n) ∈ match r"
using Times(1) build_nfa_impl_state_cnt left_IH_take
by (fastforce simp add: nth_append min_absorb2)
have "IH s (q0 + state_cnt r) qf (collect_subfmlas r phis)
(build_nfa_impl s (q0 + state_cnt r, qf, collect_subfmlas r phis)) bss bs i"
using right.qf_not_in_SQ IH_def Times
by (auto simp: Let_def)
then have right_IH: "⋀n. n ≤ length bss ⟹ IH s (q0 + state_cnt r) qf (collect_subfmlas r phis)
(build_nfa_impl s (q0 + state_cnt r, qf, collect_subfmlas r phis)) (drop n bss) bs (i + n)"
unfolding Let_def IH_def
by (auto simp: nth_append add.assoc) (meson in_set_dropD)
have right_IH_match: "⋀n. n ≤ length bss ⟹
right.run_accept_eps {q0 + state_cnt r} (drop n bss) bs ⟷ (i + n, i + length bss) ∈ match s"
using Times(2)[OF right_IH] build_nfa_impl_state_cnt
by (auto simp: IH_def)
interpret cong: nfa_cong_Times q0 "q0 + state_cnt r" qf
"build_nfa_impl (Times r s) (q0, qf, phis)"
"build_nfa_impl r (q0, q0 + state_cnt r, phis)"
"build_nfa_impl s (q0 + state_cnt r, qf, collect_subfmlas r phis)"
apply unfold_locales
using NFA.Q_def NFA.SQ_def NFA.step_eps_def NFA.step_symb_def build_nfa_impl_state_set
by (fastforce simp add: nth_append build_nfa_impl_state_cnt build_nfa_impl_not_Nil
state_cnt_pos)+
have right_IH_Nil: "right.run_accept_eps {q0 + state_cnt r} [] bs ⟷
(i + length bss, i + length bss) ∈ match s"
using right_IH_match
by fastforce
show ?case
unfolding match_Times transs_def cong.run_accept_eps_cong left_IH_match right_IH_Nil
using left_IH_match_take right_IH_match less_imp_le_nat le_eq_less_or_eq
by auto
next
case (Star r)
then show ?case
proof (induction "length bss" arbitrary: bss bs i rule: nat_less_induct)
case 1
have transs_def: "transs = build_nfa_impl (Star r) (q0, qf, phis)"
using 1 unfolding IH_def by (auto simp: Let_def)
have qf_not_in_SQ: "qf ∉ NFA.SQ q0 (build_nfa_impl (Star r) (q0, qf, phis))"
using 1 unfolding IH_def by auto
interpret base: nfa q0 qf "build_nfa_impl (Star r) (q0, qf, phis)"
apply unfold_locales
using build_nfa_impl_state_set build_nfa_impl_not_Nil qf_not_in_SQ
unfolding NFA.Q_def NFA.SQ_def build_nfa_impl_state_cnt
by fast+
interpret left: nfa "q0 + 1" q0 "build_nfa_impl r (q0 + 1, q0, phis)"
apply unfold_locales
using build_nfa_impl_state_set build_nfa_impl_not_Nil qf_not_in_SQ
unfolding NFA.Q_def NFA.SQ_def build_nfa_impl_state_cnt
by fastforce+
from 1(3) have left_IH: "IH r (q0 + 1) q0 phis (build_nfa_impl r (q0 + 1, q0, phis)) bss bs i"
using left.qf_not_in_SQ
unfolding Let_def IH_def
from 1(3) have left_IH_take: "⋀n. n < length bss ⟹
IH r (q0 + 1) q0 phis (build_nfa_impl r (q0 + 1, q0, phis)) (take n bss) (hd (drop n bss)) i"
using left.qf_not_in_SQ
unfolding Let_def IH_def
by (auto simp add: nth_append min_absorb2 hd_drop_conv_nth) (meson in_set_takeD)
have left_IH_match: "left.run_accept_eps {q0 + 1} bss bs ⟷
(i, i + length bss) ∈ match r"
using 1(2) left_IH
unfolding build_nfa_impl_state_cnt NFA.SQ_def
by auto
have left_IH_match_take: "⋀n. n < length bss ⟹
left.run_accept_eps {q0 + 1} (take n bss) (hd (drop n bss)) ⟷
(i, i + n) ∈ match r"
using 1(2) left_IH_take
unfolding build_nfa_impl_state_cnt NFA.SQ_def
by (fastforce simp add: nth_append min_absorb2)
interpret cong: nfa_cong_Star q0 "q0 + 1" qf
"build_nfa_impl (Star r) (q0, qf, phis)"
"build_nfa_impl r (q0 + 1, q0, phis)"
apply unfold_locales
unfolding NFA.SQ_def build_nfa_impl_state_cnt NFA.step_eps_def NFA.step_symb_def
by (auto simp add: nth_append build_nfa_impl_state_cnt)
show ?case
using cong.run_accept_eps_Nil
proof (cases bss)
case Nil
show ?thesis
unfolding transs_def Nil
using cong.run_accept_eps_Nil run_Nil run_accept_eps_Nil
by auto
next
case (Cons cs css)
have aux: "⋀n j x P. n < x ⟹ j < x - n ⟹ (∀j < Suc x. P j) ⟹ P (Suc (n + j))"
by auto
from 1(3) have star_IH: "⋀n. n < length css ⟹
IH (Star r) q0 qf phis transs (drop n css) bs (i + n + 1)"
unfolding Cons Let_def IH_def
using aux[of _ _ _ "λj. ∀k<length (collect_subfmlas r phis).
(cs # css) ! j ! k = sat (collect_subfmlas r phis ! k) (i + j)"]
have IH_inst: "⋀xs i. length xs ≤ length css ⟹ IH (Star r) q0 qf phis transs xs bs i ⟶
(base.run_accept_eps {q0} xs bs ⟷ (i, i + length xs) ∈ match (Star r))"
using 1
unfolding Cons
by (auto simp add: nth_append less_Suc_eq_le transs_def)
have "⋀n. n < length css ⟹ base.run_accept_eps {q0} (drop n css) bs ⟷
(i + n + 1, i + length (cs # css)) ∈ match (Star r)"
proof -
fix n
assume assm: "n < length css"
then show "base.run_accept_eps {q0} (drop n css) bs ⟷
(i + n + 1, i + length (cs # css)) ∈ match (Star r)"
using IH_inst[of "drop n css" "i + n + 1"] star_IH
qed
then show ?thesis
using match_Star length_Cons Cons cong.run_accept_eps_cong_Cons
using cong.run_accept_eps_Nil left_IH_match left_IH_match_take
apply (auto simp add: Cons transs_def)
apply (metis Suc_less_eq add_Suc_right drop_Suc_Cons less_imp_le_nat take_Suc_Cons)
apply (metis Suc_less_eq add_Suc_right drop_Suc_Cons le_eq_less_or_eq lessThan_iff
take_Suc_Cons)
done
qed
qed
qed

lemma step_eps_closure_set_empty_list:
assumes "wf_regex r" "IH r q0 qf phis transs bss bs i" "NFA.step_eps_closure q0 transs bs q qf"
shows "NFA.step_eps_closure q0 transs [] q qf"
using assms
proof (induction r arbitrary: q0 qf phis transs q)
case (Symbol φ)
have qf_not_in_SQ: "qf ∉ NFA.SQ q0 transs"
using Symbol unfolding IH_def by (auto simp: Let_def)
have qf_not_q0_Suc_q0: "qf ∉ {q0, Suc q0}"
using Symbol unfolding IH_def
by (auto simp: NFA.SQ_def split: option.splits)
have transs_def: "transs = build_nfa_impl (Symbol φ) (q0, qf, phis)"
using Symbol(2)
by (auto simp: Let_def IH_def)
interpret base: nfa q0 qf transs
apply unfold_locales
using build_nfa_impl_state_set build_nfa_impl_not_Nil qf_not_in_SQ
unfolding IH_def NFA.Q_def NFA.SQ_def transs_def
by (auto split: option.splits)
define n where "n ≡ case pos φ phis of Some n ⇒ n | _ ⇒ length phis"
then have collect: "n < length (collect_subfmlas (Symbol φ) phis)"
"(collect_subfmlas (Symbol φ) phis) ! n = φ"
using pos_sound pos_complete by (force split: option.splits)+
have SQD: "q ∈ NFA.SQ q0 transs ⟹ q = q0 ∨ q = Suc q0" for q
by (auto simp: NFA.SQ_def transs_def split: option.splits)
have "¬base.step_eps cs q qf" if "q ∈ NFA.SQ q0 transs" for cs q
using SQD[OF that] qf_not_q0_Suc_q0
by (auto simp: NFA.step_eps_def transs_def split: option.splits transition.splits)
then show ?case
using Symbol(3)
by (auto simp: NFA.step_eps_closure_def) (metis rtranclp.simps step_eps_dest)
next
case (Plus r s)
have transs_def: "transs = build_nfa_impl (Plus r s) (q0, qf, phis)"
using Plus(4)
by (auto simp: IH_def Let_def)
define ts_l where "ts_l = build_nfa_impl r (q0 + 1, qf, phis)"
define ts_r where "ts_r = build_nfa_impl s (q0 + 1 + state_cnt r, qf, collect_subfmlas r phis)"
have len_ts: "length ts_l = state_cnt r" "length ts_r = state_cnt s" "length transs = Suc (state_cnt r + state_cnt s)"
by (auto simp: ts_l_def ts_r_def transs_def build_nfa_impl_state_cnt)
have transs_eq: "transs = split_trans (q0 + 1) (q0 + 1 + state_cnt r) # ts_l @ ts_r"
by (auto simp: transs_def ts_l_def ts_r_def)
have ts_nonempty: "ts_l = [] ⟹ False" "ts_r = [] ⟹ False"
by (auto simp: ts_l_def ts_r_def build_nfa_impl_not_Nil)
obtain phis' where collect: "collect_subfmlas (Plus r s) phis = collect_subfmlas r phis @ phis'"
using collect_subfmlas_app by auto
have qf_not_in_SQ: "qf ∉ NFA.SQ q0 (build_nfa_impl (Plus r s) (q0, qf, phis))"
using Plus unfolding IH_def by auto
interpret base: nfa q0 qf transs
apply unfold_locales
using build_nfa_impl_state_set build_nfa_impl_not_Nil qf_not_in_SQ
unfolding NFA.Q_def NFA.SQ_def build_nfa_impl_state_cnt transs_def by fast+
interpret left: nfa "Suc q0" qf ts_l
apply unfold_locales
using build_nfa_impl_state_set build_nfa_impl_not_Nil qf_not_in_SQ
unfolding NFA.Q_def NFA.SQ_def build_nfa_impl_state_cnt ts_l_def
by fastforce+
interpret right: nfa "Suc (q0 + state_cnt r)" qf ts_r
apply unfold_locales
using build_nfa_impl_state_set build_nfa_impl_not_Nil qf_not_in_SQ
unfolding NFA.Q_def NFA.SQ_def build_nfa_impl_state_cnt ts_r_def
by fastforce+
interpret cong: nfa_cong_Plus q0 "Suc q0" "Suc (q0 + state_cnt r)" qf qf qf transs ts_l ts_r
apply unfold_locales
unfolding NFA.SQ_def build_nfa_impl_state_cnt
NFA.step_eps_def NFA.step_symb_def transs_def ts_l_def ts_r_def
by (auto simp add: nth_append build_nfa_impl_state_cnt)
have "IH s (Suc (q0 + state_cnt r)) qf (collect_subfmlas r phis) ts_r bss bs i"
using right.qf_not_in_SQ IH_def Plus
by (auto simp: Let_def ts_r_def)
then have case_right: "base.step_eps_closure [] q qf" if "base.step_eps_closure bs q qf" "q ∈ right.Q" for q
using cong.right.eps_nfa'_step_eps_closure[OF that] Plus(2,3) cong.right.nfa'_eps_step_eps_closure[OF _ that(2)]
by auto
from Plus(4) have "IH r (Suc q0) qf phis ts_l bss bs i"
using left.qf_not_in_SQ
unfolding Let_def IH_def collect ts_l_def
by (auto simp: nth_append)
then have case_left: "base.step_eps_closure [] q qf" if "base.step_eps_closure bs q qf" "q ∈ left.Q" for q
using cong.eps_nfa'_step_eps_closure[OF that] Plus(1,3) cong.nfa'_eps_step_eps_closure[OF _ that(2)]
by auto
have "q = q0 ∨ q ∈ left.Q ∨ q ∈ right.Q"
using Plus(5)
by (auto simp: NFA.Q_def NFA.SQ_def len_ts dest!: NFA.step_eps_closure_dest)
moreover have ?case if q_q0: "q = q0"
proof -
have "q0 ≠ qf"
using qf_not_in_SQ
by (auto simp: NFA.SQ_def)
then obtain q' where q'_def: "base.step_eps bs q q'" "base.step_eps_closure bs q' qf"
using Plus(5)
by (auto simp: q_q0 NFA.step_eps_closure_def elim: converse_rtranclpE)
have fst_step_eps: "base.step_eps [] q q'"
using q'_def(1)
by (auto simp: q_q0 NFA.step_eps_def transs_eq)
have "q' ∈ left.Q ∨ q' ∈ right.Q"
using q'_def(1)
by (auto simp: NFA.step_eps_def NFA.Q_def NFA.SQ_def q_q0 transs_eq dest: ts_nonempty split: transition.splits)
then show ?case
using fst_step_eps case_left[OF q'_def(2)] case_right[OF q'_def(2)]
by (auto simp: NFA.step_eps_closure_def)
qed
ultimately show ?case
using Plus(5) case_left case_right
by auto
next
case (Times r s)
obtain phis' where collect: "collect_subfmlas (Times r s) phis =
collect_subfmlas r phis @ phis'"
using collect_subfmlas_app by auto
have transs_def: "transs = build_nfa_impl (Times r s) (q0, qf, phis)"
using Times unfolding IH_def by (auto simp: Let_def)
define ts_l where "ts_l = build_nfa_impl r (q0, q0 + state_cnt r, phis)"
define ts_r where "ts_r = build_nfa_impl s (q0 + state_cnt r, qf, collect_subfmlas r phis)"
have len_ts: "length ts_l = state_cnt r" "length ts_r = state_cnt s" "length transs = state_cnt r + state_cnt s"
by (auto simp: ts_l_def ts_r_def transs_def build_nfa_impl_state_cnt)
have transs_eq: "transs = ts_l @ ts_r"
by (auto simp: transs_def ts_l_def ts_r_def)
have ts_nonempty: "ts_l = [] ⟹ False" "ts_r = [] ⟹ False"
by (auto simp: ts_l_def ts_r_def build_nfa_impl_not_Nil)
have qf_not_in_SQ: "qf ∉ NFA.SQ q0 (build_nfa_impl (Times r s) (q0, qf, phis))"
using Times unfolding IH_def by auto
interpret base: nfa q0 qf transs
apply unfold_locales
using build_nfa_impl_state_set build_nfa_impl_not_Nil qf_not_in_SQ
unfolding NFA.Q_def NFA.SQ_def build_nfa_impl_state_cnt transs_def by fast+
interpret left: nfa "q0" "q0 + state_cnt r" ts_l
apply unfold_locales
using build_nfa_impl_state_set build_nfa_impl_not_Nil qf_not_in_SQ
unfolding NFA.Q_def NFA.SQ_def build_nfa_impl_state_cnt ts_l_def
by fastforce+
interpret right: nfa "q0 + state_cnt r" qf ts_r
apply unfold_locales
using build_nfa_impl_state_set build_nfa_impl_not_Nil qf_not_in_SQ
unfolding NFA.Q_def NFA.SQ_def build_nfa_impl_state_cnt ts_r_def
by fastforce+
interpret cong: nfa_cong_Times q0 "q0 + state_cnt r" qf transs ts_l ts_r
apply unfold_locales
using NFA.Q_def NFA.SQ_def NFA.step_eps_def NFA.step_symb_def build_nfa_impl_state_set
by (auto simp add: nth_append build_nfa_impl_state_cnt build_nfa_impl_not_Nil
state_cnt_pos len_ts transs_eq)
have "qf ∉ base.SQ"
using Times(4)
by (auto simp: IH_def Let_def)
then have qf_left_Q: "qf ∈ left.Q ⟹ False"
by (auto simp: NFA.Q_def NFA.SQ_def len_ts state_cnt_pos)
have left_IH: "IH r q0 (q0 + state_cnt r) phis ts_l bss bs i"
using left.qf_not_in_SQ Times
unfolding Let_def IH_def collect
by (auto simp: nth_append ts_l_def)
have case_left: "base.step_eps_closure [] q (q0 + state_cnt r)" if "left.step_eps_closure bs q (q0 + state_cnt r)" "q ∈ left.Q" and wf: "wf_regex r" for q
using that(1) Times(1)[OF wf left_IH] cong.nfa'_step_eps_closure_cong[OF _ that(2)]
by auto
have left_IH: "IH s (q0 + state_cnt r) qf (collect_subfmlas r phis) ts_r bss bs i"
using right.qf_not_in_SQ IH_def Times
by (auto simp: Let_def ts_r_def)
then have case_right: "base.step_eps_closure [] q qf" if "base.step_eps_closure bs q qf" "q ∈ right.Q" for q
using cong.right.eps_nfa'_step_eps_closure[OF that] Times(2,3) cong.right.nfa'_eps_step_eps_closure[OF _ that(2)]
by auto
have init_right: "q0 + state_cnt r ∈ right.Q"
by (auto simp: NFA.Q_def NFA.SQ_def dest: ts_nonempty)
{
assume q_left_Q: "q ∈ left.Q"
then have split: "left.step_eps_closure bs q (q0 + state_cnt r)" "base.step_eps_closure bs (q0 + state_cnt r) qf"
using cong.eps_nfa'_step_eps_closure_cong[OF Times(5)]
by (auto dest: qf_left_Q)
have empty_IH: "IH s (q0 + state_cnt r) qf (collect_subfmlas r phis) ts_r [] bs (i + length bss)"
using left_IH
by (auto simp: IH_def Let_def ts_r_def)
have "right.step_eps_closure bs (q0 + state_cnt r) qf"
using cong.right.eps_nfa'_step_eps_closure[OF split(2) init_right]
by auto
then have "right.run_accept_eps {q0 + state_cnt r} [] bs"
by (auto simp: NFA.run_accept_eps_def NFA.accept_eps_def NFA.step_eps_closure_set_def NFA.run_def)
then have wf: "wf_regex r"
using nfa_correct[OF empty_IH] Times(3) match_refl_eps
by auto
have ?case
using case_left[OF split(1) q_left_Q wf] case_right[OF split(2) init_right]
by (auto simp: NFA.step_eps_closure_def)
}
moreover have "q ∈ left.Q ∨ q ∈ right.Q"
using Times(5)
by (auto simp: NFA.Q_def NFA.SQ_def transs_eq len_ts dest!: NFA.step_eps_closure_dest)
ultimately show ?case
using case_right[OF Times(5)]
by auto
next
case (Star r)
have transs_def: "transs = build_nfa_impl (Star r) (q0, qf, phis)"
using Star unfolding IH_def by (auto simp: Let_def)
obtain ts_r where ts_r: "transs = split_trans (q0 + 1) qf # ts_r" "ts_r = build_nfa_impl r (Suc q0, q0, phis)"
using Star(3)
by (auto simp: Let_def IH_def)
have qf_not_in_SQ: "qf ∉ NFA.SQ q0 transs"
using Star unfolding IH_def transs_def by auto
interpret base: nfa q0 qf transs
apply unfold_locales
using build_nfa_impl_state_set build_nfa_impl_not_Nil qf_not_in_SQ
unfolding NFA.Q_def NFA.SQ_def build_nfa_impl_state_cnt transs_def
by fast+
interpret left: nfa "Suc q0" q0 ts_r
apply unfold_locales
using build_nfa_impl_state_set build_nfa_impl_not_Nil qf_not_in_SQ
unfolding NFA.Q_def NFA.SQ_def build_nfa_impl_state_cnt ts_r(2)
by fastforce+
interpret cong: nfa_cong_Star q0 "Suc q0" qf transs ts_r
apply unfold_locales
unfolding NFA.SQ_def build_nfa_impl_state_cnt NFA.step_eps_def NFA.step_symb_def
by (auto simp add: nth_append build_nfa_impl_state_cnt ts_r(1))
have IH: "wf_regex r" "IH r (Suc q0) q0 phis ts_r bss bs i"
using Star(2,3)
by (auto simp: Let_def IH_def NFA.SQ_def ts_r(2))
have step_eps_q'_qf: "q' = q0" if "base.step_eps bs q' qf" for q'
proof (rule ccontr)
assume "q' ≠ q0"
then have "q' ∈ left.SQ"
using that
by (auto simp: NFA.step_eps_def NFA.SQ_def ts_r(1))
then have "left.step_eps bs q' qf"
using cong.step_eps_cong_SQ that
by simp
then show "False"
using qf_not_in_SQ
by (metis NFA.Q_def UnE base.q0_sub_SQ cong.SQ_sub left.step_eps_closed subset_eq)
qed
show ?case
proof (cases "q = qf")
case False
then have base_q_q0: "base.step_eps_closure bs q q0" "base.step_eps bs q0 qf"
using Star(4) step_eps_q'_qf
by (auto simp: NFA.step_eps_closure_def) (metis rtranclp.cases)+
have base_Nil_q0_qf: "base.step_eps [] q0 qf"
by (auto simp: NFA.step_eps_def NFA.SQ_def ts_r(1))
have q_left_Q: "q ∈ left.Q"
using base_q_q0
by (auto simp: NFA.Q_def NFA.SQ_def ts_r(1) dest: step_eps_closure_dest)
have "left.step_eps_closure [] q q0"
using cong.eps_nfa'_step_eps_closure_cong[OF base_q_q0(1) q_left_Q] Star(1)[OF IH]
by auto
then show ?thesis
using cong.nfa'_step_eps_closure_cong[OF _ q_left_Q] base_Nil_q0_qf
by (auto simp: NFA.step_eps_closure_def) (meson rtranclp.rtrancl_into_rtrancl)
qed (auto simp: NFA.step_eps_closure_def)
qed auto

lemma accept_eps_iff_accept:
assumes "wf_regex r" "IH r q0 qf phis transs bss bs i"
shows "NFA.accept_eps q0 qf transs R bs = NFA.accept q0 qf transs R"
using step_eps_closure_set_empty_list[OF assms] step_eps_closure_set_mono'
unfolding NFA.accept_eps_def NFA.accept_def
by (fastforce simp: NFA.accept_eps_def NFA.accept_def NFA.step_eps_closure_set_def)

lemma run_accept_eps_iff_run_accept:
assumes "wf_regex r" "IH r q0 qf phis transs bss bs i"
shows "NFA.run_accept_eps q0 qf transs {q0} bss bs ⟷ NFA.run_accept q0 qf transs {q0} bss"
unfolding NFA.run_accept_eps_def NFA.run_accept_def accept_eps_iff_accept[OF assms] ..

end

definition pred_option' :: "('a ⇒ bool) ⇒ 'a option ⇒ bool" where
"pred_option' P z = (case z of Some z' ⇒ P z' | None ⇒ False)"

definition map_option' :: "('b ⇒ 'c option) ⇒ 'b option ⇒ 'c option" where
"map_option' f z = (case z of Some z' ⇒ f z' | None ⇒ None)"

definition while_break :: "('a ⇒ bool) ⇒ ('a ⇒ 'a option) ⇒ 'a ⇒ 'a option" where
"while_break P f x = while (pred_option' P) (map_option' f) (Some x)"

lemma wf_while_break:
assumes "wf {(t, s). P s ∧ b s ∧ Some t = c s}"
shows "wf {(t, s). pred_option P s ∧ pred_option' b s ∧ t = map_option' c s}"
proof -
have sub: "{(t, s). pred_option P s ∧ pred_option' b s ∧ t = map_option' c s} ⊆
map_prod Some Some ` {(t, s). P s ∧ b s ∧ Some t = c s} ∪ ({None} × (Some ` UNIV))"
by (auto simp: pred_option'_def map_option'_def split: option.splits)
(smt (z3) case_prodI map_prod_imageI mem_Collect_eq not_Some_eq)
show ?thesis
apply (rule wf_subset[OF _ sub])
apply (rule wf_union_compatible)
apply (rule wf_map_prod_image)
apply (fastforce simp: wf_def intro: assms)+
done
qed

lemma wf_while_break':
assumes "wf {(t, s). P s ∧ b s ∧ Some t = c s}"
shows "wf {(t, s). pred_option' P s ∧ pred_option' b s ∧ t = map_option' c s}"
by (rule wf_subset[OF wf_while_break[OF assms]]) (auto simp: pred_option'_def split: option.splits)

lemma while_break_sound:
assumes "⋀s s'. P s ⟹ b s ⟹ c s = Some s' ⟹ P s'" "⋀s. P s ⟹ ¬ b s ⟹ Q s" "wf {(t, s). P s ∧ b s ∧ Some t = c s}" "P s"
shows "pred_option Q (while_break b c s)"
proof -
have aux: "P t ⟹ b t ⟹ pred_option P (c t)" for t
using assms(1)
by (cases "c t") auto
show ?thesis
using assms aux
by (auto simp: while_break_def pred_option'_def map_option'_def split: option.splits
intro!: while_rule_lemma[where ?P="pred_option P" and ?Q="pred_option Q" and ?b="pred_option' b" and ?c="map_option' c", OF _ _ wf_while_break])
qed

lemma while_break_complete: "(⋀s. P s ⟹ b s ⟹ pred_option' P (c s)) ⟹ (⋀s. P s ⟹ ¬ b s ⟹ Q s) ⟹ wf {(t, s). P s ∧ b s ∧ Some t = c s} ⟹ P s ⟹
pred_option' Q (while_break b c s)"
unfolding while_break_def
by (rule while_rule_lemma[where ?P="pred_option' P" and ?Q="pred_option' Q" and ?b="pred_option' b" and ?c="map_option' c", OF _ _ wf_while_break'])
(force simp: pred_option'_def map_option'_def split: option.splits elim!: case_optionE)+

context
fixes args :: "(bool iarray, nat set, 'd :: timestamp, 't, 'e) args"
begin

abbreviation "reach_w ≡ reach_window args"

qualified definition "in_win = init_window args"

definition valid_window_matchP :: "'d ℐ ⇒ 't ⇒ 'e ⇒
('d × bool iarray) list ⇒ nat ⇒ (bool iarray, nat set, 'd, 't, 'e) window ⇒ bool" where
"valid_window_matchP I t0 sub rho j w ⟷ j = w_j w ∧
valid_window args t0 sub rho w ∧
reach_w t0 sub rho (w_i w, w_ti w, w_si w, w_j w, w_tj w, w_sj w) ∧
(case w_read_t args (w_tj w) of None ⇒ True
| Some t ⇒ (∀l < w_i w. memL (ts_at rho l) t I))"

lemma valid_window_matchP_reach_tj: "valid_window_matchP I t0 sub rho i w ⟹
reaches_on (w_run_t args) t0 (map fst rho) (w_tj w)"
using reach_window_run_tj
by (fastforce simp: valid_window_matchP_def simp del: reach_window.simps)

lemma valid_window_matchP_reach_sj: "valid_window_matchP I t0 sub rho i w ⟹
reaches_on (w_run_sub args) sub (map snd rho) (w_sj w)"
using reach_window_run_sj
by (fastforce simp: valid_window_matchP_def simp del: reach_window.simps)

lemma valid_window_matchP_len_rho: "valid_window_matchP I t0 sub rho i w ⟹ length rho = i"
by (auto simp: valid_window_matchP_def)

definition "matchP_loop_cond I t = (λw. w_i w < w_j w ∧ memL (the (w_read_t args (w_ti w))) t I)"

definition "matchP_loop_inv I t0 sub rho j0 tj0 sj0 t =
(λw. valid_window args t0 sub rho w ∧
w_j w = j0 ∧ w_tj w = tj0 ∧ w_sj w = sj0 ∧ (∀l < w_i w. memL (ts_at rho l) t I))"

fun ex_key :: "('c, 'd) mmap ⇒ ('d ⇒ bool) ⇒
('c ⇒ bool) ⇒ ('c, bool) mapping ⇒ (bool × ('c, bool) mapping)" where
"ex_key [] time accept ac = (False, ac)"
| "ex_key ((q, t) # qts) time accept ac = (if time t then
(case cac accept ac q of (β, ac') ⇒
if β then (True, ac') else ex_key qts time accept ac')
else ex_key qts time accept ac)"

lemma ex_key_sound:
assumes inv: "⋀q. case Mapping.lookup ac q of None ⇒ True | Some v ⇒ accept q = v"
and distinct: "distinct (map fst qts)"
and eval: "ex_key qts time accept ac = (b, ac')"
shows "b = (∃q ∈ mmap_keys qts. time (the (mmap_lookup qts q)) ∧ accept q) ∧
(∀q. case Mapping.lookup ac' q of None ⇒ True | Some v ⇒ accept q = v)"
using assms
proof (induction qts arbitrary: ac)
case (Cons a qts)
obtain q t where qt_def: "a = (q, t)"
by fastforce
show ?case
proof (cases "time t")
case True
note time_t = True
obtain β ac'' where ac''_def: "cac accept ac q = (β, ac'')"
by fastforce
have accept: "β = accept q" "⋀q. case Mapping.lookup ac'' q of None ⇒ True
| Some v ⇒ accept q = v"
using ac''_def Cons(2)
by (fastforce simp: cac_def Let_def Mapping.lookup_update' split: option.splits if_splits)+
show ?thesis
proof (cases β)
case True
then show ?thesis
using accept(2) time_t Cons(4)
by (auto simp: qt_def mmap_keys_def accept(1) mmap_lookup_def ac''_def)
next
case False
have ex_key: "ex_key qts time accept ac'' = (b, ac')"
using Cons(4) time_t False
by (auto simp: qt_def ac''_def)
show ?thesis
using Cons(1)[OF accept(2) _ ex_key] False[unfolded accept(1)] Cons(3)
by (auto simp: mmap_keys_def mmap_lookup_def qt_def)
qed
next
case False
have ex_key: "ex_key qts time accept ac = (b, ac')"
using Cons(4) False
by (auto simp: qt_def)
show ?thesis
using Cons(1)[OF Cons(2) _ ex_key] False Cons(3)
by (auto simp: mmap_keys_def mmap_lookup_def qt_def)
qed
qed (auto simp: mmap_keys_def)

fun eval_matchP :: "'d ℐ ⇒ (bool iarray, nat set, 'd, 't, 'e) window ⇒
(('d × bool) × (bool iarray, nat set, 'd, 't, 'e) window) option" where
"eval_matchP I w =
(case w_read_t args (w_tj w) of None ⇒ None | Some t ⇒
(case adv_end args w of None ⇒ None | Some w' ⇒
let w'' = while (matchP_loop_cond I t) (adv_start args) w';
(β, ac') = ex_key (w_e w'') (λt'. memR t' t I) (w_accept args) (w_ac w'') in
Some ((t, β), w''⦇w_ac := ac'⦈)))"

definition valid_window_matchF :: "'d ℐ ⇒ 't ⇒ 'e ⇒ ('d × bool iarray) list ⇒ nat ⇒
(bool iarray, nat set, 'd, 't, 'e) window ⇒ bool" where
"valid_window_matchF I t0 sub rho i w ⟷ i = w_i w ∧
valid_window args t0 sub rho w ∧
reach_w t0 sub rho (w_i w, w_ti w, w_si w, w_j w, w_tj w, w_sj w) ∧
(∀l ∈ {w_i w..<w_j w}. memR (ts_at rho i) (ts_at rho l) I)"

lemma valid_window_matchF_reach_tj: "valid_window_matchF I t0 sub rho i w ⟹
reaches_on (w_run_t args) t0 (map fst rho) (w_tj w)"
using reach_window_run_tj
by (fastforce simp: valid_window_matchF_def simp del: reach_window.simps)

lemma valid_window_matchF_reach_sj: "valid_window_matchF I t0 sub rho i w ⟹
reaches_on (w_run_sub args) sub (map snd rho) (w_sj w)"
using reach_window_run_sj
by (fastforce simp: valid_window_matchF_def simp del: reach_window.simps)

definition "matchF_loop_cond I t =
(λw. case w_read_t args (w_tj w) of None ⇒ False | Some t' ⇒ memR t t' I)"

definition "matchF_loop_inv I t0 sub rho i ti si tjm sjm =
(λw. valid_window args t0 sub (take (w_j w) rho) w ∧
w_i w = i ∧ w_ti w = ti ∧ w_si w = si ∧
reach_window args t0 sub rho (w_j w, w_tj w, w_sj w, length rho, tjm, sjm) ∧
(∀l ∈ {w_i w..<w_j w}. memR (ts_at rho i) (ts_at rho l) I))"

definition "matchF_loop_inv' t0 sub rho i ti si j tj sj =
(λw. w_i w = i ∧ w_ti w = ti ∧ w_si w = si ∧
(∃rho'. valid_window args t0 sub (rho @ rho') w ∧
reach_window args t0 sub (rho @ rho') (j, tj, sj, w_j w, w_tj w, w_sj w)))"

fun eval_matchF :: "'d ℐ ⇒ (bool iarray, nat set, 'd, 't, 'e) window ⇒
(('d × bool) × (bool iarray, nat set, 'd, 't, 'e) window) option" where
"eval_matchF I w =
(case w_read_t args (w_ti w) of None ⇒ None | Some t ⇒
(case while_break (matchF_loop_cond I t) (adv_end args) w of None ⇒ None | Some w' ⇒
(case w_read_t args (w_tj w') of None ⇒ None | Some t' ⇒
let β = (case snd (the (mmap_lookup (w_s w') {0})) of None ⇒ False
| Some tstp ⇒ memL t (fst tstp) I) in
Some ((t, β), adv_start args w'))))"

end

locale MDL_window = MDL σ
for σ :: "('a, 'd :: timestamp) trace" +
fixes r :: "('a, 'd :: timestamp) regex"
and t0 :: 't
and sub :: 'e
and args :: "(bool iarray, nat set, 'd, 't, 'e) args"
assumes init_def: "w_init args = {0 :: nat}"
and step_def: "w_step args =
NFA.delta' (IArray (build_nfa_impl r (0, state_cnt r, []))) (state_cnt r)"
and accept_def: "w_accept args = NFA.accept' (IArray (build_nfa_impl r (0, state_cnt r, []))) (state_cnt r)"
and run_t_sound: "reaches_on (w_run_t args) t0 ts t ⟹
w_run_t args t = Some (t', x) ⟹ x = τ σ (length ts)"
and run_sub_sound: "reaches_on (w_run_sub args) sub bs s ⟹
w_run_sub args s = Some (s', b) ⟹
b = IArray (map (λphi. sat phi (length bs)) (collect_subfmlas r []))"
and run_t_read: "w_run_t args t = Some (t', x) ⟹ w_read_t args t = Some x"
and read_t_run: "w_read_t args t = Some x ⟹ ∃t'. w_run_t args t = Some (t', x)"
begin

definition "qf = state_cnt r"
definition "transs = build_nfa_impl r (0, qf, [])"

abbreviation "init ≡ w_init args"
abbreviation "step ≡ w_step args"
abbreviation "accept ≡ w_accept args"
abbreviation "run ≡ NFA.run' (IArray transs) qf"
abbreviation "wacc ≡ Window.acc (w_step args) (w_accept args)"
abbreviation "rw ≡ reach_window args"

abbreviation "valid_matchP ≡ valid_window_matchP args"
abbreviation "eval_mP ≡ eval_matchP args"
abbreviation "matchP_inv ≡ matchP_loop_inv args"
abbreviation "matchP_cond ≡ matchP_loop_cond args"

abbreviation "valid_matchF ≡ valid_window_matchF args"
abbreviation "eval_mF ≡ eval_matchF args"
abbreviation "matchF_inv ≡ matchF_loop_inv args"
abbreviation "matchF_inv' ≡ matchF_loop_inv' args"
abbreviation "matchF_cond ≡ matchF_loop_cond args"

lemma run_t_sound':
assumes "reaches_on (w_run_t args) t0 ts t" "i < length ts"
shows "ts ! i = τ σ i"
proof -
obtain t' t'' where t'_def: "reaches_on (w_run_t args) t0 (take i ts) t'"
"w_run_t args t' = Some (t'', ts ! i)"
using reaches_on_split[OF assms]
by auto
show ?thesis
using run_t_sound[OF t'_def] assms(2)
by simp
qed

lemma run_sub_sound':
assumes "reaches_on (w_run_sub args) sub bs s" "i < length bs"
shows "bs ! i = IArray (map (λphi. sat phi i) (collect_subfmlas r []))"
proof -
obtain s' s'' where s'_def: "reaches_on (w_run_sub args) sub (take i bs) s'"
"w_run_sub args s' = Some (s'', bs ! i)"
using reaches_on_split[OF assms]
by auto
show ?thesis
using run_sub_sound[OF s'_def] assms(2)
by simp
qed

lemma run_ts: "reaches_on (w_run_t args) t ts t' ⟹ t = t0 ⟹ chain_le ts"
proof (induction t ts t' rule: reaches_on_rev_induct)
case (2 s s' v vs s'')
show ?case
proof (cases vs rule: rev_cases)
case (snoc zs z)
show ?thesis
using 2(3)[OF 2(4)]
using chain_le_app[OF _ τ_mono[of "length zs" "Suc (length zs)" σ]]
run_t_sound'[OF reaches_on_app[OF 2(1,2), unfolded 2(4)], of "length zs"]
run_t_sound'[OF reaches_on_app[OF 2(1,2), unfolded 2(4)], of "Suc (length zs)"]
unfolding snoc
by (auto simp: nth_append)
qed (auto intro: chain_le.intros)
qed (auto intro: chain_le.intros)

lemma ts_at_tau: "reaches_on (w_run_t args) t0 (map fst rho) t ⟹ i < length rho ⟹
ts_at rho i = τ σ i"
using run_t_sound'
unfolding ts_at_def
by fastforce

lemma length_bs_at: "reaches_on (w_run_sub args) sub (map snd rho) s ⟹ i < length rho ⟹
IArray.length (bs_at rho i) = length (collect_subfmlas r [])"
using run_sub_sound'
unfolding bs_at_def
by fastforce

lemma bs_at_nth: "reaches_on (w_run_sub args) sub (map snd rho) s ⟹ i < length rho ⟹
n < IArray.length (bs_at rho i) ⟹
IArray.sub (bs_at rho i) n ⟷ sat (collect_subfmlas r [] ! n) i"
using run_sub_sound'
unfolding bs_at_def
by fastforce

lemma ts_at_mono: "⋀i j. reaches_on (w_run_t args) t0 (map fst rho) t ⟹
i ≤ j ⟹ j < length rho ⟹ ts_at rho i ≤ ts_at rho j"
using ts_at_tau
by fastforce

lemma steps_is_run: "steps (w_step args) rho q ij = run q (sub_bs rho ij)"
unfolding NFA.run'_def steps_def step_def transs_def qf_def ..

lemma acc_is_accept: "wacc rho q (i, j) = w_accept args (run q (sub_bs rho (i, j)))"
unfolding acc_def steps_is_run by auto

lemma iarray_list_of: "IArray (IArray.list_of xs) = xs"
by (cases xs) auto

lemma map_iarray_list_of: "map IArray (map IArray.list_of bss) = bss"
using iarray_list_of
by (induction bss) auto

lemma acc_match:
fixes ts :: "'d list"
assumes "reaches_on (w_run_sub args) sub (map snd rho) s" "i ≤ j" "j ≤ length rho" "wf_regex r"
shows "wacc rho {0} (i, j) ⟷ (i, j) ∈ match r"
proof -
have j_eq: "j = i + length (sub_bs rho (i, j))"
using assms by auto
define bs where "bs = map (λphi. sat phi j) (collect_subfmlas r [])"
have IH: "IH r 0 qf [] transs (map IArray.list_of (sub_bs rho (i, j))) bs i"
unfolding IH_def transs_def qf_def NFA.SQ_def build_nfa_impl_state_cnt bs_def
using assms run_sub_sound bs_at_nth length_bs_at by fastforce
interpret NFA_array: nfa_array transs "IArray transs" qf
by unfold_locales (auto simp: qf_def transs_def build_nfa_impl_state_cnt)
have run_run': "NFA_array.run R (map IArray.list_of (sub_bs rho (i, j))) = NFA_array.run' R (sub_bs rho (i, j))" for R
using NFA_array.run'_eq[of "sub_bs rho (i, j)" "map IArray.list_of (sub_bs rho (i, j))"]
unfolding map_iarray_list_of
by auto
show ?thesis
using nfa_correct[OF IH, unfolded NFA.run_accept_def]
unfolding run_accept_eps_iff_run_accept[OF assms(4) IH] acc_is_accept NFA.run_accept_def run_run' NFA_array.accept'_eq
by (simp add: j_eq[symmetric] accept_def assms(2) qf_def transs_def)
qed

lemma accept_match:
fixes ts :: "'d list"
shows "reaches_on (w_run_sub args) sub (map snd rho) s ⟹ i ≤ j ⟹ j ≤ length rho ⟹ wf_regex r ⟹
w_accept args (steps (w_step args) rho {0} (i, j)) ⟷ (i, j) ∈ match r"
using acc_match acc_is_accept steps_is_run
by metis

lemma drop_take_drop: "i ≤ j ⟹ j ≤ length rho ⟹ drop i (take j rho) @ drop j rho = drop i rho"
apply (induction i arbitrary: j rho)
by auto (metis append_take_drop_id diff_add drop_drop drop_take)

lemma take_Suc: "drop n xs = y # ys ⟹ take n xs @ [y] = take (Suc n) xs"
by (metis drop_all list.distinct(1) list.sel(1) not_less take_hd_drop)

lemma valid_init_matchP: "valid_matchP I t0 sub [] 0 (init_window args t0 sub)"
using valid_init_window
by (fastforce simp: valid_window_matchP_def Let_def intro: reaches_on.intros split: option.splits)

lemma valid_init_matchF: "valid_matchF I t0 sub [] 0 (init_window args t0 sub)"
using valid_init_window
by (fastforce simp: valid_window_matchF_def Let_def intro: reaches_on.intros split: option.splits)

lemma valid_eval_matchP:
assumes valid_before': "valid_matchP I t0 sub rho j w"
and before_end: "w_run_t args (w_tj w) = Some (tj''', t)" "w_run_sub args (w_sj w) = Some (sj''', b)"
and wf: "wf_regex r"
shows "∃w'. eval_mP I w = Some ((τ σ j, sat (MatchP I r) j), w') ∧
t = τ σ j ∧ valid_matchP I t0 sub (rho @ [(t, b)]) (Suc j) w'"
proof -
obtain w' where w'_def: "adv_end args w = Some w'"
using before_end
by (fastforce simp: adv_end_def Let_def split: prod.splits)
define st where "st = w_st w'"
define i where "i = w_i w'"
define ti where "ti = w_ti w'"
define si where "si = w_si w'"
define tj where "tj = w_tj w'"
define sj where "sj = w_sj w'"
define s where "s = w_s w'"
define e where "e = w_e w'"
define rho' where "rho' = rho @ [(t, b)]"
have reaches_on': "reaches_on (w_run_t args) t0 (map fst rho') tj'''"
using valid_before' reach_window_run_tj[OF reach_window_app[OF _ before_end]]
by (auto simp: valid_window_matchP_def rho'_def)
have rho_mono: "⋀t'. t' ∈ set (map fst rho) ⟹ t' ≤ t"
using ts_at_mono[OF reaches_on'] nat_less_le
by (fastforce simp: rho'_def ts_at_def nth_append in_set_conv_nth split: list.splits)
have valid_adv_end_w: "valid_window args t0 sub rho' w'"
using valid_before' valid_adv_end[OF _ before_end rho_mono]
by (auto simp: valid_window_matchP_def rho'_def w'_def)
have w_ij_adv_end: "w_i w' = w_i w" "w_j w' = Suc j"
using valid_before' w'_def
by (auto simp: valid_window_matchP_def adv_end_def Let_def before_end split: prod.splits)
have valid_before: "rw t0 sub rho' (i, ti, si, Suc j, tj, sj)"
"⋀i j. i ≤ j ⟹ j < length rho' ⟹ ts_at rho' i ≤ ts_at rho' j"
"∀q. mmap_lookup e q = sup_leadsto init step rho' i (Suc j) q"
"valid_s init step st accept rho' i i (Suc j) s"
"w_j w' = Suc j" "i ≤ Suc j"
unfolding valid_window_def Let_def ti_def si_def i_def tj_def sj_def s_def e_def w_ij_adv_end st_def
by auto
have t_props: "∀l < i. memL (ts_at rho' l) t I"
using valid_before'

note reaches_on_tj = reach_window_run_tj[OF valid_before(1)]
note reaches_on_sj = reach_window_run_sj[OF valid_before(1)]
have length_rho': "length rho' = Suc j" "length rho = j"
using valid_before
by (auto simp: rho'_def)
have j_len_rho': "j < length rho'"
by (auto simp: length_rho')
have tj_eq: "t = τ σ j" "t = ts_at rho' j"
using run_t_sound'[OF reaches_on_tj, of j]
by (auto simp: rho'_def length_rho' nth_append ts_at_def)
have bj_def: "b = bs_at rho' j"
using run_sub_sound'[OF reaches_on_sj, of j]
by (auto simp: rho'_def length_rho' nth_append bs_at_def)
define w'' where loop_def: "w'' = while (matchP_cond I t) (adv_start args) w'"
have inv_before: "matchP_inv I t0 sub rho' (Suc j) tj sj t w'"
unfolding matchP_loop_inv_def
by (auto simp: tj_def sj_def i_def)
have loop: "matchP_inv I t0 sub rho' (Suc j) tj sj t w'' ∧ ¬matchP_cond I t w''"
unfolding loop_def
proof (rule while_rule_lemma[of "matchP_inv I t0 sub rho' (Suc j) tj sj t"])
fix w_cur :: "(bool iarray, nat set, 'd, 't, 'e) window"
assume assms: "matchP_inv I t0 sub rho' (Suc j) tj sj t w_cur" "matchP_cond I t w_cur"
define st_cur where "st_cur = w_st w_cur"
define i_cur where "i_cur = w_i w_cur"
define ti_cur where "ti_cur = w_ti w_cur"
define si_cur where "si_cur = w_si w_cur"
define s_cur where "s_cur = w_s w_cur"
define e_cur where "e_cur = w_e w_cur"
have valid_loop: "rw t0 sub rho' (i_cur, ti_cur, si_cur, Suc j, tj, sj)"
"⋀i j. i ≤ j ⟹ j < length rho' ⟹ ts_at rho' i ≤ ts_at rho' j"
"∀q. mmap_lookup e_cur q = sup_leadsto init step rho' i_cur (Suc j) q"
"valid_s init step st_cur accept rho' i_cur i_cur (Suc j) s_cur"
"w_j w_cur = Suc j"
using assms(1)[unfolded matchP_loop_inv_def valid_window_matchP_def] valid_before(6)
ti_cur_def si_cur_def i_cur_def s_cur_def e_cur_def
by (auto simp: valid_window_def Let_def init_def step_def st_cur_def accept_def
split: option.splits)
obtain ti'_cur si'_cur t_cur b_cur where run_si_cur:
"w_run_t args ti_cur = Some (ti'_cur, t_cur)" "w_run_sub args si_cur = Some (si'_cur, b_cur)"
"t_cur = ts_at rho' i_cur" "b_cur = bs_at rho' i_cur"
using assms(2) reach_window_run_si[OF valid_loop(1)] reach_window_run_ti[OF valid_loop(1)]
unfolding matchP_loop_cond_def valid_loop(5) i_cur_def
by auto
have "⋀l. l < i_cur ⟹ memL (ts_at rho' l) t I"
using assms(1)
unfolding matchP_loop_inv_def i_cur_def
by auto
then have "⋀l. l < Suc (i_cur) ⟹ memL (ts_at rho' l) t I"
using assms(2) run_t_read[OF run_si_cur(1), unfolded run_si_cur(3)]
unfolding matchP_loop_cond_def i_cur_def ti_cur_def
by (auto simp: less_Suc_eq)
then show "matchP_inv I t0 sub rho' (Suc j) tj sj t (adv_start args w_cur)"
unfolding matchP_loop_inv_def matchP_loop_cond_def
by fastforce
next
{
fix w1 w2
assume lassms: "matchP_inv I t0 sub rho' (Suc j) tj sj t w1" "matchP_cond I t w1"
define i_cur where "i_cur = w_i w1"
define ti_cur where "ti_cur = w_ti w1"
define si_cur where "si_cur = w_si w1"
have valid_loop: "rw t0 sub rho' (i_cur, ti_cur, si_cur, Suc j, tj, sj)" "w_j w1 = Suc j"
using lassms(1)[unfolded matchP_loop_inv_def valid_window_matchP_def] valid_before(6)
ti_cur_def si_cur_def i_cur_def
by (auto simp: valid_window_def Let_def)
obtain ti'_cur si'_cur t_cur b_cur where run_si_cur:
"w_run_t args ti_cur = Some (ti'_cur, t_cur)"
"w_run_sub args si_cur = Some (si'_cur, b_cur)"
using lassms(2) reach_window_run_si[OF valid_loop(1)] reach_window_run_ti[OF valid_loop(1)]
unfolding matchP_loop_cond_def valid_loop i_cur_def
by auto
have w1_ij: "w_i w1 < Suc j" "w_j w1 = Suc j"
using lassms
unfolding matchP_loop_inv_def matchP_loop_cond_def
by auto
have w2_ij: "w_i w2 = Suc (w_i w1)" "w_j w2 = Suc j"
using w1_ij lassms(3) run_si_cur(1,2)
unfolding ti_cur_def si_cur_def
by (auto simp: adv_start_def Let_def split: option.splits prod.splits if_splits)
have "w_j w2 - w_i w2 < w_j w1 - w_i w1"
using w1_ij w2_ij
by auto
}
then have "{(s', s). matchP_inv I t0 sub rho' (Suc j) tj sj t s ∧ matchP_cond I t s ∧
s' = adv_start args s} ⊆ measure (λw. w_j w - w_i w)"
by auto
then show "wf {(s', s). matchP_inv I t0 sub rho' (Suc j) tj sj t s ∧ matchP_cond I t s ∧
using wf_measure wf_subset by auto
qed (auto simp: inv_before)
have valid_w': "valid_window args t0 sub rho' w''"
using conjunct1[OF loop]
unfolding matchP_loop_inv_def
by auto
have w_tsj_w': "w_tj w'' = tj" "w_sj w'' = sj" "w_j w'' = Suc j"
using loop
by (auto simp: matchP_loop_inv_def)
define st' where "st' = w_st w''"
define ac where "ac = w_ac w''"
define i' where "i' = w_i w''"
define ti' where "ti' = w_ti w''"
define si' where "si' = w_si w''"
define s' where "s' = w_s w''"
define e' where "e' = w_e w''"
define tj' where "tj' = w_tj w''"
define sj' where "sj' = w_sj w''"
have i'_le_Suc_j: "i' ≤ Suc j"
using loop
unfolding matchP_loop_inv_def
by (auto simp: valid_window_def Let_def i'_def)
have valid_after: "rw t0 sub rho' (i', ti', si', Suc j, tj', sj')"
"⋀i j. i ≤ j ⟹ j < length rho' ⟹ ts_at rho' i ≤ ts_at rho' j"
"distinct (map fst e')"
"∀q. mmap_lookup e' q = sup_leadsto init step rho' i' (Suc j) q"
"⋀q. case Mapping.lookup ac q of None ⇒ True | Some v ⇒ accept q = v"
"valid_s init step st' accept rho' i' i' (Suc j) s'" "i' ≤ Suc j" "Suc j ≤ length rho'"
using valid_w' i'_le_Suc_j
unfolding valid_window_def Let_def i'_def ti'_def si'_def s'_def e'_def tj'_def sj'_def ac_def st'_def w_tsj_w'
by auto
note lookup_e' = valid_after(3,4,5,6)
obtain β ac' where ac'_def: "ex_key e' (λt'. memR t' t I)
(w_accept args) ac = (β, ac')"
by fastforce
have β_def: "β = (∃q∈mmap_keys e'. memR (the (mmap_lookup e' q)) t I ∧ accept q)"
"⋀q. case Mapping.lookup ac' q of None ⇒ True | Some v ⇒ accept q = v"
using ex_key_sound[OF valid_after(5) valid_after(3) ac'_def]
by auto
have i'_set: "⋀l. l < w_i w'' ⟹ memL (ts_at rho' l) (ts_at rho' j) I"
using loop length_rho' i'_le_Suc_j
unfolding matchP_loop_inv_def
by (auto simp: ts_at_def rho'_def nth_append i'_def)
have b_alt: "(∃q ∈ mmap_keys e'. memR (the (mmap_lookup e' q)) t I ∧ accept q) ⟷ sat (MatchP I r) j"
proof (rule iffI)
assume "∃q ∈ mmap_keys e'. memR (the (mmap_lookup e' q)) t I ∧ accept q"
then obtain q where q_def: "q ∈ mmap_keys e'"
"memR (the (mmap_lookup e' q)) t I" "accept q"
by auto
then obtain ts' where ts_def: "mmap_lookup e' q = Some ts'"
by (auto dest: Mapping_keys_dest)
have "sup_leadsto init step rho' i' (Suc j) q = Some ts'"
using lookup_e' ts_def q_def valid_after(4,7,8)
then obtain l where l_def: "l < i'" "steps step rho' init (l,  Suc j) = q"
"ts_at rho' l = ts'"
unfolding i'_def
by fastforce
have l_le_j: "l ≤ j" and l_le_Suc_j: "l ≤ Suc j"
using l_def(1) i'_le_Suc_j
by (auto simp: i'_def)
have tau_l: "l < j ⟹ fst (rho ! l) = τ σ l"
using run_t_sound'[OF reaches_on_tj, of l] length_rho'
by (auto simp: rho'_def nth_append)
have tau_l_left: "memL ts' t I"
unfolding l_def(3)[symmetric] tj_eq(2)
using i'_set l_def(1)
by (auto simp: i'_def)
have "(l, Suc j) ∈ match r"
using accept_match[OF reaches_on_sj l_le_Suc_j _ wf] q_def(3) length_rho' init_def l_def(2)
rho'_def
by auto
then show "sat (MatchP I r) j"
using l_le_j q_def(2) ts_at_tau[OF reaches_on_tj] tau_l_left
by (auto simp: mem_def tj_eq rho'_def ts_def l_def(3)[symmetric] tau_l tj_def ts_at_def
nth_append length_rho' intro: exI[of _ l] split: if_splits)
next
assume "sat (MatchP I r) j"
then obtain l where l_def: "l ≤ j" "l ≤ Suc j" "mem (τ σ l) (τ σ j) I" "(l, Suc j) ∈ match r"
by auto
show "(∃q∈mmap_keys e'. memR (the (mmap_lookup e' q)) t I ∧ accept q)"
proof -
have l_lt_j: "l < Suc j"
using l_def(1) by auto
then have ts_at_l_j: "ts_at rho' l ≤ ts_at rho' j"
using ts_at_mono[OF reaches_on' _ j_len_rho']
by (auto simp: rho'_def length_rho')
have ts_j_l: "memL (ts_at rho' l) (ts_at rho' j) I"
using l_def(3) ts_at_tau[OF reaches_on_tj] l_lt_j length_rho' tj_eq
unfolding rho'_def mem_def
by auto
have "i' = Suc j ∨ ¬memL (ts_at rho' i') (ts_at rho' j) I"
proof (rule Meson.disj_comm, rule disjCI)
assume "i' ≠ Suc j"
then have i'_j: "i' < Suc j"
using valid_after
by auto
obtain t' b' where tbi_cur_def: "w_read_t args ti' = Some t'"
"t' = ts_at rho' i'" "b' = bs_at rho' i'"
using reach_window_run_ti[OF valid_after(1) i'_j]
by auto
show "¬memL (ts_at rho' i') (ts_at rho' j) I"
using loop tbi_cur_def(1) i'_j length_rho'
unfolding matchP_loop_inv_def matchP_loop_cond_def tj_eq(2) ti'_def[symmetric]
by (auto simp: i'_def tbi_cur_def)
qed
then have l_lt_i': "l < i'"
proof (rule disjE)
assume assm: "¬memL (ts_at rho' i') (ts_at rho' j) I"
show "l < i'"
proof (rule ccontr)
assume "¬l < i'"
then have ts_at_i'_l: "ts_at rho' i' ≤ ts_at rho' l"
using ts_at_mono[OF reaches_on'] l_lt_j length_rho'
by (auto simp: rho'_def length_rho')
show False
using assm memL_mono[OF ts_j_l ts_at_i'_l]
by auto
qed
define q where q_def: "q = steps step rho' init (l, Suc j)"
then obtain l' where l'_def: "sup_leadsto init step rho' i' (Suc j) q = Some (ts_at rho' l')"
"l ≤ l'" "l' < i'"