[isabelle-dev] Typing problem in autogenerated axiom

[Alexander Krauss]

Hi Dominique,

> Just to make sure I understand this correctly: The proof term that is
> stored with a theorem will contain no nonempty sorts at all (not even
> in intermediate proof steps)?
Yes. Unfinished proofs can still contain them, but they are normalized 
away when the theorem is stored/closed.

> Can you give me a very rough estimate for when this patch is planned
> (like in a few days, months, years, decades, eras, ...)?

"a few months" is probably the most realistic option on your list. But 
if you like, we can make our current code available to you... at your 
own risk, of course.

> Disciplined overloading (i.e., where the overloaded only occurs in
> combination with instance-declarations of type classes), however, can
> be done. To see this, we have to understand how Coq handles type
> classes:
[...]

What you are describing is essentially the dictionary construction. We 
are doing essentially the same thing, passing dictionaries around 
explicitly. With a bit of luck, you could then avoid doing this 
yourself, and just need to recover the implicit arguments setup somehow...

>> How do you handle the
>> interactions between Pure and HOL, or is this even a problem when
>> translating into another type theory?
> 
> I am not sure what interactions you mean. Do you mean things like the
> relation between --> and ==> and the relation between = and ==? As far
> as I see, there are no problems there. For example, one can map -->
> and ==> to the same Coq constant, and then all the HOL/Pure
> interrelation axioms (like impI) are trivial lemmas in Coq.

Interesting. Maybe some of our problems are due to the fact that we are 
trying to keep the part of the reasoning that uses Pure in Pure (mostly 
concerning the outermost !!/==> structure), and to map only the HOL part 
to ZF. But just throwing them together is probably the right thing to do 
for Coq...

>> I would actually like it if even axiomatized constants would get topsorted
>> declared types in consts.ML
> 
> If I understand correctly, the constant typing rule makes the sorts of
> constants completely irrelevant from the logical point of view anyway.
> So it seems that giving sorts to a constant does not have any other
> effect than declaring a constraint for that constant. Am I right?

I think so.

Alex