X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Ftactics%2FRingReflection.ma;h=84a076ad99d28cb5c0ebe3eab29cfdbf71a3db6d;hb=11a6c88f3e717b019be2eae71711c70473b5467a;hp=bd88498502e23bed029a7d995898f307d03d4844;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/tactics/RingReflection.ma b/helm/software/matita/contribs/CoRN-Decl/tactics/RingReflection.ma index bd8849850..84a076ad9 100644 --- a/helm/software/matita/contribs/CoRN-Decl/tactics/RingReflection.ma +++ b/helm/software/matita/contribs/CoRN-Decl/tactics/RingReflection.ma @@ -16,63 +16,61 @@ set "baseuri" "cic:/matita/CoRN-Decl/tactics/RingReflection". +include "CoRN.ma". + (* $Id: RingReflection.v,v 1.4 2004/04/23 10:01:06 lcf Exp $ *) (* begin hide *) -(* INCLUDE -CRings -*) +include "algebra/CRings.ma". -(* INCLUDE -AlgReflection -*) +include "tactics/AlgReflection.ma". (* UNEXPORTED -Section Ring_Interpretation_Function. +Section Ring_Interpretation_Function *) -inline cic:/CoRN/tactics/RingReflection/R.var. +alias id "R" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/R.var". -inline cic:/CoRN/tactics/RingReflection/val.var. +alias id "val" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/val.var". -inline cic:/CoRN/tactics/RingReflection/unop.var. +alias id "unop" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/unop.var". -inline cic:/CoRN/tactics/RingReflection/binop.var. +alias id "binop" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/binop.var". -inline cic:/CoRN/tactics/RingReflection/pfun.var. +alias id "pfun" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/pfun.var". -inline cic:/CoRN/tactics/RingReflection/interpR.ind. +inline "cic:/CoRN/tactics/RingReflection/interpR.ind". -inline cic:/CoRN/tactics/RingReflection/wfR.con. +inline "cic:/CoRN/tactics/RingReflection/wfR.con". -inline cic:/CoRN/tactics/RingReflection/xexprR.ind. +inline "cic:/CoRN/tactics/RingReflection/xexprR.ind". -inline cic:/CoRN/tactics/RingReflection/xforgetR.con. +inline "cic:/CoRN/tactics/RingReflection/xforgetR.con". -inline cic:/CoRN/tactics/RingReflection/xinterpR.con. +inline "cic:/CoRN/tactics/RingReflection/xinterpR.con". -inline cic:/CoRN/tactics/RingReflection/xexprR2interpR.con. +inline "cic:/CoRN/tactics/RingReflection/xexprR2interpR.con". -inline cic:/CoRN/tactics/RingReflection/xexprR_diagram_commutes.con. +inline "cic:/CoRN/tactics/RingReflection/xexprR_diagram_commutes.con". -inline cic:/CoRN/tactics/RingReflection/xexprR2wfR.con. +inline "cic:/CoRN/tactics/RingReflection/xexprR2wfR.con". -inline cic:/CoRN/tactics/RingReflection/fexprR.ind. +inline "cic:/CoRN/tactics/RingReflection/fexprR.ind". -inline cic:/CoRN/tactics/RingReflection/fexprR_var.con. +inline "cic:/CoRN/tactics/RingReflection/fexprR_var.con". -inline cic:/CoRN/tactics/RingReflection/fexprR_int.con. +inline "cic:/CoRN/tactics/RingReflection/fexprR_int.con". -inline cic:/CoRN/tactics/RingReflection/fexprR_plus.con. +inline "cic:/CoRN/tactics/RingReflection/fexprR_plus.con". -inline cic:/CoRN/tactics/RingReflection/fexprR_mult.con. +inline "cic:/CoRN/tactics/RingReflection/fexprR_mult.con". -inline cic:/CoRN/tactics/RingReflection/fforgetR.con. +inline "cic:/CoRN/tactics/RingReflection/fforgetR.con". -inline cic:/CoRN/tactics/RingReflection/fexprR2interp.con. +inline "cic:/CoRN/tactics/RingReflection/fexprR2interp.con". -inline cic:/CoRN/tactics/RingReflection/fexprR2wf.con. +inline "cic:/CoRN/tactics/RingReflection/fexprR2wf.con". (* UNEXPORTED Opaque csg_crr. @@ -142,27 +140,31 @@ Opaque cr_mult. Opaque nexp_op. *) -inline cic:/CoRN/tactics/RingReflection/refl_interpR.con. +inline "cic:/CoRN/tactics/RingReflection/refl_interpR.con". -inline cic:/CoRN/tactics/RingReflection/interpR_wd.con. +inline "cic:/CoRN/tactics/RingReflection/interpR_wd.con". (* UNEXPORTED -End Ring_Interpretation_Function. +End Ring_Interpretation_Function *) (* UNEXPORTED -Section Ring_NormCorrect. +Section Ring_NormCorrect *) -inline cic:/CoRN/tactics/RingReflection/R.var. +alias id "R" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/R.var". -inline cic:/CoRN/tactics/RingReflection/val.var. +alias id "val" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/val.var". -inline cic:/CoRN/tactics/RingReflection/unop.var. +alias id "unop" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/unop.var". -inline cic:/CoRN/tactics/RingReflection/binop.var. +alias id "binop" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/binop.var". -inline cic:/CoRN/tactics/RingReflection/pfun.var. +alias id "pfun" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/pfun.var". + +(* NOTATION +Notation II := (interpR R val unop binop pfun). +*) (* four kinds of exprs: @@ -182,7 +184,7 @@ P: sorted on M, all M's not an I Opaque Zmult. *) -inline cic:/CoRN/tactics/RingReflection/MI_mult_corr_R.con. +inline "cic:/CoRN/tactics/RingReflection/MI_mult_corr_R.con". (* UNEXPORTED Transparent Zmult. @@ -192,7 +194,7 @@ Transparent Zmult. Opaque MI_mult. *) -inline cic:/CoRN/tactics/RingReflection/MV_mult_corr_R.con. +inline "cic:/CoRN/tactics/RingReflection/MV_mult_corr_R.con". (* UNEXPORTED Transparent MI_mult. @@ -202,7 +204,7 @@ Transparent MI_mult. Opaque MV_mult MI_mult. *) -inline cic:/CoRN/tactics/RingReflection/MM_mult_corr_R.con. +inline "cic:/CoRN/tactics/RingReflection/MM_mult_corr_R.con". (* UNEXPORTED Transparent MV_mult MI_mult. @@ -212,7 +214,7 @@ Transparent MV_mult MI_mult. Opaque MV_mult. *) -inline cic:/CoRN/tactics/RingReflection/MM_plus_corr_R.con. +inline "cic:/CoRN/tactics/RingReflection/MM_plus_corr_R.con". (* UNEXPORTED Transparent MV_mult. @@ -222,7 +224,7 @@ Transparent MV_mult. Opaque MM_plus. *) -inline cic:/CoRN/tactics/RingReflection/PM_plus_corr_R.con. +inline "cic:/CoRN/tactics/RingReflection/PM_plus_corr_R.con". (* UNEXPORTED Transparent MM_plus. @@ -232,7 +234,7 @@ Transparent MM_plus. Opaque PM_plus. *) -inline cic:/CoRN/tactics/RingReflection/PP_plus_corr_R.con. +inline "cic:/CoRN/tactics/RingReflection/PP_plus_corr_R.con". (* UNEXPORTED Transparent PM_plus. @@ -242,13 +244,13 @@ Transparent PM_plus. Opaque PM_plus MM_mult MI_mult. *) -inline cic:/CoRN/tactics/RingReflection/PM_mult_corr_R.con. +inline "cic:/CoRN/tactics/RingReflection/PM_mult_corr_R.con". (* UNEXPORTED Opaque PM_mult. *) -inline cic:/CoRN/tactics/RingReflection/PP_mult_corr_R.con. +inline "cic:/CoRN/tactics/RingReflection/PP_mult_corr_R.con". (* Transparent PP_plus PM_mult PP_mult PM_plus MI_mult. @@ -310,12 +312,12 @@ Step_final x2. Qed. *) -inline cic:/CoRN/tactics/RingReflection/NormR_corr.con. +inline "cic:/CoRN/tactics/RingReflection/NormR_corr.con". -inline cic:/CoRN/tactics/RingReflection/Tactic_lemmaR.con. +inline "cic:/CoRN/tactics/RingReflection/Tactic_lemmaR.con". (* UNEXPORTED -End Ring_NormCorrect. +End Ring_NormCorrect *) (* end hide *)