Theory Applicative_Open_State

(* Author: Joshua Schneider, ETH Zurich *)

subsection ‹Open state monad›

theory Applicative_Open_State imports
  Applicative
  "HOL-Library.Adhoc_Overloading"
begin

type_synonym ('a, 's) state = "'s ⇒ 'a × 's"

definition "ap_state f x = (λs. case f s of (g, s') ⇒ case x s' of (y, s'') ⇒ (g y, s''))"

abbreviation (input) "pure_state ≡ Pair"

adhoc_overloading Applicative.ap ap_state

applicative state
for
  pure: pure_state
  ap: "ap_state :: ('a ⇒ 'b, 's) state ⇒ ('a, 's) state ⇒ ('b, 's) state"
unfolding ap_state_def
by (auto split: prod.split)

end