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