Theory IArray_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>
*)

  (*TODO: move this lemma*)
lemma conjI4:
  assumes A B C D
  shows "A ∧ B ∧ C ∧ D"
  using assms by simp

section{*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

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

subsection{*Lemmas*}

lemma IArray_equality:
  assumes length_eq: "length A = length B"
  shows "(IArray A = IArray B) = (∀i<length A. IArray A!!i=IArray B!!i)"
  by (metis length_eq nth_equalityI sub.simps)

lemma IArray_equality':
  assumes length_eq: "length A = length B"
  and "(∀i<length A. IArray A!!i=IArray B!!i)"
  shows "(IArray A = IArray B)"
  using IArray_equality assms by blast

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

subsection{*Definitions*}

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

fun exists :: "('a => bool) => 'a iarray => bool"
  where "exists f (IArray as) = (if Option.is_none (IArray_Addenda.find f (IArray as)) then False else True)"
hide_const (open) exists

fun all :: "('a => bool) => 'a iarray => bool"
  where "all f (IArray as) = (Option.is_none (IArray_Addenda.find (λx. ¬ f x) (IArray as)))"
hide_const (open) all

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 generator*}

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

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

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

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