Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu
On 21.08.2016 12:21, Lawrence Paulson wrote:
This question is a perfect example why I dislike the use of the word âinconsistency" in connection with the work of KunÄar and Popescu. Probably most people associate that word with some sort of incorrect logical reasoning. However, their work is concerned with Isabelle's automatic detection and rejection of circular definitions.
Indeed, this misleading tale told around the work by Kuncar / Popescu
greatly subtracts from otherwise fine technical improvements.
I have already pointed out many times that it was mainly a change of the
documented situation in Isabelle/HOL. Before there was a section in the
manual saying clearly that typedefs are not fully checked. Afterwards,
the officially supported typedefs were (1) extended to typedefs
depending on overloaded consts (which was previously not covered) and
(2) the extended scheme checked by the system.
Thus the isar-ref manual entry of HOL typedef could be changed
accordingly: the system has become more user-friendly, since the user is
no longer blamed implicitly for not having read the manual when
something goes wrong; instead the system complains explicitly. In
practice, such a situation was never seen, though, because the
counter-example from the paper by Kuncar / Popescu was constructed
synthetically to illustrate a theoretical point.
This archive was generated by a fusion of
Pipermail (Mailman edition) and