equal
deleted
inserted
replaced
34 by (lifting permute_plus [where 'a="'a list"]) |
34 by (lifting permute_plus [where 'a="'a list"]) |
35 qed |
35 qed |
36 |
36 |
37 end |
37 end |
38 |
38 |
39 lemma permute_fset[simp]: |
39 lemma permute_fset[simp, eqvt]: |
40 fixes S::"('a::pt) fset" |
40 fixes S::"('a::pt) fset" |
41 shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)" |
41 shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)" |
42 and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)" |
42 and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)" |
43 by (lifting permute_list.simps) |
43 by (lifting permute_list.simps) |
44 |
|
45 declare permute_fset[eqvt] |
|
46 |
44 |
47 lemma fmap_eqvt[eqvt]: |
45 lemma fmap_eqvt[eqvt]: |
48 shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)" |
46 shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)" |
49 by (lifting map_eqvt) |
47 by (lifting map_eqvt) |
50 |
48 |
111 shows "fset_to_set S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset_to_set S" |
109 shows "fset_to_set S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset_to_set S" |
112 apply (induct S) |
110 apply (induct S) |
113 apply (simp add: fresh_set_empty) |
111 apply (simp add: fresh_set_empty) |
114 apply simp |
112 apply simp |
115 apply (unfold fresh_def) |
113 apply (unfold fresh_def) |
116 apply (simp add: supp_atom_insert) |
114 apply (simp add: supp_of_fin_insert) |
117 apply (rule conjI) |
115 apply (rule conjI) |
118 apply (unfold fresh_star_def) |
116 apply (unfold fresh_star_def) |
119 apply simp |
117 apply simp |
120 apply (unfold fresh_def) |
118 apply (unfold fresh_def) |
121 apply (simp add: supp_at_base supp_atom) |
119 apply (simp add: supp_at_base supp_atom) |