|
1 theory Subarray |
|
2 imports Array Sublist |
|
3 begin |
|
4 |
|
5 definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" |
|
6 where |
|
7 "subarray n m a h \<equiv> sublist' n m (get_array a h)" |
|
8 |
|
9 lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h" |
|
10 apply (simp add: subarray_def Heap.upd_def) |
|
11 apply (simp add: sublist'_update1) |
|
12 done |
|
13 |
|
14 lemma subarray_upd2: " i < n \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h" |
|
15 apply (simp add: subarray_def Heap.upd_def) |
|
16 apply (subst sublist'_update2) |
|
17 apply fastsimp |
|
18 apply simp |
|
19 done |
|
20 |
|
21 lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h[i - n := v]" |
|
22 unfolding subarray_def Heap.upd_def |
|
23 by (simp add: sublist'_update3) |
|
24 |
|
25 lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []" |
|
26 by (simp add: subarray_def sublist'_Nil') |
|
27 |
|
28 lemma subarray_single: "\<lbrakk> n < Heap.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]" |
|
29 by (simp add: subarray_def Heap.length_def sublist'_single) |
|
30 |
|
31 lemma length_subarray: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n" |
|
32 by (simp add: subarray_def Heap.length_def length_sublist') |
|
33 |
|
34 lemma length_subarray_0: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m" |
|
35 by (simp add: length_subarray) |
|
36 |
|
37 lemma subarray_nth_array_Cons: "\<lbrakk> i < Heap.length a h; i < j \<rbrakk> \<Longrightarrow> (get_array a h ! i) # subarray (Suc i) j a h = subarray i j a h" |
|
38 unfolding Heap.length_def subarray_def |
|
39 by (simp add: sublist'_front) |
|
40 |
|
41 lemma subarray_nth_array_back: "\<lbrakk> i < j; j \<le> Heap.length a h\<rbrakk> \<Longrightarrow> subarray i j a h = subarray i (j - 1) a h @ [get_array a h ! (j - 1)]" |
|
42 unfolding Heap.length_def subarray_def |
|
43 by (simp add: sublist'_back) |
|
44 |
|
45 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" |
|
46 unfolding subarray_def |
|
47 by (simp add: sublist'_append) |
|
48 |
|
49 lemma subarray_all: "subarray 0 (Heap.length a h) a h = get_array a h" |
|
50 unfolding Heap.length_def subarray_def |
|
51 by (simp add: sublist'_all) |
|
52 |
|
53 lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Heap.length a h \<rbrakk> \<Longrightarrow> subarray i j a h ! k = get_array a h ! (i + k)" |
|
54 unfolding Heap.length_def subarray_def |
|
55 by (simp add: nth_sublist') |
|
56 |
|
57 lemma subarray_eq_samelength_iff: "Heap.length a h = Heap.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')" |
|
58 unfolding Heap.length_def subarray_def by (rule sublist'_eq_samelength_iff) |
|
59 |
|
60 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 < Heap.length a h \<longrightarrow> P (get_array a h ! k))" |
|
61 unfolding subarray_def Heap.length_def by (rule all_in_set_sublist'_conv) |
|
62 |
|
63 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 < Heap.length a h \<longrightarrow> P (get_array a h ! k))" |
|
64 unfolding subarray_def Heap.length_def by (rule ball_in_set_sublist'_conv) |
|
65 |
|
66 end |