如果对语言环境的参数有一些定义，这将使语言环境的假设更容易编写和/或阅读和/或理解（或者因为函数非常复杂，所以会简化假设的陈述，或者它的名称使假设更易于阅读和理解），定义该函数的最佳方法是什么？
作为一个人为的例子，假设我们想将函数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 文件似乎表明它已被弃用（但我不确定）：
constrains除了上下文元素和之外，语法是完整的defines，它们是为了向后兼容而提供的。
将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它在引理中也具有与语言环境相同的 Ctrl-hover 文本defined_during。
也许网站上的一个 PDF 文件或 NEWS 文件中有一些关于它的内容，但我找不到任何明显的东西。isar-ref.pdf 发表评论：
assumes和元素都defines有助于语言环境规范。当定义从参数派生的操作时，definition（§5.4）通常更合适。
但我不确定如何使用这些信息。大概是说，当一个人通过做我所询问的事情没有获得太多收益时，应该像在语言环境中那样进行defined_after（除非引用意味着可以definition在语言环境定义中使用），这不是我想要的。（顺便说一句：这句话的第一句话会向我暗示这defines在某种程度上等同于第三个选项，它引入了一个额外的参数和假设，但事实并非如此。也许理解什么可能比 - 更微妙it-appears-Isabelle-jargon “语言环境规范”的意思是解释是什么导致 Ctrl-hover 文本在第一个和第二个选项之间有所不同，我不知道。）