19 record 'a potype = |
19 record 'a potype = |
20 pset :: "'a set" |
20 pset :: "'a set" |
21 order :: "('a * 'a) set" |
21 order :: "('a * 'a) set" |
22 |
22 |
23 definition |
23 definition |
24 monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool" |
24 monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool" where |
25 "monotone f A r = (\<forall>x\<in>A. \<forall>y\<in>A. (x, y): r --> ((f x), (f y)) : r)" |
25 "monotone f A r = (\<forall>x\<in>A. \<forall>y\<in>A. (x, y): r --> ((f x), (f y)) : r)" |
26 |
26 |
27 least :: "['a => bool, 'a potype] => 'a" |
27 definition |
|
28 least :: "['a => bool, 'a potype] => 'a" where |
28 "least P po = (SOME x. x: pset po & P x & |
29 "least P po = (SOME x. x: pset po & P x & |
29 (\<forall>y \<in> pset po. P y --> (x,y): order po))" |
30 (\<forall>y \<in> pset po. P y --> (x,y): order po))" |
30 |
31 |
31 greatest :: "['a => bool, 'a potype] => 'a" |
32 definition |
|
33 greatest :: "['a => bool, 'a potype] => 'a" where |
32 "greatest P po = (SOME x. x: pset po & P x & |
34 "greatest P po = (SOME x. x: pset po & P x & |
33 (\<forall>y \<in> pset po. P y --> (y,x): order po))" |
35 (\<forall>y \<in> pset po. P y --> (y,x): order po))" |
34 |
36 |
35 lub :: "['a set, 'a potype] => 'a" |
37 definition |
|
38 lub :: "['a set, 'a potype] => 'a" where |
36 "lub S po = least (%x. \<forall>y\<in>S. (y,x): order po) po" |
39 "lub S po = least (%x. \<forall>y\<in>S. (y,x): order po) po" |
37 |
40 |
38 glb :: "['a set, 'a potype] => 'a" |
41 definition |
|
42 glb :: "['a set, 'a potype] => 'a" where |
39 "glb S po = greatest (%x. \<forall>y\<in>S. (x,y): order po) po" |
43 "glb S po = greatest (%x. \<forall>y\<in>S. (x,y): order po) po" |
40 |
44 |
41 isLub :: "['a set, 'a potype, 'a] => bool" |
45 definition |
|
46 isLub :: "['a set, 'a potype, 'a] => bool" where |
42 "isLub S po = (%L. (L: pset po & (\<forall>y\<in>S. (y,L): order po) & |
47 "isLub S po = (%L. (L: pset po & (\<forall>y\<in>S. (y,L): order po) & |
43 (\<forall>z\<in>pset po. (\<forall>y\<in>S. (y,z): order po) --> (L,z): order po)))" |
48 (\<forall>z\<in>pset po. (\<forall>y\<in>S. (y,z): order po) --> (L,z): order po)))" |
44 |
49 |
45 isGlb :: "['a set, 'a potype, 'a] => bool" |
50 definition |
|
51 isGlb :: "['a set, 'a potype, 'a] => bool" where |
46 "isGlb S po = (%G. (G: pset po & (\<forall>y\<in>S. (G,y): order po) & |
52 "isGlb S po = (%G. (G: pset po & (\<forall>y\<in>S. (G,y): order po) & |
47 (\<forall>z \<in> pset po. (\<forall>y\<in>S. (z,y): order po) --> (z,G): order po)))" |
53 (\<forall>z \<in> pset po. (\<forall>y\<in>S. (z,y): order po) --> (z,G): order po)))" |
48 |
54 |
49 "fix" :: "[('a => 'a), 'a set] => 'a set" |
55 definition |
|
56 "fix" :: "[('a => 'a), 'a set] => 'a set" where |
50 "fix f A = {x. x: A & f x = x}" |
57 "fix f A = {x. x: A & f x = x}" |
51 |
58 |
52 interval :: "[('a*'a) set,'a, 'a ] => 'a set" |
59 definition |
|
60 interval :: "[('a*'a) set,'a, 'a ] => 'a set" where |
53 "interval r a b = {x. (a,x): r & (x,b): r}" |
61 "interval r a b = {x. (a,x): r & (x,b): r}" |
54 |
62 |
55 |
63 |
56 definition |
64 definition |
57 Bot :: "'a potype => 'a" |
65 Bot :: "'a potype => 'a" where |
58 "Bot po = least (%x. True) po" |
66 "Bot po = least (%x. True) po" |
59 |
67 |
60 Top :: "'a potype => 'a" |
68 definition |
|
69 Top :: "'a potype => 'a" where |
61 "Top po = greatest (%x. True) po" |
70 "Top po = greatest (%x. True) po" |
62 |
71 |
63 PartialOrder :: "('a potype) set" |
72 definition |
|
73 PartialOrder :: "('a potype) set" where |
64 "PartialOrder = {P. refl (pset P) (order P) & antisym (order P) & |
74 "PartialOrder = {P. refl (pset P) (order P) & antisym (order P) & |
65 trans (order P)}" |
75 trans (order P)}" |
66 |
76 |
67 CompleteLattice :: "('a potype) set" |
77 definition |
|
78 CompleteLattice :: "('a potype) set" where |
68 "CompleteLattice = {cl. cl: PartialOrder & |
79 "CompleteLattice = {cl. cl: PartialOrder & |
69 (\<forall>S. S \<subseteq> pset cl --> (\<exists>L. isLub S cl L)) & |
80 (\<forall>S. S \<subseteq> pset cl --> (\<exists>L. isLub S cl L)) & |
70 (\<forall>S. S \<subseteq> pset cl --> (\<exists>G. isGlb S cl G))}" |
81 (\<forall>S. S \<subseteq> pset cl --> (\<exists>G. isGlb S cl G))}" |
71 |
82 |
72 CLF :: "('a potype * ('a => 'a)) set" |
83 definition |
|
84 CLF :: "('a potype * ('a => 'a)) set" where |
73 "CLF = (SIGMA cl: CompleteLattice. |
85 "CLF = (SIGMA cl: CompleteLattice. |
74 {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)})" |
86 {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)})" |
75 |
87 |
76 induced :: "['a set, ('a * 'a) set] => ('a *'a)set" |
88 definition |
|
89 induced :: "['a set, ('a * 'a) set] => ('a *'a)set" where |
77 "induced A r = {(a,b). a : A & b: A & (a,b): r}" |
90 "induced A r = {(a,b). a : A & b: A & (a,b): r}" |
78 |
91 |
79 |
92 |
80 definition |
93 definition |
81 sublattice :: "('a potype * 'a set)set" |
94 sublattice :: "('a potype * 'a set)set" where |
82 "sublattice = |
95 "sublattice = |
83 (SIGMA cl: CompleteLattice. |
96 (SIGMA cl: CompleteLattice. |
84 {S. S \<subseteq> pset cl & |
97 {S. S \<subseteq> pset cl & |
85 (| pset = S, order = induced S (order cl) |): CompleteLattice})" |
98 (| pset = S, order = induced S (order cl) |): CompleteLattice})" |
86 |
99 |
87 abbreviation |
100 abbreviation |
88 sublat :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50) |
101 sublat :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50) where |
89 "S <<= cl == S : sublattice `` {cl}" |
102 "S <<= cl == S : sublattice `` {cl}" |
90 |
103 |
91 definition |
104 definition |
92 dual :: "'a potype => 'a potype" |
105 dual :: "'a potype => 'a potype" where |
93 "dual po = (| pset = pset po, order = converse (order po) |)" |
106 "dual po = (| pset = pset po, order = converse (order po) |)" |
94 |
107 |
95 locale (open) PO = |
108 locale (open) PO = |
96 fixes cl :: "'a potype" |
109 fixes cl :: "'a potype" |
97 and A :: "'a set" |
110 and A :: "'a set" |