|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{CTLind}% |
|
4 % |
|
5 \isamarkupsubsection{CTL revisited} |
|
6 % |
|
7 \begin{isamarkuptext}% |
|
8 \label{sec:CTL-revisited} |
|
9 In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a |
|
10 model checker for CTL. In particular the proof of the |
|
11 \isa{infinity{\isacharunderscore}lemma} on the way to \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} is not as |
|
12 simple as one might intuitively expect, due to the \isa{SOME} operator |
|
13 involved. The purpose of this section is to show how an inductive definition |
|
14 can help to simplify the proof of \isa{AF{\isacharunderscore}lemma{\isadigit{2}}}. |
|
15 |
|
16 Let us call a (finite or infinite) path \emph{\isa{A}-avoiding} if it does |
|
17 not touch any node in the set \isa{A}. Then \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} says |
|
18 that if no infinite path from some state \isa{s} is \isa{A}-avoiding, |
|
19 then \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. We prove this by inductively defining the set |
|
20 \isa{Avoid\ s\ A} of states reachable from \isa{s} by a finite \isa{A}-avoiding path: |
|
21 % Second proof of opposite direction, directly by well-founded induction |
|
22 % on the initial segment of M that avoids A.% |
|
23 \end{isamarkuptext}% |
|
24 \isacommand{consts}\ Avoid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline |
|
25 \isacommand{inductive}\ {\isachardoublequote}Avoid\ s\ A{\isachardoublequote}\isanewline |
|
26 \isakeyword{intros}\ {\isachardoublequote}s\ {\isasymin}\ Avoid\ s\ A{\isachardoublequote}\isanewline |
|
27 \ \ \ \ \ \ \ {\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}% |
|
28 \begin{isamarkuptext}% |
|
29 It is easy to see that for any infinite \isa{A}-avoiding path \isa{f} |
|
30 with \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path |
|
31 starting with \isa{s} because (by definition of \isa{Avoid}) there is a |
|
32 finite \isa{A}-avoiding path from \isa{s} to \isa{f\ {\isadigit{0}}}. |
|
33 The proof is by induction on \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A}. However, |
|
34 this requires the following |
|
35 reformulation, as explained in \S\ref{sec:ind-var-in-prems} above; |
|
36 the \isa{rule{\isacharunderscore}format} directive undoes the reformulation after the proof.% |
|
37 \end{isamarkuptext}% |
|
38 \isacommand{lemma}\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline |
|
39 \ \ {\isachardoublequote}t\ {\isasymin}\ Avoid\ s\ A\ \ {\isasymLongrightarrow}\isanewline |
|
40 \ \ \ {\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 |
|
41 \isacommand{apply}{\isacharparenleft}erule\ Avoid{\isachardot}induct{\isacharparenright}\isanewline |
|
42 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline |
|
43 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline |
|
44 \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 |
|
45 \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}Paths{\isacharunderscore}def\ split{\isacharcolon}nat{\isachardot}split{\isacharparenright}\isanewline |
|
46 \isacommand{done}% |
|
47 \begin{isamarkuptext}% |
|
48 \noindent |
|
49 The base case (\isa{t\ {\isacharequal}\ s}) is trivial (\isa{blast}). |
|
50 In the induction step, we have an infinite \isa{A}-avoiding path \isa{f} |
|
51 starting from \isa{u}, a successor of \isa{t}. Now we simply instantiate |
|
52 the \isa{{\isasymforall}f{\isasymin}Paths\ t} in the induction hypothesis by the path starting with |
|
53 \isa{t} and continuing with \isa{f}. That is what the above $\lambda$-term |
|
54 expresses. That fact that this is a path starting with \isa{t} and that |
|
55 the instantiated induction hypothesis implies the conclusion is shown by |
|
56 simplification. |
|
57 |
|
58 Now we come to the key lemma. It says that if \isa{t} can be reached by a |
|
59 finite \isa{A}-avoiding path from \isa{s}, then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, |
|
60 provided there is no infinite \isa{A}-avoiding path starting from \isa{s}.% |
|
61 \end{isamarkuptext}% |
|
62 \isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline |
|
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}% |
|
64 \begin{isamarkuptxt}% |
|
65 \noindent |
|
66 The trick is not to induct on \isa{t\ {\isasymin}\ Avoid\ s\ A}, as already the base |
|
67 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 |
|
68 well, which the directive \isa{rule{\isacharunderscore}format} undoes at the end (see below). |
|
69 But induction with respect to which well-founded relation? The restriction |
|
70 of \isa{M} to \isa{Avoid\ s\ A}: |
|
71 \begin{isabelle}% |
|
72 \ \ \ \ \ {\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}% |
|
73 \end{isabelle} |
|
74 As we shall see in a moment, the absence of infinite \isa{A}-avoiding paths |
|
75 starting from \isa{s} implies well-foundedness of this relation. For the |
|
76 moment we assume this and proceed with the induction:% |
|
77 \end{isamarkuptxt}% |
|
78 \isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\isanewline |
|
79 \ \ {\isachardoublequote}wf{\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}{\isachardoublequote}{\isacharparenright}\isanewline |
|
80 \ \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline |
|
81 \ \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}% |
|
82 \begin{isamarkuptxt}% |
|
83 \noindent |
|
84 Now can assume additionally (induction hypothesis) that if \isa{t\ {\isasymnotin}\ A} |
|
85 then all successors of \isa{t} that are in \isa{Avoid\ s\ A} are in |
|
86 \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. To prove the actual goal we unfold \isa{lfp} once. Now |
|
87 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 |
|
88 \isa{Avoid}-rule implies that all successors of \isa{t} are in |
|
89 \isa{Avoid\ s\ A} (because we also assume \isa{t\ {\isasymin}\ Avoid\ s\ A}), and |
|
90 hence, by the induction hypothesis, all successors of \isa{t} are indeed in |
|
91 \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Mechanically:% |
|
92 \end{isamarkuptxt}% |
|
93 \ \isacommand{apply}{\isacharparenleft}rule\ ssubst\ {\isacharbrackleft}OF\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline |
|
94 \ \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline |
|
95 \ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}% |
|
96 \begin{isamarkuptxt}% |
|
97 Having proved the main goal we return to the proof obligation that the above |
|
98 relation is indeed well-founded. This is proved by contraposition: we assume |
|
99 the relation is not well-founded. Thus there exists an infinite \isa{A}-avoiding path all in \isa{Avoid\ s\ A}, by theorem |
|
100 \isa{wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain}: |
|
101 \begin{isabelle}% |
|
102 \ \ \ \ \ 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}% |
|
103 \end{isabelle} |
|
104 From lemma \isa{ex{\isacharunderscore}infinite{\isacharunderscore}path} the existence of an infinite |
|
105 \isa{A}-avoiding path starting in \isa{s} follows, just as required for |
|
106 the contraposition.% |
|
107 \end{isamarkuptxt}% |
|
108 \isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline |
|
109 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline |
|
110 \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline |
|
111 \isacommand{apply}{\isacharparenleft}rule\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharparenright}\isanewline |
|
112 \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharparenright}\isanewline |
|
113 \isacommand{done}% |
|
114 \begin{isamarkuptext}% |
|
115 The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive means |
|
116 that the assumption is left unchanged---otherwise the \isa{{\isasymforall}p} is turned |
|
117 into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is, |
|
118 \isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now |
|
119 \begin{isabelle}% |
|
120 \ \ \ \ \ {\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}% |
|
121 \end{isabelle} |
|
122 The main theorem is simply the corollary where \isa{t\ {\isacharequal}\ s}, |
|
123 in which case the assumption \isa{t\ {\isasymin}\ Avoid\ s\ A} is trivially true |
|
124 by the first \isa{Avoid}-rule). Isabelle confirms this:% |
|
125 \end{isamarkuptext}% |
|
126 \isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\isanewline |
|
127 \ \ {\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 |
|
128 \isacommand{by}{\isacharparenleft}auto\ elim{\isacharcolon}Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isanewline |
|
129 \isanewline |
|
130 \end{isabellebody}% |
|
131 %%% Local Variables: |
|
132 %%% mode: latex |
|
133 %%% TeX-master: "root" |
|
134 %%% End: |