问题标签 [isar]

我正在尝试从 Isabelle 的一本书 [1] 中形式化一系列关于拓扑的证明。

我想编码拓扑空间（X，T）由一组“点”（某种任意类型'a的元素）和一组X的子集（称为T）组成的想法，使得：

• A1。如果元素 p 在 X 中，则在 T 中至少存在一个集合 N 也包含 p。
• A2。如果集合 U 和 V 在 T 中，并且如果 p∈(U∩V)，则在 T 中一定存在集合 N，其中 N⊆(U∩V) 和 x∈N。（如果两个集合相交，则必须有一个邻域覆盖该相交。）。

目前我有以下定义：

到目前为止，一切都很好。我能够添加各种定义并证明关于假设topspace实例的各种引理和定理。

但我如何实际创建一个？除非我误解了事物，否则到目前为止我看到的关于instanceandinstantiate关键字的示例似乎都是关于声明一个特定的抽象类（或类型或语言环境）是另一个抽象类的实例。

我如何告诉 Isabelle 一对特定的集合（例如X={1::int, 2, 3}, T={X,{}}）形成一个topspace？

同样，我如何使用我的定义来证明X={1::int, 2, 3}, T={}不符合要求？

最后，一旦我证明一个特定的具体对象 X 符合 a 的定义，topspace我如何告诉 Isabelle 现在topspace在证明关于 X 的事情时使用我已经证明的所有定义和定理？

顺便说一句，我正在使用，class因为我不知道更好。如果它不是适合这项工作的工具，我很乐意做其他事情。

[1]：Dennis Sentilles通往高等数学的桥梁

我对使用 Isabelle/Isar 编写既可读又机器检查的证明很感兴趣，我希望改进我的风格并简化我的证明。

prog-prove有以下练习：

练习 4.6。定义一个递归函数elems :: 'a list ⇒ 'a set并证明x ∈ elems xs ⟹ ∃ ys zs. xs = ys @ x # zs ∧ x ∉ elems ys。

模仿类似于我用笔和纸写的东西，我的解决方案是

但它似乎相当长。特别是，我觉得在这里调用排中律比较麻烦，我觉得应该有一些方便的示意图变量?goal，比如可以引用当前目标什么的。

我怎样才能在不牺牲清晰度的情况下缩短这个证明？

我正在尝试按照本文档（特别是幻灯片 23）在 Isabelle 中进行基本的自然演绎证明。

我知道我可以做类似的事情

但是也

达到相同的目标。

所以当我尝试写证明时

喜欢

伊莎贝尔为什么抱怨

我知道这些是 Isabelle 可以一步证明的非常简单的事情：这里的目标是生成一个人类可读的简明证明（在自然演绎的范围内），而无需咨询 Isabelle。

TL;DR：Isar 语言是否有任何编码约定？有必要尊重jEdit的折叠策略吗？

我的团队正在研究数学的形式化，所以我们的主要目的之一是获得可读的证明。对此进行调查，我们尝试以一种中间事实（和标签，如果有的话）突出的方式对证明进行编码：

等等。除了有时这会产生“短线”的扩散（顺便说一句，我不知道这是否真的是一个问题），它在某种程度上与 jEdit 折叠策略不兼容；折叠后，前一个代码块如下所示：

完全掩盖了论点。以下格式可能更好：

而且，折叠后，

这使得参数的流程变得明确。

无论如何，在我提出 5 个新的格式约定之前，我肯定想知道是否有一些事实上的标准，或者至少是否有人考虑过这一点。

我正在尝试使用 Isar 来证明一些事情；到目前为止，我已经达到了一个看起来像这样的目标：

（这plmeets是我定义的一个函数，其中plmeets P l是仿射平面中“点 P 位于 l 线上”的简写，但我认为这对我的问题并不重要。）

这个目标是三件事的结合。实际上，我已经证明了在我看来与这些事情非常接近的引理。例如，我有

产生输出

您可以看到几乎正是三个连体项目中的第一个。（我承认我的其他引理与其他两项并不完全匹配，但我会努力解决的）。

我想说“因为引理four_points_a1，我们剩下要证明的就是item2 ∧ item3”，我很确定有办法做到这一点。但是看“编程和证明”这本书对我没有任何建议。在伊莎贝尔，而不是伊萨尔，我想我会申请conjI两次将一个目标分成三个，然后解决第一个目标。

但我看不到如何在 Isar 中做到这一点。

这是数学中的一个小定理：

假设 u 不是 A 的元素，v 不是 B 的元素，f 是从 A 到 B 的单射函数。令 A' = A union {u} 和 B' = B union {v}，并定义g: A' -> B' by g(x) = f(x) 如果 x 在 A 中，并且 g(u) = v。那么 g 也是单射的。

如果我正在编写类似 OCaml 的代码，我会将 A 和 B 表示为类型，并将 f 表示为 A->B 函数，例如

然后定义一个函子

我的定理是 ifQ.f是单射的，那么 也是(Extend Q).f，我希望我的语法或多或少是正确的。

我想在 Isabelle/Isar 做同样的事情。通常，这意味着写类似

并且Q是……某事。我不知道如何在 Isabelle 中创建一个类似于QOCaml 中的仿函数的单个操作，它创建两个新的数据类型和它们之间的函数。单射性的证明似乎相当简单——只是一个四例拆分。但是我想要帮助定义我调用的新函数Q f，给定函数f。

我需要在一篇论文上做一个演示，该论文在某些时候使用了 Isabelle/Isar 和 Isabelle/HOL。

我尝试在网上搜索有关 Isabelle/HOL 和 Isabelle/Isar 的信息，以便能够在一两张幻灯片中说明这些关系。以下是我目前理解的关系：

• Isabelle - 为演绎系统提供通用基础架构
  • 基于标准 ML 编程语言
  • 提供了一个 IDE，允许您编写以后可以证明的理论。
• Isabelle/Pure - 根据此链接 的高阶逻辑的最小版本：
  • 它是可以输入到 isabelle IDE 中的实际语言吗？
  • 还是技术规范？

• Isabelle/HOL（高阶逻辑）：

  • 它是图书馆还是语言？
  • 它与 Isabelle/Pure 有什么关系？
  • 它本质上是程序性的吗？
    • 战术只存在于 Isabelle/HOL 中吗？
    • 是 LCF - 逻辑可交换函数吗？

• 伊莎贝尔/伊萨尔：

  • 基于 Isabelle/Pure 的结构化证明语言
  • 声明式
  • 它是此处所述的 Isabelle/HOL 的扩展吗？
  • 语言环境是否只存在于 Isabelle/Isar？

Isabelle/IDE 默认支持什么？

只是觉得我从不同的来源获得了相互矛盾的信息，并想解决这个问题。

提前致谢

我想在语言环境解释所需的证明中使用我的结构的一些属性

例如，假设我定义了谓词 P 并证明了一些关于对满足谓词的元素的操作的引理（add是一个封闭的二元运算，add是关联的并且存在zero中性元素）addP

我想将我的元素集解释为满足某些语言环境的结构，例如monoid

但是在我的证明目标中，我无法得到所有元素实际上都满足谓词P，并且我留下了一个通用目标，例如add zero a = a我已经证明了我的集合中的元素。

如何在我的目标中强制所有元素都满足谓词P？

如果对语言环境的参数有一些定义，这将使语言环境的假设更容易编写和/或阅读和/或理解（或者因为函数非常复杂，所以会简化假设的陈述，或者它的名称使假设更易于阅读和理解），定义该函数的最佳方法是什么？

作为一个人为的例子，假设我们想将函数fg合并到假设的陈述中（当然在这里实际上没有用）：

有人可能会考虑使用defines：

但 locales.pdf 文件似乎表明它已被弃用（但我不确定）：

constrains除了上下文元素和之外，语法是完整的defines，它们是为了向后兼容而提供的。

将Ctrl 悬停fg在语言环境中的引理上，将其defined_after命名为，constant "local.fg"而在defined_during它中是fixed fg\nfree variable. 然而，它确实实现defined_after_def了等于defined_during_def（即后者没有额外的参数或假设），第三个选项没有：

fg它在引理中也具有与语言环境相同的 Ctrl-hover 文本defined_during。

也许网站上的一个 PDF 文件或 NEWS 文件中有一些关于它的内容，但我找不到任何明显的东西。isar-ref.pdf 发表评论：

assumes和元素都defines有助于语言环境规范。当定义从参数派生的操作时，definition（§5.4）通常更合适。

但我不确定如何使用这些信息。大概是说，当一个人通过做我所询问的事情没有获得太多收益时，应该像在语言环境中那样进行defined_after（除非引用意味着可以definition在语言环境定义中使用），这不是我想要的。（顺便说一句：这句话的第一句话会向我暗示这defines在某种程度上等同于第三个选项，它引入了一个额外的参数和假设，但事实并非如此。也许理解什么可能比 - 更微妙it-appears-Isabelle-jargon “语言环境规范”的意思是解释是什么导致 Ctrl-hover 文本在第一个和第二个选项之间有所不同，我不知道。）