# Theory Vector

Up to index of Isabelle/HOL/Tame

theory Vector
imports Main EfficientNat
begin

```(*  ID:         \$Id: Vector.thy,v 1.1 2006/01/04 13:44:15 nipkow Exp \$
Author:     Gertrud Bauer, Tobias Nipkow
*)

theory Vector
imports Main EfficientNat
begin

datatype 'a vector = Vector "'a list"

subsection {* Tabulation *}

constdefs
tabulate' :: "nat × (nat => 'a) => 'a vector"
"tabulate' p ≡ Vector (map (snd p) [0 ..< fst p])"
(* map int [0..nat (fst p)])])*)
tabulate :: "nat => (nat => 'a) => 'a vector"
"tabulate n f ≡ tabulate' (n, f)"
tabulate2 :: "nat => nat => (nat => nat => 'a) => 'a vector vector"
"tabulate2 m n f ≡ tabulate m (λi .tabulate n (f i))"
tabulate3 :: "nat => nat => nat =>
(nat => nat => nat => 'a) => 'a vector vector vector"
"tabulate3 l m n f ≡ tabulate l (λi. tabulate m (λj .tabulate n (λk. f i j k)))"

syntax
"_tabulate" :: "'a => pttrn => nat => 'a vector"  ("([|_. _ < _|])")
"_tabulate2" :: "'a => pttrn => nat =>
pttrn => nat => 'a vector"
("([|_. _ < _, _ < _|])")
"_tabulate3" :: "'a => pttrn => nat =>
pttrn => nat =>
pttrn => nat => 'a vector"
("([|_. _ < _, _ < _, _ < _ |])")
translations
"[|f. x < n|]" == "tabulate n (λx. f)"
"[|f. x < m, y < n|]" == "tabulate2 m n (λx y. f)"
"[|f. x < l, y < m, z < n|]" == "tabulate3 l m n (λx y z. f)"

subsection {* Access *}

constdefs
sub1 :: "'a vector × nat => 'a"
"sub1 p ≡ let (a, n) = p in case a of (Vector as) => as ! n"
sub :: "'a vector => nat => 'a"
"sub a n ≡ sub1 (a, n)"

syntax
"_sub" :: "'a vector => nat => 'a"  ("(_[|_|])" [1000] 999)
"_sub2" :: "'a vector vector => nat => nat => 'a"  ("(_[|_,_|])" [1000] 999)
"_sub3" :: "'a vector vector vector => nat => nat => nat => 'a" ("(_[|_,_,_|])" [1000] 999)

translations
"(a[|n|])" == "sub a n"
"(as[|m, n|])" == "sub (sub as m) n"
"(as[|l, m, n|])" == "sub (sub (sub as l) m) n"

types_code
vector  ("_ vector")

consts_code
"tabulate'"  ("Vector.tabulate")
"sub1"       ("Vector.sub")

text {* examples:  @{term "[|0. i < 5|]"}, @{term "[|i. i < 5, j < 3|]"}  *}

lemma sub_tabulate: "0 ≤ i ==> i < u ==>
(tabulate u f)[|i|] = f i"
by (simp add: tabulate_def tabulate'_def sub_def sub1_def Let_def)

lemma sub_tabulate3: "0 ≤ i ==> 0 ≤ j ==> 0 ≤ k ==>
i < l ==> j < m ==> k < n ==>
(tabulate3 l m n f)[|i, j, k|] = f i j k"
by (simp add: tabulate3_def tabulate_def tabulate'_def
sub_def sub1_def Let_def  Vector.inject
split: Vector.split)

end
```

### Access

lemma sub_tabulate:

`  [| 0 ≤ i; i < u |] ==> (tabulate u f)[|i|] = f i`

lemma sub_tabulate3:

```  [| 0 ≤ i; 0 ≤ j; 0 ≤ k; i < l; j < m; k < n |]
==> (((tabulate3 l m n f)[|i|])[|j|])[|k|] = f i j k```