src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy

   using sfilter_Stream[of P "shd s" "stl s"] by simp
 
 lemma sfilter_not_P[simp]: "\<not> P (shd s) \<Longrightarrow> sfilter P s = sfilter P (stl s)"
   using sfilter_Stream[of P "shd s" "stl s"] by simp
 
-lemma sfilter_eq: 
+lemma sfilter_eq:
   assumes "ev (holds P) s"
   shows "sfilter P s = x ## s' \<longleftrightarrow>
     P x \<and> (not (holds P) suntil (HLD {x} aand nxt (\<lambda>s. sfilter P s = s'))) s"
   using assms
   by (induct rule: ev_induct_strong)

   assumes *: "alw (ev (holds P)) s"
   shows "alw Q (sfilter P s) \<longleftrightarrow> alw (\<lambda>x. Q (sfilter P x)) s"
 proof
   assume "alw Q (sfilter P s)" with * show "alw (\<lambda>x. Q (sfilter P x)) s"
   proof (coinduction arbitrary: s rule: alw_coinduct)
-    case (stl s) 
+    case (stl s)
     then have "ev (holds P) s"
       by blast
     from this stl show ?case
       by (induct rule: ev_induct_strong) auto
   qed auto
 next
   assume "alw (\<lambda>x. Q (sfilter P x)) s" with * show "alw Q (sfilter P s)"
   proof (coinduction arbitrary: s rule: alw_coinduct)
-    case (stl s) 
+    case (stl s)
     then have "ev (holds P) s"
       by blast
     from this stl show ?case
       by (induct rule: ev_induct_strong) auto
   qed auto

 qed (auto intro: suntil.intros)
 
 lemma hld_smap': "HLD x (smap f s) = HLD (f -` x) s"
   by (simp add: HLD_def)
 
+lemma pigeonhole_stream:
+  assumes "alw (HLD s) \<omega>"
+  assumes "finite s"
+  shows "\<exists>x\<in>s. alw (ev (HLD {x})) \<omega>"
+proof -
+  have "\<forall>i\<in>UNIV. \<exists>x\<in>s. \<omega> !! i = x"
+    using `alw (HLD s) \<omega>` by (simp add: alw_iff_sdrop HLD_iff)
+  from pigeonhole_infinite_rel[OF infinite_UNIV_nat `finite s` this]
+  show ?thesis
+    by (simp add: HLD_iff infinite_iff_alw_ev[symmetric])
+qed
+
+lemma ev_eq_suntil: "ev P \<omega> \<longleftrightarrow> (not P suntil P) \<omega>"
+proof
+  assume "ev P \<omega>" then show "((\<lambda>xs. \<not> P xs) suntil P) \<omega>"
+    by (induction rule: ev_induct_strong) (auto intro: suntil.intros)
+qed (auto simp: ev_suntil)
+
 end