51 and S T :: "'b :: fs" |
51 and S T :: "'b :: fs" |
52 and c::"'c::fs" |
52 and c::"'c::fs" |
53 assumes e: "(Abs_lst [atom a] T) = (Abs_lst [atom b] S)" |
53 assumes e: "(Abs_lst [atom a] T) = (Abs_lst [atom b] S)" |
54 and fcb: "\<And>a T. atom a \<sharp> f a T c" |
54 and fcb: "\<And>a T. atom a \<sharp> f a T c" |
55 and fresh: "{atom a, atom b} \<sharp>* c" |
55 and fresh: "{atom a, atom b} \<sharp>* c" |
56 and p1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a T c) = f (p \<bullet> a) (p \<bullet> T) c" |
56 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a T c) = f (p \<bullet> a) (p \<bullet> T) c" |
57 and p2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b S c) = f (p \<bullet> b) (p \<bullet> S) c" |
57 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b S c) = f (p \<bullet> b) (p \<bullet> S) c" |
58 shows "f a T c = f b S c" |
58 shows "f a T c = f b S c" |
59 proof - |
59 proof - |
60 have fin1: "finite (supp (f a T c))" |
60 have fin1: "finite (supp (f a T c))" |
61 apply(rule_tac S="supp (a, T, c)" in supports_finite) |
61 apply(rule_tac S="supp (a, T, c)" in supports_finite) |
62 apply(simp add: supports_def) |
62 apply(simp add: supports_def) |
63 apply(simp add: fresh_def[symmetric]) |
63 apply(simp add: fresh_def[symmetric]) |
64 apply(clarify) |
64 apply(clarify) |
65 apply(subst p1) |
65 apply(subst perm1) |
66 apply(simp add: supp_swap fresh_star_def) |
66 apply(simp add: supp_swap fresh_star_def) |
67 apply(simp add: swap_fresh_fresh fresh_Pair) |
67 apply(simp add: swap_fresh_fresh fresh_Pair) |
68 apply(simp add: finite_supp) |
68 apply(simp add: finite_supp) |
69 done |
69 done |
70 have fin2: "finite (supp (f b S c))" |
70 have fin2: "finite (supp (f b S c))" |
71 apply(rule_tac S="supp (b, S, c)" in supports_finite) |
71 apply(rule_tac S="supp (b, S, c)" in supports_finite) |
72 apply(simp add: supports_def) |
72 apply(simp add: supports_def) |
73 apply(simp add: fresh_def[symmetric]) |
73 apply(simp add: fresh_def[symmetric]) |
74 apply(clarify) |
74 apply(clarify) |
75 apply(subst p2) |
75 apply(subst perm2) |
76 apply(simp add: supp_swap fresh_star_def) |
76 apply(simp add: supp_swap fresh_star_def) |
77 apply(simp add: swap_fresh_fresh fresh_Pair) |
77 apply(simp add: swap_fresh_fresh fresh_Pair) |
78 apply(simp add: finite_supp) |
78 apply(simp add: finite_supp) |
79 done |
79 done |
80 obtain d::"'a::at" where fr: "atom d \<sharp> (a, b, S, T, c, f a T c, f b S c)" |
80 obtain d::"'a::at" where fr: "atom d \<sharp> (a, b, S, T, c, f a T c, f b S c)" |
179 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
179 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
180 apply(simp add: Abs_fresh_iff) |
180 apply(simp add: Abs_fresh_iff) |
181 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
181 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
182 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
182 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
183 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
183 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
184 -- "old fcb" |
184 apply(elim conjE) |
185 apply(elim conjE) |
185 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
186 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
186 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
187 apply(erule Abs_lst1_fcb) |
187 apply(erule Abs_lst1_fcb2) |
188 apply(simp add: Abs_fresh_iff) |
188 apply(simp add: Abs_fresh_iff) |
189 apply(simp add: Abs_fresh_iff) |
189 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
190 apply(erule fresh_eqvt_at) |
190 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
191 apply(simp add: finite_supp) |
191 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
192 apply(simp add: fresh_Pair fresh_at_base(1)) |
192 apply(blast) |
193 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
193 apply(blast) |
194 apply simp |
194 apply(elim conjE) |
195 apply(blast) |
195 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
196 apply(elim conjE) |
196 apply(simp add: Abs_fresh_iff) |
197 apply(erule Abs_lst1_fcb) |
197 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
198 apply(simp add: Abs_fresh_iff) |
198 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
199 apply(simp add: Abs_fresh_iff) |
199 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
200 apply(erule fresh_eqvt_at) |
|
201 apply(simp add: finite_supp) |
|
202 apply(simp add: fresh_Pair fresh_at_base(1)) |
|
203 apply(simp add: fresh_Pair) |
|
204 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
|
205 apply simp |
|
206 apply(erule conjE)+ |
|
207 apply(rule conjI) |
200 apply(rule conjI) |
208 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
201 apply(elim conjE) |
209 apply(erule Abs_lst1_fcb) |
202 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
210 apply(simp add: Abs_fresh_iff) |
203 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
211 apply(simp add: Abs_fresh_iff) |
204 apply(erule Abs_lst1_fcb2) |
212 apply(erule fresh_eqvt_at) |
205 apply(simp add: Abs_fresh_iff) |
213 apply(simp add: finite_supp) |
206 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
214 apply(simp add: fresh_Pair fresh_at_base(1)) |
207 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
215 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
208 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
216 apply simp |
209 apply(blast) |
217 apply(blast) |
210 apply(blast) |
|
211 apply(erule conjE)+ |
218 apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)") |
212 apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)") |
219 apply(erule Abs_lst1_fcb) |
213 apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)") |
220 apply(simp add: Abs_fresh_iff) |
214 apply(erule Abs_lst1_fcb2) |
221 apply(simp add: Abs_fresh_iff) |
215 apply(simp add: Abs_fresh_iff) |
222 apply(erule fresh_eqvt_at) |
216 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
223 apply(simp add: finite_supp) |
217 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
224 apply(simp add: fresh_Pair fresh_at_base(1)) |
218 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
225 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
219 apply(blast) |
226 apply simp |
220 apply(blast) |
227 apply(blast) |
221 apply(elim conjE) |
228 apply(elim conjE) |
222 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
229 apply(erule Abs_lst1_fcb) |
223 apply(simp add: Abs_fresh_iff) |
230 apply(simp add: Abs_fresh_iff) |
224 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
231 apply(simp add: Abs_fresh_iff) |
225 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
232 apply(erule fresh_eqvt_at) |
226 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
233 apply(simp add: finite_supp) |
227 apply(elim conjE) |
234 apply(simp add: fresh_Pair fresh_at_base(1)) |
228 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
235 apply(simp add: fresh_Pair) |
229 apply(simp add: Abs_fresh_iff) |
236 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
230 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
237 apply simp |
231 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
238 apply(elim conjE) |
232 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
239 apply(erule Abs_lst1_fcb) |
233 apply(elim conjE) |
240 apply(simp add: Abs_fresh_iff) |
234 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
241 apply(simp add: Abs_fresh_iff) |
235 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
242 apply(erule fresh_eqvt_at) |
236 apply(erule Abs_lst1_fcb2) |
243 apply(simp add: finite_supp) |
237 apply(simp add: Abs_fresh_iff) |
244 apply(simp add: fresh_Pair fresh_at_base(1)) |
238 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
245 apply(simp add: fresh_Pair) |
239 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
246 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
240 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
247 apply simp |
241 apply(blast) |
248 apply(erule conjE)+ |
242 apply(blast) |
249 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
243 apply(erule conjE)+ |
250 apply(erule Abs_lst1_fcb) |
244 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
251 apply(simp add: Abs_fresh_iff) |
245 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
252 apply(simp add: Abs_fresh_iff) |
246 apply(erule Abs_lst1_fcb2) |
253 apply(erule fresh_eqvt_at) |
247 apply(simp add: Abs_fresh_iff) |
254 apply(simp add: finite_supp) |
248 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
255 apply(simp add: fresh_Pair fresh_at_base(1)) |
249 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
256 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
250 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
257 apply simp |
251 apply(blast) |
258 apply(blast) |
|
259 apply(erule conjE)+ |
|
260 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
|
261 apply(erule Abs_lst1_fcb) |
|
262 apply(simp add: Abs_fresh_iff) |
|
263 apply(simp add: Abs_fresh_iff) |
|
264 apply(erule fresh_eqvt_at) |
|
265 apply(simp add: finite_supp) |
|
266 apply(simp add: fresh_Pair fresh_at_base(1)) |
|
267 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
|
268 apply simp |
|
269 apply(blast) |
252 apply(blast) |
270 apply(rule conjI) |
253 apply(rule conjI) |
271 apply(elim conjE) |
254 apply(erule conjE)+ |
272 apply(erule Abs_lst1_fcb) |
255 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
273 apply(simp add: Abs_fresh_iff) |
256 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
274 apply(simp add: Abs_fresh_iff) |
257 apply(erule Abs_lst1_fcb2) |
275 apply(erule fresh_eqvt_at) |
258 apply(simp add: Abs_fresh_iff) |
276 apply(simp add: finite_supp) |
259 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
277 apply(simp add: fresh_Pair fresh_at_base(1)) |
260 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
278 apply(simp add: eqvt_at_def swap_at_base_sort) |
261 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
279 apply simp |
262 apply(blast) |
280 apply(elim conjE) |
263 apply(blast) |
281 apply(erule Abs_lst1_fcb) |
264 apply(erule conjE)+ |
282 apply(simp add: Abs_fresh_iff) |
265 apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)") |
283 apply(simp add: Abs_fresh_iff) |
266 apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)") |
284 apply(erule fresh_eqvt_at) |
267 apply(erule Abs_lst1_fcb2) |
285 apply(simp add: finite_supp) |
268 apply(simp add: Abs_fresh_iff) |
286 apply(simp add: fresh_Pair fresh_at_base(1)) |
269 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
287 apply(simp add: fresh_Pair) |
270 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
288 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
271 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
289 apply simp |
272 apply(blast) |
290 apply(erule conjE)+ |
273 apply(blast) |
291 defer |
274 defer |
292 apply(elim conjE) |
275 apply(erule conjE)+ |
293 apply(rule conjI) |
276 apply(rule conjI) |
294 apply(erule Abs_lst1_fcb) |
277 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
295 apply(simp add: Abs_fresh_iff) |
278 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
296 apply(simp add: Abs_fresh_iff) |
279 apply(erule Abs_lst1_fcb2) |
297 apply(erule fresh_eqvt_at) |
280 apply(simp add: Abs_fresh_iff) |
298 apply(simp add: finite_supp) |
281 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
299 apply(simp add: fresh_Pair fresh_at_base(1)) |
282 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
300 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
283 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
301 apply simp |
284 apply(blast) |
302 apply(erule Abs_lst1_fcb) |
285 apply(blast) |
303 apply(simp add: Abs_fresh_iff) |
286 apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)") |
304 apply(simp add: Abs_fresh_iff) |
287 apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)") |
305 apply(erule fresh_eqvt_at) |
288 apply(erule Abs_lst1_fcb2) |
306 apply(simp add: finite_supp) |
289 apply(simp add: Abs_fresh_iff) |
307 apply(simp add: fresh_Pair fresh_at_base(1)) |
290 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
308 apply(simp add: fresh_Pair) |
291 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
309 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
292 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
310 apply simp |
293 apply(blast) |
|
294 apply(blast) |
311 oops |
295 oops |
312 |
296 |
313 end |
297 end |
314 |
298 |
315 |
299 |