*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Isabelle2016-1-RC3 available for testing: new define command*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Fri, 25 Nov 2016 12:02:41 +0100*In-reply-to*: <02944604-816d-de8f-f003-fb2ee453f9c4@sketis.net>*Organization*: TU München*References*: <26df9858-15fc-10bb-908b-a5cf02cc6dd2@sketis.net> <987e7ba9-1b29-769f-89c4-bb090e9e7cd9@gmail.com> <02944604-816d-de8f-f003-fb2ee453f9c4@sketis.net>

Am Freitag, den 25.11.2016, 11:41 +0100 schrieb Makarius: > On 25/11/16 11:03, Christian Sternagel wrote: > > > > I would have guessed (but reading isar-ref showed me otherwise) > > that > > > > Â define f where "f x = P x" > > > > is (almost) the same as > > > > Â define f where "f = (%x. P x)" > > > > but for that I need > > > > Â define f where "f x = P x" for x > > > > While this is consistent with 'have ... if ... for ...' it is > > different > > from what 'definition' does, and for some reason I was expecting to > > behave 'define' very similar to 'definition' (it might have been > > the > > name ;)). Is there a specific reason that arguments of the left- > > hand > > side of 'define' are not meta-all-quantified implicitly? > > 'define' is a proof context element and 'definition' a theory > specification element. There are different policies for variable > binding: the theory language allows more sloppiness. > > There are some more differences. In some sense, 'define' is not a > really > a definition, because Hindley-Milner polymorphism is lacking. > > It might be better to think of 'define' as a variant of 'obtain' -- > the > syntax is also quite close. But 'define' is also more specific than 'obtain'. Currently the main difference btw 'define' and 'obtain' is that I do not need to specify a proof method for 'define'. It would be nice if we do not need to provide so much redundant informations (two times the name of the defined constant and two times for each parameter...) - Johannes > > Makarius > >

**Follow-Ups**:**Re: [isabelle] Isabelle2016-1-RC3 available for testing: new define command***From:*Andreas Lochbihler

**Re: [isabelle] Isabelle2016-1-RC3 available for testing: new define command***From:*Makarius

**References**:**[isabelle] Isabelle2016-1-RC3 available for testing***From:*Makarius

**Re: [isabelle] Isabelle2016-1-RC3 available for testing: new define command***From:*Christian Sternagel

**Re: [isabelle] Isabelle2016-1-RC3 available for testing: new define command***From:*Makarius

- Previous by Date: Re: [isabelle] Isabelle2016-1-RC3 available for testing: new define command
- Next by Date: Re: [isabelle] Isabelle2016-1-RC3 available for testing: moreover then have
- Previous by Thread: Re: [isabelle] Isabelle2016-1-RC3 available for testing: new define command
- Next by Thread: Re: [isabelle] Isabelle2016-1-RC3 available for testing: new define command
- Cl-isabelle-users November 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