Theory Applicative_Stream
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