src/HOL/Library/IArray.thy
author blanchet
Wed Sep 24 15:45:55 2014 +0200 (2014-09-24)
changeset 58425 246985c6b20b
parent 58310 91ea607a34d8
child 58881 b9556a055632
permissions -rw-r--r--
simpler proof
     1 header "Immutable Arrays with Code Generation"
     2 
     3 theory IArray
     4 imports Main
     5 begin
     6 
     7 text{* Immutable arrays are lists wrapped up in an additional constructor.
     8 There are no update operations. Hence code generation can safely implement
     9 this type by efficient target language arrays.  Currently only SML is
    10 provided. Should be extended to other target languages and more operations.
    11 
    12 Note that arrays cannot be printed directly but only by turning them into
    13 lists first. Arrays could be converted back into lists for printing if they
    14 were wrapped up in an additional constructor. *}
    15 
    16 datatype 'a iarray = IArray "'a list"
    17 
    18 primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
    19 "list_of (IArray xs) = xs"
    20 hide_const (open) list_of
    21 
    22 definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
    23 [simp]: "of_fun f n = IArray (map f [0..<n])"
    24 hide_const (open) of_fun
    25 
    26 definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
    27 [simp]: "as !! n = IArray.list_of as ! n"
    28 hide_const (open) sub
    29 
    30 definition length :: "'a iarray \<Rightarrow> nat" where
    31 [simp]: "length as = List.length (IArray.list_of as)"
    32 hide_const (open) length
    33 
    34 fun all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
    35 "all p (IArray as) = (ALL a : set as. p a)"
    36 hide_const (open) all
    37 
    38 fun exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
    39 "exists p (IArray as) = (EX a : set as. p a)"
    40 hide_const (open) exists
    41 
    42 lemma list_of_code [code]:
    43 "IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
    44 by (cases as) (simp add: map_nth)
    45 
    46 
    47 subsection "Code Generation"
    48 
    49 code_reserved SML Vector
    50 
    51 code_printing
    52   type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector"
    53 | constant IArray \<rightharpoonup> (SML) "Vector.fromList"
    54 | constant IArray.all \<rightharpoonup> (SML) "Vector.all"
    55 | constant IArray.exists \<rightharpoonup> (SML) "Vector.exists"
    56 
    57 lemma [code]:
    58   "size (as :: 'a iarray) = Suc (length (IArray.list_of as))"
    59   by (cases as) simp
    60 
    61 lemma [code]:
    62   "size_iarray f as = Suc (size_list f (IArray.list_of as))"
    63   by (cases as) simp
    64 
    65 lemma [code]:
    66   "rec_iarray f as = f (IArray.list_of as)"
    67   by (cases as) simp
    68 
    69 lemma [code]:
    70   "case_iarray f as = f (IArray.list_of as)"
    71   by (cases as) simp
    72 
    73 lemma [code]:
    74   "set_iarray as = set (IArray.list_of as)"
    75   by (case_tac as) auto
    76 
    77 lemma [code]:
    78   "map_iarray f as = IArray (map f (IArray.list_of as))"
    79   by (case_tac as) auto
    80 
    81 lemma [code]:
    82   "rel_iarray r as bs = list_all2 r (IArray.list_of as) (IArray.list_of bs)"
    83   by (case_tac as) (case_tac bs, auto)
    84 
    85 lemma [code]:
    86   "HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
    87   by (cases as, cases bs) (simp add: equal)
    88 
    89 primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
    90   "tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
    91 
    92 hide_const (open) tabulate
    93 
    94 lemma [code]:
    95   "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
    96   by simp
    97 
    98 code_printing
    99   constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
   100 
   101 primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
   102   [code del]: "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
   103 
   104 hide_const (open) sub'
   105 
   106 lemma [code]:
   107   "IArray.sub' (IArray as, n) = as ! nat_of_integer n"
   108   by simp
   109 
   110 lemma [code]:
   111   "as !! n = IArray.sub' (as, integer_of_nat n)"
   112   by simp
   113 
   114 code_printing
   115   constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
   116 
   117 definition length' :: "'a iarray \<Rightarrow> integer" where
   118   [code del, simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
   119 
   120 hide_const (open) length'
   121 
   122 lemma [code]:
   123   "IArray.length' (IArray as) = integer_of_nat (List.length as)" 
   124   by simp
   125 
   126 lemma [code]:
   127   "IArray.length as = nat_of_integer (IArray.length' as)"
   128   by simp
   129 
   130 code_printing
   131   constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
   132 
   133 end