[isabelle-dev] Typing problem in autogenerated axiom
krauss at in.tum.de
Wed Dec 2 11:15:28 CET 2009
> 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
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
>> 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.
More information about the isabelle-dev