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 |
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 add_perm_eqvt |
263 |
263 |
264 lemmas [eqvt_raw] = |
264 lemmas [eqvt_raw] = |
265 permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *) |
265 permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *) |
266 |
266 |
267 text {* helper lemmas for the eqvt_tac *} |
267 text {* helper lemmas for the eqvt_tac *} |