115 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] |
115 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] |
116 unfolding fresh_star_def fresh_def |
116 unfolding fresh_star_def fresh_def |
117 unfolding swap_set_not_in[OF a1 a2] |
117 unfolding swap_set_not_in[OF a1 a2] |
118 by (rule_tac x="(a \<rightleftharpoons> b)" in exI) |
118 by (rule_tac x="(a \<rightleftharpoons> b)" in exI) |
119 (auto simp add: supp_perm swap_atom) |
119 (auto simp add: supp_perm swap_atom) |
120 |
|
121 lemma alpha_gen_swap_fun: |
|
122 assumes f_eqvt: "\<And>pi. (pi \<bullet> (f x)) = f (pi \<bullet> x)" |
|
123 assumes a1: "a \<notin> (f x) - bs" |
|
124 and a2: "b \<notin> (f x) - bs" |
|
125 shows "\<exists>pi. (bs, x) \<approx>gen (op=) f pi ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)" |
|
126 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI) |
|
127 apply(simp add: alpha_gen) |
|
128 apply(simp add: f_eqvt[symmetric] Diff_eqvt[symmetric]) |
|
129 apply(simp add: swap_set_not_in[OF a1 a2]) |
|
130 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}") |
|
131 using a1 a2 |
|
132 apply(simp add: fresh_star_def fresh_def) |
|
133 apply(blast) |
|
134 apply(simp add: supp_swap) |
|
135 done |
|
136 |
120 |
137 fun |
121 fun |
138 supp_abs_fun |
122 supp_abs_fun |
139 where |
123 where |
140 "supp_abs_fun (bs, x) = (supp x) - bs" |
124 "supp_abs_fun (bs, x) = (supp x) - bs" |