Re: [isabelle] keyword defines
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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and