Theory IArray_Addenda

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

section‹IArrays Addenda›

theory IArray_Addenda
  imports 
  "HOL-Library.IArray"
begin

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›

(*
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_printing
  constant "IArray_Addenda.find"  ⇀ (SML) "Vector.find"
| constant "IArray_Addenda.findi" ⇀ (SML) "Vector.findi"
| constant "IArray_Addenda.foldl" ⇀ (SML) "Vector.foldl"
*)

end