*To*: Gottfried Barrow <gottfried.barrow at gmx.com>*Subject*: Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step*From*: Ramana Kumar <rk436 at cam.ac.uk>*Date*: Wed, 27 Feb 2013 18:26:50 +0000*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <512E4902.2090507@gmx.com>*References*: <512DD2E4.4070305@gmx.com> <512E2B19.8030705@gmx.com> <512E4902.2090507@gmx.com>*Sender*: ramana.kumar at gmail.com

Can't you prove "(A seO B) ==> (A = B)" and then use that theorem as a rule? On Wed, Feb 27, 2013 at 5:57 PM, Gottfried Barrow <gottfried.barrow at gmx.com>wrote: > I guess the answer might be in the The Isabelle Cookbook. > > http://www.inf.kcl.ac.uk/**staff/urbanc/Cookbook/<http://www.inf.kcl.ac.uk/staff/urbanc/Cookbook/> > > Maybe in chapter 6, Tactical Reasoning. > > So far, I've enjoyed only needing a bare bones structured proof, or only a > "by(metis...)" proof that Sledgehammer found for me. > > But having to frequently have 7 lines for a proof, which is really only > about 4 or 5 lines of proof, that's weighing heavy on me. > > If someone wants to give me the ML to implement the 7 lines of proof > below, that would be good, but then, maybe to automate it, tactics are > needed. I wouldn't know anything about tactics. > > Regards, > GB > > > > On 2/27/2013 9:49 AM, Gottfried Barrow wrote: > >> I'll simplify my question. >> >> I have a very common theorem and proof pattern which uses "=", a binary >> operator "seO", and a theorem "ssO": >> >> theorem "A = B" >> proof- have >> "A seO B" >> by(simp) >> thus >> "A = B" >> by(metis ssO_eq) >> qed >> >> I'm learning proof techniques on an as-need basis, where Sledgehammer and >> metis have dramatically reduced the "need" in "as-need". >> >> Is there some way I can automate that specific proof template? >> >> Can I do that in ML? Is there an example somewhere that will show me how >> to do it? >> >> I can't set up a simp rule for the formula "(A seO B) = (A = B)" because >> it's exactly "(A seO B)" that I have to prove to get "(A = B)". >> >> Thanks, >> GB >> >> On 2/27/2013 3:33 AM, Gottfried Barrow wrote: >> >>> Hi, >>> >>> I've set up a bunch of simp rules, and I'm getting lots of 1 step proofs >>> with "by(simp)". >>> >>> However, there's one common proof which I can't figure out how to get in >>> 1 step, which is set equality for the case where I have to prove "A is a >>> subset of B and B is a subset of A", which I have to do because the auto >>> provers can't prove "A = B" directly. >>> >>> The problem is that my "A is a subset of B and B is a subset of A" is my >>> main equality "A=B", so I'm blank on how I can automate the connection >>> between the two. >>> >>> I attach a PDF. On page 7, Notation 3.1.10, I create an abbreviation for >>> "A is a subset of B and B is a subset of A". On page 8 is my Theorem 3.1.12 >>> which shows that "A is a subset of B and B is a subset of A" is equivalent >>> to "A=B". >>> >>> My theory is filling up with proofs to theorems in which I state a proof >>> step with my "equal subsets" operator, prove it with "by(simp)", and then >>> have to finish it off with the Theorem 3.1.12. >>> >>> Starting on page 37, there's 6 out of 7 theorems where I do that. Then >>> on page 39, there's the examples that show how I can get equality with my >>> "equal subsets" operator, but not with the normal "=". >>> >>> That's related to the main reason I care, which is that I'd like to show >>> finite set equality using only one automatic proof method command. >>> >>> If anyone can tell me how to do that, I'd appreciate it. >>> >>> Regards, >>> GB >>> >>> >>> >> >> >> > >

**Follow-Ups**:**Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step***From:*Gottfried Barrow

**References**:**[isabelle] Trying to reduce equality proofs from 2 to 1 step***From:*Gottfried Barrow

**Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step***From:*Gottfried Barrow

**Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step***From:*Gottfried Barrow

- Previous by Date: Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step
- Next by Date: Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step
- Previous by Thread: Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step
- Next by Thread: Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step
- Cl-isabelle-users February 2013 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