equal
deleted
inserted
replaced
4 imports Abs_Int_init |
4 imports Abs_Int_init |
5 begin |
5 begin |
6 |
6 |
7 subsection "Orderings" |
7 subsection "Orderings" |
8 |
8 |
9 text{* The basic type classes @{class order}, @{class semilattice_sup} and @{class top} are |
9 text{* The basic type classes @{class order}, @{class semilattice_sup} and @{class order_top} are |
10 defined in @{theory Main}, more precisely in theories @{theory Orderings} and @{theory Lattices}. |
10 defined in @{theory Main}, more precisely in theories @{theory Orderings} and @{theory Lattices}. |
11 If you view this theory with jedit, just click on the names to get there. *} |
11 If you view this theory with jedit, just click on the names to get there. *} |
12 |
12 |
13 class semilattice_sup_top = semilattice_sup + top |
13 class semilattice_sup_top = semilattice_sup + order_top |
14 |
14 |
15 |
15 |
16 instance "fun" :: (type, semilattice_sup_top) semilattice_sup_top .. |
16 instance "fun" :: (type, semilattice_sup_top) semilattice_sup_top .. |
17 |
17 |
18 instantiation option :: (order)order |
18 instantiation option :: (order)order |
76 end |
76 end |
77 |
77 |
78 lemma [simp]: "(Some x < Some y) = (x < y)" |
78 lemma [simp]: "(Some x < Some y) = (x < y)" |
79 by(auto simp: less_le) |
79 by(auto simp: less_le) |
80 |
80 |
81 instantiation option :: (order)bot |
81 instantiation option :: (order)order_bot |
82 begin |
82 begin |
83 |
83 |
84 definition bot_option :: "'a option" where |
84 definition bot_option :: "'a option" where |
85 "\<bottom> = None" |
85 "\<bottom> = None" |
86 |
86 |