author  haftmann 
Mon, 05 Jul 2010 15:36:37 +0200  
changeset 37718  3046ebbb43c0 
parent 37716  24bb91462892 
child 37719  271ecd4fb9f9 
permissions  rwrr 
37714  1 
(* Title: HOL/Imperative_HOL/Heap.thy 
26170  2 
Author: John Matthews, Galois Connections; Alexander Krauss, TU Muenchen 
3 
*) 

4 

5 
header {* A polymorphic heap based on cantor encodings *} 

6 

7 
theory Heap 

30738  8 
imports Main Countable 
26170  9 
begin 
10 

11 
subsection {* Representable types *} 

12 

13 
text {* The type class of representable types *} 

14 

28335  15 
class heap = typerep + countable 
26170  16 

17 
instance nat :: heap .. 

18 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
36640
diff
changeset

19 
instance prod :: (heap, heap) heap .. 
26170  20 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
36640
diff
changeset

21 
instance sum :: (heap, heap) heap .. 
26170  22 

23 
instance list :: (heap) heap .. 

24 

25 
instance option :: (heap) heap .. 

26 

27 
instance int :: heap .. 

28 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
30738
diff
changeset

29 
instance String.literal :: countable 
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
30738
diff
changeset

30 
by (rule countable_classI [of "String.literal_case to_nat"]) 
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
30738
diff
changeset

31 
(auto split: String.literal.splits) 
26170  32 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
30738
diff
changeset

33 
instance String.literal :: heap .. 
26170  34 

28335  35 
instance typerep :: heap .. 
26170  36 

37 

38 
subsection {* A polymorphic heap with dynamic arrays and references *} 

39 

37714  40 
subsubsection {* Type definitions *} 
41 

26170  42 
types addr = nat  "untyped heap references" 
37714  43 
types heap_rep = nat  "representable values" 
44 

45 
record heap = 

46 
arrays :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep list" 

47 
refs :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep" 

48 
lim :: addr 

49 

50 
definition empty :: heap where 

51 
"empty = \<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 0\<rparr>"  "why undefined?" 

26170  52 

53 
datatype 'a array = Array addr 

54 
datatype 'a ref = Ref addr  "note the phantom type 'a " 

55 

56 
primrec addr_of_array :: "'a array \<Rightarrow> addr" where 

57 
"addr_of_array (Array x) = x" 

58 

59 
primrec addr_of_ref :: "'a ref \<Rightarrow> addr" where 

60 
"addr_of_ref (Ref x) = x" 

61 

62 
lemma addr_of_array_inj [simp]: 

63 
"addr_of_array a = addr_of_array a' \<longleftrightarrow> a = a'" 

64 
by (cases a, cases a') simp_all 

65 

66 
lemma addr_of_ref_inj [simp]: 

67 
"addr_of_ref r = addr_of_ref r' \<longleftrightarrow> r = r'" 

68 
by (cases r, cases r') simp_all 

69 

70 
instance array :: (type) countable 

71 
by (rule countable_classI [of addr_of_array]) simp 

72 

73 
instance ref :: (type) countable 

74 
by (rule countable_classI [of addr_of_ref]) simp 

75 

37714  76 
text {* Syntactic convenience *} 
77 

26170  78 
setup {* 
79 
Sign.add_const_constraint (@{const_name Array}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>heap array"}) 

80 
#> Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>heap ref"}) 

81 
#> Sign.add_const_constraint (@{const_name addr_of_array}, SOME @{typ "'a\<Colon>heap array \<Rightarrow> nat"}) 

82 
#> Sign.add_const_constraint (@{const_name addr_of_ref}, SOME @{typ "'a\<Colon>heap ref \<Rightarrow> nat"}) 

83 
*} 

84 

85 

86 
subsection {* Imperative references and arrays *} 

87 

88 
text {* 

89 
References and arrays are developed in parallel, 

26586  90 
but keeping them separate makes some later proofs simpler. 
26170  91 
*} 
92 

93 
subsubsection {* Primitive operations *} 

94 

95 
definition 

96 
ref_present :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> bool" where 

97 
"ref_present r h \<longleftrightarrow> addr_of_ref r < lim h" 

98 

99 
definition 

100 
array_present :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> bool" where 

101 
"array_present a h \<longleftrightarrow> addr_of_array a < lim h" 

102 

103 
definition 

104 
get_ref :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> 'a" where 

28335  105 
"get_ref r h = from_nat (refs h (TYPEREP('a)) (addr_of_ref r))" 
26170  106 

107 
definition 

108 
get_array :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> 'a list" where 

28335  109 
"get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))" 
26170  110 

111 
definition 

112 
set_ref :: "'a\<Colon>heap ref \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where 

113 
"set_ref r x = 

28335  114 
refs_update (\<lambda>h. h(TYPEREP('a) := ((h (TYPEREP('a))) (addr_of_ref r:=to_nat x))))" 
26170  115 

116 
definition 

117 
set_array :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where 

118 
"set_array a x = 

28335  119 
arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))" 
26170  120 

37718  121 
definition ref :: "'a \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap ref \<times> heap" where 
122 
"ref x h = (let 

123 
l = lim h; 

124 
r = Ref l; 

125 
h'' = set_ref r x (h\<lparr>lim := l + 1\<rparr>) 

126 
in (r, h''))" 

26170  127 

37718  128 
definition array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where 
129 
"array xs h = (let 

130 
l = lim h; 

131 
r = Array l; 

132 
h'' = set_array r xs (h\<lparr>lim := l + 1\<rparr>) 

133 
in (r, h''))" 

134 

26170  135 
definition 
136 
upd :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where 

137 
"upd a i x h = set_array a ((get_array a h)[i:=x]) h" 

138 

139 
definition 

140 
length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where 

141 
"length a h = size (get_array a h)" 

142 

143 

144 
subsubsection {* Reference equality *} 

145 

146 
text {* 

147 
The following relations are useful for comparing arrays and references. 

148 
*} 

149 

150 
definition 

151 
noteq_refs :: "('a\<Colon>heap) ref \<Rightarrow> ('b\<Colon>heap) ref \<Rightarrow> bool" (infix "=!=" 70) 

152 
where 

28335  153 
"r =!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_ref r \<noteq> addr_of_ref s" 
26170  154 

155 
definition 

156 
noteq_arrs :: "('a\<Colon>heap) array \<Rightarrow> ('b\<Colon>heap) array \<Rightarrow> bool" (infix "=!!=" 70) 

157 
where 

28335  158 
"r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s" 
26170  159 

160 
lemma noteq_refs_sym: "r =!= s \<Longrightarrow> s =!= r" 

161 
and noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a" 

162 
and unequal_refs [simp]: "r \<noteq> r' \<longleftrightarrow> r =!= r'"  "same types!" 

163 
and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'" 

164 
unfolding noteq_refs_def noteq_arrs_def by auto 

165 

36640
7eadf5acdaf4
added lemma about irreflexivity of pointer inequality in Imperative_HOL
bulwahn
parents:
36176
diff
changeset

166 
lemma noteq_refs_irrefl: "r =!= r \<Longrightarrow> False" 
7eadf5acdaf4
added lemma about irreflexivity of pointer inequality in Imperative_HOL
bulwahn
parents:
36176
diff
changeset

167 
unfolding noteq_refs_def by auto 
7eadf5acdaf4
added lemma about irreflexivity of pointer inequality in Imperative_HOL
bulwahn
parents:
36176
diff
changeset

168 

26170  169 
lemma present_new_ref: "ref_present r h \<Longrightarrow> r =!= fst (ref v h)" 
37718  170 
by (simp add: ref_present_def ref_def Let_def noteq_refs_def) 
26170  171 

37716
24bb91462892
remove primitive operation Heap.array in favour of Heap.array_of_list
haftmann
parents:
37714
diff
changeset

172 
lemma present_new_arr: "array_present a h \<Longrightarrow> a =!!= fst (array xs h)" 
37718  173 
by (simp add: array_present_def noteq_arrs_def array_def Let_def) 
26170  174 

175 

176 
subsubsection {* Properties of heap containers *} 

177 

178 
text {* Properties of imperative arrays *} 

179 

180 
text {* FIXME: Does there exist a "canonical" array axiomatisation in 

181 
the literature? *} 

182 

183 
lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x" 

33639
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
31205
diff
changeset

184 
by (simp add: get_array_def set_array_def o_def) 
26170  185 

186 
lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h" 

187 
by (simp add: noteq_arrs_def get_array_def set_array_def) 

188 

189 
lemma set_array_same [simp]: 

190 
"set_array r x (set_array r y h) = set_array r x h" 

191 
by (simp add: set_array_def) 

192 

193 
lemma array_set_set_swap: 

194 
"r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)" 

195 
by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def) 

196 

197 
lemma array_ref_set_set_swap: 

198 
"set_array r x (set_ref r' x' h) = set_ref r' x' (set_array r x h)" 

199 
by (simp add: Let_def expand_fun_eq set_array_def set_ref_def) 

200 

201 
lemma get_array_upd_eq [simp]: 

202 
"get_array a (upd a i v h) = (get_array a h) [i := v]" 

203 
by (simp add: upd_def) 

204 

205 
lemma nth_upd_array_neq_array [simp]: 

206 
"a =!!= b \<Longrightarrow> get_array a (upd b j v h) ! i = get_array a h ! i" 

207 
by (simp add: upd_def noteq_arrs_def) 

208 

209 
lemma get_arry_array_upd_elem_neqIndex [simp]: 

210 
"i \<noteq> j \<Longrightarrow> get_array a (upd a j v h) ! i = get_array a h ! i" 

211 
by simp 

212 

213 
lemma length_upd_eq [simp]: 

214 
"length a (upd a i v h) = length a h" 

215 
by (simp add: length_def upd_def) 

216 

217 
lemma length_upd_neq [simp]: 

218 
"length a (upd b i v h) = length a h" 

219 
by (simp add: upd_def length_def set_array_def get_array_def) 

220 

221 
lemma upd_swap_neqArray: 

222 
"a =!!= a' \<Longrightarrow> 

223 
upd a i v (upd a' i' v' h) 

224 
= upd a' i' v' (upd a i v h)" 

225 
apply (unfold upd_def) 

226 
apply simp 

227 
apply (subst array_set_set_swap, assumption) 

228 
apply (subst array_get_set_neq) 

229 
apply (erule noteq_arrs_sym) 

230 
apply (simp) 

231 
done 

232 

233 
lemma upd_swap_neqIndex: 

234 
"\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> upd a i v (upd a i' v' h) = upd a i' v' (upd a i v h)" 

235 
by (auto simp add: upd_def array_set_set_swap list_update_swap) 

236 

237 
lemma get_array_init_array_list: 

37716
24bb91462892
remove primitive operation Heap.array in favour of Heap.array_of_list
haftmann
parents:
37714
diff
changeset

238 
"get_array (fst (array ls h)) (snd (array ls' h)) = ls'" 
24bb91462892
remove primitive operation Heap.array in favour of Heap.array_of_list
haftmann
parents:
37714
diff
changeset

239 
by (simp add: Let_def split_def array_def) 
26170  240 

241 
lemma set_array: 

37716
24bb91462892
remove primitive operation Heap.array in favour of Heap.array_of_list
haftmann
parents:
37714
diff
changeset

242 
"set_array (fst (array ls h)) 
24bb91462892
remove primitive operation Heap.array in favour of Heap.array_of_list
haftmann
parents:
37714
diff
changeset

243 
new_ls (snd (array ls h)) 
24bb91462892
remove primitive operation Heap.array in favour of Heap.array_of_list
haftmann
parents:
37714
diff
changeset

244 
= snd (array new_ls h)" 
24bb91462892
remove primitive operation Heap.array in favour of Heap.array_of_list
haftmann
parents:
37714
diff
changeset

245 
by (simp add: Let_def split_def array_def) 
26170  246 

247 
lemma array_present_upd [simp]: 

248 
"array_present a (upd b i v h) = array_present a h" 

249 
by (simp add: upd_def array_present_def set_array_def get_array_def) 

250 

37716
24bb91462892
remove primitive operation Heap.array in favour of Heap.array_of_list
haftmann
parents:
37714
diff
changeset

251 
(*lemma array_of_list_replicate: 
26170  252 
"array_of_list (replicate n x) = array n x" 
37716
24bb91462892
remove primitive operation Heap.array in favour of Heap.array_of_list
haftmann
parents:
37714
diff
changeset

253 
by (simp add: expand_fun_eq array_of_list_def array_def)*) 
26170  254 

255 
text {* Properties of imperative references *} 

256 

257 
lemma next_ref_fresh [simp]: 

37718  258 
assumes "(r, h') = ref x h" 
26170  259 
shows "\<not> ref_present r h" 
37718  260 
using assms by (cases h) (auto simp add: ref_def ref_present_def Let_def) 
26170  261 

262 
lemma next_ref_present [simp]: 

37718  263 
assumes "(r, h') = ref x h" 
26170  264 
shows "ref_present r h'" 
37718  265 
using assms by (cases h) (auto simp add: ref_def set_ref_def ref_present_def Let_def) 
26170  266 

267 
lemma ref_get_set_eq [simp]: "get_ref r (set_ref r x h) = x" 

268 
by (simp add: get_ref_def set_ref_def) 

269 

270 
lemma ref_get_set_neq [simp]: "r =!= s \<Longrightarrow> get_ref r (set_ref s x h) = get_ref r h" 

271 
by (simp add: noteq_refs_def get_ref_def set_ref_def) 

272 

273 
(* FIXME: We need some infrastructure to infer that locally generated 

274 
new refs (by new_ref(_no_init), new_array(')) are distinct 

275 
from all existing refs. 

276 
*) 

277 

278 
lemma ref_set_get: "set_ref r (get_ref r h) h = h" 

279 
apply (simp add: set_ref_def get_ref_def) 

280 
oops 

281 

282 
lemma set_ref_same[simp]: 

283 
"set_ref r x (set_ref r y h) = set_ref r x h" 

284 
by (simp add: set_ref_def) 

285 

286 
lemma ref_set_set_swap: 

287 
"r =!= r' \<Longrightarrow> set_ref r x (set_ref r' x' h) = set_ref r' x' (set_ref r x h)" 

288 
by (simp add: Let_def expand_fun_eq noteq_refs_def set_ref_def) 

289 

290 
lemma ref_new_set: "fst (ref v (set_ref r v' h)) = fst (ref v h)" 

37718  291 
by (simp add: ref_def set_ref_def Let_def) 
26170  292 

293 
lemma ref_get_new [simp]: 

294 
"get_ref (fst (ref v h)) (snd (ref v' h)) = v'" 

295 
by (simp add: ref_def Let_def split_def) 

296 

297 
lemma ref_set_new [simp]: 

298 
"set_ref (fst (ref v h)) new_v (snd (ref v h)) = snd (ref new_v h)" 

299 
by (simp add: ref_def Let_def split_def) 

300 

301 
lemma ref_get_new_neq: "r =!= (fst (ref v h)) \<Longrightarrow> 

302 
get_ref r (snd (ref v h)) = get_ref r h" 

37718  303 
by (simp add: get_ref_def set_ref_def ref_def Let_def noteq_refs_def) 
26170  304 

305 
lemma lim_set_ref [simp]: 

306 
"lim (set_ref r v h) = lim h" 

307 
by (simp add: set_ref_def) 

308 

309 
lemma ref_present_new_ref [simp]: 

310 
"ref_present r h \<Longrightarrow> ref_present r (snd (ref v h))" 

37718  311 
by (simp add: ref_present_def ref_def Let_def) 
26170  312 

313 
lemma ref_present_set_ref [simp]: 

314 
"ref_present r (set_ref r' v h) = ref_present r h" 

315 
by (simp add: set_ref_def ref_present_def) 

316 

34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
33639
diff
changeset

317 
lemma noteq_refsI: "\<lbrakk> ref_present r h; \<not>ref_present r' h \<rbrakk> \<Longrightarrow> r =!= r'" 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
33639
diff
changeset

318 
unfolding noteq_refs_def ref_present_def 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
33639
diff
changeset

319 
by auto 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
33639
diff
changeset

320 

26170  321 
text {* Noninteraction between imperative array and imperative references *} 
322 

323 
lemma get_array_set_ref [simp]: "get_array a (set_ref r v h) = get_array a h" 

324 
by (simp add: get_array_def set_ref_def) 

325 

326 
lemma nth_set_ref [simp]: "get_array a (set_ref r v h) ! i = get_array a h ! i" 

327 
by simp 

328 

329 
lemma get_ref_upd [simp]: "get_ref r (upd a i v h) = get_ref r h" 

330 
by (simp add: get_ref_def set_array_def upd_def) 

331 

332 
lemma new_ref_upd: "fst (ref v (upd a i v' h)) = fst (ref v h)" 

37718  333 
by (simp add: set_array_def get_array_def Let_def ref_new_set upd_def ref_def) 
26170  334 

26300  335 
text {*not actually true ???*} 
26170  336 
lemma upd_set_ref_swap: "upd a i v (set_ref r v' h) = set_ref r v' (upd a i v h)" 
337 
apply (case_tac a) 

338 
apply (simp add: Let_def upd_def) 

339 
apply auto 

26300  340 
oops 
26170  341 

342 
lemma length_new_ref[simp]: 

343 
"length a (snd (ref v h)) = length a h" 

37718  344 
by (simp add: get_array_def set_ref_def length_def ref_def Let_def) 
26170  345 

346 
lemma get_array_new_ref [simp]: 

347 
"get_array a (snd (ref v h)) = get_array a h" 

37718  348 
by (simp add: ref_def set_ref_def get_array_def Let_def) 
26170  349 

350 
lemma ref_present_upd [simp]: 

351 
"ref_present r (upd a i v h) = ref_present r h" 

352 
by (simp add: upd_def ref_present_def set_array_def get_array_def) 

353 

354 
lemma array_present_set_ref [simp]: 

355 
"array_present a (set_ref r v h) = array_present a h" 

356 
by (simp add: array_present_def set_ref_def) 

357 

358 
lemma array_present_new_ref [simp]: 

359 
"array_present a h \<Longrightarrow> array_present a (snd (ref v h))" 

37718  360 
by (simp add: array_present_def ref_def Let_def) 
26170  361 

37716
24bb91462892
remove primitive operation Heap.array in favour of Heap.array_of_list
haftmann
parents:
37714
diff
changeset

362 
hide_const (open) empty upd length array ref 
26170  363 

364 
end 