*To*: Peter Lammich <lammich at in.tum.de>, Tobias Nipkow <nipkow at in.tum.de>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] size setup for HOL/Library/Finite_Map (fmap)*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 29 Aug 2017 17:01:05 +0200*In-reply-to*: <1502812615.1546.17.camel@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> <fc29e358-5e56-97ed-75e1-c2671a0dd7da@in.tum.de> <1502812615.1546.17.camel@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.2.1

Hi Peter and Peter,

Andreas On 15/08/17 17:56, Peter Lammich wrote:

On Di, 2017-08-15 at 12:14 +0200, Tobias Nipkow wrote:I learned about lemma [measure_function]: "is_measure f â is_measure g â is_measure (size_prod f g)" by (rule is_measure.intros) from Peter Lammich who probably uses it more often. He may have some insight as to the dangers of using this by default.I have not used this very often, too. Only for small isolated examples, but not in the basis of some big developments. Nevertheless, I would be curious what would happen if one adds this lemma by default (e.g. to Main) -- PeterNot that the recursive function need not be tupled for this to help because internally the arguments are tupled anyway. It would indeed be nice if this were mention in the "function manual". In case somebody feel sufficiently au fait with this feature ... Tobias On 14/08/2017 18:05, Lars Hupel 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

**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

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

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

- Previous by Date: Re: [isabelle] Isabelle2017-RC0 requires read/write installation
- Next by Date: [isabelle] What it means to "embedd logic in Isabelle/HOL", is this a standard procedure?
- Previous by Thread: Re: [isabelle] size setup for HOL/Library/Finite_Map (fmap)
- Next by Thread: [isabelle] size for records
- 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