Re: [isabelle] instance theorems



Hi Makarius,


What exactly does this strange allusion to a ``bug in Isabelle'' mean on
the bottom of p. 8?

If there are no bugs in Isabelle, the instance theorems will be instantiated correctly. This is all. I suppose that holds for all of what I am doing, but I didn't think to write that. I do not think that there is a bug in Isabelle.
The allusion was meant to distinguish between the lack of possibility
of programmer error (barring an Isabelle bug) in the elaboration phase, and
the strong potential for user error in the use phase.

Anyway, you have all theses consts as part of axclass/instance.  From
where did you get these?  Note that the purely logical concept of
axiomatic type classes cannot express such membership.

But I have access to not only the type class definitions, but the
constant definitions as well.
The only problem is matching undefined constants such as <= to
their type class.  As the class is usually explicit, this is not
a problem.  For instance, from <= : 'a:: ord -> 'a -> bool it is
easy to figure where to put this constant.

Also, most axiomatic type classes have axioms, which contain constants
on which the axioms hold.  If these constants are not  defined, then
they are in the list.  So if order were defined without ord,
<= would be the list, but Least not.



	Makarius







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