Theory IArray_Addenda

header{*IArrays Addenda*}

theory IArray_Addenda
  imports 
  "$ISABELLE_HOME/src/HOL/Library/IArray"
begin

(*  
    Title:      IArray_Addenda.thy
    Author:     Jose Divasón <jose.divasonm at unirioja.es>
    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
*)

subsection{*Some previous instances*}

instantiation iarray :: (plus) plus
begin
definition plus_iarray :: "'a iarray => 'a iarray => 'a iarray"
  where "plus_iarray A B =  IArray.of_fun (λn. A!!n + B !! n) (IArray.length A)"
instance proof qed
end

instantiation iarray :: (minus) minus
begin
definition minus_iarray :: "'a iarray => 'a iarray => 'a iarray"
  where "minus_iarray A B =  IArray.of_fun (λn. A!!n - B !! n) (IArray.length A)"
instance proof qed
end

subsection{*Some previous definitions and properties for IArrays*}

subsubsection{*Lemmas*}

lemma of_fun_nth:
  assumes i: "i<n"
  shows "(IArray.of_fun f n) !! i = f i"
  unfolding of_fun_def using map_nth i by auto

subsubsection{*Definitions*}

fun all :: "('a => bool) => 'a iarray => bool"
where "all p (IArray as) = (ALL a : set as. p a)"
 hide_const (open) all

fun exists :: "('a => bool) => 'a iarray => bool"
where "exists p (IArray as) = (EX a : set as. p a)"
hide_const (open) exists

(*
fun find :: "('a => bool) => 'a iarray => 'a option"
  where "find f (IArray as) = List.find f as"
hide_const (open) find

primrec findi_acc_list :: "(nat × 'a => bool) => 'a list => nat => (nat × 'a) option" where
  "findi_acc_list _ [] aux = None" |
  "findi_acc_list P (x#xs) aux = (if P (aux,x) then Some (aux,x) else findi_acc_list P xs (Suc aux))"

definition "findi_list P x = findi_acc_list P x 0"

fun findi :: "(nat × 'a => bool) => 'a iarray => (nat × 'a) option"
  where "findi f (IArray as) = findi_list f as"
hide_const (open) findi

fun foldl :: "(('a × 'b) => 'b) => 'b => 'a iarray =>'b"
  where "foldl f a (IArray as) = List.foldl (λx y. f (y,x)) a as"
hide_const (open) foldl

fun filter :: "('a => bool) => 'a iarray => 'a iarray"
  where "filter f (IArray as) = IArray (List.filter f as)"
hide_const (open) filter
*)

subsection{*Code generation*}

code_const IArray_Addenda.exists
  (SML "Vector.exists")

code_const IArray_Addenda.all
  (SML "Vector.all")

(*
code_const IArray_Addenda.find
  (SML "Vector.find")

code_const IArray_Addenda.findi
  (SML "Vector.findi")

code_const IArray_Addenda.foldl
  (SML "Vector.foldl")
*)

(*Examples:*)
(*value [simp]"IArray_Matrices_2.all (λx. x>1) (IArray [7,2,4,2::real])"*)
(*value [code]"IArray_Matrices_2.all (λx. x>1) (IArray [7,2,4,2::real])"*)
(*value[code] "IArray_Matrices_2.foldl (λx. (fst x) + (snd x)) 0 (IArray [0..<8::nat])"*)
(*value[code] "IArray_Matrices_2.findi (λx. if (snd x)>0 then True else False) (IArray [0,1,3,0::real])"*)

end