equal
deleted
inserted
replaced
34 |
34 |
35 (* datatypes *) |
35 (* datatypes *) |
36 Pair_eqvt permute_list.simps permute_option.simps |
36 Pair_eqvt permute_list.simps permute_option.simps |
37 |
37 |
38 (* sets *) |
38 (* sets *) |
39 mem_eqvt empty_eqvt insert_eqvt set_eqvt |
39 mem_eqvt empty_eqvt insert_eqvt set_eqvt inter_eqvt |
40 |
40 |
41 (* fsets *) |
41 (* fsets *) |
42 permute_fset fset_eqvt |
42 permute_fset fset_eqvt |
43 |
43 |
44 |
44 |
171 lemma union_eqvt[eqvt]: |
171 lemma union_eqvt[eqvt]: |
172 shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)" |
172 shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)" |
173 unfolding Un_def |
173 unfolding Un_def |
174 by (perm_simp) (rule refl) |
174 by (perm_simp) (rule refl) |
175 |
175 |
176 lemma inter_eqvt[eqvt]: |
|
177 shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)" |
|
178 unfolding Int_def |
|
179 by (perm_simp) (rule refl) |
|
180 |
|
181 lemma Diff_eqvt[eqvt]: |
176 lemma Diff_eqvt[eqvt]: |
182 fixes A B :: "'a::pt set" |
177 fixes A B :: "'a::pt set" |
183 shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B" |
178 shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B" |
184 unfolding set_diff_eq |
179 unfolding set_diff_eq |
185 by (perm_simp) (rule refl) |
180 by (perm_simp) (rule refl) |