equal
deleted
inserted
replaced
3 Id: $Id$ |
3 Id: $Id$ |
4 Author: Clemens Ballarin, started 7 November 2003 |
4 Author: Clemens Ballarin, started 7 November 2003 |
5 Copyright: Clemens Ballarin |
5 Copyright: Clemens Ballarin |
6 *) |
6 *) |
7 |
7 |
8 header {* Orders and Lattices *} |
|
9 |
|
10 theory Lattice imports Main begin |
8 theory Lattice imports Main begin |
|
9 |
|
10 |
|
11 section {* Orders and Lattices *} |
11 |
12 |
12 text {* Object with a carrier set. *} |
13 text {* Object with a carrier set. *} |
13 |
14 |
14 record 'a partial_object = |
15 record 'a partial_object = |
15 carrier :: "'a set" |
16 carrier :: "'a set" |
|
17 |
16 |
18 |
17 subsection {* Partial Orders *} |
19 subsection {* Partial Orders *} |
18 |
20 |
19 record 'a order = "'a partial_object" + |
21 record 'a order = "'a partial_object" + |
20 le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50) |
22 le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50) |
820 qed |
822 qed |
821 qed |
823 qed |
822 |
824 |
823 (* TODO: prove dual version *) |
825 (* TODO: prove dual version *) |
824 |
826 |
|
827 |
825 subsection {* Examples *} |
828 subsection {* Examples *} |
826 |
829 |
827 subsubsection {* Powerset of a set is a complete lattice *} |
830 subsubsection {* Powerset of a Set is a Complete Lattice *} |
828 |
831 |
829 theorem powerset_is_complete_lattice: |
832 theorem powerset_is_complete_lattice: |
830 "complete_lattice (| carrier = Pow A, le = op \<subseteq> |)" |
833 "complete_lattice (| carrier = Pow A, le = op \<subseteq> |)" |
831 (is "complete_lattice ?L") |
834 (is "complete_lattice ?L") |
832 proof (rule partial_order.complete_latticeI) |
835 proof (rule partial_order.complete_latticeI) |