X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCGroups.ma;h=67d508c12fff8abca315b2a9aa0747e26de34b33;hb=f2d9db85559c7a8db11aae1153495fae4a258d54;hp=d13953b4173d9589a886eb2109e522d0e2f4fcbb;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CGroups.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CGroups.ma index d13953b41..67d508c12 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CGroups.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CGroups.ma @@ -16,6 +16,8 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CGroups". +include "CoRN.ma". + (* $Id: CGroups.v,v 1.9 2004/04/23 10:00:52 lcf Exp $ *) (*#* printing [-] %\ensuremath-% #−# *) @@ -26,9 +28,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CGroups". (*#* printing {--} %\ensuremath-% #−# *) -(* INCLUDE -CMonoids -*) +include "algebra/CMonoids.ma". (* Begin_SpecReals *) @@ -37,15 +37,17 @@ CMonoids ** Definition of the notion of Group *) -inline cic:/CoRN/algebra/CGroups/is_inverse.con. +inline "cic:/CoRN/algebra/CGroups/is_inverse.con". (* UNEXPORTED Implicit Arguments is_inverse [S]. *) -inline cic:/CoRN/algebra/CGroups/is_CGroup.con. +inline "cic:/CoRN/algebra/CGroups/is_CGroup.con". + +inline "cic:/CoRN/algebra/CGroups/CGroup.ind". -inline cic:/CoRN/algebra/CGroups/CGroup.ind. +coercion cic:/matita/CoRN-Decl/algebra/CGroups/cg_crr.con 0 (* compounds *). (* End_SpecReals *) @@ -55,7 +57,11 @@ inline cic:/CoRN/algebra/CGroups/CGroup.ind. Implicit Arguments cg_inv [c]. *) -inline cic:/CoRN/algebra/CGroups/cg_minus.con. +(* NOTATION +Notation "[--] x" := (cg_inv x) (at level 2, right associativity). +*) + +inline "cic:/CoRN/algebra/CGroups/cg_minus.con". (*#* %\begin{nameconvention}% @@ -68,6 +74,10 @@ and [ [-] ] with [minus]. Implicit Arguments cg_minus [G]. *) +(* NOTATION +Infix "[-]" := cg_minus (at level 50, left associativity). +*) + (* End_SpecReals *) (*#* @@ -77,15 +87,15 @@ Implicit Arguments cg_minus [G]. *) (* UNEXPORTED -Section CGroup_axioms. +Section CGroup_axioms *) -inline cic:/CoRN/algebra/CGroups/G.var. +alias id "G" = "cic:/CoRN/algebra/CGroups/CGroup_axioms/G.var". -inline cic:/CoRN/algebra/CGroups/cg_inverse.con. +inline "cic:/CoRN/algebra/CGroups/cg_inverse.con". (* UNEXPORTED -End CGroup_axioms. +End CGroup_axioms *) (*#* @@ -96,79 +106,79 @@ General properties of groups. *) (* UNEXPORTED -Section CGroup_basics. +Section CGroup_basics *) -inline cic:/CoRN/algebra/CGroups/G.var. +alias id "G" = "cic:/CoRN/algebra/CGroups/CGroup_basics/G.var". -inline cic:/CoRN/algebra/CGroups/cg_rht_inv_unfolded.con. +inline "cic:/CoRN/algebra/CGroups/cg_rht_inv_unfolded.con". -inline cic:/CoRN/algebra/CGroups/cg_lft_inv_unfolded.con. +inline "cic:/CoRN/algebra/CGroups/cg_lft_inv_unfolded.con". -inline cic:/CoRN/algebra/CGroups/cg_minus_correct.con. +inline "cic:/CoRN/algebra/CGroups/cg_minus_correct.con". (* UNEXPORTED Hint Resolve cg_rht_inv_unfolded cg_lft_inv_unfolded cg_minus_correct: algebra. *) -inline cic:/CoRN/algebra/CGroups/cg_inverse'.con. +inline "cic:/CoRN/algebra/CGroups/cg_inverse'.con". (* Hints for Auto *) -inline cic:/CoRN/algebra/CGroups/cg_minus_unfolded.con. +inline "cic:/CoRN/algebra/CGroups/cg_minus_unfolded.con". (* UNEXPORTED Hint Resolve cg_minus_unfolded: algebra. *) -inline cic:/CoRN/algebra/CGroups/cg_minus_wd.con. +inline "cic:/CoRN/algebra/CGroups/cg_minus_wd.con". (* UNEXPORTED Hint Resolve cg_minus_wd: algebra_c. *) -inline cic:/CoRN/algebra/CGroups/cg_minus_strext.con. +inline "cic:/CoRN/algebra/CGroups/cg_minus_strext.con". -inline cic:/CoRN/algebra/CGroups/cg_minus_is_csetoid_bin_op.con. +inline "cic:/CoRN/algebra/CGroups/cg_minus_is_csetoid_bin_op.con". -inline cic:/CoRN/algebra/CGroups/grp_inv_assoc.con. +inline "cic:/CoRN/algebra/CGroups/grp_inv_assoc.con". (* UNEXPORTED Hint Resolve grp_inv_assoc: algebra. *) -inline cic:/CoRN/algebra/CGroups/cg_inv_unique.con. +inline "cic:/CoRN/algebra/CGroups/cg_inv_unique.con". -inline cic:/CoRN/algebra/CGroups/cg_inv_inv.con. +inline "cic:/CoRN/algebra/CGroups/cg_inv_inv.con". (* UNEXPORTED Hint Resolve cg_inv_inv: algebra. *) -inline cic:/CoRN/algebra/CGroups/cg_cancel_lft.con. +inline "cic:/CoRN/algebra/CGroups/cg_cancel_lft.con". -inline cic:/CoRN/algebra/CGroups/cg_cancel_rht.con. +inline "cic:/CoRN/algebra/CGroups/cg_cancel_rht.con". -inline cic:/CoRN/algebra/CGroups/cg_inv_unique'.con. +inline "cic:/CoRN/algebra/CGroups/cg_inv_unique'.con". -inline cic:/CoRN/algebra/CGroups/cg_inv_unique_2.con. +inline "cic:/CoRN/algebra/CGroups/cg_inv_unique_2.con". -inline cic:/CoRN/algebra/CGroups/cg_zero_inv.con. +inline "cic:/CoRN/algebra/CGroups/cg_zero_inv.con". (* UNEXPORTED Hint Resolve cg_zero_inv: algebra. *) -inline cic:/CoRN/algebra/CGroups/cg_inv_zero.con. +inline "cic:/CoRN/algebra/CGroups/cg_inv_zero.con". -inline cic:/CoRN/algebra/CGroups/cg_inv_op.con. +inline "cic:/CoRN/algebra/CGroups/cg_inv_op.con". (*#* Useful for interactive proof development. *) -inline cic:/CoRN/algebra/CGroups/x_minus_x.con. +inline "cic:/CoRN/algebra/CGroups/x_minus_x.con". (*#* ** Sub-groups @@ -178,31 +188,31 @@ inline cic:/CoRN/algebra/CGroups/x_minus_x.con. *) (* UNEXPORTED -Section SubCGroups. +Section SubCGroups *) -inline cic:/CoRN/algebra/CGroups/P.var. +alias id "P" = "cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/P.var". -inline cic:/CoRN/algebra/CGroups/Punit.var. +alias id "Punit" = "cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/Punit.var". -inline cic:/CoRN/algebra/CGroups/op_pres_P.var. +alias id "op_pres_P" = "cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/op_pres_P.var". -inline cic:/CoRN/algebra/CGroups/inv_pres_P.var. +alias id "inv_pres_P" = "cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/inv_pres_P.var". -inline cic:/CoRN/algebra/CGroups/subcrr.con. +inline "cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/subcrr.con" "CGroup_basics__SubCGroups__". -inline cic:/CoRN/algebra/CGroups/subinv.con. +inline "cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/subinv.con" "CGroup_basics__SubCGroups__". -inline cic:/CoRN/algebra/CGroups/isgrp_scrr.con. +inline "cic:/CoRN/algebra/CGroups/isgrp_scrr.con". -inline cic:/CoRN/algebra/CGroups/Build_SubCGroup.con. +inline "cic:/CoRN/algebra/CGroups/Build_SubCGroup.con". (* UNEXPORTED -End SubCGroups. +End SubCGroups *) (* UNEXPORTED -End CGroup_basics. +End CGroup_basics *) (* UNEXPORTED @@ -228,21 +238,21 @@ Hint Resolve cg_minus_wd: algebra_c. *) (* UNEXPORTED -Section Assoc_properties. +Section Assoc_properties *) -inline cic:/CoRN/algebra/CGroups/G.var. +alias id "G" = "cic:/CoRN/algebra/CGroups/Assoc_properties/G.var". -inline cic:/CoRN/algebra/CGroups/assoc_2.con. +inline "cic:/CoRN/algebra/CGroups/assoc_2.con". -inline cic:/CoRN/algebra/CGroups/zero_minus.con. +inline "cic:/CoRN/algebra/CGroups/zero_minus.con". -inline cic:/CoRN/algebra/CGroups/cg_cancel_mixed.con. +inline "cic:/CoRN/algebra/CGroups/cg_cancel_mixed.con". -inline cic:/CoRN/algebra/CGroups/plus_resp_eq.con. +inline "cic:/CoRN/algebra/CGroups/plus_resp_eq.con". (* UNEXPORTED -End Assoc_properties. +End Assoc_properties *) (* UNEXPORTED @@ -258,35 +268,35 @@ Specific properties of apartness. *) (* UNEXPORTED -Section cgroups_apartness. +Section cgroups_apartness *) -inline cic:/CoRN/algebra/CGroups/G.var. +alias id "G" = "cic:/CoRN/algebra/CGroups/cgroups_apartness/G.var". -inline cic:/CoRN/algebra/CGroups/cg_add_ap_zero.con. +inline "cic:/CoRN/algebra/CGroups/cg_add_ap_zero.con". -inline cic:/CoRN/algebra/CGroups/op_rht_resp_ap.con. +inline "cic:/CoRN/algebra/CGroups/op_rht_resp_ap.con". -inline cic:/CoRN/algebra/CGroups/cg_ap_cancel_rht.con. +inline "cic:/CoRN/algebra/CGroups/cg_ap_cancel_rht.con". -inline cic:/CoRN/algebra/CGroups/plus_cancel_ap_rht.con. +inline "cic:/CoRN/algebra/CGroups/plus_cancel_ap_rht.con". -inline cic:/CoRN/algebra/CGroups/minus_ap_zero.con. +inline "cic:/CoRN/algebra/CGroups/minus_ap_zero.con". -inline cic:/CoRN/algebra/CGroups/zero_minus_apart.con. +inline "cic:/CoRN/algebra/CGroups/zero_minus_apart.con". -inline cic:/CoRN/algebra/CGroups/inv_resp_ap_zero.con. +inline "cic:/CoRN/algebra/CGroups/inv_resp_ap_zero.con". -inline cic:/CoRN/algebra/CGroups/inv_resp_ap.con. +inline "cic:/CoRN/algebra/CGroups/inv_resp_ap.con". -inline cic:/CoRN/algebra/CGroups/minus_resp_ap_rht.con. +inline "cic:/CoRN/algebra/CGroups/minus_resp_ap_rht.con". -inline cic:/CoRN/algebra/CGroups/minus_resp_ap_lft.con. +inline "cic:/CoRN/algebra/CGroups/minus_resp_ap_lft.con". -inline cic:/CoRN/algebra/CGroups/minus_cancel_ap_rht.con. +inline "cic:/CoRN/algebra/CGroups/minus_cancel_ap_rht.con". (* UNEXPORTED -End cgroups_apartness. +End cgroups_apartness *) (* UNEXPORTED @@ -298,7 +308,7 @@ Hint Resolve minus_ap_zero zero_minus_apart inv_resp_ap_zero: algebra. *) (* UNEXPORTED -Section CGroup_Ops. +Section CGroup_Ops *) (*#* @@ -312,42 +322,42 @@ by [P] and [Q]. %\end{convention}% *) -inline cic:/CoRN/algebra/CGroups/G.var. +alias id "G" = "cic:/CoRN/algebra/CGroups/CGroup_Ops/G.var". -inline cic:/CoRN/algebra/CGroups/F.var. +alias id "F" = "cic:/CoRN/algebra/CGroups/CGroup_Ops/F.var". -inline cic:/CoRN/algebra/CGroups/F'.var. +alias id "F'" = "cic:/CoRN/algebra/CGroups/CGroup_Ops/F'.var". (* begin hide *) -inline cic:/CoRN/algebra/CGroups/P.con. +inline "cic:/CoRN/algebra/CGroups/CGroup_Ops/P.con" "CGroup_Ops__". -inline cic:/CoRN/algebra/CGroups/Q.con. +inline "cic:/CoRN/algebra/CGroups/CGroup_Ops/Q.con" "CGroup_Ops__". (* end hide *) (* UNEXPORTED -Section Part_Function_Inv. +Section Part_Function_Inv *) -inline cic:/CoRN/algebra/CGroups/part_function_inv_strext.con. +inline "cic:/CoRN/algebra/CGroups/part_function_inv_strext.con". -inline cic:/CoRN/algebra/CGroups/Finv.con. +inline "cic:/CoRN/algebra/CGroups/Finv.con". (* UNEXPORTED -End Part_Function_Inv. +End Part_Function_Inv *) (* UNEXPORTED -Section Part_Function_Minus. +Section Part_Function_Minus *) -inline cic:/CoRN/algebra/CGroups/part_function_minus_strext.con. +inline "cic:/CoRN/algebra/CGroups/part_function_minus_strext.con". -inline cic:/CoRN/algebra/CGroups/Fminus.con. +inline "cic:/CoRN/algebra/CGroups/Fminus.con". (* UNEXPORTED -End Part_Function_Minus. +End Part_Function_Minus *) (*#* @@ -355,30 +365,38 @@ End Part_Function_Minus. %\end{convention}% *) -inline cic:/CoRN/algebra/CGroups/R.var. +alias id "R" = "cic:/CoRN/algebra/CGroups/CGroup_Ops/R.var". -inline cic:/CoRN/algebra/CGroups/included_FInv.con. +inline "cic:/CoRN/algebra/CGroups/included_FInv.con". -inline cic:/CoRN/algebra/CGroups/included_FInv'.con. +inline "cic:/CoRN/algebra/CGroups/included_FInv'.con". -inline cic:/CoRN/algebra/CGroups/included_FMinus.con. +inline "cic:/CoRN/algebra/CGroups/included_FMinus.con". -inline cic:/CoRN/algebra/CGroups/included_FMinus'.con. +inline "cic:/CoRN/algebra/CGroups/included_FMinus'.con". -inline cic:/CoRN/algebra/CGroups/included_FMinus''.con. +inline "cic:/CoRN/algebra/CGroups/included_FMinus''.con". (* UNEXPORTED -End CGroup_Ops. +End CGroup_Ops *) (* UNEXPORTED Implicit Arguments Finv [G]. *) +(* NOTATION +Notation "{--} x" := (Finv x) (at level 2, right associativity). +*) + (* UNEXPORTED Implicit Arguments Fminus [G]. *) +(* NOTATION +Infix "{-}" := Fminus (at level 50, left associativity). +*) + (* UNEXPORTED Hint Resolve included_FInv included_FMinus : included. *)