--- a/Nominal/Nominal2_Abs.thy	Wed Jan 19 07:06:47 2011 +0100
+++ b/Nominal/Nominal2_Abs.thy	Wed Jan 19 17:11:10 2011 +0100
@@ -491,6 +491,7 @@
               prod.exhaust[where 'a="atom set" and 'b="'a"]
               prod.exhaust[where 'a="atom list" and 'b="'a"])
 
+
 instantiation abs_set :: (pt) pt
 begin
 
@@ -723,6 +724,101 @@
   unfolding fresh_star_def
   by(auto simp add: Abs_fresh_iff)
 
+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"
+unfolding Abs_eq_iff2 alphas
+apply(simp_all add: supp_perm_singleton fresh_star_def fresh_zero_perm)
+apply(blast)+
+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)"
+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)
+  }
+  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_eq 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)
+  }
+  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_eq 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" .
+  }
+  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)"
+    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)
+  }
+  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_eq 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)
+  }
+  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_eq 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" .
+  }
+  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)"
+    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)
+  }
+  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)
+  }
+  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" .
+  }
+  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)"
+    by blast
+qed
+
 
 subsection {* Renaming of bodies of abstractions *}