什么样的类型定义在本地环境中是合法的？

在伊莎贝尔的NEWS文件，我发现

命令“typedef”现在可以在本地理论上下文中工作——无需 引入对参数或假设的依赖，这不是 可以在 Isabelle/Pure/HOL 中实现。请注意，逻辑环境可能 包含本地 typedef 的多种解释（具有不同的 非空性证明），即使在全球理论背景下也是如此。

（可以追溯到 Isabelle2009-2）。这是有关的最新消息吗typedef和当地的理论背景？此外，“不引入对参数或假设的依赖”的限制实际上意味着什么？

如果这意味着我不能在定义集中使用语言环境参数typedef，那么我就不会考虑typedef完全本地化（因为唯一允许的实例可以轻松地移动到本地上下文之外，或者我错过了什么？）。

是否（或者应该，或者是否可能）可以沿着线做一些事情（其中集合用于typedef取决于语言环境参数V):

datatype ('a, 'b) "term" = Var 'b | Fun 'a "('a, 'b) term list"

locale term_algebra =
  fixes F :: "'a set"
    and V :: "'b set"
begin

definition "domain α = {x : V. α x ~= Var x}"

typedef ('a, 'b) subst =
  "{α :: 'b => ('a, 'b) term. finite (domain α)}"

end

我目前获得的：

Locally fixed type arguments "'a", "'b" in type declaration "subst"

对此还有一些注意事项：

• 本地理论基础设施仅仅组织现有的模块概念（locale, class等）使得定义机制（definition, theorem, inductive, function等）可以在各种环境下统一工作。这不会改变逻辑基础，因此规范元素不能依赖于术语参数（fixes）或处所（assumes）不会从根本上变得更好。它们只是被改装成更大的框架，这已经是一个超逻辑的好处。

• 典型的局部理论目标是locale及其衍生品如class。这些在根据上面概述的原理的逻辑中工作：通过某些上下文进行 lambda 提升fixes and assumes。其他更雄心勃勃的目标是可以想象的，但需要一些勇敢的英雄人物来实现。例如，可以将AWE理论解释机制作为另一个本地理论目标，然后获得类型/常量/公理的参数化——通常的代价是通过显式证明项以在 LCF 证明者中实现可接受的推论（或者以放弃 LCF 为代价） ness 并通过一些预言机来完成）。

• Plain typedef如上所示（及其衍生物，如本地化codatatype and datatype最近的 HOL-BNF）的依赖类型参数可能会略有改善，但这意味着一些实现工作并不能证明目前的微薄结果是合理的。它只允许使用隐式参数编写多态类型构造，如下所示：

  context fixes type 'a
  begin
  datatype list = Nil | Cons 'a list
  end
  

  导出后你会得到'a list照常。

  进一步的复杂化：fixes type 'a不存在。 Isabelle/Pure 通过 Hindley-Milner 隐式处理类型参数。