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)