Quelle  Monitor.thy

(*<*)
theory Monitor
  imports Abstract_Monitor MFOTL Table
begin
(*>*)

section ‹Monitor implementation›

subsection ‹Monitorable formulas›

definition "mmonitorable φ ⟷ safe_formula φ ∧ MFOTL.future_reach φ ≠ ∞"

fun mmonitorable_exec :: "'a MFOTL.formula ==> bool" where
  "mmonitorable_exec (MFOTL.Eq t1 t2) = (MFOTL.is_Const t1 ∨ MFOTL.is_Const t2)"
| "mmonitorable_exec (MFOTL.Neg (MFOTL.Eq (MFOTL.Const x) (MFOTL.Const y))) = True"
| "mmonitorable_exec (MFOTL.Neg (MFOTL.Eq (MFOTL.Var x) (MFOTL.Var y))) = (x = y)"
| "mmonitorable_exec (MFOTL.Pred e ts) = True"
| "mmonitorable_exec (MFOTL.Neg (MFOTL.Or (MFOTL.Neg φ) ψ)) = (mmonitorable_exec φ ∧
    (mmonitorable_exec ψ ∧ MFOTL.fv ψ ⊆ MFOTL.fv φ ∨ (case ψ of MFOTL.Neg ψ' ==> mmonitorable_exec ψ' | _ ==> False)))"
| "mmonitorable_exec (MFOTL.Or φ ψ) = (MFOTL.fv ψ = MFOTL.fv φ ∧ mmonitorable_exec φ ∧ mmonitorable_exec ψ)"
| "mmonitorable_exec (MFOTL.Exists φ) = (mmonitorable_exec φ)"
| "mmonitorable_exec (MFOTL.Prev I φ) = (mmonitorable_exec φ)"
| "mmonitorable_exec (MFOTL.Next I φ) = (mmonitorable_exec φ ∧ right I ≠ ∞)"
| "mmonitorable_exec (MFOTL.Since φ I ψ) = (MFOTL.fv φ ⊆ MFOTL.fv ψ ∧
    (mmonitorable_exec φ ∨ (case φ of MFOTL.Neg φ' ==> mmonitorable_exec φ' | _ ==> False)) ∧ mmonitorable_exec ψ)"
| "mmonitorable_exec (MFOTL.Until φ I ψ) = (MFOTL.fv φ ⊆ MFOTL.fv ψ ∧ right I ≠ ∞ ∧
    (mmonitorable_exec φ ∨ (case φ of MFOTL.Neg φ' ==> mmonitorable_exec φ' | _ ==> False)) ∧ mmonitorable_exec ψ)"
| "mmonitorable_exec _ = False"

lemma plus_eq_enat_iff: "a + b = enat i ⟷ (∃j k. a = enat j ∧ b = enat k ∧ j + k = i)"
  by (cases a; cases b) auto

lemma minus_eq_enat_iff: "a - enat k = enat i ⟷ (∃j. a = enat j ∧ j - k = i)"
  by (cases a) auto

lemma safe_formula_mmonitorable_exec: "safe_formula φ ==> MFOTL.future_reach φ ≠ ∞ ==> mmonitorable_exec φ"
proof (induct φ rule: safe_formula.induct)
  case (5 φ ψ)
  then show ?case
    unfolding safe_formula.simps future_reach.simps mmonitorable_exec.simps
    by (fastforce split: formula.splits)
next
  case (6 φ ψ)
  then show ?case 
    unfolding safe_formula.simps future_reach.simps mmonitorable_exec.simps
    by (fastforce split: formula.splits)
next
  case (10 φ I ψ)
  then show ?case 
    unfolding safe_formula.simps future_reach.simps mmonitorable_exec.simps
    by (fastforce split: formula.splits)
next
  case (11 φ I ψ)
  then show ?case 
    unfolding safe_formula.simps future_reach.simps mmonitorable_exec.simps
    by (fastforce simp: plus_eq_enat_iff split: formula.splits)
qed (auto simp add: plus_eq_enat_iff minus_eq_enat_iff)

lemma mmonitorable_exec_mmonitorable: "mmonitorable_exec φ ==> mmonitorable φ"
proof (induct φ rule: mmonitorable_exec.induct)
  case (5 φ ψ)
  then show ?case
    unfolding mmonitorable_def mmonitorable_exec.simps safe_formula.simps
    by (fastforce split: formula.splits)
next
  case (10 φ I ψ)
  then show ?case
    unfolding mmonitorable_def mmonitorable_exec.simps safe_formula.simps
    by (fastforce split: formula.splits)
next
  case (11 φ I ψ)
  then show ?case
    unfolding mmonitorable_def mmonitorable_exec.simps safe_formula.simps
    by (fastforce simp: one_enat_def split: formula.splits)
qed (auto simp add: mmonitorable_def one_enat_def)

lemma monitorable_formula_code[code]: "mmonitorable φ = mmonitorable_exec φ"
  using mmonitorable_exec_mmonitorable safe_formula_mmonitorable_exec mmonitorable_def
  by blast



subsection ‹The executable monitor›

type_synonym ts = nat

type_synonym 'a mbuf2 = "'a table list × 'a table list"
type_synonym 'a msaux = "(ts × 'a table) list"
type_synonym 'a muaux = "(ts × 'a table × 'a table) list"

datatype 'a mformula =
    MRel "'a table"
  | MPred MFOTL.name "'a MFOTL.trm list"
  | MAnd "'a mformula" bool "'a mformula" "'a mbuf2"
  | MOr "'a mformula" "'a mformula" "'a mbuf2"
  | MExists "'a mformula"
  | MPrev I "'a mformula" bool "'a table list" "ts list"
  | MNext I "'a mformula" bool "ts list"
  | MSince bool "'a mformula" I "'a mformula" "'a mbuf2" "ts list" "'a msaux"
  | MUntil bool "'a mformula" I "'a mformula" "'a mbuf2" "ts list" "'a muaux"

record 'a mstate =
  mstate_i :: nat
  mstate_m :: "'a mformula"
  mstate_n :: nat

fun eq_rel :: "nat ==> 'a MFOTL.trm ==> 'a MFOTL.trm ==> 'a table" where
  "eq_rel n (MFOTL.Const x) (MFOTL.Const y) = (if x = y then unit_table n else empty_table)"
| "eq_rel n (MFOTL.Var x) (MFOTL.Const y) = singleton_table n x y"
| "eq_rel n (MFOTL.Const x) (MFOTL.Var y) = singleton_table n y x"
| "eq_rel n (MFOTL.Var x) (MFOTL.Var y) = undefined"

fun neq_rel :: "nat ==> 'a MFOTL.trm ==> 'a MFOTL.trm ==> 'a table" where
  "neq_rel n (MFOTL.Const x) (MFOTL.Const y) = (if x = y then empty_table else unit_table n)"
| "neq_rel n (MFOTL.Var x) (MFOTL.Var y) = (if x = y then empty_table else undefined)"
| "neq_rel _ _ _ = undefined"

fun minit0 :: "nat ==> 'a MFOTL.formula ==> 'a mformula" where
  "minit0 n (MFOTL.Neg φ) = (case φ of
    MFOTL.Eq t1 t2 ==> MRel (neq_rel n t1 t2)
  | MFOTL.Or (MFOTL.Neg φ) ψ ==> (if safe_formula ψ ∧ MFOTL.fv ψ ⊆ MFOTL.fv φ
      then MAnd (minit0 n φ) False (minit0 n ψ) ([], [])
      else (case ψ of MFOTL.Neg ψ ==> MAnd (minit0 n φ) True (minit0 n ψ) ([], []) | _ ==> undefined))
  | _ ==> undefined)"
| "minit0 n (MFOTL.Eq t1 t2) = MRel (eq_rel n t1 t2)"
| "minit0 n (MFOTL.Pred e ts) = MPred e ts"
| "minit0 n (MFOTL.Or φ ψ) = MOr (minit0 n φ) (minit0 n ψ) ([], [])"
| "minit0 n (MFOTL.Exists φ) = MExists (minit0 (Suc n) φ)"
| "minit0 n (MFOTL.Prev I φ) = MPrev I (minit0 n φ) True [] []"
| "minit0 n (MFOTL.Next I φ) = MNext I (minit0 n φ) True []"
| "minit0 n (MFOTL.Since φ I ψ) = (if safe_formula φ
    then MSince True (minit0 n φ) I (minit0 n ψ) ([], []) [] []
    else (case φ of
      MFOTL.Neg φ ==> MSince False (minit0 n φ) I (minit0 n ψ) ([], []) [] []
    | _ ==> undefined))"
| "minit0 n (MFOTL.Until φ I ψ) = (if safe_formula φ
    then MUntil True (minit0 n φ) I (minit0 n ψ) ([], []) [] []
    else (case φ of
      MFOTL.Neg φ ==> MUntil False (minit0 n φ) I (minit0 n ψ) ([], []) [] []
    | _ ==> undefined))"

definition minit :: "'a MFOTL.formula ==> 'a mstate" where
  "minit φ = (let n = MFOTL.nfv φ in (mstate_i = 0, mstate_m = minit0 n φ, mstate_n = n))"

fun mprev_next :: "I ==> 'a table list ==> ts list ==> 'a table list × 'a table list × ts list" where
  "mprev_next I [] ts = ([], [], ts)"
| "mprev_next I xs [] = ([], xs, [])"
| "mprev_next I xs [t] = ([], xs, [t])"
| "mprev_next I (x # xs) (t # t' # ts) = (let (ys, zs) = mprev_next I xs (t' # ts)
    in ((if mem (t' - t) I then x else empty_table) # ys, zs))"

fun mbuf2_add :: "'a table list ==> 'a table list ==> 'a mbuf2 ==> 'a mbuf2" where
 "mbuf2_add xs' ys' (xs, ys) = (xs @ xs', ys @ ys')"

fun mbuf2_take :: "('a table ==> 'a table ==> 'b) ==> 'a mbuf2 ==> 'b list × 'a mbuf2" where
  "mbuf2_take f (x # xs, y # ys) = (let (zs, buf) = mbuf2_take f (xs, ys) in (f x y # zs, buf))"
| "mbuf2_take f (xs, ys) = ([], (xs, ys))"

fun mbuf2t_take :: "('a table ==> 'a table ==> ts ==> 'b ==> 'b) ==> 'b ==>
  'a mbuf2 ==> ts list ==> 'b × 'a mbuf2 × ts list" where
  "mbuf2t_take f z (x # xs, y # ys) (t # ts) = mbuf2t_take f (f x y t z) (xs, ys) ts"
| "mbuf2t_take f z (xs, ys) ts = (z, (xs, ys), ts)"

fun match :: "'a MFOTL.trm list ==> 'a list ==> (nat ⇀ 'a) option" where
  "match [] [] = Some Map.empty"
| "match (MFOTL.Const x # ts) (y # ys) = (if x = y then match ts ys else None)"
| "match (MFOTL.Var x # ts) (y # ys) = (case match ts ys of
      None ==> None
    | Some f ==> (case f x of
        None ==> Some (f(x ↦ y))
      | Some z ==> if y = z then Some f else None))"
| "match _ _ = None"

definition update_since :: "I ==> bool ==> 'a table ==> 'a table ==> ts ==>
  'a msaux ==> 'a table × 'a msaux" where
  "update_since I pos rel1 rel2 nt aux =
    (let aux = (case [(t, join rel pos rel1). (t, rel) ← aux, nt - t ≤ right I] of
        [] ==> [(nt, rel2)]
      | x # aux' ==> (if fst x = nt then (fst x, snd x ∪ rel2) # aux' else (nt, rel2) # x # aux'))
    in (foldr (∪) [rel. (t, rel) ← aux, left I ≤ nt - t] {}, aux))"

definition update_until :: "I ==> bool ==> 'a table ==> 'a table ==> ts ==> 'a muaux ==> 'a muaux" where
  "update_until I pos rel1 rel2 nt aux =
    (map (λx. case x of (t, a1, a2) ==> (t, if pos then join a1 True rel1 else a1 ∪ rel1,
      if mem (nt - t) I then a2 ∪ join rel2 pos a1 else a2)) aux) @
    [(nt, rel1, if left I = 0 then rel2 else empty_table)]"

fun eval_until :: "I ==> ts ==> 'a muaux ==> 'a table list × 'a muaux" where
  "eval_until I nt [] = ([], [])"
| "eval_until I nt ((t, a1, a2) # aux) = (if t + right I < nt then
    (let (xs, aux) = eval_until I nt aux in (a2 # xs, aux)) else ([], (t, a1, a2) # aux))"

primrec meval :: "nat ==> ts ==> 'a MFOTL.database ==> 'a mformula ==> 'a table list × 'a mformula" where
  "meval n t db (MRel rel) = ([rel], MRel rel)"
| "meval n t db (MPred e ts) = ([(λf. tabulate f 0 n) ` Option.these
    (match ts ` (∪(e', x)∈db. if e = e' then {x} else {}))], MPred e ts)"
| "meval n t db (MAnd φ pos ψ buf) =
    (let (xs, φ) = meval n t db φ; (ys, ψ) = meval n t db ψ;
      (zs, buf) = mbuf2_take (λr1 r2. join r1 pos r2) (mbuf2_add xs ys buf)
    in (zs, MAnd φ pos ψ buf))"
| "meval n t db (MOr φ ψ buf) =
    (let (xs, φ) = meval n t db φ; (ys, ψ) = meval n t db ψ;
      (zs, buf) = mbuf2_take (λr1 r2. r1 ∪ r2) (mbuf2_add xs ys buf)
    in (zs, MOr φ ψ buf))"
| "meval n t db (MExists φ) =
    (let (xs, φ) = meval (Suc n) t db φ in (map (λr. tl ` r) xs, MExists φ))"
| "meval n t db (MPrev I φ first buf nts) =
    (let (xs, φ) = meval n t db φ;
      (zs, buf, nts) = mprev_next I (buf @ xs) (nts @ [t])
    in (if first then empty_table # zs else zs, MPrev I φ False buf nts))"
| "meval n t db (MNext I φ first nts) =
    (let (xs, φ) = meval n t db φ;
      (xs, first) = (case (xs, first) of (_ # xs, True) ==> (xs, False) | a ==> a);
      (zs, _, nts) = mprev_next I xs (nts @ [t])
    in (zs, MNext I φ first nts))"
| "meval n t db (MSince pos φ I ψ buf nts aux) =
    (let (xs, φ) = meval n t db φ; (ys, ψ) = meval n t db ψ;
      ((zs, aux), buf, nts) = mbuf2t_take (λr1 r2 t (zs, aux).
        let (z, aux) = update_since I pos r1 r2 t aux
        in (zs @ [z], aux)) ([], aux) (mbuf2_add xs ys buf) (nts @ [t])
    in (zs, MSince pos φ I ψ buf nts aux))"
| "meval n t db (MUntil pos φ I ψ buf nts aux) =
    (let (xs, φ) = meval n t db φ; (ys, ψ) = meval n t db ψ;
      (aux, buf, nts) = mbuf2t_take (update_until I pos) aux (mbuf2_add xs ys buf) (nts @ [t]);
      (zs, aux) = eval_until I (case nts of [] ==> t | nt # _ ==> nt) aux
    in (zs, MUntil pos φ I ψ buf nts aux))"

definition mstep :: "'a MFOTL.database × ts ==> 'a mstate ==> (nat × 'a tuple) set × 'a mstate" where
  "mstep tdb st =
     (let (xs, m) = meval (mstate_n st) (snd tdb) (fst tdb) (mstate_m st)
     in (∪ (set (map (λ(i, X). (λv. (i, v)) ` X) (List.enumerate (mstate_i st) xs))),
      (mstate_i = mstate_i st + length xs, mstate_m = m, mstate_n = mstate_n st)))"

lemma mstep_alt: "mstep tdb st =
     (let (xs, m) = meval (mstate_n st) (snd tdb) (fst tdb) (mstate_m st)
     in (∪(i, X) ∈ set (List.enumerate (mstate_i st) xs). ∪v ∈ X. {(i,v)},
      (mstate_i = mstate_i st + length xs, mstate_m = m, mstate_n = mstate_n st)))"
  unfolding mstep_def
  by (auto split: prod.split)


subsection ‹Progress›

primrec progress :: "'a MFOTL.trace ==> 'a MFOTL.formula ==> nat ==> nat" where
  "progress σ (MFOTL.Pred e ts) j = j"
| "progress σ (MFOTL.Eq t1 t2) j = j"
| "progress σ (MFOTL.Neg φ) j = progress σ φ j"
| "progress σ (MFOTL.Or φ ψ) j = min (progress σ φ j) (progress σ ψ j)"
| "progress σ (MFOTL.Exists φ) j = progress σ φ j"
| "progress σ (MFOTL.Prev I φ) j = (if j = 0 then 0 else min (Suc (progress σ φ j)) j)"
| "progress σ (MFOTL.Next I φ) j = progress σ φ j - 1"
| "progress σ (MFOTL.Since φ I ψ) j = min (progress σ φ j) (progress σ ψ j)"
| "progress σ (MFOTL.Until φ I ψ) j =
    Inf {i. ∀k. k < j ∧ k ≤ min (progress σ φ j) (progress σ ψ j) ⟶ τ σ i + right I ≥ τ σ k}"

lemma progress_And[simp]: "progress σ (MFOTL.And φ ψ) j = min (progress σ φ j) (progress σ ψ j)"
  unfolding MFOTL.And_def by simp

lemma progress_And_Not[simp]: "progress σ (MFOTL.And_Not φ ψ) j = min (progress σ φ j) (progress σ ψ j)"
  unfolding MFOTL.And_Not_def by simp

lemma progress_mono: "j ≤ j' ==> progress σ φ j ≤ progress σ φ j'"
proof (induction φ)
  case (Until φ I ψ)
  then show ?case
    by (cases "right I")
      (auto dest: trans_le_add1[OF τ_mono] intro!: cInf_superset_mono)
qed auto

lemma progress_le: "progress σ φ j ≤ j"
proof (induction φ)
  case (Until φ I ψ)
  then show ?case
    by (cases "right I")
      (auto intro: trans_le_add1[OF τ_mono] intro!: cInf_lower)
qed auto

lemma progress_0[simp]: "progress σ φ 0 = 0"
  using progress_le by auto

lemma progress_ge: "MFOTL.future_reach φ ≠ ∞ ==> ∃j. i ≤ progress σ φ j"
proof (induction φ arbitrary: i)
  case (Pred e ts)
  then show ?case by auto
next
  case (Eq t1 t2)
  then show ?case by auto
next
  case (Neg φ)
  then show ?case by simp
next
  case (Or φ1 φ2)
  from Or.prems have "MFOTL.future_reach φ1 ≠ ∞"
    by (cases "MFOTL.future_reach φ1") (auto)
  moreover from Or.prems have "MFOTL.future_reach φ2 ≠ ∞"
    by (cases "MFOTL.future_reach φ2") (auto)
  ultimately obtain j1 j2 where "i ≤ progress σ φ1 j1" and "i ≤ progress σ φ2 j2"
    using Or.IH[of i] by blast
  then have "i ≤ progress σ (MFOTL.Or φ1 φ2) (max j1 j2)"
    by (cases "j1 ≤ j2") (auto elim!: order.trans[OF _ progress_mono])
  then show ?case by blast
next
  case (Exists φ)
  then show ?case by simp
next
  case (Prev I φ)
  from Prev.prems have "MFOTL.future_reach φ ≠ ∞"
    by (cases "MFOTL.future_reach φ") (auto)
  then obtain j where "i ≤ progress σ φ j"
    using Prev.IH[of i] by blast
  then show ?case by (auto intro!: exI[of _ j] elim!: order.trans[OF _ progress_le])
next
  case (Next I φ)
  from Next.prems have "MFOTL.future_reach φ ≠ ∞"
    by (cases "MFOTL.future_reach φ") (auto)
  then obtain j where "Suc i ≤ progress σ φ j"
    using Next.IH[of "Suc i"] by blast
  then show ?case by (auto intro!: exI[of _ j])
next
  case (Since φ1 I φ2)
  from Since.prems have "MFOTL.future_reach φ1 ≠ ∞"
    by (cases "MFOTL.future_reach φ1") (auto)
  moreover from Since.prems have "MFOTL.future_reach φ2 ≠ ∞"
    by (cases "MFOTL.future_reach φ2") (auto)
  ultimately obtain j1 j2 where "i ≤ progress σ φ1 j1" and "i ≤ progress σ φ2 j2"
    using Since.IH[of i] by blast
  then have "i ≤ progress σ (MFOTL.Since φ1 I φ2) (max j1 j2)"
    by (cases "j1 ≤ j2") (auto elim!: order.trans[OF _ progress_mono])
  then show ?case by blast
next
  case (Until φ1 I φ2)
  from Until.prems obtain b where [simp]: "right I = enat b"
    by (cases "right I") (auto)
  obtain i' where "i < i'" and "τ σ i + b + 1 ≤ τ σ i'"
    using ex_le_τ[where x="τ σ i + b + 1"] by (auto simp add: less_eq_Suc_le)
  then have 1: "τ σ i + b < τ σ i'" by simp
  from Until.prems have "MFOTL.future_reach φ1 ≠ ∞"
    by (cases "MFOTL.future_reach φ1") (auto)
  moreover from Until.prems have "MFOTL.future_reach φ2 ≠ ∞"
    by (cases "MFOTL.future_reach φ2") (auto)
  ultimately obtain j1 j2 where "Suc i' ≤ progress σ φ1 j1" and "Suc i' ≤ progress σ φ2 j2"
    using Until.IH[of "Suc i'"] by blast
  then have "i ≤ progress σ (MFOTL.Until φ1 I φ2) (max j1 j2)"
    unfolding progress.simps
  proof (intro cInf_greatest, goal_cases nonempty greatest)
    case nonempty
    then show ?case
      by (auto simp: trans_le_add1[OF τ_mono] intro!: exI[of _ "max j1 j2"])
  next
    case (greatest x)
    with ‹i < i'› 1 show ?case
      by (cases "j1 ≤ j2")
        (auto dest!: spec[of _ i'] simp: max_absorb1 max_absorb2 less_eq_Suc_le
          elim: order.trans[OF _ progress_le] order.trans[OF _ progress_mono, rotated]
          dest!: not_le_imp_less[THEN less_imp_le] intro!: less_τD[THEN less_imp_le, of σ i x])
  qed
  then show ?case by blast
qed

lemma cInf_restrict_nat:
  fixes x :: nat
  assumes "x ∈ A"
  shows "Inf A = Inf {y ∈ A. y ≤ x}"
  using assms by (auto intro!: antisym intro: cInf_greatest cInf_lower Inf_nat_def1)

lemma progress_time_conv:
  assumes "∀i<j. τ σ i = τ σ' i"
  shows "progress σ φ j = progress σ' φ j"
proof (induction φ)
  case (Until φ1 I φ2)
  have *: "i ≤ j - 1 ⟷ i < j" if "j ≠ 0" for i
    using that by auto
  with Until show ?case
  proof (cases "right I")
    case (enat b)
    then show ?thesis
    proof (cases "j")
      case (Suc n)
      with enat * Until show ?thesis
        using assms τ_mono[THEN trans_le_add1]
        by (auto 6 0
          intro!: box_equals[OF arg_cong[where f=Inf]
            cInf_restrict_nat[symmetric, where x=n] cInf_restrict_nat[symmetric, where x=n]])
    qed simp
  qed simp
qed simp_all

lemma Inf_UNIV_nat: "(Inf UNIV :: nat) = 0"
  by (simp add: cInf_eq_minimum)

lemma progress_prefix_conv:
  assumes "prefix_of π σ" and "prefix_of π σ'"
  shows "progress σ φ (plen π) = progress σ' φ (plen π)"
  using assms by (auto intro: progress_time_conv τ_prefix_conv)

lemma sat_prefix_conv:
  assumes "prefix_of π σ" and "prefix_of π σ'" and "i < progress σ φ (plen π)"
  shows "MFOTL.sat σ v i φ ⟷ MFOTL.sat σ' v i φ"
using assms(3) proof (induction φ arbitrary: v i)
  case (Pred e ts)
  with Γ_prefix_conv[OF assms(1,2)] show ?case by simp
next
  case (Eq t1 t2)
  show ?case by simp
next
  case (Neg φ)
  then show ?case by simp
next
  case (Or φ1 φ2)
  then show ?case by simp
next
  case (Exists φ)
  then show ?case by simp
next
  case (Prev I φ)
  with τ_prefix_conv[OF assms(1,2)] show ?case
    by (cases i) (auto split: if_splits)
next
  case (Next I φ)
  then have "Suc i < plen π"
    by (auto intro: order.strict_trans2[OF _ progress_le[of σ φ]])
  with Next τ_prefix_conv[OF assms(1,2)] show ?case by simp
next
  case (Since φ1 I φ2)
  then have "i < plen π"
    by (auto elim!: order.strict_trans2[OF _ progress_le])
  with Since τ_prefix_conv[OF assms(1,2)] show ?case by auto
next
  case (Until φ1 I φ2)
  from Until.prems obtain b where [simp]: "right I = enat b"
    by (cases "right I") (auto simp add: Inf_UNIV_nat)
  from Until.prems obtain j where "τ σ i + b + 1 ≤ τ σ j"
    "j ≤ progress σ φ1 (plen π)" "j ≤ progress σ φ2 (plen π)"
    by atomize_elim (auto 0 4 simp add: less_eq_Suc_le not_le intro: Suc_leI dest: spec[of _ "i"]
      dest!: le_cInf_iff[THEN iffD1, rotated -1])
  then have 1: "k < progress σ φ1 (plen π)" and 2: "k < progress σ φ2 (plen π)"
    if "τ σ k ≤ τ σ i + b" for k
    using that by (fastforce elim!: order.strict_trans2[rotated] intro: less_τD[of σ])+
  have 3: "k < plen π" if "τ σ k ≤ τ σ i + b" for k
    using 1[OF that] by (simp add: less_eq_Suc_le order.trans[OF _ progress_le])

  from Until.prems have "i < progress σ' (MFOTL.Until φ1 I φ2) (plen π)"
    unfolding progress_prefix_conv[OF assms(1,2)] .
  then obtain j where "τ σ' i + b + 1 ≤ τ σ' j"
    "j ≤ progress σ' φ1 (plen π)" "j ≤ progress σ' φ2 (plen π)"
    by atomize_elim (auto 0 4 simp add: less_eq_Suc_le not_le intro: Suc_leI dest: spec[of _ "i"]
      dest!: le_cInf_iff[THEN iffD1, rotated -1])
  then have 11: "k < progress σ φ1 (plen π)" and 21: "k < progress σ φ2 (plen π)"
    if "τ σ' k ≤ τ σ' i + b" for k
    unfolding progress_prefix_conv[OF assms(1,2)]
    using that by (fastforce elim!: order.strict_trans2[rotated] intro: less_τD[of σ'])+
  have 31: "k < plen π" if "τ σ' k ≤ τ σ' i + b" for k
    using 11[OF that] by (simp add: less_eq_Suc_le order.trans[OF _ progress_le])

  show ?case unfolding sat.simps
  proof ((intro ex_cong iffI; elim conjE), goal_cases LR RL)
    case (LR j)
    with Until.IH(1)[OF 1] Until.IH(2)[OF 2] τ_prefix_conv[OF assms(1,2) 3] show ?case
      by (auto 0 4 simp: le_diff_conv add.commute dest: less_imp_le order.trans[OF τ_mono, rotated])
  next
    case (RL j)
    with Until.IH(1)[OF 11] Until.IH(2)[OF 21] τ_prefix_conv[OF assms(1,2) 31] show ?case
      by (auto 0 4 simp: le_diff_conv add.commute dest: less_imp_le order.trans[OF τ_mono, rotated])
  qed
qed


subsection ‹Specification›

definition pprogress :: "'a MFOTL.formula ==> 'a MFOTL.prefix ==> nat" where
  "pprogress φ π = (THE n. ∀σ. prefix_of π σ ⟶ progress σ φ (plen π) = n)"

lemma pprogress_eq: "prefix_of π σ ==> pprogress φ π = progress σ φ (plen π)"
  unfolding pprogress_def using progress_prefix_conv
  by blast

locale future_bounded_mfotl =
  fixes φ :: "'a MFOTL.formula"
  assumes future_bounded: "MFOTL.future_reach φ ≠ ∞"

sublocale future_bounded_mfotl ⊆ sliceable_timed_progress "MFOTL.nfv φ" "MFOTL.fv φ" "relevant_events φ"
  "λσ v i. MFOTL.sat σ v i φ" "pprogress φ"
proof (unfold_locales, goal_cases)
  case (1 x)
  then show ?case by (simp add: fvi_less_nfv)
next
  case (2 v v' σ i)
  then show ?case by (simp cong: sat_fvi_cong[rule_format])
next
  case (3 v S σ i)
  then show ?case using sat_slice_iff[of v, symmetric] by simp
next
  case (4 π π')
  moreover obtain σ where "prefix_of π' σ"
    using ex_prefix_of ..
  moreover have "prefix_of π σ"
    using prefix_of_antimono[OF ‹π ≤ π'› ‹prefix_of π' σ›] .
  ultimately show ?case
    by (simp add: pprogress_eq plen_mono progress_mono)
next
  case (5 σ x)
  obtain j where "x ≤ progress σ φ j"
    using future_bounded progress_ge by blast
  then have "x ≤ pprogress φ (take_prefix j σ)"
    by (simp add: pprogress_eq[of _ σ])
  then show ?case by force
next
  case (6 π σ σ' i v)
  then have "i < progress σ φ (plen π)"
    by (simp add: pprogress_eq)
  with 6 show ?case
    using sat_prefix_conv by blast
next
  case (7 π π')
  then have "plen π = plen π'"
    by transfer (simp add: list_eq_iff_nth_eq)
  moreover obtain σ σ' where "prefix_of π σ" "prefix_of π' σ'"
    using ex_prefix_of by blast+
  moreover have "∀i < plen π. τ σ i = τ σ' i"
    using 7 calculation
    by transfer (simp add: list_eq_iff_nth_eq)
  ultimately show ?case
    by (simp add: pprogress_eq progress_time_conv)
qed

locale monitorable_mfotl =
  fixes φ :: "'a MFOTL.formula"
  assumes monitorable: "mmonitorable φ"

sublocale monitorable_mfotl ⊆ future_bounded_mfotl
  using monitorable by unfold_locales (simp add: mmonitorable_def)


subsection ‹Correctness›

subsubsection ‹Invariants›

definition wf_mbuf2 :: "nat ==> nat ==> nat ==> (nat ==> 'a table ==> bool) ==> (nat ==> 'a table ==> bool) ==>
  'a mbuf2 ==> bool" where
  "wf_mbuf2 i ja jb P Q buf ⟷ i ≤ ja ∧ i ≤ jb ∧ (case buf of (xs, ys) ==>
    list_all2 P [i..<ja] xs ∧ list_all2 Q [i..<jb] ys)"

definition wf_mbuf2' :: "'a MFOTL.trace ==> nat ==> nat ==> 'a list set ==>
  'a MFOTL.formula ==> 'a MFOTL.formula ==> 'a mbuf2 ==> bool" where
  "wf_mbuf2' σ j n R φ ψ buf ⟷ wf_mbuf2 (min (progress σ φ j) (progress σ ψ j))
    (progress σ φ j) (progress σ ψ j)
    (λi. qtable n (MFOTL.fv φ) (mem_restr R) (λv. MFOTL.sat σ (map the v) i φ))
    (λi. qtable n (MFOTL.fv ψ) (mem_restr R) (λv. MFOTL.sat σ (map the v) i ψ)) buf"

lemma wf_mbuf2'_UNIV_alt: "wf_mbuf2' σ j n UNIV φ ψ buf ⟷ (case buf of (xs, ys) ==>
  list_all2 (λi. wf_table n (MFOTL.fv φ) (λv. MFOTL.sat σ (map the v) i φ))
    [min (progress σ φ j) (progress σ ψ j) ..< (progress σ φ j)] xs ∧
  list_all2 (λi. wf_table n (MFOTL.fv ψ) (λv. MFOTL.sat σ (map the v) i ψ))
    [min (progress σ φ j) (progress σ ψ j) ..< (progress σ ψ j)] ys)"
  unfolding wf_mbuf2'_def wf_mbuf2_def
  by (simp add: mem_restr_UNIV[THEN eqTrueI, abs_def] split: prod.split)

definition wf_ts :: "'a MFOTL.trace ==> nat ==> 'a MFOTL.formula ==> 'a MFOTL.formula ==> ts list ==> bool" where
  "wf_ts σ j φ ψ ts ⟷ list_all2 (λi t. t = τ σ i) [min (progress σ φ j) (progress σ ψ j)..<j] ts"

abbreviation "Sincep pos φ I ψ ≡ MFOTL.Since (if pos then φ else MFOTL.Neg φ) I ψ"

definition wf_since_aux :: "'a MFOTL.trace ==> nat ==> 'a list set ==> bool ==>
    'a MFOTL.formula ==> I ==> 'a MFOTL.formula ==> 'a msaux ==> nat ==> bool" where
  "wf_since_aux σ n R pos φ I ψ aux ne ⟷ sorted_wrt (λx y. fst x > fst y) aux ∧
    (∀t X. (t, X) ∈ set aux ⟶ ne ≠ 0 ∧ t ≤ τ σ (ne-1) ∧ τ σ (ne-1) - t ≤ right I ∧ (∃i. τ σ i = t) ∧
      qtable n (MFOTL.fv ψ) (mem_restr R) (λv. MFOTL.sat σ (map the v) (ne-1) (Sincep pos φ (point (τ σ (ne-1) - t)) ψ)) X) ∧
    (∀t. ne ≠ 0 ∧ t ≤ τ σ (ne-1) ∧ τ σ (ne-1) - t ≤ right I ∧ (∃i. τ σ i = t) ⟶
      (∃X. (t, X) ∈ set aux))"

lemma qtable_mem_restr_UNIV: "qtable n A (mem_restr UNIV) Q X = wf_table n A Q X"
  unfolding qtable_def by auto

lemma wf_since_aux_UNIV_alt:
  "wf_since_aux σ n UNIV pos φ I ψ aux ne ⟷ sorted_wrt (λx y. fst x > fst y) aux ∧
    (∀t X. (t, X) ∈ set aux ⟶ ne ≠ 0 ∧ t ≤ τ σ (ne-1) ∧ τ σ (ne-1) - t ≤ right I ∧ (∃i. τ σ i = t) ∧
      wf_table n (MFOTL.fv ψ)
          (λv. MFOTL.sat σ (map the v) (ne-1) (Sincep pos φ (point (τ σ (ne-1) - t)) ψ)) X) ∧
    (∀t. ne ≠ 0 ∧ t ≤ τ σ (ne-1) ∧ τ σ (ne-1) - t ≤ right I ∧ (∃i. τ σ i = t) ⟶
      (∃X. (t, X) ∈ set aux))"
  unfolding wf_since_aux_def qtable_mem_restr_UNIV ..

definition wf_until_aux :: "'a MFOTL.trace ==> nat ==> 'a list set ==> bool ==>
    'a MFOTL.formula ==> I ==> 'a MFOTL.formula ==> 'a muaux ==> nat ==> bool" where
  "wf_until_aux σ n R pos φ I ψ aux ne ⟷ list_all2 (λx i. case x of (t, r1, r2) ==> t = τ σ i ∧
      qtable n (MFOTL.fv φ) (mem_restr R) (λv. if pos then (∀k∈{i..<ne+length aux}. MFOTL.sat σ (map the v) k φ)
          else (∃k∈{i..<ne+length aux}. MFOTL.sat σ (map the v) k φ)) r1 ∧
      qtable n (MFOTL.fv ψ) (mem_restr R) (λv. (∃j. i ≤ j ∧ j < ne + length aux ∧ mem (τ σ j - τ σ i) I ∧
          MFOTL.sat σ (map the v) j ψ ∧
          (∀k∈{i..<j}. if pos then MFOTL.sat σ (map the v) k φ else ¬ MFOTL.sat σ (map the v) k φ))) r2)
    aux [ne..<ne+length aux]"

lemma wf_until_aux_UNIV_alt:
  "wf_until_aux σ n UNIV pos φ I ψ aux ne ⟷ list_all2 (λx i. case x of (t, r1, r2) ==> t = τ σ i ∧
      wf_table n (MFOTL.fv φ) (λv. if pos
          then (∀k∈{i..<ne+length aux}. MFOTL.sat σ (map the v) k φ)
          else (∃k∈{i..<ne+length aux}. MFOTL.sat σ (map the v) k φ)) r1 ∧
      wf_table n (MFOTL.fv ψ) (λv. ∃j. i ≤ j ∧ j < ne + length aux ∧ mem (τ σ j - τ σ i) I ∧
          MFOTL.sat σ (map the v) j ψ ∧
          (∀k∈{i..<j}. if pos then MFOTL.sat σ (map the v) k φ else ¬ MFOTL.sat σ (map the v) k φ)) r2)
    aux [ne..<ne+length aux]"
  unfolding wf_until_aux_def qtable_mem_restr_UNIV ..
   

inductive wf_mformula :: "'a MFOTL.trace ==> nat ==>
  nat ==> 'a list set ==> 'a mformula ==> 'a MFOTL.formula ==> bool"
  for σ j where
  Eq: "MFOTL.is_Const t1 ∨ MFOTL.is_Const t2 ==>
    ∀x∈MFOTL.fv_trm t1. x < n ==> ∀x∈MFOTL.fv_trm t2. x < n ==>
    wf_mformula σ j n R (MRel (eq_rel n t1 t2)) (MFOTL.Eq t1 t2)"
| neq_Const: "φ = MRel (neq_rel n (MFOTL.Const x) (MFOTL.Const y)) ==>
    wf_mformula σ j n R φ (MFOTL.Neg (MFOTL.Eq (MFOTL.Const x) (MFOTL.Const y)))"
| neq_Var: "x < n ==>
    wf_mformula σ j n R (MRel empty_table) (MFOTL.Neg (MFOTL.Eq (MFOTL.Var x) (MFOTL.Var x)))"
| Pred: "∀x∈MFOTL.fv (MFOTL.Pred e ts). x < n ==>
    wf_mformula σ j n R (MPred e ts) (MFOTL.Pred e ts)"
| And: "wf_mformula σ j n R φ φ' ==> wf_mformula σ j n R ψ ψ' ==>
    if pos then χ = MFOTL.And φ' ψ' ∧ ¬ (safe_formula (MFOTL.Neg ψ') ∧ MFOTL.fv ψ' ⊆ MFOTL.fv φ')
      else χ = MFOTL.And_Not φ' ψ' ∧ safe_formula ψ' ∧ MFOTL.fv ψ' ⊆ MFOTL.fv φ' ==>
    wf_mbuf2' σ j n R φ' ψ' buf ==>
    wf_mformula σ j n R (MAnd φ pos ψ buf) χ"
| Or: "wf_mformula σ j n R φ φ' ==> wf_mformula σ j n R ψ ψ' ==>
    MFOTL.fv φ' = MFOTL.fv ψ' ==>
    wf_mbuf2' σ j n R φ' ψ' buf ==>
    wf_mformula σ j n R (MOr φ ψ buf) (MFOTL.Or φ' ψ')"
| Exists: "wf_mformula σ j (Suc n) (lift_envs R) φ φ' ==>
    wf_mformula σ j n R (MExists φ) (MFOTL.Exists φ')"
| Prev: "wf_mformula σ j n R φ φ' ==>
    first ⟷ j = 0 ==>
    list_all2 (λi. qtable n (MFOTL.fv φ') (mem_restr R) (λv. MFOTL.sat σ (map the v) i φ'))
      [min (progress σ φ' j) (j-1)..<progress σ φ' j] buf ==>
    list_all2 (λi t. t = τ σ i) [min (progress σ φ' j) (j-1)..<j] nts ==>
    wf_mformula σ j n R (MPrev I φ first buf nts) (MFOTL.Prev I φ')"
| Next: "wf_mformula σ j n R φ φ' ==>
    first ⟷ progress σ φ' j = 0 ==>
    list_all2 (λi t. t = τ σ i) [progress σ φ' j - 1..<j] nts ==>
    wf_mformula σ j n R (MNext I φ first nts) (MFOTL.Next I φ')"
| Since: "wf_mformula σ j n R φ φ' ==> wf_mformula σ j n R ψ ψ' ==>
    if pos then φ'' = φ' else φ'' = MFOTL.Neg φ' ==>
    safe_formula φ'' = pos ==>
    MFOTL.fv φ' ⊆ MFOTL.fv ψ' ==>
    wf_mbuf2' σ j n R φ' ψ' buf ==>
    wf_ts σ j φ' ψ' nts ==>
    wf_since_aux σ n R pos φ' I ψ' aux (progress σ (MFOTL.Since φ'' I ψ') j) ==>
    wf_mformula σ j n R (MSince pos φ I ψ buf nts aux) (MFOTL.Since φ'' I ψ')"
| Until: "wf_mformula σ j n R φ φ' ==> wf_mformula σ j n R ψ ψ' ==>
    if pos then φ'' = φ' else φ'' = MFOTL.Neg φ' ==>
    safe_formula φ'' = pos ==>
    MFOTL.fv φ' ⊆ MFOTL.fv ψ' ==>
    wf_mbuf2' σ j n R φ' ψ' buf ==>
    wf_ts σ j φ' ψ' nts ==>
    wf_until_aux σ n R pos φ' I ψ' aux (progress σ (MFOTL.Until φ'' I ψ') j) ==>
    progress σ (MFOTL.Until φ'' I ψ') j + length aux = min (progress σ φ' j) (progress σ ψ' j) ==>
    wf_mformula σ j n R (MUntil pos φ I ψ buf nts aux) (MFOTL.Until φ'' I ψ')"

definition wf_mstate :: "'a MFOTL.formula ==> 'a MFOTL.prefix ==> 'a list set ==> 'a mstate ==> bool" where
  "wf_mstate φ π R st ⟷ mstate_n st = MFOTL.nfv φ ∧ (∀σ. prefix_of π σ ⟶
    mstate_i st = progress σ φ (plen π) ∧
    wf_mformula σ (plen π) (mstate_n st) R (mstate_m st) φ)"


subsubsection ‹Initialisation›

lemma minit0_And: "¬ (safe_formula (MFOTL.Neg ψ) ∧ MFOTL.fv ψ ⊆ MFOTL.fv φ) ==>
     minit0 n (MFOTL.And φ ψ) = MAnd (minit0 n φ) True (minit0 n ψ) ([], [])"
  unfolding MFOTL.And_def by simp

lemma minit0_And_Not: "safe_formula ψ ∧ MFOTL.fv ψ ⊆ MFOTL.fv φ ==>
  minit0 n (MFOTL.And_Not φ ψ) = (MAnd (minit0 n φ) False (minit0 n ψ) ([], []))"
  unfolding MFOTL.And_Not_def MFOTL.is_Neg_def by (simp split: formula.split)

lemma wf_mbuf2'_0: "wf_mbuf2' σ 0 n R φ ψ ([], [])"
  unfolding wf_mbuf2'_def wf_mbuf2_def by simp

lemma wf_ts_0: "wf_ts σ 0 φ ψ []"
  unfolding wf_ts_def by simp

lemma wf_since_aux_Nil: "wf_since_aux σ n R pos φ' I ψ' [] 0"
  unfolding wf_since_aux_def by simp

lemma wf_until_aux_Nil: "wf_until_aux σ n R pos φ' I ψ' [] 0"
  unfolding wf_until_aux_def by simp

lemma wf_minit0: "safe_formula φ ==> ∀x∈MFOTL.fv φ. x < n ==>
  wf_mformula σ 0 n R (minit0 n φ) φ"
  by (induction arbitrary: n R rule: safe_formula_induct)
    (auto simp add: minit0_And fvi_And minit0_And_Not fvi_And_Not
      intro!: wf_mformula.intros wf_mbuf2'_0 wf_ts_0 wf_since_aux_Nil wf_until_aux_Nil
      dest: fvi_Suc_bound)

lemma wf_mstate_minit: "safe_formula φ ==> wf_mstate φ pnil R (minit φ)"
  unfolding wf_mstate_def minit_def Let_def
  by (auto intro!: wf_minit0 fvi_less_nfv)


subsubsection ‹Evaluation›

lemma match_wf_tuple: "Some f = match ts xs ==> wf_tuple n (∪t∈set ts. MFOTL.fv_trm t) (tabulate f 0 n)"
  by (induction ts xs arbitrary: f rule: match.induct)
    (fastforce simp: wf_tuple_def split: if_splits option.splits)+

lemma match_fvi_trm_None: "Some f = match ts xs ==> ∀t∈set ts. x ∉ MFOTL.fv_trm t ==> f x = None"
  by (induction ts xs arbitrary: f rule: match.induct) (auto split: if_splits option.splits)

lemma match_fvi_trm_Some: "Some f = match ts xs ==> t ∈ set ts ==> x ∈ MFOTL.fv_trm t ==> f x ≠ None"
  by (induction ts xs arbitrary: f rule: match.induct) (auto split: if_splits option.splits)

lemma match_eval_trm: "∀t∈set ts. ∀i∈MFOTL.fv_trm t. i < n ==> Some f = match ts xs ==>
    map (MFOTL.eval_trm (tabulate (λi. the (f i)) 0 n)) ts = xs"
proof (induction ts xs arbitrary: f rule: match.induct)
  case (3 x ts y ys)
  from 3(1)[symmetric] 3(2,3) show ?case
    by (auto 0 3 dest: match_fvi_trm_Some sym split: option.splits if_splits intro!: eval_trm_cong)
qed (auto split: if_splits)

lemma wf_tuple_tabulate_Some: "wf_tuple n A (tabulate f 0 n) ==> x ∈ A ==> x < n ==> ∃y. f x = Some y"
  unfolding wf_tuple_def by auto

lemma ex_match: "wf_tuple n (∪t∈set ts. MFOTL.fv_trm t) v ==> ∀t∈set ts. ∀x∈MFOTL.fv_trm t. x < n ==>
    ∃f. match ts (map (MFOTL.eval_trm (map the v)) ts) = Some f ∧ v = tabulate f 0 n"
proof (induction ts "map (MFOTL.eval_trm (map the v)) ts" arbitrary: v rule: match.induct)
  case (3 x ts y ys)
  then show ?case
  proof (cases "x ∈ (∪t∈set ts. MFOTL.fv_trm t)")
    case True
    with 3 show ?thesis
      by (auto simp: insert_absorb dest!: wf_tuple_tabulate_Some meta_spec[of _ v])
  next
    case False
    with 3(3,4) have
      *: "map (MFOTL.eval_trm (map the v)) ts = map (MFOTL.eval_trm (map the (v[x := None]))) ts"
      by (auto simp: wf_tuple_def nth_list_update intro!: eval_trm_cong)
    from False 3(2-4) obtain f where
      "match ts (map (MFOTL.eval_trm (map the v)) ts) = Some f" "v[x := None] = tabulate f 0 n"
      unfolding *
      by (atomize_elim, intro 3(1)[of "v[x := None]"])
        (auto simp: wf_tuple_def nth_list_update intro!: eval_trm_cong)
    moreover from False this have "f x = None" "length v = n"
      by (auto dest: match_fvi_trm_None[OF sym] arg_cong[of _ _ length])
    ultimately show ?thesis using 3(3)
      by (auto simp: list_eq_iff_nth_eq wf_tuple_def)
  qed
qed (auto simp: wf_tuple_def intro: nth_equalityI)

lemma eq_rel_eval_trm: "v ∈ eq_rel n t1 t2 ==> MFOTL.is_Const t1 ∨ MFOTL.is_Const t2 ==>
  ∀x∈MFOTL.fv_trm t1 ∪ MFOTL.fv_trm t2. x < n ==>
  MFOTL.eval_trm (map the v) t1 = MFOTL.eval_trm (map the v) t2"
  by (cases t1; cases t2) (simp_all add: singleton_table_def split: if_splits)

lemma in_eq_rel: "wf_tuple n (MFOTL.fv_trm t1 ∪ MFOTL.fv_trm t2) v ==>
  MFOTL.is_Const t1 ∨ MFOTL.is_Const t2 ==>
  MFOTL.eval_trm (map the v) t1 = MFOTL.eval_trm (map the v) t2 ==>
  v ∈ eq_rel n t1 t2"
  by (cases t1; cases t2)
    (auto simp: singleton_table_def wf_tuple_def unit_table_def intro!: nth_equalityI split: if_splits)

lemma table_eq_rel: "MFOTL.is_Const t1 ∨ MFOTL.is_Const t2 ==>
  table n (MFOTL.fv_trm t1 ∪ MFOTL.fv_trm t2) (eq_rel n t1 t2)"
  by (cases t1; cases t2; simp)

lemma wf_tuple_Suc_fviD: "wf_tuple (Suc n) (MFOTL.fvi b φ) v ==> wf_tuple n (MFOTL.fvi (Suc b) φ) (tl v)"
  unfolding wf_tuple_def by (simp add: fvi_Suc nth_tl)

lemma table_fvi_tl: "table (Suc n) (MFOTL.fvi b φ) X ==> table n (MFOTL.fvi (Suc b) φ) (tl ` X)"
  unfolding table_def by (auto intro: wf_tuple_Suc_fviD)

lemma wf_tuple_Suc_fvi_SomeI: "0 ∈ MFOTL.fvi b φ ==> wf_tuple n (MFOTL.fvi (Suc b) φ) v ==>
  wf_tuple (Suc n) (MFOTL.fvi b φ) (Some x # v)"
  unfolding wf_tuple_def
  by (auto simp: fvi_Suc less_Suc_eq_0_disj)

lemma wf_tuple_Suc_fvi_NoneI: "0 ∉ MFOTL.fvi b φ ==> wf_tuple n (MFOTL.fvi (Suc b) φ) v ==>
  wf_tuple (Suc n) (MFOTL.fvi b φ) (None # v)"
  unfolding wf_tuple_def
  by (auto simp: fvi_Suc less_Suc_eq_0_disj)

lemma qtable_project_fv: "qtable (Suc n) (fv φ) (mem_restr (lift_envs R)) P X ==>
    qtable n (MFOTL.fvi (Suc 0) φ) (mem_restr R)
      (λv. ∃x. P ((if 0 ∈ fv φ then Some x else None) # v)) (tl ` X)"
  using neq0_conv by (fastforce simp: image_iff Bex_def fvi_Suc elim!: qtable_cong dest!: qtable_project)

lemma mprev: "mprev_next I xs ts = (ys, xs', ts') ==>
  list_all2 P [i..<j'] xs ==> list_all2 (λi t. t = τ σ i) [i..<j] ts ==> i ≤ j' ==> i < j ==>
  list_all2 (λi X. if mem (τ σ (Suc i) - τ σ i) I then P i X else X = empty_table)
    [i..<min j' (j-1)] ys ∧
  list_all2 P [min j' (j-1)..<j'] xs' ∧
  list_all2 (λi t. t = τ σ i) [min j' (j-1)..<j] ts'"
proof (induction I xs ts arbitrary: i ys xs' ts' rule: mprev_next.induct)
  case (1 I ts)
  then have "min j' (j-1) = i" by auto
  with 1 show ?case by auto
next
  case (3 I v v' t)
  then have "min j' (j-1) = i" by (auto simp: list_all2_Cons2 upt_eq_Cons_conv)
  with 3 show ?case by auto
next
  case (4 I x xs t t' ts)
  from 4(1)[of "tl ys" xs' ts' "Suc i"] 4(2-6) show ?case
    by (auto simp add: list_all2_Cons2 upt_eq_Cons_conv Suc_less_eq2
      elim!: list.rel_mono_strong split: prod.splits if_splits)
qed simp

lemma mnext: "mprev_next I xs ts = (ys, xs', ts') ==>
  list_all2 P [Suc i..<j'] xs ==> list_all2 (λi t. t = τ σ i) [i..<j] ts ==> Suc i ≤ j' ==> i < j ==>
  list_all2 (λi X. if mem (τ σ (Suc i) - τ σ i) I then P (Suc i) X else X = empty_table)
    [i..<min (j'-1) (j-1)] ys ∧
  list_all2 P [Suc (min (j'-1) (j-1))..<j'] xs' ∧
  list_all2 (λi t. t = τ σ i) [min (j'-1) (j-1)..<j] ts'"
proof (induction I xs ts arbitrary: i ys xs' ts' rule: mprev_next.induct)
  case (1 I ts)
  then have "min (j' - 1) (j-1) = i" by auto
  with 1 show ?case by auto
next
  case (3 I v v' t)
  then have "min (j' - 1) (j-1) = i" by (auto simp: list_all2_Cons2 upt_eq_Cons_conv)
  with 3 show ?case by auto
next
  case (4 I x xs t t' ts)
  from 4(1)[of "tl ys" xs' ts' "Suc i"] 4(2-6) show ?case
    by (auto simp add: list_all2_Cons2 upt_eq_Cons_conv Suc_less_eq2
      elim!: list.rel_mono_strong split: prod.splits if_splits) (* slow 10 sec *)
qed simp

lemma in_foldr_UnI: "x ∈ A ==> A ∈ set xs ==> x ∈ foldr (∪) xs {}"
  by (induction xs) auto

lemma in_foldr_UnE: "x ∈ foldr (∪) xs {} ==> (∧A. A ∈ set xs ==> x ∈ A ==> P) ==> P"
  by (induction xs) auto

lemma sat_the_restrict: "fv φ ⊆ A ==> MFOTL.sat σ (map the (restrict A v)) i φ = MFOTL.sat σ (map the v) i φ"
  by (rule sat_fvi_cong) (auto intro!: map_the_restrict)

lemma update_since:
  assumes pre: "wf_since_aux σ n R pos φ I ψ aux ne"
    and qtable1: "qtable n (MFOTL.fv φ) (mem_restr R) (λv. MFOTL.sat σ (map the v) ne φ) rel1"
    and qtable2: "qtable n (MFOTL.fv ψ) (mem_restr R) (λv. MFOTL.sat σ (map the v) ne ψ) rel2"
    and result_eq: "(rel, aux') = update_since I pos rel1 rel2 (τ σ ne) aux"
    and fvi_subset: "MFOTL.fv φ ⊆ MFOTL.fv ψ"
  shows "wf_since_aux σ n R pos φ I ψ aux' (Suc ne)"
    and "qtable n (MFOTL.fv ψ) (mem_restr R) (λv. MFOTL.sat σ (map the v) ne (Sincep pos φ I ψ)) rel"
proof -
  let ?wf_tuple = "λv. wf_tuple n (MFOTL.fv ψ) v"
  note sat.simps[simp del]

  define aux0 where "aux0 = [(t, join rel pos rel1). (t, rel) ← aux, τ σ ne - t ≤ right I]"
  have sorted_aux0: "sorted_wrt (λx y. fst x > fst y) aux0"
    using pre[unfolded wf_since_aux_def, THEN conjunct1]
    unfolding aux0_def
    by (induction aux) (auto simp add: sorted_wrt_append)
  have in_aux0_1: "(t, X) ∈ set aux0 ==> ne ≠ 0 ∧ t ≤ τ σ (ne-1) ∧ τ σ ne - t ≤ right I ∧
      (∃i. τ σ i = t) ∧
      qtable n (MFOTL.fv ψ) (mem_restr R) (λv. (MFOTL.sat σ (map the v) (ne-1) (Sincep pos φ (point (τ σ (ne-1) - t)) ψ) ∧
        (if pos then MFOTL.sat σ (map the v) ne φ else ¬ MFOTL.sat σ (map the v) ne φ))) X" for t X
    unfolding aux0_def using fvi_subset
    by (auto 0 1 elim!: qtable_join[OF _ qtable1] simp: sat_the_restrict
      dest!: assms(1)[unfolded wf_since_aux_def, THEN conjunct2, THEN conjunct1, rule_format])
  then have in_aux0_le_τ: "(t, X) ∈ set aux0 ==> t ≤ τ σ ne" for t X
    by (meson τ_mono diff_le_self le_trans)
  have in_aux0_2: "ne ≠ 0 ==> t ≤ τ σ (ne-1) ==> τ σ ne - t ≤ right I ==> ∃i. τ σ i = t ==>
    ∃X. (t, X) ∈ set aux0" for t
  proof -
    fix t
    assume "ne ≠ 0" "t ≤ τ σ (ne-1)" "τ σ ne - t ≤ right I" "∃i. τ σ i = t"
    then obtain X where "(t, X) ∈ set aux"
      by (atomize_elim, intro assms(1)[unfolded wf_since_aux_def, THEN conjunct2, THEN conjunct2, rule_format])
        (auto simp: gr0_conv_Suc elim!: order_trans[rotated] intro!: diff_le_mono τ_mono)
    with ‹τ σ ne - t ≤ right I› have "(t, join X pos rel1) ∈ set aux0" 
      unfolding aux0_def by (auto elim!: bexI[rotated] intro!: exI[of _ X])
    then show "∃X. (t, X) ∈ set aux0"
      by blast
  qed
  have aux0_Nil: "aux0 = [] ==> ne = 0 ∨ ne ≠ 0 ∧ (∀t. t ≤ τ σ (ne-1) ∧ τ σ ne - t ≤ right I ⟶
        (∄i. τ σ i = t))"
    using in_aux0_2 by (cases "ne = 0") (auto)

  have aux'_eq: "aux' = (case aux0 of
      [] ==> [(τ σ ne, rel2)]
    | x # aux' ==> (if fst x = τ σ ne then (fst x, snd x ∪ rel2) # aux' else (τ σ ne, rel2) # x # aux'))"
    using result_eq unfolding aux0_def update_since_def Let_def by simp
  have sorted_aux': "sorted_wrt (λx y. fst x > fst y) aux'"
    unfolding aux'_eq
    using sorted_aux0 in_aux0_le_τ by (cases aux0) (fastforce)+
  have in_aux'_1: "t ≤ τ σ ne ∧ τ σ ne - t ≤ right I ∧ (∃i. τ σ i = t) ∧
      qtable n (MFOTL.fv ψ) (mem_restr R) (λv. MFOTL.sat σ (map the v) ne (Sincep pos φ (point (τ σ ne - t)) ψ)) X"
    if aux': "(t, X) ∈ set aux'" for t X
  proof (cases aux0)
    case Nil
    with aux' show ?thesis 
      unfolding aux'_eq using qtable2 aux0_Nil
      by (auto simp: zero_enat_def[symmetric] sat_Since_rec[where i=ne]
        dest: spec[of _ "τ σ (ne-1)"] elim!: qtable_cong[OF _ refl])
  next
    case (Cons a as)
    show ?thesis
    proof (cases "t = τ σ ne")
      case t: True
      show ?thesis
      proof (cases "fst a = τ σ ne")
        case True
        with aux' Cons t have "X = snd a ∪ rel2"
          unfolding aux'_eq using sorted_aux0 by auto
        moreover from in_aux0_1[of "fst a" "snd a"] Cons have "ne ≠ 0"
          "fst a ≤ τ σ (ne - 1)" "τ σ ne - fst a ≤ right I" "∃i. τ σ i = fst a"
          "qtable n (fv ψ) (mem_restr R) (λv. MFOTL.sat σ (map the v) (ne - 1)
            (Sincep pos φ (point (τ σ (ne - 1) - fst a)) ψ) ∧ (if pos then MFOTL.sat σ (map the v) ne φ
              else ¬ MFOTL.sat σ (map the v) ne φ)) (snd a)"
          by auto
        ultimately show ?thesis using qtable2 t True
          by (auto simp: sat_Since_rec[where i=ne] sat.simps(3) elim!: qtable_union)
      next
        case False
        with aux' Cons t have "X = rel2"
          unfolding aux'_eq using sorted_aux0 in_aux0_le_τ[of "fst a" "snd a"] by auto
        with aux' Cons t False show ?thesis
          unfolding aux'_eq using qtable2 in_aux0_2[of "τ σ (ne-1)"] in_aux0_le_τ[of "fst a" "snd a"] sorted_aux0
          by (auto simp: sat_Since_rec[where i=ne] sat.simps(3) zero_enat_def[symmetric] enat_0_iff not_le
            elim!: qtable_cong[OF _ refl] dest!: le_τ_less meta_mp)
    qed
    next
      case False
      with aux' Cons have "(t, X) ∈ set aux0"
        unfolding aux'_eq by (auto split: if_splits)
      then have "ne ≠ 0" "t ≤ τ σ (ne - 1)" "τ σ ne - t ≤ right I" "∃i. τ σ i = t"
        "qtable n (fv ψ) (mem_restr R) (λv. MFOTL.sat σ (map the v) (ne - 1) (Sincep pos φ (point (τ σ (ne - 1) - t)) ψ) ∧
           (if pos then MFOTL.sat σ (map the v) ne φ else ¬ MFOTL.sat σ (map the v) ne φ)) X"
        using in_aux0_1 by blast+
      with False aux' Cons show ?thesis
        unfolding aux'_eq using qtable2
        by (fastforce simp: sat_Since_rec[where i=ne] sat.simps(3)
          diff_diff_right[where i="τ σ ne" and j="τ σ _ + τ σ ne" and k="τ σ (ne - 1)",
            OF trans_le_add2, simplified] elim!: qtable_cong[OF _ refl] order_trans dest: le_τ_less)
    qed
  qed

  have in_aux'_2: "∃X. (t, X) ∈ set aux'" if "t ≤ τ σ ne" "τ σ ne - t ≤ right I" "∃i. τ σ i = t" for t
  proof (cases "t = τ σ ne")
    case True
    then show ?thesis
    proof (cases aux0)
      case Nil
      with True show ?thesis unfolding aux'_eq by simp
    next
      case (Cons a as)
      with True show ?thesis unfolding aux'_eq
        by (cases "fst a = τ σ ne") auto
    qed
  next
    case False
    with that have "ne ≠ 0"
      using le_τ_less neq0_conv by blast
    moreover from False that have  "t ≤ τ σ (ne-1)"
      by (metis One_nat_def Suc_leI Suc_pred τ_mono diff_is_0_eq' order.antisym neq0_conv not_le)
    ultimately obtain X where "(t, X) ∈ set aux0" using ‹τ σ ne - t ≤ right I› ‹∃i. τ σ i = t›
      by atomize_elim (auto intro!: in_aux0_2)
    then show ?thesis unfolding aux'_eq using False
      by (auto intro: exI[of _ X] split: list.split)
  qed

  show "wf_since_aux σ n R pos φ I ψ aux' (Suc ne)"
    unfolding wf_since_aux_def
    by (auto dest: in_aux'_1 intro: sorted_aux' in_aux'_2)

  have rel_eq: "rel = foldr (∪) [rel. (t, rel) ← aux', left I ≤ τ σ ne - t] {}"
    unfolding aux'_eq aux0_def
    using result_eq by (simp add: update_since_def Let_def)
  have rel_alt: "rel = (∪(t, rel) ∈ set aux'. if left I ≤ τ σ ne - t then rel else empty_table)"
    unfolding rel_eq
    by (auto elim!: in_foldr_UnE bexI[rotated] intro!: in_foldr_UnI)
  show "qtable n (fv ψ) (mem_restr R) (λv. MFOTL.sat σ (map the v) ne (Sincep pos φ I ψ)) rel"
    unfolding rel_alt
  proof (rule qtable_Union[where Qi="λ(t, X) v.
    left I ≤ τ σ ne - t ∧ MFOTL.sat σ (map the v) ne (Sincep pos φ (point (τ σ ne - t)) ψ)"],
    goal_cases finite qtable equiv)
    case (equiv v)
    show ?case
    proof (rule iffI, erule sat_Since_point, goal_cases left right)
      case (left j)
      then show ?case using in_aux'_2[of "τ σ j", OF _ _ exI, OF _ _ refl] by auto
    next
      case right
      then show ?case by (auto elim!: sat_Since_pointD dest: in_aux'_1)
    qed
  qed (auto dest!: in_aux'_1 intro!: qtable_empty)
qed

lemma length_update_until: "length (update_until pos I rel1 rel2 nt aux) = Suc (length aux)"
  unfolding update_until_def by simp

lemma wf_update_until:
  assumes pre: "wf_until_aux σ n R pos φ I ψ aux ne"
    and qtable1: "qtable n (MFOTL.fv φ) (mem_restr R) (λv. MFOTL.sat σ (map the v) (ne + length aux) φ) rel1"
    and qtable2: "qtable n (MFOTL.fv ψ) (mem_restr R) (λv. MFOTL.sat σ (map the v) (ne + length aux) ψ) rel2"
    and fvi_subset: "MFOTL.fv φ ⊆ MFOTL.fv ψ"
  shows "wf_until_aux σ n R pos φ I ψ (update_until I pos rel1 rel2 (τ σ (ne + length aux)) aux) ne"
  unfolding wf_until_aux_def length_update_until
  unfolding update_until_def list.rel_map add_Suc_right upt.simps eqTrueI[OF le_add1] if_True
proof (rule list_all2_appendI, unfold list.rel_map, goal_cases old new)
  case old
  show ?case
  proof (rule list.rel_mono_strong[OF assms(1)[unfolded wf_until_aux_def]]; safe, goal_cases mono1 mono2)
    case (mono1 i X Y v)
    then show ?case
      by (fastforce simp: sat_the_restrict less_Suc_eq
        elim!: qtable_join[OF _ qtable1] qtable_union[OF _ qtable1])
  next
    case (mono2 i X Y v)
    then show ?case using fvi_subset
      by (auto 0 3 simp: sat_the_restrict less_Suc_eq split: if_splits
        elim!: qtable_union[OF _ qtable_join_fixed[OF qtable2]]
        elim: qtable_cong[OF _ refl] intro: exI[of _ "ne + length aux"]) (* slow 8 sec*)
  qed
next
  case new
  then show ?case 
    by (auto intro!: qtable_empty qtable1 qtable2[THEN qtable_cong] exI[of _ "ne + length aux"]
      simp: less_Suc_eq zero_enat_def[symmetric])
qed

lemma wf_until_aux_Cons: "wf_until_aux σ n R pos φ I ψ (a # aux) ne ==>
  wf_until_aux σ n R pos φ I ψ aux (Suc ne)"
  unfolding wf_until_aux_def
  by (simp add: upt_conv_Cons del: upt_Suc cong: if_cong)

lemma wf_until_aux_Cons1: "wf_until_aux σ n R pos φ I ψ ((t, a1, a2) # aux) ne ==> t = τ σ ne"
  unfolding wf_until_aux_def
  by (simp add: upt_conv_Cons del: upt_Suc)

lemma wf_until_aux_Cons3: "wf_until_aux σ n R pos φ I ψ ((t, a1, a2) # aux) ne ==>
  qtable n (MFOTL.fv ψ) (mem_restr R) (λv. (∃j. ne ≤ j ∧ j < Suc (ne + length aux) ∧ mem (τ σ j - τ σ ne) I ∧
    MFOTL.sat σ (map the v) j ψ ∧ (∀k∈{ne..<j}. if pos then MFOTL.sat σ (map the v) k φ else ¬ MFOTL.sat σ (map the v) k φ))) a2"
  unfolding wf_until_aux_def
  by (simp add: upt_conv_Cons del: upt_Suc)

lemma upt_append: "a ≤ b ==> b ≤ c ==> [a..<b] @ [b..<c] = [a..<c]"
  by (metis le_Suc_ex upt_add_eq_append)

lemma wf_mbuf2_add:
  assumes "wf_mbuf2 i ja jb P Q buf"
    and "list_all2 P [ja..<ja'] xs"
    and "list_all2 Q [jb..<jb'] ys"
    and "ja ≤ ja'" "jb ≤ jb'"
  shows "wf_mbuf2 i ja' jb' P Q (mbuf2_add xs ys buf)"
  using assms unfolding wf_mbuf2_def
  by (auto 0 3 simp: list_all2_append2 upt_append dest: list_all2_lengthD
    intro: exI[where x="[i..<ja]"] exI[where x="[ja..<ja']"]
           exI[where x="[i..<jb]"] exI[where x="[jb..<jb']"] split: prod.splits)

lemma mbuf2_take_eqD:
  assumes "mbuf2_take f buf = (xs, buf')"
    and "wf_mbuf2 i ja jb P Q buf"
  shows "wf_mbuf2 (min ja jb) ja jb P Q buf'"
    and "list_all2 (λi z. ∃x y. P i x ∧ Q i y ∧ z = f x y) [i..<min ja jb] xs"
  using assms unfolding wf_mbuf2_def
  by (induction f buf arbitrary: i xs buf' rule: mbuf2_take.induct)
    (fastforce simp add: list_all2_Cons2 upt_eq_Cons_conv min_absorb1 min_absorb2 split: prod.splits)+

lemma mbuf2t_take_eqD:
  assumes "mbuf2t_take f z buf nts = (z', buf', nts')"
    and "wf_mbuf2 i ja jb P Q buf"
    and "list_all2 R [i..<j] nts"
    and "ja ≤ j" "jb ≤ j"
  shows "wf_mbuf2 (min ja jb) ja jb P Q buf'"
    and "list_all2 R [min ja jb..<j] nts'"
  using assms unfolding wf_mbuf2_def
  by (induction f z buf nts arbitrary: i z' buf' nts' rule: mbuf2t_take.induct)
    (auto simp add: list_all2_Cons2 upt_eq_Cons_conv less_eq_Suc_le min_absorb1 min_absorb2
      split: prod.split)

lemma mbuf2t_take_induct[consumes 5, case_names base step]:
  assumes "mbuf2t_take f z buf nts = (z', buf', nts')"
    and "wf_mbuf2 i ja jb P Q buf"
    and "list_all2 R [i..<j] nts"
    and "ja ≤ j" "jb ≤ j"
    and "U i z"
    and "∧k x y t z. i ≤ k ==> Suc k ≤ ja ==> Suc k ≤ jb ==>
      P k x ==> Q k y ==> R k t ==> U k z ==> U (Suc k) (f x y t z)"
  shows "U (min ja jb) z'"
  using assms unfolding wf_mbuf2_def
  by (induction f z buf nts arbitrary: i z' buf' nts' rule: mbuf2t_take.induct)
    (auto simp add: list_all2_Cons2 upt_eq_Cons_conv less_eq_Suc_le min_absorb1 min_absorb2
       elim!: arg_cong2[of _ _ _ _ U, OF _ refl, THEN iffD1, rotated] split: prod.split)

lemma mbuf2_take_add':
  assumes eq: "mbuf2_take f (mbuf2_add xs ys buf) = (zs, buf')"
    and pre: "wf_mbuf2' σ j n R φ ψ buf"
    and xs: "list_all2 (λi. qtable n (MFOTL.fv φ) (mem_restr R) (λv. MFOTL.sat σ (map the v) i φ))
      [progress σ φ j..<progress σ φ j'] xs"
    and ys: "list_all2 (λi. qtable n (MFOTL.fv ψ) (mem_restr R) (λv. MFOTL.sat σ (map the v) i ψ))
      [progress σ ψ j..<progress σ ψ j'] ys"
    and "j ≤ j'"
  shows "wf_mbuf2' σ j' n R φ ψ buf'"
    and "list_all2 (λi Z. ∃X Y.
      qtable n (MFOTL.fv φ) (mem_restr R) (λv. MFOTL.sat σ (map the v) i φ) X ∧
      qtable n (MFOTL.fv ψ) (mem_restr R) (λv. MFOTL.sat σ (map the v) i ψ) Y ∧
      Z = f X Y)
      [min (progress σ φ j) (progress σ ψ j)..<min (progress σ φ j') (progress σ ψ j')] zs"
  using pre unfolding wf_mbuf2'_def
  by (force intro!: mbuf2_take_eqD[OF eq] wf_mbuf2_add[OF _ xs ys] progress_mono[OF ‹j ≤ j'›])+

lemma mbuf2t_take_add':
  assumes eq: "mbuf2t_take f z (mbuf2_add xs ys buf) nts = (z', buf', nts')"
    and pre_buf: "wf_mbuf2' σ j n R φ ψ buf"
    and pre_nts: "list_all2 (λi t. t = τ σ i) [min (progress σ φ j) (progress σ ψ j)..<j'] nts"
    and xs: "list_all2 (λi. qtable n (MFOTL.fv φ) (mem_restr R) (λv. MFOTL.sat σ (map the v) i φ))
      [progress σ φ j..<progress σ φ j'] xs"
    and ys: "list_all2 (λi. qtable n (MFOTL.fv ψ) (mem_restr R) (λv. MFOTL.sat σ (map the v) i ψ))
      [progress σ ψ j..<progress σ ψ j'] ys"
    and "j ≤ j'"
  shows "wf_mbuf2' σ j' n R φ ψ buf'"
    and "wf_ts σ j' φ ψ nts'"
  using pre_buf pre_nts unfolding wf_mbuf2'_def wf_ts_def
  by (blast intro!: mbuf2t_take_eqD[OF eq] wf_mbuf2_add[OF _ xs ys] progress_mono[OF ‹j ≤ j'›]
      progress_le)+

lemma mbuf2t_take_add_induct'[consumes 6, case_names base step]:
  assumes eq: "mbuf2t_take f z (mbuf2_add xs ys buf) nts = (z', buf', nts')"
    and pre_buf: "wf_mbuf2' σ j n R φ ψ buf"
    and pre_nts: "list_all2 (λi t. t = τ σ i) [min (progress σ φ j) (progress σ ψ j)..<j'] nts"
    and xs: "list_all2 (λi. qtable n (MFOTL.fv φ) (mem_restr R) (λv. MFOTL.sat σ (map the v) i φ))
      [progress σ φ j..<progress σ φ j'] xs"
    and ys: "list_all2 (λi. qtable n (MFOTL.fv ψ) (mem_restr R) (λv. MFOTL.sat σ (map the v) i ψ))
      [progress σ ψ j..<progress σ ψ j'] ys"
    and "j ≤ j'"
    and base: "U (min (progress σ φ j) (progress σ ψ j)) z"
    and step: "∧k X Y z. min (progress σ φ j) (progress σ ψ j) ≤ k ==>
      Suc k ≤ progress σ φ j' ==> Suc k ≤ progress σ ψ j' ==>
      qtable n (MFOTL.fv φ) (mem_restr R) (λv. MFOTL.sat σ (map the v) k φ) X ==>
      qtable n (MFOTL.fv ψ) (mem_restr R) (λv. MFOTL.sat σ (map the v) k ψ) Y ==>
      U k z ==> U (Suc k) (f X Y (τ σ k) z)"
  shows "U (min (progress σ φ j') (progress σ ψ j')) z'"
  using pre_buf pre_nts unfolding wf_mbuf2'_def wf_ts_def
  by (blast intro!: mbuf2t_take_induct[OF eq] wf_mbuf2_add[OF _ xs ys] progress_mono[OF ‹j ≤ j'›]
      progress_le base step)

lemma progress_Until_le: "progress σ (formula.Until φ I ψ) j ≤ min (progress σ φ j) (progress σ ψ j)"
  by (cases "right I") (auto simp: trans_le_add1 intro!: cInf_lower)

lemma list_all2_upt_Cons: "P a x ==> list_all2 P [Suc a..<b] xs ==> Suc a ≤ b ==>
  list_all2 P [a..<b] (x # xs)"
  by (simp add: list_all2_Cons2 upt_eq_Cons_conv)

lemma list_all2_upt_append: "list_all2 P [a..<b] xs ==> list_all2 P [b..<c] ys ==>
  a ≤ b ==> b ≤ c ==> list_all2 P [a..<c] (xs @ ys)"
  by (induction xs arbitrary: a) (auto simp add: list_all2_Cons2 upt_eq_Cons_conv)

lemma meval:
  assumes "wf_mformula σ j n R φ φ'"
  shows "case meval n (τ σ j) (Γ σ j) φ of (xs, φ_n) ==> wf_mformula σ (Suc j) n R φ_n φ' ∧
    list_all2 (λi. qtable n (MFOTL.fv φ') (mem_restr R) (λv. MFOTL.sat σ (map the v) i φ'))
    [progress σ φ' j..<progress σ φ' (Suc j)] xs"
using assms proof (induction φ arbitrary: n R φ')
  case (MRel rel)
  then show ?case
    by (cases pred: wf_mformula)
      (auto simp add: ball_Un intro: wf_mformula.intros qtableI table_eq_rel eq_rel_eval_trm
        in_eq_rel qtable_empty qtable_unit_table)
next
  case (MPred e ts)
  then show ?case
    by (cases pred: wf_mformula)
      (auto 0 4 simp: table_def in_these_eq match_wf_tuple match_eval_trm image_iff dest: ex_match
        split: if_splits intro!: wf_mformula.intros qtableI elim!: bexI[rotated])
next
  case (MAnd φ pos ψ buf)
  from MAnd.prems show ?case
    by (cases pred: wf_mformula)
      (auto simp: fvi_And sat_And fvi_And_Not sat_And_Not sat_the_restrict
       dest!: MAnd.IH split: if_splits prod.splits intro!: wf_mformula.And qtable_join
       dest: mbuf2_take_add' elim!: list.rel_mono_strong)
next
  case (MOr φ ψ buf)
  from MOr.prems show ?case
    by (cases pred: wf_mformula)
      (auto dest!: MOr.IH split: if_splits prod.splits intro!: wf_mformula.Or qtable_union
       dest: mbuf2_take_add' elim!: list.rel_mono_strong)
next
  case (MExists φ)
  from MExists.prems show ?case
    by (cases pred: wf_mformula)
      (force simp: list.rel_map fvi_Suc sat_fvi_cong nth_Cons'
        intro!: wf_mformula.Exists dest!: MExists.IH qtable_project_fv 
        elim!: list.rel_mono_strong table_fvi_tl qtable_cong sat_fvi_cong[THEN iffD1, rotated -1]
        split: if_splits)+
next
  case (MPrev I φ first buf nts)
  from MPrev.prems show ?case
  proof (cases pred: wf_mformula)
    case (Prev ψ)
    let ?xs = "fst (meval n (τ σ j) (Γ σ j) φ)"
    let ?φ = "snd (meval n (τ σ j) (Γ σ j) φ)"
    let ?ls = "fst (mprev_next I (buf @ ?xs) (nts @ [τ σ j]))"
    let ?rs = "fst (snd (mprev_next I (buf @ ?xs) (nts @ [τ σ j])))"
    let ?ts = "snd (snd (mprev_next I (buf @ ?xs) (nts @ [τ σ j])))"
    let ?P = "λi X. qtable n (fv ψ) (mem_restr R) (λv. MFOTL.sat σ (map the v) i ψ) X"
    let ?min = "min (progress σ ψ (Suc j)) (Suc j - 1)"
    from Prev MPrev.IH[of n R ψ] have IH: "wf_mformula σ (Suc j) n R ?φ ψ" and
      "list_all2 ?P [progress σ ψ j..<progress σ ψ (Suc j)] ?xs" by auto
    with Prev(4,5) have "list_all2 (λi X. if mem (τ σ (Suc i) - τ σ i) I then ?P i X else X = empty_table)
        [min (progress σ ψ j) (j - 1)..<?min] ?ls ∧
       list_all2 ?P [?min..<progress σ ψ (Suc j)] ?rs ∧
       list_all2 (λi t. t = τ σ i) [?min..<Suc j] ?ts"
      by (intro mprev)
        (auto simp: progress_mono progress_le simp del: 
          intro!: list_all2_upt_append list_all2_appendI order.trans[OF min.cobounded1])
    moreover have "min (Suc (progress σ ψ j)) j = Suc (min (progress σ ψ j) (j-1))" if "j > 0"
      using that by auto
    ultimately show ?thesis using progress_mono[of j "Suc j" σ ψ] Prev(1,3) IH 
      by (auto simp: map_Suc_upt[symmetric] upt_Suc[of 0] list.rel_map qtable_empty_iff
        simp del: upt_Suc elim!: wf_mformula.Prev list.rel_mono_strong
        split: prod.split if_split_asm)
  qed simp
next
  case (MNext I φ first nts)
  from MNext.prems show ?case
  proof (cases pred: wf_mformula)
    case (Next ψ)

    have min[simp]:
      "min (progress σ ψ j - Suc 0) (j - Suc 0) = progress σ ψ j - Suc 0"
      "min (progress σ ψ (Suc j) - Suc 0) j = progress σ ψ (Suc j) - Suc 0" for j
      using progress_le[of σ ψ j] progress_le[of σ ψ "Suc j"] by auto

    let ?xs = "fst (meval n (τ σ j) (Γ σ j) φ)"
    let ?ys = "case (?xs, first) of (_ # xs, True) ==> xs | _ ==> ?xs"
    let ?φ = "snd (meval n (τ σ j) (Γ σ j) φ)"
    let ?ls = "fst (mprev_next I ?ys (nts @ [τ σ j]))"
    let ?rs = "fst (snd (mprev_next I ?ys (nts @ [τ σ j])))"
    let ?ts = "snd (snd (mprev_next I ?ys (nts @ [τ σ j])))"
    let ?P = "λi X. qtable n (fv ψ) (mem_restr R) (λv. MFOTL.sat σ (map the v) i ψ) X"
    let ?min = "min (progress σ ψ (Suc j) - 1) (Suc j - 1)"
    from Next MNext.IH[of n R ψ] have IH: "wf_mformula σ (Suc j) n R ?φ ψ"
      "list_all2 ?P [progress σ ψ j..<progress σ ψ (Suc j)] ?xs" by auto
    with Next have "list_all2 (λi X. if mem (τ σ (Suc i) - τ σ i) I then ?P (Suc i) X else X = empty_table)
        [progress σ ψ j - 1..<?min] ?ls ∧
       list_all2 ?P [Suc ?min..<progress σ ψ (Suc j)] ?rs ∧
       list_all2 (λi t. t = τ σ i) [?min..<Suc j] ?ts" if "progress σ ψ j < progress σ ψ (Suc j)"
      using progress_le[of σ ψ j] that
      by (intro mnext)
        (auto simp: progress_mono list_all2_Cons2 upt_eq_Cons_conv
          intro!: list_all2_upt_append list_all2_appendI split: list.splits)
    then show ?thesis using progress_mono[of j "Suc j" σ ψ] progress_le[of σ ψ "Suc j"] Next IH
      by (cases "progress σ ψ (Suc j) > progress σ ψ j")
        (auto 0 3 simp: qtable_empty_iff le_Suc_eq le_diff_conv
         elim!: wf_mformula.Next list.rel_mono_strong list_all2_appendI
         split: prod.split list.splits if_split_asm)  (* slow 5 sec*)
  qed simp
next
  case (MSince pos φ I ψ buf nts aux)
  note sat.simps[simp del]
  from MSince.prems obtain φ'' φ''' ψ'' where Since_eq: "φ' = MFOTL.Since φ''' I ψ''"
    and pos: "if pos then φ''' = φ'' else φ''' = MFOTL.Neg φ''"
    and pos_eq: "safe_formula φ''' = pos"
    and φ: "wf_mformula σ j n R φ φ''"
    and ψ: "wf_mformula σ j n R ψ ψ''"
    and fvi_subset: "MFOTL.fv φ'' ⊆ MFOTL.fv ψ''"
    and buf: "wf_mbuf2' σ j n R φ'' ψ'' buf"
    and nts: "wf_ts σ j φ'' ψ'' nts"
    and aux: "wf_since_aux σ n R pos φ'' I ψ'' aux (progress σ (formula.Since φ''' I ψ'') j)"
    by (cases pred: wf_mformula) (auto)
  have φ''': "MFOTL.fv φ''' = MFOTL.fv φ''" "progress σ φ''' j = progress σ φ'' j" for j
    using pos by (simp_all split: if_splits)
  have nts_snoc: "list_all2 (λi t. t = τ σ i)
    [min (progress σ φ'' j) (progress σ ψ'' j)..<Suc j] (nts @ [τ σ j])"
    using nts unfolding wf_ts_def
    by (auto simp add: progress_le[THEN min.coboundedI1] intro: list_all2_appendI)
  have update: "wf_since_aux σ n R pos φ'' I ψ'' (snd (zs, aux')) (progress σ (formula.Since φ''' I ψ'') (Suc j)) ∧
    list_all2 (λi. qtable n (MFOTL.fv φ''' ∪ MFOTL.fv ψ'') (mem_restr R)
      (λv. MFOTL.sat σ (map the v) i (formula.Since φ''' I ψ'')))
      [progress σ (formula.Since φ''' I ψ'') j..<progress σ (formula.Since φ''' I ψ'') (Suc j)] (fst (zs, aux'))"
    if eval_φ: "fst (meval n (τ σ j) (Γ σ j) φ) = xs"
      and eval_ψ: "fst (meval n (τ σ j) (Γ σ j) ψ) = ys"
      and eq: "mbuf2t_take (λr1 r2 t (zs, aux).
        case update_since I pos r1 r2 t aux of (z, x) ==> (zs @ [z], x))
        ([], aux) (mbuf2_add xs ys buf) (nts @ [τ σ j]) = ((zs, aux'), buf', nts')"
    for xs ys zs aux' buf' nts'
    unfolding progress.simps φ'''
  proof (rule mbuf2t_take_add_induct'[where j'="Suc j" and z'="(zs, aux')", OF eq buf nts_snoc],
      goal_cases xs ys _ base step)
    case xs
    then show ?case 
      using MSince.IH(1)[OF φ] eval_φ by auto
  next
    case ys
    then show ?case 
      using MSince.IH(2)[OF ψ] eval_ψ by auto
  next
    case base
    then show ?case
     using aux by (simp add: φ''')
  next
    case (step k X Y z)
    then show ?case
      using fvi_subset pos
      by (auto simp: Un_absorb1 elim!: update_since(1) list_all2_appendI dest!: update_since(2)
        split: prod.split if_splits)
  qed simp
  with MSince.IH(1)[OF φ] MSince.IH(2)[OF ψ] show ?case
    by (auto 0 3 simp: Since_eq split: prod.split
      intro: wf_mformula.Since[OF _  _ pos pos_eq fvi_subset]
      elim: mbuf2t_take_add'(1)[OF _ buf nts_snoc] mbuf2t_take_add'(2)[OF _ buf nts_snoc])
next
  case (MUntil pos φ I ψ buf nts aux)
  note sat.simps[simp del] progress.simps[simp del]
  from MUntil.prems obtain φ'' φ''' ψ'' where Until_eq: "φ' = MFOTL.Until φ''' I ψ''"
    and pos: "if pos then φ''' = φ'' else φ''' = MFOTL.Neg φ''"
    and pos_eq: "safe_formula φ''' = pos"
    and φ: "wf_mformula σ j n R φ φ''"
    and ψ: "wf_mformula σ j n R ψ ψ''"
    and fvi_subset: "MFOTL.fv φ'' ⊆ MFOTL.fv ψ''"
    and buf: "wf_mbuf2' σ j n R φ'' ψ'' buf"
    and nts: "wf_ts σ j φ'' ψ'' nts"
    and aux: "wf_until_aux σ n R pos φ'' I ψ'' aux (progress σ (formula.Until φ''' I ψ'') j)"
    and length_aux: "progress σ (formula.Until φ''' I ψ'') j + length aux =
      min (progress σ φ'' j) (progress σ ψ'' j)"
    by (cases pred: wf_mformula) (auto)
  have φ''': "progress σ φ''' j = progress σ φ'' j" for j
    using pos by (simp_all add: progress.simps split: if_splits)
  have nts_snoc: "list_all2 (λi t. t = τ σ i)
    [min (progress σ φ'' j) (progress σ ψ'' j)..<Suc j] (nts @ [τ σ j])"
    using nts unfolding wf_ts_def
    by (auto simp add: progress_le[THEN min.coboundedI1] intro: list_all2_appendI)
  {
    fix xs ys zs aux' aux'' buf' nts'
    assume eval_φ: "fst (meval n (τ σ j) (Γ σ j) φ) = xs"
      and eval_ψ: "fst (meval n (τ σ j) (Γ σ j) ψ) = ys"
      and eq1: "mbuf2t_take (update_until I pos) aux (mbuf2_add xs ys buf) (nts @ [τ σ j]) =
        (aux', buf', nts')"
      and eq2: "eval_until I (case nts' of [] ==> τ σ j | nt # _ ==> nt) aux' = (zs, aux'')"
    have update1: "wf_until_aux σ n R pos φ'' I ψ'' aux' (progress σ (formula.Until φ''' I ψ'') j) ∧
      progress σ (formula.Until φ''' I ψ'') j + length aux' =
        min (progress σ φ''' (Suc j)) (progress σ ψ'' (Suc j))"
      using MUntil.IH(1)[OF φ] eval_φ MUntil.IH(2)[OF ψ]
        eval_ψ nts_snoc nts_snoc length_aux aux fvi_subset
      unfolding φ'''
      by (elim mbuf2t_take_add_induct'[where j'="Suc j", OF eq1 buf])
        (auto simp: length_update_until elim: wf_update_until)
    have nts': "wf_ts σ (Suc j) φ'' ψ'' nts'"
      using MUntil.IH(1)[OF φ] eval_φ MUntil.IH(2)[OF ψ] eval_ψ nts_snoc
      unfolding wf_ts_def
      by (intro mbuf2t_take_eqD(2)[OF eq1]) (auto simp: progress_mono progress_le
        intro: wf_mbuf2_add buf[unfolded wf_mbuf2'_def])
    have "i ≤ progress σ (formula.Until φ''' I ψ'') (Suc j) ==>
      wf_until_aux σ n R pos φ'' I ψ'' aux' i ==>
      i + length aux' = min (progress σ φ''' (Suc j)) (progress σ ψ'' (Suc j)) ==>
      wf_until_aux σ n R pos φ'' I ψ'' aux'' (progress σ (formula.Until φ''' I ψ'') (Suc j)) ∧
        i + length zs = progress σ (formula.Until φ''' I ψ'') (Suc j) ∧
        i + length zs + length aux'' = min (progress σ φ''' (Suc j)) (progress σ ψ'' (Suc j)) ∧
        list_all2 (λi. qtable n (MFOTL.fv ψ'') (mem_restr R)
          (λv. MFOTL.sat σ (map the v) i (formula.Until (if pos then φ'' else MFOTL.Neg φ'') I ψ'')))
          [i..<i + length zs] zs" for i
      using eq2
    proof (induction aux' arbitrary: zs aux'' i)
      case Nil
      then show ?case by (auto dest!: antisym[OF progress_Until_le])
    next
      case (Cons a aux')
      obtain t a1 a2 where "a = (t, a1, a2)" by (cases a)
      from Cons.prems(2) have aux': "wf_until_aux σ n R pos φ'' I ψ'' aux' (Suc i)"
        by (rule wf_until_aux_Cons)
      from Cons.prems(2) have 1: "t = τ σ i"
        unfolding ‹a = (t, a1, a2)› by (rule wf_until_aux_Cons1)
      from Cons.prems(2) have 3: "qtable n (MFOTL.fv ψ'') (mem_restr R) (λv.
        (∃j≥i. j < Suc (i + length aux') ∧ mem (τ σ j - τ σ i) I ∧ MFOTL.sat σ (map the v) j ψ'' ∧
        (∀k∈{i..<j}. if pos then MFOTL.sat σ (map the v) k φ'' else ¬ MFOTL.sat σ (map the v) k φ''))) a2"
        unfolding ‹a = (t, a1, a2)› by (rule wf_until_aux_Cons3)
      from Cons.prems(3) have Suc_i_aux': "Suc i + length aux' =
          min (progress σ φ''' (Suc j)) (progress σ ψ'' (Suc j))"
        by simp
      have "i ≥ progress σ (formula.Until φ''' I ψ'') (Suc j)"
        if "enat (case nts' of [] ==> τ σ j | nt # x ==> nt) ≤ enat t + right I"
        using that nts' unfolding wf_ts_def progress.simps
        by (auto simp add: 1 list_all2_Cons2 upt_eq_Cons_conv φ'''
          intro!: cInf_lower τ_mono elim!: order.trans[rotated] simp del: upt_Suc split: if_splits list.splits)
      moreover
      have "Suc i ≤ progress σ (formula.Until φ''' I ψ'') (Suc j)"
        if "enat t + right I < enat (case nts' of [] ==> τ σ j | nt # x ==> nt)"
      proof -
        from that obtain m where m: "right I = enat m" by (cases "right I") auto
        have τ_min:  "τ σ (min j k) = min (τ σ j) (τ σ k)" for k
          by (simp add: min_of_mono monoI)
        have le_progress_iff[simp]: "i ≤ progress σ φ i ⟷ progress σ φ i = i" for φ i
          using progress_le[of σ φ i] by auto
        have min_Suc[simp]: "min j (Suc j) = j" by auto
        let ?X = "{i. ∀k. k < Suc j ∧ k ≤min (progress σ φ''' (Suc j)) (progress σ ψ'' (Suc j)) ⟶ enat (τ σ k) ≤ enat (τ σ i) + right I}"
        let ?min = "min j (min (progress σ φ'' (Suc j)) (progress σ ψ'' (Suc j)))"
        have "τ σ ?min ≤ τ σ j"
          by (rule τ_mono) auto
        from m have "?X ≠ {}"
          by (auto dest!: τ_mono[of _ "progress σ φ'' (Suc j)" σ]
           simp: not_le not_less φ''' intro!: exI[of _ "progress σ φ'' (Suc j)"])
        thm less_le_trans[of "τ σ i + m" "τ σ _" "τ σ _ + m"]
        from m show ?thesis
          using that nts' unfolding wf_ts_def progress.simps
          by (intro cInf_greatest[OF ‹?X ≠ {}›])
            (auto simp: 1 φ''' not_le not_less list_all2_Cons2 upt_eq_Cons_conv less_Suc_eq
              simp del: upt_Suc split: list.splits if_splits
              dest!: spec[of _ "?min"] less_le_trans[of "τ σ i + m" "τ σ _" "τ σ _ + m"] less_τD)
      qed
      moreover have *: "k < progress σ ψ (Suc j)" if
        "enat (τ σ i) + right I < enat (case nts' of [] ==> τ σ j | nt # x ==> nt)"
        "enat (τ σ k - τ σ i) ≤ right I" "ψ = ψ'' ∨ ψ = φ''" for k ψ
      proof -
        from that(1,2) obtain m where "right I = enat m"
           "τ σ i + m < (case nts' of [] ==> τ σ j | nt # x ==> nt)" "τ σ k - τ σ i ≤ m"
          by (cases "right I") auto
        with that(3) nts' progress_le[of σ ψ'' "Suc j"] progress_le[of σ φ'' "Suc j"]
        show ?thesis
          unfolding wf_ts_def le_diff_conv
          by (auto simp: not_le list_all2_Cons2 upt_eq_Cons_conv less_Suc_eq add.commute
            simp del: upt_Suc split: list.splits if_splits dest!: le_less_trans[of "τ σ k"] less_τD)
      qed
      ultimately show ?case using Cons.prems Suc_i_aux'[simplified]
        unfolding ‹a = (t, a1, a2)›
        by (auto simp: φ''' 1 sat.simps upt_conv_Cons dest!:  Cons.IH[OF _ aux' Suc_i_aux']
          simp del: upt_Suc split: if_splits prod.splits intro!: iff_exI qtable_cong[OF 3 refl])
    qed
    note this[OF progress_mono[OF le_SucI, OF order.refl] conjunct1[OF update1] conjunct2[OF update1]]
  }
  note update = this
  from MUntil.IH(1)[OF φ] MUntil.IH(2)[OF ψ] pos pos_eq fvi_subset show ?case
    by (auto 0 4 simp: Until_eq φ''' progress.simps(3) split: prod.split if_splits
      dest!: update[OF refl refl, rotated]
      intro!: wf_mformula.Until
      elim!: list.rel_mono_strong qtable_cong
      elim: mbuf2t_take_add'(1)[OF _ buf nts_snoc] mbuf2t_take_add'(2)[OF _ buf nts_snoc])
qed


subsubsection ‹Monitor step›

lemma wf_mstate_mstep: "wf_mstate φ π R st ==> last_ts π ≤ snd tdb ==>
  wf_mstate φ (psnoc π tdb) R (snd (mstep tdb st))"
  unfolding wf_mstate_def mstep_def Let_def
  by (fastforce simp add: progress_mono le_imp_diff_is_add split: prod.splits
      elim!: prefix_of_psnocE dest: meval list_all2_lengthD)

lemma mstep_output_iff: 
  assumes "wf_mstate φ π R st" "last_ts π ≤ snd tdb" "prefix_of (psnoc π tdb) σ" "mem_restr R v" 
  shows "(i, v) ∈ fst (mstep tdb st) ⟷
    progress σ φ (plen π) ≤ i ∧ i < progress σ φ (Suc (plen π)) ∧
    wf_tuple (MFOTL.nfv φ) (MFOTL.fv φ) v ∧ MFOTL.sat σ (map the v) i φ"
proof -
  from prefix_of_psnocE[OF assms(3,2)] have "prefix_of π σ" 
    "Γ σ (plen π) = fst tdb" "τ σ (plen π) = snd tdb" by auto
  moreover from assms(1) ‹prefix_of π σ› have "mstate_n st = MFOTL.nfv φ"
    "mstate_i st = progress σ φ (plen π)" "wf_mformula σ (plen π) (mstate_n st) R (mstate_m st) φ"
    unfolding wf_mstate_def by blast+
  moreover from meval[OF ‹wf_mformula σ (plen π) (mstate_n st) R (mstate_m st) φ›] obtain Vs st' where
    "meval (mstate_n st) (τ σ (plen π)) (Γ σ (plen π)) (mstate_m st) = (Vs, st')"
    "wf_mformula σ (Suc (plen π)) (mstate_n st) R st' φ"
    "list_all2 (λi. qtable (mstate_n st) (fv φ) (mem_restr R) (λv. MFOTL.sat σ (map the v) i φ))
      [progress σ φ (plen π)..<progress σ φ (Suc (plen π))] Vs" by blast
  moreover from this assms(4) have "qtable (mstate_n st) (fv φ) (mem_restr R)
    (λv. MFOTL.sat σ (map the v) i φ) (Vs ! (i - progress σ φ (plen π)))"
      if "progress σ φ (plen π) ≤ i" "i < progress σ φ (Suc (plen π))"
    using that by (auto simp: list_all2_conv_all_nth
      dest!: spec[of _ "(i - progress σ φ (plen π))"])
  ultimately show ?thesis
    using assms(4) unfolding mstep_def Let_def
    by (auto simp: in_set_enumerate_eq list_all2_conv_all_nth progress_mono le_imp_diff_is_add
      elim!: in_qtableE in_qtableI intro!: bexI[of _ "(i, Vs ! (i - progress σ φ (plen π)))"])
qed


subsubsection ‹Monitor function›

definition minit_safe where
  "minit_safe φ = (if mmonitorable_exec φ then minit φ else undefined)"

lemma minit_safe_minit: "mmonitorable φ ==> minit_safe φ = minit φ"
  unfolding minit_safe_def monitorable_formula_code by simp

lemma (in monitorable_mfotl) mstep_mverdicts:
  assumes wf: "wf_mstate φ π R st"
    and le[simp]: "last_ts π ≤ snd tdb"
    and restrict: "mem_restr R v"
  shows "(i, v) ∈ fst (mstep tdb st) ⟷ (i, v) ∈ M (psnoc π tdb) - M π"
proof -
  obtain σ where p2: "prefix_of (psnoc π tdb) σ"
    using ex_prefix_of by blast
  with le have p1: "prefix_of π σ" by (blast elim!: prefix_of_psnocE)
  show ?thesis
    unfolding M_def
    by (auto 0 3 simp: p2 progress_prefix_conv[OF _ p1] sat_prefix_conv[OF _ p1] not_less
        pprogress_eq[OF p1] pprogress_eq[OF p2]
      dest:  mstep_output_iff[OF wf le p2 restrict, THEN iffD1] spec[of _ σ]
             mstep_output_iff[OF wf le _ restrict, THEN iffD1] progress_sat_cong[OF p1]
      intro: mstep_output_iff[OF wf le p2 restrict, THEN iffD2] p1)
qed

primrec msteps0 where
  "msteps0 [] st = ({}, st)"
| "msteps0 (tdb # π) st =
    (let (V', st') = mstep tdb st; (V'', st'') = msteps0 π st' in (V' ∪ V'', st''))"

primrec msteps0_stateless where
  "msteps0_stateless [] st = {}"
| "msteps0_stateless (tdb # π) st = (let (V', st') = mstep tdb st in V' ∪ msteps0_stateless π st')"

lemma msteps0_msteps0_stateless: "fst (msteps0 w st) = msteps0_stateless w st"
  by (induct w arbitrary: st) (auto simp: split_beta)

lift_definition msteps :: "'a MFOTL.prefix ==> 'a mstate ==> (nat × 'a option list) set × 'a mstate"
  is msteps0 .

lift_definition msteps_stateless :: "'a MFOTL.prefix ==> 'a mstate ==> (nat × 'a option list) set"
  is msteps0_stateless .

lemma msteps_msteps_stateless: "fst (msteps w st) = msteps_stateless w st"
  by transfer (rule msteps0_msteps0_stateless)

lemma msteps0_snoc: "msteps0 (π @ [tdb]) st =
   (let (V', st') = msteps0 π st; (V'', st'') = mstep tdb st' in (V' ∪ V'', st''))"
  by (induct π arbitrary: st) (auto split: prod.splits)

lemma msteps_psnoc: "last_ts π ≤ snd tdb ==> msteps (psnoc π tdb) st =
   (let (V', st') = msteps π st; (V'', st'') = mstep tdb st' in (V' ∪ V'', st''))"
  by transfer (auto simp: msteps0_snoc split: list.splits prod.splits if_splits)

definition monitor where
  "monitor φ π = msteps_stateless π (minit_safe φ)"

lemma Suc_length_conv_snoc: "(Suc n = length xs) = (∃y ys. xs = ys @ [y] ∧ length ys = n)"
  by (cases xs rule: rev_cases) auto

lemma (in monitorable_mfotl) wf_mstate_msteps: "wf_mstate φ π R st ==> mem_restr R v ==> π ≤ π' ==>
  X = msteps (pdrop (plen π) π') st ==> wf_mstate φ π' R (snd X) ∧
  ((i, v) ∈ fst X) = ((i, v) ∈ M π' - M π)"
proof (induct "plen π' - plen π" arbitrary: X st π π')
  case 0
  from 0(1,4,5) have "π = π'"  "X = ({}, st)"
    by (transfer; auto)+
  with 0(2) show ?case by simp
next
  case (Suc x)
  from Suc(2,5) obtain π'' tdb where "x = plen π'' - plen π"  "π ≤ π''"
    "π' = psnoc π'' tdb" "pdrop (plen π) (psnoc π'' tdb) = psnoc (pdrop (plen π) π'') tdb"
    "last_ts (pdrop (plen π) π'') ≤ snd tdb" "last_ts π'' ≤ snd tdb"
    "π'' ≤ psnoc π'' tdb"
  proof (atomize_elim, transfer, elim exE, goal_cases prefix)
    case (prefix _ _ π' _ π_tdb)
    then show ?case
    proof (cases π_tdb rule: rev_cases)
      case (snoc π tdb)
      with prefix show ?thesis
        by (intro bexI[of _ "π' @ π"] exI[of _ tdb])
          (force simp: sorted_append append_eq_Cons_conv split: list.splits if_splits)+
    qed simp
  qed
  with Suc(1)[OF this(1) Suc.prems(1,2) this(2) refl] Suc.prems show ?case
    unfolding msteps_msteps_stateless[symmetric]
    by (auto simp: msteps_psnoc split_beta mstep_mverdicts
      dest: mono_monitor[THEN set_mp, rotated] intro!: wf_mstate_mstep)
qed

lemma (in monitorable_mfotl) wf_mstate_msteps_stateless:
  assumes "wf_mstate φ π R st" "mem_restr R v" "π ≤ π'"
  shows "(i, v) ∈ msteps_stateless (pdrop (plen π) π') st ⟷ (i, v) ∈ M π' - M π"
  using wf_mstate_msteps[OF assms refl] unfolding msteps_msteps_stateless by simp

lemma (in monitorable_mfotl) wf_mstate_msteps_stateless_UNIV: "wf_mstate φ π UNIV st ==> π ≤ π' ==>
  msteps_stateless (pdrop (plen π) π') st = M π' - M π"
  by (auto dest: wf_mstate_msteps_stateless[OF _ mem_restr_UNIV])

lemma (in monitorable_mfotl) mverdicts_Nil: "M pnil = {}"
  by (simp add: M_def pprogress_eq)

lemma wf_mstate_minit_safe: "mmonitorable φ ==> wf_mstate φ pnil R (minit_safe φ)"
  using wf_mstate_minit minit_safe_minit mmonitorable_def by metis

lemma (in monitorable_mfotl) monitor_mverdicts: "monitor φ π = M π"
  unfolding monitor_def using monitorable
  by (subst wf_mstate_msteps_stateless_UNIV[OF wf_mstate_minit_safe, simplified])
    (auto simp: mmonitorable_def mverdicts_Nil)

subsection ‹Collected correctness results›

context monitorable_mfotl
begin

text ‹We summarize the main results proved above.
 begin{enumerate}
 item The term @{term M} describes semantically the monitor's expected behaviour:
 begin{itemize}
 item @{thm[source] mono_monitor}: @{thm mono_monitor[no_vars]}
 item @{thm[source] sound_monitor}: @{thm sound_monitor[no_vars]}
 item @{thm[source] complete_monitor}: @{thm complete_monitor[no_vars]}
 item @{thm[source] sliceable_M}: @{thm sliceable_M[no_vars]}
 end{itemize}
 item The executable monitor's online interface @{term minit_safe} and @{term mstep}
 preserves the invariant @{term wf_mstate} and produces the the verdicts according
 to @{term M}:
 begin{itemize}
 item @{thm[source] wf_mstate_minit_safe}: @{thm wf_mstate_minit_safe[no_vars]}
 item @{thm[source] wf_mstate_mstep}: @{thm wf_mstate_mstep[no_vars]}
 item @{thm[source] mstep_mverdicts}: @{thm mstep_mverdicts[no_vars]}
 end{itemize}
 item The executable monitor's offline interface @{term monitor} implements @{term M}:
 begin{itemize}
 item @{thm[source] monitor_mverdicts}: @{thm monitor_mverdicts[no_vars]}
 end{itemize}
 end{enumerate}
 ›

end

(*<*)
end
(*>*)