Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Local varification/unvarification in Isabelle/ML?


view this post on Zulip Email Gateway (Nov 18 2020 at 00:09):

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: Dec 05 2021 at 23:19 UTC