proof - Isabelle 中的运算符重载

In lại 作者：行者123 更新时间：2023-12-03 22:45:03 28 4

theory Prueba
imports Main HOL
begin

primrec suma::"nat ⇒ nat ⇒ nat" where
"suma 0 n = 0" |
"suma (Suc x) n = 0"
no_notation suma (infix "+" 65)

value "2 + (1 :: nat)"

no_notation Groups.plus_class.plus (infixl "+" 65)

notation suma (infixl "+" 65)

28 4 0

• Isabelle/Pure Isabelle/HOL Isabelle/Isar 概念性问题

  我需要在一篇论文中做一个演示，该论文在某些时候使用了 Isabelle/Isar 和 Isabelle/HOL。 我尝试在线研究 Isabelle/HOL 和 Isabelle/Isar，以便能够在一

• isabelle - Isabelle 可以不导入任何理论吗？

  我想在一个名为 List 的理论中定义我自己的列表类型，但已经有一个同名的理论。 有没有比Main更轻量级的理论？ ? 最佳答案 请注意 $ISABELLE_HOME/src/HOL/ex/Seq.t

• isabelle - Isabelle 中的商型模式是什么？

  Isabelle 中的“商型模式”是什么？ 我在互联网上找不到任何解释。 最佳答案 如果你能从你看到这句话的地方引用一点会更好。我知道“模式匹配”，我知道“商类型”，但我不知道“商类型模式”。 我宁愿

• isabelle - 如何在 Isabelle 证明中打印局部变量和 ?thesis(在 Isabelle 中调试)？

  有时我发现很难使用 Isabelle，因为我无法像在正常编程中那样使用“打印命令”。 比如我想看什么?thesis .具体语义书说: The unknown ?thesis is implicitly

• isabelle - 证明 isabelle 中的简单不等式

  我是 isabelle 的新手，并试图证明以下简单的不等式: lemma ineq: "(a::real) > 0 ⟹ a 0 ⟹ b 0" proof have "1/a + 1/b >

• isabelle - Isabelle 中的错误名称绑定(bind)

  输入以下定义时 datatype env = "nat => 'a option" Isabelle/jedit 显示一个感叹号并说 Legacy feature! Bad name binding:

• isabelle - 如何删除 Isabelle 中的重复子目标？

  在 Isabelle 中，有时会遇到存在重复子目标的场景。例如，想象以下证明脚本: lemma "a ∧ a" apply (rule conjI) 目标: proof (prove): step

• isabelle - Isabelle/jEdit 中的颜色代码是什么意思？

  Isabelle/jEdit 中的颜色代码是什么意思？我在 Isabelle/jEdit manual 中找不到他们的描述.它唯一写的是 Prover feedback works via color

• isabelle - 在 Isabelle 中定义有限集

  如何在 Isabelle 中定义常量集？例如像 {1,2,3}(给它一个更有趣的转折，1,2,3 是实数)，或 {x\in N: x < m}，其中 m 是某个固定数字 - 或者，也许更难，集合 {N

• isabelle - 在 Isabelle 中量化句子的特定部分

  假设我在 Isabelle 中写了一个引理“(∀a. P a ⟹ Q a) ⟹ R b”。 ∀a只会量化 P a .如果我想量化超过 P a ⟹ Q a但是，在 ∀a 后面加上括号(即“(∀a. (P

• isabelle - Isabelle/Isar 的假设语义是什么？

  使用 Isar 时，我发现了一个令人惊讶的行为(对我而言)。 我尝试使用假设，有时 Isar 提示它无法解决未决目标，例如我最典型的例子是有一个假设但无法假设它: lemma assumes "A

• isabelle - 如何查看 Isabelle 证明目标中的隐藏类型变量？

  在伊莎贝尔中，人们通常可以达到证明目标，其中中间类型的术语对于证明的正确性至关重要。例如，考虑以下引理，将 nat 42 转换为 'a word，然后再返回: theory Test imports

• isabelle - 在 Isabelle 中加载预编译的堆镜像

  已关注 how-to-use-persistent-heap-images-to-make-loading-of-theories-faster-in-isabelle另一个建议是我为 Nominal

• isabelle - 如何在 Isabelle 中定义偏函数？

  我尝试使用 partial_function 关键字定义部分函数。它不起作用。这是最能表达直觉的: partial_function (tailrec) oddity :: "nat => nat"

• isabelle - 在 Isabelle 中引入类型缩写

  我知道如何在 Isabelle 中制作“术语缩写”，但我可以制作行为相同的“类型缩写”吗？ 我可以定义一个“术语缩写”使用 abbreviation "foo == True" 从此以后，输出中出现的

• isabelle - 在 Isabelle 中将集合转换为列表

  如何在 Isabelle 中将集合转换为列表？ 我对带有签名的函数定义感兴趣: "'a set => 'a list" 我该如何定义？ 最佳答案 通过搜索 "'a set" "'a list"在我偶然

• isabelle - 使用 Isabelle 简化器重写非相等等价关系

  我想用简化词来替换不等式的子项。我将通过一个示例来说明这一点，而不是对我的问题进行通用定义: 假设我有一个简单的编程语言和一个基于它的 Hoare 逻辑。假设我们有 if、while 和序列操作。此外

• isabelle - 在 Isabelle 中定义常量之间的函数

  我是一名刚开始习惯 Isabelle 的数学家，而本应非常简单的事情却令人沮丧。如何定义两个常量之间的函数？比如说，函数 f: {1,2,3}\to {1,2,4} 映射 1 到 1、2 到 4 和

• isabelle - 在 Isabelle 中使用 "find_theorems"

  我想找到定理。我已阅读 find_theorems 上的部分在 Isabelle/Isar reference manual : find_theorems criteria Retrieves fa

• isabelle - 在 Isabelle/HOL 中未定义

  我试图在 Isabelle/HOL 中证明这个引理。 引理“(0::nat) ≠ undefined” 但是挑剔的人找到了这个和它的否定的反例 引理“(0::nat) = undefined” 这怎么