X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcontribs%2FCoRN-Decl%2Ftactics%2FGroupReflection.ma;h=c314cc08968d84c20d8988ad80aa6195d67bcfc4;hb=62596f4e0a109e43c9df5da20571827c8b905ce4;hp=15858b6bea3cc2523aaa3a1956c187db8a788647;hpb=0e0d5c57eb154bf20d101f09e560401434156c1d;p=helm.git diff --git a/matita/contribs/CoRN-Decl/tactics/GroupReflection.ma b/matita/contribs/CoRN-Decl/tactics/GroupReflection.ma index 15858b6be..c314cc089 100644 --- a/matita/contribs/CoRN-Decl/tactics/GroupReflection.ma +++ b/matita/contribs/CoRN-Decl/tactics/GroupReflection.ma @@ -16,63 +16,61 @@ set "baseuri" "cic:/matita/CoRN-Decl/tactics/GroupReflection". +include "CoRN.ma". + (* $Id: GroupReflection.v,v 1.3 2004/04/23 10:01:06 lcf Exp $ *) (* begin hide *) -(* INCLUDE -CAbGroups -*) +include "algebra/CAbGroups.ma". -(* INCLUDE -AlgReflection -*) +include "tactics/AlgReflection.ma". (* UNEXPORTED -Section Group_Interpretation_Function. +Section Group_Interpretation_Function *) -inline cic:/CoRN/tactics/GroupReflection/G.var. +inline "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/G.var" "Group_Interpretation_Function__". -inline cic:/CoRN/tactics/GroupReflection/val.var. +inline "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/val.var" "Group_Interpretation_Function__". -inline cic:/CoRN/tactics/GroupReflection/unop.var. +inline "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/unop.var" "Group_Interpretation_Function__". -inline cic:/CoRN/tactics/GroupReflection/binop.var. +inline "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/binop.var" "Group_Interpretation_Function__". -inline cic:/CoRN/tactics/GroupReflection/pfun.var. +inline "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/pfun.var" "Group_Interpretation_Function__". -inline cic:/CoRN/tactics/GroupReflection/interpG.ind. +inline "cic:/CoRN/tactics/GroupReflection/interpG.ind". -inline cic:/CoRN/tactics/GroupReflection/wfG.con. +inline "cic:/CoRN/tactics/GroupReflection/wfG.con". -inline cic:/CoRN/tactics/GroupReflection/xexprG.ind. +inline "cic:/CoRN/tactics/GroupReflection/xexprG.ind". -inline cic:/CoRN/tactics/GroupReflection/xforgetG.con. +inline "cic:/CoRN/tactics/GroupReflection/xforgetG.con". -inline cic:/CoRN/tactics/GroupReflection/xinterpG.con. +inline "cic:/CoRN/tactics/GroupReflection/xinterpG.con". -inline cic:/CoRN/tactics/GroupReflection/xexprG2interpG.con. +inline "cic:/CoRN/tactics/GroupReflection/xexprG2interpG.con". -inline cic:/CoRN/tactics/GroupReflection/xexprG_diagram_commutes.con. +inline "cic:/CoRN/tactics/GroupReflection/xexprG_diagram_commutes.con". -inline cic:/CoRN/tactics/GroupReflection/xexprG2wfG.con. +inline "cic:/CoRN/tactics/GroupReflection/xexprG2wfG.con". -inline cic:/CoRN/tactics/GroupReflection/fexprG.ind. +inline "cic:/CoRN/tactics/GroupReflection/fexprG.ind". -inline cic:/CoRN/tactics/GroupReflection/fexprG_var.con. +inline "cic:/CoRN/tactics/GroupReflection/fexprG_var.con". -inline cic:/CoRN/tactics/GroupReflection/fexprG_zero.con. +inline "cic:/CoRN/tactics/GroupReflection/fexprG_zero.con". -inline cic:/CoRN/tactics/GroupReflection/fexprG_plus.con. +inline "cic:/CoRN/tactics/GroupReflection/fexprG_plus.con". -inline cic:/CoRN/tactics/GroupReflection/fexprG_mult_int.con. +inline "cic:/CoRN/tactics/GroupReflection/fexprG_mult_int.con". -inline cic:/CoRN/tactics/GroupReflection/fforgetG.con. +inline "cic:/CoRN/tactics/GroupReflection/fforgetG.con". -inline cic:/CoRN/tactics/GroupReflection/fexprG2interp.con. +inline "cic:/CoRN/tactics/GroupReflection/fexprG2interp.con". -inline cic:/CoRN/tactics/GroupReflection/fexprG2wf.con. +inline "cic:/CoRN/tactics/GroupReflection/fexprG2wf.con". (* UNEXPORTED Opaque csg_crr. @@ -126,27 +124,31 @@ Opaque cg_inv. Opaque cg_minus. *) -inline cic:/CoRN/tactics/GroupReflection/refl_interpG.con. +inline "cic:/CoRN/tactics/GroupReflection/refl_interpG.con". -inline cic:/CoRN/tactics/GroupReflection/interpG_wd.con. +inline "cic:/CoRN/tactics/GroupReflection/interpG_wd.con". (* UNEXPORTED -End Group_Interpretation_Function. +End Group_Interpretation_Function *) (* UNEXPORTED -Section Group_NormCorrect. +Section Group_NormCorrect *) -inline cic:/CoRN/tactics/GroupReflection/G.var. +inline "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/G.var" "Group_NormCorrect__". -inline cic:/CoRN/tactics/GroupReflection/val.var. +inline "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/val.var" "Group_NormCorrect__". -inline cic:/CoRN/tactics/GroupReflection/unop.var. +inline "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/unop.var" "Group_NormCorrect__". -inline cic:/CoRN/tactics/GroupReflection/binop.var. +inline "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/binop.var" "Group_NormCorrect__". -inline cic:/CoRN/tactics/GroupReflection/pfun.var. +inline "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/pfun.var" "Group_NormCorrect__". + +(* NOTATION +Notation II := (interpG G val unop binop pfun). +*) (* four kinds of exprs: @@ -162,13 +164,13 @@ M: sorted on V P: sorted on M, all M's not an I *) -inline cic:/CoRN/tactics/GroupReflection/MI_mult_comm_int.con. +inline "cic:/CoRN/tactics/GroupReflection/MI_mult_comm_int.con". (* UNEXPORTED Opaque Zmult. *) -inline cic:/CoRN/tactics/GroupReflection/MI_mult_corr_G.con. +inline "cic:/CoRN/tactics/GroupReflection/MI_mult_corr_G.con". (* UNEXPORTED Transparent Zmult. @@ -178,13 +180,13 @@ Transparent Zmult. Opaque MI_mult. *) -inline cic:/CoRN/tactics/GroupReflection/MV_mult_corr_G.con. +inline "cic:/CoRN/tactics/GroupReflection/MV_mult_corr_G.con". (* UNEXPORTED Opaque MV_mult. *) -inline cic:/CoRN/tactics/GroupReflection/MM_mult_corr_G.con. +inline "cic:/CoRN/tactics/GroupReflection/MM_mult_corr_G.con". (* UNEXPORTED Transparent MV_mult MI_mult. @@ -194,7 +196,7 @@ Transparent MV_mult MI_mult. Opaque MV_mult. *) -inline cic:/CoRN/tactics/GroupReflection/MM_plus_corr_G.con. +inline "cic:/CoRN/tactics/GroupReflection/MM_plus_corr_G.con". (* UNEXPORTED Transparent MV_mult. @@ -204,7 +206,7 @@ Transparent MV_mult. Opaque MM_plus. *) -inline cic:/CoRN/tactics/GroupReflection/PM_plus_corr_G.con. +inline "cic:/CoRN/tactics/GroupReflection/PM_plus_corr_G.con". (* UNEXPORTED Transparent MM_plus. @@ -214,7 +216,7 @@ Transparent MM_plus. Opaque PM_plus. *) -inline cic:/CoRN/tactics/GroupReflection/PP_plus_corr_G.con. +inline "cic:/CoRN/tactics/GroupReflection/PP_plus_corr_G.con". (* UNEXPORTED Transparent PM_plus. @@ -224,20 +226,20 @@ Transparent PM_plus. Opaque PM_plus MM_mult MI_mult. *) -inline cic:/CoRN/tactics/GroupReflection/PM_mult_corr_G.con. +inline "cic:/CoRN/tactics/GroupReflection/PM_mult_corr_G.con". (* UNEXPORTED Opaque PM_mult. *) -inline cic:/CoRN/tactics/GroupReflection/PP_mult_corr_G.con. +inline "cic:/CoRN/tactics/GroupReflection/PP_mult_corr_G.con". -inline cic:/CoRN/tactics/GroupReflection/NormG_corr_G.con. +inline "cic:/CoRN/tactics/GroupReflection/NormG_corr_G.con". -inline cic:/CoRN/tactics/GroupReflection/Tactic_lemmaG.con. +inline "cic:/CoRN/tactics/GroupReflection/Tactic_lemmaG.con". (* UNEXPORTED -End Group_NormCorrect. +End Group_NormCorrect *) (* end hide *)