src/HOL/Library/Array.thy
changeset 26170 66e6b967ccf1
child 26182 8262ec0e8782
equal deleted inserted replaced
26169:73027318f9ba 26170:66e6b967ccf1
       
     1 (*  Title:      HOL/Library/Array.thy
       
     2     ID:         $Id$
       
     3     Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
       
     4 *)
       
     5 
       
     6 header {* Monadic arrays *}
       
     7 
       
     8 theory Array
       
     9 imports Heap_Monad
       
    10 begin
       
    11 
       
    12 subsection {* Primitives *}
       
    13 
       
    14 definition
       
    15   new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where
       
    16   [code del]: "new n x = Heap_Monad.heap (Heap.array n x)"
       
    17 
       
    18 definition
       
    19   of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where
       
    20   [code del]: "of_list xs = Heap_Monad.heap (Heap.array_of_list xs)"
       
    21 
       
    22 definition
       
    23   length :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
       
    24   [code del]: "length arr = Heap_Monad.heap (\<lambda>h. (Heap.length arr h, h))"
       
    25 
       
    26 definition
       
    27   nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap"
       
    28 where
       
    29   [code del]: "nth a i = (do len \<leftarrow> length a;
       
    30                  (if i < len
       
    31                      then Heap_Monad.heap (\<lambda>h. (get_array a h ! i, h))
       
    32                      else raise (''array lookup: index out of range''))
       
    33               done)"
       
    34 
       
    35 -- {* FIXME adjustion for List theory *}
       
    36 no_syntax
       
    37   nth  :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!" 100)
       
    38 
       
    39 abbreviation
       
    40   nth_list :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!" 100)
       
    41 where
       
    42   "nth_list \<equiv> List.nth"
       
    43 
       
    44 definition
       
    45   upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap"
       
    46 where
       
    47   [code del]: "upd i x a = (do len \<leftarrow> length a;
       
    48                       (if i < len
       
    49                            then Heap_Monad.heap (\<lambda>h. ((), Heap.upd a i x h))
       
    50                            else raise (''array update: index out of range''));
       
    51                       return a
       
    52                    done)" 
       
    53 
       
    54 lemma upd_return:
       
    55   "upd i x a \<guillemotright> return a = upd i x a"
       
    56   unfolding upd_def by (simp add: monad_simp)
       
    57 
       
    58 
       
    59 subsection {* Derivates *}
       
    60 
       
    61 definition
       
    62   map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap"
       
    63 where
       
    64   "map_entry i f a = (do
       
    65      x \<leftarrow> nth a i;
       
    66      upd i (f x) a
       
    67    done)"
       
    68 
       
    69 definition
       
    70   swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap"
       
    71 where
       
    72   "swap i x a = (do
       
    73      y \<leftarrow> nth a i;
       
    74      upd i x a;
       
    75      return x
       
    76    done)"
       
    77 
       
    78 definition
       
    79   make :: "nat \<Rightarrow> (nat \<Rightarrow> 'a\<Colon>heap) \<Rightarrow> 'a array Heap"
       
    80 where
       
    81   "make n f = of_list (map f [0 ..< n])"
       
    82 
       
    83 definition
       
    84   freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap"
       
    85 where
       
    86   "freeze a = (do
       
    87      n \<leftarrow> length a;
       
    88      mapM (nth a) [0..<n]
       
    89    done)"
       
    90 
       
    91 definition
       
    92   map :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap"
       
    93 where
       
    94   "map f a = (do
       
    95      n \<leftarrow> length a;
       
    96      foldM (\<lambda>n. map_entry n f) [0..<n] a
       
    97    done)"
       
    98 
       
    99 hide (open) const new map -- {* avoid clashed with some popular names *}
       
   100 
       
   101 
       
   102 subsection {* Converting arrays to lists *}
       
   103 
       
   104 primrec list_of_aux :: "nat \<Rightarrow> ('a\<Colon>heap) array \<Rightarrow> 'a list \<Rightarrow> 'a list Heap" where
       
   105   "list_of_aux 0 a xs = return xs"
       
   106   | "list_of_aux (Suc n) a xs = (do
       
   107         x \<leftarrow> Array.nth a n;
       
   108         list_of_aux n a (x#xs)
       
   109      done)"
       
   110 
       
   111 definition list_of :: "('a\<Colon>heap) array \<Rightarrow> 'a list Heap" where
       
   112   "list_of a = (do n \<leftarrow> Array.length a;
       
   113                    list_of_aux n a []
       
   114                 done)"
       
   115 
       
   116 
       
   117 subsection {* Properties *}
       
   118 
       
   119 lemma array_make [code func]:
       
   120   "Array.new n x = make n (\<lambda>_. x)"
       
   121   by (induct n) (simp_all add: make_def new_def Heap_Monad.heap_def
       
   122     monad_simp array_of_list_replicate [symmetric]
       
   123     map_replicate_trivial replicate_append_same
       
   124     of_list_def)
       
   125 
       
   126 lemma array_of_list_make [code func]:
       
   127   "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
       
   128   unfolding make_def map_nth ..
       
   129 
       
   130 end