Quelle Subarray.thy Sprache: Isabelle

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

quality100%

¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.