author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 64911  f0e07600de47 
child 67399  eab6ce8368fa 
permissions  rwrr 
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" 

63117  16 
shows "prefix xl yl" 
58627  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" 

63117  24 
shows "prefix xl yl \<or> prefix 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 
62093  68 
notes [[inductive_internals]] 
61681
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 

63117  300 
hence "prefix xl yl \<or> prefix yl xl" using shift_prefix_cases by auto 
58627  301 
thus ?thesis proof 
63117  302 
assume "prefix xl yl" 
303 
then obtain yl1 where yl: "yl = xl @ yl1" by (elim prefixE) 

58627  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 

63117  309 
assume "prefix yl xl" 
310 
then obtain xl1 where xl: "xl = yl @ xl1" by (elim prefixE) 

58627  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 
62093  597 
notes [[inductive_internals]] 
61681
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 

64320
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63117
diff
changeset

665 
lemma sfilter_eq: 
59000  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) 

64320
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63117
diff
changeset

688 
case (stl s) 
59000  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) 

64320
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63117
diff
changeset

697 
case (stl s) 
59000  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 

64320
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63117
diff
changeset

770 
lemma pigeonhole_stream: 
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63117
diff
changeset

771 
assumes "alw (HLD s) \<omega>" 
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63117
diff
changeset

772 
assumes "finite s" 
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63117
diff
changeset

773 
shows "\<exists>x\<in>s. alw (ev (HLD {x})) \<omega>" 
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63117
diff
changeset

774 
proof  
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63117
diff
changeset

775 
have "\<forall>i\<in>UNIV. \<exists>x\<in>s. \<omega> !! i = x" 
64911  776 
using \<open>alw (HLD s) \<omega>\<close> by (simp add: alw_iff_sdrop HLD_iff) 
777 
from pigeonhole_infinite_rel[OF infinite_UNIV_nat \<open>finite s\<close> this] 

64320
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63117
diff
changeset

778 
show ?thesis 
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63117
diff
changeset

779 
by (simp add: HLD_iff infinite_iff_alw_ev[symmetric]) 
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63117
diff
changeset

780 
qed 
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63117
diff
changeset

781 

ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63117
diff
changeset

782 
lemma ev_eq_suntil: "ev P \<omega> \<longleftrightarrow> (not P suntil P) \<omega>" 
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63117
diff
changeset

783 
proof 
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63117
diff
changeset

784 
assume "ev P \<omega>" then show "((\<lambda>xs. \<not> P xs) suntil P) \<omega>" 
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63117
diff
changeset

785 
by (induction rule: ev_induct_strong) (auto intro: suntil.intros) 
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63117
diff
changeset

786 
qed (auto simp: ev_suntil) 
ba194424b895
HOLProbability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63117
diff
changeset

787 

62390  788 
end 