equal
deleted
inserted
replaced
926 |
926 |
927 lemma Inter_eqvt [eqvt]: |
927 lemma Inter_eqvt [eqvt]: |
928 shows "p \<bullet> (\<Inter> S) = \<Inter> (p \<bullet> S)" |
928 shows "p \<bullet> (\<Inter> S) = \<Inter> (p \<bullet> S)" |
929 unfolding Inter_eq |
929 unfolding Inter_eq |
930 by (perm_simp) (rule refl) |
930 by (perm_simp) (rule refl) |
|
931 |
|
932 lemma foldr_eqvt[eqvt]: |
|
933 "p \<bullet> foldr a b c = foldr (p \<bullet> a) (p \<bullet> b) (p \<bullet> c)" |
|
934 apply (induct b) |
|
935 apply simp_all |
|
936 apply (perm_simp) |
|
937 apply simp |
|
938 done |
931 |
939 |
932 (* FIXME: eqvt attribute *) |
940 (* FIXME: eqvt attribute *) |
933 lemma Sigma_eqvt: |
941 lemma Sigma_eqvt: |
934 shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)" |
942 shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)" |
935 unfolding Sigma_def |
943 unfolding Sigma_def |