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(*>*)