# Re: [isabelle] Best practice for lemmas about functions which return tuples

```Dear Cornelius,

```
For proving, I try to avoid functions that return tuples, precisely because of these ugly tuple assumptions and case expressions. When it conceptually makes sense to tuple results (like in your case), I usually define the projections as separate constants and work with them in the proofs. In your example, you could define the functions start_of_ipv4cidr and end_of_ipv4cidr and use them consistently in the proofs. Then, proof obligations as you mention simplify to x : {start_of_ipv4cidr (a, b)..end_of_ipv4cidr (a, b)}.
```
Best,
Andreas

```
PS: Name spaces in Isabelle are strictly separated by the kind they refer to. So a class, a type, a function, and a theorem can all have the same name. It is sometimes even sensible to do so, but that depends on the application.
```
On 04/05/15 22:04, C. Diekmann wrote:
```
```Dear isabelle users,

I have a function which returns a tuple.

Background: Given an IPv4 address sapce in CIDR notation, it returns
the start and end IP.
Example: ipv4cidr_to_interval 192.168.0.0/24 = (0xC0A80000, 0xC0A800FF)

I can show the correctness of this function:

lemma ipv4cidr_to_interval: "ipv4cidr_to_interval (base, len) = (s,e)
â ipv4range_from_bitmask base len = {s .. e}"

However, in many proof obligations, expressions similar to the one below occur:

x â (case ipv4cidr_to_interval (a, b) of (x, xa) â {x..xa})
or
case ipv4cidr_to_interval a of (x, xa) â {x..xa})

The lemma ipv4cidr_to_interval doesn't help as simplification rule
here. My question: What is the best way to state lemmas about tupels
such that they server best as simplification rules?

By the way: Is it okay to give lemmas and definitions/functions the same name?

Best,
Cornelius

```
```

```

• Follow-Ups:

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