Theory LinearTemporalLogic

theory LinearTemporalLogic
imports Traces AnswerIndexedFamilies Main
begin

chapter ‹Linear-time Temporal Logic›

datatype (atoms_ltl: 'a) ltl =
      True_ltl                             (‹true⇩l›)
    | Not_ltl ‹'a ltl›                     (‹not⇩l _› [85] 85)
    | Prop_ltl ‹'a›                          (‹prop⇩l'(_')›)
    | Or_ltl ‹'a ltl› ‹'a ltl›             (‹_ or⇩l _› [82,82] 81)
    | And_ltl ‹'a ltl› ‹'a ltl›            (‹_ and⇩l _  › [82,82] 81)
    | Next_ltl ‹'a ltl›                    (‹X⇩l _› [88] 87)
    | Until_ltl ‹'a ltl› ‹'a ltl›          (‹_ U⇩l  _› [84,84] 83)

fun lsatisfying_AiF :: ‹'a ⇒ 'a state infinite_trace AiF› (‹lsat∙›) where
‹lsat∙ x T = {t. x ∈ L (t 0)}› |
‹lsat∙ x F = {t. x ∉ L (t 0)}›

fun x_operator :: ‹'a infinite_trace AiF ⇒ 'a infinite_trace AiF› (‹X·›) where
‹X· t T = {x | x. itdrop 1 x ∈ (t T)}›|
‹X· t F = {x | x. itdrop 1 x ∈ (t F)}›

fun u_operator :: ‹'a infinite_trace AiF ⇒ 'a infinite_trace AiF ⇒ 'a infinite_trace AiF› (infix ‹U·› 61) where
‹(a U· b) T = {x | x. ∃k. (∀i<k. itdrop i x ∈ (a T)) ∧ itdrop k x ∈ (b T)}›|
‹(a U· b) F = {x | x. ∀k. (∃i<k. itdrop i x ∈ (a F)) ∨ itdrop k x ∈ (b F)}›

fun ltl_semantics :: ‹'a ltl ⇒ 'a state infinite_trace AiF› (‹⟦_⟧⇩l›) where
‹⟦ true⇩l    ⟧⇩l = T∙›|
‹⟦ not⇩l φ   ⟧⇩l = ¬· ⟦ φ ⟧⇩l›|
‹⟦ prop⇩l(a) ⟧⇩l = lsat∙ a›|
‹⟦ φ or⇩l ψ  ⟧⇩l = ⟦ φ ⟧⇩l ∨· ⟦ ψ ⟧⇩l›|
‹⟦ φ and⇩l ψ ⟧⇩l = ⟦ φ ⟧⇩l ∧· ⟦ ψ ⟧⇩l›|
‹⟦ X⇩l φ     ⟧⇩l = X· ⟦ φ ⟧⇩l›|
‹⟦ φ U⇩l ψ   ⟧⇩l = ⟦ φ ⟧⇩l U· ⟦ ψ ⟧⇩l›

lemma excluded_middle_ltl' : 
  shows ‹(Γ ∉ ⟦φ⟧⇩l T) ⟷ (Γ ∈ ⟦φ⟧⇩l F)›
  and   ‹(Γ ∉ ⟦φ⟧⇩l F) ⟷ (Γ ∈ ⟦φ⟧⇩l T)›
proof (induct ‹φ› arbitrary: ‹Γ›)
qed auto

lemma excluded_middle_ltl: ‹Γ ∈ ⟦φ⟧⇩l T ∨ Γ ∈ ⟦φ⟧⇩l F›
  using excluded_middle_ltl' by blast

definition false_ltl (‹false⇩l›) where
  false_ltl_def[simp]: ‹false⇩l = not⇩l true⇩l›

definition implies_ltl :: ‹'a ltl ⇒ 'a ltl ⇒ 'a ltl› (infix ‹implies⇩l› 80)  where
  implies_ltl_def[simp]: ‹φ implies⇩l ψ = (not⇩l φ or⇩l ψ)›

definition final_ltl :: ‹'a ltl ⇒ 'a ltl› (‹F⇩l _›) where
  final_ltl_def[simp]: ‹(F⇩l φ) = (true⇩l U⇩l φ)›

definition global_ltl :: ‹'a ltl ⇒ 'a ltl› (‹G⇩l _›) where
  global_ltl_def[simp]: ‹(G⇩l φ) = (not⇩l F⇩l (not⇩l φ))›

section ‹Linear temporal logic equivalence›

fun ltl_semantics' :: ‹'a state infinite_trace ⇒ 'a ltl ⇒ bool› (infix ‹⊨⇩l› 60) where
  ‹Γ ⊨⇩l true⇩l    = True›
| ‹Γ ⊨⇩l not⇩l φ   = (¬ Γ ⊨⇩l φ)›
| ‹Γ ⊨⇩l prop⇩l(a) = (a ∈ L (Γ 0))›
| ‹Γ ⊨⇩l φ or⇩l ψ  = (Γ ⊨⇩l φ ∨ Γ ⊨⇩l ψ)›
| ‹Γ ⊨⇩l φ and⇩l ψ = (Γ ⊨⇩l φ ∧ Γ ⊨⇩l ψ)›
| ‹Γ ⊨⇩l (X⇩l φ)   = itdrop 1 Γ ⊨⇩l φ›
| ‹Γ ⊨⇩l (φ U⇩l ψ) = (∃k. (∀i<k. itdrop i Γ ⊨⇩l φ) ∧ itdrop k Γ ⊨⇩l ψ)›


section ‹Linear temporal logic lemmas›
lemma ‹⟦ F⇩l (F⇩l φ) ⟧⇩l = ⟦ F⇩l φ ⟧⇩l›
proof (rule AiF_cases)
  show ‹⟦F⇩l F⇩l φ⟧⇩l T = ⟦F⇩l φ⟧⇩l T›
    apply (clarsimp intro!: set_eqI, rule)
     apply auto[1]
    by (clarsimp, metis add_0)
next
  show ‹⟦F⇩l F⇩l φ⟧⇩l F = ⟦F⇩l φ⟧⇩l F›
    apply (clarsimp intro!: set_eqI, rule)
     apply (clarsimp, metis add_0)
    by simp
qed

lemma ltl_equivalence: 
  shows ‹   Γ ⊨⇩l φ  = (Γ ∈ ⟦ φ ⟧⇩l T)›
  and   ‹(¬ Γ ⊨⇩l φ) = (Γ ∈ ⟦ φ ⟧⇩l F)›
proof(induct ‹φ› arbitrary: ‹Γ›)
qed auto

end