author | wenzelm |
Wed, 25 Mar 2015 11:39:52 +0100 | |
changeset 59809 | 87641097d0f3 |
parent 58860 | fee7cfa69c50 |
child 67406 | 23307fd33906 |
permissions | -rw-r--r-- |
17914 | 1 |
(*<*)theory CTL imports Base begin(*>*) |
9958 | 2 |
|
58860 | 3 |
subsection{*Computation Tree Logic --- CTL*} |
9958 | 4 |
|
10212 | 5 |
text{*\label{sec:CTL} |
11494 | 6 |
\index{CTL|(}% |
10867 | 7 |
The semantics of PDL only needs reflexive transitive closure. |
8 |
Let us be adventurous and introduce a more expressive temporal operator. |
|
9 |
We extend the datatype |
|
10149 | 10 |
@{text formula} by a new constructor |
58860 | 11 |
*} |
10149 | 12 |
(*<*) |
18724 | 13 |
datatype formula = Atom "atom" |
10149 | 14 |
| Neg formula |
15 |
| And formula formula |
|
16 |
| AX formula |
|
17 |
| EF formula(*>*) |
|
58860 | 18 |
| AF formula |
9958 | 19 |
|
10149 | 20 |
text{*\noindent |
10983 | 21 |
which stands for ``\emph{A}lways in the \emph{F}uture'': |
22 |
on all infinite paths, at some point the formula holds. |
|
23 |
Formalizing the notion of an infinite path is easy |
|
10159 | 24 |
in HOL: it is simply a function from @{typ nat} to @{typ state}. |
58860 | 25 |
*} |
9958 | 26 |
|
27015 | 27 |
definition Paths :: "state \<Rightarrow> (nat \<Rightarrow> state)set" where |
28 |
"Paths s \<equiv> {p. s = p 0 \<and> (\<forall>i. (p i, p(i+1)) \<in> M)}" |
|
10149 | 29 |
|
30 |
text{*\noindent |
|
15904 | 31 |
This definition allows a succinct statement of the semantics of @{const AF}: |
10867 | 32 |
\footnote{Do not be misled: neither datatypes nor recursive functions can be |
10149 | 33 |
extended by new constructors or equations. This is just a trick of the |
12815 | 34 |
presentation (see \S\ref{sec:doc-prep-suppress}). In reality one has to define |
35 |
a new datatype and a new function.} |
|
58860 | 36 |
*} |
10149 | 37 |
(*<*) |
27015 | 38 |
primrec valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80) where |
39 |
"s \<Turnstile> Atom a = (a \<in> L s)" | |
|
40 |
"s \<Turnstile> Neg f = (~(s \<Turnstile> f))" | |
|
41 |
"s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)" | |
|
42 |
"s \<Turnstile> AX f = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)" | |
|
43 |
"s \<Turnstile> EF f = (\<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<Turnstile> f)" | |
|
10149 | 44 |
(*>*) |
27015 | 45 |
"s \<Turnstile> AF f = (\<forall>p \<in> Paths s. \<exists>i. p i \<Turnstile> f)" |
9958 | 46 |
|
10149 | 47 |
text{*\noindent |
15904 | 48 |
Model checking @{const AF} involves a function which |
10159 | 49 |
is just complicated enough to warrant a separate definition: |
58860 | 50 |
*} |
10149 | 51 |
|
27015 | 52 |
definition af :: "state set \<Rightarrow> state set \<Rightarrow> state set" where |
53 |
"af A T \<equiv> A \<union> {s. \<forall>t. (s, t) \<in> M \<longrightarrow> t \<in> T}" |
|
10149 | 54 |
|
55 |
text{*\noindent |
|
10867 | 56 |
Now we define @{term "mc(AF f)"} as the least set @{term T} that includes |
10149 | 57 |
@{term"mc f"} and all states all of whose direct successors are in @{term T}: |
58860 | 58 |
*} |
10149 | 59 |
(*<*) |
27015 | 60 |
primrec mc :: "formula \<Rightarrow> state set" where |
61 |
"mc(Atom a) = {s. a \<in> L s}" | |
|
62 |
"mc(Neg f) = -mc f" | |
|
63 |
"mc(And f g) = mc f \<inter> mc g" | |
|
64 |
"mc(AX f) = {s. \<forall>t. (s,t) \<in> M \<longrightarrow> t \<in> mc f}" | |
|
65 |
"mc(EF f) = lfp(\<lambda>T. mc f \<union> M\<inverse> `` T)"|(*>*) |
|
58860 | 66 |
"mc(AF f) = lfp(af(mc f))" |
10159 | 67 |
|
68 |
text{*\noindent |
|
15904 | 69 |
Because @{const af} is monotone in its second argument (and also its first, but |
10983 | 70 |
that is irrelevant), @{term"af A"} has a least fixed point: |
58860 | 71 |
*} |
10159 | 72 |
|
58860 | 73 |
lemma mono_af: "mono(af A)" |
74 |
apply(simp add: mono_def af_def) |
|
75 |
apply blast |
|
10159 | 76 |
done |
10149 | 77 |
(*<*) |
58860 | 78 |
lemma mono_ef: "mono(\<lambda>T. A \<union> M\<inverse> `` T)" |
79 |
apply(rule monoI) |
|
80 |
by(blast) |
|
9958 | 81 |
|
10149 | 82 |
lemma EF_lemma: |
58860 | 83 |
"lfp(\<lambda>T. A \<union> M\<inverse> `` T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}" |
84 |
apply(rule equalityI) |
|
85 |
apply(rule subsetI) |
|
86 |
apply(simp) |
|
87 |
apply(erule lfp_induct_set) |
|
88 |
apply(rule mono_ef) |
|
89 |
apply(simp) |
|
90 |
apply(blast intro: rtrancl_trans) |
|
91 |
apply(rule subsetI) |
|
92 |
apply(simp, clarify) |
|
93 |
apply(erule converse_rtrancl_induct) |
|
94 |
apply(subst lfp_unfold[OF mono_ef]) |
|
95 |
apply(blast) |
|
96 |
apply(subst lfp_unfold[OF mono_ef]) |
|
97 |
by(blast) |
|
10149 | 98 |
(*>*) |
10159 | 99 |
text{* |
10867 | 100 |
All we need to prove now is @{prop"mc(AF f) = {s. s \<Turnstile> AF f}"}, which states |
15904 | 101 |
that @{term mc} and @{text"\<Turnstile>"} agree for @{const AF}\@. |
10867 | 102 |
This time we prove the two inclusions separately, starting |
10159 | 103 |
with the easy one: |
58860 | 104 |
*} |
9958 | 105 |
|
27015 | 106 |
theorem AF_lemma1: "lfp(af A) \<subseteq> {s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A}" |
10159 | 107 |
|
108 |
txt{*\noindent |
|
15904 | 109 |
In contrast to the analogous proof for @{const EF}, and just |
11494 | 110 |
for a change, we do not use fixed point induction. Park-induction, |
111 |
named after David Park, is weaker but sufficient for this proof: |
|
10995 | 112 |
\begin{center} |
113 |
@{thm lfp_lowerbound[of _ "S",no_vars]} \hfill (@{thm[source]lfp_lowerbound}) |
|
114 |
\end{center} |
|
10225 | 115 |
The instance of the premise @{prop"f S \<subseteq> S"} is proved pointwise, |
15102 | 116 |
a decision that \isa{auto} takes for us: |
58860 | 117 |
*} |
118 |
apply(rule lfp_lowerbound) |
|
119 |
apply(auto simp add: af_def Paths_def) |
|
10363 | 120 |
|
10225 | 121 |
txt{* |
10363 | 122 |
@{subgoals[display,indent=0,margin=70,goals_limit=1]} |
15102 | 123 |
In this remaining case, we set @{term t} to @{term"p(1::nat)"}. |
15106 | 124 |
The rest is automatic, which is surprising because it involves |
125 |
finding the instantiation @{term"\<lambda>i::nat. p(i+1)"} |
|
126 |
for @{text"\<forall>p"}. |
|
58860 | 127 |
*} |
10159 | 128 |
|
58860 | 129 |
apply(erule_tac x = "p 1" in allE) |
130 |
apply(auto) |
|
131 |
done |
|
9958 | 132 |
|
10225 | 133 |
|
9958 | 134 |
text{* |
10867 | 135 |
The opposite inclusion is proved by contradiction: if some state |
10159 | 136 |
@{term s} is not in @{term"lfp(af A)"}, then we can construct an |
11494 | 137 |
infinite @{term A}-avoiding path starting from~@{term s}. The reason is |
15904 | 138 |
that by unfolding @{const lfp} we find that if @{term s} is not in |
9958 | 139 |
@{term"lfp(af A)"}, then @{term s} is not in @{term A} and there is a |
10983 | 140 |
direct successor of @{term s} that is again not in \mbox{@{term"lfp(af |
141 |
A)"}}. Iterating this argument yields the promised infinite |
|
9958 | 142 |
@{term A}-avoiding path. Let us formalize this sketch. |
143 |
||
10867 | 144 |
The one-step argument in the sketch above |
145 |
is proved by a variant of contraposition: |
|
58860 | 146 |
*} |
9958 | 147 |
|
148 |
lemma not_in_lfp_afD: |
|
58860 | 149 |
"s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t) \<in> M \<and> t \<notin> lfp(af A))" |
150 |
apply(erule contrapos_np) |
|
151 |
apply(subst lfp_unfold[OF mono_af]) |
|
152 |
apply(simp add: af_def) |
|
153 |
done |
|
9958 | 154 |
|
155 |
text{*\noindent |
|
10867 | 156 |
We assume the negation of the conclusion and prove @{term"s : lfp(af A)"}. |
15904 | 157 |
Unfolding @{const lfp} once and |
158 |
simplifying with the definition of @{const af} finishes the proof. |
|
9958 | 159 |
|
160 |
Now we iterate this process. The following construction of the desired |
|
10895 | 161 |
path is parameterized by a predicate @{term Q} that should hold along the path: |
58860 | 162 |
*} |
9958 | 163 |
|
27015 | 164 |
primrec path :: "state \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> (nat \<Rightarrow> state)" where |
165 |
"path s Q 0 = s" | |
|
166 |
"path s Q (Suc n) = (SOME t. (path s Q n,t) \<in> M \<and> Q t)" |
|
9958 | 167 |
|
168 |
text{*\noindent |
|
12699 | 169 |
Element @{term"n+1::nat"} on this path is some arbitrary successor |
10895 | 170 |
@{term t} of element @{term n} such that @{term"Q t"} holds. Remember that @{text"SOME t. R t"} |
10654 | 171 |
is some arbitrary but fixed @{term t} such that @{prop"R t"} holds (see \S\ref{sec:SOME}). Of |
10867 | 172 |
course, such a @{term t} need not exist, but that is of no |
15904 | 173 |
concern to us since we will only use @{const path} when a |
10159 | 174 |
suitable @{term t} does exist. |
9958 | 175 |
|
10895 | 176 |
Let us show that if each state @{term s} that satisfies @{term Q} |
177 |
has a successor that again satisfies @{term Q}, then there exists an infinite @{term Q}-path: |
|
58860 | 178 |
*} |
9958 | 179 |
|
10159 | 180 |
lemma infinity_lemma: |
10895 | 181 |
"\<lbrakk> Q s; \<forall>s. Q s \<longrightarrow> (\<exists> t. (s,t) \<in> M \<and> Q t) \<rbrakk> \<Longrightarrow> |
58860 | 182 |
\<exists>p\<in>Paths s. \<forall>i. Q(p i)" |
9958 | 183 |
|
184 |
txt{*\noindent |
|
10983 | 185 |
First we rephrase the conclusion slightly because we need to prove simultaneously |
186 |
both the path property and the fact that @{term Q} holds: |
|
58860 | 187 |
*} |
9958 | 188 |
|
12489 | 189 |
apply(subgoal_tac |
58860 | 190 |
"\<exists>p. s = p 0 \<and> (\<forall>i::nat. (p i, p(i+1)) \<in> M \<and> Q(p i))") |
9958 | 191 |
|
192 |
txt{*\noindent |
|
10159 | 193 |
From this proposition the original goal follows easily: |
58860 | 194 |
*} |
9958 | 195 |
|
58860 | 196 |
apply(simp add: Paths_def, blast) |
10159 | 197 |
|
198 |
txt{*\noindent |
|
10895 | 199 |
The new subgoal is proved by providing the witness @{term "path s Q"} for @{term p}: |
58860 | 200 |
*} |
10159 | 201 |
|
58860 | 202 |
apply(rule_tac x = "path s Q" in exI) |
203 |
apply(clarsimp) |
|
10159 | 204 |
|
205 |
txt{*\noindent |
|
11494 | 206 |
After simplification and clarification, the subgoal has the following form: |
10363 | 207 |
@{subgoals[display,indent=0,margin=70,goals_limit=1]} |
11494 | 208 |
It invites a proof by induction on @{term i}: |
58860 | 209 |
*} |
10159 | 210 |
|
58860 | 211 |
apply(induct_tac i) |
212 |
apply(simp) |
|
10159 | 213 |
|
214 |
txt{*\noindent |
|
10983 | 215 |
After simplification, the base case boils down to |
10363 | 216 |
@{subgoals[display,indent=0,margin=70,goals_limit=1]} |
10159 | 217 |
The conclusion looks exceedingly trivial: after all, @{term t} is chosen such that @{prop"(s,t):M"} |
218 |
holds. However, we first have to show that such a @{term t} actually exists! This reasoning |
|
219 |
is embodied in the theorem @{thm[source]someI2_ex}: |
|
220 |
@{thm[display,eta_contract=false]someI2_ex} |
|
221 |
When we apply this theorem as an introduction rule, @{text"?P x"} becomes |
|
10895 | 222 |
@{prop"(s, x) : M & Q x"} and @{text"?Q x"} becomes @{prop"(s,x) : M"} and we have to prove |
223 |
two subgoals: @{prop"EX a. (s, a) : M & Q a"}, which follows from the assumptions, and |
|
224 |
@{prop"(s, x) : M & Q x ==> (s,x) : M"}, which is trivial. Thus it is not surprising that |
|
10159 | 225 |
@{text fast} can prove the base case quickly: |
58860 | 226 |
*} |
10159 | 227 |
|
58860 | 228 |
apply(fast intro: someI2_ex) |
10159 | 229 |
|
230 |
txt{*\noindent |
|
11494 | 231 |
What is worth noting here is that we have used \methdx{fast} rather than |
10212 | 232 |
@{text blast}. The reason is that @{text blast} would fail because it cannot |
233 |
cope with @{thm[source]someI2_ex}: unifying its conclusion with the current |
|
11149 | 234 |
subgoal is non-trivial because of the nested schematic variables. For |
10212 | 235 |
efficiency reasons @{text blast} does not even attempt such unifications. |
236 |
Although @{text fast} can in principle cope with complicated unification |
|
237 |
problems, in practice the number of unifiers arising is often prohibitive and |
|
238 |
the offending rule may need to be applied explicitly rather than |
|
239 |
automatically. This is what happens in the step case. |
|
10159 | 240 |
|
10212 | 241 |
The induction step is similar, but more involved, because now we face nested |
16069 | 242 |
occurrences of @{text SOME}. As a result, @{text fast} is no longer able to |
10212 | 243 |
solve the subgoal and we apply @{thm[source]someI2_ex} by hand. We merely |
244 |
show the proof commands but do not describe the details: |
|
58860 | 245 |
*} |
10159 | 246 |
|
58860 | 247 |
apply(simp) |
248 |
apply(rule someI2_ex) |
|
249 |
apply(blast) |
|
250 |
apply(rule someI2_ex) |
|
251 |
apply(blast) |
|
252 |
apply(blast) |
|
253 |
done |
|
9958 | 254 |
|
10159 | 255 |
text{* |
15904 | 256 |
Function @{const path} has fulfilled its purpose now and can be forgotten. |
10867 | 257 |
It was merely defined to provide the witness in the proof of the |
10171 | 258 |
@{thm[source]infinity_lemma}. Aficionados of minimal proofs might like to know |
10159 | 259 |
that we could have given the witness without having to define a new function: |
260 |
the term |
|
55415 | 261 |
@{term[display]"rec_nat s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)"} |
10895 | 262 |
is extensionally equal to @{term"path s Q"}, |
55415 | 263 |
where @{term rec_nat} is the predefined primitive recursor on @{typ nat}. |
58860 | 264 |
*} |
10159 | 265 |
(*<*) |
13552 | 266 |
lemma |
10895 | 267 |
"\<lbrakk> Q s; \<forall> s. Q s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> Q t) \<rbrakk> \<Longrightarrow> |
58860 | 268 |
\<exists> p\<in>Paths s. \<forall> i. Q(p i)" |
9958 | 269 |
apply(subgoal_tac |
58860 | 270 |
"\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> Q(p i))") |
271 |
apply(simp add: Paths_def) |
|
272 |
apply(blast) |
|
273 |
apply(rule_tac x = "rec_nat s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)" in exI) |
|
274 |
apply(simp) |
|
275 |
apply(intro strip) |
|
276 |
apply(induct_tac i) |
|
277 |
apply(simp) |
|
278 |
apply(fast intro: someI2_ex) |
|
279 |
apply(simp) |
|
280 |
apply(rule someI2_ex) |
|
281 |
apply(blast) |
|
282 |
apply(rule someI2_ex) |
|
283 |
apply(blast) |
|
284 |
by(blast) |
|
10159 | 285 |
(*>*) |
9958 | 286 |
|
10159 | 287 |
text{* |
288 |
At last we can prove the opposite direction of @{thm[source]AF_lemma1}: |
|
58860 | 289 |
*} |
10159 | 290 |
|
58860 | 291 |
theorem AF_lemma2: "{s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A} \<subseteq> lfp(af A)" |
10159 | 292 |
|
293 |
txt{*\noindent |
|
10237 | 294 |
The proof is again pointwise and then by contraposition: |
58860 | 295 |
*} |
10159 | 296 |
|
58860 | 297 |
apply(rule subsetI) |
298 |
apply(erule contrapos_pp) |
|
299 |
apply simp |
|
10159 | 300 |
|
301 |
txt{* |
|
10363 | 302 |
@{subgoals[display,indent=0,goals_limit=1]} |
10159 | 303 |
Applying the @{thm[source]infinity_lemma} as a destruction rule leaves two subgoals, the second |
304 |
premise of @{thm[source]infinity_lemma} and the original subgoal: |
|
58860 | 305 |
*} |
10159 | 306 |
|
58860 | 307 |
apply(drule infinity_lemma) |
10159 | 308 |
|
309 |
txt{* |
|
10363 | 310 |
@{subgoals[display,indent=0,margin=65]} |
10159 | 311 |
Both are solved automatically: |
58860 | 312 |
*} |
9958 | 313 |
|
58860 | 314 |
apply(auto dest: not_in_lfp_afD) |
315 |
done |
|
9958 | 316 |
|
10159 | 317 |
text{* |
10867 | 318 |
If you find these proofs too complicated, we recommend that you read |
319 |
\S\ref{sec:CTL-revisited}, where we show how inductive definitions lead to |
|
10217 | 320 |
simpler arguments. |
321 |
||
322 |
The main theorem is proved as for PDL, except that we also derive the |
|
323 |
necessary equality @{text"lfp(af A) = ..."} by combining |
|
324 |
@{thm[source]AF_lemma1} and @{thm[source]AF_lemma2} on the spot: |
|
10159 | 325 |
*} |
326 |
||
58860 | 327 |
theorem "mc f = {s. s \<Turnstile> f}" |
328 |
apply(induct_tac f) |
|
329 |
apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2]) |
|
10159 | 330 |
done |
331 |
||
332 |
text{* |
|
10281 | 333 |
|
10867 | 334 |
The language defined above is not quite CTL\@. The latter also includes an |
10983 | 335 |
until-operator @{term"EU f g"} with semantics ``there \emph{E}xists a path |
11494 | 336 |
where @{term f} is true \emph{U}ntil @{term g} becomes true''. We need |
337 |
an auxiliary function: |
|
10281 | 338 |
*} |
339 |
||
340 |
primrec |
|
27027 | 341 |
until:: "state set \<Rightarrow> state set \<Rightarrow> state \<Rightarrow> state list \<Rightarrow> bool" where |
342 |
"until A B s [] = (s \<in> B)" | |
|
10281 | 343 |
"until A B s (t#p) = (s \<in> A \<and> (s,t) \<in> M \<and> until A B t p)" |
27027 | 344 |
(*<*)definition |
345 |
eusem :: "state set \<Rightarrow> state set \<Rightarrow> state set" where |
|
10281 | 346 |
"eusem A B \<equiv> {s. \<exists>p. until A B s p}"(*>*) |
347 |
||
348 |
text{*\noindent |
|
11494 | 349 |
Expressing the semantics of @{term EU} is now straightforward: |
10983 | 350 |
@{prop[display]"s \<Turnstile> EU f g = (\<exists>p. until {t. t \<Turnstile> f} {t. t \<Turnstile> g} s p)"} |
10281 | 351 |
Note that @{term EU} is not definable in terms of the other operators! |
352 |
||
353 |
Model checking @{term EU} is again a least fixed point construction: |
|
10839 | 354 |
@{text[display]"mc(EU f g) = lfp(\<lambda>T. mc g \<union> mc f \<inter> (M\<inverse> `` T))"} |
10281 | 355 |
|
10171 | 356 |
\begin{exercise} |
10281 | 357 |
Extend the datatype of formulae by the above until operator |
358 |
and prove the equivalence between semantics and model checking, i.e.\ that |
|
10186 | 359 |
@{prop[display]"mc(EU f g) = {s. s \<Turnstile> EU f g}"} |
360 |
%For readability you may want to annotate {term EU} with its customary syntax |
|
361 |
%{text[display]"| EU formula formula E[_ U _]"} |
|
362 |
%which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}. |
|
363 |
\end{exercise} |
|
58620 | 364 |
For more CTL exercises see, for example, Huth and Ryan @{cite "Huth-Ryan-book"}. |
10281 | 365 |
*} |
366 |
||
367 |
(*<*) |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
27027
diff
changeset
|
368 |
definition eufix :: "state set \<Rightarrow> state set \<Rightarrow> state set \<Rightarrow> state set" where |
10839 | 369 |
"eufix A B T \<equiv> B \<union> A \<inter> (M\<inverse> `` T)" |
10281 | 370 |
|
371 |
lemma "lfp(eufix A B) \<subseteq> eusem A B" |
|
372 |
apply(rule lfp_lowerbound) |
|
46932 | 373 |
apply(auto simp add: eusem_def eufix_def) |
374 |
apply(rule_tac x = "[]" in exI) |
|
10281 | 375 |
apply simp |
46932 | 376 |
apply(rule_tac x = "xa#xb" in exI) |
377 |
apply simp |
|
10281 | 378 |
done |
379 |
||
58860 | 380 |
lemma mono_eufix: "mono(eufix A B)" |
381 |
apply(simp add: mono_def eufix_def) |
|
382 |
apply blast |
|
10281 | 383 |
done |
384 |
||
58860 | 385 |
lemma "eusem A B \<subseteq> lfp(eufix A B)" |
386 |
apply(clarsimp simp add: eusem_def) |
|
387 |
apply(erule rev_mp) |
|
388 |
apply(rule_tac x = x in spec) |
|
389 |
apply(induct_tac p) |
|
11231 | 390 |
apply(subst lfp_unfold[OF mono_eufix]) |
58860 | 391 |
apply(simp add: eufix_def) |
392 |
apply(clarsimp) |
|
11231 | 393 |
apply(subst lfp_unfold[OF mono_eufix]) |
58860 | 394 |
apply(simp add: eufix_def) |
395 |
apply blast |
|
10281 | 396 |
done |
10178 | 397 |
|
10281 | 398 |
(* |
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
27027
diff
changeset
|
399 |
definition eusem :: "state set \<Rightarrow> state set \<Rightarrow> state set" where |
10281 | 400 |
"eusem A B \<equiv> {s. \<exists>p\<in>Paths s. \<exists>j. p j \<in> B \<and> (\<forall>i < j. p i \<in> A)}" |
401 |
||
48994 | 402 |
axiomatization where |
10281 | 403 |
M_total: "\<exists>t. (s,t) \<in> M" |
404 |
||
405 |
consts apath :: "state \<Rightarrow> (nat \<Rightarrow> state)" |
|
406 |
primrec |
|
407 |
"apath s 0 = s" |
|
408 |
"apath s (Suc i) = (SOME t. (apath s i,t) \<in> M)" |
|
409 |
||
410 |
lemma [iff]: "apath s \<in> Paths s"; |
|
12815 | 411 |
apply(simp add: Paths_def); |
10281 | 412 |
apply(blast intro: M_total[THEN someI_ex]) |
413 |
done |
|
414 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
27027
diff
changeset
|
415 |
definition pcons :: "state \<Rightarrow> (nat \<Rightarrow> state) \<Rightarrow> (nat \<Rightarrow> state)" where |
10281 | 416 |
"pcons s p == \<lambda>i. case i of 0 \<Rightarrow> s | Suc j \<Rightarrow> p j" |
417 |
||
418 |
lemma pcons_PathI: "[| (s,t) : M; p \<in> Paths t |] ==> pcons s p \<in> Paths s"; |
|
12815 | 419 |
by(simp add: Paths_def pcons_def split: nat.split); |
10281 | 420 |
|
421 |
lemma "lfp(eufix A B) \<subseteq> eusem A B" |
|
422 |
apply(rule lfp_lowerbound) |
|
12815 | 423 |
apply(clarsimp simp add: eusem_def eufix_def); |
10281 | 424 |
apply(erule disjE); |
425 |
apply(rule_tac x = "apath x" in bexI); |
|
426 |
apply(rule_tac x = 0 in exI); |
|
427 |
apply simp; |
|
428 |
apply simp; |
|
429 |
apply(clarify); |
|
430 |
apply(rule_tac x = "pcons xb p" in bexI); |
|
431 |
apply(rule_tac x = "j+1" in exI); |
|
12815 | 432 |
apply (simp add: pcons_def split: nat.split); |
433 |
apply (simp add: pcons_PathI) |
|
10281 | 434 |
done |
435 |
*) |
|
436 |
(*>*) |
|
12334 | 437 |
|
438 |
text{* Let us close this section with a few words about the executability of |
|
439 |
our model checkers. It is clear that if all sets are finite, they can be |
|
440 |
represented as lists and the usual set operations are easily |
|
15904 | 441 |
implemented. Only @{const lfp} requires a little thought. Fortunately, theory |
58620 | 442 |
@{text While_Combinator} in the Library~@{cite "HOL-Library"} provides a |
12334 | 443 |
theorem stating that in the case of finite sets and a monotone |
444 |
function~@{term F}, the value of \mbox{@{term"lfp F"}} can be computed by |
|
445 |
iterated application of @{term F} to~@{term"{}"} until a fixed point is |
|
446 |
reached. It is actually possible to generate executable functional programs |
|
11494 | 447 |
from HOL definitions, but that is beyond the scope of the tutorial.% |
12334 | 448 |
\index{CTL|)} *} |
10212 | 449 |
(*<*)end(*>*) |