Isabelle/HOL限制共域

Question

我很抱歉最近问了这么多伊莎贝尔的问题。现在我有一个类型的问题。

我想使用法新社理论中引入的type_synonym。

type_synonym my_fun = "nat ⇒ real"

在我自己的理论中，我有一个地方：

fixes n :: nat

and f :: "my_fun"

and A :: "nat set"

defines A: "A ≡ {0..n}"

但是，在我的用例中，函数f的输出始终是集合{0..n}中的自然数。我想把这作为一个条件(或者有更好的方法来做呢？)我发现的唯一方法是：

assumes "∀v. ∃ i. f v = i ∧ i ∈ A"

因为

assumes "∀v. f v ∈ A"

不管用。

如果我让伊莎贝尔给我看一下所涉及的类型，我觉得没问题：

∀v::nat. ∃i::nat. (f::nat ⇒ real) v = real i ∧ i ∈ (A::nat set)

当然，现在我不能输入这样的内容：

have "f ` {0..10} ⊆ A"

但我必须证明这一点。我知道这个问题是从哪里来的。不过，在这种情况下，我不知道如何处理。处理这个问题的正常方法是什么？我想使用my_fun，因为它具有与我的理论相同的含义。

(再次)谢谢。

Answer 1

如果仔细观察∀v::nat. ∃i::nat. (f::nat ⇒ real) v = real i ∧ i ∈ (A::nat set)，您将能够看到用于在nat和real之间进行隐式类型转换的机制:在区域设置上下文中的假设语句中，出现了缩写real (调用在Nat.thy中为semiring_1定义的of_nat )。

当然，您可以显式地使用相同的机制。例如，可以将A::real set定义为A ≡ image real {0..n}，而不是将A::nat set定义为A ≡ {0..n}。然后您可以使用range f ⊆ A而不是assumes "∀v. ∃ i. f v = i ∧ i ∈ A”。然而，我怀疑是否有一种普遍接受的正确方法:这取决于你到底在努力实现什么。尽管如此，为了便于讨论，您的区域设置可能如下所示：

type_synonym my_fun = "nat ⇒ real"

locale myloc_basis =
  fixes n :: nat

abbreviation (in myloc_basis) A where "A ≡ image real {0..n}"

locale myloc = myloc_basis +
  fixes f :: "my_fun"
  assumes range: "range f ⊆ A"

lemma (in myloc) "f ` {0..10} ⊆ A"
  using range by auto

--我想把它作为一个条件(或者有更好的方法来做？)。

答案取决于对f的了解。如果只知道关于f范围的一个条件，正如你的问题的陈述所暗示的那样，那么，我想，你只能说是一种假设。

顺便提一下，据我所知，defines被认为是过时的，最好避免在locale：stackoverflow.com/questions/56497678的规范中使用它。