*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] size setup for HOL/Library/Finite_Map (fmap)*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 15 Aug 2017 12:14:20 +0200*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>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:52.0) Gecko/20100101 Thunderbird/52.2.1

I learned about lemma [measure_function]: "is_measure f â is_measure g â is_measure (size_prod f g)" by (rule is_measure.intros)

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

**Attachment:
smime.p7s**

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

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