Theory State_Monad_Ext

theory State_Monad_Ext
imports State_Monad
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