[isabelle] Proving set equality -- set-up question


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 :)


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
Description: S/MIME Kryptografische Unterschrift

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.