Theory Monitor

theory Monitor
  imports MDL Temporal
begin

type_synonym ('h, 't) time = "('h × 't) option"

datatype (dead 'a, dead 't :: timestamp, dead 'h) vydra_aux =
    VYDRA_None
  | VYDRA_Bool bool 'h
  | VYDRA_Atom 'a 'h
  | VYDRA_Neg "('a, 't, 'h) vydra_aux"
  | VYDRA_Bin "bool ⇒ bool ⇒ bool" "('a, 't, 'h) vydra_aux" "('a, 't, 'h) vydra_aux"
  | VYDRA_Prev "'t ℐ" "('a, 't, 'h) vydra_aux" 'h "('t × bool) option"
  | VYDRA_Next "'t ℐ" "('a, 't, 'h) vydra_aux" 'h "'t option"
  | VYDRA_Since "'t ℐ" "('a, 't, 'h) vydra_aux" "('a, 't, 'h) vydra_aux" "('h, 't) time" nat nat "nat option" "'t option"
  | VYDRA_Until "'t ℐ" "('h, 't) time" "('a, 't, 'h) vydra_aux" "('a, 't, 'h) vydra_aux" "('h, 't) time" nat "('t × bool × bool) option"
  | VYDRA_MatchP "'t ℐ" "transition iarray" nat
    "(bool iarray, nat set, 't, ('h, 't) time, ('a, 't, 'h) vydra_aux list) window"
  | VYDRA_MatchF "'t ℐ" "transition iarray" nat
    "(bool iarray, nat set, 't, ('h, 't) time, ('a, 't, 'h) vydra_aux list) window"

type_synonym ('a, 't, 'h) vydra = "nat × ('a, 't, 'h) vydra_aux"

fun msize_vydra :: "nat ⇒ ('a, 't :: timestamp, 'h) vydra_aux ⇒ nat" where
  "msize_vydra n VYDRA_None = 0"
| "msize_vydra n (VYDRA_Bool b e) = 0"
| "msize_vydra n (VYDRA_Atom a e) = 0"
| "msize_vydra (Suc n) (VYDRA_Bin f v1 v2) = msize_vydra n v1 + msize_vydra n v2 + 1"
| "msize_vydra (Suc n) (VYDRA_Neg v) = msize_vydra n v + 1"
| "msize_vydra (Suc n) (VYDRA_Prev I v e tb) = msize_vydra n v + 1"
| "msize_vydra (Suc n) (VYDRA_Next I v e to) = msize_vydra n v + 1"
| "msize_vydra (Suc n) (VYDRA_Since I vphi vpsi e cphi cpsi cppsi tppsi) = msize_vydra n vphi + msize_vydra n vpsi + 1"
| "msize_vydra (Suc n) (VYDRA_Until I e vphi vpsi epsi c zo) = msize_vydra n vphi + msize_vydra n vpsi + 1"
| "msize_vydra (Suc n) (VYDRA_MatchP I transs qf w) = size_list (msize_vydra n) (w_si w) + size_list (msize_vydra n) (w_sj w) + 1"
| "msize_vydra (Suc n) (VYDRA_MatchF I transs qf w) = size_list (msize_vydra n) (w_si w) + size_list (msize_vydra n) (w_sj w) + 1"
| "msize_vydra _ _ = 0"

fun next_vydra :: "('a, 't :: timestamp, 'h) vydra_aux ⇒ nat" where
  "next_vydra (VYDRA_Next I v e None) = 1"
| "next_vydra _ = 0"

context
  fixes init_hd :: "'h"
    and run_hd :: "'h ⇒ ('h × ('t :: timestamp × 'a set)) option"
begin

definition t0 :: "('h, 't) time" where
  "t0 = (case run_hd init_hd of None ⇒ None | Some (e', (t, X)) ⇒ Some (e', t))"

fun run_t :: "('h, 't) time ⇒ (('h, 't) time × 't) option" where
  "run_t None = None"
| "run_t (Some (e, t)) = (case run_hd e of None ⇒ Some (None, t)
  | Some (e', (t', X)) ⇒ Some (Some (e', t'), t))"

fun read_t :: "('h, 't) time ⇒ 't option" where
  "read_t None = None"
| "read_t (Some (e, t)) = Some t"

lemma run_t_read: "run_t x = Some (x', t) ⟹ read_t x = Some t"
  by (cases x) (auto split: option.splits)

lemma read_t_run: "read_t x = Some t ⟹ ∃x'. run_t x = Some (x', t)"
  by (cases x) (auto split: option.splits)

lemma reach_event_t: "reaches_on run_hd e vs e'' ⟹ run_hd e = Some (e', (t, X)) ⟹
  run_hd e'' = Some (e''', (t', X')) ⟹
  reaches_on run_t (Some (e', t)) (map fst vs) (Some (e''', t'))"
proof (induction e vs e'' arbitrary: t' X' e''' rule: reaches_on_rev_induct)
  case (2 s s' v vs s'')
  obtain v_t v_X where v_def: "v = (v_t, v_X)"
    by (cases v) auto
  have run_t_s'': "run_t (Some (s'', v_t)) = Some (Some (e''', t'), v_t)"
    by (auto simp: 2(5))
  show ?case
    using reaches_on_app[OF 2(3)[OF 2(4) 2(2)[unfolded v_def]] run_t_s'']
    by (auto simp: v_def)
qed (auto intro: reaches_on.intros)

lemma reach_event_t0_t:
  assumes "reaches_on run_hd init_hd vs e''" "run_hd e'' = Some (e''', (t', X'))"
  shows "reaches_on run_t t0 (map fst vs) (Some (e''', t'))"
proof -
  have t0_not_None: "t0 ≠ None"
    apply (rule reaches_on.cases[OF assms(1)])
    using assms(2)
    by (auto simp: t0_def split: option.splits prod.splits)
  then show ?thesis
    using reach_event_t[OF assms(1) _ assms(2)]
    by (auto simp: t0_def split: option.splits)
qed

lemma reaches_on_run_hd_t:
  assumes "reaches_on run_hd init_hd vs e"
  shows "∃x. reaches_on run_t t0 (map fst vs) x"
proof (cases vs rule: rev_cases)
  case (snoc ys y)
  show ?thesis
    using assms
    apply (cases y)
    apply (auto simp: snoc dest!: reaches_on_split_last)
    apply (meson reaches_on_app[OF reach_event_t0_t] read_t.simps(2) read_t_run)
    done
qed (auto intro: reaches_on.intros)

definition "run_subs run = (λvs. let vs' = map run vs in
  (if (∃x ∈ set vs'. Option.is_none x) then None
   else Some (map (fst ∘ the) vs', iarray_of_list (map (snd ∘ snd ∘ the) vs'))))"

lemma run_subs_lD: "run_subs run vs = Some (vs', bs) ⟹
  length vs' = length vs ∧ IArray.length bs = length vs"
  by (auto simp: run_subs_def Let_def iarray_of_list_def split: option.splits if_splits)

lemma run_subs_vD: "run_subs run vs = Some (vs', bs) ⟹ j < length vs ⟹
  ∃vj' tj bj. run (vs ! j) = Some (vj', (tj, bj)) ∧ vs' ! j = vj' ∧ IArray.sub bs j = bj"
  apply (cases "run (vs ! j)")
   apply (auto simp: Option.is_none_def run_subs_def Let_def iarray_of_list_def
      split: option.splits if_splits)
  by (metis image_eqI nth_mem)

fun msize_fmla :: "('a, 'b :: timestamp) formula ⇒ nat"
  and msize_regex :: "('a, 'b) regex ⇒ nat" where
  "msize_fmla (Bool b) = 0"
| "msize_fmla (Atom a) = 0"
| "msize_fmla (Neg phi) = Suc (msize_fmla phi)"
| "msize_fmla (Bin f phi psi) = Suc (msize_fmla phi + msize_fmla psi)"
| "msize_fmla (Prev I phi) = Suc (msize_fmla phi)"
| "msize_fmla (Next I phi) = Suc (msize_fmla phi)"
| "msize_fmla (Since phi I psi) = Suc (max (msize_fmla phi) (msize_fmla psi))"
| "msize_fmla (Until phi I psi) = Suc (max (msize_fmla phi) (msize_fmla psi))"
| "msize_fmla (MatchP I r) = Suc (msize_regex r)"
| "msize_fmla (MatchF I r) = Suc (msize_regex r)"
| "msize_regex (Lookahead phi) = msize_fmla phi"
| "msize_regex (Symbol phi) = msize_fmla phi"
| "msize_regex (Plus r s) = max (msize_regex r) (msize_regex s)"
| "msize_regex (Times r s) = max (msize_regex r) (msize_regex s)"
| "msize_regex (Star r) = msize_regex r"

lemma collect_subfmlas_msize: "x ∈ set (collect_subfmlas r []) ⟹
  msize_fmla x ≤ msize_regex r"
proof (induction r)
  case (Lookahead phi)
  then show ?case
    by (auto split: if_splits)
next
  case (Symbol phi)
  then show ?case
    by (auto split: if_splits)
next
  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

definition "until_ready I t c zo = (case (c, zo) of (Suc _, Some (t', b1, b2)) ⇒ (b2 ∧ memL t t' I) ∨ ¬b1 | _ ⇒ False)"

definition "while_since_cond I t = (λ(vpsi, e, cpsi :: nat, cppsi, tppsi). cpsi > 0 ∧ memL (the (read_t e)) t I)"
definition "while_since_body run =
  (λ(vpsi, e, cpsi :: nat, cppsi, tppsi).
    case run vpsi of Some (vpsi', (t', b')) ⇒
      Some (vpsi', fst (the (run_t e)), cpsi - 1, if b' then Some cpsi else cppsi, if b' then Some t' else tppsi)
      | _ ⇒ None
    )"

definition "while_until_cond I t = (λ(vphi, vpsi, epsi, c, zo). ¬until_ready I t c zo ∧ (case read_t epsi of Some t' ⇒ memR t t' I | None ⇒ False))"
definition "while_until_body run =
  (λ(vphi, vpsi, epsi, c, zo). case run_t epsi of Some (epsi', t') ⇒
    (case run vphi of Some (vphi', (_, b1)) ⇒
      (case run vpsi of Some (vpsi', (_, b2)) ⇒ Some (vphi', vpsi', epsi', Suc c, Some (t', b1, b2))
      | _ ⇒ None)
    | _ ⇒ None))"

function (sequential) run :: "nat ⇒ ('a, 't, 'h) vydra_aux ⇒ (('a, 't, 'h) vydra_aux × ('t × bool)) option" where
  "run n (VYDRA_None) = None"
| "run n (VYDRA_Bool b e) = (case run_hd e of None ⇒ None
    | Some (e', (t, _)) ⇒ Some (VYDRA_Bool b e', (t, b)))"
| "run n (VYDRA_Atom a e) = (case run_hd e of None ⇒ None
    | Some (e', (t, X)) ⇒ Some (VYDRA_Atom a e', (t, a ∈ X)))"
| "run (Suc n) (VYDRA_Neg v) = (case run n v of None ⇒ None
    | Some (v', (t, b)) ⇒ Some (VYDRA_Neg v', (t, ¬b)))"
| "run (Suc n) (VYDRA_Bin f vl vr) = (case run n vl of None ⇒ None
    | Some (vl', (t, bl)) ⇒ (case run n vr of None ⇒ None
    | Some (vr', (_, br)) ⇒ Some (VYDRA_Bin f vl' vr', (t, f bl br))))"
| "run (Suc n) (VYDRA_Prev I v e tb) = (case run_hd e of Some (e', (t, _)) ⇒
        (let β = (case tb of Some (t', b') ⇒ b' ∧ mem t' t I | None ⇒ False) in
        case run n v of Some (v', _, b') ⇒ Some (VYDRA_Prev I v' e' (Some (t, b')), (t, β))
        | None ⇒ Some (VYDRA_None, (t, β)))
    | None ⇒ None)"
| "run (Suc n) (VYDRA_Next I v e to) = (case run_hd e of Some (e', (t, _)) ⇒
    (case to of None ⇒
      (case run n v of Some (v', _, _) ⇒ run (Suc n) (VYDRA_Next I v' e' (Some t))
      | None ⇒ None)
    | Some t' ⇒
      (case run n v of Some (v', _, b) ⇒ Some (VYDRA_Next I v' e' (Some t), (t', b ∧ mem t' t I))
      | None ⇒ if mem t' t I then None else Some (VYDRA_None, (t', False))))
    | None ⇒ None)"
| "run (Suc n) (VYDRA_Since I vphi vpsi e cphi cpsi cppsi tppsi) = (case run n vphi of
    Some (vphi', (t, b1)) ⇒
      let cphi = (if b1 then Suc cphi else 0) in
      let cpsi = Suc cpsi in
      let cppsi = map_option Suc cppsi in
      (case while_break (while_since_cond I t) (while_since_body (run n)) (vpsi, e, cpsi, cppsi, tppsi) of Some (vpsi', e', cpsi', cppsi', tppsi') ⇒
        (let β = (case cppsi' of Some k ⇒ k - 1 ≤ cphi ∧ memR (the tppsi') t I | _ ⇒ False) in
         Some (VYDRA_Since I vphi' vpsi' e' cphi cpsi' cppsi' tppsi', (t, β)))
      | _ ⇒ None)
    | _ ⇒ None)"
| "run (Suc n) (VYDRA_Until I e vphi vpsi epsi c zo) = (case run_t e of Some (e', t) ⇒
      (case while_break (while_until_cond I t) (while_until_body (run n)) (vphi, vpsi, epsi, c, zo) of Some (vphi', vpsi', epsi', c', zo') ⇒
        if c' = 0 then None else
        (case zo' of Some (t', b1, b2) ⇒
          (if b2 ∧ memL t t' I then Some (VYDRA_Until I e' vphi' vpsi' epsi' (c' - 1) zo', (t, True))
          else if ¬b1 then Some (VYDRA_Until I e' vphi' vpsi' epsi' (c' - 1) zo', (t, False))
          else (case read_t epsi' of Some t' ⇒ Some (VYDRA_Until I e' vphi' vpsi' epsi' (c' - 1) zo', (t, False)) | _ ⇒ None))
        | _ ⇒ None)
      | _ ⇒ None)
    | _ ⇒ None)"
| "run (Suc n) (VYDRA_MatchP I transs qf w) =
    (case eval_matchP (init_args ({0}, NFA.delta' transs qf, NFA.accept' transs qf)
      (run_t, read_t) (run_subs (run n))) I w of None ⇒ None
    | Some ((t, b), w') ⇒ Some (VYDRA_MatchP I transs qf w', (t, b)))"
| "run (Suc n) (VYDRA_MatchF I transs qf w) =
    (case eval_matchF (init_args ({0}, NFA.delta' transs qf, NFA.accept' transs qf)
      (run_t, read_t) (run_subs (run n))) I w of None ⇒ None
    | Some ((t, b), w') ⇒ Some (VYDRA_MatchF I transs qf w', (t, b)))"
| "run _ _ = undefined"
  by pat_completeness auto
termination
  by (relation "(λp. size (fst p)) <*mlex*> (λp. next_vydra (snd p)) <*mlex*> (λp. msize_vydra (fst p) (snd p)) <*mlex*> {}") (auto simp: mlex_prod_def)

lemma wf_since: "wf {(t, s). while_since_cond I tt s ∧ Some t = while_since_body (run n) s}"
proof -
  let ?X = "{(t, s). while_since_cond I tt s ∧ Some t = while_since_body (run n) s}"
  have sub: "?X ⊆ measure (λ(vpsi, e, cpsi, cppsi, tppsi). cpsi)"
    by (auto simp: while_since_cond_def while_since_body_def Let_def split: option.splits)
  then show ?thesis
    using wf_subset[OF wf_measure]
    by auto
qed

definition run_vydra :: "('a, 't, 'h) vydra ⇒ (('a, 't, 'h) vydra × ('t × bool)) option" where
  "run_vydra v = (case v of (n, w) ⇒ map_option (apfst (Pair n)) (run n w))"

fun sub :: "nat ⇒ ('a, 't) formula ⇒ ('a, 't, 'h) vydra_aux" where
  "sub n (Bool b) = VYDRA_Bool b init_hd"
| "sub n (Atom a) = VYDRA_Atom a init_hd"
| "sub (Suc n) (Neg phi) = VYDRA_Neg (sub n phi)"
| "sub (Suc n) (Bin f phi psi) = VYDRA_Bin f (sub n phi) (sub n psi)"
| "sub (Suc n) (Prev I phi) = VYDRA_Prev I (sub n phi) init_hd None"
| "sub (Suc n) (Next I phi) = VYDRA_Next I (sub n phi) init_hd None"
| "sub (Suc n) (Since phi I psi) = VYDRA_Since I (sub n phi) (sub n psi) t0 0 0 None None"
| "sub (Suc n) (Until phi I psi) = VYDRA_Until I t0 (sub n phi) (sub n psi) t0 0 None"
| "sub (Suc n) (MatchP I r) = (let qf = state_cnt r;
    transs = iarray_of_list (build_nfa_impl r (0, qf, [])) in
    VYDRA_MatchP I transs qf (init_window (init_args
      ({0}, NFA.delta' transs qf, NFA.accept' transs qf)
      (run_t, read_t) (run_subs (run n)))
      t0 (map (sub n) (collect_subfmlas r []))))"
| "sub (Suc n) (MatchF I r) = (let qf = state_cnt r;
    transs = iarray_of_list (build_nfa_impl r (0, qf, [])) in
    VYDRA_MatchF I transs qf (init_window (init_args
      ({0}, NFA.delta' transs qf, NFA.accept' transs qf)
      (run_t, read_t) (run_subs (run n)))
      t0 (map (sub n) (collect_subfmlas r []))))"
| "sub _ _ = undefined"

definition init_vydra :: "('a, 't) formula ⇒ ('a, 't, 'h) vydra" where
  "init_vydra φ = (let n = msize_fmla φ in (n, sub n φ))"

end

locale VYDRA_MDL = MDL σ
  for σ :: "('a, 't :: timestamp) trace" +
  fixes init_hd :: "'h"
    and run_hd :: "'h ⇒ ('h × ('t × 'a set)) option"
  assumes run_hd_sound: "reaches run_hd init_hd n s ⟹ run_hd s = Some (s', (t, X)) ⟹ (t, X) = (τ σ n, Γ σ n)"
begin

lemma reaches_on_run_hd: "reaches_on run_hd init_hd es s ⟹ run_hd s = Some (s', (t, X)) ⟹ t = τ σ (length es) ∧ X = Γ σ (length es)"
  using run_hd_sound
  by (auto dest: reaches_on_n)

abbreviation "ru_t ≡ run_t run_hd"
abbreviation "l_t0 ≡ t0 init_hd run_hd"
abbreviation "ru ≡ run run_hd"
abbreviation "su ≡ sub init_hd run_hd"

lemma ru_t_event: "reaches_on ru_t t ts t' ⟹ t = l_t0 ⟹ ru_t t' = Some (t'', x) ⟹
  ∃rho e tt. t' = Some (e, tt) ∧ reaches_on run_hd init_hd rho e ∧ length rho = Suc (length ts) ∧
  x = τ σ (length ts)"
proof (induction t ts t' arbitrary: t'' x rule: reaches_on_rev_induct)
  case (1 s)
  show ?case
    using 1 reaches_on_run_hd[OF reaches_on.intros(1)]
    by (auto simp: t0_def split: option.splits intro!: reaches_on.intros)
next
  case (2 s s' v vs s'')
  obtain rho e tt where rho_def: "s' = Some (e, tt)" "reaches_on run_hd init_hd rho e"
    "length rho = Suc (length vs)"
    using 2(3)[OF 2(4,2)]
    by auto
  then show ?case
    using 2(2,5) reaches_on_app[OF rho_def(2)] reaches_on_run_hd[OF rho_def(2)]
    by (fastforce split: option.splits)
qed

lemma ru_t_tau: "reaches_on ru_t l_t0 ts t' ⟹ ru_t t' = Some (t'', x) ⟹ x = τ σ (length ts)"
  using ru_t_event
  by fastforce

lemma ru_t_Some_tau:
  assumes "reaches_on ru_t l_t0 ts (Some (e, t))"
  shows "t = τ σ (length ts)"
proof -
  obtain z where z_def: "ru_t (Some (e, t)) = Some (z, t)"
    by (cases "run_hd e") auto
  show ?thesis
    by (rule ru_t_tau[OF assms z_def])
qed

lemma ru_t_tau_in:
  assumes "reaches_on ru_t l_t0 ts t" "j < length ts"
  shows "ts ! j = τ σ j"
proof -
  obtain t' where t'_def: "reaches_on ru_t l_t0 (take j ts) t'" "reaches_on ru_t t' (drop j ts) t"
    using reaches_on_split'[OF assms(1), where ?i=j] assms(2)
    by auto
  have drop: "drop j ts = ts ! j # tl (drop j ts)"
    using assms(2)
    by (cases "drop j ts") (auto simp add: nth_via_drop)
  obtain t'' where t''_def: "ru_t t' = Some (t'', ts ! j)"
    using t'_def(2) assms(2) drop
    by (auto elim: reaches_on.cases)
  show ?thesis
    using ru_t_event[OF t'_def(1) refl t''_def] assms(2)
    by auto
qed

lemmas run_hd_tau_in = ru_t_tau_in[OF reach_event_t0_t, simplified]

fun last_before :: "(nat ⇒ bool) ⇒ nat ⇒ nat option" where
  "last_before P 0 = None"
| "last_before P (Suc n) = (if P n then Some n else last_before P n)"

lemma last_before_None: "last_before P n = None ⟹ m < n ⟹ ¬P m"
proof (induction P n rule: last_before.induct)
  case (2 P n)
  then show ?case
    by (cases "m = n") (auto split: if_splits)
qed (auto split: if_splits)

lemma last_before_Some: "last_before P n = Some m ⟹ m < n ∧ P m ∧ (∀k ∈ {m<..<n}. ¬P k)"
  apply (induction P n rule: last_before.induct)
   apply (auto split: if_splits)
  apply (metis greaterThanLessThan_iff less_antisym)
  done

inductive wf_vydra :: "('a, 't :: timestamp) formula ⇒ nat ⇒ nat ⇒ ('a, 't, 'h) vydra_aux ⇒ bool" where
  "wf_vydra phi i n w ⟹ ru n w = None ⟹ wf_vydra (Prev I phi) (Suc i) (Suc n) VYDRA_None"
| "wf_vydra phi i n w ⟹ ru n w = None ⟹ wf_vydra (Next I phi) i (Suc n) VYDRA_None"
| "reaches_on run_hd init_hd es sub' ⟹ length es = i ⟹ wf_vydra (Bool b) i n (VYDRA_Bool b sub')"
| "reaches_on run_hd init_hd es sub' ⟹ length es = i ⟹ wf_vydra (Atom a) i n (VYDRA_Atom a sub')"
| "wf_vydra phi i n v ⟹ wf_vydra (Neg phi) i (Suc n) (VYDRA_Neg v)"
| "wf_vydra phi i n v ⟹ wf_vydra psi i n v' ⟹ wf_vydra (Bin f phi psi) i (Suc n) (VYDRA_Bin f v v')"
| "wf_vydra phi i n v ⟹ reaches_on run_hd init_hd es sub' ⟹ length es = i ⟹
   wf_vydra (Prev I phi) i (Suc n) (VYDRA_Prev I v sub' (case i of 0 ⇒ None | Suc j ⇒ Some (τ σ j, sat phi j)))"
| "wf_vydra phi i n v ⟹ reaches_on run_hd init_hd es sub' ⟹ length es = i ⟹
   wf_vydra (Next I phi) (i - 1) (Suc n) (VYDRA_Next I v sub' (case i of 0 ⇒ None | Suc j ⇒ Some (τ σ j)))"
| "wf_vydra phi i n vphi ⟹ wf_vydra psi j n vpsi ⟹ j ≤ i ⟹
   reaches_on ru_t l_t0 es sub' ⟹ length es = j ⟹ (⋀t. t ∈ set es ⟹ memL t (τ σ i) I) ⟹
   cphi = i - (case last_before (λk. ¬sat phi k) i of None ⇒ 0 | Some k ⇒ Suc k) ⟹ cpsi = i - j ⟹
   cppsi = (case last_before (sat psi) j of None ⇒ None | Some k ⇒ Some (i - k)) ⟹
   tppsi = (case last_before (sat psi) j of None ⇒ None | Some k ⇒ Some (τ σ k)) ⟹
   wf_vydra (Since phi I psi) i (Suc n) (VYDRA_Since I vphi vpsi sub' cphi cpsi cppsi tppsi)"
| "wf_vydra phi j n vphi ⟹ wf_vydra psi j n vpsi ⟹ i ≤ j ⟹
   reaches_on ru_t l_t0 es back ⟹ length es = i ⟹
   reaches_on ru_t l_t0 es' front ⟹ length es' = j ⟹ (⋀t. t ∈ set es' ⟹ memR (τ σ i) t I) ⟹
   c = j - i ⟹ z = (case j of 0 ⇒ None | Suc k ⇒ Some (τ σ k, sat phi k, sat psi k)) ⟹
   (⋀k. k ∈ {i..<j - 1} ⟹ sat phi k ∧ (memL (τ σ i) (τ σ k) I ⟶ ¬sat psi k)) ⟹
   wf_vydra (Until phi I psi) i (Suc n) (VYDRA_Until I back vphi vpsi front c z)"
| "valid_window_matchP args I l_t0 (map (su n) (collect_subfmlas r [])) xs i w ⟹
    n ≥ msize_regex r ⟹ qf = state_cnt r ⟹
    transs = iarray_of_list (build_nfa_impl r (0, qf, [])) ⟹
    args = init_args ({0}, NFA.delta' transs qf, NFA.accept' transs qf)
      (ru_t, read_t) (run_subs (ru n)) ⟹
    wf_vydra (MatchP I r) i (Suc n) (VYDRA_MatchP I transs qf w)"
| "valid_window_matchF args I l_t0 (map (su n) (collect_subfmlas r [])) xs i w ⟹
    n ≥ msize_regex r ⟹ qf = state_cnt r ⟹
    transs = iarray_of_list (build_nfa_impl r (0, qf, [])) ⟹
    args = init_args ({0}, NFA.delta' transs qf, NFA.accept' transs qf)
      (ru_t, read_t) (run_subs (ru n)) ⟹
    wf_vydra (MatchF I r) i (Suc n) (VYDRA_MatchF I transs qf w)"

lemma reach_run_subs_len:
  assumes reaches_ons: "reaches_on (run_subs (ru n)) (map (su n) (collect_subfmlas r [])) rho vs"
  shows "length vs = length (collect_subfmlas r [])"
  using reaches_ons run_subs_lD
  by (induction "map (su n) (collect_subfmlas r [])" rho vs rule: reaches_on_rev_induct) fastforce+

lemma reach_run_subs_run:
  assumes reaches_ons: "reaches_on (run_subs (ru n)) (map (su n) (collect_subfmlas r [])) rho vs"
    and subfmla: "j < length (collect_subfmlas r [])" "phi = collect_subfmlas r [] ! j"
  shows "∃rho'. reaches_on (ru n) (su n phi) rho' (vs ! j) ∧ length rho' = length rho"
  using reaches_ons subfmla
proof (induction "map (su n) (collect_subfmlas r [])" rho vs rule: reaches_on_rev_induct)
  case 1
  then show ?case
    by (auto intro: reaches_on.intros)
next
  case (2 s' v vs' s'')
  note len_s'_vs = reach_run_subs_len[OF 2(1)]
  obtain rho' where reach_s'_vs: "reaches_on (ru n) (su n phi) rho' (s' ! j)"
    "length rho' = length vs'"
    using 2(2)[OF 2(4,5)]
    by auto
  note run_subslD = run_subs_lD[OF 2(3)]
  note run_subsvD = run_subs_vD[OF 2(3) 2(4)[unfolded len_s'_vs[symmetric]]]
  obtain vj' tj bj where vj'_def: "ru n (s' ! j) = Some (vj', tj, bj)"
    "s'' ! j = vj'" "IArray.sub v j = bj"
    using run_subsvD by auto
  obtain rho'' where rho''_def: "reaches_on (ru n) (su n phi) rho'' (s'' ! j)"
    "length rho'' = Suc (length vs')"
    using reaches_on_app[OF reach_s'_vs(1) vj'_def(1)] vj'_def(2) reach_s'_vs(2)
    by auto
  then show ?case
    using conjunct1[OF run_subslD, unfolded len_s'_vs[symmetric]]
    by auto
qed

lemma IArray_nth_equalityI: "IArray.length xs = length ys ⟹
  (⋀i. i < IArray.length xs ⟹ IArray.sub xs i = ys ! i) ⟹ xs = IArray ys"
  by (induction xs arbitrary: ys) (auto intro: nth_equalityI)

lemma bs_sat:
  assumes IH: "⋀phi i v v' b. phi ∈ set (collect_subfmlas r []) ⟹ wf_vydra phi i n v ⟹ ru n v = Some (v', b) ⟹ snd b = sat phi i"
    and reaches_ons: "⋀j. j < length (collect_subfmlas r []) ⟹ wf_vydra (collect_subfmlas r [] ! j) i n (vs ! j)"
    and run_subs: "run_subs (ru n) vs = Some (vs', bs)" "length vs = length (collect_subfmlas r [])"
  shows "bs = iarray_of_list (map (λphi. sat phi i) (collect_subfmlas r []))"
proof -
  have "⋀j. j < length (collect_subfmlas r []) ⟹
    IArray.sub bs j = sat (collect_subfmlas r [] ! j) i"
  proof -
    fix j
    assume lassm: "j < length (collect_subfmlas r [])"
    define phi where "phi = collect_subfmlas r [] ! j"
    have phi_in_set: "phi ∈ set (collect_subfmlas r [])"
      using lassm
      by (auto simp: phi_def)
    have wf: "wf_vydra phi i n (vs ! j)"
      using reaches_ons lassm phi_def
      by metis
    show "IArray.sub bs j = sat (collect_subfmlas r [] ! j) i"
      using IH(1)[OF phi_in_set wf] run_subs_vD[OF run_subs(1) lassm[folded run_subs(2)]]
      unfolding phi_def[symmetric]
      by auto
  qed
  moreover have "length (IArray.list_of bs) = length vs"
    using run_subs(1)
    by (auto simp: run_subs_def Let_def iarray_of_list_def split: if_splits)
  ultimately show ?thesis
    using run_subs(2)
    by (auto simp: iarray_of_list_def intro!: IArray_nth_equalityI)
qed

lemma run_induct[case_names Bool Atom Neg Bin Prev Next Since Until MatchP MatchF, consumes 1]:
  fixes phi :: "('a, 't) formula"
  assumes "msize_fmla phi ≤ n" "(⋀b n. P n (Bool b))" "(⋀a n. P n (Atom a))"
    "(⋀n phi. msize_fmla phi ≤ n ⟹ P n phi ⟹ P (Suc n) (Neg phi))"
    "(⋀n f phi psi. msize_fmla (Bin f phi psi) ≤ Suc n ⟹ P n phi ⟹ P n psi ⟹
      P (Suc n) (Bin f phi psi))"
    "(⋀n I phi. msize_fmla phi ≤ n ⟹ P n phi ⟹ P (Suc n) (Prev I phi))"
    "(⋀n I phi. msize_fmla phi ≤ n ⟹ P n phi ⟹ P (Suc n) (Next I phi))"
    "(⋀n I phi psi. msize_fmla phi ≤ n ⟹ msize_fmla psi ≤ n ⟹ P n phi ⟹ P n psi ⟹ P (Suc n) (Since phi I psi))"
    "(⋀n I phi psi. msize_fmla phi ≤ n ⟹ msize_fmla psi ≤ n ⟹ P n phi ⟹ P n psi ⟹ P (Suc n) (Until phi I psi))"
    "(⋀n I r. msize_fmla (MatchP I r) ≤ Suc n ⟹ (⋀x. msize_fmla x ≤ n ⟹ P n x) ⟹
      P (Suc n) (MatchP I r))"
    "(⋀n I r. msize_fmla (MatchF I r) ≤ Suc n ⟹ (⋀x. msize_fmla x ≤ n ⟹ P n x) ⟹
      P (Suc n) (MatchF I r))"
  shows "P n phi"
  using assms(1)
proof (induction n arbitrary: phi rule: nat_less_induct)
  case (1 n)
  show ?case
  proof (cases n)
    case 0
    show ?thesis
      using 1 assms(2-)
      by (cases phi) (auto simp: 0)
  next
    case (Suc m)
    show ?thesis
      using 1 assms(2-)
      by (cases phi) (auto simp: Suc)
  qed
qed

lemma wf_vydra_sub: "msize_fmla φ ≤ n ⟹ wf_vydra φ 0 n (su n φ)"
proof (induction n φ rule: run_induct)
  case (Prev n I phi)
  then show ?case
    using wf_vydra.intros(7)[where ?i=0, OF _ reaches_on.intros(1)]
    by auto
next
  case (Next n I phi)
  then show ?case
    using wf_vydra.intros(8)[where ?i=0, OF _ reaches_on.intros(1)]
    by auto
next
  case (MatchP n I r)
  let ?qf = "state_cnt r"
  let ?transs = "iarray_of_list (build_nfa_impl r (0, ?qf, []))"
  let ?args = "init_args ({0}, NFA.delta' ?transs ?qf, NFA.accept' ?transs ?qf) (ru_t, read_t) (run_subs (ru n))"
  show ?case
    using MatchP valid_init_window[of ?args l_t0 "map (su n) (collect_subfmlas r [])", simplified]
    by (auto simp: Let_def valid_window_matchP_def split: option.splits intro: reaches_on.intros
        intro!: wf_vydra.intros(11)[where ?xs="[]", OF _ _ refl refl refl])
next
  case (MatchF n I r)
  let ?qf = "state_cnt r"
  let ?transs = "iarray_of_list (build_nfa_impl r (0, ?qf, []))"
  let ?args = "init_args ({0}, NFA.delta' ?transs ?qf, NFA.accept' ?transs ?qf) (ru_t, read_t) (run_subs (ru n))"
  show ?case
    using MatchF valid_init_window[of ?args l_t0 "map (su n) (collect_subfmlas r [])", simplified]
    by (auto simp: Let_def valid_window_matchF_def split: option.splits intro: reaches_on.intros
        intro!: wf_vydra.intros(12)[where ?xs="[]", OF _ _ refl refl refl])
qed (auto simp: Let_def intro: wf_vydra.intros reaches_on.intros)

lemma ru_t_Some: "∃e' et. ru_t e = Some (e', et)" if reaches_Suc_i: "reaches_on run_hd init_hd fs f" "length fs = Suc i"
  and aux: "reaches_on ru_t l_t0 es e" "length es ≤ i" for es e
proof -
  obtain fs' ft where ft_def: "reaches_on ru_t l_t0 (map fst (fs' :: ('t × 'a set) list)) (Some (f, ft))"
    "map fst fs = map fst fs' @ [ft]" "length fs' = i"
    using reaches_Suc_i
    by (cases fs rule: rev_cases) (auto dest!: reaches_on_split_last reach_event_t0_t)
  show ?thesis
  proof (cases "length es = i")
    case True
    have e_def: "e = Some (f, ft)"
      using reaches_on_inj[OF aux(1) ft_def(1)]
      by (auto simp: True ft_def(3))
    then show ?thesis
      by (cases "run_hd f") (auto simp: e_def)
  next
    case False
    obtain s' s'' where split: "reaches_on ru_t l_t0 (take (length es) (map fst fs')) s'"
      "ru_t s' = Some (s'', map fst fs' ! (length es))"
      using reaches_on_split[OF ft_def(1), where ?i="length es"] False aux(2)
      by (auto simp: ft_def(3))
    show ?thesis
      using reaches_on_inj[OF aux(1) split(1)] aux(2)
      by (auto simp: ft_def(3) split(2))
  qed
qed

lemma vydra_sound_aux:
  assumes "msize_fmla φ ≤ n" "wf_vydra φ i n v" "ru n v = Some (v', t, b)" "bounded_future_fmla φ" "wf_fmla φ"
  shows "wf_vydra φ (Suc i) n v' ∧ (∃es e. reaches_on run_hd init_hd es e ∧ length es = Suc i) ∧ t = τ σ i ∧ b = sat φ i"
  using assms
proof (induction n φ arbitrary: i v v' t b rule: run_induct)
  case (Bool β n)
  then show ?case
    using reaches_on_run_hd reaches_on_app wf_vydra.intros(3)[OF reaches_on_app refl]
    by (fastforce elim!: wf_vydra.cases[of _ _ _ "v"] split: option.splits)
next
  case (Atom a n)
  then show ?case
    using reaches_on_run_hd reaches_on_app wf_vydra.intros(4)[OF reaches_on_app refl]
    by (fastforce elim!: wf_vydra.cases[of _ _ _ v] split: option.splits)
next
  case (Neg n x)
  have IH: "wf_vydra x i n v ⟹ ru n v = Some (v', t, b) ⟹ wf_vydra x (Suc i) n v' ∧ (∃es e. reaches_on run_hd init_hd es e ∧ length es = Suc i) ∧ t = τ σ i ∧ b = sat x i" for v v' t b
    using Neg(2,5,6)
    by auto
  show ?case
    apply (rule wf_vydra.cases[OF Neg(3)])
    using Neg(4) IH wf_vydra.intros(5)
    by (fastforce split: option.splits)+
next
  case (Bin n f x1 x2)
  have IH1: "wf_vydra x1 i n v ⟹ ru n v = Some (v', t, b) ⟹ wf_vydra x1 (Suc i) n v' ∧ (∃es e. reaches_on run_hd init_hd es e ∧ length es = Suc i) ∧ t = τ σ i ∧ b = sat x1 i" for v v' t b
    using Bin(2,6,7)
    by auto
  have IH2: "wf_vydra x2 i n v ⟹ ru n v = Some (v', t, b) ⟹ wf_vydra x2 (Suc i) n v' ∧ t = τ σ i ∧ b = sat x2 i" for v v' t b
    using Bin(3,6,7)
    by auto
  show ?case
    apply (rule wf_vydra.cases[OF Bin(4)])
    using Bin(5) IH1 IH2 wf_vydra.intros(6)
    by (fastforce split: option.splits)+
next
  case (Prev n I phi)
  show ?case
  proof (cases i)
    case 0
    then show ?thesis
      using Prev run_hd_sound[OF reaches.intros(1)] wf_vydra.intros(7)[OF _ reaches_on.intros(2)[OF _ reaches_on.intros(1)], where ?i="Suc 0", simplified]
      by (fastforce split: nat.splits option.splits dest!: reaches_on_NilD elim!: wf_vydra.cases[of _ _ _ v] intro: wf_vydra.intros(1) reaches_on.intros(2)[OF _ reaches_on.intros(1)])
  next
    case (Suc j)
    obtain vphi es sub where v_def: "v = VYDRA_Prev I vphi sub (Some (τ σ j, sat phi j))"
      "wf_vydra phi i n vphi" "reaches_on run_hd init_hd es sub" "length es = i"
      using Prev(3,4)
      by (auto simp: Suc elim!: wf_vydra.cases[of _ _ _ v])
    obtain sub' X where run_sub: "run_hd sub = Some (sub', (t, X))"
      using Prev(4)
      by (auto simp: v_def(1) Let_def split: option.splits)
    note reaches_sub' = reaches_on_app[OF v_def(3) run_sub]
    have t_def: "t = τ σ (Suc j)"
      using reaches_on_run_hd[OF v_def(3) run_sub]
      by (auto simp: Suc v_def(2,4))
    show ?thesis
    proof (cases "v' = VYDRA_None")
      case v'_def: True
      show ?thesis
        using Prev(4) v_def(2) reaches_sub'
        by (auto simp: Suc Let_def v_def(1,4) v'_def run_sub t_def split: option.splits intro: wf_vydra.intros(1))
    next
      case False
      obtain vphi' where ru_vphi: "ru n vphi = Some (vphi', (τ σ i, sat phi i))"
        using Prev(2)[OF v_def(2)] Prev(4,5,6) False
        by (auto simp: v_def(1) Let_def split: option.splits)
      have wf': "wf_vydra phi (Suc (Suc j)) n vphi'"
        using Prev(2)[OF v_def(2) ru_vphi] Prev(5,6)
        by (auto simp: Suc)
      show ?thesis
        using Prev(4) wf_vydra.intros(7)[OF wf' reaches_sub'] reaches_sub'
        by (auto simp: Let_def Suc t_def v_def(1,4) run_sub ru_vphi)
    qed
  qed
next
  case (Next n I phi)
  obtain w sub to es where v_def: "v = VYDRA_Next I w sub to" "wf_vydra phi (length es) n w"
    "reaches_on run_hd init_hd es sub" "length es = (case to of None ⇒ 0 | _ ⇒ Suc i)"
    "case to of None ⇒ i = 0 | Some told ⇒ told = τ σ i"
    using Next(3,4)
    by (auto elim!: wf_vydra.cases[of _ _ _ v] split: option.splits nat.splits)
  obtain sub' tnew X where run_sub: "run_hd sub = Some (sub', (tnew, X))"
    using Next(4)
    by (auto simp: v_def(1) split: option.splits)
  have tnew_def: "tnew = τ σ (length es)"
    using reaches_on_run_hd[OF v_def(3) run_sub]
    by auto
  have aux: ?case if aux_assms: "wf_vydra phi (Suc i) n w"
    "ru (Suc n) (VYDRA_Next I w sub (Some t0)) = Some (v', t, b)"
    "reaches_on run_hd init_hd es sub" "length es = Suc i" "t0 = τ σ i" for w sub t0 es
    using aux_assms(1,2,5) wf_vydra.intros(2)[OF aux_assms(1)]
      Next(2)[where ?i="Suc i" and ?v="w"] Next(5,6) reaches_on_run_hd[OF aux_assms(3)]
      wf_vydra.intros(8)[OF _ reaches_on_app[OF aux_assms(3)], where ?phi=phi and ?i="Suc (Suc i)" and ?n="n"] aux_assms(3)
    by (auto simp: run_sub aux_assms(4,5) split: option.splits if_splits)
  show ?case
  proof (cases to)
    case None
    obtain w' z where w_def: "ru (Suc n) v = ru (Suc n) (VYDRA_Next I w' sub' (Some tnew))"
      "ru n w = Some (w', z)"
      using Next(4)
      by (cases "ru n w") (auto simp: v_def(1) run_sub None split: option.splits)
    have wf: "wf_vydra phi (Suc i) n w'"
      using v_def w_def(2) Next(2,5,6)
      by (cases z) (auto simp: None intro: wf_vydra.intros(1))
    show ?thesis
      using aux[OF wf Next(4)[unfolded w_def(1)] reaches_on_app[OF v_def(3) run_sub]] v_def(4,5) tnew_def
      by (auto simp: None)
  next
    case (Some z)
    show ?thesis
      using aux[OF _ _ v_def(3), where ?w="w"] v_def(2,4,5) Next(4)
      by (auto simp: v_def(1) Some simp del: run.simps)
  qed
next
  case (Since n I phi psi)
  obtain vphi vpsi e cphi cpsi cppsi tppsi j es where v_def:
    "v = VYDRA_Since I vphi vpsi e cphi cpsi cppsi tppsi"
    "wf_vydra phi i n vphi" "wf_vydra psi j n vpsi" "j ≤ i"
    "reaches_on ru_t l_t0 es e" "length es = j" "⋀t. t ∈ set es ⟹ memL t (τ σ i) I"
    "cphi = i - (case last_before (λk. ¬sat phi k) i of None ⇒ 0 | Some k ⇒ Suc k)" "cpsi = i - j"
    "cppsi = (case last_before (sat psi) j of None ⇒ None | Some k ⇒ Some (i - k))"
    "tppsi = (case last_before (sat psi) j of None ⇒ None | Some k ⇒ Some (τ σ k))"
    using Since(5)
    by (auto elim: wf_vydra.cases)
  obtain vphi' b1 where run_vphi: "ru n vphi = Some (vphi', t, b1)"
    using Since(6)
    by (auto simp: v_def(1) Let_def split: option.splits)
  obtain fs f where wf_vphi': "wf_vydra phi (Suc i) n vphi'"
    and reaches_Suc_i: "reaches_on run_hd init_hd fs f" "length fs = Suc i"
    and t_def: "t = τ σ i" and b1_def: "b1 = sat phi i"
    using Since(3)[OF v_def(2) run_vphi] Since(7,8)
    by auto
  note ru_t_Some = ru_t_Some[OF reaches_Suc_i]
  define loop_inv where "loop_inv = (λ(vpsi, e, cpsi :: nat, cppsi, tppsi).
    let j = Suc i - cpsi in cpsi ≤ Suc i ∧
    wf_vydra psi j n vpsi ∧ (∃es. reaches_on ru_t l_t0 es e ∧ length es = j ∧ (∀t ∈ set es. memL t (τ σ i) I)) ∧
    cppsi = (case last_before (sat psi) j of None ⇒ None | Some k ⇒ Some (Suc i - k)) ∧
    tppsi = (case last_before (sat psi) j of None ⇒ None | Some k ⇒ Some (τ σ k)))"
  define loop_init where "loop_init = (vpsi, e, Suc cpsi, map_option Suc cppsi, tppsi)"
  obtain vpsi' e' cpsi' cppsi' tppsi' where loop_def: "while_break (while_since_cond I t) (while_since_body run_hd (ru n)) loop_init =
    Some (vpsi', e', cpsi', cppsi', tppsi')"
    using Since(6)
    by (auto simp: v_def(1) run_vphi loop_init_def Let_def split: option.splits)
  have j_def: "j = i - cpsi"
    using v_def(4,9)
    by auto
  have "cpsi ≤ i"
    using v_def(9)
    by auto
  then have loop_inv_init: "loop_inv loop_init"
    using v_def(3,5,6,7,10,11) last_before_Some
    by (fastforce simp: loop_inv_def loop_init_def Let_def j_def split: option.splits)
  have wf_loop: "wf {(s', s). loop_inv s ∧ while_since_cond I t s ∧ Some s' = while_since_body run_hd (ru n) s}"
    by (auto intro: wf_subset[OF wf_since])
  have step_loop: "loop_inv s'" if loop_assms: "loop_inv s" "while_since_cond I t s" "while_since_body run_hd (ru n) s = Some s'" for s s'
  proof -
    obtain vpsi e cpsi cppsi tppsi where s_def: "s = (vpsi, e, cpsi, cppsi, tppsi)"
      by (cases s) auto
    define j where "j = Suc i - cpsi"
    obtain es where loop_before: "cpsi ≤ Suc i" "wf_vydra psi j n vpsi"
      "reaches_on ru_t l_t0 es e" "length es = j" "⋀t. t ∈ set es ⟹ memL t (τ σ i) I"
      "cppsi = (case last_before (sat psi) j of None ⇒ None | Some k ⇒ Some (Suc i - k))"
      "tppsi = (case last_before (sat psi) j of None ⇒ None | Some k ⇒ Some (τ σ k))"
      using loop_assms(1)
      by (auto simp: s_def j_def loop_inv_def Let_def)
    obtain tt h where tt_def: "read_t e = Some tt" "memL tt t I" "e = Some (h, tt)"
      using ru_t_Some[OF loop_before(3)] loop_before(4) loop_assms(2)
      by (cases e) (fastforce simp: while_since_cond_def s_def j_def split: option.splits)+
    obtain e' where e'_def: "reaches_on ru_t l_t0 (es @ [tt]) e'" "ru_t e = Some (e', tt)"
      using reaches_on_app[OF loop_before(3)] tt_def(1)
      by (cases "run_hd h") (auto simp: tt_def(3))
    obtain vpsi' t' b' where run_vpsi: "ru n vpsi = Some (vpsi', (t', b'))"
      using loop_assms(3)
      by (auto simp: while_since_body_def s_def Let_def split: option.splits)
    have wf_psi': "wf_vydra psi (Suc j) n vpsi'" and t'_def: "t' = τ σ j" and b'_def: "b' = sat psi j"
      using Since(4)[OF loop_before(2) run_vpsi] Since(7,8)
      by auto
    define j' where j'_def: "j' = Suc i - (cpsi - Suc 0)"
    have cpsi_pos: "cpsi > 0"
      using loop_assms(2)
      by (auto simp: while_since_cond_def s_def)
    have j'_j: "j' = Suc j"
      using loop_before(1) cpsi_pos
      by (auto simp: j'_def j_def)
    define cppsi' where "cppsi' = (if b' then Some cpsi else cppsi)"
    define tppsi' where "tppsi' = (if b' then Some t' else tppsi)"
    have cppsi': "cppsi' = (case last_before (sat psi) j' of None ⇒ None | Some k ⇒ Some (Suc i - k))"
      using cpsi_pos loop_before(1)
      by (auto simp: cppsi'_def b'_def j'_j loop_before(6) j_def)
    have tppsi': "tppsi' = (case last_before (sat psi) j' of None ⇒ None | Some k ⇒ Some (τ σ k))"
      by (auto simp: tppsi'_def t'_def b'_def j'_j loop_before(7) split: option.splits)
    have s'_def: "s' = (vpsi', fst (the (ru_t e)), cpsi - Suc 0, cppsi', tppsi')"
      using loop_assms(3)
      by (auto simp: while_since_body_def s_def run_vpsi cppsi'_def tppsi'_def)
    show ?thesis
      using loop_before(1,4,5) tt_def(2) wf_psi'[folded j'_j] cppsi' tppsi' e'_def(1)
      by (fastforce simp: loop_inv_def s'_def j'_def[symmetric] e'_def(2) j'_j t_def)
  qed
  have loop: "loop_inv (vpsi', e', cpsi', cppsi', tppsi')" "¬while_since_cond I t (vpsi', e', cpsi', cppsi', tppsi')"
    using while_break_sound[where ?P="loop_inv" and ?Q="λs. loop_inv s ∧ ¬while_since_cond I t s", OF step_loop _ wf_loop loop_inv_init]
    by (auto simp: loop_def)
  define cphi' where "cphi' = (if b1 then Suc cphi else 0)"
  have v'_def: "v' = VYDRA_Since I vphi' vpsi' e' cphi' cpsi' cppsi' tppsi'"
    and b_def: "b = (case cppsi' of None ⇒ False | Some k ⇒ k - 1 ≤ cphi' ∧ memR (the tppsi') t I)"
    using Since(6)
    by (auto simp: v_def(1) run_vphi loop_init_def[symmetric] loop_def cphi'_def Let_def split: option.splits)
  have read_t_e': "cpsi' > 0 ⟹ read_t e' = None ⟹ False"
    using loop(1) ru_t_Some[where ?e=e'] run_t_read
    by (fastforce simp: loop_inv_def Let_def)
  define j' where "j' = Suc i - cpsi'"
  have wf_vpsi': "wf_vydra psi j' n vpsi'" and cpsi'_le_Suc_i: "cpsi' ≤ Suc i"
    and cppsi'_def: "cppsi' = (case last_before (sat psi) j' of None ⇒ None | Some k ⇒ Some (Suc i - k))"
    and tppsi'_def: "tppsi' = (case last_before (sat psi) j' of None ⇒ None | Some k ⇒ Some (τ σ k))"
    using loop(1)
    by (auto simp: loop_inv_def j'_def[symmetric])
  obtain es' where es'_def: "reaches_on ru_t l_t0 es' e'" "length es' = j'" "⋀t. t ∈ set es' ⟹ memL t (τ σ i) I"
    using loop(1)
    by (auto simp: loop_inv_def j'_def[symmetric])
  have wf_v': "wf_vydra (Since phi I psi) (Suc i) (Suc n) v'"
    and cphi'_sat: "cphi' = Suc i - (case last_before (λk. ¬sat phi k) (Suc i) of None ⇒ 0 | Some k ⇒ Suc k)"
    using cpsi'_le_Suc_i last_before_Some es'_def(3) memL_mono'[OF _ τ_mono[of i "Suc i" σ]]
    by (force simp: v'_def cppsi'_def tppsi'_def j'_def cphi'_def b1_def v_def(8) split: option.splits
        intro!: wf_vydra.intros(9)[OF wf_vphi' wf_vpsi' _ es'_def(1-2)])+
  have "j' = Suc i ∨ ¬memL (τ σ j') (τ σ i) I"
    using loop(2) j'_def read_t_e' ru_t_tau[OF es'_def(1)] read_t_run[where ?run_hd=run_hd]
    by (fastforce simp: while_since_cond_def es'_def(2) t_def split: option.splits)
  then have tau_k_j': "k ≤ i ⟹ memL (τ σ k) (τ σ i) I ⟷ k < j'" for k
    using ru_t_tau_in[OF es'_def(1)] es'_def(3) τ_mono[of j' k σ] memL_mono
    by (fastforce simp: es'_def(2) in_set_conv_nth)
  have b_sat: "b = sat (Since phi I psi) i"
  proof (rule iffI)
    assume b: "b"
    obtain m where m_def: "last_before (sat psi) j' = Some m" "i - m ≤ cphi'" "memR (τ σ m) (τ σ i) I"
      using b
      by (auto simp: b_def t_def cppsi'_def tppsi'_def split: option.splits)
    note aux = last_before_Some[OF m_def(1)]
    have mem: "mem (τ σ m) (τ σ i) I"
      using m_def(3) tau_k_j' aux
      by (auto simp: mem_def j'_def)
    have sat_phi: "sat phi x" if "m < x" "x ≤ i" for x
      using m_def(2) that le_neq_implies_less
      by (fastforce simp: cphi'_sat dest: last_before_None last_before_Some split: option.splits if_splits)
    show "sat (Since phi I psi) i"
      using aux mem sat_phi
      by (auto simp: j'_def intro!: exI[of _ m])
  next
    assume sat: "sat (Since phi I psi) i"
    then obtain k where k_def: "k ≤ i" "mem (τ σ k) (τ σ i) I" "sat psi k" "⋀k'. k < k' ∧ k' ≤ i ⟹ sat phi k'"
      by auto
    have k_j': "k < j'"
      using tau_k_j'[OF k_def(1)] k_def(2)
      by (auto simp: mem_def)
    obtain m where m_def: "last_before (sat psi) j' = Some m"
      using last_before_None[where ?P="sat psi" and ?n=j' and ?m=k] k_def(3) k_j'
      by (cases "last_before (sat psi) j'") auto
    have cppsi'_Some: "cppsi' = Some (Suc i - m)"
      by (auto simp: cppsi'_def m_def)
    have tppsi'_Some: "tppsi' = Some (τ σ m)"
      by (auto simp: tppsi'_def m_def)
    have m_k: "k ≤ m"
      using last_before_Some[OF m_def] k_def(3) k_j'
      by auto
    have tau_i_m: "memR (τ σ m) (τ σ i) I"
      using τ_mono[OF m_k, where ?s=σ] memR_mono k_def(2)
      by (auto simp: mem_def)
    have "i - m ≤ cphi'"
      using k_def(1) k_def(4) m_k
      apply (cases "k = i")
       apply (auto simp: cphi'_sat b1_def dest!: last_before_Some split: option.splits)
      apply (metis diff_le_mono2 le_neq_implies_less le_trans less_imp_le_nat nat_le_linear)
      done
    then show "b"
      using tau_i_m
      by (auto simp: b_def t_def cppsi'_Some tppsi'_Some)
  qed
  show ?case
    using wf_v' reaches_Suc_i
    by (auto simp: t_def b_sat)
next
  case (Until n I phi psi)
  obtain "back" vphi vpsi front c z es es' j where v_def:
    "v = VYDRA_Until I back vphi vpsi front c z"
    "wf_vydra phi j n vphi" "wf_vydra psi j n vpsi" "i ≤ j"
    "reaches_on ru_t l_t0 es back" "length es = i"
    "reaches_on ru_t l_t0 es' front" "length es' = j" "⋀t. t ∈ set es' ⟹ memR (τ σ i) t I"
    "c = j - i" "z = (case j of 0 ⇒ None | Suc k ⇒ Some (τ σ k, sat phi k, sat psi k))"
    "⋀k. k ∈ {i..<j - 1} ⟹ sat phi k ∧ (memL (τ σ i) (τ σ k) I ⟶ ¬sat psi k)"
    using Until(5)
    by (auto elim: wf_vydra.cases)
  define loop_init where "loop_init = (vphi, vpsi, front, c, z)"
  obtain back' vphi' vpsi' epsi' c' zo' zt zb1 zb2 where run_back: "ru_t back = Some (back', t)"
    and loop_def: "while_break (while_until_cond I t) (while_until_body run_hd (ru n)) loop_init = Some (vphi', vpsi', epsi', c', zo')"
    and v'_def: "v' = VYDRA_Until I back' vphi' vpsi' epsi' (c' - 1) zo'"
    and c'_pos: "¬c' = 0"
    and zo'_Some: "zo' = Some (zt, (zb1, zb2))"
    and b_def: "b = (zb2 ∧ memL t zt I)"
    using Until(6)
    apply (auto simp: v_def(1) Let_def loop_init_def[symmetric] split: option.splits nat.splits if_splits)
    done
  define j' where "j' = i + c'"
  have j_eq: "j = i + c"
    using v_def(4)
    by (auto simp: v_def(10))
  have t_def: "t = τ σ i"
    using ru_t_tau[OF v_def(5) run_back]
    by (auto simp: v_def(6))
  define loop_inv where "loop_inv = (λ(vphi, vpsi, epsi, c, zo).
    let j = i + c in
    wf_vydra phi j n vphi ∧ wf_vydra psi j n vpsi ∧
    (∃gs. reaches_on ru_t l_t0 gs epsi ∧ length gs = j ∧ (∀t. t ∈ set gs ⟶ memR (τ σ i) t I)) ∧
    zo = (case j of 0 ⇒ None | Suc k ⇒ Some (τ σ k, sat phi k, sat psi k)) ∧
    (∀k. k ∈ {i..<j - 1} ⟶ sat phi k ∧ (memL (τ σ i) (τ σ k) I ⟶ ¬sat psi k)))"
  have loop_inv_init: "loop_inv loop_init"
    using v_def(2,3,7,9,12)
    by (auto simp: loop_inv_def loop_init_def j_eq[symmetric] v_def(8,11))
  have loop_step: "loop_inv s'" if loop_assms: "loop_inv s" "while_until_cond I t s" "while_until_body run_hd (ru n) s = Some s'" for s s'
  proof -
    obtain vphi_cur vpsi_cur epsi_cur c_cur zo_cur where s_def: "s = (vphi_cur, vpsi_cur, epsi_cur, c_cur, zo_cur)"
      by (cases s) auto
    define j_cur where "j_cur = i + c_cur"
    obtain epsi'_cur t'_cur vphi'_cur tphi_cur bphi_cur vpsi'_cur tpsi_cur bpsi_cur where
      run_epsi: "ru_t epsi_cur = Some (epsi'_cur, t'_cur)"
      and run_vphi: "ru n vphi_cur = Some (vphi'_cur, (tphi_cur, bphi_cur))"
      and run_vpsi: "ru n vpsi_cur = Some (vpsi'_cur, (tpsi_cur, bpsi_cur))"
      using loop_assms(2,3)
      apply (auto simp: while_until_cond_def while_until_body_def s_def split: option.splits dest: read_t_run[where ?run_hd=run_hd])
      done
    have wf: "wf_vydra phi j_cur n vphi_cur" "wf_vydra psi j_cur n vpsi_cur"
      and zo_cur_def: "zo_cur = (case j_cur of 0 ⇒ None | Suc k ⇒ Some (τ σ k, sat phi k, sat psi k))"
      using loop_assms(1)
      by (auto simp: loop_inv_def s_def j_cur_def[symmetric])
    have wf': "wf_vydra phi (Suc j_cur) n vphi'_cur" "tphi_cur = τ σ j_cur" "bphi_cur = sat phi j_cur"
      "wf_vydra psi (Suc j_cur) n vpsi'_cur" "tpsi_cur = τ σ j_cur" "bpsi_cur = sat psi j_cur"
      using Until(3)[OF wf(1) run_vphi] Until(4)[OF wf(2) run_vpsi] Until(7,8)
      apply (auto)
      done
    have s'_def: "s' = (vphi'_cur, vpsi'_cur, epsi'_cur, Suc c_cur, Some (t'_cur, (bphi_cur, bpsi_cur)))"
      using loop_assms(3)
      by (auto simp: while_until_body_def s_def run_epsi run_vphi run_vpsi)
    obtain gs_cur where gs_cur_def: "reaches_on ru_t l_t0 gs_cur epsi_cur"
      "length gs_cur = j_cur" "⋀t. t ∈ set gs_cur ⟹ memR (τ σ i) t I"
      using loop_assms(1)
      by (auto simp: loop_inv_def s_def j_cur_def[symmetric])
    have t'_cur_def: "t'_cur = τ σ j_cur"
      using ru_t_tau[OF gs_cur_def(1) run_epsi]
      by (auto simp: gs_cur_def(2))
    have t'_cur_right_I: "memR t t'_cur I"
      using loop_assms(2) run_t_read[OF run_epsi]
      by (auto simp: while_until_cond_def s_def)
    have c_cur_zero: "c_cur = 0 ⟹ j_cur = i"
      by (auto simp: j_cur_def)
    have "k ∈ {i..<Suc j_cur - 1} ⟹ sat phi k ∧ (memL (τ σ i) (τ σ k) I ⟶ ¬sat psi k)" for k
      using loop_assms(1,2)
      by (cases "k = j_cur - Suc 0") (auto simp: while_until_cond_def loop_inv_def j_cur_def[symmetric] zo_cur_def s_def until_ready_def t_def split: nat.splits dest: c_cur_zero)
    then show ?thesis
      using wf' t'_cur_right_I
      using reaches_on_app[OF gs_cur_def(1) run_epsi] gs_cur_def(2,3)
      by (auto simp: loop_inv_def s'_def j_cur_def[symmetric] t_def t'_cur_def intro!: exI[of _ "gs_cur @ [t'_cur]"])
  qed
  have wf_loop: "wf {(s', s). loop_inv s ∧ while_until_cond I t s ∧ Some s' = while_until_body run_hd (ru n) s}"
  proof -
    obtain m where m_def: "¬τ σ m ≤ τ σ i + right I"
      using ex_lt_τ[where ?x="right I" and ?s=σ] Until(7)
      by auto
    define X where "X = {(s', s). loop_inv s ∧ while_until_cond I t s ∧ Some s' = while_until_body run_hd (ru n) s}"
    have "memR t (τ σ (i + c)) I ⟹ i + c < m" for c
      using m_def order_trans[OF τ_mono[where ?i=m and ?j="i + c" and ?s=σ]]
      by (fastforce simp: t_def dest!: memR_dest)
    then have "X ⊆ measure (λ(vphi, vpsi, epsi, c, zo). m - c)"
      by (fastforce simp: X_def while_until_cond_def while_until_body_def loop_inv_def Let_def split: option.splits
          dest!: read_t_run[where ?run_hd=run_hd] dest: ru_t_tau)
    then show ?thesis
      using wf_subset
      by (auto simp: X_def[symmetric])
  qed
  have loop: "loop_inv (vphi', vpsi', epsi', c', zo')" "¬while_until_cond I t (vphi', vpsi', epsi', c', zo')"
    using while_break_sound[where ?Q="λs. loop_inv s ∧ ¬while_until_cond I t s", OF _ _ wf_loop loop_inv_init] loop_step
    by (auto simp: loop_def)
  have tau_right_I: "k < j' ⟹ memR (τ σ i) (τ σ k) I" for k
    using loop(1) ru_t_tau_in
    by (auto simp: loop_inv_def j'_def[symmetric] in_set_conv_nth)
  have read_t_epsi': "read_t epsi' = Some et ⟹ et = τ σ j'" for et
    using loop(1) ru_t_tau
    by (fastforce simp: loop_inv_def Let_def j'_def dest!: read_t_run[where ?run_hd=run_hd])
  have end_cond: "until_ready I t c' zo' ∨ ¬(memR (τ σ i) (τ σ j') I)"
    unfolding t_def[symmetric]
    using Until(6) c'_pos loop(2)[unfolded while_until_cond_def]
    by (auto simp: until_ready_def v_def(1) run_back loop_init_def[symmetric] loop_def zo'_Some split: if_splits option.splits nat.splits dest: read_t_epsi')
  have Suc_i_le_j': "Suc i ≤ j'" and c'_j': "c' - Suc 0 = j' - Suc i"
    using end_cond c'_pos
    by (auto simp: until_ready_def j'_def split: nat.splits)
  have zo'_def: "zo' = (case j' of 0 ⇒ None | Suc k ⇒ Some (τ σ k, sat phi k, sat psi k))"
    and sat_phi: "k ∈ {i..<j' - 1} ⟹ sat phi k"
    and not_sat_psi: "k ∈ {i..<j' - 1} ⟹ memL (τ σ i) (τ σ k) I ⟹ ¬sat psi k" for k
    using loop(1)
    by (auto simp: loop_inv_def j'_def[symmetric])
  have b_sat: "b = sat (Until phi I psi) i"
  proof (rule iffI)
    assume b: "b"
    have mem: "mem (τ σ i) (τ σ (j' - Suc 0)) I"
      using b zo'_def tau_right_I[where ?k="j' -