equal
deleted
inserted
replaced
1000 size_fset_simps[of "\<lambda>_. 0", unfolded add_0_left add_0_right, |
1000 size_fset_simps[of "\<lambda>_. 0", unfolded add_0_left add_0_right, |
1001 folded size_fset_overloaded_def] |
1001 folded size_fset_overloaded_def] |
1002 |
1002 |
1003 lemma fset_size_o_map: "inj f \<Longrightarrow> size_fset g \<circ> fimage f = size_fset (g \<circ> f)" |
1003 lemma fset_size_o_map: "inj f \<Longrightarrow> size_fset g \<circ> fimage f = size_fset (g \<circ> f)" |
1004 unfolding size_fset_def fimage_def |
1004 unfolding size_fset_def fimage_def |
1005 by (auto simp: Abs_fset_inverse setsum_reindex_cong[OF subset_inj_on[OF _ top_greatest]]) |
1005 by (auto simp: Abs_fset_inverse setsum.reindex_cong[OF subset_inj_on[OF _ top_greatest]]) |
1006 |
1006 |
1007 setup {* |
1007 setup {* |
1008 BNF_LFP_Size.register_size_global @{type_name fset} @{const_name size_fset} |
1008 BNF_LFP_Size.register_size_global @{type_name fset} @{const_name size_fset} |
1009 @{thms size_fset_simps size_fset_overloaded_simps} @{thms fset_size_o_map} |
1009 @{thms size_fset_simps size_fset_overloaded_simps} @{thms fset_size_o_map} |
1010 *} |
1010 *} |