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 25 2022 at 02:35 UTC