10133
|
1 |
(*<*)theory CTL = Base:(*>*)
|
9958
|
2 |
|
10133
|
3 |
subsection{*Computation tree logic---CTL*}
|
9958
|
4 |
|
|
5 |
datatype ctl_form = Atom atom
|
|
6 |
| NOT ctl_form
|
|
7 |
| And ctl_form ctl_form
|
|
8 |
| AX ctl_form
|
|
9 |
| EF ctl_form
|
|
10 |
| AF ctl_form;
|
|
11 |
|
|
12 |
consts valid :: "state \<Rightarrow> ctl_form \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80)
|
|
13 |
|
|
14 |
constdefs Paths :: "state \<Rightarrow> (nat \<Rightarrow> state)set"
|
|
15 |
"Paths s \<equiv> {p. s = p 0 \<and> (\<forall>i. (p i, p(i+1)) \<in> M)}";
|
|
16 |
|
|
17 |
primrec
|
10133
|
18 |
"s \<Turnstile> Atom a = (a \<in> L s)"
|
9958
|
19 |
"s \<Turnstile> NOT f = (~(s \<Turnstile> f))"
|
|
20 |
"s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)"
|
|
21 |
"s \<Turnstile> AX f = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)"
|
|
22 |
"s \<Turnstile> EF f = (\<exists>t. (s,t) \<in> M^* \<and> t \<Turnstile> f)"
|
|
23 |
"s \<Turnstile> AF f = (\<forall>p \<in> Paths s. \<exists>i. p i \<Turnstile> f)";
|
|
24 |
|
|
25 |
constdefs af :: "state set \<Rightarrow> state set \<Rightarrow> state set"
|
|
26 |
"af A T \<equiv> A \<union> {s. \<forall>t. (s, t) \<in> M \<longrightarrow> t \<in> T}";
|
|
27 |
|
|
28 |
lemma mono_af: "mono(af A)";
|
|
29 |
by(force simp add: af_def intro:monoI);
|
|
30 |
|
|
31 |
consts mc :: "ctl_form \<Rightarrow> state set";
|
|
32 |
primrec
|
10133
|
33 |
"mc(Atom a) = {s. a \<in> L s}"
|
9958
|
34 |
"mc(NOT f) = -mc f"
|
|
35 |
"mc(And f g) = mc f \<inter> mc g"
|
|
36 |
"mc(AX f) = {s. \<forall>t. (s,t) \<in> M \<longrightarrow> t \<in> mc f}"
|
|
37 |
"mc(EF f) = lfp(\<lambda>T. mc f \<union> {s. \<exists>t. (s,t)\<in>M \<and> t\<in>T})"
|
|
38 |
"mc(AF f) = lfp(af(mc f))";
|
|
39 |
|
|
40 |
lemma mono_ef: "mono(\<lambda>T. A \<union> {s. \<exists>t. (s,t)\<in>M \<and> t\<in>T})";
|
|
41 |
apply(rule monoI);
|
|
42 |
by(blast);
|
|
43 |
|
|
44 |
lemma lfp_conv_EF:
|
|
45 |
"lfp(\<lambda>T. A \<union> {s. \<exists>t. (s,t)\<in>M \<and> t\<in>T}) = {s. \<exists>t. (s,t) \<in> M^* \<and> t \<in> A}";
|
|
46 |
apply(rule equalityI);
|
|
47 |
apply(rule subsetI);
|
|
48 |
apply(simp);
|
|
49 |
apply(erule Lfp.induct);
|
|
50 |
apply(rule mono_ef);
|
|
51 |
apply(simp);
|
|
52 |
apply(blast intro: r_into_rtrancl rtrancl_trans);
|
|
53 |
apply(rule subsetI);
|
|
54 |
apply(simp);
|
|
55 |
apply(erule exE);
|
|
56 |
apply(erule conjE);
|
|
57 |
apply(erule_tac P = "t\<in>A" in rev_mp);
|
|
58 |
apply(erule converse_rtrancl_induct);
|
|
59 |
apply(rule ssubst [OF lfp_Tarski[OF mono_ef]]);
|
|
60 |
apply(blast);
|
|
61 |
apply(rule ssubst [OF lfp_Tarski[OF mono_ef]]);
|
|
62 |
by(blast);
|
|
63 |
|
|
64 |
theorem lfp_subset_AF:
|
|
65 |
"lfp(af A) \<subseteq> {s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A}";
|
|
66 |
apply(rule subsetI);
|
|
67 |
apply(erule Lfp.induct[OF _ mono_af]);
|
|
68 |
apply(simp add: af_def Paths_def);
|
|
69 |
apply(erule disjE);
|
|
70 |
apply(blast);
|
|
71 |
apply(clarify);
|
|
72 |
apply(erule_tac x = "p 1" in allE);
|
|
73 |
apply(clarsimp);
|
|
74 |
apply(erule_tac x = "\<lambda>i. p(i+1)" in allE);
|
|
75 |
apply(simp);
|
|
76 |
by(blast);
|
|
77 |
|
|
78 |
text{*
|
|
79 |
The opposite direction is proved by contradiction: if some state
|
|
80 |
{term s} is not in @{term"lfp(af A)"}, then we can construct an
|
|
81 |
infinite @{term A}-avoiding path starting from @{term s}. The reason is
|
|
82 |
that by unfolding @{term"lfp"} we find that if @{term s} is not in
|
|
83 |
@{term"lfp(af A)"}, then @{term s} is not in @{term A} and there is a
|
|
84 |
direct successor of @{term s} that is again not in @{term"lfp(af
|
|
85 |
A)"}. Iterating this argument yields the promised infinite
|
|
86 |
@{term A}-avoiding path. Let us formalize this sketch.
|
|
87 |
|
|
88 |
The one-step argument in the above sketch
|
|
89 |
*};
|
|
90 |
|
|
91 |
lemma not_in_lfp_afD:
|
|
92 |
"s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t)\<in>M \<and> t \<notin> lfp(af A))";
|
|
93 |
apply(erule swap);
|
|
94 |
apply(rule ssubst[OF lfp_Tarski[OF mono_af]]);
|
|
95 |
by(simp add:af_def);
|
|
96 |
|
|
97 |
text{*\noindent
|
|
98 |
is proved by a variant of contraposition (@{thm[source]swap}:
|
|
99 |
@{thm swap[no_vars]}), i.e.\ assuming the negation of the conclusion
|
|
100 |
and proving @{term"s : lfp(af A)"}. Unfolding @{term lfp} once and
|
|
101 |
simplifying with the definition of @{term af} finishes the proof.
|
|
102 |
|
|
103 |
Now we iterate this process. The following construction of the desired
|
|
104 |
path is parameterized by a predicate @{term P} that should hold along the path:
|
|
105 |
*};
|
|
106 |
|
|
107 |
consts path :: "state \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> (nat \<Rightarrow> state)";
|
|
108 |
primrec
|
|
109 |
"path s P 0 = s"
|
|
110 |
"path s P (Suc n) = (SOME t. (path s P n,t) \<in> M \<and> P t)";
|
|
111 |
|
|
112 |
text{*\noindent
|
|
113 |
Element @{term"n+1"} on this path is some arbitrary successor
|
|
114 |
@{term"t"} of element @{term"n"} such that @{term"P t"} holds. Of
|
|
115 |
course, such a @{term"t"} may in general not exist, but that is of no
|
|
116 |
concern to us since we will only use @{term path} in such cases where a
|
|
117 |
suitable @{term"t"} does exist.
|
|
118 |
|
|
119 |
Now we prove that if each state @{term"s"} that satisfies @{term"P"}
|
|
120 |
has a successor that again satisfies @{term"P"}, then there exists an infinite @{term"P"}-path.
|
|
121 |
*};
|
|
122 |
|
|
123 |
lemma seq_lemma:
|
|
124 |
"\<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)";
|
|
125 |
|
|
126 |
txt{*\noindent
|
|
127 |
First we rephrase the conclusion slightly because we need to prove both the path property
|
|
128 |
and the fact that @{term"P"} holds simultaneously:
|
|
129 |
*};
|
|
130 |
|
|
131 |
apply(subgoal_tac "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(i+1)) \<in> M \<and> P(p i))");
|
|
132 |
|
|
133 |
txt{*\noindent
|
|
134 |
From this proposition the original goal follows easily
|
|
135 |
*};
|
|
136 |
|
|
137 |
apply(simp add:Paths_def, blast);
|
|
138 |
apply(rule_tac x = "path s P" in exI);
|
|
139 |
apply(simp);
|
|
140 |
apply(intro strip);
|
|
141 |
apply(induct_tac i);
|
|
142 |
apply(simp);
|
10000
|
143 |
apply(fast intro:someI2_ex);
|
9958
|
144 |
apply(simp);
|
10000
|
145 |
apply(rule someI2_ex);
|
9958
|
146 |
apply(blast);
|
10000
|
147 |
apply(rule someI2_ex);
|
9958
|
148 |
apply(blast);
|
|
149 |
by(blast);
|
|
150 |
|
|
151 |
lemma seq_lemma:
|
|
152 |
"\<lbrakk> P s; \<forall> s. P s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> P t) \<rbrakk> \<Longrightarrow>
|
|
153 |
\<exists> p\<in>Paths s. \<forall> i. P(p i)";
|
|
154 |
apply(subgoal_tac
|
|
155 |
"\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> P(p i))");
|
|
156 |
apply(simp add:Paths_def);
|
|
157 |
apply(blast);
|
|
158 |
apply(rule_tac x = "nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> P u)" in exI);
|
|
159 |
apply(simp);
|
|
160 |
apply(intro strip);
|
|
161 |
apply(induct_tac i);
|
|
162 |
apply(simp);
|
10000
|
163 |
apply(fast intro:someI2_ex);
|
9958
|
164 |
apply(simp);
|
10000
|
165 |
apply(rule someI2_ex);
|
9958
|
166 |
apply(blast);
|
10000
|
167 |
apply(rule someI2_ex);
|
9958
|
168 |
apply(blast);
|
|
169 |
by(blast);
|
|
170 |
|
|
171 |
theorem AF_subset_lfp:
|
|
172 |
"{s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
|
|
173 |
apply(rule subsetI);
|
|
174 |
apply(erule contrapos2);
|
|
175 |
apply simp;
|
|
176 |
apply(drule seq_lemma);
|
|
177 |
by(auto dest:not_in_lfp_afD);
|
|
178 |
|
|
179 |
|
|
180 |
(*
|
|
181 |
Second proof of opposite direction, directly by wellfounded induction
|
|
182 |
on the initial segment of M that avoids A.
|
|
183 |
|
|
184 |
Avoid s A = the set of successors of s that can be reached by a finite A-avoiding path
|
|
185 |
*)
|
|
186 |
|
|
187 |
consts Avoid :: "state \<Rightarrow> state set \<Rightarrow> state set";
|
|
188 |
inductive "Avoid s A"
|
|
189 |
intros "s \<in> Avoid s A"
|
|
190 |
"\<lbrakk> t \<in> Avoid s A; t \<notin> A; (t,u) \<in> M \<rbrakk> \<Longrightarrow> u \<in> Avoid s A";
|
|
191 |
|
|
192 |
(* For any infinite A-avoiding path (f) in Avoid s A,
|
|
193 |
there is some infinite A-avoiding path (p) in Avoid s A that starts with s.
|
|
194 |
*)
|
|
195 |
lemma ex_infinite_path[rule_format]:
|
|
196 |
"t \<in> Avoid s A \<Longrightarrow>
|
|
197 |
\<forall>f. t = f 0 \<longrightarrow> (\<forall>i. (f i, f (Suc i)) \<in> M \<and> f i \<in> Avoid s A \<and> f i \<notin> A)
|
|
198 |
\<longrightarrow> (\<exists> p\<in>Paths s. \<forall>i. p i \<notin> A)";
|
|
199 |
apply(simp add:Paths_def);
|
|
200 |
apply(erule Avoid.induct);
|
|
201 |
apply(blast);
|
|
202 |
apply(rule allI);
|
|
203 |
apply(erule_tac x = "\<lambda>i. case i of 0 \<Rightarrow> t | Suc i \<Rightarrow> f i" in allE);
|
|
204 |
by(force split:nat.split);
|
|
205 |
|
|
206 |
lemma Avoid_in_lfp[rule_format(no_asm)]:
|
|
207 |
"\<forall>p\<in>Paths s. \<exists>i. p i \<in> A \<Longrightarrow> t \<in> Avoid s A \<longrightarrow> t \<in> lfp(af A)";
|
|
208 |
apply(subgoal_tac "wf{(y,x). (x,y)\<in>M \<and> x \<in> Avoid s A \<and> y \<in> Avoid s A \<and> x \<notin> A}");
|
|
209 |
apply(erule_tac a = t in wf_induct);
|
|
210 |
apply(clarsimp);
|
|
211 |
apply(rule ssubst [OF lfp_Tarski[OF mono_af]]);
|
|
212 |
apply(unfold af_def);
|
|
213 |
apply(blast intro:Avoid.intros);
|
|
214 |
apply(erule contrapos2);
|
|
215 |
apply(simp add:wf_iff_no_infinite_down_chain);
|
|
216 |
apply(erule exE);
|
|
217 |
apply(rule ex_infinite_path);
|
|
218 |
by(auto);
|
|
219 |
|
|
220 |
theorem AF_subset_lfp:
|
|
221 |
"{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
|
|
222 |
apply(rule subsetI);
|
|
223 |
apply(simp);
|
|
224 |
apply(erule Avoid_in_lfp);
|
|
225 |
by(rule Avoid.intros);
|
|
226 |
|
|
227 |
|
|
228 |
theorem "mc f = {s. s \<Turnstile> f}";
|
|
229 |
apply(induct_tac f);
|
|
230 |
by(auto simp add: lfp_conv_EF equalityI[OF lfp_subset_AF AF_subset_lfp]);
|
|
231 |
|
10133
|
232 |
(*<*)end(*>*)
|