1.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex Wed Feb 02 18:06:00 2005 +0100
1.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex Wed Feb 02 18:06:25 2005 +0100
1.3 @@ -87,11 +87,9 @@
1.4 \isamarkuptrue%
1.5 \isacommand{lemma}\ mono{\isacharunderscore}ef{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
1.6 \isamarkupfalse%
1.7 -\isacommand{apply}{\isacharparenleft}rule\ monoI{\isacharparenright}\isanewline
1.8 \isamarkupfalse%
1.9 -\isacommand{apply}\ blast\isanewline
1.10 \isamarkupfalse%
1.11 -\isacommand{done}\isamarkupfalse%
1.12 +\isamarkupfalse%
1.13 %
1.14 \begin{isamarkuptext}%
1.15 \noindent
1.16 @@ -101,112 +99,30 @@
1.17 \isamarkuptrue%
1.18 \isacommand{lemma}\ EF{\isacharunderscore}lemma{\isacharcolon}\isanewline
1.19 \ \ {\isachardoublequote}lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}\isamarkupfalse%
1.20 -%
1.21 -\begin{isamarkuptxt}%
1.22 -\noindent
1.23 -The equality is proved in the canonical fashion by proving that each set
1.24 -includes the other; the inclusion is shown pointwise:%
1.25 -\end{isamarkuptxt}%
1.26 \isamarkuptrue%
1.27 -\isacommand{apply}{\isacharparenleft}rule\ equalityI{\isacharparenright}\isanewline
1.28 -\ \isamarkupfalse%
1.29 -\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
1.30 -\ \isamarkupfalse%
1.31 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse%
1.32 \isamarkupfalse%
1.33 -%
1.34 -\begin{isamarkuptxt}%
1.35 -\noindent
1.36 -Simplification leaves us with the following first subgoal
1.37 -\begin{isabelle}%
1.38 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A%
1.39 -\end{isabelle}
1.40 -which is proved by \isa{lfp}-induction:%
1.41 -\end{isamarkuptxt}%
1.42 -\ \isamarkuptrue%
1.43 -\isacommand{apply}{\isacharparenleft}erule\ lfp{\isacharunderscore}induct{\isacharparenright}\isanewline
1.44 -\ \ \isamarkupfalse%
1.45 -\isacommand{apply}{\isacharparenleft}rule\ mono{\isacharunderscore}ef{\isacharparenright}\isanewline
1.46 -\ \isamarkupfalse%
1.47 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse%
1.48 -%
1.49 -\begin{isamarkuptxt}%
1.50 -\noindent
1.51 -Having disposed of the monotonicity subgoal,
1.52 -simplification leaves us with the following goal:
1.53 -\begin{isabelle}
1.54 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymor}\isanewline
1.55 -\ \ \ \ \ \ \ \ \ x\ {\isasymin}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ {\isacharparenleft}lfp\ {\isacharparenleft}\dots{\isacharparenright}\ {\isasyminter}\ {\isacharbraceleft}x{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isacharparenright}\isanewline
1.56 -\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A
1.57 -\end{isabelle}
1.58 -It is proved by \isa{blast}, using the transitivity of
1.59 -\isa{M\isactrlsup {\isacharasterisk}}.%
1.60 -\end{isamarkuptxt}%
1.61 -\ \isamarkuptrue%
1.62 -\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtrancl{\isacharunderscore}trans{\isacharparenright}\isamarkupfalse%
1.63 -%
1.64 -\begin{isamarkuptxt}%
1.65 -We now return to the second set inclusion subgoal, which is again proved
1.66 -pointwise:%
1.67 -\end{isamarkuptxt}%
1.68 +\isamarkupfalse%
1.69 +\isamarkupfalse%
1.70 +\isamarkupfalse%
1.71 \isamarkuptrue%
1.72 -\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
1.73 \isamarkupfalse%
1.74 -\isacommand{apply}{\isacharparenleft}simp{\isacharcomma}\ clarify{\isacharparenright}\isamarkupfalse%
1.75 -%
1.76 -\begin{isamarkuptxt}%
1.77 -\noindent
1.78 -After simplification and clarification we are left with
1.79 -\begin{isabelle}%
1.80 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ t\ {\isasymin}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}%
1.81 -\end{isabelle}
1.82 -This goal is proved by induction on \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}}. But since the model
1.83 -checker works backwards (from \isa{t} to \isa{s}), we cannot use the
1.84 -induction theorem \isa{rtrancl{\isacharunderscore}induct}: it works in the
1.85 -forward direction. Fortunately the converse induction theorem
1.86 -\isa{converse{\isacharunderscore}rtrancl{\isacharunderscore}induct} already exists:
1.87 -\begin{isabelle}%
1.88 -\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ b{\isacharsemicolon}\isanewline
1.89 -\isaindent{\ \ \ \ \ \ }{\isasymAnd}y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}z{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ y{\isasymrbrakk}\isanewline
1.90 -\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ P\ a%
1.91 -\end{isabelle}
1.92 -It says that if \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}} and we know \isa{P\ b} then we can infer
1.93 -\isa{P\ a} provided each step backwards from a predecessor \isa{z} of
1.94 -\isa{b} preserves \isa{P}.%
1.95 -\end{isamarkuptxt}%
1.96 +\isamarkupfalse%
1.97 +\isamarkupfalse%
1.98 \isamarkuptrue%
1.99 -\isacommand{apply}{\isacharparenleft}erule\ converse{\isacharunderscore}rtrancl{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse%
1.100 -%
1.101 -\begin{isamarkuptxt}%
1.102 -\noindent
1.103 -The base case
1.104 -\begin{isabelle}%
1.105 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}%
1.106 -\end{isabelle}
1.107 -is solved by unrolling \isa{lfp} once%
1.108 -\end{isamarkuptxt}%
1.109 -\ \isamarkuptrue%
1.110 -\isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharparenright}\isamarkupfalse%
1.111 -%
1.112 -\begin{isamarkuptxt}%
1.113 -\begin{isabelle}%
1.114 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}%
1.115 -\end{isabelle}
1.116 -and disposing of the resulting trivial subgoal automatically:%
1.117 -\end{isamarkuptxt}%
1.118 -\ \isamarkuptrue%
1.119 -\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isamarkupfalse%
1.120 -%
1.121 -\begin{isamarkuptxt}%
1.122 -\noindent
1.123 -The proof of the induction step is identical to the one for the base case:%
1.124 -\end{isamarkuptxt}%
1.125 +\isamarkupfalse%
1.126 \isamarkuptrue%
1.127 -\isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharparenright}\isanewline
1.128 \isamarkupfalse%
1.129 -\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
1.130 \isamarkupfalse%
1.131 -\isacommand{done}\isamarkupfalse%
1.132 +\isamarkuptrue%
1.133 +\isamarkupfalse%
1.134 +\isamarkuptrue%
1.135 +\isamarkupfalse%
1.136 +\isamarkuptrue%
1.137 +\isamarkupfalse%
1.138 +\isamarkuptrue%
1.139 +\isamarkupfalse%
1.140 +\isamarkupfalse%
1.141 +\isamarkupfalse%
1.142 %
1.143 \begin{isamarkuptext}%
1.144 The main theorem is proved in the familiar manner: induction followed by
1.145 @@ -215,11 +131,9 @@
1.146 \isamarkuptrue%
1.147 \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline
1.148 \isamarkupfalse%
1.149 -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
1.150 \isamarkupfalse%
1.151 -\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma{\isacharparenright}\isanewline
1.152 \isamarkupfalse%
1.153 -\isacommand{done}\isamarkupfalse%
1.154 +\isamarkupfalse%
1.155 %
1.156 \begin{isamarkuptext}%
1.157 \begin{exercise}