Theory Formula

(*<*)
theory Formula
  imports
    Event_Data
    Regex
    "MFOTL_Monitor.Interval"
    "MFOTL_Monitor.Trace"
    "MFOTL_Monitor.Abstract_Monitor"
    "HOL-Library.Mapping"
    Containers.Set_Impl
begin
(*>*)

section ‹Metric first-order dynamic logic›

derive (eq) ceq enat

instantiation enat :: ccompare begin
definition ccompare_enat :: "enat comparator option" where
  "ccompare_enat = Some (λx y. if x = y then order.Eq else if x < y then order.Lt else order.Gt)"

instance by intro_classes
    (auto simp: ccompare_enat_def split: if_splits intro!: comparator.intro)
end

context begin

subsection ‹Formulas and satisfiability›

qualified type_synonym name = String.literal
qualified type_synonym event = "(name × event_data list)"
qualified type_synonym database = "(name, event_data list set list) mapping"
qualified type_synonym prefix = "(name × event_data list) prefix"
qualified type_synonym trace = "(name × event_data list) trace"

qualified type_synonym env = "event_data list"

subsubsection ‹Syntax›

qualified datatype trm = is_Var: Var nat | is_Const: Const event_data
  | Plus trm trm | Minus trm trm | UMinus trm | Mult trm trm | Div trm trm | Mod trm trm
  | F2i trm | I2f trm

qualified primrec fvi_trm :: "nat ⇒ trm ⇒ nat set" where
  "fvi_trm b (Var x) = (if b ≤ x then {x - b} else {})"
| "fvi_trm b (Const _) = {}"
| "fvi_trm b (Plus x y) = fvi_trm b x ∪ fvi_trm b y"
| "fvi_trm b (Minus x y) = fvi_trm b x ∪ fvi_trm b y"
| "fvi_trm b (UMinus x) = fvi_trm b x"
| "fvi_trm b (Mult x y) = fvi_trm b x ∪ fvi_trm b y"
| "fvi_trm b (Div x y) = fvi_trm b x ∪ fvi_trm b y"
| "fvi_trm b (Mod x y) = fvi_trm b x ∪ fvi_trm b y"
| "fvi_trm b (F2i x) = fvi_trm b x"
| "fvi_trm b (I2f x) = fvi_trm b x"

abbreviation "fv_trm ≡ fvi_trm 0"

qualified primrec eval_trm :: "env ⇒ trm ⇒ event_data" where
  "eval_trm v (Var x) = v ! x"
| "eval_trm v (Const x) = x"
| "eval_trm v (Plus x y) = eval_trm v x + eval_trm v y"
| "eval_trm v (Minus x y) = eval_trm v x - eval_trm v y"
| "eval_trm v (UMinus x) = - eval_trm v x"
| "eval_trm v (Mult x y) = eval_trm v x * eval_trm v y"
| "eval_trm v (Div x y) = eval_trm v x div eval_trm v y"
| "eval_trm v (Mod x y) = eval_trm v x mod eval_trm v y"
| "eval_trm v (F2i x) = EInt (integer_of_event_data (eval_trm v x))"
| "eval_trm v (I2f x) = EFloat (double_of_event_data (eval_trm v x))"

lemma eval_trm_fv_cong: "∀x∈fv_trm t. v ! x = v' ! x ⟹ eval_trm v t = eval_trm v' t"
  by (induction t) simp_all


qualified datatype agg_type = Agg_Cnt | Agg_Min | Agg_Max | Agg_Sum | Agg_Avg | Agg_Med
qualified type_synonym agg_op = "agg_type × event_data"

definition flatten_multiset :: "(event_data × enat) set ⇒ event_data list" where
  "flatten_multiset M = concat (map (λ(x, c). replicate (the_enat c) x) (csorted_list_of_set M))"

fun eval_agg_op :: "agg_op ⇒ (event_data × enat) set ⇒ event_data" where
  "eval_agg_op (Agg_Cnt, y0) M = EInt (integer_of_int (length (flatten_multiset M)))"
| "eval_agg_op (Agg_Min, y0) M = (case flatten_multiset M of
      [] ⇒ y0
    | x # xs ⇒ foldl min x xs)"
| "eval_agg_op (Agg_Max, y0) M = (case flatten_multiset M of
      [] ⇒ y0
    | x # xs ⇒ foldl max x xs)"
| "eval_agg_op (Agg_Sum, y0) M = foldl plus y0 (flatten_multiset M)"
| "eval_agg_op (Agg_Avg, y0) M = EFloat (let xs = flatten_multiset M in case xs of
      [] ⇒ 0
    | _ ⇒ double_of_event_data (foldl plus (EInt 0) xs) / double_of_int (length xs))"
| "eval_agg_op (Agg_Med, y0) M = EFloat (let xs = flatten_multiset M; u = length xs in
    if u = 0 then 0 else
      let u' = u div 2 in
      if even u then
        (double_of_event_data (xs ! (u'-1)) + double_of_event_data (xs ! u')) / double_of_int 2
      else double_of_event_data (xs ! u'))"

qualified datatype (discs_sels) formula = Pred name "trm list"
  | Let name formula formula
  | Eq trm trm | Less trm trm | LessEq trm trm
  | Neg formula | Or formula formula | And formula formula | Ands "formula list" | Exists formula
  | Agg nat agg_op nat trm formula
  | Prev ℐ formula | Next ℐ formula
  | Since formula ℐ formula | Until formula ℐ formula
  | MatchF ℐ "formula Regex.regex" | MatchP ℐ "formula Regex.regex"

qualified definition "FF = Exists (Neg (Eq (Var 0) (Var 0)))"
qualified definition "TT ≡ Neg FF"

qualified fun fvi :: "nat ⇒ formula ⇒ nat set" where
  "fvi b (Pred r ts) = (⋃t∈set ts. fvi_trm b t)"
| "fvi b (Let p φ ψ) = fvi b ψ"
| "fvi b (Eq t1 t2) = fvi_trm b t1 ∪ fvi_trm b t2"
| "fvi b (Less t1 t2) = fvi_trm b t1 ∪ fvi_trm b t2"
| "fvi b (LessEq t1 t2) = fvi_trm b t1 ∪ fvi_trm b t2"
| "fvi b (Neg φ) = fvi b φ"
| "fvi b (Or φ ψ) = fvi b φ ∪ fvi b ψ"
| "fvi b (And φ ψ) = fvi b φ ∪ fvi b ψ"
| "fvi b (Ands φs) = (let xs = map (fvi b) φs in ⋃x∈set xs. x)"
| "fvi b (Exists φ) = fvi (Suc b) φ"
| "fvi b (Agg y ω b' f φ) = fvi (b + b') φ ∪ fvi_trm (b + b') f ∪ (if b ≤ y then {y - b} else {})"
| "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 ψ"
| "fvi b (MatchF I r) = Regex.fv_regex (fvi b) r"
| "fvi b (MatchP I r) = Regex.fv_regex (fvi b) r"

abbreviation "fv ≡ fvi 0"
abbreviation "fv_regex ≡ Regex.fv_regex fv"

lemma fv_abbrevs[simp]: "fv TT = {}" "fv FF = {}"
  unfolding TT_def FF_def by auto

lemma fv_subset_Ands: "φ ∈ set φs ⟹ fv φ ⊆ fv (Ands φs)"
  by auto

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

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

lemma fvi_trm_plus: "x ∈ fvi_trm (b + c) t ⟷ x + c ∈ fvi_trm b t"
  by (induction t) auto

lemma fvi_trm_iff_fv_trm: "x ∈ fvi_trm b t ⟷ x + b ∈ fv_trm t"
  using fvi_trm_plus[where b=0 and c=b] by simp_all

lemma fvi_plus: "x ∈ fvi (b + c) φ ⟷ x + c ∈ fvi b φ"
proof (induction φ arbitrary: b rule: formula.induct)
  case (Exists φ)
  then show ?case by force
next
  case (Agg y ω b' f φ)
  have *: "b + c + b' = b + b' + c" by simp
  from Agg show ?case by (force simp: * fvi_trm_plus)
qed (auto simp add: fvi_trm_plus fv_regex_commute[where g = "λx. x + c"])

lemma fvi_Suc: "x ∈ fvi (Suc b) φ ⟷ Suc x ∈ fvi b φ"
  using fvi_plus[where c=1] by simp

lemma fvi_plus_bound:
  assumes "∀i∈fvi (b + c) φ. i < n"
  shows "∀i∈fvi b φ. i < c + n"
proof
  fix i
  assume "i ∈ fvi b φ"
  show "i < c + n"
  proof (cases "i < c")
    case True
    then show ?thesis by simp
  next
    case False
    then obtain i' where "i = i' + c"
      using nat_le_iff_add by (auto simp: not_less)
    with assms ‹i ∈ fvi b φ› show ?thesis by (simp add: fvi_plus)
  qed
qed

lemma fvi_Suc_bound:
  assumes "∀i∈fvi (Suc b) φ. i < n"
  shows "∀i∈fvi b φ. i < Suc n"
  using assms fvi_plus_bound[where c=1] by simp

lemma fvi_iff_fv: "x ∈ fvi b φ ⟷ x + b ∈ fv φ"
  using fvi_plus[where b=0 and c=b] by simp_all

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

qualified abbreviation nfv_regex where
  "nfv_regex ≡ Regex.nfv_regex fv"

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

lemma nfv_simps[simp]:
  "nfv (Let p φ ψ) = nfv ψ"
  "nfv (Neg φ) = nfv φ"
  "nfv (Or φ ψ) = max (nfv φ) (nfv ψ)"
  "nfv (And φ ψ) = max (nfv φ) (nfv ψ)"
  "nfv (Prev I φ) = nfv φ"
  "nfv (Next I φ) = nfv φ"
  "nfv (Since φ I ψ) = max (nfv φ) (nfv ψ)"
  "nfv (Until φ I ψ) = max (nfv φ) (nfv ψ)"
  "nfv (MatchP I r) = Regex.nfv_regex fv r"
  "nfv (MatchF I r) = Regex.nfv_regex fv r"
  "nfv_regex (Regex.Skip n) = 0"
  "nfv_regex (Regex.Test φ) = Max (insert 0 (Suc ` fv φ))"
  "nfv_regex (Regex.Plus r s) = max (nfv_regex r) (nfv_regex s)"
  "nfv_regex (Regex.Times r s) = max (nfv_regex r) (nfv_regex s)"
  "nfv_regex (Regex.Star r) = nfv_regex r"
  unfolding nfv_def Regex.nfv_regex_def by (simp_all add: image_Un Max_Un[symmetric])

lemma nfv_Ands[simp]: "nfv (Ands l) = Max (insert 0 (nfv ` set l))"
proof (induction l)
  case Nil
  then show ?case unfolding nfv_def by simp
next
  case (Cons a l)
  have "fv (Ands (a # l)) = fv a ∪ fv (Ands l)" by simp
  then have "nfv (Ands (a # l)) = max (nfv a) (nfv (Ands l))"
    unfolding nfv_def
    by (auto simp: image_Un Max.union[symmetric])
  with Cons.IH show ?case
    by (cases l) auto
qed

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

lemma fvi_less_nfv_regex: "∀i∈fv_regex φ. i < nfv_regex φ"
  unfolding Regex.nfv_regex_def
  by (auto simp add: Max_gr_iff intro: max.strict_coboundedI2)

subsubsection ‹Future reach›

qualified fun future_bounded :: "formula ⇒ bool" where
  "future_bounded (Pred _ _) = True"
| "future_bounded (Let p φ ψ) = (future_bounded φ ∧ future_bounded ψ)"
| "future_bounded (Eq _ _) = True"
| "future_bounded (Less _ _) = True"
| "future_bounded (LessEq _ _) = True"
| "future_bounded (Neg φ) = future_bounded φ"
| "future_bounded (Or φ ψ) = (future_bounded φ ∧ future_bounded ψ)"
| "future_bounded (And φ ψ) = (future_bounded φ ∧ future_bounded ψ)"
| "future_bounded (Ands l) = list_all future_bounded l"
| "future_bounded (Exists φ) = future_bounded φ"
| "future_bounded (Agg y ω b f φ) = future_bounded φ"
| "future_bounded (Prev I φ) = future_bounded φ"
| "future_bounded (Next I φ) = future_bounded φ"
| "future_bounded (Since φ I ψ) = (future_bounded φ ∧ future_bounded ψ)"
| "future_bounded (Until φ I ψ) = (future_bounded φ ∧ future_bounded ψ ∧ right I ≠ ∞)"
| "future_bounded (MatchP I r) = Regex.pred_regex future_bounded r"
| "future_bounded (MatchF I r) = (Regex.pred_regex future_bounded r ∧ right I ≠ ∞)"


subsubsection ‹Semantics›

definition "ecard A = (if finite A then card A else ∞)"

qualified fun sat :: "trace ⇒ (name ⇀ nat ⇒ event_data list set) ⇒ env ⇒ nat ⇒ formula ⇒ bool" where
  "sat σ V v i (Pred r ts) = (case V r of
       None ⇒ (r, map (eval_trm v) ts) ∈ Γ σ i
     | Some X ⇒ map (eval_trm v) ts ∈ X i)"
| "sat σ V v i (Let p φ ψ) =
    sat σ (V(p ↦ λi. {v. length v = nfv φ ∧ sat σ V v i φ})) v i ψ"
| "sat σ V v i (Eq t1 t2) = (eval_trm v t1 = eval_trm v t2)"
| "sat σ V v i (Less t1 t2) = (eval_trm v t1 < eval_trm v t2)"
| "sat σ V v i (LessEq t1 t2) = (eval_trm v t1 ≤ eval_trm v t2)"
| "sat σ V v i (Neg φ) = (¬ sat σ V v i φ)"
| "sat σ V v i (Or φ ψ) = (sat σ V v i φ ∨ sat σ V v i ψ)"
| "sat σ V v i (And φ ψ) = (sat σ V v i φ ∧ sat σ V v i ψ)"
| "sat σ V v i (Ands l) = (∀φ ∈ set l. sat σ V v i φ)"
| "sat σ V v i (Exists φ) = (∃z. sat σ V (z # v) i φ)"
| "sat σ V v i (Agg y ω b f φ) =
    (let M = {(x, ecard Zs) | x Zs. Zs = {zs. length zs = b ∧ sat σ V (zs @ v) i φ ∧ eval_trm (zs @ v) f = x} ∧ Zs ≠ {}}
    in (M = {} ⟶ fv φ ⊆ {0..<b}) ∧ v ! y = eval_agg_op ω M)"
| "sat σ V v i (Prev I φ) = (case i of 0 ⇒ False | Suc j ⇒ mem (τ σ i - τ σ j) I ∧ sat σ V v j φ)"
| "sat σ V v i (Next I φ) = (mem (τ σ (Suc i) - τ σ i) I ∧ sat σ V v (Suc i) φ)"
| "sat σ V v i (Since φ I ψ) = (∃j≤i. mem (τ σ i - τ σ j) I ∧ sat σ V v j ψ ∧ (∀k ∈ {j <.. i}. sat σ V v k φ))"
| "sat σ V v i (Until φ I ψ) = (∃j≥i. mem (τ σ j - τ σ i) I ∧ sat σ V v j ψ ∧ (∀k ∈ {i ..< j}. sat σ V v k φ))"
| "sat σ V v i (MatchP I r) = (∃j≤i. mem (τ σ i - τ σ j) I ∧ Regex.match (sat σ V v) r j i)"
| "sat σ V v i (MatchF I r) = (∃j≥i. mem (τ σ j - τ σ i) I ∧ Regex.match (sat σ V v) r i j)"

lemma sat_abbrevs[simp]:
  "sat σ V v i TT" "¬ sat σ V v i FF"
  unfolding TT_def FF_def by auto

lemma sat_Ands: "sat σ V v i (Ands l) ⟷ (∀φ∈set l. sat σ V v i φ)"
  by (simp add: list_all_iff)

lemma sat_Until_rec: "sat σ V v i (Until φ I ψ) ⟷
  mem 0 I ∧ sat σ V v i ψ ∨
  (Δ σ (i + 1) ≤ right I ∧ sat σ V v i φ ∧ sat σ V 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 v j ψ" "∀k ∈ {i ..< j}. sat σ V 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 v i φ" by auto
    moreover from False j have "sat σ V 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 v i φ" and
   "next": "sat σ V 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 v j ψ" "∀k ∈ {i + 1 ..< j}. sat σ V 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 v i (Since φ I ψ) ⟷
  mem 0 I ∧ sat σ V v i ψ ∨
  (i > 0 ∧ Δ σ i ≤ right I ∧ sat σ V v i φ ∧ sat σ V 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 v j ψ" "∀k ∈ {j <.. i}. sat σ V 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 v i φ" by auto
    moreover from False j have "sat σ V 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 v i φ" and
   "prev": "sat σ V 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 v j ψ" "∀k ∈ {j <.. i - 1}. sat σ V 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_MatchF_rec: "sat σ V v i (MatchF I r) ⟷ mem 0 I ∧ Regex.eps (sat σ V v) i r ∨
  Δ σ (i + 1) ≤ right I ∧ (∃s ∈ Regex.lpd (sat σ V v) i r. sat σ V v (i + 1) (MatchF (subtract (Δ σ (i + 1)) I) s))"
  (is "?L ⟷ ?R1 ∨ ?R2")
proof (rule iffI; (elim disjE conjE bexE)?)
  assume ?L
  then obtain j where j: "j ≥ i" "mem (τ σ j - τ σ i) I" and "Regex.match (sat σ V v) r i j" by auto
  then show "?R1 ∨ ?R2"
  proof (cases "i < j")
    case True
    with ‹Regex.match (sat σ V v) r i j› lpd_match[of i j "sat σ V v" r]
    obtain s where "s ∈ Regex.lpd (sat σ V v) i r" "Regex.match (sat σ V v) s (i + 1) j" by auto
    with True j have ?R2
      by (cases "right I")
        (auto simp: le_diff_conv le_diff_conv2 intro!: exI[of _ j] elim: le_trans[rotated])
    then show ?thesis by blast
  qed (auto simp: eps_match)
next
  assume "enat (Δ σ (i + 1)) ≤ right I"
  moreover
  fix s
  assume [simp]: "s ∈ Regex.lpd (sat σ V v) i r" and "sat σ V v (i + 1) (MatchF (subtract (Δ σ (i + 1)) I) s)"
  then obtain j where "j > i" "Regex.match (sat σ V v) s (i + 1) j"
    "mem (τ σ j - τ σ (Suc i)) (subtract (Δ σ (i + 1)) I)" by (auto simp: Suc_le_eq)
  ultimately show ?L
    by (cases "right I")
      (auto simp: le_diff_conv lpd_match intro!: exI[of _ j] bexI[of _ s])
qed (auto simp: eps_match intro!: exI[of _ i])

lemma sat_MatchP_rec: "sat σ V v i (MatchP I r) ⟷ mem 0 I ∧ Regex.eps (sat σ V v) i r ∨
  i > 0 ∧ Δ σ i ≤ right I ∧ (∃s ∈ Regex.rpd (sat σ V v) i r. sat σ V v (i - 1) (MatchP (subtract (Δ σ i) I) s))"
  (is "?L ⟷ ?R1 ∨ ?R2")
proof (rule iffI; (elim disjE conjE bexE)?)
  assume ?L
  then obtain j where j: "j ≤ i" "mem (τ σ i - τ σ j) I" and "Regex.match (sat σ V v) r j i" by auto
  then show "?R1 ∨ ?R2"
  proof (cases "j < i")
    case True
    with ‹Regex.match (sat σ V v) r j i› rpd_match[of j i "sat σ V v" r]
    obtain s where "s ∈ Regex.rpd (sat σ V v) i r" "Regex.match (sat σ V v) s j (i - 1)" by auto
    with True j have ?R2
      by (cases "right I")
        (auto simp: le_diff_conv le_diff_conv2 intro!: exI[of _ j] elim: le_trans)
    then show ?thesis by blast
  qed (auto simp: eps_match)
next
  assume "enat (Δ σ i) ≤ right I"
  moreover
  fix s
  assume [simp]: "s ∈ Regex.rpd (sat σ V v) i r" and "sat σ V v (i - 1) (MatchP (subtract (Δ σ i) I) s)" "i > 0"
  then obtain j where "j < i" "Regex.match (sat σ V v) s j (i - 1)"
    "mem (τ σ (i - 1) - τ σ j) (subtract (Δ σ i) I)" by (auto simp: gr0_conv_Suc less_Suc_eq_le)
  ultimately show ?L
    by (cases "right I")
      (auto simp: le_diff_conv rpd_match intro!: exI[of _ j] bexI[of _ s])
qed (auto simp: eps_match intro!: exI[of _ i])

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

lemma sat_MatchP_0: "sat σ V v 0 (MatchP I r) ⟷ mem 0 I ∧ Regex.eps (sat σ V v) 0 r"
  by (auto simp: eps_match)

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

lemma sat_MatchP_point: "sat σ V v i (MatchP I r) ⟹
    (⋀j. j ≤ i ⟹ mem (τ σ i - τ σ j) I ⟹ sat σ V v i (MatchP (point (τ σ i - τ σ j)) r) ⟹ P) ⟹ P"
  by (auto intro: diff_le_self)

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

lemma sat_MatchP_pointD: "sat σ V v i (MatchP (point t) r) ⟹ mem t I ⟹ sat σ V v i (MatchP I r)"
  by auto

lemma sat_fv_cong: "∀x∈fv φ. v!x = v'!x ⟹ sat σ V v i φ = sat σ V v' i φ"
proof (induct φ arbitrary: V v v' i rule: formula.induct)
  case (Pred n ts)
  show ?case by (simp cong: map_cong eval_trm_fv_cong[OF Pred[simplified, THEN bspec]] split: option.splits)
next
  case (Let p b φ ψ)
  then show ?case
    by auto
next
  case (Eq x1 x2)
  then show ?case unfolding fvi.simps sat.simps by (metis UnCI eval_trm_fv_cong)
next
  case (Less x1 x2)
  then show ?case unfolding fvi.simps sat.simps by (metis UnCI eval_trm_fv_cong)
next
  case (LessEq x1 x2)
  then show ?case unfolding fvi.simps sat.simps by (metis UnCI eval_trm_fv_cong)
next
  case (Ands l)
  have "⋀φ. φ ∈ set l ⟹ sat σ V v i φ = sat σ V v' i φ"
  proof -
    fix φ assume "φ ∈ set l"
    then have "fv φ ⊆ fv (Ands l)" using fv_subset_Ands by blast
    then have "∀x∈fv φ. v!x = v'!x" using Ands.prems by blast
    then show "sat σ V v i φ = sat σ V v' i φ" using Ands.hyps ‹φ ∈ set l› by blast
  qed
  then show ?case using sat_Ands by blast
next
  case (Exists φ)
  then show ?case unfolding sat.simps by (intro iff_exI) (simp add: fvi_Suc nth_Cons')
next
  case (Agg y ω b f φ)
  have "v ! y = v' ! y"
    using Agg.prems by simp
  moreover have "sat σ V (zs @ v) i φ = sat σ V (zs @ v') i φ" if "length zs = b" for zs
    using that Agg.prems by (simp add: Agg.hyps[where v="zs @ v" and v'="zs @ v'"]
        nth_append fvi_iff_fv(1)[where b=b])
  moreover have "eval_trm (zs @ v) f = eval_trm (zs @ v') f" if "length zs = b" for zs
    using that Agg.prems by (auto intro!: eval_trm_fv_cong[where v="zs @ v" and v'="zs @ v'"]
        simp: nth_append fvi_iff_fv(1)[where b=b] fvi_trm_iff_fv_trm[where b="length zs"])
  ultimately show ?case
    by (simp cong: conj_cong)
next
  case (MatchF I r)
  then have "Regex.match (sat σ V v) r = Regex.match (sat σ V v') r"
    by (intro match_fv_cong) (auto simp: fv_regex_alt)
  then show ?case
    by auto
next
  case (MatchP I r)
  then have "Regex.match (sat σ V v) r = Regex.match (sat σ V v') r"
    by (intro match_fv_cong) (auto simp: fv_regex_alt)
  then show ?case
    by auto
qed (auto 10 0 split: nat.splits intro!: iff_exI)

lemma match_fv_cong:
  "∀x∈fv_regex r. v!x = v'!x ⟹ Regex.match (sat σ V v) r = Regex.match (sat σ V v') r"
  by (rule match_fv_cong, rule sat_fv_cong) (auto simp: fv_regex_alt)

lemma eps_fv_cong:
  "∀x∈fv_regex r. v!x = v'!x ⟹ Regex.eps (sat σ V v) i r = Regex.eps (sat σ V v') i r"
  unfolding eps_match by (erule match_fv_cong[THEN fun_cong, THEN fun_cong])


subsection ‹Past-only formulas›

fun past_only :: "formula ⇒ bool" where
  "past_only (Pred _ _) = True"
| "past_only (Eq _ _) = True"
| "past_only (Less _ _) = True"
| "past_only (LessEq _ _) = True"
| "past_only (Let _ α β) = (past_only α ∧ past_only β)"
| "past_only (Neg ψ) = past_only ψ"
| "past_only (Or α β) = (past_only α ∧ past_only β)"
| "past_only (And α β) = (past_only α ∧ past_only β)"
| "past_only (Ands l) = (∀α∈set l. past_only α)"
| "past_only (Exists ψ) = past_only ψ"
| "past_only (Agg _ _ _ _ ψ) = past_only ψ"
| "past_only (Prev _ ψ) = past_only ψ"
| "past_only (Next _ _) = False"
| "past_only (Since α _ β) = (past_only α ∧ past_only β)"
| "past_only (Until α _ β) = False"
| "past_only (MatchP _ r) = Regex.pred_regex past_only r"
| "past_only (MatchF _ _) = False"

lemma past_only_sat:
  assumes "prefix_of π σ" "prefix_of π σ'"
  shows "i < plen π ⟹ dom V = dom V' ⟹
     (⋀p i. p ∈ dom V ⟹ i < plen π ⟹ the (V p) i = the (V' p) i) ⟹
     past_only φ ⟹ sat σ V v i φ = sat σ' V' v i φ"
proof (induction φ arbitrary: V V' v i)
  case (Pred e ts)
  show ?case proof (cases "V e")
    case None
    then have "V' e = None" using ‹dom V = dom V'› by auto
    with None Γ_prefix_conv[OF assms(1,2) Pred(1)] show ?thesis by simp
  next
    case (Some a)
    moreover obtain a' where "V' e = Some a'" using Some ‹dom V = dom V'› by auto
    moreover have "the (V e) i = the (V' e) i"
      using Some Pred(1,3) by (fastforce intro: domI)
    ultimately show ?thesis by simp
  qed
next
  case (Let p φ ψ)
  let ?V = "λV σ. (V(p ↦ λi. {v. length v = nfv φ ∧ sat σ V v i φ}))"
  show ?case unfolding sat.simps proof (rule Let.IH(2))
    show "i < plen π" by fact
    from Let.prems show "past_only ψ" by simp
    from Let.prems show "dom (?V V σ) = dom (?V V' σ')"
      by (simp del: fun_upd_apply)
  next
    fix p' i
    assume *: "p' ∈ dom (?V V σ)" "i < plen π"
    show "the (?V V σ p') i = the (?V V' σ' p') i" proof (cases "p' = p")
      case True
      with Let ‹i < plen π› show ?thesis by auto
    next
      case False
      with * show ?thesis by (auto intro!: Let.prems(3))
    qed
  qed
next
  case (Ands l)
  with Γ_prefix_conv[OF assms] show ?case by simp
next
  case (Prev I φ)
  with τ_prefix_conv[OF assms] show ?case by (simp split: nat.split)
next
  case (Since φ1 I φ2)
  with τ_prefix_conv[OF assms] show ?case by auto
next
  case (MatchP I r)
  then have "Regex.match (sat σ V v) r a b = Regex.match (sat σ' V' v) r a b" if "b < plen π" for a b
    using that by (intro Regex.match_cong_strong) (auto simp: regex.pred_set)
  with τ_prefix_conv[OF assms] MatchP(2) show ?case by auto
qed auto


subsection ‹Safe formulas›

fun remove_neg :: "formula ⇒ formula" where
  "remove_neg (Neg φ) = φ"
| "remove_neg φ = φ"

lemma fvi_remove_neg[simp]: "fvi b (remove_neg φ) = fvi b φ"
  by (cases φ) simp_all

lemma partition_cong[fundef_cong]:
  "xs = ys ⟹ (⋀x. x∈set xs ⟹ f x = g x) ⟹ partition f xs = partition g ys"
  by (induction xs arbitrary: ys) auto

lemma size_remove_neg[termination_simp]: "size (remove_neg φ) ≤ size φ"
  by (cases φ) simp_all

fun is_constraint :: "formula ⇒ bool" where
  "is_constraint (Eq t1 t2) = True"
| "is_constraint (Less t1 t2) = True"
| "is_constraint (LessEq t1 t2) = True"
| "is_constraint (Neg (Eq t1 t2)) = True"
| "is_constraint (Neg (Less t1 t2)) = True"
| "is_constraint (Neg (LessEq t1 t2)) = True"
| "is_constraint _ = False"

definition safe_assignment :: "nat set ⇒ formula ⇒ bool" where
  "safe_assignment X φ = (case φ of
       Eq (Var x) (Var y) ⇒ (x ∉ X ⟷ y ∈ X)
     | Eq (Var x) t ⇒ (x ∉ X ∧ fv_trm t ⊆ X)
     | Eq t (Var x) ⇒ (x ∉ X ∧ fv_trm t ⊆ X)
     | _ ⇒ False)"

fun safe_formula :: "formula ⇒ bool" where
  "safe_formula (Eq t1 t2) = (is_Const t1 ∧ (is_Const t2 ∨ is_Var t2) ∨ is_Var t1 ∧ is_Const t2)"
| "safe_formula (Neg (Eq (Var x) (Var y))) = (x = y)"
| "safe_formula (Less t1 t2) = False"
| "safe_formula (LessEq t1 t2) = False"
| "safe_formula (Pred e ts) = (∀t∈set ts. is_Var t ∨ is_Const t)"
| "safe_formula (Let p φ ψ) = ({0..<nfv φ} ⊆ fv φ ∧ safe_formula φ ∧ safe_formula ψ)"
| "safe_formula (Neg φ) = (fv φ = {} ∧ safe_formula φ)"
| "safe_formula (Or φ ψ) = (fv ψ = fv φ ∧ safe_formula φ ∧ safe_formula ψ)"
| "safe_formula (And φ ψ) = (safe_formula φ ∧
    (safe_assignment (fv φ) ψ ∨ safe_formula ψ ∨
      fv ψ ⊆ fv φ ∧ (is_constraint ψ ∨ (case ψ of Neg ψ' ⇒ safe_formula ψ' | _ ⇒ False))))"
| "safe_formula (Ands l) = (let (pos, neg) = partition safe_formula l in pos ≠ [] ∧
    list_all safe_formula (map remove_neg neg) ∧ ⋃(set (map fv neg)) ⊆ ⋃(set (map fv pos)))"
| "safe_formula (Exists φ) = (safe_formula φ)"
| "safe_formula (Agg y ω b f φ) = (safe_formula φ ∧ y + b ∉ fv φ ∧ {0..<b} ⊆ fv φ ∧ fv_trm f ⊆ fv φ)"
| "safe_formula (Prev I φ) = (safe_formula φ)"
| "safe_formula (Next I φ) = (safe_formula φ)"
| "safe_formula (Since φ I ψ) = (fv φ ⊆ fv ψ ∧
    (safe_formula φ ∨ (case φ of Neg φ' ⇒ safe_formula φ' | _ ⇒ False)) ∧ safe_formula ψ)"
| "safe_formula (Until φ I ψ) = (fv φ ⊆ fv ψ ∧
    (safe_formula φ ∨ (case φ of Neg φ' ⇒ safe_formula φ' | _ ⇒ False)) ∧ safe_formula ψ)"
| "safe_formula (MatchP I r) = Regex.safe_regex fv (λg φ. safe_formula φ ∨
     (g = Lax ∧ (case φ of Neg φ' ⇒ safe_formula φ' | _ ⇒ False))) Past Strict r"
| "safe_formula (MatchF I r) = Regex.safe_regex fv (λg φ. safe_formula φ ∨
     (g = Lax ∧ (case φ of Neg φ' ⇒ safe_formula φ' | _ ⇒ False))) Futu Strict r"

abbreviation "safe_regex ≡ Regex.safe_regex fv (λg φ. safe_formula φ ∨
  (g = Lax ∧ (case φ of Neg φ' ⇒ safe_formula φ' | _ ⇒ False)))"

lemma safe_regex_safe_formula:
  "safe_regex m g r ⟹ φ ∈ Regex.atms r ⟹ safe_formula φ ∨
  (∃ψ. φ = Neg ψ ∧ safe_formula ψ)"
  by (cases g) (auto dest!: safe_regex_safe[rotated] split: formula.splits[where formula=φ])

lemma safe_abbrevs[simp]: "safe_formula TT" "safe_formula FF"
  unfolding TT_def FF_def by auto

definition safe_neg :: "formula ⇒ bool" where
  "safe_neg φ ⟷ (¬ safe_formula φ ⟶ safe_formula (remove_neg φ))"

definition atms :: "formula Regex.regex ⇒ formula set" where
  "atms r = (⋃φ ∈ Regex.atms r.
     if safe_formula φ then {φ} else case φ of Neg φ' ⇒ {φ'} | _ ⇒ {})"

lemma atms_simps[simp]:
  "atms (Regex.Skip n) = {}"
  "atms (Regex.Test φ) = (if safe_formula φ then {φ} else case φ of Neg φ' ⇒ {φ'} | _ ⇒ {})"
  "atms (Regex.Plus r s) = atms r ∪ atms s"
  "atms (Regex.Times r s) = atms r ∪ atms s"
  "atms (Regex.Star r) = atms r"
  unfolding atms_def by auto

lemma finite_atms[simp]: "finite (atms r)"
  by (induct r) (auto split: formula.splits)

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

lemma safe_formula_induct[consumes 1, case_names Eq_Const Eq_Var1 Eq_Var2 neq_Var Pred Let
    And_assign And_safe And_constraint And_Not Ands Neg Or Exists Agg
    Prev Next Since Not_Since Until Not_Until MatchP MatchF]:
  assumes "safe_formula φ"
    and Eq_Const: "⋀c d. P (Eq (Const c) (Const d))"
    and Eq_Var1: "⋀c x. P (Eq (Const c) (Var x))"
    and Eq_Var2: "⋀c x. P (Eq (Var x) (Const c))"
    and neq_Var: "⋀x. P (Neg (Eq (Var x) (Var x)))"
    and Pred: "⋀e ts. ∀t∈set ts. is_Var t ∨ is_Const t ⟹ P (Pred e ts)"
    and Let: "⋀p φ ψ. {0..<nfv φ} ⊆ fv φ ⟹ safe_formula φ ⟹ safe_formula ψ ⟹ P φ ⟹ P ψ ⟹ P (Let p φ ψ)"
    and And_assign: "⋀φ ψ. safe_formula φ ⟹ safe_assignment (fv φ) ψ ⟹ P φ ⟹ P (And φ ψ)"
    and And_safe: "⋀φ ψ. safe_formula φ ⟹ ¬ safe_assignment (fv φ) ψ ⟹ safe_formula ψ ⟹
      P φ ⟹ P ψ ⟹ P (And φ ψ)"
    and And_constraint: "⋀φ ψ. safe_formula φ ⟹ ¬ safe_assignment (fv φ) ψ ⟹ ¬ safe_formula ψ ⟹
      fv ψ ⊆ fv φ ⟹ is_constraint ψ ⟹ P φ ⟹ P (And φ ψ)"
    and And_Not: "⋀φ ψ. safe_formula φ ⟹ ¬ safe_assignment (fv φ) (Neg ψ) ⟹ ¬ safe_formula (Neg ψ) ⟹
      fv (Neg ψ) ⊆ fv φ ⟹ ¬ is_constraint (Neg ψ) ⟹ safe_formula ψ ⟹ P φ ⟹ P ψ ⟹ P (And φ (Neg ψ))"
    and Ands: "⋀l pos neg. (pos, neg) = partition safe_formula l ⟹ pos ≠ [] ⟹
      list_all safe_formula pos ⟹ list_all safe_formula (map remove_neg neg) ⟹
      (⋃φ∈set neg. fv φ) ⊆ (⋃φ∈set pos. fv φ) ⟹
      list_all P pos ⟹ list_all P (map remove_neg neg) ⟹ P (Ands l)"
    and Neg: "⋀φ. fv φ = {} ⟹ safe_formula φ ⟹ P φ ⟹ P (Neg φ)"
    and Or: "⋀φ ψ. fv ψ = fv φ ⟹ safe_formula φ ⟹ safe_formula ψ ⟹ P φ ⟹ P ψ ⟹ P (Or φ ψ)"
    and Exists: "⋀φ. safe_formula φ ⟹ P φ ⟹ P (Exists φ)"
    and Agg: "⋀y ω b f φ. y + b ∉ fv φ ⟹ {0..<b} ⊆ fv φ ⟹ fv_trm f ⊆ fv φ ⟹
      safe_formula φ ⟹ P φ ⟹ P (Agg y ω b f φ)"
    and Prev: "⋀I φ. safe_formula φ ⟹ P φ ⟹ P (Prev I φ)"
    and Next: "⋀I φ. safe_formula φ ⟹ P φ ⟹ P (Next I φ)"
    and Since: "⋀φ I ψ. fv φ ⊆ fv ψ ⟹ safe_formula φ ⟹ safe_formula ψ ⟹ P φ ⟹ P ψ ⟹ P (Since φ I ψ)"
    and Not_Since: "⋀φ I ψ. fv (Neg φ) ⊆ fv ψ ⟹ safe_formula φ ⟹
      ¬ safe_formula (Neg φ) ⟹ safe_formula ψ ⟹ P φ ⟹ P ψ ⟹ P (Since (Neg φ) I ψ )"
    and Until: "⋀φ I ψ. fv φ ⊆ fv ψ ⟹ safe_formula φ ⟹ safe_formula ψ ⟹ P φ ⟹ P ψ ⟹ P (Until φ I ψ)"
    and Not_Until: "⋀φ I ψ. fv (Neg φ) ⊆ fv ψ ⟹ safe_formula φ ⟹
      ¬ safe_formula (Neg φ) ⟹ safe_formula ψ ⟹ P φ ⟹ P ψ ⟹ P (Until (Neg φ) I ψ)"
    and MatchP: "⋀I r. safe_regex Past Strict r ⟹ ∀φ ∈ atms r. P φ ⟹ P (MatchP I r)"
    and MatchF: "⋀I r. safe_regex Futu Strict r ⟹ ∀φ ∈ atms r. P φ ⟹ P (MatchF I r)"
  shows "P φ"
using assms(1) proof (induction φ rule: safe_formula.induct)
  case (1 t1 t2)
  then show ?case using Eq_Const Eq_Var1 Eq_Var2 by (auto simp: trm.is_Const_def trm.is_Var_def)
next
  case (9 φ ψ)
  from ‹safe_formula (And φ ψ)› have "safe_formula φ" by simp
  from ‹safe_formula (And φ ψ)› consider
    (a) "safe_assignment (fv φ) ψ"
    | (b) "¬ safe_assignment (fv φ) ψ" "safe_formula ψ"
    | (c) "fv ψ ⊆ fv φ" "¬ safe_assignment (fv φ) ψ" "¬ safe_formula ψ" "is_constraint ψ"
    | (d) ψ' where "fv ψ ⊆ fv φ" "¬ safe_assignment (fv φ) ψ" "¬ safe_formula ψ" "¬ is_constraint ψ"
        "ψ = Neg ψ'" "safe_formula ψ'"
    by (cases ψ) auto
  then show ?case proof cases
    case a
    then show ?thesis using "9.IH" ‹safe_formula φ› by (intro And_assign)
  next
    case b
    then show ?thesis using "9.IH" ‹safe_formula φ› by (intro And_safe)
  next
    case c
    then show ?thesis using "9.IH" ‹safe_formula φ› by (intro And_constraint)
  next
    case d
    then show ?thesis using "9.IH" ‹safe_formula φ› by (blast intro!: And_Not)
  qed
next
  case (10 l)
  obtain pos neg where posneg: "(pos, neg) = partition safe_formula l" by simp
  have "pos ≠ []" using "10.prems" posneg by simp
  moreover have "list_all safe_formula pos" using posneg by (simp add: list.pred_set)
  moreover have safe_remove_neg: "list_all safe_formula (map remove_neg neg)" using "10.prems" posneg by auto
  moreover have "list_all P pos"
    using posneg "10.IH"(1) by (simp add: list_all_iff)
  moreover have "list_all P (map remove_neg neg)"
    using "10.IH"(2)[OF posneg] safe_remove_neg by (simp add: list_all_iff)
  ultimately show ?case using "10.IH"(1) "10.prems" Ands posneg by simp
next
  case (15 φ I ψ)
  then show ?case
  proof (cases φ)
    case (Ands l)
    then show ?thesis using "15.IH"(1) "15.IH"(3) "15.prems" Since by auto
  qed (auto 0 3 elim!: disjE_Not2 intro: Since Not_Since) (*SLOW*)
next
  case (16 φ I ψ)
  then show ?case
  proof (cases φ)
    case (Ands l)
    then show ?thesis using "16.IH"(1) "16.IH"(3) "16.prems" Until by auto
  qed (auto 0 3 elim!: disjE_Not2 intro: Until Not_Until) (*SLOW*)
next
  case (17 I r)
  then show ?case
    by (intro MatchP) (auto simp: atms_def dest: safe_regex_safe_formula split: if_splits)
next
  case (18 I r)
  then show ?case
    by (intro MatchF) (auto simp: atms_def dest: safe_regex_safe_formula split: if_splits)
qed (auto simp: assms)

lemma safe_formula_NegD:
  "safe_formula (Formula.Neg φ) ⟹ fv φ = {} ∨ (∃x. φ = Formula.Eq (Formula.Var x) (Formula.Var x))"
  by (induct "Formula.Neg φ" rule: safe_formula_induct) auto


subsection ‹Slicing traces›

qualified fun matches ::
  "env ⇒ formula ⇒ name × event_data list ⇒ bool" where
  "matches v (Pred r ts) e = (fst e = r ∧ map (eval_trm v) ts = snd e)"
| "matches v (Let p φ ψ) e =
    ((∃v'. matches v' φ e ∧ matches v ψ (p, v')) ∨
    fst e ≠ p ∧ matches v ψ e)"
| "matches v (Eq _ _) e = False"
| "matches v (Less _ _) e = False"
| "matches v (LessEq _ _) e = False"
| "matches v (Neg φ) e = matches v φ e"
| "matches v (Or φ ψ) e = (matches v φ e ∨ matches v ψ e)"
| "matches v (And φ ψ) e = (matches v φ e ∨ matches v ψ e)"
| "matches v (Ands l) e = (∃φ∈set l. matches v φ e)"
| "matches v (Exists φ) e = (∃z. matches (z # v) φ e)"
| "matches v (Agg y ω b f φ) e = (∃zs. length zs = b ∧ matches (zs @ 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)"
| "matches v (MatchP I r) e = (∃φ ∈ Regex.atms r. matches v φ e)"
| "matches v (MatchF I r) e = (∃φ ∈ Regex.atms r. matches v φ e)"

lemma matches_cong:
  "∀x∈fv φ. v!x = v'!x ⟹ matches v φ e = matches v' φ e"
proof (induct φ arbitrary: v v' e)
  case (Pred n ts)
  show ?case
    by (simp cong: map_cong eval_trm_fv_cong[OF Pred(1)[simplified, THEN bspec]])
next
  case (Let p b φ ψ)
  then show ?case
    by (cases e) (auto 11 0)
next
  case (Ands l)
  have "⋀φ. φ ∈ (set l) ⟹ matches v φ e = matches v' φ e"
  proof -
    fix φ assume "φ ∈ (set l)"
    then have "fv φ ⊆ fv (Ands l)" using fv_subset_Ands by blast
    then have "∀x∈fv φ. v!x = v'!x" using Ands.prems by blast
    then show "matches v φ e = matches v' φ e" using Ands.hyps ‹φ ∈ set l› by blast
  qed
  then show ?case by simp
next
  case (Exists φ)
  then show ?case unfolding matches.simps by (intro iff_exI) (simp add: fvi_Suc nth_Cons')
next
  case (Agg y ω b f φ)
  have "matches (zs @ v) φ e = matches (zs @ v') φ e" if "length zs = b" for zs
    using that Agg.prems by (simp add: Agg.hyps[where v="zs @ v" and v'="zs @ v'"]
        nth_append fvi_iff_fv(1)[where b=b])
  then show ?case by auto
qed (auto 9 0 simp add: nth_Cons' fv_regex_alt)

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

lemma sat_slice_strong:
  assumes "v ∈ S" "dom V = dom V'"
    "⋀p v i. p ∈ dom V ⟹ (p, v) ∈ relevant_events φ S ⟹ v ∈ the (V p) i ⟷ v ∈ the (V' p) i"
  shows "relevant_events φ S - {e. fst e ∈ dom V} ⊆ E ⟹
    sat σ V v i φ ⟷ sat (map_Γ (λD. D ∩ E) σ) V' v i φ"
  using assms
proof (induction φ arbitrary: V V' v S i)
  case (Pred r ts)
  show ?case proof (cases "V r")
    case None
    then have "V' r = None" using ‹dom V = dom V'› by auto
    with None Pred(1,2) show ?thesis by (auto simp: domIff dest!: subsetD)
  next
    case (Some a)
    moreover obtain a' where "V' r = Some a'" using Some ‹dom V = dom V'› by auto
    moreover have "(map (eval_trm v) ts ∈ the (V r) i) = (map (eval_trm v) ts ∈ the (V' r) i)"
      using Some Pred(2,4) by (fastforce intro: domI)
    ultimately show ?thesis by simp
  qed
next
  case (Let p φ ψ)
  from Let.prems show ?case unfolding sat.simps
  proof (intro Let(2)[of S], goal_cases relevant v dom V)
    case (V p' v' i)
    then show ?case
    proof (cases "p' = p")
      case [simp]: True
      with V show ?thesis
        unfolding fun_upd_apply eqTrueI[OF True] if_True option.sel mem_Collect_eq
      proof (intro ex_cong conj_cong refl Let(1)[where
        S="{v'. (∃v ∈ S. matches v ψ (p, v'))}" and V=V],
        goal_cases relevant' v' dom' V')
        case relevant'
        then show ?case
          by (elim subset_trans[rotated]) (auto simp: set_eq_iff)
      next
        case (V' p' v' i)
        then show ?case
          by (intro V(4)) (auto simp: set_eq_iff)
      qed auto
    next
      case False
      with V(2,3,5,6) show ?thesis
        unfolding fun_upd_apply eq_False[THEN iffD2, OF False] if_False
        by (intro V(4)) (auto simp: False)
    qed
  qed (auto simp: dom_def)
next
  case (Or φ ψ)
  show ?case using Or.IH[of S V v V'] Or.prems
    by (auto simp: Collect_disj_eq Int_Un_distrib subset_iff)
next
  case (And φ ψ)
  show ?case using And.IH[of S V v V'] And.prems
    by (auto simp: Collect_disj_eq Int_Un_distrib subset_iff)
next
  case (Ands l)
  obtain "relevant_events (Ands l) S - {e. fst e ∈ dom V} ⊆ E" "v ∈ S" using Ands.prems(1) Ands.prems(2) by blast
  then have "{e. S ∩ {v. matches v (Ands l) e} ≠ {}} - {e. fst e ∈ dom V} ⊆ E" by simp
  have "⋀φ. φ ∈ set l ⟹ sat σ V v i φ ⟷ sat (map_Γ (λD. D ∩ E) σ) V' v i φ"
  proof -
    fix φ assume "φ ∈ set l"
    have "relevant_events φ S = {e. S ∩ {v. matches v φ e} ≠ {}}" by simp
    have "{e. S ∩ {v. matches v φ e} ≠ {}} ⊆ {e. S ∩ {v. matches v (Ands l) e} ≠ {}}" (is "?A ⊆ ?B")
    proof (rule subsetI)
      fix e assume "e ∈ ?A"
      then have "S ∩ {v. matches v φ e} ≠ {}" by blast
      moreover have "S ∩ {v. matches v (Ands l) e} ≠ {}"
      proof -
        obtain v where "v ∈ S" "matches v φ e" using calculation by blast
        then show ?thesis using ‹φ ∈ set l› by auto
      qed
      then show "e ∈ ?B" by blast
    qed
    then have "relevant_events φ S - {e. fst e ∈ dom V} ⊆ E" using Ands.prems(1) by auto
    then show "sat σ V v i φ ⟷ sat (map_Γ (λD. D ∩ E) σ) V' v i φ"
      using Ands.prems(2,3) ‹φ ∈ set l›
      by (intro Ands.IH[of φ S V v V' i] Ands.prems(4)) auto
  qed
  show ?case using ‹⋀φ. φ ∈ set l ⟹ sat σ V v i φ = sat (map_Γ (λD. D ∩ E) σ) V' v i φ› sat_Ands by blast
next
  case (Exists φ)
  have "sat σ V (z # v) i φ = sat (map_Γ (λD. D ∩ E) σ) V' (z # v) i φ" for z
    using Exists.prems(1-3) by (intro Exists.IH[where S="{z # v | v. v ∈ S}"] Exists.prems(4)) auto
  then show ?case by simp
next
  case (Agg y ω b f φ)
  have "sat σ V (zs @ v) i φ = sat (map_Γ (λD. D ∩ E) σ) V' (zs @ v) i φ" if "length zs = b" for zs
    using that Agg.prems(1-3) by (intro Agg.IH[where S="{zs @ v | v. v ∈ S}"] Agg.prems(4)) auto
  then show ?case by (simp cong: conj_cong)
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 V] Since.prems
   by (auto simp: Collect_disj_eq Int_Un_distrib subset_iff)
next
  case (Until φ I ψ)
  show ?case using Until.IH[of S V] Until.prems
    by (auto simp: Collect_disj_eq Int_Un_distrib subset_iff)
next
  case (MatchP I r)
  from MatchP.prems(1-3) have "Regex.match (sat σ V v) r = Regex.match (sat (map_Γ (λD. D ∩ E) σ) V' v) r"
    by (intro Regex.match_fv_cong MatchP(1)[of _ S V v] MatchP.prems(4)) auto
  then show ?case
    by auto
next
  case (MatchF I r)
  from MatchF.prems(1-3) have "Regex.match (sat σ V v) r = Regex.match (sat (map_Γ (λD. D ∩ E) σ) V' v) r"
    by (intro Regex.match_fv_cong MatchF(1)[of _ S V v] MatchF.prems(4)) auto
  then show ?case
    by auto
qed simp_all


subsection ‹Translation to n-ary conjunction›

fun get_and_list :: "formula ⇒ formula list" where
  "get_and_list (Ands l) = l"
| "get_and_list φ = [φ]"

lemma fv_get_and: "(⋃x∈(set (get_and_list φ)). fvi b x) = fvi b φ"
  by (induction φ rule: get_and_list.induct) simp_all

lemma safe_get_and: "safe_formula φ ⟹ list_all safe_neg (get_and_list φ)"
  by (induction φ rule: get_and_list.induct) (simp_all add: safe_neg_def list_all_iff)

lemma sat_get_and: "sat σ V v i φ ⟷ list_all (sat σ V v i) (get_and_list φ)"
  by (induction φ rule: get_and_list.induct) (simp_all add: list_all_iff)

fun convert_multiway :: "formula ⇒ formula" where
  "convert_multiway (Neg φ) = Neg (convert_multiway φ)"
| "convert_multiway (Or φ ψ) = Or (convert_multiway φ) (convert_multiway ψ)"
| "convert_multiway (And φ ψ) = (if safe_assignment (fv φ) ψ then
      And (convert_multiway φ) ψ
    else if safe_formula ψ then
      Ands (get_and_list (convert_multiway φ) @ get_and_list (convert_multiway ψ))
    else if is_constraint ψ then
      And (convert_multiway φ) ψ
    else Ands (convert_multiway ψ # get_and_list (convert_multiway φ)))"
| "convert_multiway (Exists φ) = Exists (convert_multiway φ)"
| "convert_multiway (Agg y ω b f φ) = Agg y ω b f (convert_multiway φ)"
| "convert_multiway (Prev I φ) = Prev I (convert_multiway φ)"
| "convert_multiway (Next I φ) = Next I (convert_multiway φ)"
| "convert_multiway (Since φ I ψ) = Since (convert_multiway φ) I (convert_multiway ψ)"
| "convert_multiway (Until φ I ψ) = Until (convert_multiway φ) I (convert_multiway ψ)"
| "convert_multiway (MatchP I r) = MatchP I (Regex.map_regex convert_multiway r)"
| "convert_multiway (MatchF I r) = MatchF I (Regex.map_regex convert_multiway r)"
| "convert_multiway φ = φ"

abbreviation "convert_multiway_regex ≡ Regex.map_regex convert_multiway"

lemma fv_safe_get_and:
  "safe_formula φ ⟹ fv φ ⊆ (⋃x∈(set (filter safe_formula (get_and_list φ))). fv x)"
proof (induction φ rule: get_and_list.induct)
  case (1 l)
  obtain pos neg where posneg: "(pos, neg) = partition safe_formula l" by simp
  have "get_and_list (Ands l) = l" by simp
  have sub: "(⋃x∈set neg. fv x) ⊆ (⋃x∈set pos. fv x)" using "1.prems" posneg by simp
  then have "fv (Ands l) ⊆ (⋃x∈set pos. fv x)"
  proof -
    have "fv (Ands l) = (⋃x∈set pos. fv x) ∪ (⋃x∈set neg. fv x)" using posneg by auto
    then show ?thesis using sub by simp
  qed
  then show ?case using posneg by auto
qed auto

lemma ex_safe_get_and:
  "safe_formula φ ⟹ list_ex safe_formula (get_and_list φ)"
proof (induction φ rule: get_and_list.induct)
  case (1 l)
  have "get_and_list (Ands l) = l" by simp
  obtain pos neg where posneg: "(pos, neg) = partition safe_formula l" by simp
  then have "pos ≠ []" using "1.prems" by simp
  then obtain x where "x ∈ set pos" by fastforce
  then show ?case using posneg using Bex_set_list_ex by fastforce
qed simp_all

lemma case_NegE: "(case φ of Neg φ' ⇒ P φ' | _ ⇒ False) ⟹ (⋀φ'. φ = Neg φ' ⟹ P φ' ⟹ Q) ⟹ Q"
  by (cases φ) simp_all

lemma convert_multiway_remove_neg: "safe_formula (remove_neg φ) ⟹ convert_multiway (remove_neg φ) = remove_neg (convert_multiway φ)"
  by (cases φ) (auto elim: case_NegE)

lemma fv_convert_multiway: "safe_formula φ ⟹ fvi b (convert_multiway φ) = fvi b φ"
proof (induction φ arbitrary: b rule: safe_formula.induct)
  case (9 φ ψ)
  then show ?case by (cases ψ) (auto simp: fv_get_and Un_commute)
next
  case (15 φ I ψ)
  show ?case proof (cases "safe_formula φ")
    case True
    with 15 show ?thesis by simp
  next
    case False
    with "15.prems" obtain φ' where "φ = Neg φ'" by (simp split: formula.splits)
    with False 15 show ?thesis by simp
  qed
next
  case (16 φ I ψ)
  show ?case proof (cases "safe_formula φ")
    case True
    with 16 show ?thesis by simp
  next
    case False
    with "16.prems" obtain φ' where "φ = Neg φ'" by (simp split: formula.splits)
    with False 16 show ?thesis by simp
  qed
next
  case (17 I r)
  then show ?case
    unfolding convert_multiway.simps fvi.simps fv_regex_alt regex.set_map image_image
    by (intro arg_cong[where f=Union, OF image_cong[OF refl]])
      (auto dest!: safe_regex_safe_formula)
next
  case (18 I r)
  then show ?case
    unfolding convert_multiway.simps fvi.simps fv_regex_alt regex.set_map image_image
    by (intro arg_cong[where f=Union, OF image_cong[OF refl]])
      (auto dest!: safe_regex_safe_formula)
qed (auto simp del: convert_multiway.simps(3))

lemma get_and_nonempty:
  assumes "safe_formula φ"
  shows "get_and_list φ ≠ []"
  using assms by (induction φ) auto

lemma future_bounded_get_and:
  "list_all future_bounded (get_and_list φ) = future_bounded φ"
  by (induction φ) simp_all

lemma safe_convert_multiway: "safe_formula φ ⟹ safe_formula (convert_multiway φ)"
proof (induction φ rule: safe_formula_induct)
  case (And_safe φ ψ)
  let ?a = "And φ ψ"
  let ?b = "convert_multiway ?a"
  let ?cφ = "convert_multiway φ"
  let ?cψ = "convert_multiway ψ"
  have b_def: "?b = Ands (get_and_list ?cφ @ get_and_list ?cψ)"
    using And_safe by simp
  show ?case proof -
    let ?l = "get_and_list ?cφ @ get_and_list ?cψ"
    obtain pos neg where posneg: "(pos, neg) = partition safe_formula ?l" by simp
    then have "list_all safe_formula pos" by (auto simp: list_all_iff)
    have lsafe_neg: "list_all safe_neg ?l"
      using And_safe ‹safe_formula φ› ‹safe_formula ψ›
      by (simp add: safe_get_and)
    then have "list_all safe_formula (map remove_neg neg)"
    proof -
      have "⋀x. x ∈ set neg ⟹ safe_formula (remove_neg x)"
      proof -
        fix x assume "x ∈ set neg"
        then have "¬ safe_formula x" using posneg by auto
        moreover have "safe_neg x" using lsafe_neg ‹x ∈ set neg›
          unfolding safe_neg_def list_all_iff partition_set[OF posneg[symmetric], symmetric]
          by simp
        ultimately show "safe_formula (remove_neg x)" using safe_neg_def by blast
      qed
      then show ?thesis by (auto simp: list_all_iff)
    qed

    have pos_filter: "pos = filter safe_formula (get_and_list ?cφ @ get_and_list ?cψ)"
      using posneg by simp
    have "(⋃x∈set neg. fv x) ⊆ (⋃x∈set pos. fv x)"
    proof -
      have 1: "fv ?cφ ⊆ (⋃x∈(set (filter safe_formula (get_and_list ?cφ))). fv x)" (is "_ ⊆ ?fvφ")
        using And_safe ‹safe_formula φ› by (blast intro!: fv_safe_get_and)
      have 2: "fv ?cψ ⊆ (⋃x∈(set (filter safe_formula (get_and_list ?cψ))). fv x)" (is "_ ⊆ ?fvψ")
        using And_safe ‹safe_formula ψ› by (blast intro!: fv_safe_get_and)
      have "(⋃x∈set neg. fv x) ⊆ fv ?cφ ∪ fv ?cψ" proof -
        have "⋃ (fv ` set neg) ⊆ ⋃ (fv ` (set pos ∪ set neg))"
          by simp
        also have "... ⊆ fv (convert_multiway φ) ∪ fv (convert_multiway ψ)"
          unfolding partition_set[OF posneg[symmetric], simplified]
          by (simp add: fv_get_and)
        finally show ?thesis .
      qed
      then have "(⋃x∈set neg. fv x) ⊆ ?fvφ ∪ ?fvψ" using 1 2 by blast
      then show ?thesis unfolding pos_filter by simp
    qed
    have "pos ≠ []"
    proof -
      obtain x where "x ∈ set (get_and_list ?cφ)" "safe_formula x"
        using And_safe ‹safe_formula φ› ex_safe_get_and by (auto simp: list_ex_iff)
      then show ?thesis
        unfolding pos_filter by (auto simp: filter_empty_conv)
    qed
    then show ?thesis unfolding b_def
      using ‹⋃ (fv ` set neg) ⊆ ⋃ (fv ` set pos)› ‹list_all safe_formula (map remove_neg neg)›
        ‹list_all safe_formula pos› posneg
      by simp
  qed
next
  case (And_Not φ ψ)
  let ?a = "And φ (Neg ψ)"
  let ?b = "convert_multiway ?a"
  let ?cφ = "convert_multiway φ"
  let ?cψ = "convert_multiway ψ"
  have b_def: "?b = Ands (Neg ?cψ # get_and_list ?cφ)"
    using And_Not by simp
  show ?case proof -
    let ?l = "Neg ?cψ # get_and_list ?cφ"
    note ‹safe_formula ?cφ›
    then have "list_all safe_neg (get_and_list ?cφ)" by (simp add: safe_get_and)
    moreover have "safe_neg (Neg ?cψ)"
      using ‹safe_formula ?cψ› by (simp add: safe_neg_def)
    then have lsafe_neg: "list_all safe_neg ?l" using calculation by simp
    obtain pos neg where posneg: "(pos, neg) = partition safe_formula ?l" by simp
    then have "list_all safe_formula pos" by (auto simp: list_all_iff)
    then have "list_all safe_formula (map remove_neg neg)"
    proof -
      have "⋀x. x ∈ (set neg) ⟹ safe_formula (remove_neg x)"
      proof -
        fix x assume "x ∈ set neg"
        then have "¬ safe_formula x" using posneg by (auto simp del: filter.simps)
        moreover have "safe_neg x" using lsafe_neg ‹x ∈ set neg›
          unfolding safe_neg_def list_all_iff partition_set[OF posneg[symmetric], symmetric]
          by simp
        ultimately show "safe_formula (remove_neg x)" using safe_neg_def by blast
      qed
      then show ?thesis using Ball_set_list_all by force
    qed

    have pos_filter: "pos = filter safe_formula ?l"
      using posneg by simp
    have neg_filter: "neg = filter (Not ∘ safe_formula) ?l"
      using posneg by simp
    have "(⋃x∈(set neg). fv x) ⊆ (⋃x∈(set pos). fv x)"
    proof -
      have fv_neg: "(⋃x∈(set neg). fv x) ⊆ (⋃x∈(set ?l). fv x)" using posneg by auto
      have "(⋃x∈(set ?l). fv x) ⊆ fv ?cφ ∪ fv ?cψ"
        using ‹safe_formula φ› ‹safe_formula ψ›
        by (simp add: fv_get_and fv_convert_multiway)
      also have "fv ?cφ ∪ fv ?cψ ⊆ fv ?cφ"
        using ‹safe_formula φ› ‹safe_formula ψ› ‹fv (Neg ψ) ⊆ fv φ›
        by (simp add: fv_convert_multiway[symmetric])
      finally have "(⋃x∈(set neg). fv x) ⊆ fv ?cφ"
        using fv_neg unfolding neg_filter by blast
      then show ?thesis
        unfolding pos_filter
        using fv_safe_get_and[OF And_Not.IH(1)]
        by auto
    qed
    have "pos ≠ []"
    proof -
      obtain x where "x ∈ set (get_and_list ?cφ)" "safe_formula x"
        using And_Not.IH ‹safe_formula φ› ex_safe_get_and by (auto simp: list_ex_iff)
      then show ?thesis
        unfolding pos_filter by (auto simp: filter_empty_conv)
    qed
    then show ?thesis unfolding b_def
      using ‹⋃ (fv ` set neg) ⊆ ⋃ (fv ` set pos)› ‹list_all safe_formula (map remove_neg neg)›
        ‹list_all safe_formula pos› posneg
      by simp
  qed
next
  case (Neg φ)
  have "safe_formula (Neg φ') ⟷ safe_formula φ'" if "fv φ' = {}" for φ'
    using that by (cases "Neg φ'" rule: safe_formula.cases) simp_all
  with Neg show ?case by (simp add: fv_convert_multiway)
next
  case (MatchP I r)
  then show ?case
    by (auto 0 3 simp: atms_def fv_convert_multiway intro!: safe_regex_map_regex
      elim!: disjE_Not2 case_NegE
      dest: safe_regex_safe_formula split: if_splits)
next
  case (MatchF I r)
  then show ?case
    by (auto 0 3 simp: atms_def fv_convert_multiway intro!: safe_regex_map_regex
      elim!: disjE_Not2 case_NegE
      dest: safe_regex_safe_formula split: if_splits)
qed (auto simp: fv_convert_multiway)

lemma future_bounded_convert_multiway: "safe_formula φ ⟹ future_bounded (convert_multiway φ) = future_bounded φ"
proof (induction φ rule: safe_formula_induct)
  case (And_safe φ ψ)
  let ?a = "And φ ψ"
  let ?b = "convert_multiway ?a"
  let ?cφ = "convert_multiway φ"
  let ?cψ = "convert_multiway ψ"
  have b_def: "?b = Ands (get_and_list ?cφ @ get_and_list ?cψ)"
    using And_safe by simp
  have "future_bounded ?a = (future_bounded ?cφ ∧ future_bounded ?cψ)"
    using And_safe by simp
  moreover have "future_bounded ?cφ = list_all future_bounded (get_and_list ?cφ)"
    using ‹safe_formula φ› by (simp add: future_bounded_get_and safe_convert_multiway)
  moreover have "future_bounded ?cψ = list_all future_bounded (get_and_list ?cψ)"
    using ‹safe_formula ψ› by (simp add: future_bounded_get_and safe_convert_multiway)
  moreover have "future_bounded ?b = list_all future_bounded (get_and_list ?cφ @ get_and_list ?cψ)"
    unfolding b_def by simp
  ultimately show ?case by simp
next
  case (And_Not φ ψ)
  let ?a = "And φ (Neg ψ)"
  let ?b = "convert_multiway ?a"
  let ?cφ = "convert_multiway φ"
  let ?cψ = "convert_multiway ψ"
  have b_def: "?b = Ands (Neg ?cψ # get_and_list ?cφ)"
    using And_Not by simp
  have "future_bounded ?a = (future_bounded ?cφ ∧ future_bounded ?cψ)"
    using And_Not by simp
  moreover have "future_bounded ?cφ = list_all future_bounded (get_and_list ?cφ)"
    using ‹safe_formula φ› by (simp add: future_bounded_get_and safe_convert_multiway)
  moreover have "future_bounded ?b = list_all future_bounded (Neg ?cψ # get_and_list ?cφ)"
    unfolding b_def by (simp add: list.pred_map o_def)
  ultimately show ?case by auto
next
  case (MatchP I r)
  then show ?case
    by (fastforce simp: atms_def regex.pred_set regex.set_map ball_Un
        elim: safe_regex_safe_formula[THEN disjE_Not2])
next
  case (MatchF I r)
  then show ?case
    by (fastforce simp: atms_def regex.pred_set regex.set_map ball_Un
        elim: safe_regex_safe_formula[THEN disjE_Not2])
qed auto

lemma sat_convert_multiway: "safe_formula φ ⟹ sat σ V v i (convert_multiway φ) ⟷ sat σ V v i φ"
proof (induction φ arbitrary: v i rule: safe_formula_induct)
  case (And_safe φ ψ)
  let ?a = "And φ ψ"
  let ?b = "convert_multiway ?a"
  let ?la = "get_and_list (convert_multiway φ)"
  let ?lb = "get_and_list (convert_multiway ψ)"
  let ?sat = "sat σ V v i"
  have b_def: "?b = Ands (?la @ ?lb)" using And_safe by simp
  have "list_all ?sat ?la ⟷ ?sat φ" using And_safe sat_get_and by blast
  moreover have "list_all ?sat ?lb ⟷ ?sat ψ" using And_safe sat_get_and by blast
  ultimately show ?case using And_safe by (auto simp: list.pred_set)
next
  case (And_Not φ ψ)
  let ?a = "And φ (Neg ψ)"
  let ?b = "convert_multiway ?a"
  let ?la = "get_and_list (convert_multiway φ)"
  let ?lb = "convert_multiway ψ"
  let ?sat = "sat σ V v i"
  have b_def: "?b = Ands (Neg ?lb # ?la)" using And_Not by simp
  have "list_all ?sat ?la ⟷ ?sat φ" using And_Not sat_get_and by blast
  then show ?case using And_Not by (auto simp: list.pred_set)
next
  case (Agg y ω b f φ)
  then show ?case
    by (simp add: nfv_def fv_convert_multiway cong: conj_cong)
next
  case (MatchP I r)
  then have "Regex.match (sat σ V v) (convert_multiway_regex r) = Regex.match (sat σ V v) r"
    unfolding match_map_regex
    by (intro Regex.match_fv_cong)
      (auto 0 4 simp: atms_def elim!: disjE_Not2 dest!: safe_regex_safe_formula)
  then show ?case
    by auto
next
  case (MatchF I r)
  then have "Regex.match (sat σ V v) (convert_multiway_regex r) = Regex.match (sat σ V v) r"
    unfolding match_map_regex
    by (intro Regex.match_fv_cong)
      (auto 0 4 simp: atms_def elim!: disjE_Not2 dest!: safe_regex_safe_formula)
  then show ?case
    by auto
qed (auto cong: nat.case_cong)

end (*context*)

interpretation Formula_slicer: abstract_slicer "relevant_events φ" for φ .

lemma sat_slice_iff:
  assumes "v ∈ S"
  shows "Formula.sat σ V v i φ ⟷ Formula.sat (Formula_slicer.slice φ S σ) V v i φ"
  by (rule sat_slice_strong[OF assms]) auto

lemma Neg_splits:
  "P (case φ of formula.Neg ψ ⇒ f ψ | φ ⇒ g φ) =
   ((∀ψ. φ = formula.Neg ψ ⟶ P (f ψ)) ∧ ((¬ Formula.is_Neg φ) ⟶ P (g φ)))"
  "P (case φ of formula.Neg ψ ⇒ f ψ | _ ⇒ g φ) =
   (¬ ((∃ψ. φ = formula.Neg ψ ∧ ¬ P (f ψ)) ∨ ((¬ Formula.is_Neg φ) ∧ ¬ P (g φ))))"
  by (cases φ; auto simp: Formula.is_Neg_def)+

(*<*)
end
(*>*)