如何声明一个不尊重排序约束的引理（使用OFCLASS）

问题描述：

我该如何声明Isabelle/HOL中不遵守排序约束的引理？如何声明一个不尊重排序约束的引理（使用OFCLASS）

要解释为什么这是有道理的，请看下面的例子理论：

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

这种理论定义了一个类型的类“嵌入”用一个类型参数“嵌入”。（基本上，可嵌入类通过明确枚举来表征可数数字，但我选择这只是一个非常简单的例子。）

为了简化类型类的实例验证，理论指出了一个辅助引理OFCLASS_I，它显示目标的形式OFCLASS(...,embeddable)。这个引理可以用来解决instance产生的证明义务。

首先，我为什么要这么做？（在本理论，apply (rule OFCLASS_I)确实相同内建apply intro_classes，因此是无用的。）在更复杂的情况下，有两个原因这样的引理：

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

然而，上述理论没有在伊莎贝尔/ HOL（均未2015或2016-RC1）工作，因为引理不类型检查。排序约束“embedding ::（_ :: embeddable => _）”不满足。然而，这种类型的限制并不是逻辑必然性（它不是由逻辑内核强制执行，而是由更高级别执行）。

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

答

以下是一个不同的解决方案，在证明引理之后不需要“清理”（this answer需要“修复”之后的排序约束）。

的思想是定义一个新的常数（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

答

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

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接受。该方法在更复杂的设置中工作（我已经使用过几次），但我更喜欢更优雅的设置。

如何声明一个不尊重排序约束的引理（使用OFCLASS）

相关推荐