Re: [isabelle] Let's find a proof of a lemma

On Mon, Dec 20, 2010 at 1:33 PM, Victor Porton <porton at> wrote:
> Let's find a proof of the following lemma, which is forgotten in ZF theory:
> lemma right_comp_id_any: "r<=Sigma(A,B) ==> r O id(C) = restrict(r,C)"
> I think I can, spending some time, find a proof myself, but I suspect my proof won't be optimal.

This trivial lemma has a trivial proof. Just unfold the definitions
and apply auto:

lemma right_comp_id_any: "r O id(C) = restrict(r,C)"
unfolding restrict_def comp_def by auto

Notice that your assumption "r<=Sigma(A,B)" is completely irrelevant
to the conclusion, which mentions neither A nor B.

> Note that you have asked me to not send anymore missing lemmas in ZF. But this my message serves a different purpose, not to suggest its addition to ZF but to ask to help to find an elegant proof. (If you'll ask to not send messages like this, this will be the last.)

You have called this lemma "forgotten"; does this mean something
different to you than "missing"?

You might think this lemma would be a useful addition to the
Isabelle/ZF libraries, but I would suggest waiting to make such
judgments: Getting more experience writing nontrivial proofs in
Isabelle will give you a better idea of what kinds of library lemmas
are really useful. Working on a submission to the AFP would be a very
good idea.

- Brian

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