380 and S T :: "'b :: fs" |
380 and S T :: "'b :: fs" |
381 assumes e: "(Abs_res (atom ` xs) T) = (Abs_res (atom ` ys) S)" |
381 assumes e: "(Abs_res (atom ` xs) T) = (Abs_res (atom ` ys) S)" |
382 and f1: "\<And>x. x \<in> atom ` xs \<Longrightarrow> x \<in> supp T \<Longrightarrow> x \<sharp> f xs T" |
382 and f1: "\<And>x. x \<in> atom ` xs \<Longrightarrow> x \<in> supp T \<Longrightarrow> x \<sharp> f xs T" |
383 and f2: "\<And>x. supp T - atom ` xs = supp S - atom ` ys \<Longrightarrow> x \<in> atom ` ys \<Longrightarrow> x \<in> supp S \<Longrightarrow> x \<sharp> f xs T" |
383 and f2: "\<And>x. supp T - atom ` xs = supp S - atom ` ys \<Longrightarrow> x \<in> atom ` ys \<Longrightarrow> x \<in> supp S \<Longrightarrow> x \<sharp> f xs T" |
384 and eqv: "\<And>p. p \<bullet> T = S \<Longrightarrow> supp p \<subseteq> atom ` xs \<inter> supp T \<union> atom ` ys \<inter> supp S |
384 and eqv: "\<And>p. p \<bullet> T = S \<Longrightarrow> supp p \<subseteq> atom ` xs \<inter> supp T \<union> atom ` ys \<inter> supp S |
385 \<Longrightarrow> p \<bullet> (atom ` xs \<inter> supp T) = atom ` ys \<inter> supp S |
385 \<Longrightarrow> p \<bullet> (atom ` xs \<inter> supp T) = atom ` ys \<inter> supp S \<Longrightarrow> p \<bullet> (f xs T) = f ys S" |
386 \<Longrightarrow> p \<bullet> (f xs T) = f ys S" |
|
387 shows "f xs T = f ys S" |
386 shows "f xs T = f ys S" |
388 using e apply - |
387 using e apply - |
389 apply (subst (asm) Abs_eq_res_set) |
388 apply (subst (asm) Abs_eq_res_set) |
390 apply (subst (asm) Abs_eq_iff2) |
389 apply (subst (asm) Abs_eq_iff2) |
391 apply (simp add: alphas) |
390 apply (simp add: alphas) |
419 apply (erule Abs_res_fcb) |
418 apply (erule Abs_res_fcb) |
420 apply (simp add: Abs_fresh_iff) |
419 apply (simp add: Abs_fresh_iff) |
421 apply (simp add: Abs_fresh_iff) |
420 apply (simp add: Abs_fresh_iff) |
422 apply auto[1] |
421 apply auto[1] |
423 apply (simp add: fresh_def fresh_star_def) |
422 apply (simp add: fresh_def fresh_star_def) |
424 apply (rule contra_subsetD) |
423 apply (rule contra_subsetD[OF supp_subst]) |
425 apply (rule supp_subst) |
|
426 apply simp |
424 apply simp |
427 apply blast |
425 apply blast |
|
426 apply clarify |
428 apply (simp add: subst_eqvt) |
427 apply (simp add: subst_eqvt) |
429 apply clarify |
|
430 apply (subst Abs_eq_iff) |
428 apply (subst Abs_eq_iff) |
431 apply (rule_tac x="0::perm" in exI) |
429 apply (rule_tac x="0::perm" in exI) |
432 apply (subgoal_tac "p \<bullet> subst \<theta>' t = subst \<theta>' (p \<bullet> t)") |
430 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
433 prefer 2 |
|
434 apply (subgoal_tac "\<theta>' = p \<bullet> \<theta>'") |
|
435 apply (simp add: subst_eqvt) |
|
436 apply (rule sym) |
|
437 apply (rule perm_supp_eq) |
|
438 apply (subgoal_tac "(atom ` fset xs \<inter> supp t \<union> atom ` fset xsa \<inter> supp (p \<bullet> t)) \<sharp>* \<theta>'") |
|
439 apply (metis Diff_partition fresh_star_Un) |
|
440 apply (simp add: fresh_star_Un fresh_star_inter1) |
|
441 apply (simp add: alphas fresh_star_zero) |
431 apply (simp add: alphas fresh_star_zero) |
442 apply (simp add: subst_eqvt) |
|
443 apply auto[1] |
432 apply auto[1] |
444 apply (subgoal_tac "atom xa \<in> p \<bullet> (atom ` fset xs \<inter> supp t)") |
433 apply (subgoal_tac "atom xa \<in> p \<bullet> (atom ` fset xs \<inter> supp t)") |
445 apply (simp add: inter_eqvt) |
434 apply (simp add: inter_eqvt) |
446 apply blast |
435 apply blast |
447 apply (subgoal_tac "atom xa \<in> supp(p \<bullet> t)") |
436 apply (subgoal_tac "atom xa \<in> supp(p \<bullet> t)") |
448 apply (auto simp add: IntI image_eqI) |
437 apply (auto simp add: IntI image_eqI) |
449 apply (drule subsetD[OF supp_subst]) |
438 apply (drule subsetD[OF supp_subst]) |
450 apply (simp add: fresh_star_def fresh_def) |
439 apply (simp add: fresh_star_def fresh_def) |
451 apply (subgoal_tac "x \<in> p \<bullet> (atom ` fset xs \<inter> supp t)") |
440 apply (subgoal_tac "x \<in> p \<bullet> (atom ` fset xs \<inter> supp t)") |
452 apply (simp add: ) |
441 apply (simp) |
453 apply (subgoal_tac "x \<in> supp(p \<bullet> t)") |
442 apply (subgoal_tac "x \<in> supp(p \<bullet> t)") |
454 apply (metis inf1I inter_eqvt mem_def supp_eqvt ) |
443 apply (metis inf1I inter_eqvt mem_def supp_eqvt) |
455 apply (rotate_tac 4) |
444 apply (subgoal_tac "x \<notin> supp \<theta>'") |
456 apply (drule sym) |
445 apply (metis UnE subsetD supp_subst) |
457 apply (simp add: subst_eqvt) |
446 apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>')") |
458 apply (drule subsetD[OF supp_subst]) |
|
459 apply auto[1] |
|
460 apply (rotate_tac 2) |
|
461 apply (subst (asm) fresh_star_permute_iff[symmetric]) |
|
462 apply (simp add: fresh_star_def fresh_def) |
447 apply (simp add: fresh_star_def fresh_def) |
|
448 apply (simp (no_asm) add: fresh_star_permute_iff) |
|
449 apply (rule perm_supp_eq) |
|
450 apply (simp add: fresh_def fresh_star_def) |
463 apply blast |
451 apply blast |
464 done |
452 done |
465 |
453 |
466 |
454 |
467 text {* Some Tests about Alpha-Equality *} |
455 text {* Some Tests about Alpha-Equality *} |