*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Thu, 28 Feb 2013 10:53:55 +0100*In-reply-to*: <512DD2E4.4070305@gmx.com>*References*: <512DD2E4.4070305@gmx.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.11) Gecko/20121122 Icedove/10.0.11

On 27.02.2013 10:33, 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.

You could a conditional rewrite rule "A <= B; B <= A ==> A = B".

-- Lars

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

- Previous by Date: Re: [isabelle] Suggesting to add common isabelle user questions to the wiki
- 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: [isabelle] Calling external provers from Isabelle
- 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