A few experiments (with horrible results) using notation...

diff --git a/helm/matita/library/algebra/monoids.ma b/helm/matita/library/algebra/monoids.ma
index 782da09d7a85150ae86ada7b02311bd4fb4c1a78..9fd7330426ab7a70e312d43f806081ae34bd1c95 100644 (file)
--- a/helm/matita/library/algebra/monoids.ma
+++ b/helm/matita/library/algebra/monoids.ma
@@ -29,29 +29,34 @@ record Monoid : Type ≝
  
 coercion cic:/matita/algebra/monoids/semigroup.con.
 
+notation "hvbox(! \sub S)"
+for @{ 'munit $S }.
+
+interpretation "Monoid unit" 'munit S =
+ (cic:/matita/algebra/monoids/e.con S).
+
 definition is_left_inverse ≝
- λM:Monoid. let op ≝ op M in let e ≝ e M in
+ λM:Monoid.
   λopp: M → M.
-   ∀x:M. op (opp x) x = e.
+   ∀x:M. op M (opp x) x = ! \sub M.
 
 definition is_right_inverse ≝
- λM:Monoid. let op ≝ op M in let e ≝ e M in
+ λM:Monoid.
   λopp: M → M.
-   ∀x:M. op x (opp x) = e.
+   ∀x:M. op M x (opp x) = ! \sub M.
 
 theorem is_left_inverse_to_is_right_inverse_to_eq:
  ∀M:Monoid. ∀oppL,oppR.
   is_left_inverse M oppL → is_right_inverse M oppR → 
    ∀x:M. oppL x = oppR x.
  intros;
- letin op ≝ (op M);
- letin e ≝ (e M);
  generalize in match (H x); intro;
- change in H2 with (op (oppL x) x = e); 
- generalize in match (eq_f ? ? (λy. op y (oppR x)) ? ? H2);
- simplify; fold simplify op;
+ generalize in match (eq_f ? ? (λy. op M y (oppR x)) ? ? H2);
+ simplify; fold simplify (op M);
  intro; clear H2;
- generalize in match (properties (semigroup M)); intro;
+ generalize in match (properties (semigroup M));
+ fold simplify (Type_of_Monoid M);
+ intro;
  unfold isSemiGroup in H2; unfold associative in H2;
  rewrite > H2 in H3; clear H2;
  rewrite > H1 in H3;

diff --git a/helm/matita/library/algebra/semigroups.ma b/helm/matita/library/algebra/semigroups.ma
index bea3ae584a3c456af650c82b443628f64a575a38..93a139ca760e5113f6b87d00a8f09d5552861e48 100644 (file)
--- a/helm/matita/library/algebra/semigroups.ma
+++ b/helm/matita/library/algebra/semigroups.ma
@@ -27,11 +27,21 @@ record SemiGroup : Type ≝
  
 coercion cic:/matita/algebra/semigroups/carrier.con.
 
+notation "hvbox(a break * \sub S b)" 
+  left associative with precedence 55
+for @{ 'ptimes $S $a $b }.
+
+interpretation "Semigroup operation" 'times a b =
+ (cic:/matita/algebra/semigroups/op.con _ a b).
+
+interpretation "Semigroup operation" 'ptimes S a b =
+ (cic:/matita/algebra/semigroups/op.con S a b).
+
 definition is_left_unit ≝
- λS:SemiGroup. λe:S. ∀x:S. op S e x = x.
+ λS:SemiGroup. λe:S. ∀x:S. e * x = x.
  
 definition is_right_unit ≝
- λS:SemiGroup. λe:S. ∀x:S. op S x e = x.
+ λS:SemiGroup. λe:S. ∀x:S. x * e = x.
 
 theorem is_left_unit_to_is_right_unit_to_eq:
  ∀S:SemiGroup. ∀e1,e2:S.