*To*: OndÅej KunÄar <kuncar at in.tum.de>*Subject*: Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu*From*: Ken Kubota <mail at kenkubota.de>*Date*: Mon, 22 Aug 2016 19:39:50 +0200*Cc*: Andrei Popescu <a.popescu at mdx.ac.uk>, "Prof. Lawrence C. Paulson" <lp15 at cam.ac.uk>, "Dr. Markus Wenzel" <makarius at sketis.net>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <5bfdc080-bf44-a033-9827-6d8c3b7fef05@in.tum.de>*References*: <CDD6C40D-96BE-46B5-99F1-C9C35A8CE6D6@kenkubota.de> <AM3PR01MB1313544EEAE1E863CEF17D97B7E90@AM3PR01MB1313.eurprd01.prod.exchangelabs.com> <0192D3B0-CE89-40F5-A978-629B40D5E207@kenkubota.de> <5bfdc080-bf44-a033-9827-6d8c3b7fef05@in.tum.de>

But then, looking at the revised version, the problem still seems to be caused by the language. The first line ("consts" â) seems to be a declaration, and the third line ("defs" â) a definition. Declarations like this allow the declared constant to practically behave like a variable, since the constant can be specified (defined) much later. In Q0/R0 there are no such declarations. If one would try to express the same in the language of R0, only one possibility would be left. The definition ("defs" â) could not be placed first, since it requires tau, which would be introduced by the latter type definition ("typedef" â) not available at the beginning. Hence first type tau has to be defined (being a mere abbreviation) on the basis of a variable "c" as: tau := [\x:bool . x=T \/ x=c:bool] Proving tau_T (i.e., T is element of tau; '_' denotes lambda application) then makes tau a type (being non-empty). Finally, c = ~(AL x,y:tau . x=y) could be introduced as a hypothesis. Since it leads to a contradiction, it is shown to be false (hence, c != ~(AL x,y:tau . x=y) ), which is the desired result. In summary, the solution would be not allowing declarations in the mathematical language, but only definitions, like in Q0/R0. Concerning the question of definitions, they shouldn't be part of the kernel, since non-logical axioms should be avoided as discussed in section 3 at https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-August/msg00069.html Also, implementing definitions within the logical core contradicts to the LCF philosophy of a small trusted kernel. For this reason, definitions in R0 are mere abbreviations located outside of the logical kernel. They also can be removed at any time (and re-introduced again) without modifying the theorems already obtained. Ken Kubota > Am 21.08.2016 um 21:17 schrieb OndÅej KunÄar <kuncar at in.tum.de>: > > On 08/21/2016 07:35 PM, Ken Kubota wrote: >> Dear Andrei, >> >> Thank you for the quick answer, and also thanks to Larry Paulson and Makarius Wenzel. >> >> I had read the abbreviated notation with the forall quantifier too quickly, but still the third restriction specified at >> http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf (p. 33) or at [Gordon/Melham, 1993, p. 220]. >> seems to be violated, as the type variable sigma occurs in the definiens, but not in (the type of) the definiendum. > > That's a typo, that type should be tau, the type that was defined on the previous line. I've already uploaded an updated version of the draft. > > Btw, we usually use alpha, beta, gamma for type variables, not sigma. But this is not mentioned until page 7. > > Ondrej ____________________ Ken Kubota doi: 10.4444/100 http://dx.doi.org/10.4444/100

**Follow-Ups**:

**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:*Andrei Popescu

**Re: [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:*OndÅej KunÄar

- 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