isabelle

1热度

1回答

我注意到，Isabelle自动简化了¬ (a ∈ (- A))和¬ (x = y)到a ∉ A和x ≠ y。下面是一个简单的笔和纸证明自然推演，但在伊莎贝尔失败。在第二行中，¬ (a ∈ (- A))简化为a ∉ - A。从后者，我们不能申请ComplD，但为什么？ lemma "- (- A) ⊆ (A::'a set)" proof fix a assume "a ∈ - (-

2热度

2回答

通过感应证明的自由类型变量

虽然试图通过归纳证明继续传递样式中的函数的引理，但我遇到了一个自由类型变量的问题。在我的归纳假设中，延续是一个变量，但其类型涉及一个免费类型变量。因此，当我尝试应用i.h时，Isabelle不能将具体类型的类型变量统一起来。我已经熟了这个小例子： fun add_k :: "nat ⇒ nat ⇒ (nat ⇒ 'a) ⇒ 'a" where "add_k 0 m k = k m" | "ad

1热度

1回答

类型导入似乎并没有为我工作在Isabelle2016

我是一个完整的初学者Isabelle，我必须做错了，因为下面看似简单的测试代码只是不编译我： theory testit imports "~~/src/HOL/Library/Inner_Product" begin thm inner_zero_left typ "real_inner" end 在jedit界面中，thm命令似乎工作正常（所以它在In

2热度

2回答

伊莎贝尔的习惯性微积分证明

我在尝试使用一些简单的实际分析问题来学习伊莎贝尔。以下是我的一个证明。它检查直到最后。 theory l2 imports "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis" "~~/src/HOL/Multivariate_Analysis/Derivative" "~~/src/HOL/Mul

0热度

1回答

为什么'linordered_field_class.frac_le'规则不起作用？（Isabelle）

我想在Isar证明中使用规则linordered_field_class.frac_le。这里是代码片段（它可能取决于证明的以前的部分，但这不太可能）。 n是nat类型。 ... then have 4:"2 ≤ (2^(n+1)::real)" by simp have 1:"(0::real)≤(1::real)" by simp have 2: "1≤(1::r

-4热度

1回答

极限C^N（具有|c| <1）为0（伊莎贝尔）

有谁知道表示 "¦c¦<1 ==> (λn. c^n) ---> 0" 在实数规则？我发现使用“查询”面板以下规则： Limits.LIMSEQ_rabs_realpow_zero2: ¦?c¦ < 1 ⟹ op^?c ---> 0 Limits.LIMSEQ_rabs_realpow_zero: ¦?c¦ < 1 ⟹ op^¦?c¦ ---> 0 Limits.LIMSEQ_real

0热度

1回答

感应证明与三个基本案例（伊莎贝尔）

我想能够证明一个声明在n（nat类型）上的归纳。它由一个条件组成，前提条件的前提条件是n> = 2。前提条件为假的条件总是如此。所以我想证明n = 0，n = 1和n = 2的情况都与主要归纳步骤分开。是否有可能通过诱导基地情况下，像下面做一个证明： lemma "P (n::nat) --> Q" proof (induct n) case 0 show ?case

1热度

1回答

在Isabelle中证明了像“∃x。a^x = b”这样的引理吗？

有谁知道在哪里类似于 ∃(x::real). a^x = (b::real) 引理可能被发现的？我在'查询'中找不到类似的东西，但它似乎非常方便。

0热度

1回答

伊莎贝尔/ HOL使用加法/减法关联

我想证明的形式 lemma assoc: "b + (c - d) = (b + c) - d" AFAIK关联性定理是图书馆的一部分，但并未标注简化的东西，所以我需要给手动添加它们。他们在什么地方定义了哪些合适的名称？哪些是theory？

1热度

1回答

总理在伊莎贝尔的定义

我遵循伊莎贝尔教程。在第25页，它引用了素数的定义。我这样写： definition prime :: "nat ⇒ bool" where "prime p ≡ 1 < p ∧ (∀m. m dvd p ⟶ m = 1 ∨ m = p)" 这被伊莎贝尔接受。但是，当我尝试 value "prime (Suc 0)" 它给人的错误 Wellsortedness error (in cod