doc-src/TutorialI/CTL/document/CTL.tex
author nipkow
Fri Oct 06 12:31:53 2000 +0200 (2000-10-06)
changeset 10159 a72ddfdbfca0
parent 10149 7cfdf6a330a0
child 10171 59d6633835fa
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@10149
    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@10159
    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
FIXME OF/of with undescore?
nipkow@10159
    70
nipkow@10159
    71
leads to the following somewhat involved proof state
nipkow@10159
    72
\begin{isabelle}
nipkow@10159
    73
\ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline
nipkow@10159
    74
\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ \isadigit{0}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
nipkow@10159
    75
\ \ \ \ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymand}\isanewline
nipkow@10159
    76
\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\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
    77
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
nipkow@10159
    78
\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
nipkow@10159
    79
\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A
nipkow@10159
    80
\end{isabelle}
nipkow@10159
    81
Now we eliminate the disjunction. The case \isa{p\ \isadigit{0}\ {\isasymin}\ A} is trivial:%
nipkow@10159
    82
\end{isamarkuptxt}%
nipkow@10123
    83
\isacommand{apply}{\isacharparenleft}erule\ disjE{\isacharparenright}\isanewline
nipkow@10159
    84
\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}%
nipkow@10159
    85
\begin{isamarkuptxt}%
nipkow@10159
    86
\noindent
nipkow@10159
    87
In the other case we set \isa{t} to \isa{p\ \isadigit{1}} and simplify matters:%
nipkow@10159
    88
\end{isamarkuptxt}%
nipkow@10123
    89
\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ \isadigit{1}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
nipkow@10159
    90
\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
nipkow@10159
    91
\begin{isamarkuptxt}%
nipkow@10159
    92
\begin{isabelle}
nipkow@10159
    93
\ \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
    94
\ \ \ \ \ \ \ \ \ \ \ {\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
    95
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
nipkow@10159
    96
\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A
nipkow@10159
    97
\end{isabelle}
nipkow@10159
    98
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
    99
first element. The rest is practically automatic:%
nipkow@10159
   100
\end{isamarkuptxt}%
nipkow@10123
   101
\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
   102
\isacommand{apply}\ simp\isanewline
nipkow@10159
   103
\isacommand{apply}\ blast\isanewline
nipkow@10159
   104
\isacommand{done}%
nipkow@10123
   105
\begin{isamarkuptext}%
nipkow@10159
   106
The opposite containment is proved by contradiction: if some state
nipkow@10159
   107
\isa{s} is not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then we can construct an
nipkow@10123
   108
infinite \isa{A}-avoiding path starting from \isa{s}. The reason is
nipkow@10123
   109
that by unfolding \isa{lfp} we find that if \isa{s} is not in
nipkow@10123
   110
\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then \isa{s} is not in \isa{A} and there is a
nipkow@10123
   111
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
   112
\isa{A}-avoiding path. Let us formalize this sketch.
nipkow@10123
   113
nipkow@10123
   114
The one-step argument in the above sketch%
nipkow@10123
   115
\end{isamarkuptext}%
nipkow@10123
   116
\isacommand{lemma}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharcolon}\isanewline
nipkow@10123
   117
\ {\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
   118
\isacommand{apply}{\isacharparenleft}erule\ swap{\isacharparenright}\isanewline
nipkow@10123
   119
\isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}Tarski{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline
nipkow@10159
   120
\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\isacharparenright}\isanewline
nipkow@10159
   121
\isacommand{done}%
nipkow@10123
   122
\begin{isamarkuptext}%
nipkow@10123
   123
\noindent
nipkow@10123
   124
is proved by a variant of contraposition (\isa{swap}:
nipkow@10123
   125
\isa{{\isasymlbrakk}{\isasymnot}\ Pa{\isacharsemicolon}\ {\isasymnot}\ P\ {\isasymLongrightarrow}\ Pa{\isasymrbrakk}\ {\isasymLongrightarrow}\ P}), i.e.\ assuming the negation of the conclusion
nipkow@10123
   126
and proving \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Unfolding \isa{lfp} once and
nipkow@10123
   127
simplifying with the definition of \isa{af} finishes the proof.
nipkow@10123
   128
nipkow@10123
   129
Now we iterate this process. The following construction of the desired
nipkow@10123
   130
path is parameterized by a predicate \isa{P} that should hold along the path:%
nipkow@10123
   131
\end{isamarkuptext}%
nipkow@10123
   132
\isacommand{consts}\ path\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}state\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}{\isachardoublequote}\isanewline
nipkow@10123
   133
\isacommand{primrec}\isanewline
nipkow@10123
   134
{\isachardoublequote}path\ s\ P\ \isadigit{0}\ {\isacharequal}\ s{\isachardoublequote}\isanewline
nipkow@10123
   135
{\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
   136
\begin{isamarkuptext}%
nipkow@10123
   137
\noindent
nipkow@10123
   138
Element \isa{n\ {\isacharplus}\ \isadigit{1}} on this path is some arbitrary successor
nipkow@10159
   139
\isa{t} of element \isa{n} such that \isa{P\ t} holds.  Remember that \isa{SOME\ t{\isachardot}\ R\ t}
nipkow@10159
   140
is some arbitrary but fixed \isa{t} such that \isa{R\ t} holds (see \S\ref{sec-SOME}). Of
nipkow@10123
   141
course, such a \isa{t} may in general not exist, but that is of no
nipkow@10123
   142
concern to us since we will only use \isa{path} in such cases where a
nipkow@10123
   143
suitable \isa{t} does exist.
nipkow@10123
   144
nipkow@10159
   145
Let us show that if each state \isa{s} that satisfies \isa{P}
nipkow@10159
   146
has a successor that again satisfies \isa{P}, then there exists an infinite \isa{P}-path:%
nipkow@10123
   147
\end{isamarkuptext}%
nipkow@10159
   148
\isacommand{lemma}\ infinity{\isacharunderscore}lemma{\isacharcolon}\isanewline
nipkow@10159
   149
\ \ {\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
   150
\ \ \ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}%
nipkow@10123
   151
\begin{isamarkuptxt}%
nipkow@10123
   152
\noindent
nipkow@10123
   153
First we rephrase the conclusion slightly because we need to prove both the path property
nipkow@10123
   154
and the fact that \isa{P} holds simultaneously:%
nipkow@10123
   155
\end{isamarkuptxt}%
nipkow@10159
   156
\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
   157
\begin{isamarkuptxt}%
nipkow@10159
   158
\noindent
nipkow@10159
   159
From this proposition the original goal follows easily:%
nipkow@10159
   160
\end{isamarkuptxt}%
nipkow@10159
   161
\ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}%
nipkow@10159
   162
\begin{isamarkuptxt}%
nipkow@10159
   163
\noindent
nipkow@10159
   164
The new subgoal is proved by providing the witness \isa{path\ s\ P} for \isa{p}:%
nipkow@10159
   165
\end{isamarkuptxt}%
nipkow@10159
   166
\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}path\ s\ P{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
nipkow@10159
   167
\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
nipkow@10159
   168
\begin{isamarkuptxt}%
nipkow@10159
   169
\noindent
nipkow@10159
   170
After simplification and clarification the subgoal has the following compact form
nipkow@10159
   171
\begin{isabelle}
nipkow@10159
   172
\ \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
   173
\ \ \ \ \ \ \ \ {\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
   174
\ \ \ \ \ \ \ \ \ \ \ \ P\ {\isacharparenleft}path\ s\ P\ i{\isacharparenright}
nipkow@10159
   175
\end{isabelle}
nipkow@10159
   176
and invites a proof by induction on \isa{i}:%
nipkow@10159
   177
\end{isamarkuptxt}%
nipkow@10159
   178
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline
nipkow@10159
   179
\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}%
nipkow@10123
   180
\begin{isamarkuptxt}%
nipkow@10123
   181
\noindent
nipkow@10159
   182
After simplification the base case boils down to
nipkow@10159
   183
\begin{isabelle}
nipkow@10159
   184
\ \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
   185
\ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M
nipkow@10159
   186
\end{isabelle}
nipkow@10159
   187
The conclusion looks exceedingly trivial: after all, \isa{t} is chosen such that \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M}
nipkow@10159
   188
holds. However, we first have to show that such a \isa{t} actually exists! This reasoning
nipkow@10159
   189
is embodied in the theorem \isa{someI\isadigit{2}{\isacharunderscore}ex}:
nipkow@10159
   190
\begin{isabelle}%
nipkow@10159
   191
\ \ \ \ \ {\isasymlbrakk}{\isasymexists}a{\isachardot}\ {\isacharquery}P\ a{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharparenleft}Eps\ {\isacharquery}P{\isacharparenright}%
nipkow@10159
   192
\end{isabelle}
nipkow@10159
   193
When we apply this theorem as an introduction rule, \isa{{\isacharquery}P\ x} becomes
nipkow@10159
   194
\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
   195
two subgoals: \isa{{\isasymexists}a{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ a{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ a}, which follows from the assumptions, and
nipkow@10159
   196
\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
   197
\isa{fast} can prove the base case quickly:%
nipkow@10123
   198
\end{isamarkuptxt}%
nipkow@10159
   199
\ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}%
nipkow@10159
   200
\begin{isamarkuptxt}%
nipkow@10159
   201
\noindent
nipkow@10159
   202
What is worth noting here is that we have used \isa{fast} rather than \isa{blast}.
nipkow@10159
   203
The reason is that \isa{blast} would fail because it cannot cope with \isa{someI\isadigit{2}{\isacharunderscore}ex}:
nipkow@10159
   204
unifying its conclusion with the current subgoal is nontrivial because of the nested schematic
nipkow@10159
   205
variables. For efficiency reasons \isa{blast} does not even attempt such unifications.
nipkow@10159
   206
Although \isa{fast} can in principle cope with complicated unification problems, in practice
nipkow@10159
   207
the number of unifiers arising is often prohibitive and the offending rule may need to be applied
nipkow@10159
   208
explicitly rather than automatically.
nipkow@10159
   209
nipkow@10159
   210
The induction step is similar, but more involved, because now we face nested occurrences of
nipkow@10159
   211
\isa{SOME}. We merely show the proof commands but do not describe th details:%
nipkow@10159
   212
\end{isamarkuptxt}%
nipkow@10123
   213
\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
nipkow@10133
   214
\isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
nipkow@10123
   215
\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
nipkow@10133
   216
\isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
nipkow@10123
   217
\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
nipkow@10159
   218
\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
nipkow@10159
   219
\isacommand{done}%
nipkow@10159
   220
\begin{isamarkuptext}%
nipkow@10159
   221
Function \isa{path} has fulfilled its purpose now and can be forgotten
nipkow@10159
   222
about. It was merely defined to provide the witness in the proof of the
nipkow@10159
   223
\isa{infinity{\isacharunderscore}lemma}. Afficionados of minimal proofs might like to know
nipkow@10159
   224
that we could have given the witness without having to define a new function:
nipkow@10159
   225
the term
nipkow@10159
   226
\begin{isabelle}%
nipkow@10159
   227
\ \ \ \ \ 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
   228
\end{isabelle}
nipkow@10159
   229
where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}, whose defining
nipkow@10159
   230
equations we omit, is extensionally equal to \isa{path\ s\ P}.%
nipkow@10159
   231
\end{isamarkuptext}%
nipkow@10159
   232
%
nipkow@10159
   233
\begin{isamarkuptext}%
nipkow@10159
   234
At last we can prove the opposite direction of \isa{AF{\isacharunderscore}lemma\isadigit{1}}:%
nipkow@10159
   235
\end{isamarkuptext}%
nipkow@10159
   236
\isacommand{theorem}\ AF{\isacharunderscore}lemma\isadigit{2}{\isacharcolon}\isanewline
nipkow@10159
   237
{\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
   238
\begin{isamarkuptxt}%
nipkow@10159
   239
\noindent
nipkow@10159
   240
The proof is again pointwise and then by contraposition (\isa{contrapos\isadigit{2}} is the rule
nipkow@10159
   241
\isa{{\isasymlbrakk}{\isacharquery}Q{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P\ {\isasymLongrightarrow}\ {\isasymnot}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P}):%
nipkow@10159
   242
\end{isamarkuptxt}%
nipkow@10123
   243
\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
nipkow@10123
   244
\isacommand{apply}{\isacharparenleft}erule\ contrapos\isadigit{2}{\isacharparenright}\isanewline
nipkow@10159
   245
\isacommand{apply}\ simp%
nipkow@10159
   246
\begin{isamarkuptxt}%
nipkow@10159
   247
\begin{isabelle}
nipkow@10159
   248
\ \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
   249
\end{isabelle}
nipkow@10159
   250
Applying the \isa{infinity{\isacharunderscore}lemma} as a destruction rule leaves two subgoals, the second
nipkow@10159
   251
premise of \isa{infinity{\isacharunderscore}lemma} and the original subgoal:%
nipkow@10159
   252
\end{isamarkuptxt}%
nipkow@10159
   253
\isacommand{apply}{\isacharparenleft}drule\ infinity{\isacharunderscore}lemma{\isacharparenright}%
nipkow@10159
   254
\begin{isamarkuptxt}%
nipkow@10159
   255
\begin{isabelle}
nipkow@10159
   256
\ \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
   257
\ \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
   258
\ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A
nipkow@10159
   259
\end{isabelle}
nipkow@10159
   260
Both are solved automatically:%
nipkow@10159
   261
\end{isamarkuptxt}%
nipkow@10159
   262
\ \isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline
nipkow@10159
   263
\isacommand{done}%
nipkow@10159
   264
\begin{isamarkuptext}%
nipkow@10159
   265
The main theorem is proved as for PDL, except that we also derive the necessary equality
nipkow@10159
   266
\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
   267
on the spot:%
nipkow@10159
   268
\end{isamarkuptext}%
nipkow@10123
   269
\isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline
nipkow@10123
   270
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
nipkow@10159
   271
\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
   272
\isacommand{done}%
nipkow@10159
   273
\begin{isamarkuptext}%
nipkow@10159
   274
Let us close this section with a few words about the executability of \isa{mc}.
nipkow@10159
   275
It is clear that if all sets are finite, they can be represented as lists and the usual
nipkow@10159
   276
set operations are easily implemented. Only \isa{lfp} requires a little thought.
nipkow@10159
   277
Fortunately the HOL library proves that in the case of finite sets and a monotone \isa{F},
nipkow@10159
   278
\isa{lfp\ F} can be computed by iterated application of \isa{F} to \isa{{\isacharbraceleft}{\isacharbraceright}} until
nipkow@10159
   279
a fixpoint is reached. It is possible to generate executable functional programs
nipkow@10159
   280
from HOL definitions, but that is beyond the scope of the tutorial.%
nipkow@10159
   281
\end{isamarkuptext}%
nipkow@10123
   282
\end{isabellebody}%
nipkow@10123
   283
%%% Local Variables:
nipkow@10123
   284
%%% mode: latex
nipkow@10123
   285
%%% TeX-master: "root"
nipkow@10123
   286
%%% End: