Re: [isabelle] Finding theorems via intro



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

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 snapshot.

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









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