28 by (simp add: sublist'_update3) |
28 by (simp add: sublist'_update3) |
29 |
29 |
30 lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []" |
30 lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []" |
31 by (simp add: subarray_def sublist'_Nil') |
31 by (simp add: subarray_def sublist'_Nil') |
32 |
32 |
33 lemma subarray_single: "\<lbrakk> n < Array.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]" |
33 lemma subarray_single: "\<lbrakk> n < Array.length h a \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]" |
34 by (simp add: subarray_def length_def sublist'_single) |
34 by (simp add: subarray_def length_def sublist'_single) |
35 |
35 |
36 lemma length_subarray: "m \<le> Array.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n" |
36 lemma length_subarray: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray n m a h) = m - n" |
37 by (simp add: subarray_def length_def length_sublist') |
37 by (simp add: subarray_def length_def length_sublist') |
38 |
38 |
39 lemma length_subarray_0: "m \<le> Array.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m" |
39 lemma length_subarray_0: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray 0 m a h) = m" |
40 by (simp add: length_subarray) |
40 by (simp add: length_subarray) |
41 |
41 |
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" |
42 lemma subarray_nth_array_Cons: "\<lbrakk> i < Array.length h a; i < j \<rbrakk> \<Longrightarrow> (get_array a h ! i) # subarray (Suc i) j a h = subarray i j a h" |
43 unfolding Array.length_def subarray_def |
43 unfolding Array.length_def subarray_def |
44 by (simp add: sublist'_front) |
44 by (simp add: sublist'_front) |
45 |
45 |
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)]" |
46 lemma subarray_nth_array_back: "\<lbrakk> i < j; j \<le> Array.length h a\<rbrakk> \<Longrightarrow> subarray i j a h = subarray i (j - 1) a h @ [get_array a h ! (j - 1)]" |
47 unfolding Array.length_def subarray_def |
47 unfolding Array.length_def subarray_def |
48 by (simp add: sublist'_back) |
48 by (simp add: sublist'_back) |
49 |
49 |
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" |
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" |
51 unfolding subarray_def |
51 unfolding subarray_def |
52 by (simp add: sublist'_append) |
52 by (simp add: sublist'_append) |
53 |
53 |
54 lemma subarray_all: "subarray 0 (Array.length a h) a h = get_array a h" |
54 lemma subarray_all: "subarray 0 (Array.length h a) a h = get_array a h" |
55 unfolding Array.length_def subarray_def |
55 unfolding Array.length_def subarray_def |
56 by (simp add: sublist'_all) |
56 by (simp add: sublist'_all) |
57 |
57 |
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)" |
58 lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Array.length h a \<rbrakk> \<Longrightarrow> subarray i j a h ! k = get_array a h ! (i + k)" |
59 unfolding Array.length_def subarray_def |
59 unfolding Array.length_def subarray_def |
60 by (simp add: nth_sublist') |
60 by (simp add: nth_sublist') |
61 |
61 |
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')" |
62 lemma subarray_eq_samelength_iff: "Array.length h a = Array.length h' a \<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')" |
63 unfolding Array.length_def subarray_def by (rule sublist'_eq_samelength_iff) |
63 unfolding Array.length_def subarray_def by (rule sublist'_eq_samelength_iff) |
64 |
64 |
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))" |
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 h a \<longrightarrow> P (get_array a h ! k))" |
66 unfolding subarray_def Array.length_def by (rule all_in_set_sublist'_conv) |
66 unfolding subarray_def Array.length_def by (rule all_in_set_sublist'_conv) |
67 |
67 |
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))" |
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 h a \<longrightarrow> P (get_array a h ! k))" |
69 unfolding subarray_def Array.length_def by (rule ball_in_set_sublist'_conv) |
69 unfolding subarray_def Array.length_def by (rule ball_in_set_sublist'_conv) |
70 |
70 |
71 end |
71 end |