X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Foverlap%2Fo-algebra.ma;h=40b2f72bb5dab9c2d53b979059e9b88bf0b7c063;hb=e1d6716c5560b046e0a7d0d871cc01a64cb31ca8;hp=c55131315b21261d7fb493f1af47342a224f2a61;hpb=b0f18f8992623be7c7dde1890d51c7404e9930ab;p=helm.git

diff --git a/helm/software/matita/nlibrary/overlap/o-algebra.ma b/helm/software/matita/nlibrary/overlap/o-algebra.ma
index c55131315..40b2f72bb 100644
--- a/helm/software/matita/nlibrary/overlap/o-algebra.ma
+++ b/helm/software/matita/nlibrary/overlap/o-algebra.ma
@@ -36,9 +36,9 @@ interpretation "unary morphism1 comprehension with proof" 'comprehension_by s \e
 (* USARE L'ESISTENZIALE DEBOLE *)
 nrecord OAlgebra : Type[2] := {
   oa_P :> setoid1;
-  oa_leq : binary_morphism1 oa_P oa_P CPROP; (*CSC: dovrebbe essere CProp bug refiner*)
-  oa_overlap: binary_morphism1 oa_P oa_P CPROP;
-  binary_meet: binary_morphism1 oa_P oa_P oa_P;
+  oa_leq : unary_morphism1 oa_P (unary_morphism1_setoid1 oa_P CPROP); (*CSC: dovrebbe essere CProp bug refiner*)
+  oa_overlap: unary_morphism1 oa_P (unary_morphism1_setoid1 oa_P CPROP);
+  binary_meet: unary_morphism1 oa_P (unary_morphism1_setoid1 oa_P oa_P);
 (*CSC:  oa_join: ∀I:setoid.unary_morphism1 (setoid1_of_setoid … I ⇒ oa_P) oa_P;*)
   oa_one: oa_P;
   oa_zero: oa_P;
@@ -63,11 +63,11 @@ nrecord OAlgebra : Type[2] := {
       ∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q
 }.
 
-interpretation "o-algebra leq" 'leq a b = (fun21 ??? (oa_leq ?) a b).
+interpretation "o-algebra leq" 'leq a b = (fun11 ?? (fun11 ?? (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 = (fun21 ??? (oa_overlap ?) a b).
+interpretation "o-algebra overlap" 'overlap a b = (fun11 ?? (fun11 ?? (oa_overlap ?) a) b).
 
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)" 
 non associative with precedence 50 for @{ 'oa_meet $p }.
@@ -106,7 +106,7 @@ intros; split;
 qed.*)
 
 interpretation "o-algebra binary meet" 'and a b = 
-  (fun21 ??? (binary_meet ?) a b).
+  (fun11 ?? (fun11 ?? (binary_meet ?) a) b).
 
 (*
 prefer coercion Type1_OF_OAlgebra.
@@ -209,10 +209,7 @@ nlemma ORelation_eq_respects_leq_or_f_minus_:
  napply (. (or_prop3 … a' …)^-1); (*CSC: why a'? *)
  napply (. ?‡#)
   [##2: napply (a r)
-  | ngeneralize in match r in ⊢ %;
-    nchange with (or_f … a' = or_f … a);
-    napply (.= †e^-1);
-    napply #]
+  | napply (e^-1); //]
  napply (. (or_prop3 …));
  napply oa_overlap_sym;
  nassumption.
@@ -221,9 +218,9 @@ nqed.
 nlemma ORelation_eq2:
  ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
   r=r' → r⎻ = r'⎻.
- #P; #Q; #a; #a'; #e; #x;
+ #P; #Q; #a; #a'; #e; #x; #x'; #Hx; napply (.= †Hx);
  napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_minus_
-  [ napply e | napply e^-1]
+  [ napply e | napply (e^-1)]
 nqed.
 
 ndefinition or_f_minus_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q)
@@ -260,9 +257,9 @@ nqed.
 nlemma ORelation_eq3:
  ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
   r=r' → r* = r'*.
- #P; #Q; #a; #a'; #e; #x;
+ #P; #Q; #a; #a'; #e; #x; #x'; #Hx; napply (.= †Hx);
  napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_star_
-  [ napply e | napply e^-1]
+  [ napply e | napply (e^-1)]
 nqed.
 
 ndefinition or_f_star_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q)
@@ -296,9 +293,9 @@ nqed.
 nlemma ORelation_eq4:
  ∀P,Q:OAlgebra.∀r,r':ORelation P Q.
   r=r' → r⎻* = r'⎻*.
- #P; #Q; #a; #a'; #e; #x;
+ #P; #Q; #a; #a'; #e; #x; #x'; #Hx; napply (.= †Hx);
  napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_minus_star_
-  [ napply e | napply e^-1]
+  [ napply e | napply (e^-1)]
 nqed.
 
 ndefinition or_f_minus_star_morphism1:
@@ -499,8 +496,9 @@ nqed.
 ncheck (λA,B,C,f,g.coerc_to_unary_morphism1 ??? (mk_uffa ??? (composition1 A B C f g))). 
 *)
 ndefinition ORelation_composition : ∀P,Q,R. 
-  binary_morphism1 (ORelation_setoid P Q) (ORelation_setoid Q R) (ORelation_setoid P R).
-#P; #Q; #R; @
+  unary_morphism1 (ORelation_setoid P Q)
+   (unary_morphism1_setoid1 (ORelation_setoid Q R) (ORelation_setoid P R)).
+#P; #Q; #R; napply mk_binary_morphism1
 [ #F; #G; @
   [ napply (G ∘ F) (* napply (comp1_unary_morphisms … G F) (*CSC: was (G ∘ F);*) *)
   | napply (G⎻* ∘ F⎻* ) (* napply (comp1_unary_morphisms … G⎻* F⎻* ) (*CSC: was (G⎻* ∘ F⎻* );*)*)
@@ -516,7 +514,7 @@ ndefinition ORelation_composition : ∀P,Q,R.
     napply (.= (or_prop3 … G …));
     napply or_prop3
   ]
-##| #a;#a';#b;#b';#e;#e1;#x;nnormalize;napply (.= †(e x));napply e1]
+##| nnormalize; /3/]
 nqed.
 
 (*