equal
deleted
inserted
replaced
1091 lemma finite_eqvt [eqvt]: |
1091 lemma finite_eqvt [eqvt]: |
1092 shows "p \<bullet> finite A = finite (p \<bullet> A)" |
1092 shows "p \<bullet> finite A = finite (p \<bullet> A)" |
1093 unfolding finite_def |
1093 unfolding finite_def |
1094 by (perm_simp) (rule refl) |
1094 by (perm_simp) (rule refl) |
1095 |
1095 |
|
1096 lemma Let_eqvt [eqvt]: |
|
1097 "p \<bullet> Let x y = Let (p \<bullet> x) (p \<bullet> y)" |
|
1098 unfolding Let_def permute_fun_app_eq .. |
1096 |
1099 |
1097 subsubsection {* Equivariance for product operations *} |
1100 subsubsection {* Equivariance for product operations *} |
1098 |
1101 |
1099 lemma fst_eqvt [eqvt]: |
1102 lemma fst_eqvt [eqvt]: |
1100 shows "p \<bullet> (fst x) = fst (p \<bullet> x)" |
1103 shows "p \<bullet> (fst x) = fst (p \<bullet> x)" |