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



On 25/11/16 12:02, Johannes HÃlzl wrote:
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'.

Another difference is that define'd constants may appear in show statements, but obtain'ed ones may not.

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...)
Indeed. I would also like to be able to drop the "xxx where" part. I can live with the "for" clause, though.

Andreas




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