src/HOL/Imperative_HOL/Heap.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 39250 548a3e5521ab
child 42463 f270e3e18be5
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
     1 (*  Title:      HOL/Imperative_HOL/Heap.thy
     2     Author:     John Matthews, Galois Connections; Alexander Krauss, TU Muenchen
     3 *)
     4 
     5 header {* A polymorphic heap based on cantor encodings *}
     6 
     7 theory Heap
     8 imports Main "~~/src/HOL/Library/Countable"
     9 begin
    10 
    11 subsection {* Representable types *}
    12 
    13 text {* The type class of representable types *}
    14 
    15 class heap = typerep + countable
    16 
    17 instance unit :: heap ..
    18 
    19 instance bool :: heap ..
    20 
    21 instance nat :: heap ..
    22 
    23 instance prod :: (heap, heap) heap ..
    24 
    25 instance sum :: (heap, heap) heap ..
    26 
    27 instance list :: (heap) heap ..
    28 
    29 instance option :: (heap) heap ..
    30 
    31 instance int :: heap ..
    32 
    33 instance String.literal :: heap ..
    34 
    35 instance typerep :: heap ..
    36 
    37 
    38 subsection {* A polymorphic heap with dynamic arrays and references *}
    39 
    40 text {*
    41   References and arrays are developed in parallel,
    42   but keeping them separate makes some later proofs simpler.
    43 *}
    44 
    45 types addr = nat -- "untyped heap references"
    46 types heap_rep = nat -- "representable values"
    47 
    48 record heap =
    49   arrays :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep list"
    50   refs :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep"
    51   lim  :: addr
    52 
    53 definition empty :: heap where
    54   "empty = \<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 0\<rparr>"
    55 
    56 datatype 'a array = Array addr
    57 datatype 'a ref = Ref addr -- "note the phantom type 'a "
    58 
    59 primrec addr_of_array :: "'a array \<Rightarrow> addr" where
    60   "addr_of_array (Array x) = x"
    61 
    62 primrec addr_of_ref :: "'a ref \<Rightarrow> addr" where
    63   "addr_of_ref (Ref x) = x"
    64 
    65 lemma addr_of_array_inj [simp]:
    66   "addr_of_array a = addr_of_array a' \<longleftrightarrow> a = a'"
    67   by (cases a, cases a') simp_all
    68 
    69 lemma addr_of_ref_inj [simp]:
    70   "addr_of_ref r = addr_of_ref r' \<longleftrightarrow> r = r'"
    71   by (cases r, cases r') simp_all
    72 
    73 instance array :: (type) countable
    74   by (rule countable_classI [of addr_of_array]) simp
    75 
    76 instance ref :: (type) countable
    77   by (rule countable_classI [of addr_of_ref]) simp
    78 
    79 text {* Syntactic convenience *}
    80 
    81 setup {*
    82   Sign.add_const_constraint (@{const_name Array}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>heap array"})
    83   #> Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>heap ref"})
    84   #> Sign.add_const_constraint (@{const_name addr_of_array}, SOME @{typ "'a\<Colon>heap array \<Rightarrow> nat"})
    85   #> Sign.add_const_constraint (@{const_name addr_of_ref}, SOME @{typ "'a\<Colon>heap ref \<Rightarrow> nat"})
    86 *}
    87 
    88 hide_const (open) empty
    89 
    90 end