From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,
I would like to understand if there exist Isabelle/ML functions for local
varification/unvarification of types/terms/theorems in any of the publicly
available Isabelle libraries (of course, I would expect such functions to
handle mixed schematic/fixed type/term variables in a type/term/theorem,
and take into account the names in the context and the names that occur in
the type/term/theorem that is being varified/unvarified). For example,
consider the following problem:
definition "test x = (SOME x. True)"
context
fixes x :: 'a
begin
definition "test_of_a = test x"
ML‹
val thm = Thm.full_prop_of @{thm test_of_a_def}
val out = try Logic.unvarify_global thm (NONE)
val out' = try Logic.varify_global thm (NONE)
›
end
While it is not very difficult to develop this functionality, it seems like
a good candidate for something already available. However, I was not able
to find anything similar to the functionality that I seek after a
reasonably thorough search of the Isabelle/ML source code. Of course, if
anyone familiar with the Isabelle/ML source code is confident that the
functionality that I seek is not available in the standard distribution, I
would highly appreciate a confirmation.
Kind Regards,
Mikhail Chekhov
Last updated: Jan 04 2025 at 20:18 UTC