(* ID: $Id: Vector.thy,v 1.1 2006/01/04 13:44:15 nipkow Exp $
Author: Gertrud Bauer, Tobias Nipkow
*)
header {* Vector *}
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
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