[isabelle-dev] Find_Theorems interface

Peter Lammich lammich at in.tum.de
Sat Nov 13 18:02:29 CET 2021


I noticed that the Find_Theorems signature does not allow 
to decouple the filtering of the theorems from the obtaining of the
unfiltered 'master' list of theorems.

This yields to me being forced to duplicate the filtering code, just to
filter over another source of theorems.

My use-case:

  find_in_theorems <filters> in <fact_refs>

to search in explicitly stated theorems, e.g.

  find_in_theorems "_+_" in algebra_simps


  Find_Theorems hides filtering, and only exposes combined function
that filters all theorems from context.

Proposed solution:
  add filter_theorems and filter_theorems_cmd to FIND_THEOREMS

This has proved a very valuable tool for searching large fact
databases, such as Hoare-rules in my Isabelle-LLVM project. 
Back then, I simply copy-pasted the code from find_in_theorems, but now
stumbled over the code-duplication again as some changes are necessary
to transition to 2021-1.

Please advise me if I should simply commit such a change (and hopefully
remember it on the next release, when I can use it from my tools (that
work on release versions)), or how to get such a change in, or if the
strong hiding is intentional, and I have to live with the code


More information about the isabelle-dev mailing list