author | wenzelm |
Sun, 15 Nov 2015 12:39:51 +0100 | |
changeset 61681 | ca53150406c9 |
parent 61239 | dd949db0ade8 |
child 62093 | bd73a2279fcd |
permissions | -rw-r--r-- |
58627 | 1 |
(* Title: HOL/Library/Linear_Temporal_Logic_on_Streams.thy |
2 |
Author: Andrei Popescu, TU Muenchen |
|
3 |
Author: Dmitriy Traytel, TU Muenchen |
|
4 |
*) |
|
5 |
||
60500 | 6 |
section \<open>Linear Temporal Logic on Streams\<close> |
58627 | 7 |
|
8 |
theory Linear_Temporal_Logic_on_Streams |
|
59000 | 9 |
imports Stream Sublist Extended_Nat Infinite_Set |
58627 | 10 |
begin |
11 |
||
60500 | 12 |
section\<open>Preliminaries\<close> |
58627 | 13 |
|
14 |
lemma shift_prefix: |
|
15 |
assumes "xl @- xs = yl @- ys" and "length xl \<le> length yl" |
|
16 |
shows "prefixeq xl yl" |
|
17 |
using assms proof(induct xl arbitrary: yl xs ys) |
|
18 |
case (Cons x xl yl xs ys) |
|
19 |
thus ?case by (cases yl) auto |
|
20 |
qed auto |
|
21 |
||
22 |
lemma shift_prefix_cases: |
|
23 |
assumes "xl @- xs = yl @- ys" |
|
24 |
shows "prefixeq xl yl \<or> prefixeq yl xl" |
|
61239 | 25 |
using shift_prefix[OF assms] |
26 |
by (cases "length xl \<le> length yl") (metis, metis assms nat_le_linear shift_prefix) |
|
58627 | 27 |
|
28 |
||
60500 | 29 |
section\<open>Linear temporal logic\<close> |
58627 | 30 |
|
31 |
(* Propositional connectives: *) |
|
32 |
abbreviation (input) IMPL (infix "impl" 60) |
|
33 |
where "\<phi> impl \<psi> \<equiv> \<lambda> xs. \<phi> xs \<longrightarrow> \<psi> xs" |
|
34 |
||
35 |
abbreviation (input) OR (infix "or" 60) |
|
36 |
where "\<phi> or \<psi> \<equiv> \<lambda> xs. \<phi> xs \<or> \<psi> xs" |
|
37 |
||
38 |
abbreviation (input) AND (infix "aand" 60) |
|
39 |
where "\<phi> aand \<psi> \<equiv> \<lambda> xs. \<phi> xs \<and> \<psi> xs" |
|
40 |
||
41 |
abbreviation (input) "not \<phi> \<equiv> \<lambda> xs. \<not> \<phi> xs" |
|
42 |
||
43 |
abbreviation (input) "true \<equiv> \<lambda> xs. True" |
|
44 |
||
45 |
abbreviation (input) "false \<equiv> \<lambda> xs. False" |
|
46 |
||
47 |
lemma impl_not_or: "\<phi> impl \<psi> = (not \<phi>) or \<psi>" |
|
48 |
by blast |
|
49 |
||
50 |
lemma not_or: "not (\<phi> or \<psi>) = (not \<phi>) aand (not \<psi>)" |
|
51 |
by blast |
|
52 |
||
53 |
lemma not_aand: "not (\<phi> aand \<psi>) = (not \<phi>) or (not \<psi>)" |
|
54 |
by blast |
|
55 |
||
56 |
lemma non_not[simp]: "not (not \<phi>) = \<phi>" by simp |
|
57 |
||
58 |
(* Temporal (LTL) connectives: *) |
|
59 |
fun holds where "holds P xs \<longleftrightarrow> P (shd xs)" |
|
60 |
fun nxt where "nxt \<phi> xs = \<phi> (stl xs)" |
|
61 |
||
59000 | 62 |
definition "HLD s = holds (\<lambda>x. x \<in> s)" |
63 |
||
64 |
abbreviation HLD_nxt (infixr "\<cdot>" 65) where |
|
65 |
"s \<cdot> P \<equiv> HLD s aand nxt P" |
|
66 |
||
61681
ca53150406c9
option "inductive_defs" controls exposure of def and mono facts;
wenzelm
parents:
61239
diff
changeset
|
67 |
context |
ca53150406c9
option "inductive_defs" controls exposure of def and mono facts;
wenzelm
parents:
61239
diff
changeset
|
68 |
notes [[inductive_defs]] |
ca53150406c9
option "inductive_defs" controls exposure of def and mono facts;
wenzelm
parents:
61239
diff
changeset
|
69 |
begin |
ca53150406c9
option "inductive_defs" controls exposure of def and mono facts;
wenzelm
parents:
61239
diff
changeset
|
70 |
|
58627 | 71 |
inductive ev for \<phi> where |
72 |
base: "\<phi> xs \<Longrightarrow> ev \<phi> xs" |
|
73 |
| |
|
74 |
step: "ev \<phi> (stl xs) \<Longrightarrow> ev \<phi> xs" |
|
75 |
||
76 |
coinductive alw for \<phi> where |
|
77 |
alw: "\<lbrakk>\<phi> xs; alw \<phi> (stl xs)\<rbrakk> \<Longrightarrow> alw \<phi> xs" |
|
78 |
||
79 |
(* weak until: *) |
|
80 |
coinductive UNTIL (infix "until" 60) for \<phi> \<psi> where |
|
81 |
base: "\<psi> xs \<Longrightarrow> (\<phi> until \<psi>) xs" |
|
82 |
| |
|
83 |
step: "\<lbrakk>\<phi> xs; (\<phi> until \<psi>) (stl xs)\<rbrakk> \<Longrightarrow> (\<phi> until \<psi>) xs" |
|
84 |
||
61681
ca53150406c9
option "inductive_defs" controls exposure of def and mono facts;
wenzelm
parents:
61239
diff
changeset
|
85 |
end |
ca53150406c9
option "inductive_defs" controls exposure of def and mono facts;
wenzelm
parents:
61239
diff
changeset
|
86 |
|
58627 | 87 |
lemma holds_mono: |
88 |
assumes holds: "holds P xs" and 0: "\<And> x. P x \<Longrightarrow> Q x" |
|
89 |
shows "holds Q xs" |
|
90 |
using assms by auto |
|
91 |
||
92 |
lemma holds_aand: |
|
93 |
"(holds P aand holds Q) steps \<longleftrightarrow> holds (\<lambda> step. P step \<and> Q step) steps" by auto |
|
94 |
||
59000 | 95 |
lemma HLD_iff: "HLD s \<omega> \<longleftrightarrow> shd \<omega> \<in> s" |
96 |
by (simp add: HLD_def) |
|
97 |
||
98 |
lemma HLD_Stream[simp]: "HLD X (x ## \<omega>) \<longleftrightarrow> x \<in> X" |
|
99 |
by (simp add: HLD_iff) |
|
100 |
||
58627 | 101 |
lemma nxt_mono: |
102 |
assumes nxt: "nxt \<phi> xs" and 0: "\<And> xs. \<phi> xs \<Longrightarrow> \<psi> xs" |
|
103 |
shows "nxt \<psi> xs" |
|
104 |
using assms by auto |
|
105 |
||
59000 | 106 |
declare ev.intros[intro] |
107 |
declare alw.cases[elim] |
|
108 |
||
109 |
lemma ev_induct_strong[consumes 1, case_names base step]: |
|
110 |
"ev \<phi> x \<Longrightarrow> (\<And>xs. \<phi> xs \<Longrightarrow> P xs) \<Longrightarrow> (\<And>xs. ev \<phi> (stl xs) \<Longrightarrow> \<not> \<phi> xs \<Longrightarrow> P (stl xs) \<Longrightarrow> P xs) \<Longrightarrow> P x" |
|
111 |
by (induct rule: ev.induct) auto |
|
112 |
||
113 |
lemma alw_coinduct[consumes 1, case_names alw stl]: |
|
114 |
"X x \<Longrightarrow> (\<And>x. X x \<Longrightarrow> \<phi> x) \<Longrightarrow> (\<And>x. X x \<Longrightarrow> \<not> alw \<phi> (stl x) \<Longrightarrow> X (stl x)) \<Longrightarrow> alw \<phi> x" |
|
115 |
using alw.coinduct[of X x \<phi>] by auto |
|
116 |
||
58627 | 117 |
lemma ev_mono: |
118 |
assumes ev: "ev \<phi> xs" and 0: "\<And> xs. \<phi> xs \<Longrightarrow> \<psi> xs" |
|
119 |
shows "ev \<psi> xs" |
|
61239 | 120 |
using ev by induct (auto simp: 0) |
58627 | 121 |
|
122 |
lemma alw_mono: |
|
123 |
assumes alw: "alw \<phi> xs" and 0: "\<And> xs. \<phi> xs \<Longrightarrow> \<psi> xs" |
|
124 |
shows "alw \<psi> xs" |
|
61239 | 125 |
using alw by coinduct (auto simp: 0) |
58627 | 126 |
|
127 |
lemma until_monoL: |
|
128 |
assumes until: "(\<phi>1 until \<psi>) xs" and 0: "\<And> xs. \<phi>1 xs \<Longrightarrow> \<phi>2 xs" |
|
129 |
shows "(\<phi>2 until \<psi>) xs" |
|
130 |
using until by coinduct (auto elim: UNTIL.cases simp: 0) |
|
131 |
||
132 |
lemma until_monoR: |
|
133 |
assumes until: "(\<phi> until \<psi>1) xs" and 0: "\<And> xs. \<psi>1 xs \<Longrightarrow> \<psi>2 xs" |
|
134 |
shows "(\<phi> until \<psi>2) xs" |
|
135 |
using until by coinduct (auto elim: UNTIL.cases simp: 0) |
|
136 |
||
137 |
lemma until_mono: |
|
138 |
assumes until: "(\<phi>1 until \<psi>1) xs" and |
|
139 |
0: "\<And> xs. \<phi>1 xs \<Longrightarrow> \<phi>2 xs" "\<And> xs. \<psi>1 xs \<Longrightarrow> \<psi>2 xs" |
|
140 |
shows "(\<phi>2 until \<psi>2) xs" |
|
141 |
using until by coinduct (auto elim: UNTIL.cases simp: 0) |
|
142 |
||
143 |
lemma until_false: "\<phi> until false = alw \<phi>" |
|
144 |
proof- |
|
145 |
{fix xs assume "(\<phi> until false) xs" hence "alw \<phi> xs" |
|
61239 | 146 |
by coinduct (auto elim: UNTIL.cases) |
58627 | 147 |
} |
148 |
moreover |
|
149 |
{fix xs assume "alw \<phi> xs" hence "(\<phi> until false) xs" |
|
61239 | 150 |
by coinduct auto |
58627 | 151 |
} |
152 |
ultimately show ?thesis by blast |
|
153 |
qed |
|
154 |
||
155 |
lemma ev_nxt: "ev \<phi> = (\<phi> or nxt (ev \<phi>))" |
|
61239 | 156 |
by (rule ext) (metis ev.simps nxt.simps) |
58627 | 157 |
|
158 |
lemma alw_nxt: "alw \<phi> = (\<phi> aand nxt (alw \<phi>))" |
|
61239 | 159 |
by (rule ext) (metis alw.simps nxt.simps) |
58627 | 160 |
|
161 |
lemma ev_ev[simp]: "ev (ev \<phi>) = ev \<phi>" |
|
162 |
proof- |
|
163 |
{fix xs |
|
164 |
assume "ev (ev \<phi>) xs" hence "ev \<phi> xs" |
|
61239 | 165 |
by induct auto |
58627 | 166 |
} |
61239 | 167 |
thus ?thesis by auto |
58627 | 168 |
qed |
169 |
||
170 |
lemma alw_alw[simp]: "alw (alw \<phi>) = alw \<phi>" |
|
171 |
proof- |
|
172 |
{fix xs |
|
173 |
assume "alw \<phi> xs" hence "alw (alw \<phi>) xs" |
|
61239 | 174 |
by coinduct auto |
58627 | 175 |
} |
61239 | 176 |
thus ?thesis by auto |
58627 | 177 |
qed |
178 |
||
179 |
lemma ev_shift: |
|
180 |
assumes "ev \<phi> xs" |
|
181 |
shows "ev \<phi> (xl @- xs)" |
|
61239 | 182 |
using assms by (induct xl) auto |
58627 | 183 |
|
184 |
lemma ev_imp_shift: |
|
185 |
assumes "ev \<phi> xs" shows "\<exists> xl xs2. xs = xl @- xs2 \<and> \<phi> xs2" |
|
186 |
using assms by induct (metis shift.simps(1), metis shift.simps(2) stream.collapse)+ |
|
187 |
||
188 |
lemma alw_ev_shift: "alw \<phi> xs1 \<Longrightarrow> ev (alw \<phi>) (xl @- xs1)" |
|
61239 | 189 |
by (auto intro: ev_shift) |
58627 | 190 |
|
191 |
lemma alw_shift: |
|
192 |
assumes "alw \<phi> (xl @- xs)" |
|
193 |
shows "alw \<phi> xs" |
|
61239 | 194 |
using assms by (induct xl) auto |
58627 | 195 |
|
196 |
lemma ev_ex_nxt: |
|
197 |
assumes "ev \<phi> xs" |
|
198 |
shows "\<exists> n. (nxt ^^ n) \<phi> xs" |
|
199 |
using assms proof induct |
|
200 |
case (base xs) thus ?case by (intro exI[of _ 0]) auto |
|
201 |
next |
|
202 |
case (step xs) |
|
203 |
then obtain n where "(nxt ^^ n) \<phi> (stl xs)" by blast |
|
204 |
thus ?case by (intro exI[of _ "Suc n"]) (metis funpow.simps(2) nxt.simps o_def) |
|
205 |
qed |
|
206 |
||
207 |
lemma alw_sdrop: |
|
208 |
assumes "alw \<phi> xs" shows "alw \<phi> (sdrop n xs)" |
|
209 |
by (metis alw_shift assms stake_sdrop) |
|
210 |
||
211 |
lemma nxt_sdrop: "(nxt ^^ n) \<phi> xs \<longleftrightarrow> \<phi> (sdrop n xs)" |
|
212 |
by (induct n arbitrary: xs) auto |
|
213 |
||
214 |
definition "wait \<phi> xs \<equiv> LEAST n. (nxt ^^ n) \<phi> xs" |
|
215 |
||
216 |
lemma nxt_wait: |
|
217 |
assumes "ev \<phi> xs" shows "(nxt ^^ (wait \<phi> xs)) \<phi> xs" |
|
218 |
unfolding wait_def using ev_ex_nxt[OF assms] by(rule LeastI_ex) |
|
219 |
||
220 |
lemma nxt_wait_least: |
|
221 |
assumes ev: "ev \<phi> xs" and nxt: "(nxt ^^ n) \<phi> xs" shows "wait \<phi> xs \<le> n" |
|
222 |
unfolding wait_def using ev_ex_nxt[OF ev] by (metis Least_le nxt) |
|
223 |
||
224 |
lemma sdrop_wait: |
|
225 |
assumes "ev \<phi> xs" shows "\<phi> (sdrop (wait \<phi> xs) xs)" |
|
226 |
using nxt_wait[OF assms] unfolding nxt_sdrop . |
|
227 |
||
228 |
lemma sdrop_wait_least: |
|
229 |
assumes ev: "ev \<phi> xs" and nxt: "\<phi> (sdrop n xs)" shows "wait \<phi> xs \<le> n" |
|
230 |
using assms nxt_wait_least unfolding nxt_sdrop by auto |
|
231 |
||
232 |
lemma nxt_ev: "(nxt ^^ n) \<phi> xs \<Longrightarrow> ev \<phi> xs" |
|
61239 | 233 |
by (induct n arbitrary: xs) auto |
58627 | 234 |
|
235 |
lemma not_ev: "not (ev \<phi>) = alw (not \<phi>)" |
|
236 |
proof(rule ext, safe) |
|
237 |
fix xs assume "not (ev \<phi>) xs" thus "alw (not \<phi>) xs" |
|
61239 | 238 |
by (coinduct) auto |
58627 | 239 |
next |
240 |
fix xs assume "ev \<phi> xs" and "alw (not \<phi>) xs" thus False |
|
61239 | 241 |
by (induct) auto |
58627 | 242 |
qed |
243 |
||
244 |
lemma not_alw: "not (alw \<phi>) = ev (not \<phi>)" |
|
245 |
proof- |
|
246 |
have "not (alw \<phi>) = not (alw (not (not \<phi>)))" by simp |
|
247 |
also have "... = ev (not \<phi>)" unfolding not_ev[symmetric] by simp |
|
248 |
finally show ?thesis . |
|
249 |
qed |
|
250 |
||
251 |
lemma not_ev_not[simp]: "not (ev (not \<phi>)) = alw \<phi>" |
|
252 |
unfolding not_ev by simp |
|
253 |
||
254 |
lemma not_alw_not[simp]: "not (alw (not \<phi>)) = ev \<phi>" |
|
255 |
unfolding not_alw by simp |
|
256 |
||
257 |
lemma alw_ev_sdrop: |
|
258 |
assumes "alw (ev \<phi>) (sdrop m xs)" |
|
259 |
shows "alw (ev \<phi>) xs" |
|
260 |
using assms |
|
261 |
by coinduct (metis alw_nxt ev_shift funpow_swap1 nxt.simps nxt_sdrop stake_sdrop) |
|
262 |
||
263 |
lemma ev_alw_imp_alw_ev: |
|
264 |
assumes "ev (alw \<phi>) xs" shows "alw (ev \<phi>) xs" |
|
61239 | 265 |
using assms by induct (metis (full_types) alw_mono ev.base, metis alw alw_nxt ev.step) |
58627 | 266 |
|
267 |
lemma alw_aand: "alw (\<phi> aand \<psi>) = alw \<phi> aand alw \<psi>" |
|
268 |
proof- |
|
269 |
{fix xs assume "alw (\<phi> aand \<psi>) xs" hence "(alw \<phi> aand alw \<psi>) xs" |
|
270 |
by (auto elim: alw_mono) |
|
271 |
} |
|
272 |
moreover |
|
273 |
{fix xs assume "(alw \<phi> aand alw \<psi>) xs" hence "alw (\<phi> aand \<psi>) xs" |
|
61239 | 274 |
by coinduct auto |
58627 | 275 |
} |
276 |
ultimately show ?thesis by blast |
|
277 |
qed |
|
278 |
||
279 |
lemma ev_or: "ev (\<phi> or \<psi>) = ev \<phi> or ev \<psi>" |
|
280 |
proof- |
|
281 |
{fix xs assume "(ev \<phi> or ev \<psi>) xs" hence "ev (\<phi> or \<psi>) xs" |
|
282 |
by (auto elim: ev_mono) |
|
283 |
} |
|
284 |
moreover |
|
285 |
{fix xs assume "ev (\<phi> or \<psi>) xs" hence "(ev \<phi> or ev \<psi>) xs" |
|
61239 | 286 |
by induct auto |
58627 | 287 |
} |
288 |
ultimately show ?thesis by blast |
|
289 |
qed |
|
290 |
||
291 |
lemma ev_alw_aand: |
|
292 |
assumes \<phi>: "ev (alw \<phi>) xs" and \<psi>: "ev (alw \<psi>) xs" |
|
293 |
shows "ev (alw (\<phi> aand \<psi>)) xs" |
|
294 |
proof- |
|
295 |
obtain xl xs1 where xs1: "xs = xl @- xs1" and \<phi>\<phi>: "alw \<phi> xs1" |
|
296 |
using \<phi> by (metis ev_imp_shift) |
|
297 |
moreover obtain yl ys1 where xs2: "xs = yl @- ys1" and \<psi>\<psi>: "alw \<psi> ys1" |
|
298 |
using \<psi> by (metis ev_imp_shift) |
|
299 |
ultimately have 0: "xl @- xs1 = yl @- ys1" by auto |
|
300 |
hence "prefixeq xl yl \<or> prefixeq yl xl" using shift_prefix_cases by auto |
|
301 |
thus ?thesis proof |
|
302 |
assume "prefixeq xl yl" |
|
303 |
then obtain yl1 where yl: "yl = xl @ yl1" by (elim prefixeqE) |
|
304 |
have xs1': "xs1 = yl1 @- ys1" using 0 unfolding yl by simp |
|
305 |
have "alw \<phi> ys1" using \<phi>\<phi> unfolding xs1' by (metis alw_shift) |
|
306 |
hence "alw (\<phi> aand \<psi>) ys1" using \<psi>\<psi> unfolding alw_aand by auto |
|
307 |
thus ?thesis unfolding xs2 by (auto intro: alw_ev_shift) |
|
308 |
next |
|
309 |
assume "prefixeq yl xl" |
|
310 |
then obtain xl1 where xl: "xl = yl @ xl1" by (elim prefixeqE) |
|
311 |
have ys1': "ys1 = xl1 @- xs1" using 0 unfolding xl by simp |
|
312 |
have "alw \<psi> xs1" using \<psi>\<psi> unfolding ys1' by (metis alw_shift) |
|
313 |
hence "alw (\<phi> aand \<psi>) xs1" using \<phi>\<phi> unfolding alw_aand by auto |
|
314 |
thus ?thesis unfolding xs1 by (auto intro: alw_ev_shift) |
|
315 |
qed |
|
316 |
qed |
|
317 |
||
318 |
lemma ev_alw_alw_impl: |
|
319 |
assumes "ev (alw \<phi>) xs" and "alw (alw \<phi> impl ev \<psi>) xs" |
|
320 |
shows "ev \<psi> xs" |
|
61239 | 321 |
using assms by induct auto |
58627 | 322 |
|
323 |
lemma ev_alw_stl[simp]: "ev (alw \<phi>) (stl x) \<longleftrightarrow> ev (alw \<phi>) x" |
|
324 |
by (metis (full_types) alw_nxt ev_nxt nxt.simps) |
|
325 |
||
326 |
lemma alw_alw_impl_ev: |
|
327 |
"alw (alw \<phi> impl ev \<psi>) = (ev (alw \<phi>) impl alw (ev \<psi>))" (is "?A = ?B") |
|
328 |
proof- |
|
329 |
{fix xs assume "?A xs \<and> ev (alw \<phi>) xs" hence "alw (ev \<psi>) xs" |
|
61239 | 330 |
by coinduct (auto elim: ev_alw_alw_impl) |
58627 | 331 |
} |
332 |
moreover |
|
333 |
{fix xs assume "?B xs" hence "?A xs" |
|
61239 | 334 |
by coinduct auto |
58627 | 335 |
} |
336 |
ultimately show ?thesis by blast |
|
337 |
qed |
|
338 |
||
339 |
lemma ev_alw_impl: |
|
340 |
assumes "ev \<phi> xs" and "alw (\<phi> impl \<psi>) xs" shows "ev \<psi> xs" |
|
61239 | 341 |
using assms by induct auto |
58627 | 342 |
|
343 |
lemma ev_alw_impl_ev: |
|
344 |
assumes "ev \<phi> xs" and "alw (\<phi> impl ev \<psi>) xs" shows "ev \<psi> xs" |
|
345 |
using ev_alw_impl[OF assms] by simp |
|
346 |
||
347 |
lemma alw_mp: |
|
348 |
assumes "alw \<phi> xs" and "alw (\<phi> impl \<psi>) xs" |
|
349 |
shows "alw \<psi> xs" |
|
350 |
proof- |
|
351 |
{assume "alw \<phi> xs \<and> alw (\<phi> impl \<psi>) xs" hence ?thesis |
|
61239 | 352 |
by coinduct auto |
58627 | 353 |
} |
354 |
thus ?thesis using assms by auto |
|
355 |
qed |
|
356 |
||
357 |
lemma all_imp_alw: |
|
358 |
assumes "\<And> xs. \<phi> xs" shows "alw \<phi> xs" |
|
359 |
proof- |
|
360 |
{assume "\<forall> xs. \<phi> xs" |
|
361 |
hence ?thesis by coinduct auto |
|
362 |
} |
|
363 |
thus ?thesis using assms by auto |
|
364 |
qed |
|
365 |
||
366 |
lemma alw_impl_ev_alw: |
|
367 |
assumes "alw (\<phi> impl ev \<psi>) xs" |
|
368 |
shows "alw (ev \<phi> impl ev \<psi>) xs" |
|
61239 | 369 |
using assms by coinduct (auto dest: ev_alw_impl) |
58627 | 370 |
|
371 |
lemma ev_holds_sset: |
|
372 |
"ev (holds P) xs \<longleftrightarrow> (\<exists> x \<in> sset xs. P x)" (is "?L \<longleftrightarrow> ?R") |
|
373 |
proof safe |
|
374 |
assume ?L thus ?R by induct (metis holds.simps stream.set_sel(1), metis stl_sset) |
|
375 |
next |
|
376 |
fix x assume "x \<in> sset xs" "P x" |
|
377 |
thus ?L by (induct rule: sset_induct) (simp_all add: ev.base ev.step) |
|
378 |
qed |
|
379 |
||
380 |
(* LTL as a program logic: *) |
|
381 |
lemma alw_invar: |
|
382 |
assumes "\<phi> xs" and "alw (\<phi> impl nxt \<phi>) xs" |
|
383 |
shows "alw \<phi> xs" |
|
384 |
proof- |
|
385 |
{assume "\<phi> xs \<and> alw (\<phi> impl nxt \<phi>) xs" hence ?thesis |
|
61239 | 386 |
by coinduct auto |
58627 | 387 |
} |
388 |
thus ?thesis using assms by auto |
|
389 |
qed |
|
390 |
||
391 |
lemma variance: |
|
392 |
assumes 1: "\<phi> xs" and 2: "alw (\<phi> impl (\<psi> or nxt \<phi>)) xs" |
|
393 |
shows "(alw \<phi> or ev \<psi>) xs" |
|
394 |
proof- |
|
395 |
{assume "\<not> ev \<psi> xs" hence "alw (not \<psi>) xs" unfolding not_ev[symmetric] . |
|
396 |
moreover have "alw (not \<psi> impl (\<phi> impl nxt \<phi>)) xs" |
|
61239 | 397 |
using 2 by coinduct auto |
58627 | 398 |
ultimately have "alw (\<phi> impl nxt \<phi>) xs" by(auto dest: alw_mp) |
399 |
with 1 have "alw \<phi> xs" by(rule alw_invar) |
|
400 |
} |
|
401 |
thus ?thesis by blast |
|
402 |
qed |
|
403 |
||
404 |
lemma ev_alw_imp_nxt: |
|
405 |
assumes e: "ev \<phi> xs" and a: "alw (\<phi> impl (nxt \<phi>)) xs" |
|
406 |
shows "ev (alw \<phi>) xs" |
|
407 |
proof- |
|
408 |
obtain xl xs1 where xs: "xs = xl @- xs1" and \<phi>: "\<phi> xs1" |
|
409 |
using e by (metis ev_imp_shift) |
|
410 |
have "\<phi> xs1 \<and> alw (\<phi> impl (nxt \<phi>)) xs1" using a \<phi> unfolding xs by (metis alw_shift) |
|
61239 | 411 |
hence "alw \<phi> xs1" by(coinduct xs1 rule: alw.coinduct) auto |
58627 | 412 |
thus ?thesis unfolding xs by (auto intro: alw_ev_shift) |
413 |
qed |
|
414 |
||
415 |
||
59000 | 416 |
inductive ev_at :: "('a stream \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a stream \<Rightarrow> bool" for P :: "'a stream \<Rightarrow> bool" where |
417 |
base: "P \<omega> \<Longrightarrow> ev_at P 0 \<omega>" |
|
418 |
| step:"\<not> P \<omega> \<Longrightarrow> ev_at P n (stl \<omega>) \<Longrightarrow> ev_at P (Suc n) \<omega>" |
|
419 |
||
420 |
inductive_simps ev_at_0[simp]: "ev_at P 0 \<omega>" |
|
421 |
inductive_simps ev_at_Suc[simp]: "ev_at P (Suc n) \<omega>" |
|
422 |
||
423 |
lemma ev_at_imp_snth: "ev_at P n \<omega> \<Longrightarrow> P (sdrop n \<omega>)" |
|
424 |
by (induction n arbitrary: \<omega>) auto |
|
425 |
||
426 |
lemma ev_at_HLD_imp_snth: "ev_at (HLD X) n \<omega> \<Longrightarrow> \<omega> !! n \<in> X" |
|
427 |
by (auto dest!: ev_at_imp_snth simp: HLD_iff) |
|
428 |
||
429 |
lemma ev_at_HLD_single_imp_snth: "ev_at (HLD {x}) n \<omega> \<Longrightarrow> \<omega> !! n = x" |
|
430 |
by (drule ev_at_HLD_imp_snth) simp |
|
431 |
||
432 |
lemma ev_at_unique: "ev_at P n \<omega> \<Longrightarrow> ev_at P m \<omega> \<Longrightarrow> n = m" |
|
433 |
proof (induction arbitrary: m rule: ev_at.induct) |
|
434 |
case (base \<omega>) then show ?case |
|
435 |
by (simp add: ev_at.simps[of _ _ \<omega>]) |
|
436 |
next |
|
437 |
case (step \<omega> n) from step.prems step.hyps step.IH[of "m - 1"] show ?case |
|
438 |
by (auto simp add: ev_at.simps[of _ _ \<omega>]) |
|
439 |
qed |
|
440 |
||
441 |
lemma ev_iff_ev_at: "ev P \<omega> \<longleftrightarrow> (\<exists>n. ev_at P n \<omega>)" |
|
442 |
proof |
|
443 |
assume "ev P \<omega>" then show "\<exists>n. ev_at P n \<omega>" |
|
444 |
by (induction rule: ev_induct_strong) (auto intro: ev_at.intros) |
|
445 |
next |
|
446 |
assume "\<exists>n. ev_at P n \<omega>" |
|
447 |
then obtain n where "ev_at P n \<omega>" |
|
448 |
by auto |
|
449 |
then show "ev P \<omega>" |
|
450 |
by induction auto |
|
451 |
qed |
|
452 |
||
453 |
lemma ev_at_shift: "ev_at (HLD X) i (stake (Suc i) \<omega> @- \<omega>' :: 's stream) \<longleftrightarrow> ev_at (HLD X) i \<omega>" |
|
454 |
by (induction i arbitrary: \<omega>) (auto simp: HLD_iff) |
|
455 |
||
456 |
lemma ev_iff_ev_at_unqiue: "ev P \<omega> \<longleftrightarrow> (\<exists>!n. ev_at P n \<omega>)" |
|
457 |
by (auto intro: ev_at_unique simp: ev_iff_ev_at) |
|
458 |
||
459 |
lemma alw_HLD_iff_streams: "alw (HLD X) \<omega> \<longleftrightarrow> \<omega> \<in> streams X" |
|
460 |
proof |
|
461 |
assume "alw (HLD X) \<omega>" then show "\<omega> \<in> streams X" |
|
462 |
proof (coinduction arbitrary: \<omega>) |
|
463 |
case (streams \<omega>) then show ?case by (cases \<omega>) auto |
|
464 |
qed |
|
465 |
next |
|
466 |
assume "\<omega> \<in> streams X" then show "alw (HLD X) \<omega>" |
|
467 |
proof (coinduction arbitrary: \<omega>) |
|
468 |
case (alw \<omega>) then show ?case by (cases \<omega>) auto |
|
469 |
qed |
|
470 |
qed |
|
471 |
||
472 |
lemma not_HLD: "not (HLD X) = HLD (- X)" |
|
473 |
by (auto simp: HLD_iff) |
|
474 |
||
475 |
lemma not_alw_iff: "\<not> (alw P \<omega>) \<longleftrightarrow> ev (not P) \<omega>" |
|
476 |
using not_alw[of P] by (simp add: fun_eq_iff) |
|
477 |
||
478 |
lemma not_ev_iff: "\<not> (ev P \<omega>) \<longleftrightarrow> alw (not P) \<omega>" |
|
479 |
using not_alw_iff[of "not P" \<omega>, symmetric] by simp |
|
480 |
||
481 |
lemma ev_Stream: "ev P (x ## s) \<longleftrightarrow> P (x ## s) \<or> ev P s" |
|
482 |
by (auto elim: ev.cases) |
|
483 |
||
484 |
lemma alw_ev_imp_ev_alw: |
|
485 |
assumes "alw (ev P) \<omega>" shows "ev (P aand alw (ev P)) \<omega>" |
|
486 |
proof - |
|
487 |
have "ev P \<omega>" using assms by auto |
|
488 |
from this assms show ?thesis |
|
489 |
by induct auto |
|
490 |
qed |
|
491 |
||
492 |
lemma ev_False: "ev (\<lambda>x. False) \<omega> \<longleftrightarrow> False" |
|
493 |
proof |
|
494 |
assume "ev (\<lambda>x. False) \<omega>" then show False |
|
495 |
by induct auto |
|
496 |
qed auto |
|
497 |
||
498 |
lemma alw_False: "alw (\<lambda>x. False) \<omega> \<longleftrightarrow> False" |
|
499 |
by auto |
|
500 |
||
501 |
lemma ev_iff_sdrop: "ev P \<omega> \<longleftrightarrow> (\<exists>m. P (sdrop m \<omega>))" |
|
502 |
proof safe |
|
503 |
assume "ev P \<omega>" then show "\<exists>m. P (sdrop m \<omega>)" |
|
504 |
by (induct rule: ev_induct_strong) (auto intro: exI[of _ 0] exI[of _ "Suc n" for n]) |
|
505 |
next |
|
506 |
fix m assume "P (sdrop m \<omega>)" then show "ev P \<omega>" |
|
507 |
by (induct m arbitrary: \<omega>) auto |
|
508 |
qed |
|
509 |
||
510 |
lemma alw_iff_sdrop: "alw P \<omega> \<longleftrightarrow> (\<forall>m. P (sdrop m \<omega>))" |
|
511 |
proof safe |
|
512 |
fix m assume "alw P \<omega>" then show "P (sdrop m \<omega>)" |
|
513 |
by (induct m arbitrary: \<omega>) auto |
|
514 |
next |
|
515 |
assume "\<forall>m. P (sdrop m \<omega>)" then show "alw P \<omega>" |
|
516 |
by (coinduction arbitrary: \<omega>) (auto elim: allE[of _ 0] allE[of _ "Suc n" for n]) |
|
517 |
qed |
|
518 |
||
519 |
lemma infinite_iff_alw_ev: "infinite {m. P (sdrop m \<omega>)} \<longleftrightarrow> alw (ev P) \<omega>" |
|
520 |
unfolding infinite_nat_iff_unbounded_le alw_iff_sdrop ev_iff_sdrop |
|
521 |
by simp (metis le_Suc_ex le_add1) |
|
522 |
||
523 |
lemma alw_inv: |
|
524 |
assumes stl: "\<And>s. f (stl s) = stl (f s)" |
|
525 |
shows "alw P (f s) \<longleftrightarrow> alw (\<lambda>x. P (f x)) s" |
|
526 |
proof |
|
527 |
assume "alw P (f s)" then show "alw (\<lambda>x. P (f x)) s" |
|
528 |
by (coinduction arbitrary: s rule: alw_coinduct) |
|
529 |
(auto simp: stl) |
|
530 |
next |
|
531 |
assume "alw (\<lambda>x. P (f x)) s" then show "alw P (f s)" |
|
532 |
by (coinduction arbitrary: s rule: alw_coinduct) (auto simp: stl[symmetric]) |
|
533 |
qed |
|
534 |
||
535 |
lemma ev_inv: |
|
536 |
assumes stl: "\<And>s. f (stl s) = stl (f s)" |
|
537 |
shows "ev P (f s) \<longleftrightarrow> ev (\<lambda>x. P (f x)) s" |
|
538 |
proof |
|
539 |
assume "ev P (f s)" then show "ev (\<lambda>x. P (f x)) s" |
|
540 |
by (induction "f s" arbitrary: s) (auto simp: stl) |
|
541 |
next |
|
542 |
assume "ev (\<lambda>x. P (f x)) s" then show "ev P (f s)" |
|
543 |
by induction (auto simp: stl[symmetric]) |
|
544 |
qed |
|
545 |
||
546 |
lemma alw_smap: "alw P (smap f s) \<longleftrightarrow> alw (\<lambda>x. P (smap f x)) s" |
|
547 |
by (rule alw_inv) simp |
|
548 |
||
549 |
lemma ev_smap: "ev P (smap f s) \<longleftrightarrow> ev (\<lambda>x. P (smap f x)) s" |
|
550 |
by (rule ev_inv) simp |
|
551 |
||
552 |
lemma alw_cong: |
|
553 |
assumes P: "alw P \<omega>" and eq: "\<And>\<omega>. P \<omega> \<Longrightarrow> Q1 \<omega> \<longleftrightarrow> Q2 \<omega>" |
|
554 |
shows "alw Q1 \<omega> \<longleftrightarrow> alw Q2 \<omega>" |
|
555 |
proof - |
|
556 |
from eq have "(alw P aand Q1) = (alw P aand Q2)" by auto |
|
557 |
then have "alw (alw P aand Q1) \<omega> = alw (alw P aand Q2) \<omega>" by auto |
|
558 |
with P show "alw Q1 \<omega> \<longleftrightarrow> alw Q2 \<omega>" |
|
559 |
by (simp add: alw_aand) |
|
560 |
qed |
|
561 |
||
562 |
lemma ev_cong: |
|
563 |
assumes P: "alw P \<omega>" and eq: "\<And>\<omega>. P \<omega> \<Longrightarrow> Q1 \<omega> \<longleftrightarrow> Q2 \<omega>" |
|
564 |
shows "ev Q1 \<omega> \<longleftrightarrow> ev Q2 \<omega>" |
|
565 |
proof - |
|
566 |
from P have "alw (\<lambda>xs. Q1 xs \<longrightarrow> Q2 xs) \<omega>" by (rule alw_mono) (simp add: eq) |
|
567 |
moreover from P have "alw (\<lambda>xs. Q2 xs \<longrightarrow> Q1 xs) \<omega>" by (rule alw_mono) (simp add: eq) |
|
568 |
moreover note ev_alw_impl[of Q1 \<omega> Q2] ev_alw_impl[of Q2 \<omega> Q1] |
|
569 |
ultimately show "ev Q1 \<omega> \<longleftrightarrow> ev Q2 \<omega>" |
|
570 |
by auto |
|
571 |
qed |
|
572 |
||
573 |
lemma alwD: "alw P x \<Longrightarrow> P x" |
|
574 |
by auto |
|
575 |
||
576 |
lemma alw_alwD: "alw P \<omega> \<Longrightarrow> alw (alw P) \<omega>" |
|
577 |
by simp |
|
578 |
||
579 |
lemma alw_ev_stl: "alw (ev P) (stl \<omega>) \<longleftrightarrow> alw (ev P) \<omega>" |
|
580 |
by (auto intro: alw.intros) |
|
581 |
||
582 |
lemma holds_Stream: "holds P (x ## s) \<longleftrightarrow> P x" |
|
583 |
by simp |
|
584 |
||
585 |
lemma holds_eq1[simp]: "holds (op = x) = HLD {x}" |
|
586 |
by rule (auto simp: HLD_iff) |
|
587 |
||
588 |
lemma holds_eq2[simp]: "holds (\<lambda>y. y = x) = HLD {x}" |
|
589 |
by rule (auto simp: HLD_iff) |
|
590 |
||
591 |
lemma not_holds_eq[simp]: "holds (- op = x) = not (HLD {x})" |
|
592 |
by rule (auto simp: HLD_iff) |
|
593 |
||
60500 | 594 |
text \<open>Strong until\<close> |
59000 | 595 |
|
61681
ca53150406c9
option "inductive_defs" controls exposure of def and mono facts;
wenzelm
parents:
61239
diff
changeset
|
596 |
context |
ca53150406c9
option "inductive_defs" controls exposure of def and mono facts;
wenzelm
parents:
61239
diff
changeset
|
597 |
notes [[inductive_defs]] |
ca53150406c9
option "inductive_defs" controls exposure of def and mono facts;
wenzelm
parents:
61239
diff
changeset
|
598 |
begin |
ca53150406c9
option "inductive_defs" controls exposure of def and mono facts;
wenzelm
parents:
61239
diff
changeset
|
599 |
|
59000 | 600 |
inductive suntil (infix "suntil" 60) for \<phi> \<psi> where |
601 |
base: "\<psi> \<omega> \<Longrightarrow> (\<phi> suntil \<psi>) \<omega>" |
|
602 |
| step: "\<phi> \<omega> \<Longrightarrow> (\<phi> suntil \<psi>) (stl \<omega>) \<Longrightarrow> (\<phi> suntil \<psi>) \<omega>" |
|
603 |
||
604 |
inductive_simps suntil_Stream: "(\<phi> suntil \<psi>) (x ## s)" |
|
605 |
||
61681
ca53150406c9
option "inductive_defs" controls exposure of def and mono facts;
wenzelm
parents:
61239
diff
changeset
|
606 |
end |
ca53150406c9
option "inductive_defs" controls exposure of def and mono facts;
wenzelm
parents:
61239
diff
changeset
|
607 |
|
59000 | 608 |
lemma suntil_induct_strong[consumes 1, case_names base step]: |
609 |
"(\<phi> suntil \<psi>) x \<Longrightarrow> |
|
610 |
(\<And>\<omega>. \<psi> \<omega> \<Longrightarrow> P \<omega>) \<Longrightarrow> |
|
611 |
(\<And>\<omega>. \<phi> \<omega> \<Longrightarrow> \<not> \<psi> \<omega> \<Longrightarrow> (\<phi> suntil \<psi>) (stl \<omega>) \<Longrightarrow> P (stl \<omega>) \<Longrightarrow> P \<omega>) \<Longrightarrow> P x" |
|
612 |
using suntil.induct[of \<phi> \<psi> x P] by blast |
|
613 |
||
614 |
lemma ev_suntil: "(\<phi> suntil \<psi>) \<omega> \<Longrightarrow> ev \<psi> \<omega>" |
|
61239 | 615 |
by (induct rule: suntil.induct) auto |
59000 | 616 |
|
617 |
lemma suntil_inv: |
|
618 |
assumes stl: "\<And>s. f (stl s) = stl (f s)" |
|
619 |
shows "(P suntil Q) (f s) \<longleftrightarrow> ((\<lambda>x. P (f x)) suntil (\<lambda>x. Q (f x))) s" |
|
620 |
proof |
|
621 |
assume "(P suntil Q) (f s)" then show "((\<lambda>x. P (f x)) suntil (\<lambda>x. Q (f x))) s" |
|
622 |
by (induction "f s" arbitrary: s) (auto simp: stl intro: suntil.intros) |
|
623 |
next |
|
624 |
assume "((\<lambda>x. P (f x)) suntil (\<lambda>x. Q (f x))) s" then show "(P suntil Q) (f s)" |
|
625 |
by induction (auto simp: stl[symmetric] intro: suntil.intros) |
|
626 |
qed |
|
627 |
||
628 |
lemma suntil_smap: "(P suntil Q) (smap f s) \<longleftrightarrow> ((\<lambda>x. P (smap f x)) suntil (\<lambda>x. Q (smap f x))) s" |
|
629 |
by (rule suntil_inv) simp |
|
630 |
||
631 |
lemma hld_smap: "HLD x (smap f s) = holds (\<lambda>y. f y \<in> x) s" |
|
632 |
by (simp add: HLD_def) |
|
633 |
||
634 |
lemma suntil_mono: |
|
635 |
assumes eq: "\<And>\<omega>. P \<omega> \<Longrightarrow> Q1 \<omega> \<Longrightarrow> Q2 \<omega>" "\<And>\<omega>. P \<omega> \<Longrightarrow> R1 \<omega> \<Longrightarrow> R2 \<omega>" |
|
636 |
assumes *: "(Q1 suntil R1) \<omega>" "alw P \<omega>" shows "(Q2 suntil R2) \<omega>" |
|
637 |
using * by induct (auto intro: eq suntil.intros) |
|
638 |
||
639 |
lemma suntil_cong: |
|
640 |
"alw P \<omega> \<Longrightarrow> (\<And>\<omega>. P \<omega> \<Longrightarrow> Q1 \<omega> \<longleftrightarrow> Q2 \<omega>) \<Longrightarrow> (\<And>\<omega>. P \<omega> \<Longrightarrow> R1 \<omega> \<longleftrightarrow> R2 \<omega>) \<Longrightarrow> |
|
641 |
(Q1 suntil R1) \<omega> \<longleftrightarrow> (Q2 suntil R2) \<omega>" |
|
642 |
using suntil_mono[of P Q1 Q2 R1 R2 \<omega>] suntil_mono[of P Q2 Q1 R2 R1 \<omega>] by auto |
|
643 |
||
644 |
lemma ev_suntil_iff: "ev (P suntil Q) \<omega> \<longleftrightarrow> ev Q \<omega>" |
|
645 |
proof |
|
646 |
assume "ev (P suntil Q) \<omega>" then show "ev Q \<omega>" |
|
647 |
by induct (auto dest: ev_suntil) |
|
648 |
next |
|
649 |
assume "ev Q \<omega>" then show "ev (P suntil Q) \<omega>" |
|
650 |
by induct (auto intro: suntil.intros) |
|
651 |
qed |
|
652 |
||
653 |
lemma true_suntil: "((\<lambda>_. True) suntil P) = ev P" |
|
654 |
by (simp add: suntil_def ev_def) |
|
655 |
||
656 |
lemma suntil_lfp: "(\<phi> suntil \<psi>) = lfp (\<lambda>P s. \<psi> s \<or> (\<phi> s \<and> P (stl s)))" |
|
657 |
by (simp add: suntil_def) |
|
658 |
||
659 |
lemma sfilter_P[simp]: "P (shd s) \<Longrightarrow> sfilter P s = shd s ## sfilter P (stl s)" |
|
660 |
using sfilter_Stream[of P "shd s" "stl s"] by simp |
|
661 |
||
662 |
lemma sfilter_not_P[simp]: "\<not> P (shd s) \<Longrightarrow> sfilter P s = sfilter P (stl s)" |
|
663 |
using sfilter_Stream[of P "shd s" "stl s"] by simp |
|
664 |
||
665 |
lemma sfilter_eq: |
|
666 |
assumes "ev (holds P) s" |
|
667 |
shows "sfilter P s = x ## s' \<longleftrightarrow> |
|
668 |
P x \<and> (not (holds P) suntil (HLD {x} aand nxt (\<lambda>s. sfilter P s = s'))) s" |
|
669 |
using assms |
|
670 |
by (induct rule: ev_induct_strong) |
|
671 |
(auto simp add: HLD_iff intro: suntil.intros elim: suntil.cases) |
|
672 |
||
673 |
lemma sfilter_streams: |
|
674 |
"alw (ev (holds P)) \<omega> \<Longrightarrow> \<omega> \<in> streams A \<Longrightarrow> sfilter P \<omega> \<in> streams {x\<in>A. P x}" |
|
675 |
proof (coinduction arbitrary: \<omega>) |
|
676 |
case (streams \<omega>) |
|
677 |
then have "ev (holds P) \<omega>" by blast |
|
678 |
from this streams show ?case |
|
679 |
by (induct rule: ev_induct_strong) (auto elim: streamsE) |
|
680 |
qed |
|
681 |
||
682 |
lemma alw_sfilter: |
|
683 |
assumes *: "alw (ev (holds P)) s" |
|
684 |
shows "alw Q (sfilter P s) \<longleftrightarrow> alw (\<lambda>x. Q (sfilter P x)) s" |
|
685 |
proof |
|
686 |
assume "alw Q (sfilter P s)" with * show "alw (\<lambda>x. Q (sfilter P x)) s" |
|
687 |
proof (coinduction arbitrary: s rule: alw_coinduct) |
|
688 |
case (stl s) |
|
689 |
then have "ev (holds P) s" |
|
690 |
by blast |
|
691 |
from this stl show ?case |
|
692 |
by (induct rule: ev_induct_strong) auto |
|
693 |
qed auto |
|
694 |
next |
|
695 |
assume "alw (\<lambda>x. Q (sfilter P x)) s" with * show "alw Q (sfilter P s)" |
|
696 |
proof (coinduction arbitrary: s rule: alw_coinduct) |
|
697 |
case (stl s) |
|
698 |
then have "ev (holds P) s" |
|
699 |
by blast |
|
700 |
from this stl show ?case |
|
701 |
by (induct rule: ev_induct_strong) auto |
|
702 |
qed auto |
|
703 |
qed |
|
704 |
||
705 |
lemma ev_sfilter: |
|
706 |
assumes *: "alw (ev (holds P)) s" |
|
707 |
shows "ev Q (sfilter P s) \<longleftrightarrow> ev (\<lambda>x. Q (sfilter P x)) s" |
|
708 |
proof |
|
709 |
assume "ev Q (sfilter P s)" from this * show "ev (\<lambda>x. Q (sfilter P x)) s" |
|
710 |
proof (induction "sfilter P s" arbitrary: s rule: ev_induct_strong) |
|
711 |
case (step s) |
|
712 |
then have "ev (holds P) s" |
|
713 |
by blast |
|
714 |
from this step show ?case |
|
715 |
by (induct rule: ev_induct_strong) auto |
|
716 |
qed auto |
|
717 |
next |
|
718 |
assume "ev (\<lambda>x. Q (sfilter P x)) s" then show "ev Q (sfilter P s)" |
|
719 |
proof (induction rule: ev_induct_strong) |
|
720 |
case (step s) then show ?case |
|
721 |
by (cases "P (shd s)") auto |
|
722 |
qed auto |
|
723 |
qed |
|
724 |
||
725 |
lemma holds_sfilter: |
|
726 |
assumes "ev (holds Q) s" shows "holds P (sfilter Q s) \<longleftrightarrow> (not (holds Q) suntil (holds (Q aand P))) s" |
|
727 |
proof |
|
728 |
assume "holds P (sfilter Q s)" with assms show "(not (holds Q) suntil (holds (Q aand P))) s" |
|
729 |
by (induct rule: ev_induct_strong) (auto intro: suntil.intros) |
|
730 |
next |
|
731 |
assume "(not (holds Q) suntil (holds (Q aand P))) s" then show "holds P (sfilter Q s)" |
|
732 |
by induct auto |
|
733 |
qed |
|
734 |
||
735 |
lemma suntil_aand_nxt: |
|
736 |
"(\<phi> suntil (\<phi> aand nxt \<psi>)) \<omega> \<longleftrightarrow> (\<phi> aand nxt (\<phi> suntil \<psi>)) \<omega>" |
|
737 |
proof |
|
738 |
assume "(\<phi> suntil (\<phi> aand nxt \<psi>)) \<omega>" then show "(\<phi> aand nxt (\<phi> suntil \<psi>)) \<omega>" |
|
739 |
by induction (auto intro: suntil.intros) |
|
740 |
next |
|
741 |
assume "(\<phi> aand nxt (\<phi> suntil \<psi>)) \<omega>" |
|
742 |
then have "(\<phi> suntil \<psi>) (stl \<omega>)" "\<phi> \<omega>" |
|
743 |
by auto |
|
744 |
then show "(\<phi> suntil (\<phi> aand nxt \<psi>)) \<omega>" |
|
745 |
by (induction "stl \<omega>" arbitrary: \<omega>) |
|
746 |
(auto elim: suntil.cases intro: suntil.intros) |
|
747 |
qed |
|
748 |
||
749 |
lemma alw_sconst: "alw P (sconst x) \<longleftrightarrow> P (sconst x)" |
|
750 |
proof |
|
751 |
assume "P (sconst x)" then show "alw P (sconst x)" |
|
752 |
by coinduction auto |
|
753 |
qed auto |
|
754 |
||
755 |
lemma ev_sconst: "ev P (sconst x) \<longleftrightarrow> P (sconst x)" |
|
756 |
proof |
|
757 |
assume "ev P (sconst x)" then show "P (sconst x)" |
|
758 |
by (induction "sconst x") auto |
|
759 |
qed auto |
|
760 |
||
761 |
lemma suntil_sconst: "(\<phi> suntil \<psi>) (sconst x) \<longleftrightarrow> \<psi> (sconst x)" |
|
762 |
proof |
|
763 |
assume "(\<phi> suntil \<psi>) (sconst x)" then show "\<psi> (sconst x)" |
|
764 |
by (induction "sconst x") auto |
|
765 |
qed (auto intro: suntil.intros) |
|
766 |
||
767 |
lemma hld_smap': "HLD x (smap f s) = HLD (f -` x) s" |
|
768 |
by (simp add: HLD_def) |
|
58627 | 769 |
|
770 |
end |