1 (* Title: HOLCF/Sprod3 |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 |
1 |
5 Class instance of ** for class pcpo |
2 (* legacy ML bindings *) |
6 *) |
|
7 |
3 |
8 (* for compatibility with old HOLCF-Version *) |
4 val spair_def = thm "spair_def"; |
9 Goal "UU = Ispair UU UU"; |
5 val sfst_def = thm "sfst_def"; |
10 by (simp_tac (HOL_ss addsimps [UU_def,UU_sprod_def]) 1); |
6 val ssnd_def = thm "ssnd_def"; |
11 qed "inst_sprod_pcpo"; |
7 val ssplit_def = thm "ssplit_def"; |
|
8 val inst_sprod_pcpo = thm "inst_sprod_pcpo"; |
|
9 val sprod3_lemma1 = thm "sprod3_lemma1"; |
|
10 val sprod3_lemma2 = thm "sprod3_lemma2"; |
|
11 val sprod3_lemma3 = thm "sprod3_lemma3"; |
|
12 val contlub_Ispair1 = thm "contlub_Ispair1"; |
|
13 val sprod3_lemma4 = thm "sprod3_lemma4"; |
|
14 val sprod3_lemma5 = thm "sprod3_lemma5"; |
|
15 val sprod3_lemma6 = thm "sprod3_lemma6"; |
|
16 val contlub_Ispair2 = thm "contlub_Ispair2"; |
|
17 val cont_Ispair1 = thm "cont_Ispair1"; |
|
18 val cont_Ispair2 = thm "cont_Ispair2"; |
|
19 val contlub_Isfst = thm "contlub_Isfst"; |
|
20 val contlub_Issnd = thm "contlub_Issnd"; |
|
21 val cont_Isfst = thm "cont_Isfst"; |
|
22 val cont_Issnd = thm "cont_Issnd"; |
|
23 val spair_eq = thm "spair_eq"; |
|
24 val beta_cfun_sprod = thm "beta_cfun_sprod"; |
|
25 val inject_spair = thm "inject_spair"; |
|
26 val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2"; |
|
27 val strict_spair = thm "strict_spair"; |
|
28 val strict_spair1 = thm "strict_spair1"; |
|
29 val strict_spair2 = thm "strict_spair2"; |
|
30 val strict_spair_rev = thm "strict_spair_rev"; |
|
31 val defined_spair_rev = thm "defined_spair_rev"; |
|
32 val defined_spair = thm "defined_spair"; |
|
33 val Exh_Sprod2 = thm "Exh_Sprod2"; |
|
34 val sprodE = thm "sprodE"; |
|
35 val strict_sfst = thm "strict_sfst"; |
|
36 val strict_sfst1 = thm "strict_sfst1"; |
|
37 val strict_sfst2 = thm "strict_sfst2"; |
|
38 val strict_ssnd = thm "strict_ssnd"; |
|
39 val strict_ssnd1 = thm "strict_ssnd1"; |
|
40 val strict_ssnd2 = thm "strict_ssnd2"; |
|
41 val sfst2 = thm "sfst2"; |
|
42 val ssnd2 = thm "ssnd2"; |
|
43 val defined_sfstssnd = thm "defined_sfstssnd"; |
|
44 val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2"; |
|
45 val lub_sprod2 = thm "lub_sprod2"; |
|
46 val thelub_sprod2 = thm "thelub_sprod2"; |
|
47 val ssplit1 = thm "ssplit1"; |
|
48 val ssplit2 = thm "ssplit2"; |
|
49 val ssplit3 = thm "ssplit3"; |
|
50 val Sprod_rews = [strict_sfst1, strict_sfst2, |
|
51 strict_ssnd1, strict_ssnd2, sfst2, ssnd2, defined_spair, |
|
52 ssplit1, ssplit2] |
12 |
53 |
13 Addsimps [inst_sprod_pcpo RS sym]; |
|
14 |
|
15 (* ------------------------------------------------------------------------ *) |
|
16 (* continuity of Ispair, Isfst, Issnd *) |
|
17 (* ------------------------------------------------------------------------ *) |
|
18 |
|
19 Goal |
|
20 "[| chain(Y); x~= UU; lub(range(Y))~= UU |] ==>\ |
|
21 \ Ispair (lub(range Y)) x =\ |
|
22 \ Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) \ |
|
23 \ (lub(range(%i. Issnd(Ispair(Y i) x))))"; |
|
24 by (res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1); |
|
25 by (rtac lub_equal 1); |
|
26 by (atac 1); |
|
27 by (rtac (monofun_Isfst RS ch2ch_monofun) 1); |
|
28 by (rtac ch2ch_fun 1); |
|
29 by (rtac (monofun_Ispair1 RS ch2ch_monofun) 1); |
|
30 by (atac 1); |
|
31 by (rtac allI 1); |
|
32 by (Asm_simp_tac 1); |
|
33 by (rtac sym 1); |
|
34 by (dtac chain_UU_I_inverse2 1); |
|
35 by (etac exE 1); |
|
36 by (rtac lub_chain_maxelem 1); |
|
37 by (etac Issnd2 1); |
|
38 by (rtac allI 1); |
|
39 by (rename_tac "j" 1); |
|
40 by (case_tac "Y(j)=UU" 1); |
|
41 by Auto_tac; |
|
42 qed "sprod3_lemma1"; |
|
43 |
|
44 Goal |
|
45 "[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\ |
|
46 \ Ispair (lub(range Y)) x =\ |
|
47 \ Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))\ |
|
48 \ (lub(range(%i. Issnd(Ispair(Y i) x))))"; |
|
49 by (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1); |
|
50 by (atac 1); |
|
51 by (rtac trans 1); |
|
52 by (rtac strict_Ispair1 1); |
|
53 by (rtac (strict_Ispair RS sym) 1); |
|
54 by (rtac disjI1 1); |
|
55 by (rtac chain_UU_I_inverse 1); |
|
56 by Auto_tac; |
|
57 by (etac (chain_UU_I RS spec) 1); |
|
58 by (atac 1); |
|
59 qed "sprod3_lemma2"; |
|
60 |
|
61 |
|
62 Goal |
|
63 "[| chain(Y); x = UU |] ==>\ |
|
64 \ Ispair (lub(range Y)) x =\ |
|
65 \ Ispair (lub(range(%i. Isfst(Ispair (Y i) x))))\ |
|
66 \ (lub(range(%i. Issnd(Ispair (Y i) x))))"; |
|
67 by (etac ssubst 1); |
|
68 by (rtac trans 1); |
|
69 by (rtac strict_Ispair2 1); |
|
70 by (rtac (strict_Ispair RS sym) 1); |
|
71 by (rtac disjI1 1); |
|
72 by (rtac chain_UU_I_inverse 1); |
|
73 by (rtac allI 1); |
|
74 by (simp_tac Sprod0_ss 1); |
|
75 qed "sprod3_lemma3"; |
|
76 |
|
77 Goal "contlub(Ispair)"; |
|
78 by (rtac contlubI 1); |
|
79 by (strip_tac 1); |
|
80 by (rtac (expand_fun_eq RS iffD2) 1); |
|
81 by (strip_tac 1); |
|
82 by (stac (lub_fun RS thelubI) 1); |
|
83 by (etac (monofun_Ispair1 RS ch2ch_monofun) 1); |
|
84 by (rtac trans 1); |
|
85 by (rtac (thelub_sprod RS sym) 2); |
|
86 by (rtac ch2ch_fun 2); |
|
87 by (etac (monofun_Ispair1 RS ch2ch_monofun) 2); |
|
88 by (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1); |
|
89 by (res_inst_tac [("Q","lub(range(Y))=UU")] (excluded_middle RS disjE) 1); |
|
90 by (etac sprod3_lemma1 1); |
|
91 by (atac 1); |
|
92 by (atac 1); |
|
93 by (etac sprod3_lemma2 1); |
|
94 by (atac 1); |
|
95 by (atac 1); |
|
96 by (etac sprod3_lemma3 1); |
|
97 by (atac 1); |
|
98 qed "contlub_Ispair1"; |
|
99 |
|
100 Goal |
|
101 "[| chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==>\ |
|
102 \ Ispair x (lub(range Y)) =\ |
|
103 \ Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\ |
|
104 \ (lub(range(%i. Issnd (Ispair x (Y i)))))"; |
|
105 by (res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1); |
|
106 by (rtac sym 1); |
|
107 by (dtac chain_UU_I_inverse2 1); |
|
108 by (etac exE 1); |
|
109 by (rtac lub_chain_maxelem 1); |
|
110 by (etac Isfst2 1); |
|
111 by (rtac allI 1); |
|
112 by (rename_tac "j" 1); |
|
113 by (case_tac "Y(j)=UU" 1); |
|
114 by Auto_tac; |
|
115 qed "sprod3_lemma4"; |
|
116 |
|
117 Goal |
|
118 "[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\ |
|
119 \ Ispair x (lub(range Y)) =\ |
|
120 \ Ispair (lub(range(%i. Isfst(Ispair x (Y i)))))\ |
|
121 \ (lub(range(%i. Issnd(Ispair x (Y i)))))"; |
|
122 by (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1); |
|
123 by (atac 1); |
|
124 by (rtac trans 1); |
|
125 by (rtac strict_Ispair2 1); |
|
126 by (rtac (strict_Ispair RS sym) 1); |
|
127 by (rtac disjI2 1); |
|
128 by (rtac chain_UU_I_inverse 1); |
|
129 by (rtac allI 1); |
|
130 by (asm_simp_tac Sprod0_ss 1); |
|
131 by (etac (chain_UU_I RS spec) 1); |
|
132 by (atac 1); |
|
133 qed "sprod3_lemma5"; |
|
134 |
|
135 Goal |
|
136 "[| chain(Y); x = UU |] ==>\ |
|
137 \ Ispair x (lub(range Y)) =\ |
|
138 \ Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\ |
|
139 \ (lub(range(%i. Issnd (Ispair x (Y i)))))"; |
|
140 by (res_inst_tac [("s","UU"),("t","x")] ssubst 1); |
|
141 by (atac 1); |
|
142 by (rtac trans 1); |
|
143 by (rtac strict_Ispair1 1); |
|
144 by (rtac (strict_Ispair RS sym) 1); |
|
145 by (rtac disjI1 1); |
|
146 by (rtac chain_UU_I_inverse 1); |
|
147 by (rtac allI 1); |
|
148 by (simp_tac Sprod0_ss 1); |
|
149 qed "sprod3_lemma6"; |
|
150 |
|
151 Goal "contlub(Ispair(x))"; |
|
152 by (rtac contlubI 1); |
|
153 by (strip_tac 1); |
|
154 by (rtac trans 1); |
|
155 by (rtac (thelub_sprod RS sym) 2); |
|
156 by (etac (monofun_Ispair2 RS ch2ch_monofun) 2); |
|
157 by (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1); |
|
158 by (res_inst_tac [("Q","lub(range(Y))=UU")] (excluded_middle RS disjE) 1); |
|
159 by (etac sprod3_lemma4 1); |
|
160 by (atac 1); |
|
161 by (atac 1); |
|
162 by (etac sprod3_lemma5 1); |
|
163 by (atac 1); |
|
164 by (atac 1); |
|
165 by (etac sprod3_lemma6 1); |
|
166 by (atac 1); |
|
167 qed "contlub_Ispair2"; |
|
168 |
|
169 Goal "cont(Ispair)"; |
|
170 by (rtac monocontlub2cont 1); |
|
171 by (rtac monofun_Ispair1 1); |
|
172 by (rtac contlub_Ispair1 1); |
|
173 qed "cont_Ispair1"; |
|
174 |
|
175 |
|
176 Goal "cont(Ispair(x))"; |
|
177 by (rtac monocontlub2cont 1); |
|
178 by (rtac monofun_Ispair2 1); |
|
179 by (rtac contlub_Ispair2 1); |
|
180 qed "cont_Ispair2"; |
|
181 |
|
182 Goal "contlub(Isfst)"; |
|
183 by (rtac contlubI 1); |
|
184 by (strip_tac 1); |
|
185 by (stac (lub_sprod RS thelubI) 1); |
|
186 by (atac 1); |
|
187 by (res_inst_tac [("Q","lub(range(%i. Issnd(Y(i))))=UU")] (excluded_middle RS disjE) 1); |
|
188 by (asm_simp_tac Sprod0_ss 1); |
|
189 by (res_inst_tac [("s","UU"),("t","lub(range(%i. Issnd(Y(i))))")] ssubst 1); |
|
190 by (atac 1); |
|
191 by (rtac trans 1); |
|
192 by (asm_simp_tac Sprod0_ss 1); |
|
193 by (rtac sym 1); |
|
194 by (rtac chain_UU_I_inverse 1); |
|
195 by (rtac allI 1); |
|
196 by (rtac strict_Isfst 1); |
|
197 by (rtac contrapos_np 1); |
|
198 by (etac (defined_IsfstIssnd RS conjunct2) 2); |
|
199 by (fast_tac (HOL_cs addSDs [monofun_Issnd RS ch2ch_monofun RS chain_UU_I RS spec]) 1); |
|
200 qed "contlub_Isfst"; |
|
201 |
|
202 Goal "contlub(Issnd)"; |
|
203 by (rtac contlubI 1); |
|
204 by (strip_tac 1); |
|
205 by (stac (lub_sprod RS thelubI) 1); |
|
206 by (atac 1); |
|
207 by (res_inst_tac [("Q","lub(range(%i. Isfst(Y(i))))=UU")] (excluded_middle RS disjE) 1); |
|
208 by (asm_simp_tac Sprod0_ss 1); |
|
209 by (res_inst_tac [("s","UU"),("t","lub(range(%i. Isfst(Y(i))))")] ssubst 1); |
|
210 by (atac 1); |
|
211 by (asm_simp_tac Sprod0_ss 1); |
|
212 by (rtac sym 1); |
|
213 by (rtac chain_UU_I_inverse 1); |
|
214 by (rtac allI 1); |
|
215 by (rtac strict_Issnd 1); |
|
216 by (rtac contrapos_np 1); |
|
217 by (etac (defined_IsfstIssnd RS conjunct1) 2); |
|
218 by (fast_tac (HOL_cs addSDs [monofun_Isfst RS ch2ch_monofun RS chain_UU_I RS spec]) 1); |
|
219 qed "contlub_Issnd"; |
|
220 |
|
221 Goal "cont(Isfst)"; |
|
222 by (rtac monocontlub2cont 1); |
|
223 by (rtac monofun_Isfst 1); |
|
224 by (rtac contlub_Isfst 1); |
|
225 qed "cont_Isfst"; |
|
226 |
|
227 Goal "cont(Issnd)"; |
|
228 by (rtac monocontlub2cont 1); |
|
229 by (rtac monofun_Issnd 1); |
|
230 by (rtac contlub_Issnd 1); |
|
231 qed "cont_Issnd"; |
|
232 |
|
233 Goal "[|x1=x2;y1=y2|] ==> (:x1,y1:) = (:x2,y2:)"; |
|
234 by (fast_tac HOL_cs 1); |
|
235 qed "spair_eq"; |
|
236 |
|
237 (* ------------------------------------------------------------------------ *) |
|
238 (* convert all lemmas to the continuous versions *) |
|
239 (* ------------------------------------------------------------------------ *) |
|
240 |
|
241 Goalw [spair_def] |
|
242 "(LAM x y. Ispair x y)$a$b = Ispair a b"; |
|
243 by (stac beta_cfun 1); |
|
244 by (simp_tac (simpset() addsimps [cont_Ispair2, cont_Ispair1, cont2cont_CF1L]) 1); |
|
245 by (stac beta_cfun 1); |
|
246 by (rtac cont_Ispair2 1); |
|
247 by (rtac refl 1); |
|
248 qed "beta_cfun_sprod"; |
|
249 |
|
250 Addsimps [beta_cfun_sprod]; |
|
251 |
|
252 Goalw [spair_def] |
|
253 "[| aa~=UU ; ba~=UU ; (:a,b:)=(:aa,ba:) |] ==> a=aa & b=ba"; |
|
254 by (etac inject_Ispair 1); |
|
255 by (atac 1); |
|
256 by (etac box_equals 1); |
|
257 by (rtac beta_cfun_sprod 1); |
|
258 by (rtac beta_cfun_sprod 1); |
|
259 qed "inject_spair"; |
|
260 |
|
261 Goalw [spair_def] "UU = (:UU,UU:)"; |
|
262 by (rtac sym 1); |
|
263 by (rtac trans 1); |
|
264 by (rtac beta_cfun_sprod 1); |
|
265 by (rtac sym 1); |
|
266 by (rtac inst_sprod_pcpo 1); |
|
267 qed "inst_sprod_pcpo2"; |
|
268 |
|
269 Goalw [spair_def] |
|
270 "(a=UU | b=UU) ==> (:a,b:)=UU"; |
|
271 by (rtac trans 1); |
|
272 by (rtac beta_cfun_sprod 1); |
|
273 by (rtac trans 1); |
|
274 by (rtac (inst_sprod_pcpo RS sym) 2); |
|
275 by (etac strict_Ispair 1); |
|
276 qed "strict_spair"; |
|
277 |
|
278 Goalw [spair_def] "(:UU,b:) = UU"; |
|
279 by (stac beta_cfun_sprod 1); |
|
280 by (rtac trans 1); |
|
281 by (rtac (inst_sprod_pcpo RS sym) 2); |
|
282 by (rtac strict_Ispair1 1); |
|
283 qed "strict_spair1"; |
|
284 |
|
285 Goalw [spair_def] "(:a,UU:) = UU"; |
|
286 by (stac beta_cfun_sprod 1); |
|
287 by (rtac trans 1); |
|
288 by (rtac (inst_sprod_pcpo RS sym) 2); |
|
289 by (rtac strict_Ispair2 1); |
|
290 qed "strict_spair2"; |
|
291 |
|
292 Addsimps [strict_spair1,strict_spair2]; |
|
293 |
|
294 Goalw [spair_def] "(:x,y:)~=UU ==> ~x=UU & ~y=UU"; |
|
295 by (rtac strict_Ispair_rev 1); |
|
296 by Auto_tac; |
|
297 qed "strict_spair_rev"; |
|
298 |
|
299 Goalw [spair_def] "(:a,b:) = UU ==> (a = UU | b = UU)"; |
|
300 by (rtac defined_Ispair_rev 1); |
|
301 by Auto_tac; |
|
302 qed "defined_spair_rev"; |
|
303 |
|
304 Goalw [spair_def] |
|
305 "[|a~=UU; b~=UU|] ==> (:a,b:) ~= UU"; |
|
306 by (stac beta_cfun_sprod 1); |
|
307 by (stac inst_sprod_pcpo 1); |
|
308 by (etac defined_Ispair 1); |
|
309 by (atac 1); |
|
310 qed "defined_spair"; |
|
311 |
|
312 Goalw [spair_def] |
|
313 "z=UU | (? a b. z=(:a,b:) & a~=UU & b~=UU)"; |
|
314 by (rtac (Exh_Sprod RS disjE) 1); |
|
315 by (rtac disjI1 1); |
|
316 by (stac inst_sprod_pcpo 1); |
|
317 by (atac 1); |
|
318 by (rtac disjI2 1); |
|
319 by (etac exE 1); |
|
320 by (etac exE 1); |
|
321 by (rtac exI 1); |
|
322 by (rtac exI 1); |
|
323 by (rtac conjI 1); |
|
324 by (stac beta_cfun_sprod 1); |
|
325 by (fast_tac HOL_cs 1); |
|
326 by (fast_tac HOL_cs 1); |
|
327 qed "Exh_Sprod2"; |
|
328 |
|
329 |
|
330 val [prem1,prem2] = Goalw [spair_def] |
|
331 "[|p=UU ==> Q; !!x y. [| p=(:x,y:); x~=UU; y~=UU|] ==> Q|] ==> Q"; |
|
332 by (rtac IsprodE 1); |
|
333 by (rtac prem1 1); |
|
334 by (stac inst_sprod_pcpo 1); |
|
335 by (atac 1); |
|
336 by (rtac prem2 1); |
|
337 by (atac 2); |
|
338 by (atac 2); |
|
339 by (stac beta_cfun_sprod 1); |
|
340 by (atac 1); |
|
341 qed "sprodE"; |
|
342 |
|
343 |
|
344 Goalw [sfst_def] |
|
345 "p=UU==>sfst$p=UU"; |
|
346 by (stac beta_cfun 1); |
|
347 by (rtac cont_Isfst 1); |
|
348 by (rtac strict_Isfst 1); |
|
349 by (rtac (inst_sprod_pcpo RS subst) 1); |
|
350 by (atac 1); |
|
351 qed "strict_sfst"; |
|
352 |
|
353 Goalw [sfst_def,spair_def] |
|
354 "sfst$(:UU,y:) = UU"; |
|
355 by (stac beta_cfun_sprod 1); |
|
356 by (stac beta_cfun 1); |
|
357 by (rtac cont_Isfst 1); |
|
358 by (rtac strict_Isfst1 1); |
|
359 qed "strict_sfst1"; |
|
360 |
|
361 Goalw [sfst_def,spair_def] |
|
362 "sfst$(:x,UU:) = UU"; |
|
363 by (stac beta_cfun_sprod 1); |
|
364 by (stac beta_cfun 1); |
|
365 by (rtac cont_Isfst 1); |
|
366 by (rtac strict_Isfst2 1); |
|
367 qed "strict_sfst2"; |
|
368 |
|
369 Goalw [ssnd_def] |
|
370 "p=UU==>ssnd$p=UU"; |
|
371 by (stac beta_cfun 1); |
|
372 by (rtac cont_Issnd 1); |
|
373 by (rtac strict_Issnd 1); |
|
374 by (rtac (inst_sprod_pcpo RS subst) 1); |
|
375 by (atac 1); |
|
376 qed "strict_ssnd"; |
|
377 |
|
378 Goalw [ssnd_def,spair_def] |
|
379 "ssnd$(:UU,y:) = UU"; |
|
380 by (stac beta_cfun_sprod 1); |
|
381 by (stac beta_cfun 1); |
|
382 by (rtac cont_Issnd 1); |
|
383 by (rtac strict_Issnd1 1); |
|
384 qed "strict_ssnd1"; |
|
385 |
|
386 Goalw [ssnd_def,spair_def] |
|
387 "ssnd$(:x,UU:) = UU"; |
|
388 by (stac beta_cfun_sprod 1); |
|
389 by (stac beta_cfun 1); |
|
390 by (rtac cont_Issnd 1); |
|
391 by (rtac strict_Issnd2 1); |
|
392 qed "strict_ssnd2"; |
|
393 |
|
394 Goalw [sfst_def,spair_def] |
|
395 "y~=UU ==>sfst$(:x,y:)=x"; |
|
396 by (stac beta_cfun_sprod 1); |
|
397 by (stac beta_cfun 1); |
|
398 by (rtac cont_Isfst 1); |
|
399 by (etac Isfst2 1); |
|
400 qed "sfst2"; |
|
401 |
|
402 Goalw [ssnd_def,spair_def] |
|
403 "x~=UU ==>ssnd$(:x,y:)=y"; |
|
404 by (stac beta_cfun_sprod 1); |
|
405 by (stac beta_cfun 1); |
|
406 by (rtac cont_Issnd 1); |
|
407 by (etac Issnd2 1); |
|
408 qed "ssnd2"; |
|
409 |
|
410 |
|
411 Goalw [sfst_def,ssnd_def,spair_def] |
|
412 "p~=UU ==> sfst$p ~=UU & ssnd$p ~=UU"; |
|
413 by (stac beta_cfun 1); |
|
414 by (rtac cont_Issnd 1); |
|
415 by (stac beta_cfun 1); |
|
416 by (rtac cont_Isfst 1); |
|
417 by (rtac defined_IsfstIssnd 1); |
|
418 by (rtac (inst_sprod_pcpo RS subst) 1); |
|
419 by (atac 1); |
|
420 qed "defined_sfstssnd"; |
|
421 |
|
422 Goalw [sfst_def,ssnd_def,spair_def] "(:sfst$p , ssnd$p:) = p"; |
|
423 by (stac beta_cfun_sprod 1); |
|
424 by (stac beta_cfun 1); |
|
425 by (rtac cont_Issnd 1); |
|
426 by (stac beta_cfun 1); |
|
427 by (rtac cont_Isfst 1); |
|
428 by (rtac (surjective_pairing_Sprod RS sym) 1); |
|
429 qed "surjective_pairing_Sprod2"; |
|
430 |
|
431 Goalw [sfst_def,ssnd_def,spair_def] |
|
432 "chain(S) ==> range(S) <<| \ |
|
433 \ (: lub(range(%i. sfst$(S i))), lub(range(%i. ssnd$(S i))) :)"; |
|
434 by (stac beta_cfun_sprod 1); |
|
435 by (stac (beta_cfun RS ext) 1); |
|
436 by (rtac cont_Issnd 1); |
|
437 by (stac (beta_cfun RS ext) 1); |
|
438 by (rtac cont_Isfst 1); |
|
439 by (etac lub_sprod 1); |
|
440 qed "lub_sprod2"; |
|
441 |
|
442 |
|
443 bind_thm ("thelub_sprod2", lub_sprod2 RS thelubI); |
|
444 (* |
|
445 "chain ?S1 ==> |
|
446 lub (range ?S1) = |
|
447 (:lub (range (%i. sfst$(?S1 i))), lub (range (%i. ssnd$(?S1 i))):)" : thm |
|
448 *) |
|
449 |
|
450 Goalw [ssplit_def] |
|
451 "ssplit$f$UU=UU"; |
|
452 by (stac beta_cfun 1); |
|
453 by (Simp_tac 1); |
|
454 by (stac strictify1 1); |
|
455 by (rtac refl 1); |
|
456 qed "ssplit1"; |
|
457 |
|
458 Goalw [ssplit_def] |
|
459 "[|x~=UU;y~=UU|] ==> ssplit$f$(:x,y:)= f$x$y"; |
|
460 by (stac beta_cfun 1); |
|
461 by (Simp_tac 1); |
|
462 by (stac strictify2 1); |
|
463 by (rtac defined_spair 1); |
|
464 by (assume_tac 1); |
|
465 by (assume_tac 1); |
|
466 by (stac beta_cfun 1); |
|
467 by (Simp_tac 1); |
|
468 by (stac sfst2 1); |
|
469 by (assume_tac 1); |
|
470 by (stac ssnd2 1); |
|
471 by (assume_tac 1); |
|
472 by (rtac refl 1); |
|
473 qed "ssplit2"; |
|
474 |
|
475 |
|
476 Goalw [ssplit_def] |
|
477 "ssplit$spair$z=z"; |
|
478 by (stac beta_cfun 1); |
|
479 by (Simp_tac 1); |
|
480 by (case_tac "z=UU" 1); |
|
481 by (hyp_subst_tac 1); |
|
482 by (rtac strictify1 1); |
|
483 by (rtac trans 1); |
|
484 by (rtac strictify2 1); |
|
485 by (atac 1); |
|
486 by (stac beta_cfun 1); |
|
487 by (Simp_tac 1); |
|
488 by (rtac surjective_pairing_Sprod2 1); |
|
489 qed "ssplit3"; |
|
490 |
|
491 (* ------------------------------------------------------------------------ *) |
|
492 (* install simplifier for Sprod *) |
|
493 (* ------------------------------------------------------------------------ *) |
|
494 |
|
495 val Sprod_rews = [strict_sfst1,strict_sfst2, |
|
496 strict_ssnd1,strict_ssnd2,sfst2,ssnd2,defined_spair, |
|
497 ssplit1,ssplit2]; |
|
498 Addsimps Sprod_rews; |
|
499 |
|