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

updated generated files;

%
\begin{isabellebody}%
\def\isabellecontext{PDL}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupsubsection{Propositional Dynamic Logic --- PDL%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\index{PDL|(}
The formulae of PDL are built up from atomic propositions via
negation and conjunction and the two temporal
connectives \isa{AX} and \isa{EF}\@. Since formulae are essentially
syntax trees, they are naturally modelled as a datatype:%
\footnote{The customary definition of PDL
\cite{HarelKT-DL} looks quite different from ours, but the two are easily
shown to be equivalent.}%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{datatype}\isamarkupfalse%
\ formula\ {\isaliteral{3D}{\isacharequal}}\ Atom\ {\isaliteral{22}{\isachardoublequoteopen}}atom{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Neg\ formula\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ And\ formula\ formula\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ AX\ formula\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ EF\ formula%
\begin{isamarkuptext}%
\noindent
This resembles the boolean expression case study in
\S\ref{sec:boolex}.
A validity relation between states and formulae specifies the semantics.
The syntax annotation allows us to write \isa{s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ f} instead of
\hbox{\isa{valid\ s\ f}}. The definition is by recursion over the syntax:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{primrec}\isamarkupfalse%
\ valid\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ formula\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{8}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}{\isadigit{8}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}\ {\isadigit{8}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
\isakeyword{where}\isanewline
{\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ Atom\ a\ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ L\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
{\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ Neg\ f\ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}{\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ f{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
{\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ And\ f\ g\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ f\ {\isaliteral{5C3C616E643E}{\isasymand}}\ s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ g{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
{\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ AX\ f\ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ t\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ f{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
{\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ EF\ f\ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ t\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ f{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
\noindent
The first three equations should be self-explanatory. The temporal formula
\isa{AX\ f} means that \isa{f} is true in \emph{A}ll ne\emph{X}t states whereas
\isa{EF\ f} means that there \emph{E}xists some \emph{F}uture state in which \isa{f} is
true. The future is expressed via \isa{\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}}, the reflexive transitive
closure. Because of reflexivity, the future includes the present.

Now we come to the model checker itself. It maps a formula into the
set of states where the formula is true.  It too is defined by
recursion over the syntax:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{primrec}\isamarkupfalse%
\ mc\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}formula\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ set{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
{\isaliteral{22}{\isachardoublequoteopen}}mc{\isaliteral{28}{\isacharparenleft}}Atom\ a{\isaliteral{29}{\isacharparenright}}\ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}s{\isaliteral{2E}{\isachardot}}\ a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ L\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
{\isaliteral{22}{\isachardoublequoteopen}}mc{\isaliteral{28}{\isacharparenleft}}Neg\ f{\isaliteral{29}{\isacharparenright}}\ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}mc\ f{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
{\isaliteral{22}{\isachardoublequoteopen}}mc{\isaliteral{28}{\isacharparenleft}}And\ f\ g{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ mc\ f\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ mc\ g{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
{\isaliteral{22}{\isachardoublequoteopen}}mc{\isaliteral{28}{\isacharparenleft}}AX\ f{\isaliteral{29}{\isacharparenright}}\ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ \ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ mc\ f{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
{\isaliteral{22}{\isachardoublequoteopen}}mc{\isaliteral{28}{\isacharparenleft}}EF\ f{\isaliteral{29}{\isacharparenright}}\ \ \ \ {\isaliteral{3D}{\isacharequal}}\ lfp{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}T{\isaliteral{2E}{\isachardot}}\ mc\ f\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ {\isaliteral{28}{\isacharparenleft}}M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ T{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
\noindent
Only the equation for \isa{EF} deserves some comments. Remember that the
postfix \isa{{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}} and the infix \isa{{\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}} are predefined and denote the
converse of a relation and the image of a set under a relation.  Thus
\isa{M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ T} is the set of all predecessors of \isa{T} and the least
fixed point (\isa{lfp}) of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}T{\isaliteral{2E}{\isachardot}}\ mc\ f\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ T} is the least set
\isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you
find it hard to see that \isa{mc\ {\isaliteral{28}{\isacharparenleft}}EF\ f{\isaliteral{29}{\isacharparenright}}} contains exactly those states from
which there is a path to a state where \isa{f} is true, do not worry --- this
will be proved in a moment.

First we prove monotonicity of the function inside \isa{lfp}
in order to make sure it really has a least fixed point.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ mono{\isaliteral{5F}{\isacharunderscore}}ef{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}mono{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}T{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ {\isaliteral{28}{\isacharparenleft}}M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ T{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}rule\ monoI{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{apply}\isamarkupfalse%
\ blast\isanewline
\isacommand{done}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
\noindent
Now we can relate model checking and semantics. For the \isa{EF} case we need
a separate lemma:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ EF{\isaliteral{5F}{\isacharunderscore}}lemma{\isaliteral{3A}{\isacharcolon}}\isanewline
\ \ {\isaliteral{22}{\isachardoublequoteopen}}lfp{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}T{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ {\isaliteral{28}{\isacharparenleft}}M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ T{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
%
\begin{isamarkuptxt}%
\noindent
The equality is proved in the canonical fashion by proving that each set
includes the other; the inclusion is shown pointwise:%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}rule\ equalityI{\isaliteral{29}{\isacharparenright}}\isanewline
\ \isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}rule\ subsetI{\isaliteral{29}{\isacharparenright}}\isanewline
\ \isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}%
\begin{isamarkuptxt}%
\noindent
Simplification leaves us with the following first subgoal
\begin{isabelle}%
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}s{\isaliteral{2E}{\isachardot}}\ s\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}T{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ T{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A%
\end{isabelle}
which is proved by \isa{lfp}-induction:%
\end{isamarkuptxt}%
\isamarkuptrue%
\ \isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}erule\ lfp{\isaliteral{5F}{\isacharunderscore}}induct{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ \isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}rule\ mono{\isaliteral{5F}{\isacharunderscore}}ef{\isaliteral{29}{\isacharparenright}}\isanewline
\ \isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}%
\begin{isamarkuptxt}%
\noindent
Having disposed of the monotonicity subgoal,
simplification leaves us with the following goal:
\begin{isabelle}
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymor}\isanewline
\ \ \ \ \ \ \ \ \ x\ {\isasymin}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ {\isacharparenleft}lfp\ {\isacharparenleft}\dots{\isacharparenright}\ {\isasyminter}\ {\isacharbraceleft}x{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A
\end{isabelle}
It is proved by \isa{blast}, using the transitivity of 
\isa{M\isactrlsup {\isacharasterisk}}.%
\end{isamarkuptxt}%
\isamarkuptrue%
\ \isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}blast\ intro{\isaliteral{3A}{\isacharcolon}}\ rtrancl{\isaliteral{5F}{\isacharunderscore}}trans{\isaliteral{29}{\isacharparenright}}%
\begin{isamarkuptxt}%
We now return to the second set inclusion subgoal, which is again proved
pointwise:%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}rule\ subsetI{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{2C}{\isacharcomma}}\ clarify{\isaliteral{29}{\isacharparenright}}%
\begin{isamarkuptxt}%
\noindent
After simplification and clarification we are left with
\begin{isabelle}%
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3B}{\isacharsemicolon}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}T{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ T{\isaliteral{29}{\isacharparenright}}%
\end{isabelle}
This goal is proved by induction on \isa{{\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}}. But since the model
checker works backwards (from \isa{t} to \isa{s}), we cannot use the
induction theorem \isa{rtrancl{\isaliteral{5F}{\isacharunderscore}}induct}: it works in the
forward direction. Fortunately the converse induction theorem
\isa{converse{\isaliteral{5F}{\isacharunderscore}}rtrancl{\isaliteral{5F}{\isacharunderscore}}induct} already exists:
\begin{isabelle}%
\ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3B}{\isacharsemicolon}}\ P\ b{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isaindent{\ \ \ \ \ \ }{\isaliteral{5C3C416E643E}{\isasymAnd}}y\ z{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}z{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3B}{\isacharsemicolon}}\ P\ z{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ y{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
\isaindent{\ \ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ a%
\end{isabelle}
It says that if \isa{{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}} and we know \isa{P\ b} then we can infer
\isa{P\ a} provided each step backwards from a predecessor \isa{z} of
\isa{b} preserves \isa{P}.%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}erule\ converse{\isaliteral{5F}{\isacharunderscore}}rtrancl{\isaliteral{5F}{\isacharunderscore}}induct{\isaliteral{29}{\isacharparenright}}%
\begin{isamarkuptxt}%
\noindent
The base case
\begin{isabelle}%
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ t{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}T{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ T{\isaliteral{29}{\isacharparenright}}%
\end{isabelle}
is solved by unrolling \isa{lfp} once%
\end{isamarkuptxt}%
\isamarkuptrue%
\ \isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}subst\ lfp{\isaliteral{5F}{\isacharunderscore}}unfold{\isaliteral{5B}{\isacharbrackleft}}OF\ mono{\isaliteral{5F}{\isacharunderscore}}ef{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}%
\begin{isamarkuptxt}%
\begin{isabelle}%
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ t{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}T{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ T{\isaliteral{29}{\isacharparenright}}%
\end{isabelle}
and disposing of the resulting trivial subgoal automatically:%
\end{isamarkuptxt}%
\isamarkuptrue%
\ \isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}blast{\isaliteral{29}{\isacharparenright}}%
\begin{isamarkuptxt}%
\noindent
The proof of the induction step is identical to the one for the base case:%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}subst\ lfp{\isaliteral{5F}{\isacharunderscore}}unfold{\isaliteral{5B}{\isacharbrackleft}}OF\ mono{\isaliteral{5F}{\isacharunderscore}}ef{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}blast{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{done}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
The main theorem is proved in the familiar manner: induction followed by
\isa{auto} augmented with the lemma as a simplification rule.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\isamarkupfalse%
\ {\isaliteral{22}{\isachardoublequoteopen}}mc\ f\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}s{\isaliteral{2E}{\isachardot}}\ s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ f{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ f{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{apply}\isamarkupfalse%
{\isaliteral{28}{\isacharparenleft}}auto\ simp\ add{\isaliteral{3A}{\isacharcolon}}\ EF{\isaliteral{5F}{\isacharunderscore}}lemma{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{done}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
\begin{exercise}
\isa{AX} has a dual operator \isa{EN} 
(``there exists a next state such that'')%
\footnote{We cannot use the customary \isa{EX}: it is reserved
as the \textsc{ascii}-equivalent of \isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}}.}
with the intended semantics
\begin{isabelle}%
\ \ \ \ \ s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ EN\ f\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ t\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ f{\isaliteral{29}{\isacharparenright}}%
\end{isabelle}
Fortunately, \isa{EN\ f} can already be expressed as a PDL formula. How?

Show that the semantics for \isa{EF} satisfies the following recursion equation:
\begin{isabelle}%
\ \ \ \ \ s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ EF\ f\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ f\ {\isaliteral{5C3C6F723E}{\isasymor}}\ s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ EN\ {\isaliteral{28}{\isacharparenleft}}EF\ f{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
\end{isabelle}
\end{exercise}
\index{PDL|)}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: