From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 12 Dec 2008 11:59:32 +0000 (+0000)
Subject: thanks to the new fixes to notation, I can define \land for both pairs and
X-Git-Tag: make_still_working~4417
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fac7052d076fbfe531dd95aa57d8ec2381f23648;p=helm.git

thanks to the new fixes to notation, I can define \land for both pairs and
families!
---

diff --git a/helm/software/matita/contribs/formal_topology/o-algebra.ma b/helm/software/matita/contribs/formal_topology/o-algebra.ma
new file mode 100644
index 000000000..2c2a60171
--- /dev/null
+++ b/helm/software/matita/contribs/formal_topology/o-algebra.ma
@@ -0,0 +1,67 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "datatypes/categories.ma".
+include "datatypes/bool.ma".
+include "logic/cprop_connectives.ma". 
+
+record OAlgebra : Type := {
+  oa_P :> setoid;
+  oa_leq : oa_P → oa_P → CProp;
+  oa_overlap: oa_P → oa_P → CProp;
+  oa_meet: ∀I:Type.(I → oa_P) → oa_P;
+  oa_join: ∀I:Type.(I → oa_P) → oa_P;
+  oa_one: oa_P;
+  oa_zero: oa_P;
+  oa_leq_refl: ∀a:oa_P.oa_leq a a;
+  oa_leq_antisym: ∀a,b:oa_P.oa_leq a b → oa_leq b a → a = b;
+  oa_leq_trans: ∀a,b,c:oa_P.oa_leq a b → oa_leq b c → oa_leq a c;
+  oa_overlap_sym: ∀a,b:oa_P.oa_overlap a b → oa_overlap b a;
+  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);
+  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;
+  oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p;
+  oa_one_top: ∀p:oa_P.oa_leq p oa_one;
+  oa_overlap_preservers_meet: 
+    ∀p,q.oa_overlap p q → oa_overlap p (oa_meet bool (λx.match x with [ true ⇒ p | false ⇒ q ]));
+  oa_join_split: 
+    ∀I.∀p,q_i.oa_overlap p (oa_join I q_i) ↔ ∃i:I.oa_overlap p (q_i i);
+  oa_density: 
+    ∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q    
+}.
+
+interpretation "o-algebra leq" 'leq a b = (oa_leq _ a b).
+
+notation "hovbox(a mpadded width -150% (>)< b)" non associative with precedence 45
+for @{ 'overlap $a $b}.
+interpretation "o-algebra overlap" 'overlap a b = (oa_overlap _ a b).
+
+notation > "hovbox(a ∧ b)" left associative with precedence 50
+for @{ 'oa_meet (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) }.
+notation > "hovbox(∧ f)" non associative with precedence 60
+for @{ 'oa_meet $f }.
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.5 (∧) \sub(ident i ∈ I) break p)" non associative with precedence 50
+for @{ 'oa_meet (λ${ident i}:$I.$p) }.
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.5 (∧) \nbsp p)" non associative with precedence 50
+for @{ 'oa_meet (λ${ident i}.($p $_)) }.
+notation < "hovbox(a ∧ b)" left associative with precedence 50
+for @{ 'oa_meet (λx__:$_.match x__ with [ true ⇒ $a | false ⇒ $b ]) }.
+
+interpretation "o-algebra meet" 'oa_meet \eta.f = (oa_meet _ _ f).
+include "nat/nat.ma".  
+
+lemma x : ∀A:OAlgebra.∀x,y:A.∀f:ℕ→A. (x ∧ y >< x) → x = ∧ (λi:ℕ.x) ∧ ∧ f.  
+  
+
+notation ""
+