|
1 (* Title: HOLCF/Up1.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
|
6 Lifting. |
|
7 *) |
|
8 |
|
9 header {* The type of lifted values *} |
|
10 |
|
11 theory Up = Cfun + Sum_Type + Datatype: |
|
12 |
|
13 (* new type for lifting *) |
|
14 |
|
15 typedef (Up) ('a) "u" = "{x::(unit + 'a).True}" |
|
16 by auto |
|
17 |
|
18 instance u :: (sq_ord)sq_ord .. |
|
19 |
|
20 consts |
|
21 Iup :: "'a => ('a)u" |
|
22 Ifup :: "('a->'b)=>('a)u => 'b" |
|
23 |
|
24 defs |
|
25 Iup_def: "Iup x == Abs_Up(Inr(x))" |
|
26 Ifup_def: "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f$z" |
|
27 |
|
28 defs (overloaded) |
|
29 less_up_def: "(op <<) == (%x1 x2. case Rep_Up(x1) of |
|
30 Inl(y1) => True |
|
31 | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False |
|
32 | Inr(z2) => y2<<z2))" |
|
33 |
|
34 lemma Abs_Up_inverse2: "Rep_Up (Abs_Up y) = y" |
|
35 apply (simp (no_asm) add: Up_def Abs_Up_inverse) |
|
36 done |
|
37 |
|
38 lemma Exh_Up: "z = Abs_Up(Inl ()) | (? x. z = Iup x)" |
|
39 apply (unfold Iup_def) |
|
40 apply (rule Rep_Up_inverse [THEN subst]) |
|
41 apply (rule_tac s = "Rep_Up z" in sumE) |
|
42 apply (rule disjI1) |
|
43 apply (rule_tac f = "Abs_Up" in arg_cong) |
|
44 apply (rule unit_eq [THEN subst]) |
|
45 apply assumption |
|
46 apply (rule disjI2) |
|
47 apply (rule exI) |
|
48 apply (rule_tac f = "Abs_Up" in arg_cong) |
|
49 apply assumption |
|
50 done |
|
51 |
|
52 lemma inj_Abs_Up: "inj(Abs_Up)" |
|
53 apply (rule inj_on_inverseI) |
|
54 apply (rule Abs_Up_inverse2) |
|
55 done |
|
56 |
|
57 lemma inj_Rep_Up: "inj(Rep_Up)" |
|
58 apply (rule inj_on_inverseI) |
|
59 apply (rule Rep_Up_inverse) |
|
60 done |
|
61 |
|
62 lemma inject_Iup: "Iup x=Iup y ==> x=y" |
|
63 apply (unfold Iup_def) |
|
64 apply (rule inj_Inr [THEN injD]) |
|
65 apply (rule inj_Abs_Up [THEN injD]) |
|
66 apply assumption |
|
67 done |
|
68 |
|
69 declare inject_Iup [dest!] |
|
70 |
|
71 lemma defined_Iup: "Iup x~=Abs_Up(Inl ())" |
|
72 apply (unfold Iup_def) |
|
73 apply (rule notI) |
|
74 apply (rule notE) |
|
75 apply (rule Inl_not_Inr) |
|
76 apply (rule sym) |
|
77 apply (erule inj_Abs_Up [THEN injD]) |
|
78 done |
|
79 |
|
80 |
|
81 lemma upE: "[| p=Abs_Up(Inl ()) ==> Q; !!x. p=Iup(x)==>Q|] ==>Q" |
|
82 apply (rule Exh_Up [THEN disjE]) |
|
83 apply fast |
|
84 apply (erule exE) |
|
85 apply fast |
|
86 done |
|
87 |
|
88 lemma Ifup1: "Ifup(f)(Abs_Up(Inl ()))=UU" |
|
89 apply (unfold Ifup_def) |
|
90 apply (subst Abs_Up_inverse2) |
|
91 apply (subst sum_case_Inl) |
|
92 apply (rule refl) |
|
93 done |
|
94 |
|
95 lemma Ifup2: |
|
96 "Ifup(f)(Iup(x))=f$x" |
|
97 apply (unfold Ifup_def Iup_def) |
|
98 apply (subst Abs_Up_inverse2) |
|
99 apply (subst sum_case_Inr) |
|
100 apply (rule refl) |
|
101 done |
|
102 |
|
103 lemmas Up0_ss = Ifup1 Ifup2 |
|
104 |
|
105 declare Ifup1 [simp] Ifup2 [simp] |
|
106 |
|
107 lemma less_up1a: |
|
108 "Abs_Up(Inl ())<< z" |
|
109 apply (unfold less_up_def) |
|
110 apply (subst Abs_Up_inverse2) |
|
111 apply (subst sum_case_Inl) |
|
112 apply (rule TrueI) |
|
113 done |
|
114 |
|
115 lemma less_up1b: |
|
116 "~(Iup x) << (Abs_Up(Inl ()))" |
|
117 apply (unfold Iup_def less_up_def) |
|
118 apply (rule notI) |
|
119 apply (rule iffD1) |
|
120 prefer 2 apply (assumption) |
|
121 apply (subst Abs_Up_inverse2) |
|
122 apply (subst Abs_Up_inverse2) |
|
123 apply (subst sum_case_Inr) |
|
124 apply (subst sum_case_Inl) |
|
125 apply (rule refl) |
|
126 done |
|
127 |
|
128 lemma less_up1c: |
|
129 "(Iup x) << (Iup y)=(x<<y)" |
|
130 apply (unfold Iup_def less_up_def) |
|
131 apply (subst Abs_Up_inverse2) |
|
132 apply (subst Abs_Up_inverse2) |
|
133 apply (subst sum_case_Inr) |
|
134 apply (subst sum_case_Inr) |
|
135 apply (rule refl) |
|
136 done |
|
137 |
|
138 declare less_up1a [iff] less_up1b [iff] less_up1c [iff] |
|
139 |
|
140 lemma refl_less_up: "(p::'a u) << p" |
|
141 apply (rule_tac p = "p" in upE) |
|
142 apply auto |
|
143 done |
|
144 |
|
145 lemma antisym_less_up: "[|(p1::'a u) << p2;p2 << p1|] ==> p1=p2" |
|
146 apply (rule_tac p = "p1" in upE) |
|
147 apply simp |
|
148 apply (rule_tac p = "p2" in upE) |
|
149 apply (erule sym) |
|
150 apply simp |
|
151 apply (rule_tac p = "p2" in upE) |
|
152 apply simp |
|
153 apply simp |
|
154 apply (drule antisym_less, assumption) |
|
155 apply simp |
|
156 done |
|
157 |
|
158 lemma trans_less_up: "[|(p1::'a u) << p2;p2 << p3|] ==> p1 << p3" |
|
159 apply (rule_tac p = "p1" in upE) |
|
160 apply simp |
|
161 apply (rule_tac p = "p2" in upE) |
|
162 apply simp |
|
163 apply (rule_tac p = "p3" in upE) |
|
164 apply auto |
|
165 apply (blast intro: trans_less) |
|
166 done |
|
167 |
|
168 (* Class Instance u::(pcpo)po *) |
|
169 |
|
170 instance u :: (pcpo)po |
|
171 apply (intro_classes) |
|
172 apply (rule refl_less_up) |
|
173 apply (rule antisym_less_up, assumption+) |
|
174 apply (rule trans_less_up, assumption+) |
|
175 done |
|
176 |
|
177 (* for compatibility with old HOLCF-Version *) |
|
178 lemma inst_up_po: "(op <<)=(%x1 x2. case Rep_Up(x1) of |
|
179 Inl(y1) => True |
|
180 | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False |
|
181 | Inr(z2) => y2<<z2))" |
|
182 apply (fold less_up_def) |
|
183 apply (rule refl) |
|
184 done |
|
185 |
|
186 (* -------------------------------------------------------------------------*) |
|
187 (* type ('a)u is pointed *) |
|
188 (* ------------------------------------------------------------------------ *) |
|
189 |
|
190 lemma minimal_up: "Abs_Up(Inl ()) << z" |
|
191 apply (simp (no_asm) add: less_up1a) |
|
192 done |
|
193 |
|
194 lemmas UU_up_def = minimal_up [THEN minimal2UU, symmetric, standard] |
|
195 |
|
196 lemma least_up: "EX x::'a u. ALL y. x<<y" |
|
197 apply (rule_tac x = "Abs_Up (Inl ())" in exI) |
|
198 apply (rule minimal_up [THEN allI]) |
|
199 done |
|
200 |
|
201 (* -------------------------------------------------------------------------*) |
|
202 (* access to less_up in class po *) |
|
203 (* ------------------------------------------------------------------------ *) |
|
204 |
|
205 lemma less_up2b: "~ Iup(x) << Abs_Up(Inl ())" |
|
206 apply (simp (no_asm) add: less_up1b) |
|
207 done |
|
208 |
|
209 lemma less_up2c: "(Iup(x)<<Iup(y)) = (x<<y)" |
|
210 apply (simp (no_asm) add: less_up1c) |
|
211 done |
|
212 |
|
213 (* ------------------------------------------------------------------------ *) |
|
214 (* Iup and Ifup are monotone *) |
|
215 (* ------------------------------------------------------------------------ *) |
|
216 |
|
217 lemma monofun_Iup: "monofun(Iup)" |
|
218 |
|
219 apply (unfold monofun) |
|
220 apply (intro strip) |
|
221 apply (erule less_up2c [THEN iffD2]) |
|
222 done |
|
223 |
|
224 lemma monofun_Ifup1: "monofun(Ifup)" |
|
225 apply (unfold monofun) |
|
226 apply (intro strip) |
|
227 apply (rule less_fun [THEN iffD2]) |
|
228 apply (intro strip) |
|
229 apply (rule_tac p = "xa" in upE) |
|
230 apply simp |
|
231 apply simp |
|
232 apply (erule monofun_cfun_fun) |
|
233 done |
|
234 |
|
235 lemma monofun_Ifup2: "monofun(Ifup(f))" |
|
236 apply (unfold monofun) |
|
237 apply (intro strip) |
|
238 apply (rule_tac p = "x" in upE) |
|
239 apply simp |
|
240 apply simp |
|
241 apply (rule_tac p = "y" in upE) |
|
242 apply simp |
|
243 apply simp |
|
244 apply (erule monofun_cfun_arg) |
|
245 done |
|
246 |
|
247 (* ------------------------------------------------------------------------ *) |
|
248 (* Some kind of surjectivity lemma *) |
|
249 (* ------------------------------------------------------------------------ *) |
|
250 |
|
251 lemma up_lemma1: "z=Iup(x) ==> Iup(Ifup(LAM x. x)(z)) = z" |
|
252 apply simp |
|
253 done |
|
254 |
|
255 (* ------------------------------------------------------------------------ *) |
|
256 (* ('a)u is a cpo *) |
|
257 (* ------------------------------------------------------------------------ *) |
|
258 |
|
259 lemma lub_up1a: "[|chain(Y);EX i x. Y(i)=Iup(x)|] |
|
260 ==> range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x. x) (Y(i))))))" |
|
261 apply (rule is_lubI) |
|
262 apply (rule ub_rangeI) |
|
263 apply (rule_tac p = "Y (i) " in upE) |
|
264 apply (rule_tac s = "Abs_Up (Inl ())" and t = "Y (i) " in subst) |
|
265 apply (erule sym) |
|
266 apply (rule minimal_up) |
|
267 apply (rule_tac t = "Y (i) " in up_lemma1 [THEN subst]) |
|
268 apply assumption |
|
269 apply (rule less_up2c [THEN iffD2]) |
|
270 apply (rule is_ub_thelub) |
|
271 apply (erule monofun_Ifup2 [THEN ch2ch_monofun]) |
|
272 apply (rule_tac p = "u" in upE) |
|
273 apply (erule exE) |
|
274 apply (erule exE) |
|
275 apply (rule_tac P = "Y (i) <<Abs_Up (Inl ())" in notE) |
|
276 apply (rule_tac s = "Iup (x) " and t = "Y (i) " in ssubst) |
|
277 apply assumption |
|
278 apply (rule less_up2b) |
|
279 apply (erule subst) |
|
280 apply (erule ub_rangeD) |
|
281 apply (rule_tac t = "u" in up_lemma1 [THEN subst]) |
|
282 apply assumption |
|
283 apply (rule less_up2c [THEN iffD2]) |
|
284 apply (rule is_lub_thelub) |
|
285 apply (erule monofun_Ifup2 [THEN ch2ch_monofun]) |
|
286 apply (erule monofun_Ifup2 [THEN ub2ub_monofun]) |
|
287 done |
|
288 |
|
289 lemma lub_up1b: "[|chain(Y); ALL i x. Y(i)~=Iup(x)|] ==> range(Y) <<| Abs_Up (Inl ())" |
|
290 apply (rule is_lubI) |
|
291 apply (rule ub_rangeI) |
|
292 apply (rule_tac p = "Y (i) " in upE) |
|
293 apply (rule_tac s = "Abs_Up (Inl ())" and t = "Y (i) " in ssubst) |
|
294 apply assumption |
|
295 apply (rule refl_less) |
|
296 apply (rule notE) |
|
297 apply (drule spec) |
|
298 apply (drule spec) |
|
299 apply assumption |
|
300 apply assumption |
|
301 apply (rule minimal_up) |
|
302 done |
|
303 |
|
304 lemmas thelub_up1a = lub_up1a [THEN thelubI, standard] |
|
305 (* |
|
306 [| chain ?Y1; EX i x. ?Y1 i = Iup x |] ==> |
|
307 lub (range ?Y1) = Iup (lub (range (%i. Iup (LAM x. x) (?Y1 i)))) |
|
308 *) |
|
309 |
|
310 lemmas thelub_up1b = lub_up1b [THEN thelubI, standard] |
|
311 (* |
|
312 [| chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==> |
|
313 lub (range ?Y1) = UU_up |
|
314 *) |
|
315 |
|
316 lemma cpo_up: "chain(Y::nat=>('a)u) ==> EX x. range(Y) <<|x" |
|
317 apply (rule disjE) |
|
318 apply (rule_tac [2] exI) |
|
319 apply (erule_tac [2] lub_up1a) |
|
320 prefer 2 apply (assumption) |
|
321 apply (rule_tac [2] exI) |
|
322 apply (erule_tac [2] lub_up1b) |
|
323 prefer 2 apply (assumption) |
|
324 apply fast |
|
325 done |
|
326 |
|
327 (* Class instance of ('a)u for class pcpo *) |
|
328 |
|
329 instance u :: (pcpo)pcpo |
|
330 apply (intro_classes) |
|
331 apply (erule cpo_up) |
|
332 apply (rule least_up) |
|
333 done |
|
334 |
|
335 constdefs |
|
336 up :: "'a -> ('a)u" |
|
337 "up == (LAM x. Iup(x))" |
|
338 fup :: "('a->'c)-> ('a)u -> 'c" |
|
339 "fup == (LAM f p. Ifup(f)(p))" |
|
340 |
|
341 translations |
|
342 "case l of up$x => t1" == "fup$(LAM x. t1)$l" |
|
343 |
|
344 (* for compatibility with old HOLCF-Version *) |
|
345 lemma inst_up_pcpo: "UU = Abs_Up(Inl ())" |
|
346 apply (simp add: UU_def UU_up_def) |
|
347 done |
|
348 |
|
349 (* -------------------------------------------------------------------------*) |
|
350 (* some lemmas restated for class pcpo *) |
|
351 (* ------------------------------------------------------------------------ *) |
|
352 |
|
353 lemma less_up3b: "~ Iup(x) << UU" |
|
354 apply (subst inst_up_pcpo) |
|
355 apply (rule less_up2b) |
|
356 done |
|
357 |
|
358 lemma defined_Iup2: "Iup(x) ~= UU" |
|
359 apply (subst inst_up_pcpo) |
|
360 apply (rule defined_Iup) |
|
361 done |
|
362 declare defined_Iup2 [iff] |
|
363 |
|
364 (* ------------------------------------------------------------------------ *) |
|
365 (* continuity for Iup *) |
|
366 (* ------------------------------------------------------------------------ *) |
|
367 |
|
368 lemma contlub_Iup: "contlub(Iup)" |
|
369 apply (rule contlubI) |
|
370 apply (intro strip) |
|
371 apply (rule trans) |
|
372 apply (rule_tac [2] thelub_up1a [symmetric]) |
|
373 prefer 3 apply fast |
|
374 apply (erule_tac [2] monofun_Iup [THEN ch2ch_monofun]) |
|
375 apply (rule_tac f = "Iup" in arg_cong) |
|
376 apply (rule lub_equal) |
|
377 apply assumption |
|
378 apply (rule monofun_Ifup2 [THEN ch2ch_monofun]) |
|
379 apply (erule monofun_Iup [THEN ch2ch_monofun]) |
|
380 apply simp |
|
381 done |
|
382 |
|
383 lemma cont_Iup: "cont(Iup)" |
|
384 apply (rule monocontlub2cont) |
|
385 apply (rule monofun_Iup) |
|
386 apply (rule contlub_Iup) |
|
387 done |
|
388 declare cont_Iup [iff] |
|
389 |
|
390 (* ------------------------------------------------------------------------ *) |
|
391 (* continuity for Ifup *) |
|
392 (* ------------------------------------------------------------------------ *) |
|
393 |
|
394 lemma contlub_Ifup1: "contlub(Ifup)" |
|
395 apply (rule contlubI) |
|
396 apply (intro strip) |
|
397 apply (rule trans) |
|
398 apply (rule_tac [2] thelub_fun [symmetric]) |
|
399 apply (erule_tac [2] monofun_Ifup1 [THEN ch2ch_monofun]) |
|
400 apply (rule ext) |
|
401 apply (rule_tac p = "x" in upE) |
|
402 apply simp |
|
403 apply (rule lub_const [THEN thelubI, symmetric]) |
|
404 apply simp |
|
405 apply (erule contlub_cfun_fun) |
|
406 done |
|
407 |
|
408 |
|
409 lemma contlub_Ifup2: "contlub(Ifup(f))" |
|
410 apply (rule contlubI) |
|
411 apply (intro strip) |
|
412 apply (rule disjE) |
|
413 defer 1 |
|
414 apply (subst thelub_up1a) |
|
415 apply assumption |
|
416 apply assumption |
|
417 apply simp |
|
418 prefer 2 |
|
419 apply (subst thelub_up1b) |
|
420 apply assumption |
|
421 apply assumption |
|
422 apply simp |
|
423 apply (rule chain_UU_I_inverse [symmetric]) |
|
424 apply (rule allI) |
|
425 apply (rule_tac p = "Y(i)" in upE) |
|
426 apply simp |
|
427 apply simp |
|
428 apply (subst contlub_cfun_arg) |
|
429 apply (erule monofun_Ifup2 [THEN ch2ch_monofun]) |
|
430 apply (rule lub_equal2) |
|
431 apply (rule_tac [2] monofun_Rep_CFun2 [THEN ch2ch_monofun]) |
|
432 apply (erule_tac [2] monofun_Ifup2 [THEN ch2ch_monofun]) |
|
433 apply (erule_tac [2] monofun_Ifup2 [THEN ch2ch_monofun]) |
|
434 apply (rule chain_mono2 [THEN exE]) |
|
435 prefer 2 apply (assumption) |
|
436 apply (erule exE) |
|
437 apply (erule exE) |
|
438 apply (rule exI) |
|
439 apply (rule_tac s = "Iup (x) " and t = "Y (i) " in ssubst) |
|
440 apply assumption |
|
441 apply (rule defined_Iup2) |
|
442 apply (rule exI) |
|
443 apply (intro strip) |
|
444 apply (rule_tac p = "Y (i) " in upE) |
|
445 prefer 2 apply simp |
|
446 apply (rule_tac P = "Y (i) = UU" in notE) |
|
447 apply fast |
|
448 apply (subst inst_up_pcpo) |
|
449 apply assumption |
|
450 apply fast |
|
451 done |
|
452 |
|
453 lemma cont_Ifup1: "cont(Ifup)" |
|
454 apply (rule monocontlub2cont) |
|
455 apply (rule monofun_Ifup1) |
|
456 apply (rule contlub_Ifup1) |
|
457 done |
|
458 |
|
459 lemma cont_Ifup2: "cont(Ifup(f))" |
|
460 apply (rule monocontlub2cont) |
|
461 apply (rule monofun_Ifup2) |
|
462 apply (rule contlub_Ifup2) |
|
463 done |
|
464 |
|
465 |
|
466 (* ------------------------------------------------------------------------ *) |
|
467 (* continuous versions of lemmas for ('a)u *) |
|
468 (* ------------------------------------------------------------------------ *) |
|
469 |
|
470 lemma Exh_Up1: "z = UU | (EX x. z = up$x)" |
|
471 |
|
472 apply (unfold up_def) |
|
473 apply simp |
|
474 apply (subst inst_up_pcpo) |
|
475 apply (rule Exh_Up) |
|
476 done |
|
477 |
|
478 lemma inject_up: "up$x=up$y ==> x=y" |
|
479 apply (unfold up_def) |
|
480 apply (rule inject_Iup) |
|
481 apply auto |
|
482 done |
|
483 |
|
484 lemma defined_up: " up$x ~= UU" |
|
485 apply (unfold up_def) |
|
486 apply auto |
|
487 done |
|
488 |
|
489 lemma upE1: |
|
490 "[| p=UU ==> Q; !!x. p=up$x==>Q|] ==>Q" |
|
491 apply (unfold up_def) |
|
492 apply (rule upE) |
|
493 apply (simp only: inst_up_pcpo) |
|
494 apply fast |
|
495 apply simp |
|
496 done |
|
497 |
|
498 lemmas up_conts = cont_lemmas1 cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_CF1L |
|
499 |
|
500 lemma fup1: "fup$f$UU=UU" |
|
501 apply (unfold up_def fup_def) |
|
502 apply (subst inst_up_pcpo) |
|
503 apply (subst beta_cfun) |
|
504 apply (intro up_conts) |
|
505 apply (subst beta_cfun) |
|
506 apply (rule cont_Ifup2) |
|
507 apply simp |
|
508 done |
|
509 |
|
510 lemma fup2: "fup$f$(up$x)=f$x" |
|
511 apply (unfold up_def fup_def) |
|
512 apply (simplesubst beta_cfun) |
|
513 apply (rule cont_Iup) |
|
514 apply (subst beta_cfun) |
|
515 apply (intro up_conts) |
|
516 apply (subst beta_cfun) |
|
517 apply (rule cont_Ifup2) |
|
518 apply simp |
|
519 done |
|
520 |
|
521 lemma less_up4b: "~ up$x << UU" |
|
522 apply (unfold up_def fup_def) |
|
523 apply simp |
|
524 apply (rule less_up3b) |
|
525 done |
|
526 |
|
527 lemma less_up4c: |
|
528 "(up$x << up$y) = (x<<y)" |
|
529 apply (unfold up_def fup_def) |
|
530 apply simp |
|
531 done |
|
532 |
|
533 lemma thelub_up2a: |
|
534 "[| chain(Y); EX i x. Y(i) = up$x |] ==> |
|
535 lub(range(Y)) = up$(lub(range(%i. fup$(LAM x. x)$(Y i))))" |
|
536 apply (unfold up_def fup_def) |
|
537 apply (subst beta_cfun) |
|
538 apply (rule cont_Iup) |
|
539 apply (subst beta_cfun) |
|
540 apply (intro up_conts) |
|
541 apply (subst beta_cfun [THEN ext]) |
|
542 apply (rule cont_Ifup2) |
|
543 apply (rule thelub_up1a) |
|
544 apply assumption |
|
545 apply (erule exE) |
|
546 apply (erule exE) |
|
547 apply (rule exI) |
|
548 apply (rule exI) |
|
549 apply (erule box_equals) |
|
550 apply (rule refl) |
|
551 apply simp |
|
552 done |
|
553 |
|
554 |
|
555 |
|
556 lemma thelub_up2b: |
|
557 "[| chain(Y); ! i x. Y(i) ~= up$x |] ==> lub(range(Y)) = UU" |
|
558 apply (unfold up_def fup_def) |
|
559 apply (subst inst_up_pcpo) |
|
560 apply (rule thelub_up1b) |
|
561 apply assumption |
|
562 apply (intro strip) |
|
563 apply (drule spec) |
|
564 apply (drule spec) |
|
565 apply simp |
|
566 done |
|
567 |
|
568 |
|
569 lemma up_lemma2: "(EX x. z = up$x) = (z~=UU)" |
|
570 apply (rule iffI) |
|
571 apply (erule exE) |
|
572 apply simp |
|
573 apply (rule defined_up) |
|
574 apply (rule_tac p = "z" in upE1) |
|
575 apply (erule notE) |
|
576 apply assumption |
|
577 apply (erule exI) |
|
578 done |
|
579 |
|
580 |
|
581 lemma thelub_up2a_rev: "[| chain(Y); lub(range(Y)) = up$x |] ==> EX i x. Y(i) = up$x" |
|
582 apply (rule exE) |
|
583 apply (rule chain_UU_I_inverse2) |
|
584 apply (rule up_lemma2 [THEN iffD1]) |
|
585 apply (erule exI) |
|
586 apply (rule exI) |
|
587 apply (rule up_lemma2 [THEN iffD2]) |
|
588 apply assumption |
|
589 done |
|
590 |
|
591 lemma thelub_up2b_rev: "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x. Y(i) ~= up$x" |
|
592 apply (blast dest!: chain_UU_I [THEN spec] exI [THEN up_lemma2 [THEN iffD1]]) |
|
593 done |
|
594 |
|
595 |
|
596 lemma thelub_up3: "chain(Y) ==> lub(range(Y)) = UU | |
|
597 lub(range(Y)) = up$(lub(range(%i. fup$(LAM x. x)$(Y i))))" |
|
598 apply (rule disjE) |
|
599 apply (rule_tac [2] disjI1) |
|
600 apply (rule_tac [2] thelub_up2b) |
|
601 prefer 2 apply (assumption) |
|
602 prefer 2 apply (assumption) |
|
603 apply (rule_tac [2] disjI2) |
|
604 apply (rule_tac [2] thelub_up2a) |
|
605 prefer 2 apply (assumption) |
|
606 prefer 2 apply (assumption) |
|
607 apply fast |
|
608 done |
|
609 |
|
610 lemma fup3: "fup$up$x=x" |
|
611 apply (rule_tac p = "x" in upE1) |
|
612 apply (simp add: fup1 fup2) |
|
613 apply (simp add: fup1 fup2) |
|
614 done |
|
615 |
|
616 (* ------------------------------------------------------------------------ *) |
|
617 (* install simplifier for ('a)u *) |
|
618 (* ------------------------------------------------------------------------ *) |
|
619 |
|
620 declare fup1 [simp] fup2 [simp] defined_up [simp] |
|
621 |
|
622 end |
|
623 |
|
624 |
|
625 |