[isabelle-dev] Typing problem in autogenerated axiom

Makarius makarius at sketis.net
Wed Dec 2 16:57:24 CET 2009

On Wed, 2 Dec 2009, Dominique Unruh wrote:

> Considering the future plans for completely removing sorts from
> Isabelle, I tend towards approach B.

I would not call this a "future plan", but a very old one that has not
been fully implemented yet.  The foundations of Pure/HOL with type classes
on top of Pure/HOL without type classes go back to my definitional version
of "axiomatic type classes" from 1994 -- in 1992/1993 type classes have
been truely axiomatic, and wrong.  Later we have refined these ideas a
lot, relating them with locales (Florian Haftmann has mentioned some
papers already).  The last step to apply the expansion to proof terms as
well was last anticipated for Dec. 2006 / Jan. 2007.  Now we are much
closer to an actual implementation.

>>> and that
>>> Isabelle proof terms may contain free variables (which implies that in
>>> Pure all terms
>>> are inhabited) while Coq proof terms may not.)
>
>> You mean types? And I guess your reasoning refers to hidden term variables
>> which occur in the proof, but not in the proved proposition?
>
> Yes, that what I meant. These are produced for example if we use "fix
> x::'a" in Isar and then only use x to show non-emptiness of 'a.

You can have both fixed term and type variables hidden in a proof term,
but not occurring in the final proposition.  They essentially act like
global constants.  In certain situations, the system replaces term
variables by the "dummy_pattern" constant. There are very few situations
where the user can actually conduct meaningful proofs involving such
unofficial "variables".

Note that "to show non-emptiness of 'a" is vacous in the Pure framework:
types are always inhabited.  This is implicit in the formulation of the
basic calculus, and allows certain implicit communations on "fixes" vs.
"assumes" that would not be possible in Coq, for example.

Makarius