*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 09:49:45 -0600*In-reply-to*: <512DD2E4.4070305@gmx.com>*References*: <512DD2E4.4070305@gmx.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

I'll simplify my question.

theorem "A = B" proof- have "A seO B" by(simp) thus "A = B" by(metis ssO_eq) qed

Is there some way I can automate that specific proof template?

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 "Ais a subset of B and B is a subset of A", which I have to do becausethe 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. Thenon page 39, there's the examples that show how I can get equality withmy "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:*Gottfried Barrow

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

- Previous by Date: [isabelle] Calling external provers from Isabelle
- Next by Date: Re: [isabelle] Calling external provers from Isabelle
- Previous by Thread: [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