3 \def\isabellecontext{CTLind}%
18 \isamarkupsubsection{CTL Revisited%
22 \begin{isamarkuptext}%
23 \label{sec:CTL-revisited}
25 The purpose of this section is twofold: to demonstrate
26 some of the induction principles and heuristics discussed above and to
27 show how inductive definitions can simplify proofs.
28 In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a
29 model checker for CTL\@. In particular the proof of the
30 \isa{infinity{\isacharunderscore}lemma} on the way to \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} is not as
31 simple as one might expect, due to the \isa{SOME} operator
32 involved. Below we give a simpler proof of \isa{AF{\isacharunderscore}lemma{\isadigit{2}}}
33 based on an auxiliary inductive definition.
35 Let us call a (finite or infinite) path \emph{\isa{A}-avoiding} if it does
36 not touch any node in the set \isa{A}. Then \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} says
37 that if no infinite path from some state \isa{s} is \isa{A}-avoiding,
38 then \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. We prove this by inductively defining the set
39 \isa{Avoid\ s\ A} of states reachable from \isa{s} by a finite \isa{A}-avoiding path:
40 % Second proof of opposite direction, directly by well-founded induction
41 % on the initial segment of M that avoids A.%
44 \isacommand{inductive{\isacharunderscore}set}\isamarkupfalse%
46 \ \ Avoid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequoteclose}\isanewline
47 \ \ \isakeyword{for}\ s\ {\isacharcolon}{\isacharcolon}\ state\ \isakeyword{and}\ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ set{\isachardoublequoteclose}\isanewline
48 \isakeyword{where}\isanewline
49 \ \ \ \ {\isachardoublequoteopen}s\ {\isasymin}\ Avoid\ s\ A{\isachardoublequoteclose}\isanewline
50 \ \ {\isacharbar}\ {\isachardoublequoteopen}{\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{\isachardoublequoteclose}%
51 \begin{isamarkuptext}%
52 It is easy to see that for any infinite \isa{A}-avoiding path \isa{f}
53 with \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path
54 starting with \isa{s} because (by definition of \isa{Avoid}) there is a
55 finite \isa{A}-avoiding path from \isa{s} to \isa{f\ {\isadigit{0}}}.
56 The proof is by induction on \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A}. However,
57 this requires the following
58 reformulation, as explained in \S\ref{sec:ind-var-in-prems} above;
59 the \isa{rule{\isacharunderscore}format} directive undoes the reformulation after the proof.%
62 \isacommand{lemma}\isamarkupfalse%
63 \ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
64 \ \ {\isachardoublequoteopen}t\ {\isasymin}\ Avoid\ s\ A\ \ {\isasymLongrightarrow}\isanewline
65 \ \ \ {\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}{\isachardoublequoteclose}\isanewline
72 \isacommand{apply}\isamarkupfalse%
73 {\isacharparenleft}erule\ Avoid{\isachardot}induct{\isacharparenright}\isanewline
74 \ \isacommand{apply}\isamarkupfalse%
75 {\isacharparenleft}blast{\isacharparenright}\isanewline
76 \isacommand{apply}\isamarkupfalse%
77 {\isacharparenleft}clarify{\isacharparenright}\isanewline
78 \isacommand{apply}\isamarkupfalse%
79 {\isacharparenleft}drule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}i{\isachardot}\ case\ i\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ t\ {\isacharbar}\ Suc\ i\ {\isasymRightarrow}\ f\ i{\isachardoublequoteclose}\ \isakeyword{in}\ bspec{\isacharparenright}\isanewline
80 \isacommand{apply}\isamarkupfalse%
81 {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ Paths{\isacharunderscore}def\ split{\isacharcolon}\ nat{\isachardot}split{\isacharparenright}\isanewline
82 \isacommand{done}\isamarkupfalse%
91 \begin{isamarkuptext}%
93 The base case (\isa{t\ {\isacharequal}\ s}) is trivial and proved by \isa{blast}.
94 In the induction step, we have an infinite \isa{A}-avoiding path \isa{f}
95 starting from \isa{u}, a successor of \isa{t}. Now we simply instantiate
96 the \isa{{\isasymforall}f{\isasymin}Paths\ t} in the induction hypothesis by the path starting with
97 \isa{t} and continuing with \isa{f}. That is what the above $\lambda$-term
98 expresses. Simplification shows that this is a path starting with \isa{t}
99 and that the instantiated induction hypothesis implies the conclusion.
101 Now we come to the key lemma. Assuming that no infinite \isa{A}-avoiding
102 path starts from \isa{s}, we want to show \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. For the
103 inductive proof this must be generalized to the statement that every point \isa{t}
104 ``between'' \isa{s} and \isa{A}, in other words all of \isa{Avoid\ s\ A},
105 is contained in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}:%
108 \isacommand{lemma}\isamarkupfalse%
109 \ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline
110 \ \ {\isachardoublequoteopen}{\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}{\isachardoublequoteclose}%
117 \begin{isamarkuptxt}%
119 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}}.
120 If \isa{t} is already in \isa{A}, then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} is
121 trivial. If \isa{t} is not in \isa{A} but all successors are in
122 \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}} (induction hypothesis), then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} is
125 The formal counterpart of this proof sketch is a well-founded induction
126 on~\isa{M} restricted to \isa{Avoid\ s\ A\ {\isacharminus}\ A}, roughly speaking:
128 \ \ \ \ \ {\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}%
130 As we shall see presently, the absence of infinite \isa{A}-avoiding paths
131 starting from \isa{s} implies well-foundedness of this relation. For the
132 moment we assume this and proceed with the induction:%
135 \isacommand{apply}\isamarkupfalse%
136 {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequoteopen}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}{\isachardoublequoteclose}{\isacharparenright}\isanewline
137 \ \isacommand{apply}\isamarkupfalse%
138 {\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline
139 \ \isacommand{apply}\isamarkupfalse%
140 {\isacharparenleft}clarsimp{\isacharparenright}%
141 \begin{isamarkuptxt}%
144 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\isanewline
145 \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ }{\isasymforall}y{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ A\ {\isasymlongrightarrow}\isanewline
146 \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ {\isasymforall}y{\isachardot}\ }y\ {\isasymin}\ Avoid\ s\ A\ {\isasymlongrightarrow}\ y\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharsemicolon}\isanewline
147 \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ }t\ {\isasymin}\ Avoid\ s\ A{\isasymrbrakk}\isanewline
148 \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ }{\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline
149 \ {\isadigit{2}}{\isachardot}\ {\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\isanewline
150 \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}%
152 Now the induction hypothesis states that if \isa{t\ {\isasymnotin}\ A}
153 then all successors of \isa{t} that are in \isa{Avoid\ s\ A} are in
154 \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Unfolding \isa{lfp} in the conclusion of the first
155 subgoal once, we have to prove that \isa{t} is in \isa{A} or all successors
156 of \isa{t} are in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. But if \isa{t} is not in \isa{A},
158 \isa{Avoid}-rule implies that all successors of \isa{t} are in
159 \isa{Avoid\ s\ A}, because we also assume \isa{t\ {\isasymin}\ Avoid\ s\ A}.
160 Hence, by the induction hypothesis, all successors of \isa{t} are indeed in
161 \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Mechanically:%
164 \ \isacommand{apply}\isamarkupfalse%
165 {\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline
166 \ \isacommand{apply}\isamarkupfalse%
167 {\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline
168 \ \isacommand{apply}\isamarkupfalse%
169 {\isacharparenleft}blast\ intro{\isacharcolon}\ Avoid{\isachardot}intros{\isacharparenright}%
170 \begin{isamarkuptxt}%
171 Having proved the main goal, we return to the proof obligation that the
172 relation used above is indeed well-founded. This is proved by contradiction: if
173 the relation is not well-founded then there exists an infinite \isa{A}-avoiding path all in \isa{Avoid\ s\ A}, by theorem
174 \isa{wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain}:
176 \ \ \ \ \ 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}%
178 From lemma \isa{ex{\isacharunderscore}infinite{\isacharunderscore}path} the existence of an infinite
179 \isa{A}-avoiding path starting in \isa{s} follows, contradiction.%
182 \isacommand{apply}\isamarkupfalse%
183 {\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline
184 \isacommand{apply}\isamarkupfalse%
185 {\isacharparenleft}simp\ add{\isacharcolon}\ wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline
186 \isacommand{apply}\isamarkupfalse%
187 {\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
188 \isacommand{apply}\isamarkupfalse%
189 {\isacharparenleft}rule\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharparenright}\isanewline
190 \isacommand{apply}\isamarkupfalse%
191 {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Paths{\isacharunderscore}def{\isacharparenright}\isanewline
192 \isacommand{done}\isamarkupfalse%
201 \begin{isamarkuptext}%
202 The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive in the
203 statement of the lemma means
204 that the assumption is left unchanged; otherwise the \isa{{\isasymforall}p}
206 into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is,
207 \isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now
209 \ \ \ \ \ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\ t\ {\isasymin}\ Avoid\ s\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}%
211 The main theorem is simply the corollary where \isa{t\ {\isacharequal}\ s},
212 when the assumption \isa{t\ {\isasymin}\ Avoid\ s\ A} is trivially true
213 by the first \isa{Avoid}-rule. Isabelle confirms this:%
217 \isacommand{theorem}\isamarkupfalse%
218 \ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\ \ {\isachardoublequoteopen}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
225 \isacommand{by}\isamarkupfalse%
226 {\isacharparenleft}auto\ elim{\isacharcolon}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}\ Avoid{\isachardot}intros{\isacharparenright}\isanewline
251 %%% TeX-master: "root"