equal
deleted
inserted
replaced
1044 apply(simp_all) |
1044 apply(simp_all) |
1045 apply(perm_simp exclude: foldr) |
1045 apply(perm_simp exclude: foldr) |
1046 apply(simp) |
1046 apply(simp) |
1047 done |
1047 done |
1048 |
1048 |
1049 thm eqvts_raw |
|
1050 |
|
1051 |
|
1052 (* FIXME: eqvt attribute *) |
1049 (* FIXME: eqvt attribute *) |
1053 lemma Sigma_eqvt: |
1050 lemma Sigma_eqvt: |
1054 shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)" |
1051 shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)" |
1055 unfolding Sigma_def |
1052 unfolding Sigma_def |
1056 unfolding SUP_def |
1053 unfolding SUP_def |
1129 by simp |
1126 by simp |
1130 |
1127 |
1131 lemma fun_upd_eqvt[eqvt]: |
1128 lemma fun_upd_eqvt[eqvt]: |
1132 shows "p \<bullet> (f(x := y)) = (p \<bullet> f)((p \<bullet> x) := (p \<bullet> y))" |
1129 shows "p \<bullet> (f(x := y)) = (p \<bullet> f)((p \<bullet> x) := (p \<bullet> y))" |
1133 unfolding fun_upd_def |
1130 unfolding fun_upd_def |
1134 by (simp) |
1131 by simp |
1135 |
1132 |
|
1133 lemma comp_eqvt [eqvt]: |
|
1134 shows "p \<bullet> (f \<circ> g) = (p \<bullet> f) \<circ> (p \<bullet> g)" |
|
1135 unfolding comp_def |
|
1136 by simp |
1136 |
1137 |
1137 subsubsection {* Equivariance for product operations *} |
1138 subsubsection {* Equivariance for product operations *} |
1138 |
1139 |
1139 lemma fst_eqvt [eqvt]: |
1140 lemma fst_eqvt [eqvt]: |
1140 shows "p \<bullet> (fst x) = fst (p \<bullet> x)" |
1141 shows "p \<bullet> (fst x) = fst (p \<bullet> x)" |