doc-src/TutorialI/CTL/document/CTL.tex
 author nipkow Fri Oct 06 12:31:53 2000 +0200 (2000-10-06) changeset 10159 a72ddfdbfca0 parent 10149 7cfdf6a330a0 child 10171 59d6633835fa permissions -rw-r--r--
*** empty log message ***
1 %
2 \begin{isabellebody}%
3 \def\isabellecontext{CTL}%
4 %
5 \isamarkupsubsection{Computation tree logic---CTL}
6 %
7 \begin{isamarkuptext}%
8 The semantics of PDL only needs transitive reflexive closure.
9 Let us now be a bit more adventurous and introduce a new temporal operator
10 that goes beyond transitive reflexive closure. We extend the datatype
11 \isa{formula} by a new constructor%
12 \end{isamarkuptext}%
13 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AF\ formula%
14 \begin{isamarkuptext}%
15 \noindent
16 which stands for "always in the future":
17 on all paths, at some point the formula holds. Formalizing the notion of an infinite path is easy
18 in HOL: it is simply a function from \isa{nat} to \isa{state}.%
19 \end{isamarkuptext}%
20 \isacommand{constdefs}\ Paths\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}set{\isachardoublequote}\isanewline
21 \ \ \ \ \ \ \ \ \ {\isachardoublequote}Paths\ s\ {\isasymequiv}\ {\isacharbraceleft}p{\isachardot}\ s\ {\isacharequal}\ p\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p{\isacharparenleft}i{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}{\isacharbraceright}{\isachardoublequote}%
22 \begin{isamarkuptext}%
23 \noindent
24 This definition allows a very succinct statement of the semantics of \isa{AF}:
25 \footnote{Do not be mislead: neither datatypes nor recursive functions can be
26 extended by new constructors or equations. This is just a trick of the
27 presentation. In reality one has to define a new datatype and a new function.}%
28 \end{isamarkuptext}%
29 {\isachardoublequote}s\ {\isasymTurnstile}\ AF\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequote}%
30 \begin{isamarkuptext}%
31 \noindent
32 Model checking \isa{AF} involves a function which
33 is just complicated enough to warrant a separate definition:%
34 \end{isamarkuptext}%
35 \isacommand{constdefs}\ af\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline
36 \ \ \ \ \ \ \ \ \ {\isachardoublequote}af\ A\ T\ {\isasymequiv}\ A\ {\isasymunion}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\ t\ {\isasymin}\ T{\isacharbraceright}{\isachardoublequote}%
37 \begin{isamarkuptext}%
38 \noindent
39 Now we define \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}} as the least set \isa{T} that contains
40 \isa{mc\ f} and all states all of whose direct successors are in \isa{T}:%
41 \end{isamarkuptext}%
42 {\isachardoublequote}mc{\isacharparenleft}AF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}af{\isacharparenleft}mc\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
43 \begin{isamarkuptext}%
44 \noindent
45 Because \isa{af} is monotone in its second argument (and also its first, but
46 that is irrelevant) \isa{af\ A} has a least fixpoint:%
47 \end{isamarkuptext}%
48 \isacommand{lemma}\ mono{\isacharunderscore}af{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
49 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ mono{\isacharunderscore}def\ af{\isacharunderscore}def{\isacharparenright}\isanewline
50 \isacommand{apply}\ blast\isanewline
51 \isacommand{done}%
52 \begin{isamarkuptext}%
53 All we need to prove now is that \isa{mc} and \isa{{\isasymTurnstile}}
54 agree for \isa{AF}, i.e.\ that \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ AF\ f{\isacharbraceright}}. This time we prove the two containments separately, starting
55 with the easy one:%
56 \end{isamarkuptext}%
58 \ \ {\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}%
59 \begin{isamarkuptxt}%
60 \noindent
61 The proof is again pointwise. Fixpoint induction on the premise \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} followed
62 by simplification and clarification%
63 \end{isamarkuptxt}%
64 \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
65 \isacommand{apply}{\isacharparenleft}erule\ Lfp{\isachardot}induct{\isacharbrackleft}OF\ {\isacharunderscore}\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline
66 \isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}%
67 \begin{isamarkuptxt}%
68 \noindent
69 FIXME OF/of with undescore?
71 leads to the following somewhat involved proof state
72 \begin{isabelle}
73 \ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline
74 \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ \isadigit{0}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
75 \ \ \ \ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymand}\isanewline
76 \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\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
77 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
78 \ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
79 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A
80 \end{isabelle}
81 Now we eliminate the disjunction. The case \isa{p\ \isadigit{0}\ {\isasymin}\ A} is trivial:%
82 \end{isamarkuptxt}%
83 \isacommand{apply}{\isacharparenleft}erule\ disjE{\isacharparenright}\isanewline
84 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}%
85 \begin{isamarkuptxt}%
86 \noindent
87 In the other case we set \isa{t} to \isa{p\ \isadigit{1}} and simplify matters:%
88 \end{isamarkuptxt}%
89 \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ \isadigit{1}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
90 \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
91 \begin{isamarkuptxt}%
92 \begin{isabelle}
93 \ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\ p\ \isadigit{1}\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharsemicolon}\isanewline
94 \ \ \ \ \ \ \ \ \ \ \ {\isasymforall}pa{\isachardot}\ p\ \isadigit{1}\ {\isacharequal}\ pa\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
95 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
96 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A
97 \end{isabelle}
98 It merely remains to set \isa{pa} to \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ \isadigit{1}{\isacharparenright}}, i.e.\ \isa{p} without its
99 first element. The rest is practically automatic:%
100 \end{isamarkuptxt}%
101 \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ p{\isacharparenleft}i{\isacharplus}\isadigit{1}{\isacharparenright}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
102 \isacommand{apply}\ simp\isanewline
103 \isacommand{apply}\ blast\isanewline
104 \isacommand{done}%
105 \begin{isamarkuptext}%
106 The opposite containment is proved by contradiction: if some state
107 \isa{s} is not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then we can construct an
108 infinite \isa{A}-avoiding path starting from \isa{s}. The reason is
109 that by unfolding \isa{lfp} we find that if \isa{s} is not in
110 \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then \isa{s} is not in \isa{A} and there is a
111 direct successor of \isa{s} that is again not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Iterating this argument yields the promised infinite
112 \isa{A}-avoiding path. Let us formalize this sketch.
114 The one-step argument in the above sketch%
115 \end{isamarkuptext}%
116 \isacommand{lemma}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharcolon}\isanewline
117 \ {\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
118 \isacommand{apply}{\isacharparenleft}erule\ swap{\isacharparenright}\isanewline
119 \isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}Tarski{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline
121 \isacommand{done}%
122 \begin{isamarkuptext}%
123 \noindent
124 is proved by a variant of contraposition (\isa{swap}:
125 \isa{{\isasymlbrakk}{\isasymnot}\ Pa{\isacharsemicolon}\ {\isasymnot}\ P\ {\isasymLongrightarrow}\ Pa{\isasymrbrakk}\ {\isasymLongrightarrow}\ P}), i.e.\ assuming the negation of the conclusion
126 and proving \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Unfolding \isa{lfp} once and
127 simplifying with the definition of \isa{af} finishes the proof.
129 Now we iterate this process. The following construction of the desired
130 path is parameterized by a predicate \isa{P} that should hold along the path:%
131 \end{isamarkuptext}%
132 \isacommand{consts}\ path\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}state\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}{\isachardoublequote}\isanewline
133 \isacommand{primrec}\isanewline
134 {\isachardoublequote}path\ s\ P\ \isadigit{0}\ {\isacharequal}\ s{\isachardoublequote}\isanewline
135 {\isachardoublequote}path\ s\ P\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ P\ n{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isachardoublequote}%
136 \begin{isamarkuptext}%
137 \noindent
138 Element \isa{n\ {\isacharplus}\ \isadigit{1}} on this path is some arbitrary successor
139 \isa{t} of element \isa{n} such that \isa{P\ t} holds.  Remember that \isa{SOME\ t{\isachardot}\ R\ t}
140 is some arbitrary but fixed \isa{t} such that \isa{R\ t} holds (see \S\ref{sec-SOME}). Of
141 course, such a \isa{t} may in general not exist, but that is of no
142 concern to us since we will only use \isa{path} in such cases where a
143 suitable \isa{t} does exist.
145 Let us show that if each state \isa{s} that satisfies \isa{P}
146 has a successor that again satisfies \isa{P}, then there exists an infinite \isa{P}-path:%
147 \end{isamarkuptext}%
148 \isacommand{lemma}\ infinity{\isacharunderscore}lemma{\isacharcolon}\isanewline
149 \ \ {\isachardoublequote}{\isasymlbrakk}\ P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\isanewline
150 \ \ \ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}%
151 \begin{isamarkuptxt}%
152 \noindent
153 First we rephrase the conclusion slightly because we need to prove both the path property
154 and the fact that \isa{P} holds simultaneously:%
155 \end{isamarkuptxt}%
156 \isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}{\isasymexists}p{\isachardot}\ s\ {\isacharequal}\ p\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}p{\isacharparenleft}i{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}%
157 \begin{isamarkuptxt}%
158 \noindent
159 From this proposition the original goal follows easily:%
160 \end{isamarkuptxt}%
161 \ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}%
162 \begin{isamarkuptxt}%
163 \noindent
164 The new subgoal is proved by providing the witness \isa{path\ s\ P} for \isa{p}:%
165 \end{isamarkuptxt}%
166 \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}path\ s\ P{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
167 \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
168 \begin{isamarkuptxt}%
169 \noindent
170 After simplification and clarification the subgoal has the following compact form
171 \begin{isabelle}
172 \ \isadigit{1}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline
173 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\isanewline
174 \ \ \ \ \ \ \ \ \ \ \ \ P\ {\isacharparenleft}path\ s\ P\ i{\isacharparenright}
175 \end{isabelle}
176 and invites a proof by induction on \isa{i}:%
177 \end{isamarkuptxt}%
178 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline
179 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}%
180 \begin{isamarkuptxt}%
181 \noindent
182 After simplification the base case boils down to
183 \begin{isabelle}
184 \ \isadigit{1}{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline
185 \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M
186 \end{isabelle}
187 The conclusion looks exceedingly trivial: after all, \isa{t} is chosen such that \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M}
188 holds. However, we first have to show that such a \isa{t} actually exists! This reasoning
189 is embodied in the theorem \isa{someI\isadigit{2}{\isacharunderscore}ex}:
190 \begin{isabelle}%
191 \ \ \ \ \ {\isasymlbrakk}{\isasymexists}a{\isachardot}\ {\isacharquery}P\ a{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharparenleft}Eps\ {\isacharquery}P{\isacharparenright}%
192 \end{isabelle}
193 When we apply this theorem as an introduction rule, \isa{{\isacharquery}P\ x} becomes
194 \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ x} and \isa{{\isacharquery}Q\ x} becomes \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M} and we have to prove
195 two subgoals: \isa{{\isasymexists}a{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ a{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ a}, which follows from the assumptions, and
196 \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ x\ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M}, which is trivial. Thus it is not surprising that
197 \isa{fast} can prove the base case quickly:%
198 \end{isamarkuptxt}%
199 \ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}%
200 \begin{isamarkuptxt}%
201 \noindent
202 What is worth noting here is that we have used \isa{fast} rather than \isa{blast}.
203 The reason is that \isa{blast} would fail because it cannot cope with \isa{someI\isadigit{2}{\isacharunderscore}ex}:
204 unifying its conclusion with the current subgoal is nontrivial because of the nested schematic
205 variables. For efficiency reasons \isa{blast} does not even attempt such unifications.
206 Although \isa{fast} can in principle cope with complicated unification problems, in practice
207 the number of unifiers arising is often prohibitive and the offending rule may need to be applied
208 explicitly rather than automatically.
210 The induction step is similar, but more involved, because now we face nested occurrences of
211 \isa{SOME}. We merely show the proof commands but do not describe th details:%
212 \end{isamarkuptxt}%
213 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
215 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
217 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
218 \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
219 \isacommand{done}%
220 \begin{isamarkuptext}%
221 Function \isa{path} has fulfilled its purpose now and can be forgotten
222 about. It was merely defined to provide the witness in the proof of the
223 \isa{infinity{\isacharunderscore}lemma}. Afficionados of minimal proofs might like to know
224 that we could have given the witness without having to define a new function:
225 the term
226 \begin{isabelle}%
227 \ \ \ \ \ nat{\isacharunderscore}rec\ s\ {\isacharparenleft}{\isasymlambda}n\ t{\isachardot}\ SOME\ u{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ u{\isacharparenright}%
228 \end{isabelle}
229 where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}, whose defining
230 equations we omit, is extensionally equal to \isa{path\ s\ P}.%
231 \end{isamarkuptext}%
232 %
233 \begin{isamarkuptext}%
234 At last we can prove the opposite direction of \isa{AF{\isacharunderscore}lemma\isadigit{1}}:%
235 \end{isamarkuptext}%
237 {\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}%
238 \begin{isamarkuptxt}%
239 \noindent
240 The proof is again pointwise and then by contraposition (\isa{contrapos\isadigit{2}} is the rule
241 \isa{{\isasymlbrakk}{\isacharquery}Q{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P\ {\isasymLongrightarrow}\ {\isasymnot}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P}):%
242 \end{isamarkuptxt}%
243 \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
245 \isacommand{apply}\ simp%
246 \begin{isamarkuptxt}%
247 \begin{isabelle}
248 \ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A
249 \end{isabelle}
250 Applying the \isa{infinity{\isacharunderscore}lemma} as a destruction rule leaves two subgoals, the second
251 premise of \isa{infinity{\isacharunderscore}lemma} and the original subgoal:%
252 \end{isamarkuptxt}%
253 \isacommand{apply}{\isacharparenleft}drule\ infinity{\isacharunderscore}lemma{\isacharparenright}%
254 \begin{isamarkuptxt}%
255 \begin{isabelle}
256 \ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\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
257 \ \isadigit{2}{\isachardot}\ {\isasymAnd}s{\isachardot}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline
258 \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A
259 \end{isabelle}
260 Both are solved automatically:%
261 \end{isamarkuptxt}%
262 \ \isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline
263 \isacommand{done}%
264 \begin{isamarkuptext}%
265 The main theorem is proved as for PDL, except that we also derive the necessary equality
266 \isa{lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isacharequal}\ {\isachardot}{\isachardot}{\isachardot}} by combining \isa{AF{\isacharunderscore}lemma\isadigit{1}} and \isa{AF{\isacharunderscore}lemma\isadigit{2}}
267 on the spot:%
268 \end{isamarkuptext}%
269 \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline
270 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
272 \isacommand{done}%
273 \begin{isamarkuptext}%
274 Let us close this section with a few words about the executability of \isa{mc}.
275 It is clear that if all sets are finite, they can be represented as lists and the usual
276 set operations are easily implemented. Only \isa{lfp} requires a little thought.
277 Fortunately the HOL library proves that in the case of finite sets and a monotone \isa{F},
278 \isa{lfp\ F} can be computed by iterated application of \isa{F} to \isa{{\isacharbraceleft}{\isacharbraceright}} until
279 a fixpoint is reached. It is possible to generate executable functional programs
280 from HOL definitions, but that is beyond the scope of the tutorial.%
281 \end{isamarkuptext}%
282 \end{isabellebody}%
283 %%% Local Variables:
284 %%% mode: latex
285 %%% TeX-master: "root"
286 %%% End: