26 end |
26 end |
27 |
27 |
28 lemma permute_fset[simp, eqvt]: |
28 lemma permute_fset[simp, eqvt]: |
29 fixes S::"('a::pt) fset" |
29 fixes S::"('a::pt) fset" |
30 shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)" |
30 shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)" |
31 and "(p \<bullet> finsert x S) = finsert (p \<bullet> x) (p \<bullet> S)" |
31 and "(p \<bullet> insert_fset x S) = insert_fset (p \<bullet> x) (p \<bullet> S)" |
32 by (lifting permute_list.simps) |
32 by (lifting permute_list.simps) |
33 |
33 |
34 lemma fmap_eqvt[eqvt]: |
34 lemma map_fset_eqvt[eqvt]: |
35 shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)" |
35 shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)" |
36 by (lifting map_eqvt) |
36 by (lifting map_eqvt) |
37 |
37 |
38 lemma fset_eqvt[eqvt]: |
38 lemma fset_eqvt[eqvt]: |
39 shows "p \<bullet> (fset S) = fset (p \<bullet> S)" |
39 shows "p \<bullet> (fset S) = fset (p \<bullet> S)" |
40 by (lifting set_eqvt) |
40 by (lifting set_eqvt) |
42 lemma supp_fset [simp]: |
42 lemma supp_fset [simp]: |
43 shows "supp (fset S) = supp S" |
43 shows "supp (fset S) = supp S" |
44 unfolding supp_def |
44 unfolding supp_def |
45 by (perm_simp) (simp add: fset_cong) |
45 by (perm_simp) (simp add: fset_cong) |
46 |
46 |
47 lemma supp_fempty [simp]: |
47 lemma supp_empty_fset [simp]: |
48 shows "supp {||} = {}" |
48 shows "supp {||} = {}" |
49 unfolding supp_def |
49 unfolding supp_def |
50 by simp |
50 by simp |
51 |
51 |
52 lemma supp_finsert [simp]: |
52 lemma supp_insert_fset [simp]: |
53 fixes x::"'a::fs" |
53 fixes x::"'a::fs" |
54 and S::"'a fset" |
54 and S::"'a fset" |
55 shows "supp (finsert x S) = supp x \<union> supp S" |
55 shows "supp (insert_fset x S) = supp x \<union> supp S" |
56 apply(subst supp_fset[symmetric]) |
56 apply(subst supp_fset[symmetric]) |
57 apply(simp add: supp_fset supp_of_fin_insert) |
57 apply(simp add: supp_fset supp_of_fin_insert) |
58 done |
58 done |
59 |
59 |
60 lemma fset_finite_supp: |
60 lemma fset_finite_supp: |
68 instance fset :: (fs) fs |
68 instance fset :: (fs) fs |
69 apply (default) |
69 apply (default) |
70 apply (rule fset_finite_supp) |
70 apply (rule fset_finite_supp) |
71 done |
71 done |
72 |
72 |
73 lemma atom_fmap_cong: |
73 lemma atom_map_fset_cong: |
74 shows "fmap atom x = fmap atom y \<longleftrightarrow> x = y" |
74 shows "map_fset atom x = map_fset atom y \<longleftrightarrow> x = y" |
75 apply(rule inj_fmap_eq_iff) |
75 apply(rule inj_map_fset_eq_iff) |
76 apply(simp add: inj_on_def) |
76 apply(simp add: inj_on_def) |
77 done |
77 done |
78 |
78 |
79 lemma supp_fmap_atom: |
79 lemma supp_map_fset_atom: |
80 shows "supp (fmap atom S) = supp S" |
80 shows "supp (map_fset atom S) = supp S" |
81 unfolding supp_def |
81 unfolding supp_def |
82 apply(perm_simp) |
82 apply(perm_simp) |
83 apply(simp add: atom_fmap_cong) |
83 apply(simp add: atom_map_fset_cong) |
84 done |
84 done |
85 |
85 |
86 lemma supp_at_fset: |
86 lemma supp_at_fset: |
87 fixes S::"('a::at_base) fset" |
87 fixes S::"('a::at_base) fset" |
88 shows "supp S = fset (fmap atom S)" |
88 shows "supp S = fset (map_fset atom S)" |
89 apply (induct S) |
89 apply (induct S) |
90 apply (simp add: supp_fempty) |
90 apply (simp add: supp_empty_fset) |
91 apply (simp add: supp_finsert) |
91 apply (simp add: supp_insert_fset) |
92 apply (simp add: supp_at_base) |
92 apply (simp add: supp_at_base) |
93 done |
93 done |
94 |
94 |
95 lemma fresh_star_atom: |
95 lemma fresh_star_atom: |
96 fixes a::"'a::at_base" |
96 fixes a::"'a::at_base" |