*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*: Tue, 23 Aug 2016 13:24:01 +0200*Cc*: Andrei Popescu <a.popescu at mdx.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>

Using the current Isabelle 2016, it is not possible for me to reproduce the problem. If I understand Andrei Popescu and Makarius Wenzel correctly, declarations of constants earlier than and separated from their definitions should be possible, but circular dependencies not anymore in the 2016 version of Isabelle. Nevertheless, the error message reports a problem with the definition of the constant, even if circularity is avoided by removing 'c' from tau ('T'). Could you please provide a working example (for the 2016 version of Isabelle) by correcting my attempt (shown with the results below)? Please note that line "consts c:Î" ("consts c:alpha") at http://www21.in.tum.de/~kuncar/kuncar-popescu-jar2016.pdf (p. 3) still differs from line "consts c :: bool" in http://www21.in.tum.de/~kuncar/documents/False.tar.gz available via http://www21.in.tum.de/~kuncar/documents/patch.html Ken Kubota (* using 'a, "(overloaded)", "definition", and c is removed from T *) consts c :: 'a typedef (overloaded) T = "{True}" by blast definition c_bool_def: "c::bool â if (â(x::T) y. x = y) then False else True" (*ERROR: Bad head of lhs: existing constant "c"*) (* using 'a, "(overloaded)" and "definition" *) consts c :: 'a typedef (overloaded) T = "{True, c}" by blast definition c_bool_def: "c::bool â if (â(x::T) y. x = y) then False else True" (*ERROR: Bad head of lhs: existing constant "c"*) (* using "(overloaded)" and "definition" *) consts c :: bool typedef (overloaded) T = "{True, c}" by blast definition c_bool_def: "c::bool â if (â(x::T) y. x = y) then False else True" (*ERROR: Bad head of lhs: existing constant "c"*) (* original version by Ondrej Kuncar, with "defs" *) consts c :: bool typedef T = "{True, c}" by blast defs c_bool_def: "c::bool â if (â(x::T) y. x = y) then False else True" (* several errors in current Isabelle 2016 *) > 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

**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: [isabelle] Abbreviation makes Isabelle/HOL very slow
- 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