From 3969d815396a22dca5e71c5f85fa3ec66d79849e Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 19 Dec 2008 20:37:07 +0000
Subject: [PATCH] ...

---
 .../formal_topology/overlap/o-algebra.ma      | 25 ++++++++++++++++---
 helm/software/matita/predefined_virtuals.ml   | 19 ++++++++------
 2 files changed, 32 insertions(+), 12 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 b5410f7af..877887ad9 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -48,6 +48,19 @@ intros; constructor 1; intros;
 | apply (IF_THEN_ELSE_p T c c1 a a' H);]
 qed.
 
+interpretation "mk " 'comprehension T P = 
+  (mk_unary_morphism T _ P _).
+
+notation > "hvbox({ ident i ∈ s | term 19 p | by })" with precedence 90
+for @{ 'comprehension_by $s (\lambda ${ident i}. $p) $by}.
+
+interpretation "unary morphism comprehension with proof" 'comprehension_by s f p = 
+  (mk_unary_morphism s _ f p).
+
+definition A : ∀S:setoid.∀a,b:S.ums BOOL S.
+apply (λS,a,b.{ x ∈ BOOL | match x with [ true ⇒ a | false ⇒ b] | IF_THEN_ELSE_p S a b}).
+qed.
+
 record OAlgebra : Type := {
   oa_P :> setoid;
   oa_leq : binary_morphism1 oa_P oa_P CPROP; (* CPROP is setoid1 *)
@@ -66,7 +79,8 @@ record OAlgebra : Type := {
   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 (if_then_else oa_P p q));
+       (oa_meet ? { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p oa_P p q });
+     (*(oa_meet BOOL (if_then_else oa_P p q));*)
   oa_join_split: (* ha I → oa_P da castare a funX (ums A oa_P) *)
       ∀I:setoid.∀p.∀q:ums I oa_P.oa_overlap p (oa_join I q) ⇔ ∃i:I.oa_overlap p (q i);
   (*oa_base : setoid;
@@ -89,10 +103,13 @@ for @{ 'oa_meet (λ${ident i}:$I.$p) }.
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)" non associative with precedence 50
 for @{ 'oa_meet (λ${ident i}.($p $_)) }.
 notation < "hovbox(a ∧ b)" left associative with precedence 50
-for @{ 'oa_meet2 $a $b }.
+for @{ 'oa_meet
+  ($foo $bar $baz 
+    (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) 
+    $res) }.
 
-interpretation "o-algebra meet" 'oa_meet \eta.f = (fun_1 __ (oa_meet __) f).
-interpretation "o-algebra binary meet" 'and x y = (fun_1 __ (oa_meet _ BOOL) (if_then_else _ x y)).
+interpretation "o-algebra meet" 'oa_meet f = (fun_1 __ (oa_meet __) f).
+(*interpretation "o-algebra binary meet" 'and x y = (fun_1 __ (oa_meet _ BOOL) (if_then_else _ x y)).*)
 
 (*
 notation > "hovbox(a ∨ b)" left associative with precedence 49
diff --git a/helm/software/matita/predefined_virtuals.ml b/helm/software/matita/predefined_virtuals.ml
index 01b18e469..e89af7d2b 100644
--- a/helm/software/matita/predefined_virtuals.ml
+++ b/helm/software/matita/predefined_virtuals.ml
@@ -150,7 +150,7 @@ let predefined_virtuals = [
  ["\\smile"                                          ], "⌣", [symbol];
  ["\\blank"                                          ], "␣", [symbol];
  ["\\HorizontalLine"                                 ], "─", [symbol];
- ["\\loz"; "\\lozenge"                                ], "◊", [symbol];
+ ["\\loz"; "\\lozenge";"<>"                                ], "◊", [symbol];
  ["\\starf"; "\\bigstar"                              ], "★", [symbol];
  ["\\phone"                                          ], "☎", [symbol];
  ["\\female"                                         ], "♀", [symbol];
@@ -828,7 +828,7 @@ let predefined_virtuals = [
  ["\\NotNestedLessLess"                              ], "⒡̸", [circle];
  ["\\NotNestedGreaterGreater"                        ], "⒢̸", [circle];
  ["\\oS"; "\\circledS"                                ], "Ⓢ", [circle];
- ["\\cir"                                            ], "○", [circle];
+ ["\\cir";"()"                                            ], "○", [circle];
  ["\\xcirc"; "\\bigcirc"                              ], "◯", [circle];
 (* }}} *)
 
@@ -839,7 +839,7 @@ let predefined_virtuals = [
  ["\\sdotb"; "\\dotsquare"                            ], "⊡", [square];
  ["\\uhblk"                                          ], "▀", [square];
  ["\\lhblk"                                          ], "▄", [square];
- ["\\squ"; "\\square"; "\\Square"                      ], "□", [square];
+ ["\\squ"; "\\square"; "\\Square";"[]"                      ], "□", [square];
  ["\\squf"; "\\squarf"; "\\blacksquare"                ], "▪", [square];
  ["\\rect"                                           ], "▭", [square];
  ["\\marker"                                         ], "▮", [square];
@@ -1502,10 +1502,13 @@ let load_predefined_virtuals () =
 ;;
 
 let predefined_classes = [
- [ "→"; "⇉"; "⇒"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; "⥤"; "⥰"; ] ;
- [ "≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; ];
- [ "_" ; "⎽"; "⎼"; "⎻"; "⎺"; ];
- [ "<"; "≺"; "≮"; "⊀"; ] ;
+ ["→"; "⇉"; "⇒"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; "⥤"; "⥰"; ] ;
+ ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; ];
+ ["_" ; "⎽"; "⎼"; "⎻"; "⎺"; ];
+ ["<"; "≺"; "≮"; "⊀"; ] ;
+ ["□"; "◽"; "▪"; "◾"; ];
+ ["○"; "∘";  "ø"; ] ;
+ ["◊"; "♢"; "⧫"; "♦"; ];
  ["a"; "α"; "𝕒"; ] ;
  ["A"; "ℵ"; "𝔸"; ] ;
  ["b"; "β"; "ß"; "𝕓"; ] ;
@@ -1534,7 +1537,7 @@ let predefined_classes = [
  ["M"; "ℳ"; "𝕄"; ] ;
  ["n"; "𝕟"; ] ;
  ["N"; "ℕ"; "№"; ] ;
- ["o"; "θ"; "ϑ"; "𝕠"; "ø"; "∘"; ] ;
+ ["o"; "θ"; "ϑ"; "𝕠"; ];
  ["O"; "Θ"; "𝕆"; ] ;
  ["p"; "π"; "𝕡"; ] ;
  ["P"; "Π"; "℘"; "ℙ"; ] ;
-- 
2.39.2