Theory State_Monad_Ext

subsection ‹State Monad›

theory State_Monad_Ext
  imports "HOL-Library.State_Monad"
begin

definition fun_app_lifted :: "('M,'a  ('M, 'b) state) state  ('M,'a) state  ('M,'b) state" where
  "fun_app_lifted fT xT  do { f  fT; x  xT; f x }"

bundle state_monad_syntax begin

notation fun_app_lifted (infixl "." 999)
type_synonym ('a,'M,'b) fun_lifted = "'a  ('M,'b) state" ("_ ==_ _" [3,1000,2] 2)
type_synonym ('a,'b) dpfun = "'a ==('a'b) 'b" (infixr "T" 2)
type_notation state ("[_| _]")

notation State_Monad.return ("_")
notation (ASCII) State_Monad.return ("(#_#)")
notation Transfer.Rel ("Rel")

end

context includes state_monad_syntax begin

qualified lemma return_app_return:
  "f . x = f x"
  unfolding fun_app_lifted_def bind_left_identity ..

qualified lemma return_app_return_meta:
  "f . x  f x"
  unfolding return_app_return .

qualified definition ifT :: "('M, bool) state  ('M, 'a) state  ('M, 'a) state  ('M, 'a) state" where
  "ifT bT xT yT  do {b  bT; if b then xT else yT}"
end

end