Quelle  TL.thy

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