# Theory Fair_Stream

```section ‹Fair Streams›

theory Fair_Stream imports "HOL-Library.Stream" begin

definition upt_lists :: ‹nat list stream› where
‹upt_lists ≡ smap (upt 0) (stl nats)›

definition fair_nats :: ‹nat stream› where
‹fair_nats ≡ flat upt_lists›

definition fair :: ‹'a stream ⇒ bool› where
‹fair s ≡ ∀x ∈ sset s. ∀m. ∃n ≥ m. s !! n = x›

lemma upt_lists_snth: ‹x ≤ n ⟹ x ∈ set (upt_lists !! n)›
unfolding upt_lists_def by auto

lemma all_ex_upt_lists: ‹∃n ≥ m. x ∈ set (upt_lists !! n)›
using upt_lists_snth by (meson dual_order.strict_trans1 gt_ex nle_le)

lemma upt_lists_ne: ‹∀xs ∈ sset upt_lists. xs ≠ []›
unfolding upt_lists_def by (simp add: sset_range)

lemma sset_flat_stl: ‹sset (flat (stl s)) ⊆ sset (flat s)›
proof (cases s)
case (SCons x xs)
then show ?thesis
by (cases x) (simp add: stl_sset subsetI, auto)
qed

lemma flat_snth_nth:
assumes ‹x = s !! n ! m› ‹m < length (s !! n)› ‹∀xs ∈ sset s. xs ≠ []›
shows ‹∃n' ≥ n. x = flat s !! n'›
using assms
proof (induct n arbitrary: s)
case 0
then show ?case
using flat_snth by fastforce
next
case (Suc n)
have ‹?case = (∃n' ≥ n. x = flat s !! Suc n')›
by (metis Suc_le_D Suc_le_mono)
also have ‹… = (∃n' ≥ n. x = stl (flat s) !! n')›
by simp
finally have ‹?case = (∃n' ≥ n. x = (tl (shd s) @- flat (stl s)) !! n')›
using Suc.prems flat_unfold by (simp add: shd_sset)
then have ?case if ‹∃n' ≥ n. x = flat (stl s) !! n'›
moreover {
have ‹x = stl s !! n ! m› ‹ m < length (stl s !! n)›
using Suc.prems by simp_all
moreover have ‹∀xs ∈ sset (stl s). xs ≠ []›
using Suc.prems by (cases s) simp_all
ultimately have ‹∃n' ≥ n. x = flat (stl s) !! n'›
using Suc.hyps by blast }
ultimately show ?case .
qed

lemma all_ex_fair_nats: ‹∃n ≥ m. fair_nats !! n = x›
proof -
have ‹∃n ≥ m. x ∈ set (upt_lists !! n)›
using all_ex_upt_lists .
then have ‹∃n ≥ m. ∃k < length (upt_lists !! n). upt_lists !! n ! k = x›
then obtain n k where ‹m ≤ n› ‹k < length (upt_lists !! n)› ‹upt_lists !! n ! k = x›
by blast
then obtain n' where ‹n ≤ n'› ‹x = flat upt_lists !! n'›
using flat_snth_nth upt_lists_ne by metis
moreover have ‹m ≤ n'›
using ‹m ≤ n› ‹n ≤ n'› by simp
ultimately show ?thesis
unfolding fair_nats_def by blast
qed

lemma fair_surj:
assumes ‹surj f›
shows ‹fair (smap f fair_nats)›
using assms unfolding fair_def by (metis UNIV_I all_ex_fair_nats imageE snth_smap)

definition fair_stream :: ‹(nat ⇒ 'a) ⇒ 'a stream› where
‹fair_stream f ≡ smap f fair_nats›

theorem fair_stream: ‹surj f ⟹ fair (fair_stream f)›
unfolding fair_stream_def using fair_surj .

theorem UNIV_stream: ‹surj f ⟹ sset (fair_stream f) = UNIV›
unfolding fair_stream_def using all_ex_fair_nats by (metis sset_range stream.set_map surjI)

end
```