Email Gateway (Aug 22 2022 at 14:27): Email Gateway (Aug 22 2022 at 14:27):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Makarius,
I was replacing some 'def "f == %x. P x"' by the new 'define' command
and have two comments:
1) For 'definition' the constant name and the 'where' can be dropped, e.g.,
definition "f = ..."
I do this a lot, because
definition f where "f = ..."
seems a bit silly (I mostly do this whenever I deem the type of "f" to
be so obvious that I do not want to state it explicitly). I would like
to have the same option also for 'define'.
2) 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?
cheers
chris
Email Gateway (Aug 22 2022 at 14:27):From: Makarius <makarius@sketis.net>
'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
Email Gateway (Aug 22 2022 at 14:27):From: Johannes Hölzl <hoelzl@in.tum.de>
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)
thatdefine 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...)
Makarius
Email Gateway (Aug 22 2022 at 14:27):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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)
thatdefine 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
Email Gateway (Aug 22 2022 at 14:28):From: Makarius <makarius@sketis.net>
These Isar proof context policies are important for the purity and
clarity of the language.
In Isar 2016 there has been clarification towards proper use of Isar in
various respects. Overall, the text becomes shorter and only in a few
cases a bit longer.
I recommend to buy the whole package, and not look back on older forms.
Makarius
Last updated: Apr 26 2024 at 20:16 UTC