doc-src/TutorialI/CTL/document/CTL.tex
author wenzelm
Thu Oct 12 18:09:06 2000 +0200 (2000-10-12)
changeset 10211 1bece7f35762
parent 10192 4c2584e23ade
child 10212 33fe2d701ddd
permissions -rw-r--r--
updated;
     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 \isa{blast}.
   201 The reason is that \isa{blast} would fail because it cannot cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}:
   202 unifying its conclusion with the current subgoal is nontrivial because of the nested schematic
   203 variables. For efficiency reasons \isa{blast} does not even attempt such unifications.
   204 Although \isa{fast} can in principle cope with complicated unification problems, in practice
   205 the number of unifiers arising is often prohibitive and the offending rule may need to be applied
   206 explicitly rather than automatically.
   207 
   208 The induction step is similar, but more involved, because now we face nested occurrences of
   209 \isa{SOME}. We merely show the proof commands but do not describe th details:%
   210 \end{isamarkuptxt}%
   211 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   212 \isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline
   213 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   214 \isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline
   215 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   216 \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   217 \isacommand{done}%
   218 \begin{isamarkuptext}%
   219 Function \isa{path} has fulfilled its purpose now and can be forgotten
   220 about. It was merely defined to provide the witness in the proof of the
   221 \isa{infinity{\isacharunderscore}lemma}. Aficionados of minimal proofs might like to know
   222 that we could have given the witness without having to define a new function:
   223 the term
   224 \begin{isabelle}%
   225 \ \ \ \ \ nat{\isacharunderscore}rec\ s\ {\isacharparenleft}{\isasymlambda}n\ t{\isachardot}\ SOME\ u{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ u{\isacharparenright}%
   226 \end{isabelle}
   227 is extensionally equal to \isa{path\ s\ P},
   228 where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}, whose defining
   229 equations we omit.%
   230 \end{isamarkuptext}%
   231 %
   232 \begin{isamarkuptext}%
   233 At last we can prove the opposite direction of \isa{AF{\isacharunderscore}lemma{\isadigit{1}}}:%
   234 \end{isamarkuptext}%
   235 \isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\isanewline
   236 {\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}%
   237 \begin{isamarkuptxt}%
   238 \noindent
   239 The proof is again pointwise and then by contraposition (\isa{contrapos{\isadigit{2}}} is the rule
   240 \isa{{\isasymlbrakk}{\isacharquery}Q{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P\ {\isasymLongrightarrow}\ {\isasymnot}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P}):%
   241 \end{isamarkuptxt}%
   242 \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
   243 \isacommand{apply}{\isacharparenleft}erule\ contrapos{\isadigit{2}}{\isacharparenright}\isanewline
   244 \isacommand{apply}\ simp%
   245 \begin{isamarkuptxt}%
   246 \begin{isabelle}
   247 \ \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
   248 \end{isabelle}
   249 Applying the \isa{infinity{\isacharunderscore}lemma} as a destruction rule leaves two subgoals, the second
   250 premise of \isa{infinity{\isacharunderscore}lemma} and the original subgoal:%
   251 \end{isamarkuptxt}%
   252 \isacommand{apply}{\isacharparenleft}drule\ infinity{\isacharunderscore}lemma{\isacharparenright}%
   253 \begin{isamarkuptxt}%
   254 \begin{isabelle}
   255 \ \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
   256 \ \isadigit{2}{\isachardot}\ {\isasymAnd}s{\isachardot}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline
   257 \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A
   258 \end{isabelle}
   259 Both are solved automatically:%
   260 \end{isamarkuptxt}%
   261 \ \isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline
   262 \isacommand{done}%
   263 \begin{isamarkuptext}%
   264 The main theorem is proved as for PDL, except that we also derive the necessary equality
   265 \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}}}
   266 on the spot:%
   267 \end{isamarkuptext}%
   268 \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline
   269 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
   270 \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
   271 \isacommand{done}%
   272 \begin{isamarkuptext}%
   273 The above language is not quite CTL. The latter also includes an
   274 until-operator, which is the subject of the following exercise.
   275 It is not definable in terms of the other operators!
   276 \begin{exercise}
   277 Extend the datatype of formulae by the binary until operator \isa{EU\ f\ g} with semantics
   278 ``there exist a path where \isa{f} is true until \isa{g} becomes true''
   279 \begin{isabelle}%
   280 \ \ \ \ \ 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}%
   281 \end{isabelle}
   282 and model checking algorithm
   283 \begin{isabelle}%
   284 \ \ \ \ \ 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}%
   285 \end{isabelle}
   286 Prove the equivalence between semantics and model checking, i.e.\ that
   287 \begin{isabelle}%
   288 \ \ \ \ \ mc\ {\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ EU\ f\ g{\isacharbraceright}%
   289 \end{isabelle}
   290 %For readability you may want to annotate {term EU} with its customary syntax
   291 %{text[display]"| EU formula formula    E[_ U _]"}
   292 %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
   293 \end{exercise}
   294 For more CTL exercises see, for example \cite{Huth-Ryan-book}.
   295 \bigskip
   296 
   297 Let us close this section with a few words about the executability of our model checkers.
   298 It is clear that if all sets are finite, they can be represented as lists and the usual
   299 set operations are easily implemented. Only \isa{lfp} requires a little thought.
   300 Fortunately the HOL library proves that in the case of finite sets and a monotone \isa{F},
   301 \isa{lfp\ F} can be computed by iterated application of \isa{F} to \isa{{\isacharbraceleft}{\isacharbraceright}} until
   302 a fixpoint is reached. It is actually possible to generate executable functional programs
   303 from HOL definitions, but that is beyond the scope of the tutorial.%
   304 \end{isamarkuptext}%
   305 \end{isabellebody}%
   306 %%% Local Variables:
   307 %%% mode: latex
   308 %%% TeX-master: "root"
   309 %%% End: