equal
deleted
inserted
replaced
4 |
4 |
5 Equivariance, supp and freshness lemmas for various operators |
5 Equivariance, supp and freshness lemmas for various operators |
6 (contains many, but not all such lemmas). |
6 (contains many, but not all such lemmas). |
7 *) |
7 *) |
8 theory Nominal2_Eqvt |
8 theory Nominal2_Eqvt |
9 imports Nominal2_Base Nominal2_Atoms |
9 imports Nominal2_Base |
10 uses ("nominal_thmdecls.ML") |
10 uses ("nominal_thmdecls.ML") |
11 ("nominal_permeq.ML") |
11 ("nominal_permeq.ML") |
12 ("nominal_eqvt.ML") |
12 ("nominal_eqvt.ML") |
13 begin |
13 begin |
14 |
14 |
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 atom_eqvt 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 |
286 |
285 |
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 {* |
|
292 val test1 = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) []; |
|
293 val test2 = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- |
|
294 (Scan.repeat (Args.const true))) [] |
|
295 *} |
|
296 |
|
297 method_setup perm_simp = |
290 method_setup perm_simp = |
298 {* test1 -- test2 >> |
291 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *} |
299 (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt [] consts))) *} |
292 {* pushes permutations inside. *} |
300 {* pushes permutations inside *} |
|
301 |
293 |
302 method_setup perm_strict_simp = |
294 method_setup perm_strict_simp = |
303 {* test1 -- test2 >> |
295 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *} |
304 (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL |
296 {* pushes permutations inside, raises an error if it cannot solve all permutations. *} |
305 (Nominal_Permeq.eqvt_strict_tac ctxt thms consts))) *} |
|
306 {* pushes permutations inside, raises an error if it cannot solve all permutations *} |
|
307 |
297 |
308 declare [[trace_eqvt = true]] |
298 declare [[trace_eqvt = true]] |
309 |
299 |
310 lemma |
300 lemma |
311 fixes B::"'a::pt" |
301 fixes B::"'a::pt" |