author | berghofe |
Fri, 01 Jul 2005 13:54:12 +0200 | |
changeset 16633 | 208ebc9311f2 |
parent 16417 | 9bc16273c2d4 |
child 22271 | 51a80e238b29 |
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 |
|
16417 | 14 |
theory Semilat imports While_Combinator begin |
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 |
||
13649 | 27 |
syntax (xsymbols) |
28 |
"@lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<le>\<^sub>_ _)" [50, 1000, 51] 50) |
|
29 |
||
10496 | 30 |
consts |
13006 | 31 |
"@plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /+'__ _)" [65, 1000, 66] 65) |
10496 | 32 |
defs |
33 |
plussub_def: "x +_f y == f x y" |
|
34 |
||
13649 | 35 |
syntax (xsymbols) |
36 |
"@plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /+\<^sub>_ _)" [65, 1000, 66] 65) |
|
37 |
||
38 |
syntax (xsymbols) |
|
39 |
"@plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65) |
|
40 |
||
10496 | 41 |
|
42 |
constdefs |
|
13006 | 43 |
ord :: "('a*'a)set \<Rightarrow> 'a ord" |
10496 | 44 |
"ord r == %x y. (x,y):r" |
45 |
||
13006 | 46 |
order :: "'a ord \<Rightarrow> bool" |
10496 | 47 |
"order r == (!x. x <=_r x) & |
13006 | 48 |
(!x y. x <=_r y & y <=_r x \<longrightarrow> x=y) & |
49 |
(!x y z. x <=_r y & y <=_r z \<longrightarrow> x <=_r z)" |
|
10496 | 50 |
|
13006 | 51 |
acc :: "'a ord \<Rightarrow> bool" |
10496 | 52 |
"acc r == wf{(y,x) . x <_r y}" |
53 |
||
13006 | 54 |
top :: "'a ord \<Rightarrow> 'a \<Rightarrow> bool" |
10496 | 55 |
"top r T == !x. x <=_r T" |
56 |
||
13006 | 57 |
closed :: "'a set \<Rightarrow> 'a binop \<Rightarrow> bool" |
10496 | 58 |
"closed A f == !x:A. !y:A. x +_f y : A" |
59 |
||
13006 | 60 |
semilat :: "'a sl \<Rightarrow> bool" |
10496 | 61 |
"semilat == %(A,r,f). order r & closed A f & |
62 |
(!x:A. !y:A. x <=_r x +_f y) & |
|
63 |
(!x:A. !y:A. y <=_r x +_f y) & |
|
13006 | 64 |
(!x:A. !y:A. !z:A. x <=_r z & y <=_r z \<longrightarrow> x +_f y <=_r z)" |
10496 | 65 |
|
13006 | 66 |
is_ub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
10496 | 67 |
"is_ub r x y u == (x,u):r & (y,u):r" |
68 |
||
13006 | 69 |
is_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
70 |
"is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)" |
|
10496 | 71 |
|
13006 | 72 |
some_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" |
13074 | 73 |
"some_lub r x y == SOME z. is_lub r x y z"; |
10496 | 74 |
|
13365 | 75 |
locale (open) semilat = |
13074 | 76 |
fixes A :: "'a set" |
77 |
and r :: "'a ord" |
|
78 |
and f :: "'a binop" |
|
79 |
assumes semilat: "semilat(A,r,f)" |
|
10496 | 80 |
|
81 |
lemma order_refl [simp, intro]: |
|
13006 | 82 |
"order r \<Longrightarrow> x <=_r x"; |
10496 | 83 |
by (simp add: order_def) |
84 |
||
85 |
lemma order_antisym: |
|
13006 | 86 |
"\<lbrakk> order r; x <=_r y; y <=_r x \<rbrakk> \<Longrightarrow> x = y" |
10496 | 87 |
apply (unfold order_def) |
13074 | 88 |
apply (simp (no_asm_simp)) |
10496 | 89 |
done |
90 |
||
91 |
lemma order_trans: |
|
13006 | 92 |
"\<lbrakk> order r; x <=_r y; y <=_r z \<rbrakk> \<Longrightarrow> x <=_r z" |
10496 | 93 |
apply (unfold order_def) |
94 |
apply blast |
|
95 |
done |
|
96 |
||
97 |
lemma order_less_irrefl [intro, simp]: |
|
13006 | 98 |
"order r \<Longrightarrow> ~ x <_r x" |
10496 | 99 |
apply (unfold order_def lesssub_def) |
100 |
apply blast |
|
101 |
done |
|
102 |
||
103 |
lemma order_less_trans: |
|
13006 | 104 |
"\<lbrakk> order r; x <_r y; y <_r z \<rbrakk> \<Longrightarrow> x <_r z" |
10496 | 105 |
apply (unfold order_def lesssub_def) |
106 |
apply blast |
|
107 |
done |
|
108 |
||
109 |
lemma topD [simp, intro]: |
|
13006 | 110 |
"top r T \<Longrightarrow> x <=_r T" |
10496 | 111 |
by (simp add: top_def) |
112 |
||
113 |
lemma top_le_conv [simp]: |
|
13006 | 114 |
"\<lbrakk> order r; top r T \<rbrakk> \<Longrightarrow> (T <=_r x) = (x = T)" |
10496 | 115 |
by (blast intro: order_antisym) |
116 |
||
117 |
lemma semilat_Def: |
|
118 |
"semilat(A,r,f) == order r & closed A f & |
|
119 |
(!x:A. !y:A. x <=_r x +_f y) & |
|
120 |
(!x:A. !y:A. y <=_r x +_f y) & |
|
13006 | 121 |
(!x:A. !y:A. !z:A. x <=_r z & y <=_r z \<longrightarrow> x +_f y <=_r z)" |
10918 | 122 |
apply (unfold semilat_def split_conv [THEN eq_reflection]) |
10496 | 123 |
apply (rule refl [THEN eq_reflection]) |
124 |
done |
|
125 |
||
13074 | 126 |
lemma (in semilat) orderI [simp, intro]: |
127 |
"order r" |
|
128 |
by (insert semilat) (simp add: semilat_Def) |
|
129 |
||
130 |
lemma (in semilat) closedI [simp, intro]: |
|
131 |
"closed A f" |
|
132 |
by (insert semilat) (simp add: semilat_Def) |
|
133 |
||
13077 | 134 |
lemma closedD: |
135 |
"\<lbrakk> closed A f; x:A; y:A \<rbrakk> \<Longrightarrow> x +_f y : A" |
|
136 |
by (unfold closed_def) blast |
|
137 |
||
138 |
lemma closed_UNIV [simp]: "closed UNIV f" |
|
139 |
by (simp add: closed_def) |
|
140 |
||
141 |
||
142 |
lemma (in semilat) closed_f [simp, intro]: |
|
143 |
"\<lbrakk>x:A; y:A\<rbrakk> \<Longrightarrow> x +_f y : A" |
|
144 |
by (simp add: closedD [OF closedI]) |
|
145 |
||
146 |
lemma (in semilat) refl_r [intro, simp]: |
|
147 |
"x <=_r x" |
|
148 |
by simp |
|
149 |
||
150 |
lemma (in semilat) antisym_r [intro?]: |
|
151 |
"\<lbrakk> x <=_r y; y <=_r x \<rbrakk> \<Longrightarrow> x = y" |
|
152 |
by (rule order_antisym) auto |
|
153 |
||
154 |
lemma (in semilat) trans_r [trans, intro?]: |
|
155 |
"\<lbrakk>x <=_r y; y <=_r z\<rbrakk> \<Longrightarrow> x <=_r z" |
|
156 |
by (auto intro: order_trans) |
|
157 |
||
158 |
||
159 |
lemma (in semilat) ub1 [simp, intro?]: |
|
13074 | 160 |
"\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> x <=_r x +_f y" |
161 |
by (insert semilat) (unfold semilat_Def, simp) |
|
162 |
||
13077 | 163 |
lemma (in semilat) ub2 [simp, intro?]: |
13074 | 164 |
"\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> y <=_r x +_f y" |
165 |
by (insert semilat) (unfold semilat_Def, simp) |
|
10496 | 166 |
|
13077 | 167 |
lemma (in semilat) lub [simp, intro?]: |
13074 | 168 |
"\<lbrakk> x <=_r z; y <=_r z; x:A; y:A; z:A \<rbrakk> \<Longrightarrow> x +_f y <=_r z"; |
169 |
by (insert semilat) (unfold semilat_Def, simp) |
|
170 |
||
171 |
||
172 |
lemma (in semilat) plus_le_conv [simp]: |
|
173 |
"\<lbrakk> x:A; y:A; z:A \<rbrakk> \<Longrightarrow> (x +_f y <=_r z) = (x <=_r z & y <=_r z)" |
|
13077 | 174 |
by (blast intro: ub1 ub2 lub order_trans) |
13074 | 175 |
|
176 |
lemma (in semilat) le_iff_plus_unchanged: |
|
177 |
"\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> (x <=_r y) = (x +_f y = y)" |
|
178 |
apply (rule iffI) |
|
13077 | 179 |
apply (blast intro: antisym_r refl_r lub ub2) |
13074 | 180 |
apply (erule subst) |
10496 | 181 |
apply simp |
182 |
done |
|
183 |
||
13074 | 184 |
lemma (in semilat) le_iff_plus_unchanged2: |
185 |
"\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> (x <=_r y) = (y +_f x = y)" |
|
10496 | 186 |
apply (rule iffI) |
13074 | 187 |
apply (blast intro: order_antisym lub order_refl ub1) |
10496 | 188 |
apply (erule subst) |
189 |
apply simp |
|
190 |
done |
|
191 |
||
192 |
||
13074 | 193 |
lemma (in semilat) plus_assoc [simp]: |
13068 | 194 |
assumes a: "a \<in> A" and b: "b \<in> A" and c: "c \<in> A" |
195 |
shows "a +_f (b +_f c) = a +_f b +_f c" |
|
196 |
proof - |
|
197 |
from a b have ab: "a +_f b \<in> A" .. |
|
198 |
from this c have abc: "(a +_f b) +_f c \<in> A" .. |
|
199 |
from b c have bc: "b +_f c \<in> A" .. |
|
200 |
from a this have abc': "a +_f (b +_f c) \<in> A" .. |
|
201 |
||
13077 | 202 |
show ?thesis |
203 |
proof |
|
13068 | 204 |
show "a +_f (b +_f c) <=_r (a +_f b) +_f c" |
13074 | 205 |
proof - |
13068 | 206 |
from a b have "a <=_r a +_f b" .. |
207 |
also from ab c have "\<dots> <=_r \<dots> +_f c" .. |
|
208 |
finally have "a<": "a <=_r (a +_f b) +_f c" . |
|
209 |
from a b have "b <=_r a +_f b" .. |
|
210 |
also from ab c have "\<dots> <=_r \<dots> +_f c" .. |
|
211 |
finally have "b<": "b <=_r (a +_f b) +_f c" . |
|
212 |
from ab c have "c<": "c <=_r (a +_f b) +_f c" .. |
|
213 |
from "b<" "c<" b c abc have "b +_f c <=_r (a +_f b) +_f c" .. |
|
214 |
from "a<" this a bc abc show ?thesis .. |
|
215 |
qed |
|
216 |
show "(a +_f b) +_f c <=_r a +_f (b +_f c)" |
|
217 |
proof - |
|
218 |
from b c have "b <=_r b +_f c" .. |
|
219 |
also from a bc have "\<dots> <=_r a +_f \<dots>" .. |
|
220 |
finally have "b<": "b <=_r a +_f (b +_f c)" . |
|
221 |
from b c have "c <=_r b +_f c" .. |
|
222 |
also from a bc have "\<dots> <=_r a +_f \<dots>" .. |
|
223 |
finally have "c<": "c <=_r a +_f (b +_f c)" . |
|
224 |
from a bc have "a<": "a <=_r a +_f (b +_f c)" .. |
|
225 |
from "a<" "b<" a b abc' have "a +_f b <=_r a +_f (b +_f c)" .. |
|
226 |
from this "c<" ab c abc' show ?thesis .. |
|
227 |
qed |
|
228 |
qed |
|
229 |
qed |
|
230 |
||
13074 | 231 |
lemma (in semilat) plus_com_lemma: |
232 |
"\<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a +_f b <=_r b +_f a" |
|
13068 | 233 |
proof - |
13074 | 234 |
assume a: "a \<in> A" and b: "b \<in> A" |
13077 | 235 |
from b a have "a <=_r b +_f a" .. |
236 |
moreover from b a have "b <=_r b +_f a" .. |
|
237 |
moreover note a b |
|
238 |
moreover from b a have "b +_f a \<in> A" .. |
|
239 |
ultimately show ?thesis .. |
|
13068 | 240 |
qed |
241 |
||
13074 | 242 |
lemma (in semilat) plus_commutative: |
243 |
"\<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a +_f b = b +_f a" |
|
244 |
by(blast intro: order_antisym plus_com_lemma) |
|
13068 | 245 |
|
10496 | 246 |
lemma is_lubD: |
13006 | 247 |
"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 | 248 |
by (simp add: is_lub_def) |
249 |
||
250 |
lemma is_ubI: |
|
13006 | 251 |
"\<lbrakk> (x,u) : r; (y,u) : r \<rbrakk> \<Longrightarrow> is_ub r x y u" |
10496 | 252 |
by (simp add: is_ub_def) |
253 |
||
254 |
lemma is_ubD: |
|
13006 | 255 |
"is_ub r x y u \<Longrightarrow> (x,u) : r & (y,u) : r" |
10496 | 256 |
by (simp add: is_ub_def) |
257 |
||
258 |
||
259 |
lemma is_lub_bigger1 [iff]: |
|
260 |
"is_lub (r^* ) x y y = ((x,y):r^* )" |
|
261 |
apply (unfold is_lub_def is_ub_def) |
|
262 |
apply blast |
|
263 |
done |
|
264 |
||
265 |
lemma is_lub_bigger2 [iff]: |
|
266 |
"is_lub (r^* ) x y x = ((y,x):r^* )" |
|
267 |
apply (unfold is_lub_def is_ub_def) |
|
268 |
apply blast |
|
12542 | 269 |
done |
10496 | 270 |
|
271 |
lemma extend_lub: |
|
13006 | 272 |
"\<lbrakk> single_valued r; is_lub (r^* ) x y u; (x',x) : r \<rbrakk> |
273 |
\<Longrightarrow> EX v. is_lub (r^* ) x' y v" |
|
10496 | 274 |
apply (unfold is_lub_def is_ub_def) |
275 |
apply (case_tac "(y,x) : r^*") |
|
276 |
apply (case_tac "(y,x') : r^*") |
|
277 |
apply blast |
|
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
11085
diff
changeset
|
278 |
apply (blast elim: converse_rtranclE dest: single_valuedD) |
10496 | 279 |
apply (rule exI) |
280 |
apply (rule conjI) |
|
12566
fe20540bcf93
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
nipkow
parents:
12542
diff
changeset
|
281 |
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
|
282 |
apply (blast intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl |
10797 | 283 |
elim: converse_rtranclE dest: single_valuedD) |
12542 | 284 |
done |
10496 | 285 |
|
10797 | 286 |
lemma single_valued_has_lubs [rule_format]: |
13006 | 287 |
"\<lbrakk> single_valued r; (x,u) : r^* \<rbrakk> \<Longrightarrow> (!y. (y,u) : r^* \<longrightarrow> |
10496 | 288 |
(EX z. is_lub (r^* ) x y z))" |
289 |
apply (erule converse_rtrancl_induct) |
|
290 |
apply clarify |
|
291 |
apply (erule converse_rtrancl_induct) |
|
292 |
apply blast |
|
12566
fe20540bcf93
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
nipkow
parents:
12542
diff
changeset
|
293 |
apply (blast intro: converse_rtrancl_into_rtrancl) |
10496 | 294 |
apply (blast intro: extend_lub) |
295 |
done |
|
296 |
||
297 |
lemma some_lub_conv: |
|
13006 | 298 |
"\<lbrakk> acyclic r; is_lub (r^* ) x y u \<rbrakk> \<Longrightarrow> some_lub (r^* ) x y = u" |
10496 | 299 |
apply (unfold some_lub_def is_lub_def) |
300 |
apply (rule someI2) |
|
301 |
apply assumption |
|
302 |
apply (blast intro: antisymD dest!: acyclic_impl_antisym_rtrancl) |
|
12542 | 303 |
done |
10496 | 304 |
|
305 |
lemma is_lub_some_lub: |
|
13006 | 306 |
"\<lbrakk> single_valued r; acyclic r; (x,u):r^*; (y,u):r^* \<rbrakk> |
307 |
\<Longrightarrow> is_lub (r^* ) x y (some_lub (r^* ) x y)"; |
|
10797 | 308 |
by (fastsimp dest: single_valued_has_lubs simp add: some_lub_conv) |
10496 | 309 |
|
12542 | 310 |
subsection{*An executable lub-finder*} |
311 |
||
312 |
constdefs |
|
313 |
exec_lub :: "('a * 'a) set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a binop" |
|
314 |
"exec_lub r f x y == while (\<lambda>z. (x,z) \<notin> r\<^sup>*) f y" |
|
315 |
||
316 |
||
317 |
lemma acyclic_single_valued_finite: |
|
318 |
"\<lbrakk>acyclic r; single_valued r; (x,y) \<in> r\<^sup>*\<rbrakk> |
|
319 |
\<Longrightarrow> finite (r \<inter> {a. (x, a) \<in> r\<^sup>*} \<times> {b. (b, y) \<in> r\<^sup>*})" |
|
320 |
apply(erule converse_rtrancl_induct) |
|
321 |
apply(rule_tac B = "{}" in finite_subset) |
|
322 |
apply(simp only:acyclic_def) |
|
323 |
apply(blast intro:rtrancl_into_trancl2 rtrancl_trancl_trancl) |
|
324 |
apply simp |
|
325 |
apply(rename_tac x x') |
|
326 |
apply(subgoal_tac "r \<inter> {a. (x,a) \<in> r\<^sup>*} \<times> {b. (b,y) \<in> r\<^sup>*} = |
|
327 |
insert (x,x') (r \<inter> {a. (x', a) \<in> r\<^sup>*} \<times> {b. (b, y) \<in> r\<^sup>*})") |
|
328 |
apply simp |
|
12566
fe20540bcf93
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
nipkow
parents:
12542
diff
changeset
|
329 |
apply(blast intro:converse_rtrancl_into_rtrancl |
12542 | 330 |
elim:converse_rtranclE dest:single_valuedD) |
331 |
done |
|
332 |
||
333 |
||
12773 | 334 |
lemma exec_lub_conv: |
335 |
"\<lbrakk> acyclic r; !x y. (x,y) \<in> r \<longrightarrow> f x = y; is_lub (r\<^sup>*) x y u \<rbrakk> \<Longrightarrow> |
|
336 |
exec_lub r f x y = u"; |
|
12542 | 337 |
apply(unfold exec_lub_def) |
338 |
apply(rule_tac P = "\<lambda>z. (y,z) \<in> r\<^sup>* \<and> (z,u) \<in> r\<^sup>*" and |
|
339 |
r = "(r \<inter> {(a,b). (y,a) \<in> r\<^sup>* \<and> (b,u) \<in> r\<^sup>*})^-1" in while_rule) |
|
340 |
apply(blast dest: is_lubD is_ubD) |
|
341 |
apply(erule conjE) |
|
342 |
apply(erule_tac z = u in converse_rtranclE) |
|
343 |
apply(blast dest: is_lubD is_ubD) |
|
344 |
apply(blast dest:rtrancl_into_rtrancl) |
|
345 |
apply(rename_tac s) |
|
346 |
apply(subgoal_tac "is_ub (r\<^sup>*) x y s") |
|
347 |
prefer 2; apply(simp add:is_ub_def) |
|
348 |
apply(subgoal_tac "(u, s) \<in> r\<^sup>*") |
|
349 |
prefer 2; apply(blast dest:is_lubD) |
|
350 |
apply(erule converse_rtranclE) |
|
351 |
apply blast |
|
352 |
apply(simp only:acyclic_def) |
|
353 |
apply(blast intro:rtrancl_into_trancl2 rtrancl_trancl_trancl) |
|
354 |
apply(rule finite_acyclic_wf) |
|
355 |
apply simp |
|
356 |
apply(erule acyclic_single_valued_finite) |
|
357 |
apply(blast intro:single_valuedI) |
|
358 |
apply(simp add:is_lub_def is_ub_def) |
|
359 |
apply simp |
|
360 |
apply(erule acyclic_subset) |
|
361 |
apply blast |
|
362 |
apply simp |
|
363 |
apply(erule conjE) |
|
364 |
apply(erule_tac z = u in converse_rtranclE) |
|
365 |
apply(blast dest: is_lubD is_ubD) |
|
366 |
apply(blast dest:rtrancl_into_rtrancl) |
|
367 |
done |
|
368 |
||
12773 | 369 |
lemma is_lub_exec_lub: |
370 |
"\<lbrakk> single_valued r; acyclic r; (x,u):r^*; (y,u):r^*; !x y. (x,y) \<in> r \<longrightarrow> f x = y \<rbrakk> |
|
371 |
\<Longrightarrow> is_lub (r^* ) x y (exec_lub r f x y)" |
|
372 |
by (fastsimp dest: single_valued_has_lubs simp add: exec_lub_conv) |
|
373 |
||
10496 | 374 |
end |