Re: [isabelle] Finding theorems via intro
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Finding theorems via intro
- From: Andreas Lochbihler <lochbihl at ipd.info.uni-karlsruhe.de>
- Date: Tue, 08 Jul 2008 07:37:07 +0200
- In-reply-to: <firstname.lastname@example.org>
- References: <email@example.com>
- User-agent: Thunderbird 188.8.131.52 (X11/20080502)
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
because ?a would have to be instantiated to a, although
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.
Quoting Makarius <makarius at sketis.net>:
Quoting Andreas Lochbihler <lochbihl at ipd.info.uni-karlsruhe.de>:
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^*
Quoting Gerwin Klein <gerwin.klein at nicta.com.au>:
The search tries to return the shortest name (although it should
actually prefer names without numbers).
The fix is now in cvs, or you can get it in the next developer's
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:
This archive was generated by a fusion of
Pipermail (Mailman edition) and