Quelle  Formula.thy

(*<*)
theory Formula
  imports Trace Regex
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 I "('n, 'a) formula"                     (‹Y _ _› [1000, 65] 65)
| Next I "('n, 'a) formula"                     (‹X _ _› [1000, 65] 65)
| Once I "('n, 'a) formula"                     (‹P _ _› [1000, 65] 65)
| Historically I "('n, 'a) formula"             (‹H _ _› [1000, 65] 65)
| Eventually I "('n, 'a) formula"               (‹F _ _› [1000, 65] 65)
| Always I "('n, 'a) formula"                   (‹G _ _› [1000, 65] 65)
| Since "('n, 'a) formula" I "('n, 'a) formula" (‹_ S _ _› [60,1000,60] 60)
| Until "('n, 'a) formula" I "('n, 'a) formula" (‹_ U _ _› [60,1000,60] 60)
| MatchP I "('n, 'a) formula Regex.regex" (‹\◃ _ _› [1000,60] 60)
| MatchF I "('n, 'a) formula Regex.regex" (‹\▹ _ _› [1000,60] 60)

fun fv :: "('n, 'a) formula ==> 'n set" where
  "fv (r † ts) = ∪ (fv_trm ` set ts)"
| "fv \<top> = {}"
| "fv \<bottom> = {}"
| "fv (x \<approx> 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 ψ"
| "fv (\<triangleleft> I r) = Regex.collect fv r"
| "fv (\<triangleright> I r) = Regex.collect fv r"

fun "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 \<top> = {}"
| "consts \<bottom> = {}"
| "consts (x \<approx> 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 ψ"
| "consts (\<triangleleft> I r) = Regex.collect consts r"
| "consts (\<triangleright> I r) = Regex.collect consts r"

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 \<top> = True"
| "future_bounded \<bottom> = True"
| "future_bounded (_ † _) = True"
| "future_bounded (_ \<approx> _) = 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 ≠ ∞)"
| "future_bounded (\<triangleleft> I r) = Regex.pred_regex future_bounded r"
| "future_bounded (\<triangleright> I r) = (Regex.pred_regex future_bounded r ∧ 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\<lbrakk>ts\<rbrakk> = v'\<lbrakk>ts\<rbrakk>"
  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\<lbrace>[]\<rbrace> = []"
  by (simp add: eval_trms_set_def)

lemma eval_trms_set_Cons: 
  "vs\<lbrace>(t # ts)\<rbrace> = vs{t} # vs\<lbrace>ts\<rbrace>"
  by (simp add: eval_trms_set_def)

fun sat :: "('n, 'a) trace ==> ('n, 'a) env ==> nat ==> ('n, 'a) formula ==> bool" (‹⟨_, _, _⟩ ⊨ _› [56, 56, 56, 56] 55) where
  "⟨σ, v, i⟩ ⊨ \<top> = True"
| "⟨σ, v, i⟩ ⊨ \<bottom> = False"
| "⟨σ, v, i⟩ ⊨ r † ts = ((r, v\<lbrakk>ts\<rbrakk>) ∈ Γ σ i)"
| "⟨σ, v, i⟩ ⊨ x \<approx> 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⟩ ⊨ φ))"
| "⟨σ, v, i⟩ ⊨ (\<triangleleft> I r) = (∃j≤i. mem (τ σ i - τ σ j) I ∧ Regex.match (λk φ. ⟨σ, v, k⟩ ⊨ φ) r j i)"
| "⟨σ, v, i⟩ ⊨ (\<triangleright> I r) = (∃j≥i. mem (τ σ j - τ σ i) I ∧ Regex.match (λk φ. ⟨σ, v, k⟩ ⊨ φ) r i j)"

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 collect_alt split: nat.splits intro!: iff_exI eval_trm_fv_cong
  elim!: match_cong_strong[THEN iffD1, rotated])

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⟩ ⊨ \<top> 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⟩ ⊨ \<top> 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
(*>*)