*To*: cl-isabelle-users at lists.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 11:57:22 -0600*In-reply-to*: <512E2B19.8030705@gmx.com>*References*: <512DD2E4.4070305@gmx.com> <512E2B19.8030705@gmx.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

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.

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 "=", abinary operator "seO", and a theorem "ssO":theorem "A = B" proof- have "A seO B" by(simp) thus "A = B" by(metis ssO_eq) qedI'm learning proof techniques on an as-need basis, where Sledgehammerand 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 mehow 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 stepproofs with "by(simp)".However, there's one common proof which I can't figure out how to getin 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 dobecause 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" ismy main equality "A=B", so I'm blank on how I can automate theconnection between the two.I attach a PDF. On page 7, Notation 3.1.10, I create an abbreviationfor "A is a subset of B and B is a subset of A". On page 8 is myTheorem 3.1.12 which shows that "A is a subset of B and B is a subsetof A" is equivalent to "A=B".My theory is filling up with proofs to theorems in which I state aproof 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 getequality 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 toshow 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:*Ramana Kumar

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

- Previous by Date: [isabelle] Reminder: CICM/MKM deadline approaching
- 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