doc-src/TutorialI/CTL/CTL.thy
 author nipkow Wed Dec 06 13:22:58 2000 +0100 (2000-12-06) changeset 10608 620647438780 parent 10363 6e8002c1790e child 10654 458068404143 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@10242  70 that is irrelevant) @{term"af A"} has a least fixed point:  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@10281  90  apply(blast intro: 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@10225  110 In contrast to the analogous property for @{term EF}, and just  nipkow@10242  111 for a change, we do not use fixed point induction but a weaker theorem,  nipkow@10225  112 @{thm[source]lfp_lowerbound}:  nipkow@10225  113 @{thm[display]lfp_lowerbound[of _ "S",no_vars]}  nipkow@10225  114 The instance of the premise @{prop"f S \ S"} is proved pointwise,  nipkow@10281  115 a decision that clarification takes for us:  nipkow@10159  116 *};  nipkow@10225  117 apply(rule lfp_lowerbound);  nipkow@10159  118 apply(clarsimp simp add: af_def Paths_def);  nipkow@10363  119 nipkow@10225  120 txt{*  nipkow@10363  121 @{subgoals[display,indent=0,margin=70,goals_limit=1]}  nipkow@10159  122 Now we eliminate the disjunction. The case @{prop"p 0 \ A"} is trivial:  nipkow@10159  123 *};  nipkow@10159  124 nipkow@9958  125 apply(erule disjE);  nipkow@9958  126  apply(blast);  nipkow@10159  127 nipkow@10159  128 txt{*\noindent  nipkow@10159  129 In the other case we set @{term t} to @{term"p 1"} and simplify matters:  nipkow@10159  130 *};  nipkow@10159  131 nipkow@9958  132 apply(erule_tac x = "p 1" in allE);  nipkow@9958  133 apply(clarsimp);  nipkow@10159  134 nipkow@10159  135 txt{*  nipkow@10363  136 @{subgoals[display,indent=0,margin=70,goals_limit=1]}  nipkow@10159  137 It merely remains to set @{term pa} to @{term"\i. p(i+1)"}, i.e.\ @{term p} without its  nipkow@10159  138 first element. The rest is practically automatic:  nipkow@10159  139 *};  nipkow@10159  140 nipkow@9958  141 apply(erule_tac x = "\i. p(i+1)" in allE);  nipkow@10159  142 apply simp;  nipkow@10159  143 apply blast;  nipkow@10159  144 done;  nipkow@9958  145 nipkow@10225  146 nipkow@9958  147 text{*  nipkow@10159  148 The opposite containment is proved by contradiction: if some state  nipkow@10159  149 @{term s} is not in @{term"lfp(af A)"}, then we can construct an  nipkow@9958  150 infinite @{term A}-avoiding path starting from @{term s}. The reason is  nipkow@10159  151 that by unfolding @{term lfp} we find that if @{term s} is not in  nipkow@9958  152 @{term"lfp(af A)"}, then @{term s} is not in @{term A} and there is a  nipkow@9958  153 direct successor of @{term s} that is again not in @{term"lfp(af  nipkow@9958  154 A)"}. Iterating this argument yields the promised infinite  nipkow@9958  155 @{term A}-avoiding path. Let us formalize this sketch.  nipkow@9958  156 nipkow@9958  157 The one-step argument in the above sketch  nipkow@9958  158 *};  nipkow@9958  159 nipkow@9958  160 lemma not_in_lfp_afD:  nipkow@9958  161  "s \ lfp(af A) \ s \ A \ (\ t. (s,t)\M \ t \ lfp(af A))";  paulson@10235  162 apply(erule contrapos_np);  nipkow@10186  163 apply(rule ssubst[OF lfp_unfold[OF mono_af]]);  nipkow@10159  164 apply(simp add:af_def);  nipkow@10159  165 done;  nipkow@9958  166 nipkow@9958  167 text{*\noindent  nipkow@10237  168 is proved by a variant of contraposition:  nipkow@10237  169 assume the negation of the conclusion and prove @{term"s : lfp(af A)"}.  nipkow@10237  170 Unfolding @{term lfp} once and  nipkow@9958  171 simplifying with the definition of @{term af} finishes the proof.  nipkow@9958  172 nipkow@9958  173 Now we iterate this process. The following construction of the desired  nipkow@9958  174 path is parameterized by a predicate @{term P} that should hold along the path:  nipkow@9958  175 *};  nipkow@9958  176 nipkow@9958  177 consts path :: "state \ (state \ bool) \ (nat \ state)";  nipkow@9958  178 primrec  nipkow@9958  179 "path s P 0 = s"  nipkow@9958  180 "path s P (Suc n) = (SOME t. (path s P n,t) \ M \ P t)";  nipkow@9958  181 nipkow@9958  182 text{*\noindent  nipkow@9958  183 Element @{term"n+1"} on this path is some arbitrary successor  nipkow@10159  184 @{term t} of element @{term n} such that @{term"P t"} holds. Remember that @{text"SOME t. R t"}  nipkow@10159  185 is some arbitrary but fixed @{term t} such that @{prop"R t"} holds (see \S\ref{sec-SOME}). Of  nipkow@10159  186 course, such a @{term t} may in general not exist, but that is of no  nipkow@9958  187 concern to us since we will only use @{term path} in such cases where a  nipkow@10159  188 suitable @{term t} does exist.  nipkow@9958  189 nipkow@10159  190 Let us show that if each state @{term s} that satisfies @{term P}  nipkow@10159  191 has a successor that again satisfies @{term P}, then there exists an infinite @{term P}-path:  nipkow@9958  192 *};  nipkow@9958  193 nipkow@10159  194 lemma infinity_lemma:  nipkow@10159  195  "\ P s; \s. P s \ (\ t. (s,t) \ M \ P t) \ \  nipkow@10159  196  \p\Paths s. \i. P(p i)";  nipkow@9958  197 nipkow@9958  198 txt{*\noindent  nipkow@9958  199 First we rephrase the conclusion slightly because we need to prove both the path property  nipkow@10159  200 and the fact that @{term P} holds simultaneously:  nipkow@9958  201 *};  nipkow@9958  202 nipkow@10159  203 apply(subgoal_tac "\p. s = p 0 \ (\i. (p i,p(i+1)) \ M \ P(p i))");  nipkow@9958  204 nipkow@9958  205 txt{*\noindent  nipkow@10159  206 From this proposition the original goal follows easily:  nipkow@9958  207 *};  nipkow@9958  208 nipkow@9958  209  apply(simp add:Paths_def, blast);  nipkow@10159  210 nipkow@10159  211 txt{*\noindent  nipkow@10159  212 The new subgoal is proved by providing the witness @{term "path s P"} for @{term p}:  nipkow@10159  213 *};  nipkow@10159  214 nipkow@9958  215 apply(rule_tac x = "path s P" in exI);  nipkow@10159  216 apply(clarsimp);  nipkow@10159  217 nipkow@10159  218 txt{*\noindent  nipkow@10159  219 After simplification and clarification the subgoal has the following compact form  nipkow@10363  220 @{subgoals[display,indent=0,margin=70,goals_limit=1]}  nipkow@10159  221 and invites a proof by induction on @{term i}:  nipkow@10159  222 *};  nipkow@10159  223 nipkow@9958  224 apply(induct_tac i);  nipkow@9958  225  apply(simp);  nipkow@10159  226 nipkow@10159  227 txt{*\noindent  nipkow@10159  228 After simplification the base case boils down to  nipkow@10363  229 @{subgoals[display,indent=0,margin=70,goals_limit=1]}  nipkow@10159  230 The conclusion looks exceedingly trivial: after all, @{term t} is chosen such that @{prop"(s,t):M"}  nipkow@10159  231 holds. However, we first have to show that such a @{term t} actually exists! This reasoning  nipkow@10159  232 is embodied in the theorem @{thm[source]someI2_ex}:  nipkow@10159  233 @{thm[display,eta_contract=false]someI2_ex}  nipkow@10159  234 When we apply this theorem as an introduction rule, @{text"?P x"} becomes  nipkow@10159  235 @{prop"(s, x) : M & P x"} and @{text"?Q x"} becomes @{prop"(s,x) : M"} and we have to prove  nipkow@10159  236 two subgoals: @{prop"EX a. (s, a) : M & P a"}, which follows from the assumptions, and  nipkow@10159  237 @{prop"(s, x) : M & P x ==> (s,x) : M"}, which is trivial. Thus it is not surprising that  nipkow@10159  238 @{text fast} can prove the base case quickly:  nipkow@10159  239 *};  nipkow@10159  240 wenzelm@10000  241  apply(fast intro:someI2_ex);  nipkow@10159  242 nipkow@10159  243 txt{*\noindent  nipkow@10212  244 What is worth noting here is that we have used @{text fast} rather than  nipkow@10212  245 @{text blast}. The reason is that @{text blast} would fail because it cannot  nipkow@10212  246 cope with @{thm[source]someI2_ex}: unifying its conclusion with the current  nipkow@10212  247 subgoal is nontrivial because of the nested schematic variables. For  nipkow@10212  248 efficiency reasons @{text blast} does not even attempt such unifications.  nipkow@10212  249 Although @{text fast} can in principle cope with complicated unification  nipkow@10212  250 problems, in practice the number of unifiers arising is often prohibitive and  nipkow@10212  251 the offending rule may need to be applied explicitly rather than  nipkow@10212  252 automatically. This is what happens in the step case.  nipkow@10159  253 nipkow@10212  254 The induction step is similar, but more involved, because now we face nested  nipkow@10212  255 occurrences of @{text SOME}. As a result, @{text fast} is no longer able to  nipkow@10212  256 solve the subgoal and we apply @{thm[source]someI2_ex} by hand. We merely  nipkow@10212  257 show the proof commands but do not describe the details:  nipkow@10159  258 *};  nipkow@10159  259 nipkow@9958  260 apply(simp);  wenzelm@10000  261 apply(rule someI2_ex);  nipkow@9958  262  apply(blast);  wenzelm@10000  263 apply(rule someI2_ex);  nipkow@9958  264  apply(blast);  nipkow@10159  265 apply(blast);  nipkow@10159  266 done;  nipkow@9958  267 nipkow@10159  268 text{*  nipkow@10159  269 Function @{term path} has fulfilled its purpose now and can be forgotten  nipkow@10159  270 about. It was merely defined to provide the witness in the proof of the  nipkow@10171  271 @{thm[source]infinity_lemma}. Aficionados of minimal proofs might like to know  nipkow@10159  272 that we could have given the witness without having to define a new function:  nipkow@10159  273 the term  nipkow@10159  274 @{term[display]"nat_rec s (\n t. SOME u. (t,u)\M \ P u)"}  nipkow@10171  275 is extensionally equal to @{term"path s P"},  nipkow@10159  276 where @{term nat_rec} is the predefined primitive recursor on @{typ nat}, whose defining  nipkow@10171  277 equations we omit.  nipkow@10159  278 *};  nipkow@10159  279 (*<*)  nipkow@10159  280 lemma infinity_lemma:  nipkow@9958  281 "\ P s; \ s. P s \ (\ t. (s,t)\M \ P t) \ \  nipkow@9958  282  \ p\Paths s. \ i. P(p i)";  nipkow@9958  283 apply(subgoal_tac  nipkow@9958  284  "\ p. s = p 0 \ (\ i. (p i,p(Suc i))\M \ P(p i))");  nipkow@9958  285  apply(simp add:Paths_def);  nipkow@9958  286  apply(blast);  nipkow@9958  287 apply(rule_tac x = "nat_rec s (\n t. SOME u. (t,u)\M \ P u)" in exI);  nipkow@9958  288 apply(simp);  nipkow@9958  289 apply(intro strip);  nipkow@9958  290 apply(induct_tac i);  nipkow@9958  291  apply(simp);  wenzelm@10000  292  apply(fast intro:someI2_ex);  nipkow@9958  293 apply(simp);  wenzelm@10000  294 apply(rule someI2_ex);  nipkow@9958  295  apply(blast);  wenzelm@10000  296 apply(rule someI2_ex);  nipkow@9958  297  apply(blast);  nipkow@9958  298 by(blast);  nipkow@10159  299 (*>*)  nipkow@9958  300 nipkow@10159  301 text{*  nipkow@10159  302 At last we can prove the opposite direction of @{thm[source]AF_lemma1}:  nipkow@10159  303 *};  nipkow@10159  304 nipkow@10159  305 theorem AF_lemma2:  nipkow@9958  306 "{s. \ p \ Paths s. \ i. p i \ A} \ lfp(af A)";  nipkow@10159  307 nipkow@10159  308 txt{*\noindent  nipkow@10237  309 The proof is again pointwise and then by contraposition:  nipkow@10159  310 *};  nipkow@10159  311 nipkow@9958  312 apply(rule subsetI);  paulson@10235  313 apply(erule contrapos_pp);  nipkow@9958  314 apply simp;  nipkow@10159  315 nipkow@10159  316 txt{*  nipkow@10363  317 @{subgoals[display,indent=0,goals_limit=1]}  nipkow@10159  318 Applying the @{thm[source]infinity_lemma} as a destruction rule leaves two subgoals, the second  nipkow@10159  319 premise of @{thm[source]infinity_lemma} and the original subgoal:  nipkow@10159  320 *};  nipkow@10159  321 nipkow@10159  322 apply(drule infinity_lemma);  nipkow@10159  323 nipkow@10159  324 txt{*  nipkow@10363  325 @{subgoals[display,indent=0,margin=65]}  nipkow@10159  326 Both are solved automatically:  nipkow@10159  327 *};  nipkow@9958  328 nipkow@10159  329  apply(auto dest:not_in_lfp_afD);  nipkow@10159  330 done;  nipkow@9958  331 nipkow@10159  332 text{*  nipkow@10217  333 If you found the above proofs somewhat complicated we recommend you read  nipkow@10217  334 \S\ref{sec:CTL-revisited} where we shown how inductive definitions lead to  nipkow@10217  335 simpler arguments.  nipkow@10217  336 nipkow@10217  337 The main theorem is proved as for PDL, except that we also derive the  nipkow@10217  338 necessary equality @{text"lfp(af A) = ..."} by combining  nipkow@10217  339 @{thm[source]AF_lemma1} and @{thm[source]AF_lemma2} on the spot:  nipkow@10159  340 *}  nipkow@10159  341 nipkow@10159  342 theorem "mc f = {s. s \ f}";  nipkow@10159  343 apply(induct_tac f);  nipkow@10159  344 apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2]);  nipkow@10159  345 done  nipkow@10159  346 nipkow@10159  347 text{*  nipkow@10281  348 nipkow@10171  349 The above language is not quite CTL. The latter also includes an  nipkow@10281  350 until-operator @{term"EU f g"} with semantics there exist a path  nipkow@10281  351 where @{term f} is true until @{term g} becomes true''. With the help  nipkow@10281  352 of an auxiliary function  nipkow@10281  353 *}  nipkow@10281  354 nipkow@10281  355 consts until:: "state set \ state set \ state \ state list \ bool"  nipkow@10281  356 primrec  nipkow@10281  357 "until A B s [] = (s \ B)"  nipkow@10281  358 "until A B s (t#p) = (s \ A \ (s,t) \ M \ until A B t p)"  nipkow@10281  359 (*<*)constdefs  nipkow@10281  360  eusem :: "state set \ state set \ state set"  nipkow@10281  361 "eusem A B \ {s. \p. until A B s p}"(*>*)  nipkow@10281  362 nipkow@10281  363 text{*\noindent  nipkow@10281  364 the semantics of @{term EU} is straightforward:  nipkow@10281  365 @{text[display]"s \ EU f g = (\p. until A B s p)"}  nipkow@10281  366 Note that @{term EU} is not definable in terms of the other operators!  nipkow@10281  367 nipkow@10281  368 Model checking @{term EU} is again a least fixed point construction:  nipkow@10281  369 @{text[display]"mc(EU f g) = lfp(\T. mc g \ mc f \ (M^-1 ^^ T))"}  nipkow@10281  370 nipkow@10171  371 \begin{exercise}  nipkow@10281  372 Extend the datatype of formulae by the above until operator  nipkow@10281  373 and prove the equivalence between semantics and model checking, i.e.\ that  nipkow@10186  374 @{prop[display]"mc(EU f g) = {s. s \ EU f g}"}  nipkow@10186  375 %For readability you may want to annotate {term EU} with its customary syntax  nipkow@10186  376 %{text[display]"| EU formula formula E[_ U _]"}  nipkow@10186  377 %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.  nipkow@10186  378 \end{exercise}  nipkow@10281  379 For more CTL exercises see, for example, \cite{Huth-Ryan-book}.  nipkow@10281  380 *}  nipkow@10281  381 nipkow@10281  382 (*<*)  nipkow@10281  383 constdefs  nipkow@10281  384  eufix :: "state set \ state set \ state set \ state set"  nipkow@10281  385 "eufix A B T \ B \ A \ (M^-1 ^^ T)"  nipkow@10281  386 nipkow@10281  387 lemma "lfp(eufix A B) \ eusem A B"  nipkow@10281  388 apply(rule lfp_lowerbound)  nipkow@10281  389 apply(clarsimp simp add:eusem_def eufix_def);  nipkow@10281  390 apply(erule disjE);  nipkow@10281  391  apply(rule_tac x = "[]" in exI);  nipkow@10281  392  apply simp  nipkow@10281  393 apply(clarsimp);  nipkow@10281  394 apply(rule_tac x = "y#xc" in exI);  nipkow@10281  395 apply simp;  nipkow@10281  396 done  nipkow@10281  397 nipkow@10281  398 lemma mono_eufix: "mono(eufix A B)";  nipkow@10281  399 apply(simp add: mono_def eufix_def);  nipkow@10281  400 apply blast;  nipkow@10281  401 done  nipkow@10281  402 nipkow@10281  403 lemma "eusem A B \ lfp(eufix A B)";  nipkow@10281  404 apply(clarsimp simp add:eusem_def);  nipkow@10281  405 apply(erule rev_mp);  nipkow@10281  406 apply(rule_tac x = x in spec);  nipkow@10281  407 apply(induct_tac p);  nipkow@10281  408  apply(rule ssubst[OF lfp_unfold[OF mono_eufix]]);  nipkow@10281  409  apply(simp add:eufix_def);  nipkow@10281  410 apply(clarsimp);  nipkow@10281  411 apply(rule ssubst[OF lfp_unfold[OF mono_eufix]]);  nipkow@10281  412 apply(simp add:eufix_def);  nipkow@10281  413 apply blast;  nipkow@10281  414 done  nipkow@10178  415 nipkow@10281  416 (*  nipkow@10281  417 constdefs  nipkow@10281  418  eusem :: "state set \ state set \ state set"  nipkow@10281  419 "eusem A B \ {s. \p\Paths s. \j. p j \ B \ (\i < j. p i \ A)}"  nipkow@10281  420 nipkow@10281  421 axioms  nipkow@10281  422 M_total: "\t. (s,t) \ M"  nipkow@10281  423 nipkow@10281  424 consts apath :: "state \ (nat \ state)"  nipkow@10281  425 primrec  nipkow@10281  426 "apath s 0 = s"  nipkow@10281  427 "apath s (Suc i) = (SOME t. (apath s i,t) \ M)"  nipkow@10281  428 nipkow@10281  429 lemma [iff]: "apath s \ Paths s";  nipkow@10281  430 apply(simp add:Paths_def);  nipkow@10281  431 apply(blast intro: M_total[THEN someI_ex])  nipkow@10281  432 done  nipkow@10281  433 nipkow@10281  434 constdefs  nipkow@10281  435  pcons :: "state \ (nat \ state) \ (nat \ state)"  nipkow@10281  436 "pcons s p == \i. case i of 0 \ s | Suc j \ p j"  nipkow@10281  437 nipkow@10281  438 lemma pcons_PathI: "[| (s,t) : M; p \ Paths t |] ==> pcons s p \ Paths s";  nipkow@10281  439 by(simp add:Paths_def pcons_def split:nat.split);  nipkow@10281  440 nipkow@10281  441 lemma "lfp(eufix A B) \ eusem A B"  nipkow@10281  442 apply(rule lfp_lowerbound)  nipkow@10281  443 apply(clarsimp simp add:eusem_def eufix_def);  nipkow@10281  444 apply(erule disjE);  nipkow@10281  445  apply(rule_tac x = "apath x" in bexI);  nipkow@10281  446  apply(rule_tac x = 0 in exI);  nipkow@10281  447  apply simp;  nipkow@10281  448  apply simp;  nipkow@10281  449 apply(clarify);  nipkow@10281  450 apply(rule_tac x = "pcons xb p" in bexI);  nipkow@10281  451  apply(rule_tac x = "j+1" in exI);  nipkow@10281  452  apply (simp add:pcons_def split:nat.split);  nipkow@10281  453 apply (simp add:pcons_PathI)  nipkow@10281  454 done  nipkow@10281  455 *)  nipkow@10281  456 (*>*)  nipkow@10281  457 text{*  nipkow@10186  458 Let us close this section with a few words about the executability of our model checkers.  nipkow@10159  459 It is clear that if all sets are finite, they can be represented as lists and the usual  nipkow@10159  460 set operations are easily implemented. Only @{term lfp} requires a little thought.  nipkow@10159  461 Fortunately the HOL library proves that in the case of finite sets and a monotone @{term F},  nipkow@10159  462 @{term"lfp F"} can be computed by iterated application of @{term F} to @{term"{}"} until  nipkow@10242  463 a fixed point is reached. It is actually possible to generate executable functional programs  nipkow@10159  464 from HOL definitions, but that is beyond the scope of the tutorial.  nipkow@10159  465 *}  nipkow@10212  466 (*<*)end(*>*)