author | wenzelm |
Sun, 22 Jul 2012 21:59:14 +0200 | |
changeset 48424 | e6b0c14f04c8 |
parent 44890 | 22f665a2e91c |
child 62042 | 6c6ccf573479 |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Hoare/SepLogHeap.thy |
14074 | 2 |
Author: Tobias Nipkow |
3 |
Copyright 2002 TUM |
|
4 |
||
5 |
Heap abstractions (at the moment only Path and List) |
|
6 |
for Separation Logic. |
|
7 |
*) |
|
8 |
||
18576 | 9 |
theory SepLogHeap |
10 |
imports Main |
|
11 |
begin |
|
18447 | 12 |
|
42174 | 13 |
type_synonym heap = "(nat \<Rightarrow> nat option)" |
14074 | 14 |
|
16972 | 15 |
text{* @{text "Some"} means allocated, @{text "None"} means |
16 |
free. Address @{text "0"} serves as the null reference. *} |
|
14074 | 17 |
|
18 |
subsection "Paths in the heap" |
|
19 |
||
38353 | 20 |
primrec Path :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool" |
21 |
where |
|
22 |
"Path h x [] y = (x = y)" |
|
23 |
| "Path h x (a#as) y = (x\<noteq>0 \<and> a=x \<and> (\<exists>b. h x = Some b \<and> Path h b as y))" |
|
14074 | 24 |
|
25 |
lemma [iff]: "Path h 0 xs y = (xs = [] \<and> y = 0)" |
|
16972 | 26 |
by (cases xs) simp_all |
14074 | 27 |
|
28 |
lemma [simp]: "x\<noteq>0 \<Longrightarrow> Path h x as z = |
|
29 |
(as = [] \<and> z = x \<or> (\<exists>y bs. as = x#bs \<and> h x = Some y & Path h y bs z))" |
|
16972 | 30 |
by (cases as) auto |
14074 | 31 |
|
32 |
lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)" |
|
16972 | 33 |
by (induct as) auto |
14074 | 34 |
|
35 |
lemma Path_upd[simp]: |
|
36 |
"\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y" |
|
16972 | 37 |
by (induct as) simp_all |
14074 | 38 |
|
39 |
||
40 |
subsection "Lists on the heap" |
|
41 |
||
38353 | 42 |
definition List :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool" |
43 |
where "List h x as = Path h x as 0" |
|
14074 | 44 |
|
45 |
lemma [simp]: "List h x [] = (x = 0)" |
|
16972 | 46 |
by (simp add: List_def) |
14074 | 47 |
|
48 |
lemma [simp]: |
|
49 |
"List h x (a#as) = (x\<noteq>0 \<and> a=x \<and> (\<exists>y. h x = Some y \<and> List h y as))" |
|
16972 | 50 |
by (simp add: List_def) |
14074 | 51 |
|
52 |
lemma [simp]: "List h 0 as = (as = [])" |
|
16972 | 53 |
by (cases as) simp_all |
14074 | 54 |
|
55 |
lemma List_non_null: "a\<noteq>0 \<Longrightarrow> |
|
56 |
List h a as = (\<exists>b bs. as = a#bs \<and> h a = Some b \<and> List h b bs)" |
|
16972 | 57 |
by (cases as) simp_all |
14074 | 58 |
|
59 |
theorem notin_List_update[simp]: |
|
60 |
"\<And>x. a \<notin> set as \<Longrightarrow> List (h(a := y)) x as = List h x as" |
|
16972 | 61 |
by (induct as) simp_all |
14074 | 62 |
|
63 |
lemma List_unique: "\<And>x bs. List h x as \<Longrightarrow> List h x bs \<Longrightarrow> as = bs" |
|
16972 | 64 |
by (induct as) (auto simp add:List_non_null) |
14074 | 65 |
|
66 |
lemma List_unique1: "List h p as \<Longrightarrow> \<exists>!as. List h p as" |
|
16972 | 67 |
by (blast intro: List_unique) |
14074 | 68 |
|
69 |
lemma List_app: "\<And>x. List h x (as@bs) = (\<exists>y. Path h x as y \<and> List h y bs)" |
|
16972 | 70 |
by (induct as) auto |
14074 | 71 |
|
72 |
lemma List_hd_not_in_tl[simp]: "List h b as \<Longrightarrow> h a = Some b \<Longrightarrow> a \<notin> set as" |
|
73 |
apply (clarsimp simp add:in_set_conv_decomp) |
|
74 |
apply(frule List_app[THEN iffD1]) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42174
diff
changeset
|
75 |
apply(fastforce dest: List_unique) |
14074 | 76 |
done |
77 |
||
78 |
lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as" |
|
16972 | 79 |
by (induct as) (auto dest:List_hd_not_in_tl) |
14074 | 80 |
|
81 |
lemma list_in_heap: "\<And>p. List h p ps \<Longrightarrow> set ps \<subseteq> dom h" |
|
16972 | 82 |
by (induct ps) auto |
14074 | 83 |
|
84 |
lemma list_ortho_sum1[simp]: |
|
85 |
"\<And>p. \<lbrakk> List h1 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps" |
|
16972 | 86 |
by (induct ps) (auto simp add:map_add_def split:option.split) |
14074 | 87 |
|
18447 | 88 |
|
14074 | 89 |
lemma list_ortho_sum2[simp]: |
90 |
"\<And>p. \<lbrakk> List h2 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps" |
|
16972 | 91 |
by (induct ps) (auto simp add:map_add_def split:option.split) |
14074 | 92 |
|
93 |
end |