# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1265047040 -3600
# Node ID 683483199a5df08ec9c1aa7368d3a9bb99ea9a34
# Parent  272ea46a1766bdf7296033a8669c63def5a2e7f5
added a single-binder alpha equivalence; showed one half of the equivalence proof between general and single binder case

diff -r 272ea46a1766 -r 683483199a5d Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Mon Feb 01 16:46:07 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Mon Feb 01 18:57:20 2010 +0100
@@ -269,5 +269,54 @@
   shows "(Abs bs x) = (Abs cs y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
   by (lifting alpha_abs.simps(1))
 
+
+
+(* 
+  below is a construction site for showing that in the
+  single-binder case, the old and new alpha equivalence 
+  coincide
+*)
+
+fun
+  alpha1
+where
+  "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))"
+
+notation 
+  alpha1 ("_ \<approx>abs1 _")
+
+lemma
+  assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b"
+  shows "({a}, x) \<approx>abs ({b}, y)"
+using a
+apply(simp)
+apply(erule disjE)
+apply(simp)
+apply(rule exI)
+apply(rule alpha_gen_refl)
+apply(simp)
+apply(rule_tac x="(a \<rightleftharpoons> b)" in  exI)
+apply(simp add: alpha_gen)
+apply(simp add: fresh_def)
+apply(rule conjI)
+apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in  permute_eq_iff[THEN iffD1])
+apply(rule trans)
+apply(simp add: Diff_eqvt supp_eqvt)
+apply(subst swap_set_not_in)
+back
+apply(simp)
+apply(simp)
+apply(simp add: permute_set_eq)
+apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1])
+apply(simp add: permute_self)
+apply(simp add: Diff_eqvt supp_eqvt)
+apply(simp add: permute_set_eq)
+apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")
+apply(simp add: fresh_star_def fresh_def)
+apply(blast)
+apply(simp add: supp_swap)
+done
+
+
 end