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