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
        https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-August/msg00093.html
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:    http://isabelle.in.tum.de/doc/isar-ref.pdf

Your noncircular example should be written as follows:

consts c :: 'a

typedef T = "{True}" by blast

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

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

consts cc :: 'a

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

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

The theory is also attached.

Andrei

Attachment: Defs.thy
Description: Defs.thy



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