src/HOL/Library/IArray.thy
author kuncar
Sat, 16 Mar 2013 20:51:47 +0100
changeset 51438 a614e456870b
parent 51161 6ed12ae3b3e1
child 52435 6646bb548c6b
permissions -rw-r--r--
drop a workaround because of 8739f8abbecb
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50138
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     1
header "Immutable Arrays with Code Generation"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     2
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     3
theory IArray
51094
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
     4
imports Main
50138
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     5
begin
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     6
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     7
text{* Immutable arrays are lists wrapped up in an additional constructor.
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     8
There are no update operations. Hence code generation can safely implement
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     9
this type by efficient target language arrays.  Currently only SML is
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    10
provided. Should be extended to other target languages and more operations.
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    11
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    12
Note that arrays cannot be printed directly but only by turning them into
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    13
lists first. Arrays could be converted back into lists for printing if they
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    14
were wrapped up in an additional constructor. *}
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    15
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    16
datatype 'a iarray = IArray "'a list"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    17
51094
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    18
primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
50138
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    19
"list_of (IArray xs) = xs"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    20
hide_const (open) list_of
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    21
51094
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    22
definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    23
[simp]: "of_fun f n = IArray (map f [0..<n])"
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    24
hide_const (open) of_fun
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    25
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    26
definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    27
[simp]: "as !! n = IArray.list_of as ! n"
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    28
hide_const (open) sub
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    29
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    30
definition length :: "'a iarray \<Rightarrow> nat" where
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    31
[simp]: "length as = List.length (IArray.list_of as)"
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    32
hide_const (open) length
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    33
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    34
lemma list_of_code [code]:
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    35
"IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    36
by (cases as) (simp add: map_nth)
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    37
50138
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    38
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    39
subsection "Code Generation"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    40
51094
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    41
code_reserved SML Vector
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    42
50138
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    43
code_type iarray
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    44
  (SML "_ Vector.vector")
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    45
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    46
code_const IArray
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    47
  (SML "Vector.fromList")
51094
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    48
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51143
diff changeset
    49
lemma [code]:
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51143
diff changeset
    50
"size (as :: 'a iarray) = 0"
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51143
diff changeset
    51
by (cases as) simp
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51143
diff changeset
    52
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51143
diff changeset
    53
lemma [code]:
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51143
diff changeset
    54
"iarray_size f as = Suc (list_size f (IArray.list_of as))"
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51143
diff changeset
    55
by (cases as) simp
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51143
diff changeset
    56
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51143
diff changeset
    57
lemma [code]:
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51143
diff changeset
    58
"iarray_rec f as = f (IArray.list_of as)"
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51143
diff changeset
    59
by (cases as) simp
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51143
diff changeset
    60
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51143
diff changeset
    61
lemma [code]:
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51143
diff changeset
    62
"iarray_case f as = f (IArray.list_of as)"
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51143
diff changeset
    63
by (cases as) simp
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51143
diff changeset
    64
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51143
diff changeset
    65
lemma [code]:
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51143
diff changeset
    66
"HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51143
diff changeset
    67
by (cases as, cases bs) (simp add: equal)
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51143
diff changeset
    68
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51094
diff changeset
    69
primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51094
diff changeset
    70
"tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
51094
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    71
hide_const (open) tabulate
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    72
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    73
lemma [code]:
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51094
diff changeset
    74
"IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
51094
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    75
by simp 
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    76
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    77
code_const IArray.tabulate
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    78
  (SML "Vector.tabulate")
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    79
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51094
diff changeset
    80
primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51094
diff changeset
    81
"sub' (as, n) = IArray.list_of as ! nat_of_integer n"
51094
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    82
hide_const (open) sub'
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    83
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    84
lemma [code]:
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51094
diff changeset
    85
"as !! n = IArray.sub' (as, integer_of_nat n)"
51094
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    86
by simp
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    87
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    88
code_const IArray.sub'
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    89
  (SML "Vector.sub")
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    90
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51094
diff changeset
    91
definition length' :: "'a iarray \<Rightarrow> integer" where
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51094
diff changeset
    92
[simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
51094
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    93
hide_const (open) length'
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    94
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    95
lemma [code]:
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51094
diff changeset
    96
"IArray.length as = nat_of_integer (IArray.length' as)"
51094
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    97
by simp
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    98
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
    99
code_const IArray.length'
50138
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
   100
  (SML "Vector.length")
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
   101
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
   102
end
51094
84b03c49c223 IArray ignorant of particular representation of nat
haftmann
parents: 50138
diff changeset
   103