1 (* Title: HOLCF/Discrete.thy |
1 (* Title: HOLCF/Discrete.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 |
5 |
5 Discrete CPOs. |
6 Discrete CPOs. |
6 *) |
7 *) |
7 |
8 |
8 Discrete = Discrete1 + |
9 theory Discrete |
|
10 imports Cont Datatype |
|
11 begin |
9 |
12 |
10 instance discr :: (type)cpo (discr_cpo) |
13 datatype 'a discr = Discr "'a :: type" |
|
14 |
|
15 instance discr :: (type) sq_ord .. |
|
16 |
|
17 defs (overloaded) |
|
18 less_discr_def: "((op <<)::('a::type)discr=>'a discr=>bool) == op =" |
|
19 |
|
20 lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)" |
|
21 apply (unfold less_discr_def) |
|
22 apply (rule refl) |
|
23 done |
|
24 |
|
25 instance discr :: (type) po |
|
26 proof |
|
27 fix x y z :: "'a discr" |
|
28 show "x << x" by simp |
|
29 { assume "x << y" and "y << x" thus "x = y" by simp } |
|
30 { assume "x << y" and "y << z" thus "x << z" by simp } |
|
31 qed |
|
32 |
|
33 lemma discr_chain0: |
|
34 "!!S::nat=>('a::type)discr. chain S ==> S i = S 0" |
|
35 apply (unfold chain_def) |
|
36 apply (induct_tac "i") |
|
37 apply (rule refl) |
|
38 apply (erule subst) |
|
39 apply (rule sym) |
|
40 apply fast |
|
41 done |
|
42 |
|
43 lemma discr_chain_range0: |
|
44 "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}" |
|
45 apply (fast elim: discr_chain0) |
|
46 done |
|
47 declare discr_chain_range0 [simp] |
|
48 |
|
49 lemma discr_cpo: |
|
50 "!!S. chain S ==> ? x::('a::type)discr. range(S) <<| x" |
|
51 apply (unfold is_lub_def is_ub_def) |
|
52 apply (simp (no_asm_simp)) |
|
53 done |
|
54 |
|
55 instance discr :: (type)cpo |
|
56 by (intro_classes, rule discr_cpo) |
11 |
57 |
12 constdefs |
58 constdefs |
13 undiscr :: ('a::type)discr => 'a |
59 undiscr :: "('a::type)discr => 'a" |
14 "undiscr x == (case x of Discr y => y)" |
60 "undiscr x == (case x of Discr y => y)" |
15 |
61 |
|
62 lemma undiscr_Discr [simp]: "undiscr(Discr x) = x" |
|
63 apply (unfold undiscr_def) |
|
64 apply (simp (no_asm)) |
|
65 done |
|
66 |
|
67 lemma discr_chain_f_range0: |
|
68 "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}" |
|
69 apply (fast dest: discr_chain0 elim: arg_cong) |
|
70 done |
|
71 |
|
72 lemma cont_discr [iff]: "cont(%x::('a::type)discr. f x)" |
|
73 apply (unfold cont is_lub_def is_ub_def) |
|
74 apply (simp (no_asm) add: discr_chain_f_range0) |
|
75 done |
|
76 |
16 end |
77 end |