16 done |
16 done |
17 |
17 |
18 instantiation FSet.fset :: (pt) pt |
18 instantiation FSet.fset :: (pt) pt |
19 begin |
19 begin |
20 |
20 |
21 term "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
22 |
|
23 quotient_definition |
21 quotient_definition |
24 "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
22 "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
25 is |
23 is |
26 "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list" |
24 "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list" |
27 |
25 |
28 instance proof |
26 instance |
|
27 proof |
29 fix x :: "'a fset" and p q :: "perm" |
28 fix x :: "'a fset" and p q :: "perm" |
30 show "0 \<bullet> x = x" |
29 show "0 \<bullet> x = x" |
31 by (lifting permute_zero [where 'a="'a list"]) |
30 by (lifting permute_zero [where 'a="'a list"]) |
32 show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x" |
31 show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x" |
33 by (lifting permute_plus [where 'a="'a list"]) |
32 by (lifting permute_plus [where 'a="'a list"]) |
34 qed |
33 qed |
35 |
34 |
36 end |
35 end |
37 |
36 |
38 lemma permute_fset[eqvt]: |
37 lemma permute_fset[eqvt]: |
39 "p \<bullet> ({||} :: 'a :: pt fset) = {||}" |
38 "(p \<bullet> {||}) = ({||} :: 'a::pt fset)" |
40 "p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)" |
39 "p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)" |
41 by (lifting permute_list.simps) |
40 by (lifting permute_list.simps) |
42 |
41 |
43 lemma map_eqvt[eqvt]: "pi \<bullet> (map f l) = map (pi \<bullet> f) (pi \<bullet> l)" |
42 lemma fmap_eqvt[eqvt]: |
44 apply (induct l) |
43 shows "pi \<bullet> (fmap f l) = fmap (pi \<bullet> f) (pi \<bullet> l)" |
45 apply (simp_all) |
|
46 apply (simp only: eqvt_apply) |
|
47 done |
|
48 |
|
49 lemma fmap_eqvt[eqvt]: "pi \<bullet> (fmap f l) = fmap (pi \<bullet> f) (pi \<bullet> l)" |
|
50 by (lifting map_eqvt) |
44 by (lifting map_eqvt) |
51 |
45 |
52 lemma fset_to_set_eqvt[eqvt]: "pi \<bullet> (fset_to_set x) = fset_to_set (pi \<bullet> x)" |
46 lemma fset_to_set_eqvt[eqvt]: "pi \<bullet> (fset_to_set x) = fset_to_set (pi \<bullet> x)" |
53 by (lifting set_eqvt) |
47 by (lifting set_eqvt) |
54 |
48 |