equal
deleted
inserted
replaced
7 |
7 |
8 theory SetPcpo |
8 theory SetPcpo |
9 imports Adm |
9 imports Adm |
10 begin |
10 begin |
11 |
11 |
12 instantiation set :: (type) sq_ord |
12 instantiation set :: (type) po |
13 begin |
13 begin |
14 |
14 |
15 definition |
15 definition |
16 less_set_def: "(op \<sqsubseteq>) = (op \<subseteq>)" |
16 less_set_def: "(op \<sqsubseteq>) = (op \<subseteq>)" |
17 |
17 |
18 instance .. |
18 instance |
|
19 by (intro_classes, auto simp add: less_set_def) |
|
20 |
19 end |
21 end |
20 |
|
21 instance set :: (type) po |
|
22 by (intro_classes, auto simp add: less_set_def) |
|
23 |
22 |
24 instance set :: (finite) finite_po .. |
23 instance set :: (finite) finite_po .. |
25 |
24 |
26 lemma Union_is_lub: "A <<| Union A" |
25 lemma Union_is_lub: "A <<| Union A" |
27 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 |