# HG changeset patch
# User traytel
# Date 1362731678 -3600
# Node ID 197ad6b8f7630b80662245a1b2cc0158270707d5
# Parent  716a94cc5aaf1f4dbc11c11f26b2fca946020e80
some simp rules for fset

diff -r 716a94cc5aaf -r 197ad6b8f763 src/HOL/BNF/More_BNFs.thy
--- a/src/HOL/BNF/More_BNFs.thy	Thu Mar 07 18:14:30 2013 +0100
+++ b/src/HOL/BNF/More_BNFs.thy	Fri Mar 08 09:34:38 2013 +0100
@@ -470,6 +470,8 @@
   unfolding fset_rel_def fset_rel_aux by simp
 qed auto
 
+lemmas [simp] = fset.map_comp' fset.map_id' fset.set_natural'
+
 lemma fset_rel_fset: "set_rel \<chi> (fset A1) (fset A2) = fset_rel \<chi> A1 A2"
 unfolding fset_rel_def set_rel_def by auto 
 
diff -r 716a94cc5aaf -r 197ad6b8f763 src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Thu Mar 07 18:14:30 2013 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Fri Mar 08 09:34:38 2013 +0100
@@ -722,6 +722,9 @@
   shows "map_fset f (S |\<union>| T) = map_fset f S |\<union>| map_fset f T"
   by (descending) (simp)
 
+lemma in_fset_map_fset[simp]: "a |\<in>| map_fset f X = (\<exists>b. b |\<in>| X \<and> a = f b)"
+  by descending auto
+
 
 subsection {* card_fset *}