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

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

  •  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
  •  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