如何查看在伊莎贝尔证明目标隐藏式变量？

在伊莎贝尔，经常可以击中目标，证明在中间类型的术语是一个证明的正确性至关重要。例如，请考虑以下引理转换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，然而，该声明是假的。

不幸的是，我似乎无法得到伊莎贝尔显示此中间类型的给我。

我已经试过如下：所有这些

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的原始转储，但我希望有一个更好的办法。

在证明目标中显示中间术语类型是否有很好的方法？

来源

2013-03-19 davidg

只是澄清一下：你指的是'〜/ src/HOL/Word/Word'中的'unat'，对吧？（不是说这与答案有关，但它可能有助于后来的访问者重现您的问题。） – chris 2013-03-19 02:10:32

Btw：在下面的“所有这些只是显示”我想你的意思是'42'而不是'3'？ – chris 2013-03-19 02:31:54

@chris：谢谢。我已经更新了两个。 – davidg 2013-03-19 02:47:09

在Isabelle/jEdit中，您可以随时“控制悬停”（即按住控制按钮并将鼠标悬停在某个常量上）以获取更多信息。对于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 （通过控制点击len，您可以直接跳到t的定义他的类型班，这也很方便）。

所以你的问题的答案是：是的，控制悬停在伊莎贝尔/ jEdit。

来源

2013-03-19 02:28:58 chris

感谢您的建议。我意识到这个jEdit功能，但没有想到在这种情况下使用它。我真的希望能够在输出中显示类型，所以我可以复制/粘贴结果，比较另一个术语等。 – davidg 2013-03-19 02:48:26

为了让伊莎贝尔告诉你联合国行政法庭的类型在这个例子中，要声明如下：

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

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

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

来源

2013-03-19 08:56:00 lsf37

谢谢。我不知道'show_consts'。当'show_all_types'功能过于可怕而不能考虑时，看起来很有用，但仍然意味着您不能将结果复制/粘贴到新定理中。 – davidg 2013-03-19 11:33:36

是的，复制/粘贴到新的定理中仍然是一个问题。我没有很好的解决方案。 – lsf37 2013-03-20 14:18:20

运行命令：

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中的一个错误？

来源

2013-03-19 11:32:27 davidg

错误请求和特性报告的跟踪器是'isabelle-users'邮件列表。所有这些'show_'选项都有点难以跟踪。请注意，'show_markup'从根本上改变了Isabelle/jEdit的工作方式 - 这也在NEWS和isar-ref手册中有所解释。 – Makarius 2013-03-20 20:00:53

如何查看在伊莎贝尔证明目标隐藏式变量？

回答

相关问题