|
1 (* Title: HOLCF/porder.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for theory porder.thy |
|
7 *) |
|
8 |
|
9 open Porder; |
|
10 |
|
11 |
|
12 val box_less = prove_goal Porder.thy |
|
13 "[| a << b; c << a; b << d|] ==> c << d" |
|
14 (fn prems => |
|
15 [ |
|
16 (cut_facts_tac prems 1), |
|
17 (etac trans_less 1), |
|
18 (etac trans_less 1), |
|
19 (atac 1) |
|
20 ]); |
|
21 |
|
22 (* ------------------------------------------------------------------------ *) |
|
23 (* lubs are unique *) |
|
24 (* ------------------------------------------------------------------------ *) |
|
25 |
|
26 val unique_lub = prove_goalw Porder.thy [is_lub, is_ub] |
|
27 "[| S <<| x ; S <<| y |] ==> x=y" |
|
28 ( fn prems => |
|
29 [ |
|
30 (cut_facts_tac prems 1), |
|
31 (etac conjE 1), |
|
32 (etac conjE 1), |
|
33 (rtac antisym_less 1), |
|
34 (rtac mp 1),((etac allE 1) THEN (atac 1) THEN (atac 1)), |
|
35 (rtac mp 1),((etac allE 1) THEN (atac 1) THEN (atac 1)) |
|
36 ]); |
|
37 |
|
38 (* ------------------------------------------------------------------------ *) |
|
39 (* chains are monotone functions *) |
|
40 (* ------------------------------------------------------------------------ *) |
|
41 |
|
42 val chain_mono = prove_goalw Porder.thy [is_chain] |
|
43 " is_chain(F) ==> x<y --> F(x)<<F(y)" |
|
44 ( fn prems => |
|
45 [ |
|
46 (cut_facts_tac prems 1), |
|
47 (nat_ind_tac "y" 1), |
|
48 (rtac impI 1), |
|
49 (etac less_zeroE 1), |
|
50 (rtac (less_Suc_eq RS ssubst) 1), |
|
51 (strip_tac 1), |
|
52 (etac disjE 1), |
|
53 (rtac trans_less 1), |
|
54 (etac allE 2), |
|
55 (atac 2), |
|
56 (fast_tac HOL_cs 1), |
|
57 (hyp_subst_tac 1), |
|
58 (etac allE 1), |
|
59 (atac 1) |
|
60 ]); |
|
61 |
|
62 val chain_mono3 = prove_goal Porder.thy |
|
63 "[| is_chain(F); x <= y |] ==> F(x) << F(y)" |
|
64 (fn prems => |
|
65 [ |
|
66 (cut_facts_tac prems 1), |
|
67 (rtac (le_imp_less_or_eq RS disjE) 1), |
|
68 (atac 1), |
|
69 (etac (chain_mono RS mp) 1), |
|
70 (atac 1), |
|
71 (hyp_subst_tac 1), |
|
72 (rtac refl_less 1) |
|
73 ]); |
|
74 |
|
75 (* ------------------------------------------------------------------------ *) |
|
76 (* Lemma for reasoning by cases on the natural numbers *) |
|
77 (* ------------------------------------------------------------------------ *) |
|
78 |
|
79 val nat_less_cases = prove_goal Porder.thy |
|
80 "[| m::nat < n ==> P(n,m); m=n ==> P(n,m);n < m ==> P(n,m)|]==>P(n,m)" |
|
81 ( fn prems => |
|
82 [ |
|
83 (res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1), |
|
84 (etac disjE 2), |
|
85 (etac (hd (tl (tl prems))) 1), |
|
86 (etac (sym RS hd (tl prems)) 1), |
|
87 (etac (hd prems) 1) |
|
88 ]); |
|
89 |
|
90 (* ------------------------------------------------------------------------ *) |
|
91 (* The range of a chain is a totaly ordered << *) |
|
92 (* ------------------------------------------------------------------------ *) |
|
93 |
|
94 val chain_is_tord = prove_goalw Porder.thy [is_tord] |
|
95 "is_chain(F) ==> is_tord(range(F))" |
|
96 ( fn prems => |
|
97 [ |
|
98 (cut_facts_tac prems 1), |
|
99 (rewrite_goals_tac [range_def]), |
|
100 (rtac allI 1 ), |
|
101 (rtac allI 1 ), |
|
102 (rtac (mem_Collect_eq RS ssubst) 1), |
|
103 (rtac (mem_Collect_eq RS ssubst) 1), |
|
104 (strip_tac 1), |
|
105 (etac conjE 1), |
|
106 (etac exE 1), |
|
107 (etac exE 1), |
|
108 (hyp_subst_tac 1), |
|
109 (hyp_subst_tac 1), |
|
110 (res_inst_tac [("m","xa"),("n","xb")] (nat_less_cases) 1), |
|
111 (rtac disjI1 1), |
|
112 (rtac (chain_mono RS mp) 1), |
|
113 (atac 1), |
|
114 (atac 1), |
|
115 (rtac disjI1 1), |
|
116 (hyp_subst_tac 1), |
|
117 (rtac refl_less 1), |
|
118 (rtac disjI2 1), |
|
119 (rtac (chain_mono RS mp) 1), |
|
120 (atac 1), |
|
121 (atac 1) |
|
122 ]); |
|
123 |
|
124 |
|
125 (* ------------------------------------------------------------------------ *) |
|
126 (* technical lemmas about lub and is_lub, use above results about @ *) |
|
127 (* ------------------------------------------------------------------------ *) |
|
128 |
|
129 val lubI = prove_goal Porder.thy "(? x. M <<| x) ==> M <<| lub(M)" |
|
130 (fn prems => |
|
131 [ |
|
132 (cut_facts_tac prems 1), |
|
133 (rtac (lub RS ssubst) 1), |
|
134 (etac selectI2 1) |
|
135 ]); |
|
136 |
|
137 val lubE = prove_goal Porder.thy " M <<| lub(M) ==> ? x. M <<| x" |
|
138 (fn prems => |
|
139 [ |
|
140 (cut_facts_tac prems 1), |
|
141 (etac exI 1) |
|
142 ]); |
|
143 |
|
144 val lub_eq = prove_goal Porder.thy |
|
145 "(? x. M <<| x) = M <<| lub(M)" |
|
146 (fn prems => |
|
147 [ |
|
148 (rtac (lub RS ssubst) 1), |
|
149 (rtac (select_eq_Ex RS subst) 1), |
|
150 (rtac refl 1) |
|
151 ]); |
|
152 |
|
153 |
|
154 val thelubI = prove_goal Porder.thy " M <<| l ==> lub(M) = l" |
|
155 (fn prems => |
|
156 [ |
|
157 (cut_facts_tac prems 1), |
|
158 (rtac unique_lub 1), |
|
159 (rtac (lub RS ssubst) 1), |
|
160 (etac selectI 1), |
|
161 (atac 1) |
|
162 ]); |
|
163 |
|
164 |
|
165 (* ------------------------------------------------------------------------ *) |
|
166 (* access to some definition as inference rule *) |
|
167 (* ------------------------------------------------------------------------ *) |
|
168 |
|
169 val is_lubE = prove_goalw Porder.thy [is_lub] |
|
170 "S <<| x ==> S <| x & (! u. S <| u --> x << u)" |
|
171 (fn prems => |
|
172 [ |
|
173 (cut_facts_tac prems 1), |
|
174 (atac 1) |
|
175 ]); |
|
176 |
|
177 val is_lubI = prove_goalw Porder.thy [is_lub] |
|
178 "S <| x & (! u. S <| u --> x << u) ==> S <<| x" |
|
179 (fn prems => |
|
180 [ |
|
181 (cut_facts_tac prems 1), |
|
182 (atac 1) |
|
183 ]); |
|
184 |
|
185 val is_chainE = prove_goalw Porder.thy [is_chain] |
|
186 "is_chain(F) ==> ! i. F(i) << F(Suc(i))" |
|
187 (fn prems => |
|
188 [ |
|
189 (cut_facts_tac prems 1), |
|
190 (atac 1)]); |
|
191 |
|
192 val is_chainI = prove_goalw Porder.thy [is_chain] |
|
193 "! i. F(i) << F(Suc(i)) ==> is_chain(F) " |
|
194 (fn prems => |
|
195 [ |
|
196 (cut_facts_tac prems 1), |
|
197 (atac 1)]); |
|
198 |
|
199 (* ------------------------------------------------------------------------ *) |
|
200 (* technical lemmas about (least) upper bounds of chains *) |
|
201 (* ------------------------------------------------------------------------ *) |
|
202 |
|
203 val ub_rangeE = prove_goalw Porder.thy [is_ub] |
|
204 "range(S) <| x ==> ! i. S(i) << x" |
|
205 (fn prems => |
|
206 [ |
|
207 (cut_facts_tac prems 1), |
|
208 (strip_tac 1), |
|
209 (rtac mp 1), |
|
210 (etac spec 1), |
|
211 (rtac rangeI 1) |
|
212 ]); |
|
213 |
|
214 val ub_rangeI = prove_goalw Porder.thy [is_ub] |
|
215 "! i. S(i) << x ==> range(S) <| x" |
|
216 (fn prems => |
|
217 [ |
|
218 (cut_facts_tac prems 1), |
|
219 (strip_tac 1), |
|
220 (etac rangeE 1), |
|
221 (hyp_subst_tac 1), |
|
222 (etac spec 1) |
|
223 ]); |
|
224 |
|
225 val is_ub_lub = (is_lubE RS conjunct1 RS ub_rangeE RS spec); |
|
226 (* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1 *) |
|
227 |
|
228 val is_lub_lub = (is_lubE RS conjunct2 RS spec RS mp); |
|
229 (* [| ?S3 <<| ?x3; ?S3 <| ?x1 |] ==> ?x3 << ?x1 *) |
|
230 |
|
231 (* ------------------------------------------------------------------------ *) |
|
232 (* Prototype lemmas for class pcpo *) |
|
233 (* ------------------------------------------------------------------------ *) |
|
234 |
|
235 (* ------------------------------------------------------------------------ *) |
|
236 (* a technical argument about << on void *) |
|
237 (* ------------------------------------------------------------------------ *) |
|
238 |
|
239 val less_void = prove_goal Porder.thy "(u1::void << u2) = (u1 = u2)" |
|
240 (fn prems => |
|
241 [ |
|
242 (rtac (inst_void_po RS ssubst) 1), |
|
243 (rewrite_goals_tac [less_void_def]), |
|
244 (rtac iffI 1), |
|
245 (rtac injD 1), |
|
246 (atac 2), |
|
247 (rtac inj_inverseI 1), |
|
248 (rtac Rep_Void_inverse 1), |
|
249 (etac arg_cong 1) |
|
250 ]); |
|
251 |
|
252 (* ------------------------------------------------------------------------ *) |
|
253 (* void is pointed. The least element is UU_void *) |
|
254 (* ------------------------------------------------------------------------ *) |
|
255 |
|
256 val minimal_void = prove_goal Porder.thy "UU_void << x" |
|
257 (fn prems => |
|
258 [ |
|
259 (rtac (inst_void_po RS ssubst) 1), |
|
260 (rewrite_goals_tac [less_void_def]), |
|
261 (simp_tac (HOL_ss addsimps [unique_void]) 1) |
|
262 ]); |
|
263 |
|
264 (* ------------------------------------------------------------------------ *) |
|
265 (* UU_void is the trivial lub of all chains in void *) |
|
266 (* ------------------------------------------------------------------------ *) |
|
267 |
|
268 val lub_void = prove_goalw Porder.thy [is_lub] "M <<| UU_void" |
|
269 (fn prems => |
|
270 [ |
|
271 (rtac conjI 1), |
|
272 (rewrite_goals_tac [is_ub]), |
|
273 (strip_tac 1), |
|
274 (rtac (inst_void_po RS ssubst) 1), |
|
275 (rewrite_goals_tac [less_void_def]), |
|
276 (simp_tac (HOL_ss addsimps [unique_void]) 1), |
|
277 (strip_tac 1), |
|
278 (rtac minimal_void 1) |
|
279 ]); |
|
280 |
|
281 (* ------------------------------------------------------------------------ *) |
|
282 (* lub(?M) = UU_void *) |
|
283 (* ------------------------------------------------------------------------ *) |
|
284 |
|
285 val thelub_void = (lub_void RS thelubI); |
|
286 |
|
287 (* ------------------------------------------------------------------------ *) |
|
288 (* void is a cpo wrt. countable chains *) |
|
289 (* ------------------------------------------------------------------------ *) |
|
290 |
|
291 val cpo_void = prove_goal Porder.thy |
|
292 "is_chain(S::nat=>void) ==> ? x. range(S) <<| x " |
|
293 (fn prems => |
|
294 [ |
|
295 (cut_facts_tac prems 1), |
|
296 (res_inst_tac [("x","UU_void")] exI 1), |
|
297 (rtac lub_void 1) |
|
298 ]); |
|
299 |
|
300 (* ------------------------------------------------------------------------ *) |
|
301 (* end of prototype lemmas for class pcpo *) |
|
302 (* ------------------------------------------------------------------------ *) |
|
303 |
|
304 |
|
305 (* ------------------------------------------------------------------------ *) |
|
306 (* the reverse law of anti--symmetrie of << *) |
|
307 (* ------------------------------------------------------------------------ *) |
|
308 |
|
309 val antisym_less_inverse = prove_goal Porder.thy "x=y ==> x << y & y << x" |
|
310 (fn prems => |
|
311 [ |
|
312 (cut_facts_tac prems 1), |
|
313 (rtac conjI 1), |
|
314 ((rtac subst 1) THEN (rtac refl_less 2) THEN (atac 1)), |
|
315 ((rtac subst 1) THEN (rtac refl_less 2) THEN (etac sym 1)) |
|
316 ]); |
|
317 |
|
318 (* ------------------------------------------------------------------------ *) |
|
319 (* results about finite chains *) |
|
320 (* ------------------------------------------------------------------------ *) |
|
321 |
|
322 val lub_finch1 = prove_goalw Porder.thy [max_in_chain_def] |
|
323 "[| is_chain(C) ; max_in_chain(i,C)|] ==> range(C) <<| C(i)" |
|
324 (fn prems => |
|
325 [ |
|
326 (cut_facts_tac prems 1), |
|
327 (rtac is_lubI 1), |
|
328 (rtac conjI 1), |
|
329 (rtac ub_rangeI 1), |
|
330 (rtac allI 1), |
|
331 (res_inst_tac [("m","i")] nat_less_cases 1), |
|
332 (rtac (antisym_less_inverse RS conjunct2) 1), |
|
333 (etac (disjI1 RS less_or_eq_imp_le RS rev_mp) 1), |
|
334 (etac spec 1), |
|
335 (rtac (antisym_less_inverse RS conjunct2) 1), |
|
336 (etac (disjI2 RS less_or_eq_imp_le RS rev_mp) 1), |
|
337 (etac spec 1), |
|
338 (etac (chain_mono RS mp) 1), |
|
339 (atac 1), |
|
340 (strip_tac 1), |
|
341 (etac (ub_rangeE RS spec) 1) |
|
342 ]); |
|
343 |
|
344 val lub_finch2 = prove_goalw Porder.thy [finite_chain_def] |
|
345 "finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain(i,C))" |
|
346 (fn prems=> |
|
347 [ |
|
348 (cut_facts_tac prems 1), |
|
349 (rtac lub_finch1 1), |
|
350 (etac conjunct1 1), |
|
351 (rtac selectI2 1), |
|
352 (etac conjunct2 1) |
|
353 ]); |
|
354 |
|
355 |
|
356 val bin_chain = prove_goal Porder.thy "x<<y ==> is_chain(%i. if(i=0,x,y))" |
|
357 (fn prems => |
|
358 [ |
|
359 (cut_facts_tac prems 1), |
|
360 (rtac is_chainI 1), |
|
361 (rtac allI 1), |
|
362 (nat_ind_tac "i" 1), |
|
363 (asm_simp_tac nat_ss 1), |
|
364 (asm_simp_tac nat_ss 1), |
|
365 (rtac refl_less 1) |
|
366 ]); |
|
367 |
|
368 val bin_chainmax = prove_goalw Porder.thy [max_in_chain_def,le_def] |
|
369 "x<<y ==> max_in_chain(Suc(0),%i. if(i=0,x,y))" |
|
370 (fn prems => |
|
371 [ |
|
372 (cut_facts_tac prems 1), |
|
373 (rtac allI 1), |
|
374 (nat_ind_tac "j" 1), |
|
375 (asm_simp_tac nat_ss 1), |
|
376 (asm_simp_tac nat_ss 1) |
|
377 ]); |
|
378 |
|
379 val lub_bin_chain = prove_goal Porder.thy |
|
380 "x << y ==> range(%i. if(i = 0,x,y)) <<| y" |
|
381 (fn prems=> |
|
382 [ (cut_facts_tac prems 1), |
|
383 (res_inst_tac [("s","if(Suc(0) = 0,x,y)")] subst 1), |
|
384 (rtac lub_finch1 2), |
|
385 (etac bin_chain 2), |
|
386 (etac bin_chainmax 2), |
|
387 (simp_tac nat_ss 1) |
|
388 ]); |
|
389 |
|
390 (* ------------------------------------------------------------------------ *) |
|
391 (* the maximal element in a chain is its lub *) |
|
392 (* ------------------------------------------------------------------------ *) |
|
393 |
|
394 val lub_chain_maxelem = prove_goal Porder.thy |
|
395 "[|is_chain(Y);? i.Y(i)=c;!i.Y(i)<<c|] ==> lub(range(Y)) = c" |
|
396 (fn prems => |
|
397 [ |
|
398 (cut_facts_tac prems 1), |
|
399 (rtac thelubI 1), |
|
400 (rtac is_lubI 1), |
|
401 (rtac conjI 1), |
|
402 (etac ub_rangeI 1), |
|
403 (strip_tac 1), |
|
404 (res_inst_tac [("P","%i.Y(i)=c")] exE 1), |
|
405 (atac 1), |
|
406 (hyp_subst_tac 1), |
|
407 (etac (ub_rangeE RS spec) 1) |
|
408 ]); |
|
409 |
|
410 (* ------------------------------------------------------------------------ *) |
|
411 (* the lub of a constant chain is the constant *) |
|
412 (* ------------------------------------------------------------------------ *) |
|
413 |
|
414 val lub_const = prove_goal Porder.thy "range(%x.c) <<| c" |
|
415 (fn prems => |
|
416 [ |
|
417 (rtac is_lubI 1), |
|
418 (rtac conjI 1), |
|
419 (rtac ub_rangeI 1), |
|
420 (strip_tac 1), |
|
421 (rtac refl_less 1), |
|
422 (strip_tac 1), |
|
423 (etac (ub_rangeE RS spec) 1) |
|
424 ]); |
|
425 |
|
426 |
|
427 |