X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fo-algebra.ma;h=b5410f7aff9876888d8d5b4b07c8d8311991adb6;hb=4dfb1305a9c4a7c292f4b1957de1454d46c1ab8a;hp=f04b0a70ca86ed5c33e8638aeeb1011a49b2a7b5;hpb=f2bf34a07e2494d81ab7c3b44c143dec33e51fe8;p=helm.git

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 f04b0a70c..b5410f7af 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -12,10 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "datatypes/bool.ma".
 include "datatypes/categories.ma".
 include "logic/cprop_connectives.ma". 
 
+inductive bool : Type := true : bool | false : bool.
+
 lemma ums : setoid → setoid → setoid.
 intros (S T);
 constructor 1;
@@ -75,21 +76,12 @@ record OAlgebra : Type := {
       ∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q
 }.
 
-(*
-axiom Al : OAlgebra.
-axiom x : carr (oa_P Al).
-definition wwww := (oa_density Al x x).
-definition X := ((λx:Type.λa:x.True) ? wwww).
-*)
-
 interpretation "o-algebra leq" 'leq a b = (fun1 ___ (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 = (fun1 ___ (oa_overlap _) a b).
 
-notation > "hovbox(a ∧ b)" left associative with precedence 50
-for @{ 'oa_meet2 $a $b }.
 notation > "hovbox(∧ f)" non associative with precedence 60
 for @{ 'oa_meet $f }.
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (ident i ∈  I) break term 90 p)" non associative with precedence 50
@@ -100,7 +92,8 @@ notation < "hovbox(a ∧ b)" left associative with precedence 50
 for @{ 'oa_meet2 $a $b }.
 
 interpretation "o-algebra meet" 'oa_meet \eta.f = (fun_1 __ (oa_meet __) f).
-interpretation "o-algebra binary meet" 'oa_meet2 x y = (fun_1 __ (oa_meet _ BOOL) (if_then_else _ x y)).
+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
 for @{ 'oa_join (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) }.
@@ -117,34 +110,49 @@ interpretation "o-algebra join" 'oa_join \eta.f = (oa_join _ _ f).
 *)
 
 record ORelation (P,Q : OAlgebra) : Type ≝ {
-  or_f : P → Q;
-  or_f_minus_star : P → Q;
-  or_f_star : Q → P;
-  or_f_minus : Q → P;
+  or_f :> P ⇒ Q;
+  or_f_minus_star : P ⇒ Q;
+  or_f_star : Q ⇒ P;
+  or_f_minus : Q ⇒ P;
   or_prop1 : ∀p,q. or_f p ≤ q ⇔ p ≤ or_f_star q;
   or_prop2 : ∀p,q. or_f_minus p ≤ q ⇔ p ≤ or_f_minus_star q;
   or_prop3 : ∀p,q. or_f p >< q ⇔ p >< or_f_minus q
 }.
 
-notation < "⨍ \sub (term 90 r)" non associative with precedence 90 for @{'OR_f $r}.
-notation < "⨍ \sub (term 90 r) term 90 a" non associative with precedence 70 for @{'OR_f_app1 $r $a}.
-notation > "⨍_(term 90 r)" non associative with precedence 90 for @{'OR_f $r}.
-interpretation "o-relation f" 'OR_f r = (or_f _ _ r).
-interpretation "o-relation f x" 'OR_f_app1 r a = (or_f _ _ r a).
+notation "r \sup *" non associative with precedence 90 for @{'OR_f_star $r}.
+notation > "r *" non associative with precedence 90 for @{'OR_f_star $r}.
+interpretation "o-relation f*" 'OR_f_star r = (or_f_star _ _ r).
+
+notation "r \sup (⎻* )" non associative with precedence 90 for @{'OR_f_minus_star $r}.
+notation > "r⎻*" non associative with precedence 90 for @{'OR_f_minus_star $r}.
+interpretation "o-relation f⎻*" 'OR_f_minus_star r = (or_f_minus_star _ _ r).
 
+notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
+notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
+interpretation "o-relation f⎻" 'OR_f_minus r = (or_f_minus _ _ r).
+
+axiom DAEMON: False.
 
 definition ORelation_setoid : OAlgebra → OAlgebra → setoid1.
 intros (P Q);
 constructor 1;
 [ apply (ORelation P Q);
 | constructor 1;
-   [ apply (λp,q. ∀a.⨍_p a = ⨍_q a (* ∧ f^-1 a = .... *));
-   | whd; simplify; intros; apply refl;
-   | whd; simplify; intros; apply (H ? \sup -1);
-   | whd; simplify; intros; apply trans; [2: apply H;|3: apply H1]]]
+   [ 
+     alias symbol "and" = "constructive and".
+     apply (λp,q.
+            (∀a.p⎻* a = q⎻* a) ∧ 
+            (∀a.p⎻ a  = q⎻ a) ∧
+            (∀a.p a   = q a) ∧ 
+            (∀a.p* a  = q* a)); 
+   | whd; simplify; intros; repeat split; intros; apply refl;
+   | whd; simplify; intros; cases H; cases H1; cases H3; clear H H3 H1;
+     repeat split; intros; apply sym; generalize in match a;assumption;
+   | whd; simplify; intros; elim DAEMON;]]
 qed.  
 
-axiom DAEMON: False.
+lemma hint : ∀P,Q. ORelation_setoid P Q → P ⇒ Q. intros; apply (or_f ?? c);qed.
+coercion hint.
 
 definition composition : ∀P,Q,R. 
   binary_morphism1 (ORelation_setoid P Q) (ORelation_setoid Q R) (ORelation_setoid P R).
@@ -152,7 +160,7 @@ intros;
 constructor 1;
 [ intros (F G);
   constructor 1;
-  [ apply (λx.⨍_G (⨍_F x));
+  [ constructor 1; [apply (λx. G (F x)); | intros; apply (†(†H));]
   |2,3,4,5,6,7: cases DAEMON;]
 | intros; cases DAEMON;]
 qed.
@@ -162,8 +170,9 @@ split;
 [ apply (OAlgebra);
 | intros; apply (ORelation_setoid o o1);
 | intro O; split;
-  [1,2,3,4: apply (λx.x);
-  |*:intros;split;intros; assumption; ] 
+  [1,2,3,4: constructor 1; [1,3,5,7:apply (λx.x);|*:intros;assumption]
+  |5,6,7:intros;split;intros; assumption; ] 
+|4: apply composition;
 |*: elim DAEMON;]
 qed.