Re: [isabelle] Declaring equal for a type; BNF not working on the left
On 11/7/2013 1:49 AM, Andreas Lochbihler wrote:
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  or
directly construct a type with non-free type constructors . 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  a little, but without knowing
the advantages of either, I'd pick  over . 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  also gives
some instruction about specific Isar commands related to that, and
explains things like Reb and Abs.
From , 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,
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
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
'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