author | haftmann |
Mon, 05 Jul 2010 16:46:23 +0200 | |
changeset 37716 | 271ecd4fb9f9 |
parent 36098 | 53992c639da5 |
child 37796 | 08bd610b2583 |
permissions | -rw-r--r-- |
bulwahn@36098 | 1 |
(* Title: HOL/Imperative_HOL/ex/Subarray.thy |
bulwahn@36098 | 2 |
Author: Lukas Bulwahn, TU Muenchen |
bulwahn@36098 | 3 |
*) |
bulwahn@36098 | 4 |
|
bulwahn@36098 | 5 |
header {* Theorems about sub arrays *} |
bulwahn@36098 | 6 |
|
bulwahn@27656 | 7 |
theory Subarray |
bulwahn@27656 | 8 |
imports Array Sublist |
bulwahn@27656 | 9 |
begin |
bulwahn@27656 | 10 |
|
haftmann@37716 | 11 |
definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" where |
bulwahn@27656 | 12 |
"subarray n m a h \<equiv> sublist' n m (get_array a h)" |
bulwahn@27656 | 13 |
|
haftmann@37716 | 14 |
lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Array.change a i v h) = subarray n m a h" |
haftmann@37716 | 15 |
apply (simp add: subarray_def Array.change_def) |
bulwahn@27656 | 16 |
apply (simp add: sublist'_update1) |
bulwahn@27656 | 17 |
done |
bulwahn@27656 | 18 |
|
haftmann@37716 | 19 |
lemma subarray_upd2: " i < n \<Longrightarrow> subarray n m a (Array.change a i v h) = subarray n m a h" |
haftmann@37716 | 20 |
apply (simp add: subarray_def Array.change_def) |
bulwahn@27656 | 21 |
apply (subst sublist'_update2) |
bulwahn@27656 | 22 |
apply fastsimp |
bulwahn@27656 | 23 |
apply simp |
bulwahn@27656 | 24 |
done |
bulwahn@27656 | 25 |
|
haftmann@37716 | 26 |
lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Array.change a i v h) = subarray n m a h[i - n := v]" |
haftmann@37716 | 27 |
unfolding subarray_def Array.change_def |
bulwahn@27656 | 28 |
by (simp add: sublist'_update3) |
bulwahn@27656 | 29 |
|
bulwahn@27656 | 30 |
lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []" |
bulwahn@27656 | 31 |
by (simp add: subarray_def sublist'_Nil') |
bulwahn@27656 | 32 |
|
haftmann@37716 | 33 |
lemma subarray_single: "\<lbrakk> n < Array.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]" |
haftmann@37716 | 34 |
by (simp add: subarray_def length_def sublist'_single) |
bulwahn@27656 | 35 |
|
haftmann@37716 | 36 |
lemma length_subarray: "m \<le> Array.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n" |
haftmann@37716 | 37 |
by (simp add: subarray_def length_def length_sublist') |
bulwahn@27656 | 38 |
|
haftmann@37716 | 39 |
lemma length_subarray_0: "m \<le> Array.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m" |
bulwahn@27656 | 40 |
by (simp add: length_subarray) |
bulwahn@27656 | 41 |
|
haftmann@37716 | 42 |
lemma subarray_nth_array_Cons: "\<lbrakk> i < Array.length a h; i < j \<rbrakk> \<Longrightarrow> (get_array a h ! i) # subarray (Suc i) j a h = subarray i j a h" |
haftmann@37716 | 43 |
unfolding Array.length_def subarray_def |
bulwahn@27656 | 44 |
by (simp add: sublist'_front) |
bulwahn@27656 | 45 |
|
haftmann@37716 | 46 |
lemma subarray_nth_array_back: "\<lbrakk> i < j; j \<le> Array.length a h\<rbrakk> \<Longrightarrow> subarray i j a h = subarray i (j - 1) a h @ [get_array a h ! (j - 1)]" |
haftmann@37716 | 47 |
unfolding Array.length_def subarray_def |
bulwahn@27656 | 48 |
by (simp add: sublist'_back) |
bulwahn@27656 | 49 |
|
bulwahn@27656 | 50 |
lemma subarray_append: "\<lbrakk> i < j; j < k \<rbrakk> \<Longrightarrow> subarray i j a h @ subarray j k a h = subarray i k a h" |
bulwahn@27656 | 51 |
unfolding subarray_def |
bulwahn@27656 | 52 |
by (simp add: sublist'_append) |
bulwahn@27656 | 53 |
|
haftmann@37716 | 54 |
lemma subarray_all: "subarray 0 (Array.length a h) a h = get_array a h" |
haftmann@37716 | 55 |
unfolding Array.length_def subarray_def |
bulwahn@27656 | 56 |
by (simp add: sublist'_all) |
bulwahn@27656 | 57 |
|
haftmann@37716 | 58 |
lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Array.length a h \<rbrakk> \<Longrightarrow> subarray i j a h ! k = get_array a h ! (i + k)" |
haftmann@37716 | 59 |
unfolding Array.length_def subarray_def |
bulwahn@27656 | 60 |
by (simp add: nth_sublist') |
bulwahn@27656 | 61 |
|
haftmann@37716 | 62 |
lemma subarray_eq_samelength_iff: "Array.length a h = Array.length a h' \<Longrightarrow> (subarray i j a h = subarray i j a h') = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> get_array a h ! i' = get_array a h' ! i')" |
haftmann@37716 | 63 |
unfolding Array.length_def subarray_def by (rule sublist'_eq_samelength_iff) |
bulwahn@27656 | 64 |
|
haftmann@37716 | 65 |
lemma all_in_set_subarray_conv: "(\<forall>j. j \<in> set (subarray l r a h) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Array.length a h \<longrightarrow> P (get_array a h ! k))" |
haftmann@37716 | 66 |
unfolding subarray_def Array.length_def by (rule all_in_set_sublist'_conv) |
bulwahn@27656 | 67 |
|
haftmann@37716 | 68 |
lemma ball_in_set_subarray_conv: "(\<forall>j \<in> set (subarray l r a h). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Array.length a h \<longrightarrow> P (get_array a h ! k))" |
haftmann@37716 | 69 |
unfolding subarray_def Array.length_def by (rule ball_in_set_sublist'_conv) |
bulwahn@27656 | 70 |
|
bulwahn@27656 | 71 |
end |