1 (*<*)theory CTL = Base:(*>*) |
1 (*<*)theory CTL = Base:;(*>*) |
2 |
2 |
3 subsection{*Computation tree logic---CTL*} |
3 subsection{*Computation tree logic---CTL*}; |
4 |
4 |
5 text{* |
5 text{* |
6 The semantics of PDL only needs transitive reflexive closure. |
6 The semantics of PDL only needs transitive reflexive closure. |
7 Let us now be a bit more adventurous and introduce a new temporal operator |
7 Let us now be a bit more adventurous and introduce a new temporal operator |
8 that goes beyond transitive reflexive closure. We extend the datatype |
8 that goes beyond transitive reflexive closure. We extend the datatype |
9 @{text formula} by a new constructor |
9 @{text formula} by a new constructor |
10 *} |
10 *}; |
11 (*<*) |
11 (*<*) |
12 datatype formula = Atom atom |
12 datatype formula = Atom atom |
13 | Neg formula |
13 | Neg formula |
14 | And formula formula |
14 | And formula formula |
15 | AX formula |
15 | AX formula |
16 | EF formula(*>*) |
16 | EF formula(*>*) |
17 | AF formula |
17 | AF formula; |
18 |
18 |
19 text{*\noindent |
19 text{*\noindent |
20 which stands for "always in the future": |
20 which stands for "always in the future": |
21 on all paths, at some point the formula holds. |
21 on all paths, at some point the formula holds. Formalizing the notion of an infinite path is easy |
22 Introducing the notion of paths (in @{term M}) |
22 in HOL: it is simply a function from @{typ nat} to @{typ state}. |
23 *} |
23 *}; |
24 |
24 |
25 constdefs Paths :: "state \<Rightarrow> (nat \<Rightarrow> state)set" |
25 constdefs Paths :: "state \<Rightarrow> (nat \<Rightarrow> state)set" |
26 "Paths s \<equiv> {p. s = p 0 \<and> (\<forall>i. (p i, p(i+1)) \<in> M)}"; |
26 "Paths s \<equiv> {p. s = p 0 \<and> (\<forall>i. (p i, p(i+1)) \<in> M)}"; |
27 |
27 |
28 text{*\noindent |
28 text{*\noindent |
29 allows a very succinct definition of the semantics of @{term AF}: |
29 This definition allows a very succinct statement of the semantics of @{term AF}: |
30 \footnote{Do not be mislead: neither datatypes nor recursive functions can be |
30 \footnote{Do not be mislead: neither datatypes nor recursive functions can be |
31 extended by new constructors or equations. This is just a trick of the |
31 extended by new constructors or equations. This is just a trick of the |
32 presentation. In reality one has to define a new datatype and a new function.} |
32 presentation. In reality one has to define a new datatype and a new function.} |
33 *} |
33 *}; |
34 (*<*) |
34 (*<*) |
35 consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80) |
35 consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80); |
36 |
36 |
37 primrec |
37 primrec |
38 "s \<Turnstile> Atom a = (a \<in> L s)" |
38 "s \<Turnstile> Atom a = (a \<in> L s)" |
39 "s \<Turnstile> Neg f = (~(s \<Turnstile> f))" |
39 "s \<Turnstile> Neg f = (~(s \<Turnstile> f))" |
40 "s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)" |
40 "s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)" |
43 (*>*) |
43 (*>*) |
44 "s \<Turnstile> AF f = (\<forall>p \<in> Paths s. \<exists>i. p i \<Turnstile> f)"; |
44 "s \<Turnstile> AF f = (\<forall>p \<in> Paths s. \<exists>i. p i \<Turnstile> f)"; |
45 |
45 |
46 text{*\noindent |
46 text{*\noindent |
47 Model checking @{term AF} involves a function which |
47 Model checking @{term AF} involves a function which |
48 is just large enough to warrant a separate definition: |
48 is just complicated enough to warrant a separate definition: |
49 *} |
49 *}; |
50 |
50 |
51 constdefs af :: "state set \<Rightarrow> state set \<Rightarrow> state set" |
51 constdefs af :: "state set \<Rightarrow> state set \<Rightarrow> state set" |
52 "af A T \<equiv> A \<union> {s. \<forall>t. (s, t) \<in> M \<longrightarrow> t \<in> T}"; |
52 "af A T \<equiv> A \<union> {s. \<forall>t. (s, t) \<in> M \<longrightarrow> t \<in> T}"; |
53 |
53 |
54 text{*\noindent |
54 text{*\noindent |
55 This function is monotone in its second argument (and also its first, but |
55 Now we define @{term "mc(AF f)"} as the least set @{term T} that contains |
56 that is irrelevant), and hence @{term"af A"} has a least fixpoint. |
|
57 *} |
|
58 |
|
59 lemma mono_af: "mono(af A)"; |
|
60 apply(simp add: mono_def af_def) |
|
61 by(blast); |
|
62 |
|
63 text{*\noindent |
|
64 Now we can define @{term "mc(AF f)"} as the least set @{term T} that contains |
|
65 @{term"mc f"} and all states all of whose direct successors are in @{term T}: |
56 @{term"mc f"} and all states all of whose direct successors are in @{term T}: |
66 *} |
57 *}; |
67 (*<*) |
58 (*<*) |
68 consts mc :: "formula \<Rightarrow> state set"; |
59 consts mc :: "formula \<Rightarrow> state set"; |
69 primrec |
60 primrec |
70 "mc(Atom a) = {s. a \<in> L s}" |
61 "mc(Atom a) = {s. a \<in> L s}" |
71 "mc(Neg f) = -mc f" |
62 "mc(Neg f) = -mc f" |
72 "mc(And f g) = mc f \<inter> mc g" |
63 "mc(And f g) = mc f \<inter> mc g" |
73 "mc(AX f) = {s. \<forall>t. (s,t) \<in> M \<longrightarrow> t \<in> mc f}" |
64 "mc(AX f) = {s. \<forall>t. (s,t) \<in> M \<longrightarrow> t \<in> mc f}" |
74 "mc(EF f) = lfp(\<lambda>T. mc f \<union> M^-1 ^^ T)"(*>*) |
65 "mc(EF f) = lfp(\<lambda>T. mc f \<union> M^-1 ^^ T)"(*>*) |
75 "mc(AF f) = lfp(af(mc f))"; |
66 "mc(AF f) = lfp(af(mc f))"; |
76 (*<*) |
67 |
77 lemma mono_ef: "mono(\<lambda>T. A \<union> M^-1 ^^ T)" |
68 text{*\noindent |
78 apply(rule monoI) |
69 Because @{term af} is monotone in its second argument (and also its first, but |
79 by(blast) |
70 that is irrelevant) @{term"af A"} has a least fixpoint: |
|
71 *}; |
|
72 |
|
73 lemma mono_af: "mono(af A)"; |
|
74 apply(simp add: mono_def af_def); |
|
75 apply blast; |
|
76 done |
|
77 (*<*) |
|
78 lemma mono_ef: "mono(\<lambda>T. A \<union> M^-1 ^^ T)"; |
|
79 apply(rule monoI); |
|
80 by(blast); |
80 |
81 |
81 lemma EF_lemma: |
82 lemma EF_lemma: |
82 "lfp(\<lambda>T. A \<union> M^-1 ^^ T) = {s. \<exists>t. (s,t) \<in> M^* \<and> t \<in> A}" |
83 "lfp(\<lambda>T. A \<union> M^-1 ^^ T) = {s. \<exists>t. (s,t) \<in> M^* \<and> t \<in> A}"; |
83 apply(rule equalityI); |
84 apply(rule equalityI); |
84 apply(rule subsetI); |
85 apply(rule subsetI); |
85 apply(simp) |
86 apply(simp); |
86 apply(erule Lfp.induct) |
87 apply(erule Lfp.induct); |
87 apply(rule mono_ef) |
88 apply(rule mono_ef); |
88 apply(simp) |
89 apply(simp); |
89 apply(blast intro: r_into_rtrancl rtrancl_trans); |
90 apply(blast intro: r_into_rtrancl rtrancl_trans); |
90 apply(rule subsetI) |
91 apply(rule subsetI); |
91 apply(simp, clarify) |
92 apply(simp, clarify); |
92 apply(erule converse_rtrancl_induct) |
93 apply(erule converse_rtrancl_induct); |
93 apply(rule ssubst[OF lfp_Tarski[OF mono_ef]]) |
94 apply(rule ssubst[OF lfp_Tarski[OF mono_ef]]); |
94 apply(blast) |
95 apply(blast); |
95 apply(rule ssubst[OF lfp_Tarski[OF mono_ef]]) |
96 apply(rule ssubst[OF lfp_Tarski[OF mono_ef]]); |
96 by(blast) |
97 by(blast); |
97 (*>*) |
98 (*>*) |
98 |
99 text{* |
99 theorem lfp_subset_AF: |
100 All we need to prove now is that @{term mc} and @{text"\<Turnstile>"} |
100 "lfp(af A) \<subseteq> {s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A}"; |
101 agree for @{term AF}, i.e.\ that @{prop"mc(AF f) = {s. s \<Turnstile> |
|
102 AF f}"}. This time we prove the two containments separately, starting |
|
103 with the easy one: |
|
104 *}; |
|
105 |
|
106 theorem AF_lemma1: |
|
107 "lfp(af A) \<subseteq> {s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A}"; |
|
108 |
|
109 txt{*\noindent |
|
110 The proof is again pointwise. Fixpoint induction on the premise @{prop"s \<in> lfp(af A)"} followed |
|
111 by simplification and clarification |
|
112 *}; |
|
113 |
101 apply(rule subsetI); |
114 apply(rule subsetI); |
102 apply(erule Lfp.induct[OF _ mono_af]); |
115 apply(erule Lfp.induct[OF _ mono_af]); |
103 apply(simp add: af_def Paths_def); |
116 apply(clarsimp simp add: af_def Paths_def); |
|
117 (*ML"Pretty.setmargin 70"; |
|
118 pr(latex xsymbols symbols);*) |
|
119 txt{*\noindent |
|
120 FIXME OF/of with undescore? |
|
121 |
|
122 leads to the following somewhat involved proof state |
|
123 \begin{isabelle} |
|
124 \ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline |
|
125 \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ \isadigit{0}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline |
|
126 \ \ \ \ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymand}\isanewline |
|
127 \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\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 |
|
128 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline |
|
129 \ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline |
|
130 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A |
|
131 \end{isabelle} |
|
132 Now we eliminate the disjunction. The case @{prop"p 0 \<in> A"} is trivial: |
|
133 *}; |
|
134 |
104 apply(erule disjE); |
135 apply(erule disjE); |
105 apply(blast); |
136 apply(blast); |
106 apply(clarify); |
137 |
|
138 txt{*\noindent |
|
139 In the other case we set @{term t} to @{term"p 1"} and simplify matters: |
|
140 *}; |
|
141 |
107 apply(erule_tac x = "p 1" in allE); |
142 apply(erule_tac x = "p 1" in allE); |
108 apply(clarsimp); |
143 apply(clarsimp); |
|
144 (*ML"Pretty.setmargin 70"; |
|
145 pr(latex xsymbols symbols);*) |
|
146 |
|
147 txt{* |
|
148 \begin{isabelle} |
|
149 \ \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 |
|
150 \ \ \ \ \ \ \ \ \ \ \ {\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 |
|
151 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline |
|
152 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A |
|
153 \end{isabelle} |
|
154 It merely remains to set @{term pa} to @{term"\<lambda>i. p(i+1)"}, i.e.\ @{term p} without its |
|
155 first element. The rest is practically automatic: |
|
156 *}; |
|
157 |
109 apply(erule_tac x = "\<lambda>i. p(i+1)" in allE); |
158 apply(erule_tac x = "\<lambda>i. p(i+1)" in allE); |
110 apply(simp); |
159 apply simp; |
111 by(blast); |
160 apply blast; |
112 |
161 done; |
113 text{* |
162 |
114 The opposite direction is proved by contradiction: if some state |
163 text{* |
115 {term s} is not in @{term"lfp(af A)"}, then we can construct an |
164 The opposite containment is proved by contradiction: if some state |
|
165 @{term s} is not in @{term"lfp(af A)"}, then we can construct an |
116 infinite @{term A}-avoiding path starting from @{term s}. The reason is |
166 infinite @{term A}-avoiding path starting from @{term s}. The reason is |
117 that by unfolding @{term"lfp"} we find that if @{term s} is not in |
167 that by unfolding @{term lfp} we find that if @{term s} is not in |
118 @{term"lfp(af A)"}, then @{term s} is not in @{term A} and there is a |
168 @{term"lfp(af A)"}, then @{term s} is not in @{term A} and there is a |
119 direct successor of @{term s} that is again not in @{term"lfp(af |
169 direct successor of @{term s} that is again not in @{term"lfp(af |
120 A)"}. Iterating this argument yields the promised infinite |
170 A)"}. Iterating this argument yields the promised infinite |
121 @{term A}-avoiding path. Let us formalize this sketch. |
171 @{term A}-avoiding path. Let us formalize this sketch. |
122 |
172 |
144 "path s P 0 = s" |
195 "path s P 0 = s" |
145 "path s P (Suc n) = (SOME t. (path s P n,t) \<in> M \<and> P t)"; |
196 "path s P (Suc n) = (SOME t. (path s P n,t) \<in> M \<and> P t)"; |
146 |
197 |
147 text{*\noindent |
198 text{*\noindent |
148 Element @{term"n+1"} on this path is some arbitrary successor |
199 Element @{term"n+1"} on this path is some arbitrary successor |
149 @{term"t"} of element @{term"n"} such that @{term"P t"} holds. Of |
200 @{term t} of element @{term n} such that @{term"P t"} holds. Remember that @{text"SOME t. R t"} |
150 course, such a @{term"t"} may in general not exist, but that is of no |
201 is some arbitrary but fixed @{term t} such that @{prop"R t"} holds (see \S\ref{sec-SOME}). Of |
|
202 course, such a @{term t} may in general not exist, but that is of no |
151 concern to us since we will only use @{term path} in such cases where a |
203 concern to us since we will only use @{term path} in such cases where a |
152 suitable @{term"t"} does exist. |
204 suitable @{term t} does exist. |
153 |
205 |
154 Now we prove that if each state @{term"s"} that satisfies @{term"P"} |
206 Let us show that if each state @{term s} that satisfies @{term P} |
155 has a successor that again satisfies @{term"P"}, then there exists an infinite @{term"P"}-path. |
207 has a successor that again satisfies @{term P}, then there exists an infinite @{term P}-path: |
156 *}; |
208 *}; |
157 |
209 |
158 lemma seq_lemma: |
210 lemma infinity_lemma: |
159 "\<lbrakk> P s; \<forall>s. P s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> P t) \<rbrakk> \<Longrightarrow> \<exists>p\<in>Paths s. \<forall>i. P(p i)"; |
211 "\<lbrakk> P s; \<forall>s. P s \<longrightarrow> (\<exists> t. (s,t) \<in> M \<and> P t) \<rbrakk> \<Longrightarrow> |
|
212 \<exists>p\<in>Paths s. \<forall>i. P(p i)"; |
160 |
213 |
161 txt{*\noindent |
214 txt{*\noindent |
162 First we rephrase the conclusion slightly because we need to prove both the path property |
215 First we rephrase the conclusion slightly because we need to prove both the path property |
163 and the fact that @{term"P"} holds simultaneously: |
216 and the fact that @{term P} holds simultaneously: |
164 *}; |
217 *}; |
165 |
218 |
166 apply(subgoal_tac "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(i+1)) \<in> M \<and> P(p i))"); |
219 apply(subgoal_tac "\<exists>p. s = p 0 \<and> (\<forall>i. (p i,p(i+1)) \<in> M \<and> P(p i))"); |
167 |
220 |
168 txt{*\noindent |
221 txt{*\noindent |
169 From this proposition the original goal follows easily |
222 From this proposition the original goal follows easily: |
170 *}; |
223 *}; |
171 |
224 |
172 apply(simp add:Paths_def, blast); |
225 apply(simp add:Paths_def, blast); |
|
226 |
|
227 txt{*\noindent |
|
228 The new subgoal is proved by providing the witness @{term "path s P"} for @{term p}: |
|
229 *}; |
|
230 |
173 apply(rule_tac x = "path s P" in exI); |
231 apply(rule_tac x = "path s P" in exI); |
174 apply(simp); |
232 apply(clarsimp); |
175 apply(intro strip); |
233 (*ML"Pretty.setmargin 70"; |
|
234 pr(latex xsymbols symbols);*) |
|
235 |
|
236 txt{*\noindent |
|
237 After simplification and clarification the subgoal has the following compact form |
|
238 \begin{isabelle} |
|
239 \ \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 |
|
240 \ \ \ \ \ \ \ \ {\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 |
|
241 \ \ \ \ \ \ \ \ \ \ \ \ P\ {\isacharparenleft}path\ s\ P\ i{\isacharparenright} |
|
242 \end{isabelle} |
|
243 and invites a proof by induction on @{term i}: |
|
244 *}; |
|
245 |
176 apply(induct_tac i); |
246 apply(induct_tac i); |
177 apply(simp); |
247 apply(simp); |
|
248 (*ML"Pretty.setmargin 70"; |
|
249 pr(latex xsymbols symbols);*) |
|
250 |
|
251 txt{*\noindent |
|
252 After simplification the base case boils down to |
|
253 \begin{isabelle} |
|
254 \ \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 |
|
255 \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M |
|
256 \end{isabelle} |
|
257 The conclusion looks exceedingly trivial: after all, @{term t} is chosen such that @{prop"(s,t):M"} |
|
258 holds. However, we first have to show that such a @{term t} actually exists! This reasoning |
|
259 is embodied in the theorem @{thm[source]someI2_ex}: |
|
260 @{thm[display,eta_contract=false]someI2_ex} |
|
261 When we apply this theorem as an introduction rule, @{text"?P x"} becomes |
|
262 @{prop"(s, x) : M & P x"} and @{text"?Q x"} becomes @{prop"(s,x) : M"} and we have to prove |
|
263 two subgoals: @{prop"EX a. (s, a) : M & P a"}, which follows from the assumptions, and |
|
264 @{prop"(s, x) : M & P x ==> (s,x) : M"}, which is trivial. Thus it is not surprising that |
|
265 @{text fast} can prove the base case quickly: |
|
266 *}; |
|
267 |
178 apply(fast intro:someI2_ex); |
268 apply(fast intro:someI2_ex); |
|
269 |
|
270 txt{*\noindent |
|
271 What is worth noting here is that we have used @{text fast} rather than @{text blast}. |
|
272 The reason is that @{text blast} would fail because it cannot cope with @{thm[source]someI2_ex}: |
|
273 unifying its conclusion with the current subgoal is nontrivial because of the nested schematic |
|
274 variables. For efficiency reasons @{text blast} does not even attempt such unifications. |
|
275 Although @{text fast} can in principle cope with complicated unification problems, in practice |
|
276 the number of unifiers arising is often prohibitive and the offending rule may need to be applied |
|
277 explicitly rather than automatically. |
|
278 |
|
279 The induction step is similar, but more involved, because now we face nested occurrences of |
|
280 @{text SOME}. We merely show the proof commands but do not describe th details: |
|
281 *}; |
|
282 |
179 apply(simp); |
283 apply(simp); |
180 apply(rule someI2_ex); |
284 apply(rule someI2_ex); |
181 apply(blast); |
285 apply(blast); |
182 apply(rule someI2_ex); |
286 apply(rule someI2_ex); |
183 apply(blast); |
287 apply(blast); |
184 by(blast); |
288 apply(blast); |
185 |
289 done; |
186 lemma seq_lemma: |
290 |
|
291 text{* |
|
292 Function @{term path} has fulfilled its purpose now and can be forgotten |
|
293 about. It was merely defined to provide the witness in the proof of the |
|
294 @{thm[source]infinity_lemma}. Afficionados of minimal proofs might like to know |
|
295 that we could have given the witness without having to define a new function: |
|
296 the term |
|
297 @{term[display]"nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> P u)"} |
|
298 where @{term nat_rec} is the predefined primitive recursor on @{typ nat}, whose defining |
|
299 equations we omit, is extensionally equal to @{term"path s P"}. |
|
300 *}; |
|
301 (*<*) |
|
302 lemma infinity_lemma: |
187 "\<lbrakk> P s; \<forall> s. P s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> P t) \<rbrakk> \<Longrightarrow> |
303 "\<lbrakk> P s; \<forall> s. P s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> P t) \<rbrakk> \<Longrightarrow> |
188 \<exists> p\<in>Paths s. \<forall> i. P(p i)"; |
304 \<exists> p\<in>Paths s. \<forall> i. P(p i)"; |
189 apply(subgoal_tac |
305 apply(subgoal_tac |
190 "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> P(p i))"); |
306 "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> P(p i))"); |
191 apply(simp add:Paths_def); |
307 apply(simp add:Paths_def); |
200 apply(rule someI2_ex); |
316 apply(rule someI2_ex); |
201 apply(blast); |
317 apply(blast); |
202 apply(rule someI2_ex); |
318 apply(rule someI2_ex); |
203 apply(blast); |
319 apply(blast); |
204 by(blast); |
320 by(blast); |
205 |
321 (*>*) |
206 theorem AF_subset_lfp: |
322 |
|
323 text{* |
|
324 At last we can prove the opposite direction of @{thm[source]AF_lemma1}: |
|
325 *}; |
|
326 |
|
327 theorem AF_lemma2: |
207 "{s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)"; |
328 "{s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)"; |
|
329 |
|
330 txt{*\noindent |
|
331 The proof is again pointwise and then by contraposition (@{thm[source]contrapos2} is the rule |
|
332 @{thm contrapos2}): |
|
333 *}; |
|
334 |
208 apply(rule subsetI); |
335 apply(rule subsetI); |
209 apply(erule contrapos2); |
336 apply(erule contrapos2); |
210 apply simp; |
337 apply simp; |
211 apply(drule seq_lemma); |
338 (*pr(latex xsymbols symbols);*) |
212 by(auto dest:not_in_lfp_afD); |
339 |
213 |
340 txt{* |
214 |
341 \begin{isabelle} |
|
342 \ \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 |
|
343 \end{isabelle} |
|
344 Applying the @{thm[source]infinity_lemma} as a destruction rule leaves two subgoals, the second |
|
345 premise of @{thm[source]infinity_lemma} and the original subgoal: |
|
346 *}; |
|
347 |
|
348 apply(drule infinity_lemma); |
|
349 (*pr(latex xsymbols symbols);*) |
|
350 |
|
351 txt{* |
|
352 \begin{isabelle} |
|
353 \ \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 |
|
354 \ \isadigit{2}{\isachardot}\ {\isasymAnd}s{\isachardot}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline |
|
355 \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A |
|
356 \end{isabelle} |
|
357 Both are solved automatically: |
|
358 *}; |
|
359 |
|
360 apply(auto dest:not_in_lfp_afD); |
|
361 done; |
|
362 |
|
363 text{* |
|
364 The main theorem is proved as for PDL, except that we also derive the necessary equality |
|
365 @{text"lfp(af A) = ..."} by combining @{thm[source]AF_lemma1} and @{thm[source]AF_lemma2} |
|
366 on the spot: |
|
367 *} |
|
368 |
|
369 theorem "mc f = {s. s \<Turnstile> f}"; |
|
370 apply(induct_tac f); |
|
371 apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2]); |
|
372 done |
|
373 |
|
374 text{* |
|
375 Let us close this section with a few words about the executability of @{term mc}. |
|
376 It is clear that if all sets are finite, they can be represented as lists and the usual |
|
377 set operations are easily implemented. Only @{term lfp} requires a little thought. |
|
378 Fortunately the HOL library proves that in the case of finite sets and a monotone @{term F}, |
|
379 @{term"lfp F"} can be computed by iterated application of @{term F} to @{term"{}"} until |
|
380 a fixpoint is reached. It is possible to generate executable functional programs |
|
381 from HOL definitions, but that is beyond the scope of the tutorial. |
|
382 *} |
|
383 |
|
384 (*<*) |
215 (* |
385 (* |
216 Second proof of opposite direction, directly by wellfounded induction |
386 Second proof of opposite direction, directly by wellfounded induction |
217 on the initial segment of M that avoids A. |
387 on the initial segment of M that avoids A. |
218 |
388 |
219 Avoid s A = the set of successors of s that can be reached by a finite A-avoiding path |
389 Avoid s A = the set of successors of s that can be reached by a finite A-avoiding path |