src/HOL/Imperative_HOL/ex/Subarray.thy
author bulwahn
Thu Apr 08 08:17:27 2010 +0200 (2010-04-08 ago)
changeset 36098 53992c639da5
parent 30689 b14b2cc4e25e
child 37719 271ecd4fb9f9
permissions -rw-r--r--
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
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
bulwahn@27656
     8
imports Array Sublist
bulwahn@27656
     9
begin
bulwahn@27656
    10
bulwahn@27656
    11
definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list"
bulwahn@27656
    12
where
bulwahn@27656
    13
  "subarray n m a h \<equiv> sublist' n m (get_array a h)"
bulwahn@27656
    14
bulwahn@27656
    15
lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
bulwahn@27656
    16
apply (simp add: subarray_def Heap.upd_def)
bulwahn@27656
    17
apply (simp add: sublist'_update1)
bulwahn@27656
    18
done
bulwahn@27656
    19
bulwahn@27656
    20
lemma subarray_upd2: " i < n  \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
bulwahn@27656
    21
apply (simp add: subarray_def Heap.upd_def)
bulwahn@27656
    22
apply (subst sublist'_update2)
bulwahn@27656
    23
apply fastsimp
bulwahn@27656
    24
apply simp
bulwahn@27656
    25
done
bulwahn@27656
    26
bulwahn@27656
    27
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]"
bulwahn@27656
    28
unfolding subarray_def Heap.upd_def
bulwahn@27656
    29
by (simp add: sublist'_update3)
bulwahn@27656
    30
bulwahn@27656
    31
lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
bulwahn@27656
    32
by (simp add: subarray_def sublist'_Nil')
bulwahn@27656
    33
bulwahn@27656
    34
lemma subarray_single: "\<lbrakk> n < Heap.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]" 
bulwahn@27656
    35
by (simp add: subarray_def Heap.length_def sublist'_single)
bulwahn@27656
    36
bulwahn@27656
    37
lemma length_subarray: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n"
bulwahn@27656
    38
by (simp add: subarray_def Heap.length_def length_sublist')
bulwahn@27656
    39
bulwahn@27656
    40
lemma length_subarray_0: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m"
bulwahn@27656
    41
by (simp add: length_subarray)
bulwahn@27656
    42
bulwahn@27656
    43
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"
bulwahn@27656
    44
unfolding Heap.length_def subarray_def
bulwahn@27656
    45
by (simp add: sublist'_front)
bulwahn@27656
    46
bulwahn@27656
    47
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)]"
bulwahn@27656
    48
unfolding Heap.length_def subarray_def
bulwahn@27656
    49
by (simp add: sublist'_back)
bulwahn@27656
    50
bulwahn@27656
    51
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
    52
unfolding subarray_def
bulwahn@27656
    53
by (simp add: sublist'_append)
bulwahn@27656
    54
bulwahn@27656
    55
lemma subarray_all: "subarray 0 (Heap.length a h) a h = get_array a h"
bulwahn@27656
    56
unfolding Heap.length_def subarray_def
bulwahn@27656
    57
by (simp add: sublist'_all)
bulwahn@27656
    58
bulwahn@27656
    59
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)"
bulwahn@27656
    60
unfolding Heap.length_def subarray_def
bulwahn@27656
    61
by (simp add: nth_sublist')
bulwahn@27656
    62
bulwahn@27656
    63
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')"
bulwahn@27656
    64
unfolding Heap.length_def subarray_def by (rule sublist'_eq_samelength_iff)
bulwahn@27656
    65
bulwahn@27656
    66
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))"
bulwahn@27656
    67
unfolding subarray_def Heap.length_def by (rule all_in_set_sublist'_conv)
bulwahn@27656
    68
bulwahn@27656
    69
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))"
bulwahn@27656
    70
unfolding subarray_def Heap.length_def by (rule ball_in_set_sublist'_conv)
bulwahn@27656
    71
bulwahn@27656
    72
end