|
1 (* Title: HOLCF/ssum3.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for ssum3.thy |
|
7 *) |
|
8 |
|
9 open Ssum3; |
|
10 |
|
11 (* ------------------------------------------------------------------------ *) |
|
12 (* continuity for Isinl and Isinr *) |
|
13 (* ------------------------------------------------------------------------ *) |
|
14 |
|
15 |
|
16 val contlub_Isinl = prove_goal Ssum3.thy "contlub(Isinl)" |
|
17 (fn prems => |
|
18 [ |
|
19 (rtac contlubI 1), |
|
20 (strip_tac 1), |
|
21 (rtac trans 1), |
|
22 (rtac (thelub_ssum1a RS sym) 2), |
|
23 (rtac allI 3), |
|
24 (rtac exI 3), |
|
25 (rtac refl 3), |
|
26 (etac (monofun_Isinl RS ch2ch_monofun) 2), |
|
27 (res_inst_tac [("Q","lub(range(Y))=UU")] classical2 1), |
|
28 (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1), |
|
29 (atac 1), |
|
30 (res_inst_tac [("f","Isinl")] arg_cong 1), |
|
31 (rtac (chain_UU_I_inverse RS sym) 1), |
|
32 (rtac allI 1), |
|
33 (res_inst_tac [("s","UU"),("t","Y(i)")] ssubst 1), |
|
34 (etac (chain_UU_I RS spec ) 1), |
|
35 (atac 1), |
|
36 (rtac Iwhen1 1), |
|
37 (res_inst_tac [("f","Isinl")] arg_cong 1), |
|
38 (rtac lub_equal 1), |
|
39 (atac 1), |
|
40 (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
|
41 (etac (monofun_Isinl RS ch2ch_monofun) 1), |
|
42 (rtac allI 1), |
|
43 (res_inst_tac [("Q","Y(k)=UU")] classical2 1), |
|
44 (asm_simp_tac Ssum_ss 1), |
|
45 (asm_simp_tac Ssum_ss 1) |
|
46 ]); |
|
47 |
|
48 val contlub_Isinr = prove_goal Ssum3.thy "contlub(Isinr)" |
|
49 (fn prems => |
|
50 [ |
|
51 (rtac contlubI 1), |
|
52 (strip_tac 1), |
|
53 (rtac trans 1), |
|
54 (rtac (thelub_ssum1b RS sym) 2), |
|
55 (rtac allI 3), |
|
56 (rtac exI 3), |
|
57 (rtac refl 3), |
|
58 (etac (monofun_Isinr RS ch2ch_monofun) 2), |
|
59 (res_inst_tac [("Q","lub(range(Y))=UU")] classical2 1), |
|
60 (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1), |
|
61 (atac 1), |
|
62 ((rtac arg_cong 1) THEN (rtac (chain_UU_I_inverse RS sym) 1)), |
|
63 (rtac allI 1), |
|
64 (res_inst_tac [("s","UU"),("t","Y(i)")] ssubst 1), |
|
65 (etac (chain_UU_I RS spec ) 1), |
|
66 (atac 1), |
|
67 (rtac (strict_IsinlIsinr RS subst) 1), |
|
68 (rtac Iwhen1 1), |
|
69 ((rtac arg_cong 1) THEN (rtac lub_equal 1)), |
|
70 (atac 1), |
|
71 (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
|
72 (etac (monofun_Isinr RS ch2ch_monofun) 1), |
|
73 (rtac allI 1), |
|
74 (res_inst_tac [("Q","Y(k)=UU")] classical2 1), |
|
75 (asm_simp_tac Ssum_ss 1), |
|
76 (asm_simp_tac Ssum_ss 1) |
|
77 ]); |
|
78 |
|
79 val contX_Isinl = prove_goal Ssum3.thy "contX(Isinl)" |
|
80 (fn prems => |
|
81 [ |
|
82 (rtac monocontlub2contX 1), |
|
83 (rtac monofun_Isinl 1), |
|
84 (rtac contlub_Isinl 1) |
|
85 ]); |
|
86 |
|
87 val contX_Isinr = prove_goal Ssum3.thy "contX(Isinr)" |
|
88 (fn prems => |
|
89 [ |
|
90 (rtac monocontlub2contX 1), |
|
91 (rtac monofun_Isinr 1), |
|
92 (rtac contlub_Isinr 1) |
|
93 ]); |
|
94 |
|
95 |
|
96 (* ------------------------------------------------------------------------ *) |
|
97 (* continuity for Iwhen in the firts two arguments *) |
|
98 (* ------------------------------------------------------------------------ *) |
|
99 |
|
100 val contlub_Iwhen1 = prove_goal Ssum3.thy "contlub(Iwhen)" |
|
101 (fn prems => |
|
102 [ |
|
103 (rtac contlubI 1), |
|
104 (strip_tac 1), |
|
105 (rtac trans 1), |
|
106 (rtac (thelub_fun RS sym) 2), |
|
107 (etac (monofun_Iwhen1 RS ch2ch_monofun) 2), |
|
108 (rtac (expand_fun_eq RS iffD2) 1), |
|
109 (strip_tac 1), |
|
110 (rtac trans 1), |
|
111 (rtac (thelub_fun RS sym) 2), |
|
112 (rtac ch2ch_fun 2), |
|
113 (etac (monofun_Iwhen1 RS ch2ch_monofun) 2), |
|
114 (rtac (expand_fun_eq RS iffD2) 1), |
|
115 (strip_tac 1), |
|
116 (res_inst_tac [("p","xa")] IssumE 1), |
|
117 (asm_simp_tac Ssum_ss 1), |
|
118 (rtac (lub_const RS thelubI RS sym) 1), |
|
119 (asm_simp_tac Ssum_ss 1), |
|
120 (etac contlub_cfun_fun 1), |
|
121 (asm_simp_tac Ssum_ss 1), |
|
122 (rtac (lub_const RS thelubI RS sym) 1) |
|
123 ]); |
|
124 |
|
125 val contlub_Iwhen2 = prove_goal Ssum3.thy "contlub(Iwhen(f))" |
|
126 (fn prems => |
|
127 [ |
|
128 (rtac contlubI 1), |
|
129 (strip_tac 1), |
|
130 (rtac trans 1), |
|
131 (rtac (thelub_fun RS sym) 2), |
|
132 (etac (monofun_Iwhen2 RS ch2ch_monofun) 2), |
|
133 (rtac (expand_fun_eq RS iffD2) 1), |
|
134 (strip_tac 1), |
|
135 (res_inst_tac [("p","x")] IssumE 1), |
|
136 (asm_simp_tac Ssum_ss 1), |
|
137 (rtac (lub_const RS thelubI RS sym) 1), |
|
138 (asm_simp_tac Ssum_ss 1), |
|
139 (rtac (lub_const RS thelubI RS sym) 1), |
|
140 (asm_simp_tac Ssum_ss 1), |
|
141 (etac contlub_cfun_fun 1) |
|
142 ]); |
|
143 |
|
144 (* ------------------------------------------------------------------------ *) |
|
145 (* continuity for Iwhen in its third argument *) |
|
146 (* ------------------------------------------------------------------------ *) |
|
147 |
|
148 (* ------------------------------------------------------------------------ *) |
|
149 (* first 5 ugly lemmas *) |
|
150 (* ------------------------------------------------------------------------ *) |
|
151 |
|
152 val ssum_lemma9 = prove_goal Ssum3.thy |
|
153 "[| is_chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x.Y(i)=Isinl(x)" |
|
154 (fn prems => |
|
155 [ |
|
156 (cut_facts_tac prems 1), |
|
157 (strip_tac 1), |
|
158 (res_inst_tac [("p","Y(i)")] IssumE 1), |
|
159 (etac exI 1), |
|
160 (etac exI 1), |
|
161 (res_inst_tac [("P","y=UU")] notE 1), |
|
162 (atac 1), |
|
163 (rtac (less_ssum3d RS iffD1) 1), |
|
164 (etac subst 1), |
|
165 (etac subst 1), |
|
166 (etac is_ub_thelub 1) |
|
167 ]); |
|
168 |
|
169 |
|
170 val ssum_lemma10 = prove_goal Ssum3.thy |
|
171 "[| is_chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x.Y(i)=Isinr(x)" |
|
172 (fn prems => |
|
173 [ |
|
174 (cut_facts_tac prems 1), |
|
175 (strip_tac 1), |
|
176 (res_inst_tac [("p","Y(i)")] IssumE 1), |
|
177 (rtac exI 1), |
|
178 (etac trans 1), |
|
179 (rtac strict_IsinlIsinr 1), |
|
180 (etac exI 2), |
|
181 (res_inst_tac [("P","xa=UU")] notE 1), |
|
182 (atac 1), |
|
183 (rtac (less_ssum3c RS iffD1) 1), |
|
184 (etac subst 1), |
|
185 (etac subst 1), |
|
186 (etac is_ub_thelub 1) |
|
187 ]); |
|
188 |
|
189 val ssum_lemma11 = prove_goal Ssum3.thy |
|
190 "[| is_chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\ |
|
191 \ Iwhen(f,g,lub(range(Y))) = lub(range(%i. Iwhen(f,g,Y(i))))" |
|
192 (fn prems => |
|
193 [ |
|
194 (cut_facts_tac prems 1), |
|
195 (asm_simp_tac Ssum_ss 1), |
|
196 (rtac (chain_UU_I_inverse RS sym) 1), |
|
197 (rtac allI 1), |
|
198 (res_inst_tac [("s","Isinl(UU)"),("t","Y(i)")] subst 1), |
|
199 (rtac (inst_ssum_pcpo RS subst) 1), |
|
200 (rtac (chain_UU_I RS spec RS sym) 1), |
|
201 (atac 1), |
|
202 (etac (inst_ssum_pcpo RS ssubst) 1), |
|
203 (asm_simp_tac Ssum_ss 1) |
|
204 ]); |
|
205 |
|
206 val ssum_lemma12 = prove_goal Ssum3.thy |
|
207 "[| is_chain(Y); lub(range(Y)) = Isinl(x); ~ x = UU |] ==>\ |
|
208 \ Iwhen(f,g,lub(range(Y))) = lub(range(%i. Iwhen(f,g,Y(i))))" |
|
209 (fn prems => |
|
210 [ |
|
211 (cut_facts_tac prems 1), |
|
212 (asm_simp_tac Ssum_ss 1), |
|
213 (res_inst_tac [("t","x")] subst 1), |
|
214 (rtac inject_Isinl 1), |
|
215 (rtac trans 1), |
|
216 (atac 2), |
|
217 (rtac (thelub_ssum1a RS sym) 1), |
|
218 (atac 1), |
|
219 (etac ssum_lemma9 1), |
|
220 (atac 1), |
|
221 (rtac trans 1), |
|
222 (rtac contlub_cfun_arg 1), |
|
223 (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
|
224 (atac 1), |
|
225 (rtac lub_equal2 1), |
|
226 (rtac (chain_mono2 RS exE) 1), |
|
227 (atac 2), |
|
228 (rtac chain_UU_I_inverse2 1), |
|
229 (rtac (inst_ssum_pcpo RS ssubst) 1), |
|
230 (etac swap 1), |
|
231 (rtac inject_Isinl 1), |
|
232 (rtac trans 1), |
|
233 (etac sym 1), |
|
234 (etac notnotD 1), |
|
235 (rtac exI 1), |
|
236 (strip_tac 1), |
|
237 (rtac (ssum_lemma9 RS spec RS exE) 1), |
|
238 (atac 1), |
|
239 (atac 1), |
|
240 (res_inst_tac [("t","Y(i)")] ssubst 1), |
|
241 (atac 1), |
|
242 (rtac trans 1), |
|
243 (rtac cfun_arg_cong 1), |
|
244 (rtac Iwhen2 1), |
|
245 (res_inst_tac [("P","Y(i)=UU")] swap 1), |
|
246 (fast_tac HOL_cs 1), |
|
247 (rtac (inst_ssum_pcpo RS ssubst) 1), |
|
248 (res_inst_tac [("t","Y(i)")] ssubst 1), |
|
249 (atac 1), |
|
250 (fast_tac HOL_cs 1), |
|
251 (rtac (Iwhen2 RS ssubst) 1), |
|
252 (res_inst_tac [("P","Y(i)=UU")] swap 1), |
|
253 (fast_tac HOL_cs 1), |
|
254 (rtac (inst_ssum_pcpo RS ssubst) 1), |
|
255 (res_inst_tac [("t","Y(i)")] ssubst 1), |
|
256 (atac 1), |
|
257 (fast_tac HOL_cs 1), |
|
258 (simp_tac Cfun_ss 1), |
|
259 (rtac (monofun_fapp2 RS ch2ch_monofun) 1), |
|
260 (etac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
|
261 (etac (monofun_Iwhen3 RS ch2ch_monofun) 1) |
|
262 ]); |
|
263 |
|
264 |
|
265 val ssum_lemma13 = prove_goal Ssum3.thy |
|
266 "[| is_chain(Y); lub(range(Y)) = Isinr(x); ~ x = UU |] ==>\ |
|
267 \ Iwhen(f,g,lub(range(Y))) = lub(range(%i. Iwhen(f,g,Y(i))))" |
|
268 (fn prems => |
|
269 [ |
|
270 (cut_facts_tac prems 1), |
|
271 (asm_simp_tac Ssum_ss 1), |
|
272 (res_inst_tac [("t","x")] subst 1), |
|
273 (rtac inject_Isinr 1), |
|
274 (rtac trans 1), |
|
275 (atac 2), |
|
276 (rtac (thelub_ssum1b RS sym) 1), |
|
277 (atac 1), |
|
278 (etac ssum_lemma10 1), |
|
279 (atac 1), |
|
280 (rtac trans 1), |
|
281 (rtac contlub_cfun_arg 1), |
|
282 (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
|
283 (atac 1), |
|
284 (rtac lub_equal2 1), |
|
285 (rtac (chain_mono2 RS exE) 1), |
|
286 (atac 2), |
|
287 (rtac chain_UU_I_inverse2 1), |
|
288 (rtac (inst_ssum_pcpo RS ssubst) 1), |
|
289 (etac swap 1), |
|
290 (rtac inject_Isinr 1), |
|
291 (rtac trans 1), |
|
292 (etac sym 1), |
|
293 (rtac (strict_IsinlIsinr RS subst) 1), |
|
294 (etac notnotD 1), |
|
295 (rtac exI 1), |
|
296 (strip_tac 1), |
|
297 (rtac (ssum_lemma10 RS spec RS exE) 1), |
|
298 (atac 1), |
|
299 (atac 1), |
|
300 (res_inst_tac [("t","Y(i)")] ssubst 1), |
|
301 (atac 1), |
|
302 (rtac trans 1), |
|
303 (rtac cfun_arg_cong 1), |
|
304 (rtac Iwhen3 1), |
|
305 (res_inst_tac [("P","Y(i)=UU")] swap 1), |
|
306 (fast_tac HOL_cs 1), |
|
307 (dtac notnotD 1), |
|
308 (rtac (inst_ssum_pcpo RS ssubst) 1), |
|
309 (rtac (strict_IsinlIsinr RS ssubst) 1), |
|
310 (res_inst_tac [("t","Y(i)")] ssubst 1), |
|
311 (atac 1), |
|
312 (fast_tac HOL_cs 1), |
|
313 (rtac (Iwhen3 RS ssubst) 1), |
|
314 (res_inst_tac [("P","Y(i)=UU")] swap 1), |
|
315 (fast_tac HOL_cs 1), |
|
316 (dtac notnotD 1), |
|
317 (rtac (inst_ssum_pcpo RS ssubst) 1), |
|
318 (rtac (strict_IsinlIsinr RS ssubst) 1), |
|
319 (res_inst_tac [("t","Y(i)")] ssubst 1), |
|
320 (atac 1), |
|
321 (fast_tac HOL_cs 1), |
|
322 (simp_tac Cfun_ss 1), |
|
323 (rtac (monofun_fapp2 RS ch2ch_monofun) 1), |
|
324 (etac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
|
325 (etac (monofun_Iwhen3 RS ch2ch_monofun) 1) |
|
326 ]); |
|
327 |
|
328 |
|
329 val contlub_Iwhen3 = prove_goal Ssum3.thy "contlub(Iwhen(f)(g))" |
|
330 (fn prems => |
|
331 [ |
|
332 (rtac contlubI 1), |
|
333 (strip_tac 1), |
|
334 (res_inst_tac [("p","lub(range(Y))")] IssumE 1), |
|
335 (etac ssum_lemma11 1), |
|
336 (atac 1), |
|
337 (etac ssum_lemma12 1), |
|
338 (atac 1), |
|
339 (atac 1), |
|
340 (etac ssum_lemma13 1), |
|
341 (atac 1), |
|
342 (atac 1) |
|
343 ]); |
|
344 |
|
345 val contX_Iwhen1 = prove_goal Ssum3.thy "contX(Iwhen)" |
|
346 (fn prems => |
|
347 [ |
|
348 (rtac monocontlub2contX 1), |
|
349 (rtac monofun_Iwhen1 1), |
|
350 (rtac contlub_Iwhen1 1) |
|
351 ]); |
|
352 |
|
353 val contX_Iwhen2 = prove_goal Ssum3.thy "contX(Iwhen(f))" |
|
354 (fn prems => |
|
355 [ |
|
356 (rtac monocontlub2contX 1), |
|
357 (rtac monofun_Iwhen2 1), |
|
358 (rtac contlub_Iwhen2 1) |
|
359 ]); |
|
360 |
|
361 val contX_Iwhen3 = prove_goal Ssum3.thy "contX(Iwhen(f)(g))" |
|
362 (fn prems => |
|
363 [ |
|
364 (rtac monocontlub2contX 1), |
|
365 (rtac monofun_Iwhen3 1), |
|
366 (rtac contlub_Iwhen3 1) |
|
367 ]); |
|
368 |
|
369 (* ------------------------------------------------------------------------ *) |
|
370 (* continuous versions of lemmas for 'a ++ 'b *) |
|
371 (* ------------------------------------------------------------------------ *) |
|
372 |
|
373 val strict_sinl = prove_goalw Ssum3.thy [sinl_def] "sinl[UU]=UU" |
|
374 (fn prems => |
|
375 [ |
|
376 (simp_tac (Ssum_ss addsimps [contX_Isinl]) 1), |
|
377 (rtac (inst_ssum_pcpo RS sym) 1) |
|
378 ]); |
|
379 |
|
380 val strict_sinr = prove_goalw Ssum3.thy [sinr_def] "sinr[UU]=UU" |
|
381 (fn prems => |
|
382 [ |
|
383 (simp_tac (Ssum_ss addsimps [contX_Isinr]) 1), |
|
384 (rtac (inst_ssum_pcpo RS sym) 1) |
|
385 ]); |
|
386 |
|
387 val noteq_sinlsinr = prove_goalw Ssum3.thy [sinl_def,sinr_def] |
|
388 "sinl[a]=sinr[b] ==> a=UU & b=UU" |
|
389 (fn prems => |
|
390 [ |
|
391 (cut_facts_tac prems 1), |
|
392 (rtac noteq_IsinlIsinr 1), |
|
393 (etac box_equals 1), |
|
394 (asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1), |
|
395 (asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1) |
|
396 ]); |
|
397 |
|
398 val inject_sinl = prove_goalw Ssum3.thy [sinl_def,sinr_def] |
|
399 "sinl[a1]=sinl[a2]==> a1=a2" |
|
400 (fn prems => |
|
401 [ |
|
402 (cut_facts_tac prems 1), |
|
403 (rtac inject_Isinl 1), |
|
404 (etac box_equals 1), |
|
405 (asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1), |
|
406 (asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1) |
|
407 ]); |
|
408 |
|
409 val inject_sinr = prove_goalw Ssum3.thy [sinl_def,sinr_def] |
|
410 "sinr[a1]=sinr[a2]==> a1=a2" |
|
411 (fn prems => |
|
412 [ |
|
413 (cut_facts_tac prems 1), |
|
414 (rtac inject_Isinr 1), |
|
415 (etac box_equals 1), |
|
416 (asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1), |
|
417 (asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1) |
|
418 ]); |
|
419 |
|
420 |
|
421 val defined_sinl = prove_goal Ssum3.thy |
|
422 "~x=UU ==> ~sinl[x]=UU" |
|
423 (fn prems => |
|
424 [ |
|
425 (cut_facts_tac prems 1), |
|
426 (etac swap 1), |
|
427 (rtac inject_sinl 1), |
|
428 (rtac (strict_sinl RS ssubst) 1), |
|
429 (etac notnotD 1) |
|
430 ]); |
|
431 |
|
432 val defined_sinr = prove_goal Ssum3.thy |
|
433 "~x=UU ==> ~sinr[x]=UU" |
|
434 (fn prems => |
|
435 [ |
|
436 (cut_facts_tac prems 1), |
|
437 (etac swap 1), |
|
438 (rtac inject_sinr 1), |
|
439 (rtac (strict_sinr RS ssubst) 1), |
|
440 (etac notnotD 1) |
|
441 ]); |
|
442 |
|
443 val Exh_Ssum1 = prove_goalw Ssum3.thy [sinl_def,sinr_def] |
|
444 "z=UU | (? a. z=sinl[a] & ~a=UU) | (? b. z=sinr[b] & ~b=UU)" |
|
445 (fn prems => |
|
446 [ |
|
447 (asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1), |
|
448 (rtac (inst_ssum_pcpo RS ssubst) 1), |
|
449 (rtac Exh_Ssum 1) |
|
450 ]); |
|
451 |
|
452 |
|
453 val ssumE = prove_goalw Ssum3.thy [sinl_def,sinr_def] |
|
454 "[|p=UU ==> Q ;\ |
|
455 \ !!x.[|p=sinl[x]; ~x=UU |] ==> Q;\ |
|
456 \ !!y.[|p=sinr[y]; ~y=UU |] ==> Q|] ==> Q" |
|
457 (fn prems => |
|
458 [ |
|
459 (rtac IssumE 1), |
|
460 (resolve_tac prems 1), |
|
461 (rtac (inst_ssum_pcpo RS ssubst) 1), |
|
462 (atac 1), |
|
463 (resolve_tac prems 1), |
|
464 (atac 2), |
|
465 (asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1), |
|
466 (resolve_tac prems 1), |
|
467 (atac 2), |
|
468 (asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1) |
|
469 ]); |
|
470 |
|
471 |
|
472 val ssumE2 = prove_goalw Ssum3.thy [sinl_def,sinr_def] |
|
473 "[|!!x.[|p=sinl[x]|] ==> Q;\ |
|
474 \ !!y.[|p=sinr[y]|] ==> Q|] ==> Q" |
|
475 (fn prems => |
|
476 [ |
|
477 (rtac IssumE2 1), |
|
478 (resolve_tac prems 1), |
|
479 (rtac (beta_cfun RS ssubst) 1), |
|
480 (rtac contX_Isinl 1), |
|
481 (atac 1), |
|
482 (resolve_tac prems 1), |
|
483 (rtac (beta_cfun RS ssubst) 1), |
|
484 (rtac contX_Isinr 1), |
|
485 (atac 1) |
|
486 ]); |
|
487 |
|
488 val when1 = prove_goalw Ssum3.thy [when_def,sinl_def,sinr_def] |
|
489 "when[f][g][UU] = UU" |
|
490 (fn prems => |
|
491 [ |
|
492 (rtac (inst_ssum_pcpo RS ssubst) 1), |
|
493 (rtac (beta_cfun RS ssubst) 1), |
|
494 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
495 contX_Iwhen3,contX2contX_CF1L]) 1)), |
|
496 (rtac (beta_cfun RS ssubst) 1), |
|
497 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
498 contX_Iwhen3,contX2contX_CF1L]) 1)), |
|
499 (rtac (beta_cfun RS ssubst) 1), |
|
500 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
501 contX_Iwhen3,contX2contX_CF1L]) 1)), |
|
502 (simp_tac Ssum_ss 1) |
|
503 ]); |
|
504 |
|
505 val when2 = prove_goalw Ssum3.thy [when_def,sinl_def,sinr_def] |
|
506 "~x=UU==>when[f][g][sinl[x]] = f[x]" |
|
507 (fn prems => |
|
508 [ |
|
509 (cut_facts_tac prems 1), |
|
510 (rtac (beta_cfun RS ssubst) 1), |
|
511 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
512 contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
513 (rtac (beta_cfun RS ssubst) 1), |
|
514 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
515 contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
516 (rtac (beta_cfun RS ssubst) 1), |
|
517 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
518 contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
519 (rtac (beta_cfun RS ssubst) 1), |
|
520 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
521 contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
522 (asm_simp_tac Ssum_ss 1) |
|
523 ]); |
|
524 |
|
525 |
|
526 |
|
527 val when3 = prove_goalw Ssum3.thy [when_def,sinl_def,sinr_def] |
|
528 "~x=UU==>when[f][g][sinr[x]] = g[x]" |
|
529 (fn prems => |
|
530 [ |
|
531 (cut_facts_tac prems 1), |
|
532 (rtac (beta_cfun RS ssubst) 1), |
|
533 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
534 contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
535 (rtac (beta_cfun RS ssubst) 1), |
|
536 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
537 contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
538 (rtac (beta_cfun RS ssubst) 1), |
|
539 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
540 contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
541 (rtac (beta_cfun RS ssubst) 1), |
|
542 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
543 contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
544 (asm_simp_tac Ssum_ss 1) |
|
545 ]); |
|
546 |
|
547 |
|
548 val less_ssum4a = prove_goalw Ssum3.thy [sinl_def,sinr_def] |
|
549 "(sinl[x] << sinl[y]) = (x << y)" |
|
550 (fn prems => |
|
551 [ |
|
552 (rtac (beta_cfun RS ssubst) 1), |
|
553 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
554 contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
555 (rtac (beta_cfun RS ssubst) 1), |
|
556 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
557 contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
558 (rtac less_ssum3a 1) |
|
559 ]); |
|
560 |
|
561 val less_ssum4b = prove_goalw Ssum3.thy [sinl_def,sinr_def] |
|
562 "(sinr[x] << sinr[y]) = (x << y)" |
|
563 (fn prems => |
|
564 [ |
|
565 (rtac (beta_cfun RS ssubst) 1), |
|
566 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
567 contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
568 (rtac (beta_cfun RS ssubst) 1), |
|
569 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
570 contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
571 (rtac less_ssum3b 1) |
|
572 ]); |
|
573 |
|
574 val less_ssum4c = prove_goalw Ssum3.thy [sinl_def,sinr_def] |
|
575 "(sinl[x] << sinr[y]) = (x = UU)" |
|
576 (fn prems => |
|
577 [ |
|
578 (rtac (beta_cfun RS ssubst) 1), |
|
579 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
580 contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
581 (rtac (beta_cfun RS ssubst) 1), |
|
582 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
583 contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
584 (rtac less_ssum3c 1) |
|
585 ]); |
|
586 |
|
587 val less_ssum4d = prove_goalw Ssum3.thy [sinl_def,sinr_def] |
|
588 "(sinr[x] << sinl[y]) = (x = UU)" |
|
589 (fn prems => |
|
590 [ |
|
591 (rtac (beta_cfun RS ssubst) 1), |
|
592 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
593 contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
594 (rtac (beta_cfun RS ssubst) 1), |
|
595 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
596 contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
597 (rtac less_ssum3d 1) |
|
598 ]); |
|
599 |
|
600 val ssum_chainE = prove_goalw Ssum3.thy [sinl_def,sinr_def] |
|
601 "is_chain(Y) ==> (!i.? x.Y(i)=sinl[x])|(!i.? y.Y(i)=sinr[y])" |
|
602 (fn prems => |
|
603 [ |
|
604 (cut_facts_tac prems 1), |
|
605 (asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1), |
|
606 (etac ssum_lemma4 1) |
|
607 ]); |
|
608 |
|
609 |
|
610 val thelub_ssum2a = prove_goalw Ssum3.thy [sinl_def,sinr_def,when_def] |
|
611 "[| is_chain(Y); !i.? x. Y(i) = sinl[x] |] ==>\ |
|
612 \ lub(range(Y)) = sinl[lub(range(%i. when[LAM x. x][LAM y. UU][Y(i)]))]" |
|
613 (fn prems => |
|
614 [ |
|
615 (cut_facts_tac prems 1), |
|
616 (rtac (beta_cfun RS ssubst) 1), |
|
617 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
618 (rtac (beta_cfun RS ssubst) 1), |
|
619 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
620 (rtac (beta_cfun RS ssubst) 1), |
|
621 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
622 (rtac (beta_cfun RS ext RS ssubst) 1), |
|
623 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
624 (rtac thelub_ssum1a 1), |
|
625 (atac 1), |
|
626 (rtac allI 1), |
|
627 (etac allE 1), |
|
628 (etac exE 1), |
|
629 (rtac exI 1), |
|
630 (etac box_equals 1), |
|
631 (rtac refl 1), |
|
632 (asm_simp_tac (Ssum_ss addsimps [contX_Isinl]) 1) |
|
633 ]); |
|
634 |
|
635 val thelub_ssum2b = prove_goalw Ssum3.thy [sinl_def,sinr_def,when_def] |
|
636 "[| is_chain(Y); !i.? x. Y(i) = sinr[x] |] ==>\ |
|
637 \ lub(range(Y)) = sinr[lub(range(%i. when[LAM y. UU][LAM x. x][Y(i)]))]" |
|
638 (fn prems => |
|
639 [ |
|
640 (cut_facts_tac prems 1), |
|
641 (rtac (beta_cfun RS ssubst) 1), |
|
642 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
643 contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
644 (rtac (beta_cfun RS ssubst) 1), |
|
645 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
646 contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
647 (rtac (beta_cfun RS ssubst) 1), |
|
648 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
649 contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
650 (rtac (beta_cfun RS ext RS ssubst) 1), |
|
651 (REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2, |
|
652 contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)), |
|
653 (rtac thelub_ssum1b 1), |
|
654 (atac 1), |
|
655 (rtac allI 1), |
|
656 (etac allE 1), |
|
657 (etac exE 1), |
|
658 (rtac exI 1), |
|
659 (etac box_equals 1), |
|
660 (rtac refl 1), |
|
661 (asm_simp_tac (Ssum_ss addsimps |
|
662 [contX_Isinr,contX_Isinl,contX_Iwhen1,contX_Iwhen2, |
|
663 contX_Iwhen3]) 1) |
|
664 ]); |
|
665 |
|
666 val thelub_ssum2a_rev = prove_goalw Ssum3.thy [sinl_def,sinr_def] |
|
667 "[| is_chain(Y); lub(range(Y)) = sinl[x]|] ==> !i.? x.Y(i)=sinl[x]" |
|
668 (fn prems => |
|
669 [ |
|
670 (cut_facts_tac prems 1), |
|
671 (asm_simp_tac (Ssum_ss addsimps |
|
672 [contX_Isinr,contX_Isinl,contX_Iwhen1,contX_Iwhen2, |
|
673 contX_Iwhen3]) 1), |
|
674 (etac ssum_lemma9 1), |
|
675 (asm_simp_tac (Ssum_ss addsimps |
|
676 [contX_Isinr,contX_Isinl,contX_Iwhen1,contX_Iwhen2, |
|
677 contX_Iwhen3]) 1) |
|
678 ]); |
|
679 |
|
680 val thelub_ssum2b_rev = prove_goalw Ssum3.thy [sinl_def,sinr_def] |
|
681 "[| is_chain(Y); lub(range(Y)) = sinr[x]|] ==> !i.? x.Y(i)=sinr[x]" |
|
682 (fn prems => |
|
683 [ |
|
684 (cut_facts_tac prems 1), |
|
685 (asm_simp_tac (Ssum_ss addsimps |
|
686 [contX_Isinr,contX_Isinl,contX_Iwhen1,contX_Iwhen2, |
|
687 contX_Iwhen3]) 1), |
|
688 (etac ssum_lemma10 1), |
|
689 (asm_simp_tac (Ssum_ss addsimps |
|
690 [contX_Isinr,contX_Isinl,contX_Iwhen1,contX_Iwhen2, |
|
691 contX_Iwhen3]) 1) |
|
692 ]); |
|
693 |
|
694 val thelub_ssum3 = prove_goal Ssum3.thy |
|
695 "is_chain(Y) ==>\ |
|
696 \ lub(range(Y)) = sinl[lub(range(%i. when[LAM x. x][LAM y. UU][Y(i)]))]\ |
|
697 \ | lub(range(Y)) = sinr[lub(range(%i. when[LAM y. UU][LAM x. x][Y(i)]))]" |
|
698 (fn prems => |
|
699 [ |
|
700 (cut_facts_tac prems 1), |
|
701 (rtac (ssum_chainE RS disjE) 1), |
|
702 (atac 1), |
|
703 (rtac disjI1 1), |
|
704 (etac thelub_ssum2a 1), |
|
705 (atac 1), |
|
706 (rtac disjI2 1), |
|
707 (etac thelub_ssum2b 1), |
|
708 (atac 1) |
|
709 ]); |
|
710 |
|
711 |
|
712 val when4 = prove_goal Ssum3.thy |
|
713 "when[sinl][sinr][z]=z" |
|
714 (fn prems => |
|
715 [ |
|
716 (res_inst_tac [("p","z")] ssumE 1), |
|
717 (asm_simp_tac (Cfun_ss addsimps [when1,when2,when3]) 1), |
|
718 (asm_simp_tac (Cfun_ss addsimps [when1,when2,when3]) 1), |
|
719 (asm_simp_tac (Cfun_ss addsimps [when1,when2,when3]) 1) |
|
720 ]); |
|
721 |
|
722 |
|
723 (* ------------------------------------------------------------------------ *) |
|
724 (* install simplifier for Ssum *) |
|
725 (* ------------------------------------------------------------------------ *) |
|
726 |
|
727 val Ssum_rews = [strict_sinl,strict_sinr,when1,when2,when3]; |
|
728 val Ssum_ss = Cfun_ss addsimps Ssum_rews; |