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