标签: isabelle

这个问题扩展了如何隐藏定义的常量的问题。

我进口的理论A，B以及C，也许在将来也D，E......所有的理论定义一个函数f。我想f在不改变导入的理论的情况下隐藏我当前理论中的定义。当我写term f我得到A.f。当我添加hide_const (open) f到我当前的理论时，A.f是隐藏的，但现在我得到B.f了f. 我怎样才能完全隐藏f？我需要类似的东西(hide_const (open) f)+。

我有这个C代码:

while(p->next)   p = p->next;

我想证明无论列表有多长,当这个循环结束时,p->next等于NULL,EIP引用此循环后的下一条指令.

但我不能.有谁知道如何在Isabelle/HOL中证明循环？

我试图用partial_function关键字定义部分函数.那没起效.这是最能表达直觉的:

partial_function (tailrec) oddity :: "nat => nat"
where
  "oddity Zero = Zero "
| "oddity (Succ (Succ n)) = n"

然后我尝试了以下内容:

partial_function (tailrec) oddity :: "nat => nat"
where
  "oddity arg = ( case arg of (Succ (Succ n)) => n
                          | Zero => Zero
                )"

partial_function (tailrec) oddity :: "nat => nat"
where
  "oddity (Succ(Succ n)) = n
   | oddity Zero = Zero"

partial_function (tailrec) oddity :: "nat => nat"
where
  "oddity n =
   (if n …

我在 Isabelle 中遇到了一个使用以下规则的自然演绎问题集classical：

( \\<not> A ==> A) ==>A\n

我更习惯使用“排中律”（excluded_middle）和“归谬法”（ccontr）。

我假设这classical与上述两者相同，但我无法从中证明它们中的任何一个，也无法证明lemma "A \xe2\x88\x92\xe2\x86\x92 \xc2\xac \xc2\xac A"问题集中的哪个。我不认为我只是误解了这个规则，因为我成功地使用它lemma "\xc2\xac \xc2\xac A \xe2\x88\x92\xe2\x86\x92 A"从问题集中证明了。有人可以给我一些使用此规则的提示/策略/演示吗？

这是一个示例函数:

fun divide :: "enat option ? enat option ? real option" where
  "divide (Some ?) _ = None"
| "divide _ (Some ?) = None"
| "divide _ (Some 0) = None"
| "divide (Some a) (Some b) = Some (a / b)"
| "divide _ _ = None"

Isabelle HOL向我显示以下错误:

Malformed definition:
Non-constructor pattern not allowed in sequential mode.
?uw_. divide uw_ (Some 0) = None

为什么模式匹配工作正常Some ?并且不起作用Some 0？?是类常量infinity和0 …

我THE x. A在Isabelle/HOL标准库的源代码中看到了构造.这个结构表示什么？它似乎与之相似SOME x. A.

于是我上网查了一下，发现是这样的：

https://isabelle.in.tum.de/library/HOL/HOL/Map.html（地图）

https://isabelle.in.tum.de/library/HOL/HOL-Library/Mapping.html（映射）

以“地图”一词开头的两种理论。我通读了很长一段时间，但我无法真正辨别出它们之间的任何显着差异。有没有什么时候我应该使用前者而不是后者，反之亦然？

提前致谢！

大约2-3周前,我开始学习定理证明者Isabelle.我仍然是一个绝对的初学者,到目前为止我使用了"Isabelle/HOL中的编程和证明"教程.

到目前为止,我发现的矩阵唯一的帮助是查看HOL库中的源代码.

现在我想学习如何证明矩阵的属性.矩阵的lambda语法对我来说仍然是新的.在Isabelle中使用矩阵是否有任何教程或基本/中间示例？

我正在为Isabelle2013/HOL寻找免费提供的优质教程和文档(除了谷歌和挖掘之后的明显的教程和文档).你能推荐一下吗？

假设我写了一个用于反转列表的函数.我想用value命令测试它,只是为了向自己保证我可能做对了.但输出看起来很可怕:

value "reverse [1,8,3]"
> "[1 + 1 + 1, 1 + 1 + (1 + 1) + (1 + 1 + (1 + 1)), 1]" :: "'a list"

如果我告诉Isabelle将这些数字字符视为自然,输出会更糟:

value "reverse [1::nat,8,3]"
> "[Suc (Suc (Suc 0)), Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))), Suc 0]" :: "nat list"

有时候我会求助于使用字符串,但对于所有这些撇号而言,这看起来有点滑稽:

value "reverse [''1'',''8'',''3'']"
> "[''3'', ''8'', ''1'']" :: "char list list"

我可以指示伊莎贝尔漂亮的打印机打印Suc (Suc (Suc 0))的3,等等？也许通过放弃一些神奇的咒语,syntax或translations命令？

这是我的完整示例,如果您想将其粘贴到Isabelle中:

theory …