src/HOL/Imperative_HOL/ex/Subarray.thy
changeset 37805 0f797d586ce5
parent 37802 f2e9c104cebd
child 37806 a7679be14442
     1.1 --- a/src/HOL/Imperative_HOL/ex/Subarray.thy	Tue Jul 13 16:00:56 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Subarray.thy	Tue Jul 13 16:12:40 2010 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  begin
     1.5  
     1.6  definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" where
     1.7 -  "subarray n m a h \<equiv> sublist' n m (get_array a h)"
     1.8 +  "subarray n m a h \<equiv> sublist' n m (get_array h a)"
     1.9  
    1.10  lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
    1.11  apply (simp add: subarray_def Array.update_def)
    1.12 @@ -30,7 +30,7 @@
    1.13  lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
    1.14  by (simp add: subarray_def sublist'_Nil')
    1.15  
    1.16 -lemma subarray_single: "\<lbrakk> n < Array.length h a \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]" 
    1.17 +lemma subarray_single: "\<lbrakk> n < Array.length h a \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array h a ! n]" 
    1.18  by (simp add: subarray_def length_def sublist'_single)
    1.19  
    1.20  lemma length_subarray: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray n m a h) = m - n"
    1.21 @@ -39,11 +39,11 @@
    1.22  lemma length_subarray_0: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray 0 m a h) = m"
    1.23  by (simp add: length_subarray)
    1.24  
    1.25 -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"
    1.26 +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"
    1.27  unfolding Array.length_def subarray_def
    1.28  by (simp add: sublist'_front)
    1.29  
    1.30 -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)]"
    1.31 +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)]"
    1.32  unfolding Array.length_def subarray_def
    1.33  by (simp add: sublist'_back)
    1.34  
    1.35 @@ -51,21 +51,21 @@
    1.36  unfolding subarray_def
    1.37  by (simp add: sublist'_append)
    1.38  
    1.39 -lemma subarray_all: "subarray 0 (Array.length h a) a h = get_array a h"
    1.40 +lemma subarray_all: "subarray 0 (Array.length h a) a h = get_array h a"
    1.41  unfolding Array.length_def subarray_def
    1.42  by (simp add: sublist'_all)
    1.43  
    1.44 -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)"
    1.45 +lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Array.length h a \<rbrakk> \<Longrightarrow> subarray i j a h ! k = get_array h a ! (i + k)"
    1.46  unfolding Array.length_def subarray_def
    1.47  by (simp add: nth_sublist')
    1.48  
    1.49 -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')"
    1.50 +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 h a ! i' = get_array h' a ! i')"
    1.51  unfolding Array.length_def subarray_def by (rule sublist'_eq_samelength_iff)
    1.52  
    1.53 -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))"
    1.54 +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 h a ! k))"
    1.55  unfolding subarray_def Array.length_def by (rule all_in_set_sublist'_conv)
    1.56  
    1.57 -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))"
    1.58 +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 h a ! k))"
    1.59  unfolding subarray_def Array.length_def by (rule ball_in_set_sublist'_conv)
    1.60  
    1.61  end
    1.62 \ No newline at end of file