# Theory Heap

theory Heap
imports Countable
```(*  Title:      HOL/Imperative_HOL/Heap.thy
Author:     John Matthews, Galois Connections; Alexander Krauss, TU Muenchen
*)

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 ― ‹untyped heap references›
type_synonym heap_rep = nat ― ‹representable values›

record heap =
arrays :: "typerep ⇒ addr ⇒ heap_rep list"
refs :: "typerep ⇒ addr ⇒ heap_rep"

definition empty :: heap where
"empty = ⦇arrays = (λ_ _. []), refs = (λ_ _. 0), lim = 0⦈"

datatype 'a array = Array addr ― ‹note the phantom type 'a›
datatype 'a ref = Ref addr ― ‹note the phantom type 'a›

by (cases a, cases a') simp_all

by (cases r, cases r') simp_all

instance array :: (type) countable
by (rule countable_classI [of addr_of_array]) simp

instance ref :: (type) countable
by (rule countable_classI [of addr_of_ref]) simp

instance array :: (type) heap ..
instance ref :: (type) heap ..

text ‹Syntactic convenience›

setup ‹
Sign.add_const_constraint (@{const_name Array}, SOME @{typ "nat ⇒ 'a::heap array"})
#> Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat ⇒ 'a::heap ref"})