doc-src/TutorialI/CTL/CTL.thy
 author nipkow Thu Oct 12 18:38:23 2000 +0200 (2000-10-12) changeset 10212 33fe2d701ddd parent 10210 e8aa81362f41 child 10217 e61e7e1eacaf permissions -rw-r--r--
*** empty log message ***
 nipkow@10159  1 (*<*)theory CTL = Base:;(*>*)  nipkow@9958  2 nipkow@10159  3 subsection{*Computation tree logic---CTL*};  nipkow@9958  4 nipkow@10212  5 text{*\label{sec:CTL}  nipkow@10149  6 The semantics of PDL only needs transitive reflexive closure.  nipkow@10149  7 Let us now be a bit more adventurous and introduce a new temporal operator  nipkow@10149  8 that goes beyond transitive reflexive closure. We extend the datatype  nipkow@10149  9 @{text formula} by a new constructor  nipkow@10159  10 *};  nipkow@10149  11 (*<*)  nipkow@10149  12 datatype formula = Atom atom  nipkow@10149  13  | Neg formula  nipkow@10149  14  | And formula formula  nipkow@10149  15  | AX formula  nipkow@10149  16  | EF formula(*>*)  nipkow@10159  17  | AF formula;  nipkow@9958  18 nipkow@10149  19 text{*\noindent  nipkow@10149  20 which stands for "always in the future":  nipkow@10159  21 on all paths, at some point the formula holds. Formalizing the notion of an infinite path is easy  nipkow@10159  22 in HOL: it is simply a function from @{typ nat} to @{typ state}.  nipkow@10159  23 *};  nipkow@9958  24 nipkow@9958  25 constdefs Paths :: "state \ (nat \ state)set"  nipkow@10149  26  "Paths s \ {p. s = p 0 \ (\i. (p i, p(i+1)) \ M)}";  nipkow@10149  27 nipkow@10149  28 text{*\noindent  nipkow@10159  29 This definition allows a very succinct statement of the semantics of @{term AF}:  nipkow@10149  30 \footnote{Do not be mislead: neither datatypes nor recursive functions can be  nipkow@10149  31 extended by new constructors or equations. This is just a trick of the  nipkow@10149  32 presentation. In reality one has to define a new datatype and a new function.}  nipkow@10159  33 *};  nipkow@10149  34 (*<*)  nipkow@10159  35 consts valid :: "state \ formula \ bool" ("(_ \ _)" [80,80] 80);  nipkow@9958  36 nipkow@9958  37 primrec  nipkow@10133  38 "s \ Atom a = (a \ L s)"  nipkow@10149  39 "s \ Neg f = (~(s \ f))"  nipkow@9958  40 "s \ And f g = (s \ f \ s \ g)"  nipkow@9958  41 "s \ AX f = (\t. (s,t) \ M \ t \ f)"  nipkow@9958  42 "s \ EF f = (\t. (s,t) \ M^* \ t \ f)"  nipkow@10149  43 (*>*)  nipkow@9958  44 "s \ AF f = (\p \ Paths s. \i. p i \ f)";  nipkow@9958  45 nipkow@10149  46 text{*\noindent  nipkow@10149  47 Model checking @{term AF} involves a function which  nipkow@10159  48 is just complicated enough to warrant a separate definition:  nipkow@10159  49 *};  nipkow@10149  50 nipkow@9958  51 constdefs af :: "state set \ state set \ state set"  nipkow@10149  52  "af A T \ A \ {s. \t. (s, t) \ M \ t \ T}";  nipkow@10149  53 nipkow@10149  54 text{*\noindent  nipkow@10159  55 Now we define @{term "mc(AF f)"} as the least set @{term T} that contains  nipkow@10149  56 @{term"mc f"} and all states all of whose direct successors are in @{term T}:  nipkow@10159  57 *};  nipkow@10149  58 (*<*)  nipkow@10149  59 consts mc :: "formula \ state set";  nipkow@9958  60 primrec  nipkow@10133  61 "mc(Atom a) = {s. a \ L s}"  nipkow@10149  62 "mc(Neg f) = -mc f"  nipkow@9958  63 "mc(And f g) = mc f \ mc g"  nipkow@9958  64 "mc(AX f) = {s. \t. (s,t) \ M \ t \ mc f}"  nipkow@10149  65 "mc(EF f) = lfp(\T. mc f \ M^-1 ^^ T)"(*>*)  nipkow@9958  66 "mc(AF f) = lfp(af(mc f))";  nipkow@10159  67 nipkow@10159  68 text{*\noindent  nipkow@10159  69 Because @{term af} is monotone in its second argument (and also its first, but  nipkow@10159  70 that is irrelevant) @{term"af A"} has a least fixpoint:  nipkow@10159  71 *};  nipkow@10159  72 nipkow@10159  73 lemma mono_af: "mono(af A)";  nipkow@10159  74 apply(simp add: mono_def af_def);  nipkow@10159  75 apply blast;  nipkow@10159  76 done  nipkow@10149  77 (*<*)  nipkow@10159  78 lemma mono_ef: "mono(\T. A \ M^-1 ^^ T)";  nipkow@10159  79 apply(rule monoI);  nipkow@10159  80 by(blast);  nipkow@9958  81 nipkow@10149  82 lemma EF_lemma:  nipkow@10159  83  "lfp(\T. A \ M^-1 ^^ T) = {s. \t. (s,t) \ M^* \ t \ A}";  nipkow@9958  84 apply(rule equalityI);  nipkow@9958  85  apply(rule subsetI);  nipkow@10159  86  apply(simp);  wenzelm@10210  87  apply(erule lfp_induct);  nipkow@10159  88  apply(rule mono_ef);  nipkow@10159  89  apply(simp);  nipkow@9958  90  apply(blast intro: r_into_rtrancl rtrancl_trans);  nipkow@10159  91 apply(rule subsetI);  nipkow@10159  92 apply(simp, clarify);  nipkow@10159  93 apply(erule converse_rtrancl_induct);  nipkow@10186  94  apply(rule ssubst[OF lfp_unfold[OF mono_ef]]);  nipkow@10159  95  apply(blast);  nipkow@10186  96 apply(rule ssubst[OF lfp_unfold[OF mono_ef]]);  nipkow@10159  97 by(blast);  nipkow@10149  98 (*>*)  nipkow@10159  99 text{*  nipkow@10159  100 All we need to prove now is that @{term mc} and @{text"\"}  nipkow@10159  101 agree for @{term AF}, i.e.\ that @{prop"mc(AF f) = {s. s \  nipkow@10159  102 AF f}"}. This time we prove the two containments separately, starting  nipkow@10159  103 with the easy one:  nipkow@10159  104 *};  nipkow@9958  105 nipkow@10159  106 theorem AF_lemma1:  nipkow@10159  107  "lfp(af A) \ {s. \ p \ Paths s. \ i. p i \ A}";  nipkow@10159  108 nipkow@10159  109 txt{*\noindent  nipkow@10159  110 The proof is again pointwise. Fixpoint induction on the premise @{prop"s \ lfp(af A)"} followed  nipkow@10159  111 by simplification and clarification  nipkow@10159  112 *};  nipkow@10159  113 nipkow@9958  114 apply(rule subsetI);  wenzelm@10210  115 apply(erule lfp_induct[OF _ mono_af]);  nipkow@10159  116 apply(clarsimp simp add: af_def Paths_def);  nipkow@10159  117 (*ML"Pretty.setmargin 70";  nipkow@10159  118 pr(latex xsymbols symbols);*)  nipkow@10159  119 txt{*\noindent  nipkow@10159  120 leads to the following somewhat involved proof state  nipkow@10159  121 \begin{isabelle}  nipkow@10159  122 \ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline  nipkow@10159  123 \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ \isadigit{0}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline  nipkow@10159  124 \ \ \ \ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymand}\isanewline  nipkow@10159  125 \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}p{\isachardot}\ t\ {\isacharequal}\ p\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline  nipkow@10159  126 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline  nipkow@10159  127 \ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline  nipkow@10159  128 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A  nipkow@10159  129 \end{isabelle}  nipkow@10159  130 Now we eliminate the disjunction. The case @{prop"p 0 \ A"} is trivial:  nipkow@10159  131 *};  nipkow@10159  132 nipkow@9958  133 apply(erule disjE);  nipkow@9958  134  apply(blast);  nipkow@10159  135 nipkow@10159  136 txt{*\noindent  nipkow@10159  137 In the other case we set @{term t} to @{term"p 1"} and simplify matters:  nipkow@10159  138 *};  nipkow@10159  139 nipkow@9958  140 apply(erule_tac x = "p 1" in allE);  nipkow@9958  141 apply(clarsimp);  nipkow@10159  142 (*ML"Pretty.setmargin 70";  nipkow@10159  143 pr(latex xsymbols symbols);*)  nipkow@10159  144 nipkow@10159  145 txt{*  nipkow@10159  146 \begin{isabelle}  nipkow@10159  147 \ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\ p\ \isadigit{1}\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharsemicolon}\isanewline  nipkow@10159  148 \ \ \ \ \ \ \ \ \ \ \ {\isasymforall}pa{\isachardot}\ p\ \isadigit{1}\ {\isacharequal}\ pa\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline  nipkow@10159  149 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline  nipkow@10159  150 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A  nipkow@10159  151 \end{isabelle}  nipkow@10159  152 It merely remains to set @{term pa} to @{term"\i. p(i+1)"}, i.e.\ @{term p} without its  nipkow@10159  153 first element. The rest is practically automatic:  nipkow@10159  154 *};  nipkow@10159  155 nipkow@9958  156 apply(erule_tac x = "\i. p(i+1)" in allE);  nipkow@10159  157 apply simp;  nipkow@10159  158 apply blast;  nipkow@10159  159 done;  nipkow@9958  160 nipkow@9958  161 text{*  nipkow@10159  162 The opposite containment is proved by contradiction: if some state  nipkow@10159  163 @{term s} is not in @{term"lfp(af A)"}, then we can construct an  nipkow@9958  164 infinite @{term A}-avoiding path starting from @{term s}. The reason is  nipkow@10159  165 that by unfolding @{term lfp} we find that if @{term s} is not in  nipkow@9958  166 @{term"lfp(af A)"}, then @{term s} is not in @{term A} and there is a  nipkow@9958  167 direct successor of @{term s} that is again not in @{term"lfp(af  nipkow@9958  168 A)"}. Iterating this argument yields the promised infinite  nipkow@9958  169 @{term A}-avoiding path. Let us formalize this sketch.  nipkow@9958  170 nipkow@9958  171 The one-step argument in the above sketch  nipkow@9958  172 *};  nipkow@9958  173 nipkow@9958  174 lemma not_in_lfp_afD:  nipkow@9958  175  "s \ lfp(af A) \ s \ A \ (\ t. (s,t)\M \ t \ lfp(af A))";  nipkow@9958  176 apply(erule swap);  nipkow@10186  177 apply(rule ssubst[OF lfp_unfold[OF mono_af]]);  nipkow@10159  178 apply(simp add:af_def);  nipkow@10159  179 done;  nipkow@9958  180 nipkow@9958  181 text{*\noindent  nipkow@9958  182 is proved by a variant of contraposition (@{thm[source]swap}:  nipkow@9958  183 @{thm swap[no_vars]}), i.e.\ assuming the negation of the conclusion  nipkow@9958  184 and proving @{term"s : lfp(af A)"}. Unfolding @{term lfp} once and  nipkow@9958  185 simplifying with the definition of @{term af} finishes the proof.  nipkow@9958  186 nipkow@9958  187 Now we iterate this process. The following construction of the desired  nipkow@9958  188 path is parameterized by a predicate @{term P} that should hold along the path:  nipkow@9958  189 *};  nipkow@9958  190 nipkow@9958  191 consts path :: "state \ (state \ bool) \ (nat \ state)";  nipkow@9958  192 primrec  nipkow@9958  193 "path s P 0 = s"  nipkow@9958  194 "path s P (Suc n) = (SOME t. (path s P n,t) \ M \ P t)";  nipkow@9958  195 nipkow@9958  196 text{*\noindent  nipkow@9958  197 Element @{term"n+1"} on this path is some arbitrary successor  nipkow@10159  198 @{term t} of element @{term n} such that @{term"P t"} holds. Remember that @{text"SOME t. R t"}  nipkow@10159  199 is some arbitrary but fixed @{term t} such that @{prop"R t"} holds (see \S\ref{sec-SOME}). Of  nipkow@10159  200 course, such a @{term t} may in general not exist, but that is of no  nipkow@9958  201 concern to us since we will only use @{term path} in such cases where a  nipkow@10159  202 suitable @{term t} does exist.  nipkow@9958  203 nipkow@10159  204 Let us show that if each state @{term s} that satisfies @{term P}  nipkow@10159  205 has a successor that again satisfies @{term P}, then there exists an infinite @{term P}-path:  nipkow@9958  206 *};  nipkow@9958  207 nipkow@10159  208 lemma infinity_lemma:  nipkow@10159  209  "\ P s; \s. P s \ (\ t. (s,t) \ M \ P t) \ \  nipkow@10159  210  \p\Paths s. \i. P(p i)";  nipkow@9958  211 nipkow@9958  212 txt{*\noindent  nipkow@9958  213 First we rephrase the conclusion slightly because we need to prove both the path property  nipkow@10159  214 and the fact that @{term P} holds simultaneously:  nipkow@9958  215 *};  nipkow@9958  216 nipkow@10159  217 apply(subgoal_tac "\p. s = p 0 \ (\i. (p i,p(i+1)) \ M \ P(p i))");  nipkow@9958  218 nipkow@9958  219 txt{*\noindent  nipkow@10159  220 From this proposition the original goal follows easily:  nipkow@9958  221 *};  nipkow@9958  222 nipkow@9958  223  apply(simp add:Paths_def, blast);  nipkow@10159  224 nipkow@10159  225 txt{*\noindent  nipkow@10159  226 The new subgoal is proved by providing the witness @{term "path s P"} for @{term p}:  nipkow@10159  227 *};  nipkow@10159  228 nipkow@9958  229 apply(rule_tac x = "path s P" in exI);  nipkow@10159  230 apply(clarsimp);  nipkow@10159  231 (*ML"Pretty.setmargin 70";  nipkow@10159  232 pr(latex xsymbols symbols);*)  nipkow@10159  233 nipkow@10159  234 txt{*\noindent  nipkow@10159  235 After simplification and clarification the subgoal has the following compact form  nipkow@10159  236 \begin{isabelle}  nipkow@10159  237 \ \isadigit{1}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline  nipkow@10159  238 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\isanewline  nipkow@10159  239 \ \ \ \ \ \ \ \ \ \ \ \ P\ {\isacharparenleft}path\ s\ P\ i{\isacharparenright}  nipkow@10159  240 \end{isabelle}  nipkow@10159  241 and invites a proof by induction on @{term i}:  nipkow@10159  242 *};  nipkow@10159  243 nipkow@9958  244 apply(induct_tac i);  nipkow@9958  245  apply(simp);  nipkow@10159  246 (*ML"Pretty.setmargin 70";  nipkow@10159  247 pr(latex xsymbols symbols);*)  nipkow@10159  248 nipkow@10159  249 txt{*\noindent  nipkow@10159  250 After simplification the base case boils down to  nipkow@10159  251 \begin{isabelle}  nipkow@10159  252 \ \isadigit{1}{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline  nipkow@10159  253 \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M  nipkow@10159  254 \end{isabelle}  nipkow@10159  255 The conclusion looks exceedingly trivial: after all, @{term t} is chosen such that @{prop"(s,t):M"}  nipkow@10159  256 holds. However, we first have to show that such a @{term t} actually exists! This reasoning  nipkow@10159  257 is embodied in the theorem @{thm[source]someI2_ex}:  nipkow@10159  258 @{thm[display,eta_contract=false]someI2_ex}  nipkow@10159  259 When we apply this theorem as an introduction rule, @{text"?P x"} becomes  nipkow@10159  260 @{prop"(s, x) : M & P x"} and @{text"?Q x"} becomes @{prop"(s,x) : M"} and we have to prove  nipkow@10159  261 two subgoals: @{prop"EX a. (s, a) : M & P a"}, which follows from the assumptions, and  nipkow@10159  262 @{prop"(s, x) : M & P x ==> (s,x) : M"}, which is trivial. Thus it is not surprising that  nipkow@10159  263 @{text fast} can prove the base case quickly:  nipkow@10159  264 *};  nipkow@10159  265 wenzelm@10000  266  apply(fast intro:someI2_ex);  nipkow@10159  267 nipkow@10159  268 txt{*\noindent  nipkow@10212  269 What is worth noting here is that we have used @{text fast} rather than  nipkow@10212  270 @{text blast}. The reason is that @{text blast} would fail because it cannot  nipkow@10212  271 cope with @{thm[source]someI2_ex}: unifying its conclusion with the current  nipkow@10212  272 subgoal is nontrivial because of the nested schematic variables. For  nipkow@10212  273 efficiency reasons @{text blast} does not even attempt such unifications.  nipkow@10212  274 Although @{text fast} can in principle cope with complicated unification  nipkow@10212  275 problems, in practice the number of unifiers arising is often prohibitive and  nipkow@10212  276 the offending rule may need to be applied explicitly rather than  nipkow@10212  277 automatically. This is what happens in the step case.  nipkow@10159  278 nipkow@10212  279 The induction step is similar, but more involved, because now we face nested  nipkow@10212  280 occurrences of @{text SOME}. As a result, @{text fast} is no longer able to  nipkow@10212  281 solve the subgoal and we apply @{thm[source]someI2_ex} by hand. We merely  nipkow@10212  282 show the proof commands but do not describe the details:  nipkow@10159  283 *};  nipkow@10159  284 nipkow@9958  285 apply(simp);  wenzelm@10000  286 apply(rule someI2_ex);  nipkow@9958  287  apply(blast);  wenzelm@10000  288 apply(rule someI2_ex);  nipkow@9958  289  apply(blast);  nipkow@10159  290 apply(blast);  nipkow@10159  291 done;  nipkow@9958  292 nipkow@10159  293 text{*  nipkow@10159  294 Function @{term path} has fulfilled its purpose now and can be forgotten  nipkow@10159  295 about. It was merely defined to provide the witness in the proof of the  nipkow@10171  296 @{thm[source]infinity_lemma}. Aficionados of minimal proofs might like to know  nipkow@10159  297 that we could have given the witness without having to define a new function:  nipkow@10159  298 the term  nipkow@10159  299 @{term[display]"nat_rec s (\n t. SOME u. (t,u)\M \ P u)"}  nipkow@10171  300 is extensionally equal to @{term"path s P"},  nipkow@10159  301 where @{term nat_rec} is the predefined primitive recursor on @{typ nat}, whose defining  nipkow@10171  302 equations we omit.  nipkow@10159  303 *};  nipkow@10159  304 (*<*)  nipkow@10159  305 lemma infinity_lemma:  nipkow@9958  306 "\ P s; \ s. P s \ (\ t. (s,t)\M \ P t) \ \  nipkow@9958  307  \ p\Paths s. \ i. P(p i)";  nipkow@9958  308 apply(subgoal_tac  nipkow@9958  309  "\ p. s = p 0 \ (\ i. (p i,p(Suc i))\M \ P(p i))");  nipkow@9958  310  apply(simp add:Paths_def);  nipkow@9958  311  apply(blast);  nipkow@9958  312 apply(rule_tac x = "nat_rec s (\n t. SOME u. (t,u)\M \ P u)" in exI);  nipkow@9958  313 apply(simp);  nipkow@9958  314 apply(intro strip);  nipkow@9958  315 apply(induct_tac i);  nipkow@9958  316  apply(simp);  wenzelm@10000  317  apply(fast intro:someI2_ex);  nipkow@9958  318 apply(simp);  wenzelm@10000  319 apply(rule someI2_ex);  nipkow@9958  320  apply(blast);  wenzelm@10000  321 apply(rule someI2_ex);  nipkow@9958  322  apply(blast);  nipkow@9958  323 by(blast);  nipkow@10159  324 (*>*)  nipkow@9958  325 nipkow@10159  326 text{*  nipkow@10159  327 At last we can prove the opposite direction of @{thm[source]AF_lemma1}:  nipkow@10159  328 *};  nipkow@10159  329 nipkow@10159  330 theorem AF_lemma2:  nipkow@9958  331 "{s. \ p \ Paths s. \ i. p i \ A} \ lfp(af A)";  nipkow@10159  332 nipkow@10159  333 txt{*\noindent  nipkow@10159  334 The proof is again pointwise and then by contraposition (@{thm[source]contrapos2} is the rule  nipkow@10159  335 @{thm contrapos2}):  nipkow@10159  336 *};  nipkow@10159  337 nipkow@9958  338 apply(rule subsetI);  nipkow@9958  339 apply(erule contrapos2);  nipkow@9958  340 apply simp;  nipkow@10159  341 (*pr(latex xsymbols symbols);*)  nipkow@10159  342 nipkow@10159  343 txt{*  nipkow@10159  344 \begin{isabelle}  nipkow@10159  345 \ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A  nipkow@10159  346 \end{isabelle}  nipkow@10159  347 Applying the @{thm[source]infinity_lemma} as a destruction rule leaves two subgoals, the second  nipkow@10159  348 premise of @{thm[source]infinity_lemma} and the original subgoal:  nipkow@10159  349 *};  nipkow@10159  350 nipkow@10159  351 apply(drule infinity_lemma);  nipkow@10159  352 (*pr(latex xsymbols symbols);*)  nipkow@10159  353 nipkow@10159  354 txt{*  nipkow@10159  355 \begin{isabelle}  nipkow@10159  356 \ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ {\isasymforall}s{\isachardot}\ s\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}\isanewline  nipkow@10159  357 \ \isadigit{2}{\isachardot}\ {\isasymAnd}s{\isachardot}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline  nipkow@10159  358 \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A  nipkow@10159  359 \end{isabelle}  nipkow@10159  360 Both are solved automatically:  nipkow@10159  361 *};  nipkow@9958  362 nipkow@10159  363  apply(auto dest:not_in_lfp_afD);  nipkow@10159  364 done;  nipkow@9958  365 nipkow@10159  366 text{*  nipkow@10159  367 The main theorem is proved as for PDL, except that we also derive the necessary equality  nipkow@10159  368 @{text"lfp(af A) = ..."} by combining @{thm[source]AF_lemma1} and @{thm[source]AF_lemma2}  nipkow@10159  369 on the spot:  nipkow@10159  370 *}  nipkow@10159  371 nipkow@10159  372 theorem "mc f = {s. s \ f}";  nipkow@10159  373 apply(induct_tac f);  nipkow@10159  374 apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2]);  nipkow@10159  375 done  nipkow@10159  376 nipkow@10159  377 text{*  nipkow@10171  378 The above language is not quite CTL. The latter also includes an  nipkow@10178  379 until-operator, which is the subject of the following exercise.  nipkow@10171  380 It is not definable in terms of the other operators!  nipkow@10171  381 \begin{exercise}  nipkow@10178  382 Extend the datatype of formulae by the binary until operator @{term"EU f g"} with semantics  nipkow@10178  383 there exist a path where @{term f} is true until @{term g} becomes true''  nipkow@10178  384 @{text[display]"s \ EU f g = (\p\Paths s. \j. p j \ g \ (\i < j. p i \ f))"}  nipkow@10171  385 and model checking algorithm  nipkow@10178  386 @{text[display]"mc(EU f g) = lfp(\T. mc g \ mc f \ (M^-1 ^^ T))"}  nipkow@10186  387 Prove the equivalence between semantics and model checking, i.e.\ that  nipkow@10186  388 @{prop[display]"mc(EU f g) = {s. s \ EU f g}"}  nipkow@10186  389 %For readability you may want to annotate {term EU} with its customary syntax  nipkow@10186  390 %{text[display]"| EU formula formula E[_ U _]"}  nipkow@10186  391 %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.  nipkow@10186  392 \end{exercise}  nipkow@10192  393 For more CTL exercises see, for example \cite{Huth-Ryan-book}.  nipkow@10186  394 \bigskip  nipkow@10178  395 nipkow@10186  396 Let us close this section with a few words about the executability of our model checkers.  nipkow@10159  397 It is clear that if all sets are finite, they can be represented as lists and the usual  nipkow@10159  398 set operations are easily implemented. Only @{term lfp} requires a little thought.  nipkow@10159  399 Fortunately the HOL library proves that in the case of finite sets and a monotone @{term F},  nipkow@10159  400 @{term"lfp F"} can be computed by iterated application of @{term F} to @{term"{}"} until  nipkow@10186  401 a fixpoint is reached. It is actually possible to generate executable functional programs  nipkow@10159  402 from HOL definitions, but that is beyond the scope of the tutorial.  nipkow@10159  403 *}  nipkow@10212  404 (*<*)end(*>*)