Session MFOTL_Monitor

Theory Trace

(*<*)
theory Trace
  imports "HOL-Library.Stream"
begin
(*>*)

section ‹Traces and trace prefixes›

subsection ‹Infinite traces›

coinductive ssorted :: "'a :: linorder stream  bool" where
  "shd s  shd (stl s)  ssorted (stl s)  ssorted s"

lemma ssorted_siterate[simp]: "(n. n  f n)  ssorted (siterate f n)"
  by (coinduction arbitrary: n) auto

lemma ssortedD: "ssorted s  s !! i  stl s !! i"
  by (induct i arbitrary: s) (auto elim: ssorted.cases)

lemma ssorted_sdrop: "ssorted s  ssorted (sdrop i s)"
  by (coinduction arbitrary: i s) (auto elim: ssorted.cases ssortedD)

lemma ssorted_monoD: "ssorted s  i  j  s !! i  s !! j"
proof (induct "j - i" arbitrary: j)
  case (Suc x)
  from Suc(1)[of "j - 1"] Suc(2-4) ssortedD[of s "j - 1"]
    show ?case by (cases j) (auto simp: le_Suc_eq Suc_diff_le)
qed simp

lemma sorted_stake: "ssorted s  sorted (stake i s)"
  by (induct i arbitrary: s)
    (auto elim: ssorted.cases simp: in_set_conv_nth
      intro!: ssorted_monoD[of _ 0, simplified, THEN order_trans, OF _ ssortedD])

lemma ssorted_monoI: "i j. i  j  s !! i  s !! j  ssorted s"
  by (coinduction arbitrary: s)
    (auto dest: spec2[of _ "Suc _" "Suc _"] spec2[of _ 0 "Suc 0"])

lemma ssorted_iff_mono: "ssorted s  (i j. i  j  s !! i  s !! j)"
  using ssorted_monoI ssorted_monoD by metis

lemma ssorted_iff_le_Suc: "ssorted s  (i. s !! i  s !! Suc i)"
  using mono_iff_le_Suc[of "snth s"] by (simp add: mono_def ssorted_iff_mono)

definition "sincreasing s = (x. i. x < s !! i)"

lemma sincreasingI: "(x. i. x < s !! i)  sincreasing s"
  by (simp add: sincreasing_def)

lemma sincreasing_grD:
  fixes x :: "'a :: semilattice_sup"
  assumes "sincreasing s"
  shows "j>i. x < s !! j"
proof -
  let ?A = "insert x {s !! n | n. n  i}"
  from assms obtain j where *: "Sup_fin ?A < s !! j"
    by (auto simp: sincreasing_def)
  then have "x < s !! j"
    by (rule order.strict_trans1[rotated]) (auto intro: Sup_fin.coboundedI)
  moreover have "i < j"
  proof (rule ccontr)
    assume "¬ i < j"
    then have "s !! j  ?A" by (auto simp: not_less)
    then have "s !! j  Sup_fin ?A"
      by (auto intro: Sup_fin.coboundedI)
    with * show False by simp
  qed
  ultimately show ?thesis by blast
qed

lemma sincreasing_siterate_nat[simp]:
  fixes n :: nat
  assumes "(n. n < f n)"
  shows "sincreasing (siterate f n)"
unfolding sincreasing_def proof
  fix x
  show "i. x < siterate f n !! i"
  proof (induction x)
    case 0
    have "0 < siterate f n !! 1"
      using order.strict_trans1[OF le0 assms] by simp
    then show ?case ..
  next
    case (Suc x)
    then obtain i where "x < siterate f n !! i" ..
    then have "Suc x < siterate f n !! Suc i"
      using order.strict_trans1[OF _ assms] by (simp del: snth.simps)
    then show ?case ..
  qed
qed

lemma sincreasing_stl: "sincreasing s  sincreasing (stl s)" for s :: "'a :: semilattice_sup stream"
  by (auto 0 4 simp: gr0_conv_Suc intro!: sincreasingI dest: sincreasing_grD[of s 0])

typedef 'a trace = "{s :: ('a set × nat) stream. ssorted (smap snd s)  sincreasing (smap snd s)}"
  by (intro exI[of _ "smap (λi. ({}, i)) nats"])
    (auto simp: stream.map_comp stream.map_ident cong: stream.map_cong)

setup_lifting type_definition_trace

lift_definition Γ :: "'a trace  nat  'a set" is
  "λs i. fst (s !! i)" .
lift_definition τ :: "'a trace  nat  nat" is
  "λs i. snd (s !! i)" .

lemma stream_eq_iff: "s = s'  (n. s !! n = s' !! n)"
  by (metis stream.map_cong0 stream_smap_nats)

lemma trace_eqI: "(i. Γ σ i = Γ σ' i)  (i. τ σ i = τ σ' i)  σ = σ'"
  by transfer (auto simp: stream_eq_iff intro!: prod_eqI)

lemma τ_mono[simp]: "i  j  τ s i  τ s j"
  by transfer (auto simp: ssorted_iff_mono)

lemma ex_le_τ: "ji. x  τ s j"
  by (transfer fixing: i x) (auto dest!: sincreasing_grD[of _ i x] less_imp_le)

lemma le_τ_less: σ i  τ σ j  j < i  τ σ i = τ σ j"
  by (simp add: antisym)

lemma less_τD: σ i < τ σ j  i < j"
  by (meson τ_mono less_le_not_le not_le_imp_less)

abbreviation "Δ s i  τ s i - τ s (i - 1)"

lift_definition map_Γ :: "('a set  'b set)  'a trace  'b trace" is
  "λf s. smap (λ(x, i). (f x, i)) s"
  by (auto simp: stream.map_comp prod.case_eq_if cong: stream.map_cong)

lemma Γ_map_Γ[simp]: (map_Γ f s) i = f (Γ s i)"
  by transfer (simp add: prod.case_eq_if)

lemma τ_map_Γ[simp]: (map_Γ f s) i = τ s i"
  by transfer (simp add: prod.case_eq_if)

lemma map_Γ_id[simp]: "map_Γ id s = s"
  by transfer (simp add: stream.map_id)

lemma map_Γ_comp: "map_Γ g (map_Γ f s) = map_Γ (g  f) s"
  by transfer (simp add: stream.map_comp comp_def prod.case_eq_if case_prod_beta')

lemma map_Γ_cong: "σ1 = σ2  (x. f1 x = f2 x)  map_Γ f1 σ1 = map_Γ f2 σ2"
  by transfer (auto intro!: stream.map_cong)


subsection ‹Finite trace prefixes›

typedef 'a prefix = "{p :: ('a set × nat) list. sorted (map snd p)}"
  by (auto intro!: exI[of _ "[]"])

setup_lifting type_definition_prefix

lift_definition pmap_Γ :: "('a set  'b set)  'a prefix  'b prefix" is
  "λf. map (λ(x, i). (f x, i))"
  by (simp add: split_beta comp_def)

lift_definition last_ts :: "'a prefix  nat" is
  "λp. (case p of []  0 | _  snd (last p))" .

lift_definition first_ts :: "nat  'a prefix  nat" is
  "λn p. (case p of []  n | _  snd (hd p))" .

lift_definition pnil :: "'a prefix" is "[]" by simp

lift_definition plen :: "'a prefix  nat" is "length" .

lift_definition psnoc :: "'a prefix  'a set × nat  'a prefix" is
  "λp x. if (case p of []  0 | _  snd (last p))  snd x then p @ [x] else []"
proof (goal_cases sorted_psnoc)
  case (sorted_psnoc p x)
  then show ?case
    by (induction p) (auto split: if_splits list.splits)
qed

instantiation prefix :: (type) order begin

lift_definition less_eq_prefix :: "'a prefix  'a prefix  bool" is
  "λp q. r. q = p @ r" .

definition less_prefix :: "'a prefix  'a prefix  bool" where
  "less_prefix x y = (x  y  ¬ y  x)"

instance
proof (standard, goal_cases less refl trans antisym)
  case (less x y)
  then show ?case unfolding less_prefix_def ..
next
  case (refl x)
  then show ?case by transfer auto
next
  case (trans x y z)
  then show ?case by transfer auto
next
  case (antisym x y)
  then show ?case by transfer auto
qed

end

lemma psnoc_inject[simp]:
  "last_ts p  snd x  last_ts q  snd y  psnoc p x = psnoc q y  (p = q  x = y)"
  by transfer auto

lift_definition prefix_of :: "'a prefix  'a trace  bool" is "λp s. stake (length p) s = p" .

lemma prefix_of_pnil[simp]: "prefix_of pnil σ"
  by transfer auto

lemma plen_pnil[simp]: "plen pnil = 0"
  by transfer auto

lemma prefix_of_pmap_Γ[simp]: "prefix_of π σ  prefix_of (pmap_Γ f π) (map_Γ f σ)"
  by transfer auto

lemma plen_mono: "π  π'  plen π  plen π'"
  by transfer auto

lemma prefix_of_psnocE: "prefix_of (psnoc p x) s  last_ts p  snd x 
  (prefix_of p s  Γ s (plen p) = fst x  τ s (plen p) = snd x  P)  P"
  by transfer (simp del: stake.simps add: stake_Suc)

lemma le_pnil[simp]: "pnil  π"
  by transfer auto

lift_definition take_prefix :: "nat  'a trace  'a prefix" is stake
  by (auto dest: sorted_stake)

lemma plen_take_prefix[simp]: "plen (take_prefix i σ) = i"
  by transfer auto

lemma plen_psnoc[simp]: "last_ts π  snd x  plen (psnoc π x) = plen π + 1"
  by transfer auto

lemma prefix_of_take_prefix[simp]: "prefix_of (take_prefix i σ) σ"
  by transfer auto

lift_definition pdrop :: "nat  'a prefix  'a prefix" is drop
  by (auto simp: drop_map[symmetric] sorted_drop)

lemma pdrop_0[simp]: "pdrop 0 π = π"
  by transfer auto

lemma prefix_of_antimono: "π  π'  prefix_of π' s  prefix_of π s"
  by transfer (auto simp del: stake_add simp add: stake_add[symmetric])

lemma prefix_of_imp_linear: "prefix_of π σ  prefix_of π' σ  π  π'  π'  π"
proof transfer
  fix π π' and σ :: "('a set × nat) stream"
  assume assms: "stake (length π) σ = π" "stake (length π') σ = π'"
  show "(r. π' = π @ r)  (r. π = π' @ r)"
  proof (cases "length π" "length π'" rule: le_cases)
    case le
    then have "π' = take (length π) π' @ drop (length π) π'"
      by simp
    moreover have "take (length π) π' = π"
      using assms le by (metis min.absorb1 take_stake)
    ultimately show ?thesis by auto
  next
    case ge
    then have "π = take (length π') π @ drop (length π') π"
      by simp
    moreover have "take (length π') π = π'"
      using assms ge by (metis min.absorb1 take_stake)
    ultimately show ?thesis by auto
  qed
qed

lemma ex_prefix_of: "s. prefix_of p s"
proof (transfer, intro bexI CollectI conjI)
  fix p :: "('a set × nat) list"
  assume *: "sorted (map snd p)"
  let  = "p @- smap (Pair undefined) (fromN (snd (last p)))"
  show "stake (length p)  = p" by (simp add: stake_shift)
  have le_last: "snd (p ! i)  snd (last p)" if "i < length p" for i
    using sorted_nth_mono[OF *, of i "length p - 1"] that
    by (cases p) (auto simp: last_conv_nth nth_Cons')
  with * show "ssorted (smap snd )"
    by (force simp: ssorted_iff_mono sorted_iff_nth_mono shift_snth)
  show "sincreasing (smap snd )"
  proof (rule sincreasingI)
    fix x
    have "x < smap snd  !! Suc (length p + x)"
      by simp (metis Suc_pred add.commute diff_Suc_Suc length_greater_0_conv less_add_Suc1 less_diff_conv)
    then show "i. x < smap snd  !! i" ..
  qed
qed

lemma τ_prefix_conv: "prefix_of p s  prefix_of p s'  i < plen p  τ s i = τ s' i"
  by transfer (simp add: stake_nth[symmetric])

lemma Γ_prefix_conv: "prefix_of p s  prefix_of p s'  i < plen p  Γ s i = Γ s' i"
  by transfer (simp add: stake_nth[symmetric])

lemma sincreasing_sdrop:
  fixes s :: "('a :: semilattice_sup) stream"
  assumes "sincreasing s"
  shows "sincreasing (sdrop n s)"
proof (rule sincreasingI)
  fix x
  obtain i where "n < i" and "x < s !! i"
    using sincreasing_grD[OF assms] by blast
  then have "x < sdrop n s !! (i - n)"
    by (simp add: sdrop_snth)
  then show "i. x < sdrop n s !! i" ..
qed

lemma ssorted_shift:
  "ssorted (xs @- s) = (sorted xs  ssorted s  (xset xs. ysset s. x  y))"
proof safe
  assume *: "ssorted (xs @- s)"
  then show "sorted xs"
    by (auto simp: ssorted_iff_mono shift_snth sorted_iff_nth_mono split: if_splits)
  from ssorted_sdrop[OF *, of "length xs"] show "ssorted s"
    by (auto simp: sdrop_shift)
  fix x y assume "x  set xs" "y  sset s"
  then obtain i j where "i < length xs" "xs ! i = x" "s !! j = y"
    by (auto simp: set_conv_nth sset_range)
  with ssorted_monoD[OF *, of i "j + length xs"] show "x  y" by auto
next
  assume "sorted xs" "ssorted s" "xset xs. ysset s. x  y"
  then show "ssorted (xs @- s)"
  proof (coinduction arbitrary: xs s)
    case (ssorted xs s)
    with ‹ssorted s show ?case
      by (subst (asm) ssorted.simps) (auto 0 4 simp: neq_Nil_conv shd_sset intro: exI[of _ "_ # _"])
  qed
qed

lemma sincreasing_shift:
  assumes "sincreasing s"
  shows "sincreasing (xs @- s)"
proof (rule sincreasingI)
  fix x
  from assms obtain i where "x < s !! i"
    unfolding sincreasing_def by blast
  then have "x < (xs @- s) !! (length xs + i)"
    by simp
  then show "i. x < (xs @- s) !! i" ..
qed

lift_definition replace_prefix :: "'a prefix  'a trace  'a trace" is
   "λπ σ. if ssorted (smap snd (π @- sdrop (length π) σ)) then
     π @- sdrop (length π) σ else smap (λi. ({}, i)) nats"
  by (auto split: if_splits simp: stream.map_comp stream.map_ident sdrop_smap[symmetric]
    simp del: sdrop_smap intro!: sincreasing_shift sincreasing_sdrop cong: stream.map_cong)

lemma prefix_of_replace_prefix:
  "prefix_of (pmap_Γ f π) σ  prefix_of π (replace_prefix π σ)"
proof (transfer; safe; goal_cases)
  case (1 f π σ)
  then show ?case
    by (subst (asm) (2) stake_sdrop[symmetric, of _ "length π"])
      (auto 0 3 simp: ssorted_shift split_beta o_def stake_shift sdrop_smap[symmetric]
        ssorted_sdrop not_le simp del: sdrop_smap)
qed

lemma map_Γ_replace_prefix:
  "x. f (f x) = f x  prefix_of (pmap_Γ f π) σ  map_Γ f (replace_prefix π σ) = map_Γ f σ"
proof (transfer; safe; goal_cases)
  case (1 f π σ)
  then show ?case
    by (subst (asm) (2) stake_sdrop[symmetric, of σ "length π"],
        subst (3) stake_sdrop[symmetric, of σ "length π"])
      (auto simp: ssorted_shift split_beta o_def stake_shift sdrop_smap[symmetric] ssorted_sdrop
        not_le simp del: sdrop_smap cong: map_cong)
qed

lemma prefix_of_pmap_Γ_D:
  assumes "prefix_of (pmap_Γ f π) σ"
  shows "σ'. prefix_of π σ'  prefix_of (pmap_Γ f π) (map_Γ f σ')"
proof -
  from assms(1) obtain σ' where 1: "prefix_of π σ'"
    using ex_prefix_of by blast
  then have "prefix_of (pmap_Γ f π) (map_Γ f σ')"
    by transfer simp
  with 1 show ?thesis by blast
qed

lemma prefix_of_map_Γ_D:
  assumes "prefix_of π' (map_Γ f σ)"
  shows "π''. π' = pmap_Γ f π''  prefix_of π'' σ"
  using assms
  by transfer (auto intro!: exI[of _ "stake (length _) _"] elim: sym dest: sorted_stake)

lift_definition pts :: "'a prefix  nat list" is "map snd" .

lemma pts_pmap_Γ[simp]: "pts (pmap_Γ f π) = pts π"
  by (transfer fixing: f) (simp add: split_beta)

(*<*)
end
(*>*)

Theory Table

(*<*)
theory Table
  imports Main
begin
(*>*)

section ‹Finite tables›

primrec tabulate :: "(nat  'a)  nat  nat  'a list" where
  "tabulate f x 0 = []"
| "tabulate f x (Suc n) = f x # tabulate f (Suc x) n"

lemma tabulate_alt: "tabulate f x n = map f [x ..< x + n]"
  by (induct n arbitrary: x) (auto simp: not_le Suc_le_eq upt_rec)

lemma length_tabulate[simp]: "length (tabulate f x n) = n"
  by (induction n arbitrary: x) simp_all

lemma map_tabulate[simp]: "map f (tabulate g x n) = tabulate (λx. f (g x)) x n"
  by (induction n arbitrary: x) simp_all

lemma nth_tabulate[simp]: "k < n  tabulate f x n ! k = f (x + k)"
proof (induction n arbitrary: x k)
  case (Suc n)
  then show ?case by (cases k) simp_all
qed simp

type_synonym 'a tuple = "'a option list"
type_synonym 'a table = "'a tuple set"

definition wf_tuple :: "nat  nat set  'a tuple  bool" where
  "wf_tuple n V x  length x = n  (i<n. x!i = None  i  V)"

definition table :: "nat  nat set  'a table  bool" where
  "table n V X  (xX. wf_tuple n V x)"

definition "empty_table = {}"

definition "unit_table n = {replicate n None}"

definition "singleton_table n i x = {tabulate (λj. if i = j then Some x else None) 0 n}"

lemma in_empty_table[simp]: "¬ x  empty_table"
  unfolding empty_table_def by simp

lemma empty_table[simp]: "table n V empty_table"
  unfolding table_def empty_table_def by simp

lemma unit_table_wf_tuple[simp]: "V = {}  x  unit_table n  wf_tuple n V x"
  unfolding unit_table_def wf_tuple_def by simp

lemma unit_table[simp]: "V = {}  table n V (unit_table n)"
  unfolding table_def by simp

lemma in_unit_table: "v  unit_table n  wf_tuple n {} v"
  unfolding unit_table_def wf_tuple_def by (auto intro!: nth_equalityI)

lemma singleton_table_wf_tuple[simp]: "V = {i}  x  singleton_table n i z  wf_tuple n V x"
  unfolding singleton_table_def wf_tuple_def by simp

lemma singleton_table[simp]: "V = {i}  table n V (singleton_table n i z)"
  unfolding table_def by simp

lemma table_Un[simp]: "table n V X  table n V Y  table n V (X  Y)"
  unfolding table_def by auto

lemma wf_tuple_length: "wf_tuple n V x  length x = n"
  unfolding wf_tuple_def by simp


fun join1 :: "'a tuple × 'a tuple  'a tuple option" where
  "join1 ([], []) = Some []"
| "join1 (None # xs, None # ys) = map_option (Cons None) (join1 (xs, ys))"
| "join1 (Some x # xs, None # ys) = map_option (Cons (Some x)) (join1 (xs, ys))"
| "join1 (None # xs, Some y # ys) = map_option (Cons (Some y)) (join1 (xs, ys))"
| "join1 (Some x # xs, Some y # ys) = (if x = y
    then map_option (Cons (Some x)) (join1 (xs, ys))
    else None)"
| "join1 _ = None"

definition join :: "'a table  bool  'a table  'a table" where
  "join A pos B = (if pos then Option.these (join1 ` (A × B))
    else A - Option.these (join1 ` (A × B)))"

lemma join_True_code[code]: "join A True B = (a  A. b  B. set_option (join1 (a, b)))"
  unfolding join_def by (force simp: Option.these_def image_iff)

lemma join_False_alt: "join X False Y = X - join X True Y"
  unfolding join_def by auto

lemma self_join1: "join1 (xs, ys)  Some xs  join1 (zs, ys)  Some xs"
  by (induct "(zs, ys)" arbitrary: zs ys xs rule: join1.induct; auto; auto)

lemma join_False_code[code]: "join A False B = {a  A. b  B. join1 (a, b)  Some a}"
  unfolding join_False_alt join_True_code
  by (auto simp: Option.these_def image_iff dest: self_join1)

lemma wf_tuple_Nil[simp]: "wf_tuple n A [] = (n = 0)"
  unfolding wf_tuple_def by auto

lemma Suc_pred': "Suc (x - Suc 0) = (case x of 0  Suc 0 | _  x)"
  by (auto split: nat.splits)

lemma wf_tuple_Cons[simp]:
  "wf_tuple n A (x # xs)  ((if x = None then 0  A else 0  A) 
   (m. n = Suc m  wf_tuple m ((λx. x - 1) ` (A - {0})) xs))"
  unfolding wf_tuple_def
  by (auto 0 3 simp: nth_Cons image_iff Ball_def gr0_conv_Suc Suc_pred' split: nat.splits)

lemma join1_wf_tuple:
  "join1 (v1, v2) = Some v  wf_tuple n A v1  wf_tuple n B v2  wf_tuple n (A  B) v"
  by (induct "(v1, v2)" arbitrary: n v v1 v2 A B rule: join1.induct)
    (auto simp: image_Un Un_Diff split: if_splits)

lemma join_wf_tuple: "x  join X b Y 
  v  X. wf_tuple n A v  v  Y. wf_tuple n B v  (¬ b  B  A)  A  B = C  wf_tuple n C x"
  unfolding join_def
  by (fastforce simp: Option.these_def image_iff sup_absorb1 dest: join1_wf_tuple split: if_splits)

lemma join_table: "table n A X  table n B Y  (¬ b  B  A)  A  B = C 
  table n C (join X b Y)"
  unfolding table_def by (auto elim!: join_wf_tuple)

lemma wf_tuple_Suc: "wf_tuple (Suc m) A a  a  [] 
   wf_tuple m ((λx. x - 1) ` (A - {0})) (tl a)  (0  A  hd a  None)"
  by (cases a) (auto simp: nth_Cons image_iff split: nat.splits)

lemma table_project: "table (Suc n) A X  table n ((λx. x - Suc 0) ` (A - {0})) (tl ` X)"
  unfolding table_def
  by (auto simp: wf_tuple_Suc)

definition restrict where
  "restrict A v = map (λi. if i  A then v ! i else None) [0 ..< length v]"

lemma restrict_Nil[simp]: "restrict A [] = []"
  unfolding restrict_def by auto

lemma restrict_Cons[simp]: "restrict A (x # xs) =
  (if 0  A then x # restrict ((λx. x - 1) ` (A - {0})) xs else None # restrict ((λx. x - 1) ` A) xs)"
  unfolding restrict_def
  by (auto simp: map_upt_Suc image_iff Suc_pred' Ball_def simp del: upt_Suc split: nat.splits)

lemma wf_tuple_restrict: "wf_tuple n B v  A  B = C  wf_tuple n C (restrict A v)"
  unfolding restrict_def wf_tuple_def by auto

lemma wf_tuple_restrict_simple: "wf_tuple n B v  A  B  wf_tuple n A (restrict A v)"
  unfolding restrict_def wf_tuple_def by auto

lemma nth_restrict: "i  A  i < length v  restrict A v ! i = v ! i"
  unfolding restrict_def by auto

lemma restrict_eq_Nil[simp]: "restrict A v = []  v = []"
  unfolding restrict_def by auto

lemma length_restrict[simp]: "length (restrict A v) = length v"
  unfolding restrict_def by auto

lemma join1_Some_restrict:
  fixes x y :: "'a tuple"
  assumes "wf_tuple n A x" "wf_tuple n B y"
  shows "join1 (x, y) = Some z  wf_tuple n (A  B) z  restrict A z = x  restrict B z = y"
  using assms
proof (induct "(x, y)" arbitrary: n x y z A B rule: join1.induct)
  case (2 xs ys)
  then show ?case
    by (cases z) (auto 4 0 simp: image_Un Un_Diff)+
next
  case (3 x xs ys)
  then show ?case
    by (cases z) (auto 4 0 simp: image_Un Un_Diff)+
next
  case (4 xs y ys)
  then show ?case
    by (cases z) (auto 4 0 simp: image_Un Un_Diff)+
next
  case (5 x xs y ys)
  then show ?case
    by (cases z) (auto 4 0 simp: image_Un Un_Diff)+
qed auto

lemma restrict_idle: "wf_tuple n A v  restrict A v = v"
  by (induct v arbitrary: n A) (auto split: if_splits)

lemma map_the_restrict:
  "i  A  map the (restrict A v) ! i = map the v ! i"
  by (induct v arbitrary: A i) (auto simp: nth_Cons' gr0_conv_Suc split: option.splits)

lemma join_restrict:
  fixes X Y :: "'a tuple set"
  assumes "v. v  X  wf_tuple n A v" "v. v  Y  wf_tuple n B v" "¬ b  B  A"
  shows "v  join X b Y 
    wf_tuple n (A  B) v  restrict A v  X  (if b then restrict B v  Y else restrict B v  Y)"
  by (auto 4 4 simp: join_def Option.these_def image_iff assms wf_tuple_restrict sup_absorb1 restrict_idle
    restrict_idle[OF assms(1)] elim: assms
    dest: join1_Some_restrict[OF assms(1,2), THEN iffD1, rotated -1]
    dest!: spec[of _ "Some v"]
    intro!: exI[of _ "Some v"] join1_Some_restrict[THEN iffD2, symmetric] bexI[rotated])

lemma join_restrict_table:
  assumes "table n A X" "table n B Y" "¬ b  B  A"
  shows "v  join X b Y 
    wf_tuple n (A  B) v  restrict A v  X  (if b then restrict B v  Y else restrict B v  Y)"
  using assms unfolding table_def
  by (simp add: join_restrict)

lemma join_restrict_annotated:
  fixes X Y :: "'a tuple set"
  assumes "¬ b =simp=> B  A"
  shows "join {v. wf_tuple n A v  P v} b {v. wf_tuple n B v  Q v} =
    {v. wf_tuple n (A  B) v  P (restrict A v)  (if b then Q (restrict B v) else ¬ Q (restrict B v))}"
  using assms
  by (intro set_eqI, subst join_restrict) (auto simp: wf_tuple_restrict_simple simp_implies_def)

lemma in_joinI: "table n A X  table n B Y  (¬b  B  A)  wf_tuple n (A  B) v 
  restrict A v  X  (b  restrict B v  Y)  (¬b  restrict B v  Y)  v  join X b Y"
  unfolding table_def
  by (subst join_restrict) (auto)

lemma in_joinE: "v  join X b Y  table n A X  table n B Y  (¬ b  B  A) 
  (wf_tuple n (A  B) v  restrict A v  X  if b then restrict B v  Y else restrict B v  Y  P)  P"
  unfolding table_def
  by (subst (asm) join_restrict) (auto)

definition qtable :: "nat  nat set  ('a tuple  bool)  ('a tuple  bool) 
  'a table  bool" where
  "qtable n A P Q X  table n A X  (x. (x  X  P x  Q x)  (wf_tuple n A x  P x  Q x  x  X))"

abbreviation wf_table where
  "wf_table n A Q X  qtable n A (λ_. True) Q X"

lemma wf_table_iff: "wf_table n A Q X  (x. x  X  (Q x  wf_tuple n A x))"
  unfolding qtable_def table_def by auto

lemma table_wf_table: "table n A X = wf_table n A (λv. v  X) X"
  unfolding table_def wf_table_iff by auto

lemma qtableI: "table n A X 
  (x. x  X  wf_tuple n A x  P x  Q x) 
  (x. wf_tuple n A x  P x  Q x  x  X) 
  qtable n A P Q X"
  unfolding qtable_def table_def by auto

lemma in_qtableI: "qtable n A P Q X  wf_tuple n A x  P x  Q x  x  X"
  unfolding qtable_def by blast

lemma in_qtableE: "qtable n A P Q X  x  X  P x  (wf_tuple n A x  Q x  R)  R"
  unfolding qtable_def table_def by blast

lemma qtable_empty: "(x. wf_tuple n A x  P x  Q x  False)  qtable n A P Q empty_table"
  unfolding qtable_def table_def empty_table_def by auto

lemma qtable_empty_iff: "qtable n A P Q empty_table = (x. wf_tuple n A x  P x  Q x  False)"
  unfolding qtable_def table_def empty_table_def by auto

lemma qtable_unit_table: "(x. wf_tuple n {} x  P x  Q x)  qtable n {} P Q (unit_table n)"
  unfolding qtable_def table_def in_unit_table by auto

lemma qtable_union: "qtable n A P Q1 X  qtable n A P Q2 Y 
  (x. wf_tuple n A x  P x  Q x  Q1 x  Q2 x)  qtable n A P Q (X  Y)"
  unfolding qtable_def table_def by blast

lemma qtable_Union: "finite I  (i. i  I  qtable n A P (Qi i) (Xi i)) 
  (x. wf_tuple n A x  P x  Q x  (i  I. Qi i x))  qtable n A P Q (i  I. Xi i)"
proof (induct I arbitrary: Q rule: finite_induct)
  case (insert i F)
  then show ?case
    by (auto intro!: qtable_union[where ?Q1.0 = "Qi i" and ?Q2.0 = "λx. iF. Qi i x"])
qed (auto intro!: qtable_empty[unfolded empty_table_def])

lemma qtable_join: 
  assumes "qtable n A P Q1 X" "qtable n B P Q2 Y" "¬ b  B  A" "C = A  B"
  "x. wf_tuple n C x  P x  P (restrict A x)  P (restrict B x)"
  "x. b  wf_tuple n C x  P x  Q x  Q1 (restrict A x)  Q2 (restrict B x)"
  "x. ¬ b  wf_tuple n C x  P x  Q x  Q1 (restrict A x)  ¬ Q2 (restrict B x)"
  shows "qtable n C P Q (join X b Y)"
proof (rule qtableI)
  from assms(1-4) show "table n C (join X b Y)" 
    unfolding qtable_def by (auto simp: join_table)
next
  fix x assume "x  join X b Y" "wf_tuple n C x" "P x"
  with assms(1-3) assms(5-7)[of x] show "Q x" unfolding qtable_def
    by (auto 0 2 simp: wf_tuple_restrict_simple elim!: in_joinE split: if_splits)
next
  fix x assume "wf_tuple n C x" "P x" "Q x"
  with assms(1-4) assms(5-7)[of x] show "x  join X b Y" unfolding qtable_def
    by (auto dest: wf_tuple_restrict_simple intro!: in_joinI[of n A X B Y])
qed

lemma qtable_join_fixed: 
  assumes "qtable n A P Q1 X" "qtable n B P Q2 Y" "¬ b  B  A" "C = A  B"
  "x. wf_tuple n C x  P x  P (restrict A x)  P (restrict B x)"
  shows "qtable n C P (λx. Q1 (restrict A x)  (if b then Q2 (restrict B x) else ¬ Q2 (restrict B x))) (join X b Y)"
  by (rule qtable_join[OF assms]) auto

lemma wf_tuple_cong:
  assumes "wf_tuple n A v" "wf_tuple n A w" "x  A. map the v ! x = map the w ! x"
  shows "v = w"
proof -
  from assms(1,2) have "length v = length w" unfolding wf_tuple_def by simp
  from this assms show "v = w"
  proof (induct v w arbitrary: n A rule: list_induct2)
    case (Cons x xs y ys)
    let ?n = "n - 1" and ?A = "(λx. x - 1) ` (A - {0})"
    have *: "map the xs ! z = map the ys ! z" if "z  ?A" for z
      using that Cons(5)[THEN bspec, of "Suc z"]
      by (cases z) (auto simp: le_Suc_eq split: if_splits)
    from Cons(1,3-5) show ?case
      by (auto intro!: Cons(2)[of ?n ?A] * split: if_splits)
  qed simp
qed

definition mem_restr :: "'a list set  'a tuple  bool" where
  "mem_restr A x  (yA. list_all2 (λa b. a  None  a = Some b) x y)"

lemma mem_restrI: "y  A  length y = n  wf_tuple n V x  iV. x ! i = Some (y ! i)  mem_restr A x"
  unfolding mem_restr_def wf_tuple_def by (force simp add: list_all2_conv_all_nth)

lemma mem_restrE: "mem_restr A x  wf_tuple n V x  iV. i < n 
  (y. y  A  iV. x ! i = Some (y ! i)  P)  P"
  unfolding mem_restr_def wf_tuple_def by (fastforce simp add: list_all2_conv_all_nth)

lemma mem_restr_IntD: "mem_restr (A  B) v  mem_restr A v  mem_restr B v"
  unfolding mem_restr_def by auto

lemma mem_restr_Un_iff: "mem_restr (A  B) x  mem_restr A x  mem_restr B x"
  unfolding mem_restr_def by blast

lemma mem_restr_UNIV [simp]: "mem_restr UNIV x"
  unfolding mem_restr_def
  by (auto simp add: list.rel_map intro!: exI[of _ "map the x"] list.rel_refl)

lemma restrict_mem_restr[simp]: "mem_restr A x  mem_restr A (restrict V x)"
  unfolding mem_restr_def restrict_def
  by (auto simp: list_all2_conv_all_nth elim!: bexI[rotated])

definition lift_envs :: "'a list set  'a list set" where
  "lift_envs R = (λ(a,b). a # b) ` (UNIV × R)"

lemma lift_envs_mem_restr[simp]: "mem_restr A x  mem_restr (lift_envs A) (a # x)"
  by (auto simp: mem_restr_def lift_envs_def)

lemma qtable_project:
  assumes "qtable (Suc n) A (mem_restr (lift_envs R)) P X"
  shows "qtable n ((λx. x - Suc 0) ` (A - {0})) (mem_restr R)
      (λv. x. P ((if 0  A then Some x else None) # v)) (tl ` X)"
      (is "qtable n ?A (mem_restr R) ?P ?X")
proof ((rule qtableI; (elim exE)?), goal_cases table left right)
  case table
  with assms show ?case
    unfolding qtable_def by (simp add: table_project) 
next
  case (left v)
  from assms have "[]  X"
    unfolding qtable_def table_def by fastforce
  with left(1) obtain x where "x # v  X"
    by (metis (no_types, hide_lams) image_iff hd_Cons_tl)    
  with assms show ?case
    by (rule in_qtableE) (auto simp: left(3) split: if_splits)
next
  case (right v x)
  with assms have "(if 0  A then Some x else None) # v  X"
    by (elim in_qtableI) auto
  then show ?case
    by (auto simp: image_iff elim: bexI[rotated])
qed

lemma qtable_cong: "qtable n A P Q X  A = B  (v. P v  Q v  Q' v)  qtable n B P Q' X"
  by (auto simp: qtable_def)

(*<*)
end
(*>*)

Theory Abstract_Monitor

(*<*)
theory Abstract_Monitor
  imports Trace Table
begin
(*>*)

section ‹Abstract monitors and slicing›

subsection ‹First-order specifications›

text ‹
  We abstract from first-order trace specifications by referring only to their
  semantics. A first-order specification is described by a finite set of free
  variables and a satisfaction function that defines for every trace the pairs
  of valuations and time-points for which the specification is satisfied.
›

locale fo_spec =
  fixes
    nfv :: nat and fv :: "nat set" and
    sat :: "'a trace  'b list  nat  bool"
  assumes
    fv_less_nfv: "x  fv  x < nfv" and
    sat_fv_cong: "(x. x  fv  v!x = v'!x)  sat σ v i = sat σ v' i"
begin

definition verdicts :: "'a trace  (nat × 'b tuple) set" where
  "verdicts σ = {(i, v). wf_tuple nfv fv v  sat σ (map the v) i}"

end

text ‹
  We usually employ a monitor to find the ‹violations› of a specification.
  That is, the monitor should output the satisfactions of its negation.
  Moreover, all monitor implementations must work with finite prefixes.
  We are therefore interested in co-safety properties, which allow us to
  identify all satisfactions on finite prefixes.
›

locale cosafety_fo_spec = fo_spec +
  assumes cosafety_lr: "sat σ v i  π. prefix_of π σ  (σ'. prefix_of π σ'  sat σ' v i)"
begin

lemma cosafety: "sat σ v i  (π. prefix_of π σ  (σ'. prefix_of π σ'  sat σ' v i))"
  using cosafety_lr by blast

end

subsection ‹Monitor function›

text ‹
  We model monitors abstractly as functions from prefixes to verdict sets.
  The following locale specifies a minimal set of properties that any
  reasonable monitor should have.
›

locale monitor = fo_spec +
  fixes M :: "'a prefix  (nat × 'b tuple) set"
  assumes
    mono_monitor: "π  π'  M π  M π'" and
    wf_monitor: "(i, v)  M π  wf_tuple nfv fv v" and
    sound_monitor: "(i, v)  M π  prefix_of π σ  sat σ (map the v) i" and
    complete_monitor: "prefix_of π σ  wf_tuple nfv fv v 
      (σ. prefix_of π σ  sat σ (map the v) i)  π'. prefix_of π' σ  (i, v)  M π'"

text ‹
  A monitor for a co-safety specification computes precisely the set of all
  satisfactions in the limit:
›

abbreviation (in monitor) "M_limit σ  {M π | π. prefix_of π σ}"

locale cosafety_monitor = cosafety_fo_spec + monitor
begin

lemma M_limit_eq: "M_limit σ = verdicts σ"
proof
  show "{M π | π. prefix_of π σ}  verdicts σ"
    by (auto simp: verdicts_def wf_monitor sound_monitor)
next
  show "{M π | π. prefix_of π σ}  verdicts σ"
    unfolding verdicts_def
  proof safe
    fix i v
    assume "wf_tuple nfv fv v" and "sat σ (map the v) i"
    then obtain π where "prefix_of π σ  (σ'. prefix_of π σ'  sat σ' (map the v) i)"
      using cosafety_lr by blast
    with ‹wf_tuple nfv fv v obtain π' where "prefix_of π' σ  (i, v)  M π'"
      using complete_monitor by blast
    then show "(i, v)  {M π | π. prefix_of π σ}"
      by blast
  qed
qed

end

text ‹
  The monitor function termM adds some information over termsat, namely
  when a verdict is output. One possible behavior is that the monitor outputs
  its verdicts for one time-point at a time, in increasing order of
  time-points. Then termM is uniquely defined by a progress function, which
  returns for every prefix the time-point up to which all verdicts are computed.
›

locale progress = fo_spec _ _ sat for sat :: "'a trace  'b list  nat  bool" +
  fixes progress :: "'a prefix  nat"
  assumes
    progress_mono: "π  π'  progress π  progress π'" and
    ex_progress_ge: "π. prefix_of π σ  x  progress π" and
    progress_sat_cong: "prefix_of π σ  prefix_of π σ'  i < progress π 
      sat σ v i  sat σ' v i"
    ― ‹The last condition is not necessary to obtain a proper monitor function.
      However, it corresponds to the intuitive understanding of monitor progress,
      and it results in a stronger characterisation. In particular, it implies that
      the specification is co-safety, as we will show below.›
begin

definition M :: "'a prefix  (nat × 'b tuple) set" where
  "M π = {(i, v). i < progress π  wf_tuple nfv fv v 
    (σ. prefix_of π σ  sat σ (map the v) i)}"

lemma M_alt: "M π = {(i, v). i < progress π  wf_tuple nfv fv v 
    (σ. prefix_of π σ  sat σ (map the v) i)}"
  using ex_prefix_of[of π]
  by (auto simp: M_def cong: progress_sat_cong)

end

sublocale progress  cosafety_monitor _ _ _ M
proof
  fix i v and σ :: "'a trace"
  assume "sat σ v i"
  moreover obtain π where *: "prefix_of π σ" "i < progress π"
    using ex_progress_ge by (auto simp: less_eq_Suc_le)
  ultimately have "sat σ' v i" if "prefix_of π σ'" for σ'
    using that by (simp cong: progress_sat_cong)
  with * show "π. prefix_of π σ  (σ'. prefix_of π σ'  sat σ' v i)"
    by blast
next
  fix π π' :: "'a prefix"
  assume "π  π'"
  then show "M π  M π'"
    by (auto simp: M_def intro: progress_mono prefix_of_antimono
        elim: order.strict_trans2)
next
  fix i v π and σ :: "'a trace"
  assume *: "(i, v)  M π"
  then show "wf_tuple nfv fv v"
    by (simp add: M_def)
  assume "prefix_of π σ"
  with * show "sat σ (map the v) i"
    by (simp add: M_def)
next
  fix i v π and σ :: "'a trace"
  assume *: "prefix_of π σ" "wf_tuple nfv fv v" "σ'. prefix_of π σ'  sat σ' (map the v) i"
  show "π'. prefix_of π' σ  (i, v)  M π'"
  proof (cases "i < progress π")
    case True
    with * show ?thesis by (auto simp: M_def)
  next
    case False
    obtain π' where **: "prefix_of π' σ  i < progress π'"
      using ex_progress_ge by (auto simp: less_eq_Suc_le)
    then have "π  π'"
      using ‹prefix_of π σ prefix_of_imp_linear False progress_mono
      by (blast intro: order.strict_trans2)
    with * ** show ?thesis
      by (auto simp: M_def intro: prefix_of_antimono)
  qed
qed

subsection ‹Slicing›

text ‹Sliceable specifications can be evaluated meaningfully on a subset of events.›

locale abstract_slicer =
  fixes relevant_events :: "'b list set  'a set"
begin

abbreviation slice :: "'b list set  'a trace  'a trace" where
  "slice S  map_Γ (λD. D  relevant_events S)"

abbreviation pslice :: "'b list set  'a prefix  'a prefix" where
  "pslice S  pmap_Γ (λD. D  relevant_events S)"

lemma prefix_of_psliceI: "prefix_of π σ  prefix_of (pslice S π) (slice S σ)"
  by (transfer fixing: S) auto

lemma plen_pslice[simp]: "plen (pslice S π) = plen π"
  by (transfer fixing: S) simp

lemma pslice_pnil[simp]: "pslice S pnil = pnil"
  by (transfer fixing: S) simp

lemma last_ts_pslice[simp]: "last_ts (pslice S π) = last_ts π"
  by (transfer fixing: S) (simp add: last_map case_prod_beta split: list.split)

abbreviation verdict_filter :: "'b list set  (nat × 'b tuple) set  (nat × 'b tuple) set" where
  "verdict_filter S V  {(i, v)  V. mem_restr S v}"

end

locale sliceable_fo_spec = fo_spec _ _ sat + abstract_slicer relevant_events
  for relevant_events :: "'b list set  'a set" and sat :: "'a trace  'b list  nat  bool" +
  assumes sliceable: "v  S  sat (slice S σ) v i  sat σ v i"
begin

lemma union_verdicts_slice:
  assumes part: "𝒮 = UNIV"
  shows "((λS. verdict_filter S (verdicts (slice S σ))) ` 𝒮) = verdicts σ"
proof safe
  fix S i and v :: "'b tuple"
  assume "(i, v)  verdicts (slice S σ)"
  then have tuple: "wf_tuple nfv fv v" and "sat (slice S σ) (map the v) i"
    by (auto simp: verdicts_def)
  assume "mem_restr S v"
  then obtain v' where "v'  S" and 1: "ifv. v ! i = Some (v' ! i)"
    using tuple by (auto simp: fv_less_nfv elim: mem_restrE)
  then have "sat (slice S σ) v' i"
    using sat (slice S σ) (map the v) i tuple
    by (auto simp: wf_tuple_length fv_less_nfv cong: sat_fv_cong)
  then have "sat σ v' i"
    using sliceable[OF v'  S] by simp
  then have "sat σ (map the v) i"
    using tuple 1
    by (auto simp: wf_tuple_length fv_less_nfv cong: sat_fv_cong)
  then show "(i, v)  verdicts σ"
    using tuple by (simp add: verdicts_def)
next
  fix i and v :: "'b tuple"
  assume "(i, v)  verdicts σ"
  then have tuple: "wf_tuple nfv fv v" and "sat σ (map the v) i"
    by (auto simp: verdicts_def)
  from part obtain S where "S  𝒮" and "map the v  S"
    by blast
  then have "mem_restr S v"
    using mem_restrI[of "map the v" S nfv fv] tuple
    by (auto simp: wf_tuple_def fv_less_nfv)
  moreover have "sat (slice S σ) (map the v) i"
    using sat σ (map the v) i sliceable[OF ‹map the v  S] by simp
  then have "(i, v)  verdicts (slice S σ)"
    using tuple by (simp add: verdicts_def)
  ultimately show "(i, v)  (S𝒮. verdict_filter S (verdicts (slice S σ)))"
    using S  𝒮 by blast
qed

end

text ‹
  We define a similar notion for monitors. It is potentially stronger because
  the time-point at which verdicts are output must not change.
›

locale sliceable_monitor = monitor _ _ sat M + abstract_slicer relevant_events
  for relevant_events :: "'b list set  'a set" and sat :: "'a trace  'b list  nat  bool" and M +
  assumes sliceable_M: "mem_restr S v  (i, v)  M (pslice S π)  (i, v)  M π"
begin

lemma union_M_pslice:
  assumes part: "𝒮 = UNIV"
  shows "((λS. verdict_filter S (M (pslice S π))) ` 𝒮) = M π"
proof safe
  fix S i and v :: "'b tuple"
  assume "mem_restr S v" and "(i, v)  M (pslice S π)"
  then show "(i, v)  M π" using sliceable_M by blast
next
  fix i and v :: "'b tuple"
  assume "(i, v)  M π"
  then have tuple: "wf_tuple nfv fv v"
    by (rule wf_monitor)
  from part obtain S where "S  𝒮" and "map the v  S"
    by blast
  then have "mem_restr S v"
    using mem_restrI[of "map the v" S nfv fv] tuple
    by (auto simp: wf_tuple_def fv_less_nfv)
  then have "(i, v)  M (pslice S π)"
    using (i, v)  M π sliceable_M by blast
  then show "(i, v)  (S𝒮. verdict_filter S (M (pslice S π)))"
    using S  𝒮 ‹mem_restr S v by blast
qed

end

text ‹
  If the specification is sliceable and the monitor's progress depends only on
  time-stamps, then also the monitor itself is sliceable.
›

locale timed_progress = progress +
  assumes progress_time_conv: "pts π = pts π'  progress π = progress π'"

locale sliceable_timed_progress = sliceable_fo_spec + timed_progress
begin

lemma progress_pslice[simp]: "progress (pslice S π) = progress π"
  by (simp cong: progress_time_conv)

end

sublocale sliceable_timed_progress  sliceable_monitor _ _ _ _ M
proof
  fix S :: "'a list set" and v i π
  assume *: "mem_restr S v"
  show "(i, v)  M (pslice S π)  (i, v)  M π" (is "?L  ?R")
  proof
    assume ?L
    with * show ?R
      by (auto 0 4 simp: M_def wf_tuple_def elim!: mem_restrE
          box_equals[OF sliceable sat_fv_cong sat_fv_cong, THEN iffD1, rotated -1]
          intro: prefix_of_psliceI dest: fv_less_nfv spec[of _ "slice S _"])
  next
    assume ?R
    with * show ?L
      by (auto 0 4 simp: M_alt wf_tuple_def elim!: mem_restrE
        box_equals[OF sliceable sat_fv_cong sat_fv_cong, THEN iffD2, rotated -1]
        intro: exI[of _ "slice S _"] prefix_of_psliceI dest: fv_less_nfv)
  qed
qed

(*<*)
end
(*>*)

Theory Interval

(*<*)
theory Interval
  imports "HOL-Library.Extended_Nat" "HOL-Library.Product_Lexorder"
begin
(*>*)

section ‹Intervals›

typedef= "{(i :: nat, j :: enat). i  j}"
  by (intro exI[of _ "(0, )"]) auto

setup_lifting type_definition_ℐ

instantiation:: equal begin
lift_definition equal_ℐ :: "ℐ  bool" is "(=)" .
instance by standard (transfer, auto)
end

instantiation:: linorder begin
lift_definition less_eq_ℐ :: "ℐ  bool" is "(≤)" .
lift_definition less_ℐ :: "ℐ  bool" is "(<)" .
instance by standard (transfer, auto)+
end


lift_definition all ::  is "(0, )" by simp
lift_definition left :: "ℐ  nat" is fst .
lift_definition right :: "ℐ  enat" is snd .
lift_definition point :: "nat  ℐ" is "λn. (n, enat n)" by simp
lift_definition init :: "nat  ℐ" is "λn. (0, enat n)" by auto
abbreviation mem where "mem n I  (left I  n  n  right I)"
lift_definition subtract :: "nat  ℐ" is
  "λn (i, j). (i - n, j - enat n)" by (auto simp: diff_enat_def split: enat.splits)
lift_definition add :: "nat  ℐ" is
  "λn (a, b). (a, b + enat n)" by (auto simp add: add_increasing2)

lemma left_right: "left I  right I"
  by transfer auto

lemma point_simps[simp]:
  "left (point n) = n"
  "right (point n) = n"
  by (transfer; auto)+

lemma init_simps[simp]:
  "left (init n) = 0"
  "right (init n) = n"
  by (transfer; auto)+

lemma subtract_simps[simp]:
  "left (subtract n I) = left I - n"
  "right (subtract n I) = right I - n"
  "subtract 0 I = I"
  "subtract x (point y) = point (y - x)"
  by (transfer; auto)+

definition shifted :: "ℐ  ℐ set" where
  "shifted I = (λn. subtract n I) ` {0 .. (case right I of   left I | enat n  n)}"

lemma subtract_too_much: "i > (case right I of   left I | enat n  n) 
  subtract i I = subtract (case right I of   left I | enat n  n) I"
  by transfer (auto split: enat.splits)

lemma subtract_shifted: "subtract n I  shifted I"
  by (cases "n  (case right I of   left I | enat n  n)")
    (auto simp: shifted_def subtract_too_much)

lemma finite_shifted: "finite (shifted I)"
  unfolding shifted_def by auto

definition interval :: "nat  enat  ℐ" where
  "interval l r = (if l  r then Abs_ℐ (l, r) else undefined)"

lemma [code abstract]: "Rep_ℐ (interval l r) = (if l  r then (l, r) else Rep_ℐ undefined)"
  unfolding interval_def using Abs_ℐ_inverse by simp

(*<*)
end
(*>*)

Theory MFOTL

(*<*)
theory MFOTL
  imports Interval Trace Abstract_Monitor
begin
(*>*)

section ‹Metric first-order temporal logic›

context begin

subsection ‹Formulas and satisfiability›

qualified type_synonym name = string
qualified type_synonym 'a event = "(name × 'a list)"
qualified type_synonym 'a database = "'a event set"
qualified type_synonym 'a prefix = "(name × 'a list) prefix"
qualified type_synonym 'a trace = "(name × 'a list) trace"

qualified type_synonym 'a env = "'a list"

qualified datatype 'a trm = Var nat | is_Const: Const 'a

qualified primrec fvi_trm :: "nat  'a trm  nat set" where
  "fvi_trm b (Var x) = (if b  x then {x - b} else {})"
| "fvi_trm b (Const _) = {}"

abbreviation "fv_trm  fvi_trm 0"

qualified primrec eval_trm :: "'a env  'a trm  'a" where
  "eval_trm v (Var x) = v ! x"
| "eval_trm v (Const x) = x"

lemma eval_trm_cong: "xfv_trm t. v ! x = v' ! x  eval_trm v t = eval_trm v' t"
  by (cases t) simp_all

qualified datatype (discs_sels) 'a formula = Pred name "'a trm list" | Eq "'a trm" "'a trm"
  | Neg "'a formula" | Or "'a formula" "'a formula" | Exists "'a formula"
  | Prev  "'a formula" | Next  "'a formula"
  | Since "'a formula"  "'a formula" | Until "'a formula"  "'a formula"

qualified primrec fvi :: "nat  'a formula  nat set" where
  "fvi b (Pred r ts) = (tset ts. fvi_trm b t)"
| "fvi b (Eq t1 t2) = fvi_trm b t1  fvi_trm b t2"
| "fvi b (Neg φ) = fvi b φ"
| "fvi b (Or φ ψ) = fvi b φ  fvi b ψ"
| "fvi b (Exists φ) = fvi (Suc b) φ"
| "fvi b (Prev I φ) = fvi b φ"
| "fvi b (Next I φ) = fvi b φ"
| "fvi b (Since φ I ψ) = fvi b φ  fvi b ψ"
| "fvi b (Until φ I ψ) = fvi b φ  fvi b ψ"

abbreviation "fv  fvi 0"

lemma finite_fvi_trm[simp]: "finite (fvi_trm b t)"
  by (cases t) simp_all

lemma finite_fvi[simp]: "finite (fvi b φ)"
  by (induction φ arbitrary: b) simp_all

lemma fvi_trm_Suc: "x  fvi_trm (Suc b) t  Suc x  fvi_trm b t"
  by (cases t) auto

lemma fvi_Suc: "x  fvi (Suc b) φ  Suc x  fvi b φ"
  by (induction φ arbitrary: b) (simp_all add: fvi_trm_Suc)

lemma fvi_Suc_bound:
  assumes "ifvi (Suc b) φ. i < n"
  shows "ifvi b φ. i < Suc n"
proof
  fix i
  assume "i  fvi b φ"
  with assms show "i < Suc n" by (cases i) (simp_all add: fvi_Suc)
qed

qualified definition nfv :: "'a formula  nat" where
  "nfv φ = Max (insert 0 (Suc ` fv φ))"

qualified definition envs :: "'a formula  'a env set" where
  "envs φ = {v. length v = nfv φ}"

lemma nfv_simps[simp]:
  "nfv (Neg φ) = nfv φ"
  "nfv (Or φ ψ) = max (nfv φ) (nfv ψ)"
  "nfv (Prev I φ) = nfv φ"
  "nfv (Next I φ) = nfv φ"
  "nfv (Since φ I ψ) = max (nfv φ) (nfv ψ)"
  "nfv (Until φ I ψ) = max (nfv φ) (nfv ψ)"
  unfolding nfv_def by (simp_all add: image_Un Max_Un[symmetric])

lemma fvi_less_nfv: "ifv φ. i < nfv φ"
  unfolding nfv_def
  by (auto simp add: Max_gr_iff intro: max.strict_coboundedI2)


qualified primrec future_reach :: "'a formula  enat" where
  "future_reach (Pred _ _) = 0"
| "future_reach (Eq _ _) = 0"
| "future_reach (Neg φ) = future_reach φ"
| "future_reach (Or φ ψ) = max (future_reach φ) (future_reach ψ)"
| "future_reach (Exists φ) = future_reach φ"
| "future_reach (Prev I φ) = future_reach φ - left I"
| "future_reach (Next I φ) = future_reach φ + right I + 1"
| "future_reach (Since φ I ψ) = max (future_reach φ) (future_reach ψ - left I)"
| "future_reach (Until φ I ψ) = max (future_reach φ) (future_reach ψ) + right I + 1"


qualified primrec sat :: "'a trace  'a env  nat  'a formula  bool" where
  "sat σ v i (Pred r ts) = ((r, map (eval_trm v) ts)  Γ σ i)"
| "sat σ v i (Eq t1 t2) = (eval_trm v t1 = eval_trm v t2)"
| "sat σ v i (Neg φ) = (¬ sat σ v i φ)"
| "sat σ v i (Or φ ψ) = (sat σ v i φ  sat σ v i ψ)"
| "sat σ v i (Exists φ) = (z. sat σ (z # v) i φ)"
| "sat σ v i (Prev I φ) = (case i of 0  False | Suc j  mem (τ σ i - τ σ j) I  sat σ v j φ)"
| "sat σ v i (Next I φ) = (mem (τ σ (Suc i) - τ σ i) I  sat σ v (Suc i) φ)"
| "sat σ v i (Since φ I ψ) = (ji. mem (τ σ i - τ σ j) I  sat σ v j ψ  (k  {j <.. i}. sat σ v k φ))"
| "sat σ v i (Until φ I ψ) = (ji. mem (τ σ j - τ σ i) I  sat σ v j ψ  (k  {i ..< j}. sat σ v k φ))"

lemma sat_Until_rec: "sat σ v i (Until φ I ψ) 
  mem 0 I  sat σ v i ψ 
  (Δ σ (i + 1)  right I  sat σ v i φ  sat σ v (i + 1) (Until φ (subtract (Δ σ (i + 1)) I) ψ))"
  (is "?L  ?R")
proof (rule iffI; (elim disjE conjE)?)
  assume ?L
  then obtain j where j: "i  j" "mem (τ σ j - τ σ i) I" "sat σ v j ψ" "k  {i ..< j}. sat σ v k φ"
    by auto
  then show ?R
  proof (cases "i = j")
    case False
    with j(1,2) have σ (i + 1)  right I"
      by (auto elim: order_trans[rotated] simp: diff_le_mono)
    moreover from False j(1,4) have "sat σ v i φ" by auto
    moreover from False j have "sat σ v (i + 1) (Until φ (subtract (Δ σ (i + 1)) I) ψ)"
      by (cases "right I") (auto simp: le_diff_conv le_diff_conv2 intro!: exI[of _ j])
    ultimately show ?thesis by blast
  qed simp
next
  assume Δ: σ (i + 1)  right I" and now: "sat σ v i φ" and
   "next": "sat σ v (i + 1) (Until φ (subtract (Δ σ (i + 1)) I) ψ)"
  from "next" obtain j where j: "i + 1  j" "mem (τ σ j - τ σ (i + 1)) ((subtract (Δ σ (i + 1)) I))"
      "sat σ v j ψ" "k  {i + 1 ..< j}. sat σ v k φ"
    by auto
  from Δ j(1,2) have "mem (τ σ j - τ σ i) I"
    by (cases "right I") (auto simp: le_diff_conv2)
  with now j(1,3,4) show ?L by (auto simp: le_eq_less_or_eq[of i] intro!: exI[of _ j])
qed auto

lemma sat_Since_rec: "sat σ v i (Since φ I ψ) 
  mem 0 I  sat σ v i ψ 
  (i > 0  Δ σ i  right I  sat σ v i φ  sat σ v (i - 1) (Since φ (subtract (Δ σ i) I) ψ))"
  (is "?L  ?R")
proof (rule iffI; (elim disjE conjE)?)
  assume ?L
  then obtain j where j: "j  i" "mem (τ σ i - τ σ j) I" "sat σ v j ψ" "k  {j <.. i}. sat σ v k φ"
    by auto
  then show ?R
  proof (cases "i = j")
    case False
    with j(1) obtain k where [simp]: "i = k + 1"
      by (cases i) auto
    with j(1,2) False have σ i  right I"
      by (auto elim: order_trans[rotated] simp: diff_le_mono2 le_Suc_eq)
    moreover from False j(1,4) have "sat σ v i φ" by auto
    moreover from False j have "sat σ v (i - 1) (Since φ (subtract (Δ σ i) I) ψ)"
      by (cases "right I") (auto simp: le_diff_conv le_diff_conv2 intro!: exI[of _ j])
    ultimately show ?thesis by auto
  qed simp
next
  assume i: "0 < i" and Δ: σ i  right I" and now: "sat σ v i φ" and
   "prev": "sat σ v (i - 1) (Since φ (subtract (Δ σ i) I) ψ)"
  from "prev" obtain j where j: "j  i - 1" "mem (τ σ (i - 1) - τ σ j) ((subtract (Δ σ i) I))"
      "sat σ v j ψ" "k  {j <.. i - 1}. sat σ v k φ"
    by auto
  from Δ i j(1,2) have "mem (τ σ i - τ σ j) I"
    by (cases "right I") (auto simp: le_diff_conv2)
  with now i j(1,3,4) show ?L by (auto simp: le_Suc_eq gr0_conv_Suc intro!: exI[of _ j])
qed auto

lemma sat_Since_0: "sat σ v 0 (Since φ I ψ)  mem 0 I  sat σ v 0 ψ"
  by auto

lemma sat_Since_point: "sat σ v i (Since φ I ψ) 
    (j. j  i  mem (τ σ i - τ σ j) I  sat σ v i (Since φ (point (τ σ i - τ σ j)) ψ)  P)  P"
  by (auto intro: diff_le_self)

lemma sat_Since_pointD: "sat σ v i (Since φ (point t) ψ)  mem t I  sat σ v i (Since φ I ψ)"
  by auto

lemma eval_trm_fvi_cong: "xfv_trm t. v!x = v'!x  eval_trm v t = eval_trm v' t"
  by (cases t) simp_all

lemma sat_fvi_cong: "xfv φ. v!x = v'!x  sat σ v i φ = sat σ v' i φ"
proof (induct φ arbitrary: v v' i)
  case (Pred n ts)
  show ?case by (simp cong: map_cong eval_trm_fvi_cong[OF Pred[simplified, THEN bspec]])
next
  case (Eq x1 x2)
  then show ?case  unfolding fvi.simps sat.simps by (metis UnCI eval_trm_fvi_cong)
next
  case (Exists φ)
  then show ?case unfolding sat.simps by (intro iff_exI) (simp add: fvi_Suc nth_Cons')
qed (auto 8 0 simp add: nth_Cons' split: nat.splits intro!: iff_exI)


subsection ‹Defined connectives›

qualified definition "And φ ψ = Neg (Or (Neg φ) (Neg ψ))"

lemma fvi_And: "fvi b (And φ ψ) = fvi b φ  fvi b ψ"
  unfolding And_def by simp

lemma nfv_And[simp]: "nfv (And φ ψ) = max (nfv φ) (nfv ψ)"
  unfolding nfv_def by (simp add: fvi_And image_Un Max_Un[symmetric])

lemma future_reach_And: "future_reach (And φ ψ) = max (future_reach φ) (future_reach ψ)"
  unfolding And_def by simp

lemma sat_And: "sat σ v i (And φ ψ) = (sat σ v i φ  sat σ v i ψ)"
  unfolding And_def by simp

qualified definition "And_Not φ ψ = Neg (Or (Neg φ) ψ)"

lemma fvi_And_Not: "fvi b (And_Not φ ψ) = fvi b φ  fvi b ψ"
  unfolding And_Not_def by simp

lemma nfv_And_Not[simp]: "nfv (And_Not φ ψ) = max (nfv φ) (nfv ψ)"
  unfolding nfv_def by (simp add: fvi_And_Not image_Un Max_Un[symmetric])

lemma future_reach_And_Not: "future_reach (And_Not φ ψ) = max (future_reach φ) (future_reach ψ)"
  unfolding And_Not_def by simp

lemma sat_And_Not: "sat σ v i (And_Not φ ψ) = (sat σ v i φ  ¬ sat σ v i ψ)"
  unfolding And_Not_def by simp


subsection ‹Safe formulas›

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

lemma disjE_Not2: "P  Q  (P  R)  (¬P  Q  R)  R"
  by blast

lemma safe_formula_induct[consumes 1]:
  assumes "safe_formula φ"
    and "t1 t2. MFOTL.is_Const t1  P (MFOTL.Eq t1 t2)"
    and "t1 t2. MFOTL.is_Const t2  P (MFOTL.Eq t1 t2)"
    and "x y. P (MFOTL.Neg (MFOTL.Eq (MFOTL.Const x) (MFOTL.Const y)))"
    and "x y. x = y  P (MFOTL.Neg (MFOTL.Eq (MFOTL.Var x) (MFOTL.Var y)))"
    and "e ts. P (MFOTL.Pred e ts)"
    and "φ ψ. ¬ (safe_formula (MFOTL.Neg ψ)  MFOTL.fv ψ  MFOTL.fv φ)  P φ  P ψ  P (MFOTL.And φ ψ)"
    and "φ ψ. safe_formula ψ  MFOTL.fv ψ  MFOTL.fv φ  P φ  P ψ  P (MFOTL.And_Not φ ψ)"
    and "φ ψ. MFOTL.fv ψ = MFOTL.fv φ  P φ  P ψ  P (MFOTL.Or φ ψ)"
    and "φ. P φ  P (MFOTL.Exists φ)"
    and "I φ. P φ  P (MFOTL.Prev I φ)"
    and "I φ. P φ  P (MFOTL.Next I φ)"
    and "φ I ψ. MFOTL.fv φ  MFOTL.fv ψ  safe_formula φ  P φ  P ψ  P (MFOTL.Since φ I ψ)"
    and "φ I ψ. MFOTL.fv (MFOTL.Neg φ)  MFOTL.fv ψ 
      ¬ safe_formula (MFOTL.Neg φ)  P φ  P ψ  P (MFOTL.Since (MFOTL.Neg φ) I ψ )"
    and "φ I ψ. MFOTL.fv φ  MFOTL.fv ψ  safe_formula φ  P φ  P ψ  P (MFOTL.Until φ I ψ)"
    and "φ I ψ. MFOTL.fv (MFOTL.Neg φ)  MFOTL.fv ψ 
      ¬ safe_formula (MFOTL.Neg φ)  P φ  P ψ  P (MFOTL.Until (MFOTL.Neg φ) I ψ)"
  shows "P φ"
  using assms(1)
proof (induction rule: safe_formula.induct)
  case (5 φ ψ)
  then show ?case
    by (cases ψ)
      (auto 0 3 elim!: disjE_Not2 intro: assms[unfolded MFOTL.And_def MFOTL.And_Not_def])
next
  case (10 φ I ψ)
  then show ?case
    by (cases φ) (auto 0 3 elim!: disjE_Not2 intro: assms)
next
  case (11 φ I ψ)
  then show ?case
    by (cases φ) (auto 0 3 elim!: disjE_Not2 intro: assms)
qed (auto intro: assms)


subsection ‹Slicing traces›

qualified primrec matches :: "'a env  'a formula  name × 'a list  bool" where
  "matches v (Pred r ts) e = (r = fst e  map (eval_trm v) ts = snd e)"
| "matches v (Eq _ _) e = False"
| "matches v (Neg φ) e = matches v φ e"
| "matches v (Or φ ψ) e = (matches v φ e  matches v ψ e)"
| "matches v (Exists φ) e = (z. matches (z # v) φ e)"
| "matches v (Prev I φ) e = matches v φ e"
| "matches v (Next I φ) e = matches v φ e"
| "matches v (Since φ I ψ) e = (matches v φ e  matches v ψ e)"
| "matches v (Until φ I ψ) e = (matches v φ e  matches v ψ e)"

lemma matches_fvi_cong: "xfv φ. v!x = v'!x  matches v φ e = matches v' φ e"
proof (induct φ arbitrary: v v')
  case (Pred n ts)
  show ?case by (simp cong: map_cong eval_trm_fvi_cong[OF Pred[simplified, THEN bspec]])
next
  case (Exists φ)
  then show ?case unfolding matches.simps by (intro iff_exI) (simp add: fvi_Suc nth_Cons')
qed (auto 5 0 simp add: nth_Cons')

abbreviation relevant_events where "relevant_events φ S  {e. S  {v. matches v φ e}  {}}"

lemma sat_slice_strong: "relevant_events φ S  E  v  S 
  sat σ v i φ  sat (map_Γ (λD. D  E) σ) v i φ"
proof (induction φ arbitrary: v S i)
  case (Pred r ts)
  then show ?case by (auto simp: subset_eq)
next
  case (Eq t1 t2)
  show ?case
    unfolding sat.simps
    by simp
next
  case (Neg φ)
  then show ?case by simp
next
  case (Or φ ψ)
  show ?case using Or.IH[of S] Or.prems
    by (auto simp: Collect_disj_eq Int_Un_distrib subset_iff)
next
  case (Exists φ)
  have "sat σ (z # v) i φ = sat (map_Γ (λD. D  E) σ) (z # v) i φ" for z
    using Exists.prems by (auto intro!: Exists.IH[of "{z # v | v. v  S}"])
  then show ?case by simp
next
  case (Prev I φ)
  then show ?case by (auto cong: nat.case_cong)
next
  case (Next I φ)
  then show ?case by simp
next
  case (Since φ I ψ)
  show ?case using Since.IH[of S] Since.prems
   by (auto simp: Collect_disj_eq Int_Un_distrib subset_iff)
next
  case (Until φ I ψ)
  show ?case using Until.IH[of S] Until.prems
   by (auto simp: Collect_disj_eq Int_Un_distrib subset_iff)
qed

end (*context*)

interpretation MFOTL_slicer: abstract_slicer "relevant_events φ" for φ .

lemma sat_slice_iff:
  assumes "v  S"
  shows "MFOTL.sat σ v i φ  MFOTL.sat (MFOTL_slicer.slice φ S σ) v i φ"
  by (rule sat_slice_strong[of S, OF subset_refl assms])

lemma slice_replace_prefix:
  "prefix_of (MFOTL_slicer.pslice φ R π) σ 
    MFOTL_slicer.slice φ R (replace_prefix π σ) = MFOTL_slicer.slice φ R σ"
  by (rule map_Γ_replace_prefix) auto

(*<*)
end
(*>*)

Theory Monitor

(*<*)
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  "'a mformula" bool "'a table list" "ts list"
  | MNext  "'a mformula" bool "ts list"
  | MSince bool "'a mformula"  "'a mformula" "'a mbuf2" "ts list" "'a msaux"
  | MUntil bool "'a mformula"  "'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 :: "ℐ  '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 :: "ℐ  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 :: "ℐ  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 :: "ℐ  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  '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  '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 
    xMFOTL.fv_trm t1. x < n  xMFOTL.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: "xMFOTL.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 φ  xMFOTL.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 (tset 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  tset 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: "tset ts. iMFOTL.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 (tset ts. MFOTL.fv_trm t) v  tset ts. xMFOTL.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  (tset 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 
  xMFOTL.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.
        (ji. 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