# Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step

*To*: cl-isabelle-users at lists.cam.ac.uk
*Subject*: Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step
*From*: Thomas Sewell <Thomas.Sewell at nicta.com.au>
*Date*: Fri, 01 Mar 2013 13:41:47 +1100
*In-reply-to*: <512F2933.5020605@in.tum.de>
*References*: <512DD2E4.4070305@gmx.com> <512F2933.5020605@in.tum.de>
*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:11.0) Gecko/20120410 Thunderbird/11.0.1

`I think that the problem with providing "A <= B; B <= A ==> A = B" as a
``conditional rewrite rule is that the simplifier will (probably) see this
``as a rule for rewriting A into B rather than a rule for rewriting "A =
``B" into True. This is too general, it will be applied anywhere there is
``an A with an appropriate type.
`

`One solution is to resolve your rule with Eq_TrueI, for instance, "thm
``equalityI[THEN Eq_TrueI]". Your rule should then look like "A <= B; B <=
``A ==> (A = B) == True", which strongly suggests to the simplifier that
``it should be used only for rewriting actual equalities.
`

`For some reason the system seems to figure this out by itself when given
``the equalityI rule from HOL, which may invalidate this comment.
`
Yours,
Thomas.

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