1.1 --- a/src/HOL/Imperative_HOL/Heap.thy	Mon Jul 05 15:25:42 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap.thy	Mon Jul 05 15:36:37 2010 +0200
     1.3 @@ -93,14 +93,6 @@
     1.4  subsubsection {* Primitive operations *}
     1.5  
     1.6  definition
     1.7 -  new_ref :: "heap \<Rightarrow> ('a\<Colon>heap) ref \<times> heap" where
     1.8 -  "new_ref h = (let l = lim h in (Ref l, h\<lparr>lim := l + 1\<rparr>))"
     1.9 -
    1.10 -definition
    1.11 -  new_array :: "heap \<Rightarrow> ('a\<Colon>heap) array \<times> heap" where
    1.12 -  "new_array h = (let l = lim h in (Array l, h\<lparr>lim := l + 1\<rparr>))"
    1.13 -
    1.14 -definition
    1.15    ref_present :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> bool" where
    1.16    "ref_present r h \<longleftrightarrow> addr_of_ref r < lim h"
    1.17  
    1.18 @@ -126,21 +118,20 @@
    1.19    "set_array a x = 
    1.20    arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))"
    1.21  
    1.22 +definition ref :: "'a \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap ref \<times> heap" where
    1.23 +  "ref x h = (let
    1.24 +     l = lim h;
    1.25 +     r = Ref l;
    1.26 +     h'' = set_ref r x (h\<lparr>lim := l + 1\<rparr>)
    1.27 +   in (r, h''))"
    1.28  
    1.29 -subsubsection {* Interface operations *}
    1.30 -
    1.31 -definition
    1.32 -  ref :: "'a \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap ref \<times> heap" where
    1.33 -  "ref x h = (let (r, h') = new_ref h;
    1.34 -                   h''    = set_ref r x h'
    1.35 -         in (r, h''))"
    1.36 -
    1.37 -definition
    1.38 -  array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
    1.39 -  "array xs h = (let (r, h') = new_array h;
    1.40 -                      h'' = set_array r xs h'
    1.41 -        in (r, h''))"  
    1.42 -
    1.43 +definition array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
    1.44 +  "array xs h = (let
    1.45 +     l = lim h;
    1.46 +     r = Array l;
    1.47 +     h'' = set_array r xs (h\<lparr>lim := l + 1\<rparr>)
    1.48 +   in (r, h''))"
    1.49 +  
    1.50  definition
    1.51    upd :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
    1.52    "upd a i x h = set_array a ((get_array a h)[i:=x]) h"
    1.53 @@ -176,10 +167,10 @@
    1.54    unfolding noteq_refs_def by auto
    1.55  
    1.56  lemma present_new_ref: "ref_present r h \<Longrightarrow> r =!= fst (ref v h)"
    1.57 -  by (simp add: ref_present_def new_ref_def ref_def Let_def noteq_refs_def)
    1.58 +  by (simp add: ref_present_def ref_def Let_def noteq_refs_def)
    1.59  
    1.60  lemma present_new_arr: "array_present a h \<Longrightarrow> a =!!= fst (array xs h)"
    1.61 -  by (simp add: array_present_def noteq_arrs_def new_array_def array_def Let_def)
    1.62 +  by (simp add: array_present_def noteq_arrs_def array_def Let_def)
    1.63  
    1.64  
    1.65  subsubsection {* Properties of heap containers *}
    1.66 @@ -264,14 +255,14 @@
    1.67  text {* Properties of imperative references *}
    1.68  
    1.69  lemma next_ref_fresh [simp]:
    1.70 -  assumes "(r, h') = new_ref h"
    1.71 +  assumes "(r, h') = ref x h"
    1.72    shows "\<not> ref_present r h"
    1.73 -  using assms by (cases h) (auto simp add: new_ref_def ref_present_def Let_def)
    1.74 +  using assms by (cases h) (auto simp add: ref_def ref_present_def Let_def)
    1.75  
    1.76  lemma next_ref_present [simp]:
    1.77 -  assumes "(r, h') = new_ref h"
    1.78 +  assumes "(r, h') = ref x h"
    1.79    shows "ref_present r h'"
    1.80 -  using assms by (cases h) (auto simp add: new_ref_def ref_present_def Let_def)
    1.81 +  using assms by (cases h) (auto simp add: ref_def set_ref_def ref_present_def Let_def)
    1.82  
    1.83  lemma ref_get_set_eq [simp]: "get_ref r (set_ref r x h) = x"
    1.84    by (simp add: get_ref_def set_ref_def)
    1.85 @@ -297,7 +288,7 @@
    1.86    by (simp add: Let_def expand_fun_eq noteq_refs_def set_ref_def)
    1.87  
    1.88  lemma ref_new_set: "fst (ref v (set_ref r v' h)) = fst (ref v h)"
    1.89 -  by (simp add: ref_def new_ref_def set_ref_def Let_def)
    1.90 +  by (simp add: ref_def set_ref_def Let_def)
    1.91  
    1.92  lemma ref_get_new [simp]:
    1.93    "get_ref (fst (ref v h)) (snd (ref v' h)) = v'"
    1.94 @@ -309,7 +300,7 @@
    1.95  
    1.96  lemma ref_get_new_neq: "r =!= (fst (ref v h)) \<Longrightarrow> 
    1.97    get_ref r (snd (ref v h)) = get_ref r h"
    1.98 -  by (simp add: get_ref_def set_ref_def ref_def Let_def new_ref_def noteq_refs_def)
    1.99 +  by (simp add: get_ref_def set_ref_def ref_def Let_def noteq_refs_def)
   1.100  
   1.101  lemma lim_set_ref [simp]:
   1.102    "lim (set_ref r v h) = lim h"
   1.103 @@ -317,7 +308,7 @@
   1.104  
   1.105  lemma ref_present_new_ref [simp]: 
   1.106    "ref_present r h \<Longrightarrow> ref_present r (snd (ref v h))"
   1.107 -  by (simp add: new_ref_def ref_present_def ref_def Let_def)
   1.108 +  by (simp add: ref_present_def ref_def Let_def)
   1.109  
   1.110  lemma ref_present_set_ref [simp]:
   1.111    "ref_present r (set_ref r' v h) = ref_present r h"
   1.112 @@ -339,7 +330,7 @@
   1.113    by (simp add: get_ref_def set_array_def upd_def)
   1.114  
   1.115  lemma new_ref_upd: "fst (ref v (upd a i v' h)) = fst (ref v h)"
   1.116 -  by (simp add: set_array_def get_array_def Let_def ref_new_set upd_def ref_def  new_ref_def)
   1.117 +  by (simp add: set_array_def get_array_def Let_def ref_new_set upd_def ref_def)
   1.118  
   1.119  text {*not actually true ???*}
   1.120  lemma upd_set_ref_swap: "upd a i v (set_ref r v' h) = set_ref r v' (upd a i v h)"
   1.121 @@ -350,11 +341,11 @@
   1.122  
   1.123  lemma length_new_ref[simp]: 
   1.124    "length a (snd (ref v h)) = length a h"
   1.125 -  by (simp add: get_array_def set_ref_def length_def new_ref_def ref_def Let_def)
   1.126 +  by (simp add: get_array_def set_ref_def length_def  ref_def Let_def)
   1.127  
   1.128  lemma get_array_new_ref [simp]: 
   1.129    "get_array a (snd (ref v h)) = get_array a h"
   1.130 -  by (simp add: new_ref_def ref_def set_ref_def get_array_def Let_def)
   1.131 +  by (simp add: ref_def set_ref_def get_array_def Let_def)
   1.132  
   1.133  lemma ref_present_upd [simp]: 
   1.134    "ref_present r (upd a i v h) = ref_present r h"
   1.135 @@ -366,7 +357,7 @@
   1.136  
   1.137  lemma array_present_new_ref [simp]:
   1.138    "array_present a h \<Longrightarrow> array_present a (snd (ref v h))"
   1.139 -  by (simp add: array_present_def new_ref_def ref_def Let_def)
   1.140 +  by (simp add: array_present_def ref_def Let_def)
   1.141  
   1.142  hide_const (open) empty upd length array ref
   1.143  

     2.1 --- a/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 05 15:25:42 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 05 15:36:37 2010 +0200
     2.3 @@ -324,8 +324,6 @@
     2.4    apply (elim crel_heap)
     2.5    unfolding Heap.ref_def
     2.6    apply (simp add: Let_def)
     2.7 -  unfolding Heap.new_ref_def
     2.8 -  apply (simp add: Let_def)
     2.9    unfolding ref_present_def
    2.10    apply auto
    2.11    unfolding get_ref_def set_ref_def