[isabelle-dev] Typing problem in autogenerated axiom

[Makarius]

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