[isabelle] safe for boolean equality


I have a lemma which states the equality of two boolean values:

lemma (in algebra) commutative: "(! a b . a * b = b * a) = ((op l->) = (op r->))";

If I use apply safe on this I get two sub-goals:

1. (! a b . a * b = b * a) ==> (op l-> ) = (op r->)
2. /\ a b . a * b = b * a

The first sub-goal is provable, but the second is too weak. What is the rule for
splitting a boolean equality in two implications.

Best regards,

Viorel Preoteasa

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