src/HOL/Imperative_HOL/Heap.thy
changeset 37714 2eb2b048057b
parent 37678 0040bafffdef
child 37716 24bb91462892
--- a/src/HOL/Imperative_HOL/Heap.thy	Mon Jul 05 14:35:00 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy	Mon Jul 05 15:12:20 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Heap.thy
+(*  Title:      HOL/Imperative_HOL/Heap.thy
     Author:     John Matthews, Galois Connections; Alexander Krauss, TU Muenchen
 *)
 
@@ -14,8 +14,6 @@
 
 class heap = typerep + countable
 
-text {* Instances for common HOL types *}
-
 instance nat :: heap ..
 
 instance prod :: (heap, heap) heap ..
@@ -34,47 +32,23 @@
 
 instance String.literal :: heap ..
 
-text {* Reflected types themselves are heap-representable *}
-
-instantiation typerep :: countable
-begin
-
-fun to_nat_typerep :: "typerep \<Rightarrow> nat" where
-  "to_nat_typerep (Typerep.Typerep c ts) = to_nat (to_nat c, to_nat (map to_nat_typerep ts))"
-
-instance
-proof (rule countable_classI)
-  fix t t' :: typerep and ts
-  have "(\<forall>t'. to_nat_typerep t = to_nat_typerep t' \<longrightarrow> t = t')
-    \<and> (\<forall>ts'. map to_nat_typerep ts = map to_nat_typerep ts' \<longrightarrow> ts = ts')"
-  proof (induct rule: typerep.induct)
-    case (Typerep c ts) show ?case
-    proof (rule allI, rule impI)
-      fix t'
-      assume hyp: "to_nat_typerep (Typerep.Typerep c ts) = to_nat_typerep t'"
-      then obtain c' ts' where t': "t' = (Typerep.Typerep c' ts')"
-        by (cases t') auto
-      with Typerep hyp have "c = c'" and "ts = ts'" by simp_all
-      with t' show "Typerep.Typerep c ts = t'" by simp
-    qed
-  next
-    case Nil_typerep then show ?case by simp
-  next
-    case (Cons_typerep t ts) then show ?case by auto
-  qed
-  then have "to_nat_typerep t = to_nat_typerep t' \<Longrightarrow> t = t'" by auto
-  moreover assume "to_nat_typerep t = to_nat_typerep t'"
-  ultimately show "t = t'" by simp
-qed
-
-end
-
 instance typerep :: heap ..
 
 
 subsection {* A polymorphic heap with dynamic arrays and references *}
 
+subsubsection {* Type definitions *}
+
 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 "
@@ -99,6 +73,8 @@
 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"})
@@ -106,16 +82,6 @@
   #> Sign.add_const_constraint (@{const_name addr_of_ref}, SOME @{typ "'a\<Colon>heap ref \<Rightarrow> nat"})
 *}
 
-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>_. undefined), refs = (\<lambda>_. undefined), lim = 0\<rparr>" -- "why undefined?"
-
 
 subsection {* Imperative references and arrays *}
 
@@ -160,6 +126,7 @@
   "set_array a x = 
   arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))"
 
+
 subsubsection {* Interface operations *}
 
 definition
@@ -305,7 +272,6 @@
   "array_of_list (replicate n x) = array n x"
   by (simp add: expand_fun_eq array_of_list_def array_def)
 
-
 text {* Properties of imperative references *}
 
 lemma next_ref_fresh [simp]: