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