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"  (‹(‹indent=1 notation=‹prefix Next››○_)› [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"  (‹(‹indent=1 notation=‹prefix Box››□_)› [80] 80)
  where "(□P) s ⟷ (∀s2. tsuffix s2 s ⟶ P s2)"

definition Diamond :: "'a temporal ⇒ 'a temporal"  (‹(‹indent=1 notation=‹prefix Diamond››◇_)› [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"
proof -
  have "Finite nil ∧ s = nil @@ s" by simp
  then show ?thesis unfolding suffix_def ..
qed

lemma suffix_trans:
  assumes "suffix y x"
    and "suffix z y"
  shows "suffix z x"
proof -
  from assms obtain s1 s2
    where "Finite s1 ∧ x = s1 @@ y"
      and "Finite s2 ∧ y = s2 @@ z"
    unfolding suffix_def by iprover
  then have "Finite (s1 @@ s2) ∧ x = (s1 @@ s2) @@ z"
    by (simp add: Conc_assoc)
  then show ?thesis unfolding suffix_def ..
qed

lemma reflT: "s ≠ UU ∧ s ≠ nil ⟶ (s ⊨ □F ❙⟶ F)"
proof
  assume s: "s ≠ UU ∧ s ≠ nil"
  have "F s" if box_F: "∀s2. tsuffix s2 s ⟶ F s2"
  proof -
    from s and suffix_refl [of s] have "tsuffix s s"
      by (simp add: tsuffix_def)
    also from box_F have "?this ⟶ F s" ..
    finally show ?thesis .
  qed
  then show "s ⊨ □F ❙⟶ F"
    by (simp add: satisfies_def IMPLIES_def Box_def)
qed

lemma transT: "s ⊨ □F ❙⟶ □□F"
proof -
  have "F s2" if *: "tsuffix s1 s" "tsuffix s2 s1"
    and **: "∀s'. tsuffix s' s ⟶ F s'"
    for s1 s2
  proof -
    from * have "tsuffix s2 s"
      by (auto simp: tsuffix_def elim: suffix_trans)
    also from ** have "?this ⟶ F s2" ..
    finally show ?thesis .
  qed
  then show ?thesis
    by (simp add: satisfies_def IMPLIES_def Box_def)
qed

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: assumes "⊫ P" shows "❙⊫ (□(Init P))"
proof -
  from assms have "❙⊫ (Init P)" by (rule STL1b)
  then show ?thesis by (rule STL1a)
qed

(*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