author | haftmann |
Fri, 23 Jul 2010 10:58:13 +0200 | |
changeset 37947 | 844977c7abeb |
parent 37806 | a7679be14442 |
child 44890 | 22f665a2e91c |
permissions | -rw-r--r-- |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
30689
diff
changeset
|
1 |
(* Title: HOL/Imperative_HOL/ex/Subarray.thy |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
30689
diff
changeset
|
2 |
Author: Lukas Bulwahn, TU Muenchen |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
30689
diff
changeset
|
3 |
*) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
30689
diff
changeset
|
4 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
30689
diff
changeset
|
5 |
header {* Theorems about sub arrays *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
30689
diff
changeset
|
6 |
|
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
7 |
theory Subarray |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
8 |
imports Array Sublist |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
9 |
begin |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
10 |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36098
diff
changeset
|
11 |
definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" where |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
12 |
"subarray n m a h \<equiv> sublist' n m (Array.get h a)" |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
13 |
|
37796 | 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) |
|
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
16 |
apply (simp add: sublist'_update1) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
17 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
18 |
|
37796 | 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) |
|
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
21 |
apply (subst sublist'_update2) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
22 |
apply fastsimp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
23 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
24 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
25 |
|
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]" |
27 |
unfolding subarray_def Array.update_def |
|
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
28 |
by (simp add: sublist'_update3) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
29 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
30 |
lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
31 |
by (simp add: subarray_def sublist'_Nil') |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
32 |
|
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
33 |
lemma subarray_single: "\<lbrakk> n < Array.length h a \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [Array.get h a ! n]" |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36098
diff
changeset
|
34 |
by (simp add: subarray_def length_def sublist'_single) |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
35 |
|
37802 | 36 |
lemma length_subarray: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray n m a h) = m - n" |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36098
diff
changeset
|
37 |
by (simp add: subarray_def length_def length_sublist') |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
38 |
|
37802 | 39 |
lemma length_subarray_0: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray 0 m a h) = m" |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
40 |
by (simp add: length_subarray) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
41 |
|
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
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" |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36098
diff
changeset
|
43 |
unfolding Array.length_def subarray_def |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
44 |
by (simp add: sublist'_front) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
45 |
|
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
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)]" |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36098
diff
changeset
|
47 |
unfolding Array.length_def subarray_def |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
48 |
by (simp add: sublist'_back) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
49 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
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" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
51 |
unfolding subarray_def |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
52 |
by (simp add: sublist'_append) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
53 |
|
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
54 |
lemma subarray_all: "subarray 0 (Array.length h a) a h = Array.get h a" |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36098
diff
changeset
|
55 |
unfolding Array.length_def subarray_def |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
56 |
by (simp add: sublist'_all) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
57 |
|
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
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)" |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36098
diff
changeset
|
59 |
unfolding Array.length_def subarray_def |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
60 |
by (simp add: nth_sublist') |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
61 |
|
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
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')" |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36098
diff
changeset
|
63 |
unfolding Array.length_def subarray_def by (rule sublist'_eq_samelength_iff) |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
64 |
|
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
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))" |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36098
diff
changeset
|
66 |
unfolding subarray_def Array.length_def by (rule all_in_set_sublist'_conv) |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
67 |
|
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
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))" |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36098
diff
changeset
|
69 |
unfolding subarray_def Array.length_def by (rule ball_in_set_sublist'_conv) |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
70 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
71 |
end |