1 (* Title: HOLCF/cprod3.ML |
1 (* Title: HOLCF/Cprod3 |
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 Cprod3.thy |
6 Class instance of * for class pcpo and cpo. |
7 *) |
7 *) |
8 |
8 |
9 open Cprod3; |
|
10 |
|
11 (* for compatibility with old HOLCF-Version *) |
9 (* for compatibility with old HOLCF-Version *) |
12 qed_goal "inst_cprod_pcpo" thy "UU = (UU,UU)" |
10 val prems = goal thy "UU = (UU,UU)"; |
13 (fn prems => |
11 by (simp_tac (HOL_ss addsimps [UU_def,UU_cprod_def]) 1); |
14 [ |
12 qed "inst_cprod_pcpo"; |
15 (simp_tac (HOL_ss addsimps [UU_def,UU_cprod_def]) 1) |
|
16 ]); |
|
17 |
13 |
18 (* ------------------------------------------------------------------------ *) |
14 (* ------------------------------------------------------------------------ *) |
19 (* continuity of (_,_) , fst, snd *) |
15 (* continuity of (_,_) , fst, snd *) |
20 (* ------------------------------------------------------------------------ *) |
16 (* ------------------------------------------------------------------------ *) |
21 |
17 |
22 qed_goal "Cprod3_lemma1" Cprod3.thy |
18 val prems = goal Cprod3.thy |
23 "chain(Y::(nat=>'a::cpo)) ==>\ |
19 "chain(Y::(nat=>'a::cpo)) ==>\ |
24 \ (lub(range(Y)),(x::'b::cpo)) =\ |
20 \ (lub(range(Y)),(x::'b::cpo)) =\ |
25 \ (lub(range(%i. fst(Y i,x))),lub(range(%i. snd(Y i,x))))" |
21 \ (lub(range(%i. fst(Y i,x))),lub(range(%i. snd(Y i,x))))"; |
26 (fn prems => |
22 by (cut_facts_tac prems 1); |
27 [ |
23 by (res_inst_tac [("f1","Pair")] (arg_cong RS cong) 1); |
28 (cut_facts_tac prems 1), |
24 by (rtac lub_equal 1); |
29 (res_inst_tac [("f1","Pair")] (arg_cong RS cong) 1), |
25 by (atac 1); |
30 (rtac lub_equal 1), |
26 by (rtac (monofun_fst RS ch2ch_monofun) 1); |
31 (atac 1), |
27 by (rtac ch2ch_fun 1); |
32 (rtac (monofun_fst RS ch2ch_monofun) 1), |
28 by (rtac (monofun_pair1 RS ch2ch_monofun) 1); |
33 (rtac ch2ch_fun 1), |
29 by (atac 1); |
34 (rtac (monofun_pair1 RS ch2ch_monofun) 1), |
30 by (rtac allI 1); |
35 (atac 1), |
31 by (Simp_tac 1); |
36 (rtac allI 1), |
32 by (rtac sym 1); |
37 (Simp_tac 1), |
33 by (Simp_tac 1); |
38 (rtac sym 1), |
34 by (rtac (lub_const RS thelubI) 1); |
39 (Simp_tac 1), |
35 qed "Cprod3_lemma1"; |
40 (rtac (lub_const RS thelubI) 1) |
36 |
41 ]); |
37 val prems = goal Cprod3.thy "contlub(Pair)"; |
42 |
38 by (rtac contlubI 1); |
43 qed_goal "contlub_pair1" Cprod3.thy "contlub(Pair)" |
39 by (strip_tac 1); |
44 (fn prems => |
40 by (rtac (expand_fun_eq RS iffD2) 1); |
45 [ |
41 by (strip_tac 1); |
46 (rtac contlubI 1), |
42 by (stac (lub_fun RS thelubI) 1); |
47 (strip_tac 1), |
43 by (etac (monofun_pair1 RS ch2ch_monofun) 1); |
48 (rtac (expand_fun_eq RS iffD2) 1), |
44 by (rtac trans 1); |
49 (strip_tac 1), |
45 by (rtac (thelub_cprod RS sym) 2); |
50 (stac (lub_fun RS thelubI) 1), |
46 by (rtac ch2ch_fun 2); |
51 (etac (monofun_pair1 RS ch2ch_monofun) 1), |
47 by (etac (monofun_pair1 RS ch2ch_monofun) 2); |
52 (rtac trans 1), |
48 by (etac Cprod3_lemma1 1); |
53 (rtac (thelub_cprod RS sym) 2), |
49 qed "contlub_pair1"; |
54 (rtac ch2ch_fun 2), |
50 |
55 (etac (monofun_pair1 RS ch2ch_monofun) 2), |
51 val prems = goal Cprod3.thy |
56 (etac Cprod3_lemma1 1) |
|
57 ]); |
|
58 |
|
59 qed_goal "Cprod3_lemma2" Cprod3.thy |
|
60 "chain(Y::(nat=>'a::cpo)) ==>\ |
52 "chain(Y::(nat=>'a::cpo)) ==>\ |
61 \ ((x::'b::cpo),lub(range Y)) =\ |
53 \ ((x::'b::cpo),lub(range Y)) =\ |
62 \ (lub(range(%i. fst(x,Y i))),lub(range(%i. snd(x, Y i))))" |
54 \ (lub(range(%i. fst(x,Y i))),lub(range(%i. snd(x, Y i))))"; |
63 (fn prems => |
55 by (cut_facts_tac prems 1); |
64 [ |
56 by (res_inst_tac [("f1","Pair")] (arg_cong RS cong) 1); |
65 (cut_facts_tac prems 1), |
57 by (rtac sym 1); |
66 (res_inst_tac [("f1","Pair")] (arg_cong RS cong) 1), |
58 by (Simp_tac 1); |
67 (rtac sym 1), |
59 by (rtac (lub_const RS thelubI) 1); |
68 (Simp_tac 1), |
60 by (rtac lub_equal 1); |
69 (rtac (lub_const RS thelubI) 1), |
61 by (atac 1); |
70 (rtac lub_equal 1), |
62 by (rtac (monofun_snd RS ch2ch_monofun) 1); |
71 (atac 1), |
63 by (rtac (monofun_pair2 RS ch2ch_monofun) 1); |
72 (rtac (monofun_snd RS ch2ch_monofun) 1), |
64 by (atac 1); |
73 (rtac (monofun_pair2 RS ch2ch_monofun) 1), |
65 by (rtac allI 1); |
74 (atac 1), |
66 by (Simp_tac 1); |
75 (rtac allI 1), |
67 qed "Cprod3_lemma2"; |
76 (Simp_tac 1) |
68 |
77 ]); |
69 val prems = goal Cprod3.thy "contlub(Pair(x))"; |
78 |
70 by (rtac contlubI 1); |
79 qed_goal "contlub_pair2" Cprod3.thy "contlub(Pair(x))" |
71 by (strip_tac 1); |
80 (fn prems => |
72 by (rtac trans 1); |
81 [ |
73 by (rtac (thelub_cprod RS sym) 2); |
82 (rtac contlubI 1), |
74 by (etac (monofun_pair2 RS ch2ch_monofun) 2); |
83 (strip_tac 1), |
75 by (etac Cprod3_lemma2 1); |
84 (rtac trans 1), |
76 qed "contlub_pair2"; |
85 (rtac (thelub_cprod RS sym) 2), |
77 |
86 (etac (monofun_pair2 RS ch2ch_monofun) 2), |
78 val prems = goal Cprod3.thy "cont(Pair)"; |
87 (etac Cprod3_lemma2 1) |
79 by (rtac monocontlub2cont 1); |
88 ]); |
80 by (rtac monofun_pair1 1); |
89 |
81 by (rtac contlub_pair1 1); |
90 qed_goal "cont_pair1" Cprod3.thy "cont(Pair)" |
82 qed "cont_pair1"; |
91 (fn prems => |
83 |
92 [ |
84 val prems = goal Cprod3.thy "cont(Pair(x))"; |
93 (rtac monocontlub2cont 1), |
85 by (rtac monocontlub2cont 1); |
94 (rtac monofun_pair1 1), |
86 by (rtac monofun_pair2 1); |
95 (rtac contlub_pair1 1) |
87 by (rtac contlub_pair2 1); |
96 ]); |
88 qed "cont_pair2"; |
97 |
89 |
98 qed_goal "cont_pair2" Cprod3.thy "cont(Pair(x))" |
90 val prems = goal Cprod3.thy "contlub(fst)"; |
99 (fn prems => |
91 by (rtac contlubI 1); |
100 [ |
92 by (strip_tac 1); |
101 (rtac monocontlub2cont 1), |
93 by (stac (lub_cprod RS thelubI) 1); |
102 (rtac monofun_pair2 1), |
94 by (atac 1); |
103 (rtac contlub_pair2 1) |
95 by (Simp_tac 1); |
104 ]); |
96 qed "contlub_fst"; |
105 |
97 |
106 qed_goal "contlub_fst" Cprod3.thy "contlub(fst)" |
98 val prems = goal Cprod3.thy "contlub(snd)"; |
107 (fn prems => |
99 by (rtac contlubI 1); |
108 [ |
100 by (strip_tac 1); |
109 (rtac contlubI 1), |
101 by (stac (lub_cprod RS thelubI) 1); |
110 (strip_tac 1), |
102 by (atac 1); |
111 (stac (lub_cprod RS thelubI) 1), |
103 by (Simp_tac 1); |
112 (atac 1), |
104 qed "contlub_snd"; |
113 (Simp_tac 1) |
105 |
114 ]); |
106 val prems = goal Cprod3.thy "cont(fst)"; |
115 |
107 by (rtac monocontlub2cont 1); |
116 qed_goal "contlub_snd" Cprod3.thy "contlub(snd)" |
108 by (rtac monofun_fst 1); |
117 (fn prems => |
109 by (rtac contlub_fst 1); |
118 [ |
110 qed "cont_fst"; |
119 (rtac contlubI 1), |
111 |
120 (strip_tac 1), |
112 val prems = goal Cprod3.thy "cont(snd)"; |
121 (stac (lub_cprod RS thelubI) 1), |
113 by (rtac monocontlub2cont 1); |
122 (atac 1), |
114 by (rtac monofun_snd 1); |
123 (Simp_tac 1) |
115 by (rtac contlub_snd 1); |
124 ]); |
116 qed "cont_snd"; |
125 |
|
126 qed_goal "cont_fst" Cprod3.thy "cont(fst)" |
|
127 (fn prems => |
|
128 [ |
|
129 (rtac monocontlub2cont 1), |
|
130 (rtac monofun_fst 1), |
|
131 (rtac contlub_fst 1) |
|
132 ]); |
|
133 |
|
134 qed_goal "cont_snd" Cprod3.thy "cont(snd)" |
|
135 (fn prems => |
|
136 [ |
|
137 (rtac monocontlub2cont 1), |
|
138 (rtac monofun_snd 1), |
|
139 (rtac contlub_snd 1) |
|
140 ]); |
|
141 |
117 |
142 (* |
118 (* |
143 -------------------------------------------------------------------------- |
119 -------------------------------------------------------------------------- |
144 more lemmas for Cprod3.thy |
120 more lemmas for Cprod3.thy |
145 |
121 |
148 |
124 |
149 (* ------------------------------------------------------------------------ *) |
125 (* ------------------------------------------------------------------------ *) |
150 (* convert all lemmas to the continuous versions *) |
126 (* convert all lemmas to the continuous versions *) |
151 (* ------------------------------------------------------------------------ *) |
127 (* ------------------------------------------------------------------------ *) |
152 |
128 |
153 qed_goalw "beta_cfun_cprod" Cprod3.thy [cpair_def] |
129 val prems = goalw Cprod3.thy [cpair_def] |
154 "(LAM x y.(x,y))`a`b = (a,b)" |
130 "(LAM x y.(x,y))`a`b = (a,b)"; |
155 (fn prems => |
131 by (stac beta_cfun 1); |
156 [ |
132 by (simp_tac (simpset() addsimps [cont_pair1,cont_pair2,cont2cont_CF1L]) 1); |
157 (stac beta_cfun 1), |
133 by (stac beta_cfun 1); |
158 (simp_tac (simpset() addsimps [cont_pair1,cont_pair2,cont2cont_CF1L]) 1), |
134 by (rtac cont_pair2 1); |
159 (stac beta_cfun 1), |
135 by (rtac refl 1); |
160 (rtac cont_pair2 1), |
136 qed "beta_cfun_cprod"; |
161 (rtac refl 1) |
137 |
162 ]); |
138 val prems = goalw Cprod3.thy [cpair_def] |
163 |
139 " <a,b>=<aa,ba> ==> a=aa & b=ba"; |
164 qed_goalw "inject_cpair" Cprod3.thy [cpair_def] |
140 by (cut_facts_tac prems 1); |
165 " <a,b>=<aa,ba> ==> a=aa & b=ba" |
141 by (dtac (beta_cfun_cprod RS subst) 1); |
166 (fn prems => |
142 by (dtac (beta_cfun_cprod RS subst) 1); |
167 [ |
143 by (etac Pair_inject 1); |
168 (cut_facts_tac prems 1), |
144 by (fast_tac HOL_cs 1); |
169 (dtac (beta_cfun_cprod RS subst) 1), |
145 qed "inject_cpair"; |
170 (dtac (beta_cfun_cprod RS subst) 1), |
146 |
171 (etac Pair_inject 1), |
147 val prems = goalw Cprod3.thy [cpair_def] "UU = <UU,UU>"; |
172 (fast_tac HOL_cs 1) |
148 by (rtac sym 1); |
173 ]); |
149 by (rtac trans 1); |
174 |
150 by (rtac beta_cfun_cprod 1); |
175 qed_goalw "inst_cprod_pcpo2" Cprod3.thy [cpair_def] "UU = <UU,UU>" |
151 by (rtac sym 1); |
176 (fn prems => |
152 by (rtac inst_cprod_pcpo 1); |
177 [ |
153 qed "inst_cprod_pcpo2"; |
178 (rtac sym 1), |
154 |
179 (rtac trans 1), |
155 val prems = goal Cprod3.thy |
180 (rtac beta_cfun_cprod 1), |
156 "<a,b> = UU ==> a = UU & b = UU"; |
181 (rtac sym 1), |
157 by (cut_facts_tac prems 1); |
182 (rtac inst_cprod_pcpo 1) |
158 by (dtac (inst_cprod_pcpo2 RS subst) 1); |
183 ]); |
159 by (etac inject_cpair 1); |
184 |
160 qed "defined_cpair_rev"; |
185 qed_goal "defined_cpair_rev" Cprod3.thy |
161 |
186 "<a,b> = UU ==> a = UU & b = UU" |
162 val prems = goalw Cprod3.thy [cpair_def] |
187 (fn prems => |
163 "? a b. z=<a,b>"; |
188 [ |
164 by (rtac PairE 1); |
189 (cut_facts_tac prems 1), |
165 by (rtac exI 1); |
190 (dtac (inst_cprod_pcpo2 RS subst) 1), |
166 by (rtac exI 1); |
191 (etac inject_cpair 1) |
167 by (etac (beta_cfun_cprod RS ssubst) 1); |
192 ]); |
168 qed "Exh_Cprod2"; |
193 |
169 |
194 qed_goalw "Exh_Cprod2" Cprod3.thy [cpair_def] |
170 val prems = goalw Cprod3.thy [cpair_def] |
195 "? a b. z=<a,b>" |
171 "[|!!x y. [|p=<x,y> |] ==> Q|] ==> Q"; |
196 (fn prems => |
172 by (rtac PairE 1); |
197 [ |
173 by (resolve_tac prems 1); |
198 (rtac PairE 1), |
174 by (etac (beta_cfun_cprod RS ssubst) 1); |
199 (rtac exI 1), |
175 qed "cprodE"; |
200 (rtac exI 1), |
176 |
201 (etac (beta_cfun_cprod RS ssubst) 1) |
177 val prems = goalw Cprod3.thy [cfst_def,cpair_def] |
202 ]); |
178 "cfst`<x,y>=x"; |
203 |
179 by (cut_facts_tac prems 1); |
204 qed_goalw "cprodE" Cprod3.thy [cpair_def] |
180 by (stac beta_cfun_cprod 1); |
205 "[|!!x y. [|p=<x,y> |] ==> Q|] ==> Q" |
181 by (stac beta_cfun 1); |
206 (fn prems => |
182 by (rtac cont_fst 1); |
207 [ |
183 by (Simp_tac 1); |
208 (rtac PairE 1), |
184 qed "cfst2"; |
209 (resolve_tac prems 1), |
185 |
210 (etac (beta_cfun_cprod RS ssubst) 1) |
186 val prems = goalw Cprod3.thy [csnd_def,cpair_def] |
211 ]); |
187 "csnd`<x,y>=y"; |
212 |
188 by (cut_facts_tac prems 1); |
213 qed_goalw "cfst2" Cprod3.thy [cfst_def,cpair_def] |
189 by (stac beta_cfun_cprod 1); |
214 "cfst`<x,y>=x" |
190 by (stac beta_cfun 1); |
215 (fn prems => |
191 by (rtac cont_snd 1); |
216 [ |
192 by (Simp_tac 1); |
217 (cut_facts_tac prems 1), |
193 qed "csnd2"; |
218 (stac beta_cfun_cprod 1), |
194 |
219 (stac beta_cfun 1), |
195 val _ = goal Cprod3.thy "cfst`UU = UU"; |
220 (rtac cont_fst 1), |
196 by (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,cfst2]) 1); |
221 (Simp_tac 1) |
197 qed "cfst_strict"; |
222 ]); |
198 val _ = goal Cprod3.thy "csnd`UU = UU"; |
223 |
199 by (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,csnd2]) 1); |
224 qed_goalw "csnd2" Cprod3.thy [csnd_def,cpair_def] |
200 qed "csnd_strict"; |
225 "csnd`<x,y>=y" |
201 |
226 (fn prems => |
202 val prems = goalw Cprod3.thy [cfst_def,csnd_def,cpair_def] "<cfst`p , csnd`p> = p"; |
227 [ |
203 by (stac beta_cfun_cprod 1); |
228 (cut_facts_tac prems 1), |
204 by (stac beta_cfun 1); |
229 (stac beta_cfun_cprod 1), |
205 by (rtac cont_snd 1); |
230 (stac beta_cfun 1), |
206 by (stac beta_cfun 1); |
231 (rtac cont_snd 1), |
207 by (rtac cont_fst 1); |
232 (Simp_tac 1) |
208 by (rtac (surjective_pairing RS sym) 1); |
233 ]); |
209 qed "surjective_pairing_Cprod2"; |
234 |
210 |
235 qed_goal "cfst_strict" Cprod3.thy "cfst`UU = UU" (fn _ => [ |
211 val prems = goalw Cprod3.thy [cfst_def,csnd_def,cpair_def] |
236 (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,cfst2]) 1)]); |
212 "<xa,ya> << <x,y> ==> xa<<x & ya << y"; |
237 qed_goal "csnd_strict" Cprod3.thy "csnd`UU = UU" (fn _ => [ |
213 by (cut_facts_tac prems 1); |
238 (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,csnd2]) 1)]); |
214 by (rtac less_cprod4c 1); |
239 |
215 by (dtac (beta_cfun_cprod RS subst) 1); |
240 qed_goalw "surjective_pairing_Cprod2" Cprod3.thy |
216 by (dtac (beta_cfun_cprod RS subst) 1); |
241 [cfst_def,csnd_def,cpair_def] "<cfst`p , csnd`p> = p" |
217 by (atac 1); |
242 (fn prems => |
218 qed "less_cprod5c"; |
243 [ |
219 |
244 (stac beta_cfun_cprod 1), |
220 val prems = goalw Cprod3.thy [cfst_def,csnd_def,cpair_def] |
245 (stac beta_cfun 1), |
|
246 (rtac cont_snd 1), |
|
247 (stac beta_cfun 1), |
|
248 (rtac cont_fst 1), |
|
249 (rtac (surjective_pairing RS sym) 1) |
|
250 ]); |
|
251 |
|
252 qed_goalw "less_cprod5c" Cprod3.thy [cfst_def,csnd_def,cpair_def] |
|
253 "<xa,ya> << <x,y> ==> xa<<x & ya << y" |
|
254 (fn prems => |
|
255 [ |
|
256 (cut_facts_tac prems 1), |
|
257 (rtac less_cprod4c 1), |
|
258 (dtac (beta_cfun_cprod RS subst) 1), |
|
259 (dtac (beta_cfun_cprod RS subst) 1), |
|
260 (atac 1) |
|
261 ]); |
|
262 |
|
263 qed_goalw "lub_cprod2" Cprod3.thy [cfst_def,csnd_def,cpair_def] |
|
264 "[|chain(S)|] ==> range(S) <<| \ |
221 "[|chain(S)|] ==> range(S) <<| \ |
265 \ <(lub(range(%i. cfst`(S i)))) , lub(range(%i. csnd`(S i)))>" |
222 \ <(lub(range(%i. cfst`(S i)))) , lub(range(%i. csnd`(S i)))>"; |
266 (fn prems => |
223 by (cut_facts_tac prems 1); |
267 [ |
224 by (stac beta_cfun_cprod 1); |
268 (cut_facts_tac prems 1), |
225 by (stac (beta_cfun RS ext) 1); |
269 (stac beta_cfun_cprod 1), |
226 by (rtac cont_snd 1); |
270 (stac (beta_cfun RS ext) 1), |
227 by (stac (beta_cfun RS ext) 1); |
271 (rtac cont_snd 1), |
228 by (rtac cont_fst 1); |
272 (stac (beta_cfun RS ext) 1), |
229 by (rtac lub_cprod 1); |
273 (rtac cont_fst 1), |
230 by (atac 1); |
274 (rtac lub_cprod 1), |
231 qed "lub_cprod2"; |
275 (atac 1) |
|
276 ]); |
|
277 |
232 |
278 bind_thm ("thelub_cprod2", lub_cprod2 RS thelubI); |
233 bind_thm ("thelub_cprod2", lub_cprod2 RS thelubI); |
279 (* |
234 (* |
280 chain ?S1 ==> |
235 chain ?S1 ==> |
281 lub (range ?S1) = |
236 lub (range ?S1) = |
282 <lub (range (%i. cfst`(?S1 i))), lub (range (%i. csnd`(?S1 i)))>" |
237 <lub (range (%i. cfst`(?S1 i))), lub (range (%i. csnd`(?S1 i)))>" |
283 *) |
238 *) |
284 qed_goalw "csplit2" Cprod3.thy [csplit_def] |
239 val prems = goalw Cprod3.thy [csplit_def] |
285 "csplit`f`<x,y> = f`x`y" |
240 "csplit`f`<x,y> = f`x`y"; |
286 (fn prems => |
241 by (stac beta_cfun 1); |
287 [ |
242 by (Simp_tac 1); |
288 (stac beta_cfun 1), |
243 by (simp_tac (simpset() addsimps [cfst2,csnd2]) 1); |
289 (Simp_tac 1), |
244 qed "csplit2"; |
290 (simp_tac (simpset() addsimps [cfst2,csnd2]) 1) |
245 |
291 ]); |
246 val prems = goalw Cprod3.thy [csplit_def] |
292 |
247 "csplit`cpair`z=z"; |
293 qed_goalw "csplit3" Cprod3.thy [csplit_def] |
248 by (stac beta_cfun 1); |
294 "csplit`cpair`z=z" |
249 by (Simp_tac 1); |
295 (fn prems => |
250 by (simp_tac (simpset() addsimps [surjective_pairing_Cprod2]) 1); |
296 [ |
251 qed "csplit3"; |
297 (stac beta_cfun 1), |
|
298 (Simp_tac 1), |
|
299 (simp_tac (simpset() addsimps [surjective_pairing_Cprod2]) 1) |
|
300 ]); |
|
301 |
252 |
302 (* ------------------------------------------------------------------------ *) |
253 (* ------------------------------------------------------------------------ *) |
303 (* install simplifier for Cprod *) |
254 (* install simplifier for Cprod *) |
304 (* ------------------------------------------------------------------------ *) |
255 (* ------------------------------------------------------------------------ *) |
305 |
256 |