很抱歉最近问了这么多伊莎贝尔的问题。现在我有一个类型问题。
我想使用法新社理论中引入的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因为它与我的理论具有相同的含义。
谢谢你(再次(。
如果你仔细观察∀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被认为是过时的，最好避免在语言环境的规范中使用它：stackoverflow.com/questions/56497678。