(* 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