[isabelle-dev] [isabelle] safe for boolean equality

[Lawrence Paulson]

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


On 14 Jun 2010, at 15:24, Brian Huffman wrote:

> 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.