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.oa_overlap p (oa_join I q) ↔ ∃i:I.oa_overlap p (q 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.7 (∧) \below (ident i ∈ I) break term 90 p)" non associative with precedence 50
54 for @{ 'oa_meet (λ${ident i}:$I.$p) }.
55 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 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 (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
60 interpretation "o-algebra meet" 'oa_meet \eta.f = (oa_meet _ _ f).
62 notation > "hovbox(a ∨ b)" left associative with precedence 49
63 for @{ 'oa_join (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) }.
64 notation > "hovbox(∨ f)" non associative with precedence 59
66 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈ I) break term 90 p)" non associative with precedence 49
67 for @{ 'oa_join (λ${ident i}:$I.$p) }.
68 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)" non associative with precedence 49
69 for @{ 'oa_join (λ${ident i}.($p $_)) }.
70 notation < "hovbox(a ∨ b)" left associative with precedence 49
71 for @{ 'oa_join (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
73 interpretation "o-algebra join" 'oa_join \eta.f = (oa_join _ _ f).
76 include "nat/plus.ma".
78 lemma x : ∀A:OAlgebra.∀x,y:A.∀f:ℕ→A.
80 (x ∧ y >< x ∨ y ∧ x) →
81 x = ∧ (λi:ℕ.x ∧ f i) ∧ ∨ (λi:ℕ.∧ (λx.f (x+i))) → x = y.