equal
deleted
inserted
replaced
22 |
22 |
23 |
23 |
24 section {* eqvt lemmas *} |
24 section {* eqvt lemmas *} |
25 |
25 |
26 lemmas [eqvt] = |
26 lemmas [eqvt] = |
27 conj_eqvt Not_eqvt ex_eqvt all_eqvt imp_eqvt |
27 conj_eqvt Not_eqvt ex_eqvt all_eqvt imp_eqvt uminus_eqvt |
28 imp_eqvt[folded induct_implies_def] |
28 imp_eqvt[folded induct_implies_def] |
29 uminus_eqvt |
29 all_eqvt[folded induct_forall_def] |
30 |
30 |
31 (* nominal *) |
31 (* nominal *) |
32 supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt |
32 supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt |
33 swap_eqvt flip_eqvt |
33 swap_eqvt flip_eqvt |
34 |
34 |
38 (* sets *) |
38 (* sets *) |
39 mem_eqvt empty_eqvt insert_eqvt set_eqvt |
39 mem_eqvt empty_eqvt insert_eqvt set_eqvt |
40 |
40 |
41 (* fsets *) |
41 (* fsets *) |
42 permute_fset fset_eqvt |
42 permute_fset fset_eqvt |
|
43 |
43 |
44 |
44 text {* helper lemmas for the perm_simp *} |
45 text {* helper lemmas for the perm_simp *} |
45 |
46 |
46 definition |
47 definition |
47 "unpermute p = permute (- p)" |
48 "unpermute p = permute (- p)" |