[isabelle-dev] Typing problem in autogenerated axiom

Andreas Schropp schropp at in.tum.de
Thu Dec 3 19:35:23 CET 2009

Dominique Unruh wrote:
>> Most of our problems stem from HOL and Pure sharing a function space,
>> whereas ZF has its own set theoretic one, which is of course very different
>> from the Pure one. I solved this by a stratification of types into HOL/Pure
>> parts, and carrying this stratification schematically through the whole
>> translation process, which works because proof constants are only
>> schematically polymorphic.
> Yes, the nice thing about Coq is that it is almost an exact superset
> of what is available in HOL (at least when we use the various optional
> Coq-axioms like excluded-middle and extensionality-of-equality).

Hmm, what about typedefs? I thought they are a peculiarity of HOL and 
its set-theoretic model. What do they correspond to in Coq?

> So overall, I think the best approach for me is approach B, because it
> should work well and be compatible with the current plans for the
> Isabelle kernel.

Yes, it sounds like that.

> Best,
> Dominique

More information about the isabelle-dev mailing list