32 by (lifting permute_plus [where 'a="'a list"]) |
32 by (lifting permute_plus [where 'a="'a list"]) |
33 qed |
33 qed |
34 |
34 |
35 end |
35 end |
36 |
36 |
37 lemma permute_fset[eqvt]: |
37 lemma permute_fset[simp, eqvt]: |
38 "(p \<bullet> {||}) = ({||} :: 'a::pt fset)" |
38 fixes S::"('a::pt) fset" |
39 "p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)" |
39 shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)" |
|
40 and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)" |
40 by (lifting permute_list.simps) |
41 by (lifting permute_list.simps) |
41 |
42 |
42 lemma fmap_eqvt[eqvt]: |
43 lemma fmap_eqvt[eqvt]: |
43 shows "p \<bullet> (fmap f l) = fmap (p \<bullet> f) (p \<bullet> l)" |
44 shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)" |
44 by (lifting map_eqvt) |
45 by (lifting map_eqvt) |
45 |
46 |
46 lemma fset_to_set_eqvt[eqvt]: |
47 lemma fset_to_set_eqvt[eqvt]: |
47 shows "p \<bullet> (fset_to_set x) = fset_to_set (p \<bullet> x)" |
48 shows "p \<bullet> (fset_to_set S) = fset_to_set (p \<bullet> S)" |
48 by (lifting set_eqvt) |
49 by (lifting set_eqvt) |
49 |
50 |
50 lemma fin_fset_to_set: |
51 lemma fin_fset_to_set[simp]: |
51 shows "finite (fset_to_set x)" |
52 shows "finite (fset_to_set S)" |
52 by (induct x) (simp_all) |
53 by (induct S) (simp_all) |
53 |
54 |
54 lemma supp_fset_to_set: |
55 lemma supp_fset_to_set: |
55 "supp (fset_to_set x) = supp x" |
56 shows "supp (fset_to_set S) = supp S" |
56 apply (simp add: supp_def) |
57 apply (simp add: supp_def) |
57 apply (simp add: eqvts) |
58 apply (simp add: eqvts) |
58 apply (simp add: fset_cong) |
59 apply (simp add: fset_cong) |
59 done |
60 done |
60 |
61 |
|
62 lemma supp_finsert: |
|
63 fixes x::"'a::fs" |
|
64 shows "supp (finsert x S) = supp x \<union> supp S" |
|
65 apply(subst supp_fset_to_set[symmetric]) |
|
66 apply(simp add: supp_fset_to_set) |
|
67 apply(simp add: supp_of_fin_insert) |
|
68 apply(simp add: supp_fset_to_set) |
|
69 done |
|
70 |
|
71 lemma supp_fempty: |
|
72 shows "supp {||} = {}" |
|
73 unfolding supp_def |
|
74 by simp |
|
75 |
|
76 instance fset :: (fs) fs |
|
77 apply (default) |
|
78 apply (induct_tac x rule: fset_induct) |
|
79 apply (simp add: supp_fempty) |
|
80 apply (simp add: supp_finsert) |
|
81 apply (simp add: finite_supp) |
|
82 done |
|
83 |
61 lemma atom_fmap_cong: |
84 lemma atom_fmap_cong: |
62 shows "(fmap atom x = fmap atom y) = (x = y)" |
85 shows "fmap atom x = fmap atom y \<longleftrightarrow> x = y" |
63 apply(rule inj_fmap_eq_iff) |
86 apply(rule inj_fmap_eq_iff) |
64 apply(simp add: inj_on_def) |
87 apply(simp add: inj_on_def) |
65 done |
88 done |
66 |
89 |
67 lemma supp_fmap_atom: |
90 lemma supp_fmap_atom: |
68 shows "supp (fmap atom x) = supp x" |
91 shows "supp (fmap atom S) = supp S" |
69 unfolding supp_def |
92 unfolding supp_def |
70 apply (perm_simp) |
93 apply(perm_simp) |
71 apply (simp add: atom_fmap_cong) |
94 apply(simp add: atom_fmap_cong) |
72 done |
|
73 |
|
74 lemma supp_atom_finsert: |
|
75 "supp (finsert (x :: atom) S) = supp x \<union> supp S" |
|
76 apply (subst supp_fset_to_set[symmetric]) |
|
77 apply (simp add: supp_finite_atom_set) |
|
78 apply (simp add: supp_atom_insert[OF fin_fset_to_set]) |
|
79 apply (simp add: supp_fset_to_set) |
|
80 done |
|
81 |
|
82 lemma supp_at_finsert: |
|
83 fixes a::"'a::at_base" |
|
84 shows "supp (finsert a S) = supp a \<union> supp S" |
|
85 apply (subst supp_fset_to_set[symmetric]) |
|
86 apply (simp add: supp_finite_atom_set) |
|
87 apply (simp add: supp_at_base_insert[OF fin_fset_to_set]) |
|
88 apply (simp add: supp_fset_to_set) |
|
89 done |
|
90 |
|
91 lemma supp_fempty: |
|
92 "supp {||} = {}" |
|
93 by (simp add: supp_def eqvts) |
|
94 |
|
95 instance fset :: (at_base) fs |
|
96 apply (default) |
|
97 apply (induct_tac x rule: fset_induct) |
|
98 apply (simp add: supp_fempty) |
|
99 apply (simp add: supp_at_finsert) |
|
100 apply (simp add: supp_at_base) |
|
101 done |
95 done |
102 |
96 |
103 lemma supp_at_fset: |
97 lemma supp_at_fset: |
104 fixes S::"('a::at_base) fset" |
98 fixes S::"('a::at_base) fset" |
105 shows "supp S = fset_to_set (fmap atom S)" |
99 shows "supp S = fset_to_set (fmap atom S)" |
106 apply (induct S) |
100 apply (induct S) |
107 apply (simp add: supp_fempty) |
101 apply (simp add: supp_fempty) |
108 apply (simp add: supp_at_finsert) |
102 apply (simp add: supp_finsert) |
109 apply (simp add: supp_at_base) |
103 apply (simp add: supp_at_base) |
110 done |
104 done |
111 |
105 |
|
106 |
112 end |
107 end |