doc-src/TutorialI/CTL/document/CTL.tex
 author nipkow Fri Oct 13 18:02:08 2000 +0200 (2000-10-13) changeset 10217 e61e7e1eacaf parent 10212 33fe2d701ddd child 10225 b9fd52525b69 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 \label{sec:CTL}

     9 The semantics of PDL only needs transitive reflexive closure.

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

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

    12 \isa{formula} by a new constructor%

    13 \end{isamarkuptext}%

    14 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AF\ formula%

    15 \begin{isamarkuptext}%

    16 \noindent

    17 which stands for "always in the future":

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

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

    20 \end{isamarkuptext}%

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

    22 \ \ \ \ \ \ \ \ \ {\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}%

    23 \begin{isamarkuptext}%

    24 \noindent

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

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

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

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

    29 \end{isamarkuptext}%

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

    31 \begin{isamarkuptext}%

    32 \noindent

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

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

    35 \end{isamarkuptext}%

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

    37 \ \ \ \ \ \ \ \ \ {\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}%

    38 \begin{isamarkuptext}%

    39 \noindent

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

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

    42 \end{isamarkuptext}%

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

    44 \begin{isamarkuptext}%

    45 \noindent

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

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

    48 \end{isamarkuptext}%

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

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

    51 \isacommand{apply}\ blast\isanewline

    52 \isacommand{done}%

    53 \begin{isamarkuptext}%

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

    55 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

    56 with the easy one:%

    57 \end{isamarkuptext}%

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

    59 \ \ {\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}%

    60 \begin{isamarkuptxt}%

    61 \noindent

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

    63 by simplification and clarification%

    64 \end{isamarkuptxt}%

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

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

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

    68 \begin{isamarkuptxt}%

    69 \noindent

    70 leads to the following somewhat involved proof state

    71 \begin{isabelle}

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

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

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

    75 \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\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

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

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

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

    79 \end{isabelle}

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

    81 \end{isamarkuptxt}%

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

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

    84 \begin{isamarkuptxt}%

    85 \noindent

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

    87 \end{isamarkuptxt}%

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

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

    90 \begin{isamarkuptxt}%

    91 \begin{isabelle}

    92 \ \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

    93 \ \ \ \ \ \ \ \ \ \ \ {\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

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

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

    96 \end{isabelle}

    97 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

    98 first element. The rest is practically automatic:%

    99 \end{isamarkuptxt}%

   100 \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

   101 \isacommand{apply}\ simp\isanewline

   102 \isacommand{apply}\ blast\isanewline

   103 \isacommand{done}%

   104 \begin{isamarkuptext}%

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

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

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

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

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

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

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

   112

   113 The one-step argument in the above sketch%

   114 \end{isamarkuptext}%

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

   116 \ {\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

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

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

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

   120 \isacommand{done}%

   121 \begin{isamarkuptext}%

   122 \noindent

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

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

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

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

   127

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

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

   130 \end{isamarkuptext}%

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

   132 \isacommand{primrec}\isanewline

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

   134 {\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}%

   135 \begin{isamarkuptext}%

   136 \noindent

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

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

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

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

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

   142 suitable \isa{t} does exist.

   143

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

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

   146 \end{isamarkuptext}%

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

   148 \ \ {\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

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

   150 \begin{isamarkuptxt}%

   151 \noindent

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

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

   154 \end{isamarkuptxt}%

   155 \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}%

   156 \begin{isamarkuptxt}%

   157 \noindent

   158 From this proposition the original goal follows easily:%

   159 \end{isamarkuptxt}%

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

   161 \begin{isamarkuptxt}%

   162 \noindent

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

   164 \end{isamarkuptxt}%

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

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

   167 \begin{isamarkuptxt}%

   168 \noindent

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

   170 \begin{isabelle}

   171 \ \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

   172 \ \ \ \ \ \ \ \ {\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

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

   174 \end{isabelle}

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

   176 \end{isamarkuptxt}%

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

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

   179 \begin{isamarkuptxt}%

   180 \noindent

   181 After simplification the base case boils down to

   182 \begin{isabelle}

   183 \ \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

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

   185 \end{isabelle}

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

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

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

   189 \begin{isabelle}%

   190 \ \ \ \ \ {\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}%

   191 \end{isabelle}

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

   193 \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

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

   195 \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

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

   197 \end{isamarkuptxt}%

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

   199 \begin{isamarkuptxt}%

   200 \noindent

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

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

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

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

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

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

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

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

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

   210

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

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

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

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

   215 \end{isamarkuptxt}%

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

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

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

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

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

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

   222 \isacommand{done}%

   223 \begin{isamarkuptext}%

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

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

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

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

   228 the term

   229 \begin{isabelle}%

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

   231 \end{isabelle}

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

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

   234 equations we omit.%

   235 \end{isamarkuptext}%

   236 %

   237 \begin{isamarkuptext}%

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

   239 \end{isamarkuptext}%

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

   241 {\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}%

   242 \begin{isamarkuptxt}%

   243 \noindent

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

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

   246 \end{isamarkuptxt}%

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

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

   249 \isacommand{apply}\ simp%

   250 \begin{isamarkuptxt}%

   251 \begin{isabelle}

   252 \ \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

   253 \end{isabelle}

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

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

   256 \end{isamarkuptxt}%

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

   258 \begin{isamarkuptxt}%

   259 \begin{isabelle}

   260 \ \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

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

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

   263 \end{isabelle}

   264 Both are solved automatically:%

   265 \end{isamarkuptxt}%

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

   267 \isacommand{done}%

   268 \begin{isamarkuptext}%

   269 If you found the above proofs somewhat complicated we recommend you read

   270 \S\ref{sec:CTL-revisited} where we shown how inductive definitions lead to

   271 simpler arguments.

   272

   273 The main theorem is proved as for PDL, except that we also derive the

   274 necessary equality \isa{lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isacharequal}\ {\isachardot}{\isachardot}{\isachardot}} by combining

   275 \isa{AF{\isacharunderscore}lemma{\isadigit{1}}} and \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} on the spot:%

   276 \end{isamarkuptext}%

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

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

   279 \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

   280 \isacommand{done}%

   281 \begin{isamarkuptext}%

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

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

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

   285 \begin{exercise}

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

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

   288 \begin{isabelle}%

   289 \ \ \ \ \ 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}%

   290 \end{isabelle}

   291 and model checking algorithm

   292 \begin{isabelle}%

   293 \ \ \ \ \ 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}%

   294 \end{isabelle}

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

   296 \begin{isabelle}%

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

   298 \end{isabelle}

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

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

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

   302 \end{exercise}

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

   304 \bigskip

   305

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

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

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

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

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

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

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

   313 \end{isamarkuptext}%

   314 \end{isabellebody}%

   315 %%% Local Variables:

   316 %%% mode: latex

   317 %%% TeX-master: "root"

   318 %%% End: