doc-src/TutorialI/CTL/document/CTL.tex
changeset 10159 a72ddfdbfca0
parent 10149 7cfdf6a330a0
child 10171 59d6633835fa
     1.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex	Fri Oct 06 01:21:17 2000 +0200
     1.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex	Fri Oct 06 12:31:53 2000 +0200
     1.3 @@ -14,14 +14,14 @@
     1.4  \begin{isamarkuptext}%
     1.5  \noindent
     1.6  which stands for "always in the future":
     1.7 -on all paths, at some point the formula holds. 
     1.8 -Introducing the notion of paths (in \isa{M})%
     1.9 +on all paths, at some point the formula holds. Formalizing the notion of an infinite path is easy
    1.10 +in HOL: it is simply a function from \isa{nat} to \isa{state}.%
    1.11  \end{isamarkuptext}%
    1.12  \isacommand{constdefs}\ Paths\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}set{\isachardoublequote}\isanewline
    1.13  \ \ \ \ \ \ \ \ \ {\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}%
    1.14  \begin{isamarkuptext}%
    1.15  \noindent
    1.16 -allows a very succinct definition of the semantics of \isa{AF}:
    1.17 +This definition allows a very succinct statement of the semantics of \isa{AF}:
    1.18  \footnote{Do not be mislead: neither datatypes nor recursive functions can be
    1.19  extended by new constructors or equations. This is just a trick of the
    1.20  presentation. In reality one has to define a new datatype and a new function.}%
    1.21 @@ -30,40 +30,81 @@
    1.22  \begin{isamarkuptext}%
    1.23  \noindent
    1.24  Model checking \isa{AF} involves a function which
    1.25 -is just large enough to warrant a separate definition:%
    1.26 +is just complicated enough to warrant a separate definition:%
    1.27  \end{isamarkuptext}%
    1.28  \isacommand{constdefs}\ af\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline
    1.29  \ \ \ \ \ \ \ \ \ {\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}%
    1.30  \begin{isamarkuptext}%
    1.31  \noindent
    1.32 -This function is monotone in its second argument (and also its first, but
    1.33 -that is irrelevant), and hence \isa{af\ A} has a least fixpoint.%
    1.34 +Now we define \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}} as the least set \isa{T} that contains
    1.35 +\isa{mc\ f} and all states all of whose direct successors are in \isa{T}:%
    1.36 +\end{isamarkuptext}%
    1.37 +{\isachardoublequote}mc{\isacharparenleft}AF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}af{\isacharparenleft}mc\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
    1.38 +\begin{isamarkuptext}%
    1.39 +\noindent
    1.40 +Because \isa{af} is monotone in its second argument (and also its first, but
    1.41 +that is irrelevant) \isa{af\ A} has a least fixpoint:%
    1.42  \end{isamarkuptext}%
    1.43  \isacommand{lemma}\ mono{\isacharunderscore}af{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
    1.44  \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ mono{\isacharunderscore}def\ af{\isacharunderscore}def{\isacharparenright}\isanewline
    1.45 -\isacommand{by}{\isacharparenleft}blast{\isacharparenright}%
    1.46 +\isacommand{apply}\ blast\isanewline
    1.47 +\isacommand{done}%
    1.48  \begin{isamarkuptext}%
    1.49 +All we need to prove now is that \isa{mc} and \isa{{\isasymTurnstile}}
    1.50 +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
    1.51 +with the easy one:%
    1.52 +\end{isamarkuptext}%
    1.53 +\isacommand{theorem}\ AF{\isacharunderscore}lemma\isadigit{1}{\isacharcolon}\isanewline
    1.54 +\ \ {\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}%
    1.55 +\begin{isamarkuptxt}%
    1.56  \noindent
    1.57 -Now we can define \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}} as the least set \isa{T} that contains
    1.58 -\isa{mc\ f} and all states all of whose direct successors are in \isa{T}:%
    1.59 -\end{isamarkuptext}%
    1.60 -{\isachardoublequote}mc{\isacharparenleft}AF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}af{\isacharparenleft}mc\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
    1.61 -\isacommand{theorem}\ lfp{\isacharunderscore}subset{\isacharunderscore}AF{\isacharcolon}\isanewline
    1.62 -{\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}\isanewline
    1.63 +The proof is again pointwise. Fixpoint induction on the premise \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} followed
    1.64 +by simplification and clarification%
    1.65 +\end{isamarkuptxt}%
    1.66  \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
    1.67  \isacommand{apply}{\isacharparenleft}erule\ Lfp{\isachardot}induct{\isacharbrackleft}OF\ {\isacharunderscore}\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline
    1.68 -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}\isanewline
    1.69 +\isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}%
    1.70 +\begin{isamarkuptxt}%
    1.71 +\noindent
    1.72 +FIXME OF/of with undescore?
    1.73 +
    1.74 +leads to the following somewhat involved proof state
    1.75 +\begin{isabelle}
    1.76 +\ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline
    1.77 +\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ \isadigit{0}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
    1.78 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymand}\isanewline
    1.79 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\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
    1.80 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
    1.81 +\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
    1.82 +\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A
    1.83 +\end{isabelle}
    1.84 +Now we eliminate the disjunction. The case \isa{p\ \isadigit{0}\ {\isasymin}\ A} is trivial:%
    1.85 +\end{isamarkuptxt}%
    1.86  \isacommand{apply}{\isacharparenleft}erule\ disjE{\isacharparenright}\isanewline
    1.87 -\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
    1.88 -\isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
    1.89 +\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}%
    1.90 +\begin{isamarkuptxt}%
    1.91 +\noindent
    1.92 +In the other case we set \isa{t} to \isa{p\ \isadigit{1}} and simplify matters:%
    1.93 +\end{isamarkuptxt}%
    1.94  \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ \isadigit{1}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
    1.95 -\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isanewline
    1.96 +\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
    1.97 +\begin{isamarkuptxt}%
    1.98 +\begin{isabelle}
    1.99 +\ \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
   1.100 +\ \ \ \ \ \ \ \ \ \ \ {\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
   1.101 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
   1.102 +\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A
   1.103 +\end{isabelle}
   1.104 +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
   1.105 +first element. The rest is practically automatic:%
   1.106 +\end{isamarkuptxt}%
   1.107  \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
   1.108 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   1.109 -\isacommand{by}{\isacharparenleft}blast{\isacharparenright}%
   1.110 +\isacommand{apply}\ simp\isanewline
   1.111 +\isacommand{apply}\ blast\isanewline
   1.112 +\isacommand{done}%
   1.113  \begin{isamarkuptext}%
   1.114 -The opposite direction is proved by contradiction: if some state
   1.115 -{term s} is not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then we can construct an
   1.116 +The opposite containment is proved by contradiction: if some state
   1.117 +\isa{s} is not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then we can construct an
   1.118  infinite \isa{A}-avoiding path starting from \isa{s}. The reason is
   1.119  that by unfolding \isa{lfp} we find that if \isa{s} is not in
   1.120  \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then \isa{s} is not in \isa{A} and there is a
   1.121 @@ -76,7 +117,8 @@
   1.122  \ {\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
   1.123  \isacommand{apply}{\isacharparenleft}erule\ swap{\isacharparenright}\isanewline
   1.124  \isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}Tarski{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline
   1.125 -\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\isacharparenright}%
   1.126 +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\isacharparenright}\isanewline
   1.127 +\isacommand{done}%
   1.128  \begin{isamarkuptext}%
   1.129  \noindent
   1.130  is proved by a variant of contraposition (\isa{swap}:
   1.131 @@ -94,113 +136,149 @@
   1.132  \begin{isamarkuptext}%
   1.133  \noindent
   1.134  Element \isa{n\ {\isacharplus}\ \isadigit{1}} on this path is some arbitrary successor
   1.135 -\isa{t} of element \isa{n} such that \isa{P\ t} holds.  Of
   1.136 +\isa{t} of element \isa{n} such that \isa{P\ t} holds.  Remember that \isa{SOME\ t{\isachardot}\ R\ t}
   1.137 +is some arbitrary but fixed \isa{t} such that \isa{R\ t} holds (see \S\ref{sec-SOME}). Of
   1.138  course, such a \isa{t} may in general not exist, but that is of no
   1.139  concern to us since we will only use \isa{path} in such cases where a
   1.140  suitable \isa{t} does exist.
   1.141  
   1.142 -Now we prove that if each state \isa{s} that satisfies \isa{P}
   1.143 -has a successor that again satisfies \isa{P}, then there exists an infinite \isa{P}-path.%
   1.144 +Let us show that if each state \isa{s} that satisfies \isa{P}
   1.145 +has a successor that again satisfies \isa{P}, then there exists an infinite \isa{P}-path:%
   1.146  \end{isamarkuptext}%
   1.147 -\isacommand{lemma}\ seq{\isacharunderscore}lemma{\isacharcolon}\isanewline
   1.148 -{\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}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}%
   1.149 +\isacommand{lemma}\ infinity{\isacharunderscore}lemma{\isacharcolon}\isanewline
   1.150 +\ \ {\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
   1.151 +\ \ \ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}%
   1.152  \begin{isamarkuptxt}%
   1.153  \noindent
   1.154  First we rephrase the conclusion slightly because we need to prove both the path property
   1.155  and the fact that \isa{P} holds simultaneously:%
   1.156  \end{isamarkuptxt}%
   1.157 -\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}%
   1.158 +\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}%
   1.159 +\begin{isamarkuptxt}%
   1.160 +\noindent
   1.161 +From this proposition the original goal follows easily:%
   1.162 +\end{isamarkuptxt}%
   1.163 +\ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}%
   1.164 +\begin{isamarkuptxt}%
   1.165 +\noindent
   1.166 +The new subgoal is proved by providing the witness \isa{path\ s\ P} for \isa{p}:%
   1.167 +\end{isamarkuptxt}%
   1.168 +\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}path\ s\ P{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
   1.169 +\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
   1.170 +\begin{isamarkuptxt}%
   1.171 +\noindent
   1.172 +After simplification and clarification the subgoal has the following compact form
   1.173 +\begin{isabelle}
   1.174 +\ \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
   1.175 +\ \ \ \ \ \ \ \ {\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
   1.176 +\ \ \ \ \ \ \ \ \ \ \ \ P\ {\isacharparenleft}path\ s\ P\ i{\isacharparenright}
   1.177 +\end{isabelle}
   1.178 +and invites a proof by induction on \isa{i}:%
   1.179 +\end{isamarkuptxt}%
   1.180 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline
   1.181 +\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}%
   1.182  \begin{isamarkuptxt}%
   1.183  \noindent
   1.184 -From this proposition the original goal follows easily%
   1.185 +After simplification the base case boils down to
   1.186 +\begin{isabelle}
   1.187 +\ \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
   1.188 +\ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M
   1.189 +\end{isabelle}
   1.190 +The conclusion looks exceedingly trivial: after all, \isa{t} is chosen such that \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M}
   1.191 +holds. However, we first have to show that such a \isa{t} actually exists! This reasoning
   1.192 +is embodied in the theorem \isa{someI\isadigit{2}{\isacharunderscore}ex}:
   1.193 +\begin{isabelle}%
   1.194 +\ \ \ \ \ {\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}%
   1.195 +\end{isabelle}
   1.196 +When we apply this theorem as an introduction rule, \isa{{\isacharquery}P\ x} becomes
   1.197 +\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
   1.198 +two subgoals: \isa{{\isasymexists}a{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ a{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ a}, which follows from the assumptions, and
   1.199 +\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
   1.200 +\isa{fast} can prove the base case quickly:%
   1.201  \end{isamarkuptxt}%
   1.202 -\ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}\isanewline
   1.203 -\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}path\ s\ P{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
   1.204 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   1.205 -\isacommand{apply}{\isacharparenleft}intro\ strip{\isacharparenright}\isanewline
   1.206 -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline
   1.207 -\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   1.208 -\ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
   1.209 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   1.210 -\isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
   1.211 -\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   1.212 -\isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
   1.213 -\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   1.214 -\isacommand{by}{\isacharparenleft}blast{\isacharparenright}\isanewline
   1.215 -\isanewline
   1.216 -\isacommand{lemma}\ seq{\isacharunderscore}lemma{\isacharcolon}\isanewline
   1.217 -{\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
   1.218 -\ {\isasymexists}\ p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}\ i{\isachardot}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}\isanewline
   1.219 -\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\isanewline
   1.220 -\ {\isachardoublequote}{\isasymexists}\ p{\isachardot}\ s\ {\isacharequal}\ p\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}p{\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}{\isasymin}M\ {\isasymand}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}\isanewline
   1.221 -\ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharparenright}\isanewline
   1.222 -\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   1.223 -\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}nat{\isacharunderscore}rec\ s\ {\isacharparenleft}{\isasymlambda}n\ t{\isachardot}\ SOME\ u{\isachardot}\ {\isacharparenleft}t{\isacharcomma}u{\isacharparenright}{\isasymin}M\ {\isasymand}\ P\ u{\isacharparenright}{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
   1.224 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   1.225 -\isacommand{apply}{\isacharparenleft}intro\ strip{\isacharparenright}\isanewline
   1.226 -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline
   1.227 -\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   1.228 -\ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
   1.229 +\ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}%
   1.230 +\begin{isamarkuptxt}%
   1.231 +\noindent
   1.232 +What is worth noting here is that we have used \isa{fast} rather than \isa{blast}.
   1.233 +The reason is that \isa{blast} would fail because it cannot cope with \isa{someI\isadigit{2}{\isacharunderscore}ex}:
   1.234 +unifying its conclusion with the current subgoal is nontrivial because of the nested schematic
   1.235 +variables. For efficiency reasons \isa{blast} does not even attempt such unifications.
   1.236 +Although \isa{fast} can in principle cope with complicated unification problems, in practice
   1.237 +the number of unifiers arising is often prohibitive and the offending rule may need to be applied
   1.238 +explicitly rather than automatically.
   1.239 +
   1.240 +The induction step is similar, but more involved, because now we face nested occurrences of
   1.241 +\isa{SOME}. We merely show the proof commands but do not describe th details:%
   1.242 +\end{isamarkuptxt}%
   1.243  \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   1.244  \isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
   1.245  \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   1.246  \isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
   1.247  \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   1.248 -\isacommand{by}{\isacharparenleft}blast{\isacharparenright}\isanewline
   1.249 -\isanewline
   1.250 -\isacommand{theorem}\ AF{\isacharunderscore}subset{\isacharunderscore}lfp{\isacharcolon}\isanewline
   1.251 -{\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
   1.252 +\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   1.253 +\isacommand{done}%
   1.254 +\begin{isamarkuptext}%
   1.255 +Function \isa{path} has fulfilled its purpose now and can be forgotten
   1.256 +about. It was merely defined to provide the witness in the proof of the
   1.257 +\isa{infinity{\isacharunderscore}lemma}. Afficionados of minimal proofs might like to know
   1.258 +that we could have given the witness without having to define a new function:
   1.259 +the term
   1.260 +\begin{isabelle}%
   1.261 +\ \ \ \ \ nat{\isacharunderscore}rec\ s\ {\isacharparenleft}{\isasymlambda}n\ t{\isachardot}\ SOME\ u{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ u{\isacharparenright}%
   1.262 +\end{isabelle}
   1.263 +where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}, whose defining
   1.264 +equations we omit, is extensionally equal to \isa{path\ s\ P}.%
   1.265 +\end{isamarkuptext}%
   1.266 +%
   1.267 +\begin{isamarkuptext}%
   1.268 +At last we can prove the opposite direction of \isa{AF{\isacharunderscore}lemma\isadigit{1}}:%
   1.269 +\end{isamarkuptext}%
   1.270 +\isacommand{theorem}\ AF{\isacharunderscore}lemma\isadigit{2}{\isacharcolon}\isanewline
   1.271 +{\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}%
   1.272 +\begin{isamarkuptxt}%
   1.273 +\noindent
   1.274 +The proof is again pointwise and then by contraposition (\isa{contrapos\isadigit{2}} is the rule
   1.275 +\isa{{\isasymlbrakk}{\isacharquery}Q{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P\ {\isasymLongrightarrow}\ {\isasymnot}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P}):%
   1.276 +\end{isamarkuptxt}%
   1.277  \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
   1.278  \isacommand{apply}{\isacharparenleft}erule\ contrapos\isadigit{2}{\isacharparenright}\isanewline
   1.279 -\isacommand{apply}\ simp\isanewline
   1.280 -\isacommand{apply}{\isacharparenleft}drule\ seq{\isacharunderscore}lemma{\isacharparenright}\isanewline
   1.281 -\isacommand{by}{\isacharparenleft}auto\ dest{\isacharcolon}not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline
   1.282 -\isanewline
   1.283 -\isanewline
   1.284 -\isanewline
   1.285 -\isanewline
   1.286 -\isacommand{consts}\ Avoid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline
   1.287 -\isacommand{inductive}\ {\isachardoublequote}Avoid\ s\ A{\isachardoublequote}\isanewline
   1.288 -\isakeyword{intros}\ {\isachardoublequote}s\ {\isasymin}\ Avoid\ s\ A{\isachardoublequote}\isanewline
   1.289 -\ \ \ \ \ \ \ {\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}\isanewline
   1.290 -\isanewline
   1.291 -\isanewline
   1.292 -\isacommand{lemma}\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
   1.293 -{\isachardoublequote}t\ {\isasymin}\ Avoid\ s\ A\ \ {\isasymLongrightarrow}\isanewline
   1.294 -\ {\isasymforall}f{\isachardot}\ t\ {\isacharequal}\ f\ \isadigit{0}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}f\ i{\isacharcomma}\ f\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ f\ i\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ f\ i\ {\isasymnotin}\ A{\isacharparenright}\isanewline
   1.295 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A{\isacharparenright}{\isachardoublequote}\isanewline
   1.296 -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharparenright}\isanewline
   1.297 -\isacommand{apply}{\isacharparenleft}erule\ Avoid{\isachardot}induct{\isacharparenright}\isanewline
   1.298 -\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   1.299 -\isacommand{apply}{\isacharparenleft}rule\ allI{\isacharparenright}\isanewline
   1.300 -\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ case\ i\ of\ \isadigit{0}\ {\isasymRightarrow}\ t\ {\isacharbar}\ Suc\ i\ {\isasymRightarrow}\ f\ i{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
   1.301 -\isacommand{by}{\isacharparenleft}force\ split{\isacharcolon}nat{\isachardot}split{\isacharparenright}\isanewline
   1.302 -\isanewline
   1.303 -\isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline
   1.304 -{\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}\isanewline
   1.305 -\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\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
   1.306 -\ \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline
   1.307 -\ \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isanewline
   1.308 -\ \isacommand{apply}{\isacharparenleft}rule\ ssubst\ {\isacharbrackleft}OF\ lfp{\isacharunderscore}Tarski{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline
   1.309 -\ \isacommand{apply}{\isacharparenleft}unfold\ af{\isacharunderscore}def{\isacharparenright}\isanewline
   1.310 -\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isanewline
   1.311 -\isacommand{apply}{\isacharparenleft}erule\ contrapos\isadigit{2}{\isacharparenright}\isanewline
   1.312 -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline
   1.313 -\isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
   1.314 -\isacommand{apply}{\isacharparenleft}rule\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharparenright}\isanewline
   1.315 -\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
   1.316 -\isanewline
   1.317 -\isacommand{theorem}\ AF{\isacharunderscore}subset{\isacharunderscore}lfp{\isacharcolon}\isanewline
   1.318 -{\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
   1.319 -\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
   1.320 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   1.321 -\isacommand{apply}{\isacharparenleft}erule\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharparenright}\isanewline
   1.322 -\isacommand{by}{\isacharparenleft}rule\ Avoid{\isachardot}intros{\isacharparenright}\isanewline
   1.323 -\isanewline
   1.324 -\isanewline
   1.325 +\isacommand{apply}\ simp%
   1.326 +\begin{isamarkuptxt}%
   1.327 +\begin{isabelle}
   1.328 +\ \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
   1.329 +\end{isabelle}
   1.330 +Applying the \isa{infinity{\isacharunderscore}lemma} as a destruction rule leaves two subgoals, the second
   1.331 +premise of \isa{infinity{\isacharunderscore}lemma} and the original subgoal:%
   1.332 +\end{isamarkuptxt}%
   1.333 +\isacommand{apply}{\isacharparenleft}drule\ infinity{\isacharunderscore}lemma{\isacharparenright}%
   1.334 +\begin{isamarkuptxt}%
   1.335 +\begin{isabelle}
   1.336 +\ \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
   1.337 +\ \isadigit{2}{\isachardot}\ {\isasymAnd}s{\isachardot}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline
   1.338 +\ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A
   1.339 +\end{isabelle}
   1.340 +Both are solved automatically:%
   1.341 +\end{isamarkuptxt}%
   1.342 +\ \isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline
   1.343 +\isacommand{done}%
   1.344 +\begin{isamarkuptext}%
   1.345 +The main theorem is proved as for PDL, except that we also derive the necessary equality
   1.346 +\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}}
   1.347 +on the spot:%
   1.348 +\end{isamarkuptext}%
   1.349  \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline
   1.350  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
   1.351 -\isacommand{by}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma\ equalityI{\isacharbrackleft}OF\ lfp{\isacharunderscore}subset{\isacharunderscore}AF\ AF{\isacharunderscore}subset{\isacharunderscore}lfp{\isacharbrackright}{\isacharparenright}\isanewline
   1.352 +\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
   1.353 +\isacommand{done}%
   1.354 +\begin{isamarkuptext}%
   1.355 +Let us close this section with a few words about the executability of \isa{mc}.
   1.356 +It is clear that if all sets are finite, they can be represented as lists and the usual
   1.357 +set operations are easily implemented. Only \isa{lfp} requires a little thought.
   1.358 +Fortunately the HOL library proves that in the case of finite sets and a monotone \isa{F},
   1.359 +\isa{lfp\ F} can be computed by iterated application of \isa{F} to \isa{{\isacharbraceleft}{\isacharbraceright}} until
   1.360 +a fixpoint is reached. It is possible to generate executable functional programs
   1.361 +from HOL definitions, but that is beyond the scope of the tutorial.%
   1.362 +\end{isamarkuptext}%
   1.363  \end{isabellebody}%
   1.364  %%% Local Variables:
   1.365  %%% mode: latex