update in groud_2 and models

[helm.git] / helm / software / matita / library / algebra / finite_groups.ma

diff --git a/helm/software/matita/library/algebra/finite_groups.ma b/helm/software/matita/library/algebra/finite_groups.ma
index 8b1beb7027e18648a6948f178931bcf64915d6da..30408be37d28e7db2cd5047c913bca0087729c3d 100644 (file)
--- a/helm/software/matita/library/algebra/finite_groups.ma
+++ b/helm/software/matita/library/algebra/finite_groups.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "algebra/groups.ma".
+include "nat/relevant_equations.ma".
 
 record finite_enumerable (T:Type) : Type≝
  { order: nat;
@@ -28,14 +29,9 @@ for @{ 'repr $C $i }.
 
 (* CSC: multiple interpretations in the same file are not considered in the
  right order
-interpretation "Finite_enumerable representation" 'repr C i =
- (cic:/matita/algebra/finite_groups/repr.con C _ i).*)
+interpretation "Finite_enumerable representation" 'repr C i = (repr C ? i).*)
  
-notation < "hvbox(|C|)" with precedence 89
-for @{ 'card $C }.
-
-interpretation "Finite_enumerable order" 'card C =
- (cic:/matita/algebra/finite_groups/order.con C _).
+interpretation "Finite_enumerable order" 'card C = (order C ?).
 
 record finite_enumerable_SemiGroup : Type≝
  { semigroup:> SemiGroup;
@@ -43,17 +39,15 @@ record finite_enumerable_SemiGroup : Type≝
  }.
 
 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).
+ (repr S (is_finite_enumerable S) i).
 
-notation "hvbox(ι e)" with precedence 60
+notation "hvbox(\iota e)" with precedence 60
 for @{ 'index_of_finite_enumerable_semigroup $e }.
 
 interpretation "Index_of_finite_enumerable representation"
  'index_of_finite_enumerable_semigroup e
 =
- (cic:/matita/algebra/finite_groups/index_of.con _
-  (cic:/matita/algebra/finite_groups/is_finite_enumerable.con _) e).
+ (index_of ? (is_finite_enumerable ?) e).
 
 
 (* several definitions/theorems to be moved somewhere else *)
@@ -251,8 +245,7 @@ elim n;
       [ apply (H1 ? ? ? ? Hcut);
         apply le_S;
         assumption
-      | alias id "eq_pred_to_eq" = "cic:/matita/nat/relevant_equations/eq_pred_to_eq.con".
-apply eq_pred_to_eq;
+      | apply eq_pred_to_eq;
         [ apply (ltn_to_ltO ? ? H7)
         | apply (ltn_to_ltO ? ? H6)
         | assumption
@@ -334,7 +327,7 @@ theorem finite_enumerable_SemiGroup_to_left_cancellable_to_right_cancellable_to_
  ∀G:finite_enumerable_SemiGroup.
   left_cancellable ? (op G) →
   right_cancellable ? (op G) →
-   ∃e:G. isMonoid (mk_PreMonoid G e).
+   ∃e:G. IsMonoid (mk_PreMonoid G e).
 intros;
 letin f ≝(λn.ι(G \sub O · G \sub n));
 cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
@@ -353,24 +346,24 @@ cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
     clearbody GOGO;
     rewrite < HH in GOGO;
     rewrite < HH in GOGO:(? ? % ?);
-    rewrite > (op_associative ? G) in GOGO;
+    rewrite > (op_is_associative ? G) in GOGO;
     letin GaGa ≝(H ? ? ? GOGO);
     clearbody GaGa;
     clear GOGO;
     constructor 1;
     [ simplify;
-      apply (semigroup_properties G)
+      apply (is_semi_group G)
     | unfold is_left_unit; intro;
       letin GaxGax ≝(refl_eq ? (G \sub a ·x));
       clearbody GaxGax; (* demo *)
       rewrite < GaGa in GaxGax:(? ? % ?);
-      rewrite > (op_associative ? (semigroup_properties G)) in GaxGax;
+      rewrite > (op_is_associative ? G) in GaxGax;
       apply (H ? ? ? GaxGax)
     | unfold is_right_unit; intro;
       letin GaxGax ≝(refl_eq ? (x·G \sub a));
       clearbody GaxGax;
       rewrite < GaGa in GaxGax:(? ? % ?);
-      rewrite < (op_associative ? (semigroup_properties G)) in GaxGax;
+      rewrite < (op_is_associative ? G) in GaxGax;
       apply (H1 ? ? ? GaxGax)
     ]
   ]