1(*  Title:      HOL/HOLCF/IOA/TL.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>A General Temporal Logic\<close>
6
7theory TL
8imports Pred Sequence
9begin
10
11default_sort type
12
13type_synonym 'a temporal = "'a Seq predicate"
14
15definition validT :: "'a Seq predicate \<Rightarrow> bool"    ("\<^bold>\<TTurnstile> _" [9] 8)
16  where "(\<^bold>\<TTurnstile> P) \<longleftrightarrow> (\<forall>s. s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> (s \<Turnstile> P))"
17
18definition unlift :: "'a lift \<Rightarrow> 'a"
19  where "unlift x = (case x of Def y \<Rightarrow> y)"
20
21definition Init :: "'a predicate \<Rightarrow> 'a temporal"  ("\<langle>_\<rangle>" [0] 1000)
22  where "Init P s = P (unlift (HD \<cdot> s))"
23    \<comment> \<open>this means that for \<open>nil\<close> and \<open>UU\<close> the effect is unpredictable\<close>
24
25definition Next :: "'a temporal \<Rightarrow> 'a temporal"  ("\<circle>(_)" [80] 80)
26  where "(\<circle>P) s \<longleftrightarrow> (if TL \<cdot> s = UU \<or> TL \<cdot> s = nil then P s else P (TL \<cdot> s))"
27
28definition suffix :: "'a Seq \<Rightarrow> 'a Seq \<Rightarrow> bool"
29  where "suffix s2 s \<longleftrightarrow> (\<exists>s1. Finite s1 \<and> s = s1 @@ s2)"
30
31definition tsuffix :: "'a Seq \<Rightarrow> 'a Seq \<Rightarrow> bool"
32  where "tsuffix s2 s \<longleftrightarrow> s2 \<noteq> nil \<and> s2 \<noteq> UU \<and> suffix s2 s"
33
34definition Box :: "'a temporal \<Rightarrow> 'a temporal"  ("\<box>(_)" [80] 80)
35  where "(\<box>P) s \<longleftrightarrow> (\<forall>s2. tsuffix s2 s \<longrightarrow> P s2)"
36
37definition Diamond :: "'a temporal \<Rightarrow> 'a temporal"  ("\<diamond>(_)" [80] 80)
38  where "\<diamond>P = (\<^bold>\<not> (\<box>(\<^bold>\<not> P)))"
39
40definition Leadsto :: "'a temporal \<Rightarrow> 'a temporal \<Rightarrow> 'a temporal"  (infixr "\<leadsto>" 22)
41  where "(P \<leadsto> Q) = (\<box>(P \<^bold>\<longrightarrow> (\<diamond>Q)))"
42
43
44lemma simple: "\<box>\<diamond>(\<^bold>\<not> P) = (\<^bold>\<not> \<diamond>\<box>P)"
45  by (auto simp add: Diamond_def NOT_def Box_def)
46
47lemma Boxnil: "nil \<Turnstile> \<box>P"
48  by (simp add: satisfies_def Box_def tsuffix_def suffix_def nil_is_Conc)
49
50lemma Diamondnil: "\<not> (nil \<Turnstile> \<diamond>P)"
51  using Boxnil by (simp add: Diamond_def satisfies_def NOT_def)
52
53lemma Diamond_def2: "(\<diamond>F) s \<longleftrightarrow> (\<exists>s2. tsuffix s2 s \<and> F s2)"
54  by (simp add: Diamond_def NOT_def Box_def)
55
56
57subsection \<open>TLA Axiomatization by Merz\<close>
58
59lemma suffix_refl: "suffix s s"
60  apply (simp add: suffix_def)
61  apply (rule_tac x = "nil" in exI)
62  apply auto
63  done
64
65lemma reflT: "s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> F)"
66  apply (simp add: satisfies_def IMPLIES_def Box_def)
67  apply (rule impI)+
68  apply (erule_tac x = "s" in allE)
69  apply (simp add: tsuffix_def suffix_refl)
70  done
71
72lemma suffix_trans: "suffix y x \<Longrightarrow> suffix z y \<Longrightarrow> suffix z x"
73  apply (simp add: suffix_def)
74  apply auto
75  apply (rule_tac x = "s1 @@ s1a" in exI)
76  apply auto
77  apply (simp add: Conc_assoc)
78  done
79
80lemma transT: "s \<Turnstile> \<box>F \<^bold>\<longrightarrow> \<box>\<box>F"
81  apply (simp add: satisfies_def IMPLIES_def Box_def tsuffix_def)
82  apply auto
83  apply (drule suffix_trans)
84  apply assumption
85  apply (erule_tac x = "s2a" in allE)
86  apply auto
87  done
88
89lemma normalT: "s \<Turnstile> \<box>(F \<^bold>\<longrightarrow> G) \<^bold>\<longrightarrow> \<box>F \<^bold>\<longrightarrow> \<box>G"
90  by (simp add: satisfies_def IMPLIES_def Box_def)
91
92
93subsection \<open>TLA Rules by Lamport\<close>
94
95lemma STL1a: "\<^bold>\<TTurnstile> P \<Longrightarrow> \<^bold>\<TTurnstile> (\<box>P)"
96  by (simp add: validT_def satisfies_def Box_def tsuffix_def)
97
98lemma STL1b: "\<TTurnstile> P \<Longrightarrow> \<^bold>\<TTurnstile> (Init P)"
99  by (simp add: valid_def validT_def satisfies_def Init_def)
100
101lemma STL1: "\<TTurnstile> P \<Longrightarrow> \<^bold>\<TTurnstile> (\<box>(Init P))"
102  apply (rule STL1a)
103  apply (erule STL1b)
104  done
105
106(*Note that unlift and HD is not at all used!*)
107lemma STL4: "\<TTurnstile> (P \<^bold>\<longrightarrow> Q) \<Longrightarrow> \<^bold>\<TTurnstile> (\<box>(Init P) \<^bold>\<longrightarrow> \<box>(Init Q))"
108  by (simp add: valid_def validT_def satisfies_def IMPLIES_def Box_def Init_def)
109
110
111subsection \<open>LTL Axioms by Manna/Pnueli\<close>
112
113lemma tsuffix_TL [rule_format]: "s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> tsuffix s2 (TL \<cdot> s) \<longrightarrow> tsuffix s2 s"
114  apply (unfold tsuffix_def suffix_def)
115  apply auto
116  apply (Seq_case_simp s)
117  apply (rule_tac x = "a \<leadsto> s1" in exI)
118  apply auto
119  done
120
121lemmas tsuffix_TL2 = conjI [THEN tsuffix_TL]
122
123lemma LTL1: "s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> (F \<^bold>\<and> (\<circle>(\<box>F))))"
124  supply if_split [split del] 
125  apply (unfold Next_def satisfies_def NOT_def IMPLIES_def AND_def Box_def)
126  apply auto
127  text \<open>\<open>\<box>F \<^bold>\<longrightarrow> F\<close>\<close>
128  apply (erule_tac x = "s" in allE)
129  apply (simp add: tsuffix_def suffix_refl)
130  text \<open>\<open>\<box>F \<^bold>\<longrightarrow> \<circle>\<box>F\<close>\<close>
131  apply (simp split: if_split)
132  apply auto
133  apply (drule tsuffix_TL2)
134  apply assumption+
135  apply auto
136  done
137
138lemma LTL2a: "s \<Turnstile> \<^bold>\<not> (\<circle>F) \<^bold>\<longrightarrow> (\<circle>(\<^bold>\<not> F))"
139  by (simp add: Next_def satisfies_def NOT_def IMPLIES_def)
140
141lemma LTL2b: "s \<Turnstile> (\<circle>(\<^bold>\<not> F)) \<^bold>\<longrightarrow> (\<^bold>\<not> (\<circle>F))"
142  by (simp add: Next_def satisfies_def NOT_def IMPLIES_def)
143
144lemma LTL3: "ex \<Turnstile> (\<circle>(F \<^bold>\<longrightarrow> G)) \<^bold>\<longrightarrow> (\<circle>F) \<^bold>\<longrightarrow> (\<circle>G)"
145  by (simp add: Next_def satisfies_def NOT_def IMPLIES_def)
146
147lemma ModusPonens: "\<^bold>\<TTurnstile> (P \<^bold>\<longrightarrow> Q) \<Longrightarrow> \<^bold>\<TTurnstile> P \<Longrightarrow> \<^bold>\<TTurnstile> Q"
148  by (simp add: validT_def satisfies_def IMPLIES_def)
149
150end
151