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