Theory More_IArray

(*
    Authors:    Ralph Bottesch
                Maximilian Haslbeck
                René Thiemann
    License:    BSD
*)
section ‹Auxiliary Lemmas and Definitions for Immutable Arrays›

text ‹We define some definitions on immutable arrays, and modify the simplication
  rules so that IArrays will mainly operate pointwise, and not as lists.
  To be more precise, IArray.of-fun will become the main constructor.›
theory More_IArray
  imports "HOL-Library.IArray" 
begin

definition iarray_update :: "'a iarray ⇒ nat ⇒ 'a ⇒ 'a iarray" where
  "iarray_update a i x = IArray.of_fun (λ j. if j = i then x else a !! j) (IArray.length a)" 

lemma iarray_cong: "n = m ⟹ (⋀ i. i < m ⟹ f i = g i) ⟹ IArray.of_fun f n = IArray.of_fun g m" 
  by auto

lemma iarray_cong': "(⋀ i. i < n ⟹ f i = g i) ⟹ IArray.of_fun f n = IArray.of_fun g n" 
  by (rule iarray_cong, auto)

lemma iarray_update_length[simp]: "IArray.length (iarray_update a i x) = IArray.length a" 
  unfolding iarray_update_def by simp

lemma iarray_length_of_fun[simp]: "IArray.length (IArray.of_fun f n) = n" by simp

lemma iarray_update_of_fun[simp]: "iarray_update (IArray.of_fun f n) i x = IArray.of_fun (f (i := x)) n" 
  unfolding iarray_update_def iarray_length_of_fun
  by (rule iarray_cong, auto)

fun iarray_append where "iarray_append (IArray xs) x = IArray (xs @ [x])" 

lemma iarray_append_code[code]: "iarray_append xs x = IArray (IArray.list_of xs @ [x])"
  by (cases xs, auto)

lemma iarray_append_of_fun[simp]: "iarray_append (IArray.of_fun f n) x = IArray.of_fun (f (n := x)) (Suc n)" 
  by auto

declare iarray_append.simps[simp del]

lemma iarray_of_fun_sub[simp]: "i < n ⟹ IArray.of_fun f n !! i = f i" 
  by auto

lemma IArray_of_fun_conv: "IArray xs = IArray.of_fun (λ i. xs ! i) (length xs)" 
  by (auto intro!: nth_equalityI)

declare IArray.of_fun_def[simp del]
declare IArray.sub_def[simp del]

lemmas iarray_simps = iarray_update_of_fun iarray_append_of_fun IArray_of_fun_conv iarray_of_fun_sub

end