isabelle - 如何查看 Isabelle 证明目标中的隐藏类型变量？

Question

在伊莎贝尔中，人们通常可以达到证明目标，其中中间类型的术语对于证明的正确性至关重要。例如，考虑以下引理，将 nat 42 转换为 'a word，然后再返回:

theory Test
imports "~~/src/HOL/Word/Word"
begin

lemma "unat (of_nat 42) = 42"
  ...

现在这个陈述的真实性取决于of_nat 42的类型:如果它是32 word，那么这个陈述就是真实的，如果它是一个 2个字，然而，这个说法是错误的。

不幸的是，我似乎无法让 Isabelle 向我显示这种中间类型。

我尝试过以下方法:

• 声明 [[show_types]]
• 声明 [[show_sorts]]
• local_setup {* Config.put show_all_types true *}

所有这些都只显示:

unat (of_nat (42::nat)) = (42::nat)

在紧要关头，人们可以这样做:

apply (tactic {* (fn t => (tracing (PolyML.makestring (prems_of t)); all_tac t))  *})

确实获取了术语的原始转储，但我希望有更好的方法。

是否有一种在证明目标中显示中间项类型的好方法？

Answer 1

在 Isabelle/jEdit 中，您始终可以将“control-hover”(即按住控制按钮并将鼠标悬停在常量上)以获得附加信息。对于 of_nat 中

lemma "unat (of_nat 42) = 42"

这会导致

constant "Nat.semiring_1_class.of_nat"
:: nat => 'a word

现在您可以对 'a word 的 'a 递归执行相同的操作，并将得到

:: len
free type variable

告诉你'a是len类型(通过按住control键点击len，你可以直接跳转到这个的定义type class，这也很方便)。

所以你的问题的答案是:是的，在 Isabelle/jEdit 中控制悬停。