1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "datatypes/categories.ma".
16 include "datatypes/bool.ma".
17 include "logic/cprop_connectives.ma".
19 record OAlgebra : Type := {
21 oa_leq : oa_P → oa_P → CProp;
22 oa_overlap: oa_P → oa_P → CProp;
23 oa_meet: ∀I:Type.(I → oa_P) → oa_P;
24 oa_join: ∀I:Type.(I → oa_P) → oa_P;
27 oa_leq_refl: ∀a:oa_P.oa_leq a a;
28 oa_leq_antisym: ∀a,b:oa_P.oa_leq a b → oa_leq b a → a = b;
29 oa_leq_trans: ∀a,b,c:oa_P.oa_leq a b → oa_leq b c → oa_leq a c;
30 oa_overlap_sym: ∀a,b:oa_P.oa_overlap a b → oa_overlap b a;
31 oa_meet_inf: ∀I:Type.∀p_i.∀p:oa_P.oa_leq p (oa_meet I p_i) → ∀i:I.oa_leq p (p_i i);
32 oa_join_sup: ∀I:Type.∀p_i.∀p:oa_P.oa_leq (oa_join I p_i) p → ∀i:I.oa_leq (p_i i) p;
33 oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p;
34 oa_one_top: ∀p:oa_P.oa_leq p oa_one;
35 oa_overlap_preservers_meet:
36 ∀p,q.oa_overlap p q → oa_overlap p (oa_meet bool (λx.match x with [ true ⇒ p | false ⇒ q ]));
38 ∀I.∀p,q_i.oa_overlap p (oa_join I q_i) ↔ ∃i:I.oa_overlap p (q_i i);
40 ∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q
43 interpretation "o-algebra leq" 'leq a b = (oa_leq _ a b).
45 notation "hovbox(a mpadded width -150% (>)< b)" non associative with precedence 45
46 for @{ 'overlap $a $b}.
47 interpretation "o-algebra overlap" 'overlap a b = (oa_overlap _ a b).
49 notation > "hovbox(a ∧ b)" left associative with precedence 50
50 for @{ 'oa_meet (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) }.
51 notation > "hovbox(∧ f)" non associative with precedence 60
53 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.5 (∧) \sub(ident i ∈ I) break p)" non associative with precedence 50
54 for @{ 'oa_meet (λ${ident i}:$I.$p) }.
55 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.5 (∧) \nbsp p)" non associative with precedence 50
56 for @{ 'oa_meet (λ${ident i}.($p $_)) }.
57 notation < "hovbox(a ∧ b)" left associative with precedence 50
58 for @{ 'oa_meet (λx__:$_.match x__ with [ true ⇒ $a | false ⇒ $b ]) }.
60 interpretation "o-algebra meet" 'oa_meet \eta.f = (oa_meet _ _ f).
63 lemma x : ∀A:OAlgebra.∀x,y:A.∀f:ℕ→A. (x ∧ y >< x) → x = ∧ (λi:ℕ.x) ∧ ∧ f.