# HG changeset patch
# User kuncar
# Date 1417785276 -3600
# Node ID 32dd7adba5a4233f27e31514de5f1df402730dad
# Parent  eacf75e4da95e8443fde0cb42152931fa6107a93
tuned proof; forget the transfer rule for size_fset

diff -r eacf75e4da95 -r 32dd7adba5a4 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Fri Dec 05 14:14:36 2014 +0100
+++ b/src/HOL/Library/FSet.thy	Fri Dec 05 14:14:36 2014 +0100
@@ -1001,14 +1001,16 @@
     folded size_fset_overloaded_def]
 
 lemma fset_size_o_map: "inj f \<Longrightarrow> size_fset g \<circ> fimage f = size_fset (g \<circ> f)"
-  unfolding size_fset_def fimage_def
-  by (auto simp: Abs_fset_inverse setsum.reindex_cong[OF subset_inj_on[OF _ top_greatest]])
-
+  apply (subst fun_eq_iff)
+  including fset.lifting by transfer (auto intro: setsum.reindex_cong subset_inj_on)
+  
 setup {*
 BNF_LFP_Size.register_size_global @{type_name fset} @{const_name size_fset}
   @{thms size_fset_simps size_fset_overloaded_simps} @{thms fset_size_o_map}
 *}
 
+lifting_update fset.lifting
+lifting_forget fset.lifting
 
 subsection {* Advanced relator customization *}