equal
deleted
inserted
replaced
1 (* Title: HOLCF/Discrete1.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 |
|
5 Proves that 'a discr is a cpo |
|
6 *) |
|
7 |
|
8 Goalw [less_discr_def] "((x::('a::type)discr) << y) = (x=y)"; |
|
9 by (rtac refl 1); |
|
10 qed "discr_less_eq"; |
|
11 AddIffs [discr_less_eq]; |
|
12 |
|
13 Goalw [chain_def] |
|
14 "!!S::nat=>('a::type)discr. chain S ==> S i = S 0"; |
|
15 by (induct_tac "i" 1); |
|
16 by (rtac refl 1); |
|
17 by (etac subst 1); |
|
18 by (rtac sym 1); |
|
19 by (Fast_tac 1); |
|
20 qed "discr_chain0"; |
|
21 |
|
22 Goal |
|
23 "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"; |
|
24 by (fast_tac (claset() addEs [discr_chain0]) 1); |
|
25 qed "discr_chain_range0"; |
|
26 Addsimps [discr_chain_range0]; |
|
27 |
|
28 Goalw [is_lub_def,is_ub_def] |
|
29 "!!S. chain S ==> ? x::('a::type)discr. range(S) <<| x"; |
|
30 by (Asm_simp_tac 1); |
|
31 qed "discr_cpo"; |
|