Email Gateway (Aug 19 2022 at 09:27): Email Gateway (Aug 19 2022 at 09:27):From: René Neumann <rene.neumann@in.tum.de>
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é
smime.p7s
Email Gateway (Aug 19 2022 at 09:27):From: Makarius <makarius@sketis.net>
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).
Makarius
Last updated: Apr 25 2024 at 08:20 UTC