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