247 eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt |
247 eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt |
248 True_eqvt False_eqvt ex_eqvt all_eqvt ex1_eqvt |
248 True_eqvt False_eqvt ex_eqvt all_eqvt ex1_eqvt |
249 imp_eqvt [folded induct_implies_def] |
249 imp_eqvt [folded induct_implies_def] |
250 |
250 |
251 (* nominal *) |
251 (* nominal *) |
252 supp_eqvt fresh_eqvt |
252 supp_eqvt fresh_eqvt add_perm_eqvt |
253 |
253 |
254 (* datatypes *) |
254 (* datatypes *) |
255 permute_prod.simps append_eqvt rev_eqvt set_eqvt |
255 permute_prod.simps append_eqvt rev_eqvt set_eqvt |
256 map_eqvt fst_eqvt snd_eqvt Pair_eqvt permute_list.simps |
256 map_eqvt fst_eqvt snd_eqvt Pair_eqvt permute_list.simps |
257 |
257 |
258 (* sets *) |
258 (* sets *) |
259 empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt |
259 empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt |
260 Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt |
260 Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt |
261 |
261 |
262 add_perm_eqvt |
262 |
263 |
|
264 lemmas [eqvt_raw] = |
263 lemmas [eqvt_raw] = |
265 permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *) |
264 permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *) |
266 |
265 |
267 text {* helper lemmas for the eqvt_tac *} |
266 text {* helper lemmas for the eqvt_tac *} |
268 |
267 |
287 (* provides perm_simp methods *) |
286 (* provides perm_simp methods *) |
288 use "nominal_permeq.ML" |
287 use "nominal_permeq.ML" |
289 setup Nominal_Permeq.setup |
288 setup Nominal_Permeq.setup |
290 |
289 |
291 ML {* |
290 ML {* |
292 val test1 = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) []; |
291 val add_thms = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) []; |
293 val test2 = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- |
292 val exclude_consts = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- |
294 (Scan.repeat (Args.const true))) [] |
293 (Scan.repeat (Args.const true))) [] |
|
294 |
|
295 val parser = |
|
296 add_thms -- exclude_consts || |
|
297 exclude_consts -- add_thms >> swap |
295 *} |
298 *} |
296 |
299 |
297 method_setup perm_simp = |
300 method_setup perm_simp = |
298 {* test1 -- test2 >> |
301 {* parser >> |
299 (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt [] consts))) *} |
302 (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL |
|
303 (Nominal_Permeq.eqvt_tac ctxt [] consts))) *} |
300 {* pushes permutations inside *} |
304 {* pushes permutations inside *} |
301 |
305 |
302 method_setup perm_strict_simp = |
306 method_setup perm_strict_simp = |
303 {* test1 -- test2 >> |
307 {* parser >> |
304 (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL |
308 (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL |
305 (Nominal_Permeq.eqvt_strict_tac ctxt thms consts))) *} |
309 (Nominal_Permeq.eqvt_strict_tac ctxt thms consts))) *} |
306 {* pushes permutations inside, raises an error if it cannot solve all permutations *} |
310 {* pushes permutations inside, raises an error if it cannot solve all permutations *} |
307 |
311 |
308 declare [[trace_eqvt = true]] |
312 declare [[trace_eqvt = true]] |
309 |
313 |
310 lemma |
314 lemma |