X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Falgebra%2Ffinite_groups.ma;h=79521e20650c95f8a2016df8c0e82ae921a432ad;hb=dccfee15d96938072fbdf4004a06e5b59ba876dc;hp=2f80525e704b3cc21682f843589b7317a7117934;hpb=e871e95f9ce6abc7fe6cd0e10c8cff60cd9a72e4;p=helm.git

diff --git a/matita/library/algebra/finite_groups.ma b/matita/library/algebra/finite_groups.ma
index 2f80525e7..79521e206 100644
--- a/matita/library/algebra/finite_groups.ma
+++ b/matita/library/algebra/finite_groups.ma
@@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/algebra/finite_groups/".
 
 include "algebra/groups.ma".
 
-record finite_enumerable (T:Type) : Type ≝
+record finite_enumerable (T:Type) : Type≝
  { order: nat;
    repr: nat → T;
    index_of: T → nat;
@@ -39,35 +39,11 @@ for @{ 'card $C }.
 interpretation "Finite_enumerable order" 'card C =
  (cic:/matita/algebra/finite_groups/order.con C _).
 
-record finite_enumerable_SemiGroup : Type ≝
+record finite_enumerable_SemiGroup : Type≝
  { semigroup:> SemiGroup;
    is_finite_enumerable:> finite_enumerable semigroup
  }.
 
-notation < "S"
-for @{ 'semigroup_of_finite_enumerable_semigroup $S }.
-
-interpretation "Semigroup_of_finite_enumerable_semigroup"
- 'semigroup_of_finite_enumerable_semigroup S
-=
- (cic:/matita/algebra/finite_groups/semigroup.con S).
-
-notation < "S"
-for @{ 'magma_of_finite_enumerable_semigroup $S }.
-
-interpretation "Magma_of_finite_enumerable_semigroup"
- 'magma_of_finite_enumerable_semigroup S
-=
- (cic:/matita/algebra/finite_groups/Magma_of_finite_enumerable_SemiGroup.con S).
- 
-notation < "S"
-for @{ 'type_of_finite_enumerable_semigroup $S }.
-
-interpretation "Type_of_finite_enumerable_semigroup"
- 'type_of_finite_enumerable_semigroup S
-=
- (cic:/matita/algebra/finite_groups/Type_of_finite_enumerable_SemiGroup.con S).
-
 interpretation "Finite_enumerable representation" 'repr S i =
  (cic:/matita/algebra/finite_groups/repr.con S
   (cic:/matita/algebra/finite_groups/is_finite_enumerable.con S) i).
@@ -84,7 +60,7 @@ interpretation "Index_of_finite_enumerable representation"
 
 (* several definitions/theorems to be moved somewhere else *)
 
-definition ltb ≝ λn,m. leb n m ∧ notb (eqb n m).
+definition ltb ≝λn,m. leb n m ∧ notb (eqb n m).
 
 theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
 intros;
@@ -205,12 +181,13 @@ unfold lt in H;
 apply (le_S_S ? ? H).
 qed.
 
+(* moved to nat/order.ma 
 theorem lt_O_S: ∀n. O < S n.
 intro;
 unfold lt;
 apply le_S_S;
 apply le_O_n.
-qed.
+qed. *)
 
 theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
 intros;
@@ -240,8 +217,8 @@ elim n;
 | clear n;
   letin f' ≝
    (λx.
-    let fSn1 ≝ f (S n1) in
-     let fx ≝ f x in
+    let fSn1 ≝f (S n1) in
+     let fx ≝f x in
       match ltb fSn1 fx with
       [ true ⇒ pred fx
       | false ⇒ fx
@@ -489,48 +466,48 @@ elim n;
   ]
 ].
 qed.
-
+(* demo *)
 theorem finite_enumerable_SemiGroup_to_left_cancellable_to_right_cancellable_to_isMonoid:
  ∀G:finite_enumerable_SemiGroup.
   left_cancellable ? (op G) →
   right_cancellable ? (op G) →
    ∃e:G. isMonoid (mk_PreMonoid G e).
 intros;
-letin f ≝ (λn.ι(G \sub O · G \sub n));
+letin f ≝(λn.ι(G \sub O · G \sub n));
 cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
-[ letin EX ≝ (Hcut O ?);
+[ letin EX ≝(Hcut O ?);
   [ apply le_O_n
   | clearbody EX;
     clear Hcut;
     unfold f in EX;
     elim EX;
     clear EX;
-    letin HH ≝ (eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
+    letin HH ≝(eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
     clearbody HH;
     rewrite > (repr_index_of ? (is_finite_enumerable G)) in HH;
     apply (ex_intro ? ? (G \sub a));
-    letin GOGO ≝ (refl_eq ? (repr ? (is_finite_enumerable G) O));
+    letin GOGO ≝(refl_eq ? (repr ? (is_finite_enumerable G) O));
     clearbody GOGO;
     rewrite < HH in GOGO;
     rewrite < HH in GOGO:(? ? % ?);
-    rewrite > (associative ? G) in GOGO;
-    letin GaGa ≝ (H ? ? ? GOGO);
+    rewrite > (op_associative ? G) in GOGO;
+    letin GaGa ≝(H ? ? ? GOGO);
     clearbody GaGa;
     clear GOGO;
     constructor 1;
     [ simplify;
       apply (semigroup_properties G)
     | unfold is_left_unit; intro;
-      letin GaxGax ≝ (refl_eq ? (G \sub a ·x));
-      clearbody GaxGax;
+      letin GaxGax ≝(refl_eq ? (G \sub a ·x));
+      clearbody GaxGax; (* demo *)
       rewrite < GaGa in GaxGax:(? ? % ?);
-      rewrite > (associative ? (semigroup_properties G)) in GaxGax;
+      rewrite > (op_associative ? (semigroup_properties G)) in GaxGax;
       apply (H ? ? ? GaxGax)
     | unfold is_right_unit; intro;
-      letin GaxGax ≝ (refl_eq ? (x·G \sub a));
+      letin GaxGax ≝(refl_eq ? (x·G \sub a));
       clearbody GaxGax;
       rewrite < GaGa in GaxGax:(? ? % ?);
-      rewrite < (associative ? (semigroup_properties G)) in GaxGax;
+      rewrite < (op_associative ? (semigroup_properties G)) in GaxGax;
       apply (H1 ? ? ? GaxGax)
     ]
   ]
@@ -540,7 +517,7 @@ cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
     elim H3;
     assumption
   | intros;
-    change in H5 with (ι(G \sub O · G \sub x) = ι(G \sub O · G \sub y));
+    simplify in H5;
     cut (G \sub (ι(G \sub O · G \sub x)) = G \sub (ι(G \sub O · G \sub y)));
     [ rewrite > (repr_index_of ? ? (G \sub O · G \sub x))  in Hcut;
       rewrite > (repr_index_of ? ? (G \sub O · G \sub y))  in Hcut;