doc-src/TutorialI/CTL/document/CTL.tex
 author nipkow Thu Oct 12 18:38:23 2000 +0200 (2000-10-12) changeset 10212 33fe2d701ddd parent 10211 1bece7f35762 child 10217 e61e7e1eacaf permissions -rw-r--r--
*** empty log message ***
     1 %

     2 \begin{isabellebody}%

     3 \def\isabellecontext{CTL}%

     4 %

     5 \isamarkupsubsection{Computation tree logic---CTL}

     6 %

     7 \begin{isamarkuptext}%

     8 The semantics of PDL only needs transitive reflexive closure.

     9 Let us now be a bit more adventurous and introduce a new temporal operator

    10 that goes beyond transitive reflexive closure. We extend the datatype

    11 \isa{formula} by a new constructor%

    12 \end{isamarkuptext}%

    13 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AF\ formula%

    14 \begin{isamarkuptext}%

    15 \noindent

    16 which stands for "always in the future":

    17 on all paths, at some point the formula holds. Formalizing the notion of an infinite path is easy

    18 in HOL: it is simply a function from \isa{nat} to \isa{state}.%

    19 \end{isamarkuptext}%

    20 \isacommand{constdefs}\ Paths\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}set{\isachardoublequote}\isanewline

    21 \ \ \ \ \ \ \ \ \ {\isachardoublequote}Paths\ s\ {\isasymequiv}\ {\isacharbraceleft}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}{\isacharbraceright}{\isachardoublequote}%

    22 \begin{isamarkuptext}%

    23 \noindent

    24 This definition allows a very succinct statement of the semantics of \isa{AF}:

    25 \footnote{Do not be mislead: neither datatypes nor recursive functions can be

    26 extended by new constructors or equations. This is just a trick of the

    27 presentation. In reality one has to define a new datatype and a new function.}%

    28 \end{isamarkuptext}%

    29 {\isachardoublequote}s\ {\isasymTurnstile}\ AF\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequote}%

    30 \begin{isamarkuptext}%

    31 \noindent

    32 Model checking \isa{AF} involves a function which

    33 is just complicated enough to warrant a separate definition:%

    34 \end{isamarkuptext}%

    35 \isacommand{constdefs}\ af\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline

    36 \ \ \ \ \ \ \ \ \ {\isachardoublequote}af\ A\ T\ {\isasymequiv}\ A\ {\isasymunion}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\ t\ {\isasymin}\ T{\isacharbraceright}{\isachardoublequote}%

    37 \begin{isamarkuptext}%

    38 \noindent

    39 Now we define \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}} as the least set \isa{T} that contains

    40 \isa{mc\ f} and all states all of whose direct successors are in \isa{T}:%

    41 \end{isamarkuptext}%

    42 {\isachardoublequote}mc{\isacharparenleft}AF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}af{\isacharparenleft}mc\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}%

    43 \begin{isamarkuptext}%

    44 \noindent

    45 Because \isa{af} is monotone in its second argument (and also its first, but

    46 that is irrelevant) \isa{af\ A} has a least fixpoint:%

    47 \end{isamarkuptext}%

    48 \isacommand{lemma}\ mono{\isacharunderscore}af{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline

    49 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ mono{\isacharunderscore}def\ af{\isacharunderscore}def{\isacharparenright}\isanewline

    50 \isacommand{apply}\ blast\isanewline

    51 \isacommand{done}%

    52 \begin{isamarkuptext}%

    53 All we need to prove now is that \isa{mc} and \isa{{\isasymTurnstile}}

    54 agree for \isa{AF}, i.e.\ that \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ AF\ f{\isacharbraceright}}. This time we prove the two containments separately, starting

    55 with the easy one:%

    56 \end{isamarkuptext}%

    57 \isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{1}}{\isacharcolon}\isanewline

    58 \ \ {\isachardoublequote}lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}%

    59 \begin{isamarkuptxt}%

    60 \noindent

    61 The proof is again pointwise. Fixpoint induction on the premise \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} followed

    62 by simplification and clarification%

    63 \end{isamarkuptxt}%

    64 \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline

    65 \isacommand{apply}{\isacharparenleft}erule\ lfp{\isacharunderscore}induct{\isacharbrackleft}OF\ {\isacharunderscore}\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline

    66 \isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}%

    67 \begin{isamarkuptxt}%

    68 \noindent

    69 leads to the following somewhat involved proof state

    70 \begin{isabelle}

    71 \ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline

    72 \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ \isadigit{0}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline

    73 \ \ \ \ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymand}\isanewline

    74 \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}p{\isachardot}\ t\ {\isacharequal}\ p\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline

    75 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline

    76 \ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline

    77 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A

    78 \end{isabelle}

    79 Now we eliminate the disjunction. The case \isa{p\ {\isadigit{0}}\ {\isasymin}\ A} is trivial:%

    80 \end{isamarkuptxt}%

    81 \isacommand{apply}{\isacharparenleft}erule\ disjE{\isacharparenright}\isanewline

    82 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}%

    83 \begin{isamarkuptxt}%

    84 \noindent

    85 In the other case we set \isa{t} to \isa{p\ {\isadigit{1}}} and simplify matters:%

    86 \end{isamarkuptxt}%

    87 \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ {\isadigit{1}}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline

    88 \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%

    89 \begin{isamarkuptxt}%

    90 \begin{isabelle}

    91 \ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\ p\ \isadigit{1}\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharsemicolon}\isanewline

    92 \ \ \ \ \ \ \ \ \ \ \ {\isasymforall}pa{\isachardot}\ p\ \isadigit{1}\ {\isacharequal}\ pa\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline

    93 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline

    94 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A

    95 \end{isabelle}

    96 It merely remains to set \isa{pa} to \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}}, i.e.\ \isa{p} without its

    97 first element. The rest is practically automatic:%

    98 \end{isamarkuptxt}%

    99 \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline

   100 \isacommand{apply}\ simp\isanewline

   101 \isacommand{apply}\ blast\isanewline

   102 \isacommand{done}%

   103 \begin{isamarkuptext}%

   104 The opposite containment is proved by contradiction: if some state

   105 \isa{s} is not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then we can construct an

   106 infinite \isa{A}-avoiding path starting from \isa{s}. The reason is

   107 that by unfolding \isa{lfp} we find that if \isa{s} is not in

   108 \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then \isa{s} is not in \isa{A} and there is a

   109 direct successor of \isa{s} that is again not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Iterating this argument yields the promised infinite

   110 \isa{A}-avoiding path. Let us formalize this sketch.

   111

   112 The one-step argument in the above sketch%

   113 \end{isamarkuptext}%

   114 \isacommand{lemma}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharcolon}\isanewline

   115 \ {\isachardoublequote}s\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ s\ {\isasymnotin}\ A\ {\isasymand}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}{\isasymin}M\ {\isasymand}\ t\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline

   116 \isacommand{apply}{\isacharparenleft}erule\ swap{\isacharparenright}\isanewline

   117 \isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline

   118 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\isacharparenright}\isanewline

   119 \isacommand{done}%

   120 \begin{isamarkuptext}%

   121 \noindent

   122 is proved by a variant of contraposition (\isa{swap}:

   123 \isa{{\isasymlbrakk}{\isasymnot}\ Q{\isacharsemicolon}\ {\isasymnot}\ P\ {\isasymLongrightarrow}\ Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ P}), i.e.\ assuming the negation of the conclusion

   124 and proving \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Unfolding \isa{lfp} once and

   125 simplifying with the definition of \isa{af} finishes the proof.

   126

   127 Now we iterate this process. The following construction of the desired

   128 path is parameterized by a predicate \isa{P} that should hold along the path:%

   129 \end{isamarkuptext}%

   130 \isacommand{consts}\ path\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}state\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}{\isachardoublequote}\isanewline

   131 \isacommand{primrec}\isanewline

   132 {\isachardoublequote}path\ s\ P\ {\isadigit{0}}\ {\isacharequal}\ s{\isachardoublequote}\isanewline

   133 {\isachardoublequote}path\ s\ P\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ P\ n{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isachardoublequote}%

   134 \begin{isamarkuptext}%

   135 \noindent

   136 Element \isa{n\ {\isacharplus}\ {\isadigit{1}}} on this path is some arbitrary successor

   137 \isa{t} of element \isa{n} such that \isa{P\ t} holds.  Remember that \isa{SOME\ t{\isachardot}\ R\ t}

   138 is some arbitrary but fixed \isa{t} such that \isa{R\ t} holds (see \S\ref{sec-SOME}). Of

   139 course, such a \isa{t} may in general not exist, but that is of no

   140 concern to us since we will only use \isa{path} in such cases where a

   141 suitable \isa{t} does exist.

   142

   143 Let us show that if each state \isa{s} that satisfies \isa{P}

   144 has a successor that again satisfies \isa{P}, then there exists an infinite \isa{P}-path:%

   145 \end{isamarkuptext}%

   146 \isacommand{lemma}\ infinity{\isacharunderscore}lemma{\isacharcolon}\isanewline

   147 \ \ {\isachardoublequote}{\isasymlbrakk}\ P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\isanewline

   148 \ \ \ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}%

   149 \begin{isamarkuptxt}%

   150 \noindent

   151 First we rephrase the conclusion slightly because we need to prove both the path property

   152 and the fact that \isa{P} holds simultaneously:%

   153 \end{isamarkuptxt}%

   154 \isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}{\isasymexists}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}%

   155 \begin{isamarkuptxt}%

   156 \noindent

   157 From this proposition the original goal follows easily:%

   158 \end{isamarkuptxt}%

   159 \ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}%

   160 \begin{isamarkuptxt}%

   161 \noindent

   162 The new subgoal is proved by providing the witness \isa{path\ s\ P} for \isa{p}:%

   163 \end{isamarkuptxt}%

   164 \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}path\ s\ P{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline

   165 \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%

   166 \begin{isamarkuptxt}%

   167 \noindent

   168 After simplification and clarification the subgoal has the following compact form

   169 \begin{isabelle}

   170 \ \isadigit{1}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline

   171 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\isanewline

   172 \ \ \ \ \ \ \ \ \ \ \ \ P\ {\isacharparenleft}path\ s\ P\ i{\isacharparenright}

   173 \end{isabelle}

   174 and invites a proof by induction on \isa{i}:%

   175 \end{isamarkuptxt}%

   176 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline

   177 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}%

   178 \begin{isamarkuptxt}%

   179 \noindent

   180 After simplification the base case boils down to

   181 \begin{isabelle}

   182 \ \isadigit{1}{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline

   183 \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M

   184 \end{isabelle}

   185 The conclusion looks exceedingly trivial: after all, \isa{t} is chosen such that \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M}

   186 holds. However, we first have to show that such a \isa{t} actually exists! This reasoning

   187 is embodied in the theorem \isa{someI{\isadigit{2}}{\isacharunderscore}ex}:

   188 \begin{isabelle}%

   189 \ \ \ \ \ {\isasymlbrakk}{\isasymexists}a{\isachardot}\ {\isacharquery}P\ a{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharparenleft}SOME\ x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}%

   190 \end{isabelle}

   191 When we apply this theorem as an introduction rule, \isa{{\isacharquery}P\ x} becomes

   192 \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ x} and \isa{{\isacharquery}Q\ x} becomes \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M} and we have to prove

   193 two subgoals: \isa{{\isasymexists}a{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ a{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ a}, which follows from the assumptions, and

   194 \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ x\ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M}, which is trivial. Thus it is not surprising that

   195 \isa{fast} can prove the base case quickly:%

   196 \end{isamarkuptxt}%

   197 \ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}%

   198 \begin{isamarkuptxt}%

   199 \noindent

   200 What is worth noting here is that we have used \isa{fast} rather than

   201 \isa{blast}.  The reason is that \isa{blast} would fail because it cannot

   202 cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}: unifying its conclusion with the current

   203 subgoal is nontrivial because of the nested schematic variables. For

   204 efficiency reasons \isa{blast} does not even attempt such unifications.

   205 Although \isa{fast} can in principle cope with complicated unification

   206 problems, in practice the number of unifiers arising is often prohibitive and

   207 the offending rule may need to be applied explicitly rather than

   208 automatically. This is what happens in the step case.

   209

   210 The induction step is similar, but more involved, because now we face nested

   211 occurrences of \isa{SOME}. As a result, \isa{fast} is no longer able to

   212 solve the subgoal and we apply \isa{someI{\isadigit{2}}{\isacharunderscore}ex} by hand.  We merely

   213 show the proof commands but do not describe the details:%

   214 \end{isamarkuptxt}%

   215 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline

   216 \isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline

   217 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline

   218 \isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline

   219 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline

   220 \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline

   221 \isacommand{done}%

   222 \begin{isamarkuptext}%

   223 Function \isa{path} has fulfilled its purpose now and can be forgotten

   224 about. It was merely defined to provide the witness in the proof of the

   225 \isa{infinity{\isacharunderscore}lemma}. Aficionados of minimal proofs might like to know

   226 that we could have given the witness without having to define a new function:

   227 the term

   228 \begin{isabelle}%

   229 \ \ \ \ \ nat{\isacharunderscore}rec\ s\ {\isacharparenleft}{\isasymlambda}n\ t{\isachardot}\ SOME\ u{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ u{\isacharparenright}%

   230 \end{isabelle}

   231 is extensionally equal to \isa{path\ s\ P},

   232 where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}, whose defining

   233 equations we omit.%

   234 \end{isamarkuptext}%

   235 %

   236 \begin{isamarkuptext}%

   237 At last we can prove the opposite direction of \isa{AF{\isacharunderscore}lemma{\isadigit{1}}}:%

   238 \end{isamarkuptext}%

   239 \isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\isanewline

   240 {\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}%

   241 \begin{isamarkuptxt}%

   242 \noindent

   243 The proof is again pointwise and then by contraposition (\isa{contrapos{\isadigit{2}}} is the rule

   244 \isa{{\isasymlbrakk}{\isacharquery}Q{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P\ {\isasymLongrightarrow}\ {\isasymnot}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P}):%

   245 \end{isamarkuptxt}%

   246 \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline

   247 \isacommand{apply}{\isacharparenleft}erule\ contrapos{\isadigit{2}}{\isacharparenright}\isanewline

   248 \isacommand{apply}\ simp%

   249 \begin{isamarkuptxt}%

   250 \begin{isabelle}

   251 \ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A

   252 \end{isabelle}

   253 Applying the \isa{infinity{\isacharunderscore}lemma} as a destruction rule leaves two subgoals, the second

   254 premise of \isa{infinity{\isacharunderscore}lemma} and the original subgoal:%

   255 \end{isamarkuptxt}%

   256 \isacommand{apply}{\isacharparenleft}drule\ infinity{\isacharunderscore}lemma{\isacharparenright}%

   257 \begin{isamarkuptxt}%

   258 \begin{isabelle}

   259 \ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ {\isasymforall}s{\isachardot}\ s\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}\isanewline

   260 \ \isadigit{2}{\isachardot}\ {\isasymAnd}s{\isachardot}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline

   261 \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A

   262 \end{isabelle}

   263 Both are solved automatically:%

   264 \end{isamarkuptxt}%

   265 \ \isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline

   266 \isacommand{done}%

   267 \begin{isamarkuptext}%

   268 The main theorem is proved as for PDL, except that we also derive the necessary equality

   269 \isa{lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isacharequal}\ {\isachardot}{\isachardot}{\isachardot}} by combining \isa{AF{\isacharunderscore}lemma{\isadigit{1}}} and \isa{AF{\isacharunderscore}lemma{\isadigit{2}}}

   270 on the spot:%

   271 \end{isamarkuptext}%

   272 \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline

   273 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline

   274 \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma\ equalityI{\isacharbrackleft}OF\ AF{\isacharunderscore}lemma{\isadigit{1}}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharbrackright}{\isacharparenright}\isanewline

   275 \isacommand{done}%

   276 \begin{isamarkuptext}%

   277 The above language is not quite CTL. The latter also includes an

   278 until-operator, which is the subject of the following exercise.

   279 It is not definable in terms of the other operators!

   280 \begin{exercise}

   281 Extend the datatype of formulae by the binary until operator \isa{EU\ f\ g} with semantics

   282 there exist a path where \isa{f} is true until \isa{g} becomes true''

   283 \begin{isabelle}%

   284 \ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}j{\isachardot}\ p\ j\ {\isasymTurnstile}\ g\ {\isasymand}\ {\isacharparenleft}{\isasymexists}i\ {\isacharless}\ j{\isachardot}\ p\ i\ {\isasymTurnstile}\ f{\isacharparenright}{\isacharparenright}%

   285 \end{isabelle}

   286 and model checking algorithm

   287 \begin{isabelle}%

   288 \ \ \ \ \ mc{\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ g\ {\isasymunion}\ mc\ f\ {\isasyminter}\ {\isacharparenleft}M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isacharparenright}%

   289 \end{isabelle}

   290 Prove the equivalence between semantics and model checking, i.e.\ that

   291 \begin{isabelle}%

   292 \ \ \ \ \ mc\ {\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ EU\ f\ g{\isacharbraceright}%

   293 \end{isabelle}

   294 %For readability you may want to annotate {term EU} with its customary syntax

   295 %{text[display]"| EU formula formula    E[_ U _]"}

   296 %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.

   297 \end{exercise}

   298 For more CTL exercises see, for example \cite{Huth-Ryan-book}.

   299 \bigskip

   300

   301 Let us close this section with a few words about the executability of our model checkers.

   302 It is clear that if all sets are finite, they can be represented as lists and the usual

   303 set operations are easily implemented. Only \isa{lfp} requires a little thought.

   304 Fortunately the HOL library proves that in the case of finite sets and a monotone \isa{F},

   305 \isa{lfp\ F} can be computed by iterated application of \isa{F} to \isa{{\isacharbraceleft}{\isacharbraceright}} until

   306 a fixpoint is reached. It is actually possible to generate executable functional programs

   307 from HOL definitions, but that is beyond the scope of the tutorial.%

   308 \end{isamarkuptext}%

   309 \end{isabellebody}%

   310 %%% Local Variables:

   311 %%% mode: latex

   312 %%% TeX-master: "root"

   313 %%% End: