个人中心
文章发布
退出
作者热门文章
- html - 出于某种原因，IE8 对我的 Sass 文件中继承的 html5 CSS 不友好？
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景？
27
4
我想在一个名为 List 的理论中定义我自己的列表类型，但已经有一个同名的理论。
有没有比Main更轻量级的理论？ ?
最佳答案
请注意 $ISABELLE_HOME/src/HOL/ex/Seq.thy给出了一个定义您自己的列表数据类型以进行实验的最小示例，而没有着手解决如何使用其 Main 下面的系统的微妙问题。入口点。 (初学者会感到困惑，专家不会这样做。)
理论上，你能导入的最原始的理论是 Pure ，但这只是基本的逻辑框架，还没有像 HOL 那样的任何对象逻辑。出于好奇，您可以查看 $ISABELLE_HOME/src/HOL/ex/Higher_Order_Logic.thy从 Pure 开始并定义了 H.O.L.最重要的是，没有您期望从完整的 Isabelle/HOL 中获得的任何高级理论和工具。
关于isabelle - Isabelle 可以不导入任何理论吗？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/11336535/
27
4
0
我需要在一篇论文中做一个演示，该论文在某些时候使用了 Isabelle/Isar 和 Isabelle/HOL。 我尝试在线研究 Isabelle/HOL 和 Isabelle/Isar，以便能够在一
我想在一个名为 List 的理论中定义我自己的列表类型，但已经有一个同名的理论。 有没有比Main更轻量级的理论？ ? 最佳答案 请注意 $ISABELLE_HOME/src/HOL/ex/Seq.t
Isabelle 中的“商型模式”是什么？ 我在互联网上找不到任何解释。 最佳答案 如果你能从你看到这句话的地方引用一点会更好。我知道“模式匹配”，我知道“商类型”，但我不知道“商类型模式”。 我宁愿
有时我发现很难使用 Isabelle，因为我无法像在正常编程中那样使用“打印命令”。 比如我想看什么?thesis .具体语义书说: The unknown ?thesis is implicitly
我是 isabelle 的新手，并试图证明以下简单的不等式: lemma ineq: "(a::real) > 0 ⟹ a 0 ⟹ b 0" proof have "1/a + 1/b >
输入以下定义时 datatype env = "nat => 'a option" Isabelle/jedit 显示一个感叹号并说 Legacy feature! Bad name binding:
在 Isabelle 中，有时会遇到存在重复子目标的场景。例如，想象以下证明脚本: lemma "a ∧ a" apply (rule conjI) 目标: proof (prove): step
Isabelle/jEdit 中的颜色代码是什么意思？我在 Isabelle/jEdit manual 中找不到他们的描述.它唯一写的是 Prover feedback works via color
如何在 Isabelle 中定义常量集？例如像 {1,2,3}(给它一个更有趣的转折，1,2,3 是实数)，或 {x\in N: x < m}，其中 m 是某个固定数字 - 或者，也许更难，集合 {N
假设我在 Isabelle 中写了一个引理“(∀a. P a ⟹ Q a) ⟹ R b”。 ∀a只会量化 P a .如果我想量化超过 P a ⟹ Q a但是，在 ∀a 后面加上括号(即“(∀a. (P
使用 Isar 时，我发现了一个令人惊讶的行为(对我而言)。 我尝试使用假设，有时 Isar 提示它无法解决未决目标，例如我最典型的例子是有一个假设但无法假设它: lemma assumes "A
在伊莎贝尔中，人们通常可以达到证明目标，其中中间类型的术语对于证明的正确性至关重要。例如，考虑以下引理，将 nat 42 转换为 'a word，然后再返回: theory Test imports
已关注 how-to-use-persistent-heap-images-to-make-loading-of-theories-faster-in-isabelle另一个建议是我为 Nominal
我尝试使用 partial_function 关键字定义部分函数。它不起作用。这是最能表达直觉的: partial_function (tailrec) oddity :: "nat => nat"
我知道如何在 Isabelle 中制作“术语缩写”，但我可以制作行为相同的“类型缩写”吗？ 我可以定义一个“术语缩写”使用 abbreviation "foo == True" 从此以后，输出中出现的
如何在 Isabelle 中将集合转换为列表？ 我对带有签名的函数定义感兴趣: "'a set => 'a list" 我该如何定义？ 最佳答案 通过搜索 "'a set" "'a list"在我偶然
我想用简化词来替换不等式的子项。我将通过一个示例来说明这一点，而不是对我的问题进行通用定义: 假设我有一个简单的编程语言和一个基于它的 Hoare 逻辑。假设我们有 if、while 和序列操作。此外
我是一名刚开始习惯 Isabelle 的数学家，而本应非常简单的事情却令人沮丧。如何定义两个常量之间的函数？比如说，函数 f: {1,2,3}\to {1,2,4} 映射 1 到 1、2 到 4 和
我想找到定理。我已阅读 find_theorems 上的部分在 Isabelle/Isar reference manual : find_theorems criteria Retrieves fa
我试图在 Isabelle/HOL 中证明这个引理。 引理“(0::nat) ≠ undefined” 但是挑剔的人找到了这个和它的否定的反例 引理“(0::nat) = undefined” 这怎么
我是一名优秀的程序员,十分优秀！