From 3cf6181bded05eb63140d1b2ba4f2f5791a73b48 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 28 Jun 2010 20:15:28 +0000 Subject: [PATCH] better notation for oalgebra --- .../formal_topology/overlap/o-algebra.ma | 49 +++++++++++-------- 1 file changed, 28 insertions(+), 21 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma index 806859a45..0a2e84880 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma @@ -51,40 +51,47 @@ interpretation "unary morphism1 comprehension with proof" 'comprehension_by s \e (* per il set-indexing vedere capitolo BPTools (foundational tools), Sect. 0.3.4 complete lattices, Definizione 0.9 *) (* USARE L'ESISTENZIALE DEBOLE *) + + +notation > "A × B ⇉2,1 C" non associative with precedence 70 for @{binary_morphism1 $A $B $C}. +notation > "A × B ⇉2,2 C" non associative with precedence 70 for @{binary_morphism2 $A $B $C}. +notation > "B ⇉1,1 C" non associative with precedence 80 for @{arrows1 SET $B $C}. +notation > "B ⇉1,2 C" non associative with precedence 80 for @{unary_morphism2 $B $C}. +notation > "hvbox(a break ≤ b)" non associative with precedence 45 for @{oa_leq $a $b}. +notation > "a >< b" non associative with precedence 45 for @{oa_overlap $a $b}. +notation > "⋁ p" non associative with precedence 45 for @{oa_join ? $p}. +notation > "⋀ p" non associative with precedence 45 for @{oa_meet ? $p}. record OAlgebra : Type2 := { oa_P :> SET1; - oa_leq : binary_morphism1 oa_P oa_P CPROP; - oa_overlap: binary_morphism1 oa_P oa_P CPROP; - oa_meet: ∀I:SET.unary_morphism2 (I ⇒ oa_P) oa_P; - oa_join: ∀I:SET.unary_morphism2 (I ⇒ oa_P) oa_P; + oa_leq : oa_P × oa_P ⇉2,1 CPROP; + oa_overlap: oa_P × oa_P ⇉2,1 CPROP; + oa_meet: ∀I:SET.(I ⇒ oa_P) ⇉1,2 oa_P; + oa_join: ∀I:SET.(I ⇒ oa_P) ⇉1,2 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:SET.∀p_i:I ⇒ oa_P.∀p:oa_P. - oa_leq p (oa_meet I p_i) = (∀i:I.oa_leq p (p_i i)); - oa_join_sup: ∀I:SET.∀p_i:I ⇒ oa_P.∀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_leq_refl: ∀a:oa_P. a ≤ a; + oa_leq_antisym: ∀a,b:oa_P.a ≤ b → b ≤ a → a = b; + oa_leq_trans: ∀a,b,c:oa_P.a ≤ b → b ≤ c → a ≤ c; + oa_overlap_sym: ∀a,b:oa_P.a >< b → b >< a; + oa_meet_inf: ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.p ≤ (⋀ p_i) = (∀i:I.p ≤ (p_i i)); + oa_join_sup: ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.(⋁ p_i) ≤ p = (∀i:I.p_i i ≤ p); + oa_zero_bot: ∀p:oa_P.oa_zero ≤ p; + oa_one_top: ∀p:oa_P.p ≤ oa_one; oa_overlap_preserves_meet_: - ∀p,q:oa_P.oa_overlap p q → oa_overlap p - (oa_meet ? { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p oa_P p q }); - oa_join_split: - ∀I:SET.∀p.∀q:I ⇒ oa_P. - oa_overlap p (oa_join I q) = (∃i:I.oa_overlap p (q i)); + ∀p,q:oa_P.p >< q → + p >< (⋀ { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p oa_P p q }); + oa_join_split: ∀I:SET.∀p.∀q:I ⇒ oa_P.p >< (⋁ q) = (∃i:I.p >< (q i)); (*oa_base : setoid; 1) enum non e' il nome giusto perche' non e' suriettiva 2) manca (vedere altro capitolo) la "suriettivita'" come immagine di insiemi di oa_base oa_enum : ums oa_base oa_P; oa_density: ∀p,q.(∀i.oa_overlap p (oa_enum i) → oa_overlap q (oa_enum i)) → oa_leq p q *) - oa_density: - ∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q + oa_density: ∀p,q.(∀r.p >< r → q >< r) → p ≤ q }. +notation "hvbox(a break ≤ b)" non associative with precedence 45 for @{ 'leq $a $b }. + interpretation "o-algebra leq" 'leq a b = (fun21 ??? (oa_leq ?) a b). notation "hovbox(a mpadded width -150% (>)< b)" non associative with precedence 45 -- 2.39.2