(* Title: HOL/Imperative_HOL/ex/Subarray.thy
Author: Lukas Bulwahn, TU Muenchen
*)
section \<open>Theorems about sub arrays\<close>
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
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
