[isabelle] Proof extraction involving typedef and overloading [concerning: Isabelle Foundation & Certification]

[This thread has become too volumnious to be followed in detail by a
casual bystander, so I try here with Âone issue â one mailÂ.]

I did a glimpse at Alexander Krauss and Andreas Schropp, A mechanized
translation from higher-order logic to set theory. According to my
knowledge this had been the definite reference for taming overloading
and typedef until recently.

The critical passages are:

ÂAbstracting  out  unresolvable  overloading  would  give  rise  to
dependent  types.
This  is  no  problem  in  the  set-theoretic  interpretation,  but  as
 the  overloading
elimination is currently implemented as a preprocessing step on the HOL
it does not handle such overloading. This can be fixed by collapsing the
ent parts of the translation. However, to remove unresolvable
overloading from
type definitions while staying in HOL, one has to eliminate the type
altogether, replacing it by its representing type together with a predicate.
It appears that this subtle issue was overlooked in all proof sketches
of con-
servativity of overloading so far. Practically, this form of overloading
seems  to  be  quite  rare.  It  does  not  occur  in  the  main  HOL
image,  but  a  few
instances exist in the HOLCF development.Â

ÂThe fact that we uncovered a notable omission in all previous proofs of
conservativity of overloading shows that our approach of Âimplemented
semantics is also useful for better understanding the logical system.Â

Has anyone tried to apply proof extraction to a Âinconsistent typedefÂ
example? According to my blurry understanding of the whole picture this
should fail then!? Maybe this would deserve a reference.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.