Theory MLTL_Encoding

section ‹ MLTL Encoding ›
theory MLTL_Encoding

imports Main

begin

subsection ‹ Syntax ›

datatype (atoms_mltl: 'a) mltl =
    True_mltl                                     ("Truem")
  | False_mltl                                    ("Falsem")
  | Prop_mltl 'a                                  ("Propm '(_')")
  | Not_mltl "'a mltl"                            ("Notm _" [85] 85)
  | And_mltl "'a mltl" "'a mltl"                  ("_ Andm _" [82, 82] 81)
  | Or_mltl "'a mltl" "'a mltl"                   ("_ Orm _" [81, 81] 80)
  | Future_mltl "nat" "nat" "'a mltl"             ("Fm '[_',_'] _" [88, 88, 88] 87)
  | Global_mltl "nat" "nat" "'a mltl"             ("Gm '[_',_'] _" [88, 88, 88] 87)
  | Until_mltl "'a mltl" "nat" "nat" "'a mltl"    ("_ Um '[_',_'] _" [84, 84, 84, 84] 83)
  | Release_mltl "'a mltl" "nat" "nat" "'a mltl"  ("_ Rm '[_',_'] _" [84, 84, 84, 84] 83)

definition Implies_mltl ("_ Impliesm _" [81, 81] 80)
  where "φ Impliesm ψ ≡ Notm φ Orm ψ"

definition Iff_mltl ("_ Iffm _" [81, 81] 80)
  where "φ Iffm ψ ≡ (φ Impliesm ψ) Andm (ψ Impliesm φ)"

subsubsection ‹ Binding Examples ›
(*Not binds more tightly than And, Or*)
value "Notm Propm (p) Andm Propm (q) =
       And_mltl (Not_mltl (Prop_mltl p)) (Prop_mltl q)"
(*And binds more tightly than Or*)
value "p Andm q Orm r = Or_mltl (And_mltl p q) r"
(*Future and Global binds tighest*)
value "Fm [0, 1] p Andm q = And_mltl (Future_mltl 0 1 p) q"
(*Until and Release bind tighter than And/Or*)
value "p Um [0,1] q Andm r = And_mltl (Until_mltl p 0 1 q) r"

subsection ‹ Semantics ›

(* NOTE: Added π ≠ [] in Prop_mltl *)
primrec semantics_mltl :: "['a set list, 'a mltl] ⇒ bool" ("_ ⊨m _" [80,80] 80)
where
  "π ⊨m Truem = True"
| "π ⊨m Falsem = False"
| "π ⊨m Propm (q) = (π ≠ [] ∧ q ∈ (π ! 0))"
| "π ⊨m Notm φ = (¬ π ⊨m φ)"
| "π ⊨m φ Andm ψ = (π ⊨m φ ∧ π ⊨m ψ)"
| "π ⊨m φ Orm ψ = (π ⊨m φ ∨ π ⊨m ψ)"
| "π ⊨m (Fm [a, b] φ) = (a ≤ b ∧ length π > a ∧
      (∃i::nat. (i ≥ a ∧ i ≤ b) ∧ (drop i π) ⊨m φ))"
| "π ⊨m (Gm [a, b] φ) = (a ≤ b ∧ (length π ≤ a ∨
      (∀i::nat. (i ≥ a ∧ i ≤ b) ⟶ (drop i π) ⊨m φ)))"
| "π ⊨m (φ Um [a, b] ψ) =  (a ≤ b ∧ length π > a ∧
      (∃i::nat. (i ≥ a ∧ i ≤ b) ∧ ((drop i π) ⊨m ψ
        ∧ (∀j. j ≥ a ∧ j<i ⟶ (drop j π) ⊨m φ))))"
| "π ⊨m (φ Rm [a, b] ψ) = (a ≤ b ∧ (length π ≤ a ∨
      (∀i::nat. (i ≥ a ∧ i ≤ b) ⟶ (((drop i π) ⊨m ψ))) ∨
      (∃j. j ≥ a ∧ j ≤ b-1 ∧ (drop j π) ⊨m φ ∧
         (∀k. a ≤ k ∧ k ≤ j ⟶ (drop k π) ⊨m ψ))))"

subsubsection ‹ Examples ›

lemma
  "[{0::nat}] ⊨m Notm (Fm [0,2] Propm (0)) = False"
  by auto

lemma
  "[{0::nat}] ⊨m Fm [0,2] (Notm Propm (0)) = True"
  proof-
    have "¬ (drop 1 [{0}] ≠ [] ∧ 0 ∈ drop 1 [{0}] ! 0)"
      by simp
    then have "(∃i. (0 ≤ i ∧ i ≤ 2) ∧ ¬ (drop i [{0}] ≠ [] ∧ 0 ∈ drop i [{0}] ! 0))"
      by auto
    then show ?thesis
      unfolding semantics_mltl.simps
      by blast
  qed

lemma
  "[{0::nat}] ⊨m Gm [0,2] Propm (0::nat) = False"
  by auto


end