helm/software/matita/contribs/CoRN-Procedural/tactics/FieldReflection.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 (* $Id: FieldReflection.v,v 1.4 2004/04/23 10:01:06 lcf Exp $ *)
  20
  21 (* begin hide *)
  22
  23 include "algebra/CFields.ma".
  24
  25 include "tactics/AlgReflection.ma".
  26
  27 (* UNEXPORTED
  28 Section Field_Interpretation_Function
  29 *)
  30
  31 alias id "F" = "cic:/CoRN/tactics/FieldReflection/Field_Interpretation_Function/F.var".
  32
  33 alias id "val" = "cic:/CoRN/tactics/FieldReflection/Field_Interpretation_Function/val.var".
  34
  35 alias id "unop" = "cic:/CoRN/tactics/FieldReflection/Field_Interpretation_Function/unop.var".
  36
  37 alias id "binop" = "cic:/CoRN/tactics/FieldReflection/Field_Interpretation_Function/binop.var".
  38
  39 alias id "pfun" = "cic:/CoRN/tactics/FieldReflection/Field_Interpretation_Function/pfun.var".
  40
  41 inline procedural "cic:/CoRN/tactics/FieldReflection/interpF.ind".
  42
  43 inline procedural "cic:/CoRN/tactics/FieldReflection/wfF.con".
  44
  45 inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF.ind".
  46
  47 inline procedural "cic:/CoRN/tactics/FieldReflection/xforgetF.con".
  48
  49 inline procedural "cic:/CoRN/tactics/FieldReflection/xinterpF.con".
  50
  51 inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF2interpF.con".
  52
  53 inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF_diagram_commutes.con".
  54
  55 inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF2wfF.con".
  56
  57 inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF.ind".
  58
  59 inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_var.con".
  60
  61 inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_int.con".
  62
  63 inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_plus.con".
  64
  65 inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_mult.con".
  66
  67 inline procedural "cic:/CoRN/tactics/FieldReflection/fforgetF.con".
  68
  69 inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF2interpF.con".
  70
  71 inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF2wfF.con".
  72
  73 include "tactics/Opaque_algebra.ma".
  74
  75 inline procedural "cic:/CoRN/tactics/FieldReflection/refl_interpF.con".
  76
  77 inline procedural "cic:/CoRN/tactics/FieldReflection/interpF_wd.con".
  78
  79 (* UNEXPORTED
  80 End Field_Interpretation_Function
  81 *)
  82
  83 (* UNEXPORTED
  84 Section Field_NormCorrect
  85 *)
  86
  87 alias id "F" = "cic:/CoRN/tactics/FieldReflection/Field_NormCorrect/F.var".
  88
  89 alias id "val" = "cic:/CoRN/tactics/FieldReflection/Field_NormCorrect/val.var".
  90
  91 alias id "unop" = "cic:/CoRN/tactics/FieldReflection/Field_NormCorrect/unop.var".
  92
  93 alias id "binop" = "cic:/CoRN/tactics/FieldReflection/Field_NormCorrect/binop.var".
  94
  95 alias id "pfun" = "cic:/CoRN/tactics/FieldReflection/Field_NormCorrect/pfun.var".
  96
  97 (* NOTATION
  98 Notation II := (interpF F val unop binop pfun).
  99 *)
 100
 101 (*
 102 four kinds of exprs:
 103
 104   I     (expr_int _)
 105   V     (expr_var _)
 106   M     (expr_mult V M)
 107         I
 108   P     (expr_plus M P)
 109         I
 110
 111 M: sorted on V
 112 P: sorted on M, all M's not an I
 113 *)
 114
 115 (* UNEXPORTED
 116 Opaque Zmult.
 117 *)
 118
 119 inline procedural "cic:/CoRN/tactics/FieldReflection/MI_mult_corr_F.con".
 120
 121 (* UNEXPORTED
 122 Transparent Zmult.
 123 *)
 124
 125 (* UNEXPORTED
 126 Opaque MI_mult.
 127 *)
 128
 129 inline procedural "cic:/CoRN/tactics/FieldReflection/MV_mult_corr_F.con".
 130
 131 (* UNEXPORTED
 132 Transparent MI_mult.
 133 *)
 134
 135 (* UNEXPORTED
 136 Opaque MV_mult MI_mult.
 137 *)
 138
 139 inline procedural "cic:/CoRN/tactics/FieldReflection/MM_mult_corr_F.con".
 140
 141 (* UNEXPORTED
 142 Transparent MV_mult MI_mult.
 143 *)
 144
 145 (* UNEXPORTED
 146 Opaque MV_mult.
 147 *)
 148
 149 inline procedural "cic:/CoRN/tactics/FieldReflection/MM_plus_corr_F.con".
 150
 151 (* UNEXPORTED
 152 Transparent MV_mult.
 153 *)
 154
 155 (* UNEXPORTED
 156 Opaque MM_plus.
 157 *)
 158
 159 inline procedural "cic:/CoRN/tactics/FieldReflection/PM_plus_corr_F.con".
 160
 161 (* UNEXPORTED
 162 Transparent MM_plus.
 163 *)
 164
 165 (* UNEXPORTED
 166 Opaque PM_plus.
 167 *)
 168
 169 inline procedural "cic:/CoRN/tactics/FieldReflection/PP_plus_corr_F.con".
 170
 171 (* UNEXPORTED
 172 Transparent PM_plus.
 173 *)
 174
 175 (* UNEXPORTED
 176 Opaque PM_plus MM_mult MI_mult.
 177 *)
 178
 179 inline procedural "cic:/CoRN/tactics/FieldReflection/PM_mult_corr_F.con".
 180
 181 (* UNEXPORTED
 182 Opaque PM_mult.
 183 *)
 184
 185 inline procedural "cic:/CoRN/tactics/FieldReflection/PP_mult_corr_F.con".
 186
 187 (* UNEXPORTED
 188 Transparent PP_plus PM_mult PP_mult PM_plus MI_mult.
 189 *)
 190
 191 inline procedural "cic:/CoRN/tactics/FieldReflection/FF_plus_corr_F.con".
 192
 193 inline procedural "cic:/CoRN/tactics/FieldReflection/FF_mult_corr_F.con".
 194
 195 (* UNEXPORTED
 196 Transparent FF_div.
 197 *)
 198
 199 inline procedural "cic:/CoRN/tactics/FieldReflection/FF_div_corr_F.con".
 200
 201 inline procedural "cic:/CoRN/tactics/FieldReflection/NormF_corr.con".
 202
 203 inline procedural "cic:/CoRN/tactics/FieldReflection/Norm_wfF.con".
 204
 205 inline procedural "cic:/CoRN/tactics/FieldReflection/expr_is_zero_corr_F.con".
 206
 207 inline procedural "cic:/CoRN/tactics/FieldReflection/Tactic_lemma_zero_F.con".
 208
 209 inline procedural "cic:/CoRN/tactics/FieldReflection/Tactic_lemmaF.con".
 210
 211 (* UNEXPORTED
 212 End Field_NormCorrect
 213 *)
 214
 215 (* end hide *)
 216