src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy
 changeset 64320 ba194424b895 parent 63117 acb6d72fc42e child 64911 f0e07600de47
```     1.1 --- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Thu Oct 20 18:41:58 2016 +0200
1.2 +++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Thu Oct 20 18:41:59 2016 +0200
1.3 @@ -662,7 +662,7 @@
1.4  lemma sfilter_not_P[simp]: "\<not> P (shd s) \<Longrightarrow> sfilter P s = sfilter P (stl s)"
1.5    using sfilter_Stream[of P "shd s" "stl s"] by simp
1.6
1.7 -lemma sfilter_eq:
1.8 +lemma sfilter_eq:
1.9    assumes "ev (holds P) s"
1.10    shows "sfilter P s = x ## s' \<longleftrightarrow>
1.11      P x \<and> (not (holds P) suntil (HLD {x} aand nxt (\<lambda>s. sfilter P s = s'))) s"
1.12 @@ -685,7 +685,7 @@
1.13  proof
1.14    assume "alw Q (sfilter P s)" with * show "alw (\<lambda>x. Q (sfilter P x)) s"
1.15    proof (coinduction arbitrary: s rule: alw_coinduct)
1.16 -    case (stl s)
1.17 +    case (stl s)
1.18      then have "ev (holds P) s"
1.19        by blast
1.20      from this stl show ?case
1.21 @@ -694,7 +694,7 @@
1.22  next
1.23    assume "alw (\<lambda>x. Q (sfilter P x)) s" with * show "alw Q (sfilter P s)"
1.24    proof (coinduction arbitrary: s rule: alw_coinduct)
1.25 -    case (stl s)
1.26 +    case (stl s)
1.27      then have "ev (holds P) s"
1.28        by blast
1.29      from this stl show ?case
1.30 @@ -767,4 +767,22 @@
1.31  lemma hld_smap': "HLD x (smap f s) = HLD (f -` x) s"
1.33
1.34 +lemma pigeonhole_stream:
1.35 +  assumes "alw (HLD s) \<omega>"
1.36 +  assumes "finite s"
1.37 +  shows "\<exists>x\<in>s. alw (ev (HLD {x})) \<omega>"
1.38 +proof -
1.39 +  have "\<forall>i\<in>UNIV. \<exists>x\<in>s. \<omega> !! i = x"
1.40 +    using `alw (HLD s) \<omega>` by (simp add: alw_iff_sdrop HLD_iff)
1.41 +  from pigeonhole_infinite_rel[OF infinite_UNIV_nat `finite s` this]
1.42 +  show ?thesis
1.43 +    by (simp add: HLD_iff infinite_iff_alw_ev[symmetric])
1.44 +qed
1.45 +
1.46 +lemma ev_eq_suntil: "ev P \<omega> \<longleftrightarrow> (not P suntil P) \<omega>"
1.47 +proof
1.48 +  assume "ev P \<omega>" then show "((\<lambda>xs. \<not> P xs) suntil P) \<omega>"
1.49 +    by (induction rule: ev_induct_strong) (auto intro: suntil.intros)
1.50 +qed (auto simp: ev_suntil)
1.51 +
1.52  end
```