src/HOL/Library/IArray.thy
author haftmann
Wed Jul 18 20:51:21 2018 +0200 (9 months ago)
changeset 68658 16cc1161ad7f
parent 68657 65ad2bfc19d2
child 68659 db0c70767d86
permissions -rw-r--r--
tuned equation
haftmann@68657
     1
(*  Title:      HOL/Library/IArray.thy
haftmann@68657
     2
    Author:     Tobias Nipkow, TU Muenchen
haftmann@68657
     3
*)
haftmann@68657
     4
haftmann@68654
     5
section \<open>Immutable Arrays with Code Generation\<close>
nipkow@50138
     6
nipkow@50138
     7
theory IArray
haftmann@51094
     8
imports Main
nipkow@50138
     9
begin
nipkow@50138
    10
haftmann@68657
    11
subsection \<open>Fundamental operations\<close>
haftmann@68657
    12
haftmann@68657
    13
text \<open>Immutable arrays are lists wrapped up in an additional constructor.
nipkow@50138
    14
There are no update operations. Hence code generation can safely implement
nipkow@50138
    15
this type by efficient target language arrays.  Currently only SML is
haftmann@68657
    16
provided. Could be extended to other target languages and more operations.\<close>
nipkow@50138
    17
wenzelm@61115
    18
context
wenzelm@61115
    19
begin
wenzelm@61115
    20
blanchet@58310
    21
datatype 'a iarray = IArray "'a list"
nipkow@50138
    22
wenzelm@61115
    23
qualified primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
nipkow@50138
    24
"list_of (IArray xs) = xs"
nipkow@50138
    25
wenzelm@61115
    26
qualified definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
haftmann@51094
    27
[simp]: "of_fun f n = IArray (map f [0..<n])"
haftmann@51094
    28
wenzelm@61115
    29
qualified definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
haftmann@51094
    30
[simp]: "as !! n = IArray.list_of as ! n"
haftmann@51094
    31
wenzelm@61115
    32
qualified definition length :: "'a iarray \<Rightarrow> nat" where
haftmann@51094
    33
[simp]: "length as = List.length (IArray.list_of as)"
haftmann@51094
    34
haftmann@68656
    35
qualified primrec all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
haftmann@68656
    36
"all p (IArray as) \<longleftrightarrow> (\<forall>a \<in> set as. p a)"
nipkow@54459
    37
haftmann@68656
    38
qualified primrec exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
haftmann@68656
    39
"exists p (IArray as) \<longleftrightarrow> (\<exists>a \<in> set as. p a)"
nipkow@54459
    40
haftmann@51094
    41
lemma list_of_code [code]:
haftmann@51094
    42
"IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
haftmann@51094
    43
by (cases as) (simp add: map_nth)
haftmann@51094
    44
haftmann@68655
    45
lemma of_fun_nth:
haftmann@68655
    46
"IArray.of_fun f n !! i = f i" if "i < n"
haftmann@68655
    47
using that by (simp add: map_nth)
haftmann@68655
    48
wenzelm@61115
    49
end
wenzelm@61115
    50
nipkow@50138
    51
haftmann@68657
    52
subsection \<open>Generic code equations\<close>
haftmann@51094
    53
haftmann@51161
    54
lemma [code]:
haftmann@68658
    55
  "size (as :: 'a iarray) = Suc (IArray.length as)"
blanchet@58269
    56
  by (cases as) simp
haftmann@51161
    57
haftmann@51161
    58
lemma [code]:
blanchet@58269
    59
  "size_iarray f as = Suc (size_list f (IArray.list_of as))"
blanchet@58269
    60
  by (cases as) simp
blanchet@58269
    61
blanchet@58269
    62
lemma [code]:
blanchet@58269
    63
  "rec_iarray f as = f (IArray.list_of as)"
blanchet@58269
    64
  by (cases as) simp
blanchet@58269
    65
blanchet@58269
    66
lemma [code]:
blanchet@58269
    67
  "case_iarray f as = f (IArray.list_of as)"
blanchet@58269
    68
  by (cases as) simp
haftmann@51161
    69
haftmann@51161
    70
lemma [code]:
blanchet@58269
    71
  "set_iarray as = set (IArray.list_of as)"
wenzelm@63649
    72
  by (cases as) auto
blanchet@58269
    73
blanchet@58269
    74
lemma [code]:
blanchet@58269
    75
  "map_iarray f as = IArray (map f (IArray.list_of as))"
wenzelm@63649
    76
  by (cases as) auto
haftmann@51161
    77
haftmann@51161
    78
lemma [code]:
blanchet@58269
    79
  "rel_iarray r as bs = list_all2 r (IArray.list_of as) (IArray.list_of bs)"
wenzelm@63649
    80
  by (cases as, cases bs) auto
haftmann@51161
    81
haftmann@51161
    82
lemma [code]:
blanchet@58269
    83
  "HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
blanchet@58269
    84
  by (cases as, cases bs) (simp add: equal)
haftmann@51161
    85
haftmann@59457
    86
context term_syntax
haftmann@59457
    87
begin
haftmann@59457
    88
haftmann@59457
    89
lemma [code]:
haftmann@59457
    90
  "Code_Evaluation.term_of (as :: 'a::typerep iarray) =
haftmann@59457
    91
    Code_Evaluation.Const (STR ''IArray.iarray.IArray'') (TYPEREP('a list \<Rightarrow> 'a iarray)) <\<cdot>> (Code_Evaluation.term_of (IArray.list_of as))"
haftmann@59457
    92
  by (subst term_of_anything) rule
haftmann@59457
    93
haftmann@59457
    94
end
haftmann@59457
    95
haftmann@68657
    96
haftmann@68657
    97
subsection \<open>Auxiliary operations for code generation\<close>
haftmann@68657
    98
haftmann@68657
    99
context
haftmann@68657
   100
begin
haftmann@68657
   101
haftmann@68657
   102
qualified primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
haftmann@68657
   103
  "tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
haftmann@68657
   104
haftmann@68657
   105
lemma [code]:
haftmann@68657
   106
  "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
haftmann@68657
   107
  by simp
haftmann@68657
   108
haftmann@68657
   109
qualified primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
haftmann@68657
   110
  "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
haftmann@68657
   111
haftmann@68657
   112
lemma [code]:
haftmann@68657
   113
  "IArray.sub' (IArray as, n) = as ! nat_of_integer n"
haftmann@68657
   114
  by simp
haftmann@68657
   115
haftmann@68657
   116
lemma [code]:
haftmann@68657
   117
  "as !! n = IArray.sub' (as, integer_of_nat n)"
haftmann@68657
   118
  by simp
haftmann@68657
   119
haftmann@68657
   120
qualified definition length' :: "'a iarray \<Rightarrow> integer" where
haftmann@68657
   121
  [simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
haftmann@68657
   122
haftmann@68657
   123
lemma [code]:
haftmann@68657
   124
  "IArray.length' (IArray as) = integer_of_nat (List.length as)"
haftmann@68657
   125
  by simp
haftmann@68657
   126
haftmann@68657
   127
lemma [code]:
haftmann@68657
   128
  "IArray.length as = nat_of_integer (IArray.length' as)"
haftmann@68657
   129
  by simp
nipkow@50138
   130
nipkow@50138
   131
end
haftmann@68657
   132
haftmann@68657
   133
haftmann@68657
   134
subsection \<open>Code Generation for SML\<close>
haftmann@68657
   135
haftmann@68657
   136
text \<open>Note that arrays cannot be printed directly but only by turning them into
haftmann@68657
   137
lists first. Arrays could be converted back into lists for printing if they
haftmann@68657
   138
were wrapped up in an additional constructor.\<close>
haftmann@68657
   139
haftmann@68657
   140
code_reserved SML Vector
haftmann@68657
   141
haftmann@68657
   142
code_printing
haftmann@68657
   143
  type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector"
haftmann@68657
   144
| constant IArray \<rightharpoonup> (SML) "Vector.fromList"
haftmann@68657
   145
| constant IArray.all \<rightharpoonup> (SML) "Vector.all"
haftmann@68657
   146
| constant IArray.exists \<rightharpoonup> (SML) "Vector.exists"
haftmann@68657
   147
| constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
haftmann@68657
   148
| constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
haftmann@68657
   149
| constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
haftmann@68657
   150
haftmann@68657
   151
end