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

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 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.





Thanks for the help again. I looked at [2] a little, but without knowing the advantages of either, I'd pick [2] over [1]. That's because I constantly see emails about lifting and transfer, where quotients are a part of that, so I need to learn all that anyway. The doc [2] also gives some instruction about specific Isar commands related to that, and explains things like Reb and Abs.

From [1], they write, "Building a theory library that implements a new abstract type can take a lot of work." If I knew my datatype was going to be a winner, then I'd want to research it all and set things up right, because you only want to do things once. However, the datatype could be a loser, so I first need to prove enough theorems about it to think it's worth setting up in a more sophisticated way.

Also, I need the experience working with more basic things anyway, because I'm still working on learning how to use datatype, fun, primrec, and function.

Thinking about equality can be a brainbuster, because it's so basic, and you generally just use "=".

Other than the methods you mentioned, there's an easy way to associate a function with HOL.eq, and that's with an axiom.

That's what I did with another type, where the type has to have axioms. I can easily say `theorem bar [intro?]: "foo a b ==> a = b", because the axiom says "(foo a b) <-> (a = b)". So "=" is still the function HOL.eq, but the intro rule makes it easy to set up proving equality, which came from a tip by Lars.

I thought using my new type in a local might be the thing to do, but I don't understand locales that well. From what you told me, I sort of left off here:

1) Variable 'a is special.

2) Instantiation sometimes works in the background to help you out, but sometimes it doesn't, at which times you must know what you're doing.

I put me an assumes axiom in a local like this:

locale mTloc =
assumes mTeq_ax: "mTeq == HOL.eq"
theorem mTeq_imp_HOL_eq [simp]:
"(mTeq x y) ==> (x = y)"
by (metis (full_types) mT.distinct(1) mTeq.simps(3) mTeq_ax)

Doing that confused the issue for me even more about how type variables are used in locales. First, the locale complains with this warning:

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

It then uses 'b variables in the theorem. My goal was to determine whether what's proved in the locale is only true in the locale, where I already know that some things proved in a local are not completely localized:

locale P_by_sorry
theorem P_is_true: "P" sorry

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)"
x, y :: 'a mT
type variables:
'a :: type *)

It can't use the locale theorem to prove the global theorem because the locale theorem is using 'b variables, and the global theorem is using 'a variables. I am left pondering the subject of type variables, though I must move on.


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