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

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.

BTW, the shortest structured proof that is not a script looks like

lemma A unfolding a_def b_def c_def auto

To avoid confusion: There is a "by" missing:

lemma A unfolding a_def b_def c_def by auto

The Isar method "contradiction" allows to present to two preconditions
in either order -- this often happens in practice. For notE the negated
formula has to come first, to eliminate it properly.

Never saw this method before. I'll have a look.

  -- Lars

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