*To*: Ramana Kumar <rk436 at cam.ac.uk>*Subject*: Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Wed, 27 Feb 2013 16:21:24 -0600*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CAMej=25_=rN--ygVsqs390-Q-Suf8WC6US95oCJ8RgnycveJ-g@mail.gmail.com>*References*: <512DD2E4.4070305@gmx.com> <512E2B19.8030705@gmx.com> <512E4902.2090507@gmx.com> <CAMej=25_=rN--ygVsqs390-Q-Suf8WC6US95oCJ8RgnycveJ-g@mail.gmail.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

Ramana, Thanks for the tip. I proved something like this: theorem name [simp]: "(A seO B) ==> (A = B)" by(metis foo) It then caused some non-terminating things to start happening.

(A = B) ====> (A seO B) --> (A = B),

My simp rule expands "seO" into the formula "(x IN A --> x IN B) & (x IN B --> x IN A)".

"(A seO B)" apply(simp).

Thanks, GB On 2/27/2013 12:26 PM, Ramana Kumar wrote:

Can't you prove "(A seO B) ==> (A = B)" and then use that theorem as arule?On Wed, Feb 27, 2013 at 5:57 PM, Gottfried Barrow<gottfried.barrow at gmx.com <mailto: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/ 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:*Lars Noschinski

**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

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

- Previous by Date: Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step
- Next by Date: [isabelle] Supporting native Unicode input in Isabelle/jEdit
- 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