author  haftmann 
Thu, 08 Jan 2009 17:10:41 +0100  
changeset 29399  ebcd69a00872 
parent 28952  src/HOL/Library/Heap.thy@15a4b2cf8c34 
child 30738  0842e906300c 
permissions  rwrr 
26170  1 
(* Title: HOL/Library/Heap.thy 
2 
ID: $Id$ 

3 
Author: John Matthews, Galois Connections; Alexander Krauss, TU Muenchen 

4 
*) 

5 

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

7 

8 
theory Heap 

28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28524
diff
changeset

9 
imports Plain "~~/src/HOL/List" Countable Typerep 
26170  10 
begin 
11 

12 
subsection {* Representable types *} 

13 

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

15 

28335  16 
class heap = typerep + countable 
26170  17 

18 
text {* Instances for common HOL types *} 

19 

20 
instance nat :: heap .. 

21 

22 
instance "*" :: (heap, heap) heap .. 

23 

24 
instance "+" :: (heap, heap) heap .. 

25 

26 
instance list :: (heap) heap .. 

27 

28 
instance option :: (heap) heap .. 

29 

30 
instance int :: heap .. 

31 

32 
instance message_string :: countable 

33 
by (rule countable_classI [of "message_string_case to_nat"]) 

34 
(auto split: message_string.splits) 

35 

36 
instance message_string :: heap .. 

37 

38 
text {* Reflected types themselves are heaprepresentable *} 

39 

28335  40 
instantiation typerep :: countable 
26170  41 
begin 
42 

28335  43 
fun to_nat_typerep :: "typerep \<Rightarrow> nat" where 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28524
diff
changeset

44 
"to_nat_typerep (Typerep.Typerep c ts) = to_nat (to_nat c, to_nat (map to_nat_typerep ts))" 
26170  45 

26932  46 
instance 
47 
proof (rule countable_classI) 

28335  48 
fix t t' :: typerep and ts 
49 
have "(\<forall>t'. to_nat_typerep t = to_nat_typerep t' \<longrightarrow> t = t') 

50 
\<and> (\<forall>ts'. map to_nat_typerep ts = map to_nat_typerep ts' \<longrightarrow> ts = ts')" 

51 
proof (induct rule: typerep.induct) 

52 
case (Typerep c ts) show ?case 

26170  53 
proof (rule allI, rule impI) 
54 
fix t' 

28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28524
diff
changeset

55 
assume hyp: "to_nat_typerep (Typerep.Typerep c ts) = to_nat_typerep t'" 
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28524
diff
changeset

56 
then obtain c' ts' where t': "t' = (Typerep.Typerep c' ts')" 
26170  57 
by (cases t') auto 
28335  58 
with Typerep hyp have "c = c'" and "ts = ts'" by simp_all 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28524
diff
changeset

59 
with t' show "Typerep.Typerep c ts = t'" by simp 
26170  60 
qed 
61 
next 

28335  62 
case Nil_typerep then show ?case by simp 
26170  63 
next 
28335  64 
case (Cons_typerep t ts) then show ?case by auto 
26170  65 
qed 
28335  66 
then have "to_nat_typerep t = to_nat_typerep t' \<Longrightarrow> t = t'" by auto 
67 
moreover assume "to_nat_typerep t = to_nat_typerep t'" 

26170  68 
ultimately show "t = t'" by simp 
69 
qed 

70 

71 
end 

72 

28335  73 
instance typerep :: heap .. 
26170  74 

75 

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

77 

78 
types addr = nat  "untyped heap references" 

79 

80 
datatype 'a array = Array addr 

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

82 

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

84 
"addr_of_array (Array x) = x" 

85 

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

87 
"addr_of_ref (Ref x) = x" 

88 

89 
lemma addr_of_array_inj [simp]: 

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

91 
by (cases a, cases a') simp_all 

92 

93 
lemma addr_of_ref_inj [simp]: 

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

95 
by (cases r, cases r') simp_all 

96 

97 
instance array :: (type) countable 

98 
by (rule countable_classI [of addr_of_array]) simp 

99 

100 
instance ref :: (type) countable 

101 
by (rule countable_classI [of addr_of_ref]) simp 

102 

103 
setup {* 

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

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

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

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

108 
*} 

109 

110 
types heap_rep = nat  "representable values" 

111 

112 
record heap = 

28335  113 
arrays :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep list" 
114 
refs :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep" 

26170  115 
lim :: addr 
116 

117 
definition empty :: heap where 

28524  118 
"empty = \<lparr>arrays = (\<lambda>_. undefined), refs = (\<lambda>_. undefined), lim = 0\<rparr>"  "why undefined?" 
26170  119 

120 

121 
subsection {* Imperative references and arrays *} 

122 

123 
text {* 

124 
References and arrays are developed in parallel, 

26586  125 
but keeping them separate makes some later proofs simpler. 
26170  126 
*} 
127 

128 
subsubsection {* Primitive operations *} 

129 

130 
definition 

131 
new_ref :: "heap \<Rightarrow> ('a\<Colon>heap) ref \<times> heap" where 

132 
"new_ref h = (let l = lim h in (Ref l, h\<lparr>lim := l + 1\<rparr>))" 

133 

134 
definition 

135 
new_array :: "heap \<Rightarrow> ('a\<Colon>heap) array \<times> heap" where 

136 
"new_array h = (let l = lim h in (Array l, h\<lparr>lim := l + 1\<rparr>))" 

137 

138 
definition 

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

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

141 

142 
definition 

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

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

145 

146 
definition 

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

28335  148 
"get_ref r h = from_nat (refs h (TYPEREP('a)) (addr_of_ref r))" 
26170  149 

150 
definition 

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

28335  152 
"get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))" 
26170  153 

154 
definition 

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

156 
"set_ref r x = 

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

159 
definition 

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

161 
"set_array a x = 

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

164 
subsubsection {* Interface operations *} 

165 

166 
definition 

167 
ref :: "'a \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap ref \<times> heap" where 

168 
"ref x h = (let (r, h') = new_ref h; 

169 
h'' = set_ref r x h' 

170 
in (r, h''))" 

171 

172 
definition 

173 
array :: "nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where 

174 
"array n x h = (let (r, h') = new_array h; 

175 
h'' = set_array r (replicate n x) h' 

176 
in (r, h''))" 

177 

178 
definition 

179 
array_of_list :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where 

180 
"array_of_list xs h = (let (r, h') = new_array h; 

181 
h'' = set_array r xs h' 

182 
in (r, h''))" 

183 

184 
definition 

185 
upd :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where 

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

187 

188 
definition 

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

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

191 

192 
definition 

193 
array_ran :: "('a\<Colon>heap) option array \<Rightarrow> heap \<Rightarrow> 'a set" where 

194 
"array_ran a h = {e. Some e \<in> set (get_array a h)}" 

195 
 {*FIXME*} 

196 

197 

198 
subsubsection {* Reference equality *} 

199 

200 
text {* 

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

202 
*} 

203 

204 
definition 

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

206 
where 

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

209 
definition 

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

211 
where 

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

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

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

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

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

218 
unfolding noteq_refs_def noteq_arrs_def by auto 

219 

220 
lemma present_new_ref: "ref_present r h \<Longrightarrow> r =!= fst (ref v h)" 

221 
by (simp add: ref_present_def new_ref_def ref_def Let_def noteq_refs_def) 

222 

223 
lemma present_new_arr: "array_present a h \<Longrightarrow> a =!!= fst (array v x h)" 

224 
by (simp add: array_present_def noteq_arrs_def new_array_def array_def Let_def) 

225 

226 

227 
subsubsection {* Properties of heap containers *} 

228 

229 
text {* Properties of imperative arrays *} 

230 

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

232 
the literature? *} 

233 

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

235 
by (simp add: get_array_def set_array_def) 

236 

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

238 
by (simp add: noteq_arrs_def get_array_def set_array_def) 

239 

240 
lemma set_array_same [simp]: 

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

242 
by (simp add: set_array_def) 

243 

244 
lemma array_set_set_swap: 

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

246 
by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def) 

247 

248 
lemma array_ref_set_set_swap: 

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

250 
by (simp add: Let_def expand_fun_eq set_array_def set_ref_def) 

251 

252 
lemma get_array_upd_eq [simp]: 

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

254 
by (simp add: upd_def) 

255 

256 
lemma nth_upd_array_neq_array [simp]: 

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

258 
by (simp add: upd_def noteq_arrs_def) 

259 

260 
lemma get_arry_array_upd_elem_neqIndex [simp]: 

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

262 
by simp 

263 

264 
lemma length_upd_eq [simp]: 

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

266 
by (simp add: length_def upd_def) 

267 

268 
lemma length_upd_neq [simp]: 

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

270 
by (simp add: upd_def length_def set_array_def get_array_def) 

271 

272 
lemma upd_swap_neqArray: 

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

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

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

276 
apply (unfold upd_def) 

277 
apply simp 

278 
apply (subst array_set_set_swap, assumption) 

279 
apply (subst array_get_set_neq) 

280 
apply (erule noteq_arrs_sym) 

281 
apply (simp) 

282 
done 

283 

284 
lemma upd_swap_neqIndex: 

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

286 
by (auto simp add: upd_def array_set_set_swap list_update_swap) 

287 

288 
lemma get_array_init_array_list: 

289 
"get_array (fst (array_of_list ls h)) (snd (array_of_list ls' h)) = ls'" 

290 
by (simp add: Let_def split_def array_of_list_def) 

291 

292 
lemma set_array: 

293 
"set_array (fst (array_of_list ls h)) 

294 
new_ls (snd (array_of_list ls h)) 

295 
= snd (array_of_list new_ls h)" 

296 
by (simp add: Let_def split_def array_of_list_def) 

297 

298 
lemma array_present_upd [simp]: 

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

300 
by (simp add: upd_def array_present_def set_array_def get_array_def) 

301 

302 
lemma array_of_list_replicate: 

303 
"array_of_list (replicate n x) = array n x" 

304 
by (simp add: expand_fun_eq array_of_list_def array_def) 

305 

306 

307 
text {* Properties of imperative references *} 

308 

309 
lemma next_ref_fresh [simp]: 

310 
assumes "(r, h') = new_ref h" 

311 
shows "\<not> ref_present r h" 

312 
using assms by (cases h) (auto simp add: new_ref_def ref_present_def Let_def) 

313 

314 
lemma next_ref_present [simp]: 

315 
assumes "(r, h') = new_ref h" 

316 
shows "ref_present r h'" 

317 
using assms by (cases h) (auto simp add: new_ref_def ref_present_def Let_def) 

318 

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

320 
by (simp add: get_ref_def set_ref_def) 

321 

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

323 
by (simp add: noteq_refs_def get_ref_def set_ref_def) 

324 

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

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

327 
from all existing refs. 

328 
*) 

329 

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

331 
apply (simp add: set_ref_def get_ref_def) 

332 
oops 

333 

334 
lemma set_ref_same[simp]: 

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

336 
by (simp add: set_ref_def) 

337 

338 
lemma ref_set_set_swap: 

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

340 
by (simp add: Let_def expand_fun_eq noteq_refs_def set_ref_def) 

341 

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

343 
by (simp add: ref_def new_ref_def set_ref_def Let_def) 

344 

345 
lemma ref_get_new [simp]: 

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

347 
by (simp add: ref_def Let_def split_def) 

348 

349 
lemma ref_set_new [simp]: 

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

351 
by (simp add: ref_def Let_def split_def) 

352 

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

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

355 
by (simp add: get_ref_def set_ref_def ref_def Let_def new_ref_def noteq_refs_def) 

356 

357 
lemma lim_set_ref [simp]: 

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

359 
by (simp add: set_ref_def) 

360 

361 
lemma ref_present_new_ref [simp]: 

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

363 
by (simp add: new_ref_def ref_present_def ref_def Let_def) 

364 

365 
lemma ref_present_set_ref [simp]: 

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

367 
by (simp add: set_ref_def ref_present_def) 

368 

369 
lemma array_ranI: "\<lbrakk> Some b = get_array a h ! i; i < Heap.length a h \<rbrakk> \<Longrightarrow> b \<in> array_ran a h" 

370 
unfolding array_ran_def Heap.length_def by simp 

371 

372 
lemma array_ran_upd_array_Some: 

373 
assumes "cl \<in> array_ran a (Heap.upd a i (Some b) h)" 

374 
shows "cl \<in> array_ran a h \<or> cl = b" 

375 
proof  

376 
have "set (get_array a h[i := Some b]) \<subseteq> insert (Some b) (set (get_array a h))" by (rule set_update_subset_insert) 

377 
with assms show ?thesis 

378 
unfolding array_ran_def Heap.upd_def by fastsimp 

379 
qed 

380 

381 
lemma array_ran_upd_array_None: 

382 
assumes "cl \<in> array_ran a (Heap.upd a i None h)" 

383 
shows "cl \<in> array_ran a h" 

384 
proof  

385 
have "set (get_array a h[i := None]) \<subseteq> insert None (set (get_array a h))" by (rule set_update_subset_insert) 

386 
with assms show ?thesis 

387 
unfolding array_ran_def Heap.upd_def by auto 

388 
qed 

389 

390 

391 
text {* Noninteraction between imperative array and imperative references *} 

392 

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

394 
by (simp add: get_array_def set_ref_def) 

395 

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

397 
by simp 

398 

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

400 
by (simp add: get_ref_def set_array_def upd_def) 

401 

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

403 
by (simp add: set_array_def get_array_def Let_def ref_new_set upd_def ref_def new_ref_def) 

404 

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

408 
apply (simp add: Let_def upd_def) 

409 
apply auto 

26300  410 
oops 
26170  411 

412 
lemma length_new_ref[simp]: 

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

414 
by (simp add: get_array_def set_ref_def length_def new_ref_def ref_def Let_def) 

415 

416 
lemma get_array_new_ref [simp]: 

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

418 
by (simp add: new_ref_def ref_def set_ref_def get_array_def Let_def) 

419 

420 
lemma ref_present_upd [simp]: 

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

422 
by (simp add: upd_def ref_present_def set_array_def get_array_def) 

423 

424 
lemma array_present_set_ref [simp]: 

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

426 
by (simp add: array_present_def set_ref_def) 

427 

428 
lemma array_present_new_ref [simp]: 

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

430 
by (simp add: array_present_def new_ref_def ref_def Let_def) 

431 

432 
hide (open) const empty array array_of_list upd length ref 

433 

434 
end 