src/HOL/Imperative_HOL/ex/Subarray.thy
author huffman
Sun Apr 01 16:09:58 2012 +0200 (2012-04-01)
changeset 47255 30a1692557b0
parent 47108 2a1953f0d20d
child 58889 5b7a9633cfa8
permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
bulwahn@36098
     1
(*  Title:      HOL/Imperative_HOL/ex/Subarray.thy
bulwahn@36098
     2
    Author:     Lukas Bulwahn, TU Muenchen
bulwahn@36098
     3
*)
bulwahn@36098
     4
bulwahn@36098
     5
header {* Theorems about sub arrays *}
bulwahn@36098
     6
bulwahn@27656
     7
theory Subarray
huffman@47108
     8
imports "~~/src/HOL/Imperative_HOL/Array" Sublist
bulwahn@27656
     9
begin
bulwahn@27656
    10
haftmann@37719
    11
definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" where
haftmann@37806
    12
  "subarray n m a h \<equiv> sublist' n m (Array.get h a)"
bulwahn@27656
    13
haftmann@37796
    14
lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
haftmann@37796
    15
apply (simp add: subarray_def Array.update_def)
bulwahn@27656
    16
apply (simp add: sublist'_update1)
bulwahn@27656
    17
done
bulwahn@27656
    18
haftmann@37796
    19
lemma subarray_upd2: " i < n  \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
haftmann@37796
    20
apply (simp add: subarray_def Array.update_def)
bulwahn@27656
    21
apply (subst sublist'_update2)
nipkow@44890
    22
apply fastforce
bulwahn@27656
    23
apply simp
bulwahn@27656
    24
done
bulwahn@27656
    25
haftmann@37796
    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]"
haftmann@37796
    27
unfolding subarray_def Array.update_def
bulwahn@27656
    28
by (simp add: sublist'_update3)
bulwahn@27656
    29
bulwahn@27656
    30
lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
bulwahn@27656
    31
by (simp add: subarray_def sublist'_Nil')
bulwahn@27656
    32
haftmann@37806
    33
lemma subarray_single: "\<lbrakk> n < Array.length h a \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [Array.get h a ! n]" 
haftmann@37719
    34
by (simp add: subarray_def length_def sublist'_single)
bulwahn@27656
    35
haftmann@37802
    36
lemma length_subarray: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray n m a h) = m - n"
haftmann@37719
    37
by (simp add: subarray_def length_def length_sublist')
bulwahn@27656
    38
haftmann@37802
    39
lemma length_subarray_0: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray 0 m a h) = m"
bulwahn@27656
    40
by (simp add: length_subarray)
bulwahn@27656
    41
haftmann@37806
    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"
haftmann@37719
    43
unfolding Array.length_def subarray_def
bulwahn@27656
    44
by (simp add: sublist'_front)
bulwahn@27656
    45
haftmann@37806
    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)]"
haftmann@37719
    47
unfolding Array.length_def subarray_def
bulwahn@27656
    48
by (simp add: sublist'_back)
bulwahn@27656
    49
bulwahn@27656
    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"
bulwahn@27656
    51
unfolding subarray_def
bulwahn@27656
    52
by (simp add: sublist'_append)
bulwahn@27656
    53
haftmann@37806
    54
lemma subarray_all: "subarray 0 (Array.length h a) a h = Array.get h a"
haftmann@37719
    55
unfolding Array.length_def subarray_def
bulwahn@27656
    56
by (simp add: sublist'_all)
bulwahn@27656
    57
haftmann@37806
    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)"
haftmann@37719
    59
unfolding Array.length_def subarray_def
bulwahn@27656
    60
by (simp add: nth_sublist')
bulwahn@27656
    61
haftmann@37806
    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')"
haftmann@37719
    63
unfolding Array.length_def subarray_def by (rule sublist'_eq_samelength_iff)
bulwahn@27656
    64
haftmann@37806
    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))"
haftmann@37719
    66
unfolding subarray_def Array.length_def by (rule all_in_set_sublist'_conv)
bulwahn@27656
    67
haftmann@37806
    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))"
haftmann@37719
    69
unfolding subarray_def Array.length_def by (rule ball_in_set_sublist'_conv)
bulwahn@27656
    70
bulwahn@27656
    71
end