在 Isabelle 中证明关于 THE 的直观陈述 [英] Proving intuitive statements about THE in Isabelle

问题描述

我想在 Isabelle 中证明类似这个引理的东西

I would like to prove something like this lemma in Isabelle

lemma assumes "y = (THE x. P x)" shows "P (THE x. P x)"

我想这个假设意味着 THE x.P x 存在并且是明确定义的.所以这个引理也应该是真的

I imagine that the assumption implies that THE x. P x exists and is well-defined. So this lemma ought to be true too

lemma assumes "y = (THE x. P x)" shows "∃! x. P x"

我不知道如何证明这一点，因为当我在 Isabelle 的查询框中键入name: the"时，我已经查看了所有出现的定理，但它们似乎没有用.我也找不到 THE 的定义，虽然我对它的含义有一个直观的认识，但我不确定如何定义它.我试过这样的事情，虽然我确定这是错误的

I'm not sure how to prove this because I've looked through all the theorems that turn up when I type "name: the" into the query box in Isabelle and they don't seem useful. I can't find the definition of THE either and I am not sure how to define it although I have an intuitive idea of what it means. I tried something like this although I am sure this is wrong

"(∃!x. P x) ⟹ THE x. P x = (SOME x. P x)"

甚至可能没用，因为我也不知道如何定义 SOME！

and maybe even useless because I don't know how to define SOME either!

推荐答案

不幸的是，假设并不不暗示 THE x.P x 存在"，至少在某种意义上不是你会觉得满意的.由于 HOL 是一个整体逻辑，因此逻辑中没有明确定义"的概念.

Unfortunately, the assumption does not imply that THE x. P x ‘exists’, at least not in a sense that you would find satisfying. As HOL is a total logic, there is no notion of ‘well-definedness’ in the logic.

如果你写THE x.P x 当没有唯一的 x 满足 P 时，则 THE x.P x 是 仍然是一个在 HOL 中存在"的值，但是你无法证明任何有意义的值(很像 undefined 常量)，当然也不是P 持有的一种.SOME也是一样，与THE基本相同，不同的是对于THE，必须有一个唯一财产证明和SOME唯一性不是必需的.

If you write THE x. P x when there is no unique x that satisfies P, then THE x. P x is still a value that ‘exists’ in HOL, but one that you cannot prove anything meaningful about (much like the undefined constant) and certainly not one for which P holds. The same is true for SOME, which is basically the same as THE with the difference that for THE, there has to be a unique witness for the property and for SOME uniqueness is not required.

展示关于 SOME x 的一些东西的典型方法.P x 是你首先证明一个见证人存在(即 ∃x.P x)，然后你把它插入到一个像 someI_ex 这样的规则中，然后它告诉P (SOME x.P x) 确实成立.

The typical approach for showing something about SOME x. P x is that you first show that a witness exists (i.e. ∃x. P x) and then you plug that into a rule like someI_ex which then tells you that P (SOME x. P x) indeed holds.

THE 也一样，只是你必须证明有 one 见证人——这就是 ∃!意味着(参见定理Ex1_def).可以显示这种独特的存在，例如使用规则 ex_ex1I 或 ex1I.然后您可以将该事实插入到 theI' 和 the1_equality 中以获得您想要的结果.

It's the same for THE, except that there you have to show that there is exactly one witness – which is what the ∃! means (cf. the theorem Ex1_def). Showing this unique existence can be done e.g. with the rules ex_ex1I or ex1I. Then you can plug that fact into theI' and the1_equality to get the results you want.

顺便说一下，SOME 的常数称为 Eps(如希尔伯特的 ε 运算符")，其他的为 The 和Ex1.如果你输入例如term Eps，你可以按住 ctrl 键点击 Eps，它会带你到它的定义(或者，如果是 Eps 和 而不是它们的公理化).

By the way, the constant for SOME is called Eps (as in ‘Hilbert's ε operator’) and the others are The and Ex1. If you type e.g. term Eps, you can ctrl-click on the Eps and it takes you to its definition (or, in case of Eps and The rather their axiomatisations).

还有一个用于自然数的 LEAST 组合子，它与 SOME 非常相似，有时非常有用(它被称为Least"，引理是 LeastI_ex 和 Least_le).

There's also a LEAST combinator for natural numbers that is very similar to SOME and can be quite useful sometimes (it's called ‘Least’ and the lemmas are LeastI_ex and Least_le).

另一边注:这种认为仅仅因为你可以写下一个术语，它不一定在直觉意义上明确定义"的想法在 Isabelle 中很常见:你可以除以零，你可以写下导数不可微函数的度量，不可测集的度量，不可积函数的积分等.然后您会得到某种虚拟值(例如 0 表示被零除或完全荒谬的东西，例如 THEx. 错误)，但大多数讨论导数、积分等实际性质的定理确实明确要求该事物实际上是明确定义的.

Another side note: This idea that just because you can write down a term, it is not necessarily ‘well-defined’ in an intuitive sense is very common in Isabelle: you can divide by zero, you can write down the derivative of a non-differentiable function, the measure of a non-measurable set, the integral of a non-integrable function etc. You then get some kind of dummy value (e.g. 0 for division by zero or something completely absurd like THE x. False), but most of the theorems that talk about actual properties of derivatives, integrals, etc. do explicitly require that the thing is actually well-defined.

这篇关于在 Isabelle 中证明关于 THE 的直观陈述的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！