Quellcode-Bibliothek 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 "(\<TTurnstile> 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 = (\<not> (◻(\<not> P)))"

definition Leadsto :: "'a temporal ==> 'a temporal ==> 'a temporal"  (infixr ‹↝› 22)
  where "(P ↝ Q) = (◻(P \<longrightarrow> (♢Q)))"


lemma simple: "◻♢(\<not> P) = (\<not> ♢◻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 \<longrightarrow> 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 \<longrightarrow> F"
    by (simp add: satisfies_def IMPLIES_def Box_def)
qed

lemma transT: "s ⊨ ◻F \<longrightarrow> ◻◻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 \<longrightarrow> G) \<longrightarrow> ◻F \<longrightarrow> ◻G"
  by (simp add: satisfies_def IMPLIES_def Box_def)


subsection ‹TLA Rules by Lamport›

lemma STL1a: "\<TTurnstile> P ==> \<TTurnstile> (◻P)"
  by (simp add: validT_def satisfies_def Box_def tsuffix_def)

lemma STL1b: "⊨!!! P ==> \<TTurnstile> (Init P)"
  by (simp add: valid_def validT_def satisfies_def Init_def)

lemma STL1: assumes "⊨!!! P" shows "\<TTurnstile> (◻(Init P))"
proof -
  from assms have "\<TTurnstile> (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 \<longrightarrow> Q) ==> \<TTurnstile> (◻(Init P) \<longrightarrow> ◻(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 \<longrightarrow> (F \<and> (◯(◻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 ⊨ \<not> (◯F) \<longrightarrow> (◯(\<not> F))"
  by (simp add: Next_def satisfies_def NOT_def IMPLIES_def)

lemma LTL2b: "s ⊨ (◯(\<not> F)) \<longrightarrow> (\<not> (◯F))"
  by (simp add: Next_def satisfies_def NOT_def IMPLIES_def)

lemma LTL3: "ex ⊨ (◯(F \<longrightarrow> G)) \<longrightarrow> (◯F) \<longrightarrow> (◯G)"
  by (simp add: Next_def satisfies_def NOT_def IMPLIES_def)

lemma ModusPonens: "\<TTurnstile> (P \<longrightarrow> Q) ==> \<TTurnstile> P ==> \<TTurnstile> Q"
  by (simp add: validT_def satisfies_def IMPLIES_def)

end