From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 19 Jan 2006 13:40:44 +0000 (+0000)
Subject: A few experiments (with horrible results) using notation...
X-Git-Tag: make_still_working~7812
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ceb1ffa3c01551ba51c1afcd85d693726c7fd3d9;hp=768514ae739c7b9a8c5a89a3684496912d1ced05;p=helm.git

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 782da09d7..9fd733042 100644
--- 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 bea3ae584..93a139ca7 100644
--- 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.