11352
|
1 |
|
|
2 |
theory CTL = Main:
|
|
3 |
|
|
4 |
section {* CTL formulae *}
|
|
5 |
|
|
6 |
text {*
|
11355
|
7 |
\tweakskip We formalize basic concepts of Computational Tree Logic
|
|
8 |
(CTL) \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the
|
|
9 |
simply-typed set theory of HOL.
|
|
10 |
|
|
11 |
By using the common technique of ``shallow embedding'', a CTL
|
|
12 |
formula is identified with the corresponding set of states where it
|
|
13 |
holds. Consequently, CTL operations such as negation, conjunction,
|
|
14 |
disjunction simply become complement, intersection, union of sets.
|
|
15 |
We only require a separate operation for implication, as point-wise
|
|
16 |
inclusion is usually not encountered in plain set-theory.
|
11352
|
17 |
*}
|
|
18 |
|
|
19 |
lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2
|
|
20 |
|
|
21 |
types 'a ctl = "'a set"
|
|
22 |
constdefs
|
|
23 |
imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl" (infixr "\<rightarrow>" 75)
|
|
24 |
"p \<rightarrow> q \<equiv> - p \<union> q"
|
|
25 |
|
|
26 |
lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" by (unfold imp_def) auto
|
|
27 |
lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" by (unfold imp_def) rule
|
|
28 |
|
|
29 |
|
|
30 |
text {*
|
11355
|
31 |
\smallskip The CTL path operators are more interesting; they are
|
|
32 |
based on an arbitrary, but fixed model @{text \<M>}, which is simply
|
|
33 |
a transition relation over states @{typ "'a"}.
|
11352
|
34 |
*}
|
|
35 |
|
|
36 |
consts model :: "('a \<times> 'a) set" ("\<M>")
|
|
37 |
|
|
38 |
text {*
|
11355
|
39 |
The operators @{text \<EX>}, @{text \<EF>}, @{text \<EG>} are taken
|
|
40 |
as primitives, while @{text \<AX>}, @{text \<AF>}, @{text \<AG>} are
|
11352
|
41 |
defined as derived ones. The formula @{text "\<EX> p"} holds in a
|
|
42 |
state @{term s}, iff there is a successor state @{term s'} (with
|
|
43 |
respect to the model @{term \<M>}), such that @{term p} holds in
|
|
44 |
@{term s'}. The formula @{text "\<EF> p"} holds in a state @{term
|
|
45 |
s}, iff there is a path in @{text \<M>}, starting from @{term s},
|
|
46 |
such that there exists a state @{term s'} on the path, such that
|
|
47 |
@{term p} holds in @{term s'}. The formula @{text "\<EG> p"} holds
|
|
48 |
in a state @{term s}, iff there is a path, starting from @{term s},
|
|
49 |
such that for all states @{term s'} on the path, @{term p} holds in
|
|
50 |
@{term s'}. It is easy to see that @{text "\<EF> p"} and @{text
|
|
51 |
"\<EG> p"} may be expressed using least and greatest fixed points
|
|
52 |
\cite{McMillan-PhDThesis}.
|
|
53 |
*}
|
|
54 |
|
|
55 |
constdefs
|
|
56 |
EX :: "'a ctl \<Rightarrow> 'a ctl" ("\<EX> _" [80] 90) "\<EX> p \<equiv> {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
|
|
57 |
EF :: "'a ctl \<Rightarrow> 'a ctl" ("\<EF> _" [80] 90) "\<EF> p \<equiv> lfp (\<lambda>s. p \<union> \<EX> s)"
|
|
58 |
EG :: "'a ctl \<Rightarrow> 'a ctl" ("\<EG> _" [80] 90) "\<EG> p \<equiv> gfp (\<lambda>s. p \<inter> \<EX> s)"
|
|
59 |
|
|
60 |
text {*
|
11355
|
61 |
@{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined
|
|
62 |
dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text
|
|
63 |
"\<EG>"}.
|
11352
|
64 |
*}
|
|
65 |
|
|
66 |
constdefs
|
|
67 |
AX :: "'a ctl \<Rightarrow> 'a ctl" ("\<AX> _" [80] 90) "\<AX> p \<equiv> - \<EX> - p"
|
|
68 |
AF :: "'a ctl \<Rightarrow> 'a ctl" ("\<AF> _" [80] 90) "\<AF> p \<equiv> - \<EG> - p"
|
|
69 |
AG :: "'a ctl \<Rightarrow> 'a ctl" ("\<AG> _" [80] 90) "\<AG> p \<equiv> - \<EF> - p"
|
|
70 |
|
|
71 |
lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def
|
|
72 |
|
|
73 |
|
|
74 |
section {* Basic fixed point properties *}
|
|
75 |
|
|
76 |
text {*
|
11355
|
77 |
\tweakskip First of all, we use the de-Morgan property of fixed
|
|
78 |
points
|
11352
|
79 |
*}
|
|
80 |
|
|
81 |
lemma lfp_gfp: "lfp f = - gfp (\<lambda>s . - (f (- s)))"
|
|
82 |
proof
|
|
83 |
show "lfp f \<subseteq> - gfp (\<lambda>s. - f (- s))"
|
|
84 |
proof
|
|
85 |
fix x assume l: "x \<in> lfp f"
|
|
86 |
show "x \<in> - gfp (\<lambda>s. - f (- s))"
|
|
87 |
proof
|
|
88 |
assume "x \<in> gfp (\<lambda>s. - f (- s))"
|
|
89 |
then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)" by (unfold gfp_def) auto
|
|
90 |
then have "f (- u) \<subseteq> - u" by auto
|
|
91 |
then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
|
|
92 |
from l and this have "x \<notin> u" by auto
|
|
93 |
then show False by contradiction
|
|
94 |
qed
|
|
95 |
qed
|
|
96 |
show "- gfp (\<lambda>s. - f (- s)) \<subseteq> lfp f"
|
|
97 |
proof (rule lfp_greatest)
|
|
98 |
fix u assume "f u \<subseteq> u"
|
|
99 |
then have "- u \<subseteq> - f u" by auto
|
|
100 |
then have "- u \<subseteq> - f (- (- u))" by simp
|
|
101 |
then have "- u \<subseteq> gfp (\<lambda>s. - f (- s))" by (rule gfp_upperbound)
|
|
102 |
then show "- gfp (\<lambda>s. - f (- s)) \<subseteq> u" by auto
|
|
103 |
qed
|
|
104 |
qed
|
|
105 |
|
|
106 |
lemma lfp_gfp': "- lfp f = gfp (\<lambda>s. - (f (- s)))"
|
|
107 |
by (simp add: lfp_gfp)
|
|
108 |
|
|
109 |
lemma gfp_lfp': "- gfp f = lfp (\<lambda>s. - (f (- s)))"
|
|
110 |
by (simp add: lfp_gfp)
|
|
111 |
|
|
112 |
text {*
|
|
113 |
in order to give dual fixed point representations of @{term "AF p"}
|
|
114 |
and @{term "AG p"}:
|
|
115 |
*}
|
|
116 |
|
|
117 |
lemma AF_lfp: "\<AF> p = lfp (\<lambda>s. p \<union> \<AX> s)" by (simp add: lfp_gfp)
|
|
118 |
lemma AG_gfp: "\<AG> p = gfp (\<lambda>s. p \<inter> \<AX> s)" by (simp add: lfp_gfp)
|
|
119 |
|
|
120 |
lemma EF_fp: "\<EF> p = p \<union> \<EX> \<EF> p"
|
|
121 |
proof -
|
|
122 |
have "mono (\<lambda>s. p \<union> \<EX> s)" by rule (auto simp add: EX_def)
|
|
123 |
then show ?thesis by (simp only: EF_def) (rule lfp_unfold)
|
|
124 |
qed
|
|
125 |
|
|
126 |
lemma AF_fp: "\<AF> p = p \<union> \<AX> \<AF> p"
|
|
127 |
proof -
|
|
128 |
have "mono (\<lambda>s. p \<union> \<AX> s)" by rule (auto simp add: AX_def EX_def)
|
|
129 |
then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)
|
|
130 |
qed
|
|
131 |
|
|
132 |
lemma EG_fp: "\<EG> p = p \<inter> \<EX> \<EG> p"
|
|
133 |
proof -
|
|
134 |
have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule (auto simp add: EX_def)
|
|
135 |
then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
|
|
136 |
qed
|
|
137 |
|
|
138 |
text {*
|
|
139 |
From the greatest fixed point definition of @{term "\<AG> p"}, we
|
|
140 |
derive as a consequence of the Knaster-Tarski theorem on the one
|
|
141 |
hand that @{term "\<AG> p"} is a fixed point of the monotonic
|
|
142 |
function @{term "\<lambda>s. p \<inter> \<AX> s"}.
|
|
143 |
*}
|
|
144 |
|
|
145 |
lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
|
|
146 |
proof -
|
11355
|
147 |
have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule (auto simp add: AX_def EX_def)
|
|
148 |
then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
|
11352
|
149 |
qed
|
|
150 |
|
|
151 |
text {*
|
|
152 |
This fact may be split up into two inequalities (merely using
|
|
153 |
transitivity of @{text "\<subseteq>" }, which is an instance of the overloaded
|
|
154 |
@{text "\<le>"} in Isabelle/HOL).
|
|
155 |
*}
|
|
156 |
|
|
157 |
lemma AG_fp_1: "\<AG> p \<subseteq> p"
|
|
158 |
proof -
|
|
159 |
note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> p" by auto
|
|
160 |
finally show ?thesis .
|
|
161 |
qed
|
|
162 |
|
|
163 |
text {**}
|
|
164 |
|
|
165 |
lemma AG_fp_2: "\<AG> p \<subseteq> \<AX> \<AG> p"
|
|
166 |
proof -
|
|
167 |
note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> \<AX> \<AG> p" by auto
|
|
168 |
finally show ?thesis .
|
|
169 |
qed
|
|
170 |
|
|
171 |
text {*
|
|
172 |
On the other hand, we have from the Knaster-Tarski fixed point
|
|
173 |
theorem that any other post-fixed point of @{term "\<lambda>s. p \<inter> AX s"} is
|
|
174 |
smaller than @{term "AG p"}. A post-fixed point is a set of states
|
|
175 |
@{term q} such that @{term "q \<subseteq> p \<inter> AX q"}. This leads to the
|
|
176 |
following co-induction principle for @{term "AG p"}.
|
|
177 |
*}
|
|
178 |
|
|
179 |
lemma AG_I: "q \<subseteq> p \<inter> \<AX> q \<Longrightarrow> q \<subseteq> \<AG> p"
|
|
180 |
by (simp only: AG_gfp) (rule gfp_upperbound)
|
|
181 |
|
|
182 |
|
|
183 |
section {* The tree induction principle \label{sec:calc-ctl-tree-induct} *}
|
|
184 |
|
|
185 |
text {*
|
|
186 |
\tweakskip With the most basic facts available, we are now able to
|
|
187 |
establish a few more interesting results, leading to the \emph{tree
|
|
188 |
induction} principle for @{text AG} (see below). We will use some
|
|
189 |
elementary monotonicity and distributivity rules.
|
|
190 |
*}
|
|
191 |
|
|
192 |
lemma AX_int: "\<AX> (p \<inter> q) = \<AX> p \<inter> \<AX> q" by auto
|
|
193 |
lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<AX> p \<subseteq> \<AX> q" by auto
|
11355
|
194 |
lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<AG> p \<subseteq> \<AG> q"
|
|
195 |
by (simp only: AG_gfp, rule gfp_mono) auto
|
11352
|
196 |
|
|
197 |
text {*
|
|
198 |
The formula @{term "AG p"} implies @{term "AX p"} (we use
|
|
199 |
substitution of @{text "\<subseteq>"} with monotonicity).
|
|
200 |
*}
|
|
201 |
|
|
202 |
lemma AG_AX: "\<AG> p \<subseteq> \<AX> p"
|
|
203 |
proof -
|
|
204 |
have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
|
|
205 |
also have "\<AG> p \<subseteq> p" by (rule AG_fp_1) moreover note AX_mono
|
|
206 |
finally show ?thesis .
|
|
207 |
qed
|
|
208 |
|
|
209 |
text {*
|
|
210 |
Furthermore we show idempotency of the @{text "\<AG>"} operator.
|
|
211 |
The proof is a good example of how accumulated facts may get
|
|
212 |
used to feed a single rule step.
|
|
213 |
*}
|
|
214 |
|
|
215 |
lemma AG_AG: "\<AG> \<AG> p = \<AG> p"
|
|
216 |
proof
|
|
217 |
show "\<AG> \<AG> p \<subseteq> \<AG> p" by (rule AG_fp_1)
|
|
218 |
next
|
|
219 |
show "\<AG> p \<subseteq> \<AG> \<AG> p"
|
|
220 |
proof (rule AG_I)
|
|
221 |
have "\<AG> p \<subseteq> \<AG> p" ..
|
|
222 |
moreover have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
|
|
223 |
ultimately show "\<AG> p \<subseteq> \<AG> p \<inter> \<AX> \<AG> p" ..
|
|
224 |
qed
|
|
225 |
qed
|
|
226 |
|
|
227 |
text {*
|
11355
|
228 |
\smallskip We now give an alternative characterization of the @{text
|
|
229 |
"\<AG>"} operator, which describes the @{text "\<AG>"} operator in
|
|
230 |
an ``operational'' way by tree induction: In a state holds @{term
|
|
231 |
"AG p"} iff in that state holds @{term p}, and in all reachable
|
|
232 |
states @{term s} follows from the fact that @{term p} holds in
|
|
233 |
@{term s}, that @{term p} also holds in all successor states of
|
|
234 |
@{term s}. We use the co-induction principle @{thm [source] AG_I}
|
|
235 |
to establish this in a purely algebraic manner.
|
11352
|
236 |
*}
|
|
237 |
|
|
238 |
theorem AG_induct: "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p"
|
|
239 |
proof
|
|
240 |
show "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> p" (is "?lhs \<subseteq> _")
|
|
241 |
proof (rule AG_I)
|
|
242 |
show "?lhs \<subseteq> p \<inter> \<AX> ?lhs"
|
|
243 |
proof
|
|
244 |
show "?lhs \<subseteq> p" ..
|
|
245 |
show "?lhs \<subseteq> \<AX> ?lhs"
|
|
246 |
proof -
|
|
247 |
{
|
|
248 |
have "\<AG> (p \<rightarrow> \<AX> p) \<subseteq> p \<rightarrow> \<AX> p" by (rule AG_fp_1)
|
|
249 |
also have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..
|
|
250 |
finally have "?lhs \<subseteq> \<AX> p" by auto
|
|
251 |
}
|
|
252 |
moreover
|
|
253 |
{
|
|
254 |
have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> (p \<rightarrow> \<AX> p)" ..
|
|
255 |
also have "\<dots> \<subseteq> \<AX> \<dots>" by (rule AG_fp_2)
|
|
256 |
finally have "?lhs \<subseteq> \<AX> \<AG> (p \<rightarrow> \<AX> p)" .
|
|
257 |
}
|
|
258 |
ultimately have "?lhs \<subseteq> \<AX> p \<inter> \<AX> \<AG> (p \<rightarrow> \<AX> p)" ..
|
|
259 |
also have "\<dots> = \<AX> ?lhs" by (simp only: AX_int)
|
|
260 |
finally show ?thesis .
|
|
261 |
qed
|
|
262 |
qed
|
|
263 |
qed
|
|
264 |
next
|
|
265 |
show "\<AG> p \<subseteq> p \<inter> \<AG> (p \<rightarrow> \<AX> p)"
|
|
266 |
proof
|
|
267 |
show "\<AG> p \<subseteq> p" by (rule AG_fp_1)
|
|
268 |
show "\<AG> p \<subseteq> \<AG> (p \<rightarrow> \<AX> p)"
|
|
269 |
proof -
|
|
270 |
have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
|
|
271 |
also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX) moreover note AG_mono
|
|
272 |
also have "\<AX> p \<subseteq> (p \<rightarrow> \<AX> p)" .. moreover note AG_mono
|
|
273 |
finally show ?thesis .
|
|
274 |
qed
|
|
275 |
qed
|
|
276 |
qed
|
|
277 |
|
|
278 |
|
|
279 |
section {* An application of tree induction \label{sec:calc-ctl-commute} *}
|
|
280 |
|
|
281 |
text {*
|
|
282 |
\tweakskip Further interesting properties of CTL expressions may be
|
|
283 |
demonstrated with the help of tree induction; here we show that
|
|
284 |
@{text \<AX>} and @{text \<AG>} commute.
|
|
285 |
*}
|
|
286 |
|
|
287 |
theorem AG_AX_commute: "\<AG> \<AX> p = \<AX> \<AG> p"
|
|
288 |
proof -
|
|
289 |
have "\<AG> \<AX> p = \<AX> p \<inter> \<AX> \<AG> \<AX> p" by (rule AG_fp)
|
|
290 |
also have "\<dots> = \<AX> (p \<inter> \<AG> \<AX> p)" by (simp only: AX_int)
|
|
291 |
also have "p \<inter> \<AG> \<AX> p = \<AG> p" (is "?lhs = _")
|
|
292 |
proof
|
|
293 |
have "\<AX> p \<subseteq> p \<rightarrow> \<AX> p" ..
|
|
294 |
also have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p" by (rule AG_induct)
|
11758
|
295 |
also note Int_mono AG_mono
|
|
296 |
ultimately show "?lhs \<subseteq> \<AG> p" by fast
|
11352
|
297 |
next
|
|
298 |
have "\<AG> p \<subseteq> p" by (rule AG_fp_1)
|
|
299 |
moreover
|
|
300 |
{
|
|
301 |
have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
|
|
302 |
also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX)
|
|
303 |
also note AG_mono
|
|
304 |
ultimately have "\<AG> p \<subseteq> \<AG> \<AX> p" .
|
|
305 |
}
|
|
306 |
ultimately show "\<AG> p \<subseteq> ?lhs" ..
|
|
307 |
qed
|
|
308 |
finally show ?thesis .
|
|
309 |
qed
|
|
310 |
|
|
311 |
end
|