Quelle  Heap.thy   Sprache: Isabelle

(*  Title:      HOL/Hoare/Heap.thy
    Author:     Tobias Nipkow
    Copyright   2002 TUM
*)

section ‹Pointers, heaps and heap abstractions›

text ‹See the paper by Mehta and Nipkow.›

theory Heap
  imports Main
begin

subsection "References"

datatype 'a ref = Null | Ref 'a

lemma not_Null_eq [iff]: "(x \ Null) = (\y. x = Ref y)"
  by (induct x) auto

lemma not_Ref_eq [iff]: "(\y. x \ Ref y) = (x = Null)"
  by (induct x) auto

primrec addr :: "'a ref \ 'a" where
  "addr (Ref a) = a"


subsection "The heap"

subsubsection "Paths in the heap"

primrec Path :: "('a \ 'a ref) \ 'a ref \ 'a list \ 'a ref \ bool" where
  "Path h x [] y \ x = y"
| "Path h x (a#as) y \ x = Ref a \ Path h (h a) as y"

lemma [iff]: "Path h Null xs y = (xs = [] \ y = Null)"
apply(case_tac xs)
apply fastforce
apply fastforce
done

lemma [simp]: "Path h (Ref a) as z =
 (as = [] ∧ z = Ref a  ∨  (∃bs. as = a#bs ∧ Path h (h a) bs z))"
apply(case_tac as)
apply fastforce
apply fastforce
done

lemma [simp]: "\x. Path f x (as@bs) z = (\y. Path f x as y \ Path f y bs z)"
by(induct as, simp+)

lemma Path_upd[simp]:
 "\x. u \ set as \ Path (f(u := v)) x as y = Path f x as y"
by(induct as, simp, simp add:eq_sym_conv)

lemma Path_snoc:
 "Path (f(a := q)) p as (Ref a) \ Path (f(a := q)) p (as @ [a]) q"
by simp


subsubsection "Non-repeating paths"

definition distPath :: "('a \ 'a ref) \ 'a ref \ 'a list \ 'a ref \ bool"
  where "distPath h x as y \ Path h x as y \ distinct as"

text‹The term 🍋‹distPath h x as y› expresses the fact that a
non-repeating path 🍋‹as› connects location 🍋‹x› to location
🍋‹y› by means of the 🍋‹h› field. In the case where ‹x
= y›, and there is a cycle from 🍋‹x› to itself, 🍋‹as› can
be both 🍋‹[]› and the non-repeating list of nodes in the
cycle.›

lemma neq_dP: "p \ q \ Path h p Ps q \ distinct Ps \
 ∃a Qs. p = Ref a ∧ Ps = a#Qs ∧ a ∉ set Qs"
by (case_tac Ps, auto)


lemma neq_dP_disp: "\ p \ q; distPath h p Ps q \ \
 ∃a Qs. p = Ref a ∧ Ps = a#Qs ∧ a ∉ set Qs"
apply (simp only:distPath_def)
by (case_tac Ps, auto)


subsubsection "Lists on the heap"

paragraph "Relational abstraction"

definition List :: "('a \ 'a ref) \ 'a ref \ 'a list \ bool"
  where "List h x as = Path h x as Null"

lemma [simp]: "List h x [] = (x = Null)"
by(simp add:List_def)

lemma [simp]: "List h x (a#as) = (x = Ref a \ List h (h a) as)"
by(simp add:List_def)

lemma [simp]: "List h Null as = (as = [])"
by(case_tac as, simp_all)

lemma List_Ref[simp]: "List h (Ref a) as = (\bs. as = a#bs \ List h (h a) bs)"
by(case_tac as, simp_all, fast)

theorem notin_List_update[simp]:
 "\x. a \ set as \ List (h(a := y)) x as = List h x as"
apply(induct as)
apply simp
apply(clarsimp simp add:fun_upd_apply)
done

lemma List_unique: "\x bs. List h x as \ List h x bs \ as = bs"
by(induct as, simp, clarsimp)

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, simp, clarsimp)

lemma List_hd_not_in_tl[simp]: "List h (h a) as \ 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"
apply(induct as, simp)
apply(fastforce dest:List_hd_not_in_tl)
done

lemma Path_is_List:
  "\Path h b Ps (Ref a); a \ set Ps\ \ List (h(a := Null)) b (Ps @ [a])"
apply (induct Ps arbitrary: b)
apply (auto simp add:fun_upd_apply)
done


subsubsection "Functional abstraction"

definition islist :: "('a \ 'a ref) \ 'a ref \ bool"
  where "islist h p \ (\as. List h p as)"

definition list :: "('a \ 'a ref) \ 'a ref \ 'a list"
  where "list h p = (SOME as. List h p as)"

lemma List_conv_islist_list: "List h p as = (islist h p \ as = list h p)"
apply(simp add:islist_def list_def)
apply(rule iffI)
apply(rule conjI)
apply blast
apply(subst some1_equality)
  apply(erule List_unique1)
 apply assumption
apply(rule refl)
apply simp
apply(rule someI_ex)
apply fast
done

lemma [simp]: "islist h Null"
by(simp add:islist_def)

lemma [simp]: "islist h (Ref a) = islist h (h a)"
by(simp add:islist_def)

lemma [simp]: "list h Null = []"
by(simp add:list_def)

lemma list_Ref_conv[simp]:
 "islist h (h a) \ list h (Ref a) = a # list h (h a)"
apply(insert List_Ref[of h])
apply(fastforce simp:List_conv_islist_list)
done

lemma [simp]: "islist h (h a) \ a \ set(list h (h a))"
apply(insert List_hd_not_in_tl[of h])
apply(simp add:List_conv_islist_list)
done

lemma list_upd_conv[simp]:
 "islist h p \ y \ set(list h p) \ list (h(y := q)) p = list h p"
apply(drule notin_List_update[of _ _ h q p])
apply(simp add:List_conv_islist_list)
done

lemma islist_upd[simp]:
 "islist h p \ y \ set(list h p) \ islist (h(y := q)) p"
apply(frule notin_List_update[of _ _ h q p])
apply(simp add:List_conv_islist_list)
done

end