author  haftmann 
Fri, 16 Jul 2010 13:58:29 +0200  
changeset 37842  27e7047d9ae6 
parent 37830  01d308b00bcf 
child 37845  b70d7a347964 
permissions  rwrr 
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/manualcamllight/node14.15.html 

14 
and http://www.smlnj.org/doc/Conversion/toplevelcomparison.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 {* Noninteraction 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 tailrecursive 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 

299 
code_type ref (Scala "!Heap.Ref[_]") 

300 
code_const Ref (Scala "!error(\"bare Ref\")") 

301 
code_const ref (Scala "('_: Unit)/ =>/ Heap.Ref((_))") 

302 
code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.lookup((_))") 

303 
code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.update((_), (_))") 

304 

37758  305 
end 