59 by (lifting map_eqvt) |
59 by (lifting map_eqvt) |
60 |
60 |
61 lemma fset_to_set_eqvt[eqvt]: "pi \<bullet> (fset_to_set x) = fset_to_set (pi \<bullet> x)" |
61 lemma fset_to_set_eqvt[eqvt]: "pi \<bullet> (fset_to_set x) = fset_to_set (pi \<bullet> x)" |
62 by (lifting set_eqvt) |
62 by (lifting set_eqvt) |
63 |
63 |
|
64 lemma fin_fset_to_set: |
|
65 "finite (fset_to_set x)" |
|
66 by (induct x) (simp_all) |
|
67 |
64 lemma supp_fset_to_set: |
68 lemma supp_fset_to_set: |
65 "supp (fset_to_set x) = supp x" |
69 "supp (fset_to_set x) = supp x" |
66 apply (simp add: supp_def) |
70 apply (simp add: supp_def) |
67 apply (simp add: eqvts) |
71 apply (simp add: eqvts) |
68 apply (simp add: fset_cong) |
72 apply (simp add: fset_cong) |
78 "supp (fmap atom x) = supp x" |
82 "supp (fmap atom x) = supp x" |
79 apply (simp add: supp_def) |
83 apply (simp add: supp_def) |
80 apply (simp add: eqvts eqvts_raw atom_fmap_cong) |
84 apply (simp add: eqvts eqvts_raw atom_fmap_cong) |
81 done |
85 done |
82 |
86 |
83 (*lemma "\<not> (memb x S) \<Longrightarrow> \<not> (memb y T) \<Longrightarrow> ((x # S) \<approx> (y # T)) = (x = y \<and> S \<approx> T)"*) |
87 lemma supp_atom_insert: |
|
88 "finite (xs :: atom set) \<Longrightarrow> supp (insert x xs) = supp x \<union> supp xs" |
|
89 apply (simp add: supp_finite_atom_set) |
|
90 apply (simp add: supp_atom) |
|
91 done |
84 |
92 |
85 lemma infinite_Un: |
93 lemma atom_image_cong: |
86 shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T" |
94 shows "(atom ` X = atom ` Y) = (X = Y)" |
87 by simp |
95 apply(rule inj_image_eq_iff) |
|
96 apply(simp add: inj_on_def) |
|
97 done |
88 |
98 |
89 lemma supp_insert: "supp (insert (x :: 'a :: fs) xs) = supp x \<union> supp xs" |
99 lemma atom_eqvt_raw: |
90 oops |
100 fixes p::"perm" |
|
101 shows "(p \<bullet> atom) = atom" |
|
102 by (simp add: expand_fun_eq permute_fun_def atom_eqvt) |
91 |
103 |
92 lemma supp_finsert: |
104 lemma supp_finite_at_set: |
93 "supp (finsert (x :: 'a :: fs) S) = supp x \<union> supp S" |
105 fixes S::"('a :: at) set" |
|
106 assumes a: "finite S" |
|
107 shows "supp S = atom ` S" |
|
108 apply(rule finite_supp_unique) |
|
109 apply(simp add: supports_def) |
|
110 apply (rule finite_induct[OF a]) |
|
111 apply (simp add: eqvts) |
|
112 apply (simp) |
|
113 apply clarify |
|
114 apply (subst atom_image_cong[symmetric]) |
|
115 apply (subst atom_eqvt_raw[symmetric]) |
|
116 apply (subst eqvts[symmetric]) |
|
117 apply (rule swap_set_not_in) |
|
118 apply simp_all |
|
119 apply(rule finite_imageI) |
|
120 apply(rule a) |
|
121 apply (subst atom_image_cong[symmetric]) |
|
122 apply (subst atom_eqvt_raw[symmetric]) |
|
123 apply (subst eqvts[symmetric]) |
|
124 apply (rule swap_set_in) |
|
125 apply simp_all |
|
126 done |
|
127 |
|
128 lemma supp_at_insert: |
|
129 "finite (xs :: ('a :: at) set) \<Longrightarrow> supp (insert x xs) = supp x \<union> supp xs" |
|
130 apply (simp add: supp_finite_at_set) |
|
131 apply (simp add: supp_at_base) |
|
132 done |
|
133 |
|
134 lemma supp_atom_finsert: |
|
135 "supp (finsert (x :: atom) S) = supp x \<union> supp S" |
94 apply (subst supp_fset_to_set[symmetric]) |
136 apply (subst supp_fset_to_set[symmetric]) |
95 apply simp |
137 apply (simp add: supp_finite_atom_set) |
96 (* apply (simp add: supp_insert supp_fset_to_set) *) |
138 apply (simp add: supp_atom_insert[OF fin_fset_to_set]) |
97 oops |
139 apply (simp add: supp_fset_to_set) |
|
140 done |
98 |
141 |
99 instance fset :: (fs) fs |
142 lemma supp_at_finsert: |
|
143 "supp (finsert (x :: 'a :: at) S) = supp x \<union> supp S" |
|
144 apply (subst supp_fset_to_set[symmetric]) |
|
145 apply (simp add: supp_finite_atom_set) |
|
146 apply (simp add: supp_at_insert[OF fin_fset_to_set]) |
|
147 apply (simp add: supp_fset_to_set) |
|
148 done |
|
149 |
|
150 instance fset :: (at) fs |
100 apply (default) |
151 apply (default) |
101 apply (induct_tac x rule: fset_induct) |
152 apply (induct_tac x rule: fset_induct) |
102 apply (simp add: supp_def eqvts) |
153 apply (simp add: supp_def eqvts) |
103 (* apply (simp add: supp_finsert) *) |
154 apply (simp add: supp_at_finsert) |
104 (* apply default ? *) |
155 apply (simp add: supp_at_base) |
105 oops |
156 done |
106 |
157 |
107 end |
158 end |