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