查找类型的 class 的实例化

Question

在 Isabelle/HOL 中，如何找到给定 class 的给定类型的实例化位置？例如，为了 post，其中 real 被实例化为 conditionally_complete_linorder。为了证明这个问题：我可能想知道这个是为了获得类似实例化的灵感，为了向某人展示它，为了 Isabelle/HOL 练习阅读，出于好奇等等。我目前的进程：

首先，检查它实际上是：键入 instantiation real :: conditionally_complete_linorder begin end 并查看我是否收到错误消息 "No parameters and no pending instance proof obligations in instantiation."

接下来，最好在 where 之前，我需要知道 how 即它是直接的，还是通过 [=87= 隐含的]es C_1[、C_2、C_3 等]。然后，我需要找到这些实例化的位置，显式 instantiation real :: conditionally_complete_linorder 或 C_i 的隐式实例化（两种情况的过程相同）。我不知道如何找出方法，所以我必须检查显式实例化，然后检查所有可能的隐式实例化。

对于显式，我可以做一个 grep -Ern ~/.local/src/Isabelle2019 -e 'instantiation real :: conditionally_complete_linorder'（希望空格不奇怪，或者做一个更强大的搜索:)）。重复 AFP 位置。或者，留在 jEdit window:

我可以通过键入 term "x::'a::conditionally_complete_linorder" 找到 class 本身的定义位置，然后按住 Ctrl 并单击 class 名称，然后检查 real 使用 Ctrl-f 在该文件中直接实例化。
然后我可以检查它是否在定义类型 real 的地方实例化，方法是键入 term "x::real" 并按住 Ctrl 单击 real，然后按 Ctrl-f conditionally_complete_linorder 在该文件中。

（如果它在任何一个地方，它将是导入层次结构中更靠下的那个，但我发现只完成这两个步骤更简单。）但是，如果两个地方都没有打开它，那么要么无论出于何种原因，它都会在其他地方显式实例化或隐式实例化。因此 grep 更健壮。

如果显式没有任何结果，那么我会检查隐式。查看 class_deps 图，我可以看到 conditionally_complete_linorder 可以来自 complete_linorder 或 linear_continuum。然后我可以通过查看 real 是否被实例化为它们中的任何一个来继续搜索（忽略任何我碰巧知道 real 不能被实例化为）。我还可以检查它是否被实例化为 conditioanlly_complete_lattice 和 linorder，这是我所看到的 conditionally_complete_linorder 是 * 的简单（无额外假设）组合。递归地重复所有这些 classes 直到找到实例化。在这种情况下，我可以看到 linear_continuum_topology 暗示 linear_continuum，所以用 grep -Ern ~/.local/src/Isabelle2019 -e "instantiation.*real" | grep continuum 一石二鸟，找到 /path/to/.local/src/Isabelle2019/src/HOL/Real.thy:897:instantiation real :: linear_continuum.

这个过程相当繁琐。更少但仍然相当乏味**是在 Real.thy 中获取 class_deps 图表和 Ctrl-f for "instantiation real" 并寻找实例化：原始 class，它的超classes，或者暗示它的classes。然后在每个文件中定义 classes 搜索 "instantiation real"。递归执行此操作直到完成。在这种情况下，我会在 Real.thy.

中找到我需要的东西

有没有更简单的方法？希望我只是错过了一些明显的东西。

* 我无法在 Conditionally_Complete_Lattices.thy 中按住 Ctrl 并单击直接跳转到 linorder，我猜是因为它是预构建的，所以我必须执行 term "x::'a::linorder"又来了。

** 而且也不那么健壮，因为它是 minus grep-ing，它可以打开更奇怪的实例化位置，然后我再次不确定这是否会在实践中出现。

谢谢

Answer 1

您可以在下面的代码清单中导入理论，然后使用命令find_instantiations。我将留下代码而不作进一步解释，但如果您需要更多详细信息或怀疑某些地方不太正确，请随时在评论中提出更多问题。

section ‹Auxiliary commands›
theory aux_cmd
  imports Complex_Main
  keywords "find_instantiations" :: thy_decl  
begin

subsection ‹Commands›

ML ‹

fun find_instantiations ctxt c =
  let
    val {classes, ...} = ctxt |> Proof_Context.tsig_of |> Type.rep_tsig;
    val algebra = classes |> #2 
    val arities = algebra |> Sorts.arities_of;
  in  
    Symtab.lookup arities c
    |> the
    |> map #1
    |> Sorts.minimize_sort algebra
  end

fun find_instantiations_cmd tc st = 
  let
    val ctxt = Toplevel.context_of st;
    val _ = tc 
      |> Syntax.parse_typ ctxt 
      |> dest_Type 
      |> fst 
      |> find_instantiations ctxt 
      |> map Pretty.str 
      |> Pretty.writeln_chunks
  in () end

val q = Outer_Syntax.command
  \<^command_keyword>‹find_instantiations› 
  "find all instantiations of a given type constructor"
  (Parse.type_const >> (fn tc => Toplevel.keep (find_instantiations_cmd tc)));

›


subsection ‹Examples›

find_instantiations filter
find_instantiations nat
find_instantiations real

end

备注

如果您发现任何问题，我很乐意提供修正，但希望在合理的延迟下进一步回复。
该命令同时查找显式和隐式实例化，即它还查找通过使用命令 instance 或 instantiation 以外的方式实现的实例化，例如在 ML 函数中。
不幸的是，该命令没有为您提供执行实例化的文件的位置 - 这是更难以实现的事情，特别是考虑到实例化也可以通过编程方式执行。尽管如此，我相信，如果给出所有实例化的列表，几乎总是很容易使用导入理论的 in-built 搜索功能来缩小执行实例化的确切位置。

查找类型的 class 的实例化

Find the instantiation of a class for a type

isabelle