Theory Formula

(*<*)
theory Formula
  imports Trace
begin
(*>*)

section ‹Metric First-Order Temporal Logic›

subsection ‹Syntax›

type_synonym ('n, 'a) event = "('n × 'a list)"
type_synonym ('n, 'a) database = "('n, 'a) event set"
type_synonym ('n, 'a) prefix = "('n × 'a list) prefix"
type_synonym ('n, 'a) trace = "('n × 'a list) trace"
type_synonym ('n, 'a) env = "'n ⇒ 'a"
type_synonym ('n, 'a) envset = "'n ⇒ 'a set"

datatype (fv_trm: 'n, 'a) trm = is_Var: Var 'n (‹v›) | is_Const: Const 'a (‹c›)

lemma in_fv_trm_conv: "x ∈ fv_trm t ⟷ t = v x"
  by (cases t) auto

datatype ('n, 'a) formula = 
  TT                                            (‹⊤›)
| FF                                            (‹⊥›)
| Eq_Const 'n 'a                                (‹_ ≈ _› [85, 85] 85)
| Pred 'n "('n, 'a) trm list"                   (‹_ † _› [85, 85] 85)
| Neg "('n, 'a) formula"                        (‹¬F _› [82] 82)
| Or "('n, 'a) formula" "('n, 'a) formula"      (infixr ‹∨F› 80)
| And "('n, 'a) formula" "('n, 'a) formula"     (infixr ‹∧F› 80)
| Imp "('n, 'a) formula" "('n, 'a) formula"     (infixr ‹⟶F› 79)
| Iff "('n, 'a) formula" "('n, 'a) formula"     (infixr ‹⟷F› 79)
| Exists "'n" "('n, 'a) formula"                (‹∃F_. _› [70,70] 70)
| Forall "'n" "('n, 'a) formula"                (‹∀F_. _› [70,70] 70)
| Prev ℐ "('n, 'a) formula"                     (‹Y _ _› [1000, 65] 65)
| Next ℐ "('n, 'a) formula"                     (‹X _ _› [1000, 65] 65)
| Once ℐ "('n, 'a) formula"                     (‹P _ _› [1000, 65] 65)
| Historically ℐ "('n, 'a) formula"             (‹H _ _› [1000, 65] 65)
| Eventually ℐ "('n, 'a) formula"               (‹F _ _› [1000, 65] 65)
| Always ℐ "('n, 'a) formula"                   (‹G _ _› [1000, 65] 65)
| Since "('n, 'a) formula" ℐ "('n, 'a) formula" (‹_ S _ _› [60,1000,60] 60)
| Until "('n, 'a) formula" ℐ "('n, 'a) formula" (‹_ U _ _› [60,1000,60] 60)

primrec fv :: "('n, 'a) formula ⇒ 'n set" where
  "fv (r † ts) = ⋃ (fv_trm ` set ts)"
| "fv ⊤ = {}"
| "fv ⊥ = {}"
| "fv (x ≈ c) = {x}"
| "fv (¬F φ) = fv φ"
| "fv (φ ∨F ψ) = fv φ ∪ fv ψ"
| "fv (φ ∧F ψ) = fv φ ∪ fv ψ"
| "fv (φ ⟶F ψ) = fv φ ∪ fv ψ"
| "fv (φ ⟷F ψ) = fv φ ∪ fv ψ"
| "fv (∃Fx. φ) = fv φ - {x}"
| "fv (∀Fx. φ) = fv φ - {x}"
| "fv (Y I φ) = fv φ"
| "fv (X I φ) = fv φ"
| "fv (P I φ) = fv φ"
| "fv (H I φ) = fv φ"
| "fv (F I φ) = fv φ"
| "fv (G I φ) = fv φ"
| "fv (φ S I ψ) = fv φ ∪ fv ψ"
| "fv (φ U I ψ) = fv φ ∪ fv ψ"

primrec "consts" :: "('n, 'a) formula ⇒ 'a set" where
  "consts (r † ts) = {}" ― ‹terms may also contain constants,
     but these only filter out values from the trace and do not introduce
     new values of interest (i.e., do not extend the active domain)›
| "consts ⊤ = {}"
| "consts ⊥ = {}"
| "consts (x ≈ c) = {c}"
| "consts (¬F φ) = consts φ"
| "consts (φ ∨F ψ) = consts φ ∪ consts ψ"
| "consts (φ ∧F ψ) = consts φ ∪ consts ψ"
| "consts (φ ⟶F ψ) = consts φ ∪ consts ψ"
| "consts (φ ⟷F ψ) = consts φ ∪ consts ψ"
| "consts (∃Fx. φ) = consts φ"
| "consts (∀Fx. φ) = consts φ"
| "consts (Y I φ) = consts φ"
| "consts (X I φ) = consts φ"
| "consts (P I φ) = consts φ"
| "consts (H I φ) = consts φ"
| "consts (F I φ) = consts φ"
| "consts (G I φ) = consts φ"
| "consts (φ S I ψ) = consts φ ∪ consts ψ"
| "consts (φ U I ψ) = consts φ ∪ consts ψ"

lemma finite_fv_trm[simp]: "finite (fv_trm t)"
  by (cases t) simp_all

lemma finite_fv[simp]: "finite (fv φ)"
  by (induction φ) simp_all

lemma finite_consts[simp]: "finite (consts φ)"
  by (induction φ) simp_all

definition nfv :: "('n, 'a) formula ⇒ nat" where
  "nfv φ = card (fv φ)"

fun future_bounded :: "('n, 'a) formula ⇒ bool" where
  "future_bounded ⊤ = True"
| "future_bounded ⊥ = True"
| "future_bounded (_ † _) = True"
| "future_bounded (_ ≈ _) = True"
| "future_bounded (¬F φ) = future_bounded φ"
| "future_bounded (φ ∨F ψ) = (future_bounded φ ∧ future_bounded ψ)"
| "future_bounded (φ ∧F ψ) = (future_bounded φ ∧ future_bounded ψ)"
| "future_bounded (φ ⟶F ψ) = (future_bounded φ ∧ future_bounded ψ)"
| "future_bounded (φ ⟷F ψ) = (future_bounded φ ∧ future_bounded ψ)"
| "future_bounded (∃F_. φ) = future_bounded φ"
| "future_bounded (∀F_. φ) = future_bounded φ"
| "future_bounded (Y I φ) = future_bounded φ"
| "future_bounded (X I φ) = future_bounded φ"
| "future_bounded (P I φ) = future_bounded φ"
| "future_bounded (H I φ) = future_bounded φ"
| "future_bounded (F I φ) = (future_bounded φ ∧ right I ≠ ∞)"
| "future_bounded (G I φ) = (future_bounded φ ∧ right I ≠ ∞)"
| "future_bounded (φ S I ψ) = (future_bounded φ ∧ future_bounded ψ)"
| "future_bounded (φ U I ψ) = (future_bounded φ ∧ future_bounded ψ ∧ right I ≠ ∞)"

subsection ‹Semantics›

primrec eval_trm :: "('n, 'a) env ⇒ ('n, 'a) trm ⇒ 'a"(‹_⟦_⟧› [70,89] 89) where
  "eval_trm v (v x) = v x"
| "eval_trm v (c x) = x"

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

definition eval_trms :: "('n, 'a) env ⇒ ('n, 'a) trm list ⇒ 'a list" (‹_⟦_⟧› [70,89] 89) where
  "eval_trms v ts = map (eval_trm v) ts"

lemma eval_trms_fv_cong: 
  "∀t∈set ts. ∀x∈fv_trm t. v x = v' x ⟹ v⟦ts⟧ = v'⟦ts⟧"
  using eval_trm_fv_cong[of _ v v']
  by (auto simp: eval_trms_def)

(* vs :: "'a envset" is used whenever we define executable functions *)
primrec eval_trm_set :: "('n, 'a) envset ⇒ ('n, 'a) trm ⇒ ('n, 'a) trm × 'a set"(‹_⦃_⦄› [70,89] 89) where
  "eval_trm_set vs (v x) = (v x, vs x)"
| "eval_trm_set vs (c x) = (c x, {x})"

definition eval_trms_set :: "('n, 'a) envset ⇒ ('n, 'a) trm list ⇒ (('n, 'a) trm × 'a set) list" (‹_⦃_⦄› [70,89] 89)
  where "eval_trms_set vs ts = map (eval_trm_set vs) ts"

lemma eval_trms_set_Nil: "vs⦃[]⦄ = []"
  by (simp add: eval_trms_set_def)

lemma eval_trms_set_Cons: 
  "vs⦃(t # ts)⦄ = vs⦃t⦄ # vs⦃ts⦄"
  by (simp add: eval_trms_set_def)

primrec sat :: "('n, 'a) trace ⇒ ('n, 'a) env ⇒ nat ⇒ ('n, 'a) formula ⇒ bool" (‹⟨_, _, _⟩ ⊨ _› [56, 56, 56, 56] 55) where
  "⟨σ, v, i⟩ ⊨ ⊤ = True"
| "⟨σ, v, i⟩ ⊨ ⊥ = False"
| "⟨σ, v, i⟩ ⊨ r † ts = ((r, v⟦ts⟧) ∈ Γ σ i)"
| "⟨σ, v, i⟩ ⊨ x ≈ c = (v x = c)"
| "⟨σ, v, i⟩ ⊨ ¬F φ = (¬ ⟨σ, v, i⟩ ⊨ φ)"
| "⟨σ, v, i⟩ ⊨ φ ∨F ψ = (⟨σ, v, i⟩ ⊨ φ ∨ ⟨σ, v, i⟩ ⊨ ψ)"
| "⟨σ, v, i⟩ ⊨ φ ∧F ψ = (⟨σ, v, i⟩ ⊨ φ ∧ ⟨σ, v, i⟩ ⊨ ψ)"
| "⟨σ, v, i⟩ ⊨ φ ⟶F ψ = (⟨σ, v, i⟩ ⊨ φ ⟶ ⟨σ, v, i⟩ ⊨ ψ)"
| "⟨σ, v, i⟩ ⊨ φ ⟷F ψ = (⟨σ, v, i⟩ ⊨ φ ⟷ ⟨σ, v, i⟩ ⊨ ψ)"
| "⟨σ, v, i⟩ ⊨ ∃Fx. φ = (∃z. ⟨σ, v(x := z), i⟩ ⊨ φ)"
| "⟨σ, v, i⟩ ⊨ ∀Fx. φ = (∀z. ⟨σ, v(x := z), i⟩ ⊨ φ)"
| "⟨σ, v, i⟩ ⊨ Y I φ = (case i of 0 ⇒ False | Suc j ⇒ mem (τ σ i - τ σ j) I ∧ ⟨σ, v, j⟩ ⊨ φ)"
| "⟨σ, v, i⟩ ⊨ X I φ = (mem (τ σ (Suc i) - τ σ i) I ∧ ⟨σ, v, Suc i⟩ ⊨ φ)"
| "⟨σ, v, i⟩ ⊨ P I φ = (∃j≤i. mem (τ σ i - τ σ j) I ∧ ⟨σ, v, j⟩ ⊨ φ)"
| "⟨σ, v, i⟩ ⊨ H I φ = (∀j≤i. mem (τ σ i - τ σ j) I ⟶ ⟨σ, v, j⟩ ⊨ φ)"
| "⟨σ, v, i⟩ ⊨ F I φ = (∃j≥i. mem (τ σ j - τ σ i) I ∧ ⟨σ, v, j⟩ ⊨ φ)"
| "⟨σ, v, i⟩ ⊨ G I φ = (∀j≥i. mem (τ σ j - τ σ i) I ⟶ ⟨σ, v, j⟩ ⊨ φ)"
| "⟨σ, v, i⟩ ⊨ φ S I ψ = (∃j≤i. mem (τ σ i - τ σ j) I ∧ ⟨σ, v, j⟩ ⊨ ψ ∧ (∀k∈{j<..i}. ⟨σ, v, k⟩ ⊨ φ))"
| "⟨σ, v, i⟩ ⊨ φ U I ψ = (∃j≥i. mem (τ σ j - τ σ i) I ∧ ⟨σ, v, j⟩ ⊨ ψ ∧ (∀k∈{i..<j}. ⟨σ, v, k⟩ ⊨ φ))"

lemma sat_fv_cong: "∀x∈fv φ. v x = v' x ⟹ ⟨σ, v, i⟩ ⊨ φ = ⟨σ, v', i⟩ ⊨ φ"
proof (induct φ arbitrary: v v' i)
  case (Pred n ts)
  thus ?case
    by (simp cong: map_cong eval_trms_fv_cong[rule_format, OF Pred[simplified, rule_format]] 
        split: option.splits)
next
  case (Exists t φ)
  then show ?case unfolding sat.simps 
    by (intro iff_exI) (simp add: nth_Cons')
next
  case (Forall t φ)
  then show ?case unfolding sat.simps 
    by (intro iff_allI) (simp add: nth_Cons')
qed (auto 10 0 simp: Let_def split: nat.splits intro!: iff_exI eval_trm_fv_cong)

lemma sat_Until_rec: "⟨σ, v, i⟩ ⊨ φ U I ψ ⟷
  (mem 0 I ∧ ⟨σ, v, i⟩ ⊨ ψ ∨
   Δ σ (i + 1) ≤ right I ∧ ⟨σ, v, i⟩ ⊨ φ ∧ ⟨σ, v, i + 1⟩ ⊨ φ U (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" "⟨σ, v, j⟩ ⊨ ψ" "∀k ∈ {i ..< j}. ⟨σ, 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 "⟨σ, v, i⟩ ⊨ φ" by auto
    moreover from False j have "⟨σ, v, i + 1⟩ ⊨ φ U (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: "⟨σ, v, i⟩ ⊨ φ" and
   "next": "⟨σ, v, i + 1⟩ ⊨ φ U (subtract (Δ σ (i + 1)) I) ψ"
  from "next" obtain j where j: "i + 1 ≤ j" "mem (τ σ j - τ σ (i + 1)) (subtract (Δ σ (i + 1)) I)"
      "⟨σ, v, j⟩ ⊨ ψ" "∀k ∈ {i + 1 ..< j}. ⟨σ, 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: "⟨σ, v, i⟩ ⊨ φ S I ψ ⟷
  mem 0 I ∧ ⟨σ, v, i⟩ ⊨ ψ ∨
  (i > 0 ∧ Δ σ i ≤ right I ∧ ⟨σ, v, i⟩ ⊨ φ ∧ ⟨σ, v, i - 1⟩ ⊨ φ S (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" "⟨σ, v, j⟩ ⊨ ψ" "∀k ∈ {j <.. i}. ⟨σ, 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 "⟨σ, v, i⟩ ⊨ φ" by auto
    moreover from False j have "⟨σ, v, i - 1⟩ ⊨ φ S (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: "⟨σ, v, i⟩ ⊨ φ" and
   "prev": "⟨σ, v, i - 1⟩ ⊨ φ S (subtract (Δ σ i) I) ψ"
  from "prev" obtain j where j: "j ≤ i - 1" "mem (τ σ (i - 1) - τ σ j) ((subtract (Δ σ i) I))"
      "⟨σ, v, j⟩ ⊨ ψ" "∀k ∈ {j <.. i - 1}. ⟨σ, 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: "⟨σ, v, 0⟩ ⊨ φ S I ψ ⟷ mem 0 I ∧ ⟨σ, v, 0⟩ ⊨ ψ"
  by auto

lemma sat_Since_point: "⟨σ, v, i⟩ ⊨ φ S I ψ ⟹
    (⋀j. j ≤ i ⟹ mem (τ σ i - τ σ j) I ⟹ ⟨σ, v, i⟩ ⊨ φ S (point (τ σ i - τ σ j)) ψ ⟹ P) ⟹ P"
  by (auto intro: diff_le_self)

lemma sat_Since_pointD: "⟨σ, v, i⟩ ⊨ φ S (point t) ψ ⟹ mem t I ⟹ ⟨σ, v, i⟩ ⊨ φ S I ψ"
  by auto

lemma sat_Once_Since: "⟨σ, v, i⟩ ⊨ P I φ = ⟨σ, v, i⟩ ⊨ ⊤ S I φ"
  by auto

lemma sat_Once_rec: "⟨σ, v, i⟩ ⊨ P I φ ⟷
  mem 0 I ∧ ⟨σ, v, i⟩ ⊨ φ ∨ 
  (i > 0 ∧ Δ σ i ≤ right I ∧ ⟨σ, v, i - 1⟩ ⊨ P (subtract (Δ σ i) I) φ)"
  unfolding sat_Once_Since
  by (subst sat_Since_rec) auto

lemma sat_Historically_Once: "⟨σ, v, i⟩ ⊨ H I φ = ⟨σ, v, i⟩ ⊨ ¬F (P I ¬F φ)"
  by auto

lemma sat_Historically_rec: "⟨σ, v, i⟩ ⊨ H I φ ⟷
  (mem 0 I ⟶ ⟨σ, v, i⟩ ⊨ φ) ∧ 
  (i > 0 ⟶ Δ σ i ≤ right I ⟶ ⟨σ, v, i - 1⟩ ⊨ H (subtract (Δ σ i) I) φ)"
  unfolding sat_Historically_Once sat.simps(5)
  by (subst sat_Once_rec) auto

lemma sat_Eventually_Until: "⟨σ, v, i⟩ ⊨ F I φ = ⟨σ, v, i⟩ ⊨ ⊤ U I φ"
  by auto

lemma sat_Eventually_rec: "⟨σ, v, i⟩ ⊨ F I φ ⟷
  mem 0 I ∧ ⟨σ, v, i⟩ ⊨ φ ∨ 
  (Δ σ (i + 1) ≤ right I ∧ ⟨σ, v, i + 1⟩ ⊨ F (subtract (Δ σ (i + 1)) I) φ)"
  unfolding sat_Eventually_Until
  by (subst sat_Until_rec) auto

lemma sat_Always_Eventually: "⟨σ, v, i⟩ ⊨ G I φ = ⟨σ, v, i⟩ ⊨ ¬F (F I ¬F φ)"
  by auto

lemma sat_Always_rec: "⟨σ, v, i⟩ ⊨ G I φ ⟷
  (mem 0 I ⟶ ⟨σ, v, i⟩ ⊨ φ) ∧ 
  (Δ σ (i + 1) ≤ right I ⟶ ⟨σ, v, i + 1⟩ ⊨ G (subtract (Δ σ (i + 1)) I) φ)"
  unfolding sat_Always_Eventually sat.simps(5)
  by (subst sat_Eventually_rec) auto

bundle MFOTL_syntax
begin

text ‹ For bold font, type ``backslash'' followed by the word ``bold''  ›
notation Var (‹v›)
     and Const (‹c›)

text ‹ For subscripts type ``backslash'' followed by ``sub''  ›
notation TT (‹⊤›)
     and FF (‹⊥›)
     and Pred (‹_ † _› [85, 85] 85)
     and Eq_Const (‹_ ≈ _› [85, 85] 85)
     and Neg (‹¬F _› [82] 82)
     and And (infixr ‹∧F› 80)
     and Or (infixr ‹∨F› 80)
     and Imp (infixr ‹⟶F› 79)
     and Iff (infixr ‹⟷F› 79)
     and Exists (‹∃F_. _› [70,70] 70)
     and Forall (‹∀F_. _› [70,70] 70)
     and Prev (‹Y _ _› [1000, 65] 65)
     and Next (‹X _ _› [1000, 65] 65)
     and Once (‹P _ _› [1000, 65] 65)
     and Eventually (‹F _ _› [1000, 65] 65)
     and Historically (‹H _ _› [1000, 65] 65)
     and Always (‹G _ _› [1000, 65] 65)
     and Since (‹_ S _ _› [60,1000,60] 60)
     and Until (‹_ U _ _› [60,1000,60] 60)

notation eval_trm (‹_⟦_⟧› [70,89] 89)
     and eval_trms (‹_⟦_⟧› [70,89] 89)
     and eval_trm_set (‹_⦃_⦄› [70,89] 89)
     and eval_trms_set (‹_⦃_⦄› [70,89] 89)
     and sat (‹⟨_, _, _⟩ ⊨ _› [56, 56, 56, 56] 55)
     and Interval.interval (‹[_,_]›)

end

unbundle no MFOTL_syntax

(*<*)
end
(*>*)