如何在假设的语言环境中使用写在语言环境参数上的定义？

Question

如果对语言环境的参数有一些定义，这将使语言环境的假设更容易编写 and/or 阅读 and/or 理解（或者因为函数非常复杂所以会简化假设的陈述，或其名称使假设更易于阅读和理解），定义该函数的最佳方式是什么？

作为一个人为的例子，假设我们想将函数 fg 合并到假设的陈述中（当然这里实际上没有用）：

locale defined_after =
  fixes f :: "'a ⇒ 'b ⇒ 'c"
    and g :: "'b ⇒ 'a"
  assumes "∀a. ∃b. f a b = f (g b) b"
      and univ: "(UNIV::'b set) = {b}"
begin

definition fg :: "'b ⇒ 'c" where
  "fg b ≡ f (g b) b"

lemma "∀b b'. fg b = fg b'" using univ the_elem_eq by (metis (full_types))

(* etc *)

end

有人可能会考虑使用 defines：

locale defined_during =
  fixes f :: "'a ⇒ 'b ⇒ 'c"
    and g :: "'b ⇒ 'a"
    and fg :: "'b ⇒ 'c" 
  defines fg_def: "fg b ≡ f (g b) b"
  assumes "∀a. ∃b. f a b = fg b"
      and univ: "(UNIV::'b set) = {b}"
begin

lemma "∀b b'. fg b = fg b'" using univ the_elem_eq by (metis (full_types))

end

但 locales.pdf 文档似乎表明它已被弃用（但我不确定）：

The grammar is complete with the exception of the context elements constrains and defines, which are provided for backward compatibility.

将 Ctrl 悬停在 fg 上，在语言环境 defined_after 的引理中将其命名为 constant "local.fg"，而在 defined_during 中则为 fixed fg\nfree variable。然而，它确实实现了 defined_after_def 等于 defined_during_def（即后者没有额外的参数或假设），第三个选项没有：

locale extra_defined_during =
  fixes f :: "'a ⇒ 'b ⇒ 'c"
    and g :: "'b ⇒ 'a"
    and fg :: "'b ⇒ 'c" 
  assumes fg_def: "fg b ≡ f (g b) b"
      and "∀a. ∃b. f a b = fg b"
      and univ: "(UNIV::'b set) = {b}"
begin

lemma "∀b b'. fg b = fg b'" using univ the_elem_eq by (metis (full_types))

end

它在引理中的 fg 也具有与 defined_during 语言环境相同的 Ctrl-悬停文本。

也许网站上的某个 PDF 或 NEWS 文件中有关于它的内容，但我找不到任何明显的内容。 isar-ref.pdf发表评论：

Both assumes and defines elements contribute to the locale specification. When defining an operation derived from the parameters, definition (§5.4) is usually more appropriate.

但我不确定如何使用这些信息。大概是说当一个人通过做我所要求的事情没有得到太多时，应该按照语言环境 defined_after 进行（除非引用意味着可以在语言环境定义中使用 definition ），这不是我想要的。（顺便说一句：这句话的第一句话向我暗示 defines 在某种程度上等同于引入额外参数和假设的第三个选项，但事实并非如此。也许理解可能-subtler-than-it-appears-Isabelle-jargon "locale specification" 意味着可以解释是什么导致 Ctrl-悬停文本在第一个选项和第二个选项之间有所不同，我不知道。）

Answer 1

规范元素 defines 确实不是我推荐使用的内容。它可以追溯到 definition 在语言环境上下文中不可用并且所有定义都必须在语言环境声明本身中完成的时代。

如今，解决您的问题的标准方法是将语言环境分为两部分：首先定义一个语言环境 l1，没有复杂的假设，但带有相关参数。（如果您需要一些假设来证明定义的合理性，例如 function 的终止证明，请包括这些假设。）然后像往常一样在 l1 中定义函数 fg。最后，定义扩展 l1 的实际语言环境 l。然后，您可以在 l.

的假设中使用 fg 的定义

locale l = l1 + assumes "... fg ..."

如何在假设的语言环境中使用写在语言环境参数上的定义？

How to use a definition written on locale parameters in the assumptions of the locale?

isabelle

isar