*To*: René Neumann <rene.neumann at in.tum.de>*Subject*: Re: [isabelle] Proving set equality -- set-up question*From*: Makarius <makarius at sketis.net>*Date*: Tue, 4 Dec 2012 21:16:07 +0100 (CET)*Cc*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <50BE1372.1020602@in.tum.de>*References*: <50BE1372.1020602@in.tum.de>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Tue, 4 Dec 2012, René Neumann wrote:

when proving some set equality "A = B", I'd like to use a lemma like lemma set_eqI__comp: (* = subset_antisym[OF subsetI subsetI] *) "⟦ ⋀x. x ∈ A ⟹ x ∈ B; ⋀x. x ∈ B ⟹ x ∈ A ⟧ ⟹ A = B" by blast Unfortunately, this is not in the regular intro-set, hence "proof" would apply subset_antisym only, requiring a little bit more boilerplate to reach the final setup. Before I put such a rule in my Misc.thy with a nice [intro!], I'd like to ask if there is a reason not to: Because, normally there is a reason for something being the way it is in Isabelle/HOL :)

In the worst case it is a historical reason ... but not here.

Makarius

**References**:**[isabelle] Proving set equality -- set-up question***From:*René Neumann

- Previous by Date: Re: [isabelle] Indexed Sum/Product Operator
- Next by Date: Re: [isabelle] Indexed Sum/Product Operator
- Previous by Thread: [isabelle] Proving set equality -- set-up question
- Next by Thread: [isabelle] Launch of Elbe 1.63
- Cl-isabelle-users December 2012 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