helm/software/matita/contribs/procedural/CoRN/devel/loeb/per/csetfun.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "CoRN.ma".
  18
  19 include "algebra/CSetoids.ma".
  20
  21 include "algebra/CSetoidFun.ma".
  22
  23 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/ap_fun.con" as definition.
  24
  25 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/eq_fun.con" as definition.
  26
  27 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/irrefl_apfun.con" as lemma.
  28
  29 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/cotrans_apfun.con" as lemma.
  30
  31 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/ta_apfun.con" as lemma.
  32
  33 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/sym_apfun.con" as lemma.
  34
  35 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/FS_is_CSetoid.con" as definition.
  36
  37 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/FS_as_CSetoid.con" as definition.
  38
  39 (* UNEXPORTED
  40 Print associative.
  41 *)
  42
  43 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/comp.con" as definition.
  44
  45 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/comp_as_bin_op.con" as definition.
  46
  47 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/assoc_comp.con" as lemma.
  48
  49 include "algebra/CSemiGroups.ma".
  50
  51 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/FS_as_CSemiGroup.con" as definition.
  52
  53 include "algebra/CMonoids.ma".
  54
  55 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/FS_id.con" as definition.
  56
  57 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/id_is_rht_unit.con" as lemma.
  58
  59 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/id_is_lft_unit.con" as lemma.
  60
  61 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/FS_is_CMonoid.con" as definition.
  62
  63 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/FS_as_CMonoid.con" as definition.
  64
  65 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/PS_as_CMonoid.con" as definition.
  66
  67 include "algebra/CGroups.ma".
  68
  69 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/Inv_is_bij.con" as lemma.
  70
  71 (* Lemma Inv_is_bij :
  72  forall (A B : CSetoid) (f : CSetoid_fun A B) (H : bijective f),
  73  bijective (Inv f H).
  74 intros A B f.
  75 case f.
  76 unfold fun_strext in |- *.
  77 intros f0 H5.
  78 unfold bijective in |- *.
  79 intro H.
  80 elim H.
  81 clear H.
  82 unfold injective in |- *.
  83 unfold surjective in |- *.
  84 intros H0 H1.
  85 split.
  86 unfold Inv in |- *.
  87 simpl in |- *.
  88 unfold invfun in |- *.
  89 simpl in |- *.
  90 unfold sigT_rect in |- *.
  91 intros a0 a1 H2.
  92 case H1.
  93 case (H1 a1).
  94 intros x H3 y H4.
  95 simpl in H3.
  96 simpl in H4.
  97 simpl in H0.
  98 simpl in H1.
  99 apply H5.
 100 astepl a0.
 101 astepr a1.
 102 exact H2.
 103
 104 simpl in |- *.
 105 unfold invfun in |- *.
 106 simpl in |- *.
 107 unfold sigT_rect in |- *.
 108 intros b.
 109 exists (f0 b).
 110 case (H1 (f0 b)).
 111 simpl in |- *.
 112 intros x H2.
 113 simpl in H0.
 114 simpl in H1.
 115 apply not_ap_imp_eq.
 116 red in |- *.
 117 intro H3.
 118 set (H4 := H0 x b H3) in *.
 119 set (H6 := ap_imp_neq B (f0 x) (f0 b) H4) in *.
 120 intuition.
 121 Qed.*)
 122
 123 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/PS_Inv.con" as definition.
 124
 125 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/Inv_as_un_op.con" as definition.
 126
 127 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/PS_is_CGroup.con" as lemma.
 128
 129 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/PS_as_CGroup.con" as definition.
 130
 131 (* In het algemeen niet Abels! *)
 132