Re: [isabelle] safe for boolean equality

On Thu, Jun 10, 2010 at 12:43 AM, Viorel Preoteasa
<viorel.preoteasa at> wrote:
> Hello,
> 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.

The problem is that safe tries to be helpful by eliminating equalities
from the assumptions, unfolding them in the rest of the subgoal. In
this case the assumption "(op l-> ) = (op r->)" in goal 2 is
eliminated; since "op |->" does not appear in the rest of the subgoal,
the equality just goes away. This is often a reasonable behavior for
free variables, but it is NOT generally safe for variables fixed in
locales or structured proofs, and it is certainly not generally safe
for constants. This undesirable behavior has been noted before on the
list, and I would consider it a bug. (I really wish we had some kind
of issue-tracking system for such things, since they seem to be so
quickly forgotten after being mentioned on the mailing list.)

> What is the rule
> for
> splitting a boolean equality in two implications.

You can use "apply (rule iffI)" or even just "apply rule". Either of
these should result in the two subgoals that you expect.

> Best regards,
> Viorel Preoteasa

- Brian

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