remove primitive operation Heap.array in favour of Heap.array_of_list
authorhaftmann
Mon Jul 05 15:25:42 2010 +0200 (2010-07-05 ago)
changeset 3771624bb91462892
parent 37715 44b27ea94a16
child 37717 ede4b8397e01
remove primitive operation Heap.array in favour of Heap.array_of_list
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Heap.thy
src/HOL/Imperative_HOL/Relational.thy
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Mon Jul 05 15:12:20 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Mon Jul 05 15:25:42 2010 +0200
     1.3 @@ -12,11 +12,11 @@
     1.4  
     1.5  definition
     1.6    new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where
     1.7 -  [code del]: "new n x = Heap_Monad.heap (Heap.array n x)"
     1.8 +  [code del]: "new n x = Heap_Monad.heap (Heap.array (replicate n x))"
     1.9  
    1.10  definition
    1.11    of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where
    1.12 -  [code del]: "of_list xs = Heap_Monad.heap (Heap.array_of_list xs)"
    1.13 +  [code del]: "of_list xs = Heap_Monad.heap (Heap.array xs)"
    1.14  
    1.15  definition
    1.16    length :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
    1.17 @@ -93,7 +93,7 @@
    1.18  
    1.19  lemma array_make [code]:
    1.20    "Array.new n x = make n (\<lambda>_. x)"
    1.21 -  by (rule Heap_eqI) (simp add: make_def new_def array_of_list_replicate map_replicate_trivial of_list_def)
    1.22 +  by (rule Heap_eqI) (simp add: make_def new_def map_replicate_trivial of_list_def)
    1.23  
    1.24  lemma array_of_list_make [code]:
    1.25    "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
     2.1 --- a/src/HOL/Imperative_HOL/Heap.thy	Mon Jul 05 15:12:20 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Heap.thy	Mon Jul 05 15:25:42 2010 +0200
     2.3 @@ -136,15 +136,9 @@
     2.4           in (r, h''))"
     2.5  
     2.6  definition
     2.7 -  array :: "nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
     2.8 -  "array n x h = (let (r, h') = new_array h;
     2.9 -                       h'' = set_array r (replicate n x) h'
    2.10 -        in (r, h''))"
    2.11 -
    2.12 -definition
    2.13 -  array_of_list :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
    2.14 -  "array_of_list xs h = (let (r, h') = new_array h;
    2.15 -           h'' = set_array r xs h'
    2.16 +  array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
    2.17 +  "array xs h = (let (r, h') = new_array h;
    2.18 +                      h'' = set_array r xs h'
    2.19          in (r, h''))"  
    2.20  
    2.21  definition
    2.22 @@ -155,11 +149,6 @@
    2.23    length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where
    2.24    "length a h = size (get_array a h)"
    2.25  
    2.26 -definition
    2.27 -  array_ran :: "('a\<Colon>heap) option array \<Rightarrow> heap \<Rightarrow> 'a set" where
    2.28 -  "array_ran a h = {e. Some e \<in> set (get_array a h)}"
    2.29 -    -- {*FIXME*}
    2.30 -
    2.31  
    2.32  subsubsection {* Reference equality *}
    2.33  
    2.34 @@ -189,7 +178,7 @@
    2.35  lemma present_new_ref: "ref_present r h \<Longrightarrow> r =!= fst (ref v h)"
    2.36    by (simp add: ref_present_def new_ref_def ref_def Let_def noteq_refs_def)
    2.37  
    2.38 -lemma present_new_arr: "array_present a h \<Longrightarrow> a =!!= fst (array v x h)"
    2.39 +lemma present_new_arr: "array_present a h \<Longrightarrow> a =!!= fst (array xs h)"
    2.40    by (simp add: array_present_def noteq_arrs_def new_array_def array_def Let_def)
    2.41  
    2.42  
    2.43 @@ -255,22 +244,22 @@
    2.44  by (auto simp add: upd_def array_set_set_swap list_update_swap)
    2.45  
    2.46  lemma get_array_init_array_list:
    2.47 -  "get_array (fst (array_of_list ls h)) (snd (array_of_list ls' h)) = ls'"
    2.48 -  by (simp add: Let_def split_def array_of_list_def)
    2.49 +  "get_array (fst (array ls h)) (snd (array ls' h)) = ls'"
    2.50 +  by (simp add: Let_def split_def array_def)
    2.51  
    2.52  lemma set_array:
    2.53 -  "set_array (fst (array_of_list ls h))
    2.54 -     new_ls (snd (array_of_list ls h))
    2.55 -       = snd (array_of_list new_ls h)"
    2.56 -  by (simp add: Let_def split_def array_of_list_def)
    2.57 +  "set_array (fst (array ls h))
    2.58 +     new_ls (snd (array ls h))
    2.59 +       = snd (array new_ls h)"
    2.60 +  by (simp add: Let_def split_def array_def)
    2.61  
    2.62  lemma array_present_upd [simp]: 
    2.63    "array_present a (upd b i v h) = array_present a h"
    2.64    by (simp add: upd_def array_present_def set_array_def get_array_def)
    2.65  
    2.66 -lemma array_of_list_replicate:
    2.67 +(*lemma array_of_list_replicate:
    2.68    "array_of_list (replicate n x) = array n x"
    2.69 -  by (simp add: expand_fun_eq array_of_list_def array_def)
    2.70 +  by (simp add: expand_fun_eq array_of_list_def array_def)*)
    2.71  
    2.72  text {* Properties of imperative references *}
    2.73  
    2.74 @@ -338,28 +327,6 @@
    2.75    unfolding noteq_refs_def ref_present_def
    2.76    by auto
    2.77  
    2.78 -lemma array_ranI: "\<lbrakk> Some b = get_array a h ! i; i < Heap.length a h \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
    2.79 -unfolding array_ran_def Heap.length_def by simp
    2.80 -
    2.81 -lemma array_ran_upd_array_Some:
    2.82 -  assumes "cl \<in> array_ran a (Heap.upd a i (Some b) h)"
    2.83 -  shows "cl \<in> array_ran a h \<or> cl = b"
    2.84 -proof -
    2.85 -  have "set (get_array a h[i := Some b]) \<subseteq> insert (Some b) (set (get_array a h))" by (rule set_update_subset_insert)
    2.86 -  with assms show ?thesis 
    2.87 -    unfolding array_ran_def Heap.upd_def by fastsimp
    2.88 -qed
    2.89 -
    2.90 -lemma array_ran_upd_array_None:
    2.91 -  assumes "cl \<in> array_ran a (Heap.upd a i None h)"
    2.92 -  shows "cl \<in> array_ran a h"
    2.93 -proof -
    2.94 -  have "set (get_array a h[i := None]) \<subseteq> insert None (set (get_array a h))" by (rule set_update_subset_insert)
    2.95 -  with assms show ?thesis
    2.96 -    unfolding array_ran_def Heap.upd_def by auto
    2.97 -qed
    2.98 -
    2.99 -
   2.100  text {* Non-interaction between imperative array and imperative references *}
   2.101  
   2.102  lemma get_array_set_ref [simp]: "get_array a (set_ref r v h) = get_array a h"
   2.103 @@ -401,6 +368,6 @@
   2.104    "array_present a h \<Longrightarrow> array_present a (snd (ref v h))"
   2.105    by (simp add: array_present_def new_ref_def ref_def Let_def)
   2.106  
   2.107 -hide_const (open) empty array array_of_list upd length ref
   2.108 +hide_const (open) empty upd length array ref
   2.109  
   2.110  end
     3.1 --- a/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 05 15:12:20 2010 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 05 15:25:42 2010 +0200
     3.3 @@ -101,8 +101,8 @@
     3.4  lemma crel_new_weak:
     3.5    assumes "crel (Array.new n v) h h' r"
     3.6    obtains "get_array r h' = List.replicate n v"
     3.7 -  using assms unfolding  Array.new_def
     3.8 -  by (elim crel_heap) (auto simp:Heap.array_def Let_def split_def)
     3.9 +  using assms unfolding Array.new_def
    3.10 +  by (elim crel_heap) (auto simp: array_def Let_def split_def)
    3.11  
    3.12  lemma crel_nth[consumes 1]:
    3.13    assumes "crel (nth a i) h h' r"