|
1 (* Title: HOLCF/Ssum0.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
|
6 Strict sum with typedef |
|
7 *) |
|
8 |
|
9 header {* The type of strict sums *} |
|
10 |
|
11 theory Ssum = Cfun: |
|
12 |
|
13 constdefs |
|
14 Sinl_Rep :: "['a,'a,'b,bool]=>bool" |
|
15 "Sinl_Rep == (%a.%x y p. (a~=UU --> x=a & p))" |
|
16 Sinr_Rep :: "['b,'a,'b,bool]=>bool" |
|
17 "Sinr_Rep == (%b.%x y p.(b~=UU --> y=b & ~p))" |
|
18 |
|
19 typedef (Ssum) ('a, 'b) "++" (infixr 10) = |
|
20 "{f.(? a. f=Sinl_Rep(a::'a))|(? b. f=Sinr_Rep(b::'b))}" |
|
21 by auto |
|
22 |
|
23 syntax (xsymbols) |
|
24 "++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20) |
|
25 syntax (HTML output) |
|
26 "++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20) |
|
27 |
|
28 consts |
|
29 Isinl :: "'a => ('a ++ 'b)" |
|
30 Isinr :: "'b => ('a ++ 'b)" |
|
31 Iwhen :: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c" |
|
32 |
|
33 defs (*defining the abstract constants*) |
|
34 Isinl_def: "Isinl(a) == Abs_Ssum(Sinl_Rep(a))" |
|
35 Isinr_def: "Isinr(b) == Abs_Ssum(Sinr_Rep(b))" |
|
36 |
|
37 Iwhen_def: "Iwhen(f)(g)(s) == @z. |
|
38 (s=Isinl(UU) --> z=UU) |
|
39 &(!a. a~=UU & s=Isinl(a) --> z=f$a) |
|
40 &(!b. b~=UU & s=Isinr(b) --> z=g$b)" |
|
41 |
|
42 (* ------------------------------------------------------------------------ *) |
|
43 (* A non-emptyness result for Sssum *) |
|
44 (* ------------------------------------------------------------------------ *) |
|
45 |
|
46 lemma SsumIl: "Sinl_Rep(a):Ssum" |
|
47 apply (unfold Ssum_def) |
|
48 apply blast |
|
49 done |
|
50 |
|
51 lemma SsumIr: "Sinr_Rep(a):Ssum" |
|
52 apply (unfold Ssum_def) |
|
53 apply blast |
|
54 done |
|
55 |
|
56 lemma inj_on_Abs_Ssum: "inj_on Abs_Ssum Ssum" |
|
57 apply (rule inj_on_inverseI) |
|
58 apply (erule Abs_Ssum_inverse) |
|
59 done |
|
60 |
|
61 (* ------------------------------------------------------------------------ *) |
|
62 (* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr *) |
|
63 (* ------------------------------------------------------------------------ *) |
|
64 |
|
65 lemma strict_SinlSinr_Rep: |
|
66 "Sinl_Rep(UU) = Sinr_Rep(UU)" |
|
67 apply (unfold Sinr_Rep_def Sinl_Rep_def) |
|
68 apply (rule ext) |
|
69 apply (rule ext) |
|
70 apply (rule ext) |
|
71 apply fast |
|
72 done |
|
73 |
|
74 lemma strict_IsinlIsinr: |
|
75 "Isinl(UU) = Isinr(UU)" |
|
76 apply (unfold Isinl_def Isinr_def) |
|
77 apply (rule strict_SinlSinr_Rep [THEN arg_cong]) |
|
78 done |
|
79 |
|
80 |
|
81 (* ------------------------------------------------------------------------ *) |
|
82 (* distinctness of Sinl_Rep, Sinr_Rep and Isinl, Isinr *) |
|
83 (* ------------------------------------------------------------------------ *) |
|
84 |
|
85 lemma noteq_SinlSinr_Rep: |
|
86 "(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU" |
|
87 apply (unfold Sinl_Rep_def Sinr_Rep_def) |
|
88 apply (blast dest!: fun_cong) |
|
89 done |
|
90 |
|
91 |
|
92 lemma noteq_IsinlIsinr: |
|
93 "Isinl(a)=Isinr(b) ==> a=UU & b=UU" |
|
94 apply (unfold Isinl_def Isinr_def) |
|
95 apply (rule noteq_SinlSinr_Rep) |
|
96 apply (erule inj_on_Abs_Ssum [THEN inj_onD]) |
|
97 apply (rule SsumIl) |
|
98 apply (rule SsumIr) |
|
99 done |
|
100 |
|
101 |
|
102 |
|
103 (* ------------------------------------------------------------------------ *) |
|
104 (* injectivity of Sinl_Rep, Sinr_Rep and Isinl, Isinr *) |
|
105 (* ------------------------------------------------------------------------ *) |
|
106 |
|
107 lemma inject_Sinl_Rep1: "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU" |
|
108 apply (unfold Sinl_Rep_def) |
|
109 apply (blast dest!: fun_cong) |
|
110 done |
|
111 |
|
112 lemma inject_Sinr_Rep1: "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU" |
|
113 apply (unfold Sinr_Rep_def) |
|
114 apply (blast dest!: fun_cong) |
|
115 done |
|
116 |
|
117 lemma inject_Sinl_Rep2: |
|
118 "[| a1~=UU ; a2~=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) |] ==> a1=a2" |
|
119 apply (unfold Sinl_Rep_def) |
|
120 apply (blast dest!: fun_cong) |
|
121 done |
|
122 |
|
123 lemma inject_Sinr_Rep2: |
|
124 "[|b1~=UU ; b2~=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) |] ==> b1=b2" |
|
125 apply (unfold Sinr_Rep_def) |
|
126 apply (blast dest!: fun_cong) |
|
127 done |
|
128 |
|
129 lemma inject_Sinl_Rep: "Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2" |
|
130 apply (case_tac "a1=UU") |
|
131 apply simp |
|
132 apply (rule inject_Sinl_Rep1 [symmetric]) |
|
133 apply (erule sym) |
|
134 apply (case_tac "a2=UU") |
|
135 apply simp |
|
136 apply (drule inject_Sinl_Rep1) |
|
137 apply simp |
|
138 apply (erule inject_Sinl_Rep2) |
|
139 apply assumption |
|
140 apply assumption |
|
141 done |
|
142 |
|
143 lemma inject_Sinr_Rep: "Sinr_Rep(b1)=Sinr_Rep(b2) ==> b1=b2" |
|
144 apply (case_tac "b1=UU") |
|
145 apply simp |
|
146 apply (rule inject_Sinr_Rep1 [symmetric]) |
|
147 apply (erule sym) |
|
148 apply (case_tac "b2=UU") |
|
149 apply simp |
|
150 apply (drule inject_Sinr_Rep1) |
|
151 apply simp |
|
152 apply (erule inject_Sinr_Rep2) |
|
153 apply assumption |
|
154 apply assumption |
|
155 done |
|
156 |
|
157 lemma inject_Isinl: "Isinl(a1)=Isinl(a2)==> a1=a2" |
|
158 apply (unfold Isinl_def) |
|
159 apply (rule inject_Sinl_Rep) |
|
160 apply (erule inj_on_Abs_Ssum [THEN inj_onD]) |
|
161 apply (rule SsumIl) |
|
162 apply (rule SsumIl) |
|
163 done |
|
164 |
|
165 lemma inject_Isinr: "Isinr(b1)=Isinr(b2) ==> b1=b2" |
|
166 apply (unfold Isinr_def) |
|
167 apply (rule inject_Sinr_Rep) |
|
168 apply (erule inj_on_Abs_Ssum [THEN inj_onD]) |
|
169 apply (rule SsumIr) |
|
170 apply (rule SsumIr) |
|
171 done |
|
172 |
|
173 declare inject_Isinl [dest!] inject_Isinr [dest!] |
|
174 |
|
175 lemma inject_Isinl_rev: "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)" |
|
176 apply blast |
|
177 done |
|
178 |
|
179 lemma inject_Isinr_rev: "b1~=b2 ==> Isinr(b1) ~= Isinr(b2)" |
|
180 apply blast |
|
181 done |
|
182 |
|
183 (* ------------------------------------------------------------------------ *) |
|
184 (* Exhaustion of the strict sum ++ *) |
|
185 (* choice of the bottom representation is arbitrary *) |
|
186 (* ------------------------------------------------------------------------ *) |
|
187 |
|
188 lemma Exh_Ssum: |
|
189 "z=Isinl(UU) | (? a. z=Isinl(a) & a~=UU) | (? b. z=Isinr(b) & b~=UU)" |
|
190 apply (unfold Isinl_def Isinr_def) |
|
191 apply (rule Rep_Ssum[unfolded Ssum_def, THEN CollectE]) |
|
192 apply (erule disjE) |
|
193 apply (erule exE) |
|
194 apply (case_tac "z= Abs_Ssum (Sinl_Rep (UU))") |
|
195 apply (erule disjI1) |
|
196 apply (rule disjI2) |
|
197 apply (rule disjI1) |
|
198 apply (rule exI) |
|
199 apply (rule conjI) |
|
200 apply (rule Rep_Ssum_inverse [symmetric, THEN trans]) |
|
201 apply (erule arg_cong) |
|
202 apply (rule_tac Q = "Sinl_Rep (a) =Sinl_Rep (UU) " in contrapos_nn) |
|
203 apply (erule_tac [2] arg_cong) |
|
204 apply (erule contrapos_nn) |
|
205 apply (rule Rep_Ssum_inverse [symmetric, THEN trans]) |
|
206 apply (rule trans) |
|
207 apply (erule arg_cong) |
|
208 apply (erule arg_cong) |
|
209 apply (erule exE) |
|
210 apply (case_tac "z= Abs_Ssum (Sinl_Rep (UU))") |
|
211 apply (erule disjI1) |
|
212 apply (rule disjI2) |
|
213 apply (rule disjI2) |
|
214 apply (rule exI) |
|
215 apply (rule conjI) |
|
216 apply (rule Rep_Ssum_inverse [symmetric, THEN trans]) |
|
217 apply (erule arg_cong) |
|
218 apply (rule_tac Q = "Sinr_Rep (b) =Sinl_Rep (UU) " in contrapos_nn) |
|
219 prefer 2 apply simp |
|
220 apply (rule strict_SinlSinr_Rep [symmetric]) |
|
221 apply (erule contrapos_nn) |
|
222 apply (rule Rep_Ssum_inverse [symmetric, THEN trans]) |
|
223 apply (rule trans) |
|
224 apply (erule arg_cong) |
|
225 apply (erule arg_cong) |
|
226 done |
|
227 |
|
228 (* ------------------------------------------------------------------------ *) |
|
229 (* elimination rules for the strict sum ++ *) |
|
230 (* ------------------------------------------------------------------------ *) |
|
231 |
|
232 lemma IssumE: |
|
233 "[|p=Isinl(UU) ==> Q ; |
|
234 !!x.[|p=Isinl(x); x~=UU |] ==> Q; |
|
235 !!y.[|p=Isinr(y); y~=UU |] ==> Q|] ==> Q" |
|
236 apply (rule Exh_Ssum [THEN disjE]) |
|
237 apply auto |
|
238 done |
|
239 |
|
240 lemma IssumE2: |
|
241 "[| !!x. [| p = Isinl(x) |] ==> Q; !!y. [| p = Isinr(y) |] ==> Q |] ==>Q" |
|
242 apply (rule IssumE) |
|
243 apply auto |
|
244 done |
|
245 |
|
246 |
|
247 |
|
248 |
|
249 (* ------------------------------------------------------------------------ *) |
|
250 (* rewrites for Iwhen *) |
|
251 (* ------------------------------------------------------------------------ *) |
|
252 |
|
253 lemma Iwhen1: |
|
254 "Iwhen f g (Isinl UU) = UU" |
|
255 apply (unfold Iwhen_def) |
|
256 apply (rule some_equality) |
|
257 apply (rule conjI) |
|
258 apply fast |
|
259 apply (rule conjI) |
|
260 apply (intro strip) |
|
261 apply (rule_tac P = "a=UU" in notE) |
|
262 apply fast |
|
263 apply (rule inject_Isinl) |
|
264 apply (rule sym) |
|
265 apply fast |
|
266 apply (intro strip) |
|
267 apply (rule_tac P = "b=UU" in notE) |
|
268 apply fast |
|
269 apply (rule inject_Isinr) |
|
270 apply (rule sym) |
|
271 apply (rule strict_IsinlIsinr [THEN subst]) |
|
272 apply fast |
|
273 apply fast |
|
274 done |
|
275 |
|
276 |
|
277 lemma Iwhen2: |
|
278 "x~=UU ==> Iwhen f g (Isinl x) = f$x" |
|
279 apply (unfold Iwhen_def) |
|
280 apply (rule some_equality) |
|
281 prefer 2 apply fast |
|
282 apply (rule conjI) |
|
283 apply (intro strip) |
|
284 apply (rule_tac P = "x=UU" in notE) |
|
285 apply assumption |
|
286 apply (rule inject_Isinl) |
|
287 apply assumption |
|
288 apply (rule conjI) |
|
289 apply (intro strip) |
|
290 apply (rule cfun_arg_cong) |
|
291 apply (rule inject_Isinl) |
|
292 apply fast |
|
293 apply (intro strip) |
|
294 apply (rule_tac P = "Isinl (x) = Isinr (b) " in notE) |
|
295 prefer 2 apply fast |
|
296 apply (rule contrapos_nn) |
|
297 apply (erule_tac [2] noteq_IsinlIsinr) |
|
298 apply fast |
|
299 done |
|
300 |
|
301 lemma Iwhen3: |
|
302 "y~=UU ==> Iwhen f g (Isinr y) = g$y" |
|
303 apply (unfold Iwhen_def) |
|
304 apply (rule some_equality) |
|
305 prefer 2 apply fast |
|
306 apply (rule conjI) |
|
307 apply (intro strip) |
|
308 apply (rule_tac P = "y=UU" in notE) |
|
309 apply assumption |
|
310 apply (rule inject_Isinr) |
|
311 apply (rule strict_IsinlIsinr [THEN subst]) |
|
312 apply assumption |
|
313 apply (rule conjI) |
|
314 apply (intro strip) |
|
315 apply (rule_tac P = "Isinr (y) = Isinl (a) " in notE) |
|
316 prefer 2 apply fast |
|
317 apply (rule contrapos_nn) |
|
318 apply (erule_tac [2] sym [THEN noteq_IsinlIsinr]) |
|
319 apply fast |
|
320 apply (intro strip) |
|
321 apply (rule cfun_arg_cong) |
|
322 apply (rule inject_Isinr) |
|
323 apply fast |
|
324 done |
|
325 |
|
326 (* ------------------------------------------------------------------------ *) |
|
327 (* instantiate the simplifier *) |
|
328 (* ------------------------------------------------------------------------ *) |
|
329 |
|
330 lemmas Ssum0_ss = strict_IsinlIsinr[symmetric] Iwhen1 Iwhen2 Iwhen3 |
|
331 |
|
332 declare Ssum0_ss [simp] |
|
333 |
|
334 (* Partial ordering for the strict sum ++ *) |
|
335 |
|
336 instance "++"::(pcpo,pcpo)sq_ord .. |
|
337 |
|
338 defs (overloaded) |
|
339 less_ssum_def: "(op <<) == (%s1 s2.@z. |
|
340 (! u x. s1=Isinl u & s2=Isinl x --> z = u << x) |
|
341 &(! v y. s1=Isinr v & s2=Isinr y --> z = v << y) |
|
342 &(! u y. s1=Isinl u & s2=Isinr y --> z = (u = UU)) |
|
343 &(! v x. s1=Isinr v & s2=Isinl x --> z = (v = UU)))" |
|
344 |
|
345 lemma less_ssum1a: |
|
346 "[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)" |
|
347 apply (unfold less_ssum_def) |
|
348 apply (rule some_equality) |
|
349 apply (drule_tac [2] conjunct1) |
|
350 apply (drule_tac [2] spec) |
|
351 apply (drule_tac [2] spec) |
|
352 apply (erule_tac [2] mp) |
|
353 prefer 2 apply fast |
|
354 apply (rule conjI) |
|
355 apply (intro strip) |
|
356 apply (erule conjE) |
|
357 apply simp |
|
358 apply (drule inject_Isinl) |
|
359 apply (drule inject_Isinl) |
|
360 apply simp |
|
361 apply (rule conjI) |
|
362 apply (intro strip) |
|
363 apply (erule conjE) |
|
364 apply simp |
|
365 apply (drule noteq_IsinlIsinr[OF sym]) |
|
366 apply simp |
|
367 apply (rule conjI) |
|
368 apply (intro strip) |
|
369 apply (erule conjE) |
|
370 apply simp |
|
371 apply (drule inject_Isinl) |
|
372 apply (drule noteq_IsinlIsinr[OF sym]) |
|
373 apply simp |
|
374 apply (rule eq_UU_iff[symmetric]) |
|
375 apply (intro strip) |
|
376 apply (erule conjE) |
|
377 apply simp |
|
378 apply (drule noteq_IsinlIsinr[OF sym]) |
|
379 apply simp |
|
380 done |
|
381 |
|
382 |
|
383 lemma less_ssum1b: |
|
384 "[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)" |
|
385 apply (unfold less_ssum_def) |
|
386 apply (rule some_equality) |
|
387 apply (drule_tac [2] conjunct2) |
|
388 apply (drule_tac [2] conjunct1) |
|
389 apply (drule_tac [2] spec) |
|
390 apply (drule_tac [2] spec) |
|
391 apply (erule_tac [2] mp) |
|
392 prefer 2 apply fast |
|
393 apply (rule conjI) |
|
394 apply (intro strip) |
|
395 apply (erule conjE) |
|
396 apply simp |
|
397 apply (drule noteq_IsinlIsinr) |
|
398 apply (drule noteq_IsinlIsinr) |
|
399 apply simp |
|
400 apply (rule conjI) |
|
401 apply (intro strip) |
|
402 apply (erule conjE) |
|
403 apply simp |
|
404 apply (drule inject_Isinr) |
|
405 apply (drule inject_Isinr) |
|
406 apply simp |
|
407 apply (rule conjI) |
|
408 apply (intro strip) |
|
409 apply (erule conjE) |
|
410 apply simp |
|
411 apply (drule noteq_IsinlIsinr) |
|
412 apply (drule inject_Isinr) |
|
413 apply simp |
|
414 apply (intro strip) |
|
415 apply (erule conjE) |
|
416 apply simp |
|
417 apply (drule inject_Isinr) |
|
418 apply (drule noteq_IsinlIsinr) |
|
419 apply simp |
|
420 apply (rule eq_UU_iff[symmetric]) |
|
421 done |
|
422 |
|
423 |
|
424 lemma less_ssum1c: |
|
425 "[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)" |
|
426 apply (unfold less_ssum_def) |
|
427 apply (rule some_equality) |
|
428 apply (rule conjI) |
|
429 apply (intro strip) |
|
430 apply (erule conjE) |
|
431 apply simp |
|
432 apply (drule inject_Isinl) |
|
433 apply (drule noteq_IsinlIsinr) |
|
434 apply simp |
|
435 apply (rule eq_UU_iff) |
|
436 apply (rule conjI) |
|
437 apply (intro strip) |
|
438 apply (erule conjE) |
|
439 apply simp |
|
440 apply (drule noteq_IsinlIsinr[OF sym]) |
|
441 apply (drule inject_Isinr) |
|
442 apply simp |
|
443 apply (rule conjI) |
|
444 apply (intro strip) |
|
445 apply (erule conjE) |
|
446 apply simp |
|
447 apply (drule inject_Isinl) |
|
448 apply (drule inject_Isinr) |
|
449 apply simp |
|
450 apply (intro strip) |
|
451 apply (erule conjE) |
|
452 apply simp |
|
453 apply (drule noteq_IsinlIsinr[OF sym]) |
|
454 apply (drule noteq_IsinlIsinr) |
|
455 apply simp |
|
456 apply (drule conjunct2) |
|
457 apply (drule conjunct2) |
|
458 apply (drule conjunct1) |
|
459 apply (drule spec) |
|
460 apply (drule spec) |
|
461 apply (erule mp) |
|
462 apply fast |
|
463 done |
|
464 |
|
465 |
|
466 lemma less_ssum1d: |
|
467 "[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)" |
|
468 apply (unfold less_ssum_def) |
|
469 apply (rule some_equality) |
|
470 apply (drule_tac [2] conjunct2) |
|
471 apply (drule_tac [2] conjunct2) |
|
472 apply (drule_tac [2] conjunct2) |
|
473 apply (drule_tac [2] spec) |
|
474 apply (drule_tac [2] spec) |
|
475 apply (erule_tac [2] mp) |
|
476 prefer 2 apply fast |
|
477 apply (rule conjI) |
|
478 apply (intro strip) |
|
479 apply (erule conjE) |
|
480 apply simp |
|
481 apply (drule noteq_IsinlIsinr) |
|
482 apply (drule inject_Isinl) |
|
483 apply simp |
|
484 apply (rule conjI) |
|
485 apply (intro strip) |
|
486 apply (erule conjE) |
|
487 apply simp |
|
488 apply (drule noteq_IsinlIsinr[OF sym]) |
|
489 apply (drule inject_Isinr) |
|
490 apply simp |
|
491 apply (rule eq_UU_iff) |
|
492 apply (rule conjI) |
|
493 apply (intro strip) |
|
494 apply (erule conjE) |
|
495 apply simp |
|
496 apply (drule noteq_IsinlIsinr) |
|
497 apply (drule noteq_IsinlIsinr[OF sym]) |
|
498 apply simp |
|
499 apply (intro strip) |
|
500 apply (erule conjE) |
|
501 apply simp |
|
502 apply (drule inject_Isinr) |
|
503 apply simp |
|
504 done |
|
505 |
|
506 |
|
507 (* ------------------------------------------------------------------------ *) |
|
508 (* optimize lemmas about less_ssum *) |
|
509 (* ------------------------------------------------------------------------ *) |
|
510 |
|
511 lemma less_ssum2a: "(Isinl x) << (Isinl y) = (x << y)" |
|
512 apply (rule less_ssum1a) |
|
513 apply (rule refl) |
|
514 apply (rule refl) |
|
515 done |
|
516 |
|
517 lemma less_ssum2b: "(Isinr x) << (Isinr y) = (x << y)" |
|
518 apply (rule less_ssum1b) |
|
519 apply (rule refl) |
|
520 apply (rule refl) |
|
521 done |
|
522 |
|
523 lemma less_ssum2c: "(Isinl x) << (Isinr y) = (x = UU)" |
|
524 apply (rule less_ssum1c) |
|
525 apply (rule refl) |
|
526 apply (rule refl) |
|
527 done |
|
528 |
|
529 lemma less_ssum2d: "(Isinr x) << (Isinl y) = (x = UU)" |
|
530 apply (rule less_ssum1d) |
|
531 apply (rule refl) |
|
532 apply (rule refl) |
|
533 done |
|
534 |
|
535 |
|
536 (* ------------------------------------------------------------------------ *) |
|
537 (* less_ssum is a partial order on ++ *) |
|
538 (* ------------------------------------------------------------------------ *) |
|
539 |
|
540 lemma refl_less_ssum: "(p::'a++'b) << p" |
|
541 apply (rule_tac p = "p" in IssumE2) |
|
542 apply (erule ssubst) |
|
543 apply (rule less_ssum2a [THEN iffD2]) |
|
544 apply (rule refl_less) |
|
545 apply (erule ssubst) |
|
546 apply (rule less_ssum2b [THEN iffD2]) |
|
547 apply (rule refl_less) |
|
548 done |
|
549 |
|
550 lemma antisym_less_ssum: "[|(p1::'a++'b) << p2; p2 << p1|] ==> p1=p2" |
|
551 apply (rule_tac p = "p1" in IssumE2) |
|
552 apply simp |
|
553 apply (rule_tac p = "p2" in IssumE2) |
|
554 apply simp |
|
555 apply (rule_tac f = "Isinl" in arg_cong) |
|
556 apply (rule antisym_less) |
|
557 apply (erule less_ssum2a [THEN iffD1]) |
|
558 apply (erule less_ssum2a [THEN iffD1]) |
|
559 apply simp |
|
560 apply (erule less_ssum2d [THEN iffD1, THEN ssubst]) |
|
561 apply (erule less_ssum2c [THEN iffD1, THEN ssubst]) |
|
562 apply (rule strict_IsinlIsinr) |
|
563 apply simp |
|
564 apply (rule_tac p = "p2" in IssumE2) |
|
565 apply simp |
|
566 apply (erule less_ssum2c [THEN iffD1, THEN ssubst]) |
|
567 apply (erule less_ssum2d [THEN iffD1, THEN ssubst]) |
|
568 apply (rule strict_IsinlIsinr [symmetric]) |
|
569 apply simp |
|
570 apply (rule_tac f = "Isinr" in arg_cong) |
|
571 apply (rule antisym_less) |
|
572 apply (erule less_ssum2b [THEN iffD1]) |
|
573 apply (erule less_ssum2b [THEN iffD1]) |
|
574 done |
|
575 |
|
576 lemma trans_less_ssum: "[|(p1::'a++'b) << p2; p2 << p3|] ==> p1 << p3" |
|
577 apply (rule_tac p = "p1" in IssumE2) |
|
578 apply simp |
|
579 apply (rule_tac p = "p3" in IssumE2) |
|
580 apply simp |
|
581 apply (rule less_ssum2a [THEN iffD2]) |
|
582 apply (rule_tac p = "p2" in IssumE2) |
|
583 apply simp |
|
584 apply (rule trans_less) |
|
585 apply (erule less_ssum2a [THEN iffD1]) |
|
586 apply (erule less_ssum2a [THEN iffD1]) |
|
587 apply simp |
|
588 apply (erule less_ssum2c [THEN iffD1, THEN ssubst]) |
|
589 apply (rule minimal) |
|
590 apply simp |
|
591 apply (rule less_ssum2c [THEN iffD2]) |
|
592 apply (rule_tac p = "p2" in IssumE2) |
|
593 apply simp |
|
594 apply (rule UU_I) |
|
595 apply (rule trans_less) |
|
596 apply (erule less_ssum2a [THEN iffD1]) |
|
597 apply (rule antisym_less_inverse [THEN conjunct1]) |
|
598 apply (erule less_ssum2c [THEN iffD1]) |
|
599 apply simp |
|
600 apply (erule less_ssum2c [THEN iffD1]) |
|
601 apply simp |
|
602 apply (rule_tac p = "p3" in IssumE2) |
|
603 apply simp |
|
604 apply (rule less_ssum2d [THEN iffD2]) |
|
605 apply (rule_tac p = "p2" in IssumE2) |
|
606 apply simp |
|
607 apply (erule less_ssum2d [THEN iffD1]) |
|
608 apply simp |
|
609 apply (rule UU_I) |
|
610 apply (rule trans_less) |
|
611 apply (erule less_ssum2b [THEN iffD1]) |
|
612 apply (rule antisym_less_inverse [THEN conjunct1]) |
|
613 apply (erule less_ssum2d [THEN iffD1]) |
|
614 apply simp |
|
615 apply (rule less_ssum2b [THEN iffD2]) |
|
616 apply (rule_tac p = "p2" in IssumE2) |
|
617 apply simp |
|
618 apply (erule less_ssum2d [THEN iffD1, THEN ssubst]) |
|
619 apply (rule minimal) |
|
620 apply simp |
|
621 apply (rule trans_less) |
|
622 apply (erule less_ssum2b [THEN iffD1]) |
|
623 apply (erule less_ssum2b [THEN iffD1]) |
|
624 done |
|
625 |
|
626 (* Class Instance ++::(pcpo,pcpo)po *) |
|
627 |
|
628 instance "++"::(pcpo,pcpo)po |
|
629 apply (intro_classes) |
|
630 apply (rule refl_less_ssum) |
|
631 apply (rule antisym_less_ssum, assumption+) |
|
632 apply (rule trans_less_ssum, assumption+) |
|
633 done |
|
634 |
|
635 (* for compatibility with old HOLCF-Version *) |
|
636 lemma inst_ssum_po: "(op <<)=(%s1 s2.@z. |
|
637 (! u x. s1=Isinl u & s2=Isinl x --> z = u << x) |
|
638 &(! v y. s1=Isinr v & s2=Isinr y --> z = v << y) |
|
639 &(! u y. s1=Isinl u & s2=Isinr y --> z = (u = UU)) |
|
640 &(! v x. s1=Isinr v & s2=Isinl x --> z = (v = UU)))" |
|
641 apply (fold less_ssum_def) |
|
642 apply (rule refl) |
|
643 done |
|
644 |
|
645 (* ------------------------------------------------------------------------ *) |
|
646 (* access to less_ssum in class po *) |
|
647 (* ------------------------------------------------------------------------ *) |
|
648 |
|
649 lemma less_ssum3a: "Isinl x << Isinl y = x << y" |
|
650 apply (simp (no_asm) add: less_ssum2a) |
|
651 done |
|
652 |
|
653 lemma less_ssum3b: "Isinr x << Isinr y = x << y" |
|
654 apply (simp (no_asm) add: less_ssum2b) |
|
655 done |
|
656 |
|
657 lemma less_ssum3c: "Isinl x << Isinr y = (x = UU)" |
|
658 apply (simp (no_asm) add: less_ssum2c) |
|
659 done |
|
660 |
|
661 lemma less_ssum3d: "Isinr x << Isinl y = (x = UU)" |
|
662 apply (simp (no_asm) add: less_ssum2d) |
|
663 done |
|
664 |
|
665 (* ------------------------------------------------------------------------ *) |
|
666 (* type ssum ++ is pointed *) |
|
667 (* ------------------------------------------------------------------------ *) |
|
668 |
|
669 lemma minimal_ssum: "Isinl UU << s" |
|
670 apply (rule_tac p = "s" in IssumE2) |
|
671 apply simp |
|
672 apply (rule less_ssum3a [THEN iffD2]) |
|
673 apply (rule minimal) |
|
674 apply simp |
|
675 apply (subst strict_IsinlIsinr) |
|
676 apply (rule less_ssum3b [THEN iffD2]) |
|
677 apply (rule minimal) |
|
678 done |
|
679 |
|
680 lemmas UU_ssum_def = minimal_ssum [THEN minimal2UU, symmetric, standard] |
|
681 |
|
682 lemma least_ssum: "? x::'a++'b.!y. x<<y" |
|
683 apply (rule_tac x = "Isinl UU" in exI) |
|
684 apply (rule minimal_ssum [THEN allI]) |
|
685 done |
|
686 |
|
687 (* ------------------------------------------------------------------------ *) |
|
688 (* Isinl, Isinr are monotone *) |
|
689 (* ------------------------------------------------------------------------ *) |
|
690 |
|
691 lemma monofun_Isinl: "monofun(Isinl)" |
|
692 apply (unfold monofun) |
|
693 apply (intro strip) |
|
694 apply (erule less_ssum3a [THEN iffD2]) |
|
695 done |
|
696 |
|
697 lemma monofun_Isinr: "monofun(Isinr)" |
|
698 apply (unfold monofun) |
|
699 apply (intro strip) |
|
700 apply (erule less_ssum3b [THEN iffD2]) |
|
701 done |
|
702 |
|
703 |
|
704 (* ------------------------------------------------------------------------ *) |
|
705 (* Iwhen is monotone in all arguments *) |
|
706 (* ------------------------------------------------------------------------ *) |
|
707 |
|
708 |
|
709 lemma monofun_Iwhen1: "monofun(Iwhen)" |
|
710 apply (unfold monofun) |
|
711 apply (intro strip) |
|
712 apply (rule less_fun [THEN iffD2]) |
|
713 apply (intro strip) |
|
714 apply (rule less_fun [THEN iffD2]) |
|
715 apply (intro strip) |
|
716 apply (rule_tac p = "xb" in IssumE) |
|
717 apply simp |
|
718 apply simp |
|
719 apply (erule monofun_cfun_fun) |
|
720 apply simp |
|
721 done |
|
722 |
|
723 lemma monofun_Iwhen2: "monofun(Iwhen(f))" |
|
724 apply (unfold monofun) |
|
725 apply (intro strip) |
|
726 apply (rule less_fun [THEN iffD2]) |
|
727 apply (intro strip) |
|
728 apply (rule_tac p = "xa" in IssumE) |
|
729 apply simp |
|
730 apply simp |
|
731 apply simp |
|
732 apply (erule monofun_cfun_fun) |
|
733 done |
|
734 |
|
735 lemma monofun_Iwhen3: "monofun(Iwhen(f)(g))" |
|
736 apply (unfold monofun) |
|
737 apply (intro strip) |
|
738 apply (rule_tac p = "x" in IssumE) |
|
739 apply simp |
|
740 apply (rule_tac p = "y" in IssumE) |
|
741 apply simp |
|
742 apply (rule_tac P = "xa=UU" in notE) |
|
743 apply assumption |
|
744 apply (rule UU_I) |
|
745 apply (rule less_ssum3a [THEN iffD1]) |
|
746 apply assumption |
|
747 apply simp |
|
748 apply (rule monofun_cfun_arg) |
|
749 apply (erule less_ssum3a [THEN iffD1]) |
|
750 apply (simp del: Iwhen2) |
|
751 apply (rule_tac s = "UU" and t = "xa" in subst) |
|
752 apply (erule less_ssum3c [THEN iffD1, symmetric]) |
|
753 apply simp |
|
754 apply (rule_tac p = "y" in IssumE) |
|
755 apply simp |
|
756 apply (simp only: less_ssum3d) |
|
757 apply (simp only: less_ssum3d) |
|
758 apply simp |
|
759 apply (rule monofun_cfun_arg) |
|
760 apply (erule less_ssum3b [THEN iffD1]) |
|
761 done |
|
762 |
|
763 |
|
764 (* ------------------------------------------------------------------------ *) |
|
765 (* some kind of exhaustion rules for chains in 'a ++ 'b *) |
|
766 (* ------------------------------------------------------------------------ *) |
|
767 |
|
768 lemma ssum_lemma1: "[|~(!i.? x. Y(i::nat)=Isinl(x))|] ==> (? i.! x. Y(i)~=Isinl(x))" |
|
769 apply fast |
|
770 done |
|
771 |
|
772 lemma ssum_lemma2: "[|(? i.!x.(Y::nat => 'a++'b)(i::nat)~=Isinl(x::'a))|] |
|
773 ==> (? i y. (Y::nat => 'a++'b)(i::nat)=Isinr(y::'b) & y~=UU)" |
|
774 apply (erule exE) |
|
775 apply (rule_tac p = "Y (i) " in IssumE) |
|
776 apply (drule spec) |
|
777 apply (erule notE, assumption) |
|
778 apply (drule spec) |
|
779 apply (erule notE, assumption) |
|
780 apply fast |
|
781 done |
|
782 |
|
783 |
|
784 lemma ssum_lemma3: "[|chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|] |
|
785 ==> (!i.? y. Y(i)=Isinr(y))" |
|
786 apply (erule exE) |
|
787 apply (erule exE) |
|
788 apply (rule allI) |
|
789 apply (rule_tac p = "Y (ia) " in IssumE) |
|
790 apply (rule exI) |
|
791 apply (rule trans) |
|
792 apply (rule_tac [2] strict_IsinlIsinr) |
|
793 apply assumption |
|
794 apply (erule_tac [2] exI) |
|
795 apply (erule conjE) |
|
796 apply (rule_tac m = "i" and n = "ia" in nat_less_cases) |
|
797 prefer 2 apply simp |
|
798 apply (rule exI, rule refl) |
|
799 apply (erule_tac P = "x=UU" in notE) |
|
800 apply (rule less_ssum3d [THEN iffD1]) |
|
801 apply (erule_tac s = "Y (i) " and t = "Isinr (x) ::'a++'b" in subst) |
|
802 apply (erule_tac s = "Y (ia) " and t = "Isinl (xa) ::'a++'b" in subst) |
|
803 apply (erule chain_mono) |
|
804 apply assumption |
|
805 apply (erule_tac P = "xa=UU" in notE) |
|
806 apply (rule less_ssum3c [THEN iffD1]) |
|
807 apply (erule_tac s = "Y (i) " and t = "Isinr (x) ::'a++'b" in subst) |
|
808 apply (erule_tac s = "Y (ia) " and t = "Isinl (xa) ::'a++'b" in subst) |
|
809 apply (erule chain_mono) |
|
810 apply assumption |
|
811 done |
|
812 |
|
813 lemma ssum_lemma4: "chain(Y) ==> (!i.? x. Y(i)=Isinl(x))|(!i.? y. Y(i)=Isinr(y))" |
|
814 apply (rule case_split_thm) |
|
815 apply (erule disjI1) |
|
816 apply (rule disjI2) |
|
817 apply (erule ssum_lemma3) |
|
818 apply (rule ssum_lemma2) |
|
819 apply (erule ssum_lemma1) |
|
820 done |
|
821 |
|
822 |
|
823 (* ------------------------------------------------------------------------ *) |
|
824 (* restricted surjectivity of Isinl *) |
|
825 (* ------------------------------------------------------------------------ *) |
|
826 |
|
827 lemma ssum_lemma5: "z=Isinl(x)==> Isinl((Iwhen (LAM x. x) (LAM y. UU))(z)) = z" |
|
828 apply simp |
|
829 apply (case_tac "x=UU") |
|
830 apply simp |
|
831 apply simp |
|
832 done |
|
833 |
|
834 (* ------------------------------------------------------------------------ *) |
|
835 (* restricted surjectivity of Isinr *) |
|
836 (* ------------------------------------------------------------------------ *) |
|
837 |
|
838 lemma ssum_lemma6: "z=Isinr(x)==> Isinr((Iwhen (LAM y. UU) (LAM x. x))(z)) = z" |
|
839 apply simp |
|
840 apply (case_tac "x=UU") |
|
841 apply simp |
|
842 apply simp |
|
843 done |
|
844 |
|
845 (* ------------------------------------------------------------------------ *) |
|
846 (* technical lemmas *) |
|
847 (* ------------------------------------------------------------------------ *) |
|
848 |
|
849 lemma ssum_lemma7: "[|Isinl(x) << z; x~=UU|] ==> ? y. z=Isinl(y) & y~=UU" |
|
850 apply (rule_tac p = "z" in IssumE) |
|
851 apply simp |
|
852 apply (erule notE) |
|
853 apply (rule antisym_less) |
|
854 apply (erule less_ssum3a [THEN iffD1]) |
|
855 apply (rule minimal) |
|
856 apply fast |
|
857 apply simp |
|
858 apply (rule notE) |
|
859 apply (erule_tac [2] less_ssum3c [THEN iffD1]) |
|
860 apply assumption |
|
861 done |
|
862 |
|
863 lemma ssum_lemma8: "[|Isinr(x) << z; x~=UU|] ==> ? y. z=Isinr(y) & y~=UU" |
|
864 apply (rule_tac p = "z" in IssumE) |
|
865 apply simp |
|
866 apply (erule notE) |
|
867 apply (erule less_ssum3d [THEN iffD1]) |
|
868 apply simp |
|
869 apply (rule notE) |
|
870 apply (erule_tac [2] less_ssum3d [THEN iffD1]) |
|
871 apply assumption |
|
872 apply fast |
|
873 done |
|
874 |
|
875 (* ------------------------------------------------------------------------ *) |
|
876 (* the type 'a ++ 'b is a cpo in three steps *) |
|
877 (* ------------------------------------------------------------------------ *) |
|
878 |
|
879 lemma lub_ssum1a: "[|chain(Y);(!i.? x. Y(i)=Isinl(x))|] ==> |
|
880 range(Y) <<| Isinl(lub(range(%i.(Iwhen (LAM x. x) (LAM y. UU))(Y i))))" |
|
881 apply (rule is_lubI) |
|
882 apply (rule ub_rangeI) |
|
883 apply (erule allE) |
|
884 apply (erule exE) |
|
885 apply (rule_tac t = "Y (i) " in ssum_lemma5 [THEN subst]) |
|
886 apply assumption |
|
887 apply (rule monofun_Isinl [THEN monofunE, THEN spec, THEN spec, THEN mp]) |
|
888 apply (rule is_ub_thelub) |
|
889 apply (erule monofun_Iwhen3 [THEN ch2ch_monofun]) |
|
890 apply (rule_tac p = "u" in IssumE2) |
|
891 apply (rule_tac t = "u" in ssum_lemma5 [THEN subst]) |
|
892 apply assumption |
|
893 apply (rule monofun_Isinl [THEN monofunE, THEN spec, THEN spec, THEN mp]) |
|
894 apply (rule is_lub_thelub) |
|
895 apply (erule monofun_Iwhen3 [THEN ch2ch_monofun]) |
|
896 apply (erule monofun_Iwhen3 [THEN ub2ub_monofun]) |
|
897 apply simp |
|
898 apply (rule less_ssum3c [THEN iffD2]) |
|
899 apply (rule chain_UU_I_inverse) |
|
900 apply (rule allI) |
|
901 apply (rule_tac p = "Y (i) " in IssumE) |
|
902 apply simp |
|
903 apply simp |
|
904 apply (erule notE) |
|
905 apply (rule less_ssum3c [THEN iffD1]) |
|
906 apply (rule_tac t = "Isinl (x) " in subst) |
|
907 apply assumption |
|
908 apply (erule ub_rangeD) |
|
909 apply simp |
|
910 done |
|
911 |
|
912 |
|
913 lemma lub_ssum1b: "[|chain(Y);(!i.? x. Y(i)=Isinr(x))|] ==> |
|
914 range(Y) <<| Isinr(lub(range(%i.(Iwhen (LAM y. UU) (LAM x. x))(Y i))))" |
|
915 apply (rule is_lubI) |
|
916 apply (rule ub_rangeI) |
|
917 apply (erule allE) |
|
918 apply (erule exE) |
|
919 apply (rule_tac t = "Y (i) " in ssum_lemma6 [THEN subst]) |
|
920 apply assumption |
|
921 apply (rule monofun_Isinr [THEN monofunE, THEN spec, THEN spec, THEN mp]) |
|
922 apply (rule is_ub_thelub) |
|
923 apply (erule monofun_Iwhen3 [THEN ch2ch_monofun]) |
|
924 apply (rule_tac p = "u" in IssumE2) |
|
925 apply simp |
|
926 apply (rule less_ssum3d [THEN iffD2]) |
|
927 apply (rule chain_UU_I_inverse) |
|
928 apply (rule allI) |
|
929 apply (rule_tac p = "Y (i) " in IssumE) |
|
930 apply simp |
|
931 apply simp |
|
932 apply (erule notE) |
|
933 apply (rule less_ssum3d [THEN iffD1]) |
|
934 apply (rule_tac t = "Isinr (y) " in subst) |
|
935 apply assumption |
|
936 apply (erule ub_rangeD) |
|
937 apply (rule_tac t = "u" in ssum_lemma6 [THEN subst]) |
|
938 apply assumption |
|
939 apply (rule monofun_Isinr [THEN monofunE, THEN spec, THEN spec, THEN mp]) |
|
940 apply (rule is_lub_thelub) |
|
941 apply (erule monofun_Iwhen3 [THEN ch2ch_monofun]) |
|
942 apply (erule monofun_Iwhen3 [THEN ub2ub_monofun]) |
|
943 done |
|
944 |
|
945 |
|
946 lemmas thelub_ssum1a = lub_ssum1a [THEN thelubI, standard] |
|
947 (* |
|
948 [| chain ?Y1; ! i. ? x. ?Y1 i = Isinl x |] ==> |
|
949 lub (range ?Y1) = Isinl |
|
950 (lub (range (%i. Iwhen (LAM x. x) (LAM y. UU) (?Y1 i)))) |
|
951 *) |
|
952 |
|
953 lemmas thelub_ssum1b = lub_ssum1b [THEN thelubI, standard] |
|
954 (* |
|
955 [| chain ?Y1; ! i. ? x. ?Y1 i = Isinr x |] ==> |
|
956 lub (range ?Y1) = Isinr |
|
957 (lub (range (%i. Iwhen (LAM y. UU) (LAM x. x) (?Y1 i)))) |
|
958 *) |
|
959 |
|
960 lemma cpo_ssum: "chain(Y::nat=>'a ++'b) ==> ? x. range(Y) <<|x" |
|
961 apply (rule ssum_lemma4 [THEN disjE]) |
|
962 apply assumption |
|
963 apply (rule exI) |
|
964 apply (erule lub_ssum1a) |
|
965 apply assumption |
|
966 apply (rule exI) |
|
967 apply (erule lub_ssum1b) |
|
968 apply assumption |
|
969 done |
|
970 |
|
971 (* Class instance of ++ for class pcpo *) |
|
972 |
|
973 instance "++" :: (pcpo,pcpo)pcpo |
|
974 apply (intro_classes) |
|
975 apply (erule cpo_ssum) |
|
976 apply (rule least_ssum) |
|
977 done |
|
978 |
|
979 consts |
|
980 sinl :: "'a -> ('a++'b)" |
|
981 sinr :: "'b -> ('a++'b)" |
|
982 sscase :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c" |
|
983 |
|
984 defs |
|
985 |
|
986 sinl_def: "sinl == (LAM x. Isinl(x))" |
|
987 sinr_def: "sinr == (LAM x. Isinr(x))" |
|
988 sscase_def: "sscase == (LAM f g s. Iwhen(f)(g)(s))" |
|
989 |
|
990 translations |
|
991 "case s of sinl$x => t1 | sinr$y => t2" == "sscase$(LAM x. t1)$(LAM y. t2)$s" |
|
992 |
|
993 (* for compatibility with old HOLCF-Version *) |
|
994 lemma inst_ssum_pcpo: "UU = Isinl UU" |
|
995 apply (simp add: UU_def UU_ssum_def) |
|
996 done |
|
997 |
|
998 declare inst_ssum_pcpo [symmetric, simp] |
|
999 |
|
1000 (* ------------------------------------------------------------------------ *) |
|
1001 (* continuity for Isinl and Isinr *) |
|
1002 (* ------------------------------------------------------------------------ *) |
|
1003 |
|
1004 lemma contlub_Isinl: "contlub(Isinl)" |
|
1005 apply (rule contlubI) |
|
1006 apply (intro strip) |
|
1007 apply (rule trans) |
|
1008 apply (rule_tac [2] thelub_ssum1a [symmetric]) |
|
1009 apply (rule_tac [3] allI) |
|
1010 apply (rule_tac [3] exI) |
|
1011 apply (rule_tac [3] refl) |
|
1012 apply (erule_tac [2] monofun_Isinl [THEN ch2ch_monofun]) |
|
1013 apply (case_tac "lub (range (Y))=UU") |
|
1014 apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst) |
|
1015 apply assumption |
|
1016 apply (rule_tac f = "Isinl" in arg_cong) |
|
1017 apply (rule chain_UU_I_inverse [symmetric]) |
|
1018 apply (rule allI) |
|
1019 apply (rule_tac s = "UU" and t = "Y (i) " in ssubst) |
|
1020 apply (erule chain_UU_I [THEN spec]) |
|
1021 apply assumption |
|
1022 apply (rule Iwhen1) |
|
1023 apply (rule_tac f = "Isinl" in arg_cong) |
|
1024 apply (rule lub_equal) |
|
1025 apply assumption |
|
1026 apply (rule monofun_Iwhen3 [THEN ch2ch_monofun]) |
|
1027 apply (erule monofun_Isinl [THEN ch2ch_monofun]) |
|
1028 apply (rule allI) |
|
1029 apply (case_tac "Y (k) =UU") |
|
1030 apply (erule ssubst) |
|
1031 apply (rule Iwhen1[symmetric]) |
|
1032 apply simp |
|
1033 done |
|
1034 |
|
1035 lemma contlub_Isinr: "contlub(Isinr)" |
|
1036 apply (rule contlubI) |
|
1037 apply (intro strip) |
|
1038 apply (rule trans) |
|
1039 apply (rule_tac [2] thelub_ssum1b [symmetric]) |
|
1040 apply (rule_tac [3] allI) |
|
1041 apply (rule_tac [3] exI) |
|
1042 apply (rule_tac [3] refl) |
|
1043 apply (erule_tac [2] monofun_Isinr [THEN ch2ch_monofun]) |
|
1044 apply (case_tac "lub (range (Y))=UU") |
|
1045 apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst) |
|
1046 apply assumption |
|
1047 apply (rule arg_cong, rule chain_UU_I_inverse [symmetric]) |
|
1048 apply (rule allI) |
|
1049 apply (rule_tac s = "UU" and t = "Y (i) " in ssubst) |
|
1050 apply (erule chain_UU_I [THEN spec]) |
|
1051 apply assumption |
|
1052 apply (rule strict_IsinlIsinr [THEN subst]) |
|
1053 apply (rule Iwhen1) |
|
1054 apply (rule arg_cong, rule lub_equal) |
|
1055 apply assumption |
|
1056 apply (rule monofun_Iwhen3 [THEN ch2ch_monofun]) |
|
1057 apply (erule monofun_Isinr [THEN ch2ch_monofun]) |
|
1058 apply (rule allI) |
|
1059 apply (case_tac "Y (k) =UU") |
|
1060 apply (simp only: Ssum0_ss) |
|
1061 apply simp |
|
1062 done |
|
1063 |
|
1064 lemma cont_Isinl: "cont(Isinl)" |
|
1065 apply (rule monocontlub2cont) |
|
1066 apply (rule monofun_Isinl) |
|
1067 apply (rule contlub_Isinl) |
|
1068 done |
|
1069 |
|
1070 lemma cont_Isinr: "cont(Isinr)" |
|
1071 apply (rule monocontlub2cont) |
|
1072 apply (rule monofun_Isinr) |
|
1073 apply (rule contlub_Isinr) |
|
1074 done |
|
1075 |
|
1076 declare cont_Isinl [iff] cont_Isinr [iff] |
|
1077 |
|
1078 |
|
1079 (* ------------------------------------------------------------------------ *) |
|
1080 (* continuity for Iwhen in the firts two arguments *) |
|
1081 (* ------------------------------------------------------------------------ *) |
|
1082 |
|
1083 lemma contlub_Iwhen1: "contlub(Iwhen)" |
|
1084 apply (rule contlubI) |
|
1085 apply (intro strip) |
|
1086 apply (rule trans) |
|
1087 apply (rule_tac [2] thelub_fun [symmetric]) |
|
1088 apply (erule_tac [2] monofun_Iwhen1 [THEN ch2ch_monofun]) |
|
1089 apply (rule expand_fun_eq [THEN iffD2]) |
|
1090 apply (intro strip) |
|
1091 apply (rule trans) |
|
1092 apply (rule_tac [2] thelub_fun [symmetric]) |
|
1093 apply (rule_tac [2] ch2ch_fun) |
|
1094 apply (erule_tac [2] monofun_Iwhen1 [THEN ch2ch_monofun]) |
|
1095 apply (rule expand_fun_eq [THEN iffD2]) |
|
1096 apply (intro strip) |
|
1097 apply (rule_tac p = "xa" in IssumE) |
|
1098 apply (simp only: Ssum0_ss) |
|
1099 apply (rule lub_const [THEN thelubI, symmetric]) |
|
1100 apply simp |
|
1101 apply (erule contlub_cfun_fun) |
|
1102 apply simp |
|
1103 apply (rule lub_const [THEN thelubI, symmetric]) |
|
1104 done |
|
1105 |
|
1106 lemma contlub_Iwhen2: "contlub(Iwhen(f))" |
|
1107 apply (rule contlubI) |
|
1108 apply (intro strip) |
|
1109 apply (rule trans) |
|
1110 apply (rule_tac [2] thelub_fun [symmetric]) |
|
1111 apply (erule_tac [2] monofun_Iwhen2 [THEN ch2ch_monofun]) |
|
1112 apply (rule expand_fun_eq [THEN iffD2]) |
|
1113 apply (intro strip) |
|
1114 apply (rule_tac p = "x" in IssumE) |
|
1115 apply (simp only: Ssum0_ss) |
|
1116 apply (rule lub_const [THEN thelubI, symmetric]) |
|
1117 apply simp |
|
1118 apply (rule lub_const [THEN thelubI, symmetric]) |
|
1119 apply simp |
|
1120 apply (erule contlub_cfun_fun) |
|
1121 done |
|
1122 |
|
1123 (* ------------------------------------------------------------------------ *) |
|
1124 (* continuity for Iwhen in its third argument *) |
|
1125 (* ------------------------------------------------------------------------ *) |
|
1126 |
|
1127 (* ------------------------------------------------------------------------ *) |
|
1128 (* first 5 ugly lemmas *) |
|
1129 (* ------------------------------------------------------------------------ *) |
|
1130 |
|
1131 lemma ssum_lemma9: "[| chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)" |
|
1132 apply (intro strip) |
|
1133 apply (rule_tac p = "Y (i) " in IssumE) |
|
1134 apply (erule exI) |
|
1135 apply (erule exI) |
|
1136 apply (rule_tac P = "y=UU" in notE) |
|
1137 apply assumption |
|
1138 apply (rule less_ssum3d [THEN iffD1]) |
|
1139 apply (erule subst) |
|
1140 apply (erule subst) |
|
1141 apply (erule is_ub_thelub) |
|
1142 done |
|
1143 |
|
1144 |
|
1145 lemma ssum_lemma10: "[| chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)" |
|
1146 apply (intro strip) |
|
1147 apply (rule_tac p = "Y (i) " in IssumE) |
|
1148 apply (rule exI) |
|
1149 apply (erule trans) |
|
1150 apply (rule strict_IsinlIsinr) |
|
1151 apply (erule_tac [2] exI) |
|
1152 apply (rule_tac P = "xa=UU" in notE) |
|
1153 apply assumption |
|
1154 apply (rule less_ssum3c [THEN iffD1]) |
|
1155 apply (erule subst) |
|
1156 apply (erule subst) |
|
1157 apply (erule is_ub_thelub) |
|
1158 done |
|
1159 |
|
1160 lemma ssum_lemma11: "[| chain(Y); lub(range(Y)) = Isinl(UU) |] ==> |
|
1161 Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))" |
|
1162 apply (simp only: Ssum0_ss) |
|
1163 apply (rule chain_UU_I_inverse [symmetric]) |
|
1164 apply (rule allI) |
|
1165 apply (rule_tac s = "Isinl (UU) " and t = "Y (i) " in subst) |
|
1166 apply (rule inst_ssum_pcpo [THEN subst]) |
|
1167 apply (rule chain_UU_I [THEN spec, symmetric]) |
|
1168 apply assumption |
|
1169 apply (erule inst_ssum_pcpo [THEN ssubst]) |
|
1170 apply (simp only: Ssum0_ss) |
|
1171 done |
|
1172 |
|
1173 lemma ssum_lemma12: "[| chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==> |
|
1174 Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))" |
|
1175 apply simp |
|
1176 apply (rule_tac t = "x" in subst) |
|
1177 apply (rule inject_Isinl) |
|
1178 apply (rule trans) |
|
1179 prefer 2 apply (assumption) |
|
1180 apply (rule thelub_ssum1a [symmetric]) |
|
1181 apply assumption |
|
1182 apply (erule ssum_lemma9) |
|
1183 apply assumption |
|
1184 apply (rule trans) |
|
1185 apply (rule contlub_cfun_arg) |
|
1186 apply (rule monofun_Iwhen3 [THEN ch2ch_monofun]) |
|
1187 apply assumption |
|
1188 apply (rule lub_equal2) |
|
1189 apply (rule chain_mono2 [THEN exE]) |
|
1190 prefer 2 apply (assumption) |
|
1191 apply (rule chain_UU_I_inverse2) |
|
1192 apply (subst inst_ssum_pcpo) |
|
1193 apply (erule contrapos_np) |
|
1194 apply (rule inject_Isinl) |
|
1195 apply (rule trans) |
|
1196 apply (erule sym) |
|
1197 apply (erule notnotD) |
|
1198 apply (rule exI) |
|
1199 apply (intro strip) |
|
1200 apply (rule ssum_lemma9 [THEN spec, THEN exE]) |
|
1201 apply assumption |
|
1202 apply assumption |
|
1203 apply (rule_tac t = "Y (i) " in ssubst) |
|
1204 apply assumption |
|
1205 apply (rule trans) |
|
1206 apply (rule cfun_arg_cong) |
|
1207 apply (rule Iwhen2) |
|
1208 apply force |
|
1209 apply (rule_tac t = "Y (i) " in ssubst) |
|
1210 apply assumption |
|
1211 apply auto |
|
1212 apply (subst Iwhen2) |
|
1213 apply force |
|
1214 apply (rule refl) |
|
1215 apply (rule monofun_Rep_CFun2 [THEN ch2ch_monofun]) |
|
1216 apply (erule monofun_Iwhen3 [THEN ch2ch_monofun]) |
|
1217 apply (erule monofun_Iwhen3 [THEN ch2ch_monofun]) |
|
1218 done |
|
1219 |
|
1220 |
|
1221 lemma ssum_lemma13: "[| chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==> |
|
1222 Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))" |
|
1223 apply simp |
|
1224 apply (rule_tac t = "x" in subst) |
|
1225 apply (rule inject_Isinr) |
|
1226 apply (rule trans) |
|
1227 prefer 2 apply (assumption) |
|
1228 apply (rule thelub_ssum1b [symmetric]) |
|
1229 apply assumption |
|
1230 apply (erule ssum_lemma10) |
|
1231 apply assumption |
|
1232 apply (rule trans) |
|
1233 apply (rule contlub_cfun_arg) |
|
1234 apply (rule monofun_Iwhen3 [THEN ch2ch_monofun]) |
|
1235 apply assumption |
|
1236 apply (rule lub_equal2) |
|
1237 apply (rule chain_mono2 [THEN exE]) |
|
1238 prefer 2 apply (assumption) |
|
1239 apply (rule chain_UU_I_inverse2) |
|
1240 apply (subst inst_ssum_pcpo) |
|
1241 apply (erule contrapos_np) |
|
1242 apply (rule inject_Isinr) |
|
1243 apply (rule trans) |
|
1244 apply (erule sym) |
|
1245 apply (rule strict_IsinlIsinr [THEN subst]) |
|
1246 apply (erule notnotD) |
|
1247 apply (rule exI) |
|
1248 apply (intro strip) |
|
1249 apply (rule ssum_lemma10 [THEN spec, THEN exE]) |
|
1250 apply assumption |
|
1251 apply assumption |
|
1252 apply (rule_tac t = "Y (i) " in ssubst) |
|
1253 apply assumption |
|
1254 apply (rule trans) |
|
1255 apply (rule cfun_arg_cong) |
|
1256 apply (rule Iwhen3) |
|
1257 apply force |
|
1258 apply (rule_tac t = "Y (i) " in ssubst) |
|
1259 apply assumption |
|
1260 apply (subst Iwhen3) |
|
1261 apply force |
|
1262 apply (rule_tac t = "Y (i) " in ssubst) |
|
1263 apply assumption |
|
1264 apply simp |
|
1265 apply (rule monofun_Rep_CFun2 [THEN ch2ch_monofun]) |
|
1266 apply (erule monofun_Iwhen3 [THEN ch2ch_monofun]) |
|
1267 apply (erule monofun_Iwhen3 [THEN ch2ch_monofun]) |
|
1268 done |
|
1269 |
|
1270 |
|
1271 lemma contlub_Iwhen3: "contlub(Iwhen(f)(g))" |
|
1272 apply (rule contlubI) |
|
1273 apply (intro strip) |
|
1274 apply (rule_tac p = "lub (range (Y))" in IssumE) |
|
1275 apply (erule ssum_lemma11) |
|
1276 apply assumption |
|
1277 apply (erule ssum_lemma12) |
|
1278 apply assumption |
|
1279 apply assumption |
|
1280 apply (erule ssum_lemma13) |
|
1281 apply assumption |
|
1282 apply assumption |
|
1283 done |
|
1284 |
|
1285 lemma cont_Iwhen1: "cont(Iwhen)" |
|
1286 apply (rule monocontlub2cont) |
|
1287 apply (rule monofun_Iwhen1) |
|
1288 apply (rule contlub_Iwhen1) |
|
1289 done |
|
1290 |
|
1291 lemma cont_Iwhen2: "cont(Iwhen(f))" |
|
1292 apply (rule monocontlub2cont) |
|
1293 apply (rule monofun_Iwhen2) |
|
1294 apply (rule contlub_Iwhen2) |
|
1295 done |
|
1296 |
|
1297 lemma cont_Iwhen3: "cont(Iwhen(f)(g))" |
|
1298 apply (rule monocontlub2cont) |
|
1299 apply (rule monofun_Iwhen3) |
|
1300 apply (rule contlub_Iwhen3) |
|
1301 done |
|
1302 |
|
1303 (* ------------------------------------------------------------------------ *) |
|
1304 (* continuous versions of lemmas for 'a ++ 'b *) |
|
1305 (* ------------------------------------------------------------------------ *) |
|
1306 |
|
1307 lemma strict_sinl [simp]: "sinl$UU =UU" |
|
1308 apply (unfold sinl_def) |
|
1309 apply (simp add: cont_Isinl) |
|
1310 done |
|
1311 |
|
1312 lemma strict_sinr [simp]: "sinr$UU=UU" |
|
1313 apply (unfold sinr_def) |
|
1314 apply (simp add: cont_Isinr) |
|
1315 done |
|
1316 |
|
1317 lemma noteq_sinlsinr: |
|
1318 "sinl$a=sinr$b ==> a=UU & b=UU" |
|
1319 apply (unfold sinl_def sinr_def) |
|
1320 apply (auto dest!: noteq_IsinlIsinr) |
|
1321 done |
|
1322 |
|
1323 lemma inject_sinl: |
|
1324 "sinl$a1=sinl$a2==> a1=a2" |
|
1325 apply (unfold sinl_def sinr_def) |
|
1326 apply auto |
|
1327 done |
|
1328 |
|
1329 lemma inject_sinr: |
|
1330 "sinr$a1=sinr$a2==> a1=a2" |
|
1331 apply (unfold sinl_def sinr_def) |
|
1332 apply auto |
|
1333 done |
|
1334 |
|
1335 declare inject_sinl [dest!] inject_sinr [dest!] |
|
1336 |
|
1337 lemma defined_sinl [simp]: "x~=UU ==> sinl$x ~= UU" |
|
1338 apply (erule contrapos_nn) |
|
1339 apply (rule inject_sinl) |
|
1340 apply auto |
|
1341 done |
|
1342 |
|
1343 lemma defined_sinr [simp]: "x~=UU ==> sinr$x ~= UU" |
|
1344 apply (erule contrapos_nn) |
|
1345 apply (rule inject_sinr) |
|
1346 apply auto |
|
1347 done |
|
1348 |
|
1349 lemma Exh_Ssum1: |
|
1350 "z=UU | (? a. z=sinl$a & a~=UU) | (? b. z=sinr$b & b~=UU)" |
|
1351 apply (unfold sinl_def sinr_def) |
|
1352 apply simp |
|
1353 apply (subst inst_ssum_pcpo) |
|
1354 apply (rule Exh_Ssum) |
|
1355 done |
|
1356 |
|
1357 |
|
1358 lemma ssumE: |
|
1359 assumes major: "p=UU ==> Q" |
|
1360 assumes prem2: "!!x.[|p=sinl$x; x~=UU |] ==> Q" |
|
1361 assumes prem3: "!!y.[|p=sinr$y; y~=UU |] ==> Q" |
|
1362 shows "Q" |
|
1363 apply (rule major [THEN IssumE]) |
|
1364 apply (subst inst_ssum_pcpo) |
|
1365 apply assumption |
|
1366 apply (rule prem2) |
|
1367 prefer 2 apply (assumption) |
|
1368 apply (simp add: sinl_def) |
|
1369 apply (rule prem3) |
|
1370 prefer 2 apply (assumption) |
|
1371 apply (simp add: sinr_def) |
|
1372 done |
|
1373 |
|
1374 |
|
1375 lemma ssumE2: |
|
1376 assumes preml: "!!x.[|p=sinl$x|] ==> Q" |
|
1377 assumes premr: "!!y.[|p=sinr$y|] ==> Q" |
|
1378 shows "Q" |
|
1379 apply (rule IssumE2) |
|
1380 apply (rule preml) |
|
1381 apply (rule_tac [2] premr) |
|
1382 apply (unfold sinl_def sinr_def) |
|
1383 apply auto |
|
1384 done |
|
1385 |
|
1386 lemmas ssum_conts = cont_lemmas1 cont_Iwhen1 cont_Iwhen2 |
|
1387 cont_Iwhen3 cont2cont_CF1L |
|
1388 |
|
1389 lemma sscase1 [simp]: |
|
1390 "sscase$f$g$UU = UU" |
|
1391 apply (unfold sscase_def sinl_def sinr_def) |
|
1392 apply (subst inst_ssum_pcpo) |
|
1393 apply (subst beta_cfun) |
|
1394 apply (intro ssum_conts) |
|
1395 apply (subst beta_cfun) |
|
1396 apply (intro ssum_conts) |
|
1397 apply (subst beta_cfun) |
|
1398 apply (intro ssum_conts) |
|
1399 apply (simp only: Ssum0_ss) |
|
1400 done |
|
1401 |
|
1402 lemma sscase2 [simp]: |
|
1403 "x~=UU==> sscase$f$g$(sinl$x) = f$x" |
|
1404 apply (unfold sscase_def sinl_def sinr_def) |
|
1405 apply (simplesubst beta_cfun) |
|
1406 apply (rule cont_Isinl) |
|
1407 apply (subst beta_cfun) |
|
1408 apply (intro ssum_conts) |
|
1409 apply (subst beta_cfun) |
|
1410 apply (intro ssum_conts) |
|
1411 apply (subst beta_cfun) |
|
1412 apply (intro ssum_conts) |
|
1413 apply simp |
|
1414 done |
|
1415 |
|
1416 lemma sscase3 [simp]: |
|
1417 "x~=UU==> sscase$f$g$(sinr$x) = g$x" |
|
1418 apply (unfold sscase_def sinl_def sinr_def) |
|
1419 apply (simplesubst beta_cfun) |
|
1420 apply (rule cont_Isinr) |
|
1421 apply (subst beta_cfun) |
|
1422 apply (intro ssum_conts) |
|
1423 apply (subst beta_cfun) |
|
1424 apply (intro ssum_conts) |
|
1425 apply (subst beta_cfun) |
|
1426 apply (intro ssum_conts) |
|
1427 apply simp |
|
1428 done |
|
1429 |
|
1430 lemma less_ssum4a: |
|
1431 "(sinl$x << sinl$y) = (x << y)" |
|
1432 apply (unfold sinl_def sinr_def) |
|
1433 apply (subst beta_cfun) |
|
1434 apply (rule cont_Isinl) |
|
1435 apply (subst beta_cfun) |
|
1436 apply (rule cont_Isinl) |
|
1437 apply (rule less_ssum3a) |
|
1438 done |
|
1439 |
|
1440 lemma less_ssum4b: |
|
1441 "(sinr$x << sinr$y) = (x << y)" |
|
1442 apply (unfold sinl_def sinr_def) |
|
1443 apply (subst beta_cfun) |
|
1444 apply (rule cont_Isinr) |
|
1445 apply (subst beta_cfun) |
|
1446 apply (rule cont_Isinr) |
|
1447 apply (rule less_ssum3b) |
|
1448 done |
|
1449 |
|
1450 lemma less_ssum4c: |
|
1451 "(sinl$x << sinr$y) = (x = UU)" |
|
1452 apply (unfold sinl_def sinr_def) |
|
1453 apply (simplesubst beta_cfun) |
|
1454 apply (rule cont_Isinr) |
|
1455 apply (subst beta_cfun) |
|
1456 apply (rule cont_Isinl) |
|
1457 apply (rule less_ssum3c) |
|
1458 done |
|
1459 |
|
1460 lemma less_ssum4d: |
|
1461 "(sinr$x << sinl$y) = (x = UU)" |
|
1462 apply (unfold sinl_def sinr_def) |
|
1463 apply (simplesubst beta_cfun) |
|
1464 apply (rule cont_Isinl) |
|
1465 apply (subst beta_cfun) |
|
1466 apply (rule cont_Isinr) |
|
1467 apply (rule less_ssum3d) |
|
1468 done |
|
1469 |
|
1470 lemma ssum_chainE: |
|
1471 "chain(Y) ==> (!i.? x.(Y i)=sinl$x)|(!i.? y.(Y i)=sinr$y)" |
|
1472 apply (unfold sinl_def sinr_def) |
|
1473 apply simp |
|
1474 apply (erule ssum_lemma4) |
|
1475 done |
|
1476 |
|
1477 lemma thelub_ssum2a: |
|
1478 "[| chain(Y); !i.? x. Y(i) = sinl$x |] ==> |
|
1479 lub(range(Y)) = sinl$(lub(range(%i. sscase$(LAM x. x)$(LAM y. UU)$(Y i))))" |
|
1480 apply (unfold sinl_def sinr_def sscase_def) |
|
1481 apply (subst beta_cfun) |
|
1482 apply (rule cont_Isinl) |
|
1483 apply (subst beta_cfun) |
|
1484 apply (intro ssum_conts) |
|
1485 apply (subst beta_cfun) |
|
1486 apply (intro ssum_conts) |
|
1487 apply (subst beta_cfun [THEN ext]) |
|
1488 apply (intro ssum_conts) |
|
1489 apply (rule thelub_ssum1a) |
|
1490 apply assumption |
|
1491 apply (rule allI) |
|
1492 apply (erule allE) |
|
1493 apply (erule exE) |
|
1494 apply (rule exI) |
|
1495 apply (erule box_equals) |
|
1496 apply (rule refl) |
|
1497 apply simp |
|
1498 done |
|
1499 |
|
1500 lemma thelub_ssum2b: |
|
1501 "[| chain(Y); !i.? x. Y(i) = sinr$x |] ==> |
|
1502 lub(range(Y)) = sinr$(lub(range(%i. sscase$(LAM y. UU)$(LAM x. x)$(Y i))))" |
|
1503 apply (unfold sinl_def sinr_def sscase_def) |
|
1504 apply (subst beta_cfun) |
|
1505 apply (rule cont_Isinr) |
|
1506 apply (subst beta_cfun) |
|
1507 apply (intro ssum_conts) |
|
1508 apply (subst beta_cfun) |
|
1509 apply (intro ssum_conts) |
|
1510 apply (subst beta_cfun [THEN ext]) |
|
1511 apply (intro ssum_conts) |
|
1512 apply (rule thelub_ssum1b) |
|
1513 apply assumption |
|
1514 apply (rule allI) |
|
1515 apply (erule allE) |
|
1516 apply (erule exE) |
|
1517 apply (rule exI) |
|
1518 apply (erule box_equals) |
|
1519 apply (rule refl) |
|
1520 apply simp |
|
1521 done |
|
1522 |
|
1523 lemma thelub_ssum2a_rev: |
|
1524 "[| chain(Y); lub(range(Y)) = sinl$x|] ==> !i.? x. Y(i)=sinl$x" |
|
1525 apply (unfold sinl_def sinr_def) |
|
1526 apply simp |
|
1527 apply (erule ssum_lemma9) |
|
1528 apply simp |
|
1529 done |
|
1530 |
|
1531 lemma thelub_ssum2b_rev: |
|
1532 "[| chain(Y); lub(range(Y)) = sinr$x|] ==> !i.? x. Y(i)=sinr$x" |
|
1533 apply (unfold sinl_def sinr_def) |
|
1534 apply simp |
|
1535 apply (erule ssum_lemma10) |
|
1536 apply simp |
|
1537 done |
|
1538 |
|
1539 lemma thelub_ssum3: "chain(Y) ==> |
|
1540 lub(range(Y)) = sinl$(lub(range(%i. sscase$(LAM x. x)$(LAM y. UU)$(Y i)))) |
|
1541 | lub(range(Y)) = sinr$(lub(range(%i. sscase$(LAM y. UU)$(LAM x. x)$(Y i))))" |
|
1542 apply (rule ssum_chainE [THEN disjE]) |
|
1543 apply assumption |
|
1544 apply (rule disjI1) |
|
1545 apply (erule thelub_ssum2a) |
|
1546 apply assumption |
|
1547 apply (rule disjI2) |
|
1548 apply (erule thelub_ssum2b) |
|
1549 apply assumption |
|
1550 done |
|
1551 |
|
1552 lemma sscase4: "sscase$sinl$sinr$z=z" |
|
1553 apply (rule_tac p = "z" in ssumE) |
|
1554 apply auto |
|
1555 done |
|
1556 |
|
1557 |
|
1558 (* ------------------------------------------------------------------------ *) |
|
1559 (* install simplifier for Ssum *) |
|
1560 (* ------------------------------------------------------------------------ *) |
|
1561 |
|
1562 lemmas Ssum_rews = strict_sinl strict_sinr defined_sinl defined_sinr |
|
1563 sscase1 sscase2 sscase3 |
|
1564 |
|
1565 end |