section ‹Stream Iterators›

theory Stream
imports LazyList
begin

subsection ‹Type definitions for streams›

text ‹Note that everything is strict in the state type.›

domain ('a,'s) Step = Done | Skip 's | Yield (lazy 'a) 's

type_synonym ('a, 's) Stepper = "'s → ('a, 's) Step"

domain ('a,'s) Stream = Stream (lazy "('a, 's) Stepper") 's


subsection ‹Converting from streams to lists›

fixrec
  unfold :: "('a, 's) Stepper -> ('s -> 'a LList)"
where
  "unfold⋅h⋅⊥ = ⊥"
| "s ≠ ⊥ ==>
    unfold⋅h⋅s =
      (case h⋅s of
        Done → LNil
      | Skip⋅s' → unfold⋅h⋅s'
      | Yield⋅x⋅s' → LCons⋅x⋅(unfold⋅h⋅s'))"

fixrec
  unfoldF :: "('a, 's) Stepper → ('s → 'a LList) → ('s → 'a LList)"
where
  "unfoldF⋅h⋅u⋅⊥ = ⊥"
| "s ≠ ⊥ ==>
    unfoldF⋅h⋅u⋅s =
      (case h⋅s of
        Done → LNil
      | Skip⋅s' → u⋅s'
      | Yield⋅x⋅s' → LCons⋅x⋅(u⋅s'))"

lemma unfold_eq_fix: "unfold⋅h = fix⋅(unfoldF⋅h)"
proof (rule below_antisym)
  show "unfold⋅h ⊑ fix⋅(unfoldF⋅h)"
    apply (rule unfold.induct, simp, simp)
    apply (subst fix_eq)
    apply (rule cfun_belowI, rename_tac s)
    apply (case_tac "s = ⊥", simp, simp)
    apply (intro monofun_cfun monofun_LAM below_refl, simp_all)
    done
  show "fix⋅(unfoldF⋅h) ⊑ unfold⋅h"
    apply (rule fix_ind, simp, simp)
    apply (subst unfold.unfold)
    apply (rule cfun_belowI, rename_tac s)
    apply (case_tac "s = ⊥", simp, simp)
    apply (intro monofun_cfun monofun_LAM below_refl, simp_all)
    done
qed

lemma unfold_ind:
    fixes P :: "('s → 'a LList) → bool"
    assumes "adm P" and "P ⊥" and "∧u. P u ==> P (unfoldF⋅h⋅u)"
    shows "P (unfold⋅h)"
unfolding unfold_eq_fix by (rule fix_ind [of P, OF assms])

fixrec
  unfold2 :: "('s → 'a LList) → ('a, 's) Step → 'a LList"
where
  "unfold2⋅u⋅Done = LNil"
| "s ≠ ⊥ ==> unfold2⋅u⋅(Skip⋅s) = u⋅s"
| "s ≠ ⊥ ==> unfold2⋅u⋅(Yield⋅x⋅s) = LCons⋅x⋅(u⋅s)"

lemma unfold2_strict [simp]: "unfold2⋅u⋅⊥ = ⊥"
by fixrec_simp

lemma unfold: "s ≠ ⊥ ==> unfold⋅h⋅s = unfold2⋅(unfold⋅h)⋅(h⋅s)"
by (case_tac "h⋅s", simp_all)

lemma unfoldF: "s ≠ ⊥ ==> unfoldF⋅h⋅u⋅s = unfold2⋅u⋅(h⋅s)"
by (case_tac "h⋅s", simp_all)

declare unfold.simps(2) [simp del]
declare unfoldF.simps(2) [simp del]
declare unfoldF [simp]

fixrec
  unstream :: "('a, 's) Stream → 'a LList"
where
  "s ≠ ⊥ ==> unstream⋅(Stream⋅h⋅s) = unfold⋅h⋅s"

lemma unstream_strict [simp]: "unstream⋅⊥ = ⊥"
by fixrec_simp


subsection ‹Converting from lists to streams›

fixrec
  streamStep :: "('a LList)_\<bottom> → ('a, ('a LList)_\<bottom>) Step"
where
  "streamStep⋅(up⋅LNil) = Done"
| "streamStep⋅(up⋅(LCons⋅x⋅xs)) = Yield⋅x⋅(up⋅xs)"

lemma streamStep_strict [simp]: "streamStep⋅(up⋅⊥) = ⊥"
by fixrec_simp

fixrec
  stream :: "'a LList → ('a, ('a LList)_\<bottom>) Stream"
where
  "stream⋅xs = Stream⋅streamStep⋅(up⋅xs)"

lemma stream_defined [simp]: "stream⋅xs ≠ ⊥"
  by simp

lemma unstream_stream [simp]:
  fixes xs :: "'a LList"
  shows "unstream⋅(stream⋅xs) = xs"
by (induct xs, simp_all add: unfold)

declare stream.simps [simp del]


subsection ‹Bisimilarity relation on streams›

definition
  bisimilar :: "('a, 's) Stream → ('a, 't) Stream → bool" (infix ‹≈› 50)
where
  "a ≈ b ⟷ unstream⋅a = unstream⋅b ∧ a ≠ ⊥ ∧ b ≠ ⊥"

lemma unstream_cong:
  "a ≈ b ==> unstream⋅a = unstream⋅b"
    unfolding bisimilar_def by simp

lemma stream_cong:
  "xs = ys ==> stream⋅xs ≈ stream⋅ys"
    unfolding bisimilar_def by simp

lemma stream_unstream_cong:
  "a ≈ b ==> stream⋅(unstream⋅a) ≈ b"
    unfolding bisimilar_def by simp

end