- renamed ocaml/ to components/

[helm.git] / helm / matita / library / algebra / semigroups.ma

diff --git a/helm/matita/library/algebra/semigroups.ma b/helm/matita/library/algebra/semigroups.ma
deleted file mode 100644 (file)
index 5b461d1..0000000
--- a/helm/matita/library/algebra/semigroups.ma
+++ /dev/null
@@ -1,64 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/algebra/semigroups".
-
-include "higher_order_defs/functions.ma".
-
-(* Magmas *)
-
-record Magma : Type ≝
- { carrier:> Type;
-   op: carrier → carrier → carrier
- }.
-
-notation < "M" for @{ 'carrier $M }.
-interpretation "carrier coercion" 'carrier S =
- (cic:/matita/algebra/semigroups/carrier.con S).
-
-notation "hvbox(a break \middot b)" 
-  left associative with precedence 55
-for @{ 'magma_op $a $b }.
-
-interpretation "magma operation" 'magma_op a b =
- (cic:/matita/algebra/semigroups/op.con _ a b).
-
-(* Semigroups *)
-
-record isSemiGroup (M:Magma) : Prop ≝
- { associative: associative ? (op M) }.
-
-record SemiGroup : Type ≝
- { magma:> Magma;
-   semigroup_properties:> isSemiGroup magma
- }.
- 
-notation < "S" for @{ 'magma $S }.
-interpretation "magma coercion" 'magma S =
- (cic:/matita/algebra/semigroups/magma.con S).
- 
-definition is_left_unit ≝
- λS:SemiGroup. λe:S. ∀x:S. e·x = x.
- 
-definition is_right_unit ≝
- λS:SemiGroup. λe:S. ∀x:S. x·e = x.
-
-theorem is_left_unit_to_is_right_unit_to_eq:
- ∀S:SemiGroup. ∀e,e':S.
-  is_left_unit ? e → is_right_unit ? e' → e=e'.
- intros;
- rewrite < (H e');
- rewrite < (H1 e) in \vdash (? ? % ?);
- reflexivity.
-qed.