Re: [isabelle] reasoning with even and odd numbers





On 19/10/2014 19:52, Amarin Phaosawasdi wrote:

One possibility:

lemma "ev 4"
using evSS[OF evSS[OF ev0]]
by(simp add: numeral_eq_Suc)

Thank you.

Is there a difference between using a proof vs adding it to simp like this?

Yes, with "using" the fact becomes part of the proof state and is simplified itself.

Tobias

lemma "ev 4"
by (simp add: numeral_eq_Suc evSS[OF evSS[OF ev0]])

Amarin


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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