[isabelle] Simplification of unique elements

Hi all!

Suppose I have some unary predicate P, and I have proved that it has a
unique satisfying solution. That is, I prove the theorem:

theorem unique [simp]: "[| P a; P b |] ==> a = b"

It seems that, even after declaring the rule as a simplification, the
rule is not always applied by Isabelle. As an example, the following
proof attempt fails.

theorem foo: "[| P a; P b |] ==> f a = f b"
apply (simp)

Alternatively, I've been doing something like

theorem foo: "[| P a; P b |] ==> f a = f b"
by (drule unique, assumption, simp)

I can see why the simplification rule wont always be applied by
Isabelle, as it would easily loop forever.

Still, what would be the best way to deal with this kind of
predicates? So that most of the deductions with them, and simple
examples such as theorem "foo", could be proved automatically?


Juan Antonio Navarro Pérez

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