Email Gateway (Aug 22 2022 at 12:42): Email Gateway (Aug 22 2022 at 12:42):From: Buday Gergely <gbuday@karolyrobert.hu>
Hi,
in the Isar reference manual, "defines" is explained as
defines a: x ≡ t defines a previously declared parameter. This is
similar to def within a proof (cf. §6.2.1), but defines takes an
equational proposition instead of variable-term pair. The left-
hand side of the equation may have additional arguments, e.g.
“defines f x 1 ... x n ≡ t”.
This vaguely resembles section 16.5.2 Extension by constant specification in Gordon & Melham: Introduction to HOL.
Is this reference the source of inspiration for this Isar keyword?
And, is there a written account on the basic definitional mechanisms of Isabelle, explained model theoretically?
Email Gateway (Aug 22 2022 at 12:43):From: Makarius <makarius@sketis.net>
On Tue, 23 Feb 2016, Buday Gergely wrote:
in the Isar reference manual, "defines" is explained as
defines a: x ≡ t defines a previously declared parameter. This is
similar to def within a proof (cf. §6.2.1), but defines takes an
equational proposition instead of variable-term pair. The left-
hand side of the equation may have additional arguments, e.g.
“defines f x 1 ... x n ≡ t”.
The 'defines' context element is just a form to write
fixes x
assumes "x == t"
and let the system do something on export. The reference to Isar 'def'
also helps, e.g. see isar-ref section 1.4.2 "Isar context elements".
There is nothing deep going on here, just some equational assumptions and
reasoning with reflexivity.
This also means, that these poor-man's definitions are not subject to
Hindley-Milner polymorphism, because the logical context is not
polymorphic.
This vaguely resembles section 16.5.2 Extension by constant
specification in Gordon & Melham: Introduction to HOL.
Why? There is nothing about HOL or any particular logic going on here.
Especially no model-theoretic magic.
And, is there a written account on the basic definitional mechanisms of
Isabelle, explained model theoretically?
See 'def' in Isar. There is not much to say about it, so relatively little
is said in the usual texts.
Makarius
Last updated: Apr 26 2024 at 08:19 UTC