doc-src/TutorialI/CTL/document/CTLind.tex

introduced @{const ...} antiquotation

%
\begin{isabellebody}%
\def\isabellecontext{CTLind}%
\isamarkupfalse%
%
\isamarkupsubsection{CTL Revisited%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\label{sec:CTL-revisited}
\index{CTL|(}%
The purpose of this section is twofold: to demonstrate
some of the induction principles and heuristics discussed above and to
show how inductive definitions can simplify proofs.
In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a
model checker for CTL\@. In particular the proof of the
\isa{infinity{\isacharunderscore}lemma} on the way to \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} is not as
simple as one might expect, due to the \isa{SOME} operator
involved. Below we give a simpler proof of \isa{AF{\isacharunderscore}lemma{\isadigit{2}}}
based on an auxiliary inductive definition.

Let us call a (finite or infinite) path \emph{\isa{A}-avoiding} if it does
not touch any node in the set \isa{A}. Then \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} says
that if no infinite path from some state \isa{s} is \isa{A}-avoiding,
then \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. We prove this by inductively defining the set
\isa{Avoid\ s\ A} of states reachable from \isa{s} by a finite \isa{A}-avoiding path:
% Second proof of opposite direction, directly by well-founded induction
% on the initial segment of M that avoids A.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\ Avoid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline
\isamarkupfalse%
\isacommand{inductive}\ {\isachardoublequote}Avoid\ s\ A{\isachardoublequote}\isanewline
\isakeyword{intros}\ {\isachardoublequote}s\ {\isasymin}\ Avoid\ s\ A{\isachardoublequote}\isanewline
\ \ \ \ \ \ \ {\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}\isamarkupfalse%
%
\begin{isamarkuptext}%
It is easy to see that for any infinite \isa{A}-avoiding path \isa{f}
with \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path
starting with \isa{s} because (by definition of \isa{Avoid}) there is a
finite \isa{A}-avoiding path from \isa{s} to \isa{f\ {\isadigit{0}}}.
The proof is by induction on \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A}. However,
this requires the following
reformulation, as explained in \S\ref{sec:ind-var-in-prems} above;
the \isa{rule{\isacharunderscore}format} directive undoes the reformulation after the proof.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequote}t\ {\isasymin}\ Avoid\ s\ A\ \ {\isasymLongrightarrow}\isanewline
\ \ \ {\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
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
The base case (\isa{t\ {\isacharequal}\ s}) is trivial and proved by \isa{blast}.
In the induction step, we have an infinite \isa{A}-avoiding path \isa{f}
starting from \isa{u}, a successor of \isa{t}. Now we simply instantiate
the \isa{{\isasymforall}f{\isasymin}Paths\ t} in the induction hypothesis by the path starting with
\isa{t} and continuing with \isa{f}. That is what the above $\lambda$-term
expresses.  Simplification shows that this is a path starting with \isa{t} 
and that the instantiated induction hypothesis implies the conclusion.

Now we come to the key lemma. Assuming that no infinite \isa{A}-avoiding
path starts from \isa{s}, we want to show \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. For the
inductive proof this must be generalized to the statement that every point \isa{t}
``between'' \isa{s} and \isa{A}, in other words all of \isa{Avoid\ s\ A},
is contained in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\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}\isamarkupfalse%
\isamarkuptrue%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkuptrue%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkuptrue%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive in the
statement of the lemma means
that the assumption is left unchanged; otherwise the \isa{{\isasymforall}p} 
would be turned
into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is,
\isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now
\begin{isabelle}%
\ \ \ \ \ {\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}%
\end{isabelle}
The main theorem is simply the corollary where \isa{t\ {\isacharequal}\ s},
when the assumption \isa{t\ {\isasymin}\ Avoid\ s\ A} is trivially true
by the first \isa{Avoid}-rule. Isabelle confirms this:%
\index{CTL|)}%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\ \ {\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
\isamarkupfalse%
\isanewline
\isamarkupfalse%
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: