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



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
> 
> 




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