author | haftmann |
Fri, 23 Jul 2010 10:58:13 +0200 | |
changeset 37947 | 844977c7abeb |
parent 37878 | d016aaead7a2 |
child 37965 | 0c1743d31b5c |
permissions | -rw-r--r-- |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
1 |
(* Title: HOL/Imperative_HOL/Ref.thy |
26170 | 2 |
Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen |
3 |
*) |
|
4 |
||
5 |
header {* Monadic references *} |
|
6 |
||
7 |
theory Ref |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
8 |
imports Array |
26170 | 9 |
begin |
10 |
||
11 |
text {* |
|
12 |
Imperative reference operations; modeled after their ML counterparts. |
|
13 |
See http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html |
|
14 |
and http://www.smlnj.org/doc/Conversion/top-level-comparison.html |
|
15 |
*} |
|
16 |
||
37753 | 17 |
subsection {* Primitives *} |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
18 |
|
37725 | 19 |
definition present :: "heap \<Rightarrow> 'a\<Colon>heap ref \<Rightarrow> bool" where |
20 |
"present h r \<longleftrightarrow> addr_of_ref r < lim h" |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
21 |
|
37725 | 22 |
definition get :: "heap \<Rightarrow> 'a\<Colon>heap ref \<Rightarrow> 'a" where |
23 |
"get h = from_nat \<circ> refs h TYPEREP('a) \<circ> addr_of_ref" |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
24 |
|
37725 | 25 |
definition set :: "'a\<Colon>heap ref \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where |
26 |
"set r x = refs_update |
|
27 |
(\<lambda>h. h(TYPEREP('a) := ((h (TYPEREP('a))) (addr_of_ref r := to_nat x))))" |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
28 |
|
37725 | 29 |
definition alloc :: "'a \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap ref \<times> heap" where |
30 |
"alloc x h = (let |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
31 |
l = lim h; |
37725 | 32 |
r = Ref l |
33 |
in (r, set r x (h\<lparr>lim := l + 1\<rparr>)))" |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
34 |
|
37725 | 35 |
definition noteq :: "'a\<Colon>heap ref \<Rightarrow> 'b\<Colon>heap ref \<Rightarrow> bool" (infix "=!=" 70) where |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
36 |
"r =!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_ref r \<noteq> addr_of_ref s" |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
37 |
|
37753 | 38 |
|
39 |
subsection {* Monad operations *} |
|
40 |
||
41 |
definition ref :: "'a\<Colon>heap \<Rightarrow> 'a ref Heap" where |
|
42 |
[code del]: "ref v = Heap_Monad.heap (alloc v)" |
|
43 |
||
44 |
definition lookup :: "'a\<Colon>heap ref \<Rightarrow> 'a Heap" ("!_" 61) where |
|
37758 | 45 |
[code del]: "lookup r = Heap_Monad.tap (\<lambda>h. get h r)" |
37753 | 46 |
|
47 |
definition update :: "'a ref \<Rightarrow> 'a\<Colon>heap \<Rightarrow> unit Heap" ("_ := _" 62) where |
|
48 |
[code del]: "update r v = Heap_Monad.heap (\<lambda>h. ((), set r v h))" |
|
49 |
||
50 |
definition change :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a Heap" where |
|
37792 | 51 |
"change f r = do { |
37753 | 52 |
x \<leftarrow> ! r; |
53 |
let y = f x; |
|
54 |
r := y; |
|
55 |
return y |
|
37792 | 56 |
}" |
37753 | 57 |
|
58 |
||
59 |
subsection {* Properties *} |
|
60 |
||
37758 | 61 |
text {* Primitives *} |
62 |
||
37725 | 63 |
lemma noteq_sym: "r =!= s \<Longrightarrow> s =!= r" |
64 |
and unequal [simp]: "r \<noteq> r' \<longleftrightarrow> r =!= r'" -- "same types!" |
|
65 |
by (auto simp add: noteq_def) |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
66 |
|
37725 | 67 |
lemma noteq_irrefl: "r =!= r \<Longrightarrow> False" |
68 |
by (auto simp add: noteq_def) |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
69 |
|
37725 | 70 |
lemma present_alloc_neq: "present h r \<Longrightarrow> r =!= fst (alloc v h)" |
71 |
by (simp add: present_def alloc_def noteq_def Let_def) |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
72 |
|
37725 | 73 |
lemma next_fresh [simp]: |
74 |
assumes "(r, h') = alloc x h" |
|
75 |
shows "\<not> present h r" |
|
76 |
using assms by (cases h) (auto simp add: alloc_def present_def Let_def) |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
77 |
|
37725 | 78 |
lemma next_present [simp]: |
79 |
assumes "(r, h') = alloc x h" |
|
80 |
shows "present h' r" |
|
81 |
using assms by (cases h) (auto simp add: alloc_def set_def present_def Let_def) |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
82 |
|
37725 | 83 |
lemma get_set_eq [simp]: |
84 |
"get (set r x h) r = x" |
|
85 |
by (simp add: get_def set_def) |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
86 |
|
37725 | 87 |
lemma get_set_neq [simp]: |
88 |
"r =!= s \<Longrightarrow> get (set s x h) r = get h r" |
|
89 |
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:
37709
diff
changeset
|
90 |
|
37725 | 91 |
lemma set_same [simp]: |
92 |
"set r x (set r y h) = set r x h" |
|
93 |
by (simp add: set_def) |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
94 |
|
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
95 |
lemma not_present_alloc [simp]: |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
96 |
"\<not> present h (fst (alloc v h))" |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
97 |
by (simp add: present_def alloc_def Let_def) |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
98 |
|
37725 | 99 |
lemma set_set_swap: |
100 |
"r =!= r' \<Longrightarrow> set r x (set r' x' h) = set r' x' (set r x h)" |
|
101 |
by (simp add: noteq_def set_def expand_fun_eq) |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
102 |
|
37725 | 103 |
lemma alloc_set: |
104 |
"fst (alloc x (set r x' h)) = fst (alloc x h)" |
|
105 |
by (simp add: alloc_def set_def Let_def) |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
106 |
|
37725 | 107 |
lemma get_alloc [simp]: |
108 |
"get (snd (alloc x h)) (fst (alloc x' h)) = x" |
|
109 |
by (simp add: alloc_def Let_def) |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
110 |
|
37725 | 111 |
lemma set_alloc [simp]: |
112 |
"set (fst (alloc v h)) v' (snd (alloc v h)) = snd (alloc v' h)" |
|
113 |
by (simp add: alloc_def Let_def) |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
114 |
|
37725 | 115 |
lemma get_alloc_neq: "r =!= fst (alloc v h) \<Longrightarrow> |
116 |
get (snd (alloc v h)) r = get h r" |
|
117 |
by (simp add: get_def set_def alloc_def Let_def noteq_def) |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
118 |
|
37725 | 119 |
lemma lim_set [simp]: |
120 |
"lim (set r v h) = lim h" |
|
121 |
by (simp add: set_def) |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
122 |
|
37725 | 123 |
lemma present_alloc [simp]: |
124 |
"present h r \<Longrightarrow> present (snd (alloc v h)) r" |
|
125 |
by (simp add: present_def alloc_def Let_def) |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
126 |
|
37725 | 127 |
lemma present_set [simp]: |
128 |
"present (set r v h) = present h" |
|
129 |
by (simp add: present_def expand_fun_eq) |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
130 |
|
37725 | 131 |
lemma noteq_I: |
132 |
"present h r \<Longrightarrow> \<not> present h r' \<Longrightarrow> r =!= r'" |
|
133 |
by (auto simp add: noteq_def present_def) |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
134 |
|
37758 | 135 |
|
136 |
text {* Monad operations *} |
|
137 |
||
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
138 |
lemma execute_ref [execute_simps]: |
37758 | 139 |
"execute (ref v) h = Some (alloc v h)" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
140 |
by (simp add: ref_def execute_simps) |
26170 | 141 |
|
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
142 |
lemma success_refI [success_intros]: |
37758 | 143 |
"success (ref v) h" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
144 |
by (auto intro: success_intros simp add: ref_def) |
37758 | 145 |
|
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
146 |
lemma crel_refI [crel_intros]: |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
147 |
assumes "(r, h') = alloc v h" |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
148 |
shows "crel (ref v) h h' r" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
149 |
by (rule crelI) (insert assms, simp add: execute_simps) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
150 |
|
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
151 |
lemma crel_refE [crel_elims]: |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
152 |
assumes "crel (ref v) h h' r" |
37796 | 153 |
obtains "get h' r = v" and "present h' r" and "\<not> present h r" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
154 |
using assms by (rule crelE) (simp add: execute_simps) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
155 |
|
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
156 |
lemma execute_lookup [execute_simps]: |
37753 | 157 |
"Heap_Monad.execute (lookup r) h = Some (get h r, h)" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
158 |
by (simp add: lookup_def execute_simps) |
26182 | 159 |
|
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
160 |
lemma success_lookupI [success_intros]: |
37758 | 161 |
"success (lookup r) h" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
162 |
by (auto intro: success_intros simp add: lookup_def) |
37758 | 163 |
|
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
164 |
lemma crel_lookupI [crel_intros]: |
37796 | 165 |
assumes "h' = h" "x = get h r" |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
166 |
shows "crel (!r) h h' x" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
167 |
by (rule crelI) (insert assms, simp add: execute_simps) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
168 |
|
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
169 |
lemma crel_lookupE [crel_elims]: |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
170 |
assumes "crel (!r) h h' x" |
37796 | 171 |
obtains "h' = h" "x = get h r" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
172 |
using assms by (rule crelE) (simp add: execute_simps) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
173 |
|
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
174 |
lemma execute_update [execute_simps]: |
37753 | 175 |
"Heap_Monad.execute (update r v) h = Some ((), set r v h)" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
176 |
by (simp add: update_def execute_simps) |
26170 | 177 |
|
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
178 |
lemma success_updateI [success_intros]: |
37758 | 179 |
"success (update r v) h" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
180 |
by (auto intro: success_intros simp add: update_def) |
37758 | 181 |
|
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
182 |
lemma crel_updateI [crel_intros]: |
37796 | 183 |
assumes "h' = set r v h" |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
184 |
shows "crel (r := v) h h' x" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
185 |
by (rule crelI) (insert assms, simp add: execute_simps) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
186 |
|
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
187 |
lemma crel_updateE [crel_elims]: |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
188 |
assumes "crel (r' := v) h h' r" |
37796 | 189 |
obtains "h' = set r' v h" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
190 |
using assms by (rule crelE) (simp add: execute_simps) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
191 |
|
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
192 |
lemma execute_change [execute_simps]: |
37753 | 193 |
"Heap_Monad.execute (change f r) h = Some (f (get h r), set r (f (get h r)) h)" |
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
194 |
by (simp add: change_def bind_def Let_def execute_simps) |
37758 | 195 |
|
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
196 |
lemma success_changeI [success_intros]: |
37758 | 197 |
"success (change f r) h" |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
198 |
by (auto intro!: success_intros crel_intros simp add: change_def) |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
199 |
|
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
200 |
lemma crel_changeI [crel_intros]: |
37796 | 201 |
assumes "h' = set r (f (get h r)) h" "x = f (get h r)" |
202 |
shows "crel (change f r) h h' x" |
|
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
203 |
by (rule crelI) (insert assms, simp add: execute_simps) |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
204 |
|
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
205 |
lemma crel_changeE [crel_elims]: |
37796 | 206 |
assumes "crel (change f r') h h' r" |
207 |
obtains "h' = set r' (f (get h r')) h" "r = f (get h r')" |
|
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset
|
208 |
using assms by (rule crelE) (simp add: execute_simps) |
26170 | 209 |
|
210 |
lemma lookup_chain: |
|
211 |
"(!r \<guillemotright> f) = f" |
|
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset
|
212 |
by (rule Heap_eqI) (auto simp add: lookup_def execute_simps intro: execute_bind) |
26170 | 213 |
|
28562 | 214 |
lemma update_change [code]: |
37725 | 215 |
"r := e = change (\<lambda>_. e) r \<guillemotright> return ()" |
216 |
by (rule Heap_eqI) (simp add: change_def lookup_chain) |
|
26170 | 217 |
|
26182 | 218 |
|
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
219 |
text {* Non-interaction between imperative array and imperative references *} |
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
220 |
|
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
221 |
lemma array_get_set [simp]: |
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
222 |
"Array.get (set r v h) = Array.get h" |
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
223 |
by (simp add: Array.get_def set_def expand_fun_eq) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
224 |
|
37796 | 225 |
lemma get_update [simp]: |
37805 | 226 |
"get (Array.update a i v h) r = get h r" |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
227 |
by (simp add: get_def Array.update_def Array.set_def) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
228 |
|
37796 | 229 |
lemma alloc_update: |
230 |
"fst (alloc v (Array.update a i v' h)) = fst (alloc v h)" |
|
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
231 |
by (simp add: Array.update_def Array.get_def Array.set_def alloc_def Let_def) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
232 |
|
37796 | 233 |
lemma update_set_swap: |
234 |
"Array.update a i v (set r v' h) = set r v' (Array.update a i v h)" |
|
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
235 |
by (simp add: Array.update_def Array.get_def Array.set_def set_def) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
236 |
|
37725 | 237 |
lemma length_alloc [simp]: |
37802 | 238 |
"Array.length (snd (alloc v h)) a = Array.length h a" |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
239 |
by (simp add: Array.length_def Array.get_def alloc_def set_def Let_def) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
240 |
|
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
241 |
lemma array_get_alloc [simp]: |
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
242 |
"Array.get (snd (alloc v h)) = Array.get h" |
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
243 |
by (simp add: Array.get_def alloc_def set_def Let_def expand_fun_eq) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
244 |
|
37796 | 245 |
lemma present_update [simp]: |
246 |
"present (Array.update a i v h) = present h" |
|
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
247 |
by (simp add: Array.update_def Array.set_def expand_fun_eq present_def) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
248 |
|
37725 | 249 |
lemma array_present_set [simp]: |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
250 |
"Array.present (set r v h) = Array.present h" |
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
251 |
by (simp add: Array.present_def set_def expand_fun_eq) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
252 |
|
37725 | 253 |
lemma array_present_alloc [simp]: |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
254 |
"Array.present h a \<Longrightarrow> Array.present (snd (alloc v h)) a" |
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
255 |
by (simp add: Array.present_def alloc_def Let_def) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
256 |
|
37725 | 257 |
lemma set_array_set_swap: |
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
258 |
"Array.set a xs (set r x' h) = set r x' (Array.set a xs h)" |
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset
|
259 |
by (simp add: Array.set_def set_def) |
37725 | 260 |
|
37796 | 261 |
hide_const (open) present get set alloc noteq lookup update change |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
262 |
|
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37709
diff
changeset
|
263 |
|
26182 | 264 |
subsection {* Code generator setup *} |
265 |
||
37753 | 266 |
text {* SML *} |
26182 | 267 |
|
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
29793
diff
changeset
|
268 |
code_type ref (SML "_/ Unsynchronized.ref") |
26182 | 269 |
code_const Ref (SML "raise/ (Fail/ \"bare Ref\")") |
37725 | 270 |
code_const ref (SML "(fn/ ()/ =>/ Unsynchronized.ref/ _)") |
26752 | 271 |
code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)") |
272 |
code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)") |
|
26182 | 273 |
|
274 |
code_reserved SML ref |
|
275 |
||
276 |
||
37753 | 277 |
text {* OCaml *} |
26182 | 278 |
|
279 |
code_type ref (OCaml "_/ ref") |
|
37830 | 280 |
code_const Ref (OCaml "failwith/ \"bare Ref\"") |
281 |
code_const ref (OCaml "(fun/ ()/ ->/ ref/ _)") |
|
282 |
code_const Ref.lookup (OCaml "(fun/ ()/ ->/ !/ _)") |
|
283 |
code_const Ref.update (OCaml "(fun/ ()/ ->/ _/ :=/ _)") |
|
26182 | 284 |
|
285 |
code_reserved OCaml ref |
|
286 |
||
287 |
||
37753 | 288 |
text {* Haskell *} |
26182 | 289 |
|
29793 | 290 |
code_type ref (Haskell "Heap.STRef/ Heap.RealWorld/ _") |
26182 | 291 |
code_const Ref (Haskell "error/ \"bare Ref\"") |
37725 | 292 |
code_const ref (Haskell "Heap.newSTRef") |
29793 | 293 |
code_const Ref.lookup (Haskell "Heap.readSTRef") |
294 |
code_const Ref.update (Haskell "Heap.writeSTRef") |
|
26182 | 295 |
|
37842 | 296 |
|
297 |
text {* Scala *} |
|
298 |
||
37878 | 299 |
code_type ref (Scala "!Ref[_]") |
37842 | 300 |
code_const Ref (Scala "!error(\"bare Ref\")") |
37878 | 301 |
code_const ref (Scala "('_: Unit)/ =>/ Ref((_))") |
302 |
code_const Ref.lookup (Scala "('_: Unit)/ =>/ lookup((_))") |
|
303 |
code_const Ref.update (Scala "('_: Unit)/ =>/ update((_), (_))") |
|
37842 | 304 |
|
37758 | 305 |
end |
37845
b70d7a347964
first roughly working version of Imperative HOL for Scala
haftmann
parents:
37842
diff
changeset
|
306 |