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