Isabelle 中带有类型参数的归纳谓词
Inductive predicate with type parameters in Isabelle
我开始学习 Isabelle 并想尝试在 Isabelle 中定义一个幺半群，但不知道如何。
在 Coq 中，我会做这样的事情：
Inductive monoid (τ : Type) (op: τ -> τ -> τ) (i: τ): Prop :=
| axioms: (forall (e: τ), op e i = e) ->
(forall (e: τ), op i e = e) ->
monoid τ op i.
我不确定如何在 Isabelle 中做同样的事情。从概念上讲，我想到了这样的事情：
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 中定义带类型参数的归纳谓词？
我对 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成立才能构成幺半群。
作为归纳定义这样做是可能的，并且具有自动生成适当的 introduction/elimination 规则的优势（以及使用 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 的定义。如果你想要 introduction/elimination 规则，你必须自己推导它们。
使用语言环境
第三个，可能也是最合适的解决方案是 locales。语言环境是一种将某些固定变量和假设保留在上下文中并在此上下文中进行推理的方法。以下示例演示如何将幺半群定义为语言环境，在该语言环境中派生引理，然后为具体示例幺半群（即列表）解释语言环境，并使用我们在语言环境中为它们证明的引理。
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' = [] *)
使用类型class
第四种可能性与语言环境相似，类型为classes。 Isabelle 支持 classes 类型（与 Haskell 中的那些一样，尽管限制性更强），您可以创建 monoid 类型 class，然后将其实例化为具体类型，例如 nat、int、'a list 等
更多信息
有关归纳谓词、语言环境和类型 classes 的更多信息，请参阅这些工具的文档：http://isabelle.in.tum.de/documentation.html
我开始学习 Isabelle 并想尝试在 Isabelle 中定义一个幺半群，但不知道如何。
在 Coq 中，我会做这样的事情：
Inductive monoid (τ : Type) (op: τ -> τ -> τ) (i: τ): Prop :=
| axioms: (forall (e: τ), op e i = e) ->
(forall (e: τ), op i e = e) ->
monoid τ op i.
我不确定如何在 Isabelle 中做同样的事情。从概念上讲，我想到了这样的事情：
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 中定义带类型参数的归纳谓词？
我对 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成立才能构成幺半群。
作为归纳定义这样做是可能的，并且具有自动生成适当的 introduction/elimination 规则的优势（以及使用 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 的定义。如果你想要 introduction/elimination 规则，你必须自己推导它们。
使用语言环境
第三个，可能也是最合适的解决方案是 locales。语言环境是一种将某些固定变量和假设保留在上下文中并在此上下文中进行推理的方法。以下示例演示如何将幺半群定义为语言环境，在该语言环境中派生引理，然后为具体示例幺半群（即列表）解释语言环境，并使用我们在语言环境中为它们证明的引理。
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' = [] *)
使用类型class
第四种可能性与语言环境相似，类型为classes。 Isabelle 支持 classes 类型（与 Haskell 中的那些一样，尽管限制性更强），您可以创建 monoid 类型 class，然后将其实例化为具体类型，例如 nat、int、'a list 等
更多信息
有关归纳谓词、语言环境和类型 classes 的更多信息，请参阅这些工具的文档：http://isabelle.in.tum.de/documentation.html