[isabelle-dev] Discovering named_theorems

[Dmitriy Traytel]

Hi all,

trying the smaller audience of isabelle-dev first.

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).

Technically, the Facts module today does not expose functions to query all the dynamic facts (mirroring the existing ones for static facts Facts.fold_static and Facts.dest_static). Concretely, I’d like to see functions a la

  val fold_dynamic: Context.generic -> (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
  val dest_dynamic: Context.generic -> bool -> T list -> T -> (string * thm list) list

and maybe also

  val fold: Context.generic -> (bool * string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
  val dest: Context.generic -> bool -> T list -> T -> (bool * string * thm list) list

which combine dynamic and static facts in Facts.

As a second step the querying tools (find_theorems, Sledgehammer, etc.) could decide what to show and what not.

Am I overlooking something fundamental, why this should/can not be done?

Dmitriy

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.