LTL

LTL.thy

theory LTL
  imports Main
begin

datatype 'a LTL
  = Latom 'a
  | Ltrue
  | Lor "'a LTL" "'a LTL" (infixl "∨t" 81)
  | Lnot "'a LTL" ("¬t _" [85] 85)
  | Lnext "'a LTL" ("○ _" [88] 87)
  | Luntil "'a LTL" "'a LTL" (infixr "∪t" 83)

definition Land (infixl "∧t" 82) where
  "Land p q = ¬t (¬t p ∨t ¬t q)"

definition Limp (infixr "→t" 80) where
  "Limp p q = ¬t p ∨t q"

definition Liff (infixl "↔t" 80) where
  "Liff p q = (p →t q) ∧t (q →t p)"

definition Lfalse where
  "Lfalse = ¬t Ltrue"

definition Lrelease (infixr "Rt" 83) where
  "Lrelease p q = ¬t (¬t p ∪t ¬t q)"

definition Lfinally ("◇ _" [88] 87) where
  "Lfinally p = Ltrue ∪t p"

definition Lglobally ("□ _" [88] 87) where
  "Lglobally p = Lfalse Rt p"

fun shift :: "(nat ⇒ 'a set) ⇒ nat ⇒ (nat ⇒ 'a set)" where
  "shift w n = (λk. w (n + k))"

primrec kripke_semantics :: "(nat ⇒ 'a set) ⇒ 'a LTL ⇒ bool" ("_ ⊨ _" [80,80] 80) where
  "w ⊨ Latom p = (p ∈ w 0)"
| "w ⊨ Ltrue = True"
| "w ⊨ p ∨t q = (w ⊨ p ∨ w ⊨ q)"
| "w ⊨ ¬t p = (¬ w ⊨ p)"
| "w ⊨ ○ p = shift w 1 ⊨ p"
| "w ⊨ p ∪t q = (∃i ≥ 0. shift w i ⊨ q ∧ (∀k. 0 ≤ k ∧ k < i ⟶ shift w k ⊨ p))"

definition valid ("⊨ _" [80] 80) where
  "⊨ p = (∀w. w ⊨ p)"

lemma notF_iff_G: "⊨ (¬t ◇ (¬t p)) = ⊨ □ p"
  unfolding Lfinally_def Lglobally_def Lrelease_def Lfalse_def valid_def
  apply simp
  done

(* Examples *)

datatype Color = red | green | yellow

locale traffic =
  assumes red_to_green: "○ (Latom red) = Latom green"
  and green_to_yellow: "○ (Latom green) = Latom yellow"
  and yellow_to_red: "○ (Latom yellow) = Latom red"

lemma (in traffic) "⊨ ○ (Latom green) →t ◇ (Latom red)"
  using red_to_green by auto