src/Doc/Tutorial/CTL/CTL.thy
 author wenzelm Sat Nov 01 14:20:38 2014 +0100 (2014-11-01) changeset 58860 fee7cfa69c50 parent 58620 7435b6a3f72e child 67406 23307fd33906 permissions -rw-r--r--
eliminated spurious semicolons;
     1 (*<*)theory CTL imports Base begin(*>*)

     2

     3 subsection{*Computation Tree Logic --- CTL*}

     4

     5 text{*\label{sec:CTL}

     6 \index{CTL|(}%

     7 The semantics of PDL only needs reflexive transitive closure.

     8 Let us be adventurous and introduce a more expressive temporal operator.

     9 We extend the datatype

    10 @{text formula} by a new constructor

    11 *}

    12 (*<*)

    13 datatype formula = Atom "atom"

    14                   | Neg formula

    15                   | And formula formula

    16                   | AX formula

    17                   | EF formula(*>*)

    18                   | AF formula

    19

    20 text{*\noindent

    21 which stands for \emph{A}lways in the \emph{F}uture'':

    22 on all infinite paths, at some point the formula holds.

    23 Formalizing the notion of an infinite path is easy

    24 in HOL: it is simply a function from @{typ nat} to @{typ state}.

    25 *}

    26

    27 definition Paths :: "state \<Rightarrow> (nat \<Rightarrow> state)set" where

    28 "Paths s \<equiv> {p. s = p 0 \<and> (\<forall>i. (p i, p(i+1)) \<in> M)}"

    29

    30 text{*\noindent

    31 This definition allows a succinct statement of the semantics of @{const AF}:

    32 \footnote{Do not be misled: neither datatypes nor recursive functions can be

    33 extended by new constructors or equations. This is just a trick of the

    34 presentation (see \S\ref{sec:doc-prep-suppress}). In reality one has to define

    35 a new datatype and a new function.}

    36 *}

    37 (*<*)

    38 primrec valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80) where

    39 "s \<Turnstile> Atom a  =  (a \<in> L s)" |

    40 "s \<Turnstile> Neg f   = (~(s \<Turnstile> f))" |

    41 "s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)" |

    42 "s \<Turnstile> AX f    = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)" |

    43 "s \<Turnstile> EF f    = (\<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<Turnstile> f)" |

    44 (*>*)

    45 "s \<Turnstile> AF f    = (\<forall>p \<in> Paths s. \<exists>i. p i \<Turnstile> f)"

    46

    47 text{*\noindent

    48 Model checking @{const AF} involves a function which

    49 is just complicated enough to warrant a separate definition:

    50 *}

    51

    52 definition af :: "state set \<Rightarrow> state set \<Rightarrow> state set" where

    53 "af A T \<equiv> A \<union> {s. \<forall>t. (s, t) \<in> M \<longrightarrow> t \<in> T}"

    54

    55 text{*\noindent

    56 Now we define @{term "mc(AF f)"} as the least set @{term T} that includes

    57 @{term"mc f"} and all states all of whose direct successors are in @{term T}:

    58 *}

    59 (*<*)

    60 primrec mc :: "formula \<Rightarrow> state set" where

    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\<inverse>  T)"|(*>*)

    66 "mc(AF f)    = lfp(af(mc f))"

    67

    68 text{*\noindent

    69 Because @{const 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\<inverse>  T)"

    79 apply(rule monoI)

    80 by(blast)

    81

    82 lemma EF_lemma:

    83   "lfp(\<lambda>T. A \<union> M\<inverse>  T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}"

    84 apply(rule equalityI)

    85  apply(rule subsetI)

    86  apply(simp)

    87  apply(erule lfp_induct_set)

    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(subst lfp_unfold[OF mono_ef])

    95  apply(blast)

    96 apply(subst lfp_unfold[OF mono_ef])

    97 by(blast)

    98 (*>*)

    99 text{*

   100 All we need to prove now is  @{prop"mc(AF f) = {s. s \<Turnstile> AF f}"}, which states

   101 that @{term mc} and @{text"\<Turnstile>"} agree for @{const AF}\@.

   102 This time we prove the two inclusions separately, starting

   103 with the easy one:

   104 *}

   105

   106 theorem AF_lemma1: "lfp(af A) \<subseteq> {s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A}"

   107

   108 txt{*\noindent

   109 In contrast to the analogous proof for @{const EF}, and just

   110 for a change, we do not use fixed point induction.  Park-induction,

   111 named after David Park, is weaker but sufficient for this proof:

   112 \begin{center}

   113 @{thm lfp_lowerbound[of _ "S",no_vars]} \hfill (@{thm[source]lfp_lowerbound})

   114 \end{center}

   115 The instance of the premise @{prop"f S \<subseteq> S"} is proved pointwise,

   116 a decision that \isa{auto} takes for us:

   117 *}

   118 apply(rule lfp_lowerbound)

   119 apply(auto simp add: af_def Paths_def)

   120

   121 txt{*

   122 @{subgoals[display,indent=0,margin=70,goals_limit=1]}

   123 In this remaining case, we set @{term t} to @{term"p(1::nat)"}.

   124 The rest is automatic, which is surprising because it involves

   125 finding the instantiation @{term"\<lambda>i::nat. p(i+1)"}

   126 for @{text"\<forall>p"}.

   127 *}

   128

   129 apply(erule_tac x = "p 1" in allE)

   130 apply(auto)

   131 done

   132

   133

   134 text{*

   135 The opposite inclusion is proved by contradiction: if some state

   136 @{term s} is not in @{term"lfp(af A)"}, then we can construct an

   137 infinite @{term A}-avoiding path starting from~@{term s}. The reason is

   138 that by unfolding @{const lfp} we find that if @{term s} is not in

   139 @{term"lfp(af A)"}, then @{term s} is not in @{term A} and there is a

   140 direct successor of @{term s} that is again not in \mbox{@{term"lfp(af

   141 A)"}}. Iterating this argument yields the promised infinite

   142 @{term A}-avoiding path. Let us formalize this sketch.

   143

   144 The one-step argument in the sketch above

   145 is proved by a variant of contraposition:

   146 *}

   147

   148 lemma not_in_lfp_afD:

   149  "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t) \<in> M \<and> t \<notin> lfp(af A))"

   150 apply(erule contrapos_np)

   151 apply(subst lfp_unfold[OF mono_af])

   152 apply(simp add: af_def)

   153 done

   154

   155 text{*\noindent

   156 We assume the negation of the conclusion and prove @{term"s : lfp(af A)"}.

   157 Unfolding @{const lfp} once and

   158 simplifying with the definition of @{const af} finishes the proof.

   159

   160 Now we iterate this process. The following construction of the desired

   161 path is parameterized by a predicate @{term Q} that should hold along the path:

   162 *}

   163

   164 primrec path :: "state \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> (nat \<Rightarrow> state)" where

   165 "path s Q 0 = s" |

   166 "path s Q (Suc n) = (SOME t. (path s Q n,t) \<in> M \<and> Q t)"

   167

   168 text{*\noindent

   169 Element @{term"n+1::nat"} on this path is some arbitrary successor

   170 @{term t} of element @{term n} such that @{term"Q t"} holds.  Remember that @{text"SOME t. R t"}

   171 is some arbitrary but fixed @{term t} such that @{prop"R t"} holds (see \S\ref{sec:SOME}). Of

   172 course, such a @{term t} need not exist, but that is of no

   173 concern to us since we will only use @{const path} when a

   174 suitable @{term t} does exist.

   175

   176 Let us show that if each state @{term s} that satisfies @{term Q}

   177 has a successor that again satisfies @{term Q}, then there exists an infinite @{term Q}-path:

   178 *}

   179

   180 lemma infinity_lemma:

   181   "\<lbrakk> Q s; \<forall>s. Q s \<longrightarrow> (\<exists> t. (s,t) \<in> M \<and> Q t) \<rbrakk> \<Longrightarrow>

   182    \<exists>p\<in>Paths s. \<forall>i. Q(p i)"

   183

   184 txt{*\noindent

   185 First we rephrase the conclusion slightly because we need to prove simultaneously

   186 both the path property and the fact that @{term Q} holds:

   187 *}

   188

   189 apply(subgoal_tac

   190   "\<exists>p. s = p 0 \<and> (\<forall>i::nat. (p i, p(i+1)) \<in> M \<and> Q(p i))")

   191

   192 txt{*\noindent

   193 From this proposition the original goal follows easily:

   194 *}

   195

   196  apply(simp add: Paths_def, blast)

   197

   198 txt{*\noindent

   199 The new subgoal is proved by providing the witness @{term "path s Q"} for @{term p}:

   200 *}

   201

   202 apply(rule_tac x = "path s Q" in exI)

   203 apply(clarsimp)

   204

   205 txt{*\noindent

   206 After simplification and clarification, the subgoal has the following form:

   207 @{subgoals[display,indent=0,margin=70,goals_limit=1]}

   208 It invites a proof by induction on @{term i}:

   209 *}

   210

   211 apply(induct_tac i)

   212  apply(simp)

   213

   214 txt{*\noindent

   215 After simplification, the base case boils down to

   216 @{subgoals[display,indent=0,margin=70,goals_limit=1]}

   217 The conclusion looks exceedingly trivial: after all, @{term t} is chosen such that @{prop"(s,t):M"}

   218 holds. However, we first have to show that such a @{term t} actually exists! This reasoning

   219 is embodied in the theorem @{thm[source]someI2_ex}:

   220 @{thm[display,eta_contract=false]someI2_ex}

   221 When we apply this theorem as an introduction rule, @{text"?P x"} becomes

   222 @{prop"(s, x) : M & Q x"} and @{text"?Q x"} becomes @{prop"(s,x) : M"} and we have to prove

   223 two subgoals: @{prop"EX a. (s, a) : M & Q a"}, which follows from the assumptions, and

   224 @{prop"(s, x) : M & Q x ==> (s,x) : M"}, which is trivial. Thus it is not surprising that

   225 @{text fast} can prove the base case quickly:

   226 *}

   227

   228  apply(fast intro: someI2_ex)

   229

   230 txt{*\noindent

   231 What is worth noting here is that we have used \methdx{fast} rather than

   232 @{text blast}.  The reason is that @{text blast} would fail because it cannot

   233 cope with @{thm[source]someI2_ex}: unifying its conclusion with the current

   234 subgoal is non-trivial because of the nested schematic variables. For

   235 efficiency reasons @{text blast} does not even attempt such unifications.

   236 Although @{text fast} can in principle cope with complicated unification

   237 problems, in practice the number of unifiers arising is often prohibitive and

   238 the offending rule may need to be applied explicitly rather than

   239 automatically. This is what happens in the step case.

   240

   241 The induction step is similar, but more involved, because now we face nested

   242 occurrences of @{text SOME}. As a result, @{text fast} is no longer able to

   243 solve the subgoal and we apply @{thm[source]someI2_ex} by hand.  We merely

   244 show the proof commands but do not describe the details:

   245 *}

   246

   247 apply(simp)

   248 apply(rule someI2_ex)

   249  apply(blast)

   250 apply(rule someI2_ex)

   251  apply(blast)

   252 apply(blast)

   253 done

   254

   255 text{*

   256 Function @{const path} has fulfilled its purpose now and can be forgotten.

   257 It was merely defined to provide the witness in the proof of the

   258 @{thm[source]infinity_lemma}. Aficionados of minimal proofs might like to know

   259 that we could have given the witness without having to define a new function:

   260 the term

   261 @{term[display]"rec_nat s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)"}

   262 is extensionally equal to @{term"path s Q"},

   263 where @{term rec_nat} is the predefined primitive recursor on @{typ nat}.

   264 *}

   265 (*<*)

   266 lemma

   267 "\<lbrakk> Q s; \<forall> s. Q s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> Q t) \<rbrakk> \<Longrightarrow>

   268  \<exists> p\<in>Paths s. \<forall> i. Q(p i)"

   269 apply(subgoal_tac

   270  "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> Q(p i))")

   271  apply(simp add: Paths_def)

   272  apply(blast)

   273 apply(rule_tac x = "rec_nat s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)" in exI)

   274 apply(simp)

   275 apply(intro strip)

   276 apply(induct_tac i)

   277  apply(simp)

   278  apply(fast intro: someI2_ex)

   279 apply(simp)

   280 apply(rule someI2_ex)

   281  apply(blast)

   282 apply(rule someI2_ex)

   283  apply(blast)

   284 by(blast)

   285 (*>*)

   286

   287 text{*

   288 At last we can prove the opposite direction of @{thm[source]AF_lemma1}:

   289 *}

   290

   291 theorem AF_lemma2: "{s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A} \<subseteq> lfp(af A)"

   292

   293 txt{*\noindent

   294 The proof is again pointwise and then by contraposition:

   295 *}

   296

   297 apply(rule subsetI)

   298 apply(erule contrapos_pp)

   299 apply simp

   300

   301 txt{*

   302 @{subgoals[display,indent=0,goals_limit=1]}

   303 Applying the @{thm[source]infinity_lemma} as a destruction rule leaves two subgoals, the second

   304 premise of @{thm[source]infinity_lemma} and the original subgoal:

   305 *}

   306

   307 apply(drule infinity_lemma)

   308

   309 txt{*

   310 @{subgoals[display,indent=0,margin=65]}

   311 Both are solved automatically:

   312 *}

   313

   314  apply(auto dest: not_in_lfp_afD)

   315 done

   316

   317 text{*

   318 If you find these proofs too complicated, we recommend that you read

   319 \S\ref{sec:CTL-revisited}, where we show how inductive definitions lead to

   320 simpler arguments.

   321

   322 The main theorem is proved as for PDL, except that we also derive the

   323 necessary equality @{text"lfp(af A) = ..."} by combining

   324 @{thm[source]AF_lemma1} and @{thm[source]AF_lemma2} on the spot:

   325 *}

   326

   327 theorem "mc f = {s. s \<Turnstile> f}"

   328 apply(induct_tac f)

   329 apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2])

   330 done

   331

   332 text{*

   333

   334 The language defined above is not quite CTL\@. The latter also includes an

   335 until-operator @{term"EU f g"} with semantics there \emph{E}xists a path

   336 where @{term f} is true \emph{U}ntil @{term g} becomes true''.  We need

   337 an auxiliary function:

   338 *}

   339

   340 primrec

   341 until:: "state set \<Rightarrow> state set \<Rightarrow> state \<Rightarrow> state list \<Rightarrow> bool" where

   342 "until A B s []    = (s \<in> B)" |

   343 "until A B s (t#p) = (s \<in> A \<and> (s,t) \<in> M \<and> until A B t p)"

   344 (*<*)definition

   345  eusem :: "state set \<Rightarrow> state set \<Rightarrow> state set" where

   346 "eusem A B \<equiv> {s. \<exists>p. until A B s p}"(*>*)

   347

   348 text{*\noindent

   349 Expressing the semantics of @{term EU} is now straightforward:

   350 @{prop[display]"s \<Turnstile> EU f g = (\<exists>p. until {t. t \<Turnstile> f} {t. t \<Turnstile> g} s p)"}

   351 Note that @{term EU} is not definable in terms of the other operators!

   352

   353 Model checking @{term EU} is again a least fixed point construction:

   354 @{text[display]"mc(EU f g) = lfp(\<lambda>T. mc g \<union> mc f \<inter> (M\<inverse>  T))"}

   355

   356 \begin{exercise}

   357 Extend the datatype of formulae by the above until operator

   358 and prove the equivalence between semantics and model checking, i.e.\ that

   359 @{prop[display]"mc(EU f g) = {s. s \<Turnstile> EU f g}"}

   360 %For readability you may want to annotate {term EU} with its customary syntax

   361 %{text[display]"| EU formula formula    E[_ U _]"}

   362 %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.

   363 \end{exercise}

   364 For more CTL exercises see, for example, Huth and Ryan @{cite "Huth-Ryan-book"}.

   365 *}

   366

   367 (*<*)

   368 definition eufix :: "state set \<Rightarrow> state set \<Rightarrow> state set \<Rightarrow> state set" where

   369 "eufix A B T \<equiv> B \<union> A \<inter> (M\<inverse>  T)"

   370

   371 lemma "lfp(eufix A B) \<subseteq> eusem A B"

   372 apply(rule lfp_lowerbound)

   373 apply(auto simp add: eusem_def eufix_def)

   374  apply(rule_tac x = "[]" in exI)

   375  apply simp

   376 apply(rule_tac x = "xa#xb" in exI)

   377 apply simp

   378 done

   379

   380 lemma mono_eufix: "mono(eufix A B)"

   381 apply(simp add: mono_def eufix_def)

   382 apply blast

   383 done

   384

   385 lemma "eusem A B \<subseteq> lfp(eufix A B)"

   386 apply(clarsimp simp add: eusem_def)

   387 apply(erule rev_mp)

   388 apply(rule_tac x = x in spec)

   389 apply(induct_tac p)

   390  apply(subst lfp_unfold[OF mono_eufix])

   391  apply(simp add: eufix_def)

   392 apply(clarsimp)

   393 apply(subst lfp_unfold[OF mono_eufix])

   394 apply(simp add: eufix_def)

   395 apply blast

   396 done

   397

   398 (*

   399 definition eusem :: "state set \<Rightarrow> state set \<Rightarrow> state set" where

   400 "eusem A B \<equiv> {s. \<exists>p\<in>Paths s. \<exists>j. p j \<in> B \<and> (\<forall>i < j. p i \<in> A)}"

   401

   402 axiomatization where

   403 M_total: "\<exists>t. (s,t) \<in> M"

   404

   405 consts apath :: "state \<Rightarrow> (nat \<Rightarrow> state)"

   406 primrec

   407 "apath s 0 = s"

   408 "apath s (Suc i) = (SOME t. (apath s i,t) \<in> M)"

   409

   410 lemma [iff]: "apath s \<in> Paths s";

   411 apply(simp add: Paths_def);

   412 apply(blast intro: M_total[THEN someI_ex])

   413 done

   414

   415 definition pcons :: "state \<Rightarrow> (nat \<Rightarrow> state) \<Rightarrow> (nat \<Rightarrow> state)" where

   416 "pcons s p == \<lambda>i. case i of 0 \<Rightarrow> s | Suc j \<Rightarrow> p j"

   417

   418 lemma pcons_PathI: "[| (s,t) : M; p \<in> Paths t |] ==> pcons s p \<in> Paths s";

   419 by(simp add: Paths_def pcons_def split: nat.split);

   420

   421 lemma "lfp(eufix A B) \<subseteq> eusem A B"

   422 apply(rule lfp_lowerbound)

   423 apply(clarsimp simp add: eusem_def eufix_def);

   424 apply(erule disjE);

   425  apply(rule_tac x = "apath x" in bexI);

   426   apply(rule_tac x = 0 in exI);

   427   apply simp;

   428  apply simp;

   429 apply(clarify);

   430 apply(rule_tac x = "pcons xb p" in bexI);

   431  apply(rule_tac x = "j+1" in exI);

   432  apply (simp add: pcons_def split: nat.split);

   433 apply (simp add: pcons_PathI)

   434 done

   435 *)

   436 (*>*)

   437

   438 text{* Let us close this section with a few words about the executability of

   439 our model checkers.  It is clear that if all sets are finite, they can be

   440 represented as lists and the usual set operations are easily

   441 implemented. Only @{const lfp} requires a little thought.  Fortunately, theory

   442 @{text While_Combinator} in the Library~@{cite "HOL-Library"} provides a

   443 theorem stating that in the case of finite sets and a monotone

   444 function~@{term F}, the value of \mbox{@{term"lfp F"}} can be computed by

   445 iterated application of @{term F} to~@{term"{}"} until a fixed point is

   446 reached. It is actually possible to generate executable functional programs

   447 from HOL definitions, but that is beyond the scope of the tutorial.%

   448 \index{CTL|)} *}

   449 (*<*)end(*>*)