author | haftmann |
Mon, 05 Jul 2010 16:46:23 +0200 | |
changeset 37719 | 271ecd4fb9f9 |
parent 37716 | 24bb91462892 |
child 37752 | d0a384c84d69 |
permissions | -rw-r--r-- |
31870 | 1 |
(* Title: HOL/Imperative_HOL/Array.thy |
26170 | 2 |
Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen |
3 |
*) |
|
4 |
||
5 |
header {* Monadic arrays *} |
|
6 |
||
7 |
theory Array |
|
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
29822
diff
changeset
|
8 |
imports Heap_Monad |
26170 | 9 |
begin |
10 |
||
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
11 |
subsection {* Primitive layer *} |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
12 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
13 |
definition |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
14 |
array_present :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> bool" where |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
15 |
"array_present a h \<longleftrightarrow> addr_of_array a < lim h" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
16 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
17 |
definition |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
18 |
get_array :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> 'a list" where |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
19 |
"get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
20 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
21 |
definition |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
22 |
set_array :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
23 |
"set_array a x = |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
24 |
arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
25 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
26 |
definition array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
27 |
"array xs h = (let |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
28 |
l = lim h; |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
29 |
r = Array l; |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
30 |
h'' = set_array r xs (h\<lparr>lim := l + 1\<rparr>) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
31 |
in (r, h''))" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
32 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
33 |
definition length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
34 |
"length a h = List.length (get_array a h)" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
35 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
36 |
definition change :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
37 |
"change a i x h = set_array a ((get_array a h)[i:=x]) h" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
38 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
39 |
text {* Properties of imperative arrays *} |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
40 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
41 |
text {* FIXME: Does there exist a "canonical" array axiomatisation in |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
42 |
the literature? *} |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
43 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
44 |
definition noteq_arrs :: "('a\<Colon>heap) array \<Rightarrow> ('b\<Colon>heap) array \<Rightarrow> bool" (infix "=!!=" 70) where |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
45 |
"r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
46 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
47 |
lemma noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
48 |
and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
49 |
unfolding noteq_arrs_def by auto |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
50 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
51 |
lemma noteq_arrs_irrefl: "r =!!= r \<Longrightarrow> False" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
52 |
unfolding noteq_arrs_def by auto |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
53 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
54 |
lemma present_new_arr: "array_present a h \<Longrightarrow> a =!!= fst (array xs h)" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
55 |
by (simp add: array_present_def noteq_arrs_def array_def Let_def) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
56 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
57 |
lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
58 |
by (simp add: get_array_def set_array_def o_def) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
59 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
60 |
lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
61 |
by (simp add: noteq_arrs_def get_array_def set_array_def) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
62 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
63 |
lemma set_array_same [simp]: |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
64 |
"set_array r x (set_array r y h) = set_array r x h" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
65 |
by (simp add: set_array_def) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
66 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
67 |
lemma array_set_set_swap: |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
68 |
"r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
69 |
by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
70 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
71 |
lemma get_array_change_eq [simp]: |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
72 |
"get_array a (change a i v h) = (get_array a h) [i := v]" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
73 |
by (simp add: change_def) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
74 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
75 |
lemma nth_change_array_neq_array [simp]: |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
76 |
"a =!!= b \<Longrightarrow> get_array a (change b j v h) ! i = get_array a h ! i" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
77 |
by (simp add: change_def noteq_arrs_def) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
78 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
79 |
lemma get_arry_array_change_elem_neqIndex [simp]: |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
80 |
"i \<noteq> j \<Longrightarrow> get_array a (change a j v h) ! i = get_array a h ! i" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
81 |
by simp |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
82 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
83 |
lemma length_change [simp]: |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
84 |
"length a (change b i v h) = length a h" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
85 |
by (simp add: change_def length_def set_array_def get_array_def) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
86 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
87 |
lemma change_swap_neqArray: |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
88 |
"a =!!= a' \<Longrightarrow> |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
89 |
change a i v (change a' i' v' h) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
90 |
= change a' i' v' (change a i v h)" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
91 |
apply (unfold change_def) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
92 |
apply simp |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
93 |
apply (subst array_set_set_swap, assumption) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
94 |
apply (subst array_get_set_neq) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
95 |
apply (erule noteq_arrs_sym) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
96 |
apply (simp) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
97 |
done |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
98 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
99 |
lemma change_swap_neqIndex: |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
100 |
"\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> change a i v (change a i' v' h) = change a i' v' (change a i v h)" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
101 |
by (auto simp add: change_def array_set_set_swap list_update_swap) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
102 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
103 |
lemma get_array_init_array_list: |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
104 |
"get_array (fst (array ls h)) (snd (array ls' h)) = ls'" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
105 |
by (simp add: Let_def split_def array_def) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
106 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
107 |
lemma set_array: |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
108 |
"set_array (fst (array ls h)) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
109 |
new_ls (snd (array ls h)) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
110 |
= snd (array new_ls h)" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
111 |
by (simp add: Let_def split_def array_def) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
112 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
113 |
lemma array_present_change [simp]: |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
114 |
"array_present a (change b i v h) = array_present a h" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
115 |
by (simp add: change_def array_present_def set_array_def get_array_def) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
116 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
117 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
118 |
|
26170 | 119 |
subsection {* Primitives *} |
120 |
||
121 |
definition |
|
122 |
new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
123 |
[code del]: "new n x = Heap_Monad.heap (Array.array (replicate n x))" |
26170 | 124 |
|
125 |
definition |
|
126 |
of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
127 |
[code del]: "of_list xs = Heap_Monad.heap (Array.array xs)" |
26170 | 128 |
|
129 |
definition |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
130 |
len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
131 |
[code del]: "len arr = Heap_Monad.heap (\<lambda>h. (Array.length arr h, h))" |
26170 | 132 |
|
133 |
definition |
|
134 |
nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap" |
|
135 |
where |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
136 |
[code del]: "nth a i = (do len \<leftarrow> len a; |
26170 | 137 |
(if i < len |
138 |
then Heap_Monad.heap (\<lambda>h. (get_array a h ! i, h)) |
|
37709 | 139 |
else raise ''array lookup: index out of range'') |
26170 | 140 |
done)" |
141 |
||
142 |
definition |
|
143 |
upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" |
|
144 |
where |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
145 |
[code del]: "upd i x a = (do len \<leftarrow> len a; |
26170 | 146 |
(if i < len |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
147 |
then Heap_Monad.heap (\<lambda>h. (a, change a i x h)) |
37709 | 148 |
else raise ''array update: index out of range'') |
26170 | 149 |
done)" |
150 |
||
151 |
lemma upd_return: |
|
152 |
"upd i x a \<guillemotright> return a = upd i x a" |
|
37709 | 153 |
by (rule Heap_eqI) (simp add: upd_def bindM_def split: option.split) |
26170 | 154 |
|
155 |
||
156 |
subsection {* Derivates *} |
|
157 |
||
158 |
definition |
|
159 |
map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" |
|
160 |
where |
|
161 |
"map_entry i f a = (do |
|
162 |
x \<leftarrow> nth a i; |
|
163 |
upd i (f x) a |
|
164 |
done)" |
|
165 |
||
166 |
definition |
|
167 |
swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap" |
|
168 |
where |
|
169 |
"swap i x a = (do |
|
170 |
y \<leftarrow> nth a i; |
|
171 |
upd i x a; |
|
27596 | 172 |
return y |
26170 | 173 |
done)" |
174 |
||
175 |
definition |
|
176 |
make :: "nat \<Rightarrow> (nat \<Rightarrow> 'a\<Colon>heap) \<Rightarrow> 'a array Heap" |
|
177 |
where |
|
178 |
"make n f = of_list (map f [0 ..< n])" |
|
179 |
||
180 |
definition |
|
181 |
freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" |
|
182 |
where |
|
183 |
"freeze a = (do |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
184 |
n \<leftarrow> len a; |
26170 | 185 |
mapM (nth a) [0..<n] |
186 |
done)" |
|
187 |
||
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
188 |
definition |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
189 |
map :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
190 |
where |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
191 |
"map f a = (do |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
192 |
n \<leftarrow> len a; |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
193 |
mapM (\<lambda>n. map_entry n f a) [0..<n]; |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
194 |
return a |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
195 |
done)" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
196 |
|
26170 | 197 |
|
198 |
||
199 |
subsection {* Properties *} |
|
200 |
||
28562 | 201 |
lemma array_make [code]: |
26170 | 202 |
"Array.new n x = make n (\<lambda>_. x)" |
37716
24bb91462892
remove primitive operation Heap.array in favour of Heap.array_of_list
haftmann
parents:
37709
diff
changeset
|
203 |
by (rule Heap_eqI) (simp add: make_def new_def map_replicate_trivial of_list_def) |
26170 | 204 |
|
28562 | 205 |
lemma array_of_list_make [code]: |
26170 | 206 |
"of_list xs = make (List.length xs) (\<lambda>n. xs ! n)" |
37709 | 207 |
by (rule Heap_eqI) (simp add: make_def map_nth) |
26170 | 208 |
|
26182 | 209 |
|
210 |
subsection {* Code generator setup *} |
|
211 |
||
212 |
subsubsection {* Logical intermediate layer *} |
|
213 |
||
214 |
definition new' where |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
215 |
[code del]: "new' = Array.new o Code_Numeral.nat_of" |
36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents:
35846
diff
changeset
|
216 |
hide_const (open) new' |
28562 | 217 |
lemma [code]: |
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
218 |
"Array.new = Array.new' o Code_Numeral.of_nat" |
26182 | 219 |
by (simp add: new'_def o_def) |
220 |
||
221 |
definition of_list' where |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
222 |
[code del]: "of_list' i xs = Array.of_list (take (Code_Numeral.nat_of i) xs)" |
36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents:
35846
diff
changeset
|
223 |
hide_const (open) of_list' |
28562 | 224 |
lemma [code]: |
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
225 |
"Array.of_list xs = Array.of_list' (Code_Numeral.of_nat (List.length xs)) xs" |
26182 | 226 |
by (simp add: of_list'_def) |
227 |
||
228 |
definition make' where |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
229 |
[code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)" |
36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents:
35846
diff
changeset
|
230 |
hide_const (open) make' |
28562 | 231 |
lemma [code]: |
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
232 |
"Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)" |
26182 | 233 |
by (simp add: make'_def o_def) |
234 |
||
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
235 |
definition len' where |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
236 |
[code del]: "len' a = Array.len a \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
237 |
hide_const (open) len' |
28562 | 238 |
lemma [code]: |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
239 |
"Array.len a = Array.len' a \<guillemotright>= (\<lambda>i. return (Code_Numeral.nat_of i))" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
240 |
by (simp add: len'_def) |
26182 | 241 |
|
242 |
definition nth' where |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
243 |
[code del]: "nth' a = Array.nth a o Code_Numeral.nat_of" |
36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents:
35846
diff
changeset
|
244 |
hide_const (open) nth' |
28562 | 245 |
lemma [code]: |
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
246 |
"Array.nth a n = Array.nth' a (Code_Numeral.of_nat n)" |
26182 | 247 |
by (simp add: nth'_def) |
248 |
||
249 |
definition upd' where |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
250 |
[code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \<guillemotright> return ()" |
36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents:
35846
diff
changeset
|
251 |
hide_const (open) upd' |
28562 | 252 |
lemma [code]: |
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
253 |
"Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a" |
37709 | 254 |
by (simp add: upd'_def upd_return) |
26182 | 255 |
|
256 |
||
257 |
subsubsection {* SML *} |
|
258 |
||
259 |
code_type array (SML "_/ array") |
|
260 |
code_const Array (SML "raise/ (Fail/ \"bare Array\")") |
|
26752 | 261 |
code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))") |
35846 | 262 |
code_const Array.of_list' (SML "(fn/ ()/ =>/ Array.fromList/ _)") |
26752 | 263 |
code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))") |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
264 |
code_const Array.len' (SML "(fn/ ()/ =>/ Array.length/ _)") |
26752 | 265 |
code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))") |
266 |
code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))") |
|
26182 | 267 |
|
268 |
code_reserved SML Array |
|
269 |
||
270 |
||
271 |
subsubsection {* OCaml *} |
|
272 |
||
273 |
code_type array (OCaml "_/ array") |
|
274 |
code_const Array (OCaml "failwith/ \"bare Array\"") |
|
32580 | 275 |
code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)") |
35846 | 276 |
code_const Array.of_list' (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)") |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
277 |
code_const Array.len' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))") |
32580 | 278 |
code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))") |
279 |
code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)") |
|
26182 | 280 |
|
281 |
code_reserved OCaml Array |
|
282 |
||
283 |
||
284 |
subsubsection {* Haskell *} |
|
285 |
||
29793 | 286 |
code_type array (Haskell "Heap.STArray/ Heap.RealWorld/ _") |
26182 | 287 |
code_const Array (Haskell "error/ \"bare Array\"") |
29793 | 288 |
code_const Array.new' (Haskell "Heap.newArray/ (0,/ _)") |
289 |
code_const Array.of_list' (Haskell "Heap.newListArray/ (0,/ _)") |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
290 |
code_const Array.len' (Haskell "Heap.lengthArray") |
29793 | 291 |
code_const Array.nth' (Haskell "Heap.readArray") |
292 |
code_const Array.upd' (Haskell "Heap.writeArray") |
|
26182 | 293 |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
294 |
hide_const (open) new map -- {* avoid clashed with some popular names *} |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
295 |
|
26170 | 296 |
end |