doc-src/TutorialI/CTL/document/CTL.tex
author nipkow
Fri Oct 06 12:31:53 2000 +0200 (2000-10-06)
changeset 10159 a72ddfdbfca0
parent 10149 7cfdf6a330a0
child 10171 59d6633835fa
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{\isachardot}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 FIXME OF/of with undescore?
    70 
    71 leads to the following somewhat involved proof state
    72 \begin{isabelle}
    73 \ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline
    74 \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ \isadigit{0}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
    75 \ \ \ \ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymand}\isanewline
    76 \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\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
    77 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
    78 \ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
    79 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A
    80 \end{isabelle}
    81 Now we eliminate the disjunction. The case \isa{p\ \isadigit{0}\ {\isasymin}\ A} is trivial:%
    82 \end{isamarkuptxt}%
    83 \isacommand{apply}{\isacharparenleft}erule\ disjE{\isacharparenright}\isanewline
    84 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}%
    85 \begin{isamarkuptxt}%
    86 \noindent
    87 In the other case we set \isa{t} to \isa{p\ \isadigit{1}} and simplify matters:%
    88 \end{isamarkuptxt}%
    89 \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ \isadigit{1}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
    90 \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
    91 \begin{isamarkuptxt}%
    92 \begin{isabelle}
    93 \ \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
    94 \ \ \ \ \ \ \ \ \ \ \ {\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
    95 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
    96 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A
    97 \end{isabelle}
    98 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
    99 first element. The rest is practically automatic:%
   100 \end{isamarkuptxt}%
   101 \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
   102 \isacommand{apply}\ simp\isanewline
   103 \isacommand{apply}\ blast\isanewline
   104 \isacommand{done}%
   105 \begin{isamarkuptext}%
   106 The opposite containment is proved by contradiction: if some state
   107 \isa{s} is not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then we can construct an
   108 infinite \isa{A}-avoiding path starting from \isa{s}. The reason is
   109 that by unfolding \isa{lfp} we find that if \isa{s} is not in
   110 \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then \isa{s} is not in \isa{A} and there is a
   111 direct successor of \isa{s} that is again not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Iterating this argument yields the promised infinite
   112 \isa{A}-avoiding path. Let us formalize this sketch.
   113 
   114 The one-step argument in the above sketch%
   115 \end{isamarkuptext}%
   116 \isacommand{lemma}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharcolon}\isanewline
   117 \ {\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
   118 \isacommand{apply}{\isacharparenleft}erule\ swap{\isacharparenright}\isanewline
   119 \isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}Tarski{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline
   120 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\isacharparenright}\isanewline
   121 \isacommand{done}%
   122 \begin{isamarkuptext}%
   123 \noindent
   124 is proved by a variant of contraposition (\isa{swap}:
   125 \isa{{\isasymlbrakk}{\isasymnot}\ Pa{\isacharsemicolon}\ {\isasymnot}\ P\ {\isasymLongrightarrow}\ Pa{\isasymrbrakk}\ {\isasymLongrightarrow}\ P}), i.e.\ assuming the negation of the conclusion
   126 and proving \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Unfolding \isa{lfp} once and
   127 simplifying with the definition of \isa{af} finishes the proof.
   128 
   129 Now we iterate this process. The following construction of the desired
   130 path is parameterized by a predicate \isa{P} that should hold along the path:%
   131 \end{isamarkuptext}%
   132 \isacommand{consts}\ path\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}state\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}{\isachardoublequote}\isanewline
   133 \isacommand{primrec}\isanewline
   134 {\isachardoublequote}path\ s\ P\ \isadigit{0}\ {\isacharequal}\ s{\isachardoublequote}\isanewline
   135 {\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}%
   136 \begin{isamarkuptext}%
   137 \noindent
   138 Element \isa{n\ {\isacharplus}\ \isadigit{1}} on this path is some arbitrary successor
   139 \isa{t} of element \isa{n} such that \isa{P\ t} holds.  Remember that \isa{SOME\ t{\isachardot}\ R\ t}
   140 is some arbitrary but fixed \isa{t} such that \isa{R\ t} holds (see \S\ref{sec-SOME}). Of
   141 course, such a \isa{t} may in general not exist, but that is of no
   142 concern to us since we will only use \isa{path} in such cases where a
   143 suitable \isa{t} does exist.
   144 
   145 Let us show that if each state \isa{s} that satisfies \isa{P}
   146 has a successor that again satisfies \isa{P}, then there exists an infinite \isa{P}-path:%
   147 \end{isamarkuptext}%
   148 \isacommand{lemma}\ infinity{\isacharunderscore}lemma{\isacharcolon}\isanewline
   149 \ \ {\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
   150 \ \ \ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}%
   151 \begin{isamarkuptxt}%
   152 \noindent
   153 First we rephrase the conclusion slightly because we need to prove both the path property
   154 and the fact that \isa{P} holds simultaneously:%
   155 \end{isamarkuptxt}%
   156 \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}%
   157 \begin{isamarkuptxt}%
   158 \noindent
   159 From this proposition the original goal follows easily:%
   160 \end{isamarkuptxt}%
   161 \ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}%
   162 \begin{isamarkuptxt}%
   163 \noindent
   164 The new subgoal is proved by providing the witness \isa{path\ s\ P} for \isa{p}:%
   165 \end{isamarkuptxt}%
   166 \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}path\ s\ P{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
   167 \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
   168 \begin{isamarkuptxt}%
   169 \noindent
   170 After simplification and clarification the subgoal has the following compact form
   171 \begin{isabelle}
   172 \ \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
   173 \ \ \ \ \ \ \ \ {\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
   174 \ \ \ \ \ \ \ \ \ \ \ \ P\ {\isacharparenleft}path\ s\ P\ i{\isacharparenright}
   175 \end{isabelle}
   176 and invites a proof by induction on \isa{i}:%
   177 \end{isamarkuptxt}%
   178 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline
   179 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}%
   180 \begin{isamarkuptxt}%
   181 \noindent
   182 After simplification the base case boils down to
   183 \begin{isabelle}
   184 \ \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
   185 \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M
   186 \end{isabelle}
   187 The conclusion looks exceedingly trivial: after all, \isa{t} is chosen such that \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M}
   188 holds. However, we first have to show that such a \isa{t} actually exists! This reasoning
   189 is embodied in the theorem \isa{someI\isadigit{2}{\isacharunderscore}ex}:
   190 \begin{isabelle}%
   191 \ \ \ \ \ {\isasymlbrakk}{\isasymexists}a{\isachardot}\ {\isacharquery}P\ a{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharparenleft}Eps\ {\isacharquery}P{\isacharparenright}%
   192 \end{isabelle}
   193 When we apply this theorem as an introduction rule, \isa{{\isacharquery}P\ x} becomes
   194 \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
   195 two subgoals: \isa{{\isasymexists}a{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ a{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ a}, which follows from the assumptions, and
   196 \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
   197 \isa{fast} can prove the base case quickly:%
   198 \end{isamarkuptxt}%
   199 \ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}%
   200 \begin{isamarkuptxt}%
   201 \noindent
   202 What is worth noting here is that we have used \isa{fast} rather than \isa{blast}.
   203 The reason is that \isa{blast} would fail because it cannot cope with \isa{someI\isadigit{2}{\isacharunderscore}ex}:
   204 unifying its conclusion with the current subgoal is nontrivial because of the nested schematic
   205 variables. For efficiency reasons \isa{blast} does not even attempt such unifications.
   206 Although \isa{fast} can in principle cope with complicated unification problems, in practice
   207 the number of unifiers arising is often prohibitive and the offending rule may need to be applied
   208 explicitly rather than automatically.
   209 
   210 The induction step is similar, but more involved, because now we face nested occurrences of
   211 \isa{SOME}. We merely show the proof commands but do not describe th details:%
   212 \end{isamarkuptxt}%
   213 \isacommand{apply}{\isacharparenleft}simp{\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}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
   217 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   218 \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   219 \isacommand{done}%
   220 \begin{isamarkuptext}%
   221 Function \isa{path} has fulfilled its purpose now and can be forgotten
   222 about. It was merely defined to provide the witness in the proof of the
   223 \isa{infinity{\isacharunderscore}lemma}. Afficionados of minimal proofs might like to know
   224 that we could have given the witness without having to define a new function:
   225 the term
   226 \begin{isabelle}%
   227 \ \ \ \ \ nat{\isacharunderscore}rec\ s\ {\isacharparenleft}{\isasymlambda}n\ t{\isachardot}\ SOME\ u{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ u{\isacharparenright}%
   228 \end{isabelle}
   229 where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}, whose defining
   230 equations we omit, is extensionally equal to \isa{path\ s\ P}.%
   231 \end{isamarkuptext}%
   232 %
   233 \begin{isamarkuptext}%
   234 At last we can prove the opposite direction of \isa{AF{\isacharunderscore}lemma\isadigit{1}}:%
   235 \end{isamarkuptext}%
   236 \isacommand{theorem}\ AF{\isacharunderscore}lemma\isadigit{2}{\isacharcolon}\isanewline
   237 {\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}%
   238 \begin{isamarkuptxt}%
   239 \noindent
   240 The proof is again pointwise and then by contraposition (\isa{contrapos\isadigit{2}} is the rule
   241 \isa{{\isasymlbrakk}{\isacharquery}Q{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P\ {\isasymLongrightarrow}\ {\isasymnot}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P}):%
   242 \end{isamarkuptxt}%
   243 \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
   244 \isacommand{apply}{\isacharparenleft}erule\ contrapos\isadigit{2}{\isacharparenright}\isanewline
   245 \isacommand{apply}\ simp%
   246 \begin{isamarkuptxt}%
   247 \begin{isabelle}
   248 \ \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
   249 \end{isabelle}
   250 Applying the \isa{infinity{\isacharunderscore}lemma} as a destruction rule leaves two subgoals, the second
   251 premise of \isa{infinity{\isacharunderscore}lemma} and the original subgoal:%
   252 \end{isamarkuptxt}%
   253 \isacommand{apply}{\isacharparenleft}drule\ infinity{\isacharunderscore}lemma{\isacharparenright}%
   254 \begin{isamarkuptxt}%
   255 \begin{isabelle}
   256 \ \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
   257 \ \isadigit{2}{\isachardot}\ {\isasymAnd}s{\isachardot}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline
   258 \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A
   259 \end{isabelle}
   260 Both are solved automatically:%
   261 \end{isamarkuptxt}%
   262 \ \isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline
   263 \isacommand{done}%
   264 \begin{isamarkuptext}%
   265 The main theorem is proved as for PDL, except that we also derive the necessary equality
   266 \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}}
   267 on the spot:%
   268 \end{isamarkuptext}%
   269 \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline
   270 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
   271 \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
   272 \isacommand{done}%
   273 \begin{isamarkuptext}%
   274 Let us close this section with a few words about the executability of \isa{mc}.
   275 It is clear that if all sets are finite, they can be represented as lists and the usual
   276 set operations are easily implemented. Only \isa{lfp} requires a little thought.
   277 Fortunately the HOL library proves that in the case of finite sets and a monotone \isa{F},
   278 \isa{lfp\ F} can be computed by iterated application of \isa{F} to \isa{{\isacharbraceleft}{\isacharbraceright}} until
   279 a fixpoint is reached. It is possible to generate executable functional programs
   280 from HOL definitions, but that is beyond the scope of the tutorial.%
   281 \end{isamarkuptext}%
   282 \end{isabellebody}%
   283 %%% Local Variables:
   284 %%% mode: latex
   285 %%% TeX-master: "root"
   286 %%% End: