1.1 --- a/doc-src/TutorialI/CTL/document/CTLind.tex Mon Mar 05 15:47:11 2001 +0100
1.2 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex Wed Mar 07 15:54:11 2001 +0100
1.3 @@ -58,56 +58,57 @@
1.4 expresses. Simplification shows that this is a path starting with \isa{t}
1.5 and that the instantiated induction hypothesis implies the conclusion.
1.6
1.7 -Now we come to the key lemma. It says that if \isa{t} can be reached by a
1.8 -finite \isa{A}-avoiding path from \isa{s}, then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}},
1.9 -provided there is no infinite \isa{A}-avoiding path starting from \isa{s}.%
1.10 +Now we come to the key lemma. Assuming that no infinite \isa{A}-avoiding
1.11 +path starts from \isa{s}, we want to show \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. This
1.12 +can be generalized by proving that every point \isa{t} ``between''
1.13 +\isa{s} and \isa{A}, i.e.\ all of \isa{Avoid\ s\ A},
1.14 +is contained in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}:%
1.15 \end{isamarkuptext}%
1.16 \isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline
1.17 \ \ {\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}%
1.18 \begin{isamarkuptxt}%
1.19 \noindent
1.20 -The trick is not to induct on \isa{t\ {\isasymin}\ Avoid\ s\ A}, as even the base
1.21 -case would be a problem, but to proceed by well-founded induction on~\isa{t}. Hence\hbox{ \isa{t\ {\isasymin}\ Avoid\ s\ A}} must be brought into the conclusion as
1.22 -well, which the directive \isa{rule{\isacharunderscore}format} undoes at the end (see below).
1.23 -But induction with respect to which well-founded relation? The
1.24 -one we want is the restriction
1.25 -of \isa{M} to \isa{Avoid\ s\ A}:
1.26 +The proof is by induction on the ``distance'' between \isa{t} and \isa{A}. Remember that \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isacharequal}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}.
1.27 +If \isa{t} is already in \isa{A}, then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} is
1.28 +trivial. If \isa{t} is not in \isa{A} but all successors are in
1.29 +\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}} (induction hypothesis), then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} is
1.30 +again trivial.
1.31 +
1.32 +The formal counterpart of this proof sketch is a well-founded induction
1.33 +w.r.t.\ \isa{M} restricted to (roughly speaking) \isa{Avoid\ s\ A\ {\isacharminus}\ A}:
1.34 \begin{isabelle}%
1.35 -\ \ \ \ \ {\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}%
1.36 +\ \ \ \ \ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}%
1.37 \end{isabelle}
1.38 As we shall see in a moment, the absence of infinite \isa{A}-avoiding paths
1.39 starting from \isa{s} implies well-foundedness of this relation. For the
1.40 moment we assume this and proceed with the induction:%
1.41 \end{isamarkuptxt}%
1.42 -\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\isanewline
1.43 -\ \ {\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.44 +\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}\ x\ {\isasymnotin}\ A{\isacharbraceright}{\isachardoublequote}{\isacharparenright}\isanewline
1.45 \ \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline
1.46 \ \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
1.47 \begin{isamarkuptxt}%
1.48 \noindent
1.49 \begin{isabelle}%
1.50 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\ x\ {\isasymin}\ Avoid\ s\ A{\isacharsemicolon}\isanewline
1.51 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ \ \ \ }{\isasymforall}y{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ y\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A\ {\isasymlongrightarrow}\isanewline
1.52 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ \ \ \ {\isasymforall}y{\isachardot}\ }y\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isasymrbrakk}\isanewline
1.53 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }{\isasymLongrightarrow}\ x\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline
1.54 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\ t\ {\isasymin}\ Avoid\ s\ A{\isacharsemicolon}\isanewline
1.55 +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ \ \ }{\isasymforall}y{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ A\ {\isasymlongrightarrow}\isanewline
1.56 +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ \ \ {\isasymforall}y{\isachardot}\ }y\ {\isasymin}\ Avoid\ s\ A\ {\isasymlongrightarrow}\ y\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isasymrbrakk}\isanewline
1.57 +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ }{\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline
1.58 \ {\isadigit{2}}{\isachardot}\ {\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\isanewline
1.59 -\isaindent{\ {\isadigit{2}}{\isachardot}\ }wf\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\isanewline
1.60 -\isaindent{\ {\isadigit{2}}{\isachardot}\ wf\ \ }{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ y\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}%
1.61 +\isaindent{\ {\isadigit{2}}{\isachardot}\ }wf\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}%
1.62 \end{isabelle}
1.63 -\REMARK{I put in this proof state but I wonder if readers will be able to
1.64 -follow this proof. You could prove that your relation is WF in a
1.65 -lemma beforehand, maybe omitting that proof.}
1.66 Now the induction hypothesis states that if \isa{t\ {\isasymnotin}\ A}
1.67 then all successors of \isa{t} that are in \isa{Avoid\ s\ A} are in
1.68 -\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. To prove the actual goal we unfold \isa{lfp} once. Now
1.69 -we have to prove that \isa{t} is in \isa{A} or all successors of \isa{t} are in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. If \isa{t} is not in \isa{A}, the second
1.70 +\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Unfolding \isa{lfp} in the conclusion of the first
1.71 +subgoal once, we have to prove that \isa{t} is in \isa{A} or all successors
1.72 +of \isa{t} are in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}: if \isa{t} is not in \isa{A},
1.73 +the second
1.74 \isa{Avoid}-rule implies that all successors of \isa{t} are in
1.75 \isa{Avoid\ s\ A} (because we also assume \isa{t\ {\isasymin}\ Avoid\ s\ A}), and
1.76 hence, by the induction hypothesis, all successors of \isa{t} are indeed in
1.77 \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Mechanically:%
1.78 \end{isamarkuptxt}%
1.79 -\ \isacommand{apply}{\isacharparenleft}rule\ ssubst\ {\isacharbrackleft}OF\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline
1.80 -\ \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline
1.81 +\ \isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline
1.82 +\ \isacommand{apply}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline
1.83 \ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}%
1.84 \begin{isamarkuptxt}%
1.85 Having proved the main goal we return to the proof obligation that the above
1.86 @@ -127,7 +128,8 @@
1.87 \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharparenright}\isanewline
1.88 \isacommand{done}%
1.89 \begin{isamarkuptext}%
1.90 -The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive means
1.91 +The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive in the
1.92 +statement of the lemma means
1.93 that the assumption is left unchanged --- otherwise the \isa{{\isasymforall}p} is turned
1.94 into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is,
1.95 \isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now