*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Declaring equal for a type; BNF not working on the left*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Thu, 07 Nov 2013 15:32:09 -0600*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <527B45F9.2070507@inf.ethz.ch>*References*: <527B1BB1.3090708@gmx.com> <527B45F9.2070507@inf.ethz.ch>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 11/7/2013 1:49 AM, Andreas Lochbihler wrote:

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 datatypepackage (and the BNF package) introduce an algebraic type whoseconstructors are free, i.e., injective and their ranges pairwisedistinct. If you want to have a coarser notion of equality, you candefine your own function such as mTeq with fancy notation such as(infix "==="), but you cannot use HOL equality = for it, and the prooftools (esp. the simplifier) will not treat it as equality either.If you really want a type with your custom equality relation, you haveto quotient your datatype through your custom equality relation [1] ordirectly construct a type with non-free type constructors [2]. Youfind more information on that in the references, but I have notexamined 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

Andreas,

1) Variable 'a is special.

I put me an assumes axiom in a local like this: locale mTloc = assumes mTeq_ax: "mTeq == HOL.eq" begin theorem mTeq_imp_HOL_eq [simp]: "(mTeq x y) ==> (x = y)" by (metis (full_types) mT.distinct(1) mTeq.simps(3) mTeq_ax) end

"Additional type variable(s) in locale specification "mTloc": 'a∷type "

locale P_by_sorry begin theorem P_is_true: "P" sorry end theorem "True & False" by(rule, simp, rule P_by_sorry.P_is_true) So I tried to prove this outside the locale: theorem "(mTeq x y) ==> (x = y)" (*variables: x, y :: 'a mT type variables: 'a :: type *) oops

Regards, GB

**Follow-Ups**:**Re: [isabelle] Declaring equal for a type; BNF not working on the left***From:*Gottfried Barrow

**References**:**[isabelle] Declaring equal for a type; BNF not working on the left***From:*Gottfried Barrow

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

- Previous by Date: Re: [isabelle] Declaring equal for a type; BNF not working on the left
- Next by Date: Re: [isabelle] Autocompletion in 2013-1
- Previous by Thread: Re: [isabelle] Declaring equal for a type; BNF not working on the left
- Next by Thread: Re: [isabelle] Declaring equal for a type; BNF not working on the left
- Cl-isabelle-users November 2013 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