X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Ftactics%2FFieldReflection.ma;h=70b61dea5a97b523772a8bb19c4c1a64f3624bdd;hb=946be00a2b9e1713e934414bd8419f267cca1077;hp=53d9f3dd07175a7a81127034d23687897cd50b8e;hpb=0e0d5c57eb154bf20d101f09e560401434156c1d;p=helm.git diff --git a/matita/contribs/CoRN-Decl/tactics/FieldReflection.ma b/matita/contribs/CoRN-Decl/tactics/FieldReflection.ma index 53d9f3dd0..70b61dea5 100644 --- a/matita/contribs/CoRN-Decl/tactics/FieldReflection.ma +++ b/matita/contribs/CoRN-Decl/tactics/FieldReflection.ma @@ -16,71 +16,67 @@ set "baseuri" "cic:/matita/CoRN-Decl/tactics/FieldReflection". +include "CoRN.ma". + (* $Id: FieldReflection.v,v 1.4 2004/04/23 10:01:06 lcf Exp $ *) (* begin hide *) -(* INCLUDE -CFields -*) +include "algebra/CFields.ma". -(* INCLUDE -AlgReflection -*) +include "tactics/AlgReflection.ma". (* UNEXPORTED Section Field_Interpretation_Function. *) -inline cic:/CoRN/tactics/FieldReflection/F.var. +inline "cic:/CoRN/tactics/FieldReflection/F.var". -inline cic:/CoRN/tactics/FieldReflection/val.var. +inline "cic:/CoRN/tactics/FieldReflection/val.var". -inline cic:/CoRN/tactics/FieldReflection/unop.var. +inline "cic:/CoRN/tactics/FieldReflection/unop.var". -inline cic:/CoRN/tactics/FieldReflection/binop.var. +inline "cic:/CoRN/tactics/FieldReflection/binop.var". -inline cic:/CoRN/tactics/FieldReflection/pfun.var. +inline "cic:/CoRN/tactics/FieldReflection/pfun.var". -inline cic:/CoRN/tactics/FieldReflection/interpF.ind. +inline "cic:/CoRN/tactics/FieldReflection/interpF.ind". -inline cic:/CoRN/tactics/FieldReflection/wfF.con. +inline "cic:/CoRN/tactics/FieldReflection/wfF.con". -inline cic:/CoRN/tactics/FieldReflection/xexprF.ind. +inline "cic:/CoRN/tactics/FieldReflection/xexprF.ind". -inline cic:/CoRN/tactics/FieldReflection/xforgetF.con. +inline "cic:/CoRN/tactics/FieldReflection/xforgetF.con". -inline cic:/CoRN/tactics/FieldReflection/xinterpF.con. +inline "cic:/CoRN/tactics/FieldReflection/xinterpF.con". -inline cic:/CoRN/tactics/FieldReflection/xexprF2interpF.con. +inline "cic:/CoRN/tactics/FieldReflection/xexprF2interpF.con". -inline cic:/CoRN/tactics/FieldReflection/xexprF_diagram_commutes.con. +inline "cic:/CoRN/tactics/FieldReflection/xexprF_diagram_commutes.con". -inline cic:/CoRN/tactics/FieldReflection/xexprF2wfF.con. +inline "cic:/CoRN/tactics/FieldReflection/xexprF2wfF.con". -inline cic:/CoRN/tactics/FieldReflection/fexprF.ind. +inline "cic:/CoRN/tactics/FieldReflection/fexprF.ind". -inline cic:/CoRN/tactics/FieldReflection/fexprF_var.con. +inline "cic:/CoRN/tactics/FieldReflection/fexprF_var.con". -inline cic:/CoRN/tactics/FieldReflection/fexprF_int.con. +inline "cic:/CoRN/tactics/FieldReflection/fexprF_int.con". -inline cic:/CoRN/tactics/FieldReflection/fexprF_plus.con. +inline "cic:/CoRN/tactics/FieldReflection/fexprF_plus.con". -inline cic:/CoRN/tactics/FieldReflection/fexprF_mult.con. +inline "cic:/CoRN/tactics/FieldReflection/fexprF_mult.con". -inline cic:/CoRN/tactics/FieldReflection/fforgetF.con. +inline "cic:/CoRN/tactics/FieldReflection/fforgetF.con". -inline cic:/CoRN/tactics/FieldReflection/fexprF2interpF.con. +inline "cic:/CoRN/tactics/FieldReflection/fexprF2interpF.con". -inline cic:/CoRN/tactics/FieldReflection/fexprF2wfF.con. +inline "cic:/CoRN/tactics/FieldReflection/fexprF2wfF.con". -(* INCLUDE -Opaque_algebra -*) +include "tactics/Opaque_algebra.ma". -inline cic:/CoRN/tactics/FieldReflection/refl_interpF.con. +inline "cic:/CoRN/tactics/FieldReflection/refl_interpF.con". -inline cic:/CoRN/tactics/FieldReflection/interpF_wd.con. +inline "cic:/CoRN/tactics/FieldReflection/interpF_wd.con". (* UNEXPORTED End Field_Interpretation_Function. @@ -90,15 +86,19 @@ End Field_Interpretation_Function. Section Field_NormCorrect. *) -inline cic:/CoRN/tactics/FieldReflection/F.var. +inline "cic:/CoRN/tactics/FieldReflection/F.var". + +inline "cic:/CoRN/tactics/FieldReflection/val.var". -inline cic:/CoRN/tactics/FieldReflection/val.var. +inline "cic:/CoRN/tactics/FieldReflection/unop.var". -inline cic:/CoRN/tactics/FieldReflection/unop.var. +inline "cic:/CoRN/tactics/FieldReflection/binop.var". -inline cic:/CoRN/tactics/FieldReflection/binop.var. +inline "cic:/CoRN/tactics/FieldReflection/pfun.var". -inline cic:/CoRN/tactics/FieldReflection/pfun.var. +(* NOTATION +Notation II := (interpF F val unop binop pfun). +*) (* four kinds of exprs: @@ -118,7 +118,7 @@ P: sorted on M, all M's not an I Opaque Zmult. *) -inline cic:/CoRN/tactics/FieldReflection/MI_mult_corr_F.con. +inline "cic:/CoRN/tactics/FieldReflection/MI_mult_corr_F.con". (* UNEXPORTED Transparent Zmult. @@ -128,7 +128,7 @@ Transparent Zmult. Opaque MI_mult. *) -inline cic:/CoRN/tactics/FieldReflection/MV_mult_corr_F.con. +inline "cic:/CoRN/tactics/FieldReflection/MV_mult_corr_F.con". (* UNEXPORTED Transparent MI_mult. @@ -138,7 +138,7 @@ Transparent MI_mult. Opaque MV_mult MI_mult. *) -inline cic:/CoRN/tactics/FieldReflection/MM_mult_corr_F.con. +inline "cic:/CoRN/tactics/FieldReflection/MM_mult_corr_F.con". (* UNEXPORTED Transparent MV_mult MI_mult. @@ -148,7 +148,7 @@ Transparent MV_mult MI_mult. Opaque MV_mult. *) -inline cic:/CoRN/tactics/FieldReflection/MM_plus_corr_F.con. +inline "cic:/CoRN/tactics/FieldReflection/MM_plus_corr_F.con". (* UNEXPORTED Transparent MV_mult. @@ -158,7 +158,7 @@ Transparent MV_mult. Opaque MM_plus. *) -inline cic:/CoRN/tactics/FieldReflection/PM_plus_corr_F.con. +inline "cic:/CoRN/tactics/FieldReflection/PM_plus_corr_F.con". (* UNEXPORTED Transparent MM_plus. @@ -168,7 +168,7 @@ Transparent MM_plus. Opaque PM_plus. *) -inline cic:/CoRN/tactics/FieldReflection/PP_plus_corr_F.con. +inline "cic:/CoRN/tactics/FieldReflection/PP_plus_corr_F.con". (* UNEXPORTED Transparent PM_plus. @@ -178,37 +178,37 @@ Transparent PM_plus. Opaque PM_plus MM_mult MI_mult. *) -inline cic:/CoRN/tactics/FieldReflection/PM_mult_corr_F.con. +inline "cic:/CoRN/tactics/FieldReflection/PM_mult_corr_F.con". (* UNEXPORTED Opaque PM_mult. *) -inline cic:/CoRN/tactics/FieldReflection/PP_mult_corr_F.con. +inline "cic:/CoRN/tactics/FieldReflection/PP_mult_corr_F.con". (* UNEXPORTED Transparent PP_plus PM_mult PP_mult PM_plus MI_mult. *) -inline cic:/CoRN/tactics/FieldReflection/FF_plus_corr_F.con. +inline "cic:/CoRN/tactics/FieldReflection/FF_plus_corr_F.con". -inline cic:/CoRN/tactics/FieldReflection/FF_mult_corr_F.con. +inline "cic:/CoRN/tactics/FieldReflection/FF_mult_corr_F.con". (* UNEXPORTED Transparent FF_div. *) -inline cic:/CoRN/tactics/FieldReflection/FF_div_corr_F.con. +inline "cic:/CoRN/tactics/FieldReflection/FF_div_corr_F.con". -inline cic:/CoRN/tactics/FieldReflection/NormF_corr.con. +inline "cic:/CoRN/tactics/FieldReflection/NormF_corr.con". -inline cic:/CoRN/tactics/FieldReflection/Norm_wfF.con. +inline "cic:/CoRN/tactics/FieldReflection/Norm_wfF.con". -inline cic:/CoRN/tactics/FieldReflection/expr_is_zero_corr_F.con. +inline "cic:/CoRN/tactics/FieldReflection/expr_is_zero_corr_F.con". -inline cic:/CoRN/tactics/FieldReflection/Tactic_lemma_zero_F.con. +inline "cic:/CoRN/tactics/FieldReflection/Tactic_lemma_zero_F.con". -inline cic:/CoRN/tactics/FieldReflection/Tactic_lemmaF.con. +inline "cic:/CoRN/tactics/FieldReflection/Tactic_lemmaF.con". (* UNEXPORTED End Field_NormCorrect.