equal
deleted
inserted
replaced
23 instance set :: (finite) finite_po .. |
23 instance set :: (finite) finite_po .. |
24 |
24 |
25 lemma Union_is_lub: "A <<| Union A" |
25 lemma Union_is_lub: "A <<| Union A" |
26 unfolding is_lub_def is_ub_def less_set_def by fast |
26 unfolding is_lub_def is_ub_def less_set_def by fast |
27 |
27 |
28 instance set :: (type) dcpo |
28 instance set :: (type) cpo |
29 by (intro_classes, rule exI, rule Union_is_lub) |
29 by (intro_classes, rule exI, rule Union_is_lub) |
30 |
30 |
31 lemma lub_eq_Union: "lub = Union" |
31 lemma lub_eq_Union: "lub = Union" |
32 by (rule ext, rule thelubI [OF Union_is_lub]) |
32 by (rule ext, rule thelubI [OF Union_is_lub]) |
33 |
33 |