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?
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
