1.1 --- a/doc-src/TutorialI/CTL/document/CTLind.tex Sun Oct 21 19:48:19 2001 +0200
1.2 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex Sun Oct 21 19:49:29 2001 +0200
1.3 @@ -1,9 +1,11 @@
1.4 %
1.5 \begin{isabellebody}%
1.6 \def\isabellecontext{CTLind}%
1.7 +\isamarkupfalse%
1.8 %
1.9 \isamarkupsubsection{CTL Revisited%
1.10 }
1.11 +\isamarkuptrue%
1.12 %
1.13 \begin{isamarkuptext}%
1.14 \label{sec:CTL-revisited}
1.15 @@ -26,10 +28,13 @@
1.16 % Second proof of opposite direction, directly by well-founded induction
1.17 % on the initial segment of M that avoids A.%
1.18 \end{isamarkuptext}%
1.19 +\isamarkuptrue%
1.20 \isacommand{consts}\ Avoid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline
1.21 +\isamarkupfalse%
1.22 \isacommand{inductive}\ {\isachardoublequote}Avoid\ s\ A{\isachardoublequote}\isanewline
1.23 \isakeyword{intros}\ {\isachardoublequote}s\ {\isasymin}\ Avoid\ s\ A{\isachardoublequote}\isanewline
1.24 -\ \ \ \ \ \ \ {\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}%
1.25 +\ \ \ \ \ \ \ {\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}\isamarkupfalse%
1.26 +%
1.27 \begin{isamarkuptext}%
1.28 It is easy to see that for any infinite \isa{A}-avoiding path \isa{f}
1.29 with \isa{f\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymin}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path
1.30 @@ -40,15 +45,23 @@
1.31 reformulation, as explained in \S\ref{sec:ind-var-in-prems} above;
1.32 the \isa{rule{\isacharunderscore}format} directive undoes the reformulation after the proof.%
1.33 \end{isamarkuptext}%
1.34 +\isamarkuptrue%
1.35 \isacommand{lemma}\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
1.36 \ \ {\isachardoublequote}t\ {\isasymin}\ Avoid\ s\ A\ \ {\isasymLongrightarrow}\isanewline
1.37 \ \ \ {\isasymforall}f{\isasymin}Paths\ t{\isachardot}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ f\ i\ {\isasymnotin}\ A{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A{\isacharparenright}{\isachardoublequote}\isanewline
1.38 +\isamarkupfalse%
1.39 \isacommand{apply}{\isacharparenleft}erule\ Avoid{\isachardot}induct{\isacharparenright}\isanewline
1.40 -\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
1.41 +\ \isamarkupfalse%
1.42 +\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
1.43 +\isamarkupfalse%
1.44 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
1.45 +\isamarkupfalse%
1.46 \isacommand{apply}{\isacharparenleft}drule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ case\ i\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ t\ {\isacharbar}\ Suc\ i\ {\isasymRightarrow}\ f\ i{\isachardoublequote}\ \isakeyword{in}\ bspec{\isacharparenright}\isanewline
1.47 +\isamarkupfalse%
1.48 \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}Paths{\isacharunderscore}def\ split{\isacharcolon}nat{\isachardot}split{\isacharparenright}\isanewline
1.49 -\isacommand{done}%
1.50 +\isamarkupfalse%
1.51 +\isacommand{done}\isamarkupfalse%
1.52 +%
1.53 \begin{isamarkuptext}%
1.54 \noindent
1.55 The base case (\isa{t\ {\isacharequal}\ s}) is trivial and proved by \isa{blast}.
1.56 @@ -65,8 +78,10 @@
1.57 ``between'' \isa{s} and \isa{A}, in other words all of \isa{Avoid\ s\ A},
1.58 is contained in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}:%
1.59 \end{isamarkuptext}%
1.60 +\isamarkuptrue%
1.61 \isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline
1.62 -\ \ {\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.63 +\ \ {\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}\isamarkupfalse%
1.64 +%
1.65 \begin{isamarkuptxt}%
1.66 \noindent
1.67 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.68 @@ -84,9 +99,14 @@
1.69 starting from \isa{s} implies well-foundedness of this relation. For the
1.70 moment we assume this and proceed with the induction:%
1.71 \end{isamarkuptxt}%
1.72 +\isamarkuptrue%
1.73 \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.74 -\ \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline
1.75 -\ \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
1.76 +\ \isamarkupfalse%
1.77 +\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline
1.78 +\ \isamarkupfalse%
1.79 +\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isamarkupfalse%
1.80 +\isamarkupfalse%
1.81 +%
1.82 \begin{isamarkuptxt}%
1.83 \noindent
1.84 \begin{isabelle}%
1.85 @@ -108,9 +128,13 @@
1.86 Hence, by the induction hypothesis, all successors of \isa{t} are indeed in
1.87 \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Mechanically:%
1.88 \end{isamarkuptxt}%
1.89 -\ \isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline
1.90 -\ \isacommand{apply}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline
1.91 -\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}%
1.92 +\ \isamarkuptrue%
1.93 +\isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline
1.94 +\ \isamarkupfalse%
1.95 +\isacommand{apply}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline
1.96 +\ \isamarkupfalse%
1.97 +\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isamarkupfalse%
1.98 +%
1.99 \begin{isamarkuptxt}%
1.100 Having proved the main goal, we return to the proof obligation that the
1.101 relation used above is indeed well-founded. This is proved by contradiction: if
1.102 @@ -122,12 +146,19 @@
1.103 From lemma \isa{ex{\isacharunderscore}infinite{\isacharunderscore}path} the existence of an infinite
1.104 \isa{A}-avoiding path starting in \isa{s} follows, contradiction.%
1.105 \end{isamarkuptxt}%
1.106 +\isamarkuptrue%
1.107 \isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline
1.108 +\isamarkupfalse%
1.109 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline
1.110 +\isamarkupfalse%
1.111 \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
1.112 +\isamarkupfalse%
1.113 \isacommand{apply}{\isacharparenleft}rule\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharparenright}\isanewline
1.114 +\isamarkupfalse%
1.115 \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharparenright}\isanewline
1.116 -\isacommand{done}%
1.117 +\isamarkupfalse%
1.118 +\isacommand{done}\isamarkupfalse%
1.119 +%
1.120 \begin{isamarkuptext}%
1.121 The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive in the
1.122 statement of the lemma means
1.123 @@ -143,9 +174,13 @@
1.124 by the first \isa{Avoid}-rule. Isabelle confirms this:%
1.125 \index{CTL|)}%
1.126 \end{isamarkuptext}%
1.127 +\isamarkuptrue%
1.128 \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}\isanewline
1.129 +\isamarkupfalse%
1.130 \isacommand{by}{\isacharparenleft}auto\ elim{\isacharcolon}Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isanewline
1.131 \isanewline
1.132 +\isamarkupfalse%
1.133 +\isamarkupfalse%
1.134 \end{isabellebody}%
1.135 %%% Local Variables:
1.136 %%% mode: latex