Re: [isabelle] safe for boolean equality



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. (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.)
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
1. Q
val it = () : unit
>

Jeremy






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