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: