Re: [isabelle] Isabelle2016-1-RC3 available for testing: new define command
On 25/11/16 12:02, Johannes HÃlzl wrote:
Another difference is that define'd constants may appear in show statements, but obtain'ed
ones may not.
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)
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
from what 'definition' does, and for some reason I was expecting to
behave 'define' very similar to 'definition' (it might have been
name ;)). Is there a specific reason that arguments of the left-
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
a definition, because Hindley-Milner polymorphism is lacking.
It might be better to think of 'define' as a variant of 'obtain' --
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'.
Indeed. I would also like to be able to drop the "xxx where" part. I can live with the
"for" clause, though.
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...)
This archive was generated by a fusion of
Pipermail (Mailman edition) and