1 (*<*)theory CTL = Base:;(*>*) |
1 (*<*)theory CTL = Base:;(*>*) |
2 |
2 |
3 subsection{*Computation tree logic---CTL*}; |
3 subsection{*Computation tree logic---CTL*}; |
4 |
4 |
5 text{* |
5 text{*\label{sec:CTL} |
6 The semantics of PDL only needs transitive reflexive closure. |
6 The semantics of PDL only needs transitive reflexive closure. |
7 Let us now be a bit more adventurous and introduce a new temporal operator |
7 Let us now be a bit more adventurous and introduce a new temporal operator |
8 that goes beyond transitive reflexive closure. We extend the datatype |
8 that goes beyond transitive reflexive closure. We extend the datatype |
9 @{text formula} by a new constructor |
9 @{text formula} by a new constructor |
10 *}; |
10 *}; |
264 *}; |
264 *}; |
265 |
265 |
266 apply(fast intro:someI2_ex); |
266 apply(fast intro:someI2_ex); |
267 |
267 |
268 txt{*\noindent |
268 txt{*\noindent |
269 What is worth noting here is that we have used @{text fast} rather than @{text blast}. |
269 What is worth noting here is that we have used @{text fast} rather than |
270 The reason is that @{text blast} would fail because it cannot cope with @{thm[source]someI2_ex}: |
270 @{text blast}. The reason is that @{text blast} would fail because it cannot |
271 unifying its conclusion with the current subgoal is nontrivial because of the nested schematic |
271 cope with @{thm[source]someI2_ex}: unifying its conclusion with the current |
272 variables. For efficiency reasons @{text blast} does not even attempt such unifications. |
272 subgoal is nontrivial because of the nested schematic variables. For |
273 Although @{text fast} can in principle cope with complicated unification problems, in practice |
273 efficiency reasons @{text blast} does not even attempt such unifications. |
274 the number of unifiers arising is often prohibitive and the offending rule may need to be applied |
274 Although @{text fast} can in principle cope with complicated unification |
275 explicitly rather than automatically. |
275 problems, in practice the number of unifiers arising is often prohibitive and |
276 |
276 the offending rule may need to be applied explicitly rather than |
277 The induction step is similar, but more involved, because now we face nested occurrences of |
277 automatically. This is what happens in the step case. |
278 @{text SOME}. We merely show the proof commands but do not describe th details: |
278 |
|
279 The induction step is similar, but more involved, because now we face nested |
|
280 occurrences of @{text SOME}. As a result, @{text fast} is no longer able to |
|
281 solve the subgoal and we apply @{thm[source]someI2_ex} by hand. We merely |
|
282 show the proof commands but do not describe the details: |
279 *}; |
283 *}; |
280 |
284 |
281 apply(simp); |
285 apply(simp); |
282 apply(rule someI2_ex); |
286 apply(rule someI2_ex); |
283 apply(blast); |
287 apply(blast); |
395 Fortunately the HOL library proves that in the case of finite sets and a monotone @{term F}, |
399 Fortunately the HOL library proves that in the case of finite sets and a monotone @{term F}, |
396 @{term"lfp F"} can be computed by iterated application of @{term F} to @{term"{}"} until |
400 @{term"lfp F"} can be computed by iterated application of @{term F} to @{term"{}"} until |
397 a fixpoint is reached. It is actually possible to generate executable functional programs |
401 a fixpoint is reached. It is actually possible to generate executable functional programs |
398 from HOL definitions, but that is beyond the scope of the tutorial. |
402 from HOL definitions, but that is beyond the scope of the tutorial. |
399 *} |
403 *} |
400 |
404 (*<*)end(*>*) |
401 (*<*) |
|
402 (* |
|
403 Second proof of opposite direction, directly by wellfounded induction |
|
404 on the initial segment of M that avoids A. |
|
405 |
|
406 Avoid s A = the set of successors of s that can be reached by a finite A-avoiding path |
|
407 *) |
|
408 |
|
409 consts Avoid :: "state \<Rightarrow> state set \<Rightarrow> state set"; |
|
410 inductive "Avoid s A" |
|
411 intros "s \<in> Avoid s A" |
|
412 "\<lbrakk> t \<in> Avoid s A; t \<notin> A; (t,u) \<in> M \<rbrakk> \<Longrightarrow> u \<in> Avoid s A"; |
|
413 |
|
414 (* For any infinite A-avoiding path (f) in Avoid s A, |
|
415 there is some infinite A-avoiding path (p) in Avoid s A that starts with s. |
|
416 *) |
|
417 lemma ex_infinite_path[rule_format]: |
|
418 "t \<in> Avoid s A \<Longrightarrow> |
|
419 \<forall>f. t = f 0 \<longrightarrow> (\<forall>i. (f i, f (Suc i)) \<in> M \<and> f i \<in> Avoid s A \<and> f i \<notin> A) |
|
420 \<longrightarrow> (\<exists> p\<in>Paths s. \<forall>i. p i \<notin> A)"; |
|
421 apply(simp add:Paths_def); |
|
422 apply(erule Avoid.induct); |
|
423 apply(blast); |
|
424 apply(rule allI); |
|
425 apply(erule_tac x = "\<lambda>i. case i of 0 \<Rightarrow> t | Suc i \<Rightarrow> f i" in allE); |
|
426 by(force split:nat.split); |
|
427 |
|
428 lemma Avoid_in_lfp[rule_format(no_asm)]: |
|
429 "\<forall>p\<in>Paths s. \<exists>i. p i \<in> A \<Longrightarrow> t \<in> Avoid s A \<longrightarrow> t \<in> lfp(af A)"; |
|
430 apply(subgoal_tac "wf{(y,x). (x,y)\<in>M \<and> x \<in> Avoid s A \<and> y \<in> Avoid s A \<and> x \<notin> A}"); |
|
431 apply(erule_tac a = t in wf_induct); |
|
432 apply(clarsimp); |
|
433 apply(rule ssubst [OF lfp_unfold[OF mono_af]]); |
|
434 apply(unfold af_def); |
|
435 apply(blast intro:Avoid.intros); |
|
436 apply(erule contrapos2); |
|
437 apply(simp add:wf_iff_no_infinite_down_chain); |
|
438 apply(erule exE); |
|
439 apply(rule ex_infinite_path); |
|
440 by(auto); |
|
441 |
|
442 theorem AF_lemma2: |
|
443 "{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)"; |
|
444 apply(rule subsetI); |
|
445 apply(simp); |
|
446 apply(erule Avoid_in_lfp); |
|
447 by(rule Avoid.intros); |
|
448 |
|
449 end(*>*) |
|