(*  Title:      HOL/Imperative_HOL/Heap.thy

    Author:     John Matthews, Galois Connections; Alexander Krauss, TU Muenchen

*)

header {* A polymorphic heap based on cantor encodings *}

theory Heap

imports Main Countable

begin

subsection {* Representable types *}

text {* The type class of representable types *}

class heap = typerep + countable

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 :: countable

  by (rule countable_classI [of "String.literal_case to_nat"])

   (auto split: String.literal.splits)

instance String.literal :: 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.

*}

types addr = nat -- "untyped heap references"

types heap_rep = nat -- "representable values"

record heap =

  arrays :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep list"

  refs :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep"

  lim  :: addr

definition empty :: heap where

  "empty = \<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 0\<rparr>" -- "why undefined?"

datatype 'a array = Array addr

datatype 'a ref = Ref addr -- "note the phantom type 'a "

primrec addr_of_array :: "'a array \<Rightarrow> addr" where

  "addr_of_array (Array x) = x"

primrec addr_of_ref :: "'a ref \<Rightarrow> addr" where

  "addr_of_ref (Ref x) = x"

lemma addr_of_array_inj [simp]:

  "addr_of_array a = addr_of_array a' \<longleftrightarrow> a = a'"

  by (cases a, cases a') simp_all

lemma addr_of_ref_inj [simp]:

  "addr_of_ref r = addr_of_ref r' \<longleftrightarrow> r = r'"

  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

text {* Syntactic convenience *}

setup {*

  Sign.add_const_constraint (@{const_name Array}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>heap array"})

  #> Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>heap ref"})

  #> Sign.add_const_constraint (@{const_name addr_of_array}, SOME @{typ "'a\<Colon>heap array \<Rightarrow> nat"})

  #> Sign.add_const_constraint (@{const_name addr_of_ref}, SOME @{typ "'a\<Colon>heap ref \<Rightarrow> nat"})

*}

end