equal
deleted
inserted
replaced
266 constdefs |
266 constdefs |
267 new_Addr :: "heap \<Rightarrow> loc option" |
267 new_Addr :: "heap \<Rightarrow> loc option" |
268 "new_Addr h \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (SOME a. h a = None)" |
268 "new_Addr h \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (SOME a. h a = None)" |
269 |
269 |
270 lemma new_AddrD: "new_Addr h = Some a \<Longrightarrow> h a = None" |
270 lemma new_AddrD: "new_Addr h = Some a \<Longrightarrow> h a = None" |
271 apply (unfold new_Addr_def) |
271 apply (auto simp add: not_Some_eq new_Addr_def) |
272 apply auto |
272 apply (erule someI) |
273 apply (case_tac "h (SOME a\<Colon>loc. h a = None)") |
|
274 apply simp |
|
275 apply (fast intro: someI2) |
|
276 done |
273 done |
277 |
274 |
278 lemma new_AddrD2: "new_Addr h = Some a \<Longrightarrow> \<forall>b. h b \<noteq> None \<longrightarrow> b \<noteq> a" |
275 lemma new_AddrD2: "new_Addr h = Some a \<Longrightarrow> \<forall>b. h b \<noteq> None \<longrightarrow> b \<noteq> a" |
279 apply (drule new_AddrD) |
276 apply (drule new_AddrD) |
280 apply auto |
277 apply auto |
281 done |
278 done |
282 |
279 |
283 lemma new_Addr_SomeI: "h a = None \<Longrightarrow> \<exists>b. new_Addr h = Some b \<and> h b = None" |
280 lemma new_Addr_SomeI: "h a = None \<Longrightarrow> \<exists>b. new_Addr h = Some b \<and> h b = None" |
284 apply (unfold new_Addr_def) |
281 apply (simp add: new_Addr_def not_Some_eq) |
285 apply (frule not_Some_eq [THEN iffD2]) |
282 apply (fast intro: someI2) |
286 apply auto |
|
287 apply (drule not_Some_eq [THEN iffD2]) |
|
288 apply auto |
|
289 apply (fast intro!: someI2) |
|
290 done |
283 done |
291 |
284 |
292 |
285 |
293 subsection "initialization" |
286 subsection "initialization" |
294 |
287 |