22 "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list" |
22 "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list" |
23 |
23 |
24 instance |
24 instance |
25 proof |
25 proof |
26 fix x :: "'a fset" and p q :: "perm" |
26 fix x :: "'a fset" and p q :: "perm" |
27 show "0 \<bullet> x = x" |
27 show "0 \<bullet> x = x" by (descending) (simp) |
28 by (lifting permute_zero [where 'a="'a list"]) |
28 show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x" by (descending) (simp) |
29 show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x" |
|
30 by (lifting permute_plus [where 'a="'a list"]) |
|
31 qed |
29 qed |
32 |
30 |
33 end |
31 end |
34 |
32 |
35 lemma permute_fset[simp, eqvt]: |
33 lemma permute_fset[simp, eqvt]: |
40 |
38 |
41 lemma fmap_eqvt[eqvt]: |
39 lemma fmap_eqvt[eqvt]: |
42 shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)" |
40 shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)" |
43 by (lifting map_eqvt) |
41 by (lifting map_eqvt) |
44 |
42 |
45 lemma fset_to_set_eqvt [eqvt]: |
43 lemma fset_eqvt[eqvt]: |
46 shows "p \<bullet> (fset_to_set S) = fset_to_set (p \<bullet> S)" |
44 shows "p \<bullet> (fset S) = fset (p \<bullet> S)" |
47 by (lifting set_eqvt) |
45 by (lifting set_eqvt) |
48 |
46 |
49 lemma fin_fset_to_set[simp]: |
47 lemma supp_fset: |
50 shows "finite (fset_to_set S)" |
48 shows "supp (fset S) = supp S" |
51 by (induct S) (simp_all) |
|
52 |
|
53 lemma supp_fset_to_set: |
|
54 shows "supp (fset_to_set S) = supp S" |
|
55 unfolding supp_def |
49 unfolding supp_def |
56 by (perm_simp) (simp add: fset_cong) |
50 by (perm_simp) (simp add: fset_cong) |
57 |
51 |
58 lemma supp_fempty: |
52 lemma supp_fempty: |
59 shows "supp {||} = {}" |
53 shows "supp {||} = {}" |
60 unfolding supp_def |
54 unfolding supp_def |
61 by simp |
55 by simp |
62 |
56 |
63 lemma supp_finsert: |
57 lemma supp_finsert: |
64 fixes x::"'a::fs" |
58 fixes x::"'a::fs" |
|
59 and S::"'a fset" |
65 shows "supp (finsert x S) = supp x \<union> supp S" |
60 shows "supp (finsert x S) = supp x \<union> supp S" |
66 apply(subst supp_fset_to_set[symmetric]) |
61 apply(subst supp_fset[symmetric]) |
67 apply(simp add: supp_fset_to_set) |
62 apply(simp add: supp_fset) |
68 apply(simp add: supp_of_fin_insert) |
63 apply(simp add: supp_of_fin_insert) |
69 apply(simp add: supp_fset_to_set) |
64 apply(simp add: supp_fset) |
70 done |
65 done |
71 |
66 |
72 |
67 |
73 instance fset :: (fs) fs |
68 instance fset :: (fs) fs |
74 apply (default) |
69 apply (default) |
91 apply(simp add: atom_fmap_cong) |
86 apply(simp add: atom_fmap_cong) |
92 done |
87 done |
93 |
88 |
94 lemma supp_at_fset: |
89 lemma supp_at_fset: |
95 fixes S::"('a::at_base) fset" |
90 fixes S::"('a::at_base) fset" |
96 shows "supp S = fset_to_set (fmap atom S)" |
91 shows "supp S = fset (fmap atom S)" |
97 apply (induct S) |
92 apply (induct S) |
98 apply (simp add: supp_fempty) |
93 apply (simp add: supp_fempty) |
99 apply (simp add: supp_finsert) |
94 apply (simp add: supp_finsert) |
100 apply (simp add: supp_at_base) |
95 apply (simp add: supp_at_base) |
101 done |
96 done |
102 |
97 |
103 lemma fresh_star_atom: |
98 lemma fresh_star_atom: |
104 fixes a::"'a::at_base" |
99 fixes a::"'a::at_base" |
105 shows "fset_to_set S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset_to_set S" |
100 shows "fset S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset S" |
106 apply (induct S) |
101 apply (induct S) |
107 apply (simp add: fresh_set_empty) |
102 apply (simp add: fresh_set_empty) |
108 apply simp |
103 apply simp |
109 apply (unfold fresh_def) |
104 apply (unfold fresh_def) |
110 apply (simp add: supp_of_fin_insert) |
105 apply (simp add: supp_of_fin_insert) |