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 f⇩T x⇩T ≡ do { f ← f⇩T; x ← x⇩T; 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 if⇩T :: "bool Heap ⇒ 'a Heap ⇒ 'a Heap ⇒ 'a Heap" where
  "if⇩T b⇩T x⇩T y⇩T ≡ do {b ← b⇩T; if b then x⇩T else y⇩T}"
end

end