(*<*)
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: "∀x∈fv_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 I "'a formula" | Next I "'a formula"
  | Since "'a formula" I "'a formula" | Until "'a formula" I "'a formula"

qualified primrec fvi :: "nat → 'a formula → nat set" where
  "fvi b (Pred r ts) = (∪t∈set 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 "∀i∈fvi (Suc b) φ. i < n"
  shows "∀i∈fvi 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: "∀i∈fv φ. 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 ψ) = (∃j≤i. mem (τ σ i - τ σ j) I ∧ sat σ v j ψ ∧ (∀k ∈ {j <.. i}. sat σ v k φ))"
| "sat σ v i (Until φ I ψ) = (∃j≥i. 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: "∀x∈fv_trm t. v!x = v'!x ==> eval_trm v t = eval_trm v' t"
  by (cases t) simp_all

lemma sat_fvi_cong: "∀x∈fv φ. 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: "∀x∈fv φ. 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
(*>*)