Isabelle中具有类型参数的归纳谓词

Question

我开始学习伊莎贝尔,并想尝试在伊莎贝尔中定义一个幺半群,但不知道如何.

在Coq中,我会做这样的事情:

Inductive monoid (? : Type) (op: ? -> ? -> ?) (i: ?): Prop :=
| axioms: (forall (e: ?), op e i = e) ->
          (forall (e: ?), op i e = e) ->
          monoid ? op i.

我不知道如何在伊莎贝尔做同样的事情.从概念上讲,我想到了这样的事情:

inductive 'a monoid "('a ? 'a ? 'a) ? 'a ? bool" for f i where
  axioms: "?f e i = e; f i e = e? ? monoid f i"

但是,这在Isabelle中无效.

如何在Isabelle中使用类型参数定义归纳谓词？

Answer 1

我对Coq知之甚少,但Isabelle的类型系统非常不同.Isabelle值不采用'类型参数',而Isabelle类型不采用'值参数'.

在Isabelle中,您的示例是一个简单的多态定义,可以这样做:

inductive monoid :: "('a ? 'a ? 'a) ? 'a ? bool" for f i where
  axioms: "?f e i = e; f i e = e? ? monoid f i"

我必须指出,这意味着即使 存在一个e这样的东西,你也有一个幺半群.你可能想写的是

inductive monoid :: "('a ? 'a ? 'a) ? 'a ? bool" for f i where
  axioms: "??e. f e i = e; ?e. f i e = e? ? monoid f i"

在这里,e在假设中普遍量化,这意味着法律必须适用于所有人 e才能构成一个幺半群.

这样做是一种归纳定义,并且具有自动生成适当的引入/消除规则(以及生成更多内容的能力inductive_cases)的优点.但是,还有其他方法.

使用定义

但是,您也可以将其写为一个简单的定义:

definition monoid :: "('a ? 'a ? 'a) ? 'a ? bool" where
  "monoid f i = ((?e. f e i = e) ? (?e. f i e = e))"

这给出了monoid作为引理的定义monoid_def.如果您想要引入/删除规则,则必须自己派生它们.

使用区域设置

第三种也许是最合适的解决方案是语言环境.区域设置是在上下文中保持某些固定变量和假设的方式.下面的示例演示如何将monoid定义为语言环境,在该语言环境中派生lemmas,然后解释具体示例monoid(即列表)的语言环境,并使用我们在语言环境中证明的lemmas.

locale monoid =
  fixes i :: 'a and f :: "'a ? 'a ? 'a"
  assumes left_neutral:  "f i e = e"
      and right_neutral: "f e i = e"
begin
  lemma neutral_unique_left:
    assumes "?e. f i' e = e"
    shows   "i' = i"
  proof-
    from right_neutral have "i' = f i' i" by simp
    also from assms have "f i' i = i" by simp
    finally show "i' = i" .
  qed
end

thm monoid.neutral_unique_left
(* Output: monoid i f ? (?e. f i' e = e) ? i' = i *)

(* Let's interpret our monoid for the type "'a list", with [] 
   as neutral element and concatenation (_ @ _) as the operation. *)
interpretation list_monoid: monoid "[]" "?xs ys. xs @ ys"
  by default simp_all

thm list_monoid.neutral_unique_left
(* Output: (?e. i' @ e = e) ? i' = [] *)

使用类型类

第四种可能性类似于locales类型类.伊莎贝尔支持类型类(像那些在Haskell,尽管更严格的),你可以创建一个monoid类型的类,然后实例它具体类型,如nat,int,'a list,等.

更多信息

有关归纳谓词,语言环境和类型类的更多信息,请参阅这些工具的文档:http://isabelle.in.tum.de/documentation.html