src/HOL/Imperative_HOL/ex/Subarray.thy
 author haftmann Fri Jul 23 10:58:13 2010 +0200 (2010-07-23) changeset 37947 844977c7abeb parent 37806 a7679be14442 child 44890 22f665a2e91c permissions -rw-r--r--
```     1 (*  Title:      HOL/Imperative_HOL/ex/Subarray.thy
```
```     2     Author:     Lukas Bulwahn, TU Muenchen
```
```     3 *)
```
```     4
```
```     5 header {* Theorems about sub arrays *}
```
```     6
```
```     7 theory Subarray
```
```     8 imports Array Sublist
```
```     9 begin
```
```    10
```
```    11 definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" where
```
```    12   "subarray n m a h \<equiv> sublist' n m (Array.get h a)"
```
```    13
```
```    14 lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
```
```    15 apply (simp add: subarray_def Array.update_def)
```
```    16 apply (simp add: sublist'_update1)
```
```    17 done
```
```    18
```
```    19 lemma subarray_upd2: " i < n  \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
```
```    20 apply (simp add: subarray_def Array.update_def)
```
```    21 apply (subst sublist'_update2)
```
```    22 apply fastsimp
```
```    23 apply simp
```
```    24 done
```
```    25
```
```    26 lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h[i - n := v]"
```
```    27 unfolding subarray_def Array.update_def
```
```    28 by (simp add: sublist'_update3)
```
```    29
```
```    30 lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
```
```    31 by (simp add: subarray_def sublist'_Nil')
```
```    32
```
```    33 lemma subarray_single: "\<lbrakk> n < Array.length h a \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [Array.get h a ! n]"
```
```    34 by (simp add: subarray_def length_def sublist'_single)
```
```    35
```
```    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')
```
```    38
```
```    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)
```
```    41
```
```    42 lemma subarray_nth_array_Cons: "\<lbrakk> i < Array.length h a; i < j \<rbrakk> \<Longrightarrow> (Array.get h a ! i) # subarray (Suc i) j a h = subarray i j a h"
```
```    43 unfolding Array.length_def subarray_def
```
```    44 by (simp add: sublist'_front)
```
```    45
```
```    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 @ [Array.get h a ! (j - 1)]"
```
```    47 unfolding Array.length_def subarray_def
```
```    48 by (simp add: sublist'_back)
```
```    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"
```
```    51 unfolding subarray_def
```
```    52 by (simp add: sublist'_append)
```
```    53
```
```    54 lemma subarray_all: "subarray 0 (Array.length h a) a h = Array.get h a"
```
```    55 unfolding Array.length_def subarray_def
```
```    56 by (simp add: sublist'_all)
```
```    57
```
```    58 lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Array.length h a \<rbrakk> \<Longrightarrow> subarray i j a h ! k = Array.get h a ! (i + k)"
```
```    59 unfolding Array.length_def subarray_def
```
```    60 by (simp add: nth_sublist')
```
```    61
```
```    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> Array.get h a ! i' = Array.get h' a ! i')"
```
```    63 unfolding Array.length_def subarray_def by (rule sublist'_eq_samelength_iff)
```
```    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 h a \<longrightarrow> P (Array.get h a ! k))"
```
```    66 unfolding subarray_def Array.length_def by (rule all_in_set_sublist'_conv)
```
```    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 h a \<longrightarrow> P (Array.get h a ! k))"
```
```    69 unfolding subarray_def Array.length_def by (rule ball_in_set_sublist'_conv)
```
```    70
```
`    71 end`