Theory Heap_Monad_Ext

theory Heap_Monad_Ext
imports Imperative_HOL
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