src/HOL/Imperative_HOL/Array.thy
changeset 29399 ebcd69a00872
parent 28562 4e74209f113e
child 29793 86cac1fab613
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Thu Jan 08 17:10:41 2009 +0100
     1.3 @@ -0,0 +1,209 @@
     1.4 +(*  Title:      HOL/Library/Array.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +header {* Monadic arrays *}
    1.10 +
    1.11 +theory Array
    1.12 +imports Heap_Monad Code_Index
    1.13 +begin
    1.14 +
    1.15 +subsection {* Primitives *}
    1.16 +
    1.17 +definition
    1.18 +  new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where
    1.19 +  [code del]: "new n x = Heap_Monad.heap (Heap.array n x)"
    1.20 +
    1.21 +definition
    1.22 +  of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where
    1.23 +  [code del]: "of_list xs = Heap_Monad.heap (Heap.array_of_list xs)"
    1.24 +
    1.25 +definition
    1.26 +  length :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
    1.27 +  [code del]: "length arr = Heap_Monad.heap (\<lambda>h. (Heap.length arr h, h))"
    1.28 +
    1.29 +definition
    1.30 +  nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap"
    1.31 +where
    1.32 +  [code del]: "nth a i = (do len \<leftarrow> length a;
    1.33 +                 (if i < len
    1.34 +                     then Heap_Monad.heap (\<lambda>h. (get_array a h ! i, h))
    1.35 +                     else raise (''array lookup: index out of range''))
    1.36 +              done)"
    1.37 +
    1.38 +-- {* FIXME adjustion for List theory *}
    1.39 +no_syntax
    1.40 +  nth  :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!" 100)
    1.41 +
    1.42 +abbreviation
    1.43 +  nth_list :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!" 100)
    1.44 +where
    1.45 +  "nth_list \<equiv> List.nth"
    1.46 +
    1.47 +definition
    1.48 +  upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap"
    1.49 +where
    1.50 +  [code del]: "upd i x a = (do len \<leftarrow> length a;
    1.51 +                      (if i < len
    1.52 +                           then Heap_Monad.heap (\<lambda>h. (a, Heap.upd a i x h))
    1.53 +                           else raise (''array update: index out of range''))
    1.54 +                   done)" 
    1.55 +
    1.56 +lemma upd_return:
    1.57 +  "upd i x a \<guillemotright> return a = upd i x a"
    1.58 +proof (rule Heap_eqI)
    1.59 +  fix h
    1.60 +  obtain len h' where "Heap_Monad.execute (Array.length a) h = (len, h')"
    1.61 +    by (cases "Heap_Monad.execute (Array.length a) h")
    1.62 +  then show "Heap_Monad.execute (upd i x a \<guillemotright> return a) h = Heap_Monad.execute (upd i x a) h"
    1.63 +    by (auto simp add: upd_def bindM_def split: sum.split)
    1.64 +qed
    1.65 +
    1.66 +
    1.67 +subsection {* Derivates *}
    1.68 +
    1.69 +definition
    1.70 +  map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap"
    1.71 +where
    1.72 +  "map_entry i f a = (do
    1.73 +     x \<leftarrow> nth a i;
    1.74 +     upd i (f x) a
    1.75 +   done)"
    1.76 +
    1.77 +definition
    1.78 +  swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap"
    1.79 +where
    1.80 +  "swap i x a = (do
    1.81 +     y \<leftarrow> nth a i;
    1.82 +     upd i x a;
    1.83 +     return y
    1.84 +   done)"
    1.85 +
    1.86 +definition
    1.87 +  make :: "nat \<Rightarrow> (nat \<Rightarrow> 'a\<Colon>heap) \<Rightarrow> 'a array Heap"
    1.88 +where
    1.89 +  "make n f = of_list (map f [0 ..< n])"
    1.90 +
    1.91 +definition
    1.92 +  freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap"
    1.93 +where
    1.94 +  "freeze a = (do
    1.95 +     n \<leftarrow> length a;
    1.96 +     mapM (nth a) [0..<n]
    1.97 +   done)"
    1.98 +
    1.99 +definition
   1.100 +   map :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap"
   1.101 +where
   1.102 +  "map f a = (do
   1.103 +     n \<leftarrow> length a;
   1.104 +     mapM (\<lambda>n. map_entry n f a) [0..<n];
   1.105 +     return a
   1.106 +   done)"
   1.107 +
   1.108 +hide (open) const new map -- {* avoid clashed with some popular names *}
   1.109 +
   1.110 +
   1.111 +subsection {* Properties *}
   1.112 +
   1.113 +lemma array_make [code]:
   1.114 +  "Array.new n x = make n (\<lambda>_. x)"
   1.115 +  by (induct n) (simp_all add: make_def new_def Heap_Monad.heap_def
   1.116 +    monad_simp array_of_list_replicate [symmetric]
   1.117 +    map_replicate_trivial replicate_append_same
   1.118 +    of_list_def)
   1.119 +
   1.120 +lemma array_of_list_make [code]:
   1.121 +  "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
   1.122 +  unfolding make_def map_nth ..
   1.123 +
   1.124 +
   1.125 +subsection {* Code generator setup *}
   1.126 +
   1.127 +subsubsection {* Logical intermediate layer *}
   1.128 +
   1.129 +definition new' where
   1.130 +  [code del]: "new' = Array.new o nat_of_index"
   1.131 +hide (open) const new'
   1.132 +lemma [code]:
   1.133 +  "Array.new = Array.new' o index_of_nat"
   1.134 +  by (simp add: new'_def o_def)
   1.135 +
   1.136 +definition of_list' where
   1.137 +  [code del]: "of_list' i xs = Array.of_list (take (nat_of_index i) xs)"
   1.138 +hide (open) const of_list'
   1.139 +lemma [code]:
   1.140 +  "Array.of_list xs = Array.of_list' (index_of_nat (List.length xs)) xs"
   1.141 +  by (simp add: of_list'_def)
   1.142 +
   1.143 +definition make' where
   1.144 +  [code del]: "make' i f = Array.make (nat_of_index i) (f o index_of_nat)"
   1.145 +hide (open) const make'
   1.146 +lemma [code]:
   1.147 +  "Array.make n f = Array.make' (index_of_nat n) (f o nat_of_index)"
   1.148 +  by (simp add: make'_def o_def)
   1.149 +
   1.150 +definition length' where
   1.151 +  [code del]: "length' = Array.length \<guillemotright>== liftM index_of_nat"
   1.152 +hide (open) const length'
   1.153 +lemma [code]:
   1.154 +  "Array.length = Array.length' \<guillemotright>== liftM nat_of_index"
   1.155 +  by (simp add: length'_def monad_simp',
   1.156 +    simp add: liftM_def comp_def monad_simp,
   1.157 +    simp add: monad_simp')
   1.158 +
   1.159 +definition nth' where
   1.160 +  [code del]: "nth' a = Array.nth a o nat_of_index"
   1.161 +hide (open) const nth'
   1.162 +lemma [code]:
   1.163 +  "Array.nth a n = Array.nth' a (index_of_nat n)"
   1.164 +  by (simp add: nth'_def)
   1.165 +
   1.166 +definition upd' where
   1.167 +  [code del]: "upd' a i x = Array.upd (nat_of_index i) x a \<guillemotright> return ()"
   1.168 +hide (open) const upd'
   1.169 +lemma [code]:
   1.170 +  "Array.upd i x a = Array.upd' a (index_of_nat i) x \<guillemotright> return a"
   1.171 +  by (simp add: upd'_def monad_simp upd_return)
   1.172 +
   1.173 +
   1.174 +subsubsection {* SML *}
   1.175 +
   1.176 +code_type array (SML "_/ array")
   1.177 +code_const Array (SML "raise/ (Fail/ \"bare Array\")")
   1.178 +code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))")
   1.179 +code_const Array.of_list (SML "(fn/ ()/ =>/ Array.fromList/ _)")
   1.180 +code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))")
   1.181 +code_const Array.length' (SML "(fn/ ()/ =>/ Array.length/ _)")
   1.182 +code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))")
   1.183 +code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))")
   1.184 +
   1.185 +code_reserved SML Array
   1.186 +
   1.187 +
   1.188 +subsubsection {* OCaml *}
   1.189 +
   1.190 +code_type array (OCaml "_/ array")
   1.191 +code_const Array (OCaml "failwith/ \"bare Array\"")
   1.192 +code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ _/ _)")
   1.193 +code_const Array.of_list (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
   1.194 +code_const Array.make' (OCaml "(fun/ ()/ ->/ Array.init/ _/ _)")
   1.195 +code_const Array.length' (OCaml "(fun/ ()/ ->/ Array.length/ _)")
   1.196 +code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ _)")
   1.197 +code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ _/ _)")
   1.198 +
   1.199 +code_reserved OCaml Array
   1.200 +
   1.201 +
   1.202 +subsubsection {* Haskell *}
   1.203 +
   1.204 +code_type array (Haskell "STArray/ RealWorld/ _")
   1.205 +code_const Array (Haskell "error/ \"bare Array\"")
   1.206 +code_const Array.new' (Haskell "newArray/ (0,/ _)")
   1.207 +code_const Array.of_list' (Haskell "newListArray/ (0,/ _)")
   1.208 +code_const Array.length' (Haskell "lengthArray")
   1.209 +code_const Array.nth' (Haskell "readArray")
   1.210 +code_const Array.upd' (Haskell "writeArray")
   1.211 +
   1.212 +end