49 |
49 |
50 lemma discr_chain_range0 [simp]: |
50 lemma discr_chain_range0 [simp]: |
51 "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}" |
51 "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}" |
52 by (fast elim: discr_chain0) |
52 by (fast elim: discr_chain0) |
53 |
53 |
54 lemma discr_directed_lemma: |
|
55 fixes S :: "'a::type discr set" |
|
56 assumes S: "directed S" |
|
57 shows "\<exists>x. S = {x}" |
|
58 proof - |
|
59 obtain x where x: "x \<in> S" |
|
60 using S by (rule directedE1) |
|
61 hence "S = {x}" |
|
62 proof (safe) |
|
63 fix y assume y: "y \<in> S" |
|
64 obtain z where "x \<sqsubseteq> z" "y \<sqsubseteq> z" |
|
65 using S x y by (rule directedE2) |
|
66 thus "y = x" by simp |
|
67 qed |
|
68 thus "\<exists>x. S = {x}" .. |
|
69 qed |
|
70 |
|
71 instance discr :: (type) dcpo |
|
72 proof |
|
73 fix S :: "'a discr set" |
|
74 assume "directed S" |
|
75 hence "\<exists>x. S = {x}" by (rule discr_directed_lemma) |
|
76 thus "\<exists>x. S <<| x" by (fast intro: is_lub_singleton) |
|
77 qed |
|
78 |
|
79 instance discr :: (finite) finite_po |
54 instance discr :: (finite) finite_po |
80 proof |
55 proof |
81 have "finite (Discr ` (UNIV :: 'a set))" |
56 have "finite (Discr ` (UNIV :: 'a set))" |
82 by (rule finite_imageI [OF finite]) |
57 by (rule finite_imageI [OF finite]) |
83 also have "(Discr ` (UNIV :: 'a set)) = UNIV" |
58 also have "(Discr ` (UNIV :: 'a set)) = UNIV" |