doc-src/TutorialI/CTL/document/CTL.tex
 author wenzelm Thu Oct 12 18:09:06 2000 +0200 (2000-10-12) changeset 10211 1bece7f35762 parent 10192 4c2584e23ade child 10212 33fe2d701ddd permissions -rw-r--r--
updated;
     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 \isa{blast}.

   201 The reason is that \isa{blast} would fail because it cannot cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}:

   202 unifying its conclusion with the current subgoal is nontrivial because of the nested schematic

   203 variables. For efficiency reasons \isa{blast} does not even attempt such unifications.

   204 Although \isa{fast} can in principle cope with complicated unification problems, in practice

   205 the number of unifiers arising is often prohibitive and the offending rule may need to be applied

   206 explicitly rather than automatically.

   207

   208 The induction step is similar, but more involved, because now we face nested occurrences of

   209 \isa{SOME}. We merely show the proof commands but do not describe th details:%

   210 \end{isamarkuptxt}%

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

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

   213 \ \isacommand{apply}{\isacharparenleft}blast{\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}blast{\isacharparenright}\isanewline

   217 \isacommand{done}%

   218 \begin{isamarkuptext}%

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

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

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

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

   223 the term

   224 \begin{isabelle}%

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

   226 \end{isabelle}

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

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

   229 equations we omit.%

   230 \end{isamarkuptext}%

   231 %

   232 \begin{isamarkuptext}%

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

   234 \end{isamarkuptext}%

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

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

   237 \begin{isamarkuptxt}%

   238 \noindent

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

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

   241 \end{isamarkuptxt}%

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

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

   244 \isacommand{apply}\ simp%

   245 \begin{isamarkuptxt}%

   246 \begin{isabelle}

   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

   248 \end{isabelle}

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

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

   251 \end{isamarkuptxt}%

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

   253 \begin{isamarkuptxt}%

   254 \begin{isabelle}

   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

   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

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

   258 \end{isabelle}

   259 Both are solved automatically:%

   260 \end{isamarkuptxt}%

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

   262 \isacommand{done}%

   263 \begin{isamarkuptext}%

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

   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}}}

   266 on the spot:%

   267 \end{isamarkuptext}%

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

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

   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

   271 \isacommand{done}%

   272 \begin{isamarkuptext}%

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

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

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

   276 \begin{exercise}

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

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

   279 \begin{isabelle}%

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

   281 \end{isabelle}

   282 and model checking algorithm

   283 \begin{isabelle}%

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

   285 \end{isabelle}

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

   287 \begin{isabelle}%

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

   289 \end{isabelle}

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

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

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

   293 \end{exercise}

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

   295 \bigskip

   296

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

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

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

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

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

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

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

   304 \end{isamarkuptext}%

   305 \end{isabellebody}%

   306 %%% Local Variables:

   307 %%% mode: latex

   308 %%% TeX-master: "root"

   309 %%% End: