13875
|
1 |
(* Title: HOL/Hoare/Heap.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 2002 TUM
|
|
5 |
|
|
6 |
Pointers, heaps and heap abstractions.
|
|
7 |
See the paper by Mehta and Nipkow.
|
|
8 |
*)
|
|
9 |
|
16417
|
10 |
theory Heap imports Main begin
|
13875
|
11 |
|
|
12 |
subsection "References"
|
|
13 |
|
|
14 |
datatype 'a ref = Null | Ref 'a
|
|
15 |
|
|
16 |
lemma not_Null_eq [iff]: "(x ~= Null) = (EX y. x = Ref y)"
|
|
17 |
by (induct x) auto
|
|
18 |
|
|
19 |
lemma not_Ref_eq [iff]: "(ALL y. x ~= Ref y) = (x = Null)"
|
|
20 |
by (induct x) auto
|
|
21 |
|
|
22 |
consts addr :: "'a ref \<Rightarrow> 'a"
|
|
23 |
primrec "addr(Ref a) = a"
|
|
24 |
|
|
25 |
|
|
26 |
section "The heap"
|
|
27 |
|
|
28 |
subsection "Paths in the heap"
|
|
29 |
|
|
30 |
consts
|
|
31 |
Path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
|
|
32 |
primrec
|
|
33 |
"Path h x [] y = (x = y)"
|
|
34 |
"Path h x (a#as) y = (x = Ref a \<and> Path h (h a) as y)"
|
|
35 |
|
|
36 |
lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)"
|
|
37 |
apply(case_tac xs)
|
|
38 |
apply fastsimp
|
|
39 |
apply fastsimp
|
|
40 |
done
|
|
41 |
|
|
42 |
lemma [simp]: "Path h (Ref a) as z =
|
|
43 |
(as = [] \<and> z = Ref a \<or> (\<exists>bs. as = a#bs \<and> Path h (h a) bs z))"
|
|
44 |
apply(case_tac as)
|
|
45 |
apply fastsimp
|
|
46 |
apply fastsimp
|
|
47 |
done
|
|
48 |
|
|
49 |
lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
|
|
50 |
by(induct as, simp+)
|
|
51 |
|
|
52 |
lemma Path_upd[simp]:
|
|
53 |
"\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
|
|
54 |
by(induct as, simp, simp add:eq_sym_conv)
|
|
55 |
|
|
56 |
lemma Path_snoc:
|
|
57 |
"Path (f(a := q)) p as (Ref a) \<Longrightarrow> Path (f(a := q)) p (as @ [a]) q"
|
|
58 |
by simp
|
|
59 |
|
|
60 |
|
|
61 |
subsection "Lists on the heap"
|
|
62 |
|
|
63 |
subsubsection "Relational abstraction"
|
|
64 |
|
|
65 |
constdefs
|
|
66 |
List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool"
|
|
67 |
"List h x as == Path h x as Null"
|
|
68 |
|
|
69 |
lemma [simp]: "List h x [] = (x = Null)"
|
|
70 |
by(simp add:List_def)
|
|
71 |
|
|
72 |
lemma [simp]: "List h x (a#as) = (x = Ref a \<and> List h (h a) as)"
|
|
73 |
by(simp add:List_def)
|
|
74 |
|
|
75 |
lemma [simp]: "List h Null as = (as = [])"
|
|
76 |
by(case_tac as, simp_all)
|
|
77 |
|
|
78 |
lemma List_Ref[simp]: "List h (Ref a) as = (\<exists>bs. as = a#bs \<and> List h (h a) bs)"
|
|
79 |
by(case_tac as, simp_all, fast)
|
|
80 |
|
|
81 |
theorem notin_List_update[simp]:
|
|
82 |
"\<And>x. a \<notin> set as \<Longrightarrow> List (h(a := y)) x as = List h x as"
|
|
83 |
apply(induct as)
|
|
84 |
apply simp
|
|
85 |
apply(clarsimp simp add:fun_upd_apply)
|
|
86 |
done
|
|
87 |
|
|
88 |
lemma List_unique: "\<And>x bs. List h x as \<Longrightarrow> List h x bs \<Longrightarrow> as = bs"
|
|
89 |
by(induct as, simp, clarsimp)
|
|
90 |
|
|
91 |
lemma List_unique1: "List h p as \<Longrightarrow> \<exists>!as. List h p as"
|
|
92 |
by(blast intro:List_unique)
|
|
93 |
|
|
94 |
lemma List_app: "\<And>x. List h x (as@bs) = (\<exists>y. Path h x as y \<and> List h y bs)"
|
|
95 |
by(induct as, simp, clarsimp)
|
|
96 |
|
|
97 |
lemma List_hd_not_in_tl[simp]: "List h (h a) as \<Longrightarrow> a \<notin> set as"
|
|
98 |
apply (clarsimp simp add:in_set_conv_decomp)
|
|
99 |
apply(frule List_app[THEN iffD1])
|
|
100 |
apply(fastsimp dest: List_unique)
|
|
101 |
done
|
|
102 |
|
|
103 |
lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
|
|
104 |
apply(induct as, simp)
|
|
105 |
apply(fastsimp dest:List_hd_not_in_tl)
|
|
106 |
done
|
|
107 |
|
|
108 |
subsection "Functional abstraction"
|
|
109 |
|
|
110 |
constdefs
|
|
111 |
islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool"
|
|
112 |
"islist h p == \<exists>as. List h p as"
|
|
113 |
list :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list"
|
|
114 |
"list h p == SOME as. List h p as"
|
|
115 |
|
|
116 |
lemma List_conv_islist_list: "List h p as = (islist h p \<and> as = list h p)"
|
|
117 |
apply(simp add:islist_def list_def)
|
|
118 |
apply(rule iffI)
|
|
119 |
apply(rule conjI)
|
|
120 |
apply blast
|
|
121 |
apply(subst some1_equality)
|
|
122 |
apply(erule List_unique1)
|
|
123 |
apply assumption
|
|
124 |
apply(rule refl)
|
|
125 |
apply simp
|
|
126 |
apply(rule someI_ex)
|
|
127 |
apply fast
|
|
128 |
done
|
|
129 |
|
|
130 |
lemma [simp]: "islist h Null"
|
|
131 |
by(simp add:islist_def)
|
|
132 |
|
|
133 |
lemma [simp]: "islist h (Ref a) = islist h (h a)"
|
|
134 |
by(simp add:islist_def)
|
|
135 |
|
|
136 |
lemma [simp]: "list h Null = []"
|
|
137 |
by(simp add:list_def)
|
|
138 |
|
|
139 |
lemma list_Ref_conv[simp]:
|
|
140 |
"islist h (h a) \<Longrightarrow> list h (Ref a) = a # list h (h a)"
|
|
141 |
apply(insert List_Ref[of h])
|
|
142 |
apply(fastsimp simp:List_conv_islist_list)
|
|
143 |
done
|
|
144 |
|
|
145 |
lemma [simp]: "islist h (h a) \<Longrightarrow> a \<notin> set(list h (h a))"
|
|
146 |
apply(insert List_hd_not_in_tl[of h])
|
|
147 |
apply(simp add:List_conv_islist_list)
|
|
148 |
done
|
|
149 |
|
|
150 |
lemma list_upd_conv[simp]:
|
|
151 |
"islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> list (h(y := q)) p = list h p"
|
|
152 |
apply(drule notin_List_update[of _ _ h q p])
|
|
153 |
apply(simp add:List_conv_islist_list)
|
|
154 |
done
|
|
155 |
|
|
156 |
lemma islist_upd[simp]:
|
|
157 |
"islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> islist (h(y := q)) p"
|
|
158 |
apply(frule notin_List_update[of _ _ h q p])
|
|
159 |
apply(simp add:List_conv_islist_list)
|
|
160 |
done
|
|
161 |
|
|
162 |
end
|