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



> 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




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