*To*: Peter Gammie <peteg42 at gmail.com>*Subject*: Re: [isabelle] size setup for HOL/Library/Finite_Map (fmap)*From*: Lars Hupel <hupel at in.tum.de>*Date*: Mon, 14 Aug 2017 18:05:55 +0200*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*In-reply-to*: <6E69D399-DF51-4454-B802-628AEA269A34@gmail.com>*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>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.2.1

> 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

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

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

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

- Previous by Date: Re: [isabelle] Worrying response from remote_vampire for property of complete_lattice (in Main)
- 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