src/HOL/ex/Subarray.thy
changeset 30689 b14b2cc4e25e
parent 30688 2d1d426e00e4
child 30690 55ef8e045931
     1.1 --- a/src/HOL/ex/Subarray.thy	Mon Mar 23 19:01:17 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,66 +0,0 @@
     1.4 -theory Subarray
     1.5 -imports Array Sublist
     1.6 -begin
     1.7 -
     1.8 -definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list"
     1.9 -where
    1.10 -  "subarray n m a h \<equiv> sublist' n m (get_array a h)"
    1.11 -
    1.12 -lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
    1.13 -apply (simp add: subarray_def Heap.upd_def)
    1.14 -apply (simp add: sublist'_update1)
    1.15 -done
    1.16 -
    1.17 -lemma subarray_upd2: " i < n  \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
    1.18 -apply (simp add: subarray_def Heap.upd_def)
    1.19 -apply (subst sublist'_update2)
    1.20 -apply fastsimp
    1.21 -apply simp
    1.22 -done
    1.23 -
    1.24 -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]"
    1.25 -unfolding subarray_def Heap.upd_def
    1.26 -by (simp add: sublist'_update3)
    1.27 -
    1.28 -lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
    1.29 -by (simp add: subarray_def sublist'_Nil')
    1.30 -
    1.31 -lemma subarray_single: "\<lbrakk> n < Heap.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]" 
    1.32 -by (simp add: subarray_def Heap.length_def sublist'_single)
    1.33 -
    1.34 -lemma length_subarray: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n"
    1.35 -by (simp add: subarray_def Heap.length_def length_sublist')
    1.36 -
    1.37 -lemma length_subarray_0: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m"
    1.38 -by (simp add: length_subarray)
    1.39 -
    1.40 -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"
    1.41 -unfolding Heap.length_def subarray_def
    1.42 -by (simp add: sublist'_front)
    1.43 -
    1.44 -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)]"
    1.45 -unfolding Heap.length_def subarray_def
    1.46 -by (simp add: sublist'_back)
    1.47 -
    1.48 -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"
    1.49 -unfolding subarray_def
    1.50 -by (simp add: sublist'_append)
    1.51 -
    1.52 -lemma subarray_all: "subarray 0 (Heap.length a h) a h = get_array a h"
    1.53 -unfolding Heap.length_def subarray_def
    1.54 -by (simp add: sublist'_all)
    1.55 -
    1.56 -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)"
    1.57 -unfolding Heap.length_def subarray_def
    1.58 -by (simp add: nth_sublist')
    1.59 -
    1.60 -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')"
    1.61 -unfolding Heap.length_def subarray_def by (rule sublist'_eq_samelength_iff)
    1.62 -
    1.63 -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))"
    1.64 -unfolding subarray_def Heap.length_def by (rule all_in_set_sublist'_conv)
    1.65 -
    1.66 -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))"
    1.67 -unfolding subarray_def Heap.length_def by (rule ball_in_set_sublist'_conv)
    1.68 -
    1.69 -end
    1.70 \ No newline at end of file