156 and fresh1: "set as \<sharp>* c" |
155 and fresh1: "set as \<sharp>* c" |
157 and fresh2: "set bs \<sharp>* c" |
156 and fresh2: "set bs \<sharp>* c" |
158 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c" |
157 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c" |
159 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
158 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
160 shows "f as x c = f bs y c" |
159 shows "f as x c = f bs y c" |
161 *) |
160 proof - |
|
161 have fin1: "finite (supp (f as x c))" |
|
162 apply(rule_tac S="supp (as, x, c)" in supports_finite) |
|
163 apply(simp add: supports_def) |
|
164 apply(simp add: fresh_def[symmetric]) |
|
165 apply(clarify) |
|
166 apply(subst perm1) |
|
167 apply(simp add: supp_swap fresh_star_def) |
|
168 apply(simp add: swap_fresh_fresh fresh_Pair) |
|
169 apply(simp add: finite_supp) |
|
170 done |
|
171 have fin2: "finite (supp (f bs y c))" |
|
172 apply(rule_tac S="supp (bs, y, c)" in supports_finite) |
|
173 apply(simp add: supports_def) |
|
174 apply(simp add: fresh_def[symmetric]) |
|
175 apply(clarify) |
|
176 apply(subst perm2) |
|
177 apply(simp add: supp_swap fresh_star_def) |
|
178 apply(simp add: swap_fresh_fresh fresh_Pair) |
|
179 apply(simp add: finite_supp) |
|
180 done |
|
181 obtain q::"perm" where |
|
182 fr1: "(q \<bullet> (set as)) \<sharp>* (as, bs, x, y, c, f as x c, f bs y c)" and |
|
183 fr2: "supp q \<sharp>* Abs_lst as x" and |
|
184 inc: "supp q \<subseteq> (set as) \<union> q \<bullet> (set as)" |
|
185 using at_set_avoiding3[where xs="set as" and c="(as, bs, x, y, c, f as x c, f bs y c)" |
|
186 and x="Abs_lst as x"] |
|
187 apply(simp add: supp_Pair finite_supp fin1 fin2 Abs_fresh_star) |
|
188 apply(erule exE) |
|
189 apply(erule conjE)+ |
|
190 apply(drule fresh_star_supp_conv) |
|
191 apply(blast) |
|
192 done |
|
193 have "Abs_lst (q \<bullet> as) (q \<bullet> x) = q \<bullet> Abs_lst as x" by simp |
|
194 also have "\<dots> = Abs_lst as x" |
|
195 apply(rule perm_supp_eq) |
|
196 apply(simp add: fr2) |
|
197 done |
|
198 finally have "Abs_lst (q \<bullet> as) (q \<bullet> x) = Abs_lst bs y" using e by simp |
|
199 then obtain r::perm where |
|
200 qq1: "q \<bullet> x = r \<bullet> y" and |
|
201 qq2: "q \<bullet> as = r \<bullet> bs" and |
|
202 qq3: "supp r \<subseteq> (set (q \<bullet> as) \<union> set bs)" |
|
203 apply - |
|
204 apply(drule_tac sym) |
|
205 apply(simp only: Abs_eq_iff2 alphas) |
|
206 apply(erule exE) |
|
207 apply(erule conjE)+ |
|
208 apply(drule_tac x="p" in meta_spec) |
|
209 apply(simp) |
|
210 apply(blast) |
|
211 done |
|
212 have "f as x c = q \<bullet> (f as x c)" |
|
213 apply(rule sym) |
|
214 apply(rule perm_supp_eq) |
|
215 using inc fcb1 fr1 |
|
216 apply(simp add: set_eqvt) |
|
217 apply(simp add: fresh_star_Pair) |
|
218 apply(auto simp add: fresh_star_def) |
|
219 done |
|
220 also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" |
|
221 apply(subst perm1) |
|
222 using inc fresh1 fr1 |
|
223 apply(simp add: set_eqvt) |
|
224 apply(simp add: fresh_star_Pair) |
|
225 apply(auto simp add: fresh_star_def) |
|
226 done |
|
227 also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
|
228 also have "\<dots> = r \<bullet> (f bs y c)" |
|
229 apply(rule sym) |
|
230 apply(subst perm2) |
|
231 using qq3 fresh2 fr1 |
|
232 apply(simp add: set_eqvt) |
|
233 apply(simp add: fresh_star_Pair) |
|
234 apply(auto simp add: fresh_star_def) |
|
235 done |
|
236 also have "... = f bs y c" |
|
237 apply(rule perm_supp_eq) |
|
238 using qq3 fr1 fcb2 |
|
239 apply(simp add: set_eqvt) |
|
240 apply(simp add: fresh_star_Pair) |
|
241 apply(auto simp add: fresh_star_def) |
|
242 done |
|
243 finally show ?thesis by simp |
|
244 qed |
162 |
245 |
163 lemma supp_zero_perm_zero: |
246 lemma supp_zero_perm_zero: |
164 shows "supp (p :: perm) = {} \<longleftrightarrow> p = 0" |
247 shows "supp (p :: perm) = {} \<longleftrightarrow> p = 0" |
165 by (metis supp_perm_singleton supp_zero_perm) |
248 by (metis supp_perm_singleton supp_zero_perm) |
166 |
249 |