6 assumes "(supp x - as) \<sharp>* p" |
6 assumes "(supp x - as) \<sharp>* p" |
7 and "p \<bullet> x = y" |
7 and "p \<bullet> x = y" |
8 and "p \<bullet> as = bs" |
8 and "p \<bullet> as = bs" |
9 shows "(as, x) \<approx>set (op =) supp p (bs, y)" |
9 shows "(as, x) \<approx>set (op =) supp p (bs, y)" |
10 using assms unfolding alphas |
10 using assms unfolding alphas |
11 by (metis Diff_eqvt atom_set_perm_eq supp_eqvt) |
11 apply(simp) |
|
12 apply(clarify) |
|
13 apply(simp only: Diff_eqvt[symmetric] supp_eqvt[symmetric]) |
|
14 apply(simp only: atom_set_perm_eq) |
|
15 done |
|
16 |
12 |
17 |
13 lemma |
18 lemma |
14 assumes "(supp x - set as) \<sharp>* p" |
19 assumes "(supp x - set as) \<sharp>* p" |
15 and "p \<bullet> x = y" |
20 and "p \<bullet> x = y" |
16 and "p \<bullet> as = bs" |
21 and "p \<bullet> as = bs" |
17 shows "(as, x) \<approx>lst (op =) supp p (bs, y)" |
22 shows "(as, x) \<approx>lst (op =) supp p (bs, y)" |
18 using assms unfolding alphas |
23 using assms unfolding alphas |
19 by (metis Diff_eqvt atom_set_perm_eq supp_eqvt supp_of_atom_list) |
24 apply(simp) |
|
25 apply(clarify) |
|
26 apply(simp only: set_eqvt[symmetric] Diff_eqvt[symmetric] supp_eqvt[symmetric]) |
|
27 apply(simp only: atom_set_perm_eq) |
|
28 done |
20 |
29 |
21 lemma |
30 lemma |
22 assumes "(supp x - as) \<sharp>* p" |
31 assumes "(supp x - as) \<sharp>* p" |
23 and "p \<bullet> x = y" |
32 and "p \<bullet> x = y" |
24 and "p \<bullet> (as \<inter> supp x) = bs \<inter> supp y" |
33 and "p \<bullet> (as \<inter> supp x) = bs \<inter> supp y" |