*To*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Subject*: Re: [isabelle] safe for boolean equality*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Mon, 14 Jun 2010 07:24:20 -0700*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4C109794.3020100@abo.fi>*References*: <4C109794.3020100@abo.fi>*Sender*: huffman.brian.c at gmail.com

On Thu, Jun 10, 2010 at 12:43 AM, Viorel Preoteasa <viorel.preoteasa at abo.fi> 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.) https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2007-February/msg00075.html https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2007-February/msg00076.html > 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

**Follow-Ups**:**Re: [isabelle] safe for boolean equality***From:*Lawrence Paulson

**Re: [isabelle] safe for boolean equality***From:*Jeremy Dawson

**References**:**[isabelle] safe for boolean equality***From:*Viorel Preoteasa

- Previous by Date: Re: [isabelle] Code generator: overloaded numeric constants
- Next by Date: [isabelle] isabelle-process
- Previous by Thread: [isabelle] safe for boolean equality
- Next by Thread: Re: [isabelle] safe for boolean equality
- Cl-isabelle-users June 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list