Re: [isabelle] Finding a rule



> 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!

Tobias





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