2

我希望为 Isabelle 理论（例如 HOL 会话）生成 HTML 文档，但不包括证明。

也就是说，我想制作像http://isabelle.in.tum.de/library/HOL/Nat.html这样的页面 ，而不是，例如，

lemma diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
  apply (rule_tac x = m in spec)
  apply (induct n)
  prefer 2
  apply (rule allI)
  apply (induct_tac x, iprover+)
  done

我只想看

lemma diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"

原因是我使用 HTML 页面来查看可用的定理，但在这种情况下，证明只会分散注意力。（我知道在生成 PDF 时可以省略证明，但我对 HTML 文档特别感兴趣。）

4

2 回答 2

1

不幸的是，目前在 Isabelle 中没有内置的方法来执行此操作（HTML 生成在几年前曾经包含一个摘要，但现在不再提供）。

您可以考虑对生成的 HTML 文件进行后处理，但这比听起来要复杂得多。

您目前最好的选择是大纲 PDF，并且正如 Chris 建议的那样，使用类似的命令

find_theorems name: "MyThy."

得到理论上所有定理的列表MyThy。您可以使用术语表达式或仅使用常量名称来扩充find_theorems命令，以将搜索范围缩小到特定常量。这通常比浏览一长串定理更有效。您可以类似地使用该命令find_consts按类型、常量名称或理论名称查找常量，例如，获取在一个理论中定义的所有常量的列表。

于 2013-08-14T09:52:29.280 回答
0

我最近遇到了coqdoc输出，并且可以从这个角度理解这个问题，尽管 Coq HTML 页面现在也显示了它们的年龄。

在 Isabelle 中，HTML 演示曾经非常重要，然后其他工具（如在线find_theorems或离线 PDF 文档）变得更加强大和有用，现在还有 Isabelle/jEdit，其显示质量与 Isabelle HTML 输出最初出现时的 HTML 浏览器相似实施的。

我不知道有一种简单的方法可以在当代 Isabelle2013 中获得您所要求的内容，但这并非不可能，主要需要对旧东西进行一些翻新以适应新概念。由于现在使用静态网页进行 HTML 浏览有点过时，因此到目前为止还没有得到优先考虑。

无论如何，Isabelle/Scala（这是官方的 Isabelle 系统编程接口）已经提供了一些公共 API 操作来从您在 Isabelle/jEdit 中在线看到的 PIDE 文档标记中获取 XML 树。对于了解该业务的人来说，从那里到一些 HTML + CSS 并不是很远。不过，在 Isabelle/jEdit 中进行一些演示可能会更快、更有用，从而绕过众多 Web 浏览器及其怪癖。

于 2013-10-09T20:32:54.230 回答