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: