1.1 --- a/doc-src/TutorialI/CTL/document/CTLind.tex	Fri Jan 12 16:05:12 2001 +0100
     1.2 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex	Fri Jan 12 16:07:20 2001 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4  \begin{isabellebody}%
     1.5  \def\isabellecontext{CTLind}%
     1.6  %
     1.7 -\isamarkupsubsection{CTL revisited%
     1.8 +\isamarkupsubsection{CTL Revisited%
     1.9  }
    1.10  %
    1.11  \begin{isamarkuptext}%
    1.12 @@ -55,9 +55,8 @@
    1.13  starting from \isa{u}, a successor of \isa{t}. Now we simply instantiate
    1.14  the \isa{{\isasymforall}f{\isasymin}Paths\ t} in the induction hypothesis by the path starting with
    1.15  \isa{t} and continuing with \isa{f}. That is what the above $\lambda$-term
    1.16 -expresses. That fact that this is a path starting with \isa{t} and that
    1.17 -the instantiated induction hypothesis implies the conclusion is shown by
    1.18 -simplification.
    1.19 +expresses.  Simplification shows that this is a path starting with \isa{t} 
    1.20 +and that the instantiated induction hypothesis implies the conclusion.
    1.21  
    1.22  Now we come to the key lemma. It says that if \isa{t} can be reached by a
    1.23  finite \isa{A}-avoiding path from \isa{s}, then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}},
    1.24 @@ -67,10 +66,11 @@
    1.25  \ \ {\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.26  \begin{isamarkuptxt}%
    1.27  \noindent
    1.28 -The trick is not to induct on \isa{t\ {\isasymin}\ Avoid\ s\ A}, as already the base
    1.29 -case would be a problem, but to proceed by well-founded induction \isa{t}. Hence \isa{t\ {\isasymin}\ Avoid\ s\ A} needs to be brought into the conclusion as
    1.30 +The trick is not to induct on \isa{t\ {\isasymin}\ Avoid\ s\ A}, as even the base
    1.31 +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.32  well, which the directive \isa{rule{\isacharunderscore}format} undoes at the end (see below).
    1.33 -But induction with respect to which well-founded relation? The restriction
    1.34 +But induction with respect to which well-founded relation? The
    1.35 +one we want is the restriction
    1.36  of \isa{M} to \isa{Avoid\ s\ A}:
    1.37  \begin{isabelle}%
    1.38  \ \ \ \ \ {\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.39 @@ -85,7 +85,19 @@
    1.40  \ \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
    1.41  \begin{isamarkuptxt}%
    1.42  \noindent
    1.43 -Now can assume additionally (induction hypothesis) that if \isa{t\ {\isasymnotin}\ A}
    1.44 +\begin{isabelle}%
    1.45 +\ {\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.46 +\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}y{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ y\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A\ {\isasymlongrightarrow}\isanewline
    1.47 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ y\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isasymrbrakk}\isanewline
    1.48 +\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ x\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline
    1.49 +\ {\isadigit{2}}{\isachardot}\ {\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\isanewline
    1.50 +\ \ \ \ wf\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\isanewline
    1.51 +\ \ \ \ \ \ \ \ {\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.52 +\end{isabelle}
    1.53 +\REMARK{I put in this proof state but I wonder if readers will be able to
    1.54 +follow this proof. You could prove that your relation is WF in a 
    1.55 +lemma beforehand, maybe omitting that proof.}
    1.56 +Now the induction hypothesis states that if \isa{t\ {\isasymnotin}\ A}
    1.57  then all successors of \isa{t} that are in \isa{Avoid\ s\ A} are in
    1.58  \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. To prove the actual goal we unfold \isa{lfp} once. Now
    1.59  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.60 @@ -99,15 +111,14 @@
    1.61  \ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}%
    1.62  \begin{isamarkuptxt}%
    1.63  Having proved the main goal we return to the proof obligation that the above
    1.64 -relation is indeed well-founded. This is proved by contraposition: we assume
    1.65 -the relation is not well-founded. Thus there exists an infinite \isa{A}-avoiding path all in \isa{Avoid\ s\ A}, by theorem
    1.66 +relation is indeed well-founded. This is proved by contradiction: if
    1.67 +the relation is not well-founded then there exists an infinite \isa{A}-avoiding path all in \isa{Avoid\ s\ A}, by theorem
    1.68  \isa{wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain}:
    1.69  \begin{isabelle}%
    1.70  \ \ \ \ \ wf\ r\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ {\isacharparenleft}{\isasymexists}f{\isachardot}\ {\isasymforall}i{\isachardot}\ {\isacharparenleft}f\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharcomma}\ f\ i{\isacharparenright}\ {\isasymin}\ r{\isacharparenright}{\isacharparenright}%
    1.71  \end{isabelle}
    1.72  From lemma \isa{ex{\isacharunderscore}infinite{\isacharunderscore}path} the existence of an infinite
    1.73 -\isa{A}-avoiding path starting in \isa{s} follows, just as required for
    1.74 -the contraposition.%
    1.75 +\isa{A}-avoiding path starting in \isa{s} follows, contradiction.%
    1.76  \end{isamarkuptxt}%
    1.77  \isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline
    1.78  \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline