Re: [isabelle] graph theory in isabelle - nominal?



My two cents worth: it might make more sense to use the quotient package than the nominal package. Your intuition is that graph equality should be naming-independent.

Define graphs as sets of pairs in some big-enough naming alphabet (naturals, strings, unspecified type 'a ...) and quotient by the equivalence relation of bijective renaming.

That should give you a new type whose notion of equality matches your intuition. You may then have a bit of work to do to define the syntax and operations you need within the new type. I've never used the quotient package and don't know how much it will help you here. I think you could, for instance, define your disjoint union operator on the pairwise representation (easy) then lift it to an operator in the graph type by showing it respects the equivalence relation (tool support desirable).

This is quite a different approach to Lars' so the relative merits should be thought about.

Yours,
    Thomas.


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.





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