Theory Vector

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