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