--- a/Nominal/Abs.thy	Sat Sep 04 14:26:09 2010 +0800
+++ b/Nominal/Abs.thy	Sun Sep 05 06:42:53 2010 +0800
@@ -6,6 +6,14 @@
         "Quotient_Product" 
 begin
 
+section {* Support w.r.t. relations *}
+
+definition 
+  "supp_rel R x = {a. infinite {b. \<not>(R ((a \<rightleftharpoons> b) \<bullet> x) x)}}"
+
+
+section {* Abstractions *}
+
 fun
   alpha_set 
 where

--- a/Nominal/Ex/SingleLet.thy	Sat Sep 04 14:26:09 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Sun Sep 05 06:42:53 2010 +0800
@@ -1,5 +1,5 @@
 theory SingleLet
-imports "../Nominal2"
+imports "../Nominal2" "../Abs"
 begin
 
 atom_decl name
@@ -45,18 +45,21 @@
 
 
 lemma supp_fv:
-  "fv_trm t = supp t \<and> fv_assg as = supp as \<and> fv_bn as = {a. infinite {b. \<not>alpha_bn ((a \<rightleftharpoons> b) \<bullet> as) as}}"
+  "fv_trm t = supp t \<and> fv_assg as = supp as \<and> fv_bn as = supp_rel alpha_bn as"
 apply(rule single_let.induct)
-apply(simp_all (no_asm_use) only: single_let.fv_defs)[2]
-apply(simp_all (no_asm_use) only: supp_def)[2]
-apply(simp_all (no_asm_use) only: single_let.perm_simps)[2]
-apply(simp_all (no_asm_use) only: single_let.eq_iff)[2]
-apply(simp_all (no_asm_use) only: de_Morgan_conj)[2]
-apply(simp_all (no_asm_use) only: Collect_disj_eq)[2]
-apply(simp_all (no_asm_use) only: finite_Un)[2]
-apply(simp_all (no_asm_use) only: de_Morgan_conj)[2]
-apply(simp_all (no_asm_use) only: Collect_disj_eq)[2]
-apply(simp)
+-- " 0A "
+apply(simp only: single_let.fv_defs supp_Pair[symmetric])
+apply(simp only: supp_abs(3)[symmetric])?
+apply(simp (no_asm) only: supp_def)
+apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
+apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
+-- " 0B"
+apply(simp only: single_let.fv_defs supp_Pair[symmetric])
+apply(simp only: supp_abs(3)[symmetric])?
+apply(simp (no_asm) only: supp_def)
+apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
+apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
+apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
 --" 1 "
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
 apply(simp only: supp_abs(3)[symmetric])
@@ -70,7 +73,7 @@
 apply(erule conjE)+
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
 apply(simp only: supp_abs(3)[symmetric])
-apply(simp (no_asm) only: supp_def)
+apply(simp (no_asm) only: supp_def supp_rel_def)
 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un)
@@ -80,7 +83,7 @@
 -- " 3 "
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
 apply(simp only: supp_abs(1)[symmetric])
-apply(simp (no_asm) only: supp_def)
+apply(simp (no_asm) only: supp_def supp_rel_def)
 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
@@ -109,7 +112,7 @@
 apply(rule conjI)
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
 apply(simp only: supp_abs(3)[symmetric])
-apply(simp (no_asm) only: supp_def)
+apply(simp (no_asm) only: supp_def supp_rel_def)
 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
@@ -119,7 +122,7 @@
 -- "other case"
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
 apply(simp only: supp_abs(3)[symmetric])
-apply(simp (no_asm) only: supp_def)
+apply(simp (no_asm) only: supp_def supp_rel_def)
 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)