27 lemma permute_list_zero: "0 \<bullet> (x :: 'a list) = x"

    27 instance proof

    28   by (rule permute_zero)

    28   fix x :: "'a fset" and p q :: "perm"

    29 

    29   show "0 \<bullet> x = x"

    30 lemma permute_fset_zero: "0 \<bullet> (x :: 'a fset) = x"

    30     by (lifting permute_zero [where 'a="'a list"])

    31   by (lifting permute_list_zero)

    31   show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x"

    32 

    32     by (lifting permute_plus [where 'a="'a list"])

    33 lemma permute_list_plus: "(p + q) \<bullet> (x :: 'a list) = p \<bullet> q \<bullet> x"

    33 qed

    34   by (rule permute_plus)

    35 

    36 lemma permute_fset_plus: "(p + q) \<bullet> (x :: 'a fset) = p \<bullet> q \<bullet> x"

    37   by (lifting permute_list_plus)

    38 

    39 instance

    40   apply default

    41   apply (rule permute_fset_zero)

    42   apply (rule permute_fset_plus)

    43   done