272 

   273 

   274 (* 

   275   below is a construction site for showing that in the

   276   single-binder case, the old and new alpha equivalence 

   277   coincide

   278 *)

   279 

   280 fun

   281   alpha1

   282 where

   283   "alpha1 (a, x) (b, y) \<longleftrightarrow> ((a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y))"

   284 

   285 notation 

   286   alpha1 ("_ \<approx>abs1 _")

   287 

   288 lemma

   289   assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b"

   290   shows "({a}, x) \<approx>abs ({b}, y)"

   291 using a

   292 apply(simp)

   293 apply(erule disjE)

   294 apply(simp)

   295 apply(rule exI)

   296 apply(rule alpha_gen_refl)

   297 apply(simp)

   298 apply(rule_tac x="(a \<rightleftharpoons> b)" in  exI)

   299 apply(simp add: alpha_gen)

   300 apply(simp add: fresh_def)

   301 apply(rule conjI)

   302 apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in  permute_eq_iff[THEN iffD1])

   303 apply(rule trans)

   304 apply(simp add: Diff_eqvt supp_eqvt)

   305 apply(subst swap_set_not_in)

   306 back

   307 apply(simp)

   308 apply(simp)

   309 apply(simp add: permute_set_eq)

   310 apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1])

   311 apply(simp add: permute_self)

   312 apply(simp add: Diff_eqvt supp_eqvt)

   313 apply(simp add: permute_set_eq)

   314 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")

   315 apply(simp add: fresh_star_def fresh_def)

   316 apply(blast)

   317 apply(simp add: supp_swap)

   318 done

   319 

   320