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