equal
deleted
inserted
replaced
42 apply (rule permute_fset_plus) |
42 apply (rule permute_fset_plus) |
43 done |
43 done |
44 |
44 |
45 end |
45 end |
46 |
46 |
47 lemma permute_fset[simp,eqvt]: |
47 lemma permute_fset[eqvt]: |
48 "p \<bullet> ({||} :: 'a :: pt fset) = {||}" |
48 "p \<bullet> ({||} :: 'a :: pt fset) = {||}" |
49 "p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)" |
49 "p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)" |
50 by (lifting permute_list.simps) |
50 by (lifting permute_list.simps) |
51 |
51 |
52 lemma map_eqvt[eqvt]: "pi \<bullet> (map f l) = map (pi \<bullet> f) (pi \<bullet> l)" |
52 lemma map_eqvt[eqvt]: "pi \<bullet> (map f l) = map (pi \<bullet> f) (pi \<bullet> l)" |