author | kleing |
Wed, 20 Mar 2002 13:21:07 +0100 | |
changeset 13062 | 4b1edf2f6bd2 |
parent 13006 | 51c5f3f11d16 |
child 13068 | 472b1c91b09f |
permissions | -rw-r--r-- |
12516 | 1 |
(* Title: HOL/MicroJava/BV/Semilat.thy |
10496 | 2 |
ID: $Id$ |
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 2000 TUM |
|
5 |
||
6 |
Semilattices |
|
7 |
*) |
|
8 |
||
12911 | 9 |
header {* |
10 |
\chapter{Bytecode Verifier}\label{cha:bv} |
|
11 |
\isaheader{Semilattices} |
|
12 |
*} |
|
10496 | 13 |
|
12542 | 14 |
theory Semilat = While_Combinator: |
10496 | 15 |
|
13006 | 16 |
types 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool" |
17 |
'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
10496 | 18 |
'a sl = "'a set * 'a ord * 'a binop" |
19 |
||
20 |
consts |
|
13006 | 21 |
"@lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /<='__ _)" [50, 1000, 51] 50) |
22 |
"@lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /<'__ _)" [50, 1000, 51] 50) |
|
10496 | 23 |
defs |
24 |
lesub_def: "x <=_r y == r x y" |
|
25 |
lesssub_def: "x <_r y == x <=_r y & x ~= y" |
|
26 |
||
27 |
consts |
|
13006 | 28 |
"@plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /+'__ _)" [65, 1000, 66] 65) |
10496 | 29 |
defs |
30 |
plussub_def: "x +_f y == f x y" |
|
31 |
||
32 |
||
33 |
constdefs |
|
13006 | 34 |
ord :: "('a*'a)set \<Rightarrow> 'a ord" |
10496 | 35 |
"ord r == %x y. (x,y):r" |
36 |
||
13006 | 37 |
order :: "'a ord \<Rightarrow> bool" |
10496 | 38 |
"order r == (!x. x <=_r x) & |
13006 | 39 |
(!x y. x <=_r y & y <=_r x \<longrightarrow> x=y) & |
40 |
(!x y z. x <=_r y & y <=_r z \<longrightarrow> x <=_r z)" |
|
10496 | 41 |
|
13006 | 42 |
acc :: "'a ord \<Rightarrow> bool" |
10496 | 43 |
"acc r == wf{(y,x) . x <_r y}" |
44 |
||
13006 | 45 |
top :: "'a ord \<Rightarrow> 'a \<Rightarrow> bool" |
10496 | 46 |
"top r T == !x. x <=_r T" |
47 |
||
13006 | 48 |
closed :: "'a set \<Rightarrow> 'a binop \<Rightarrow> bool" |
10496 | 49 |
"closed A f == !x:A. !y:A. x +_f y : A" |
50 |
||
13006 | 51 |
semilat :: "'a sl \<Rightarrow> bool" |
10496 | 52 |
"semilat == %(A,r,f). order r & closed A f & |
53 |
(!x:A. !y:A. x <=_r x +_f y) & |
|
54 |
(!x:A. !y:A. y <=_r x +_f y) & |
|
13006 | 55 |
(!x:A. !y:A. !z:A. x <=_r z & y <=_r z \<longrightarrow> x +_f y <=_r z)" |
10496 | 56 |
|
13006 | 57 |
is_ub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
10496 | 58 |
"is_ub r x y u == (x,u):r & (y,u):r" |
59 |
||
13006 | 60 |
is_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
61 |
"is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)" |
|
10496 | 62 |
|
13006 | 63 |
some_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" |
10496 | 64 |
"some_lub r x y == SOME z. is_lub r x y z" |
65 |
||
66 |
||
67 |
lemma order_refl [simp, intro]: |
|
13006 | 68 |
"order r \<Longrightarrow> x <=_r x"; |
10496 | 69 |
by (simp add: order_def) |
70 |
||
71 |
lemma order_antisym: |
|
13006 | 72 |
"\<lbrakk> order r; x <=_r y; y <=_r x \<rbrakk> \<Longrightarrow> x = y" |
10496 | 73 |
apply (unfold order_def) |
74 |
apply (simp (no_asm_simp)) |
|
75 |
done |
|
76 |
||
77 |
lemma order_trans: |
|
13006 | 78 |
"\<lbrakk> order r; x <=_r y; y <=_r z \<rbrakk> \<Longrightarrow> x <=_r z" |
10496 | 79 |
apply (unfold order_def) |
80 |
apply blast |
|
81 |
done |
|
82 |
||
83 |
lemma order_less_irrefl [intro, simp]: |
|
13006 | 84 |
"order r \<Longrightarrow> ~ x <_r x" |
10496 | 85 |
apply (unfold order_def lesssub_def) |
86 |
apply blast |
|
87 |
done |
|
88 |
||
89 |
lemma order_less_trans: |
|
13006 | 90 |
"\<lbrakk> order r; x <_r y; y <_r z \<rbrakk> \<Longrightarrow> x <_r z" |
10496 | 91 |
apply (unfold order_def lesssub_def) |
92 |
apply blast |
|
93 |
done |
|
94 |
||
95 |
lemma topD [simp, intro]: |
|
13006 | 96 |
"top r T \<Longrightarrow> x <=_r T" |
10496 | 97 |
by (simp add: top_def) |
98 |
||
99 |
lemma top_le_conv [simp]: |
|
13006 | 100 |
"\<lbrakk> order r; top r T \<rbrakk> \<Longrightarrow> (T <=_r x) = (x = T)" |
10496 | 101 |
by (blast intro: order_antisym) |
102 |
||
103 |
lemma semilat_Def: |
|
104 |
"semilat(A,r,f) == order r & closed A f & |
|
105 |
(!x:A. !y:A. x <=_r x +_f y) & |
|
106 |
(!x:A. !y:A. y <=_r x +_f y) & |
|
13006 | 107 |
(!x:A. !y:A. !z:A. x <=_r z & y <=_r z \<longrightarrow> x +_f y <=_r z)" |
10918 | 108 |
apply (unfold semilat_def split_conv [THEN eq_reflection]) |
10496 | 109 |
apply (rule refl [THEN eq_reflection]) |
110 |
done |
|
111 |
||
112 |
lemma semilatDorderI [simp, intro]: |
|
13006 | 113 |
"semilat(A,r,f) \<Longrightarrow> order r" |
10496 | 114 |
by (simp add: semilat_Def) |
115 |
||
116 |
lemma semilatDclosedI [simp, intro]: |
|
13006 | 117 |
"semilat(A,r,f) \<Longrightarrow> closed A f" |
10496 | 118 |
apply (unfold semilat_Def) |
119 |
apply simp |
|
120 |
done |
|
121 |
||
122 |
lemma semilat_ub1 [simp]: |
|
13006 | 123 |
"\<lbrakk> semilat(A,r,f); x:A; y:A \<rbrakk> \<Longrightarrow> x <=_r x +_f y" |
10496 | 124 |
by (unfold semilat_Def, simp) |
125 |
||
126 |
lemma semilat_ub2 [simp]: |
|
13006 | 127 |
"\<lbrakk> semilat(A,r,f); x:A; y:A \<rbrakk> \<Longrightarrow> y <=_r x +_f y" |
10496 | 128 |
by (unfold semilat_Def, simp) |
129 |
||
130 |
lemma semilat_lub [simp]: |
|
13006 | 131 |
"\<lbrakk> x <=_r z; y <=_r z; semilat(A,r,f); x:A; y:A; z:A \<rbrakk> \<Longrightarrow> x +_f y <=_r z"; |
10496 | 132 |
by (unfold semilat_Def, simp) |
133 |
||
134 |
||
135 |
lemma plus_le_conv [simp]: |
|
13006 | 136 |
"\<lbrakk> x:A; y:A; z:A; semilat(A,r,f) \<rbrakk> |
137 |
\<Longrightarrow> (x +_f y <=_r z) = (x <=_r z & y <=_r z)" |
|
10496 | 138 |
apply (unfold semilat_Def) |
139 |
apply (blast intro: semilat_ub1 semilat_ub2 semilat_lub order_trans) |
|
140 |
done |
|
141 |
||
142 |
lemma le_iff_plus_unchanged: |
|
13006 | 143 |
"\<lbrakk> x:A; y:A; semilat(A,r,f) \<rbrakk> \<Longrightarrow> (x <=_r y) = (x +_f y = y)" |
10496 | 144 |
apply (rule iffI) |
145 |
apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub2, assumption+) |
|
146 |
apply (erule subst) |
|
147 |
apply simp |
|
148 |
done |
|
149 |
||
150 |
lemma le_iff_plus_unchanged2: |
|
13006 | 151 |
"\<lbrakk> x:A; y:A; semilat(A,r,f) \<rbrakk> \<Longrightarrow> (x <=_r y) = (y +_f x = y)" |
10496 | 152 |
apply (rule iffI) |
153 |
apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub1, assumption+) |
|
154 |
apply (erule subst) |
|
155 |
apply simp |
|
156 |
done |
|
157 |
||
158 |
||
159 |
lemma closedD: |
|
13006 | 160 |
"\<lbrakk> closed A f; x:A; y:A \<rbrakk> \<Longrightarrow> x +_f y : A" |
10496 | 161 |
apply (unfold closed_def) |
162 |
apply blast |
|
163 |
done |
|
164 |
||
165 |
lemma closed_UNIV [simp]: "closed UNIV f" |
|
166 |
by (simp add: closed_def) |
|
167 |
||
168 |
||
169 |
lemma is_lubD: |
|
13006 | 170 |
"is_lub r x y u \<Longrightarrow> is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)" |
10496 | 171 |
by (simp add: is_lub_def) |
172 |
||
173 |
lemma is_ubI: |
|
13006 | 174 |
"\<lbrakk> (x,u) : r; (y,u) : r \<rbrakk> \<Longrightarrow> is_ub r x y u" |
10496 | 175 |
by (simp add: is_ub_def) |
176 |
||
177 |
lemma is_ubD: |
|
13006 | 178 |
"is_ub r x y u \<Longrightarrow> (x,u) : r & (y,u) : r" |
10496 | 179 |
by (simp add: is_ub_def) |
180 |
||
181 |
||
182 |
lemma is_lub_bigger1 [iff]: |
|
183 |
"is_lub (r^* ) x y y = ((x,y):r^* )" |
|
184 |
apply (unfold is_lub_def is_ub_def) |
|
185 |
apply blast |
|
186 |
done |
|
187 |
||
188 |
lemma is_lub_bigger2 [iff]: |
|
189 |
"is_lub (r^* ) x y x = ((y,x):r^* )" |
|
190 |
apply (unfold is_lub_def is_ub_def) |
|
191 |
apply blast |
|
12542 | 192 |
done |
10496 | 193 |
|
194 |
lemma extend_lub: |
|
13006 | 195 |
"\<lbrakk> single_valued r; is_lub (r^* ) x y u; (x',x) : r \<rbrakk> |
196 |
\<Longrightarrow> EX v. is_lub (r^* ) x' y v" |
|
10496 | 197 |
apply (unfold is_lub_def is_ub_def) |
198 |
apply (case_tac "(y,x) : r^*") |
|
199 |
apply (case_tac "(y,x') : r^*") |
|
200 |
apply blast |
|
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
11085
diff
changeset
|
201 |
apply (blast elim: converse_rtranclE dest: single_valuedD) |
10496 | 202 |
apply (rule exI) |
203 |
apply (rule conjI) |
|
12566
fe20540bcf93
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
nipkow
parents:
12542
diff
changeset
|
204 |
apply (blast intro: converse_rtrancl_into_rtrancl dest: single_valuedD) |
fe20540bcf93
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
nipkow
parents:
12542
diff
changeset
|
205 |
apply (blast intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl |
10797 | 206 |
elim: converse_rtranclE dest: single_valuedD) |
12542 | 207 |
done |
10496 | 208 |
|
10797 | 209 |
lemma single_valued_has_lubs [rule_format]: |
13006 | 210 |
"\<lbrakk> single_valued r; (x,u) : r^* \<rbrakk> \<Longrightarrow> (!y. (y,u) : r^* \<longrightarrow> |
10496 | 211 |
(EX z. is_lub (r^* ) x y z))" |
212 |
apply (erule converse_rtrancl_induct) |
|
213 |
apply clarify |
|
214 |
apply (erule converse_rtrancl_induct) |
|
215 |
apply blast |
|
12566
fe20540bcf93
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
nipkow
parents:
12542
diff
changeset
|
216 |
apply (blast intro: converse_rtrancl_into_rtrancl) |
10496 | 217 |
apply (blast intro: extend_lub) |
218 |
done |
|
219 |
||
220 |
lemma some_lub_conv: |
|
13006 | 221 |
"\<lbrakk> acyclic r; is_lub (r^* ) x y u \<rbrakk> \<Longrightarrow> some_lub (r^* ) x y = u" |
10496 | 222 |
apply (unfold some_lub_def is_lub_def) |
223 |
apply (rule someI2) |
|
224 |
apply assumption |
|
225 |
apply (blast intro: antisymD dest!: acyclic_impl_antisym_rtrancl) |
|
12542 | 226 |
done |
10496 | 227 |
|
228 |
lemma is_lub_some_lub: |
|
13006 | 229 |
"\<lbrakk> single_valued r; acyclic r; (x,u):r^*; (y,u):r^* \<rbrakk> |
230 |
\<Longrightarrow> is_lub (r^* ) x y (some_lub (r^* ) x y)"; |
|
10797 | 231 |
by (fastsimp dest: single_valued_has_lubs simp add: some_lub_conv) |
10496 | 232 |
|
12542 | 233 |
subsection{*An executable lub-finder*} |
234 |
||
235 |
constdefs |
|
236 |
exec_lub :: "('a * 'a) set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a binop" |
|
237 |
"exec_lub r f x y == while (\<lambda>z. (x,z) \<notin> r\<^sup>*) f y" |
|
238 |
||
239 |
||
240 |
lemma acyclic_single_valued_finite: |
|
241 |
"\<lbrakk>acyclic r; single_valued r; (x,y) \<in> r\<^sup>*\<rbrakk> |
|
242 |
\<Longrightarrow> finite (r \<inter> {a. (x, a) \<in> r\<^sup>*} \<times> {b. (b, y) \<in> r\<^sup>*})" |
|
243 |
apply(erule converse_rtrancl_induct) |
|
244 |
apply(rule_tac B = "{}" in finite_subset) |
|
245 |
apply(simp only:acyclic_def) |
|
246 |
apply(blast intro:rtrancl_into_trancl2 rtrancl_trancl_trancl) |
|
247 |
apply simp |
|
248 |
apply(rename_tac x x') |
|
249 |
apply(subgoal_tac "r \<inter> {a. (x,a) \<in> r\<^sup>*} \<times> {b. (b,y) \<in> r\<^sup>*} = |
|
250 |
insert (x,x') (r \<inter> {a. (x', a) \<in> r\<^sup>*} \<times> {b. (b, y) \<in> r\<^sup>*})") |
|
251 |
apply simp |
|
12566
fe20540bcf93
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
nipkow
parents:
12542
diff
changeset
|
252 |
apply(blast intro:converse_rtrancl_into_rtrancl |
12542 | 253 |
elim:converse_rtranclE dest:single_valuedD) |
254 |
done |
|
255 |
||
256 |
||
12773 | 257 |
lemma exec_lub_conv: |
258 |
"\<lbrakk> acyclic r; !x y. (x,y) \<in> r \<longrightarrow> f x = y; is_lub (r\<^sup>*) x y u \<rbrakk> \<Longrightarrow> |
|
259 |
exec_lub r f x y = u"; |
|
12542 | 260 |
apply(unfold exec_lub_def) |
261 |
apply(rule_tac P = "\<lambda>z. (y,z) \<in> r\<^sup>* \<and> (z,u) \<in> r\<^sup>*" and |
|
262 |
r = "(r \<inter> {(a,b). (y,a) \<in> r\<^sup>* \<and> (b,u) \<in> r\<^sup>*})^-1" in while_rule) |
|
263 |
apply(blast dest: is_lubD is_ubD) |
|
264 |
apply(erule conjE) |
|
265 |
apply(erule_tac z = u in converse_rtranclE) |
|
266 |
apply(blast dest: is_lubD is_ubD) |
|
267 |
apply(blast dest:rtrancl_into_rtrancl) |
|
268 |
apply(rename_tac s) |
|
269 |
apply(subgoal_tac "is_ub (r\<^sup>*) x y s") |
|
270 |
prefer 2; apply(simp add:is_ub_def) |
|
271 |
apply(subgoal_tac "(u, s) \<in> r\<^sup>*") |
|
272 |
prefer 2; apply(blast dest:is_lubD) |
|
273 |
apply(erule converse_rtranclE) |
|
274 |
apply blast |
|
275 |
apply(simp only:acyclic_def) |
|
276 |
apply(blast intro:rtrancl_into_trancl2 rtrancl_trancl_trancl) |
|
277 |
apply(rule finite_acyclic_wf) |
|
278 |
apply simp |
|
279 |
apply(erule acyclic_single_valued_finite) |
|
280 |
apply(blast intro:single_valuedI) |
|
281 |
apply(simp add:is_lub_def is_ub_def) |
|
282 |
apply simp |
|
283 |
apply(erule acyclic_subset) |
|
284 |
apply blast |
|
285 |
apply simp |
|
286 |
apply(erule conjE) |
|
287 |
apply(erule_tac z = u in converse_rtranclE) |
|
288 |
apply(blast dest: is_lubD is_ubD) |
|
289 |
apply(blast dest:rtrancl_into_rtrancl) |
|
290 |
done |
|
291 |
||
12773 | 292 |
lemma is_lub_exec_lub: |
293 |
"\<lbrakk> single_valued r; acyclic r; (x,u):r^*; (y,u):r^*; !x y. (x,y) \<in> r \<longrightarrow> f x = y \<rbrakk> |
|
294 |
\<Longrightarrow> is_lub (r^* ) x y (exec_lub r f x y)" |
|
295 |
by (fastsimp dest: single_valued_has_lubs simp add: exec_lub_conv) |
|
296 |
||
10496 | 297 |
end |