# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1342084292 -3600
# Node ID 0440bc1a243876b852bdf14d26246065b180fb24
# Parent  1b7c034c9e9ef42a9efe82b9cd3792cf75181c52
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)

diff -r 1b7c034c9e9e -r 0440bc1a2438 Nominal/Ex/CPS/CPS1_Plotkin.thy
--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy	Mon Jun 18 14:50:02 2012 +0100
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy	Thu Jul 12 10:11:32 2012 +0100
@@ -30,7 +30,6 @@
 apply simp
 thm Abs1_eq_iff
 apply(subst Abs1_eq_iff)
-apply(auto)[2]
 apply(rule disjI2)
 apply(rule conjI)
 apply(simp)
@@ -130,11 +129,10 @@
 apply (rename_tac M N u K)
 apply (subgoal_tac "Lam n (M+ $$ n~ $$ K) =  Lam u (M+ $$ u~ $$ K)")
 apply (simp only:)
-apply (auto simp add: Abs1_eq_iff swap_fresh_fresh fresh_at_base)[1]
+apply (auto simp add: Abs1_eq_iff flip_fresh_fresh fresh_at_base)[1]
 apply (subgoal_tac "Lam m (Na* $$ Lam n (m~ $$ n~ $$ Ka)) = Lam ma (Na* $$ Lam na (ma~ $$ na~ $$ Ka))")
 apply (simp only:)
-apply (simp add: Abs1_eq_iff swap_fresh_fresh fresh_at_base)
-apply(simp_all add: flip_def[symmetric])
+apply (simp add: Abs1_eq_iff flip_fresh_fresh fresh_at_base)
 apply (case_tac "m = ma")
 apply simp_all
 apply (case_tac "m = na")
diff -r 1b7c034c9e9e -r 0440bc1a2438 Nominal/Ex/CPS/CPS2_DanvyNielsen.thy
--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Mon Jun 18 14:50:02 2012 +0100
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Thu Jul 12 10:11:32 2012 +0100
@@ -27,8 +27,7 @@
   apply (simp add: finite_supp)
   apply (simp add: fresh_Pair)
   apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh)
-  apply(simp)
+  apply (simp add: flip_fresh_fresh)
   done
 
 termination (eqvt) by lexicographic_order
@@ -52,7 +51,7 @@
   apply (simp add: finite_supp)
   apply (simp add: fresh_Pair)
   apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh)
+  apply (simp add: flip_fresh_fresh)
   done
 
 termination (eqvt) by lexicographic_order
diff -r 1b7c034c9e9e -r 0440bc1a2438 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Mon Jun 18 14:50:02 2012 +0100
+++ b/Nominal/Ex/Lambda.thy	Thu Jul 12 10:11:32 2012 +0100
@@ -864,7 +864,7 @@
 
 lemma abs_same_binder:
   fixes t ta s sa :: "_ :: fs"
-  assumes "sort_of (atom x) = sort_of (atom y)"
+  and x y::"'a::at"
   shows "[[atom x]]lst. t = [[atom y]]lst. ta \<and> [[atom x]]lst. s = [[atom y]]lst. sa
      \<longleftrightarrow> [[atom x]]lst. (t, s) = [[atom y]]lst. (ta, sa)"
   by (cases "atom x = atom y") (auto simp add: Abs1_eq_iff assms fresh_Pair)
@@ -907,6 +907,7 @@
 
 consts P :: "lam \<Rightarrow> bool"
 
+(*
 nominal_primrec  
   A :: "lam => lam"
 where  
@@ -943,7 +944,7 @@
 apply(rule allI)
 apply(rule refl)
 oops
-
+*)
 end
 
 
diff -r 1b7c034c9e9e -r 0440bc1a2438 Nominal/Ex/Pi.thy
--- a/Nominal/Ex/Pi.thy	Mon Jun 18 14:50:02 2012 +0100
+++ b/Nominal/Ex/Pi.thy	Thu Jul 12 10:11:32 2012 +0100
@@ -103,7 +103,7 @@
   assume "a \<noteq> z"
   thus ?thesis
     using assms
-    by(simp add: piMix_eq_iff Abs1_eq_iff fresh_permute_left)
+    by (simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
 qed
 
 lemma alphaInput_mix:
@@ -123,7 +123,7 @@
   assume "b \<noteq> z"
   thus ?thesis
     using assms
-    by(simp add: piMix_eq_iff Abs1_eq_iff fresh_permute_left)
+    by(simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
 qed
 
 lemma alphaRep_mix:
@@ -143,7 +143,7 @@
   assume "b \<noteq> z"
   thus ?thesis
     using assms
-    by(simp add: piMix_eq_iff Abs1_eq_iff fresh_permute_left)
+    by(simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
 qed
 
 subsection {* Capture-Avoiding Substitution of Names *}
@@ -393,7 +393,7 @@
   apply(simp add: finite_supp)
   apply(simp)
   apply(simp add: eqvt_at_def)
-  apply(drule_tac x="(atom b \<rightleftharpoons> atom ba)" in spec)
+  apply(drule_tac x="(b \<leftrightarrow> ba)" in spec)
   apply(simp)
   done
 
diff -r 1b7c034c9e9e -r 0440bc1a2438 Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Mon Jun 18 14:50:02 2012 +0100
+++ b/Nominal/Nominal2_Abs.thy	Thu Jul 12 10:11:32 2012 +0100
@@ -792,103 +792,175 @@
 section {* Abstractions of single atoms *}
 
 lemma Abs1_eq:
-  fixes x::"'a::fs"
-  shows "Abs_set {a} x = Abs_set {a} y \<longleftrightarrow> x = y"
-  and   "Abs_res {a} x = Abs_res {a} y \<longleftrightarrow> x = y"
-  and   "Abs_lst [c] x = Abs_lst [c] y \<longleftrightarrow> x = y"
+  fixes x y::"'a::fs"
+  shows "[{atom a}]set. x = [{atom a}]set. y \<longleftrightarrow> x = y"
+  and   "[{atom a}]res. x = [{atom a}]res. y \<longleftrightarrow> x = y"
+  and   "[[atom a]]lst. x = [[atom a]]lst. y \<longleftrightarrow> x = y"
 unfolding Abs_eq_iff2 alphas
 apply(simp_all add: supp_perm_singleton fresh_star_def fresh_zero_perm)
 apply(blast)+
 done
 
+lemma Abs1_eq_fresh:
+  fixes x y::"'a::fs"
+  and a b c::"'b::at"
+  assumes "atom c \<sharp> (a, b, x, y)"
+  shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y"
+  and   "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y"
+  and   "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y"
+proof -
+  have "[{atom a}]set. x = (a \<leftrightarrow> c) \<bullet> ([{atom a}]set. x)"
+    by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
+  then have "[{atom a}]set. x = [{atom c}]set. ((a \<leftrightarrow> c) \<bullet> x)" by simp
+  moreover 
+  have "[{atom b}]set. y = (b \<leftrightarrow> c) \<bullet> ([{atom b}]set. y)"
+    by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
+  then have "[{atom b}]set. y = [{atom c}]set. ((b \<leftrightarrow> c) \<bullet> y)" by simp
+  ultimately 
+  show "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y"
+    by (simp add: Abs1_eq)
+next
+  have "[{atom a}]res. x = (a \<leftrightarrow> c) \<bullet> ([{atom a}]res. x)"
+    by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
+  then have "[{atom a}]res. x = [{atom c}]res. ((a \<leftrightarrow> c) \<bullet> x)" by simp
+  moreover 
+  have "[{atom b}]res. y = (b \<leftrightarrow> c) \<bullet> ([{atom b}]res. y)"
+    by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
+  then have "[{atom b}]res. y = [{atom c}]res. ((b \<leftrightarrow> c) \<bullet> y)" by simp
+  ultimately 
+  show "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y"
+    by (simp add: Abs1_eq)
+next
+  have "[[atom a]]lst. x = (a \<leftrightarrow> c) \<bullet> ([[atom a]]lst. x)"
+    by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
+  then have "[[atom a]]lst. x = [[atom c]]lst. ((a \<leftrightarrow> c) \<bullet> x)" by simp
+  moreover 
+  have "[[atom b]]lst. y = (b \<leftrightarrow> c) \<bullet> ([[atom b]]lst. y)"
+    by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
+  then have "[[atom b]]lst. y = [[atom c]]lst. ((b \<leftrightarrow> c) \<bullet> y)" by simp
+  ultimately 
+  show "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y"
+    by (simp add: Abs1_eq)
+qed
+
+lemma Abs1_eq_all:
+  fixes x y::"'a::fs"
+  and z::"'c::fs"
+  and a b::"'b::at"
+  shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
+  and   "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
+  and   "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
+apply -
+apply(auto) 
+apply(simp add: Abs1_eq_fresh(1)[symmetric])
+apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
+apply(drule_tac x="aa" in spec)
+apply(simp)
+apply(subst Abs1_eq_fresh(1))
+apply(auto simp add: fresh_Pair)[1]
+apply(assumption)
+apply(simp add: Abs1_eq_fresh(2)[symmetric])
+apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
+apply(drule_tac x="aa" in spec)
+apply(simp)
+apply(subst Abs1_eq_fresh(2))
+apply(auto simp add: fresh_Pair)[1]
+apply(assumption)
+apply(simp add: Abs1_eq_fresh(3)[symmetric])
+apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
+apply(drule_tac x="aa" in spec)
+apply(simp)
+apply(subst Abs1_eq_fresh(3))
+apply(auto simp add: fresh_Pair)[1]
+apply(assumption)
+done
+
 lemma Abs1_eq_iff:
-  fixes x::"'a::fs"
-  assumes "sort_of a = sort_of b"
-  and     "sort_of c = sort_of d"
-  shows "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
-  and   "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
-  and   "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y)"
+  fixes x y::"'a::fs"
+  and a b::"'b::at"
+  shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)"
+  and   "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)"
+  and   "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)"
 proof -
   { assume "a = b"
-    then have "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)
+    then have "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)
   }
   moreover
-  { assume *: "a \<noteq> b" and **: "Abs_set {a} x = Abs_set {b} y"
-    have #: "a \<sharp> Abs_set {b} y" by (simp add: **[symmetric] Abs_fresh_iff)
-    have "Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_set {b} y)" by (simp add: permute_set_def assms)
-    also have "\<dots> = Abs_set {b} y"
-      by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
-    also have "\<dots> = Abs_set {a} x" using ** by simp
-    finally have "a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
+  { assume *: "a \<noteq> b" and **: "Abs_set {atom a} x = Abs_set {atom b} y"
+    have #: "atom a \<sharp> Abs_set {atom b} y" by (simp add: **[symmetric] Abs_fresh_iff)
+    have "Abs_set {atom a} ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> (Abs_set {atom b} y)" by (simp)
+    also have "\<dots> = Abs_set {atom b} y"
+      by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
+    also have "\<dots> = Abs_set {atom a} x" using ** by simp
+    finally have "a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
   }
   moreover 
-  { assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y"
-    have "Abs_set {a} x = Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp
-    also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_set {b} y" by (simp add: permute_set_def assms)
-    also have "\<dots> = Abs_set {b} y"
-      by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
-    finally have "Abs_set {a} x = Abs_set {b} y" .
+  { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y"
+    have "Abs_set {atom a} x = Abs_set {atom a} ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp
+    also have "\<dots> = (a \<leftrightarrow> b) \<bullet> Abs_set {atom b} y" by (simp add: permute_set_def assms)
+    also have "\<dots> = Abs_set {atom b} y"
+      by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
+    finally have "Abs_set {atom a} x = Abs_set {atom b} y" .
   }
   ultimately 
-  show "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
+  show "Abs_set {atom a} x = Abs_set {atom b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)"
     by blast
 next
   { assume "a = b"
-    then have "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)
+    then have "Abs_res {atom a} x = Abs_res {atom b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)
   }
   moreover
-  { assume *: "a \<noteq> b" and **: "Abs_res {a} x = Abs_res {b} y"
-    have #: "a \<sharp> Abs_res {b} y" by (simp add: **[symmetric] Abs_fresh_iff)
-    have "Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_res {b} y)" by (simp add: permute_set_def assms)
-    also have "\<dots> = Abs_res {b} y"
-      by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
-    also have "\<dots> = Abs_res {a} x" using ** by simp
-    finally have "a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
+  { assume *: "a \<noteq> b" and **: "Abs_res {atom a} x = Abs_res {atom b} y"
+    have #: "atom a \<sharp> Abs_res {atom b} y" by (simp add: **[symmetric] Abs_fresh_iff)
+    have "Abs_res {atom a} ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> (Abs_res {atom b} y)" by (simp add: assms)
+    also have "\<dots> = Abs_res {atom b} y"
+      by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
+    also have "\<dots> = Abs_res {atom a} x" using ** by simp
+    finally have "a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
   }
   moreover 
-  { assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y"
-    have "Abs_res {a} x = Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp
-    also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_res {b} y" by (simp add: permute_set_def assms)
-    also have "\<dots> = Abs_res {b} y"
-      by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
-    finally have "Abs_res {a} x = Abs_res {b} y" .
+  { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y"
+    have "Abs_res {atom a} x = Abs_res {atom a} ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp
+    also have "\<dots> = (a \<leftrightarrow> b) \<bullet> Abs_res {atom b} y" by (simp add: permute_set_def assms)
+    also have "\<dots> = Abs_res {atom b} y"
+      by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
+    finally have "Abs_res {atom a} x = Abs_res {atom b} y" .
   }
   ultimately 
-  show "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
+  show "Abs_res {atom a} x = Abs_res {atom b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)"
     by blast
 next
-  { assume "c = d"
-    then have "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y)" by (simp add: Abs1_eq)
+  { assume "a = b"
+    then have "Abs_lst [atom a] x = Abs_lst [atom b] y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)
   }
   moreover
-  { assume *: "c \<noteq> d" and **: "Abs_lst [c] x = Abs_lst [d] y"
-    have #: "c \<sharp> Abs_lst [d] y" by (simp add: **[symmetric] Abs_fresh_iff)
-    have "Abs_lst [c] ((c \<rightleftharpoons> d) \<bullet> y) = (c \<rightleftharpoons> d) \<bullet> (Abs_lst [d] y)" by (simp add: assms)
-    also have "\<dots> = Abs_lst [d] y"
-      by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
-    also have "\<dots> = Abs_lst [c] x" using ** by simp
-    finally have "c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
+  { assume *: "a \<noteq> b" and **: "Abs_lst [atom a] x = Abs_lst [atom b] y"
+    have #: "atom a \<sharp> Abs_lst [atom b] y" by (simp add: **[symmetric] Abs_fresh_iff)
+    have "Abs_lst [atom a] ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> (Abs_lst [atom b] y)" by (simp add: assms)
+    also have "\<dots> = Abs_lst [atom b] y"
+      by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
+    also have "\<dots> = Abs_lst [atom a] x" using ** by simp
+    finally have "a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
   }
   moreover 
-  { assume *: "c \<noteq> d" and **: "x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y"
-    have "Abs_lst [c] x = Abs_lst [c] ((c \<rightleftharpoons> d) \<bullet> y)" using ** by simp
-    also have "\<dots> = (c \<rightleftharpoons> d) \<bullet> Abs_lst [d] y" by (simp add: assms)
-    also have "\<dots> = Abs_lst [d] y"
-      by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
-    finally have "Abs_lst [c] x = Abs_lst [d] y" .
+  { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y"
+    have "Abs_lst [atom a] x = Abs_lst [atom a] ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp
+    also have "\<dots> = (a \<leftrightarrow> b) \<bullet> Abs_lst [atom b] y" by (simp add: assms)
+    also have "\<dots> = Abs_lst [atom b] y"
+      by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
+    finally have "Abs_lst [atom a] x = Abs_lst [atom b] y" .
   }
   ultimately 
-  show "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y)"
+  show "Abs_lst [atom a] x = Abs_lst [atom b] y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)"
     by blast
 qed
 
 lemma Abs1_eq_iff':
   fixes x::"'a::fs"
-  assumes "sort_of a = sort_of b"
-  and     "sort_of c = sort_of d"
-  shows "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<rightleftharpoons> a) \<bullet> x = y \<and> b \<sharp> x)"
-  and   "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<rightleftharpoons> a) \<bullet> x = y \<and> b \<sharp> x)"
-  and   "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> (d \<rightleftharpoons> c) \<bullet> x = y \<and> d \<sharp> x)"
+  and a b::"'b::at"
+  shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
+  and   "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
+  and   "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
 using assms by (auto simp add: Abs1_eq_iff fresh_permute_left)
 
 
diff -r 1b7c034c9e9e -r 0440bc1a2438 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Mon Jun 18 14:50:02 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Thu Jul 12 10:11:32 2012 +0100
@@ -3054,6 +3054,12 @@
 where
   "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)"
 
+lemma flip_fresh_fresh:
+  assumes "atom a \<sharp> x" "atom b \<sharp> x"
+  shows "(a \<leftrightarrow> b) \<bullet> x = x"
+using assms
+by (simp add: flip_def swap_fresh_fresh)
+
 lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0"
   unfolding flip_def by (rule swap_self)
 
@@ -3073,7 +3079,6 @@
   by (simp add: flip_commute)
 
 lemma flip_eqvt [eqvt]: 
-  fixes a b c::"'a::at_base"
   shows "p \<bullet> (a \<leftrightarrow> b) = (p \<bullet> a \<leftrightarrow> p \<bullet> b)"
   unfolding flip_def
   by (simp add: swap_eqvt atom_eqvt)
@@ -3091,6 +3096,13 @@
 text {* the following two lemmas do not hold for at_base, 
   only for single sort atoms from at *}
 
+lemma flip_triple:
+  fixes a b c::"'a::at"
+  assumes "a \<noteq> b" and "c \<noteq> b"
+  shows "(a \<leftrightarrow> c) + (b \<leftrightarrow> c) + (a \<leftrightarrow> c) = (a \<leftrightarrow> b)"
+  unfolding flip_def
+  by (rule swap_triple) (simp_all add: assms)
+
 lemma permute_flip_at:
   fixes a b c::"'a::at"
   shows "(a \<leftrightarrow> b) \<bullet> c = (if c = a then b else if c = b then a else c)"
@@ -3106,14 +3118,6 @@
   and   "(a \<leftrightarrow> b) \<bullet> b = a"
   unfolding permute_flip_at by simp_all
 
-lemma flip_fresh_fresh:
-  fixes a b::"'a::at_base"
-  assumes "atom a \<sharp> x" "atom b \<sharp> x"
-  shows "(a \<leftrightarrow> b) \<bullet> x = x"
-using assms
-by (simp add: flip_def swap_fresh_fresh)
-
-
 
 subsection {* Syntax for coercing at-elements to the atom-type *}
 
diff -r 1b7c034c9e9e -r 0440bc1a2438 Nominal/Nominal2_FCB.thy
--- a/Nominal/Nominal2_FCB.thy	Mon Jun 18 14:50:02 2012 +0100
+++ b/Nominal/Nominal2_FCB.thy	Thu Jul 12 10:11:32 2012 +0100
@@ -22,26 +22,25 @@
 
 
 lemma Abs_lst1_fcb:
-  fixes x y :: "'a :: at_base"
+  fixes x y :: "'a :: at"
     and S T :: "'b :: fs"
-  assumes e: "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)"
-  and f1: "\<lbrakk>x \<noteq> y; atom y \<sharp> T; atom x \<sharp> (atom y \<rightleftharpoons> atom x) \<bullet> T\<rbrakk> \<Longrightarrow> atom x \<sharp> f x T"
-  and f2: "\<lbrakk>x \<noteq> y; atom y \<sharp> T; atom x \<sharp> (atom y \<rightleftharpoons> atom x) \<bullet> T\<rbrakk> \<Longrightarrow> atom y \<sharp> f x T"
-  and p: "\<lbrakk>S = (atom x \<rightleftharpoons> atom y) \<bullet> T; x \<noteq> y; atom y \<sharp> T; atom x \<sharp> S\<rbrakk> 
-    \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> (f x T) = f y S"
-  and s: "sort_of (atom x) = sort_of (atom y)"
+  assumes e: "[[atom x]]lst. T = [[atom y]]lst. S"
+  and f1: "\<lbrakk>x \<noteq> y; atom y \<sharp> T; atom x \<sharp> (y \<leftrightarrow> x) \<bullet> T\<rbrakk> \<Longrightarrow> atom x \<sharp> f x T"
+  and f2: "\<lbrakk>x \<noteq> y; atom y \<sharp> T; atom x \<sharp> (y \<leftrightarrow> x) \<bullet> T\<rbrakk> \<Longrightarrow> atom y \<sharp> f x T"
+  and p: "\<lbrakk>S = (x \<leftrightarrow> y) \<bullet> T; x \<noteq> y; atom y \<sharp> T; atom x \<sharp> S\<rbrakk> 
+    \<Longrightarrow> (x \<leftrightarrow> y) \<bullet> (f x T) = f y S"
   shows "f x T = f y S"
   using e
   apply(case_tac "atom x \<sharp> S")
-  apply(simp add: Abs1_eq_iff'[OF s s])
+  apply(simp add: Abs1_eq_iff')
   apply(elim conjE disjE)
   apply(simp)
   apply(rule trans)
-  apply(rule_tac p="(atom x \<rightleftharpoons> atom y)" in supp_perm_eq[symmetric])
+  apply(rule_tac p="(x \<leftrightarrow> y)" in supp_perm_eq[symmetric])
   apply(rule fresh_star_supp_conv)
-  apply(simp add: supp_swap fresh_star_def s f1 f2)
-  apply(simp add: swap_commute p)
-  apply(simp add: Abs1_eq_iff[OF s s])
+  apply(simp add: flip_def supp_swap fresh_star_def f1 f2)
+  apply(simp add: flip_commute p)
+  apply(simp add: Abs1_eq_iff)
   done
 
 lemma Abs_lst_fcb:
@@ -383,7 +382,7 @@
   fixes a b :: "atom"
     and x y :: "'b :: fs"
     and c::"'c :: fs"
-  assumes e: "(Abs_lst [a] x) = (Abs_lst [b] y)"
+  assumes e: "[[a]]lst. x = [[b]]lst. y"
   and fcb1: "a \<sharp> f a x c"
   and fresh: "{a, b} \<sharp>* c"
   and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c"
@@ -400,7 +399,7 @@
   fixes a b :: "'a::at"
     and x y :: "'b :: fs"
     and c::"'c :: fs"
-  assumes e: "(Abs_lst [atom a] x) = (Abs_lst [atom b] y)"
+  assumes e: "[[atom a]]lst. x = [[atom b]]lst. y"
   and fcb1: "atom a \<sharp> f a x c"
   and fresh: "{atom a, atom b} \<sharp>* c"
   and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c"