diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/CTL/document/CTL.tex --- a/doc-src/TutorialI/CTL/document/CTL.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Wed May 25 09:04:24 2005 +0200 @@ -67,13 +67,14 @@ \isamarkuptrue% \isacommand{lemma}\ mono{\isacharunderscore}af{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ mono{\isacharunderscore}def\ af{\isacharunderscore}def{\isacharparenright}\isanewline \isamarkupfalse% -\isanewline +\isacommand{apply}\ blast\isanewline +\isamarkupfalse% +\isacommand{done}\isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% @@ -89,8 +90,6 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline -\isamarkupfalse% % \begin{isamarkuptext}% All we need to prove now is \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ AF\ f{\isacharbraceright}}, which states @@ -101,13 +100,42 @@ \isamarkuptrue% \isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{1}}{\isacharcolon}\isanewline \ \ {\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% -\isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +In contrast to the analogous proof for \isa{EF}, and just +for a change, we do not use fixed point induction. Park-induction, +named after David Park, is weaker but sufficient for this proof: +\begin{center} +\isa{f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S} \hfill (\isa{lfp{\isacharunderscore}lowerbound}) +\end{center} +The instance of the premise \isa{f\ S\ {\isasymsubseteq}\ S} is proved pointwise, +a decision that \isa{auto} takes for us:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule\ lfp{\isacharunderscore}lowerbound{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ {\isadigit{0}}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\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 +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}t{\isachardot}\ {\isacharparenleft}{\isasymforall}p{\isachardot}\ }{\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ }{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A% +\end{isabelle} +In this remaining case, we set \isa{t} to \isa{p\ {\isadigit{1}}}. +The rest is automatic, which is surprising because it involves +finding the instantiation \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}} +for \isa{{\isasymforall}p}.% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ {\isadigit{1}}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline +\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% The opposite inclusion is proved by contradiction: if some state @@ -125,10 +153,13 @@ \isacommand{lemma}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharcolon}\isanewline \ {\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 \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}np{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -162,26 +193,100 @@ \isacommand{lemma}\ infinity{\isacharunderscore}lemma{\isacharcolon}\isanewline \ \ {\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 \ \ \ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}\isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +First we rephrase the conclusion slightly because we need to prove simultaneously +both the path property and the fact that \isa{Q} holds:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\isanewline +\ \ {\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% +% +\begin{isamarkuptxt}% +\noindent +From this proposition the original goal follows easily:% +\end{isamarkuptxt}% +\ \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +The new subgoal is proved by providing the witness \isa{path\ s\ Q} for \isa{p}:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}path\ s\ Q{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +After simplification and clarification, the subgoal has the following form: +\begin{isabelle}% +\ {\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 +\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 +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymLongrightarrow}\ }Q\ {\isacharparenleft}path\ s\ Q\ i{\isacharparenright}% +\end{isabelle} +It invites a proof by induction on \isa{i}:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +After simplification, the base case boils down to +\begin{isabelle}% +\ {\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 +\isaindent{\ {\isadigit{1}}{\isachardot}\ }{\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}\ {\isasymin}\ M% +\end{isabelle} +The conclusion looks exceedingly trivial: after all, \isa{t} is chosen such that \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M} +holds. However, we first have to show that such a \isa{t} actually exists! This reasoning +is embodied in the theorem \isa{someI{\isadigit{2}}{\isacharunderscore}ex}: +\begin{isabelle}% +\ \ \ \ \ {\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}% +\end{isabelle} +When we apply this theorem as an introduction rule, \isa{{\isacharquery}P\ x} becomes +\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 +two subgoals: \isa{{\isasymexists}a{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ a{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ a}, which follows from the assumptions, and +\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 +\isa{fast} can prove the base case quickly:% +\end{isamarkuptxt}% +\ \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +What is worth noting here is that we have used \methdx{fast} rather than +\isa{blast}. The reason is that \isa{blast} would fail because it cannot +cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}: unifying its conclusion with the current +subgoal is non-trivial because of the nested schematic variables. For +efficiency reasons \isa{blast} does not even attempt such unifications. +Although \isa{fast} can in principle cope with complicated unification +problems, in practice the number of unifiers arising is often prohibitive and +the offending rule may need to be applied explicitly rather than +automatically. This is what happens in the step case. + +The induction step is similar, but more involved, because now we face nested +occurrences of \isa{SOME}. As a result, \isa{fast} is no longer able to +solve the subgoal and we apply \isa{someI{\isadigit{2}}{\isacharunderscore}ex} by hand. We merely +show the proof commands but do not describe the details:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% Function \isa{path} has fulfilled its purpose now and can be forgotten. @@ -211,7 +316,6 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline \isamarkupfalse% % \begin{isamarkuptext}% @@ -219,15 +323,40 @@ \end{isamarkuptext}% \isamarkuptrue% \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% -\isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +The proof is again pointwise and then by contraposition:% +\end{isamarkuptxt}% \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline +\isamarkupfalse% +\isacommand{apply}\ simp\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\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% +\end{isabelle} +Applying the \isa{infinity{\isacharunderscore}lemma} as a destruction rule leaves two subgoals, the second +premise of \isa{infinity{\isacharunderscore}lemma} and the original subgoal:% +\end{isamarkuptxt}% \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}drule\ infinity{\isacharunderscore}lemma{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\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 +\ {\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 +\isaindent{\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }{\isasymexists}p{\isasymin}Paths\ x{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A% +\end{isabelle} +Both are solved automatically:% +\end{isamarkuptxt}% +\ \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% If you find these proofs too complicated, we recommend that you read @@ -241,9 +370,11 @@ \isamarkuptrue% \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline \isamarkupfalse% +\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 \isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% The language defined above is not quite CTL\@. The latter also includes an @@ -293,12 +424,6 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% @@ -311,8 +436,10 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline -\isanewline +\isamarkupfalse% +\isamarkupfalse% +\isamarkupfalse% +\isamarkupfalse% \isamarkupfalse% % \begin{isamarkuptext}%