标签: isabelle

我想在较弱的笔记本电脑上使用 Isabelle，并将繁重的定理搜索/证明委托给网络上的服务器。我猜想这之前已经完成了，但我找不到此任务的教程或报告。

Isabelle系统手册描述了如何自行运行 Isabelle 后端。但是，我从手册中不明白如何将现有前端之一（例如Isabelle/jEdit）连接到这样的进程。理想情况下，该设置应该适用于多个用户（并且理论文件位于用户系统上）。

到目前为止，我能实现的最好结果是在服务器上运行所有 Isabelle/jEdit，并通过 SSH/X11 转发从 Linux 笔记本电脑访问它。这很酷，但不完全是我的想法。还有其他方法吗？

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

我的团队正在研究数学的形式化，因此我们的主要目的之一是获得可读的证明。考虑到这一点，我们尝试以中间事实（和标签，如果有的话）脱颖而出的方式编写证明：

from fact1 have
  1: "Foo"
  using Thm1 Thm2 by auto
then have
  2: "Bar = FooBar"
  by simp
also from 1 have
  " ... = BarFoo"
  by blast 

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

from fact1 have
then have
also from 1 have

完全掩盖了论点。下面的格式也许更好：

from fact1
have 1: "Foo"
  using Thm1 Thm2 by auto
then 
have 2: "Bar = FooBar"
  by simp
also from 1 
have " ... = BarFoo"
  by blast 

并且，折叠之后，

from fact1
have 1: "Foo"
then …

当Isabelle在ProofGeneral中显示目标时,假设会围绕它们呈现括号,如下所示:

然而,在Isabelle/jEdit中,这似乎已经改为meta-implication箭头:

虽然我理解前者有点不标准,但我觉得它更容易阅读.有没有办法修改Isabelle/jEdit的行为以打印旧ProofGeneral风格的目标？

当我导入带有定义常量(用于递归函数或定义)f的理论文件时,如何在当前理论文件中隐藏这样的常量？换句话说,我想确保它f是一个自由变量.我不想更改导入的文件.

我很困惑证明

A ==> B ==> C ==> B 

在伊莎贝尔.显然你可以

apply simp

但我怎么能用规则证明这一点呢？

或者,有没有办法转储使用的规则simp？谢谢.

输入以下定义时

datatype env = "nat => 'a option"

Isabelle/jedit表示感叹号并说

Legacy feature! Bad name binding: "nat => 'a option" 

有什么问题,我该如何修复这种类型的同义词？

更新:甚至

datatype 'a env = "nat => 'a option"

哪个更好,理论上的定义并没有解决问题.

Isabelle/jEdit中的颜色代码是什么意思？我在Isabelle/jEdit手册中找不到他们的描述.它写的唯一的东西是

证明反馈通过颜色,框,波浪下划线,超链接,弹出窗口,图标,可点击输出工作 - 所有这些都基于Isabelle在后台制作的语义标记.

颜色用作校样脚本背景和滚动条旁边的垂直条.

你能指点一些文件或在这里解释一下吗？

我开始学习伊莎贝尔,并想尝试在伊莎贝尔中定义一个幺半群,但不知道如何.

在Coq中,我会做这样的事情:

Inductive monoid (? : Type) (op: ? -> ? -> ?) (i: ?): Prop :=
| axioms: (forall (e: ?), op e i = e) ->
          (forall (e: ?), op i e = e) ->
          monoid ? op i.

我不知道如何在伊莎贝尔做同样的事情.从概念上讲,我想到了这样的事情:

inductive 'a monoid "('a ? 'a ? 'a) ? 'a ? bool" for f i where
  axioms: "?f e i = e; f i e = e? ? monoid f i"

但是,这在Isabelle中无效.

如何在Isabelle中使用类型参数定义归纳谓词？

以下给出 bad theory import "Multivariate_Analysis"

imports Multivariate_Analysis

导入Main工作正常,如何导入模块？

如何从命令行验证* .thy文件是有效的Isabelle证明？我猜想在GUI中进行操作就等于看到没有问题/错误/警告等。但是有没有办法从命令行执行此操作？