Quelle Heap.thy Sprache: Isabelle

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

section \<open>Pointers, heaps and heap abstractions\<close>

text \<open>See the paper by Mehta and Nipkow.\<close>

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 = [] \<and> z = Ref a  \<or>  (\<exists>bs. as = a#bs \<and> 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\<open>The term \<^term>\<open>distPath h x as y\<close> expresses the fact that a
non-repeating path \<^term>\<open>as\<close> connects location \<^term>\<open>x\<close> to location
\<^term>\<open>y\<close> by means of the \<^term>\<open>h\<close> field. In the case where \<open>x
= y\<close>, and there is a cycle from \<^term>\<open>x\<close> to itself, \<^term>\<open>as\<close> can
be both \<^term>\<open>[]\<close> and the non-repeating list of nodes in the
cycle.\<close>

lemma neq_dP: "p \ q \ Path h p Ps q \ distinct Ps \
\<exists>a Qs. p = Ref a \<and> Ps = a#Qs \<and> a \<notin> set Qs"
by (case_tac Ps, auto)

lemma neq_dP_disp: "\ p \ q; distPath h p Ps q \ \
\<exists>a Qs. p = Ref a \<and> Ps = a#Qs \<and> a \<notin> 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

quality97%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.