Email Gateway (Aug 22 2022 at 10:05): Email Gateway (Aug 22 2022 at 10:05):From: "C. Diekmann" <diekmann@in.tum.de>
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
Email Gateway (Aug 22 2022 at 10:05):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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.
Email Gateway (Aug 22 2022 at 10:06):From: "C. Diekmann" <diekmann@in.tum.de>
Great idea, thanks!
2015-05-05 8:09 GMT+02:00 Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>:
Last updated: Apr 25 2024 at 20:15 UTC