1 (* Title: HOLCF/cfun2.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for cfun2.thy |
|
7 *) |
|
8 |
|
9 open Cfun2; |
|
10 |
|
11 (* ------------------------------------------------------------------------ *) |
|
12 (* access to less_cfun in class po *) |
|
13 (* ------------------------------------------------------------------------ *) |
|
14 |
|
15 val less_cfun = prove_goal Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))" |
|
16 (fn prems => |
|
17 [ |
|
18 (rtac (inst_cfun_po RS ssubst) 1), |
|
19 (fold_goals_tac [less_cfun_def]), |
|
20 (rtac refl 1) |
|
21 ]); |
|
22 |
|
23 (* ------------------------------------------------------------------------ *) |
|
24 (* Type 'a ->'b is pointed *) |
|
25 (* ------------------------------------------------------------------------ *) |
|
26 |
|
27 val minimal_cfun = prove_goalw Cfun2.thy [UU_cfun_def] "UU_cfun << f" |
|
28 (fn prems => |
|
29 [ |
|
30 (rtac (less_cfun RS ssubst) 1), |
|
31 (rtac (Abs_Cfun_inverse2 RS ssubst) 1), |
|
32 (rtac contX_const 1), |
|
33 (fold_goals_tac [UU_fun_def]), |
|
34 (rtac minimal_fun 1) |
|
35 ]); |
|
36 |
|
37 (* ------------------------------------------------------------------------ *) |
|
38 (* fapp yields continuous functions in 'a => 'b *) |
|
39 (* this is continuity of fapp in its 'second' argument *) |
|
40 (* contX_fapp2 ==> monofun_fapp2 & contlub_fapp2 *) |
|
41 (* ------------------------------------------------------------------------ *) |
|
42 |
|
43 val contX_fapp2 = prove_goal Cfun2.thy "contX(fapp(fo))" |
|
44 (fn prems => |
|
45 [ |
|
46 (res_inst_tac [("P","contX")] CollectD 1), |
|
47 (fold_goals_tac [Cfun_def]), |
|
48 (rtac Rep_Cfun 1) |
|
49 ]); |
|
50 |
|
51 val monofun_fapp2 = contX_fapp2 RS contX2mono; |
|
52 (* monofun(fapp(?fo1)) *) |
|
53 |
|
54 |
|
55 val contlub_fapp2 = contX_fapp2 RS contX2contlub; |
|
56 (* contlub(fapp(?fo1)) *) |
|
57 |
|
58 (* ------------------------------------------------------------------------ *) |
|
59 (* expanded thms contX_fapp2, contlub_fapp2 *) |
|
60 (* looks nice with mixfix syntac _[_] *) |
|
61 (* ------------------------------------------------------------------------ *) |
|
62 |
|
63 val contX_cfun_arg = (contX_fapp2 RS contXE RS spec RS mp); |
|
64 (* is_chain(?x1) ==> range(%i. ?fo3[?x1(i)]) <<| ?fo3[lub(range(?x1))] *) |
|
65 |
|
66 val contlub_cfun_arg = (contlub_fapp2 RS contlubE RS spec RS mp); |
|
67 (* is_chain(?x1) ==> ?fo4[lub(range(?x1))] = lub(range(%i. ?fo4[?x1(i)])) *) |
|
68 |
|
69 |
|
70 |
|
71 (* ------------------------------------------------------------------------ *) |
|
72 (* fapp is monotone in its 'first' argument *) |
|
73 (* ------------------------------------------------------------------------ *) |
|
74 |
|
75 val monofun_fapp1 = prove_goalw Cfun2.thy [monofun] "monofun(fapp)" |
|
76 (fn prems => |
|
77 [ |
|
78 (strip_tac 1), |
|
79 (etac (less_cfun RS subst) 1) |
|
80 ]); |
|
81 |
|
82 |
|
83 (* ------------------------------------------------------------------------ *) |
|
84 (* monotonicity of application fapp in mixfix syntax [_]_ *) |
|
85 (* ------------------------------------------------------------------------ *) |
|
86 |
|
87 val monofun_cfun_fun = prove_goal Cfun2.thy "f1 << f2 ==> f1[x] << f2[x]" |
|
88 (fn prems => |
|
89 [ |
|
90 (cut_facts_tac prems 1), |
|
91 (res_inst_tac [("x","x")] spec 1), |
|
92 (rtac (less_fun RS subst) 1), |
|
93 (etac (monofun_fapp1 RS monofunE RS spec RS spec RS mp) 1) |
|
94 ]); |
|
95 |
|
96 |
|
97 val monofun_cfun_arg = (monofun_fapp2 RS monofunE RS spec RS spec RS mp); |
|
98 (* ?x2 << ?x1 ==> ?fo5[?x2] << ?fo5[?x1] *) |
|
99 |
|
100 (* ------------------------------------------------------------------------ *) |
|
101 (* monotonicity of fapp in both arguments in mixfix syntax [_]_ *) |
|
102 (* ------------------------------------------------------------------------ *) |
|
103 |
|
104 val monofun_cfun = prove_goal Cfun2.thy |
|
105 "[|f1<<f2;x1<<x2|] ==> f1[x1] << f2[x2]" |
|
106 (fn prems => |
|
107 [ |
|
108 (cut_facts_tac prems 1), |
|
109 (rtac trans_less 1), |
|
110 (etac monofun_cfun_arg 1), |
|
111 (etac monofun_cfun_fun 1) |
|
112 ]); |
|
113 |
|
114 |
|
115 (* ------------------------------------------------------------------------ *) |
|
116 (* ch2ch - rules for the type 'a -> 'b *) |
|
117 (* use MF2 lemmas from Cont.ML *) |
|
118 (* ------------------------------------------------------------------------ *) |
|
119 |
|
120 val ch2ch_fappR = prove_goal Cfun2.thy |
|
121 "is_chain(Y) ==> is_chain(%i. f[Y(i)])" |
|
122 (fn prems => |
|
123 [ |
|
124 (cut_facts_tac prems 1), |
|
125 (etac (monofun_fapp2 RS ch2ch_MF2R) 1) |
|
126 ]); |
|
127 |
|
128 |
|
129 val ch2ch_fappL = (monofun_fapp1 RS ch2ch_MF2L); |
|
130 (* is_chain(?F) ==> is_chain(%i. ?F(i)[?x]) *) |
|
131 |
|
132 |
|
133 (* ------------------------------------------------------------------------ *) |
|
134 (* the lub of a chain of continous functions is monotone *) |
|
135 (* use MF2 lemmas from Cont.ML *) |
|
136 (* ------------------------------------------------------------------------ *) |
|
137 |
|
138 val lub_cfun_mono = prove_goal Cfun2.thy |
|
139 "is_chain(F) ==> monofun(% x.lub(range(% j.F(j)[x])))" |
|
140 (fn prems => |
|
141 [ |
|
142 (cut_facts_tac prems 1), |
|
143 (rtac lub_MF2_mono 1), |
|
144 (rtac monofun_fapp1 1), |
|
145 (rtac (monofun_fapp2 RS allI) 1), |
|
146 (atac 1) |
|
147 ]); |
|
148 |
|
149 (* ------------------------------------------------------------------------ *) |
|
150 (* a lemma about the exchange of lubs for type 'a -> 'b *) |
|
151 (* use MF2 lemmas from Cont.ML *) |
|
152 (* ------------------------------------------------------------------------ *) |
|
153 |
|
154 val ex_lubcfun = prove_goal Cfun2.thy |
|
155 "[| is_chain(F); is_chain(Y) |] ==>\ |
|
156 \ lub(range(%j. lub(range(%i. F(j)[Y(i)])))) =\ |
|
157 \ lub(range(%i. lub(range(%j. F(j)[Y(i)]))))" |
|
158 (fn prems => |
|
159 [ |
|
160 (cut_facts_tac prems 1), |
|
161 (rtac ex_lubMF2 1), |
|
162 (rtac monofun_fapp1 1), |
|
163 (rtac (monofun_fapp2 RS allI) 1), |
|
164 (atac 1), |
|
165 (atac 1) |
|
166 ]); |
|
167 |
|
168 (* ------------------------------------------------------------------------ *) |
|
169 (* the lub of a chain of cont. functions is continuous *) |
|
170 (* ------------------------------------------------------------------------ *) |
|
171 |
|
172 val contX_lubcfun = prove_goal Cfun2.thy |
|
173 "is_chain(F) ==> contX(% x.lub(range(% j.F(j)[x])))" |
|
174 (fn prems => |
|
175 [ |
|
176 (cut_facts_tac prems 1), |
|
177 (rtac monocontlub2contX 1), |
|
178 (etac lub_cfun_mono 1), |
|
179 (rtac contlubI 1), |
|
180 (strip_tac 1), |
|
181 (rtac (contlub_cfun_arg RS ext RS ssubst) 1), |
|
182 (atac 1), |
|
183 (etac ex_lubcfun 1), |
|
184 (atac 1) |
|
185 ]); |
|
186 |
|
187 (* ------------------------------------------------------------------------ *) |
|
188 (* type 'a -> 'b is chain complete *) |
|
189 (* ------------------------------------------------------------------------ *) |
|
190 |
|
191 val lub_cfun = prove_goal Cfun2.thy |
|
192 "is_chain(CCF) ==> range(CCF) <<| fabs(% x.lub(range(% i.CCF(i)[x])))" |
|
193 (fn prems => |
|
194 [ |
|
195 (cut_facts_tac prems 1), |
|
196 (rtac is_lubI 1), |
|
197 (rtac conjI 1), |
|
198 (rtac ub_rangeI 1), |
|
199 (rtac allI 1), |
|
200 (rtac (less_cfun RS ssubst) 1), |
|
201 (rtac (Abs_Cfun_inverse2 RS ssubst) 1), |
|
202 (etac contX_lubcfun 1), |
|
203 (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1), |
|
204 (etac (monofun_fapp1 RS ch2ch_monofun) 1), |
|
205 (strip_tac 1), |
|
206 (rtac (less_cfun RS ssubst) 1), |
|
207 (rtac (Abs_Cfun_inverse2 RS ssubst) 1), |
|
208 (etac contX_lubcfun 1), |
|
209 (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1), |
|
210 (etac (monofun_fapp1 RS ch2ch_monofun) 1), |
|
211 (etac (monofun_fapp1 RS ub2ub_monofun) 1) |
|
212 ]); |
|
213 |
|
214 val thelub_cfun = (lub_cfun RS thelubI); |
|
215 (* |
|
216 is_chain(?CCF1) ==> lub(range(?CCF1)) = fabs(%x. lub(range(%i. ?CCF1(i)[x]))) |
|
217 *) |
|
218 |
|
219 val cpo_cfun = prove_goal Cfun2.thy |
|
220 "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x" |
|
221 (fn prems => |
|
222 [ |
|
223 (cut_facts_tac prems 1), |
|
224 (rtac exI 1), |
|
225 (etac lub_cfun 1) |
|
226 ]); |
|
227 |
|
228 |
|
229 (* ------------------------------------------------------------------------ *) |
|
230 (* Extensionality in 'a -> 'b *) |
|
231 (* ------------------------------------------------------------------------ *) |
|
232 |
|
233 val ext_cfun = prove_goal Cfun1.thy "(!!x. f[x] = g[x]) ==> f = g" |
|
234 (fn prems => |
|
235 [ |
|
236 (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1), |
|
237 (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1), |
|
238 (res_inst_tac [("f","fabs")] arg_cong 1), |
|
239 (rtac ext 1), |
|
240 (resolve_tac prems 1) |
|
241 ]); |
|
242 |
|
243 (* ------------------------------------------------------------------------ *) |
|
244 (* Monotonicity of fabs *) |
|
245 (* ------------------------------------------------------------------------ *) |
|
246 |
|
247 val semi_monofun_fabs = prove_goal Cfun2.thy |
|
248 "[|contX(f);contX(g);f<<g|]==>fabs(f)<<fabs(g)" |
|
249 (fn prems => |
|
250 [ |
|
251 (rtac (less_cfun RS iffD2) 1), |
|
252 (rtac (Abs_Cfun_inverse2 RS ssubst) 1), |
|
253 (resolve_tac prems 1), |
|
254 (rtac (Abs_Cfun_inverse2 RS ssubst) 1), |
|
255 (resolve_tac prems 1), |
|
256 (resolve_tac prems 1) |
|
257 ]); |
|
258 |
|
259 (* ------------------------------------------------------------------------ *) |
|
260 (* Extenionality wrt. << in 'a -> 'b *) |
|
261 (* ------------------------------------------------------------------------ *) |
|
262 |
|
263 val less_cfun2 = prove_goal Cfun2.thy "(!!x. f[x] << g[x]) ==> f << g" |
|
264 (fn prems => |
|
265 [ |
|
266 (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1), |
|
267 (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1), |
|
268 (rtac semi_monofun_fabs 1), |
|
269 (rtac contX_fapp2 1), |
|
270 (rtac contX_fapp2 1), |
|
271 (rtac (less_fun RS iffD2) 1), |
|
272 (rtac allI 1), |
|
273 (resolve_tac prems 1) |
|
274 ]); |
|
275 |
|
276 |
|