Theory TL

(*  Title:      HOL/HOLCF/IOA/TL.thy
    Author:     Olaf Müller
*)

section ‹A General Temporal Logic›

theory TL
imports Pred Sequence
begin

default_sort type

type_synonym 'a temporal = "'a Seq predicate"

definition validT :: "'a Seq predicate ⇒ bool"    ("❙⊫ _" [9] 8)
  where "(❙⊫ P) ⟷ (∀s. s ≠ UU ∧ s ≠ nil ⟶ (s ⊨ P))"

definition unlift :: "'a lift ⇒ 'a"
  where "unlift x = (case x of Def y ⇒ y)"

definition Init :: "'a predicate ⇒ 'a temporal"  ("⟨_⟩" [0] 1000)
  where "Init P s = P (unlift (HD ⋅ s))"
    ― ‹this means that for ‹nil› and ‹UU› the effect is unpredictable›

definition Next :: "'a temporal ⇒ 'a temporal"  ("○(_)" [80] 80)
  where "(○P) s ⟷ (if TL ⋅ s = UU ∨ TL ⋅ s = nil then P s else P (TL ⋅ s))"

definition suffix :: "'a Seq ⇒ 'a Seq ⇒ bool"
  where "suffix s2 s ⟷ (∃s1. Finite s1 ∧ s = s1 @@ s2)"

definition tsuffix :: "'a Seq ⇒ 'a Seq ⇒ bool"
  where "tsuffix s2 s ⟷ s2 ≠ nil ∧ s2 ≠ UU ∧ suffix s2 s"

definition Box :: "'a temporal ⇒ 'a temporal"  ("□(_)" [80] 80)
  where "(□P) s ⟷ (∀s2. tsuffix s2 s ⟶ P s2)"

definition Diamond :: "'a temporal ⇒ 'a temporal"  ("◇(_)" [80] 80)
  where "◇P = (❙¬ (□(❙¬ P)))"

definition Leadsto :: "'a temporal ⇒ 'a temporal ⇒ 'a temporal"  (infixr "↝" 22)
  where "(P ↝ Q) = (□(P ❙⟶ (◇Q)))"


lemma simple: "□◇(❙¬ P) = (❙¬ ◇□P)"
  by (auto simp add: Diamond_def NOT_def Box_def)

lemma Boxnil: "nil ⊨ □P"
  by (simp add: satisfies_def Box_def tsuffix_def suffix_def nil_is_Conc)

lemma Diamondnil: "¬ (nil ⊨ ◇P)"
  using Boxnil by (simp add: Diamond_def satisfies_def NOT_def)

lemma Diamond_def2: "(◇F) s ⟷ (∃s2. tsuffix s2 s ∧ F s2)"
  by (simp add: Diamond_def NOT_def Box_def)


subsection ‹TLA Axiomatization by Merz›

lemma suffix_refl: "suffix s s"
  apply (simp add: suffix_def)
  apply (rule_tac x = "nil" in exI)
  apply auto
  done

lemma reflT: "s ≠ UU ∧ s ≠ nil ⟶ (s ⊨ □F ❙⟶ F)"
  apply (simp add: satisfies_def IMPLIES_def Box_def)
  apply (rule impI)+
  apply (erule_tac x = "s" in allE)
  apply (simp add: tsuffix_def suffix_refl)
  done

lemma suffix_trans: "suffix y x ⟹ suffix z y ⟹ suffix z x"
  apply (simp add: suffix_def)
  apply auto
  apply (rule_tac x = "s1 @@ s1a" in exI)
  apply auto
  apply (simp add: Conc_assoc)
  done

lemma transT: "s ⊨ □F ❙⟶ □□F"
  apply (simp add: satisfies_def IMPLIES_def Box_def tsuffix_def)
  apply auto
  apply (drule suffix_trans)
  apply assumption
  apply (erule_tac x = "s2a" in allE)
  apply auto
  done

lemma normalT: "s ⊨ □(F ❙⟶ G) ❙⟶ □F ❙⟶ □G"
  by (simp add: satisfies_def IMPLIES_def Box_def)


subsection ‹TLA Rules by Lamport›

lemma STL1a: "❙⊫ P ⟹ ❙⊫ (□P)"
  by (simp add: validT_def satisfies_def Box_def tsuffix_def)

lemma STL1b: "⊫ P ⟹ ❙⊫ (Init P)"
  by (simp add: valid_def validT_def satisfies_def Init_def)

lemma STL1: "⊫ P ⟹ ❙⊫ (□(Init P))"
  apply (rule STL1a)
  apply (erule STL1b)
  done

(*Note that unlift and HD is not at all used!*)
lemma STL4: "⊫ (P ❙⟶ Q) ⟹ ❙⊫ (□(Init P) ❙⟶ □(Init Q))"
  by (simp add: valid_def validT_def satisfies_def IMPLIES_def Box_def Init_def)


subsection ‹LTL Axioms by Manna/Pnueli›

lemma tsuffix_TL [rule_format]: "s ≠ UU ∧ s ≠ nil ⟶ tsuffix s2 (TL ⋅ s) ⟶ tsuffix s2 s"
  apply (unfold tsuffix_def suffix_def)
  apply auto
  apply (Seq_case_simp s)
  apply (rule_tac x = "a ↝ s1" in exI)
  apply auto
  done

lemmas tsuffix_TL2 = conjI [THEN tsuffix_TL]

lemma LTL1: "s ≠ UU ∧ s ≠ nil ⟶ (s ⊨ □F ❙⟶ (F ❙∧ (○(□F))))"
  supply if_split [split del] 
  apply (unfold Next_def satisfies_def NOT_def IMPLIES_def AND_def Box_def)
  apply auto
  text ‹‹□F ❙⟶ F››
  apply (erule_tac x = "s" in allE)
  apply (simp add: tsuffix_def suffix_refl)
  text ‹‹□F ❙⟶ ○□F››
  apply (simp split: if_split)
  apply auto
  apply (drule tsuffix_TL2)
  apply assumption+
  apply auto
  done

lemma LTL2a: "s ⊨ ❙¬ (○F) ❙⟶ (○(❙¬ F))"
  by (simp add: Next_def satisfies_def NOT_def IMPLIES_def)

lemma LTL2b: "s ⊨ (○(❙¬ F)) ❙⟶ (❙¬ (○F))"
  by (simp add: Next_def satisfies_def NOT_def IMPLIES_def)

lemma LTL3: "ex ⊨ (○(F ❙⟶ G)) ❙⟶ (○F) ❙⟶ (○G)"
  by (simp add: Next_def satisfies_def NOT_def IMPLIES_def)

lemma ModusPonens: "❙⊫ (P ❙⟶ Q) ⟹ ❙⊫ P ⟹ ❙⊫ Q"
  by (simp add: validT_def satisfies_def IMPLIES_def)

end