124 apply(simp add: permute_fun_def) |
124 apply(simp add: permute_fun_def) |
125 apply(simp add: atom_eqvt) |
125 apply(simp add: atom_eqvt) |
126 apply(simp add: atom_image_cong) |
126 apply(simp add: atom_image_cong) |
127 done |
127 done |
128 |
128 |
|
129 lemma supp_finite_at_set_aux: |
|
130 fixes S::"('a::at) set" |
|
131 assumes a: "finite S" |
|
132 shows "supp S = atom ` S" |
|
133 proof |
|
134 show "supp S \<subseteq> ((atom::'a::at \<Rightarrow> atom) ` S)" |
|
135 apply(rule supp_is_subset) |
|
136 apply(simp add: supports_def) |
|
137 apply(rule allI)+ |
|
138 apply(rule impI) |
|
139 apply(rule swap_fresh_fresh) |
|
140 apply(simp add: fresh_def) |
|
141 apply(simp add: atom_image_supp) |
|
142 apply(subst supp_finite_atom_set) |
|
143 apply(rule finite_imageI) |
|
144 apply(simp add: a) |
|
145 apply(simp) |
|
146 apply(simp add: fresh_def) |
|
147 apply(simp add: atom_image_supp) |
|
148 apply(subst supp_finite_atom_set) |
|
149 apply(rule finite_imageI) |
|
150 apply(simp add: a) |
|
151 apply(simp) |
|
152 apply(rule finite_imageI) |
|
153 apply(simp add: a) |
|
154 done |
|
155 next |
|
156 have "supp ((atom::'a::at \<Rightarrow> atom) ` S) \<subseteq> supp ((op `) (atom::'a::at \<Rightarrow> atom)) \<union> supp S" |
|
157 by (simp add: supp_fun_app) |
|
158 moreover |
|
159 have "supp ((op `) (atom::'a::at \<Rightarrow> atom)) = {}" |
|
160 apply(rule supp_fun_eqvt) |
|
161 apply(perm_simp) |
|
162 apply(simp) |
|
163 done |
|
164 moreover |
|
165 have "supp ((atom::'a::at \<Rightarrow> atom) ` S) = ((atom::'a::at \<Rightarrow> atom) ` S)" |
|
166 apply(subst supp_finite_atom_set) |
|
167 apply(rule finite_imageI) |
|
168 apply(simp add: a) |
|
169 apply(simp) |
|
170 done |
|
171 ultimately |
|
172 show "((atom::'a::at \<Rightarrow> atom) ` S) \<subseteq> supp S" by simp |
|
173 qed |
|
174 |
|
175 |
129 lemma supp_at_insert: |
176 lemma supp_at_insert: |
130 fixes S::"('a::at) set" |
177 fixes S::"('a::at) set" |
131 assumes a: "finite S" |
178 assumes a: "finite S" |
132 shows "supp (insert a S) = supp a \<union> supp S" |
179 shows "supp (insert a S) = supp a \<union> supp S" |
133 using a |
180 using a by (simp add: supp_finite_at_set supp_at_base) |
134 apply (simp add: supp_finite_at_set) |
181 |
135 apply (simp add: supp_at_base) |
|
136 done |
|
137 |
182 |
138 section {* A swapping operation for concrete atoms *} |
183 section {* A swapping operation for concrete atoms *} |
139 |
184 |
140 definition |
185 definition |
141 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |
186 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |