src/HOL/Library/IArray.thy
author wenzelm
Wed Mar 08 10:50:59 2017 +0100 (2017-03-08)
changeset 65151 a7394aa4d21c
parent 63649 e690d6f2185b
child 67613 ce654b0e6d69
permissions -rw-r--r--
tuned proofs;
     1 section "Immutable Arrays with Code Generation"
     2 
     3 theory IArray
     4 imports Main
     5 begin
     6 
     7 text\<open>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.\<close>
    15 
    16 context
    17 begin
    18 
    19 datatype 'a iarray = IArray "'a list"
    20 
    21 qualified primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
    22 "list_of (IArray xs) = xs"
    23 
    24 qualified definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
    25 [simp]: "of_fun f n = IArray (map f [0..<n])"
    26 
    27 qualified definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
    28 [simp]: "as !! n = IArray.list_of as ! n"
    29 
    30 qualified definition length :: "'a iarray \<Rightarrow> nat" where
    31 [simp]: "length as = List.length (IArray.list_of as)"
    32 
    33 qualified fun all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
    34 "all p (IArray as) = (ALL a : set as. p a)"
    35 
    36 qualified fun exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
    37 "exists p (IArray as) = (EX a : set as. p a)"
    38 
    39 lemma list_of_code [code]:
    40 "IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
    41 by (cases as) (simp add: map_nth)
    42 
    43 end
    44 
    45 
    46 subsection "Code Generation"
    47 
    48 code_reserved SML Vector
    49 
    50 code_printing
    51   type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector"
    52 | constant IArray \<rightharpoonup> (SML) "Vector.fromList"
    53 | constant IArray.all \<rightharpoonup> (SML) "Vector.all"
    54 | constant IArray.exists \<rightharpoonup> (SML) "Vector.exists"
    55 
    56 lemma [code]:
    57   "size (as :: 'a iarray) = Suc (length (IArray.list_of as))"
    58   by (cases as) simp
    59 
    60 lemma [code]:
    61   "size_iarray f as = Suc (size_list f (IArray.list_of as))"
    62   by (cases as) simp
    63 
    64 lemma [code]:
    65   "rec_iarray f as = f (IArray.list_of as)"
    66   by (cases as) simp
    67 
    68 lemma [code]:
    69   "case_iarray f as = f (IArray.list_of as)"
    70   by (cases as) simp
    71 
    72 lemma [code]:
    73   "set_iarray as = set (IArray.list_of as)"
    74   by (cases as) auto
    75 
    76 lemma [code]:
    77   "map_iarray f as = IArray (map f (IArray.list_of as))"
    78   by (cases as) auto
    79 
    80 lemma [code]:
    81   "rel_iarray r as bs = list_all2 r (IArray.list_of as) (IArray.list_of bs)"
    82   by (cases as, cases bs) auto
    83 
    84 lemma [code]:
    85   "HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
    86   by (cases as, cases bs) (simp add: equal)
    87 
    88 context
    89 begin
    90 
    91 qualified primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
    92   "tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
    93 
    94 end
    95 
    96 lemma [code]:
    97   "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
    98   by simp
    99 
   100 code_printing
   101   constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
   102 
   103 context
   104 begin
   105 
   106 qualified primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
   107   [code del]: "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
   108 
   109 end
   110 
   111 lemma [code]:
   112   "IArray.sub' (IArray as, n) = as ! nat_of_integer n"
   113   by simp
   114 
   115 lemma [code]:
   116   "as !! n = IArray.sub' (as, integer_of_nat n)"
   117   by simp
   118 
   119 code_printing
   120   constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
   121 
   122 context
   123 begin
   124 
   125 qualified definition length' :: "'a iarray \<Rightarrow> integer" where
   126   [code del, simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
   127 
   128 end
   129 
   130 lemma [code]:
   131   "IArray.length' (IArray as) = integer_of_nat (List.length as)" 
   132   by simp
   133 
   134 lemma [code]:
   135   "IArray.length as = nat_of_integer (IArray.length' as)"
   136   by simp
   137 
   138 context term_syntax
   139 begin
   140 
   141 lemma [code]:
   142   "Code_Evaluation.term_of (as :: 'a::typerep iarray) =
   143     Code_Evaluation.Const (STR ''IArray.iarray.IArray'') (TYPEREP('a list \<Rightarrow> 'a iarray)) <\<cdot>> (Code_Evaluation.term_of (IArray.list_of as))"
   144   by (subst term_of_anything) rule
   145 
   146 end
   147 
   148 code_printing
   149   constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
   150 
   151 end