3

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

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，但我希望有更好的方法。

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

4

3 回答 3

4

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

lemma "unat (of_nat 42) = 42"

这导致

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

现在你可以递归地做同样'a的事情'a word并且会得到

:: len
free type variable

它告诉你那'a是排序len（通过控制点击len，你可以直接跳转到这个类型类的定义，这也很方便）。

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

于 2013-03-19T02:28:58.120 回答
4

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

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

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

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

于 2013-03-19T08:56:00.527 回答
2

Running the command:

setup {* Config.put_global show_all_types true *}

seems to do the trick.

The goal unat (of_nat 3) = 3 becomes the hideous (but complete):

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))))

as desired.

It is interesting that a declare [[show_all_types]] does not work; the source looks like it should. Perhaps it is a bug in Isabelle2013?

于 2013-03-19T11:32:27.580 回答