equal
deleted
inserted
replaced
65 |
65 |
66 lemma fmap_eqvt[eqvt]: |
66 lemma fmap_eqvt[eqvt]: |
67 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)" |
68 by (lifting map_eqvt) |
68 by (lifting map_eqvt) |
69 |
69 |
70 lemma fset_to_set_eqvt[eqvt]: |
70 lemma fset_to_set_eqvt [eqvt]: |
71 shows "p \<bullet> (fset_to_set S) = fset_to_set (p \<bullet> S)" |
71 shows "p \<bullet> (fset_to_set S) = fset_to_set (p \<bullet> S)" |
72 by (lifting set_eqvt) |
72 by (lifting set_eqvt) |
73 |
73 |
74 lemma fin_fset_to_set[simp]: |
74 lemma fin_fset_to_set[simp]: |
75 shows "finite (fset_to_set S)" |
75 shows "finite (fset_to_set S)" |
76 by (induct S) (simp_all) |
76 by (induct S) (simp_all) |
77 |
77 |
78 lemma supp_fset_to_set: |
78 lemma supp_fset_to_set: |
79 shows "supp (fset_to_set S) = supp S" |
79 shows "supp (fset_to_set S) = supp S" |
80 apply (simp add: supp_def) |
80 unfolding supp_def |
81 apply (simp add: eqvts) |
81 by (perm_simp) (simp add: fset_cong) |
82 apply (simp add: fset_cong) |
|
83 done |
|
84 |
82 |
85 lemma supp_finsert: |
83 lemma supp_finsert: |
86 fixes x::"'a::fs" |
84 fixes x::"'a::fs" |
87 shows "supp (finsert x S) = supp x \<union> supp S" |
85 shows "supp (finsert x S) = supp x \<union> supp S" |
88 apply(subst supp_fset_to_set[symmetric]) |
86 apply(subst supp_fset_to_set[symmetric]) |