equal
deleted
inserted
replaced
1 theory Nominal2_FSet |
1 theory Nominal2_FSet |
2 imports "../Nominal-General/Nominal2_Supp" |
2 imports "../Nominal-General/Nominal2_Supp" |
|
3 "../Nominal-General/Nominal2_Atoms" |
|
4 "../Nominal-General/Nominal2_Eqvt" |
3 FSet |
5 FSet |
4 begin |
6 begin |
|
7 |
|
8 lemma "p \<bullet> {} = {}" |
|
9 apply(perm_simp) |
|
10 by simp |
5 |
11 |
6 lemma permute_rsp_fset[quot_respect]: |
12 lemma permute_rsp_fset[quot_respect]: |
7 "(op = ===> list_eq ===> list_eq) permute permute" |
13 "(op = ===> list_eq ===> list_eq) permute permute" |
8 apply (simp add: eqvts[symmetric]) |
14 apply (simp add: eqvts[symmetric]) |
9 apply clarify |
15 apply clarify |
32 by (lifting permute_plus [where 'a="'a list"]) |
38 by (lifting permute_plus [where 'a="'a list"]) |
33 qed |
39 qed |
34 |
40 |
35 end |
41 end |
36 |
42 |
37 lemma permute_fset[simp, eqvt]: |
43 lemma "p \<bullet> {} = {}" |
|
44 apply(perm_simp) |
|
45 by simp |
|
46 |
|
47 lemma permute_fset[simp]: |
38 fixes S::"('a::pt) fset" |
48 fixes S::"('a::pt) fset" |
39 shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)" |
49 shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)" |
40 and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)" |
50 and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)" |
41 by (lifting permute_list.simps) |
51 by (lifting permute_list.simps) |
|
52 |
|
53 lemma "p \<bullet> {} = {}" |
|
54 apply(perm_simp) |
|
55 by simp |
|
56 |
|
57 ML {* @{term "{}"} ; @{term "{||}"} *} |
|
58 |
|
59 declare permute_fset[eqvt] |
|
60 |
|
61 lemma "p \<bullet> {} = {}" |
|
62 apply(perm_simp) |
|
63 by simp |
|
64 |
42 |
65 |
43 lemma fmap_eqvt[eqvt]: |
66 lemma fmap_eqvt[eqvt]: |
44 shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)" |
67 shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)" |
45 by (lifting map_eqvt) |
68 by (lifting map_eqvt) |
46 |
69 |
117 apply (simp add: supp_at_base supp_atom) |
140 apply (simp add: supp_at_base supp_atom) |
118 apply clarify |
141 apply clarify |
119 apply auto |
142 apply auto |
120 done |
143 done |
121 |
144 |
|
145 lemma "p \<bullet> {} = {}" |
|
146 apply(perm_simp) |
|
147 by simp |
|
148 |
122 end |
149 end |