Theory Applicative_Stream

(* Author:     Andreas Lochbihler, ETH Zurich
   Author:     Joshua Schneider, ETH Zurich
*)

subsection ‹Streams as an applicative functor›

theory Applicative_Stream imports
  Applicative
  "HOL-Library.Stream"
  "HOL-Library.Adhoc_Overloading"
begin

primcorec (transfer) ap_stream :: "('a ⇒ 'b) stream ⇒ 'a stream ⇒ 'b stream"
where
    "shd (ap_stream f x) = shd f (shd x)"
  | "stl (ap_stream f x) = ap_stream (stl f) (stl x)"

adhoc_overloading Applicative.pure sconst
adhoc_overloading Applicative.ap ap_stream

context includes lifting_syntax applicative_syntax
begin

lemma ap_stream_id: "pure (λx. x) ⋄ x = x"
by (coinduction arbitrary: x) simp

lemma ap_stream_homo: "pure f ⋄ pure x = pure (f x)"
by coinduction simp

lemma ap_stream_interchange: "f ⋄ pure x = pure (λf. f x) ⋄ f"
by (coinduction arbitrary: f) auto

lemma ap_stream_composition: "pure (λg f x. g (f x)) ⋄ g ⋄ f ⋄ x = g ⋄ (f ⋄ x)"
by (coinduction arbitrary: g f x) auto

applicative stream (S, K)
for
  pure: sconst
  ap: ap_stream
  rel: stream_all2
  set: sset
proof -
  fix g :: "('b ⇒ 'a ⇒ 'c) stream" and f x
  show "pure (λg f x. g x (f x)) ⋄ g ⋄ f ⋄ x = g ⋄ x ⋄ (f ⋄ x)"
    by (coinduction arbitrary: g f x) auto
next
  fix x :: "'b stream" and y :: "'a stream"
  show "pure (λx y. x) ⋄ x ⋄ y = x"
    by (coinduction arbitrary: x y) auto
next
  fix R :: "'a ⇒ 'b ⇒ bool"
  show "(R ===> stream_all2 R) pure pure"
  proof
    fix x y
    assume "R x y"
    then show "stream_all2 R (pure x) (pure y)"
      by coinduction simp
  qed
next
  fix R and f :: "('a ⇒ 'b) stream" and g :: "('a ⇒ 'c) stream" and x
  assume [transfer_rule]: "stream_all2 (eq_on (sset x) ===> R) f g"
  have [transfer_rule]: "stream_all2 (eq_on (sset x)) x x" by(simp add: stream.rel_refl_strong)
  show "stream_all2 R (f ⋄ x) (g ⋄ x)" by transfer_prover
qed (rule ap_stream_homo)

lemma smap_applicative[applicative_unfold]: "smap f x = pure f ⋄ x"
unfolding ap_stream_def by (coinduction arbitrary: x) auto

lemma smap2_applicative[applicative_unfold]: "smap2 f x y = pure f ⋄ x ⋄ y"
unfolding ap_stream_def by (coinduction arbitrary: x y) auto

end

end