author | haftmann |
Fri, 09 Jul 2010 16:58:44 +0200 | |
changeset 37758 | bf86a65403a8 |
parent 37756 | 59caa6180fff |
child 37771 | 1bec64044b5e |
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 |
||
37752 | 11 |
subsection {* Primitives *} |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
12 |
|
37752 | 13 |
definition (*FIXME present :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> bool" where*) |
37719
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 |
|
37752 | 17 |
definition (*FIXME get :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a list" where*) |
37719
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 |
|
37752 | 21 |
definition (*FIXME set*) |
37719
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 |
|
37752 | 26 |
definition (*FIXME alloc*) |
27 |
array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
28 |
"array xs h = (let |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
29 |
l = lim h; |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
30 |
r = Array l; |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
31 |
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
|
32 |
in (r, h''))" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
33 |
|
37752 | 34 |
definition (*FIXME length :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> nat" where*) |
35 |
length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
36 |
"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
|
37 |
|
37752 | 38 |
definition (*FIXME update*) |
39 |
change :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
40 |
"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
|
41 |
|
37752 | 42 |
definition (*FIXME noteq*) |
43 |
noteq_arrs :: "'a\<Colon>heap array \<Rightarrow> 'b\<Colon>heap array \<Rightarrow> bool" (infix "=!!=" 70) where |
|
44 |
"r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s" |
|
45 |
||
46 |
||
47 |
subsection {* Monad operations *} |
|
48 |
||
49 |
definition new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where |
|
50 |
[code del]: "new n x = Heap_Monad.heap (array (replicate n x))" |
|
51 |
||
52 |
definition of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where |
|
53 |
[code del]: "of_list xs = Heap_Monad.heap (array xs)" |
|
54 |
||
55 |
definition make :: "nat \<Rightarrow> (nat \<Rightarrow> 'a\<Colon>heap) \<Rightarrow> 'a array Heap" where |
|
56 |
[code del]: "make n f = Heap_Monad.heap (array (map f [0 ..< n]))" |
|
57 |
||
58 |
definition len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where |
|
37758 | 59 |
[code del]: "len a = Heap_Monad.tap (\<lambda>h. length a h)" |
37752 | 60 |
|
61 |
definition nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap" where |
|
62 |
[code del]: "nth a i = Heap_Monad.guard (\<lambda>h. i < length a h) |
|
63 |
(\<lambda>h. (get_array a h ! i, h))" |
|
64 |
||
65 |
definition upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" where |
|
66 |
[code del]: "upd i x a = Heap_Monad.guard (\<lambda>h. i < length a h) |
|
67 |
(\<lambda>h. (a, change a i x h))" |
|
68 |
||
69 |
definition map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" where |
|
70 |
[code del]: "map_entry i f a = Heap_Monad.guard (\<lambda>h. i < length a h) |
|
71 |
(\<lambda>h. (a, change a i (f (get_array a h ! i)) h))" |
|
72 |
||
73 |
definition swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap" where |
|
74 |
[code del]: "swap i x a = Heap_Monad.guard (\<lambda>h. i < length a h) |
|
75 |
(\<lambda>h. (get_array a h ! i, change a i x h))" |
|
76 |
||
77 |
definition freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" where |
|
37758 | 78 |
[code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get_array a h)" |
37752 | 79 |
|
80 |
||
81 |
subsection {* Properties *} |
|
37719
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 |
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
|
84 |
the literature? *} |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
85 |
|
37758 | 86 |
text {* Primitives *} |
87 |
||
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
88 |
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
|
89 |
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
|
90 |
unfolding noteq_arrs_def by auto |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
91 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
92 |
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
|
93 |
unfolding noteq_arrs_def by auto |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
94 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
95 |
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
|
96 |
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
|
97 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
98 |
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
|
99 |
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
|
100 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
101 |
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
|
102 |
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
|
103 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
104 |
lemma set_array_same [simp]: |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
105 |
"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
|
106 |
by (simp add: set_array_def) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
107 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
108 |
lemma array_set_set_swap: |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
109 |
"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
|
110 |
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
|
111 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
112 |
lemma get_array_change_eq [simp]: |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
113 |
"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
|
114 |
by (simp add: change_def) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
115 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
116 |
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
|
117 |
"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
|
118 |
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
|
119 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
120 |
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
|
121 |
"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
|
122 |
by simp |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
123 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
124 |
lemma length_change [simp]: |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
125 |
"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
|
126 |
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
|
127 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
128 |
lemma change_swap_neqArray: |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
129 |
"a =!!= a' \<Longrightarrow> |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
130 |
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
|
131 |
= 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
|
132 |
apply (unfold change_def) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
133 |
apply simp |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
134 |
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
|
135 |
apply (subst array_get_set_neq) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
136 |
apply (erule noteq_arrs_sym) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
137 |
apply (simp) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
138 |
done |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
139 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
140 |
lemma change_swap_neqIndex: |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
141 |
"\<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
|
142 |
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
|
143 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
144 |
lemma get_array_init_array_list: |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
145 |
"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
|
146 |
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
|
147 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
148 |
lemma set_array: |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
149 |
"set_array (fst (array ls h)) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
150 |
new_ls (snd (array ls h)) |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
151 |
= snd (array new_ls h)" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
152 |
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
|
153 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
154 |
lemma array_present_change [simp]: |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
155 |
"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
|
156 |
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
|
157 |
|
37758 | 158 |
|
159 |
text {* Monad operations *} |
|
160 |
||
161 |
lemma execute_new [simp, execute_simps]: |
|
162 |
"execute (new n x) h = Some (array (replicate n x) h)" |
|
163 |
by (simp add: new_def) |
|
164 |
||
165 |
lemma success_newI [iff, success_intros]: |
|
166 |
"success (new n x) h" |
|
37752 | 167 |
by (simp add: new_def) |
26170 | 168 |
|
37758 | 169 |
lemma execute_of_list [simp, execute_simps]: |
170 |
"execute (of_list xs) h = Some (array xs h)" |
|
171 |
by (simp add: of_list_def) |
|
172 |
||
173 |
lemma success_of_listI [iff, success_intros]: |
|
174 |
"success (of_list xs) h" |
|
37752 | 175 |
by (simp add: of_list_def) |
26170 | 176 |
|
37758 | 177 |
lemma execute_make [simp, execute_simps]: |
178 |
"execute (make n f) h = Some (array (map f [0 ..< n]) h)" |
|
37752 | 179 |
by (simp add: make_def) |
26170 | 180 |
|
37758 | 181 |
lemma success_makeI [iff, success_intros]: |
182 |
"success (make n f) h" |
|
183 |
by (simp add: make_def) |
|
184 |
||
185 |
lemma execute_len [simp, execute_simps]: |
|
186 |
"execute (len a) h = Some (length a h, h)" |
|
187 |
by (simp add: len_def) |
|
188 |
||
189 |
lemma success_lenI [iff, success_intros]: |
|
190 |
"success (len a) h" |
|
37752 | 191 |
by (simp add: len_def) |
192 |
||
37758 | 193 |
lemma execute_nth [execute_simps]: |
37752 | 194 |
"i < length a h \<Longrightarrow> |
37758 | 195 |
execute (nth a i) h = Some (get_array a h ! i, h)" |
196 |
"i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None" |
|
197 |
by (simp_all add: nth_def execute_simps) |
|
198 |
||
199 |
lemma success_nthI [success_intros]: |
|
200 |
"i < length a h \<Longrightarrow> success (nth a i) h" |
|
201 |
by (auto intro: success_intros simp add: nth_def) |
|
26170 | 202 |
|
37758 | 203 |
lemma execute_upd [execute_simps]: |
37752 | 204 |
"i < length a h \<Longrightarrow> |
37758 | 205 |
execute (upd i x a) h = Some (a, change a i x h)" |
206 |
"i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None" |
|
207 |
by (simp_all add: upd_def execute_simps) |
|
26170 | 208 |
|
37758 | 209 |
lemma success_updI [success_intros]: |
210 |
"i < length a h \<Longrightarrow> success (upd i x a) h" |
|
211 |
by (auto intro: success_intros simp add: upd_def) |
|
212 |
||
213 |
lemma execute_map_entry [execute_simps]: |
|
37752 | 214 |
"i < length a h \<Longrightarrow> |
37758 | 215 |
execute (map_entry i f a) h = |
37752 | 216 |
Some (a, change a i (f (get_array a h ! i)) h)" |
37758 | 217 |
"i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None" |
218 |
by (simp_all add: map_entry_def execute_simps) |
|
37752 | 219 |
|
37758 | 220 |
lemma success_map_entryI [success_intros]: |
221 |
"i < length a h \<Longrightarrow> success (map_entry i f a) h" |
|
222 |
by (auto intro: success_intros simp add: map_entry_def) |
|
223 |
||
224 |
lemma execute_swap [execute_simps]: |
|
37752 | 225 |
"i < length a h \<Longrightarrow> |
37758 | 226 |
execute (swap i x a) h = |
37752 | 227 |
Some (get_array a h ! i, change a i x h)" |
37758 | 228 |
"i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None" |
229 |
by (simp_all add: swap_def execute_simps) |
|
230 |
||
231 |
lemma success_swapI [success_intros]: |
|
232 |
"i < length a h \<Longrightarrow> success (swap i x a) h" |
|
233 |
by (auto intro: success_intros simp add: swap_def) |
|
37752 | 234 |
|
37758 | 235 |
lemma execute_freeze [simp, execute_simps]: |
236 |
"execute (freeze a) h = Some (get_array a h, h)" |
|
237 |
by (simp add: freeze_def) |
|
238 |
||
239 |
lemma success_freezeI [iff, success_intros]: |
|
240 |
"success (freeze a) h" |
|
37752 | 241 |
by (simp add: freeze_def) |
26170 | 242 |
|
243 |
lemma upd_return: |
|
244 |
"upd i x a \<guillemotright> return a = upd i x a" |
|
37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37752
diff
changeset
|
245 |
by (rule Heap_eqI) (simp add: bind_def guard_def upd_def) |
26170 | 246 |
|
37752 | 247 |
lemma array_make: |
248 |
"new n x = make n (\<lambda>_. x)" |
|
249 |
by (rule Heap_eqI) (simp add: map_replicate_trivial) |
|
26170 | 250 |
|
37752 | 251 |
lemma array_of_list_make: |
252 |
"of_list xs = make (List.length xs) (\<lambda>n. xs ! n)" |
|
253 |
by (rule Heap_eqI) (simp add: map_nth) |
|
26170 | 254 |
|
37752 | 255 |
hide_const (open) new map |
26170 | 256 |
|
26182 | 257 |
|
258 |
subsection {* Code generator setup *} |
|
259 |
||
260 |
subsubsection {* Logical intermediate layer *} |
|
261 |
||
262 |
definition new' where |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
263 |
[code del]: "new' = Array.new o Code_Numeral.nat_of" |
37752 | 264 |
|
28562 | 265 |
lemma [code]: |
37752 | 266 |
"Array.new = new' o Code_Numeral.of_nat" |
26182 | 267 |
by (simp add: new'_def o_def) |
268 |
||
269 |
definition of_list' where |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
270 |
[code del]: "of_list' i xs = Array.of_list (take (Code_Numeral.nat_of i) xs)" |
37752 | 271 |
|
28562 | 272 |
lemma [code]: |
37752 | 273 |
"Array.of_list xs = of_list' (Code_Numeral.of_nat (List.length xs)) xs" |
26182 | 274 |
by (simp add: of_list'_def) |
275 |
||
276 |
definition make' where |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
277 |
[code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)" |
37752 | 278 |
|
28562 | 279 |
lemma [code]: |
37752 | 280 |
"Array.make n f = make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)" |
26182 | 281 |
by (simp add: make'_def o_def) |
282 |
||
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
283 |
definition len' where |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
284 |
[code del]: "len' a = Array.len a \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))" |
37752 | 285 |
|
28562 | 286 |
lemma [code]: |
37752 | 287 |
"Array.len a = len' a \<guillemotright>= (\<lambda>i. return (Code_Numeral.nat_of i))" |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
288 |
by (simp add: len'_def) |
26182 | 289 |
|
290 |
definition nth' where |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
291 |
[code del]: "nth' a = Array.nth a o Code_Numeral.nat_of" |
37752 | 292 |
|
28562 | 293 |
lemma [code]: |
37752 | 294 |
"Array.nth a n = nth' a (Code_Numeral.of_nat n)" |
26182 | 295 |
by (simp add: nth'_def) |
296 |
||
297 |
definition upd' where |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
298 |
[code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \<guillemotright> return ()" |
37752 | 299 |
|
28562 | 300 |
lemma [code]: |
37752 | 301 |
"Array.upd i x a = upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a" |
37709 | 302 |
by (simp add: upd'_def upd_return) |
26182 | 303 |
|
37752 | 304 |
lemma [code]: |
305 |
"map_entry i f a = (do |
|
306 |
x \<leftarrow> nth a i; |
|
307 |
upd i (f x) a |
|
308 |
done)" |
|
37758 | 309 |
by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def execute_simps) |
26182 | 310 |
|
37752 | 311 |
lemma [code]: |
312 |
"swap i x a = (do |
|
313 |
y \<leftarrow> nth a i; |
|
314 |
upd i x a; |
|
315 |
return y |
|
316 |
done)" |
|
37758 | 317 |
by (rule Heap_eqI) (simp add: bind_def guard_def swap_def execute_simps) |
37752 | 318 |
|
319 |
lemma [code]: |
|
320 |
"freeze a = (do |
|
321 |
n \<leftarrow> len a; |
|
37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37752
diff
changeset
|
322 |
Heap_Monad.fold_map (\<lambda>i. nth a i) [0..<n] |
37752 | 323 |
done)" |
324 |
proof (rule Heap_eqI) |
|
325 |
fix h |
|
326 |
have *: "List.map |
|
327 |
(\<lambda>x. fst (the (if x < length a h |
|
328 |
then Some (get_array a h ! x, h) else None))) |
|
329 |
[0..<length a h] = |
|
330 |
List.map (List.nth (get_array a h)) [0..<length a h]" |
|
331 |
by simp |
|
37758 | 332 |
have "execute (Heap_Monad.fold_map (Array.nth a) [0..<length a h]) h = |
37752 | 333 |
Some (get_array a h, h)" |
37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37752
diff
changeset
|
334 |
apply (subst execute_fold_map_unchanged_heap) |
37752 | 335 |
apply (simp_all add: nth_def guard_def *) |
336 |
apply (simp add: length_def map_nth) |
|
337 |
done |
|
37758 | 338 |
then have "execute (do |
37752 | 339 |
n \<leftarrow> len a; |
37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37752
diff
changeset
|
340 |
Heap_Monad.fold_map (Array.nth a) [0..<n] |
37752 | 341 |
done) h = Some (get_array a h, h)" |
342 |
by (auto intro: execute_eq_SomeI) |
|
37758 | 343 |
then show "execute (freeze a) h = execute (do |
37752 | 344 |
n \<leftarrow> len a; |
37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37752
diff
changeset
|
345 |
Heap_Monad.fold_map (Array.nth a) [0..<n] |
37752 | 346 |
done) h" by simp |
347 |
qed |
|
348 |
||
349 |
hide_const (open) new' of_list' make' len' nth' upd' |
|
350 |
||
351 |
||
352 |
text {* SML *} |
|
26182 | 353 |
|
354 |
code_type array (SML "_/ array") |
|
355 |
code_const Array (SML "raise/ (Fail/ \"bare Array\")") |
|
26752 | 356 |
code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))") |
35846 | 357 |
code_const Array.of_list' (SML "(fn/ ()/ =>/ Array.fromList/ _)") |
26752 | 358 |
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
|
359 |
code_const Array.len' (SML "(fn/ ()/ =>/ Array.length/ _)") |
26752 | 360 |
code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))") |
361 |
code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))") |
|
26182 | 362 |
|
363 |
code_reserved SML Array |
|
364 |
||
365 |
||
37752 | 366 |
text {* OCaml *} |
26182 | 367 |
|
368 |
code_type array (OCaml "_/ array") |
|
369 |
code_const Array (OCaml "failwith/ \"bare Array\"") |
|
32580 | 370 |
code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)") |
35846 | 371 |
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
|
372 |
code_const Array.len' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))") |
32580 | 373 |
code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))") |
374 |
code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)") |
|
26182 | 375 |
|
376 |
code_reserved OCaml Array |
|
377 |
||
378 |
||
37752 | 379 |
text {* Haskell *} |
26182 | 380 |
|
29793 | 381 |
code_type array (Haskell "Heap.STArray/ Heap.RealWorld/ _") |
26182 | 382 |
code_const Array (Haskell "error/ \"bare Array\"") |
29793 | 383 |
code_const Array.new' (Haskell "Heap.newArray/ (0,/ _)") |
384 |
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
|
385 |
code_const Array.len' (Haskell "Heap.lengthArray") |
29793 | 386 |
code_const Array.nth' (Haskell "Heap.readArray") |
387 |
code_const Array.upd' (Haskell "Heap.writeArray") |
|
26182 | 388 |
|
26170 | 389 |
end |