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

  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


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