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'›
    using that by (metis (no_types, opaque_lifting) add.commute add_diff_cancel_left'
        dual_order.trans le_add2 shift_snth_ge)
  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›
    by (simp add: in_set_conv_nth)
  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