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
31 alias id "G" = "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/G.var".
33 alias id "val" = "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/val.var".
35 alias id "unop" = "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/unop.var".
37 alias id "binop" = "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/binop.var".
39 alias id "pfun" = "cic:/CoRN/tactics/GroupReflection/Group_Interpretation_Function/pfun.var".
41 inline procedural "cic:/CoRN/tactics/GroupReflection/interpG.ind".
43 inline procedural "cic:/CoRN/tactics/GroupReflection/wfG.con".
45 inline procedural "cic:/CoRN/tactics/GroupReflection/xexprG.ind".
47 inline procedural "cic:/CoRN/tactics/GroupReflection/xforgetG.con".
49 inline procedural "cic:/CoRN/tactics/GroupReflection/xinterpG.con".
51 inline procedural "cic:/CoRN/tactics/GroupReflection/xexprG2interpG.con".
53 inline procedural "cic:/CoRN/tactics/GroupReflection/xexprG_diagram_commutes.con".
55 inline procedural "cic:/CoRN/tactics/GroupReflection/xexprG2wfG.con".
57 inline procedural "cic:/CoRN/tactics/GroupReflection/fexprG.ind".
59 inline procedural "cic:/CoRN/tactics/GroupReflection/fexprG_var.con".
61 inline procedural "cic:/CoRN/tactics/GroupReflection/fexprG_zero.con".
63 inline procedural "cic:/CoRN/tactics/GroupReflection/fexprG_plus.con".
65 inline procedural "cic:/CoRN/tactics/GroupReflection/fexprG_mult_int.con".
67 inline procedural "cic:/CoRN/tactics/GroupReflection/fforgetG.con".
69 inline procedural "cic:/CoRN/tactics/GroupReflection/fexprG2interp.con".
71 inline procedural "cic:/CoRN/tactics/GroupReflection/fexprG2wf.con".
125 inline procedural "cic:/CoRN/tactics/GroupReflection/refl_interpG.con".
127 inline procedural "cic:/CoRN/tactics/GroupReflection/interpG_wd.con".
130 End Group_Interpretation_Function
134 Section Group_NormCorrect
137 alias id "G" = "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/G.var".
139 alias id "val" = "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/val.var".
141 alias id "unop" = "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/unop.var".
143 alias id "binop" = "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/binop.var".
145 alias id "pfun" = "cic:/CoRN/tactics/GroupReflection/Group_NormCorrect/pfun.var".
148 Notation II := (interpG G val unop binop pfun).
162 P: sorted on M, all M's not an I
165 inline procedural "cic:/CoRN/tactics/GroupReflection/MI_mult_comm_int.con".
171 inline procedural "cic:/CoRN/tactics/GroupReflection/MI_mult_corr_G.con".
181 inline procedural "cic:/CoRN/tactics/GroupReflection/MV_mult_corr_G.con".
187 inline procedural "cic:/CoRN/tactics/GroupReflection/MM_mult_corr_G.con".
190 Transparent MV_mult MI_mult.
197 inline procedural "cic:/CoRN/tactics/GroupReflection/MM_plus_corr_G.con".
207 inline procedural "cic:/CoRN/tactics/GroupReflection/PM_plus_corr_G.con".
217 inline procedural "cic:/CoRN/tactics/GroupReflection/PP_plus_corr_G.con".
224 Opaque PM_plus MM_mult MI_mult.
227 inline procedural "cic:/CoRN/tactics/GroupReflection/PM_mult_corr_G.con".
233 inline procedural "cic:/CoRN/tactics/GroupReflection/PP_mult_corr_G.con".
235 inline procedural "cic:/CoRN/tactics/GroupReflection/NormG_corr_G.con".
237 inline procedural "cic:/CoRN/tactics/GroupReflection/Tactic_lemmaG.con".
240 End Group_NormCorrect