Theory HOL-Imperative_HOL.Heap
section ‹A polymorphic heap based on cantor encodings›
theory Heap
imports Main "HOL-Library.Countable"
begin
subsection ‹Representable types›
text ‹The type class of representable types›
class heap = typerep + countable
instance unit :: heap ..
instance bool :: heap ..
instance nat :: heap ..
instance prod :: (heap, heap) heap ..
instance sum :: (heap, heap) heap ..
instance list :: (heap) heap ..
instance option :: (heap) heap ..
instance int :: heap ..
instance String.literal :: heap ..
instance char :: heap ..
instance typerep :: heap ..
subsection ‹A polymorphic heap with dynamic arrays and references›
text ‹
References and arrays are developed in parallel,
but keeping them separate makes some later proofs simpler.
›
type_synonym addr = nat
type_synonym heap_rep = nat
record heap =
arrays :: "typerep ⇒ addr ⇒ heap_rep list"
refs :: "typerep ⇒ addr ⇒ heap_rep"
lim :: addr
definition empty :: heap where
"empty = ⦇arrays = (λ_ _. []), refs = (λ_ _. 0), lim = 0⦈"