Theory Monad_Memo_DP.Heap_Monad_Ext

subsection ‹Heap Monad›

theory Heap_Monad_Ext
  imports "HOL-Imperative_HOL.Imperative_HOL"
begin

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

bundle heap_monad_syntax begin

notation fun_app_lifted (infixl . 999)
type_synonym ('a, 'b) fun_lifted = "'a  'b Heap" (‹_ ==H⟹ _› [3,2] 2)
type_notation Heap ([_])

notation Heap_Monad.return (_)
notation (ASCII) Heap_Monad.return ((#_#))
notation Transfer.Rel (Rel)

end

context includes heap_monad_syntax begin

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

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

qualified definition ifT :: "bool Heap  'a Heap  'a Heap  'a Heap" where
  "ifT bT xT yT  do {b  bT; if b then xT else yT}"
end

end