author | haftmann |
Mon, 27 Sep 2010 11:12:01 +0200 | |
changeset 39716 | d1c12f4ee9ac |
parent 39302 | d7728f65b353 |
child 40360 | 1a73b5b90a3c |
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 |
|
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
13 |
definition present :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> bool" where |
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
14 |
"present h a \<longleftrightarrow> addr_of_array a < lim h" |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
15 |
|
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
16 |
definition get :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a list" where |
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
17 |
"get h a = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))" |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
18 |
|
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
19 |
definition set :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where |
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
20 |
"set a x = arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))" |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
21 |
|
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
22 |
definition alloc :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where |
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
23 |
"alloc xs h = (let |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
24 |
l = lim h; |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
25 |
r = Array l; |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
26 |
h'' = set r xs (h\<lparr>lim := l + 1\<rparr>) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
27 |
in (r, h''))" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
28 |
|
37802 | 29 |
definition length :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> nat" where |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
30 |
"length h a = List.length (get h a)" |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
31 |
|
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
32 |
definition update :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
33 |
"update a i x h = set a ((get h a)[i:=x]) h" |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
34 |
|
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
35 |
definition noteq :: "'a\<Colon>heap array \<Rightarrow> 'b\<Colon>heap array \<Rightarrow> bool" (infix "=!!=" 70) where |
37752 | 36 |
"r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s" |
37 |
||
38 |
||
39 |
subsection {* Monad operations *} |
|
40 |
||
41 |
definition new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where |
|
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
42 |
[code del]: "new n x = Heap_Monad.heap (alloc (replicate n x))" |
37752 | 43 |
|
44 |
definition of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where |
|
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
45 |
[code del]: "of_list xs = Heap_Monad.heap (alloc xs)" |
37752 | 46 |
|
47 |
definition make :: "nat \<Rightarrow> (nat \<Rightarrow> 'a\<Colon>heap) \<Rightarrow> 'a array Heap" where |
|
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
48 |
[code del]: "make n f = Heap_Monad.heap (alloc (map f [0 ..< n]))" |
37752 | 49 |
|
50 |
definition len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where |
|
37802 | 51 |
[code del]: "len a = Heap_Monad.tap (\<lambda>h. length h a)" |
37752 | 52 |
|
53 |
definition nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap" where |
|
37802 | 54 |
[code del]: "nth a i = Heap_Monad.guard (\<lambda>h. i < length h a) |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
55 |
(\<lambda>h. (get h a ! i, h))" |
37752 | 56 |
|
57 |
definition upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" where |
|
37802 | 58 |
[code del]: "upd i x a = Heap_Monad.guard (\<lambda>h. i < length h a) |
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
59 |
(\<lambda>h. (a, update a i x h))" |
37752 | 60 |
|
61 |
definition map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" where |
|
37802 | 62 |
[code del]: "map_entry i f a = Heap_Monad.guard (\<lambda>h. i < length h a) |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
63 |
(\<lambda>h. (a, update a i (f (get h a ! i)) h))" |
37752 | 64 |
|
65 |
definition swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap" where |
|
37802 | 66 |
[code del]: "swap i x a = Heap_Monad.guard (\<lambda>h. i < length h a) |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
67 |
(\<lambda>h. (get h a ! i, update a i x h))" |
37752 | 68 |
|
69 |
definition freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" where |
|
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
70 |
[code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get h a)" |
37752 | 71 |
|
72 |
||
73 |
subsection {* Properties *} |
|
37719
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 |
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
|
76 |
the literature? *} |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
77 |
|
37758 | 78 |
text {* Primitives *} |
79 |
||
37807 | 80 |
lemma noteq_sym: "a =!!= b \<Longrightarrow> b =!!= a" |
81 |
and unequal [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'" |
|
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
82 |
unfolding noteq_def by auto |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
83 |
|
37807 | 84 |
lemma noteq_irrefl: "r =!!= r \<Longrightarrow> False" |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
85 |
unfolding noteq_def by auto |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
86 |
|
37807 | 87 |
lemma present_alloc_noteq: "present h a \<Longrightarrow> a =!!= fst (alloc xs h)" |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
88 |
by (simp add: present_def noteq_def alloc_def Let_def) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
89 |
|
37807 | 90 |
lemma get_set_eq [simp]: "get (set r x h) r = x" |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
91 |
by (simp add: get_def set_def o_def) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
92 |
|
37807 | 93 |
lemma get_set_neq [simp]: "r =!!= s \<Longrightarrow> get (set s x h) r = get h r" |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
94 |
by (simp add: noteq_def get_def set_def) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
95 |
|
37807 | 96 |
lemma set_same [simp]: |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
97 |
"set r x (set r y h) = set r x h" |
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
98 |
by (simp add: set_def) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
99 |
|
37807 | 100 |
lemma set_set_swap: |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
101 |
"r =!!= r' \<Longrightarrow> set r x (set r' x' h) = set r' x' (set r x h)" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
102 |
by (simp add: Let_def fun_eq_iff noteq_def set_def) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
103 |
|
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
104 |
lemma get_update_eq [simp]: |
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
105 |
"get (update a i v h) a = (get h a) [i := v]" |
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
106 |
by (simp add: update_def) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
107 |
|
37807 | 108 |
lemma nth_update_neq [simp]: |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
109 |
"a =!!= b \<Longrightarrow> get (update b j v h) a ! i = get h a ! i" |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
110 |
by (simp add: update_def noteq_def) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
111 |
|
37807 | 112 |
lemma get_update_elem_neqIndex [simp]: |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
113 |
"i \<noteq> j \<Longrightarrow> get (update a j v h) a ! i = get h a ! i" |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
114 |
by simp |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
115 |
|
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
116 |
lemma length_update [simp]: |
37802 | 117 |
"length (update b i v h) = length h" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
118 |
by (simp add: update_def length_def set_def get_def fun_eq_iff) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
119 |
|
37807 | 120 |
lemma update_swap_neq: |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
121 |
"a =!!= a' \<Longrightarrow> |
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
122 |
update a i v (update a' i' v' h) |
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
123 |
= update a' i' v' (update a i v h)" |
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
124 |
apply (unfold update_def) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
125 |
apply simp |
37807 | 126 |
apply (subst set_set_swap, assumption) |
127 |
apply (subst get_set_neq) |
|
128 |
apply (erule noteq_sym) |
|
129 |
apply simp |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
130 |
done |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
131 |
|
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
132 |
lemma update_swap_neqIndex: |
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
133 |
"\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> update a i v (update a i' v' h) = update a i' v' (update a i v h)" |
37807 | 134 |
by (auto simp add: update_def set_set_swap list_update_swap) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
135 |
|
37807 | 136 |
lemma get_alloc: |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
137 |
"get (snd (alloc ls' h)) (fst (alloc ls h)) = ls'" |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
138 |
by (simp add: Let_def split_def alloc_def) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
139 |
|
37807 | 140 |
lemma set: |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
141 |
"set (fst (alloc ls h)) |
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
142 |
new_ls (snd (alloc ls h)) |
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
143 |
= snd (alloc new_ls h)" |
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
144 |
by (simp add: Let_def split_def alloc_def) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
145 |
|
37807 | 146 |
lemma present_update [simp]: |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
147 |
"present (update b i v h) = present h" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
148 |
by (simp add: update_def present_def set_def get_def fun_eq_iff) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
149 |
|
37807 | 150 |
lemma present_alloc [simp]: |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
151 |
"present (snd (alloc xs h)) (fst (alloc xs h))" |
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
152 |
by (simp add: present_def alloc_def set_def Let_def) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
153 |
|
37807 | 154 |
lemma not_present_alloc [simp]: |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
155 |
"\<not> present h (fst (alloc xs h))" |
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
156 |
by (simp add: present_def alloc_def Let_def) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
157 |
|
37758 | 158 |
|
159 |
text {* Monad operations *} |
|
160 |
||
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
161 |
lemma execute_new [execute_simps]: |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
162 |
"execute (new n x) h = Some (alloc (replicate n x) h)" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
163 |
by (simp add: new_def execute_simps) |
37758 | 164 |
|
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
165 |
lemma success_newI [success_intros]: |
37758 | 166 |
"success (new n x) h" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
167 |
by (auto intro: success_intros simp add: new_def) |
26170 | 168 |
|
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
169 |
lemma crel_newI [crel_intros]: |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
170 |
assumes "(a, h') = alloc (replicate n x) h" |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
171 |
shows "crel (new n x) h h' a" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
172 |
by (rule crelI) (simp add: assms execute_simps) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
173 |
|
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
174 |
lemma crel_newE [crel_elims]: |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
175 |
assumes "crel (new n x) h h' r" |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
176 |
obtains "r = fst (alloc (replicate n x) h)" "h' = snd (alloc (replicate n x) h)" |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
177 |
"get h' r = replicate n x" "present h' r" "\<not> present h r" |
37807 | 178 |
using assms by (rule crelE) (simp add: get_alloc execute_simps) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
179 |
|
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
180 |
lemma execute_of_list [execute_simps]: |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
181 |
"execute (of_list xs) h = Some (alloc xs h)" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
182 |
by (simp add: of_list_def execute_simps) |
37758 | 183 |
|
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
184 |
lemma success_of_listI [success_intros]: |
37758 | 185 |
"success (of_list xs) h" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
186 |
by (auto intro: success_intros simp add: of_list_def) |
26170 | 187 |
|
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
188 |
lemma crel_of_listI [crel_intros]: |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
189 |
assumes "(a, h') = alloc xs h" |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
190 |
shows "crel (of_list xs) h h' a" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
191 |
by (rule crelI) (simp add: assms execute_simps) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
192 |
|
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
193 |
lemma crel_of_listE [crel_elims]: |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
194 |
assumes "crel (of_list xs) h h' r" |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
195 |
obtains "r = fst (alloc xs h)" "h' = snd (alloc xs h)" |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
196 |
"get h' r = xs" "present h' r" "\<not> present h r" |
37807 | 197 |
using assms by (rule crelE) (simp add: get_alloc execute_simps) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
198 |
|
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
199 |
lemma execute_make [execute_simps]: |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
200 |
"execute (make n f) h = Some (alloc (map f [0 ..< n]) h)" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
201 |
by (simp add: make_def execute_simps) |
26170 | 202 |
|
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
203 |
lemma success_makeI [success_intros]: |
37758 | 204 |
"success (make n f) h" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
205 |
by (auto intro: success_intros simp add: make_def) |
37758 | 206 |
|
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
207 |
lemma crel_makeI [crel_intros]: |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
208 |
assumes "(a, h') = alloc (map f [0 ..< n]) h" |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
209 |
shows "crel (make n f) h h' a" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
210 |
by (rule crelI) (simp add: assms execute_simps) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
211 |
|
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
212 |
lemma crel_makeE [crel_elims]: |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
213 |
assumes "crel (make n f) h h' r" |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
214 |
obtains "r = fst (alloc (map f [0 ..< n]) h)" "h' = snd (alloc (map f [0 ..< n]) h)" |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
215 |
"get h' r = map f [0 ..< n]" "present h' r" "\<not> present h r" |
37807 | 216 |
using assms by (rule crelE) (simp add: get_alloc execute_simps) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
217 |
|
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
218 |
lemma execute_len [execute_simps]: |
37802 | 219 |
"execute (len a) h = Some (length h a, h)" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
220 |
by (simp add: len_def execute_simps) |
37758 | 221 |
|
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
222 |
lemma success_lenI [success_intros]: |
37758 | 223 |
"success (len a) h" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
224 |
by (auto intro: success_intros simp add: len_def) |
37752 | 225 |
|
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
226 |
lemma crel_lengthI [crel_intros]: |
37802 | 227 |
assumes "h' = h" "r = length h a" |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
228 |
shows "crel (len a) h h' r" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
229 |
by (rule crelI) (simp add: assms execute_simps) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
230 |
|
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
231 |
lemma crel_lengthE [crel_elims]: |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
232 |
assumes "crel (len a) h h' r" |
37802 | 233 |
obtains "r = length h' a" "h' = h" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
234 |
using assms by (rule crelE) (simp add: execute_simps) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
235 |
|
37758 | 236 |
lemma execute_nth [execute_simps]: |
37802 | 237 |
"i < length h a \<Longrightarrow> |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
238 |
execute (nth a i) h = Some (get h a ! i, h)" |
37802 | 239 |
"i \<ge> length h a \<Longrightarrow> execute (nth a i) h = None" |
37758 | 240 |
by (simp_all add: nth_def execute_simps) |
241 |
||
242 |
lemma success_nthI [success_intros]: |
|
37802 | 243 |
"i < length h a \<Longrightarrow> success (nth a i) h" |
37758 | 244 |
by (auto intro: success_intros simp add: nth_def) |
26170 | 245 |
|
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
246 |
lemma crel_nthI [crel_intros]: |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
247 |
assumes "i < length h a" "h' = h" "r = get h a ! i" |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
248 |
shows "crel (nth a i) h h' r" |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
249 |
by (rule crelI) (insert assms, simp add: execute_simps) |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
250 |
|
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
251 |
lemma crel_nthE [crel_elims]: |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
252 |
assumes "crel (nth a i) h h' r" |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
253 |
obtains "i < length h a" "r = get h a ! i" "h' = h" |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
254 |
using assms by (rule crelE) |
37802 | 255 |
(erule successE, cases "i < length h a", simp_all add: execute_simps) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
256 |
|
37758 | 257 |
lemma execute_upd [execute_simps]: |
37802 | 258 |
"i < length h a \<Longrightarrow> |
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
259 |
execute (upd i x a) h = Some (a, update a i x h)" |
37802 | 260 |
"i \<ge> length h a \<Longrightarrow> execute (upd i x a) h = None" |
37758 | 261 |
by (simp_all add: upd_def execute_simps) |
26170 | 262 |
|
37758 | 263 |
lemma success_updI [success_intros]: |
37802 | 264 |
"i < length h a \<Longrightarrow> success (upd i x a) h" |
37758 | 265 |
by (auto intro: success_intros simp add: upd_def) |
266 |
||
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
267 |
lemma crel_updI [crel_intros]: |
37802 | 268 |
assumes "i < length h a" "h' = update a i v h" |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
269 |
shows "crel (upd i v a) h h' a" |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
270 |
by (rule crelI) (insert assms, simp add: execute_simps) |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
271 |
|
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
272 |
lemma crel_updE [crel_elims]: |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
273 |
assumes "crel (upd i v a) h h' r" |
37802 | 274 |
obtains "r = a" "h' = update a i v h" "i < length h a" |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
275 |
using assms by (rule crelE) |
37802 | 276 |
(erule successE, cases "i < length h a", simp_all add: execute_simps) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
277 |
|
37758 | 278 |
lemma execute_map_entry [execute_simps]: |
37802 | 279 |
"i < length h a \<Longrightarrow> |
37758 | 280 |
execute (map_entry i f a) h = |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
281 |
Some (a, update a i (f (get h a ! i)) h)" |
37802 | 282 |
"i \<ge> length h a \<Longrightarrow> execute (map_entry i f a) h = None" |
37758 | 283 |
by (simp_all add: map_entry_def execute_simps) |
37752 | 284 |
|
37758 | 285 |
lemma success_map_entryI [success_intros]: |
37802 | 286 |
"i < length h a \<Longrightarrow> success (map_entry i f a) h" |
37758 | 287 |
by (auto intro: success_intros simp add: map_entry_def) |
288 |
||
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
289 |
lemma crel_map_entryI [crel_intros]: |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
290 |
assumes "i < length h a" "h' = update a i (f (get h a ! i)) h" "r = a" |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
291 |
shows "crel (map_entry i f a) h h' r" |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
292 |
by (rule crelI) (insert assms, simp add: execute_simps) |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
293 |
|
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
294 |
lemma crel_map_entryE [crel_elims]: |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
295 |
assumes "crel (map_entry i f a) h h' r" |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
296 |
obtains "r = a" "h' = update a i (f (get h a ! i)) h" "i < length h a" |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
297 |
using assms by (rule crelE) |
37802 | 298 |
(erule successE, cases "i < length h a", simp_all add: execute_simps) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
299 |
|
37758 | 300 |
lemma execute_swap [execute_simps]: |
37802 | 301 |
"i < length h a \<Longrightarrow> |
37758 | 302 |
execute (swap i x a) h = |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
303 |
Some (get h a ! i, update a i x h)" |
37802 | 304 |
"i \<ge> length h a \<Longrightarrow> execute (swap i x a) h = None" |
37758 | 305 |
by (simp_all add: swap_def execute_simps) |
306 |
||
307 |
lemma success_swapI [success_intros]: |
|
37802 | 308 |
"i < length h a \<Longrightarrow> success (swap i x a) h" |
37758 | 309 |
by (auto intro: success_intros simp add: swap_def) |
37752 | 310 |
|
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
311 |
lemma crel_swapI [crel_intros]: |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
312 |
assumes "i < length h a" "h' = update a i x h" "r = get h a ! i" |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
313 |
shows "crel (swap i x a) h h' r" |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
314 |
by (rule crelI) (insert assms, simp add: execute_simps) |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
315 |
|
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
316 |
lemma crel_swapE [crel_elims]: |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
317 |
assumes "crel (swap i x a) h h' r" |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
318 |
obtains "r = get h a ! i" "h' = update a i x h" "i < length h a" |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
319 |
using assms by (rule crelE) |
37802 | 320 |
(erule successE, cases "i < length h a", simp_all add: execute_simps) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
321 |
|
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
322 |
lemma execute_freeze [execute_simps]: |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
323 |
"execute (freeze a) h = Some (get h a, h)" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
324 |
by (simp add: freeze_def execute_simps) |
37758 | 325 |
|
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
326 |
lemma success_freezeI [success_intros]: |
37758 | 327 |
"success (freeze a) h" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
328 |
by (auto intro: success_intros simp add: freeze_def) |
26170 | 329 |
|
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
330 |
lemma crel_freezeI [crel_intros]: |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
331 |
assumes "h' = h" "r = get h a" |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
332 |
shows "crel (freeze a) h h' r" |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
333 |
by (rule crelI) (insert assms, simp add: execute_simps) |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
334 |
|
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
335 |
lemma crel_freezeE [crel_elims]: |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
336 |
assumes "crel (freeze a) h h' r" |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
337 |
obtains "h' = h" "r = get h a" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
338 |
using assms by (rule crelE) (simp add: execute_simps) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
339 |
|
26170 | 340 |
lemma upd_return: |
341 |
"upd i x a \<guillemotright> return a = upd i x a" |
|
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
342 |
by (rule Heap_eqI) (simp add: bind_def guard_def upd_def execute_simps) |
26170 | 343 |
|
37752 | 344 |
lemma array_make: |
345 |
"new n x = make n (\<lambda>_. x)" |
|
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
346 |
by (rule Heap_eqI) (simp add: map_replicate_trivial execute_simps) |
26170 | 347 |
|
37845
b70d7a347964
first roughly working version of Imperative HOL for Scala
haftmann
parents:
37842
diff
changeset
|
348 |
lemma array_of_list_make [code]: |
37752 | 349 |
"of_list xs = make (List.length xs) (\<lambda>n. xs ! n)" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
350 |
by (rule Heap_eqI) (simp add: map_nth execute_simps) |
26170 | 351 |
|
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
352 |
hide_const (open) present get set alloc length update noteq new of_list make len nth upd map_entry swap freeze |
26170 | 353 |
|
26182 | 354 |
|
355 |
subsection {* Code generator setup *} |
|
356 |
||
357 |
subsubsection {* Logical intermediate layer *} |
|
358 |
||
359 |
definition new' where |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
360 |
[code del]: "new' = Array.new o Code_Numeral.nat_of" |
37752 | 361 |
|
28562 | 362 |
lemma [code]: |
37752 | 363 |
"Array.new = new' o Code_Numeral.of_nat" |
26182 | 364 |
by (simp add: new'_def o_def) |
365 |
||
366 |
definition make' where |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
367 |
[code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)" |
37752 | 368 |
|
28562 | 369 |
lemma [code]: |
37752 | 370 |
"Array.make n f = make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)" |
26182 | 371 |
by (simp add: make'_def o_def) |
372 |
||
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
373 |
definition len' where |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
374 |
[code del]: "len' a = Array.len a \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))" |
37752 | 375 |
|
28562 | 376 |
lemma [code]: |
37752 | 377 |
"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
|
378 |
by (simp add: len'_def) |
26182 | 379 |
|
380 |
definition nth' where |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
381 |
[code del]: "nth' a = Array.nth a o Code_Numeral.nat_of" |
37752 | 382 |
|
28562 | 383 |
lemma [code]: |
37752 | 384 |
"Array.nth a n = nth' a (Code_Numeral.of_nat n)" |
26182 | 385 |
by (simp add: nth'_def) |
386 |
||
387 |
definition upd' where |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
388 |
[code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \<guillemotright> return ()" |
37752 | 389 |
|
28562 | 390 |
lemma [code]: |
37752 | 391 |
"Array.upd i x a = upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a" |
37709 | 392 |
by (simp add: upd'_def upd_return) |
26182 | 393 |
|
37752 | 394 |
lemma [code]: |
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
395 |
"Array.map_entry i f a = do { |
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
396 |
x \<leftarrow> Array.nth a i; |
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
397 |
Array.upd i (f x) a |
37792 | 398 |
}" |
37758 | 399 |
by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def execute_simps) |
26182 | 400 |
|
37752 | 401 |
lemma [code]: |
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
402 |
"Array.swap i x a = do { |
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
403 |
y \<leftarrow> Array.nth a i; |
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
404 |
Array.upd i x a; |
37752 | 405 |
return y |
37792 | 406 |
}" |
37758 | 407 |
by (rule Heap_eqI) (simp add: bind_def guard_def swap_def execute_simps) |
37752 | 408 |
|
409 |
lemma [code]: |
|
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
410 |
"Array.freeze a = do { |
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
411 |
n \<leftarrow> Array.len a; |
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
412 |
Heap_Monad.fold_map (\<lambda>i. Array.nth a i) [0..<n] |
37792 | 413 |
}" |
37752 | 414 |
proof (rule Heap_eqI) |
415 |
fix h |
|
416 |
have *: "List.map |
|
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
417 |
(\<lambda>x. fst (the (if x < Array.length h a |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
418 |
then Some (Array.get h a ! x, h) else None))) |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
419 |
[0..<Array.length h a] = |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
420 |
List.map (List.nth (Array.get h a)) [0..<Array.length h a]" |
37752 | 421 |
by simp |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
422 |
have "execute (Heap_Monad.fold_map (Array.nth a) [0..<Array.length h a]) h = |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
423 |
Some (Array.get h a, 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
|
424 |
apply (subst execute_fold_map_unchanged_heap) |
37752 | 425 |
apply (simp_all add: nth_def guard_def *) |
426 |
apply (simp add: length_def map_nth) |
|
427 |
done |
|
37792 | 428 |
then have "execute (do { |
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
429 |
n \<leftarrow> Array.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
|
430 |
Heap_Monad.fold_map (Array.nth a) [0..<n] |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
431 |
}) h = Some (Array.get h a, h)" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
432 |
by (auto intro: execute_bind_eq_SomeI simp add: execute_simps) |
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
433 |
then show "execute (Array.freeze a) h = execute (do { |
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
434 |
n \<leftarrow> Array.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
|
435 |
Heap_Monad.fold_map (Array.nth a) [0..<n] |
37792 | 436 |
}) h" by (simp add: execute_simps) |
37752 | 437 |
qed |
438 |
||
37831
fa3a2e35c4f1
repaired some implementations of imperative operations
haftmann
parents:
37827
diff
changeset
|
439 |
hide_const (open) new' make' len' nth' upd' |
37752 | 440 |
|
441 |
||
442 |
text {* SML *} |
|
26182 | 443 |
|
444 |
code_type array (SML "_/ array") |
|
445 |
code_const Array (SML "raise/ (Fail/ \"bare Array\")") |
|
26752 | 446 |
code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))") |
37831
fa3a2e35c4f1
repaired some implementations of imperative operations
haftmann
parents:
37827
diff
changeset
|
447 |
code_const Array.of_list (SML "(fn/ ()/ =>/ Array.fromList/ _)") |
26752 | 448 |
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
|
449 |
code_const Array.len' (SML "(fn/ ()/ =>/ Array.length/ _)") |
26752 | 450 |
code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))") |
451 |
code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))") |
|
39716
d1c12f4ee9ac
treat equality on refs and arrays as primitive operation
haftmann
parents:
39302
diff
changeset
|
452 |
code_const "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" (SML infixl 6 "=") |
26182 | 453 |
|
454 |
code_reserved SML Array |
|
455 |
||
456 |
||
37752 | 457 |
text {* OCaml *} |
26182 | 458 |
|
459 |
code_type array (OCaml "_/ array") |
|
460 |
code_const Array (OCaml "failwith/ \"bare Array\"") |
|
32580 | 461 |
code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)") |
37831
fa3a2e35c4f1
repaired some implementations of imperative operations
haftmann
parents:
37827
diff
changeset
|
462 |
code_const Array.of_list (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)") |
fa3a2e35c4f1
repaired some implementations of imperative operations
haftmann
parents:
37827
diff
changeset
|
463 |
code_const Array.make' (OCaml "(fun/ ()/ ->/ Array.init/ (Big'_int.int'_of'_big'_int/ _)/ |
fa3a2e35c4f1
repaired some implementations of imperative operations
haftmann
parents:
37827
diff
changeset
|
464 |
(fun k'_ ->/ _/ (Big'_int.big'_int'_of'_int/ k'_)))") |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
465 |
code_const Array.len' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))") |
32580 | 466 |
code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))") |
467 |
code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)") |
|
39716
d1c12f4ee9ac
treat equality on refs and arrays as primitive operation
haftmann
parents:
39302
diff
changeset
|
468 |
code_const "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" (OCaml infixl 4 "=") |
26182 | 469 |
|
470 |
code_reserved OCaml Array |
|
471 |
||
472 |
||
37752 | 473 |
text {* Haskell *} |
26182 | 474 |
|
29793 | 475 |
code_type array (Haskell "Heap.STArray/ Heap.RealWorld/ _") |
26182 | 476 |
code_const Array (Haskell "error/ \"bare Array\"") |
37831
fa3a2e35c4f1
repaired some implementations of imperative operations
haftmann
parents:
37827
diff
changeset
|
477 |
code_const Array.new' (Haskell "Heap.newArray") |
fa3a2e35c4f1
repaired some implementations of imperative operations
haftmann
parents:
37827
diff
changeset
|
478 |
code_const Array.of_list (Haskell "Heap.newListArray") |
fa3a2e35c4f1
repaired some implementations of imperative operations
haftmann
parents:
37827
diff
changeset
|
479 |
code_const Array.make' (Haskell "Heap.newFunArray") |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset
|
480 |
code_const Array.len' (Haskell "Heap.lengthArray") |
29793 | 481 |
code_const Array.nth' (Haskell "Heap.readArray") |
482 |
code_const Array.upd' (Haskell "Heap.writeArray") |
|
39716
d1c12f4ee9ac
treat equality on refs and arrays as primitive operation
haftmann
parents:
39302
diff
changeset
|
483 |
code_const "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" (Haskell infix 4 "==") |
d1c12f4ee9ac
treat equality on refs and arrays as primitive operation
haftmann
parents:
39302
diff
changeset
|
484 |
code_instance array :: HOL.equal (Haskell -) |
26182 | 485 |
|
37842 | 486 |
|
487 |
text {* Scala *} |
|
488 |
||
37845
b70d7a347964
first roughly working version of Imperative HOL for Scala
haftmann
parents:
37842
diff
changeset
|
489 |
code_type array (Scala "!collection.mutable.ArraySeq[_]") |
37842 | 490 |
code_const Array (Scala "!error(\"bare Array\")") |
38968
e55deaa22fff
do not print object frame around Scala includes -- this is in the responsibility of the user
haftmann
parents:
38771
diff
changeset
|
491 |
code_const Array.new' (Scala "('_: Unit)/ => / Array.alloc((_))((_))") |
e55deaa22fff
do not print object frame around Scala includes -- this is in the responsibility of the user
haftmann
parents:
38771
diff
changeset
|
492 |
code_const Array.make' (Scala "('_: Unit)/ =>/ Array.make((_))((_))") |
e55deaa22fff
do not print object frame around Scala includes -- this is in the responsibility of the user
haftmann
parents:
38771
diff
changeset
|
493 |
code_const Array.len' (Scala "('_: Unit)/ =>/ Array.len((_))") |
e55deaa22fff
do not print object frame around Scala includes -- this is in the responsibility of the user
haftmann
parents:
38771
diff
changeset
|
494 |
code_const Array.nth' (Scala "('_: Unit)/ =>/ Array.nth((_), (_))") |
e55deaa22fff
do not print object frame around Scala includes -- this is in the responsibility of the user
haftmann
parents:
38771
diff
changeset
|
495 |
code_const Array.upd' (Scala "('_: Unit)/ =>/ Array.upd((_), (_), (_))") |
e55deaa22fff
do not print object frame around Scala includes -- this is in the responsibility of the user
haftmann
parents:
38771
diff
changeset
|
496 |
code_const Array.freeze (Scala "('_: Unit)/ =>/ Array.freeze((_))") |
39716
d1c12f4ee9ac
treat equality on refs and arrays as primitive operation
haftmann
parents:
39302
diff
changeset
|
497 |
code_const "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" (Scala infixl 5 "==") |
37842 | 498 |
|
26170 | 499 |
end |