*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*: Tue, 15 Aug 2017 11:58:31 +1000*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*In-reply-to*: <33de19c7-850f-a82c-2c2b-482a0f56df12@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> <6E69D399-DF51-4454-B802-628AEA269A34@gmail.com> <33de19c7-850f-a82c-2c2b-482a0f56df12@in.tum.de>

Lars, Thanks for the pointers. I donât recall seeing the stuff you mentioned about [measure_function] being mentioned in the `functions` manual; perhaps it could be added? cheers, peter > On 15 Aug 2017, at 02:05, Lars Hupel <hupel at in.tum.de> wrote: > >> 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? > > Here's a mailing list thread on that issue: > <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-September/msg00015.html>. > >> 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? > > There is such a function: "size_prod". However, you have to tell the > function package about it. > >> (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.) > > Here's a contrived example: > > fun contrived :: "('a list Ã 'a list) â ('a list Ã 'a list)" where > "contrived (xs, y1 # y2 # ys) = contrived (y1 # xs, ys)" | > "contrived (x1 # x2 # xs, ys) = contrived (xs, x1 # ys)" | > "contrived _ = ([], [])" > > By default, the function package won't be able to derive a termination > measure for this. But you can add the following before the definition: > > lemma [measure_function]: "is_measure (size_prod size size)" > by (rule is_measure.intros) > > There's probably a good reason why this doesn't happen by default. > (Possibly time complexity of the termination prover.) If this thing > keeps happening to you (or you need nesting), try this: > > lemma [measure_function]: "is_measure f â is_measure g â is_measure > (size_prod f g)" > by (rule is_measure.intros) > > This might mess up things elsewhere though, so try it at your own risk. > > Cheers > Lars -- 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

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

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

- Previous by Date: Re: [isabelle] size setup for HOL/Library/Finite_Map (fmap)
- Next by Date: Re: [isabelle] size setup for HOL/Library/Finite_Map (fmap)
- 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