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