问题标签 [isabelle]

我想定义一个按案例证明的规则，与proof (cases rule: <rule-name>). 我设法使用case_names和consumes参数，但我没有设法绑定示意图变量?case，因此，在使用我的规则进行证明的情况下，可以编写show ?case .... 我该如何绑定它？

具体来说：我有一个受 Mizar 启发的琐碎集的概念，即空集或单例集。我想通过空与单例分析来证明平凡集的属性。到目前为止，我有：

我可以按如下方式使用它：

但我不能使用show ?case. 如果我尝试，它会给我错误消息“未绑定的示意图变量：？case”。 print_cases在证明里面输出以下内容：

这表明它不起作用，因为?P不受trivial.

顺便说一句：我使用它的完整上下文可以在https://github.com/formare/auctions/blob/master/isabelle/Auction/SetUtils.thy看到。

我正在研究一个引理，该引理表明，n如果每个单项式的指数小于或等于 ，则单项式之和的次数总是小于或等于n。

到目前为止，我要做的如下（请注意，我是 Isabelle 的初学者）：

这就是问题所在，我不明白为什么以下引理不足以完成证明。特别是，我希望最后一部分（抱歉的地方）足够简单，让大锤找到证据：

.
布赖恩霍夫曼出色回答的解决方案：
。

我想推理从有限集中选择一个元素的函数。

我试图定义一个谓词，告诉我某个给定函数是否是这样的“选择器”函数：

实际上，我想从中选择元素的那些有限集是具体类型，但是将具体类型放在'a' 位置会导致同样的麻烦。

我也尝试省略finite A，但我正在处理的集合是有限的，我什至不想在这里考虑选择公理。

现在这个定义似乎不一致：

我怎样才能chooser以合理的方式定义？我想按如下方式使用它：

大多数时候，选择集合中的一个成员很重要，而不是如何选择它。

背景：我想正式确定拍卖中的决胜局（本文第 4 节）。假设正在拍卖的物品有两个最高出价，我们需要任意选择一个应该赢得拍卖的出价者。

这是，顺便说一句，一个非常小的例子（这有点难以理解）：

我正在使用 Isabelle 进行一个项目。

出于某种原因，我必须模拟一个位/字节系统，如下所示：

我用（BTTTTTTTT）代表（11111111），（BFFFFFFFF）代表（00000000）。

但我无法证明如此明显的引理： b != b + 1

我真的需要一些帮助。

为什么以下工作：

但这失败了

和

同样，以下成功，

但这失败了

和

里面有一个函数调用word_rsplit。~~/src/HOL/Word/Word.thy

我想将 a 拆分32 word为四个8 word，这个功能似乎很完美。

引理word_rcat (word_rsplit w) = w对我也很有用。

所以我需要知道如何使用word_rsplit，如何指定'a= 32 和'b= 8。

我试图证明如果n > 0那么g n b = True（见下文）的定理。情况就是这样，因为g (Suc n) b只有调用g 0 True. 不幸的是，当我试图证明时，我的归纳中没有这个事实g 0 b。我怎样才能完成证明（我必须用什么代替sorry）？

我是vim的粉丝，但只有emacs有这个 Isabelle/HOL 环境。jEdit很棒，但我不能使用

就像在emacs中一样。

如何在jEdit中启用“跟踪” ？

我正在尝试增加FOL.thy量词MOST，我打算将其定义为简单多数，即

我不确定如何修改FOL.thy文件。在下axiomatization，我想补充：

并且，在该where条款下：

其中“...”是表达上述约束的正确方式，即P(x)和的基数~P(x)。（同样，我不确定这里有一个好名字，欢迎提出建议。）

我想在“符号”部分添加一个条目，并且由于缺乏更好的想法，选择使用 delta：

同样在该notation部分中。

1）如何正确表达基数约束？

2）我还需要修改哪些其他内容？

对于后一个问题，指出最终我想评估一些不同的结论是否是必要的、可能的或不可能的可能会有所帮助，假设前提将包括使用“大多数”和“全部”的量化断言（以及连词、析取等）。

如何使用 Isabelle/HOL 从我的源理论文件自动生成 LaTeX？

Isabelle/HOL'stutorial.pdf非常漂亮。我打算用 LaTeX 写一篇论文，里面有很多 Isabelle 代码。