Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by Kunčar/Popescu

Dear Ken,

>> My suspicion is that declarations separated from definitions generally might cause inconsistency.

Actually, this is precisely what we prove in our paper: that, under the described checks, delayed ad hoc overloaded definitions of constants (performed via declarations followed by definitions of instances at later times) and type definitions are jointly consistent under HOL deduction.

>> In order to experiment, I would need some hint how declarations of
constants (accompanied with a latter definition) work in Isabelle 2016, as asked for at
as I couldn't find any information in the manuals about it.

In Isabelle 2016, you have to be more explicit about overloading -- see section 11.3 (ad hoc overloading for constants) in the reference manual:

Your noncircular example should be written as follows:

consts c :: 'a

typedef T = "{True}" by blast

  c_bool    ? "c :: bool"
definition c_bool :: bool where
  "c_bool = (if (EX (x::T). ALL y. x = y) then False else True)"

By contrast, Ondra's circular example fails in Isabelle 2016:

consts cc :: 'a

typedef (overloaded) TT = "{True,cc}" by blast

  cc_bool    ? "cc :: bool"
definition cc_bool :: bool where
  "cc_bool = (if (EX (x::TT). ALL y. x = y) then False else True)"

The theory is also attached.


Attachment: Defs.thy
Description: Defs.thy

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