doc-src/TutorialI/CTL/document/CTL.tex
author nipkow
Fri Oct 13 18:02:08 2000 +0200 (2000-10-13)
changeset 10217 e61e7e1eacaf
parent 10212 33fe2d701ddd
child 10225 b9fd52525b69
permissions -rw-r--r--
*** empty log message ***
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{CTL}%
     4 %
     5 \isamarkupsubsection{Computation tree logic---CTL}
     6 %
     7 \begin{isamarkuptext}%
     8 \label{sec:CTL}
     9 The semantics of PDL only needs transitive reflexive closure.
    10 Let us now be a bit more adventurous and introduce a new temporal operator
    11 that goes beyond transitive reflexive closure. We extend the datatype
    12 \isa{formula} by a new constructor%
    13 \end{isamarkuptext}%
    14 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AF\ formula%
    15 \begin{isamarkuptext}%
    16 \noindent
    17 which stands for "always in the future":
    18 on all paths, at some point the formula holds. Formalizing the notion of an infinite path is easy
    19 in HOL: it is simply a function from \isa{nat} to \isa{state}.%
    20 \end{isamarkuptext}%
    21 \isacommand{constdefs}\ Paths\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}set{\isachardoublequote}\isanewline
    22 \ \ \ \ \ \ \ \ \ {\isachardoublequote}Paths\ s\ {\isasymequiv}\ {\isacharbraceleft}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}{\isacharbraceright}{\isachardoublequote}%
    23 \begin{isamarkuptext}%
    24 \noindent
    25 This definition allows a very succinct statement of the semantics of \isa{AF}:
    26 \footnote{Do not be mislead: neither datatypes nor recursive functions can be
    27 extended by new constructors or equations. This is just a trick of the
    28 presentation. In reality one has to define a new datatype and a new function.}%
    29 \end{isamarkuptext}%
    30 {\isachardoublequote}s\ {\isasymTurnstile}\ AF\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequote}%
    31 \begin{isamarkuptext}%
    32 \noindent
    33 Model checking \isa{AF} involves a function which
    34 is just complicated enough to warrant a separate definition:%
    35 \end{isamarkuptext}%
    36 \isacommand{constdefs}\ af\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline
    37 \ \ \ \ \ \ \ \ \ {\isachardoublequote}af\ A\ T\ {\isasymequiv}\ A\ {\isasymunion}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\ t\ {\isasymin}\ T{\isacharbraceright}{\isachardoublequote}%
    38 \begin{isamarkuptext}%
    39 \noindent
    40 Now we define \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}} as the least set \isa{T} that contains
    41 \isa{mc\ f} and all states all of whose direct successors are in \isa{T}:%
    42 \end{isamarkuptext}%
    43 {\isachardoublequote}mc{\isacharparenleft}AF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}af{\isacharparenleft}mc\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
    44 \begin{isamarkuptext}%
    45 \noindent
    46 Because \isa{af} is monotone in its second argument (and also its first, but
    47 that is irrelevant) \isa{af\ A} has a least fixpoint:%
    48 \end{isamarkuptext}%
    49 \isacommand{lemma}\ mono{\isacharunderscore}af{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
    50 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ mono{\isacharunderscore}def\ af{\isacharunderscore}def{\isacharparenright}\isanewline
    51 \isacommand{apply}\ blast\isanewline
    52 \isacommand{done}%
    53 \begin{isamarkuptext}%
    54 All we need to prove now is that \isa{mc} and \isa{{\isasymTurnstile}}
    55 agree for \isa{AF}, i.e.\ that \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ AF\ f{\isacharbraceright}}. This time we prove the two containments separately, starting
    56 with the easy one:%
    57 \end{isamarkuptext}%
    58 \isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{1}}{\isacharcolon}\isanewline
    59 \ \ {\isachardoublequote}lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}%
    60 \begin{isamarkuptxt}%
    61 \noindent
    62 The proof is again pointwise. Fixpoint induction on the premise \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} followed
    63 by simplification and clarification%
    64 \end{isamarkuptxt}%
    65 \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
    66 \isacommand{apply}{\isacharparenleft}erule\ lfp{\isacharunderscore}induct{\isacharbrackleft}OF\ {\isacharunderscore}\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline
    67 \isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}%
    68 \begin{isamarkuptxt}%
    69 \noindent
    70 leads to the following somewhat involved proof state
    71 \begin{isabelle}
    72 \ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline
    73 \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ \isadigit{0}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
    74 \ \ \ \ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymand}\isanewline
    75 \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\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
    76 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
    77 \ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
    78 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A
    79 \end{isabelle}
    80 Now we eliminate the disjunction. The case \isa{p\ {\isadigit{0}}\ {\isasymin}\ A} is trivial:%
    81 \end{isamarkuptxt}%
    82 \isacommand{apply}{\isacharparenleft}erule\ disjE{\isacharparenright}\isanewline
    83 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}%
    84 \begin{isamarkuptxt}%
    85 \noindent
    86 In the other case we set \isa{t} to \isa{p\ {\isadigit{1}}} and simplify matters:%
    87 \end{isamarkuptxt}%
    88 \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ {\isadigit{1}}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
    89 \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
    90 \begin{isamarkuptxt}%
    91 \begin{isabelle}
    92 \ \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
    93 \ \ \ \ \ \ \ \ \ \ \ {\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
    94 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
    95 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A
    96 \end{isabelle}
    97 It merely remains to set \isa{pa} to \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}}, i.e.\ \isa{p} without its
    98 first element. The rest is practically automatic:%
    99 \end{isamarkuptxt}%
   100 \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
   101 \isacommand{apply}\ simp\isanewline
   102 \isacommand{apply}\ blast\isanewline
   103 \isacommand{done}%
   104 \begin{isamarkuptext}%
   105 The opposite containment is proved by contradiction: if some state
   106 \isa{s} is not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then we can construct an
   107 infinite \isa{A}-avoiding path starting from \isa{s}. The reason is
   108 that by unfolding \isa{lfp} we find that if \isa{s} is not in
   109 \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then \isa{s} is not in \isa{A} and there is a
   110 direct successor of \isa{s} that is again not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Iterating this argument yields the promised infinite
   111 \isa{A}-avoiding path. Let us formalize this sketch.
   112 
   113 The one-step argument in the above sketch%
   114 \end{isamarkuptext}%
   115 \isacommand{lemma}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharcolon}\isanewline
   116 \ {\isachardoublequote}s\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ s\ {\isasymnotin}\ A\ {\isasymand}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}{\isasymin}M\ {\isasymand}\ t\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
   117 \isacommand{apply}{\isacharparenleft}erule\ swap{\isacharparenright}\isanewline
   118 \isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline
   119 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\isacharparenright}\isanewline
   120 \isacommand{done}%
   121 \begin{isamarkuptext}%
   122 \noindent
   123 is proved by a variant of contraposition (\isa{swap}:
   124 \isa{{\isasymlbrakk}{\isasymnot}\ Q{\isacharsemicolon}\ {\isasymnot}\ P\ {\isasymLongrightarrow}\ Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ P}), i.e.\ assuming the negation of the conclusion
   125 and proving \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Unfolding \isa{lfp} once and
   126 simplifying with the definition of \isa{af} finishes the proof.
   127 
   128 Now we iterate this process. The following construction of the desired
   129 path is parameterized by a predicate \isa{P} that should hold along the path:%
   130 \end{isamarkuptext}%
   131 \isacommand{consts}\ path\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}state\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}{\isachardoublequote}\isanewline
   132 \isacommand{primrec}\isanewline
   133 {\isachardoublequote}path\ s\ P\ {\isadigit{0}}\ {\isacharequal}\ s{\isachardoublequote}\isanewline
   134 {\isachardoublequote}path\ s\ P\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ P\ n{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isachardoublequote}%
   135 \begin{isamarkuptext}%
   136 \noindent
   137 Element \isa{n\ {\isacharplus}\ {\isadigit{1}}} on this path is some arbitrary successor
   138 \isa{t} of element \isa{n} such that \isa{P\ t} holds.  Remember that \isa{SOME\ t{\isachardot}\ R\ t}
   139 is some arbitrary but fixed \isa{t} such that \isa{R\ t} holds (see \S\ref{sec-SOME}). Of
   140 course, such a \isa{t} may in general not exist, but that is of no
   141 concern to us since we will only use \isa{path} in such cases where a
   142 suitable \isa{t} does exist.
   143 
   144 Let us show that if each state \isa{s} that satisfies \isa{P}
   145 has a successor that again satisfies \isa{P}, then there exists an infinite \isa{P}-path:%
   146 \end{isamarkuptext}%
   147 \isacommand{lemma}\ infinity{\isacharunderscore}lemma{\isacharcolon}\isanewline
   148 \ \ {\isachardoublequote}{\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}\ {\isasymLongrightarrow}\isanewline
   149 \ \ \ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}%
   150 \begin{isamarkuptxt}%
   151 \noindent
   152 First we rephrase the conclusion slightly because we need to prove both the path property
   153 and the fact that \isa{P} holds simultaneously:%
   154 \end{isamarkuptxt}%
   155 \isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}{\isasymexists}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}%
   156 \begin{isamarkuptxt}%
   157 \noindent
   158 From this proposition the original goal follows easily:%
   159 \end{isamarkuptxt}%
   160 \ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}%
   161 \begin{isamarkuptxt}%
   162 \noindent
   163 The new subgoal is proved by providing the witness \isa{path\ s\ P} for \isa{p}:%
   164 \end{isamarkuptxt}%
   165 \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}path\ s\ P{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
   166 \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
   167 \begin{isamarkuptxt}%
   168 \noindent
   169 After simplification and clarification the subgoal has the following compact form
   170 \begin{isabelle}
   171 \ \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
   172 \ \ \ \ \ \ \ \ {\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
   173 \ \ \ \ \ \ \ \ \ \ \ \ P\ {\isacharparenleft}path\ s\ P\ i{\isacharparenright}
   174 \end{isabelle}
   175 and invites a proof by induction on \isa{i}:%
   176 \end{isamarkuptxt}%
   177 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline
   178 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}%
   179 \begin{isamarkuptxt}%
   180 \noindent
   181 After simplification the base case boils down to
   182 \begin{isabelle}
   183 \ \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
   184 \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M
   185 \end{isabelle}
   186 The conclusion looks exceedingly trivial: after all, \isa{t} is chosen such that \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M}
   187 holds. However, we first have to show that such a \isa{t} actually exists! This reasoning
   188 is embodied in the theorem \isa{someI{\isadigit{2}}{\isacharunderscore}ex}:
   189 \begin{isabelle}%
   190 \ \ \ \ \ {\isasymlbrakk}{\isasymexists}a{\isachardot}\ {\isacharquery}P\ a{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharparenleft}SOME\ x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}%
   191 \end{isabelle}
   192 When we apply this theorem as an introduction rule, \isa{{\isacharquery}P\ x} becomes
   193 \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ x} and \isa{{\isacharquery}Q\ x} becomes \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M} and we have to prove
   194 two subgoals: \isa{{\isasymexists}a{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ a{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ a}, which follows from the assumptions, and
   195 \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ x\ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M}, which is trivial. Thus it is not surprising that
   196 \isa{fast} can prove the base case quickly:%
   197 \end{isamarkuptxt}%
   198 \ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}%
   199 \begin{isamarkuptxt}%
   200 \noindent
   201 What is worth noting here is that we have used \isa{fast} rather than
   202 \isa{blast}.  The reason is that \isa{blast} would fail because it cannot
   203 cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}: unifying its conclusion with the current
   204 subgoal is nontrivial because of the nested schematic variables. For
   205 efficiency reasons \isa{blast} does not even attempt such unifications.
   206 Although \isa{fast} can in principle cope with complicated unification
   207 problems, in practice the number of unifiers arising is often prohibitive and
   208 the offending rule may need to be applied explicitly rather than
   209 automatically. This is what happens in the step case.
   210 
   211 The induction step is similar, but more involved, because now we face nested
   212 occurrences of \isa{SOME}. As a result, \isa{fast} is no longer able to
   213 solve the subgoal and we apply \isa{someI{\isadigit{2}}{\isacharunderscore}ex} by hand.  We merely
   214 show the proof commands but do not describe the details:%
   215 \end{isamarkuptxt}%
   216 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   217 \isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline
   218 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   219 \isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline
   220 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   221 \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   222 \isacommand{done}%
   223 \begin{isamarkuptext}%
   224 Function \isa{path} has fulfilled its purpose now and can be forgotten
   225 about. It was merely defined to provide the witness in the proof of the
   226 \isa{infinity{\isacharunderscore}lemma}. Aficionados of minimal proofs might like to know
   227 that we could have given the witness without having to define a new function:
   228 the term
   229 \begin{isabelle}%
   230 \ \ \ \ \ nat{\isacharunderscore}rec\ s\ {\isacharparenleft}{\isasymlambda}n\ t{\isachardot}\ SOME\ u{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ u{\isacharparenright}%
   231 \end{isabelle}
   232 is extensionally equal to \isa{path\ s\ P},
   233 where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}, whose defining
   234 equations we omit.%
   235 \end{isamarkuptext}%
   236 %
   237 \begin{isamarkuptext}%
   238 At last we can prove the opposite direction of \isa{AF{\isacharunderscore}lemma{\isadigit{1}}}:%
   239 \end{isamarkuptext}%
   240 \isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\isanewline
   241 {\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}%
   242 \begin{isamarkuptxt}%
   243 \noindent
   244 The proof is again pointwise and then by contraposition (\isa{contrapos{\isadigit{2}}} is the rule
   245 \isa{{\isasymlbrakk}{\isacharquery}Q{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P\ {\isasymLongrightarrow}\ {\isasymnot}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P}):%
   246 \end{isamarkuptxt}%
   247 \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
   248 \isacommand{apply}{\isacharparenleft}erule\ contrapos{\isadigit{2}}{\isacharparenright}\isanewline
   249 \isacommand{apply}\ simp%
   250 \begin{isamarkuptxt}%
   251 \begin{isabelle}
   252 \ \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
   253 \end{isabelle}
   254 Applying the \isa{infinity{\isacharunderscore}lemma} as a destruction rule leaves two subgoals, the second
   255 premise of \isa{infinity{\isacharunderscore}lemma} and the original subgoal:%
   256 \end{isamarkuptxt}%
   257 \isacommand{apply}{\isacharparenleft}drule\ infinity{\isacharunderscore}lemma{\isacharparenright}%
   258 \begin{isamarkuptxt}%
   259 \begin{isabelle}
   260 \ \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
   261 \ \isadigit{2}{\isachardot}\ {\isasymAnd}s{\isachardot}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline
   262 \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A
   263 \end{isabelle}
   264 Both are solved automatically:%
   265 \end{isamarkuptxt}%
   266 \ \isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline
   267 \isacommand{done}%
   268 \begin{isamarkuptext}%
   269 If you found the above proofs somewhat complicated we recommend you read
   270 \S\ref{sec:CTL-revisited} where we shown how inductive definitions lead to
   271 simpler arguments.
   272 
   273 The main theorem is proved as for PDL, except that we also derive the
   274 necessary equality \isa{lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isacharequal}\ {\isachardot}{\isachardot}{\isachardot}} by combining
   275 \isa{AF{\isacharunderscore}lemma{\isadigit{1}}} and \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} on the spot:%
   276 \end{isamarkuptext}%
   277 \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline
   278 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
   279 \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma\ equalityI{\isacharbrackleft}OF\ AF{\isacharunderscore}lemma{\isadigit{1}}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharbrackright}{\isacharparenright}\isanewline
   280 \isacommand{done}%
   281 \begin{isamarkuptext}%
   282 The above language is not quite CTL. The latter also includes an
   283 until-operator, which is the subject of the following exercise.
   284 It is not definable in terms of the other operators!
   285 \begin{exercise}
   286 Extend the datatype of formulae by the binary until operator \isa{EU\ f\ g} with semantics
   287 ``there exist a path where \isa{f} is true until \isa{g} becomes true''
   288 \begin{isabelle}%
   289 \ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}j{\isachardot}\ p\ j\ {\isasymTurnstile}\ g\ {\isasymand}\ {\isacharparenleft}{\isasymexists}i\ {\isacharless}\ j{\isachardot}\ p\ i\ {\isasymTurnstile}\ f{\isacharparenright}{\isacharparenright}%
   290 \end{isabelle}
   291 and model checking algorithm
   292 \begin{isabelle}%
   293 \ \ \ \ \ mc{\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ g\ {\isasymunion}\ mc\ f\ {\isasyminter}\ {\isacharparenleft}M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isacharparenright}%
   294 \end{isabelle}
   295 Prove the equivalence between semantics and model checking, i.e.\ that
   296 \begin{isabelle}%
   297 \ \ \ \ \ mc\ {\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ EU\ f\ g{\isacharbraceright}%
   298 \end{isabelle}
   299 %For readability you may want to annotate {term EU} with its customary syntax
   300 %{text[display]"| EU formula formula    E[_ U _]"}
   301 %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
   302 \end{exercise}
   303 For more CTL exercises see, for example \cite{Huth-Ryan-book}.
   304 \bigskip
   305 
   306 Let us close this section with a few words about the executability of our model checkers.
   307 It is clear that if all sets are finite, they can be represented as lists and the usual
   308 set operations are easily implemented. Only \isa{lfp} requires a little thought.
   309 Fortunately the HOL library proves that in the case of finite sets and a monotone \isa{F},
   310 \isa{lfp\ F} can be computed by iterated application of \isa{F} to \isa{{\isacharbraceleft}{\isacharbraceright}} until
   311 a fixpoint is reached. It is actually possible to generate executable functional programs
   312 from HOL definitions, but that is beyond the scope of the tutorial.%
   313 \end{isamarkuptext}%
   314 \end{isabellebody}%
   315 %%% Local Variables:
   316 %%% mode: latex
   317 %%% TeX-master: "root"
   318 %%% End: