1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: FieldReflection.v,v 1.4 2004/04/23 10:01:06 lcf Exp $ *)
23 include "algebra/CFields.ma".
25 include "tactics/AlgReflection.ma".
28 Section Field_Interpretation_Function
31 alias id "F" = "cic:/CoRN/tactics/FieldReflection/Field_Interpretation_Function/F.var".
33 alias id "val" = "cic:/CoRN/tactics/FieldReflection/Field_Interpretation_Function/val.var".
35 alias id "unop" = "cic:/CoRN/tactics/FieldReflection/Field_Interpretation_Function/unop.var".
37 alias id "binop" = "cic:/CoRN/tactics/FieldReflection/Field_Interpretation_Function/binop.var".
39 alias id "pfun" = "cic:/CoRN/tactics/FieldReflection/Field_Interpretation_Function/pfun.var".
41 inline procedural "cic:/CoRN/tactics/FieldReflection/interpF.ind".
43 inline procedural "cic:/CoRN/tactics/FieldReflection/wfF.con" as definition.
45 inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF.ind".
47 inline procedural "cic:/CoRN/tactics/FieldReflection/xforgetF.con" as definition.
49 inline procedural "cic:/CoRN/tactics/FieldReflection/xinterpF.con" as definition.
51 inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF2interpF.con" as lemma.
53 inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF_diagram_commutes.con" as definition.
55 inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF2wfF.con" as lemma.
57 inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF.ind".
59 inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_var.con" as definition.
61 inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_int.con" as definition.
63 inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_plus.con" as definition.
65 inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_mult.con" as definition.
67 inline procedural "cic:/CoRN/tactics/FieldReflection/fforgetF.con" as definition.
69 inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF2interpF.con" as lemma.
71 inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF2wfF.con" as lemma.
73 include "tactics/Opaque_algebra.ma".
75 inline procedural "cic:/CoRN/tactics/FieldReflection/refl_interpF.con" as lemma.
77 inline procedural "cic:/CoRN/tactics/FieldReflection/interpF_wd.con" as lemma.
80 End Field_Interpretation_Function
84 Section Field_NormCorrect
87 alias id "F" = "cic:/CoRN/tactics/FieldReflection/Field_NormCorrect/F.var".
89 alias id "val" = "cic:/CoRN/tactics/FieldReflection/Field_NormCorrect/val.var".
91 alias id "unop" = "cic:/CoRN/tactics/FieldReflection/Field_NormCorrect/unop.var".
93 alias id "binop" = "cic:/CoRN/tactics/FieldReflection/Field_NormCorrect/binop.var".
95 alias id "pfun" = "cic:/CoRN/tactics/FieldReflection/Field_NormCorrect/pfun.var".
98 Notation II := (interpF F val unop binop pfun).
112 P: sorted on M, all M's not an I
119 inline procedural "cic:/CoRN/tactics/FieldReflection/MI_mult_corr_F.con" as lemma.
129 inline procedural "cic:/CoRN/tactics/FieldReflection/MV_mult_corr_F.con" as lemma.
136 Opaque MV_mult MI_mult.
139 inline procedural "cic:/CoRN/tactics/FieldReflection/MM_mult_corr_F.con" as lemma.
142 Transparent MV_mult MI_mult.
149 inline procedural "cic:/CoRN/tactics/FieldReflection/MM_plus_corr_F.con" as lemma.
159 inline procedural "cic:/CoRN/tactics/FieldReflection/PM_plus_corr_F.con" as lemma.
169 inline procedural "cic:/CoRN/tactics/FieldReflection/PP_plus_corr_F.con" as lemma.
176 Opaque PM_plus MM_mult MI_mult.
179 inline procedural "cic:/CoRN/tactics/FieldReflection/PM_mult_corr_F.con" as lemma.
185 inline procedural "cic:/CoRN/tactics/FieldReflection/PP_mult_corr_F.con" as lemma.
188 Transparent PP_plus PM_mult PP_mult PM_plus MI_mult.
191 inline procedural "cic:/CoRN/tactics/FieldReflection/FF_plus_corr_F.con" as lemma.
193 inline procedural "cic:/CoRN/tactics/FieldReflection/FF_mult_corr_F.con" as lemma.
199 inline procedural "cic:/CoRN/tactics/FieldReflection/FF_div_corr_F.con" as lemma.
201 inline procedural "cic:/CoRN/tactics/FieldReflection/NormF_corr.con" as lemma.
203 inline procedural "cic:/CoRN/tactics/FieldReflection/Norm_wfF.con" as lemma.
205 inline procedural "cic:/CoRN/tactics/FieldReflection/expr_is_zero_corr_F.con" as lemma.
207 inline procedural "cic:/CoRN/tactics/FieldReflection/Tactic_lemma_zero_F.con" as lemma.
209 inline procedural "cic:/CoRN/tactics/FieldReflection/Tactic_lemmaF.con" as lemma.
212 End Field_NormCorrect