Isabelle/HOL中权利取消的定义

Question

我试图在伊莎贝尔理论中定义函数合成的权利取消的性质，但是有一些错误我无法修正。

我想在Isabelle中具体说明的定义如下：

F:a→B具有右取消性质当且仅当∀C：(∀g，h:B→C)：g◦f=h◦f =⇒g=h

有可能吗？或者更准确地说，是否有可能对一种类型进行量化？

提前感谢

Answer 1

不可能对类型进行显式量化。如果您证明了一个带有类型变量的引理，它将被隐式地证明为该类型的所有实例化。

在某些情况下，您可以使用解决方案，并使用来自AFP条目孔的类型孔。这个类型的V基本上是一个元素太多的类型，其中有一个内射函数(几乎？)每个HOL类型都进入V。因此，在某些情况下，它可以作为一种动态类型来转义类型系统。

theory ...
  imports "ZFC_in_HOL.ZFC_Typeclasses"
begin


definition right_cancellation :: "('a ⇒ 'b) ⇒ bool"  where
  "right_cancellation f ≡ (∀g h :: 'b ⇒ V. g ∘ f = h ∘ f ⟶ g = h)"

在本例中，还可以显示该定义与所使用的类型无关，因此您可以只使用bool。

definition right_cancellation :: "'c itself ⇒ ('a ⇒ 'b) ⇒ bool"  where
  "right_cancellation t f ≡ (∀ g h :: 'b ⇒ 'c. g ∘ f = h ∘ f ⟶ g = h)"

lemma 
  fixes f:: "'x ⇒ 'y"
  assumes as: "a1 ≠ (a2::'a)"
    and r: "right_cancellation (A::'a itself) f"
  shows "right_cancellation (B::'b itself) f"