[isabelle-dev] Discovering named_theorems

[Dmitriy Traytel]

Hi Makarius,

> On 10 May 2016, at 22:48, Makarius <makarius at sketis.net> wrote:
> 
> On 03/03/16 14:19, Dmitriy Traytel wrote:
> 
>> I wondered whether named_theorems (or more generally all dynamic facts) deserve to be more visible. In particular when I search for
>> 
>> 	"(?a < ?c - ?b) = (?a + ?b < ?c)”
>> 
>> with find_theorems, I’d like to be reminded of algebra_simps (instead or rather in addition to Groups.ordered_ab_group_add_class.less_diff_eq).
>> 
>> Looking at the named_theorems that we have today (with grep), I see two kinds: those relevant for the working formalizer (algebra_simps, derivative_intros, ...), and those mostly relevant for tools (transfer_raw, …). It would be good to make the former ones easily discoverable (via find_theorems, potentially also Sledgehammer). If something is really irrelevant for the working formalizer, it(s binding) could in principle be concealed (preventing find_theorems from showing it).
> 
> See now the following change:
> 
> changeset:   63080:8326aa594273
> tag:         tip
> user:        wenzelm
> date:        Tue May 10 22:25:06 2016 +0200
> files:       src/Pure/Isar/proof_context.ML
> src/Pure/Tools/find_theorems.ML src/Pure/facts.ML
> description:
> find dynamic facts as well, but static ones are preferred;
> tuned;
> 
> 
> It is not precisely what you have described, but it is a
> straight-forward continuation of the existing fact retrieval.
> 
> Note that the "Duplicates" option makes a difference if dynamic facts
> actually show up. The details of these policies are from a different
> continent, and not totally clear to me.
> 
>> PS: The real reason why I am interested in this is that in the forthcoming package for non-primitive corecursion (joint work with Jasmin Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu), we would like to generate dynamic theorems for coinduction up to congruence (because the coinduction principles gets stronger with every non-primitively corecursive function defined). But this only makes sense if users are aware of those dynamic theorems, i.e. can find them easily.
> 
> Is the above sufficient for this application?

Yes, thanks!

Ticking “Duplicates” makes the result even more as I expected. But I can imagine that showing no duplicates (with static theorems preferred) is a reasonable default.

Dmitriy