(* Title: HOL/Hoare/SepLogHeap.thy Author: Tobias Nipkow Copyright 2002 TUM Heap abstractions (at the moment only Path and List) for Separation Logic. *) theory SepLogHeap imports Main begin type_synonym heap = "(nat => nat option)" text{* @{text "Some"} means allocated, @{text "None"} means free. Address @{text "0"} serves as the null reference. *} 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 = [] ∧ z = x ∨ (∃y bs. as = x#bs ∧ 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 = (∃b bs. as = a#bs ∧ h a = Some b ∧ 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