1 (* Title: HOLCF/pcpo.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for pcpo.thy |
|
7 *) |
|
8 |
|
9 open Pcpo; |
|
10 |
|
11 (* ------------------------------------------------------------------------ *) |
|
12 (* in pcpo's everthing equal to THE lub has lub properties for every chain *) |
|
13 (* ------------------------------------------------------------------------ *) |
|
14 |
|
15 val thelubE = prove_goal Pcpo.thy |
|
16 "[| is_chain(S);lub(range(S)) = l::'a::pcpo|] ==> range(S) <<| l " |
|
17 (fn prems => |
|
18 [ |
|
19 (cut_facts_tac prems 1), |
|
20 (hyp_subst_tac 1), |
|
21 (rtac lubI 1), |
|
22 (etac cpo 1) |
|
23 ]); |
|
24 |
|
25 (* ------------------------------------------------------------------------ *) |
|
26 (* Properties of the lub *) |
|
27 (* ------------------------------------------------------------------------ *) |
|
28 |
|
29 |
|
30 val is_ub_thelub = (cpo RS lubI RS is_ub_lub); |
|
31 (* is_chain(?S1) ==> ?S1(?x) << lub(range(?S1)) *) |
|
32 |
|
33 val is_lub_thelub = (cpo RS lubI RS is_lub_lub); |
|
34 (* [| is_chain(?S5); range(?S5) <| ?x1 |] ==> lub(range(?S5)) << ?x1 *) |
|
35 |
|
36 |
|
37 (* ------------------------------------------------------------------------ *) |
|
38 (* the << relation between two chains is preserved by their lubs *) |
|
39 (* ------------------------------------------------------------------------ *) |
|
40 |
|
41 val lub_mono = prove_goal Pcpo.thy |
|
42 "[|is_chain(C1::(nat=>'a::pcpo));is_chain(C2); ! k. C1(k) << C2(k)|]\ |
|
43 \ ==> lub(range(C1)) << lub(range(C2))" |
|
44 (fn prems => |
|
45 [ |
|
46 (cut_facts_tac prems 1), |
|
47 (etac is_lub_thelub 1), |
|
48 (rtac ub_rangeI 1), |
|
49 (rtac allI 1), |
|
50 (rtac trans_less 1), |
|
51 (etac spec 1), |
|
52 (etac is_ub_thelub 1) |
|
53 ]); |
|
54 |
|
55 (* ------------------------------------------------------------------------ *) |
|
56 (* the = relation between two chains is preserved by their lubs *) |
|
57 (* ------------------------------------------------------------------------ *) |
|
58 |
|
59 val lub_equal = prove_goal Pcpo.thy |
|
60 "[| is_chain(C1::(nat=>'a::pcpo));is_chain(C2);!k.C1(k)=C2(k)|]\ |
|
61 \ ==> lub(range(C1))=lub(range(C2))" |
|
62 (fn prems => |
|
63 [ |
|
64 (cut_facts_tac prems 1), |
|
65 (rtac antisym_less 1), |
|
66 (rtac lub_mono 1), |
|
67 (atac 1), |
|
68 (atac 1), |
|
69 (strip_tac 1), |
|
70 (rtac (antisym_less_inverse RS conjunct1) 1), |
|
71 (etac spec 1), |
|
72 (rtac lub_mono 1), |
|
73 (atac 1), |
|
74 (atac 1), |
|
75 (strip_tac 1), |
|
76 (rtac (antisym_less_inverse RS conjunct2) 1), |
|
77 (etac spec 1) |
|
78 ]); |
|
79 |
|
80 (* ------------------------------------------------------------------------ *) |
|
81 (* more results about mono and = of lubs of chains *) |
|
82 (* ------------------------------------------------------------------------ *) |
|
83 |
|
84 val lub_mono2 = prove_goal Pcpo.thy |
|
85 "[|? j.!i. j<i --> X(i::nat)=Y(i);is_chain(X::nat=>'a::pcpo);is_chain(Y)|]\ |
|
86 \ ==> lub(range(X))<<lub(range(Y))" |
|
87 (fn prems => |
|
88 [ |
|
89 (rtac exE 1), |
|
90 (resolve_tac prems 1), |
|
91 (rtac is_lub_thelub 1), |
|
92 (resolve_tac prems 1), |
|
93 (rtac ub_rangeI 1), |
|
94 (strip_tac 1), |
|
95 (res_inst_tac [("Q","x<i")] classical2 1), |
|
96 (res_inst_tac [("s","Y(i)"),("t","X(i)")] subst 1), |
|
97 (rtac sym 1), |
|
98 (fast_tac HOL_cs 1), |
|
99 (rtac is_ub_thelub 1), |
|
100 (resolve_tac prems 1), |
|
101 (res_inst_tac [("y","X(Suc(x))")] trans_less 1), |
|
102 (rtac (chain_mono RS mp) 1), |
|
103 (resolve_tac prems 1), |
|
104 (rtac (not_less_eq RS subst) 1), |
|
105 (atac 1), |
|
106 (res_inst_tac [("s","Y(Suc(x))"),("t","X(Suc(x))")] subst 1), |
|
107 (rtac sym 1), |
|
108 (asm_simp_tac nat_ss 1), |
|
109 (rtac is_ub_thelub 1), |
|
110 (resolve_tac prems 1) |
|
111 ]); |
|
112 |
|
113 val lub_equal2 = prove_goal Pcpo.thy |
|
114 "[|? j.!i. j<i --> X(i)=Y(i);is_chain(X::nat=>'a::pcpo);is_chain(Y)|]\ |
|
115 \ ==> lub(range(X))=lub(range(Y))" |
|
116 (fn prems => |
|
117 [ |
|
118 (rtac antisym_less 1), |
|
119 (rtac lub_mono2 1), |
|
120 (REPEAT (resolve_tac prems 1)), |
|
121 (cut_facts_tac prems 1), |
|
122 (rtac lub_mono2 1), |
|
123 (safe_tac HOL_cs), |
|
124 (step_tac HOL_cs 1), |
|
125 (safe_tac HOL_cs), |
|
126 (rtac sym 1), |
|
127 (fast_tac HOL_cs 1) |
|
128 ]); |
|
129 |
|
130 val lub_mono3 = prove_goal Pcpo.thy "[|is_chain(Y::nat=>'a::pcpo);is_chain(X);\ |
|
131 \! i. ? j. Y(i)<< X(j)|]==> lub(range(Y))<<lub(range(X))" |
|
132 (fn prems => |
|
133 [ |
|
134 (cut_facts_tac prems 1), |
|
135 (rtac is_lub_thelub 1), |
|
136 (atac 1), |
|
137 (rtac ub_rangeI 1), |
|
138 (strip_tac 1), |
|
139 (etac allE 1), |
|
140 (etac exE 1), |
|
141 (rtac trans_less 1), |
|
142 (rtac is_ub_thelub 2), |
|
143 (atac 2), |
|
144 (atac 1) |
|
145 ]); |
|
146 |
|
147 (* ------------------------------------------------------------------------ *) |
|
148 (* usefull lemmas about UU *) |
|
149 (* ------------------------------------------------------------------------ *) |
|
150 |
|
151 val eq_UU_iff = prove_goal Pcpo.thy "(x=UU)=(x<<UU)" |
|
152 (fn prems => |
|
153 [ |
|
154 (rtac iffI 1), |
|
155 (hyp_subst_tac 1), |
|
156 (rtac refl_less 1), |
|
157 (rtac antisym_less 1), |
|
158 (atac 1), |
|
159 (rtac minimal 1) |
|
160 ]); |
|
161 |
|
162 val UU_I = prove_goal Pcpo.thy "x << UU ==> x = UU" |
|
163 (fn prems => |
|
164 [ |
|
165 (rtac (eq_UU_iff RS ssubst) 1), |
|
166 (resolve_tac prems 1) |
|
167 ]); |
|
168 |
|
169 val not_less2not_eq = prove_goal Pcpo.thy "~x<<y ==> ~x=y" |
|
170 (fn prems => |
|
171 [ |
|
172 (cut_facts_tac prems 1), |
|
173 (rtac classical3 1), |
|
174 (atac 1), |
|
175 (hyp_subst_tac 1), |
|
176 (rtac refl_less 1) |
|
177 ]); |
|
178 |
|
179 |
|
180 val chain_UU_I = prove_goal Pcpo.thy |
|
181 "[|is_chain(Y);lub(range(Y))=UU|] ==> ! i.Y(i)=UU" |
|
182 (fn prems => |
|
183 [ |
|
184 (cut_facts_tac prems 1), |
|
185 (rtac allI 1), |
|
186 (rtac antisym_less 1), |
|
187 (rtac minimal 2), |
|
188 (res_inst_tac [("t","UU")] subst 1), |
|
189 (atac 1), |
|
190 (etac is_ub_thelub 1) |
|
191 ]); |
|
192 |
|
193 |
|
194 val chain_UU_I_inverse = prove_goal Pcpo.thy |
|
195 "!i.Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU" |
|
196 (fn prems => |
|
197 [ |
|
198 (cut_facts_tac prems 1), |
|
199 (rtac lub_chain_maxelem 1), |
|
200 (rtac is_chainI 1), |
|
201 (rtac allI 1), |
|
202 (res_inst_tac [("s","UU"),("t","Y(i)")] subst 1), |
|
203 (rtac sym 1), |
|
204 (etac spec 1), |
|
205 (rtac minimal 1), |
|
206 (rtac exI 1), |
|
207 (etac spec 1), |
|
208 (rtac allI 1), |
|
209 (rtac (antisym_less_inverse RS conjunct1) 1), |
|
210 (etac spec 1) |
|
211 ]); |
|
212 |
|
213 val chain_UU_I_inverse2 = prove_goal Pcpo.thy |
|
214 "~lub(range(Y::(nat=>'a::pcpo)))=UU ==> ? i.~ Y(i)=UU" |
|
215 (fn prems => |
|
216 [ |
|
217 (cut_facts_tac prems 1), |
|
218 (rtac (notall2ex RS iffD1) 1), |
|
219 (rtac swap 1), |
|
220 (rtac chain_UU_I_inverse 2), |
|
221 (etac notnotD 2), |
|
222 (atac 1) |
|
223 ]); |
|
224 |
|
225 |
|
226 val notUU_I = prove_goal Pcpo.thy "[| x<<y; ~x=UU |] ==> ~y=UU" |
|
227 (fn prems => |
|
228 [ |
|
229 (cut_facts_tac prems 1), |
|
230 (etac contrapos 1), |
|
231 (rtac UU_I 1), |
|
232 (hyp_subst_tac 1), |
|
233 (atac 1) |
|
234 ]); |
|
235 |
|
236 |
|
237 val chain_mono2 = prove_goal Pcpo.thy |
|
238 "[|? j.~Y(j)=UU;is_chain(Y::nat=>'a::pcpo)|]\ |
|
239 \ ==> ? j.!i.j<i-->~Y(i)=UU" |
|
240 (fn prems => |
|
241 [ |
|
242 (cut_facts_tac prems 1), |
|
243 (safe_tac HOL_cs), |
|
244 (step_tac HOL_cs 1), |
|
245 (strip_tac 1), |
|
246 (rtac notUU_I 1), |
|
247 (atac 2), |
|
248 (etac (chain_mono RS mp) 1), |
|
249 (atac 1) |
|
250 ]); |
|
251 |
|
252 |
|
253 |
|
254 |
|
255 (* ------------------------------------------------------------------------ *) |
|
256 (* uniqueness in void *) |
|
257 (* ------------------------------------------------------------------------ *) |
|
258 |
|
259 val unique_void2 = prove_goal Pcpo.thy "x::void=UU" |
|
260 (fn prems => |
|
261 [ |
|
262 (rtac (inst_void_pcpo RS ssubst) 1), |
|
263 (rtac (Rep_Void_inverse RS subst) 1), |
|
264 (rtac (Rep_Void_inverse RS subst) 1), |
|
265 (rtac arg_cong 1), |
|
266 (rtac box_equals 1), |
|
267 (rtac refl 1), |
|
268 (rtac (unique_void RS sym) 1), |
|
269 (rtac (unique_void RS sym) 1) |
|
270 ]); |
|
271 |
|
272 |
|