*To*: "C. Diekmann" <diekmann at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Best practice for lemmas about functions which return tuples*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 5 May 2015 08:09:31 +0200*In-reply-to*: <CAGbqCMwK0JanhW=5OutymJCmrJYLfApSGhPtyv7CTeWnNnwxZw@mail.gmail.com>*References*: <CAGbqCMwK0JanhW=5OutymJCmrJYLfApSGhPtyv7CTeWnNnwxZw@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

Dear Cornelius,

Best, Andreas

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

**Follow-Ups**:

**References**:**[isabelle] Best practice for lemmas about functions which return tuples***From:*C. Diekmann

- Previous by Date: [isabelle] size entry-point in signature TABLE
- Next by Date: Re: [isabelle] Let and commutative rewrite rules
- Previous by Thread: [isabelle] Best practice for lemmas about functions which return tuples
- Next by Thread: Re: [isabelle] Best practice for lemmas about functions which return tuples
- Cl-isabelle-users May 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list