isabelle

0热度

1回答

我想了解实施伊莎贝尔/ HOL线性逻辑：https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/ILL.html对于不syntax关键字代表什么，什么是代码的意思是： syntax "_Trueprop" :: "single_seqe" ("((_)/ ⊢ (_))" [6,6] 5)

0热度

1回答

有限域映射

我需要一个数据类型的有限映射。我使用典型的（部分）地图，直到我在证明中碰到一个路障，只能通过引入一个finite (dom m)谓词来修复。将这个事实进行到底是乏味的，那么标准库中是否有一些解决方案呢？

2热度

1回答

证明两个特定集合在Isabelle中具有相同的基数

我很难证明两个集合具有相同的基数。以下所有集合都是有限的。首先假设我们已经设定了（M :: b集合）和函数foo ::“b集合⇒b集合⇒bool” 使得（foo AC = foo BC⟷A = B）和对于M中的每一个A，实际上都有一个C，这样foo A.C. 我试图证明那张卡{S。 ∃A∈M。（S = {C.foo A C}）} = card M. 对此的非正式证明是显而易见的，但我似乎无法

0热度

1回答

如何HOLCF证明清单的双重逆转并没有改变它

下面是一个简单的理论写在普通HOL： theory ToyList imports Main begin no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65) hide_type list hide_const rev datatype 'a list = Nil ("[]")

0热度

1回答

如何分析假设中的if-expressions？

我试图证明以下引理： lemma if_assumption: "(if a = 1 then 2 else 3) = 2 ⟹ a = 1" apply (cases "a = 1") apply simp_all 简化后我得到以下公式： 3 = 2 ⟹ a ≠ 1 ⟹ False 如果表达式的结果等于2 IFF a等于1。所以，我猜测我可以以某种方式推断这个事实。如

1热度

1回答

如何在伊莎贝尔证明最大交换性质

我对伊莎贝尔非常新，所以请有怜悯。如何用此功能证明最大交换属性？ fun max :: "nat => nat => nat" where "max 0 0 = 0" | "max (Suc x) 0 = Suc x" | "max 0 (Suc x) = Suc x" | "max (Suc x) (Suc y) = Suc (max x y)" lemma "max x y = m

0热度

1回答

如何用重叠模式定义函数？

我试图定义4值逻辑（假的，真实的，无效和错误）连词功能： datatype 'a maybe = Just "'a" | Nothing | Error type_synonym bool4 = "bool maybe" abbreviation JF :: "bool4" where "JF ≡ Just False" abbreviation JT :: "bool4" where "

0热度

1回答

收敛和向量理论

Isabelle/HOL中是否存在收敛理论？我需要定义∥x(t)∥ ⟶ 0 as t ⟶ ∞。此外，我正在寻找向量理论，我找到了矩阵理论，但我找不到向量之一，Isabelle/HOL中是否存在这样的理论？干杯。

1热度

1回答

Isabelle/HOL：'simp'的证明是缓慢的，'value'是瞬时的

我是Isabelle/HOL的新手，仍然在研究锻炼练习。与此同时，我正在通过将这些证明技巧应用于组合词的问题来锻炼。我观察到一个非常不同的行为（效率方面），在'价值'和'引理'之间。能解释两个命令之间的不同评估/搜索策略吗？有没有一种方法可以在“引理”的证明中使用“价值”的速度？当然，我在问，因为我还没有在文档中找到答案（到目前为止）。什么是手册，这种效率差异将被记录和解释？下面是重现问题

0热度

1回答

Isabelle/HOL中的向量转置

我找不到在Finite_Cartesian_Product理论中转置(real,'n) vec类型向量的定义或引理。例如，如果矢量e = A x然后是e（e^T）的转置导致转置A和x（e^T = A^T x^T），我试图用转置矩阵和矢量来代替转置矢量。我可以在Isabelle/HOL中做到这一点吗？