Theory Temporal

theory Temporal
  imports MDL NFA Window
begin

fun state_cnt :: "('a, 'b :: timestamp) regex ⇒ nat" where
  "state_cnt (Lookahead phi) = 1"
| "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)
case (Lookahead φ)
  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}"
    using Lookahead unfolding IH_def
    by (auto simp: NFA.SQ_def split: option.splits)
  have transs_def: "transs = build_nfa_impl (Lookahead φ) (q0, qf, phis)"
    using Lookahead(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 (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"
      using Lookahead(1) collect
      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)
     apply (meson in_set_takeD le_add1 le_trans)
    by (meson le_add1 le_trans nth_mem)
  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
      by (auto simp add: nth_append)
    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)"]
        by (auto simp add: nth_append add.assoc dest: in_set_dropD)
      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
          by (auto simp add: nth_append)
      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"
    using valid_adv_end_w
    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
  note read_t_def = run_t_read[OF before_end(1)]
  have t_props: "∀l < i. memL (ts_at rho' l) t I"
    using valid_before'
    by (auto simp: valid_window_matchP_def i_def w_ij_adv_end read_t_def rho'_def ts_at_def nth_append)

  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'"
    using valid_adv_end_w valid_before t_props
    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)"
      using assms i_cur_def valid_adv_start valid_adv_start_bounds
      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"
        "w2 = adv_start args 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 ∧
      s' = adv_start args 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)
      by (auto simp: rho'_def sup_leadsto_app_cong)
    then obtain l where l_def: "l < i'" "steps step rho' init (l,  Suc j) = q"
      "ts_at rho' l = ts'"
      using sup_leadsto_SomeE[OF i'_le_Suc_j]
      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]
            reach_window_run_si[OF valid_after(1) i'_j] run_t_read
          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
      qed (auto simp add: l_lt_j)
      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'"
        using sup_leadsto_SomeI[OF l_lt_i'] by fastforce
      have ts_j_l': "memR (ts_at rho' l') (ts_at rho' j) I"
      proof -
        have ts_at_l_l': "ts_at rho' l ≤ ts_at rho' l'"
          using ts_at_mono[OF reaches_on' l'_def(2)] l'_def(3) valid_after(4,7,8)
          by (auto simp add: rho'_def length_rho' dual_order.order_iff_strict)
        show ?thesis
          using l_def(3) memR_mono[OF _ ts_at_l_l']
            ts_at_tau[OF reaches_on_tj] l'_def(2,3) valid_after(4,7,8)
          by (auto simp: mem_def rho'_def length_rho')
      qed
      have lookup_e'_q: "mmap_lookup e' q = Some (ts_at rho' l')"
        using lookup_e' l'_def(1