theory SepLogHeap
imports Main
begin
type_synonym heap = "(nat ⇒ nat option)"
text‹‹Some› means allocated, ‹None› means
free. Address ‹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