1 (* Title: HOLCF/cfun3.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 *) |
|
6 |
|
7 open Cfun3; |
|
8 |
|
9 (* ------------------------------------------------------------------------ *) |
|
10 (* the contlub property for fapp its 'first' argument *) |
|
11 (* ------------------------------------------------------------------------ *) |
|
12 |
|
13 val contlub_fapp1 = prove_goal Cfun3.thy "contlub(fapp)" |
|
14 (fn prems => |
|
15 [ |
|
16 (rtac contlubI 1), |
|
17 (strip_tac 1), |
|
18 (rtac (expand_fun_eq RS iffD2) 1), |
|
19 (strip_tac 1), |
|
20 (rtac (lub_cfun RS thelubI RS ssubst) 1), |
|
21 (atac 1), |
|
22 (rtac (Cfunapp2 RS ssubst) 1), |
|
23 (etac contX_lubcfun 1), |
|
24 (rtac (lub_fun RS thelubI RS ssubst) 1), |
|
25 (etac (monofun_fapp1 RS ch2ch_monofun) 1), |
|
26 (rtac refl 1) |
|
27 ]); |
|
28 |
|
29 |
|
30 (* ------------------------------------------------------------------------ *) |
|
31 (* the contX property for fapp in its first argument *) |
|
32 (* ------------------------------------------------------------------------ *) |
|
33 |
|
34 val contX_fapp1 = prove_goal Cfun3.thy "contX(fapp)" |
|
35 (fn prems => |
|
36 [ |
|
37 (rtac monocontlub2contX 1), |
|
38 (rtac monofun_fapp1 1), |
|
39 (rtac contlub_fapp1 1) |
|
40 ]); |
|
41 |
|
42 |
|
43 (* ------------------------------------------------------------------------ *) |
|
44 (* contlub, contX properties of fapp in its first argument in mixfix _[_] *) |
|
45 (* ------------------------------------------------------------------------ *) |
|
46 |
|
47 val contlub_cfun_fun = prove_goal Cfun3.thy |
|
48 "is_chain(FY) ==>\ |
|
49 \ lub(range(FY))[x] = lub(range(%i.FY(i)[x]))" |
|
50 (fn prems => |
|
51 [ |
|
52 (cut_facts_tac prems 1), |
|
53 (rtac trans 1), |
|
54 (etac (contlub_fapp1 RS contlubE RS spec RS mp RS fun_cong) 1), |
|
55 (rtac (thelub_fun RS ssubst) 1), |
|
56 (etac (monofun_fapp1 RS ch2ch_monofun) 1), |
|
57 (rtac refl 1) |
|
58 ]); |
|
59 |
|
60 |
|
61 val contX_cfun_fun = prove_goal Cfun3.thy |
|
62 "is_chain(FY) ==>\ |
|
63 \ range(%i.FY(i)[x]) <<| lub(range(FY))[x]" |
|
64 (fn prems => |
|
65 [ |
|
66 (cut_facts_tac prems 1), |
|
67 (rtac thelubE 1), |
|
68 (etac ch2ch_fappL 1), |
|
69 (etac (contlub_cfun_fun RS sym) 1) |
|
70 ]); |
|
71 |
|
72 |
|
73 (* ------------------------------------------------------------------------ *) |
|
74 (* contlub, contX properties of fapp in both argument in mixfix _[_] *) |
|
75 (* ------------------------------------------------------------------------ *) |
|
76 |
|
77 val contlub_cfun = prove_goal Cfun3.thy |
|
78 "[|is_chain(FY);is_chain(TY)|] ==>\ |
|
79 \ lub(range(FY))[lub(range(TY))] = lub(range(%i.FY(i)[TY(i)]))" |
|
80 (fn prems => |
|
81 [ |
|
82 (cut_facts_tac prems 1), |
|
83 (rtac contlub_CF2 1), |
|
84 (rtac contX_fapp1 1), |
|
85 (rtac allI 1), |
|
86 (rtac contX_fapp2 1), |
|
87 (atac 1), |
|
88 (atac 1) |
|
89 ]); |
|
90 |
|
91 val contX_cfun = prove_goal Cfun3.thy |
|
92 "[|is_chain(FY);is_chain(TY)|] ==>\ |
|
93 \ range(%i.FY(i)[TY(i)]) <<| lub(range(FY))[lub(range(TY))]" |
|
94 (fn prems => |
|
95 [ |
|
96 (cut_facts_tac prems 1), |
|
97 (rtac thelubE 1), |
|
98 (rtac (monofun_fapp1 RS ch2ch_MF2LR) 1), |
|
99 (rtac allI 1), |
|
100 (rtac monofun_fapp2 1), |
|
101 (atac 1), |
|
102 (atac 1), |
|
103 (etac (contlub_cfun RS sym) 1), |
|
104 (atac 1) |
|
105 ]); |
|
106 |
|
107 |
|
108 (* ------------------------------------------------------------------------ *) |
|
109 (* contX2contX lemma for fapp *) |
|
110 (* ------------------------------------------------------------------------ *) |
|
111 |
|
112 val contX2contX_fapp = prove_goal Cfun3.thy |
|
113 "[|contX(%x.ft(x));contX(%x.tt(x))|] ==> contX(%x.(ft(x))[tt(x)])" |
|
114 (fn prems => |
|
115 [ |
|
116 (cut_facts_tac prems 1), |
|
117 (rtac contX2contX_app2 1), |
|
118 (rtac contX2contX_app2 1), |
|
119 (rtac contX_const 1), |
|
120 (rtac contX_fapp1 1), |
|
121 (atac 1), |
|
122 (rtac contX_fapp2 1), |
|
123 (atac 1) |
|
124 ]); |
|
125 |
|
126 |
|
127 |
|
128 (* ------------------------------------------------------------------------ *) |
|
129 (* contX2mono Lemma for %x. LAM y. c1(x,y) *) |
|
130 (* ------------------------------------------------------------------------ *) |
|
131 |
|
132 val contX2mono_LAM = prove_goal Cfun3.thy |
|
133 "[|!x.contX(c1(x)); !y.monofun(%x.c1(x,y))|] ==>\ |
|
134 \ monofun(%x. LAM y. c1(x,y))" |
|
135 (fn prems => |
|
136 [ |
|
137 (cut_facts_tac prems 1), |
|
138 (rtac monofunI 1), |
|
139 (strip_tac 1), |
|
140 (rtac (less_cfun RS ssubst) 1), |
|
141 (rtac (less_fun RS ssubst) 1), |
|
142 (rtac allI 1), |
|
143 (rtac (beta_cfun RS ssubst) 1), |
|
144 (etac spec 1), |
|
145 (rtac (beta_cfun RS ssubst) 1), |
|
146 (etac spec 1), |
|
147 (etac ((hd (tl prems)) RS spec RS monofunE RS spec RS spec RS mp) 1) |
|
148 ]); |
|
149 |
|
150 (* ------------------------------------------------------------------------ *) |
|
151 (* contX2contX Lemma for %x. LAM y. c1(x,y) *) |
|
152 (* ------------------------------------------------------------------------ *) |
|
153 |
|
154 val contX2contX_LAM = prove_goal Cfun3.thy |
|
155 "[| !x.contX(c1(x)); !y.contX(%x.c1(x,y)) |] ==> contX(%x. LAM y. c1(x,y))" |
|
156 (fn prems => |
|
157 [ |
|
158 (cut_facts_tac prems 1), |
|
159 (rtac monocontlub2contX 1), |
|
160 (etac contX2mono_LAM 1), |
|
161 (rtac (contX2mono RS allI) 1), |
|
162 (etac spec 1), |
|
163 (rtac contlubI 1), |
|
164 (strip_tac 1), |
|
165 (rtac (thelub_cfun RS ssubst) 1), |
|
166 (rtac (contX2mono_LAM RS ch2ch_monofun) 1), |
|
167 (atac 1), |
|
168 (rtac (contX2mono RS allI) 1), |
|
169 (etac spec 1), |
|
170 (atac 1), |
|
171 (res_inst_tac [("f","fabs")] arg_cong 1), |
|
172 (rtac ext 1), |
|
173 (rtac (beta_cfun RS ext RS ssubst) 1), |
|
174 (etac spec 1), |
|
175 (rtac (contX2contlub RS contlubE |
|
176 RS spec RS mp ) 1), |
|
177 (etac spec 1), |
|
178 (atac 1) |
|
179 ]); |
|
180 |
|
181 (* ------------------------------------------------------------------------ *) |
|
182 (* elimination of quantifier in premisses of contX2contX_LAM yields good *) |
|
183 (* lemma for the contX tactic *) |
|
184 (* ------------------------------------------------------------------------ *) |
|
185 |
|
186 val contX2contX_LAM2 = (allI RSN (2,(allI RS contX2contX_LAM))); |
|
187 (* |
|
188 [| !!x. contX(?c1.0(x)); !!y. contX(%x. ?c1.0(x,y)) |] ==> |
|
189 contX(%x. LAM y. ?c1.0(x,y)) |
|
190 *) |
|
191 |
|
192 (* ------------------------------------------------------------------------ *) |
|
193 (* contX2contX tactic *) |
|
194 (* ------------------------------------------------------------------------ *) |
|
195 |
|
196 val contX_lemmas = [contX_const, contX_id, contX_fapp2, |
|
197 contX2contX_fapp,contX2contX_LAM2]; |
|
198 |
|
199 |
|
200 val contX_tac = (fn i => (resolve_tac contX_lemmas i)); |
|
201 |
|
202 val contX_tacR = (fn i => (REPEAT (contX_tac i))); |
|
203 |
|
204 (* ------------------------------------------------------------------------ *) |
|
205 (* function application _[_] is strict in its first arguments *) |
|
206 (* ------------------------------------------------------------------------ *) |
|
207 |
|
208 val strict_fapp1 = prove_goal Cfun3.thy "UU[x] = UU" |
|
209 (fn prems => |
|
210 [ |
|
211 (rtac (inst_cfun_pcpo RS ssubst) 1), |
|
212 (rewrite_goals_tac [UU_cfun_def]), |
|
213 (rtac (beta_cfun RS ssubst) 1), |
|
214 (contX_tac 1), |
|
215 (rtac refl 1) |
|
216 ]); |
|
217 |
|
218 |
|
219 (* ------------------------------------------------------------------------ *) |
|
220 (* results about strictify *) |
|
221 (* ------------------------------------------------------------------------ *) |
|
222 |
|
223 val Istrictify1 = prove_goalw Cfun3.thy [Istrictify_def] |
|
224 "Istrictify(f)(UU)=UU" |
|
225 (fn prems => |
|
226 [ |
|
227 (rtac select_equality 1), |
|
228 (fast_tac HOL_cs 1), |
|
229 (fast_tac HOL_cs 1) |
|
230 ]); |
|
231 |
|
232 val Istrictify2 = prove_goalw Cfun3.thy [Istrictify_def] |
|
233 "~x=UU ==> Istrictify(f)(x)=f[x]" |
|
234 (fn prems => |
|
235 [ |
|
236 (cut_facts_tac prems 1), |
|
237 (rtac select_equality 1), |
|
238 (fast_tac HOL_cs 1), |
|
239 (fast_tac HOL_cs 1) |
|
240 ]); |
|
241 |
|
242 val monofun_Istrictify1 = prove_goal Cfun3.thy "monofun(Istrictify)" |
|
243 (fn prems => |
|
244 [ |
|
245 (rtac monofunI 1), |
|
246 (strip_tac 1), |
|
247 (rtac (less_fun RS iffD2) 1), |
|
248 (strip_tac 1), |
|
249 (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1), |
|
250 (rtac (Istrictify2 RS ssubst) 1), |
|
251 (atac 1), |
|
252 (rtac (Istrictify2 RS ssubst) 1), |
|
253 (atac 1), |
|
254 (rtac monofun_cfun_fun 1), |
|
255 (atac 1), |
|
256 (hyp_subst_tac 1), |
|
257 (rtac (Istrictify1 RS ssubst) 1), |
|
258 (rtac (Istrictify1 RS ssubst) 1), |
|
259 (rtac refl_less 1) |
|
260 ]); |
|
261 |
|
262 val monofun_Istrictify2 = prove_goal Cfun3.thy "monofun(Istrictify(f))" |
|
263 (fn prems => |
|
264 [ |
|
265 (rtac monofunI 1), |
|
266 (strip_tac 1), |
|
267 (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1), |
|
268 (rtac (Istrictify2 RS ssubst) 1), |
|
269 (etac notUU_I 1), |
|
270 (atac 1), |
|
271 (rtac (Istrictify2 RS ssubst) 1), |
|
272 (atac 1), |
|
273 (rtac monofun_cfun_arg 1), |
|
274 (atac 1), |
|
275 (hyp_subst_tac 1), |
|
276 (rtac (Istrictify1 RS ssubst) 1), |
|
277 (rtac minimal 1) |
|
278 ]); |
|
279 |
|
280 |
|
281 val contlub_Istrictify1 = prove_goal Cfun3.thy "contlub(Istrictify)" |
|
282 (fn prems => |
|
283 [ |
|
284 (rtac contlubI 1), |
|
285 (strip_tac 1), |
|
286 (rtac (expand_fun_eq RS iffD2) 1), |
|
287 (strip_tac 1), |
|
288 (rtac (thelub_fun RS ssubst) 1), |
|
289 (etac (monofun_Istrictify1 RS ch2ch_monofun) 1), |
|
290 (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1), |
|
291 (rtac (Istrictify2 RS ssubst) 1), |
|
292 (atac 1), |
|
293 (rtac (Istrictify2 RS ext RS ssubst) 1), |
|
294 (atac 1), |
|
295 (rtac (thelub_cfun RS ssubst) 1), |
|
296 (atac 1), |
|
297 (rtac (beta_cfun RS ssubst) 1), |
|
298 (rtac contX_lubcfun 1), |
|
299 (atac 1), |
|
300 (rtac refl 1), |
|
301 (hyp_subst_tac 1), |
|
302 (rtac (Istrictify1 RS ssubst) 1), |
|
303 (rtac (Istrictify1 RS ext RS ssubst) 1), |
|
304 (rtac (chain_UU_I_inverse RS sym) 1), |
|
305 (rtac (refl RS allI) 1) |
|
306 ]); |
|
307 |
|
308 val contlub_Istrictify2 = prove_goal Cfun3.thy "contlub(Istrictify(f))" |
|
309 (fn prems => |
|
310 [ |
|
311 (rtac contlubI 1), |
|
312 (strip_tac 1), |
|
313 (res_inst_tac [("Q","lub(range(Y))=UU")] classical2 1), |
|
314 (res_inst_tac [("t","lub(range(Y))")] subst 1), |
|
315 (rtac sym 1), |
|
316 (atac 1), |
|
317 (rtac (Istrictify1 RS ssubst) 1), |
|
318 (rtac sym 1), |
|
319 (rtac chain_UU_I_inverse 1), |
|
320 (strip_tac 1), |
|
321 (res_inst_tac [("t","Y(i)"),("s","UU")] subst 1), |
|
322 (rtac sym 1), |
|
323 (rtac (chain_UU_I RS spec) 1), |
|
324 (atac 1), |
|
325 (atac 1), |
|
326 (rtac Istrictify1 1), |
|
327 (rtac (Istrictify2 RS ssubst) 1), |
|
328 (atac 1), |
|
329 (res_inst_tac [("s","lub(range(%i. f[Y(i)]))")] trans 1), |
|
330 (rtac contlub_cfun_arg 1), |
|
331 (atac 1), |
|
332 (rtac lub_equal2 1), |
|
333 (rtac (chain_mono2 RS exE) 1), |
|
334 (atac 2), |
|
335 (rtac chain_UU_I_inverse2 1), |
|
336 (atac 1), |
|
337 (rtac exI 1), |
|
338 (strip_tac 1), |
|
339 (rtac (Istrictify2 RS sym) 1), |
|
340 (fast_tac HOL_cs 1), |
|
341 (rtac ch2ch_monofun 1), |
|
342 (rtac monofun_fapp2 1), |
|
343 (atac 1), |
|
344 (rtac ch2ch_monofun 1), |
|
345 (rtac monofun_Istrictify2 1), |
|
346 (atac 1) |
|
347 ]); |
|
348 |
|
349 |
|
350 val contX_Istrictify1 = (contlub_Istrictify1 RS |
|
351 (monofun_Istrictify1 RS monocontlub2contX)); |
|
352 |
|
353 val contX_Istrictify2 = (contlub_Istrictify2 RS |
|
354 (monofun_Istrictify2 RS monocontlub2contX)); |
|
355 |
|
356 |
|
357 val strictify1 = prove_goalw Cfun3.thy [strictify_def] |
|
358 "strictify[f][UU]=UU" |
|
359 (fn prems => |
|
360 [ |
|
361 (rtac (beta_cfun RS ssubst) 1), |
|
362 (contX_tac 1), |
|
363 (rtac contX_Istrictify2 1), |
|
364 (rtac contX2contX_CF1L 1), |
|
365 (rtac contX_Istrictify1 1), |
|
366 (rtac (beta_cfun RS ssubst) 1), |
|
367 (rtac contX_Istrictify2 1), |
|
368 (rtac Istrictify1 1) |
|
369 ]); |
|
370 |
|
371 val strictify2 = prove_goalw Cfun3.thy [strictify_def] |
|
372 "~x=UU ==> strictify[f][x]=f[x]" |
|
373 (fn prems => |
|
374 [ |
|
375 (rtac (beta_cfun RS ssubst) 1), |
|
376 (contX_tac 1), |
|
377 (rtac contX_Istrictify2 1), |
|
378 (rtac contX2contX_CF1L 1), |
|
379 (rtac contX_Istrictify1 1), |
|
380 (rtac (beta_cfun RS ssubst) 1), |
|
381 (rtac contX_Istrictify2 1), |
|
382 (rtac Istrictify2 1), |
|
383 (resolve_tac prems 1) |
|
384 ]); |
|
385 |
|
386 |
|
387 (* ------------------------------------------------------------------------ *) |
|
388 (* Instantiate the simplifier *) |
|
389 (* ------------------------------------------------------------------------ *) |
|
390 |
|
391 val Cfun_rews = [minimal,refl_less,beta_cfun,strict_fapp1,strictify1, |
|
392 strictify2]; |
|
393 |
|
394 (* ------------------------------------------------------------------------ *) |
|
395 (* use contX_tac as autotac. *) |
|
396 (* ------------------------------------------------------------------------ *) |
|
397 |
|
398 val Cfun_ss = HOL_ss |
|
399 addsimps Cfun_rews |
|
400 setsolver |
|
401 (fn thms => (resolve_tac (TrueI::refl::thms)) ORELSE' atac ORELSE' |
|
402 (fn i => DEPTH_SOLVE_1 (contX_tac i)) |
|
403 ); |
|