|
1 (* Title: HOLCF/Sprod0.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
|
6 Strict product with typedef. |
|
7 *) |
|
8 |
|
9 header {* The type of strict products *} |
|
10 |
|
11 theory Sprod = Cfun: |
|
12 |
|
13 constdefs |
|
14 Spair_Rep :: "['a,'b] => ['a,'b] => bool" |
|
15 "Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a & y=b ))" |
|
16 |
|
17 typedef (Sprod) ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep (a::'a) (b::'b)}" |
|
18 by auto |
|
19 |
|
20 syntax (xsymbols) |
|
21 "**" :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20) |
|
22 syntax (HTML output) |
|
23 "**" :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20) |
|
24 |
|
25 subsection {* @{term Ispair}, @{term Isfst}, and @{term Issnd} *} |
|
26 |
|
27 consts |
|
28 Ispair :: "['a,'b] => ('a ** 'b)" |
|
29 Isfst :: "('a ** 'b) => 'a" |
|
30 Issnd :: "('a ** 'b) => 'b" |
|
31 |
|
32 defs |
|
33 (*defining the abstract constants*) |
|
34 |
|
35 Ispair_def: "Ispair a b == Abs_Sprod(Spair_Rep a b)" |
|
36 |
|
37 Isfst_def: "Isfst(p) == @z. (p=Ispair UU UU --> z=UU) |
|
38 &(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=a)" |
|
39 |
|
40 Issnd_def: "Issnd(p) == @z. (p=Ispair UU UU --> z=UU) |
|
41 &(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=b)" |
|
42 |
|
43 (* ------------------------------------------------------------------------ *) |
|
44 (* A non-emptyness result for Sprod *) |
|
45 (* ------------------------------------------------------------------------ *) |
|
46 |
|
47 lemma SprodI: "(Spair_Rep a b):Sprod" |
|
48 apply (unfold Sprod_def) |
|
49 apply (rule CollectI, rule exI, rule exI, rule refl) |
|
50 done |
|
51 |
|
52 lemma inj_on_Abs_Sprod: "inj_on Abs_Sprod Sprod" |
|
53 apply (rule inj_on_inverseI) |
|
54 apply (erule Abs_Sprod_inverse) |
|
55 done |
|
56 |
|
57 (* ------------------------------------------------------------------------ *) |
|
58 (* Strictness and definedness of Spair_Rep *) |
|
59 (* ------------------------------------------------------------------------ *) |
|
60 |
|
61 lemma strict_Spair_Rep: |
|
62 "(a=UU | b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)" |
|
63 apply (unfold Spair_Rep_def) |
|
64 apply (rule ext) |
|
65 apply (rule ext) |
|
66 apply (rule iffI) |
|
67 apply fast |
|
68 apply fast |
|
69 done |
|
70 |
|
71 lemma defined_Spair_Rep_rev: |
|
72 "(Spair_Rep a b) = (Spair_Rep UU UU) ==> (a=UU | b=UU)" |
|
73 apply (unfold Spair_Rep_def) |
|
74 apply (case_tac "a=UU|b=UU") |
|
75 apply assumption |
|
76 apply (fast dest: fun_cong) |
|
77 done |
|
78 |
|
79 (* ------------------------------------------------------------------------ *) |
|
80 (* injectivity of Spair_Rep and Ispair *) |
|
81 (* ------------------------------------------------------------------------ *) |
|
82 |
|
83 lemma inject_Spair_Rep: |
|
84 "[|~aa=UU ; ~ba=UU ; Spair_Rep a b = Spair_Rep aa ba |] ==> a=aa & b=ba" |
|
85 |
|
86 apply (unfold Spair_Rep_def) |
|
87 apply (drule fun_cong) |
|
88 apply (drule fun_cong) |
|
89 apply (erule iffD1 [THEN mp]) |
|
90 apply auto |
|
91 done |
|
92 |
|
93 lemma inject_Ispair: |
|
94 "[|~aa=UU ; ~ba=UU ; Ispair a b = Ispair aa ba |] ==> a=aa & b=ba" |
|
95 apply (unfold Ispair_def) |
|
96 apply (erule inject_Spair_Rep) |
|
97 apply assumption |
|
98 apply (erule inj_on_Abs_Sprod [THEN inj_onD]) |
|
99 apply (rule SprodI) |
|
100 apply (rule SprodI) |
|
101 done |
|
102 |
|
103 (* ------------------------------------------------------------------------ *) |
|
104 (* strictness and definedness of Ispair *) |
|
105 (* ------------------------------------------------------------------------ *) |
|
106 |
|
107 lemma strict_Ispair: |
|
108 "(a=UU | b=UU) ==> Ispair a b = Ispair UU UU" |
|
109 apply (unfold Ispair_def) |
|
110 apply (erule strict_Spair_Rep [THEN arg_cong]) |
|
111 done |
|
112 |
|
113 lemma strict_Ispair1: |
|
114 "Ispair UU b = Ispair UU UU" |
|
115 apply (unfold Ispair_def) |
|
116 apply (rule strict_Spair_Rep [THEN arg_cong]) |
|
117 apply (rule disjI1) |
|
118 apply (rule refl) |
|
119 done |
|
120 |
|
121 lemma strict_Ispair2: |
|
122 "Ispair a UU = Ispair UU UU" |
|
123 apply (unfold Ispair_def) |
|
124 apply (rule strict_Spair_Rep [THEN arg_cong]) |
|
125 apply (rule disjI2) |
|
126 apply (rule refl) |
|
127 done |
|
128 |
|
129 lemma strict_Ispair_rev: "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU" |
|
130 apply (rule de_Morgan_disj [THEN subst]) |
|
131 apply (erule contrapos_nn) |
|
132 apply (erule strict_Ispair) |
|
133 done |
|
134 |
|
135 lemma defined_Ispair_rev: |
|
136 "Ispair a b = Ispair UU UU ==> (a = UU | b = UU)" |
|
137 apply (unfold Ispair_def) |
|
138 apply (rule defined_Spair_Rep_rev) |
|
139 apply (rule inj_on_Abs_Sprod [THEN inj_onD]) |
|
140 apply assumption |
|
141 apply (rule SprodI) |
|
142 apply (rule SprodI) |
|
143 done |
|
144 |
|
145 lemma defined_Ispair: "[|a~=UU; b~=UU|] ==> (Ispair a b) ~= (Ispair UU UU)" |
|
146 apply (rule contrapos_nn) |
|
147 apply (erule_tac [2] defined_Ispair_rev) |
|
148 apply (rule de_Morgan_disj [THEN iffD2]) |
|
149 apply (erule conjI) |
|
150 apply assumption |
|
151 done |
|
152 |
|
153 |
|
154 (* ------------------------------------------------------------------------ *) |
|
155 (* Exhaustion of the strict product ** *) |
|
156 (* ------------------------------------------------------------------------ *) |
|
157 |
|
158 lemma Exh_Sprod: |
|
159 "z=Ispair UU UU | (? a b. z=Ispair a b & a~=UU & b~=UU)" |
|
160 apply (unfold Ispair_def) |
|
161 apply (rule Rep_Sprod[unfolded Sprod_def, THEN CollectE]) |
|
162 apply (erule exE) |
|
163 apply (erule exE) |
|
164 apply (rule excluded_middle [THEN disjE]) |
|
165 apply (rule disjI2) |
|
166 apply (rule exI) |
|
167 apply (rule exI) |
|
168 apply (rule conjI) |
|
169 apply (rule Rep_Sprod_inverse [symmetric, THEN trans]) |
|
170 apply (erule arg_cong) |
|
171 apply (rule de_Morgan_disj [THEN subst]) |
|
172 apply assumption |
|
173 apply (rule disjI1) |
|
174 apply (rule Rep_Sprod_inverse [symmetric, THEN trans]) |
|
175 apply (rule_tac f = "Abs_Sprod" in arg_cong) |
|
176 apply (erule trans) |
|
177 apply (erule strict_Spair_Rep) |
|
178 done |
|
179 |
|
180 (* ------------------------------------------------------------------------ *) |
|
181 (* general elimination rule for strict product *) |
|
182 (* ------------------------------------------------------------------------ *) |
|
183 |
|
184 lemma IsprodE: |
|
185 assumes prem1: "p=Ispair UU UU ==> Q" |
|
186 assumes prem2: "!!x y. [|p=Ispair x y; x~=UU ; y~=UU|] ==> Q" |
|
187 shows "Q" |
|
188 apply (rule Exh_Sprod [THEN disjE]) |
|
189 apply (erule prem1) |
|
190 apply (erule exE) |
|
191 apply (erule exE) |
|
192 apply (erule conjE) |
|
193 apply (erule conjE) |
|
194 apply (erule prem2) |
|
195 apply assumption |
|
196 apply assumption |
|
197 done |
|
198 |
|
199 (* ------------------------------------------------------------------------ *) |
|
200 (* some results about the selectors Isfst, Issnd *) |
|
201 (* ------------------------------------------------------------------------ *) |
|
202 |
|
203 lemma strict_Isfst: "p=Ispair UU UU ==> Isfst p = UU" |
|
204 apply (unfold Isfst_def) |
|
205 apply (rule some_equality) |
|
206 apply (rule conjI) |
|
207 apply fast |
|
208 apply (intro strip) |
|
209 apply (rule_tac P = "Ispair UU UU = Ispair a b" in notE) |
|
210 apply (rule not_sym) |
|
211 apply (rule defined_Ispair) |
|
212 apply (fast+) |
|
213 done |
|
214 |
|
215 lemma strict_Isfst1 [simp]: "Isfst(Ispair UU y) = UU" |
|
216 apply (subst strict_Ispair1) |
|
217 apply (rule strict_Isfst) |
|
218 apply (rule refl) |
|
219 done |
|
220 |
|
221 lemma strict_Isfst2 [simp]: "Isfst(Ispair x UU) = UU" |
|
222 apply (subst strict_Ispair2) |
|
223 apply (rule strict_Isfst) |
|
224 apply (rule refl) |
|
225 done |
|
226 |
|
227 lemma strict_Issnd: "p=Ispair UU UU ==>Issnd p=UU" |
|
228 apply (unfold Issnd_def) |
|
229 apply (rule some_equality) |
|
230 apply (rule conjI) |
|
231 apply fast |
|
232 apply (intro strip) |
|
233 apply (rule_tac P = "Ispair UU UU = Ispair a b" in notE) |
|
234 apply (rule not_sym) |
|
235 apply (rule defined_Ispair) |
|
236 apply (fast+) |
|
237 done |
|
238 |
|
239 lemma strict_Issnd1 [simp]: "Issnd(Ispair UU y) = UU" |
|
240 apply (subst strict_Ispair1) |
|
241 apply (rule strict_Issnd) |
|
242 apply (rule refl) |
|
243 done |
|
244 |
|
245 lemma strict_Issnd2 [simp]: "Issnd(Ispair x UU) = UU" |
|
246 apply (subst strict_Ispair2) |
|
247 apply (rule strict_Issnd) |
|
248 apply (rule refl) |
|
249 done |
|
250 |
|
251 lemma Isfst: "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x" |
|
252 apply (unfold Isfst_def) |
|
253 apply (rule some_equality) |
|
254 apply (rule conjI) |
|
255 apply (intro strip) |
|
256 apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE) |
|
257 apply (erule defined_Ispair) |
|
258 apply assumption |
|
259 apply assumption |
|
260 apply (intro strip) |
|
261 apply (rule inject_Ispair [THEN conjunct1]) |
|
262 prefer 3 apply fast |
|
263 apply (fast+) |
|
264 done |
|
265 |
|
266 lemma Issnd: "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y" |
|
267 apply (unfold Issnd_def) |
|
268 apply (rule some_equality) |
|
269 apply (rule conjI) |
|
270 apply (intro strip) |
|
271 apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE) |
|
272 apply (erule defined_Ispair) |
|
273 apply assumption |
|
274 apply assumption |
|
275 apply (intro strip) |
|
276 apply (rule inject_Ispair [THEN conjunct2]) |
|
277 prefer 3 apply fast |
|
278 apply (fast+) |
|
279 done |
|
280 |
|
281 lemma Isfst2: "y~=UU ==>Isfst(Ispair x y)=x" |
|
282 apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE]) |
|
283 apply (erule Isfst) |
|
284 apply assumption |
|
285 apply (erule ssubst) |
|
286 apply (rule strict_Isfst1) |
|
287 done |
|
288 |
|
289 lemma Issnd2: "~x=UU ==>Issnd(Ispair x y)=y" |
|
290 apply (rule_tac Q = "y=UU" in excluded_middle [THEN disjE]) |
|
291 apply (erule Issnd) |
|
292 apply assumption |
|
293 apply (erule ssubst) |
|
294 apply (rule strict_Issnd2) |
|
295 done |
|
296 |
|
297 |
|
298 (* ------------------------------------------------------------------------ *) |
|
299 (* instantiate the simplifier *) |
|
300 (* ------------------------------------------------------------------------ *) |
|
301 |
|
302 lemmas Sprod0_ss = strict_Isfst1 strict_Isfst2 strict_Issnd1 strict_Issnd2 |
|
303 Isfst2 Issnd2 |
|
304 |
|
305 declare Isfst2 [simp] Issnd2 [simp] |
|
306 |
|
307 lemma defined_IsfstIssnd: "p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU" |
|
308 apply (rule_tac p = "p" in IsprodE) |
|
309 apply simp |
|
310 apply (erule ssubst) |
|
311 apply (rule conjI) |
|
312 apply (simp add: Sprod0_ss) |
|
313 apply (simp add: Sprod0_ss) |
|
314 done |
|
315 |
|
316 |
|
317 (* ------------------------------------------------------------------------ *) |
|
318 (* Surjective pairing: equivalent to Exh_Sprod *) |
|
319 (* ------------------------------------------------------------------------ *) |
|
320 |
|
321 lemma surjective_pairing_Sprod: "z = Ispair(Isfst z)(Issnd z)" |
|
322 apply (rule_tac z1 = "z" in Exh_Sprod [THEN disjE]) |
|
323 apply (simp add: Sprod0_ss) |
|
324 apply (erule exE) |
|
325 apply (erule exE) |
|
326 apply (simp add: Sprod0_ss) |
|
327 done |
|
328 |
|
329 lemma Sel_injective_Sprod: "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y" |
|
330 apply (subgoal_tac "Ispair (Isfst x) (Issnd x) =Ispair (Isfst y) (Issnd y) ") |
|
331 apply (simp (no_asm_use) add: surjective_pairing_Sprod[symmetric]) |
|
332 apply simp |
|
333 done |
|
334 |
|
335 subsection {* The strict product is a partial order *} |
|
336 |
|
337 instance "**"::(sq_ord,sq_ord)sq_ord .. |
|
338 |
|
339 defs (overloaded) |
|
340 less_sprod_def: "p1 << p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2" |
|
341 |
|
342 (* ------------------------------------------------------------------------ *) |
|
343 (* less_sprod is a partial order on Sprod *) |
|
344 (* ------------------------------------------------------------------------ *) |
|
345 |
|
346 lemma refl_less_sprod: "(p::'a ** 'b) << p" |
|
347 apply (unfold less_sprod_def) |
|
348 apply (fast intro: refl_less) |
|
349 done |
|
350 |
|
351 lemma antisym_less_sprod: |
|
352 "[|(p1::'a ** 'b) << p2;p2 << p1|] ==> p1=p2" |
|
353 apply (unfold less_sprod_def) |
|
354 apply (rule Sel_injective_Sprod) |
|
355 apply (fast intro: antisym_less) |
|
356 apply (fast intro: antisym_less) |
|
357 done |
|
358 |
|
359 lemma trans_less_sprod: |
|
360 "[|(p1::'a**'b) << p2;p2 << p3|] ==> p1 << p3" |
|
361 apply (unfold less_sprod_def) |
|
362 apply (blast intro: trans_less) |
|
363 done |
|
364 |
|
365 instance "**"::(pcpo,pcpo)po |
|
366 by intro_classes |
|
367 (assumption | rule refl_less_sprod antisym_less_sprod trans_less_sprod)+ |
|
368 |
|
369 (* for compatibility with old HOLCF-Version *) |
|
370 lemma inst_sprod_po: "(op <<)=(%x y. Isfst x<<Isfst y&Issnd x<<Issnd y)" |
|
371 apply (fold less_sprod_def) |
|
372 apply (rule refl) |
|
373 done |
|
374 |
|
375 subsection {* The strict product is pointed *} |
|
376 (* ------------------------------------------------------------------------ *) |
|
377 (* type sprod is pointed *) |
|
378 (* ------------------------------------------------------------------------ *) |
|
379 (* |
|
380 lemma minimal_sprod: "Ispair UU UU << p" |
|
381 apply (simp add: inst_sprod_po minimal) |
|
382 done |
|
383 |
|
384 lemmas UU_sprod_def = minimal_sprod [THEN minimal2UU, symmetric, standard] |
|
385 |
|
386 lemma least_sprod: "? x::'a**'b.!y. x<<y" |
|
387 apply (rule_tac x = "Ispair UU UU" in exI) |
|
388 apply (rule minimal_sprod [THEN allI]) |
|
389 done |
|
390 *) |
|
391 (* ------------------------------------------------------------------------ *) |
|
392 (* Ispair is monotone in both arguments *) |
|
393 (* ------------------------------------------------------------------------ *) |
|
394 |
|
395 lemma monofun_Ispair1: "monofun(Ispair)" |
|
396 apply (unfold monofun) |
|
397 apply (intro strip) |
|
398 apply (rule less_fun [THEN iffD2]) |
|
399 apply (intro strip) |
|
400 apply (rule_tac Q = "xa=UU" in excluded_middle [THEN disjE]) |
|
401 apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE]) |
|
402 apply (frule notUU_I) |
|
403 apply assumption |
|
404 apply (simp_all add: Sprod0_ss inst_sprod_po refl_less minimal) |
|
405 done |
|
406 |
|
407 lemma monofun_Ispair2: "monofun(Ispair(x))" |
|
408 apply (unfold monofun) |
|
409 apply (intro strip) |
|
410 apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE]) |
|
411 apply (rule_tac Q = "xa=UU" in excluded_middle [THEN disjE]) |
|
412 apply (frule notUU_I) |
|
413 apply assumption |
|
414 apply (simp_all add: Sprod0_ss inst_sprod_po refl_less minimal) |
|
415 done |
|
416 |
|
417 lemma monofun_Ispair: "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2" |
|
418 apply (rule trans_less) |
|
419 apply (rule monofun_Ispair1 [THEN monofunE, THEN spec, THEN spec, THEN mp, THEN less_fun [THEN iffD1, THEN spec]]) |
|
420 prefer 2 apply (rule monofun_Ispair2 [THEN monofunE, THEN spec, THEN spec, THEN mp]) |
|
421 apply assumption |
|
422 apply assumption |
|
423 done |
|
424 |
|
425 (* ------------------------------------------------------------------------ *) |
|
426 (* Isfst and Issnd are monotone *) |
|
427 (* ------------------------------------------------------------------------ *) |
|
428 |
|
429 lemma monofun_Isfst: "monofun(Isfst)" |
|
430 apply (unfold monofun) |
|
431 apply (simp add: inst_sprod_po) |
|
432 done |
|
433 |
|
434 lemma monofun_Issnd: "monofun(Issnd)" |
|
435 apply (unfold monofun) |
|
436 apply (simp add: inst_sprod_po) |
|
437 done |
|
438 |
|
439 subsection {* The strict product is a cpo *} |
|
440 (* ------------------------------------------------------------------------ *) |
|
441 (* the type 'a ** 'b is a cpo *) |
|
442 (* ------------------------------------------------------------------------ *) |
|
443 |
|
444 lemma lub_sprod: |
|
445 "[|chain(S)|] ==> range(S) <<| |
|
446 Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))" |
|
447 apply (rule is_lubI) |
|
448 apply (rule ub_rangeI) |
|
449 apply (rule_tac t = "S (i) " in surjective_pairing_Sprod [THEN ssubst]) |
|
450 apply (rule monofun_Ispair) |
|
451 apply (rule is_ub_thelub) |
|
452 apply (erule monofun_Isfst [THEN ch2ch_monofun]) |
|
453 apply (rule is_ub_thelub) |
|
454 apply (erule monofun_Issnd [THEN ch2ch_monofun]) |
|
455 apply (rule_tac t = "u" in surjective_pairing_Sprod [THEN ssubst]) |
|
456 apply (rule monofun_Ispair) |
|
457 apply (rule is_lub_thelub) |
|
458 apply (erule monofun_Isfst [THEN ch2ch_monofun]) |
|
459 apply (erule monofun_Isfst [THEN ub2ub_monofun]) |
|
460 apply (rule is_lub_thelub) |
|
461 apply (erule monofun_Issnd [THEN ch2ch_monofun]) |
|
462 apply (erule monofun_Issnd [THEN ub2ub_monofun]) |
|
463 done |
|
464 |
|
465 lemmas thelub_sprod = lub_sprod [THEN thelubI, standard] |
|
466 |
|
467 lemma cpo_sprod: "chain(S::nat=>'a**'b)==>? x. range(S)<<| x" |
|
468 apply (rule exI) |
|
469 apply (erule lub_sprod) |
|
470 done |
|
471 |
|
472 instance "**" :: (pcpo, pcpo) cpo |
|
473 by intro_classes (rule cpo_sprod) |
|
474 |
|
475 |
|
476 subsection {* The strict product is a pcpo *} |
|
477 |
|
478 lemma minimal_sprod: "Ispair UU UU << p" |
|
479 apply (simp add: inst_sprod_po minimal) |
|
480 done |
|
481 |
|
482 lemmas UU_sprod_def = minimal_sprod [THEN minimal2UU, symmetric, standard] |
|
483 |
|
484 lemma least_sprod: "? x::'a**'b.!y. x<<y" |
|
485 apply (rule_tac x = "Ispair UU UU" in exI) |
|
486 apply (rule minimal_sprod [THEN allI]) |
|
487 done |
|
488 |
|
489 instance "**" :: (pcpo, pcpo) pcpo |
|
490 by intro_classes (rule least_sprod) |
|
491 |
|
492 |
|
493 subsection {* Other constants *} |
|
494 |
|
495 consts |
|
496 spair :: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *) |
|
497 sfst :: "('a**'b)->'a" |
|
498 ssnd :: "('a**'b)->'b" |
|
499 ssplit :: "('a->'b->'c)->('a**'b)->'c" |
|
500 |
|
501 syntax |
|
502 "@stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))") |
|
503 |
|
504 translations |
|
505 "(:x, y, z:)" == "(:x, (:y, z:):)" |
|
506 "(:x, y:)" == "spair$x$y" |
|
507 |
|
508 defs |
|
509 spair_def: "spair == (LAM x y. Ispair x y)" |
|
510 sfst_def: "sfst == (LAM p. Isfst p)" |
|
511 ssnd_def: "ssnd == (LAM p. Issnd p)" |
|
512 ssplit_def: "ssplit == (LAM f. strictify$(LAM p. f$(sfst$p)$(ssnd$p)))" |
|
513 |
|
514 (* for compatibility with old HOLCF-Version *) |
|
515 lemma inst_sprod_pcpo: "UU = Ispair UU UU" |
|
516 apply (simp add: UU_def UU_sprod_def) |
|
517 done |
|
518 |
|
519 declare inst_sprod_pcpo [symmetric, simp] |
|
520 |
|
521 (* ------------------------------------------------------------------------ *) |
|
522 (* continuity of Ispair, Isfst, Issnd *) |
|
523 (* ------------------------------------------------------------------------ *) |
|
524 |
|
525 lemma sprod3_lemma1: |
|
526 "[| chain(Y); x~= UU; lub(range(Y))~= UU |] ==> |
|
527 Ispair (lub(range Y)) x = |
|
528 Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) |
|
529 (lub(range(%i. Issnd(Ispair(Y i) x))))" |
|
530 apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong]) |
|
531 apply (rule lub_equal) |
|
532 apply assumption |
|
533 apply (rule monofun_Isfst [THEN ch2ch_monofun]) |
|
534 apply (rule ch2ch_fun) |
|
535 apply (rule monofun_Ispair1 [THEN ch2ch_monofun]) |
|
536 apply assumption |
|
537 apply (rule allI) |
|
538 apply (simp (no_asm_simp)) |
|
539 apply (rule sym) |
|
540 apply (drule chain_UU_I_inverse2) |
|
541 apply (erule exE) |
|
542 apply (rule lub_chain_maxelem) |
|
543 apply (erule Issnd2) |
|
544 apply (rule allI) |
|
545 apply (rename_tac "j") |
|
546 apply (case_tac "Y (j) =UU") |
|
547 apply auto |
|
548 done |
|
549 |
|
550 lemma sprod3_lemma2: |
|
551 "[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==> |
|
552 Ispair (lub(range Y)) x = |
|
553 Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) |
|
554 (lub(range(%i. Issnd(Ispair(Y i) x))))" |
|
555 apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst) |
|
556 apply assumption |
|
557 apply (rule trans) |
|
558 apply (rule strict_Ispair1) |
|
559 apply (rule strict_Ispair [symmetric]) |
|
560 apply (rule disjI1) |
|
561 apply (rule chain_UU_I_inverse) |
|
562 apply auto |
|
563 apply (erule chain_UU_I [THEN spec]) |
|
564 apply assumption |
|
565 done |
|
566 |
|
567 |
|
568 lemma sprod3_lemma3: |
|
569 "[| chain(Y); x = UU |] ==> |
|
570 Ispair (lub(range Y)) x = |
|
571 Ispair (lub(range(%i. Isfst(Ispair (Y i) x)))) |
|
572 (lub(range(%i. Issnd(Ispair (Y i) x))))" |
|
573 apply (erule ssubst) |
|
574 apply (rule trans) |
|
575 apply (rule strict_Ispair2) |
|
576 apply (rule strict_Ispair [symmetric]) |
|
577 apply (rule disjI1) |
|
578 apply (rule chain_UU_I_inverse) |
|
579 apply (rule allI) |
|
580 apply (simp add: Sprod0_ss) |
|
581 done |
|
582 |
|
583 lemma contlub_Ispair1: "contlub(Ispair)" |
|
584 apply (rule contlubI) |
|
585 apply (intro strip) |
|
586 apply (rule expand_fun_eq [THEN iffD2]) |
|
587 apply (intro strip) |
|
588 apply (subst lub_fun [THEN thelubI]) |
|
589 apply (erule monofun_Ispair1 [THEN ch2ch_monofun]) |
|
590 apply (rule trans) |
|
591 apply (rule_tac [2] thelub_sprod [symmetric]) |
|
592 apply (rule_tac [2] ch2ch_fun) |
|
593 apply (erule_tac [2] monofun_Ispair1 [THEN ch2ch_monofun]) |
|
594 apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE]) |
|
595 apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE]) |
|
596 apply (erule sprod3_lemma1) |
|
597 apply assumption |
|
598 apply assumption |
|
599 apply (erule sprod3_lemma2) |
|
600 apply assumption |
|
601 apply assumption |
|
602 apply (erule sprod3_lemma3) |
|
603 apply assumption |
|
604 done |
|
605 |
|
606 lemma sprod3_lemma4: |
|
607 "[| chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==> |
|
608 Ispair x (lub(range Y)) = |
|
609 Ispair (lub(range(%i. Isfst (Ispair x (Y i))))) |
|
610 (lub(range(%i. Issnd (Ispair x (Y i)))))" |
|
611 apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong]) |
|
612 apply (rule sym) |
|
613 apply (drule chain_UU_I_inverse2) |
|
614 apply (erule exE) |
|
615 apply (rule lub_chain_maxelem) |
|
616 apply (erule Isfst2) |
|
617 apply (rule allI) |
|
618 apply (rename_tac "j") |
|
619 apply (case_tac "Y (j) =UU") |
|
620 apply auto |
|
621 done |
|
622 |
|
623 lemma sprod3_lemma5: |
|
624 "[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==> |
|
625 Ispair x (lub(range Y)) = |
|
626 Ispair (lub(range(%i. Isfst(Ispair x (Y i))))) |
|
627 (lub(range(%i. Issnd(Ispair x (Y i)))))" |
|
628 apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst) |
|
629 apply assumption |
|
630 apply (rule trans) |
|
631 apply (rule strict_Ispair2) |
|
632 apply (rule strict_Ispair [symmetric]) |
|
633 apply (rule disjI2) |
|
634 apply (rule chain_UU_I_inverse) |
|
635 apply (rule allI) |
|
636 apply (simp add: Sprod0_ss) |
|
637 apply (erule chain_UU_I [THEN spec]) |
|
638 apply assumption |
|
639 done |
|
640 |
|
641 lemma sprod3_lemma6: |
|
642 "[| chain(Y); x = UU |] ==> |
|
643 Ispair x (lub(range Y)) = |
|
644 Ispair (lub(range(%i. Isfst (Ispair x (Y i))))) |
|
645 (lub(range(%i. Issnd (Ispair x (Y i)))))" |
|
646 apply (rule_tac s = "UU" and t = "x" in ssubst) |
|
647 apply assumption |
|
648 apply (rule trans) |
|
649 apply (rule strict_Ispair1) |
|
650 apply (rule strict_Ispair [symmetric]) |
|
651 apply (rule disjI1) |
|
652 apply (rule chain_UU_I_inverse) |
|
653 apply (rule allI) |
|
654 apply (simp add: Sprod0_ss) |
|
655 done |
|
656 |
|
657 lemma contlub_Ispair2: "contlub(Ispair(x))" |
|
658 apply (rule contlubI) |
|
659 apply (intro strip) |
|
660 apply (rule trans) |
|
661 apply (rule_tac [2] thelub_sprod [symmetric]) |
|
662 apply (erule_tac [2] monofun_Ispair2 [THEN ch2ch_monofun]) |
|
663 apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE]) |
|
664 apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE]) |
|
665 apply (erule sprod3_lemma4) |
|
666 apply assumption |
|
667 apply assumption |
|
668 apply (erule sprod3_lemma5) |
|
669 apply assumption |
|
670 apply assumption |
|
671 apply (erule sprod3_lemma6) |
|
672 apply assumption |
|
673 done |
|
674 |
|
675 lemma cont_Ispair1: "cont(Ispair)" |
|
676 apply (rule monocontlub2cont) |
|
677 apply (rule monofun_Ispair1) |
|
678 apply (rule contlub_Ispair1) |
|
679 done |
|
680 |
|
681 lemma cont_Ispair2: "cont(Ispair(x))" |
|
682 apply (rule monocontlub2cont) |
|
683 apply (rule monofun_Ispair2) |
|
684 apply (rule contlub_Ispair2) |
|
685 done |
|
686 |
|
687 lemma contlub_Isfst: "contlub(Isfst)" |
|
688 apply (rule contlubI) |
|
689 apply (intro strip) |
|
690 apply (subst lub_sprod [THEN thelubI]) |
|
691 apply assumption |
|
692 apply (rule_tac Q = "lub (range (%i. Issnd (Y (i))))=UU" in excluded_middle [THEN disjE]) |
|
693 apply (simp add: Sprod0_ss) |
|
694 apply (rule_tac s = "UU" and t = "lub (range (%i. Issnd (Y (i))))" in ssubst) |
|
695 apply assumption |
|
696 apply (rule trans) |
|
697 apply (simp add: Sprod0_ss) |
|
698 apply (rule sym) |
|
699 apply (rule chain_UU_I_inverse) |
|
700 apply (rule allI) |
|
701 apply (rule strict_Isfst) |
|
702 apply (rule contrapos_np) |
|
703 apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct2]) |
|
704 apply (fast dest!: monofun_Issnd [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec]) |
|
705 done |
|
706 |
|
707 lemma contlub_Issnd: "contlub(Issnd)" |
|
708 apply (rule contlubI) |
|
709 apply (intro strip) |
|
710 apply (subst lub_sprod [THEN thelubI]) |
|
711 apply assumption |
|
712 apply (rule_tac Q = "lub (range (%i. Isfst (Y (i))))=UU" in excluded_middle [THEN disjE]) |
|
713 apply (simp add: Sprod0_ss) |
|
714 apply (rule_tac s = "UU" and t = "lub (range (%i. Isfst (Y (i))))" in ssubst) |
|
715 apply assumption |
|
716 apply (simp add: Sprod0_ss) |
|
717 apply (rule sym) |
|
718 apply (rule chain_UU_I_inverse) |
|
719 apply (rule allI) |
|
720 apply (rule strict_Issnd) |
|
721 apply (rule contrapos_np) |
|
722 apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct1]) |
|
723 apply (fast dest!: monofun_Isfst [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec]) |
|
724 done |
|
725 |
|
726 lemma cont_Isfst: "cont(Isfst)" |
|
727 apply (rule monocontlub2cont) |
|
728 apply (rule monofun_Isfst) |
|
729 apply (rule contlub_Isfst) |
|
730 done |
|
731 |
|
732 lemma cont_Issnd: "cont(Issnd)" |
|
733 apply (rule monocontlub2cont) |
|
734 apply (rule monofun_Issnd) |
|
735 apply (rule contlub_Issnd) |
|
736 done |
|
737 |
|
738 lemma spair_eq: "[|x1=x2;y1=y2|] ==> (:x1,y1:) = (:x2,y2:)" |
|
739 apply fast |
|
740 done |
|
741 |
|
742 (* ------------------------------------------------------------------------ *) |
|
743 (* convert all lemmas to the continuous versions *) |
|
744 (* ------------------------------------------------------------------------ *) |
|
745 |
|
746 lemma beta_cfun_sprod [simp]: |
|
747 "(LAM x y. Ispair x y)$a$b = Ispair a b" |
|
748 apply (subst beta_cfun) |
|
749 apply (simp (no_asm) add: cont_Ispair2 cont_Ispair1 cont2cont_CF1L) |
|
750 apply (subst beta_cfun) |
|
751 apply (rule cont_Ispair2) |
|
752 apply (rule refl) |
|
753 done |
|
754 |
|
755 lemma inject_spair: |
|
756 "[| aa~=UU ; ba~=UU ; (:a,b:)=(:aa,ba:) |] ==> a=aa & b=ba" |
|
757 apply (unfold spair_def) |
|
758 apply (erule inject_Ispair) |
|
759 apply assumption |
|
760 apply (erule box_equals) |
|
761 apply (rule beta_cfun_sprod) |
|
762 apply (rule beta_cfun_sprod) |
|
763 done |
|
764 |
|
765 lemma inst_sprod_pcpo2: "UU = (:UU,UU:)" |
|
766 apply (unfold spair_def) |
|
767 apply (rule sym) |
|
768 apply (rule trans) |
|
769 apply (rule beta_cfun_sprod) |
|
770 apply (rule sym) |
|
771 apply (rule inst_sprod_pcpo) |
|
772 done |
|
773 |
|
774 lemma strict_spair: |
|
775 "(a=UU | b=UU) ==> (:a,b:)=UU" |
|
776 apply (unfold spair_def) |
|
777 apply (rule trans) |
|
778 apply (rule beta_cfun_sprod) |
|
779 apply (rule trans) |
|
780 apply (rule_tac [2] inst_sprod_pcpo [symmetric]) |
|
781 apply (erule strict_Ispair) |
|
782 done |
|
783 |
|
784 lemma strict_spair1: "(:UU,b:) = UU" |
|
785 apply (unfold spair_def) |
|
786 apply (subst beta_cfun_sprod) |
|
787 apply (rule trans) |
|
788 apply (rule_tac [2] inst_sprod_pcpo [symmetric]) |
|
789 apply (rule strict_Ispair1) |
|
790 done |
|
791 |
|
792 lemma strict_spair2: "(:a,UU:) = UU" |
|
793 apply (unfold spair_def) |
|
794 apply (subst beta_cfun_sprod) |
|
795 apply (rule trans) |
|
796 apply (rule_tac [2] inst_sprod_pcpo [symmetric]) |
|
797 apply (rule strict_Ispair2) |
|
798 done |
|
799 |
|
800 declare strict_spair1 [simp] strict_spair2 [simp] |
|
801 |
|
802 lemma strict_spair_rev: "(:x,y:)~=UU ==> ~x=UU & ~y=UU" |
|
803 apply (unfold spair_def) |
|
804 apply (rule strict_Ispair_rev) |
|
805 apply auto |
|
806 done |
|
807 |
|
808 lemma defined_spair_rev: "(:a,b:) = UU ==> (a = UU | b = UU)" |
|
809 apply (unfold spair_def) |
|
810 apply (rule defined_Ispair_rev) |
|
811 apply auto |
|
812 done |
|
813 |
|
814 lemma defined_spair: |
|
815 "[|a~=UU; b~=UU|] ==> (:a,b:) ~= UU" |
|
816 apply (unfold spair_def) |
|
817 apply (subst beta_cfun_sprod) |
|
818 apply (subst inst_sprod_pcpo) |
|
819 apply (erule defined_Ispair) |
|
820 apply assumption |
|
821 done |
|
822 |
|
823 lemma Exh_Sprod2: |
|
824 "z=UU | (? a b. z=(:a,b:) & a~=UU & b~=UU)" |
|
825 apply (unfold spair_def) |
|
826 apply (rule Exh_Sprod [THEN disjE]) |
|
827 apply (rule disjI1) |
|
828 apply (subst inst_sprod_pcpo) |
|
829 apply assumption |
|
830 apply (rule disjI2) |
|
831 apply (erule exE) |
|
832 apply (erule exE) |
|
833 apply (rule exI) |
|
834 apply (rule exI) |
|
835 apply (rule conjI) |
|
836 apply (subst beta_cfun_sprod) |
|
837 apply fast |
|
838 apply fast |
|
839 done |
|
840 |
|
841 |
|
842 lemma sprodE: |
|
843 assumes prem1: "p=UU ==> Q" |
|
844 assumes prem2: "!!x y. [| p=(:x,y:); x~=UU; y~=UU|] ==> Q" |
|
845 shows "Q" |
|
846 apply (rule IsprodE) |
|
847 apply (rule prem1) |
|
848 apply (subst inst_sprod_pcpo) |
|
849 apply assumption |
|
850 apply (rule prem2) |
|
851 prefer 2 apply (assumption) |
|
852 prefer 2 apply (assumption) |
|
853 apply (unfold spair_def) |
|
854 apply (subst beta_cfun_sprod) |
|
855 apply assumption |
|
856 done |
|
857 |
|
858 |
|
859 lemma strict_sfst: |
|
860 "p=UU==>sfst$p=UU" |
|
861 apply (unfold sfst_def) |
|
862 apply (subst beta_cfun) |
|
863 apply (rule cont_Isfst) |
|
864 apply (rule strict_Isfst) |
|
865 apply (rule inst_sprod_pcpo [THEN subst]) |
|
866 apply assumption |
|
867 done |
|
868 |
|
869 lemma strict_sfst1: |
|
870 "sfst$(:UU,y:) = UU" |
|
871 apply (unfold sfst_def spair_def) |
|
872 apply (subst beta_cfun_sprod) |
|
873 apply (subst beta_cfun) |
|
874 apply (rule cont_Isfst) |
|
875 apply (rule strict_Isfst1) |
|
876 done |
|
877 |
|
878 lemma strict_sfst2: |
|
879 "sfst$(:x,UU:) = UU" |
|
880 apply (unfold sfst_def spair_def) |
|
881 apply (subst beta_cfun_sprod) |
|
882 apply (subst beta_cfun) |
|
883 apply (rule cont_Isfst) |
|
884 apply (rule strict_Isfst2) |
|
885 done |
|
886 |
|
887 lemma strict_ssnd: |
|
888 "p=UU==>ssnd$p=UU" |
|
889 apply (unfold ssnd_def) |
|
890 apply (subst beta_cfun) |
|
891 apply (rule cont_Issnd) |
|
892 apply (rule strict_Issnd) |
|
893 apply (rule inst_sprod_pcpo [THEN subst]) |
|
894 apply assumption |
|
895 done |
|
896 |
|
897 lemma strict_ssnd1: |
|
898 "ssnd$(:UU,y:) = UU" |
|
899 apply (unfold ssnd_def spair_def) |
|
900 apply (subst beta_cfun_sprod) |
|
901 apply (subst beta_cfun) |
|
902 apply (rule cont_Issnd) |
|
903 apply (rule strict_Issnd1) |
|
904 done |
|
905 |
|
906 lemma strict_ssnd2: |
|
907 "ssnd$(:x,UU:) = UU" |
|
908 apply (unfold ssnd_def spair_def) |
|
909 apply (subst beta_cfun_sprod) |
|
910 apply (subst beta_cfun) |
|
911 apply (rule cont_Issnd) |
|
912 apply (rule strict_Issnd2) |
|
913 done |
|
914 |
|
915 lemma sfst2: |
|
916 "y~=UU ==>sfst$(:x,y:)=x" |
|
917 apply (unfold sfst_def spair_def) |
|
918 apply (subst beta_cfun_sprod) |
|
919 apply (subst beta_cfun) |
|
920 apply (rule cont_Isfst) |
|
921 apply (erule Isfst2) |
|
922 done |
|
923 |
|
924 lemma ssnd2: |
|
925 "x~=UU ==>ssnd$(:x,y:)=y" |
|
926 apply (unfold ssnd_def spair_def) |
|
927 apply (subst beta_cfun_sprod) |
|
928 apply (subst beta_cfun) |
|
929 apply (rule cont_Issnd) |
|
930 apply (erule Issnd2) |
|
931 done |
|
932 |
|
933 |
|
934 lemma defined_sfstssnd: |
|
935 "p~=UU ==> sfst$p ~=UU & ssnd$p ~=UU" |
|
936 apply (unfold sfst_def ssnd_def spair_def) |
|
937 apply (simplesubst beta_cfun) |
|
938 apply (rule cont_Issnd) |
|
939 apply (subst beta_cfun) |
|
940 apply (rule cont_Isfst) |
|
941 apply (rule defined_IsfstIssnd) |
|
942 apply (rule inst_sprod_pcpo [THEN subst]) |
|
943 apply assumption |
|
944 done |
|
945 |
|
946 lemma surjective_pairing_Sprod2: "(:sfst$p , ssnd$p:) = p" |
|
947 apply (unfold sfst_def ssnd_def spair_def) |
|
948 apply (subst beta_cfun_sprod) |
|
949 apply (simplesubst beta_cfun) |
|
950 apply (rule cont_Issnd) |
|
951 apply (subst beta_cfun) |
|
952 apply (rule cont_Isfst) |
|
953 apply (rule surjective_pairing_Sprod [symmetric]) |
|
954 done |
|
955 |
|
956 lemma lub_sprod2: |
|
957 "chain(S) ==> range(S) <<| |
|
958 (: lub(range(%i. sfst$(S i))), lub(range(%i. ssnd$(S i))) :)" |
|
959 apply (unfold sfst_def ssnd_def spair_def) |
|
960 apply (subst beta_cfun_sprod) |
|
961 apply (simplesubst beta_cfun [THEN ext]) |
|
962 apply (rule cont_Issnd) |
|
963 apply (subst beta_cfun [THEN ext]) |
|
964 apply (rule cont_Isfst) |
|
965 apply (erule lub_sprod) |
|
966 done |
|
967 |
|
968 |
|
969 lemmas thelub_sprod2 = lub_sprod2 [THEN thelubI, standard] |
|
970 (* |
|
971 "chain ?S1 ==> |
|
972 lub (range ?S1) = |
|
973 (:lub (range (%i. sfst$(?S1 i))), lub (range (%i. ssnd$(?S1 i))):)" : thm |
|
974 *) |
|
975 |
|
976 lemma ssplit1: |
|
977 "ssplit$f$UU=UU" |
|
978 apply (unfold ssplit_def) |
|
979 apply (subst beta_cfun) |
|
980 apply (simp (no_asm)) |
|
981 apply (subst strictify1) |
|
982 apply (rule refl) |
|
983 done |
|
984 |
|
985 lemma ssplit2: |
|
986 "[|x~=UU;y~=UU|] ==> ssplit$f$(:x,y:)= f$x$y" |
|
987 apply (unfold ssplit_def) |
|
988 apply (subst beta_cfun) |
|
989 apply (simp (no_asm)) |
|
990 apply (subst strictify2) |
|
991 apply (rule defined_spair) |
|
992 apply assumption |
|
993 apply assumption |
|
994 apply (subst beta_cfun) |
|
995 apply (simp (no_asm)) |
|
996 apply (subst sfst2) |
|
997 apply assumption |
|
998 apply (subst ssnd2) |
|
999 apply assumption |
|
1000 apply (rule refl) |
|
1001 done |
|
1002 |
|
1003 |
|
1004 lemma ssplit3: |
|
1005 "ssplit$spair$z=z" |
|
1006 apply (unfold ssplit_def) |
|
1007 apply (subst beta_cfun) |
|
1008 apply (simp (no_asm)) |
|
1009 apply (case_tac "z=UU") |
|
1010 apply (erule ssubst) |
|
1011 apply (rule strictify1) |
|
1012 apply (rule trans) |
|
1013 apply (rule strictify2) |
|
1014 apply assumption |
|
1015 apply (subst beta_cfun) |
|
1016 apply (simp (no_asm)) |
|
1017 apply (rule surjective_pairing_Sprod2) |
|
1018 done |
|
1019 |
|
1020 (* ------------------------------------------------------------------------ *) |
|
1021 (* install simplifier for Sprod *) |
|
1022 (* ------------------------------------------------------------------------ *) |
|
1023 |
|
1024 lemmas Sprod_rews = strict_sfst1 strict_sfst2 |
|
1025 strict_ssnd1 strict_ssnd2 sfst2 ssnd2 defined_spair |
|
1026 ssplit1 ssplit2 |
|
1027 declare Sprod_rews [simp] |
|
1028 |
|
1029 end |