Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]



On Thu, 22 Nov 2012, Lars Noschinski wrote:

On 22.11.2012 17:56, Makarius wrote:
* 'definition' with Pure equality (==) is quite old-fashioned. Normally
you just use HOL = or its abbreviation for bool <-> here, as you would
for 'primrec', 'fun', 'function'

(In contrast HOL --> and ! are old-fashioned/cumbersome, where Pure
==> and !! would do the job better.)

Is there actually a drawback when using == instead of = or is it a mere matter of style? I like using Pure equality because it saves me a level of parentheses when I have a binder on the right hand side.

Using == for definitions is one of these things that can be explained only historically. Many many years ago, you would have used consts/defs or even consts/axioms or even consts/rules to spell out definitional axioms using directly the == primitive of Pure. Larry explained it > 20 yeas ago as "Pure == is used to represent definitions".

If you look at modern times, a "definitional package" is some mechanism that accepts a specification (via terms or propositions) about what should be provided by the system by means of some derived definitional concept. So in 'primrec' and 'fun' you state equations, and the system will give them you as theorems (and more things), in 'inductive' you write rules about some relation, and you get them as theorems for introduction (and more things for elimination and induction).

Long ago, the old 'defs' primitive has been superseded by such a definitional package called 'definition', to do the same for basic definitions without pattern matching or recursion. So 'definition' is more like 'function' or 'theorem' than the primitive def that happens at the bottom. That foundation of the definition does use Pure == internally, but the user never has to see it in practice. In Isabelle2012 these primitive defs behind 'definition' are particulary hard to retrieve, and nobody has noticed so far :-)


	Makarius





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