14074
|
1 |
(* Title: HOL/Hoare/Heap.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 2002 TUM
|
|
5 |
|
|
6 |
Heap abstractions (at the moment only Path and List)
|
|
7 |
for Separation Logic.
|
|
8 |
*)
|
|
9 |
|
|
10 |
theory SepLogHeap = Main:
|
|
11 |
|
|
12 |
types heap = "(nat \<Rightarrow> nat option)"
|
|
13 |
|
|
14 |
text{* Some means allocated, none means free. Address 0 serves as the
|
|
15 |
null reference. *}
|
|
16 |
|
|
17 |
subsection "Paths in the heap"
|
|
18 |
|
|
19 |
consts
|
|
20 |
Path :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
|
|
21 |
primrec
|
|
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))"
|
|
24 |
|
|
25 |
lemma [iff]: "Path h 0 xs y = (xs = [] \<and> y = 0)"
|
|
26 |
apply(case_tac xs)
|
|
27 |
apply fastsimp
|
|
28 |
apply fastsimp
|
|
29 |
done
|
|
30 |
|
|
31 |
lemma [simp]: "x\<noteq>0 \<Longrightarrow> Path h x as z =
|
|
32 |
(as = [] \<and> z = x \<or> (\<exists>y bs. as = x#bs \<and> h x = Some y & Path h y bs z))"
|
|
33 |
apply(case_tac as)
|
|
34 |
apply fastsimp
|
|
35 |
apply fastsimp
|
|
36 |
done
|
|
37 |
|
|
38 |
lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
|
|
39 |
by(induct as, auto)
|
|
40 |
|
|
41 |
lemma Path_upd[simp]:
|
|
42 |
"\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
|
|
43 |
by(induct as, simp, simp add:eq_sym_conv)
|
|
44 |
|
|
45 |
|
|
46 |
subsection "Lists on the heap"
|
|
47 |
|
|
48 |
constdefs
|
|
49 |
List :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool"
|
|
50 |
"List h x as == Path h x as 0"
|
|
51 |
|
|
52 |
lemma [simp]: "List h x [] = (x = 0)"
|
|
53 |
by(simp add:List_def)
|
|
54 |
|
|
55 |
lemma [simp]:
|
|
56 |
"List h x (a#as) = (x\<noteq>0 \<and> a=x \<and> (\<exists>y. h x = Some y \<and> List h y as))"
|
|
57 |
by(simp add:List_def)
|
|
58 |
|
|
59 |
lemma [simp]: "List h 0 as = (as = [])"
|
|
60 |
by(case_tac as, simp_all)
|
|
61 |
|
|
62 |
lemma List_non_null: "a\<noteq>0 \<Longrightarrow>
|
|
63 |
List h a as = (\<exists>b bs. as = a#bs \<and> h a = Some b \<and> List h b bs)"
|
|
64 |
by(case_tac as, simp_all)
|
|
65 |
|
|
66 |
theorem notin_List_update[simp]:
|
|
67 |
"\<And>x. a \<notin> set as \<Longrightarrow> List (h(a := y)) x as = List h x as"
|
|
68 |
apply(induct as)
|
|
69 |
apply simp
|
|
70 |
apply(clarsimp simp add:fun_upd_apply)
|
|
71 |
done
|
|
72 |
|
|
73 |
lemma List_unique: "\<And>x bs. List h x as \<Longrightarrow> List h x bs \<Longrightarrow> as = bs"
|
|
74 |
by(induct as, auto simp add:List_non_null)
|
|
75 |
|
|
76 |
lemma List_unique1: "List h p as \<Longrightarrow> \<exists>!as. List h p as"
|
|
77 |
by(blast intro:List_unique)
|
|
78 |
|
|
79 |
lemma List_app: "\<And>x. List h x (as@bs) = (\<exists>y. Path h x as y \<and> List h y bs)"
|
|
80 |
by(induct as, auto)
|
|
81 |
|
|
82 |
lemma List_hd_not_in_tl[simp]: "List h b as \<Longrightarrow> h a = Some b \<Longrightarrow> a \<notin> set as"
|
|
83 |
apply (clarsimp simp add:in_set_conv_decomp)
|
|
84 |
apply(frule List_app[THEN iffD1])
|
|
85 |
apply(fastsimp dest: List_unique)
|
|
86 |
done
|
|
87 |
|
|
88 |
lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
|
|
89 |
apply(induct as, simp)
|
|
90 |
apply(fastsimp dest:List_hd_not_in_tl)
|
|
91 |
done
|
|
92 |
|
|
93 |
lemma list_in_heap: "\<And>p. List h p ps \<Longrightarrow> set ps \<subseteq> dom h"
|
|
94 |
by(induct ps, auto)
|
|
95 |
|
|
96 |
lemma list_ortho_sum1[simp]:
|
|
97 |
"\<And>p. \<lbrakk> List h1 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps"
|
|
98 |
by(induct ps, auto simp add:map_add_def split:option.split)
|
|
99 |
|
|
100 |
lemma list_ortho_sum2[simp]:
|
|
101 |
"\<And>p. \<lbrakk> List h2 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps"
|
|
102 |
by(induct ps, auto simp add:map_add_def split:option.split)
|
|
103 |
|
|
104 |
end
|