*To*: Victor Porton <porton at narod.ru>*Subject*: Re: [isabelle] Let's find a proof of a lemma*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Mon, 20 Dec 2010 14:33:02 -0800*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <359421292882808@web97.yandex.ru>*References*: <493641292880787@web77.yandex.ru> <AANLkTi=PQJh2otXJP+wFuUeUWSsrpd5ft8jP+88pzp8M@mail.gmail.com> <359421292882808@web97.yandex.ru>*Sender*: huffman.brian.c at gmail.com

2010/12/20 Victor Porton <porton at narod.ru>: > 21.12.2010, 00:58, "Brian Huffman" <brianh at cs.pdx.edu>: >> On Mon, Dec 20, 2010 at 1:33 PM, Victor Porton <porton at narod.ru>; 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 > > Thanks for your proof. I would not find a short proof myself. > Can you teach me how to find such short proofs? Has it appeared as a simple experiment (let's try "unfolding restrict_def comp_def by auto") or there are some deep magic behind? There is no magic; this proof was practically the first thing I tried. In general it is often a good idea to start by trying an automatic tactic like "auto"; sometimes you will get lucky. If "auto" can't succeed on its own, then unfolding some definitions first often helps. Here auto doesn't know any rules about "restrict", so we need to unfold its definition. It turns out that auto *does* have some rules about "O", so we don't really need to unfold that one (see compI and compE from ZF/Perm.thy). lemma right_comp_id_any: "r O id(C) = restrict(r,C)" unfolding restrict_def by auto A useful addition to the ZF libraries might be to add rules about "restrict" so that auto can do this proof all by itself. Here are some new lemmas restrictI and restrictE (compare these to compI and compE): lemma restrictI [intro!]: "[| <x, y> : r; x : A |] ==> <x, y> : restrict(r, A)" unfolding restrict_def by auto lemma restrictE [elim!]: "[| xy : restrict(r, A); !!x y. [| xy = <x, y>; <x, y> : r; x : A |] ==> P |] ==> P" unfolding restrict_def by auto With these rules declared with the intro and elim attributes, auto can now prove your lemma in one step: lemma right_comp_id_any: "r O id(C) = restrict(r,C)" by auto Rules restrictI and restrictE are the kinds of lemmas that make good additions to libraries: they make other proofs easier and more automatic. Learning to recognize and create useful lemmas like this will come with experience. - Brian

**References**:**[isabelle] Let's find a proof of a lemma***From:*Victor Porton

**Re: [isabelle] Let's find a proof of a lemma***From:*Brian Huffman

**Re: [isabelle] Let's find a proof of a lemma***From:*Victor Porton

- Previous by Date: Re: [isabelle] Let's find a proof of a lemma
- Next by Date: [isabelle] TACL 2011, first call for papers
- Previous by Thread: Re: [isabelle] Let's find a proof of a lemma
- Next by Thread: [isabelle] TACL 2011, first call for papers
- Cl-isabelle-users December 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list