我如何陈述不遵守排序约束的引理（使用 OFCLASS）

Question

如何在 Isabelle/HOL 中声明不符合排序约束的引理？

为了解释为什么这是有道理的，请考虑以下示例理论：

theory Test
imports Main
begin

class embeddable = 
  fixes embedding::"'a ⇒ nat"
  assumes "inj embedding"

lemma OFCLASS_I:
  assumes "inj (embedding::'a⇒_)"
  shows "OFCLASS('a::type,embeddable_class)"
apply intro_classes by (fact assms)

instantiation nat :: embeddable begin
definition "embedding = id"
instance
  apply (rule OFCLASS_I) unfolding embedding_nat_def by simp
end

end

这个理论定义了一个类型 class "embeddable" 和一个类型参数 "embedding"。（基本上，class 可嵌入函数通过显式枚举来表征可数数，但我选择它只是为了提供一个非常简单的示例。）

为了简化类型 class 的实例证明，该理论陈述了一个辅助引理 OFCLASS_I，它显示了 OFCLASS(...,embeddable) 形式的目标。这个引理然后可以用来解决 instance.

产生的证明义务

首先，我为什么要那个？（在目前的理论中，apply (rule OFCLASS_I) 与内置 apply intro_classes 的作用相同，因此是无用的。）在更复杂的情况下，这样的引理有两个原因：

引理可以给出类型实例化的替代标准class，使后续证明更简单。
引理可用于自动化（ML 级）实例化。这里使用 intro_classes 是有问题的，因为 intro_classes 的子目标数量可能会根据之前执行的实例证明而有所不同。（像 OFCLASS_I 这样的引理有一个稳定的、控制良好的子目标。）

然而，上述理论在Isabelle/HOL（无论是2015还是2016-RC1）中都不起作用，因为引理没有类型检查。不满足排序约束 "embedding::(_::embeddable => _)"。但是，这种类型约束不是逻辑必需的（它不是由逻辑内核强制执行的，而是更高级别执行的）。

那么，有没有一种简洁的方式来陈述上述理论？（我在回答中给出了一个有点难看的解决方案，但我正在寻找更清洁的东西。）

Answer 1

可以在 ML-level 上暂时禁用排序约束的检查，然后再重新激活。（请参阅下面的完整示例。）但该解决方案看起来非常像 hack。我们必须在上下文中更改排序约束，并记得在之后恢复它们。

theory Test
imports Main
begin

class embeddable = 
  fixes embedding::"'a ⇒ nat"
  assumes "inj embedding"

ML {*  
  val consts_to_unconstrain = [@{const_name embedding}]
  val consts_orig_constraints = map (Sign.the_const_constraint
                                @{theory}) consts_to_unconstrain
*}
setup {*
  fold (fn c => fn thy => Sign.add_const_constraint (c,NONE) thy) consts_to_unconstrain
*}

lemma OFCLASS_I:
  assumes "inj (embedding::'a⇒_)"
  shows "OFCLASS('a::type,embeddable_class)"
apply intro_classes by (fact assms)

(* Recover stored type constraints *)
setup {*
  fold2 (fn c => fn T => fn thy => Sign.add_const_constraint
            (c,SOME (Logic.unvarifyT_global T)) thy)
              consts_to_unconstrain consts_orig_constraints
*}

instantiation nat :: embeddable begin
definition "embedding = id"
instance
  apply (rule OFCLASS_I) unfolding embedding_nat_def by simp
end

end

这个理论被Isabelle/HOL接受。该方法适用于更复杂的设置（我已经使用过几次），但我更喜欢更优雅的设置。

Answer 2

以下是一个不同的解决方案，在证明引理后不需要 "clean up"（需要 "repair" 之后的排序约束）。

想法是定义一个新常量（在我的示例中为 embedding_UNCONSTRAINED），它是原始排序约束常量（embedding）的副本，除了没有排序约束（使用 local_setup 命令如下）。然后使用 embedding_UNCONSTRAINED 而不是 embedding 来陈述引理。但是通过添加属性 [unfolded embedding_UNCONSTRAINED_def]，实际存储的引理使用常量 embedding，没有排序约束。

这种方法的缺点是在引理的证明过程中，我们永远不能明确地写出任何包含 embedding 的项（因为这会添加不需要的排序约束）。但是，如果我们需要声明一个包含 embedding 的子目标，我们总是可以使用 embedding_UNCONSTRAINED 声明它，然后使用 unfolding embedding_UNCONSTRAINED 将其转换为 embedding.

theory Test
imports Main
begin

class embeddable = 
  fixes embedding::"'a ⇒ nat"
  assumes "inj embedding"

(* This does roughly:
   definition "embedding_UNCONSTRAINED == (embedding::('a::type)=>nat)" *)
local_setup {* 
  Local_Theory.define ((@{binding embedding_UNCONSTRAINED},NoSyn),((@{binding embedding_UNCONSTRAINED_def},[]),
      Const(@{const_name embedding},@{typ "'a ⇒ nat"}))) #> snd
*}

lemma OFCLASS_I [unfolded embedding_UNCONSTRAINED_def]:
  assumes "inj (embedding_UNCONSTRAINED::'a⇒_)"
  shows "OFCLASS('a::type,embeddable_class)"
apply intro_classes by (fact assms[unfolded embedding_UNCONSTRAINED_def])

thm OFCLASS_I (* The theorem now uses "embedding", but without sort "embeddable" *)

instantiation nat :: embeddable begin
definition "embedding = id"
instance
  apply (rule OFCLASS_I) unfolding embedding_nat_def by simp
end

end

我如何陈述不遵守排序约束的引理（使用 OFCLASS）

How do I state a lemma that does not respect sort constraints (for using OFCLASS)

isabelle