代码之家 › 专栏 › 技术社区 › Dominique Unruh

如何声明不遵守排序约束的引理(用于使用OFCLASS)

isabelle

1

Dominique Unruh · 技术社区 · 9 年前

如何在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

这个理论定义了一个“可嵌入”的类型类,其中有一个类型参数“嵌入”。(基本上,类embeddable通过显式枚举来表征可数,但我选择这个只是为了有一个非常简单的示例。)

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

首先,我为什么要这样?(在本理论中, apply (rule OFCLASS_I) 与内置功能相同 apply intro_classes 因此是无用的。)在更复杂的情况下,出现这种引理有两个原因:

引理可以给出类型类实例化的替代标准,使后续证明更简单。
引理可用于自动(ML级)实例化。此处使用 intro_classes 是有问题的,因为 intro_类 可以根据先前执行的实例证明而变化。(引理如 类别_I的 具有稳定、控制良好的子目标。)

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

那么,有没有一种清晰的方式来阐述上述理论呢?(我在回答中给出了一个有点难看的解决方案,但我正在寻找更干净的解决方案。)

2 回复 | 直到 9 年前

1

Dominique Unruh 9 年前

排序约束的检查可以在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接受。这种方法适用于更复杂的环境(我已经使用过几次),但我更喜欢更优雅的方法。

2

1

Community CDub 7 年前

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

这个想法是定义一个新常数( embedding_UNCONSTRAINED 在我的示例中),它是原始排序约束常量的副本( embedding ),除非没有排序约束(使用 local_setup 下面的命令)。然后,引理使用 嵌入_不受约束 而不是 嵌入 。但通过添加属性 [unfolded embedding_UNCONSTRAINED_def] 实际存储的引理使用常数 嵌入 没有排序约束。

这种方法的缺点是,在证明引理的过程中,我们永远不能明确地写出任何包含 嵌入 (因为这将添加不需要的排序约束)。但如果我们需要声明一个包含 嵌入 ,我们总是可以使用 嵌入_不受约束 然后使用例如。, unfolding embedding_UNCONSTRAINED 将其转化为 嵌入 .

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