|
1 (* Title: HOLCF/ssum2.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for ssum2.thy |
|
7 *) |
|
8 |
|
9 open Ssum2; |
|
10 |
|
11 (* ------------------------------------------------------------------------ *) |
|
12 (* access to less_ssum in class po *) |
|
13 (* ------------------------------------------------------------------------ *) |
|
14 |
|
15 val less_ssum3a = prove_goal Ssum2.thy |
|
16 "(Isinl(x) << Isinl(y)) = (x << y)" |
|
17 (fn prems => |
|
18 [ |
|
19 (rtac (inst_ssum_po RS ssubst) 1), |
|
20 (rtac less_ssum2a 1) |
|
21 ]); |
|
22 |
|
23 val less_ssum3b = prove_goal Ssum2.thy |
|
24 "(Isinr(x) << Isinr(y)) = (x << y)" |
|
25 (fn prems => |
|
26 [ |
|
27 (rtac (inst_ssum_po RS ssubst) 1), |
|
28 (rtac less_ssum2b 1) |
|
29 ]); |
|
30 |
|
31 val less_ssum3c = prove_goal Ssum2.thy |
|
32 "(Isinl(x) << Isinr(y)) = (x = UU)" |
|
33 (fn prems => |
|
34 [ |
|
35 (rtac (inst_ssum_po RS ssubst) 1), |
|
36 (rtac less_ssum2c 1) |
|
37 ]); |
|
38 |
|
39 val less_ssum3d = prove_goal Ssum2.thy |
|
40 "(Isinr(x) << Isinl(y)) = (x = UU)" |
|
41 (fn prems => |
|
42 [ |
|
43 (rtac (inst_ssum_po RS ssubst) 1), |
|
44 (rtac less_ssum2d 1) |
|
45 ]); |
|
46 |
|
47 |
|
48 (* ------------------------------------------------------------------------ *) |
|
49 (* type ssum ++ is pointed *) |
|
50 (* ------------------------------------------------------------------------ *) |
|
51 |
|
52 val minimal_ssum = prove_goal Ssum2.thy "Isinl(UU) << s" |
|
53 (fn prems => |
|
54 [ |
|
55 (res_inst_tac [("p","s")] IssumE2 1), |
|
56 (hyp_subst_tac 1), |
|
57 (rtac (less_ssum3a RS iffD2) 1), |
|
58 (rtac minimal 1), |
|
59 (hyp_subst_tac 1), |
|
60 (rtac (strict_IsinlIsinr RS ssubst) 1), |
|
61 (rtac (less_ssum3b RS iffD2) 1), |
|
62 (rtac minimal 1) |
|
63 ]); |
|
64 |
|
65 |
|
66 (* ------------------------------------------------------------------------ *) |
|
67 (* Isinl, Isinr are monotone *) |
|
68 (* ------------------------------------------------------------------------ *) |
|
69 |
|
70 val monofun_Isinl = prove_goalw Ssum2.thy [monofun] "monofun(Isinl)" |
|
71 (fn prems => |
|
72 [ |
|
73 (strip_tac 1), |
|
74 (etac (less_ssum3a RS iffD2) 1) |
|
75 ]); |
|
76 |
|
77 val monofun_Isinr = prove_goalw Ssum2.thy [monofun] "monofun(Isinr)" |
|
78 (fn prems => |
|
79 [ |
|
80 (strip_tac 1), |
|
81 (etac (less_ssum3b RS iffD2) 1) |
|
82 ]); |
|
83 |
|
84 |
|
85 (* ------------------------------------------------------------------------ *) |
|
86 (* Iwhen is monotone in all arguments *) |
|
87 (* ------------------------------------------------------------------------ *) |
|
88 |
|
89 |
|
90 val monofun_Iwhen1 = prove_goalw Ssum2.thy [monofun] "monofun(Iwhen)" |
|
91 (fn prems => |
|
92 [ |
|
93 (strip_tac 1), |
|
94 (rtac (less_fun RS iffD2) 1), |
|
95 (strip_tac 1), |
|
96 (rtac (less_fun RS iffD2) 1), |
|
97 (strip_tac 1), |
|
98 (res_inst_tac [("p","xb")] IssumE 1), |
|
99 (hyp_subst_tac 1), |
|
100 (asm_simp_tac Ssum_ss 1), |
|
101 (asm_simp_tac Ssum_ss 1), |
|
102 (etac monofun_cfun_fun 1), |
|
103 (asm_simp_tac Ssum_ss 1) |
|
104 ]); |
|
105 |
|
106 val monofun_Iwhen2 = prove_goalw Ssum2.thy [monofun] "monofun(Iwhen(f))" |
|
107 (fn prems => |
|
108 [ |
|
109 (strip_tac 1), |
|
110 (rtac (less_fun RS iffD2) 1), |
|
111 (strip_tac 1), |
|
112 (res_inst_tac [("p","xa")] IssumE 1), |
|
113 (hyp_subst_tac 1), |
|
114 (asm_simp_tac Ssum_ss 1), |
|
115 (asm_simp_tac Ssum_ss 1), |
|
116 (asm_simp_tac Ssum_ss 1), |
|
117 (etac monofun_cfun_fun 1) |
|
118 ]); |
|
119 |
|
120 val monofun_Iwhen3 = prove_goalw Ssum2.thy [monofun] "monofun(Iwhen(f)(g))" |
|
121 (fn prems => |
|
122 [ |
|
123 (strip_tac 1), |
|
124 (res_inst_tac [("p","x")] IssumE 1), |
|
125 (hyp_subst_tac 1), |
|
126 (asm_simp_tac Ssum_ss 1), |
|
127 (hyp_subst_tac 1), |
|
128 (res_inst_tac [("p","y")] IssumE 1), |
|
129 (hyp_subst_tac 1), |
|
130 (asm_simp_tac Ssum_ss 1), |
|
131 (res_inst_tac [("P","xa=UU")] notE 1), |
|
132 (atac 1), |
|
133 (rtac UU_I 1), |
|
134 (rtac (less_ssum3a RS iffD1) 1), |
|
135 (atac 1), |
|
136 (hyp_subst_tac 1), |
|
137 (asm_simp_tac Ssum_ss 1), |
|
138 (rtac monofun_cfun_arg 1), |
|
139 (etac (less_ssum3a RS iffD1) 1), |
|
140 (hyp_subst_tac 1), |
|
141 (res_inst_tac [("s","UU"),("t","xa")] subst 1), |
|
142 (etac (less_ssum3c RS iffD1 RS sym) 1), |
|
143 (asm_simp_tac Ssum_ss 1), |
|
144 (hyp_subst_tac 1), |
|
145 (res_inst_tac [("p","y")] IssumE 1), |
|
146 (hyp_subst_tac 1), |
|
147 (res_inst_tac [("s","UU"),("t","ya")] subst 1), |
|
148 (etac (less_ssum3d RS iffD1 RS sym) 1), |
|
149 (asm_simp_tac Ssum_ss 1), |
|
150 (hyp_subst_tac 1), |
|
151 (res_inst_tac [("s","UU"),("t","ya")] subst 1), |
|
152 (etac (less_ssum3d RS iffD1 RS sym) 1), |
|
153 (asm_simp_tac Ssum_ss 1), |
|
154 (hyp_subst_tac 1), |
|
155 (asm_simp_tac Ssum_ss 1), |
|
156 (rtac monofun_cfun_arg 1), |
|
157 (etac (less_ssum3b RS iffD1) 1) |
|
158 ]); |
|
159 |
|
160 |
|
161 |
|
162 |
|
163 (* ------------------------------------------------------------------------ *) |
|
164 (* some kind of exhaustion rules for chains in 'a ++ 'b *) |
|
165 (* ------------------------------------------------------------------------ *) |
|
166 |
|
167 |
|
168 val ssum_lemma1 = prove_goal Ssum2.thy |
|
169 "[|~(!i.? x.Y(i::nat)=Isinl(x))|] ==> (? i.! x.~Y(i)=Isinl(x))" |
|
170 (fn prems => |
|
171 [ |
|
172 (cut_facts_tac prems 1), |
|
173 (fast_tac HOL_cs 1) |
|
174 ]); |
|
175 |
|
176 val ssum_lemma2 = prove_goal Ssum2.thy |
|
177 "[|(? i.!x.~(Y::nat => 'a++'b)(i::nat)=Isinl(x::'a))|] ==>\ |
|
178 \ (? i y. (Y::nat => 'a++'b)(i::nat)=Isinr(y::'b) & ~y=UU)" |
|
179 (fn prems => |
|
180 [ |
|
181 (cut_facts_tac prems 1), |
|
182 (etac exE 1), |
|
183 (res_inst_tac [("p","Y(i)")] IssumE 1), |
|
184 (dtac spec 1), |
|
185 (contr_tac 1), |
|
186 (dtac spec 1), |
|
187 (contr_tac 1), |
|
188 (fast_tac HOL_cs 1) |
|
189 ]); |
|
190 |
|
191 |
|
192 val ssum_lemma3 = prove_goal Ssum2.thy |
|
193 "[|is_chain(Y);(? i x. Y(i)=Isinr(x) & ~x=UU)|] ==> (!i.? y.Y(i)=Isinr(y))" |
|
194 (fn prems => |
|
195 [ |
|
196 (cut_facts_tac prems 1), |
|
197 (etac exE 1), |
|
198 (etac exE 1), |
|
199 (rtac allI 1), |
|
200 (res_inst_tac [("p","Y(ia)")] IssumE 1), |
|
201 (rtac exI 1), |
|
202 (rtac trans 1), |
|
203 (rtac strict_IsinlIsinr 2), |
|
204 (atac 1), |
|
205 (etac exI 2), |
|
206 (etac conjE 1), |
|
207 (res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1), |
|
208 (hyp_subst_tac 2), |
|
209 (etac exI 2), |
|
210 (res_inst_tac [("P","x=UU")] notE 1), |
|
211 (atac 1), |
|
212 (rtac (less_ssum3d RS iffD1) 1), |
|
213 (res_inst_tac [("s","Y(i)"),("t","Isinr(x)")] subst 1), |
|
214 (atac 1), |
|
215 (res_inst_tac [("s","Y(ia)"),("t","Isinl(xa)")] subst 1), |
|
216 (atac 1), |
|
217 (etac (chain_mono RS mp) 1), |
|
218 (atac 1), |
|
219 (res_inst_tac [("P","xa=UU")] notE 1), |
|
220 (atac 1), |
|
221 (rtac (less_ssum3c RS iffD1) 1), |
|
222 (res_inst_tac [("s","Y(i)"),("t","Isinr(x)")] subst 1), |
|
223 (atac 1), |
|
224 (res_inst_tac [("s","Y(ia)"),("t","Isinl(xa)")] subst 1), |
|
225 (atac 1), |
|
226 (etac (chain_mono RS mp) 1), |
|
227 (atac 1) |
|
228 ]); |
|
229 |
|
230 val ssum_lemma4 = prove_goal Ssum2.thy |
|
231 "is_chain(Y) ==> (!i.? x.Y(i)=Isinl(x))|(!i.? y.Y(i)=Isinr(y))" |
|
232 (fn prems => |
|
233 [ |
|
234 (cut_facts_tac prems 1), |
|
235 (rtac classical2 1), |
|
236 (etac disjI1 1), |
|
237 (rtac disjI2 1), |
|
238 (etac ssum_lemma3 1), |
|
239 (rtac ssum_lemma2 1), |
|
240 (etac ssum_lemma1 1) |
|
241 ]); |
|
242 |
|
243 |
|
244 (* ------------------------------------------------------------------------ *) |
|
245 (* restricted surjectivity of Isinl *) |
|
246 (* ------------------------------------------------------------------------ *) |
|
247 |
|
248 val ssum_lemma5 = prove_goal Ssum2.thy |
|
249 "z=Isinl(x)==> Isinl((Iwhen (LAM x.x) (LAM y.UU))(z)) = z" |
|
250 (fn prems => |
|
251 [ |
|
252 (cut_facts_tac prems 1), |
|
253 (hyp_subst_tac 1), |
|
254 (res_inst_tac [("Q","x=UU")] classical2 1), |
|
255 (asm_simp_tac Ssum_ss 1), |
|
256 (asm_simp_tac Ssum_ss 1) |
|
257 ]); |
|
258 |
|
259 (* ------------------------------------------------------------------------ *) |
|
260 (* restricted surjectivity of Isinr *) |
|
261 (* ------------------------------------------------------------------------ *) |
|
262 |
|
263 val ssum_lemma6 = prove_goal Ssum2.thy |
|
264 "z=Isinr(x)==> Isinr((Iwhen (LAM y.UU) (LAM x.x))(z)) = z" |
|
265 (fn prems => |
|
266 [ |
|
267 (cut_facts_tac prems 1), |
|
268 (hyp_subst_tac 1), |
|
269 (res_inst_tac [("Q","x=UU")] classical2 1), |
|
270 (asm_simp_tac Ssum_ss 1), |
|
271 (asm_simp_tac Ssum_ss 1) |
|
272 ]); |
|
273 |
|
274 (* ------------------------------------------------------------------------ *) |
|
275 (* technical lemmas *) |
|
276 (* ------------------------------------------------------------------------ *) |
|
277 |
|
278 val ssum_lemma7 = prove_goal Ssum2.thy |
|
279 "[|Isinl(x) << z; ~x=UU|] ==> ? y.z=Isinl(y) & ~y=UU" |
|
280 (fn prems => |
|
281 [ |
|
282 (cut_facts_tac prems 1), |
|
283 (res_inst_tac [("p","z")] IssumE 1), |
|
284 (hyp_subst_tac 1), |
|
285 (etac notE 1), |
|
286 (rtac antisym_less 1), |
|
287 (etac (less_ssum3a RS iffD1) 1), |
|
288 (rtac minimal 1), |
|
289 (fast_tac HOL_cs 1), |
|
290 (hyp_subst_tac 1), |
|
291 (rtac notE 1), |
|
292 (etac (less_ssum3c RS iffD1) 2), |
|
293 (atac 1) |
|
294 ]); |
|
295 |
|
296 val ssum_lemma8 = prove_goal Ssum2.thy |
|
297 "[|Isinr(x) << z; ~x=UU|] ==> ? y.z=Isinr(y) & ~y=UU" |
|
298 (fn prems => |
|
299 [ |
|
300 (cut_facts_tac prems 1), |
|
301 (res_inst_tac [("p","z")] IssumE 1), |
|
302 (hyp_subst_tac 1), |
|
303 (etac notE 1), |
|
304 (etac (less_ssum3d RS iffD1) 1), |
|
305 (hyp_subst_tac 1), |
|
306 (rtac notE 1), |
|
307 (etac (less_ssum3d RS iffD1) 2), |
|
308 (atac 1), |
|
309 (fast_tac HOL_cs 1) |
|
310 ]); |
|
311 |
|
312 (* ------------------------------------------------------------------------ *) |
|
313 (* the type 'a ++ 'b is a cpo in three steps *) |
|
314 (* ------------------------------------------------------------------------ *) |
|
315 |
|
316 val lub_ssum1a = prove_goal Ssum2.thy |
|
317 "[|is_chain(Y);(!i.? x.Y(i)=Isinl(x))|] ==>\ |
|
318 \ range(Y) <<|\ |
|
319 \ Isinl(lub(range(%i.(Iwhen (LAM x.x) (LAM y.UU))(Y(i)))))" |
|
320 (fn prems => |
|
321 [ |
|
322 (cut_facts_tac prems 1), |
|
323 (rtac is_lubI 1), |
|
324 (rtac conjI 1), |
|
325 (rtac ub_rangeI 1), |
|
326 (rtac allI 1), |
|
327 (etac allE 1), |
|
328 (etac exE 1), |
|
329 (res_inst_tac [("t","Y(i)")] (ssum_lemma5 RS subst) 1), |
|
330 (atac 1), |
|
331 (rtac (monofun_Isinl RS monofunE RS spec RS spec RS mp) 1), |
|
332 (rtac is_ub_thelub 1), |
|
333 (etac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
|
334 (strip_tac 1), |
|
335 (res_inst_tac [("p","u")] IssumE2 1), |
|
336 (res_inst_tac [("t","u")] (ssum_lemma5 RS subst) 1), |
|
337 (atac 1), |
|
338 (rtac (monofun_Isinl RS monofunE RS spec RS spec RS mp) 1), |
|
339 (rtac is_lub_thelub 1), |
|
340 (etac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
|
341 (etac (monofun_Iwhen3 RS ub2ub_monofun) 1), |
|
342 (hyp_subst_tac 1), |
|
343 (rtac (less_ssum3c RS iffD2) 1), |
|
344 (rtac chain_UU_I_inverse 1), |
|
345 (rtac allI 1), |
|
346 (res_inst_tac [("p","Y(i)")] IssumE 1), |
|
347 (asm_simp_tac Ssum_ss 1), |
|
348 (asm_simp_tac Ssum_ss 2), |
|
349 (etac notE 1), |
|
350 (rtac (less_ssum3c RS iffD1) 1), |
|
351 (res_inst_tac [("t","Isinl(x)")] subst 1), |
|
352 (atac 1), |
|
353 (etac (ub_rangeE RS spec) 1) |
|
354 ]); |
|
355 |
|
356 |
|
357 val lub_ssum1b = prove_goal Ssum2.thy |
|
358 "[|is_chain(Y);(!i.? x.Y(i)=Isinr(x))|] ==>\ |
|
359 \ range(Y) <<|\ |
|
360 \ Isinr(lub(range(%i.(Iwhen (LAM y.UU) (LAM x.x))(Y(i)))))" |
|
361 (fn prems => |
|
362 [ |
|
363 (cut_facts_tac prems 1), |
|
364 (rtac is_lubI 1), |
|
365 (rtac conjI 1), |
|
366 (rtac ub_rangeI 1), |
|
367 (rtac allI 1), |
|
368 (etac allE 1), |
|
369 (etac exE 1), |
|
370 (res_inst_tac [("t","Y(i)")] (ssum_lemma6 RS subst) 1), |
|
371 (atac 1), |
|
372 (rtac (monofun_Isinr RS monofunE RS spec RS spec RS mp) 1), |
|
373 (rtac is_ub_thelub 1), |
|
374 (etac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
|
375 (strip_tac 1), |
|
376 (res_inst_tac [("p","u")] IssumE2 1), |
|
377 (hyp_subst_tac 1), |
|
378 (rtac (less_ssum3d RS iffD2) 1), |
|
379 (rtac chain_UU_I_inverse 1), |
|
380 (rtac allI 1), |
|
381 (res_inst_tac [("p","Y(i)")] IssumE 1), |
|
382 (asm_simp_tac Ssum_ss 1), |
|
383 (asm_simp_tac Ssum_ss 1), |
|
384 (etac notE 1), |
|
385 (rtac (less_ssum3d RS iffD1) 1), |
|
386 (res_inst_tac [("t","Isinr(y)")] subst 1), |
|
387 (atac 1), |
|
388 (etac (ub_rangeE RS spec) 1), |
|
389 (res_inst_tac [("t","u")] (ssum_lemma6 RS subst) 1), |
|
390 (atac 1), |
|
391 (rtac (monofun_Isinr RS monofunE RS spec RS spec RS mp) 1), |
|
392 (rtac is_lub_thelub 1), |
|
393 (etac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
|
394 (etac (monofun_Iwhen3 RS ub2ub_monofun) 1) |
|
395 ]); |
|
396 |
|
397 |
|
398 val thelub_ssum1a = lub_ssum1a RS thelubI; |
|
399 (* [| is_chain(?Y1); ! i. ? x. ?Y1(i) = Isinl(x) |] ==> *) |
|
400 (* lub(range(?Y1)) = Isinl(lub(range(%i. Iwhen(LAM x. x,LAM y. UU,?Y1(i)))))*) |
|
401 |
|
402 val thelub_ssum1b = lub_ssum1b RS thelubI; |
|
403 (* [| is_chain(?Y1); ! i. ? x. ?Y1(i) = Isinr(x) |] ==> *) |
|
404 (* lub(range(?Y1)) = Isinr(lub(range(%i. Iwhen(LAM y. UU,LAM x. x,?Y1(i)))))*) |
|
405 |
|
406 val cpo_ssum = prove_goal Ssum2.thy |
|
407 "is_chain(Y::nat=>'a ++'b) ==> ? x.range(Y) <<|x" |
|
408 (fn prems => |
|
409 [ |
|
410 (cut_facts_tac prems 1), |
|
411 (rtac (ssum_lemma4 RS disjE) 1), |
|
412 (atac 1), |
|
413 (rtac exI 1), |
|
414 (etac lub_ssum1a 1), |
|
415 (atac 1), |
|
416 (rtac exI 1), |
|
417 (etac lub_ssum1b 1), |
|
418 (atac 1) |
|
419 ]); |