1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{CTL}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \isamarkupsubsection{Computation Tree Logic --- CTL% |
|
19 } |
|
20 \isamarkuptrue% |
|
21 % |
|
22 \begin{isamarkuptext}% |
|
23 \label{sec:CTL} |
|
24 \index{CTL|(}% |
|
25 The semantics of PDL only needs reflexive transitive closure. |
|
26 Let us be adventurous and introduce a more expressive temporal operator. |
|
27 We extend the datatype |
|
28 \isa{formula} by a new constructor% |
|
29 \end{isamarkuptext}% |
|
30 \isamarkuptrue% |
|
31 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ AF\ formula% |
|
32 \begin{isamarkuptext}% |
|
33 \noindent |
|
34 which stands for ``\emph{A}lways in the \emph{F}uture'': |
|
35 on all infinite paths, at some point the formula holds. |
|
36 Formalizing the notion of an infinite path is easy |
|
37 in HOL: it is simply a function from \isa{nat} to \isa{state}.% |
|
38 \end{isamarkuptext}% |
|
39 \isamarkuptrue% |
|
40 \isacommand{definition}\isamarkupfalse% |
|
41 \ Paths\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state{\isaliteral{29}{\isacharparenright}}set{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
42 {\isaliteral{22}{\isachardoublequoteopen}}Paths\ s\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{7B}{\isacharbraceleft}}p{\isaliteral{2E}{\isachardot}}\ s\ {\isaliteral{3D}{\isacharequal}}\ p\ {\isadigit{0}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}p\ i{\isaliteral{2C}{\isacharcomma}}\ p{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M{\isaliteral{29}{\isacharparenright}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
43 \begin{isamarkuptext}% |
|
44 \noindent |
|
45 This definition allows a succinct statement of the semantics of \isa{AF}: |
|
46 \footnote{Do not be misled: neither datatypes nor recursive functions can be |
|
47 extended by new constructors or equations. This is just a trick of the |
|
48 presentation (see \S\ref{sec:doc-prep-suppress}). In reality one has to define |
|
49 a new datatype and a new function.}% |
|
50 \end{isamarkuptext}% |
|
51 \isamarkuptrue% |
|
52 {\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ AF\ f\ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}p\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Paths\ s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}i{\isaliteral{2E}{\isachardot}}\ p\ i\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ f{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
53 \begin{isamarkuptext}% |
|
54 \noindent |
|
55 Model checking \isa{AF} involves a function which |
|
56 is just complicated enough to warrant a separate definition:% |
|
57 \end{isamarkuptext}% |
|
58 \isamarkuptrue% |
|
59 \isacommand{definition}\isamarkupfalse% |
|
60 \ af\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ set{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
61 {\isaliteral{22}{\isachardoublequoteopen}}af\ A\ T\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ {\isaliteral{7B}{\isacharbraceleft}}s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ T{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
62 \begin{isamarkuptext}% |
|
63 \noindent |
|
64 Now we define \isa{mc\ {\isaliteral{28}{\isacharparenleft}}AF\ f{\isaliteral{29}{\isacharparenright}}} as the least set \isa{T} that includes |
|
65 \isa{mc\ f} and all states all of whose direct successors are in \isa{T}:% |
|
66 \end{isamarkuptext}% |
|
67 \isamarkuptrue% |
|
68 {\isaliteral{22}{\isachardoublequoteopen}}mc{\isaliteral{28}{\isacharparenleft}}AF\ f{\isaliteral{29}{\isacharparenright}}\ \ \ \ {\isaliteral{3D}{\isacharequal}}\ lfp{\isaliteral{28}{\isacharparenleft}}af{\isaliteral{28}{\isacharparenleft}}mc\ f{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
69 \begin{isamarkuptext}% |
|
70 \noindent |
|
71 Because \isa{af} is monotone in its second argument (and also its first, but |
|
72 that is irrelevant), \isa{af\ A} has a least fixed point:% |
|
73 \end{isamarkuptext}% |
|
74 \isamarkuptrue% |
|
75 \isacommand{lemma}\isamarkupfalse% |
|
76 \ mono{\isaliteral{5F}{\isacharunderscore}}af{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}mono{\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
77 % |
|
78 \isadelimproof |
|
79 % |
|
80 \endisadelimproof |
|
81 % |
|
82 \isatagproof |
|
83 \isacommand{apply}\isamarkupfalse% |
|
84 {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ mono{\isaliteral{5F}{\isacharunderscore}}def\ af{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline |
|
85 \isacommand{apply}\isamarkupfalse% |
|
86 \ blast\isanewline |
|
87 \isacommand{done}\isamarkupfalse% |
|
88 % |
|
89 \endisatagproof |
|
90 {\isafoldproof}% |
|
91 % |
|
92 \isadelimproof |
|
93 % |
|
94 \endisadelimproof |
|
95 % |
|
96 \isadelimproof |
|
97 % |
|
98 \endisadelimproof |
|
99 % |
|
100 \isatagproof |
|
101 % |
|
102 \endisatagproof |
|
103 {\isafoldproof}% |
|
104 % |
|
105 \isadelimproof |
|
106 % |
|
107 \endisadelimproof |
|
108 % |
|
109 \isadelimproof |
|
110 % |
|
111 \endisadelimproof |
|
112 % |
|
113 \isatagproof |
|
114 % |
|
115 \endisatagproof |
|
116 {\isafoldproof}% |
|
117 % |
|
118 \isadelimproof |
|
119 % |
|
120 \endisadelimproof |
|
121 % |
|
122 \begin{isamarkuptext}% |
|
123 All we need to prove now is \isa{mc\ {\isaliteral{28}{\isacharparenleft}}AF\ f{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}s{\isaliteral{2E}{\isachardot}}\ s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ AF\ f{\isaliteral{7D}{\isacharbraceright}}}, which states |
|
124 that \isa{mc} and \isa{{\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}} agree for \isa{AF}\@. |
|
125 This time we prove the two inclusions separately, starting |
|
126 with the easy one:% |
|
127 \end{isamarkuptext}% |
|
128 \isamarkuptrue% |
|
129 \isacommand{theorem}\isamarkupfalse% |
|
130 \ AF{\isaliteral{5F}{\isacharunderscore}}lemma{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}lfp{\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ {\isaliteral{7B}{\isacharbraceleft}}s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}p\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Paths\ s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}i{\isaliteral{2E}{\isachardot}}\ p\ i\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
131 \isadelimproof |
|
132 % |
|
133 \endisadelimproof |
|
134 % |
|
135 \isatagproof |
|
136 % |
|
137 \begin{isamarkuptxt}% |
|
138 \noindent |
|
139 In contrast to the analogous proof for \isa{EF}, and just |
|
140 for a change, we do not use fixed point induction. Park-induction, |
|
141 named after David Park, is weaker but sufficient for this proof: |
|
142 \begin{center} |
|
143 \isa{f\ S\ {\isaliteral{5C3C6C653E}{\isasymle}}\ S\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ lfp\ f\ {\isaliteral{5C3C6C653E}{\isasymle}}\ S} \hfill (\isa{lfp{\isaliteral{5F}{\isacharunderscore}}lowerbound}) |
|
144 \end{center} |
|
145 The instance of the premise \isa{f\ S\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ S} is proved pointwise, |
|
146 a decision that \isa{auto} takes for us:% |
|
147 \end{isamarkuptxt}% |
|
148 \isamarkuptrue% |
|
149 \isacommand{apply}\isamarkupfalse% |
|
150 {\isaliteral{28}{\isacharparenleft}}rule\ lfp{\isaliteral{5F}{\isacharunderscore}}lowerbound{\isaliteral{29}{\isacharparenright}}\isanewline |
|
151 \isacommand{apply}\isamarkupfalse% |
|
152 {\isaliteral{28}{\isacharparenleft}}auto\ simp\ add{\isaliteral{3A}{\isacharcolon}}\ af{\isaliteral{5F}{\isacharunderscore}}def\ Paths{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}% |
|
153 \begin{isamarkuptxt}% |
|
154 \begin{isabelle}% |
|
155 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}p{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}p\ {\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\isanewline |
|
156 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}p{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t{\isaliteral{2E}{\isachardot}}\ }{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}p{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{3D}{\isacharequal}}\ p\ {\isadigit{0}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}p\ i{\isaliteral{2C}{\isacharcomma}}\ p\ {\isaliteral{28}{\isacharparenleft}}Suc\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\isanewline |
|
157 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}p{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}p{\isaliteral{2E}{\isachardot}}\ }{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}i{\isaliteral{2E}{\isachardot}}\ p\ i\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
158 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}p{\isaliteral{2E}{\isachardot}}\ \ }{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}p\ i{\isaliteral{2C}{\isacharcomma}}\ p\ {\isaliteral{28}{\isacharparenleft}}Suc\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
159 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}p{\isaliteral{2E}{\isachardot}}\ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}i{\isaliteral{2E}{\isachardot}}\ p\ i\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A% |
|
160 \end{isabelle} |
|
161 In this remaining case, we set \isa{t} to \isa{p\ {\isadigit{1}}}. |
|
162 The rest is automatic, which is surprising because it involves |
|
163 finding the instantiation \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}i{\isaliteral{2E}{\isachardot}}\ p\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}} |
|
164 for \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}p}.% |
|
165 \end{isamarkuptxt}% |
|
166 \isamarkuptrue% |
|
167 \isacommand{apply}\isamarkupfalse% |
|
168 {\isaliteral{28}{\isacharparenleft}}erule{\isaliteral{5F}{\isacharunderscore}}tac\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}p\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{in}\ allE{\isaliteral{29}{\isacharparenright}}\isanewline |
|
169 \isacommand{apply}\isamarkupfalse% |
|
170 {\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}\isanewline |
|
171 \isacommand{done}\isamarkupfalse% |
|
172 % |
|
173 \endisatagproof |
|
174 {\isafoldproof}% |
|
175 % |
|
176 \isadelimproof |
|
177 % |
|
178 \endisadelimproof |
|
179 % |
|
180 \begin{isamarkuptext}% |
|
181 The opposite inclusion is proved by contradiction: if some state |
|
182 \isa{s} is not in \isa{lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}}, then we can construct an |
|
183 infinite \isa{A}-avoiding path starting from~\isa{s}. The reason is |
|
184 that by unfolding \isa{lfp} we find that if \isa{s} is not in |
|
185 \isa{lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}}, then \isa{s} is not in \isa{A} and there is a |
|
186 direct successor of \isa{s} that is again not in \mbox{\isa{lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}}}. Iterating this argument yields the promised infinite |
|
187 \isa{A}-avoiding path. Let us formalize this sketch. |
|
188 |
|
189 The one-step argument in the sketch above |
|
190 is proved by a variant of contraposition:% |
|
191 \end{isamarkuptext}% |
|
192 \isamarkuptrue% |
|
193 \isacommand{lemma}\isamarkupfalse% |
|
194 \ not{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{5F}{\isacharunderscore}}lfp{\isaliteral{5F}{\isacharunderscore}}afD{\isaliteral{3A}{\isacharcolon}}\isanewline |
|
195 \ {\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ lfp{\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ s\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}\ t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ t\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ lfp{\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
196 % |
|
197 \isadelimproof |
|
198 % |
|
199 \endisadelimproof |
|
200 % |
|
201 \isatagproof |
|
202 \isacommand{apply}\isamarkupfalse% |
|
203 {\isaliteral{28}{\isacharparenleft}}erule\ contrapos{\isaliteral{5F}{\isacharunderscore}}np{\isaliteral{29}{\isacharparenright}}\isanewline |
|
204 \isacommand{apply}\isamarkupfalse% |
|
205 {\isaliteral{28}{\isacharparenleft}}subst\ lfp{\isaliteral{5F}{\isacharunderscore}}unfold{\isaliteral{5B}{\isacharbrackleft}}OF\ mono{\isaliteral{5F}{\isacharunderscore}}af{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
206 \isacommand{apply}\isamarkupfalse% |
|
207 {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ af{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline |
|
208 \isacommand{done}\isamarkupfalse% |
|
209 % |
|
210 \endisatagproof |
|
211 {\isafoldproof}% |
|
212 % |
|
213 \isadelimproof |
|
214 % |
|
215 \endisadelimproof |
|
216 % |
|
217 \begin{isamarkuptext}% |
|
218 \noindent |
|
219 We assume the negation of the conclusion and prove \isa{s\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}}. |
|
220 Unfolding \isa{lfp} once and |
|
221 simplifying with the definition of \isa{af} finishes the proof. |
|
222 |
|
223 Now we iterate this process. The following construction of the desired |
|
224 path is parameterized by a predicate \isa{Q} that should hold along the path:% |
|
225 \end{isamarkuptext}% |
|
226 \isamarkuptrue% |
|
227 \isacommand{primrec}\isamarkupfalse% |
|
228 \ path\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
229 {\isaliteral{22}{\isachardoublequoteopen}}path\ s\ Q\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ s{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
230 {\isaliteral{22}{\isachardoublequoteopen}}path\ s\ Q\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}SOME\ t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}path\ s\ Q\ n{\isaliteral{2C}{\isacharcomma}}t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q\ t{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
231 \begin{isamarkuptext}% |
|
232 \noindent |
|
233 Element \isa{n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}} on this path is some arbitrary successor |
|
234 \isa{t} of element \isa{n} such that \isa{Q\ t} holds. Remember that \isa{SOME\ t{\isaliteral{2E}{\isachardot}}\ R\ t} |
|
235 is some arbitrary but fixed \isa{t} such that \isa{R\ t} holds (see \S\ref{sec:SOME}). Of |
|
236 course, such a \isa{t} need not exist, but that is of no |
|
237 concern to us since we will only use \isa{path} when a |
|
238 suitable \isa{t} does exist. |
|
239 |
|
240 Let us show that if each state \isa{s} that satisfies \isa{Q} |
|
241 has a successor that again satisfies \isa{Q}, then there exists an infinite \isa{Q}-path:% |
|
242 \end{isamarkuptext}% |
|
243 \isamarkuptrue% |
|
244 \isacommand{lemma}\isamarkupfalse% |
|
245 \ infinity{\isaliteral{5F}{\isacharunderscore}}lemma{\isaliteral{3A}{\isacharcolon}}\isanewline |
|
246 \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ Q\ s{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}s{\isaliteral{2E}{\isachardot}}\ Q\ s\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}\ t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline |
|
247 \ \ \ {\isaliteral{5C3C6578697374733E}{\isasymexists}}p{\isaliteral{5C3C696E3E}{\isasymin}}Paths\ s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ Q{\isaliteral{28}{\isacharparenleft}}p\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
248 \isadelimproof |
|
249 % |
|
250 \endisadelimproof |
|
251 % |
|
252 \isatagproof |
|
253 % |
|
254 \begin{isamarkuptxt}% |
|
255 \noindent |
|
256 First we rephrase the conclusion slightly because we need to prove simultaneously |
|
257 both the path property and the fact that \isa{Q} holds:% |
|
258 \end{isamarkuptxt}% |
|
259 \isamarkuptrue% |
|
260 \isacommand{apply}\isamarkupfalse% |
|
261 {\isaliteral{28}{\isacharparenleft}}subgoal{\isaliteral{5F}{\isacharunderscore}}tac\isanewline |
|
262 \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}p{\isaliteral{2E}{\isachardot}}\ s\ {\isaliteral{3D}{\isacharequal}}\ p\ {\isadigit{0}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}p\ i{\isaliteral{2C}{\isacharcomma}}\ p{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q{\isaliteral{28}{\isacharparenleft}}p\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}% |
|
263 \begin{isamarkuptxt}% |
|
264 \noindent |
|
265 From this proposition the original goal follows easily:% |
|
266 \end{isamarkuptxt}% |
|
267 \isamarkuptrue% |
|
268 \ \isacommand{apply}\isamarkupfalse% |
|
269 {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ Paths{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{2C}{\isacharcomma}}\ blast{\isaliteral{29}{\isacharparenright}}% |
|
270 \begin{isamarkuptxt}% |
|
271 \noindent |
|
272 The new subgoal is proved by providing the witness \isa{path\ s\ Q} for \isa{p}:% |
|
273 \end{isamarkuptxt}% |
|
274 \isamarkuptrue% |
|
275 \isacommand{apply}\isamarkupfalse% |
|
276 {\isaliteral{28}{\isacharparenleft}}rule{\isaliteral{5F}{\isacharunderscore}}tac\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}path\ s\ Q{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{in}\ exI{\isaliteral{29}{\isacharparenright}}\isanewline |
|
277 \isacommand{apply}\isamarkupfalse% |
|
278 {\isaliteral{28}{\isacharparenleft}}clarsimp{\isaliteral{29}{\isacharparenright}}% |
|
279 \begin{isamarkuptxt}% |
|
280 \noindent |
|
281 After simplification and clarification, the subgoal has the following form: |
|
282 \begin{isabelle}% |
|
283 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}i{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}Q\ s{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}s{\isaliteral{2E}{\isachardot}}\ Q\ s\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q\ t{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
284 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}i{\isaliteral{2E}{\isachardot}}\ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}path\ s\ Q\ i{\isaliteral{2C}{\isacharcomma}}\ SOME\ t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}path\ s\ Q\ i{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\isanewline |
|
285 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}i{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ }Q\ {\isaliteral{28}{\isacharparenleft}}path\ s\ Q\ i{\isaliteral{29}{\isacharparenright}}% |
|
286 \end{isabelle} |
|
287 It invites a proof by induction on \isa{i}:% |
|
288 \end{isamarkuptxt}% |
|
289 \isamarkuptrue% |
|
290 \isacommand{apply}\isamarkupfalse% |
|
291 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ i{\isaliteral{29}{\isacharparenright}}\isanewline |
|
292 \ \isacommand{apply}\isamarkupfalse% |
|
293 {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}% |
|
294 \begin{isamarkuptxt}% |
|
295 \noindent |
|
296 After simplification, the base case boils down to |
|
297 \begin{isabelle}% |
|
298 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}Q\ s{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}s{\isaliteral{2E}{\isachardot}}\ Q\ s\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q\ t{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
299 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}\ SOME\ t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M% |
|
300 \end{isabelle} |
|
301 The conclusion looks exceedingly trivial: after all, \isa{t} is chosen such that \isa{{\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M} |
|
302 holds. However, we first have to show that such a \isa{t} actually exists! This reasoning |
|
303 is embodied in the theorem \isa{someI{\isadigit{2}}{\isaliteral{5F}{\isacharunderscore}}ex}: |
|
304 \begin{isabelle}% |
|
305 \ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ a{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q\ x{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q\ {\isaliteral{28}{\isacharparenleft}}SOME\ x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x{\isaliteral{29}{\isacharparenright}}% |
|
306 \end{isabelle} |
|
307 When we apply this theorem as an introduction rule, \isa{{\isaliteral{3F}{\isacharquery}}P\ x} becomes |
|
308 \isa{{\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q\ x} and \isa{{\isaliteral{3F}{\isacharquery}}Q\ x} becomes \isa{{\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M} and we have to prove |
|
309 two subgoals: \isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q\ a}, which follows from the assumptions, and |
|
310 \isa{{\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M}, which is trivial. Thus it is not surprising that |
|
311 \isa{fast} can prove the base case quickly:% |
|
312 \end{isamarkuptxt}% |
|
313 \isamarkuptrue% |
|
314 \ \isacommand{apply}\isamarkupfalse% |
|
315 {\isaliteral{28}{\isacharparenleft}}fast\ intro{\isaliteral{3A}{\isacharcolon}}\ someI{\isadigit{2}}{\isaliteral{5F}{\isacharunderscore}}ex{\isaliteral{29}{\isacharparenright}}% |
|
316 \begin{isamarkuptxt}% |
|
317 \noindent |
|
318 What is worth noting here is that we have used \methdx{fast} rather than |
|
319 \isa{blast}. The reason is that \isa{blast} would fail because it cannot |
|
320 cope with \isa{someI{\isadigit{2}}{\isaliteral{5F}{\isacharunderscore}}ex}: unifying its conclusion with the current |
|
321 subgoal is non-trivial because of the nested schematic variables. For |
|
322 efficiency reasons \isa{blast} does not even attempt such unifications. |
|
323 Although \isa{fast} can in principle cope with complicated unification |
|
324 problems, in practice the number of unifiers arising is often prohibitive and |
|
325 the offending rule may need to be applied explicitly rather than |
|
326 automatically. This is what happens in the step case. |
|
327 |
|
328 The induction step is similar, but more involved, because now we face nested |
|
329 occurrences of \isa{SOME}. As a result, \isa{fast} is no longer able to |
|
330 solve the subgoal and we apply \isa{someI{\isadigit{2}}{\isaliteral{5F}{\isacharunderscore}}ex} by hand. We merely |
|
331 show the proof commands but do not describe the details:% |
|
332 \end{isamarkuptxt}% |
|
333 \isamarkuptrue% |
|
334 \isacommand{apply}\isamarkupfalse% |
|
335 {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}\isanewline |
|
336 \isacommand{apply}\isamarkupfalse% |
|
337 {\isaliteral{28}{\isacharparenleft}}rule\ someI{\isadigit{2}}{\isaliteral{5F}{\isacharunderscore}}ex{\isaliteral{29}{\isacharparenright}}\isanewline |
|
338 \ \isacommand{apply}\isamarkupfalse% |
|
339 {\isaliteral{28}{\isacharparenleft}}blast{\isaliteral{29}{\isacharparenright}}\isanewline |
|
340 \isacommand{apply}\isamarkupfalse% |
|
341 {\isaliteral{28}{\isacharparenleft}}rule\ someI{\isadigit{2}}{\isaliteral{5F}{\isacharunderscore}}ex{\isaliteral{29}{\isacharparenright}}\isanewline |
|
342 \ \isacommand{apply}\isamarkupfalse% |
|
343 {\isaliteral{28}{\isacharparenleft}}blast{\isaliteral{29}{\isacharparenright}}\isanewline |
|
344 \isacommand{apply}\isamarkupfalse% |
|
345 {\isaliteral{28}{\isacharparenleft}}blast{\isaliteral{29}{\isacharparenright}}\isanewline |
|
346 \isacommand{done}\isamarkupfalse% |
|
347 % |
|
348 \endisatagproof |
|
349 {\isafoldproof}% |
|
350 % |
|
351 \isadelimproof |
|
352 % |
|
353 \endisadelimproof |
|
354 % |
|
355 \begin{isamarkuptext}% |
|
356 Function \isa{path} has fulfilled its purpose now and can be forgotten. |
|
357 It was merely defined to provide the witness in the proof of the |
|
358 \isa{infinity{\isaliteral{5F}{\isacharunderscore}}lemma}. Aficionados of minimal proofs might like to know |
|
359 that we could have given the witness without having to define a new function: |
|
360 the term |
|
361 \begin{isabelle}% |
|
362 \ \ \ \ \ nat{\isaliteral{5F}{\isacharunderscore}}rec\ s\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}n\ t{\isaliteral{2E}{\isachardot}}\ SOME\ u{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ u{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q\ u{\isaliteral{29}{\isacharparenright}}% |
|
363 \end{isabelle} |
|
364 is extensionally equal to \isa{path\ s\ Q}, |
|
365 where \isa{nat{\isaliteral{5F}{\isacharunderscore}}rec} is the predefined primitive recursor on \isa{nat}.% |
|
366 \end{isamarkuptext}% |
|
367 \isamarkuptrue% |
|
368 % |
|
369 \isadelimproof |
|
370 % |
|
371 \endisadelimproof |
|
372 % |
|
373 \isatagproof |
|
374 % |
|
375 \endisatagproof |
|
376 {\isafoldproof}% |
|
377 % |
|
378 \isadelimproof |
|
379 % |
|
380 \endisadelimproof |
|
381 % |
|
382 \begin{isamarkuptext}% |
|
383 At last we can prove the opposite direction of \isa{AF{\isaliteral{5F}{\isacharunderscore}}lemma{\isadigit{1}}}:% |
|
384 \end{isamarkuptext}% |
|
385 \isamarkuptrue% |
|
386 \isacommand{theorem}\isamarkupfalse% |
|
387 \ AF{\isaliteral{5F}{\isacharunderscore}}lemma{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}p\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Paths\ s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}i{\isaliteral{2E}{\isachardot}}\ p\ i\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ lfp{\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
388 \isadelimproof |
|
389 % |
|
390 \endisadelimproof |
|
391 % |
|
392 \isatagproof |
|
393 % |
|
394 \begin{isamarkuptxt}% |
|
395 \noindent |
|
396 The proof is again pointwise and then by contraposition:% |
|
397 \end{isamarkuptxt}% |
|
398 \isamarkuptrue% |
|
399 \isacommand{apply}\isamarkupfalse% |
|
400 {\isaliteral{28}{\isacharparenleft}}rule\ subsetI{\isaliteral{29}{\isacharparenright}}\isanewline |
|
401 \isacommand{apply}\isamarkupfalse% |
|
402 {\isaliteral{28}{\isacharparenleft}}erule\ contrapos{\isaliteral{5F}{\isacharunderscore}}pp{\isaliteral{29}{\isacharparenright}}\isanewline |
|
403 \isacommand{apply}\isamarkupfalse% |
|
404 \ simp% |
|
405 \begin{isamarkuptxt}% |
|
406 \begin{isabelle}% |
|
407 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}p{\isaliteral{5C3C696E3E}{\isasymin}}Paths\ x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ p\ i\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A% |
|
408 \end{isabelle} |
|
409 Applying the \isa{infinity{\isaliteral{5F}{\isacharunderscore}}lemma} as a destruction rule leaves two subgoals, the second |
|
410 premise of \isa{infinity{\isaliteral{5F}{\isacharunderscore}}lemma} and the original subgoal:% |
|
411 \end{isamarkuptxt}% |
|
412 \isamarkuptrue% |
|
413 \isacommand{apply}\isamarkupfalse% |
|
414 {\isaliteral{28}{\isacharparenleft}}drule\ infinity{\isaliteral{5F}{\isacharunderscore}}lemma{\isaliteral{29}{\isacharparenright}}% |
|
415 \begin{isamarkuptxt}% |
|
416 \begin{isabelle}% |
|
417 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}s{\isaliteral{2E}{\isachardot}}\ s\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ t\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
418 \ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}p{\isaliteral{5C3C696E3E}{\isasymin}}Paths\ x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ p\ i\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline |
|
419 \isaindent{\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ }{\isaliteral{5C3C6578697374733E}{\isasymexists}}p{\isaliteral{5C3C696E3E}{\isasymin}}Paths\ x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ p\ i\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A% |
|
420 \end{isabelle} |
|
421 Both are solved automatically:% |
|
422 \end{isamarkuptxt}% |
|
423 \isamarkuptrue% |
|
424 \ \isacommand{apply}\isamarkupfalse% |
|
425 {\isaliteral{28}{\isacharparenleft}}auto\ dest{\isaliteral{3A}{\isacharcolon}}\ not{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{5F}{\isacharunderscore}}lfp{\isaliteral{5F}{\isacharunderscore}}afD{\isaliteral{29}{\isacharparenright}}\isanewline |
|
426 \isacommand{done}\isamarkupfalse% |
|
427 % |
|
428 \endisatagproof |
|
429 {\isafoldproof}% |
|
430 % |
|
431 \isadelimproof |
|
432 % |
|
433 \endisadelimproof |
|
434 % |
|
435 \begin{isamarkuptext}% |
|
436 If you find these proofs too complicated, we recommend that you read |
|
437 \S\ref{sec:CTL-revisited}, where we show how inductive definitions lead to |
|
438 simpler arguments. |
|
439 |
|
440 The main theorem is proved as for PDL, except that we also derive the |
|
441 necessary equality \isa{lfp{\isaliteral{28}{\isacharparenleft}}af\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}} by combining |
|
442 \isa{AF{\isaliteral{5F}{\isacharunderscore}}lemma{\isadigit{1}}} and \isa{AF{\isaliteral{5F}{\isacharunderscore}}lemma{\isadigit{2}}} on the spot:% |
|
443 \end{isamarkuptext}% |
|
444 \isamarkuptrue% |
|
445 \isacommand{theorem}\isamarkupfalse% |
|
446 \ {\isaliteral{22}{\isachardoublequoteopen}}mc\ f\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}s{\isaliteral{2E}{\isachardot}}\ s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ f{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
447 % |
|
448 \isadelimproof |
|
449 % |
|
450 \endisadelimproof |
|
451 % |
|
452 \isatagproof |
|
453 \isacommand{apply}\isamarkupfalse% |
|
454 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ f{\isaliteral{29}{\isacharparenright}}\isanewline |
|
455 \isacommand{apply}\isamarkupfalse% |
|
456 {\isaliteral{28}{\isacharparenleft}}auto\ simp\ add{\isaliteral{3A}{\isacharcolon}}\ EF{\isaliteral{5F}{\isacharunderscore}}lemma\ equalityI{\isaliteral{5B}{\isacharbrackleft}}OF\ AF{\isaliteral{5F}{\isacharunderscore}}lemma{\isadigit{1}}\ AF{\isaliteral{5F}{\isacharunderscore}}lemma{\isadigit{2}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
457 \isacommand{done}\isamarkupfalse% |
|
458 % |
|
459 \endisatagproof |
|
460 {\isafoldproof}% |
|
461 % |
|
462 \isadelimproof |
|
463 % |
|
464 \endisadelimproof |
|
465 % |
|
466 \begin{isamarkuptext}% |
|
467 The language defined above is not quite CTL\@. The latter also includes an |
|
468 until-operator \isa{EU\ f\ g} with semantics ``there \emph{E}xists a path |
|
469 where \isa{f} is true \emph{U}ntil \isa{g} becomes true''. We need |
|
470 an auxiliary function:% |
|
471 \end{isamarkuptext}% |
|
472 \isamarkuptrue% |
|
473 \isacommand{primrec}\isamarkupfalse% |
|
474 \isanewline |
|
475 until{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
476 {\isaliteral{22}{\isachardoublequoteopen}}until\ A\ B\ s\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
477 {\isaliteral{22}{\isachardoublequoteopen}}until\ A\ B\ s\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{23}{\isacharhash}}p{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ until\ A\ B\ t\ p{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
478 \begin{isamarkuptext}% |
|
479 \noindent |
|
480 Expressing the semantics of \isa{EU} is now straightforward: |
|
481 \begin{isabelle}% |
|
482 \ \ \ \ \ s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ EU\ f\ g\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}p{\isaliteral{2E}{\isachardot}}\ until\ {\isaliteral{7B}{\isacharbraceleft}}t{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ f{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{7B}{\isacharbraceleft}}t{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ g{\isaliteral{7D}{\isacharbraceright}}\ s\ p{\isaliteral{29}{\isacharparenright}}% |
|
483 \end{isabelle} |
|
484 Note that \isa{EU} is not definable in terms of the other operators! |
|
485 |
|
486 Model checking \isa{EU} is again a least fixed point construction: |
|
487 \begin{isabelle}% |
|
488 \ \ \ \ \ mc{\isaliteral{28}{\isacharparenleft}}EU\ f\ g{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ lfp{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}T{\isaliteral{2E}{\isachardot}}\ mc\ g\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ mc\ f\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ {\isaliteral{28}{\isacharparenleft}}M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ T{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}% |
|
489 \end{isabelle} |
|
490 |
|
491 \begin{exercise} |
|
492 Extend the datatype of formulae by the above until operator |
|
493 and prove the equivalence between semantics and model checking, i.e.\ that |
|
494 \begin{isabelle}% |
|
495 \ \ \ \ \ mc\ {\isaliteral{28}{\isacharparenleft}}EU\ f\ g{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}s{\isaliteral{2E}{\isachardot}}\ s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ EU\ f\ g{\isaliteral{7D}{\isacharbraceright}}% |
|
496 \end{isabelle} |
|
497 %For readability you may want to annotate {term EU} with its customary syntax |
|
498 %{text[display]"| EU formula formula E[_ U _]"} |
|
499 %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}. |
|
500 \end{exercise} |
|
501 For more CTL exercises see, for example, Huth and Ryan \cite{Huth-Ryan-book}.% |
|
502 \end{isamarkuptext}% |
|
503 \isamarkuptrue% |
|
504 % |
|
505 \isadelimproof |
|
506 % |
|
507 \endisadelimproof |
|
508 % |
|
509 \isatagproof |
|
510 % |
|
511 \endisatagproof |
|
512 {\isafoldproof}% |
|
513 % |
|
514 \isadelimproof |
|
515 % |
|
516 \endisadelimproof |
|
517 % |
|
518 \isadelimproof |
|
519 % |
|
520 \endisadelimproof |
|
521 % |
|
522 \isatagproof |
|
523 % |
|
524 \endisatagproof |
|
525 {\isafoldproof}% |
|
526 % |
|
527 \isadelimproof |
|
528 % |
|
529 \endisadelimproof |
|
530 % |
|
531 \isadelimproof |
|
532 % |
|
533 \endisadelimproof |
|
534 % |
|
535 \isatagproof |
|
536 % |
|
537 \endisatagproof |
|
538 {\isafoldproof}% |
|
539 % |
|
540 \isadelimproof |
|
541 % |
|
542 \endisadelimproof |
|
543 % |
|
544 \begin{isamarkuptext}% |
|
545 Let us close this section with a few words about the executability of |
|
546 our model checkers. It is clear that if all sets are finite, they can be |
|
547 represented as lists and the usual set operations are easily |
|
548 implemented. Only \isa{lfp} requires a little thought. Fortunately, theory |
|
549 \isa{While{\isaliteral{5F}{\isacharunderscore}}Combinator} in the Library~\cite{HOL-Library} provides a |
|
550 theorem stating that in the case of finite sets and a monotone |
|
551 function~\isa{F}, the value of \mbox{\isa{lfp\ F}} can be computed by |
|
552 iterated application of \isa{F} to~\isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}} until a fixed point is |
|
553 reached. It is actually possible to generate executable functional programs |
|
554 from HOL definitions, but that is beyond the scope of the tutorial.% |
|
555 \index{CTL|)}% |
|
556 \end{isamarkuptext}% |
|
557 \isamarkuptrue% |
|
558 % |
|
559 \isadelimtheory |
|
560 % |
|
561 \endisadelimtheory |
|
562 % |
|
563 \isatagtheory |
|
564 % |
|
565 \endisatagtheory |
|
566 {\isafoldtheory}% |
|
567 % |
|
568 \isadelimtheory |
|
569 % |
|
570 \endisadelimtheory |
|
571 \end{isabellebody}% |
|
572 %%% Local Variables: |
|
573 %%% mode: latex |
|
574 %%% TeX-master: "root" |
|
575 %%% End: |
|