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

-%
-\begin{isabellebody}%
-\def\isabellecontext{CTLind}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupsubsection{CTL Revisited%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\label{sec:CTL-revisited}
-\index{CTL|(}%
-The purpose of this section is twofold: to demonstrate
-some of the induction principles and heuristics discussed above and to
-show how inductive definitions can simplify proofs.
-In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a
-model checker for CTL\@. In particular the proof of the
-\isa{infinity{\isaliteral{5F}{\isacharunderscore}}lemma} on the way to \isa{AF{\isaliteral{5F}{\isacharunderscore}}lemma{\isadigit{2}}} is not as
-simple as one might expect, due to the \isa{SOME} operator
-involved. Below we give a simpler proof of \isa{AF{\isaliteral{5F}{\isacharunderscore}}lemma{\isadigit{2}}}
-based on an auxiliary inductive definition.
-
-Let us call a (finite or infinite) path \emph{\isa{A}-avoiding} if it does
-not touch any node in the set \isa{A}. Then \isa{AF{\isaliteral{5F}{\isacharunderscore}}lemma{\isadigit{2}}} says
-that if no infinite path from some state \isa{s} is \isa{A}-avoiding,
-then \isa{s\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}}. We prove this by inductively defining the set
-\isa{Avoid\ s\ A} of states reachable from \isa{s} by a finite \isa{A}-avoiding path:
-% Second proof of opposite direction, directly by well-founded induction
-% on the initial segment of M that avoids A.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse%
-\isanewline
-\ \ Avoid\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isakeyword{for}\ s\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ state\ \isakeyword{and}\ A\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isakeyword{where}\isanewline
-\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A{\isaliteral{3B}{\isacharsemicolon}}\ t\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}u{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ u\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-It is easy to see that for any infinite \isa{A}-avoiding path \isa{f}
-with \isa{f\ {\isadigit{0}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path
-starting with \isa{s} because (by definition of \isa{Avoid}) there is a
-finite \isa{A}-avoiding path from \isa{s} to \isa{f\ {\isadigit{0}}}.
-The proof is by induction on \isa{f\ {\isadigit{0}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A}. However,
-this requires the following
-reformulation, as explained in \S\ref{sec:ind-var-in-prems} above;
-the \isa{rule{\isaliteral{5F}{\isacharunderscore}}format} directive undoes the reformulation after the proof.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ ex{\isaliteral{5F}{\isacharunderscore}}infinite{\isaliteral{5F}{\isacharunderscore}}path{\isaliteral{5B}{\isacharbrackleft}}rule{\isaliteral{5F}{\isacharunderscore}}format{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A\ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline
-\ \ \ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}f{\isaliteral{5C3C696E3E}{\isasymin}}Paths\ t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ f\ i\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}p{\isaliteral{5C3C696E3E}{\isasymin}}Paths\ s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ p\ i\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}erule\ Avoid{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}blast{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}clarify{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}drule{\isaliteral{5F}{\isacharunderscore}}tac\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}i{\isaliteral{2E}{\isachardot}}\ case\ i\ of\ {\isadigit{0}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ t\ {\isaliteral{7C}{\isacharbar}}\ Suc\ i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ f\ i{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{in}\ bspec{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ Paths{\isaliteral{5F}{\isacharunderscore}}def\ split{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{2E}{\isachardot}}split{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{done}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent
-The base case (\isa{t\ {\isaliteral{3D}{\isacharequal}}\ s}) is trivial and proved by \isa{blast}.
-In the induction step, we have an infinite \isa{A}-avoiding path \isa{f}
-starting from \isa{u}, a successor of \isa{t}. Now we simply instantiate
-the \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}f{\isaliteral{5C3C696E3E}{\isasymin}}Paths\ t} in the induction hypothesis by the path starting with
-\isa{t} and continuing with \isa{f}. That is what the above $\lambda$-term
-expresses.  Simplification shows that this is a path starting with \isa{t} 
-and that the instantiated induction hypothesis implies the conclusion.
-
-Now we come to the key lemma. Assuming that no infinite \isa{A}-avoiding
-path starts from \isa{s}, we want to show \isa{s\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}}. For the
-inductive proof this must be generalized to the statement that every point \isa{t}
-``between'' \isa{s} and \isa{A}, in other words all of \isa{Avoid\ s\ A},
-is contained in \isa{lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ Avoid{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{5F}{\isacharunderscore}}lfp{\isaliteral{5B}{\isacharbrackleft}}rule{\isaliteral{5F}{\isacharunderscore}}format{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}p{\isaliteral{5C3C696E3E}{\isasymin}}Paths\ s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}i{\isaliteral{2E}{\isachardot}}\ p\ i\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp{\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\begin{isamarkuptxt}%
-\noindent
-The proof is by induction on the ``distance'' between \isa{t} and \isa{A}. Remember that \isa{lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}}.
-If \isa{t} is already in \isa{A}, then \isa{t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}} is
-trivial. If \isa{t} is not in \isa{A} but all successors are in
-\isa{lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}} (induction hypothesis), then \isa{t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}} is
-again trivial.
-
-The formal counterpart of this proof sketch is a well-founded induction
-on~\isa{M} restricted to \isa{Avoid\ s\ A\ {\isaliteral{2D}{\isacharminus}}\ A}, roughly speaking:
-\begin{isabelle}%
-\ \ \ \ \ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A{\isaliteral{7D}{\isacharbraceright}}%
-\end{isabelle}
-As we shall see presently, the absence of infinite \isa{A}-avoiding paths
-starting from \isa{s} implies well-foundedness of this relation. For the
-moment we assume this and proceed with the induction:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}subgoal{\isaliteral{5F}{\isacharunderscore}}tac\ {\isaliteral{22}{\isachardoublequoteopen}}wf{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}x{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}erule{\isaliteral{5F}{\isacharunderscore}}tac\ a\ {\isaliteral{3D}{\isacharequal}}\ t\ \isakeyword{in}\ wf{\isaliteral{5F}{\isacharunderscore}}induct{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}clarsimp{\isaliteral{29}{\isacharparenright}}%
-\begin{isamarkuptxt}%
-\noindent
-\begin{isabelle}%
-\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}p{\isaliteral{5C3C696E3E}{\isasymin}}Paths\ s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}i{\isaliteral{2E}{\isachardot}}\ p\ i\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}t{\isaliteral{2E}{\isachardot}}\ \ }{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ t\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\isanewline
-\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}t{\isaliteral{2E}{\isachardot}}\ \ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ }y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}t{\isaliteral{2E}{\isachardot}}\ \ }t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
-\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}t{\isaliteral{2E}{\isachardot}}\ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}\isanewline
-\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}p{\isaliteral{5C3C696E3E}{\isasymin}}Paths\ s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}i{\isaliteral{2E}{\isachardot}}\ p\ i\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline
-\isaindent{\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ }wf\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A{\isaliteral{7D}{\isacharbraceright}}%
-\end{isabelle}
-Now the induction hypothesis states that if \isa{t\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A}
-then all successors of \isa{t} that are in \isa{Avoid\ s\ A} are in
-\isa{lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}}. Unfolding \isa{lfp} in the conclusion of the first
-subgoal once, we have to prove that \isa{t} is in \isa{A} or all successors
-of \isa{t} are in \isa{lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}}.  But if \isa{t} is not in \isa{A},
-the second 
-\isa{Avoid}-rule implies that all successors of \isa{t} are in
-\isa{Avoid\ s\ A}, because we also assume \isa{t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A}.
-Hence, by the induction hypothesis, all successors of \isa{t} are indeed in
-\isa{lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}}. Mechanically:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\ \isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}subst\ lfp{\isaliteral{5F}{\isacharunderscore}}unfold{\isaliteral{5B}{\isacharbrackleft}}OF\ mono{\isaliteral{5F}{\isacharunderscore}}af{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}simp\ {\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{29}{\isacharparenright}}\ add{\isaliteral{3A}{\isacharcolon}}\ af{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}blast\ intro{\isaliteral{3A}{\isacharcolon}}\ Avoid{\isaliteral{2E}{\isachardot}}intros{\isaliteral{29}{\isacharparenright}}%
-\begin{isamarkuptxt}%
-Having proved the main goal, we return to the proof obligation that the 
-relation used above is indeed well-founded. This is proved by contradiction: if
-the relation is not well-founded then there exists an infinite \isa{A}-avoiding path all in \isa{Avoid\ s\ A}, by theorem
-\isa{wf{\isaliteral{5F}{\isacharunderscore}}iff{\isaliteral{5F}{\isacharunderscore}}no{\isaliteral{5F}{\isacharunderscore}}infinite{\isaliteral{5F}{\isacharunderscore}}down{\isaliteral{5F}{\isacharunderscore}}chain}:
-\begin{isabelle}%
-\ \ \ \ \ wf\ r\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}f{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}Suc\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ f\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
-\end{isabelle}
-From lemma \isa{ex{\isaliteral{5F}{\isacharunderscore}}infinite{\isaliteral{5F}{\isacharunderscore}}path} the existence of an infinite
-\isa{A}-avoiding path starting in \isa{s} follows, contradiction.%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}erule\ contrapos{\isaliteral{5F}{\isacharunderscore}}pp{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ wf{\isaliteral{5F}{\isacharunderscore}}iff{\isaliteral{5F}{\isacharunderscore}}no{\isaliteral{5F}{\isacharunderscore}}infinite{\isaliteral{5F}{\isacharunderscore}}down{\isaliteral{5F}{\isacharunderscore}}chain{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}erule\ exE{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}rule\ ex{\isaliteral{5F}{\isacharunderscore}}infinite{\isaliteral{5F}{\isacharunderscore}}path{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}auto\ simp\ add{\isaliteral{3A}{\isacharcolon}}\ Paths{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{done}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-The \isa{{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{29}{\isacharparenright}}} modifier of the \isa{rule{\isaliteral{5F}{\isacharunderscore}}format} directive in the
-statement of the lemma means
-that the assumption is left unchanged; otherwise the \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}p} 
-would be turned
-into a \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}p}, which would complicate matters below. As it is,
-\isa{Avoid{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{5F}{\isacharunderscore}}lfp} is now
-\begin{isabelle}%
-\ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}p{\isaliteral{5C3C696E3E}{\isasymin}}Paths\ s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}i{\isaliteral{2E}{\isachardot}}\ p\ i\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{3B}{\isacharsemicolon}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}%
-\end{isabelle}
-The main theorem is simply the corollary where \isa{t\ {\isaliteral{3D}{\isacharequal}}\ s},
-when the assumption \isa{t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Avoid\ s\ A} is trivially true
-by the first \isa{Avoid}-rule. Isabelle confirms this:%
-\index{CTL|)}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{theorem}\isamarkupfalse%
-\ AF{\isaliteral{5F}{\isacharunderscore}}lemma{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}p\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Paths\ s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}\ i{\isaliteral{2E}{\isachardot}}\ p\ i\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ lfp{\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}auto\ elim{\isaliteral{3A}{\isacharcolon}}\ Avoid{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{5F}{\isacharunderscore}}lfp\ intro{\isaliteral{3A}{\isacharcolon}}\ Avoid{\isaliteral{2E}{\isachardot}}intros{\isaliteral{29}{\isacharparenright}}\isanewline
-\isanewline
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: