src/HOL/Imperative_HOL/Array.thy
changeset 37719 271ecd4fb9f9
parent 37716 24bb91462892
child 37752 d0a384c84d69
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Mon Jul 05 15:36:37 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Mon Jul 05 16:46:23 2010 +0200
     1.3 @@ -8,24 +8,132 @@
     1.4  imports Heap_Monad
     1.5  begin
     1.6  
     1.7 +subsection {* Primitive layer *}
     1.8 +
     1.9 +definition 
    1.10 +  array_present :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> bool" where
    1.11 +  "array_present a h \<longleftrightarrow> addr_of_array a < lim h"
    1.12 +
    1.13 +definition
    1.14 +  get_array :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> 'a list" where
    1.15 +  "get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))"
    1.16 +
    1.17 +definition
    1.18 +  set_array :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where
    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 array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
    1.23 +  "array xs h = (let
    1.24 +     l = lim h;
    1.25 +     r = Array l;
    1.26 +     h'' = set_array r xs (h\<lparr>lim := l + 1\<rparr>)
    1.27 +   in (r, h''))"
    1.28 +
    1.29 +definition length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where
    1.30 +  "length a h = List.length (get_array a h)"
    1.31 +  
    1.32 +definition change :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
    1.33 +  "change a i x h = set_array a ((get_array a h)[i:=x]) h"
    1.34 +
    1.35 +text {* Properties of imperative arrays *}
    1.36 +
    1.37 +text {* FIXME: Does there exist a "canonical" array axiomatisation in
    1.38 +the literature?  *}
    1.39 +
    1.40 +definition noteq_arrs :: "('a\<Colon>heap) array \<Rightarrow> ('b\<Colon>heap) array \<Rightarrow> bool" (infix "=!!=" 70) where
    1.41 +  "r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s"
    1.42 +
    1.43 +lemma noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a"
    1.44 +  and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
    1.45 +  unfolding noteq_arrs_def by auto
    1.46 +
    1.47 +lemma noteq_arrs_irrefl: "r =!!= r \<Longrightarrow> False"
    1.48 +  unfolding noteq_arrs_def by auto
    1.49 +
    1.50 +lemma present_new_arr: "array_present a h \<Longrightarrow> a =!!= fst (array xs h)"
    1.51 +  by (simp add: array_present_def noteq_arrs_def array_def Let_def)
    1.52 +
    1.53 +lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x"
    1.54 +  by (simp add: get_array_def set_array_def o_def)
    1.55 +
    1.56 +lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h"
    1.57 +  by (simp add: noteq_arrs_def get_array_def set_array_def)
    1.58 +
    1.59 +lemma set_array_same [simp]:
    1.60 +  "set_array r x (set_array r y h) = set_array r x h"
    1.61 +  by (simp add: set_array_def)
    1.62 +
    1.63 +lemma array_set_set_swap:
    1.64 +  "r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)"
    1.65 +  by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def)
    1.66 +
    1.67 +lemma get_array_change_eq [simp]:
    1.68 +  "get_array a (change a i v h) = (get_array a h) [i := v]"
    1.69 +  by (simp add: change_def)
    1.70 +
    1.71 +lemma nth_change_array_neq_array [simp]:
    1.72 +  "a =!!= b \<Longrightarrow> get_array a (change b j v h) ! i = get_array a h ! i"
    1.73 +  by (simp add: change_def noteq_arrs_def)
    1.74 +
    1.75 +lemma get_arry_array_change_elem_neqIndex [simp]:
    1.76 +  "i \<noteq> j \<Longrightarrow> get_array a (change a j v h) ! i = get_array a h ! i"
    1.77 +  by simp
    1.78 +
    1.79 +lemma length_change [simp]: 
    1.80 +  "length a (change b i v h) = length a h"
    1.81 +  by (simp add: change_def length_def set_array_def get_array_def)
    1.82 +
    1.83 +lemma change_swap_neqArray:
    1.84 +  "a =!!= a' \<Longrightarrow> 
    1.85 +  change a i v (change a' i' v' h) 
    1.86 +  = change a' i' v' (change a i v h)"
    1.87 +apply (unfold change_def)
    1.88 +apply simp
    1.89 +apply (subst array_set_set_swap, assumption)
    1.90 +apply (subst array_get_set_neq)
    1.91 +apply (erule noteq_arrs_sym)
    1.92 +apply (simp)
    1.93 +done
    1.94 +
    1.95 +lemma change_swap_neqIndex:
    1.96 +  "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> change a i v (change a i' v' h) = change a i' v' (change a i v h)"
    1.97 +  by (auto simp add: change_def array_set_set_swap list_update_swap)
    1.98 +
    1.99 +lemma get_array_init_array_list:
   1.100 +  "get_array (fst (array ls h)) (snd (array ls' h)) = ls'"
   1.101 +  by (simp add: Let_def split_def array_def)
   1.102 +
   1.103 +lemma set_array:
   1.104 +  "set_array (fst (array ls h))
   1.105 +     new_ls (snd (array ls h))
   1.106 +       = snd (array new_ls h)"
   1.107 +  by (simp add: Let_def split_def array_def)
   1.108 +
   1.109 +lemma array_present_change [simp]: 
   1.110 +  "array_present a (change b i v h) = array_present a h"
   1.111 +  by (simp add: change_def array_present_def set_array_def get_array_def)
   1.112 +
   1.113 +
   1.114 +
   1.115  subsection {* Primitives *}
   1.116  
   1.117  definition
   1.118    new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where
   1.119 -  [code del]: "new n x = Heap_Monad.heap (Heap.array (replicate n x))"
   1.120 +  [code del]: "new n x = Heap_Monad.heap (Array.array (replicate n x))"
   1.121  
   1.122  definition
   1.123    of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where
   1.124 -  [code del]: "of_list xs = Heap_Monad.heap (Heap.array xs)"
   1.125 +  [code del]: "of_list xs = Heap_Monad.heap (Array.array xs)"
   1.126  
   1.127  definition
   1.128 -  length :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
   1.129 -  [code del]: "length arr = Heap_Monad.heap (\<lambda>h. (Heap.length arr h, h))"
   1.130 +  len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
   1.131 +  [code del]: "len arr = Heap_Monad.heap (\<lambda>h. (Array.length arr h, h))"
   1.132  
   1.133  definition
   1.134    nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap"
   1.135  where
   1.136 -  [code del]: "nth a i = (do len \<leftarrow> length a;
   1.137 +  [code del]: "nth a i = (do len \<leftarrow> len a;
   1.138                   (if i < len
   1.139                       then Heap_Monad.heap (\<lambda>h. (get_array a h ! i, h))
   1.140                       else raise ''array lookup: index out of range'')
   1.141 @@ -34,9 +142,9 @@
   1.142  definition
   1.143    upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap"
   1.144  where
   1.145 -  [code del]: "upd i x a = (do len \<leftarrow> length a;
   1.146 +  [code del]: "upd i x a = (do len \<leftarrow> len a;
   1.147                        (if i < len
   1.148 -                           then Heap_Monad.heap (\<lambda>h. (a, Heap.upd a i x h))
   1.149 +                           then Heap_Monad.heap (\<lambda>h. (a, change a i x h))
   1.150                             else raise ''array update: index out of range'')
   1.151                     done)" 
   1.152  
   1.153 @@ -73,7 +181,7 @@
   1.154    freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap"
   1.155  where
   1.156    "freeze a = (do
   1.157 -     n \<leftarrow> length a;
   1.158 +     n \<leftarrow> len a;
   1.159       mapM (nth a) [0..<n]
   1.160     done)"
   1.161  
   1.162 @@ -81,12 +189,11 @@
   1.163     map :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap"
   1.164  where
   1.165    "map f a = (do
   1.166 -     n \<leftarrow> length a;
   1.167 +     n \<leftarrow> len a;
   1.168       mapM (\<lambda>n. map_entry n f a) [0..<n];
   1.169       return a
   1.170     done)"
   1.171  
   1.172 -hide_const (open) new map -- {* avoid clashed with some popular names *}
   1.173  
   1.174  
   1.175  subsection {* Properties *}
   1.176 @@ -125,12 +232,12 @@
   1.177    "Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)"
   1.178    by (simp add: make'_def o_def)
   1.179  
   1.180 -definition length' where
   1.181 -  [code del]: "length' a = Array.length a \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))"
   1.182 -hide_const (open) length'
   1.183 +definition len' where
   1.184 +  [code del]: "len' a = Array.len a \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))"
   1.185 +hide_const (open) len'
   1.186  lemma [code]:
   1.187 -  "Array.length a = Array.length' a \<guillemotright>= (\<lambda>i. return (Code_Numeral.nat_of i))"
   1.188 -  by (simp add: length'_def)
   1.189 +  "Array.len a = Array.len' a \<guillemotright>= (\<lambda>i. return (Code_Numeral.nat_of i))"
   1.190 +  by (simp add: len'_def)
   1.191  
   1.192  definition nth' where
   1.193    [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of"
   1.194 @@ -154,7 +261,7 @@
   1.195  code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))")
   1.196  code_const Array.of_list' (SML "(fn/ ()/ =>/ Array.fromList/ _)")
   1.197  code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))")
   1.198 -code_const Array.length' (SML "(fn/ ()/ =>/ Array.length/ _)")
   1.199 +code_const Array.len' (SML "(fn/ ()/ =>/ Array.length/ _)")
   1.200  code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))")
   1.201  code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))")
   1.202  
   1.203 @@ -167,7 +274,7 @@
   1.204  code_const Array (OCaml "failwith/ \"bare Array\"")
   1.205  code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)")
   1.206  code_const Array.of_list' (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
   1.207 -code_const Array.length' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
   1.208 +code_const Array.len' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
   1.209  code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))")
   1.210  code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)")
   1.211  
   1.212 @@ -180,8 +287,10 @@
   1.213  code_const Array (Haskell "error/ \"bare Array\"")
   1.214  code_const Array.new' (Haskell "Heap.newArray/ (0,/ _)")
   1.215  code_const Array.of_list' (Haskell "Heap.newListArray/ (0,/ _)")
   1.216 -code_const Array.length' (Haskell "Heap.lengthArray")
   1.217 +code_const Array.len' (Haskell "Heap.lengthArray")
   1.218  code_const Array.nth' (Haskell "Heap.readArray")
   1.219  code_const Array.upd' (Haskell "Heap.writeArray")
   1.220  
   1.221 +hide_const (open) new map -- {* avoid clashed with some popular names *}
   1.222 +
   1.223  end