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

Question

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

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

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

现在这个陈述的真假取决于of_nat 42的类型：如果是32 word，那么这个陈述是真的，如果是一个2 word，那么这个陈述就是假的。

很遗憾，我似乎无法让 Isabelle 向我展示这种中间类型。

我尝试了以下方法：

• declare [[show_types]]
• declare [[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))  *})

获取term 的原始转储，但我希望有更好的方法。

有没有在证明目标中显示中间项类型的好方法？

Answer 1

在 Isabelle/jEdit 中，您始终可以将“控制悬停”（即按住控制按钮并将鼠标悬停）悬停在一个常数上以获得更多信息。对于of_nat in

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（通过控制点击len，你可以直接跳转到这个类型类的定义，这也很方便）。

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

Answer 2

为了让 Isabelle 在本例中向您展示 unat 的类型，您需要声明以下内容：

  declare [[show_types]]
  declare [[show_sorts]]
  declare [[show_consts]]

最后一行在输出窗口中打印目标中使用的每个常量的类型。这在 jEdit 和 ProofGeneral 中都有效。

这个解决方案有一个问题：如果 unat 以不同的类型多次出现，它会打印所有这些实例，但它不会告诉你哪个类型的实例是哪个出现的。不过，除了 jEdit 悬停之外，我不知道任何解决方案。

Answer 3

运行命令：

setup {* Config.put_global show_all_types true *}

似乎可以解决问题。

目标unat (of_nat 3) = 3 变得可怕（但完整）：

goal (1 subgoal):
 1. (Trueprop::bool => prop)
     ((op =::nat => nat => bool)
       ((unat::'a word => nat)
         ((of_nat::nat => 'a word)
           ((numeral::num => nat)
             ((num.Bit1::num => num) (num.One::num)))))
       ((numeral::num => nat)
         ((num.Bit1::num => num) (num.One::num))))

根据需要。

有趣的是declare [[show_all_types]] 不起作用；来源看起来应该。也许这是 Isabelle2013 中的一个错误？