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

Question

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

作为一个人为的例子，假设我们想将函数 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

与 defined_during 区域设置一样，在引理中也有相同的 fg 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 在某种程度上等同于引入额外参数和假设的第三个选项，但事实并非如此。也许理解可能比它看起来更微妙的伊莎贝尔行话“语言环境规范”意味着什么会解释是什么导致 Ctrl-悬停文本在第一个选项和第二个选项之间有所不同，我不知道。)

Answer 1

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

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

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