# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269678103 -3600
# Node ID d24f59f78a86eabc9885a18410b1b912f2dfb464
# Parent  7eb95f86f87f59b1239ef6f99a9cb33a903fd3d9
Generalize Abs_eq_iff.

diff -r 7eb95f86f87f -r d24f59f78a86 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Sat Mar 27 09:15:09 2010 +0100
+++ b/Nominal/Abs.thy	Sat Mar 27 09:21:43 2010 +0100
@@ -447,8 +447,9 @@
 
 lemma Abs_eq_iff:
   shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
-  by (lifting alpha_abs.simps(1))
-
+  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 split_rsp2[quot_respect]: "((R1 ===> R2 ===> prod_rel R1 R2 ===> op =) ===>
   prod_rel R1 R2 ===> prod_rel R1 R2 ===> op =) split split"
diff -r 7eb95f86f87f -r d24f59f78a86 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Sat Mar 27 09:15:09 2010 +0100
+++ b/Nominal/Fv.thy	Sat Mar 27 09:21:43 2010 +0100
@@ -896,7 +896,7 @@
   simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps (@{thm permute_Abs} :: perm)) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW
diff -r 7eb95f86f87f -r d24f59f78a86 Nominal/Nominal2_FSet.thy
--- a/Nominal/Nominal2_FSet.thy	Sat Mar 27 09:15:09 2010 +0100
+++ b/Nominal/Nominal2_FSet.thy	Sat Mar 27 09:21:43 2010 +0100
@@ -44,7 +44,7 @@
 
 end
 
-lemma permute_fset[simp,eqvt]:
+lemma permute_fset[eqvt]:
   "p \<bullet> ({||} :: 'a :: pt fset) = {||}"
   "p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)"
   by (lifting permute_list.simps)