1 (* Title: nominal_permeq.ML |
1 (* Title: nominal_permeq.ML |
2 Author: Christian Urban |
2 Author: Christian Urban |
3 Author: Brian Huffman |
3 Author: Brian Huffman |
4 *) |
4 *) |
5 |
5 |
|
6 infix 4 addpres addposts addexcls |
|
7 |
6 signature NOMINAL_PERMEQ = |
8 signature NOMINAL_PERMEQ = |
7 sig |
9 sig |
8 val eqvt_rule: Proof.context -> thm list -> string list -> thm -> thm |
10 datatype eqvt_config = |
9 val eqvt_strict_rule: Proof.context -> thm list -> string list -> thm -> thm |
11 Eqvt_Config of {strict_mode: bool, pre_thms: thm list, post_thms: thm list, excluded: string list} |
10 |
12 |
11 val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic |
13 val eqvt_relaxed_config: eqvt_config |
12 val eqvt_strict_tac: Proof.context -> thm list -> string list -> int -> tactic |
14 val eqvt_strict_config: eqvt_config |
13 |
15 val addpres : (eqvt_config * thm list) -> eqvt_config |
|
16 val addposts : (eqvt_config * thm list) -> eqvt_config |
|
17 val addexcls : (eqvt_config * string list) -> eqvt_config |
|
18 val delpres : eqvt_config -> eqvt_config |
|
19 val delposts : eqvt_config -> eqvt_config |
|
20 |
|
21 val eqvt_rule: Proof.context -> eqvt_config -> thm -> thm |
|
22 val eqvt_tac: Proof.context -> eqvt_config -> int -> tactic |
|
23 |
14 val perm_simp_meth: thm list * string list -> Proof.context -> Method.method |
24 val perm_simp_meth: thm list * string list -> Proof.context -> Method.method |
15 val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method |
25 val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method |
16 val args_parser: (thm list * string list) context_parser |
26 val args_parser: (thm list * string list) context_parser |
17 |
27 |
18 val trace_eqvt: bool Config.T |
28 val trace_eqvt: bool Config.T |
19 val setup: theory -> theory |
29 val setup: theory -> theory |
20 end; |
30 end; |
21 |
31 |
22 (* |
32 (* |
23 |
33 |
24 - eqvt_tac and eqvt_strict_tac take a list of theorems |
34 - eqvt_tac and eqvt_rule take a list of theorems which |
25 which are first tried to simplify permutations |
35 are first tried to simplify permutations |
26 |
36 |
27 the string list contains constants that should not be |
37 - the string list contains constants that should not be |
28 analysed (for example there is no raw eqvt-lemma for |
38 analysed (for example there is no raw eqvt-lemma for |
29 the constant The); therefore it should not be analysed |
39 the constant The); therefore it should not be analysed |
30 |
40 |
31 - setting [[trace_eqvt = true]] switches on tracing |
41 - setting [[trace_eqvt = true]] switches on tracing |
32 information |
42 information |
35 |
45 |
36 structure Nominal_Permeq: NOMINAL_PERMEQ = |
46 structure Nominal_Permeq: NOMINAL_PERMEQ = |
37 struct |
47 struct |
38 |
48 |
39 open Nominal_ThmDecls; |
49 open Nominal_ThmDecls; |
|
50 |
|
51 datatype eqvt_config = Eqvt_Config of |
|
52 {strict_mode: bool, pre_thms: thm list, post_thms: thm list, excluded: string list} |
|
53 |
|
54 fun (Eqvt_Config {strict_mode, pre_thms, post_thms, excluded}) addpres thms = |
|
55 Eqvt_Config { strict_mode = strict_mode, |
|
56 pre_thms = thms @ pre_thms, |
|
57 post_thms = post_thms, |
|
58 excluded = excluded } |
|
59 |
|
60 fun (Eqvt_Config {strict_mode, pre_thms, post_thms, excluded}) addposts thms = |
|
61 Eqvt_Config { strict_mode = strict_mode, |
|
62 pre_thms = pre_thms, |
|
63 post_thms = thms @ post_thms, |
|
64 excluded = excluded } |
|
65 |
|
66 fun (Eqvt_Config {strict_mode, pre_thms, post_thms, excluded}) addexcls excls = |
|
67 Eqvt_Config { strict_mode = strict_mode, |
|
68 pre_thms = pre_thms, |
|
69 post_thms = post_thms, |
|
70 excluded = excls @ excluded } |
|
71 |
|
72 fun delpres (Eqvt_Config {strict_mode, pre_thms, post_thms, excluded}) = |
|
73 Eqvt_Config { strict_mode = strict_mode, |
|
74 pre_thms = [], |
|
75 post_thms = post_thms, |
|
76 excluded = excluded } |
|
77 |
|
78 fun delposts (Eqvt_Config {strict_mode, pre_thms, post_thms, excluded}) = |
|
79 Eqvt_Config { strict_mode = strict_mode, |
|
80 pre_thms = pre_thms, |
|
81 post_thms = [], |
|
82 excluded = excluded } |
|
83 |
|
84 val eqvt_relaxed_config = |
|
85 Eqvt_Config { strict_mode = false, |
|
86 pre_thms = @{thms eqvt_bound}, |
|
87 post_thms = @{thms permute_pure}, |
|
88 excluded = [] } |
|
89 |
|
90 val eqvt_strict_config = |
|
91 Eqvt_Config { strict_mode = true, |
|
92 pre_thms = @{thms eqvt_bound}, |
|
93 post_thms = @{thms permute_pure}, |
|
94 excluded = [] } |
|
95 |
40 |
96 |
41 (* tracing infrastructure *) |
97 (* tracing infrastructure *) |
42 val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false); |
98 val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false); |
43 |
99 |
44 fun trace_enabled ctxt = Config.get ctxt trace_eqvt |
100 fun trace_enabled ctxt = Config.get ctxt trace_eqvt |
117 in |
173 in |
118 Conv.all_conv ctrm |
174 Conv.all_conv ctrm |
119 end |
175 end |
120 |
176 |
121 (* main conversion *) |
177 (* main conversion *) |
122 fun main_eqvt_conv ctxt strict_flag user_thms excluded ctrm = |
178 fun main_eqvt_conv ctxt config ctrm = |
123 let |
179 let |
|
180 val Eqvt_Config {strict_mode, pre_thms, post_thms, excluded} = config |
|
181 |
124 val first_conv_wrapper = |
182 val first_conv_wrapper = |
125 if trace_enabled ctxt |
183 if trace_enabled ctxt |
126 then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt)) |
184 then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt)) |
127 else Conv.first_conv |
185 else Conv.first_conv |
128 |
186 |
129 val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt |
187 val all_pre_thms = map safe_mk_equiv (pre_thms @ get_eqvts_raw_thms ctxt) |
130 val post_thms = map safe_mk_equiv @{thms permute_pure} |
188 val all_post_thms = map safe_mk_equiv post_thms |
131 in |
189 in |
132 first_conv_wrapper |
190 first_conv_wrapper |
133 [ Conv.rewrs_conv pre_thms, |
191 [ Conv.rewrs_conv all_pre_thms, |
134 eqvt_apply_conv, |
192 eqvt_apply_conv, |
135 eqvt_lambda_conv, |
193 eqvt_lambda_conv, |
136 Conv.rewrs_conv post_thms, |
194 Conv.rewrs_conv all_post_thms, |
137 progress_info_conv ctxt strict_flag excluded |
195 progress_info_conv ctxt strict_mode excluded |
138 ] ctrm |
196 ] ctrm |
139 end |
197 end |
140 |
198 |
141 (* the eqvt-tactics first eta-normalise goals in |
199 |
|
200 (* the eqvt-conversion first eta-normalises goals in |
142 order to avoid problems with inductions in the |
201 order to avoid problems with inductions in the |
143 equivariance command. *) |
202 equivariance command. *) |
144 |
203 fun eqvt_conv ctxt config = |
145 (* raises an error if some permutations cannot be eliminated *) |
204 Conv.top_conv (fn ctxt => Thm.eta_conversion then_conv (main_eqvt_conv ctxt config)) ctxt |
146 fun eqvt_strict_conv ctxt user_thms excluded = |
205 |
147 Conv.top_conv |
206 (* thms rewriter *) |
148 (fn ctxt => Thm.eta_conversion then_conv (main_eqvt_conv ctxt true user_thms excluded)) ctxt |
207 fun eqvt_rule ctxt config = |
149 |
208 Conv.fconv_rule (eqvt_conv ctxt config) |
150 (* prints a warning message if some permutations cannot be eliminated *) |
209 |
151 fun eqvt_conv ctxt user_thms excluded = |
210 (* tactic *) |
152 Conv.top_conv |
211 fun eqvt_tac ctxt config = |
153 (fn ctxt => Thm.eta_conversion then_conv (main_eqvt_conv ctxt false user_thms excluded)) ctxt |
212 CONVERSION (eqvt_conv ctxt config) |
154 |
|
155 |
|
156 (* thms rewriters *) |
|
157 fun eqvt_strict_rule ctxt user_thms excluded = |
|
158 Conv.fconv_rule (eqvt_strict_conv ctxt user_thms excluded) |
|
159 |
|
160 fun eqvt_rule ctxt user_thms excluded = |
|
161 Conv.fconv_rule (eqvt_conv ctxt user_thms excluded) |
|
162 |
|
163 (* tactics *) |
|
164 fun eqvt_strict_tac ctxt user_thms excluded = |
|
165 CONVERSION (eqvt_strict_conv ctxt user_thms excluded) |
|
166 |
|
167 fun eqvt_tac ctxt user_thms excluded = |
|
168 CONVERSION (eqvt_conv ctxt user_thms excluded) |
|
169 |
213 |
170 (* setup of the configuration value *) |
214 (* setup of the configuration value *) |
171 val setup = |
215 val setup = |
172 trace_eqvt_setup |
216 trace_eqvt_setup |
173 |
217 |
181 val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- |
225 val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- |
182 (Scan.repeat (Args.const true))) [] |
226 (Scan.repeat (Args.const true))) [] |
183 |
227 |
184 val args_parser = add_thms_parser -- exclude_consts_parser |
228 val args_parser = add_thms_parser -- exclude_consts_parser |
185 |
229 |
186 fun perm_simp_meth (thms, consts) ctxt = |
230 fun perm_simp_meth (thms, consts) ctxt = |
187 SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts)) |
231 SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt (eqvt_relaxed_config addpres thms addexcls consts))) |
188 |
232 |
189 fun perm_strict_simp_meth (thms, consts) ctxt = |
233 fun perm_strict_simp_meth (thms, consts) ctxt = |
190 SIMPLE_METHOD (HEADGOAL (eqvt_strict_tac ctxt thms consts)) |
234 SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt (eqvt_strict_config addpres thms addexcls consts))) |
191 |
235 |
192 end; (* structure *) |
236 end; (* structure *) |