Theory Monad_Memo_DP.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 f⇩T x⇩T ≡ do { f ← f⇩T; x ← x⇩T; 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 if⇩T :: "('M, bool) state ⇒ ('M, 'a) state ⇒ ('M, 'a) state ⇒ ('M, 'a) state" where
  "if⇩T b⇩T x⇩T y⇩T ≡ do {b ← b⇩T; if b then x⇩T else y⇩T}"
end

end