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



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.


	Makarius





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