equal
deleted
inserted
replaced
999 |
999 |
1000 lemma Inter_eqvt [eqvt]: |
1000 lemma Inter_eqvt [eqvt]: |
1001 shows "p \<bullet> (\<Inter> S) = \<Inter> (p \<bullet> S)" |
1001 shows "p \<bullet> (\<Inter> S) = \<Inter> (p \<bullet> S)" |
1002 unfolding Inter_eq |
1002 unfolding Inter_eq |
1003 by (perm_simp) (rule refl) |
1003 by (perm_simp) (rule refl) |
|
1004 |
|
1005 lemma foldr_eqvt[eqvt]: |
|
1006 "p \<bullet> foldr a b c = foldr (p \<bullet> a) (p \<bullet> b) (p \<bullet> c)" |
|
1007 apply (induct b) |
|
1008 apply simp_all |
|
1009 apply (perm_simp) |
|
1010 apply simp |
|
1011 done |
1004 |
1012 |
1005 (* FIXME: eqvt attribute *) |
1013 (* FIXME: eqvt attribute *) |
1006 lemma Sigma_eqvt: |
1014 lemma Sigma_eqvt: |
1007 shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)" |
1015 shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)" |
1008 unfolding Sigma_def |
1016 unfolding Sigma_def |