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.32    by (simp add: HLD_def)
    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