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



Lars, Andreas:

> On 12 Aug 2017, at 7:07 am, Lars Hupel <hupel at in.tum.de> wrote:
> 
>> This is an oversight â I'll try to add this to the theory over the next
>> couple of days.
> 
> See now <http://isabelle.in.tum.de/repos/isabelle/rev/4d2ce596f505>.
> 
> Peter, please try it out and tell me if it works for you.

Thanks Lars. I backported it to Isabelle2016-1 and indeed my termination proof now goes through.

Another question for you and Andreas: what is the substantive difference in intent between Finite_Map and FinFun? I used Finite_Map as I needed the BNF setup, but I reached for FinFun first as I knew it was there. In the fullness of time, could they perhaps be merged?

And another, but perhaps more directly for the BNF people: Iâve been tripped up on products uniformly having a constant size a few times now. Hereâs a quick theorem search:

  Basic_BNF_LFPs.prod.size(2): size (?x1.0, ?x2.0) = Suc 0

Could it too be made more useful by returning the sum of the sizes of its arguments?

(These arose in termination arguments, and the fun package seems to avoid using size on products. I wonder if such a change would impact it.)

cheers,
peter

â
http://peteg.org/





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