Email Gateway (Aug 18 2022 at 12:08): Email Gateway (Aug 18 2022 at 12:08):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Hi,
when using Isabelle's feature to search for theorems I frequently use
the "intro" command instead of a pattern to find the appropriate
introduction rule for inductively defined sets. Actually, I would like
to get the names of the introduction rules that match, i.e. those names
that I explicitly gave these rules in the inductive declaration.
However, the search result does not contain these names, but
....intros(23): ..., ....intros(34): ..., etc., which is not what I
wanted in the first place because the rules' positions in the inductive
definition are not stable when I add/delete/move some rules.
Is there some switch in Isabelle 2008 to make Isabelle display the
rules' names that are given explicitly in the inductive definition?
As a concrete example, take
lemma "(a, a) : r^*"
Doing a search for "intro" theorems, this gives (among many others)
Transitive_Closure.rtrancl.intros(1): (?a, ?a) : r^*
However, I would like to get:
Transitive_Closure.rtrancl.rtrancl_refl: (?a, ?a) : r^*
Andreas
Email Gateway (Aug 18 2022 at 12:08):From: Gerwin Klein <gerwin.klein@nicta.com.au>
Hi Andreas,
Andreas Loc
The search tries to return the shortest name (although it should actually
prefer names without numbers). To get all names that match, try the with_dups
option in the xemacs minibuffer, i.e. say:
(with_dups) intro
Cheers,
Gerwin
Email Gateway (Aug 18 2022 at 12:09):From: Brian Huffman <brianh@cs.pdx.edu>
Quoting Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>:
As a concrete example, take
lemma "(a, a) : r^*"
Doing a search for "intro" theorems, this gives (among many others)
Transitive_Closure.rtrancl.intros(1): (?a, ?a) : r^*However, I would like to get:
Transitive_Closure.rtrancl.rtrancl_refl: (?a, ?a) : r^*Andreas
Quoting Gerwin Klein <gerwin.klein@nicta.com.au>:
The search tries to return the shortest name (although it should
actually prefer names without numbers).
Indeed, it should prefer names without numbers, even if they have
longer names. I had noticed this problem before, and even coded up a
solution for it, but I never got around to cleaning up the code and
checking it in until now.
The fix is now in cvs, or you can get it in the next developer's snapshot.
Email Gateway (Aug 18 2022 at 12:09):From: Makarius <makarius@sketis.net>
Note that using the development snapshot for real work is generally a bad
idea. Especially after an official stable release we tend to throw in
many testing-unstable things.
In this particular case of a very small change it might be better to adapt
your official version manually, if you really care about that feature.
Brian's change can be accessed here:
http://isabelle.in.tum.de/isabelle-bin/mercurial.cgi/rev/084dfd231125
Makarius
Email Gateway (Aug 18 2022 at 12:09):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Thanks a lot for the change, the names now look very nice.
Meanwhile, I came, however, across another issue:
Actually, I would expect that searching for "intro" theorems should
return a list of all theorems
that unify with the current goal's conclusion, i.e. every rule that can
be applied with rule in
the current state should be found and everything that is found should be
applicable in that way. However, this apparently is not true:
For example, if the current goal is
"(?a, a) : r^*"
then if I do a search for "intro", this does not give
Transitive_Closure.rtrancl.rtrancl_refl
because ?a would have to be instantiated to a, although
apply(rule rtrancl.rtrancl_refl)
correctly instantiates ?a to a. Since unification can potentially be
expensive, it is sensible for find not to try to instantiate by default.
But is there a switch to make "find intro" print all rules that unify,
i.e. for both
"(?a, a) : r^*" and "!!a. (?a a, a) : r^*"
it should return Transitive_Closure.rtrancl.rtrancl_refl, but not for
"!!a. (?a, a) : r^*".
If this is not possible, is there a shortcut (like intro) which searches
in the conclusions for the pattern that is obtained from the current
conclusion by replacing all ?-terms with _, i.e. rtrancl_refl is found
for all three goals in the previous paragraph.
Andreas
Last updated: May 03 2024 at 04:19 UTC