tuned proof; forget the transfer rule for size_fset
authorkuncar
Fri Dec 05 14:14:36 2014 +0100 (2014-12-05)
changeset 6022832dd7adba5a4
parent 60227 eacf75e4da95
child 60229 4cd6462c1fda
tuned proof; forget the transfer rule for size_fset
src/HOL/Library/FSet.thy
     1.1 --- a/src/HOL/Library/FSet.thy	Fri Dec 05 14:14:36 2014 +0100
     1.2 +++ b/src/HOL/Library/FSet.thy	Fri Dec 05 14:14:36 2014 +0100
     1.3 @@ -1001,14 +1001,16 @@
     1.4      folded size_fset_overloaded_def]
     1.5  
     1.6  lemma fset_size_o_map: "inj f \<Longrightarrow> size_fset g \<circ> fimage f = size_fset (g \<circ> f)"
     1.7 -  unfolding size_fset_def fimage_def
     1.8 -  by (auto simp: Abs_fset_inverse setsum.reindex_cong[OF subset_inj_on[OF _ top_greatest]])
     1.9 -
    1.10 +  apply (subst fun_eq_iff)
    1.11 +  including fset.lifting by transfer (auto intro: setsum.reindex_cong subset_inj_on)
    1.12 +  
    1.13  setup {*
    1.14  BNF_LFP_Size.register_size_global @{type_name fset} @{const_name size_fset}
    1.15    @{thms size_fset_simps size_fset_overloaded_simps} @{thms fset_size_o_map}
    1.16  *}
    1.17  
    1.18 +lifting_update fset.lifting
    1.19 +lifting_forget fset.lifting
    1.20  
    1.21  subsection {* Advanced relator customization *}
    1.22