diff -r 320775fa47ca -r d0961e6d6881 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Mon Sep 27 04:56:28 2010 -0400
+++ b/Nominal/Abs.thy	Mon Sep 27 04:56:49 2010 -0400
@@ -293,7 +293,13 @@
   unfolding fun_rel_def
   by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
 
-lemma abs_exhausts:
+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))"
+  by (lifting alphas_abs)
+
+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"
@@ -301,12 +307,6 @@
               prod.exhaust[where 'a="atom set" and 'b="'a"]
               prod.exhaust[where 'a="atom list" and 'b="'a"])
 
-lemma abs_eq_iff:
-  shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (bs, x) \<approx>abs_set (cs, y)"
-  and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)"
-  and   "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)"
-  unfolding alphas_abs by (lifting alphas_abs)
-
 instantiation abs_set :: (pt) pt
 begin
 
@@ -315,14 +315,14 @@
 is
   "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
 
-lemma permute_Abs[simp]:
+lemma permute_Abs_set[simp]:
   fixes x::"'a::pt"  
   shows "(p \<bullet> (Abs_set as x)) = Abs_set (p \<bullet> as) (p \<bullet> x)"
   by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
 
 instance
   apply(default)
-  apply(case_tac [!] x rule: abs_exhausts(1))
+  apply(case_tac [!] x rule: Abs_exhausts(1))
   apply(simp_all)
   done
 
@@ -343,7 +343,7 @@
 
 instance
   apply(default)
-  apply(case_tac [!] x rule: abs_exhausts(2))
+  apply(case_tac [!] x rule: Abs_exhausts(2))
   apply(simp_all)
   done
 
@@ -364,22 +364,21 @@
 
 instance
   apply(default)
-  apply(case_tac [!] x rule: abs_exhausts(3))
+  apply(case_tac [!] x rule: Abs_exhausts(3))
   apply(simp_all)
   done
 
 end
 
-lemmas permute_abs[eqvt] = permute_Abs permute_Abs_res permute_Abs_lst
+lemmas permute_Abs[eqvt] = permute_Abs_set permute_Abs_res permute_Abs_lst
 
 
-lemma abs_swap1:
+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)"
-  unfolding abs_eq_iff
-  unfolding alphas_abs
+  unfolding Abs_eq_iff
   unfolding alphas
   unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] 
   unfolding fresh_star_def fresh_def
@@ -388,12 +387,11 @@
   by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
      (auto simp add: supp_perm swap_atom)
 
-lemma abs_swap2:
+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)"
-  unfolding abs_eq_iff
-  unfolding alphas_abs
+  unfolding Abs_eq_iff
   unfolding alphas
   unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric]
   unfolding fresh_star_def fresh_def
@@ -402,21 +400,21 @@
   by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
      (auto simp add: supp_perm swap_atom)
 
-lemma abs_supports:
+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)"
   unfolding supports_def
-  unfolding permute_abs
-  by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
+  unfolding permute_Abs
+  by (simp_all add: Abs_swap1[symmetric] Abs_swap2[symmetric])
 
 function
   supp_set  :: "('a::pt) abs_set \<Rightarrow> atom set"
 where
   "supp_set (Abs_set as x) = supp x - as"
-apply(case_tac x rule: abs_exhausts(1))
+apply(case_tac x rule: Abs_exhausts(1))
 apply(simp)
-apply(simp add: abs_eq_iff alphas_abs alphas)
+apply(simp add: Abs_eq_iff alphas_abs alphas)
 done
 
 termination supp_set 
@@ -426,9 +424,9 @@
   supp_res :: "('a::pt) abs_res \<Rightarrow> atom set"
 where
   "supp_res (Abs_res as x) = supp x - as"
-apply(case_tac x rule: abs_exhausts(2))
+apply(case_tac x rule: Abs_exhausts(2))
 apply(simp)
-apply(simp add: abs_eq_iff alphas_abs alphas)
+apply(simp add: Abs_eq_iff alphas_abs alphas)
 done
 
 termination supp_res 
@@ -438,9 +436,9 @@
   supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set"
 where
   "supp_lst (Abs_lst cs x) = (supp x) - (set cs)"
-apply(case_tac x rule: abs_exhausts(3))
+apply(case_tac x rule: Abs_exhausts(3))
 apply(simp)
-apply(simp add: abs_eq_iff alphas_abs alphas)
+apply(simp add: Abs_eq_iff alphas_abs alphas)
 done
 
 termination supp_lst 
@@ -450,86 +448,88 @@
   shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)"
   and   "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)"
   and   "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)"
-  apply(case_tac x rule: abs_exhausts(1))
+  apply(case_tac x rule: Abs_exhausts(1))
   apply(simp add: supp_eqvt Diff_eqvt)
-  apply(case_tac y rule: abs_exhausts(2))
+  apply(case_tac y rule: Abs_exhausts(2))
   apply(simp add: supp_eqvt Diff_eqvt)
-  apply(case_tac z rule: abs_exhausts(3))
+  apply(case_tac z rule: Abs_exhausts(3))
   apply(simp add: supp_eqvt Diff_eqvt set_eqvt)
   done
 
-lemma aux_fresh:
+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)"
   by (rule_tac [!] fresh_fun_eqvt_app)
      (simp_all only: eqvts_raw)
 
-lemma supp_abs_subset1:
+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)"
   unfolding supp_conv_fresh
-  by (auto dest!: aux_fresh)
+  by (auto dest!: Abs_fresh_aux)
      (simp_all add: fresh_def supp_finite_atom_set a)
 
-lemma supp_abs_subset2:
+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)"
   by (rule_tac [!] supp_is_subset)
-     (simp_all add: abs_supports a)
+     (simp_all add: Abs_supports a)
 
-lemma abs_finite_supp:
+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: supp_abs_subset1[OF a] supp_abs_subset2[OF a])
+     (simp_all add: Abs_supp_subset1[OF a] Abs_supp_subset2[OF a])
 
-lemma supp_abs:
+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)
+  by (rule_tac [!] Abs_finite_supp)
      (simp_all add: finite_supp)
 
 instance abs_set :: (fs) fs
   apply(default)
-  apply(case_tac x rule: abs_exhausts(1))
-  apply(simp add: supp_abs finite_supp)
+  apply(case_tac x rule: Abs_exhausts(1))
+  apply(simp add: supp_Abs finite_supp)
   done
 
 instance abs_res :: (fs) fs
   apply(default)
-  apply(case_tac x rule: abs_exhausts(2))
-  apply(simp add: supp_abs finite_supp)
+  apply(case_tac x rule: Abs_exhausts(2))
+  apply(simp add: supp_Abs finite_supp)
   done
 
 instance abs_lst :: (fs) fs
   apply(default)
-  apply(case_tac x rule: abs_exhausts(3))
-  apply(simp add: supp_abs finite_supp)
+  apply(case_tac x rule: Abs_exhausts(3))
+  apply(simp add: supp_Abs finite_supp)
   done
 
-lemma abs_fresh_iff:
+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)"
   unfolding fresh_def
-  unfolding supp_abs
+  unfolding supp_Abs
   by auto
 
-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))"
-  by (lifting alphas_abs)
+lemma Abs_fresh_star:
+  fixes x::"'a::fs"
+  shows "as \<sharp>* Abs_set as x"
+  and   "as \<sharp>* Abs_res as x"
+  and   "set bs \<sharp>* Abs_lst bs x"
+  unfolding fresh_star_def
+  by(simp_all add: Abs_fresh_iff)
 
 
 section {* Infrastructure for building tuples of relations and functions *}