equal
deleted
inserted
replaced
627 |
627 |
628 quotient_definition |
628 quotient_definition |
629 "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
629 "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
630 is |
630 is |
631 "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list" |
631 "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
632 by (simp add: set_eqvt[symmetric]) |
632 |
633 |
633 instance |
634 instance |
634 proof |
635 proof |
635 fix x :: "'a fset" and p q :: "perm" |
636 fix x :: "'a fset" and p q :: "perm" |
636 show "0 \<bullet> x = x" by (descending) (simp) |
637 show "0 \<bullet> x = x" by (descending) (simp) |