equal
deleted
inserted
replaced
951 lemma Inter_eqvt [eqvt]: |
951 lemma Inter_eqvt [eqvt]: |
952 shows "p \<bullet> (\<Inter> S) = \<Inter> (p \<bullet> S)" |
952 shows "p \<bullet> (\<Inter> S) = \<Inter> (p \<bullet> S)" |
953 unfolding Inter_eq |
953 unfolding Inter_eq |
954 by (perm_simp) (rule refl) |
954 by (perm_simp) (rule refl) |
955 |
955 |
956 |
|
957 (* FIXME: eqvt attribute *) |
956 (* FIXME: eqvt attribute *) |
958 lemma Sigma_eqvt: |
957 lemma Sigma_eqvt: |
959 shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)" |
958 shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)" |
960 unfolding Sigma_def |
959 unfolding Sigma_def |
961 unfolding UNION_eq_Union_image |
960 unfolding SUP_def |
962 by (perm_simp) (rule refl) |
961 by (perm_simp) (rule refl) |
963 |
962 |
964 text {* |
963 text {* |
965 In order to prove that lfp is equivariant we need two |
964 In order to prove that lfp is equivariant we need two |
966 auxiliary classes which specify that (op <=) and |
965 auxiliary classes which specify that (op <=) and |