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



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 ;)).

Why care about »foo« anyway?

This I don't understand. The situation I'm talking about is

definition foo :: …
  where "foo … = (∀x. …)"

vs.

definition foo :: …
  where "foo … ≡ ∀x. …"

(there are also other cases)

  -- Lars





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