equal
deleted
inserted
replaced
1 (* Title: HOLCF/Discrete.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 *) |
|
5 |
|
6 Goalw [undiscr_def] "undiscr(Discr x) = x"; |
|
7 by (Simp_tac 1); |
|
8 qed "undiscr_Discr"; |
|
9 Addsimps [undiscr_Discr]; |
|
10 |
|
11 Goal |
|
12 "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"; |
|
13 by (fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1); |
|
14 qed "discr_chain_f_range0"; |
|
15 |
|
16 Goalw [cont,is_lub_def,is_ub_def] "cont(%x::('a::type)discr. f x)"; |
|
17 by (simp_tac (simpset() addsimps [discr_chain_f_range0]) 1); |
|
18 qed "cont_discr"; |
|
19 AddIffs [cont_discr]; |
|