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

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.

