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