doc-src/TutorialI/CTL/document/CTLind.tex
author nipkow
Wed Dec 06 13:22:58 2000 +0100 (2000-12-06)
changeset 10608 620647438780
parent 10601 894f845c3dbf
child 10617 adc0ed64a120
permissions -rw-r--r--
*** empty log message ***
wenzelm@10267
     1
%
wenzelm@10267
     2
\begin{isabellebody}%
wenzelm@10267
     3
\def\isabellecontext{CTLind}%
wenzelm@10267
     4
%
wenzelm@10395
     5
\isamarkupsubsection{CTL revisited%
wenzelm@10395
     6
}
wenzelm@10267
     7
%
wenzelm@10267
     8
\begin{isamarkuptext}%
wenzelm@10267
     9
\label{sec:CTL-revisited}
nipkow@10283
    10
The purpose of this section is twofold: we want to demonstrate
nipkow@10283
    11
some of the induction principles and heuristics discussed above and we want to
nipkow@10283
    12
show how inductive definitions can simplify proofs.
wenzelm@10267
    13
In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a
wenzelm@10267
    14
model checker for CTL. In particular the proof of the
wenzelm@10267
    15
\isa{infinity{\isacharunderscore}lemma} on the way to \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} is not as
wenzelm@10267
    16
simple as one might intuitively expect, due to the \isa{SOME} operator
nipkow@10283
    17
involved. Below we give a simpler proof of \isa{AF{\isacharunderscore}lemma{\isadigit{2}}}
nipkow@10283
    18
based on an auxiliary inductive definition.
wenzelm@10267
    19
wenzelm@10267
    20
Let us call a (finite or infinite) path \emph{\isa{A}-avoiding} if it does
wenzelm@10267
    21
not touch any node in the set \isa{A}. Then \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} says
wenzelm@10267
    22
that if no infinite path from some state \isa{s} is \isa{A}-avoiding,
wenzelm@10267
    23
then \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. We prove this by inductively defining the set
wenzelm@10267
    24
\isa{Avoid\ s\ A} of states reachable from \isa{s} by a finite \isa{A}-avoiding path:
wenzelm@10267
    25
% Second proof of opposite direction, directly by well-founded induction
wenzelm@10267
    26
% on the initial segment of M that avoids A.%
wenzelm@10267
    27
\end{isamarkuptext}%
wenzelm@10267
    28
\isacommand{consts}\ Avoid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline
wenzelm@10267
    29
\isacommand{inductive}\ {\isachardoublequote}Avoid\ s\ A{\isachardoublequote}\isanewline
wenzelm@10267
    30
\isakeyword{intros}\ {\isachardoublequote}s\ {\isasymin}\ Avoid\ s\ A{\isachardoublequote}\isanewline
wenzelm@10267
    31
\ \ \ \ \ \ \ {\isachardoublequote}{\isasymlbrakk}\ t\ {\isasymin}\ Avoid\ s\ A{\isacharsemicolon}\ t\ {\isasymnotin}\ A{\isacharsemicolon}\ {\isacharparenleft}t{\isacharcomma}u{\isacharparenright}\ {\isasymin}\ M\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ u\ {\isasymin}\ Avoid\ s\ A{\isachardoublequote}%
wenzelm@10267
    32
\begin{isamarkuptext}%
wenzelm@10267
    33
It is easy to see that for any infinite \isa{A}-avoiding path \isa{f}
wenzelm@10267
    34
with \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path
wenzelm@10267
    35
starting with \isa{s} because (by definition of \isa{Avoid}) there is a
wenzelm@10267
    36
finite \isa{A}-avoiding path from \isa{s} to \isa{f\ {\isadigit{0}}}.
wenzelm@10267
    37
The proof is by induction on \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A}. However,
wenzelm@10267
    38
this requires the following
wenzelm@10267
    39
reformulation, as explained in \S\ref{sec:ind-var-in-prems} above;
wenzelm@10267
    40
the \isa{rule{\isacharunderscore}format} directive undoes the reformulation after the proof.%
wenzelm@10267
    41
\end{isamarkuptext}%
wenzelm@10267
    42
\isacommand{lemma}\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
wenzelm@10267
    43
\ \ {\isachardoublequote}t\ {\isasymin}\ Avoid\ s\ A\ \ {\isasymLongrightarrow}\isanewline
wenzelm@10267
    44
\ \ \ {\isasymforall}f{\isasymin}Paths\ t{\isachardot}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ f\ i\ {\isasymnotin}\ A{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A{\isacharparenright}{\isachardoublequote}\isanewline
wenzelm@10267
    45
\isacommand{apply}{\isacharparenleft}erule\ Avoid{\isachardot}induct{\isacharparenright}\isanewline
wenzelm@10267
    46
\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
wenzelm@10267
    47
\isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
wenzelm@10267
    48
\isacommand{apply}{\isacharparenleft}drule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ case\ i\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ t\ {\isacharbar}\ Suc\ i\ {\isasymRightarrow}\ f\ i{\isachardoublequote}\ \isakeyword{in}\ bspec{\isacharparenright}\isanewline
wenzelm@10267
    49
\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}Paths{\isacharunderscore}def\ split{\isacharcolon}nat{\isachardot}split{\isacharparenright}\isanewline
wenzelm@10267
    50
\isacommand{done}%
wenzelm@10267
    51
\begin{isamarkuptext}%
wenzelm@10267
    52
\noindent
wenzelm@10267
    53
The base case (\isa{t\ {\isacharequal}\ s}) is trivial (\isa{blast}).
wenzelm@10267
    54
In the induction step, we have an infinite \isa{A}-avoiding path \isa{f}
wenzelm@10267
    55
starting from \isa{u}, a successor of \isa{t}. Now we simply instantiate
wenzelm@10267
    56
the \isa{{\isasymforall}f{\isasymin}Paths\ t} in the induction hypothesis by the path starting with
wenzelm@10267
    57
\isa{t} and continuing with \isa{f}. That is what the above $\lambda$-term
wenzelm@10267
    58
expresses. That fact that this is a path starting with \isa{t} and that
wenzelm@10267
    59
the instantiated induction hypothesis implies the conclusion is shown by
wenzelm@10267
    60
simplification.
wenzelm@10267
    61
wenzelm@10267
    62
Now we come to the key lemma. It says that if \isa{t} can be reached by a
wenzelm@10267
    63
finite \isa{A}-avoiding path from \isa{s}, then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}},
wenzelm@10267
    64
provided there is no infinite \isa{A}-avoiding path starting from \isa{s}.%
wenzelm@10267
    65
\end{isamarkuptext}%
wenzelm@10267
    66
\isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline
wenzelm@10267
    67
\ \ {\isachardoublequote}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ Avoid\ s\ A\ {\isasymlongrightarrow}\ t\ {\isasymin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}%
wenzelm@10267
    68
\begin{isamarkuptxt}%
wenzelm@10267
    69
\noindent
wenzelm@10267
    70
The trick is not to induct on \isa{t\ {\isasymin}\ Avoid\ s\ A}, as already the base
wenzelm@10267
    71
case would be a problem, but to proceed by well-founded induction \isa{t}. Hence \isa{t\ {\isasymin}\ Avoid\ s\ A} needs to be brought into the conclusion as
wenzelm@10267
    72
well, which the directive \isa{rule{\isacharunderscore}format} undoes at the end (see below).
wenzelm@10267
    73
But induction with respect to which well-founded relation? The restriction
wenzelm@10267
    74
of \isa{M} to \isa{Avoid\ s\ A}:
wenzelm@10267
    75
\begin{isabelle}%
wenzelm@10267
    76
\ \ \ \ \ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ y\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}%
wenzelm@10267
    77
\end{isabelle}
wenzelm@10267
    78
As we shall see in a moment, the absence of infinite \isa{A}-avoiding paths
wenzelm@10267
    79
starting from \isa{s} implies well-foundedness of this relation. For the
wenzelm@10267
    80
moment we assume this and proceed with the induction:%
wenzelm@10267
    81
\end{isamarkuptxt}%
wenzelm@10267
    82
\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\isanewline
wenzelm@10267
    83
\ \ {\isachardoublequote}wf{\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isasymin}M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ y\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}{\isachardoublequote}{\isacharparenright}\isanewline
wenzelm@10267
    84
\ \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline
wenzelm@10267
    85
\ \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
wenzelm@10267
    86
\begin{isamarkuptxt}%
wenzelm@10267
    87
\noindent
wenzelm@10267
    88
Now can assume additionally (induction hypothesis) that if \isa{t\ {\isasymnotin}\ A}
wenzelm@10267
    89
then all successors of \isa{t} that are in \isa{Avoid\ s\ A} are in
wenzelm@10267
    90
\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. To prove the actual goal we unfold \isa{lfp} once. Now
wenzelm@10267
    91
we have to prove that \isa{t} is in \isa{A} or all successors of \isa{t} are in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. If \isa{t} is not in \isa{A}, the second
wenzelm@10267
    92
\isa{Avoid}-rule implies that all successors of \isa{t} are in
wenzelm@10267
    93
\isa{Avoid\ s\ A} (because we also assume \isa{t\ {\isasymin}\ Avoid\ s\ A}), and
wenzelm@10267
    94
hence, by the induction hypothesis, all successors of \isa{t} are indeed in
wenzelm@10267
    95
\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Mechanically:%
wenzelm@10267
    96
\end{isamarkuptxt}%
wenzelm@10267
    97
\ \isacommand{apply}{\isacharparenleft}rule\ ssubst\ {\isacharbrackleft}OF\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline
wenzelm@10267
    98
\ \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline
wenzelm@10267
    99
\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}%
wenzelm@10267
   100
\begin{isamarkuptxt}%
wenzelm@10267
   101
Having proved the main goal we return to the proof obligation that the above
wenzelm@10267
   102
relation is indeed well-founded. This is proved by contraposition: we assume
wenzelm@10267
   103
the relation is not well-founded. Thus there exists an infinite \isa{A}-avoiding path all in \isa{Avoid\ s\ A}, by theorem
wenzelm@10267
   104
\isa{wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain}:
wenzelm@10267
   105
\begin{isabelle}%
wenzelm@10267
   106
\ \ \ \ \ wf\ r\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ {\isacharparenleft}{\isasymexists}f{\isachardot}\ {\isasymforall}i{\isachardot}\ {\isacharparenleft}f\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharcomma}\ f\ i{\isacharparenright}\ {\isasymin}\ r{\isacharparenright}{\isacharparenright}%
wenzelm@10267
   107
\end{isabelle}
wenzelm@10267
   108
From lemma \isa{ex{\isacharunderscore}infinite{\isacharunderscore}path} the existence of an infinite
wenzelm@10267
   109
\isa{A}-avoiding path starting in \isa{s} follows, just as required for
wenzelm@10267
   110
the contraposition.%
wenzelm@10267
   111
\end{isamarkuptxt}%
wenzelm@10267
   112
\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline
wenzelm@10267
   113
\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline
wenzelm@10267
   114
\isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
wenzelm@10267
   115
\isacommand{apply}{\isacharparenleft}rule\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharparenright}\isanewline
wenzelm@10267
   116
\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharparenright}\isanewline
wenzelm@10267
   117
\isacommand{done}%
wenzelm@10267
   118
\begin{isamarkuptext}%
wenzelm@10267
   119
The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive means
wenzelm@10267
   120
that the assumption is left unchanged---otherwise the \isa{{\isasymforall}p} is turned
wenzelm@10267
   121
into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is,
wenzelm@10267
   122
\isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now
wenzelm@10267
   123
\begin{isabelle}%
paulson@10601
   124
\ \ \ \ \ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\ t\ {\isasymin}\ Avoid\ s\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}%
wenzelm@10267
   125
\end{isabelle}
wenzelm@10267
   126
The main theorem is simply the corollary where \isa{t\ {\isacharequal}\ s},
wenzelm@10267
   127
in which case the assumption \isa{t\ {\isasymin}\ Avoid\ s\ A} is trivially true
wenzelm@10267
   128
by the first \isa{Avoid}-rule). Isabelle confirms this:%
wenzelm@10267
   129
\end{isamarkuptext}%
wenzelm@10267
   130
\isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\isanewline
wenzelm@10267
   131
\ \ {\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}\isanewline
wenzelm@10267
   132
\isacommand{by}{\isacharparenleft}auto\ elim{\isacharcolon}Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isanewline
wenzelm@10267
   133
\isanewline
wenzelm@10267
   134
\end{isabellebody}%
wenzelm@10267
   135
%%% Local Variables:
wenzelm@10267
   136
%%% mode: latex
wenzelm@10267
   137
%%% TeX-master: "root"
wenzelm@10267
   138
%%% End: