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
(*>*)