equal
deleted
inserted
replaced
1223 shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)" |
1223 shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)" |
1224 by (lifting map_eqvt) |
1224 by (lifting map_eqvt) |
1225 |
1225 |
1226 subsubsection {* Equivariance for @{typ "('a, 'b) finfun"} *} |
1226 subsubsection {* Equivariance for @{typ "('a, 'b) finfun"} *} |
1227 |
1227 |
1228 lemma permute_finfun_update[eqvt]: |
1228 lemma finfun_update_eqvt [eqvt]: |
1229 shows "(p \<bullet> (finfun_update f a b)) = finfun_update (p \<bullet> f) (p \<bullet> a) (p \<bullet> b)" |
1229 shows "(p \<bullet> (finfun_update f a b)) = finfun_update (p \<bullet> f) (p \<bullet> a) (p \<bullet> b)" |
1230 by (transfer) (simp) |
1230 by (transfer) (simp) |
1231 |
1231 |
1232 lemma permute_finfun_const[eqvt]: |
1232 lemma finfun_const_eqvt [eqvt]: |
1233 shows "(p \<bullet> (finfun_const b)) = (finfun_const (p \<bullet> b))" |
1233 shows "(p \<bullet> (finfun_const b)) = finfun_const (p \<bullet> b)" |
|
1234 by (transfer) (simp) |
|
1235 |
|
1236 lemma finfun_apply_eqvt [eqvt]: |
|
1237 shows "(p \<bullet> (finfun_apply f b)) = finfun_apply (p \<bullet> f) (p \<bullet> b)" |
1234 by (transfer) (simp) |
1238 by (transfer) (simp) |
1235 |
1239 |
1236 |
1240 |
1237 section {* Supp, Freshness and Supports *} |
1241 section {* Supp, Freshness and Supports *} |
1238 |
1242 |
2237 by (simp add: fresh_def supp_def) |
2241 by (simp add: fresh_def supp_def) |
2238 |
2242 |
2239 lemma fresh_finfun_update: |
2243 lemma fresh_finfun_update: |
2240 shows "\<lbrakk>a \<sharp> f; a \<sharp> x; a \<sharp> y\<rbrakk> \<Longrightarrow> a \<sharp> finfun_update f x y" |
2244 shows "\<lbrakk>a \<sharp> f; a \<sharp> x; a \<sharp> y\<rbrakk> \<Longrightarrow> a \<sharp> finfun_update f x y" |
2241 unfolding fresh_conv_MOST |
2245 unfolding fresh_conv_MOST |
2242 unfolding permute_finfun_update |
2246 unfolding finfun_update_eqvt |
2243 by (elim MOST_rev_mp) (simp) |
2247 by (elim MOST_rev_mp) (simp) |
2244 |
2248 |
2245 lemma supp_finfun_const: |
2249 lemma supp_finfun_const: |
2246 shows "supp (finfun_const b) = supp(b)" |
2250 shows "supp (finfun_const b) = supp(b)" |
2247 by (simp add: supp_def) |
2251 by (simp add: supp_def) |