1.1 --- a/src/HOL/Imperative_HOL/Heap.thy	Mon Jul 05 14:35:00 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap.thy	Mon Jul 05 15:12:20 2010 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/Library/Heap.thy
     1.5 +(*  Title:      HOL/Imperative_HOL/Heap.thy
     1.6      Author:     John Matthews, Galois Connections; Alexander Krauss, TU Muenchen
     1.7  *)
     1.8  
     1.9 @@ -14,8 +14,6 @@
    1.10  
    1.11  class heap = typerep + countable
    1.12  
    1.13 -text {* Instances for common HOL types *}
    1.14 -
    1.15  instance nat :: heap ..
    1.16  
    1.17  instance prod :: (heap, heap) heap ..
    1.18 @@ -34,47 +32,23 @@
    1.19  
    1.20  instance String.literal :: heap ..
    1.21  
    1.22 -text {* Reflected types themselves are heap-representable *}
    1.23 -
    1.24 -instantiation typerep :: countable
    1.25 -begin
    1.26 -
    1.27 -fun to_nat_typerep :: "typerep \<Rightarrow> nat" where
    1.28 -  "to_nat_typerep (Typerep.Typerep c ts) = to_nat (to_nat c, to_nat (map to_nat_typerep ts))"
    1.29 -
    1.30 -instance
    1.31 -proof (rule countable_classI)
    1.32 -  fix t t' :: typerep and ts
    1.33 -  have "(\<forall>t'. to_nat_typerep t = to_nat_typerep t' \<longrightarrow> t = t')
    1.34 -    \<and> (\<forall>ts'. map to_nat_typerep ts = map to_nat_typerep ts' \<longrightarrow> ts = ts')"
    1.35 -  proof (induct rule: typerep.induct)
    1.36 -    case (Typerep c ts) show ?case
    1.37 -    proof (rule allI, rule impI)
    1.38 -      fix t'
    1.39 -      assume hyp: "to_nat_typerep (Typerep.Typerep c ts) = to_nat_typerep t'"
    1.40 -      then obtain c' ts' where t': "t' = (Typerep.Typerep c' ts')"
    1.41 -        by (cases t') auto
    1.42 -      with Typerep hyp have "c = c'" and "ts = ts'" by simp_all
    1.43 -      with t' show "Typerep.Typerep c ts = t'" by simp
    1.44 -    qed
    1.45 -  next
    1.46 -    case Nil_typerep then show ?case by simp
    1.47 -  next
    1.48 -    case (Cons_typerep t ts) then show ?case by auto
    1.49 -  qed
    1.50 -  then have "to_nat_typerep t = to_nat_typerep t' \<Longrightarrow> t = t'" by auto
    1.51 -  moreover assume "to_nat_typerep t = to_nat_typerep t'"
    1.52 -  ultimately show "t = t'" by simp
    1.53 -qed
    1.54 -
    1.55 -end
    1.56 -
    1.57  instance typerep :: heap ..
    1.58  
    1.59  
    1.60  subsection {* A polymorphic heap with dynamic arrays and references *}
    1.61  
    1.62 +subsubsection {* Type definitions *}
    1.63 +
    1.64  types addr = nat -- "untyped heap references"
    1.65 +types heap_rep = nat -- "representable values"
    1.66 +
    1.67 +record heap =
    1.68 +  arrays :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep list"
    1.69 +  refs :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep"
    1.70 +  lim  :: addr
    1.71 +
    1.72 +definition empty :: heap where
    1.73 +  "empty = \<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 0\<rparr>" -- "why undefined?"
    1.74  
    1.75  datatype 'a array = Array addr
    1.76  datatype 'a ref = Ref addr -- "note the phantom type 'a "
    1.77 @@ -99,6 +73,8 @@
    1.78  instance ref :: (type) countable
    1.79    by (rule countable_classI [of addr_of_ref]) simp
    1.80  
    1.81 +text {* Syntactic convenience *}
    1.82 +
    1.83  setup {*
    1.84    Sign.add_const_constraint (@{const_name Array}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>heap array"})
    1.85    #> Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>heap ref"})
    1.86 @@ -106,16 +82,6 @@
    1.87    #> Sign.add_const_constraint (@{const_name addr_of_ref}, SOME @{typ "'a\<Colon>heap ref \<Rightarrow> nat"})
    1.88  *}
    1.89  
    1.90 -types heap_rep = nat -- "representable values"
    1.91 -
    1.92 -record heap =
    1.93 -  arrays :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep list"
    1.94 -  refs :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep"
    1.95 -  lim  :: addr
    1.96 -
    1.97 -definition empty :: heap where
    1.98 -  "empty = \<lparr>arrays = (\<lambda>_. undefined), refs = (\<lambda>_. undefined), lim = 0\<rparr>" -- "why undefined?"
    1.99 -
   1.100  
   1.101  subsection {* Imperative references and arrays *}
   1.102  
   1.103 @@ -160,6 +126,7 @@
   1.104    "set_array a x = 
   1.105    arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))"
   1.106  
   1.107 +
   1.108  subsubsection {* Interface operations *}
   1.109  
   1.110  definition
   1.111 @@ -305,7 +272,6 @@
   1.112    "array_of_list (replicate n x) = array n x"
   1.113    by (simp add: expand_fun_eq array_of_list_def array_def)
   1.114  
   1.115 -
   1.116  text {* Properties of imperative references *}
   1.117  
   1.118  lemma next_ref_fresh [simp]: