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 18:41, Florian Haftmann wrote:
(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.

It is simpler:

a) Uniformity
b) Less symbols

Ok, these are stylistic reasons and both only hold when always using =, and not <-> (<-> can be used for all of definition, primrec, fun(ction), but only for boolean valued functions. And I don't like it for definitions anyway ;)).

Recall that 'definition', 'primrec', 'fun', 'function' are all the same category of "derived definitional concept", although of different strength and power invested in the mechanisms behind it.


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