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

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.

I can't say on the spot if and how that rule can be made implicit as some form of intro in a central place.

Note that "the regular intro-set" actually consists of several sub-parts with different priorities. There is even a split into Pure.intro and HOL.intro etc. Various tools project from that information in slightly different ways.

You say "nice" [intro!] but that would affect automated tools, splitting up goals in an aggressive way without backtracking. It will probably mess-up the normal automated process of fast, blast, auto. Larry introduced these concepts quite successfully some decades ago, and I recently refurbished his old reference manual. In Isabelle2012 it is chapter "9.4 The Classical Reasoner" in the isar-ref manual for the core concepts of intro/elim/dest.

The single "rule" steps of 'proof' and '..' use the intro/elim/dest declarations slightly differently. Pure.intro/elim/dest allow to provide further single-step rules without affecting the automated tools. So you probably need one of these here.

It requires some experimentation and study of the existing rule declarations what works smoothly for most applications. See also the print_claset and print_rules commands (although they will swamp you with tons of output).


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