Theory Subarray

(*  Title:      HOL/Imperative_HOL/ex/Subarray.thy
    Author:     Lukas Bulwahn, TU Muenchen
*)

section ‹Theorems about sub arrays›

theory Subarray
imports "../Array" List_Sublist
begin

definition subarray :: "nat ⇒ nat ⇒ ('a::heap) array ⇒ heap ⇒ 'a list" where
  "subarray n m a h ≡ nths' n m (Array.get h a)"

lemma subarray_upd: "i ≥ m ⟹ subarray n m a (Array.update a i v h) = subarray n m a h"
apply (simp add: subarray_def Array.update_def)
apply (simp add: nths'_update1)
done

lemma subarray_upd2: " i < n  ⟹ subarray n m a (Array.update a i v h) = subarray n m a h"
apply (simp add: subarray_def Array.update_def)
apply (subst nths'_update2)
apply fastforce
apply simp
done

lemma subarray_upd3: "⟦ n ≤ i; i < m⟧ ⟹ subarray n m a (Array.update a i v h) = (subarray n m a h)[i - n := v]"
unfolding subarray_def Array.update_def
by (simp add: nths'_update3)

lemma subarray_Nil: "n ≥ m ⟹ subarray n m a h = []"
by (simp add: subarray_def nths'_Nil')

lemma subarray_single: "⟦ n < Array.length h a ⟧ ⟹ subarray n (Suc n) a h = [Array.get h a ! n]" 
by (simp add: subarray_def length_def nths'_single)

lemma length_subarray: "m ≤ Array.length h a ⟹ List.length (subarray n m a h) = m - n"
by (simp add: subarray_def length_def length_nths')

lemma length_subarray_0: "m ≤ Array.length h a ⟹ List.length (subarray 0 m a h) = m"
by (simp add: length_subarray)

lemma subarray_nth_array_Cons: "⟦ i < Array.length h a; i < j ⟧ ⟹ (Array.get h a ! i) # subarray (Suc i) j a h = subarray i j a h"
unfolding Array.length_def subarray_def
by (simp add: nths'_front)

lemma subarray_nth_array_back: "⟦ i < j; j ≤ Array.length h a⟧ ⟹ subarray i j a h = subarray i (j - 1) a h @ [Array.get h a ! (j - 1)]"
unfolding Array.length_def subarray_def
by (simp add: nths'_back)

lemma subarray_append: "⟦ i ≤ j; j ≤ k ⟧ ⟹ subarray i j a h @ subarray j k a h = subarray i k a h"
unfolding subarray_def
by (simp add: nths'_append)

lemma subarray_all: "subarray 0 (Array.length h a) a h = Array.get h a"
unfolding Array.length_def subarray_def
by (simp add: nths'_all)

lemma nth_subarray: "⟦ k < j - i; j ≤ Array.length h a ⟧ ⟹ subarray i j a h ! k = Array.get h a ! (i + k)"
unfolding Array.length_def subarray_def
by (simp add: nth_nths')

lemma subarray_eq_samelength_iff: "Array.length h a = Array.length h' a ⟹ (subarray i j a h = subarray i j a h') = (∀i'. i ≤ i' ∧ i' < j ⟶ Array.get h a ! i' = Array.get h' a ! i')"
unfolding Array.length_def subarray_def by (rule nths'_eq_samelength_iff)

lemma all_in_set_subarray_conv: "(∀j. j ∈ set (subarray l r a h) ⟶ P j) = (∀k. l ≤ k ∧ k < r ∧ k < Array.length h a ⟶ P (Array.get h a ! k))"
unfolding subarray_def Array.length_def by (rule all_in_set_nths'_conv)

lemma ball_in_set_subarray_conv: "(∀j ∈ set (subarray l r a h). P j) = (∀k. l ≤ k ∧ k < r ∧ k < Array.length h a ⟶ P (Array.get h a ! k))"
unfolding subarray_def Array.length_def by (rule ball_in_set_nths'_conv)

end