# Theory TL

theory TL
imports Pred Sequence
```(*  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 (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)
done

lemma suffix_trans: "suffix y x ⟹ suffix z y ⟹ suffix z x"
apply auto
apply (rule_tac x = "s1 @@ s1a" in exI)
apply auto
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)
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
```