Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] safe for boolean equality

Email Gateway (Aug 18 2022 at 15:28):

From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
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. What is the
rule for
splitting a boolean equality in two implications.

Best regards,

Viorel Preoteasa

Email Gateway (Aug 18 2022 at 15:29):

From: Brian Huffman <brianh@cs.pdx.edu>
On Thu, Jun 10, 2010 at 12:43 AM, Viorel Preoteasa
<viorel.preoteasa@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

Email Gateway (Aug 18 2022 at 15:29):

From: Lawrence Paulson <lp15@cam.ac.uk>
Equalities involving constants have never been eliminated in this way. The equality must involve a variable, free or bound. The method has no way of knowing about constraints on the variable that are not part of the goal. In the case of a structured proof, it would be appropriate and natural to insert relevant inequalities with an appropriate “using” clause.

The problem with locale constants is that they look like free variables to this 15 year old code. We need to look at whether there is a way for this code to identify locale constants and to treat them as such.

Larry Paulson

Email Gateway (Aug 18 2022 at 15:30):

From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Brian Huffman wrote:
It also happens in the following situation, in addition to the situation
Brian mentions:

goal Main.thy "P ==> P = Q --> Q" ;
Level 0 (1 subgoal)
P = Q --> Q

1. P = Q --> Q
   val it = ["P" [.]] : Thm.thm list

   by Safe_tac ;
   Level 1 (1 subgoal)
   P = Q --> Q

2. Q
   val it = () : unit
   >

Jeremy

Last updated: Apr 26 2024 at 16:20 UTC