(* Title: HOL/Hoare/SepLogHeap.thy Author: Tobias Nipkow Copyright 2002 TUM
*)
section \<open>Heap abstractions for Separation Logic\<close>
text\<open>(at the moment only Path and List)\<close>
theory SepLogHeap imports Main begin
type_synonym heap = "(nat \ nat option)"
text\<open>\<open>Some\<close> means allocated, \<open>None\<close> means
free. Address \<open>0\<close> serves as the null reference.\<close>
subsection "Paths in the heap"
primrec Path :: "heap \ nat \ nat list \ nat \ bool" where "Path h x [] y = (x = y)"
| "Path h x (a#as) y = (x\0 \ a=x \ (\b. h x = Some b \ Path h b as y))"
lemma [iff]: "Path h 0 xs y = (xs = [] \ y = 0)" by (cases xs) simp_all
lemma [simp]: "x\0 \ Path h x as z =
(as = [] \<and> z = x \<or> (\<exists>y bs. as = x#bs \<and> h x = Some y & Path h y bs z))" by (cases as) auto
lemma [simp]: "\x. Path f x (as@bs) z = (\y. Path f x as y \ Path f y bs z)" by (induct as) auto
lemma Path_upd[simp]: "\x. u \ set as \ Path (f(u := v)) x as y = Path f x as y" by (induct as) simp_all
subsection "Lists on the heap"
definition List :: "heap \ nat \ nat list \ bool" where"List h x as = Path h x as 0"
lemma [simp]: "List h x [] = (x = 0)" by (simp add: List_def)
lemma [simp]: "List h x (a#as) = (x\0 \ a=x \ (\y. h x = Some y \ List h y as))" by (simp add: List_def)
lemma [simp]: "List h 0 as = (as = [])" by (cases as) simp_all
lemma List_non_null: "a\0 \
List h a as = (\<exists>b bs. as = a#bs \<and> h a = Some b \<and> List h b bs)" by (cases as) simp_all
theorem notin_List_update[simp]: "\x. a \ set as \ List (h(a := y)) x as = List h x as" by (induct as) simp_all
lemma List_unique: "\x bs. List h x as \ List h x bs \ as = bs" by (induct as) (auto simp add:List_non_null)
lemma List_unique1: "List h p as \ \!as. List h p as" by (blast intro: List_unique)
lemma List_app: "\x. List h x (as@bs) = (\y. Path h x as y \ List h y bs)" by (induct as) auto
lemma List_hd_not_in_tl[simp]: "List h b as \ h a = Some b \ a \ set as" apply (clarsimp simp add:in_set_conv_decomp) apply(frule List_app[THEN iffD1]) apply(fastforce dest: List_unique) done
lemma List_distinct[simp]: "\x. List h x as \ distinct as" by (induct as) (auto dest:List_hd_not_in_tl)
lemma list_in_heap: "\p. List h p ps \ set ps \ dom h" by (induct ps) auto
lemma list_ortho_sum1[simp]: "\p. \ List h1 p ps; dom h1 \ dom h2 = {}\ \ List (h1++h2) p ps" by (induct ps) (auto simp add:map_add_def split:option.split)
lemma list_ortho_sum2[simp]: "\p. \ List h2 p ps; dom h1 \ dom h2 = {}\ \ List (h1++h2) p ps" by (induct ps) (auto simp add:map_add_def split:option.split)
end
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
