1 (* Title: HOLCF/Up3.ML |
1 (* Title: HOLCF/Up3.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Franz Regensburger |
3 Author: Franz Regensburger |
4 Copyright 1993 Technische Universitaet Muenchen |
4 Copyright 1993 Technische Universitaet Muenchen |
5 |
5 |
6 Lemmas for Up3.thy |
6 Class instance of ('a)u for class pcpo |
7 *) |
7 *) |
8 |
8 |
9 open Up3; |
|
10 |
|
11 (* for compatibility with old HOLCF-Version *) |
9 (* for compatibility with old HOLCF-Version *) |
12 qed_goal "inst_up_pcpo" thy "UU = Abs_Up(Inl ())" |
10 Goal "UU = Abs_Up(Inl ())"; |
13 (fn prems => |
11 by (simp_tac (HOL_ss addsimps [UU_def,UU_up_def]) 1); |
14 [ |
12 qed "inst_up_pcpo"; |
15 (simp_tac (HOL_ss addsimps [UU_def,UU_up_def]) 1) |
|
16 ]); |
|
17 |
13 |
18 (* -------------------------------------------------------------------------*) |
14 (* -------------------------------------------------------------------------*) |
19 (* some lemmas restated for class pcpo *) |
15 (* some lemmas restated for class pcpo *) |
20 (* ------------------------------------------------------------------------ *) |
16 (* ------------------------------------------------------------------------ *) |
21 |
17 |
22 qed_goal "less_up3b" thy "~ Iup(x) << UU" |
18 Goal "~ Iup(x) << UU"; |
23 (fn prems => |
19 by (stac inst_up_pcpo 1); |
24 [ |
20 by (rtac less_up2b 1); |
25 (stac inst_up_pcpo 1), |
21 qed "less_up3b"; |
26 (rtac less_up2b 1) |
22 |
27 ]); |
23 Goal "Iup(x) ~= UU"; |
28 |
24 by (stac inst_up_pcpo 1); |
29 qed_goal "defined_Iup2" thy "Iup(x) ~= UU" |
25 by (rtac defined_Iup 1); |
30 (fn prems => |
26 qed "defined_Iup2"; |
31 [ |
|
32 (stac inst_up_pcpo 1), |
|
33 (rtac defined_Iup 1) |
|
34 ]); |
|
35 |
27 |
36 (* ------------------------------------------------------------------------ *) |
28 (* ------------------------------------------------------------------------ *) |
37 (* continuity for Iup *) |
29 (* continuity for Iup *) |
38 (* ------------------------------------------------------------------------ *) |
30 (* ------------------------------------------------------------------------ *) |
39 |
31 |
40 qed_goal "contlub_Iup" thy "contlub(Iup)" |
32 Goal "contlub(Iup)"; |
41 (fn prems => |
33 by (rtac contlubI 1); |
42 [ |
34 by (strip_tac 1); |
43 (rtac contlubI 1), |
35 by (rtac trans 1); |
44 (strip_tac 1), |
36 by (rtac (thelub_up1a RS sym) 2); |
45 (rtac trans 1), |
37 by (fast_tac HOL_cs 3); |
46 (rtac (thelub_up1a RS sym) 2), |
38 by (etac (monofun_Iup RS ch2ch_monofun) 2); |
47 (fast_tac HOL_cs 3), |
39 by (res_inst_tac [("f","Iup")] arg_cong 1); |
48 (etac (monofun_Iup RS ch2ch_monofun) 2), |
40 by (rtac lub_equal 1); |
49 (res_inst_tac [("f","Iup")] arg_cong 1), |
41 by (atac 1); |
50 (rtac lub_equal 1), |
42 by (rtac (monofun_Ifup2 RS ch2ch_monofun) 1); |
51 (atac 1), |
43 by (etac (monofun_Iup RS ch2ch_monofun) 1); |
52 (rtac (monofun_Ifup2 RS ch2ch_monofun) 1), |
44 by (asm_simp_tac Up0_ss 1); |
53 (etac (monofun_Iup RS ch2ch_monofun) 1), |
45 qed "contlub_Iup"; |
54 (asm_simp_tac Up0_ss 1) |
46 |
55 ]); |
47 Goal "cont(Iup)"; |
56 |
48 by (rtac monocontlub2cont 1); |
57 qed_goal "cont_Iup" thy "cont(Iup)" |
49 by (rtac monofun_Iup 1); |
58 (fn prems => |
50 by (rtac contlub_Iup 1); |
59 [ |
51 qed "cont_Iup"; |
60 (rtac monocontlub2cont 1), |
|
61 (rtac monofun_Iup 1), |
|
62 (rtac contlub_Iup 1) |
|
63 ]); |
|
64 |
52 |
65 |
53 |
66 (* ------------------------------------------------------------------------ *) |
54 (* ------------------------------------------------------------------------ *) |
67 (* continuity for Ifup *) |
55 (* continuity for Ifup *) |
68 (* ------------------------------------------------------------------------ *) |
56 (* ------------------------------------------------------------------------ *) |
69 |
57 |
70 qed_goal "contlub_Ifup1" thy "contlub(Ifup)" |
58 Goal "contlub(Ifup)"; |
71 (fn prems => |
59 by (rtac contlubI 1); |
72 [ |
60 by (strip_tac 1); |
73 (rtac contlubI 1), |
61 by (rtac trans 1); |
74 (strip_tac 1), |
62 by (rtac (thelub_fun RS sym) 2); |
75 (rtac trans 1), |
63 by (etac (monofun_Ifup1 RS ch2ch_monofun) 2); |
76 (rtac (thelub_fun RS sym) 2), |
64 by (rtac ext 1); |
77 (etac (monofun_Ifup1 RS ch2ch_monofun) 2), |
65 by (res_inst_tac [("p","x")] upE 1); |
78 (rtac ext 1), |
66 by (asm_simp_tac Up0_ss 1); |
79 (res_inst_tac [("p","x")] upE 1), |
67 by (rtac (lub_const RS thelubI RS sym) 1); |
80 (asm_simp_tac Up0_ss 1), |
68 by (asm_simp_tac Up0_ss 1); |
81 (rtac (lub_const RS thelubI RS sym) 1), |
69 by (etac contlub_cfun_fun 1); |
82 (asm_simp_tac Up0_ss 1), |
70 qed "contlub_Ifup1"; |
83 (etac contlub_cfun_fun 1) |
|
84 ]); |
|
85 |
71 |
86 |
72 |
87 Goal "contlub(Ifup(f))"; |
73 Goal "contlub(Ifup(f))"; |
88 by (rtac contlubI 1); |
74 by (rtac contlubI 1); |
89 by (strip_tac 1); |
75 by (strip_tac 1); |
127 by (fast_tac HOL_cs 1); |
113 by (fast_tac HOL_cs 1); |
128 by (stac inst_up_pcpo 1); |
114 by (stac inst_up_pcpo 1); |
129 by (atac 1); |
115 by (atac 1); |
130 qed "contlub_Ifup2"; |
116 qed "contlub_Ifup2"; |
131 |
117 |
132 qed_goal "cont_Ifup1" thy "cont(Ifup)" |
118 Goal "cont(Ifup)"; |
133 (fn prems => |
119 by (rtac monocontlub2cont 1); |
134 [ |
120 by (rtac monofun_Ifup1 1); |
135 (rtac monocontlub2cont 1), |
121 by (rtac contlub_Ifup1 1); |
136 (rtac monofun_Ifup1 1), |
122 qed "cont_Ifup1"; |
137 (rtac contlub_Ifup1 1) |
123 |
138 ]); |
124 Goal "cont(Ifup(f))"; |
139 |
125 by (rtac monocontlub2cont 1); |
140 qed_goal "cont_Ifup2" thy "cont(Ifup(f))" |
126 by (rtac monofun_Ifup2 1); |
141 (fn prems => |
127 by (rtac contlub_Ifup2 1); |
142 [ |
128 qed "cont_Ifup2"; |
143 (rtac monocontlub2cont 1), |
|
144 (rtac monofun_Ifup2 1), |
|
145 (rtac contlub_Ifup2 1) |
|
146 ]); |
|
147 |
129 |
148 |
130 |
149 (* ------------------------------------------------------------------------ *) |
131 (* ------------------------------------------------------------------------ *) |
150 (* continuous versions of lemmas for ('a)u *) |
132 (* continuous versions of lemmas for ('a)u *) |
151 (* ------------------------------------------------------------------------ *) |
133 (* ------------------------------------------------------------------------ *) |
270 (rtac refl 1), |
252 (rtac refl 1), |
271 (simp_tac (Up0_ss addsimps [cont_Iup]) 1) |
253 (simp_tac (Up0_ss addsimps [cont_Iup]) 1) |
272 ]); |
254 ]); |
273 |
255 |
274 |
256 |
275 qed_goal "up_lemma2" thy " (? x. z = up`x) = (z~=UU)" |
257 Goal "(? x. z = up`x) = (z~=UU)"; |
276 (fn prems => |
258 by (rtac iffI 1); |
277 [ |
259 by (etac exE 1); |
278 (rtac iffI 1), |
260 by (hyp_subst_tac 1); |
279 (etac exE 1), |
261 by (rtac defined_up 1); |
280 (hyp_subst_tac 1), |
262 by (res_inst_tac [("p","z")] upE1 1); |
281 (rtac defined_up 1), |
263 by (etac notE 1); |
282 (res_inst_tac [("p","z")] upE1 1), |
264 by (atac 1); |
283 (etac notE 1), |
265 by (etac exI 1); |
284 (atac 1), |
266 qed "up_lemma2"; |
285 (etac exI 1) |
267 |
286 ]); |
268 |
287 |
269 Goal "[| chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x"; |
288 |
270 by (rtac exE 1); |
289 qed_goal "thelub_up2a_rev" thy |
271 by (rtac chain_UU_I_inverse2 1); |
290 "[| chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x" |
272 by (rtac (up_lemma2 RS iffD1) 1); |
291 (fn prems => |
273 by (etac exI 1); |
292 [ |
274 by (rtac exI 1); |
293 (cut_facts_tac prems 1), |
275 by (rtac (up_lemma2 RS iffD2) 1); |
294 (rtac exE 1), |
276 by (atac 1); |
295 (rtac chain_UU_I_inverse2 1), |
277 qed "thelub_up2a_rev"; |
296 (rtac (up_lemma2 RS iffD1) 1), |
278 |
297 (etac exI 1), |
279 Goal "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x. Y(i) ~= up`x"; |
298 (rtac exI 1), |
280 by (cut_facts_tac prems 1); |
299 (rtac (up_lemma2 RS iffD2) 1), |
281 by (rtac allI 1); |
300 (atac 1) |
282 by (rtac (not_ex RS iffD1) 1); |
301 ]); |
283 by (rtac contrapos 1); |
302 |
284 by (etac (up_lemma2 RS iffD1) 2); |
303 qed_goal "thelub_up2b_rev" thy |
285 by (fast_tac (HOL_cs addSDs [chain_UU_I RS spec]) 1); |
304 "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x. Y(i) ~= up`x" |
286 qed "thelub_up2b_rev"; |
305 (fn prems => |
287 |
306 [ |
288 |
307 (cut_facts_tac prems 1), |
289 Goal "chain(Y) ==> lub(range(Y)) = UU | \ |
308 (rtac allI 1), |
290 \ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"; |
309 (rtac (not_ex RS iffD1) 1), |
291 by (cut_facts_tac prems 1); |
310 (rtac contrapos 1), |
292 by (rtac disjE 1); |
311 (etac (up_lemma2 RS iffD1) 2), |
293 by (rtac disjI1 2); |
312 (fast_tac (HOL_cs addSDs [chain_UU_I RS spec]) 1) |
294 by (rtac thelub_up2b 2); |
313 ]); |
295 by (atac 2); |
314 |
296 by (atac 2); |
315 |
297 by (rtac disjI2 2); |
316 qed_goal "thelub_up3" thy |
298 by (rtac thelub_up2a 2); |
317 "chain(Y) ==> lub(range(Y)) = UU |\ |
299 by (atac 2); |
318 \ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))" |
300 by (atac 2); |
319 (fn prems => |
301 by (fast_tac HOL_cs 1); |
320 [ |
302 qed "thelub_up3"; |
321 (cut_facts_tac prems 1), |
303 |
322 (rtac disjE 1), |
304 Goal "fup`up`x=x"; |
323 (rtac disjI1 2), |
305 by (res_inst_tac [("p","x")] upE1 1); |
324 (rtac thelub_up2b 2), |
306 by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1); |
325 (atac 2), |
307 by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1); |
326 (atac 2), |
308 qed "fup3"; |
327 (rtac disjI2 2), |
|
328 (rtac thelub_up2a 2), |
|
329 (atac 2), |
|
330 (atac 2), |
|
331 (fast_tac HOL_cs 1) |
|
332 ]); |
|
333 |
|
334 qed_goal "fup3" thy "fup`up`x=x" |
|
335 (fn prems => |
|
336 [ |
|
337 (res_inst_tac [("p","x")] upE1 1), |
|
338 (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1), |
|
339 (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1) |
|
340 ]); |
|
341 |
309 |
342 (* ------------------------------------------------------------------------ *) |
310 (* ------------------------------------------------------------------------ *) |
343 (* install simplifier for ('a)u *) |
311 (* install simplifier for ('a)u *) |
344 (* ------------------------------------------------------------------------ *) |
312 (* ------------------------------------------------------------------------ *) |
345 |
313 |