# 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

```
```(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.