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



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.

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


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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