|
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 |
|
10 theory Heap = Main: |
|
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 |