Theory IArray_Syntax

(*  Author:     Gertrud Bauer, Tobias Nipkow
*)

section ‹Syntax for operations on immutable arrays›

theory IArray_Syntax
imports Main "HOL-Library.IArray"
begin

subsection ‹Tabulation›

definition tabulate :: "nat  (nat  'a)  'a iarray"
where
  "tabulate n f = IArray.of_fun f n"

definition tabulate2 :: "nat  nat  (nat  nat  'a)  'a iarray iarray"
where
  "tabulate2 m n f = IArray.of_fun (λi .IArray.of_fun (f i) n) m "

definition tabulate3 :: "nat  nat  nat  
  (nat  nat  nat  'a)  'a iarray iarray iarray" where
  "tabulate3 l m n f  IArray.of_fun (λi. IArray.of_fun (λj. IArray.of_fun (λk. f i j k) n) m) l"

syntax 
 "_tabulate" :: "'a  pttrn  nat  'a iarray"  ("(_. _ < _)") 
 "_tabulate2" :: "'a  pttrn  nat  pttrn  nat  'a iarray"
   ("(_. _ < _, _ < _)")
 "_tabulate3" :: "'a  pttrn  nat  pttrn  nat  pttrn  nat  'a iarray"
   ("(_. _ < _, _ < _, _ < _ )")

translations 
  "f. x < n" == "CONST tabulate n (λx. f)"
  "f. x < m, y < n" == "CONST tabulate2 m n (λx y. f)"
  "f. x < l, y < m, z < n" == "CONST tabulate3 l m n (λx y z. f)"


subsection ‹Access›

abbreviation sub1_syntax :: "'a iarray  nat  'a"  ("(__)" [1000] 999)
where
  "an  IArray.sub a n"

abbreviation sub2_syntax :: "'a iarray iarray  nat  nat  'a"  ("(__,_)" [1000] 999)
where
  "asm, n  IArray.sub (IArray.sub as m) n"

abbreviation sub3_syntax :: "'a iarray iarray iarray  nat  nat  nat  'a"  ("(__,_,_)" [1000] 999)
where
  "asl, m, n  IArray.sub (IArray.sub (IArray.sub as l) m) n"

text ‹examples:  @{term "0. i < 5"}, @{term "i. i < 5, j < 3"}

end