*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Proving set equality -- set-up question*From*: René Neumann <rene.neumann at in.tum.de>*Date*: Tue, 04 Dec 2012 16:14:58 +0100*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/17.0 Thunderbird/17.0

Hi, 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 :) Thanks, René -- René Neumann Institut für Informatik (I7) Technische Universität München Boltzmannstr. 3 85748 Garching b. München Tel: +49-89-289-17232 Office: MI 03.11.055

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] Proving set equality -- set-up question***From:*Makarius

- Previous by Date: Re: [isabelle] Indexed Sum/Product Operator
- Next by Date: Re: [isabelle] nat_code Equation
- Previous by Thread: Re: [isabelle] Indexed Sum/Product Operator
- Next by Thread: Re: [isabelle] Proving set equality -- set-up question
- 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