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