|
1 (* Title: HOLCF/Up3.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for Up3.thy |
|
7 *) |
|
8 |
|
9 open Up3; |
|
10 |
|
11 (* -------------------------------------------------------------------------*) |
|
12 (* some lemmas restated for class pcpo *) |
|
13 (* ------------------------------------------------------------------------ *) |
|
14 |
|
15 qed_goal "less_up3b" Up3.thy "~ Iup(x) << UU" |
|
16 (fn prems => |
|
17 [ |
|
18 (stac inst_up_pcpo 1), |
|
19 (rtac less_up2b 1) |
|
20 ]); |
|
21 |
|
22 qed_goal "defined_Iup2" Up3.thy "Iup(x) ~= UU" |
|
23 (fn prems => |
|
24 [ |
|
25 (stac inst_up_pcpo 1), |
|
26 (rtac defined_Iup 1) |
|
27 ]); |
|
28 |
|
29 (* ------------------------------------------------------------------------ *) |
|
30 (* continuity for Iup *) |
|
31 (* ------------------------------------------------------------------------ *) |
|
32 |
|
33 qed_goal "contlub_Iup" Up3.thy "contlub(Iup)" |
|
34 (fn prems => |
|
35 [ |
|
36 (rtac contlubI 1), |
|
37 (strip_tac 1), |
|
38 (rtac trans 1), |
|
39 (rtac (thelub_up1a RS sym) 2), |
|
40 (fast_tac HOL_cs 3), |
|
41 (etac (monofun_Iup RS ch2ch_monofun) 2), |
|
42 (res_inst_tac [("f","Iup")] arg_cong 1), |
|
43 (rtac lub_equal 1), |
|
44 (atac 1), |
|
45 (rtac (monofun_Ifup2 RS ch2ch_monofun) 1), |
|
46 (etac (monofun_Iup RS ch2ch_monofun) 1), |
|
47 (asm_simp_tac Up0_ss 1) |
|
48 ]); |
|
49 |
|
50 qed_goal "cont_Iup" Up3.thy "cont(Iup)" |
|
51 (fn prems => |
|
52 [ |
|
53 (rtac monocontlub2cont 1), |
|
54 (rtac monofun_Iup 1), |
|
55 (rtac contlub_Iup 1) |
|
56 ]); |
|
57 |
|
58 |
|
59 (* ------------------------------------------------------------------------ *) |
|
60 (* continuity for Ifup *) |
|
61 (* ------------------------------------------------------------------------ *) |
|
62 |
|
63 qed_goal "contlub_Ifup1" Up3.thy "contlub(Ifup)" |
|
64 (fn prems => |
|
65 [ |
|
66 (rtac contlubI 1), |
|
67 (strip_tac 1), |
|
68 (rtac trans 1), |
|
69 (rtac (thelub_fun RS sym) 2), |
|
70 (etac (monofun_Ifup1 RS ch2ch_monofun) 2), |
|
71 (rtac ext 1), |
|
72 (res_inst_tac [("p","x")] upE 1), |
|
73 (asm_simp_tac Up0_ss 1), |
|
74 (rtac (lub_const RS thelubI RS sym) 1), |
|
75 (asm_simp_tac Up0_ss 1), |
|
76 (etac contlub_cfun_fun 1) |
|
77 ]); |
|
78 |
|
79 |
|
80 qed_goal "contlub_Ifup2" Up3.thy "contlub(Ifup(f))" |
|
81 (fn prems => |
|
82 [ |
|
83 (rtac contlubI 1), |
|
84 (strip_tac 1), |
|
85 (rtac disjE 1), |
|
86 (stac thelub_up1a 2), |
|
87 (atac 2), |
|
88 (atac 2), |
|
89 (asm_simp_tac Up0_ss 2), |
|
90 (stac thelub_up1b 3), |
|
91 (atac 3), |
|
92 (atac 3), |
|
93 (fast_tac HOL_cs 1), |
|
94 (asm_simp_tac Up0_ss 2), |
|
95 (rtac (chain_UU_I_inverse RS sym) 2), |
|
96 (rtac allI 2), |
|
97 (res_inst_tac [("p","Y(i)")] upE 2), |
|
98 (asm_simp_tac Up0_ss 2), |
|
99 (rtac notE 2), |
|
100 (dtac spec 2), |
|
101 (etac spec 2), |
|
102 (atac 2), |
|
103 (stac contlub_cfun_arg 1), |
|
104 (etac (monofun_Ifup2 RS ch2ch_monofun) 1), |
|
105 (rtac lub_equal2 1), |
|
106 (rtac (monofun_fapp2 RS ch2ch_monofun) 2), |
|
107 (etac (monofun_Ifup2 RS ch2ch_monofun) 2), |
|
108 (etac (monofun_Ifup2 RS ch2ch_monofun) 2), |
|
109 (rtac (chain_mono2 RS exE) 1), |
|
110 (atac 2), |
|
111 (etac exE 1), |
|
112 (etac exE 1), |
|
113 (rtac exI 1), |
|
114 (res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1), |
|
115 (atac 1), |
|
116 (rtac defined_Iup2 1), |
|
117 (rtac exI 1), |
|
118 (strip_tac 1), |
|
119 (res_inst_tac [("p","Y(i)")] upE 1), |
|
120 (asm_simp_tac Up0_ss 2), |
|
121 (res_inst_tac [("P","Y(i) = UU")] notE 1), |
|
122 (fast_tac HOL_cs 1), |
|
123 (stac inst_up_pcpo 1), |
|
124 (atac 1) |
|
125 ]); |
|
126 |
|
127 qed_goal "cont_Ifup1" Up3.thy "cont(Ifup)" |
|
128 (fn prems => |
|
129 [ |
|
130 (rtac monocontlub2cont 1), |
|
131 (rtac monofun_Ifup1 1), |
|
132 (rtac contlub_Ifup1 1) |
|
133 ]); |
|
134 |
|
135 qed_goal "cont_Ifup2" Up3.thy "cont(Ifup(f))" |
|
136 (fn prems => |
|
137 [ |
|
138 (rtac monocontlub2cont 1), |
|
139 (rtac monofun_Ifup2 1), |
|
140 (rtac contlub_Ifup2 1) |
|
141 ]); |
|
142 |
|
143 |
|
144 (* ------------------------------------------------------------------------ *) |
|
145 (* continuous versions of lemmas for ('a)u *) |
|
146 (* ------------------------------------------------------------------------ *) |
|
147 |
|
148 qed_goalw "Exh_Up1" Up3.thy [up_def] "z = UU | (? x. z = up`x)" |
|
149 (fn prems => |
|
150 [ |
|
151 (simp_tac (Up0_ss addsimps [cont_Iup]) 1), |
|
152 (stac inst_up_pcpo 1), |
|
153 (rtac Exh_Up 1) |
|
154 ]); |
|
155 |
|
156 qed_goalw "inject_up" Up3.thy [up_def] "up`x=up`y ==> x=y" |
|
157 (fn prems => |
|
158 [ |
|
159 (cut_facts_tac prems 1), |
|
160 (rtac inject_Iup 1), |
|
161 (etac box_equals 1), |
|
162 (simp_tac (Up0_ss addsimps [cont_Iup]) 1), |
|
163 (simp_tac (Up0_ss addsimps [cont_Iup]) 1) |
|
164 ]); |
|
165 |
|
166 qed_goalw "defined_up" Up3.thy [up_def] " up`x ~= UU" |
|
167 (fn prems => |
|
168 [ |
|
169 (simp_tac (Up0_ss addsimps [cont_Iup]) 1), |
|
170 (rtac defined_Iup2 1) |
|
171 ]); |
|
172 |
|
173 qed_goalw "upE1" Up3.thy [up_def] |
|
174 "[| p=UU ==> Q; !!x. p=up`x==>Q|] ==>Q" |
|
175 (fn prems => |
|
176 [ |
|
177 (rtac upE 1), |
|
178 (resolve_tac prems 1), |
|
179 (etac (inst_up_pcpo RS ssubst) 1), |
|
180 (resolve_tac (tl prems) 1), |
|
181 (asm_simp_tac (Up0_ss addsimps [cont_Iup]) 1) |
|
182 ]); |
|
183 |
|
184 |
|
185 qed_goalw "fup1" Up3.thy [up_def,fup_def] "fup`f`UU=UU" |
|
186 (fn prems => |
|
187 [ |
|
188 (stac inst_up_pcpo 1), |
|
189 (stac beta_cfun 1), |
|
190 (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, |
|
191 cont_Ifup2,cont2cont_CF1L]) 1)), |
|
192 (stac beta_cfun 1), |
|
193 (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, |
|
194 cont_Ifup2,cont2cont_CF1L]) 1)), |
|
195 (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1) |
|
196 ]); |
|
197 |
|
198 qed_goalw "fup2" Up3.thy [up_def,fup_def] "fup`f`(up`x)=f`x" |
|
199 (fn prems => |
|
200 [ |
|
201 (stac beta_cfun 1), |
|
202 (rtac cont_Iup 1), |
|
203 (stac beta_cfun 1), |
|
204 (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, |
|
205 cont_Ifup2,cont2cont_CF1L]) 1)), |
|
206 (stac beta_cfun 1), |
|
207 (rtac cont_Ifup2 1), |
|
208 (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1) |
|
209 ]); |
|
210 |
|
211 qed_goalw "less_up4b" Up3.thy [up_def,fup_def] "~ up`x << UU" |
|
212 (fn prems => |
|
213 [ |
|
214 (simp_tac (Up0_ss addsimps [cont_Iup]) 1), |
|
215 (rtac less_up3b 1) |
|
216 ]); |
|
217 |
|
218 qed_goalw "less_up4c" Up3.thy [up_def,fup_def] |
|
219 "(up`x << up`y) = (x<<y)" |
|
220 (fn prems => |
|
221 [ |
|
222 (simp_tac (Up0_ss addsimps [cont_Iup]) 1), |
|
223 (rtac less_up2c 1) |
|
224 ]); |
|
225 |
|
226 qed_goalw "thelub_up2a" Up3.thy [up_def,fup_def] |
|
227 "[| is_chain(Y); ? i x. Y(i) = up`x |] ==>\ |
|
228 \ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))" |
|
229 (fn prems => |
|
230 [ |
|
231 (cut_facts_tac prems 1), |
|
232 (stac beta_cfun 1), |
|
233 (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, |
|
234 cont_Ifup2,cont2cont_CF1L]) 1)), |
|
235 (stac beta_cfun 1), |
|
236 (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, |
|
237 cont_Ifup2,cont2cont_CF1L]) 1)), |
|
238 |
|
239 (stac (beta_cfun RS ext) 1), |
|
240 (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, |
|
241 cont_Ifup2,cont2cont_CF1L]) 1)), |
|
242 (rtac thelub_up1a 1), |
|
243 (atac 1), |
|
244 (etac exE 1), |
|
245 (etac exE 1), |
|
246 (rtac exI 1), |
|
247 (rtac exI 1), |
|
248 (etac box_equals 1), |
|
249 (rtac refl 1), |
|
250 (simp_tac (Up0_ss addsimps [cont_Iup]) 1) |
|
251 ]); |
|
252 |
|
253 |
|
254 |
|
255 qed_goalw "thelub_up2b" Up3.thy [up_def,fup_def] |
|
256 "[| is_chain(Y); ! i x. Y(i) ~= up`x |] ==> lub(range(Y)) = UU" |
|
257 (fn prems => |
|
258 [ |
|
259 (cut_facts_tac prems 1), |
|
260 (stac inst_up_pcpo 1), |
|
261 (rtac thelub_up1b 1), |
|
262 (atac 1), |
|
263 (strip_tac 1), |
|
264 (dtac spec 1), |
|
265 (dtac spec 1), |
|
266 (rtac swap 1), |
|
267 (atac 1), |
|
268 (dtac notnotD 1), |
|
269 (etac box_equals 1), |
|
270 (rtac refl 1), |
|
271 (simp_tac (Up0_ss addsimps [cont_Iup]) 1) |
|
272 ]); |
|
273 |
|
274 |
|
275 qed_goal "up_lemma2" Up3.thy " (? x.z = up`x) = (z~=UU)" |
|
276 (fn prems => |
|
277 [ |
|
278 (rtac iffI 1), |
|
279 (etac exE 1), |
|
280 (hyp_subst_tac 1), |
|
281 (rtac defined_up 1), |
|
282 (res_inst_tac [("p","z")] upE1 1), |
|
283 (etac notE 1), |
|
284 (atac 1), |
|
285 (etac exI 1) |
|
286 ]); |
|
287 |
|
288 |
|
289 qed_goal "thelub_up2a_rev" Up3.thy |
|
290 "[| is_chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x" |
|
291 (fn prems => |
|
292 [ |
|
293 (cut_facts_tac prems 1), |
|
294 (rtac exE 1), |
|
295 (rtac chain_UU_I_inverse2 1), |
|
296 (rtac (up_lemma2 RS iffD1) 1), |
|
297 (etac exI 1), |
|
298 (rtac exI 1), |
|
299 (rtac (up_lemma2 RS iffD2) 1), |
|
300 (atac 1) |
|
301 ]); |
|
302 |
|
303 qed_goal "thelub_up2b_rev" Up3.thy |
|
304 "[| is_chain(Y); lub(range(Y)) = UU |] ==> ! i x. Y(i) ~= up`x" |
|
305 (fn prems => |
|
306 [ |
|
307 (cut_facts_tac prems 1), |
|
308 (rtac allI 1), |
|
309 (rtac (not_ex RS iffD1) 1), |
|
310 (rtac contrapos 1), |
|
311 (etac (up_lemma2 RS iffD1) 2), |
|
312 (fast_tac (HOL_cs addSDs [chain_UU_I RS spec]) 1) |
|
313 ]); |
|
314 |
|
315 |
|
316 qed_goal "thelub_up3" Up3.thy |
|
317 "is_chain(Y) ==> lub(range(Y)) = UU |\ |
|
318 \ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x.x)`(Y i))))" |
|
319 (fn prems => |
|
320 [ |
|
321 (cut_facts_tac prems 1), |
|
322 (rtac disjE 1), |
|
323 (rtac disjI1 2), |
|
324 (rtac thelub_up2b 2), |
|
325 (atac 2), |
|
326 (atac 2), |
|
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" Up3.thy "fup`up`x=x" |
|
335 (fn prems => |
|
336 [ |
|
337 (res_inst_tac [("p","x")] upE1 1), |
|
338 (asm_simp_tac ((simpset_of "Cfun3") addsimps [fup1,fup2]) 1), |
|
339 (asm_simp_tac ((simpset_of "Cfun3") addsimps [fup1,fup2]) 1) |
|
340 ]); |
|
341 |
|
342 (* ------------------------------------------------------------------------ *) |
|
343 (* install simplifier for ('a)u *) |
|
344 (* ------------------------------------------------------------------------ *) |
|
345 |
|
346 val up_rews = [fup1,fup2,defined_up]; |
|
347 |