
nipkow@10123: %
nipkow@10123: \begin{isabellebody}%
nipkow@10123: \def\isabellecontext{CTL}%
wenzelm@11866: \isamarkupfalse%
nipkow@10133: %
nipkow@10971: \isamarkupsubsection{Computation Tree Logic --- CTL%
wenzelm@10395: }
wenzelm@11866: \isamarkuptrue%
nipkow@10149: %
nipkow@10149: \begin{isamarkuptext}%
nipkow@10217: \label{sec:CTL}
paulson@11494: \index{CTL|(}%
paulson@10867: The semantics of PDL only needs reflexive transitive closure.
paulson@10867: Let us be adventurous and introduce a more expressive temporal operator.
paulson@10867: We extend the datatype
nipkow@10149: \isa{formula} by a new constructor%
nipkow@10149: \end{isamarkuptext}%
wenzelm@11866: \isamarkuptrue%
wenzelm@11866: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AF\ formula\isamarkupfalse%
wenzelm@11866: %
nipkow@10149: \begin{isamarkuptext}%
nipkow@10149: \noindent
nipkow@10983: which stands for ``\emph{A}lways in the \emph{F}uture'':
nipkow@10983: on all infinite paths, at some point the formula holds.
nipkow@10983: Formalizing the notion of an infinite path is easy
nipkow@10159: in HOL: it is simply a function from \isa{nat} to \isa{state}.%
nipkow@10149: \end{isamarkuptext}%
wenzelm@11866: \isamarkuptrue%
nipkow@10123: \isacommand{constdefs}\ Paths\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}set{\isachardoublequote}\isanewline
wenzelm@11866: \ \ \ \ \ \ \ \ \ {\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}\isamarkupfalse%
wenzelm@11866: %
nipkow@10149: \begin{isamarkuptext}%
nipkow@10149: \noindent
paulson@11494: This definition allows a succinct statement of the semantics of \isa{AF}:
paulson@10867: \footnote{Do not be misled: neither datatypes nor recursive functions can be
nipkow@10149: extended by new constructors or equations. This is just a trick of the
wenzelm@12815: presentation (see \S\ref{sec:doc-prep-suppress}). In reality one has to define
wenzelm@12815: a new datatype and a new function.}%
nipkow@10149: \end{isamarkuptext}%
wenzelm@11866: \isamarkuptrue%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: {\isachardoublequote}s\ {\isasymTurnstile}\ AF\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
wenzelm@11866: %
nipkow@10149: \begin{isamarkuptext}%
nipkow@10149: \noindent
nipkow@10149: Model checking \isa{AF} involves a function which
nipkow@10159: is just complicated enough to warrant a separate definition:%
nipkow@10149: \end{isamarkuptext}%
wenzelm@11866: \isamarkuptrue%
nipkow@10123: \isacommand{constdefs}\ af\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline
wenzelm@11866: \ \ \ \ \ \ \ \ \ {\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}\isamarkupfalse%
wenzelm@11866: %
nipkow@10149: \begin{isamarkuptext}%
nipkow@10149: \noindent
paulson@10867: Now we define \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}} as the least set \isa{T} that includes
nipkow@10159: \isa{mc\ f} and all states all of whose direct successors are in \isa{T}:%
nipkow@10159: \end{isamarkuptext}%
wenzelm@11866: \isamarkuptrue%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: {\isachardoublequote}mc{\isacharparenleft}AF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}af{\isacharparenleft}mc\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
wenzelm@11866: %
nipkow@10159: \begin{isamarkuptext}%
nipkow@10159: \noindent
nipkow@10159: Because \isa{af} is monotone in its second argument (and also its first, but
nipkow@10983: that is irrelevant), \isa{af\ A} has a least fixed point:%
nipkow@10149: \end{isamarkuptext}%
wenzelm@11866: \isamarkuptrue%
nipkow@10123: \isacommand{lemma}\ mono{\isacharunderscore}af{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
wenzelm@11866: \isamarkupfalse%
nipkow@10149: \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ mono{\isacharunderscore}def\ af{\isacharunderscore}def{\isacharparenright}\isanewline
wenzelm@11866: \isamarkupfalse%
nipkow@10159: \isacommand{apply}\ blast\isanewline
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isacommand{done}\isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: %
nipkow@10149: \begin{isamarkuptext}%
paulson@10867: All we need to prove now is  \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ AF\ f{\isacharbraceright}}, which states
paulson@10867: that \isa{mc} and \isa{{\isasymTurnstile}} agree for \isa{AF}\@.
paulson@10867: This time we prove the two inclusions separately, starting
nipkow@10159: with the easy one:%
nipkow@10159: \end{isamarkuptext}%
wenzelm@11866: \isamarkuptrue%
nipkow@10187: \isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{1}}{\isacharcolon}\isanewline
nipkow@12328: \ \ {\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}\isamarkupfalse%
wenzelm@11866: %
nipkow@10159: \begin{isamarkuptxt}%
nipkow@10149: \noindent
paulson@11494: In contrast to the analogous proof for \isa{EF}, and just
paulson@11494: for a change, we do not use fixed point induction.  Park-induction,
paulson@11494: named after David Park, is weaker but sufficient for this proof:
nipkow@10995: \begin{center}
nipkow@10995: \isa{f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S} \hfill (\isa{lfp{\isacharunderscore}lowerbound})
nipkow@10995: \end{center}
nipkow@10225: The instance of the premise \isa{f\ S\ {\isasymsubseteq}\ S} is proved pointwise,
nipkow@10281: a decision that clarification takes for us:%
nipkow@10159: \end{isamarkuptxt}%
wenzelm@11866: \isamarkuptrue%
nipkow@10225: \isacommand{apply}{\isacharparenleft}rule\ lfp{\isacharunderscore}lowerbound{\isacharparenright}\isanewline
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
wenzelm@11866: %
nipkow@10159: \begin{isamarkuptxt}%
nipkow@10363: \begin{isabelle}%
nipkow@10696: \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ {\isadigit{0}}\ {\isasymin}\ A\ {\isasymor}\isanewline
wenzelm@10950: \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}}{\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ {\isadigit{0}}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
wenzelm@10950: \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}{\isasymforall}t{\isachardot}\ }{\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
wenzelm@10950: \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}{\isasymforall}p{\isachardot}\ }{\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
paulson@14379: \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ }{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
wenzelm@10950: \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
nipkow@10159: \end{isabelle}
nipkow@12699: Now we eliminate the disjunction. The case \isa{p\ {\isadigit{0}}\ {\isasymin}\ A} is trivial:%
nipkow@10159: \end{isamarkuptxt}%
wenzelm@11866: \isamarkuptrue%
nipkow@10123: \isacommand{apply}{\isacharparenleft}erule\ disjE{\isacharparenright}\isanewline
wenzelm@11866: \ \isamarkupfalse%
wenzelm@11866: \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isamarkupfalse%
wenzelm@11866: %
nipkow@10159: \begin{isamarkuptxt}%
nipkow@10159: \noindent
nipkow@12699: In the other case we set \isa{t} to \isa{p\ {\isadigit{1}}} and simplify matters:%
nipkow@10159: \end{isamarkuptxt}%
wenzelm@11866: \isamarkuptrue%
nipkow@10187: \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ {\isadigit{1}}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isamarkupfalse%
wenzelm@11866: %
nipkow@10159: \begin{isamarkuptxt}%
nipkow@10363: \begin{isabelle}%
nipkow@10696: \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\isanewline
paulson@14379: \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ }{\isasymforall}pa{\isachardot}\ p\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ pa\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
paulson@14379: \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ {\isasymforall}pa{\isachardot}\ }{\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
wenzelm@10950: \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
nipkow@10159: \end{isabelle}
nipkow@12699: It merely remains to set \isa{pa} to \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}}, that is, 
paulson@11494: \isa{p} without its first element.  The rest is automatic:%
nipkow@10159: \end{isamarkuptxt}%
wenzelm@11866: \isamarkuptrue%
nipkow@10187: \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
wenzelm@11866: \isamarkupfalse%
paulson@11494: \isacommand{apply}\ force\isanewline
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isacommand{done}\isamarkupfalse%
wenzelm@11866: %
nipkow@10123: \begin{isamarkuptext}%
paulson@10867: The opposite inclusion is proved by contradiction: if some state
nipkow@10159: \isa{s} is not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then we can construct an
paulson@11494: infinite \isa{A}-avoiding path starting from~\isa{s}. The reason is
nipkow@10123: that by unfolding \isa{lfp} we find that if \isa{s} is not in
nipkow@10123: \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then \isa{s} is not in \isa{A} and there is a
nipkow@10983: direct successor of \isa{s} that is again not in \mbox{\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}}. Iterating this argument yields the promised infinite
nipkow@10123: \isa{A}-avoiding path. Let us formalize this sketch.
nipkow@10123: 
paulson@10867: The one-step argument in the sketch above
paulson@10867: is proved by a variant of contraposition:%
nipkow@10123: \end{isamarkuptext}%
wenzelm@11866: \isamarkuptrue%
nipkow@10123: \isacommand{lemma}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharcolon}\isanewline
nipkow@10983: \ {\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
wenzelm@11866: \isamarkupfalse%
nipkow@10237: \isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}np{\isacharparenright}\isanewline
wenzelm@11866: \isamarkupfalse%
nipkow@11231: \isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline
wenzelm@11866: \isamarkupfalse%
wenzelm@12815: \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isacommand{done}\isamarkupfalse%
wenzelm@11866: %
nipkow@10123: \begin{isamarkuptext}%
nipkow@10123: \noindent
paulson@10867: We assume the negation of the conclusion and prove \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}.
nipkow@10237: Unfolding \isa{lfp} once and
nipkow@10123: simplifying with the definition of \isa{af} finishes the proof.
nipkow@10123: 
nipkow@10123: Now we iterate this process. The following construction of the desired
nipkow@10895: path is parameterized by a predicate \isa{Q} that should hold along the path:%
nipkow@10123: \end{isamarkuptext}%
wenzelm@11866: \isamarkuptrue%
nipkow@10123: \isacommand{consts}\ path\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}state\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}{\isachardoublequote}\isanewline
wenzelm@11866: \isamarkupfalse%
nipkow@10123: \isacommand{primrec}\isanewline
nipkow@10895: {\isachardoublequote}path\ s\ Q\ {\isadigit{0}}\ {\isacharequal}\ s{\isachardoublequote}\isanewline
wenzelm@11866: {\isachardoublequote}path\ s\ Q\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ Q\ n{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
wenzelm@11866: %
nipkow@10123: \begin{isamarkuptext}%
nipkow@10123: \noindent
nipkow@12699: Element \isa{n\ {\isacharplus}\ {\isadigit{1}}} on this path is some arbitrary successor
nipkow@10895: \isa{t} of element \isa{n} such that \isa{Q\ t} holds.  Remember that \isa{SOME\ t{\isachardot}\ R\ t}
nipkow@10654: is some arbitrary but fixed \isa{t} such that \isa{R\ t} holds (see \S\ref{sec:SOME}). Of
paulson@10867: course, such a \isa{t} need not exist, but that is of no
paulson@10867: concern to us since we will only use \isa{path} when a
nipkow@10123: suitable \isa{t} does exist.
nipkow@10123: 
nipkow@10895: Let us show that if each state \isa{s} that satisfies \isa{Q}
nipkow@10895: has a successor that again satisfies \isa{Q}, then there exists an infinite \isa{Q}-path:%
nipkow@10123: \end{isamarkuptext}%
wenzelm@11866: \isamarkuptrue%
nipkow@10159: \isacommand{lemma}\ infinity{\isacharunderscore}lemma{\isacharcolon}\isanewline
nipkow@10895: \ \ {\isachardoublequote}{\isasymlbrakk}\ Q\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ Q\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\isanewline
wenzelm@11866: \ \ \ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
wenzelm@11866: %
nipkow@10123: \begin{isamarkuptxt}%
nipkow@10123: \noindent
nipkow@10983: First we rephrase the conclusion slightly because we need to prove simultaneously
nipkow@10983: both the path property and the fact that \isa{Q} holds:%
nipkow@10123: \end{isamarkuptxt}%
wenzelm@11866: \isamarkuptrue%
nipkow@12489: \isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\isanewline
nipkow@12489: \ \ {\isachardoublequote}{\isasymexists}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
wenzelm@11866: %
nipkow@10123: \begin{isamarkuptxt}%
nipkow@10123: \noindent
nipkow@10159: From this proposition the original goal follows easily:%
nipkow@10123: \end{isamarkuptxt}%
wenzelm@11866: \ \isamarkuptrue%
wenzelm@12815: \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}\isamarkupfalse%
wenzelm@11866: %
nipkow@10159: \begin{isamarkuptxt}%
nipkow@10159: \noindent
nipkow@10895: The new subgoal is proved by providing the witness \isa{path\ s\ Q} for \isa{p}:%
nipkow@10159: \end{isamarkuptxt}%
wenzelm@11866: \isamarkuptrue%
nipkow@10895: \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}path\ s\ Q{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isamarkupfalse%
wenzelm@11866: %
nipkow@10159: \begin{isamarkuptxt}%
nipkow@10159: \noindent
paulson@11494: After simplification and clarification, the subgoal has the following form:
nipkow@10363: \begin{isabelle}%
nipkow@10895: \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}Q\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ Q\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}{\isasymrbrakk}\isanewline
wenzelm@10950: \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ }{\isasymLongrightarrow}\ {\isacharparenleft}path\ s\ Q\ i{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ Q\ i{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\isanewline
wenzelm@10950: \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymLongrightarrow}\ }Q\ {\isacharparenleft}path\ s\ Q\ i{\isacharparenright}%
nipkow@10159: \end{isabelle}
paulson@11494: It invites a proof by induction on \isa{i}:%
nipkow@10159: \end{isamarkuptxt}%
wenzelm@11866: \isamarkuptrue%
nipkow@10123: \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline
wenzelm@11866: \ \isamarkupfalse%
wenzelm@11866: \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse%
wenzelm@11866: %
nipkow@10159: \begin{isamarkuptxt}%
nipkow@10159: \noindent
nipkow@10983: After simplification, the base case boils down to
nipkow@10363: \begin{isabelle}%
nipkow@10895: \ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}Q\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ Q\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}{\isasymrbrakk}\isanewline
wenzelm@10950: \isaindent{\ {\isadigit{1}}{\isachardot}\ }{\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}\ {\isasymin}\ M%
nipkow@10159: \end{isabelle}
nipkow@10159: The conclusion looks exceedingly trivial: after all, \isa{t} is chosen such that \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M}
nipkow@10159: holds. However, we first have to show that such a \isa{t} actually exists! This reasoning
nipkow@10187: is embodied in the theorem \isa{someI{\isadigit{2}}{\isacharunderscore}ex}:
nipkow@10159: \begin{isabelle}%
nipkow@10696: \ \ \ \ \ {\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: \end{isabelle}
nipkow@10159: When we apply this theorem as an introduction rule, \isa{{\isacharquery}P\ x} becomes
nipkow@10895: \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ x} and \isa{{\isacharquery}Q\ x} becomes \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M} and we have to prove
nipkow@10895: two subgoals: \isa{{\isasymexists}a{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ a{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ a}, which follows from the assumptions, and
nipkow@10895: \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ x\ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M}, which is trivial. Thus it is not surprising that
nipkow@10159: \isa{fast} can prove the base case quickly:%
nipkow@10159: \end{isamarkuptxt}%
wenzelm@11866: \ \isamarkuptrue%
wenzelm@12815: \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isamarkupfalse%
wenzelm@11866: %
nipkow@10159: \begin{isamarkuptxt}%
nipkow@10159: \noindent
paulson@11494: What is worth noting here is that we have used \methdx{fast} rather than
nipkow@10212: \isa{blast}.  The reason is that \isa{blast} would fail because it cannot
nipkow@10212: cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}: unifying its conclusion with the current
nipkow@11149: subgoal is non-trivial because of the nested schematic variables. For
nipkow@10212: efficiency reasons \isa{blast} does not even attempt such unifications.
nipkow@10212: Although \isa{fast} can in principle cope with complicated unification
nipkow@10212: problems, in practice the number of unifiers arising is often prohibitive and
nipkow@10212: the offending rule may need to be applied explicitly rather than
nipkow@10212: automatically. This is what happens in the step case.
nipkow@10159: 
nipkow@10212: The induction step is similar, but more involved, because now we face nested
nipkow@10212: occurrences of \isa{SOME}. As a result, \isa{fast} is no longer able to
nipkow@10212: solve the subgoal and we apply \isa{someI{\isadigit{2}}{\isacharunderscore}ex} by hand.  We merely
nipkow@10212: show the proof commands but do not describe the details:%
nipkow@10159: \end{isamarkuptxt}%
wenzelm@11866: \isamarkuptrue%
nipkow@10123: \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
wenzelm@11866: \isamarkupfalse%
nipkow@10187: \isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline
wenzelm@11866: \ \isamarkupfalse%
wenzelm@11866: \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
wenzelm@11866: \isamarkupfalse%
nipkow@10187: \isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline
wenzelm@11866: \ \isamarkupfalse%
nipkow@10159: \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isacommand{done}\isamarkupfalse%
wenzelm@11866: %
nipkow@10159: \begin{isamarkuptext}%
paulson@10867: Function \isa{path} has fulfilled its purpose now and can be forgotten.
paulson@10867: It was merely defined to provide the witness in the proof of the
nipkow@10171: \isa{infinity{\isacharunderscore}lemma}. Aficionados of minimal proofs might like to know
nipkow@10159: that we could have given the witness without having to define a new function:
nipkow@10159: the term
nipkow@10159: \begin{isabelle}%
nipkow@10895: \ \ \ \ \ nat{\isacharunderscore}rec\ s\ {\isacharparenleft}{\isasymlambda}n\ t{\isachardot}\ SOME\ u{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ u{\isacharparenright}%
nipkow@10159: \end{isabelle}
nipkow@10895: is extensionally equal to \isa{path\ s\ Q},
paulson@10867: where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}.%
nipkow@10159: \end{isamarkuptext}%
wenzelm@11866: \isamarkuptrue%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
nipkow@10159: %
nipkow@10159: \begin{isamarkuptext}%
nipkow@10187: At last we can prove the opposite direction of \isa{AF{\isacharunderscore}lemma{\isadigit{1}}}:%
nipkow@10159: \end{isamarkuptext}%
wenzelm@11866: \isamarkuptrue%
nipkow@12328: \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}\isamarkupfalse%
wenzelm@11866: %
nipkow@10159: \begin{isamarkuptxt}%
nipkow@10159: \noindent
nipkow@10237: The proof is again pointwise and then by contraposition:%
nipkow@10159: \end{isamarkuptxt}%
wenzelm@11866: \isamarkuptrue%
nipkow@10123: \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
wenzelm@11866: \isamarkupfalse%
nipkow@10237: \isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isacommand{apply}\ simp\isamarkupfalse%
wenzelm@11866: %
nipkow@10159: \begin{isamarkuptxt}%
nipkow@10363: \begin{isabelle}%
nipkow@10363: \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ x{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A%
nipkow@10159: \end{isabelle}
nipkow@10159: Applying the \isa{infinity{\isacharunderscore}lemma} as a destruction rule leaves two subgoals, the second
nipkow@10159: premise of \isa{infinity{\isacharunderscore}lemma} and the original subgoal:%
nipkow@10159: \end{isamarkuptxt}%
wenzelm@11866: \isamarkuptrue%
wenzelm@11866: \isacommand{apply}{\isacharparenleft}drule\ infinity{\isacharunderscore}lemma{\isacharparenright}\isamarkupfalse%
wenzelm@11866: %
nipkow@10159: \begin{isamarkuptxt}%
nipkow@10363: \begin{isabelle}%
nipkow@10363: \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\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@10363: \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isasymexists}p{\isasymin}Paths\ x{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
wenzelm@10950: \isaindent{\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }{\isasymexists}p{\isasymin}Paths\ x{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A%
nipkow@10159: \end{isabelle}
nipkow@10159: Both are solved automatically:%
nipkow@10159: \end{isamarkuptxt}%
wenzelm@11866: \ \isamarkuptrue%
wenzelm@12815: \isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isacommand{done}\isamarkupfalse%
wenzelm@11866: %
nipkow@10159: \begin{isamarkuptext}%
paulson@10867: If you find these proofs too complicated, we recommend that you read
paulson@10867: \S\ref{sec:CTL-revisited}, where we show how inductive definitions lead to
nipkow@10217: simpler arguments.
nipkow@10217: 
nipkow@10217: The main theorem is proved as for PDL, except that we also derive the
nipkow@10217: necessary equality \isa{lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isacharequal}\ {\isachardot}{\isachardot}{\isachardot}} by combining
nipkow@10217: \isa{AF{\isacharunderscore}lemma{\isadigit{1}}} and \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} on the spot:%
nipkow@10159: \end{isamarkuptext}%
wenzelm@11866: \isamarkuptrue%
nipkow@10123: \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline
wenzelm@11866: \isamarkupfalse%
nipkow@10123: \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
wenzelm@11866: \isamarkupfalse%
nipkow@10187: \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
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isacommand{done}\isamarkupfalse%
wenzelm@11866: %
nipkow@10159: \begin{isamarkuptext}%
paulson@10867: The language defined above is not quite CTL\@. The latter also includes an
nipkow@10983: until-operator \isa{EU\ f\ g} with semantics ``there \emph{E}xists a path
paulson@11494: where \isa{f} is true \emph{U}ntil \isa{g} becomes true''.  We need
paulson@11494: an auxiliary function:%
nipkow@10281: \end{isamarkuptext}%
wenzelm@11866: \isamarkuptrue%
nipkow@10281: \isacommand{consts}\ until{\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ {\isasymRightarrow}\ state\ list\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
wenzelm@11866: \isamarkupfalse%
nipkow@10281: \isacommand{primrec}\isanewline
nipkow@10281: {\isachardoublequote}until\ A\ B\ s\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ B{\isacharparenright}{\isachardoublequote}\isanewline
wenzelm@11866: {\isachardoublequote}until\ A\ B\ s\ {\isacharparenleft}t{\isacharhash}p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ A\ {\isasymand}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ until\ A\ B\ t\ p{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: %
nipkow@10281: \begin{isamarkuptext}%
nipkow@10281: \noindent
paulson@11494: Expressing the semantics of \isa{EU} is now straightforward:
nipkow@10171: \begin{isabelle}%
nipkow@10983: \ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ until\ {\isacharbraceleft}t{\isachardot}\ t\ {\isasymTurnstile}\ f{\isacharbraceright}\ {\isacharbraceleft}t{\isachardot}\ t\ {\isasymTurnstile}\ g{\isacharbraceright}\ s\ p{\isacharparenright}%
nipkow@10171: \end{isabelle}
nipkow@10281: Note that \isa{EU} is not definable in terms of the other operators!
nipkow@10281: 
nipkow@10281: Model checking \isa{EU} is again a least fixed point construction:
nipkow@10171: \begin{isabelle}%
nipkow@10839: \ \ \ \ \ mc{\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ g\ {\isasymunion}\ mc\ f\ {\isasyminter}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}%
nipkow@10171: \end{isabelle}
nipkow@10281: 
nipkow@10281: \begin{exercise}
nipkow@10281: Extend the datatype of formulae by the above until operator
nipkow@10281: and prove the equivalence between semantics and model checking, i.e.\ that
nipkow@10186: \begin{isabelle}%
nipkow@10186: \ \ \ \ \ mc\ {\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ EU\ f\ g{\isacharbraceright}%
nipkow@10186: \end{isabelle}
nipkow@10186: %For readability you may want to annotate {term EU} with its customary syntax
nipkow@10186: %{text[display]"| EU formula formula    E[_ U _]"}
nipkow@10186: %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
nipkow@10186: \end{exercise}
paulson@10867: For more CTL exercises see, for example, Huth and Ryan \cite{Huth-Ryan-book}.%
nipkow@10281: \end{isamarkuptext}%
wenzelm@11866: \isamarkuptrue%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
wenzelm@11866: \isamarkupfalse%
nipkow@10281: %
nipkow@10281: \begin{isamarkuptext}%
nipkow@12334: Let us close this section with a few words about the executability of
nipkow@12334: our model checkers.  It is clear that if all sets are finite, they can be
nipkow@12334: represented as lists and the usual set operations are easily
nipkow@12334: implemented. Only \isa{lfp} requires a little thought.  Fortunately, theory
nipkow@12473: \isa{While{\isacharunderscore}Combinator} in the Library~\cite{HOL-Library} provides a
nipkow@12334: theorem stating that in the case of finite sets and a monotone
nipkow@12334: function~\isa{F}, the value of \mbox{\isa{lfp\ F}} can be computed by
nipkow@12334: iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until a fixed point is
nipkow@12334: reached. It is actually possible to generate executable functional programs
nipkow@10159: from HOL definitions, but that is beyond the scope of the tutorial.%
paulson@11494: \index{CTL|)}%
nipkow@10159: \end{isamarkuptext}%
wenzelm@11866: \isamarkuptrue%
wenzelm@11866: \isamarkupfalse%
nipkow@10123: \end{isabellebody}%
nipkow@10123: %%% Local Variables:
nipkow@10123: %%% mode: latex
nipkow@10123: %%% TeX-master: "root"
nipkow@10123: %%% End:




