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