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