Re: [isabelle] Declaring equal for a type; BNF not working on the left



Dear Gottfried,

You cannot define equality in Isabelle/HOL for any type as you wish, as the HOL axioms already define it for all types. The datatype package (and the BNF package) introduce an algebraic type whose constructors are free, i.e., injective and their ranges pairwise distinct. If you want to have a coarser notion of equality, you can define your own function such as mTeq with fancy notation such as (infix "==="), but you cannot use HOL equality = for it, and the proof tools (esp. the simplifier) will not treat it as equality either.

If you really want a type with your custom equality relation, you have to quotient your datatype through your custom equality relation [1] or directly construct a type with non-free type constructors [2]. You find more information on that in the references, but I have not examined your use case to see which route seems easier or feasible.

Andreas

[1] http://www21.in.tum.de/~kuncar/documents/huffman-kuncar-cpp2013.pdf

[2] https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-August/004413.html




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