*To*: 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*: Peter Lammich <lammich at in.tum.de>*Date*: Tue, 15 Aug 2017 11:56:55 -0400*In-reply-to*: <fc29e358-5e56-97ed-75e1-c2671a0dd7da@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>

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) --Â Â Peter > > Not 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 > >

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

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

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