[isabelle] size setup for HOL/Library/Finite_Map (fmap)



Dear BNF experts,

The `size` function for `fmap` in HOL/Library/Finite_Map in Isabelle2016-1 seems sub-optimal: it appears to ignore the sizes of the things in the map.

I tried implementing this using the approach taken in FSet and Multiset, but the `fmap` constructor is binary and Iâm not sure what shape the theorems should be (specifically the final one that composes size functions somehow).

Thanks!

cheers,
peter

-- 
http://peteg.org/





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.