|
(* Title: HOL/Imperative_HOL/Heap.thy
Author: John Matthews, Galois Connections; Alexander Krauss, TU Muenchen
*)
section \<open>A polymorphic heap based on cantor encodings\<close>
theory Heap
imports Main "HOL-Library.Countable"
begin
subsection \<open>Representable types\<close>
text \<open>The type class of representable types\<close>
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 \<open>A polymorphic heap with dynamic arrays and references\<close>
text \<open>
References and arrays are developed in parallel,
but keeping them separate makes some later proofs simpler.
\<close>
type_synonym addr = nat \<comment> \<open>untyped heap references\<close>
type_synonym heap_rep = nat \<comment> \<open>representable values\<close>
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\"
datatype 'a array = Array addr \ \note the phantom type 'a\
datatype 'a ref = Ref addr \ \note the phantom type 'a\
primrec addr_of_array :: "'a array \ addr" where
"addr_of_array (Array x) = x"
primrec addr_of_ref :: "'a ref \ addr" where
"addr_of_ref (Ref x) = x"
lemma addr_of_array_inj [simp]:
"addr_of_array a = addr_of_array a' \ a = a'"
by (cases a, cases a') simp_all
lemma addr_of_ref_inj [simp]:
"addr_of_ref r = addr_of_ref r' \ 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
instance array :: (type) heap ..
instance ref :: (type) heap ..
text \<open>Syntactic convenience\<close>
setup \<open>
Sign.add_const_constraint (\<^const_name>\<open>Array\<close>, SOME \<^typ>\<open>nat \<Rightarrow> 'a::heap array\<close>)
#> Sign.add_const_constraint (\<^const_name>\<open>Ref\<close>, SOME \<^typ>\<open>nat \<Rightarrow> 'a::heap ref\<close>)
#> Sign.add_const_constraint (\<^const_name>\<open>addr_of_array\<close>, SOME \<^typ>\<open>'a::heap array \<Rightarrow> nat\<close>)
#> Sign.add_const_constraint (\<^const_name>\<open>addr_of_ref\<close>, SOME \<^typ>\<open>'a::heap ref \<Rightarrow> nat\<close>)
\<close>
hide_const (open) empty
end
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
