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)

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
  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 .

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

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)