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: GroupReflection.v,v 1.3 2004/04/23 10:01:06 lcf Exp $ *)
23 include "algebra/CAbGroups.ma".
25 include "tactics/AlgReflection.ma".
28 Section Group_Interpretation_Function
32 cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/G.var
36 cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/val.var
40 cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/unop.var
44 cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/binop.var
48 cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/pfun.var
51 inline procedural "cic:/CoRN/tactics/GroupReflection/interpG.ind".
53 inline procedural "cic:/CoRN/tactics/GroupReflection/wfG.con" as definition.
55 inline procedural "cic:/CoRN/tactics/GroupReflection/xexprG.ind".
57 inline procedural "cic:/CoRN/tactics/GroupReflection/xforgetG.con" as definition.
59 inline procedural "cic:/CoRN/tactics/GroupReflection/xinterpG.con" as definition.
61 inline procedural "cic:/CoRN/tactics/GroupReflection/xexprG2interpG.con" as lemma.
63 inline procedural "cic:/CoRN/tactics/GroupReflection/xexprG_diagram_commutes.con" as definition.
65 inline procedural "cic:/CoRN/tactics/GroupReflection/xexprG2wfG.con" as lemma.
67 inline procedural "cic:/CoRN/tactics/GroupReflection/fexprG.ind".
69 inline procedural "cic:/CoRN/tactics/GroupReflection/fexprG_var.con" as definition.
71 inline procedural "cic:/CoRN/tactics/GroupReflection/fexprG_zero.con" as definition.
73 inline procedural "cic:/CoRN/tactics/GroupReflection/fexprG_plus.con" as definition.
75 inline procedural "cic:/CoRN/tactics/GroupReflection/fexprG_mult_int.con" as definition.
77 inline procedural "cic:/CoRN/tactics/GroupReflection/fforgetG.con" as definition.
79 inline procedural "cic:/CoRN/tactics/GroupReflection/fexprG2interp.con" as lemma.
81 inline procedural "cic:/CoRN/tactics/GroupReflection/fexprG2wf.con" as lemma.
135 inline procedural "cic:/CoRN/tactics/GroupReflection/refl_interpG.con" as lemma.
137 inline procedural "cic:/CoRN/tactics/GroupReflection/interpG_wd.con" as lemma.
140 End Group_Interpretation_Function
144 Section Group_NormCorrect
148 cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/G.var
152 cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/val.var
156 cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/unop.var
160 cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/binop.var
164 cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/pfun.var
168 Notation II := (interpG G val unop binop pfun).
182 P: sorted on M, all M's not an I
185 inline procedural "cic:/CoRN/tactics/GroupReflection/MI_mult_comm_int.con" as lemma.
191 inline procedural "cic:/CoRN/tactics/GroupReflection/MI_mult_corr_G.con" as lemma.
201 inline procedural "cic:/CoRN/tactics/GroupReflection/MV_mult_corr_G.con" as lemma.
207 inline procedural "cic:/CoRN/tactics/GroupReflection/MM_mult_corr_G.con" as lemma.
210 Transparent MV_mult MI_mult.
217 inline procedural "cic:/CoRN/tactics/GroupReflection/MM_plus_corr_G.con" as lemma.
227 inline procedural "cic:/CoRN/tactics/GroupReflection/PM_plus_corr_G.con" as lemma.
237 inline procedural "cic:/CoRN/tactics/GroupReflection/PP_plus_corr_G.con" as lemma.
244 Opaque PM_plus MM_mult MI_mult.
247 inline procedural "cic:/CoRN/tactics/GroupReflection/PM_mult_corr_G.con" as lemma.
253 inline procedural "cic:/CoRN/tactics/GroupReflection/PP_mult_corr_G.con" as lemma.
255 inline procedural "cic:/CoRN/tactics/GroupReflection/NormG_corr_G.con" as lemma.
257 inline procedural "cic:/CoRN/tactics/GroupReflection/Tactic_lemmaG.con" as lemma.
260 End Group_NormCorrect