products/Sources/formale Sprachen/Isabelle/HOL/Imperative_HOL/ex/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Subarray.thy   Sprache: Isabelle

Untersuchung 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

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.18Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff