diff -r d959bc9c800c -r a190b2b79cc8 Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Wed Nov 30 14:58:19 2011 +0000
+++ b/Nominal/Nominal2_Abs.thy	Mon Dec 05 15:34:12 2011 +0000
@@ -451,6 +451,10 @@
 apply(auto simp add: alphas_abs)[1]
 done
 
+lemma alpha_res_alpha_set:
+  "(bs, x) \<approx>res op = supp p (cs, y) \<longleftrightarrow> (bs \<inter> supp x, x) \<approx>set op = supp p (cs \<inter> supp y, y)"
+  using alpha_abs_set_abs_res alpha_abs_res_abs_set by blast
+
 section {* Quotient types *}
 
 quotient_type 
@@ -497,38 +501,34 @@
   by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
 
 lemma Abs_eq_iff:
-  shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y))"
-  and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
-  and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
+  shows "[bs]set. x = [bs']set. y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (bs', y))"
+  and   "[bs]res. x = [bs']res. y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (bs', y))"
+  and   "[cs]lst. x = [cs']lst. y \<longleftrightarrow> (\<exists>p. (cs, x) \<approx>lst (op =) supp p (cs', y))"
   by (lifting alphas_abs)
 
 lemma Abs_eq_iff2:
-  shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y) \<and> supp p \<subseteq> bs \<union> cs)"
-  and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y) \<and> supp p \<subseteq> bs \<union> cs)"
-  and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> 
-    (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y) \<and> supp p \<subseteq> set bsl \<union> set csl)"
+  shows "[bs]set. x = [bs']set. y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op=) supp p (bs', y) \<and> supp p \<subseteq> bs \<union> bs')"
+  and   "[bs]res. x = [bs']res. y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op=) supp p (bs', y) \<and> supp p \<subseteq> bs \<union> bs')"
+  and   "[cs]lst. x = [cs']lst. y \<longleftrightarrow> (\<exists>p. (cs, x) \<approx>lst (op=) supp p (cs', y) \<and> supp p \<subseteq> set cs \<union> set cs')"
   by (lifting alphas_abs_stronger)
 
-lemma alpha_res_alpha_set:
-  "(bs, x) \<approx>res op = supp p (cs, y) \<longleftrightarrow> (bs \<inter> supp x, x) \<approx>set op = supp p (cs \<inter> supp y, y)"
-  using alpha_abs_set_abs_res alpha_abs_res_abs_set by blast
 
 lemma Abs_eq_res_set:
-  "(([bs]res. x) = ([cs]res. y)) = (([(bs \<inter> supp x)]set. x) = ([(cs \<inter> supp y)]set. y))"
+  shows "[bs]res. x = [cs]res. y \<longleftrightarrow> [bs \<inter> supp x]set. x = [cs \<inter> supp y]set. y"
   unfolding Abs_eq_iff alpha_res_alpha_set by rule
 
 lemma Abs_eq_res_supp:
   assumes asm: "supp x \<subseteq> bs"
-  shows "([as]res. x) = ([as \<inter> bs]res. x)"
+  shows "[as]res. x = [as \<inter> bs]res. x"
   unfolding Abs_eq_iff alphas
   apply (rule_tac x="0::perm" in exI)
   apply (simp add: fresh_star_zero)
   using asm by blast
 
 lemma Abs_exhausts:
-  shows "(\<And>as (x::'a::pt). y1 = Abs_set as x \<Longrightarrow> P1) \<Longrightarrow> P1"
-  and   "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2"
-  and   "(\<And>as (x::'a::pt). y3 = Abs_lst as x \<Longrightarrow> P3) \<Longrightarrow> P3"
+  shows "(\<And>as (x::'a::pt). y1 = [as]set. x \<Longrightarrow> P1) \<Longrightarrow> P1"
+  and   "(\<And>as (x::'a::pt). y2 = [as]res. x \<Longrightarrow> P2) \<Longrightarrow> P2"
+  and   "(\<And>bs (x::'a::pt). y3 = [bs]lst. x \<Longrightarrow> P3) \<Longrightarrow> P3"
   by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"]
               prod.exhaust[where 'a="atom set" and 'b="'a"]
               prod.exhaust[where 'a="atom list" and 'b="'a"])
@@ -544,7 +544,7 @@
 
 lemma permute_Abs_set[simp]:
   fixes x::"'a::pt"  
-  shows "(p \<bullet> (Abs_set as x)) = Abs_set (p \<bullet> as) (p \<bullet> x)"
+  shows "(p \<bullet> ([as]set. x)) = [p \<bullet> as]set. (p \<bullet> x)"
   by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
 
 instance
@@ -565,7 +565,7 @@
 
 lemma permute_Abs_res[simp]:
   fixes x::"'a::pt"  
-  shows "(p \<bullet> (Abs_res as x)) = Abs_res (p \<bullet> as) (p \<bullet> x)"
+  shows "(p \<bullet> ([as]res. x)) = [p \<bullet> as]res. (p \<bullet> x)"
   by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
 
 instance
@@ -586,7 +586,7 @@
 
 lemma permute_Abs_lst[simp]:
   fixes x::"'a::pt"  
-  shows "(p \<bullet> (Abs_lst as x)) = Abs_lst (p \<bullet> as) (p \<bullet> x)"
+  shows "(p \<bullet> ([as]lst. x)) = [p \<bullet> as]lst. (p \<bullet> x)"
   by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"])
 
 instance
@@ -603,8 +603,8 @@
 lemma Abs_swap1:
   assumes a1: "a \<notin> (supp x) - bs"
   and     a2: "b \<notin> (supp x) - bs"
-  shows "Abs_set bs x = Abs_set ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
-  and   "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
+  shows "[bs]set. x = [(a \<rightleftharpoons> b) \<bullet> bs]set. ((a \<rightleftharpoons> b) \<bullet> x)"
+  and   "[bs]res. x = [(a \<rightleftharpoons> b) \<bullet> bs]res. ((a \<rightleftharpoons> b) \<bullet> x)"
   unfolding Abs_eq_iff
   unfolding alphas
   unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] 
@@ -617,7 +617,7 @@
 lemma Abs_swap2:
   assumes a1: "a \<notin> (supp x) - (set bs)"
   and     a2: "b \<notin> (supp x) - (set bs)"
-  shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
+  shows "[bs]lst. x = [(a \<rightleftharpoons> b) \<bullet> bs]lst. ((a \<rightleftharpoons> b) \<bullet> x)"
   unfolding Abs_eq_iff
   unfolding alphas
   unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric]
@@ -628,9 +628,9 @@
      (auto simp add: supp_perm swap_atom)
 
 lemma Abs_supports:
-  shows "((supp x) - as) supports (Abs_set as x)"
-  and   "((supp x) - as) supports (Abs_res as x)"
-  and   "((supp x) - set bs) supports (Abs_lst bs x)"
+  shows "((supp x) - as) supports ([as]set. x)"
+  and   "((supp x) - as) supports ([as]res. x)"
+  and   "((supp x) - set bs) supports ([bs]lst. x)"
   unfolding supports_def
   unfolding permute_Abs
   by (simp_all add: Abs_swap1[symmetric] Abs_swap2[symmetric])
@@ -638,26 +638,26 @@
 function
   supp_set  :: "('a::pt) abs_set \<Rightarrow> atom set"
 where
-  "supp_set (Abs_set as x) = supp x - as"
+  "supp_set ([as]set. x) = supp x - as"
 apply(case_tac x rule: Abs_exhausts(1))
 apply(simp)
 apply(simp add: Abs_eq_iff alphas_abs alphas)
 done
 
 termination supp_set 
-  by (auto intro!: local.termination)
+  by lexicographic_order
 
 function
   supp_res :: "('a::pt) abs_res \<Rightarrow> atom set"
 where
-  "supp_res (Abs_res as x) = supp x - as"
+  "supp_res ([as]res. x) = supp x - as"
 apply(case_tac x rule: Abs_exhausts(2))
 apply(simp)
 apply(simp add: Abs_eq_iff alphas_abs alphas)
 done
 
 termination supp_res 
-  by (auto intro!: local.termination)
+  by lexicographic_order
 
 function
   supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set"
@@ -668,8 +668,8 @@
 apply(simp add: Abs_eq_iff alphas_abs alphas)
 done
 
-termination supp_lst 
-  by (auto intro!: local.termination)
+termination supp_lst
+  by lexicographic_order
 
 lemma supp_funs_eqvt[eqvt]:
   shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)"
@@ -684,44 +684,43 @@
   done
 
 lemma Abs_fresh_aux:
-  shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_set (Abs bs x)"
-  and   "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"
-  and   "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)"
+  shows "a \<sharp> [bs]set. x \<Longrightarrow> a \<sharp> supp_set ([bs]set. x)"
+  and   "a \<sharp> [bs]res. x \<Longrightarrow> a \<sharp> supp_res ([bs]res. x)"
+  and   "a \<sharp> [cs]lst. x \<Longrightarrow> a \<sharp> supp_lst ([cs]lst. x)"
   by (rule_tac [!] fresh_fun_eqvt_app)
      (auto simp only: eqvt_def eqvts_raw)
 
 lemma Abs_supp_subset1:
   assumes a: "finite (supp x)"
-  shows "(supp x) - as \<subseteq> supp (Abs_set as x)"
-  and   "(supp x) - as \<subseteq> supp (Abs_res as x)"
-  and   "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)"
+  shows "(supp x) - as \<subseteq> supp ([as]set. x)"
+  and   "(supp x) - as \<subseteq> supp ([as]res. x)"
+  and   "(supp x) - (set bs) \<subseteq> supp ([bs]lst. x)"
   unfolding supp_conv_fresh
   by (auto dest!: Abs_fresh_aux)
      (simp_all add: fresh_def supp_finite_atom_set a)
 
 lemma Abs_supp_subset2:
   assumes a: "finite (supp x)"
-  shows "supp (Abs_set as x) \<subseteq> (supp x) - as"
-  and   "supp (Abs_res as x) \<subseteq> (supp x) - as"
-  and   "supp (Abs_lst bs x) \<subseteq> (supp x) - (set bs)"
+  shows "supp ([as]set. x) \<subseteq> (supp x) - as"
+  and   "supp ([as]res. x) \<subseteq> (supp x) - as"
+  and   "supp ([bs]lst. x) \<subseteq> (supp x) - (set bs)"
   by (rule_tac [!] supp_is_subset)
      (simp_all add: Abs_supports a)
 
 lemma Abs_finite_supp:
   assumes a: "finite (supp x)"
-  shows "supp (Abs_set as x) = (supp x) - as"
-  and   "supp (Abs_res as x) = (supp x) - as"
-  and   "supp (Abs_lst bs x) = (supp x) - (set bs)"
-  by (rule_tac [!] subset_antisym)
-     (simp_all add: Abs_supp_subset1[OF a] Abs_supp_subset2[OF a])
+  shows "supp ([as]set. x) = (supp x) - as"
+  and   "supp ([as]res. x) = (supp x) - as"
+  and   "supp ([bs]lst. x) = (supp x) - (set bs)"
+using Abs_supp_subset1[OF a] Abs_supp_subset2[OF a]
+  by blast+
 
 lemma supp_Abs:
   fixes x::"'a::fs"
-  shows "supp (Abs_set as x) = (supp x) - as"
-  and   "supp (Abs_res as x) = (supp x) - as"
-  and   "supp (Abs_lst bs x) = (supp x) - (set bs)"
-  by (rule_tac [!] Abs_finite_supp)
-     (simp_all add: finite_supp)
+  shows "supp ([as]set. x) = (supp x) - as"
+  and   "supp ([as]res. x) = (supp x) - as"
+  and   "supp ([bs]lst. x) = (supp x) - (set bs)"
+by (simp_all add: Abs_finite_supp finite_supp)
 
 instance abs_set :: (fs) fs
   apply(default)
@@ -743,38 +742,40 @@
 
 lemma Abs_fresh_iff:
   fixes x::"'a::fs"
-  shows "a \<sharp> Abs_set bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
-  and   "a \<sharp> Abs_res bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
-  and   "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)"
+  shows "a \<sharp> [bs]set. x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
+  and   "a \<sharp> [bs]res. x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
+  and   "a \<sharp> [cs]lst. x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)"
   unfolding fresh_def
   unfolding supp_Abs
   by auto
 
 lemma Abs_fresh_star_iff:
   fixes x::"'a::fs"
-  shows "as \<sharp>* Abs_set bs x \<longleftrightarrow> (as - bs) \<sharp>* x"
-  and   "as \<sharp>* Abs_res bs x \<longleftrightarrow> (as - bs) \<sharp>* x"
-  and   "as \<sharp>* Abs_lst cs x \<longleftrightarrow> (as - set cs) \<sharp>* x"
+  shows "as \<sharp>* ([bs]set. x) \<longleftrightarrow> (as - bs) \<sharp>* x"
+  and   "as \<sharp>* ([bs]res. x) \<longleftrightarrow> (as - bs) \<sharp>* x"
+  and   "as \<sharp>* ([cs]lst. x) \<longleftrightarrow> (as - set cs) \<sharp>* x"
   unfolding fresh_star_def
   by (auto simp add: Abs_fresh_iff)
 
 lemma Abs_fresh_star:
   fixes x::"'a::fs"
-  shows "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_set as' x"
-  and   "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_res as' x"
-  and   "bs \<subseteq> set bs' \<Longrightarrow> bs \<sharp>* Abs_lst bs' x"
+  shows "as \<subseteq> as' \<Longrightarrow> as \<sharp>* ([as']set. x)"
+  and   "as \<subseteq> as' \<Longrightarrow> as \<sharp>* ([as']res. x)"
+  and   "bs \<subseteq> set bs' \<Longrightarrow> bs \<sharp>* ([bs']lst. x)"
   unfolding fresh_star_def
   by(auto simp add: Abs_fresh_iff)
 
 lemma Abs_fresh_star2:
   fixes x::"'a::fs"
-  shows "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* Abs_set bs x \<longleftrightarrow> as \<sharp>* x"
-  and   "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* Abs_res bs x \<longleftrightarrow> as \<sharp>* x"
-  and   "cs \<inter> set ds = {} \<Longrightarrow> cs \<sharp>* Abs_lst ds x \<longleftrightarrow> cs \<sharp>* x"
+  shows "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* ([bs]set. x) \<longleftrightarrow> as \<sharp>* x"
+  and   "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* ([bs]res. x) \<longleftrightarrow> as \<sharp>* x"
+  and   "cs \<inter> set ds = {} \<Longrightarrow> cs \<sharp>* ([ds]lst. x) \<longleftrightarrow> cs \<sharp>* x"
   unfolding fresh_star_def Abs_fresh_iff
   by auto
 
 
+section {* Abstractions of single atoms *}
+
 lemma Abs1_eq:
   fixes x::"'a::fs"
   shows "Abs_set {a} x = Abs_set {a} y \<longleftrightarrow> x = y"
@@ -886,7 +887,7 @@
   and     b: "finite bs"
   shows "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 proof -
-  from b set_renaming_perm 
+  from set_renaming_perm2 
   obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast
   have ***: "q \<bullet> bs = p \<bullet> bs" using b * by (induct) (simp add: permute_set_eq, simp add: insert_eqvt)
   have "[bs]set. x =  q \<bullet> ([bs]set. x)"
@@ -906,7 +907,7 @@
   and     b: "finite bs"
   shows "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 proof -
-  from b set_renaming_perm 
+  from set_renaming_perm2 
   obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast
   have ***: "q \<bullet> bs = p \<bullet> bs" using b * by (induct) (simp add: permute_set_eq, simp add: insert_eqvt)
   have "[bs]res. x =  q \<bullet> ([bs]res. x)"
@@ -925,7 +926,7 @@
   assumes a: "(p \<bullet> (set bs)) \<sharp>* x" 
   shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 proof -
-  from a list_renaming_perm 
+  from list_renaming_perm 
   obtain q where *: "\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by blast
   have ***: "q \<bullet> bs = p \<bullet> bs" using * by (induct bs) (simp_all add: insert_eqvt)
   have "[bs]lst. x =  q \<bullet> ([bs]lst. x)"