Re: [isabelle] Finding a rule

Hi Tobias,

I too have found the expanded find functionality very useful! I did have a question about it, though: Does the "intro" keyword find all theorems matching the subgoal's conclusion, or just those that have been declared as intro rules? If not, then it would nice to be able to also find introduction rules that haven't been declared such, and similarly for destruction and elimination rules.


On Feb 9, 2006, at 1:31 AM, nipkow at wrote:

I use Isabelle/Isar with ProofGeneral, and I feel sure that at one
time I knew how to find all of the rules/theorems that matched a
certain goal.  I can no longer figure out how to do this.

A good thing you asked because this feature has indeed changed and much improved but users may have missed it. In the latest version of the tutorial
you find the documentation on pages 33 and 95.
This is what the NEWS file had to say about it:

* Command 'find_theorems' searches for a list of criteria instead of a
list of constants. Known criteria are: intro, elim, dest, name:string,
simp:term, and any term. Criteria can be preceded by '-' to select
theorems that do not match. Intro, elim, dest select theorems that
match the current goal, name:s selects theorems whose fully qualified
name contain s, and simp:term selects all simplification rules whose
lhs match term.  Any other term is interpreted as pattern and selects
all theorems matching the pattern. Available in ProofGeneral under
'ProofGeneral -> Find Theorems' or C-c C-f.  Example:

  C-c C-f (100) "(_::nat) + _ + _" intro -name: "HOL."

prints the last 100 theorems matching the pattern "(_::nat) + _ + _",
matching the current goal as introduction rule and not having "HOL."
in their name (i.e. not being defined in theory HOL).

You want the criterion 'intro'.

I find that searching for thms by patterns has become an absolutely
indispensible tool in my work. Enjoy!


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