src/HOL/Imperative_HOL/ex/Subarray.thy
 author haftmann Tue Jul 13 16:12:40 2010 +0200 (2010-07-13 ago) changeset 37805 0f797d586ce5 parent 37802 f2e9c104cebd child 37806 a7679be14442 permissions -rw-r--r--
canonical argument order for get
1 (*  Title:      HOL/Imperative_HOL/ex/Subarray.thy
2     Author:     Lukas Bulwahn, TU Muenchen
3 *)
7 theory Subarray
8 imports Array Sublist
9 begin
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 (get_array h a)"
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)
17 done
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
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
30 lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
31 by (simp add: subarray_def sublist'_Nil')
33 lemma subarray_single: "\<lbrakk> n < Array.length h a \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array h a ! n]"
34 by (simp add: subarray_def length_def sublist'_single)
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')
39 lemma length_subarray_0: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray 0 m a h) = m"
42 lemma subarray_nth_array_Cons: "\<lbrakk> i < Array.length h a; i < j \<rbrakk> \<Longrightarrow> (get_array h a ! i) # subarray (Suc i) j a h = subarray i j a h"
43 unfolding Array.length_def subarray_def
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 h a ! (j - 1)]"
47 unfolding Array.length_def subarray_def
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