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"
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
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