Re: [isabelle] size setup for HOL/Library/Finite_Map (fmap)



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/





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.