diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal/Abs.thy	Mon Apr 26 10:01:13 2010 +0200
@@ -2,8 +2,8 @@
 imports "../Nominal-General/Nominal2_Atoms" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal-General/Nominal2_Supp" 
-        "Nominal2_FSet"
         "Quotient" 
+        "Quotient_List"
         "Quotient_Product" 
 begin
 
@@ -129,16 +129,22 @@
   by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
 
 quotient_definition
+  Abs ("[_]set. _" [60, 60] 60)
+where
   "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_gen"
 is
   "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
 
 quotient_definition
+  Abs_res ("[_]res. _" [60, 60] 60)
+where
   "Abs_res::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_res"
 is
   "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
 
 quotient_definition
+  Abs_lst ("[_]lst. _" [60, 60] 60)
+where
   "Abs_lst::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_lst"
 is
   "Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)"
@@ -169,9 +175,8 @@
   shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (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)"
-  apply(simp_all add: alphas_abs)
-  apply(lifting alphas_abs)
-  done
+  unfolding alphas_abs
+  by (lifting alphas_abs)
 
 instantiation abs_gen :: (pt) pt
 begin
@@ -327,9 +332,8 @@
   shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_gen (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)"
-  apply(rule_tac [!] fresh_fun_eqvt_app)
-  apply(simp_all add: eqvts_raw)
-  done
+  by (rule_tac [!] fresh_fun_eqvt_app)
+     (simp_all add: eqvts_raw)
 
 lemma supp_abs_subset1:
   assumes a: "finite (supp x)"
@@ -337,36 +341,32 @@
   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
-  apply(auto dest!: aux_fresh)
-  apply(simp_all add: fresh_def supp_finite_atom_set a)
-  done
+  by (auto dest!: aux_fresh)
+     (simp_all add: fresh_def supp_finite_atom_set a)
 
 lemma supp_abs_subset2:
   assumes a: "finite (supp x)"
   shows "supp (Abs 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)"
-  apply(rule_tac [!] supp_is_subset)
-  apply(simp_all add: abs_supports a)
-  done
+  by (rule_tac [!] supp_is_subset)
+     (simp_all add: abs_supports a)
 
 lemma abs_finite_supp:
   assumes a: "finite (supp x)"
   shows "supp (Abs as x) = (supp x) - as"
   and   "supp (Abs_res as x) = (supp x) - as"
   and   "supp (Abs_lst bs x) = (supp x) - (set bs)"
-  apply(rule_tac [!] subset_antisym)
-  apply(simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a])
-  done
+  by (rule_tac [!] subset_antisym)
+     (simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a])
 
 lemma supp_abs:
   fixes x::"'a::fs"
   shows "supp (Abs as x) = (supp x) - as"
   and   "supp (Abs_res as x) = (supp x) - as"
   and   "supp (Abs_lst bs x) = (supp x) - (set bs)"
-  apply(rule_tac [!] abs_finite_supp)
-  apply(simp_all add: finite_supp)
-  done
+  by (rule_tac [!] abs_finite_supp)
+     (simp_all add: finite_supp)
 
 instance abs_gen :: (fs) fs
   apply(default)
@@ -397,101 +397,12 @@
 
 section {* BELOW is stuff that may or may not be needed *}
 
-lemma 
-  fixes t1 s1::"'a::fs"
-  and   t2 s2::"'b::fs"
-  shows "Abs as (t1, t2) = Abs as (s1, s2) \<longrightarrow> (Abs as t1 = Abs as s1 \<and>  Abs as t2 = Abs as s2)"
-apply(subst abs_eq_iff)
-apply(subst alphas_abs)
-apply(subst alphas)
-apply(rule impI)
-apply(erule exE)
-apply(simp add: supp_Pair)
-apply(simp add: Un_Diff)
-apply(simp add: fresh_star_union)
-apply(erule conjE)+
-apply(rule conjI)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="p" in supp_perm_eq)
-apply(simp add: supp_abs)
-apply(simp)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="p" in supp_perm_eq)
-apply(simp add: supp_abs)
-apply(simp)
-done
-
-lemma 
-  fixes t1 s1::"'a::fs"
-  and   t2 s2::"'b::fs"
-  shows "Abs as (t1, t2) = Abs bs (s1, s2) \<longrightarrow> (Abs as t1 = Abs bs s1 \<and>  Abs as t2 = Abs bs s2)"
-apply(subst abs_eq_iff)
-apply(subst alphas_abs)
-apply(subst alphas)
-apply(rule impI)
-apply(erule exE)
-apply(simp add: supp_Pair)
-apply(simp add: Un_Diff)
-apply(simp add: fresh_star_union)
-apply(erule conjE)+
-apply(rule conjI)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="p" in supp_perm_eq)
-apply(simp add: supp_abs)
-apply(simp)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="p" in supp_perm_eq)
-apply(simp add: supp_abs)
-apply(simp)
-done
-
-lemma fresh_star_eq:
-  assumes a: "as \<sharp>* p"
-  shows "\<forall>a \<in> as. p \<bullet> a = a"
-using a by (simp add: fresh_star_def fresh_def supp_perm)
-
-lemma fresh_star_set_eq:
-  assumes a: "as \<sharp>* p"
-  shows "p \<bullet> as = as"
-using a 
-apply(simp add: fresh_star_def fresh_def supp_perm permute_set_eq)
-apply(auto)
-by (metis permute_atom_def)
-
-lemma 
-  fixes t1 s1::"'a::fs"
-  and   t2 s2::"'b::fs"
-  assumes asm: "finite as"
-  shows "(Abs as t1 = Abs bs s1 \<and>  Abs as t2 = Abs bs s2) \<longrightarrow> Abs as (t1, t2) = Abs bs (s1, s2)"
-apply(subst abs_eq_iff)
-apply(subst abs_eq_iff)
-apply(subst alphas_abs)
-apply(subst alphas_abs)
-apply(subst alphas)
-apply(subst alphas)
-apply(rule impI)
-apply(erule exE | erule conjE)+
-apply(simp add: abs_eq_iff)
-apply(simp add: alphas_abs)
-apply(simp add: alphas)
-apply(rule conjI)
-apply(simp add: supp_Pair Un_Diff)
-oops
-
-
-
-(* support of concrete atom sets *)
-
 lemma supp_atom_image:
   fixes as::"'a::at_base set"
   shows "supp (atom ` as) = supp as"
 apply(simp add: supp_def)
 apply(simp add: image_eqvt)
-apply(simp add: atom_eqvt_raw)
+apply(simp add: eqvts_raw)
 apply(simp add: atom_image_cong)
 done