*To*: Ken Kubota <mail at kenkubota.de>*Subject*: Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by Kunčar/Popescu*From*: Andrei Popescu <A.Popescu at mdx.ac.uk>*Date*: Fri, 26 Aug 2016 14:55:07 +0000*Accept-language*: en-GB, en-US*Authentication-results*: spf=none (sender IP is ) smtp.mailfrom=A.Popescu@mdx.ac.uk;*Cc*: Ondřej Kunčar <kuncar at in.tum.de>, "Prof. Lawrence C. Paulson" <lp15 at cam.ac.uk>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <1D5912E0-5713-438B-B3D9-48A9CF527B7E@kenkubota.de>*References*: <CDD6C40D-96BE-46B5-99F1-C9C35A8CE6D6@kenkubota.de> <C5CAD6F5-6760-4704-A5CF-89C0FB06F053@cam.ac.uk> <9f07313f-afdc-aeb1-a51f-52bf84a7421e@in.tum.de> <7CE7A9FB-7DF1-41D6-9305-EA1A81107E3D@cam.ac.uk> <AM3PR01MB131338D89E41C0FC70D40C1EB7E80@AM3PR01MB1313.eurprd01.prod.exchangelabs.com> <282E0446-0527-418E-A708-4F7A0E358FE0@cam.ac.uk> <AM3PR01MB131320314E30705D39B139E8B7EA0@AM3PR01MB1313.eurprd01.prod.exchangelabs.com>, <1D5912E0-5713-438B-B3D9-48A9CF527B7E@kenkubota.de>*Spamdiagnosticmetadata*: NSPM*Spamdiagnosticoutput*: 1:99*Thread-index*: AQHR+wAi81lsNUW2qk6xB9kUTOFQsqBTNX0AgACcoICAAA3pAIABwWc7gAC7oQCAAYVye4ADOjqAgAA75yw=*Thread-topic*: [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**

**References**:**[isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu***From:*Ken Kubota

**Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu***From:*Lawrence Paulson

**Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu***From:*OndÅej KunÄar

**Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu***From:*Lawrence Paulson

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

*From:*Lawrence Paulson

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

*From:*Ken Kubota

- Previous by Date: Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu
- Next by Date: Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu
- Previous by Thread: Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu
- Next by Thread: Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu
- Cl-isabelle-users August 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list