*To*: Lars Hupel <hupel at in.tum.de>*Subject*: Re: [isabelle] size setup for HOL/Library/Finite_Map (fmap)*From*: Peter Gammie <peteg42 at gmail.com>*Date*: Mon, 14 Aug 2017 10:28:34 +1000*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*In-reply-to*: <4f9ff1b7-5f24-7536-b00b-8f90100135e3@in.tum.de>*References*: <5A9AD116-D935-4FC6-B51E-3C76CA107C69@gmail.com> <53f0ddba-68c3-6242-5923-2ef934125c6e@inf.ethz.ch> <9a35e6f7-765e-f668-3242-974d605749f0@in.tum.de> <4f9ff1b7-5f24-7536-b00b-8f90100135e3@in.tum.de>

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/

**Follow-Ups**:**Re: [isabelle] size setup for HOL/Library/Finite_Map (fmap)***From:*Lars Hupel

**References**:**[isabelle] size setup for HOL/Library/Finite_Map (fmap)***From:*Peter Gammie

**Re: [isabelle] size setup for HOL/Library/Finite_Map (fmap)***From:*Andreas Lochbihler

**Re: [isabelle] size setup for HOL/Library/Finite_Map (fmap)***From:*Lars Hupel

**Re: [isabelle] size setup for HOL/Library/Finite_Map (fmap)***From:*Lars Hupel

- Previous by Date: Re: [isabelle] size for records
- Next by Date: [isabelle] Worrying response from remote_vampire for property of complete_lattice (in Main)
- Previous by Thread: Re: [isabelle] size setup for HOL/Library/Finite_Map (fmap)
- Next by Thread: Re: [isabelle] size setup for HOL/Library/Finite_Map (fmap)
- Cl-isabelle-users August 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list