Isabelle/HOL基础
我看过很多有关Isabelle语法和证明策略的文档，但是很少找到关于它基础的资料。我有一些问题，如果有人能抽出时间回答，我会非常感激： 为什么Isabelle/HOL不允许不终止的函数？许多其他语言，如Haskell，允许非终止函数。 哪些符号是Isabelle元语言的一部分？我读到元语言...
如何从Isabelle/HOL生成LaTeX？
我该如何使用Isabelle/HOL从源理论文件自动生成LaTeX? Isabelle/HOL的tutorial.pdf非常漂亮。我将在LaTeX中写一篇包含大量Isabelle代码的论文。
如何逐步查看Isabelle“证明”的推理过程
最近我开始学习Isabelle，但是我找不到一个非常重要的问题的答案：如何看到Isabelle找到的'proofs'逐步推理的过程？我对"by auto"或"using Theorem_A by blast"这样的语句不满意，我想检查每个步骤的推导。当然，我已经学会了关于Isar 'proof...
如何在Isabelle中以其他格式（如S表达式、Json格式等）打印状态（即待证明的子目标）？
在Isabelle中，命令print_state可以打印需要证明的当前目标。然而，我希望将目标以其他易于处理的格式打印，例如S表达式和抽象语法树。 默认的打印模式不包括此类格式，因此我想知道如何修改Isabelle内部的ML文件。更具体地说，当前目标是如何传递以进行打印的。在传递给打印函数之...
在Isabelle中使用矛盾证明的惯用方法？
到目前为止，我在Isabelle 中使用Jeremy Siek 提出的以下方式来写矛盾证明（使用这个模式）： lemma "<expression>" proof - { assume "¬ <expression>" then have Fals...
如何在Isabelle/Isar证明中使第二种情况的假设显式地呈现出来？
我有一个以以下方式结构化的Isabelle证明:proof (cases "n = 0") case True (* lots of stuff here *) show ?thesis sorry next case False (* lots of stuff here...
我该如何轻松地在Isabelle的机器学习层面上编写简单的策略？
在Isabelle理论文件中，我可以编写简单的单行策略，例如以下内容： apply (clarsimp simp: split_def split: prod.splits) 然而，我发现当我开始编写机器学习代码来自动化证明并生成一个ML tactic对象时，这些一行代码变得相当冗长： ...
为什么Isabelle不会简化我的“if _ then _ else”结构体的主体部分？
我有以下的Isabelle目标：lemma "⟦ if foo then a ≠ a else b ≠ b ⟧ ⟹ False" 即使目标很简单，但simp、fast、clarsimp、blast、fastforce等策略都无法达成目标。 为什么Isabelle不只是简化if结构的主体，使得"...