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.

ipv4cidr_to_interval :: "(ipv4addr à nat) â (ipv4addr à ipv4addr)"

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





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